Syntax.Abstract: implement eval

fogti

Aug 26, 2024, 5:27 PM

QXX6KTFXDUOBY3WATDAZ4XIRLHSRKXLSDQSSD7OP7CDLRUHGJELAC

Dependencies

• [2] JDF4JUMS some attempts at abstract syntax
• [3] HQ2ZYTX5 add comment lexing and remove references stuff

Change contents

• replacement in core/lib/GardGround/Syntax/Abstract.hs at line 4
  [2.105]→[2.105:154](∅→∅)
  − NeutralRoot,

  − Neutral,

  − ValueError,

  − Value,
  [2.105]

  [2.154]
  + NeutralRoot(..),

  + Neutral(..),

  + ValueError(..),

  + Value(..),

  + Expr(..),
• edit in core/lib/GardGround/Syntax/Abstract.hs at line 11
  [2.171]

  [2.171]
  + eval,
• replacement in core/lib/GardGround/Syntax/Abstract.hs at line 19
  [2.310]→[2.310:353](∅→∅)
  − import GardGround.Syntax.Literal (Literal)
  [2.310]

  [2.353]
  + import GardGround.Syntax.Literal (Literal, lookupBinder)
• edit in core/lib/GardGround/Syntax/Abstract.hs at line 44
  [2.1085]

  [2.1085]
  + | VEOutOfRangeLocal Natural
• edit in core/lib/GardGround/Syntax/Abstract.hs at line 55
  [2.1539]

  [2.1539]
  + -- | Apply a value to a value
• edit in core/lib/GardGround/Syntax/Abstract.hs at line 71
  [2.2068]

  [2.2110]
  + | EAnnot Expr Expr
• edit in core/lib/GardGround/Syntax/Abstract.hs at line 97
  [2.2837]
  +

  + 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