NeutralRoot,
  Neutral,
  ValueError,
  Value,

  NeutralRoot(..),
  Neutral(..),
  ValueError(..),
  Value(..),
  Expr(..),

  eval,

import GardGround.Syntax.Literal (Literal)

import GardGround.Syntax.Literal (Literal, lookupBinder)

  | VEOutOfRangeLocal Natural

-- | Apply a value to a value

  | EAnnot Expr Expr

eval :: Expr -> [Value] -> EvalResult
eval kind env = case kind of
  ENeutralRoot (Local x) -> case lookupBinder env x of
    Nothing -> Left . VEOutOfRangeLocal $ x - (toEnum $ length env)
    Just y -> Right y
  ENeutralRoot x -> Right $ VNeutral (Neutral x mempty)
  EAnnot e _ -> eval e env
  EApply e e' -> do
    v  <- eval e  env
    v' <- eval e' env
    vapp v v'
  ELam e -> Right . VLam $ \y -> eval e (y:env)
  EPi arg e -> fmap (\res -> VPi res $ \y -> eval e (y:env)) $ eval arg env