Add builtin arithmetic operators

* also allow choosing evaluator
* ensures equivalence of evaluators up-to α-renaming
* checks server accepts answers from challenge

1 files changed, 27 insertions, 8 deletions

diff --git a/lambda-calcul/haskell/src/Minilang/Lambda.hs b/lambda-calcul/haskell/src/Minilang/Lambda.hs
index ff636ce..fbaf35d 100644
--- a/lambda-calcul/haskell/src/Minilang/Lambda.hs
+++ b/lambda-calcul/haskell/src/Minilang/Lambda.hs
@@ -1,24 +1,26 @@
 module Minilang.Lambda where
 
 import Data.Bifunctor (second)
-import Minilang.Lambda.DeBruijn (eval, eval', fromDeBruijn, toDeBruijn)
-import Minilang.Lambda.Eval (Env, Term)
+import Minilang.Lambda.DeBruijn (builtinDeBruijnEnv, eval', fromDeBruijn, toDeBruijn)
+import Minilang.Lambda.Eval (Env, Term, builtinEnvValue)
+import qualified Minilang.Lambda.Eval as Eval
 import Minilang.Lambda.Infer (Context, TypeError, extendContext, infer)
 import Minilang.Lambda.Parser (AST (..), desugar)
 import Minilang.Lambda.Unify (Type (..))
-import Minilang.REPL.Types (Language (..))
+import Minilang.REPL.Types (Evaluator (..), Language (..))
 
 -- | Top-level evaluator
 -- Load a list of expressions into given `Env` and `Context`, returning an extended
 -- `Env` and `Context` with declarations bound and the list of evaluated top-level
 -- terms along with their types.
 loadProgram ::
+  Evaluator ->
   Language ->
   Env ->
   Context ->
   [AST] ->
   Either TypeError ([(Term, Type)], Env, Context)
-loadProgram language env context exprs =
+loadProgram evaluator language env context exprs =
   fmap (\(res, e, c) -> (reverse res, e, c)) result
   where
     result =
@@ -38,7 +40,7 @@ loadProgram language env context exprs =
         exprs
 
     runExpr language (Def ident body) env context =
-      let term = evalInEnv env body
+      let term = evalInEnvWith evaluator env body
        in case language of
             Typed ->
               case infer term of
@@ -48,7 +50,7 @@ loadProgram language env context exprs =
             Untyped ->
               Right (Nothing, (ident, term) : env, context)
     runExpr language expr env context =
-      let v = evalInEnv env expr
+      let v = evalInEnvWith evaluator env expr
        in case language of
             Typed ->
               case infer v of
@@ -58,8 +60,25 @@ loadProgram language env context exprs =
             Untyped ->
               Right (Just (v, TyVar "<?>"), env, context)
 
+-- | Evaluate an 'AST' in the given 'Env' using the De Bruijn CBV evaluator.
+-- This is the default evaluator used by the server and REPL.
 evalInEnv :: Env -> AST -> Term
-evalInEnv env expr =
+evalInEnv = evalInEnvWith DeBruijn
+
+-- | Evaluate an 'AST' using the selected 'Evaluator'.
+evalInEnvWith :: Evaluator -> Env -> AST -> Term
+evalInEnvWith DeBruijn env expr =
   let term = desugar expr
-      env' = second toDeBruijn <$> env
+      -- User-defined bindings take precedence over builtins (rightmost wins
+      -- in a left-to-right lookup, so put user env first).
+      env' = (second toDeBruijn <$> env) ++ builtinDeBruijnEnv
    in fromDeBruijn $ eval' env' (toDeBruijn term)
+evalInEnvWith NbE env expr =
+  let term  = desugar expr
+      -- Build an EnvValue from the user Env by evaluating each binding's
+      -- Term in the accumulated value env (builtins always available at the
+      -- bottom).  foldl builds left-to-right so earlier bindings are visible
+      -- when evaluating later ones.
+      envV  = foldl addBinding builtinEnvValue env
+      addBinding acc (name, t) = (name, Eval.eval acc t) : acc
+   in Eval.readBack (Eval.eval envV term)