Add builtin arithmetic operators

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

8 files changed, 293 insertions, 70 deletions

diff --git a/lambda-calcul/haskell/src/Minilang/App.hs b/lambda-calcul/haskell/src/Minilang/App.hs
index 3373b75..0174547 100644
--- a/lambda-calcul/haskell/src/Minilang/App.hs
+++ b/lambda-calcul/haskell/src/Minilang/App.hs
@@ -20,9 +20,9 @@ import Data.Text.Encoding (decodeUtf8, encodeUtf8)
 import Data.Time (getCurrentTime)
 import Minilang.API (Challenge (..), LambdaAPI, Score (..), Token (..), User (..), newToken)
 import Minilang.Lambda.Parser (pretty)
-import Minilang.REPL (withInputs)
+import Minilang.REPL (withInputs, replEnvWith)
 import Minilang.REPL.Purer (PurerEnv (..))
-import Minilang.REPL.Types (Command (..), Content (..), In (..), Out (..), initialREPL)
+import Minilang.REPL.Types (Command (..), Content (..), Evaluator (..), In (..), Out (..), initialREPL)
 import Network.Wai.Application.Static (defaultFileServerSettings, staticApp)
 import Servant (ServerT, err400, err500, errBody, (:<|>) (..), err404)
 import Servant.Server (Application, Handler (..), Tagged (..))
@@ -31,15 +31,17 @@ import System.Random (StdGen)
 data Env = Env
   { gen :: TVar StdGen,
     users :: TVar (Map Token Score),
-    challenges :: [Challenge]
+    challenges :: [Challenge],
+    evaluator :: Evaluator
   }
 
-makeEnv :: StdGen -> [Challenge] -> IO Env
-makeEnv gen challenges =
+makeEnv :: StdGen -> [Challenge] -> Evaluator -> IO Env
+makeEnv gen challenges ev =
   Env
     <$> newTVarIO gen
     <*> newTVarIO mempty
     <*> pure challenges
+    <*> pure ev
 
 newtype AppM a = AppM {runAppM :: ReaderT Env IO a}
   deriving newtype (Functor, Applicative, Monad, MonadIO, MonadReader Env)
@@ -147,7 +149,8 @@ postAnswer Nothing _ = liftIO $ throwM $ err400 {errBody = "Missing token"}
 postAnswer (Just token) expected = do
   checkUserToken token
   Challenge {expr} <- getCurrentChallenge token
-  let PurerEnv {outputs} = withInputs initialREPL [Com (Load (Data expr))]
+  ev <- asks evaluator
+  let PurerEnv {outputs} = withInputs (replEnvWith ev) [Com (Load (Data expr))]
       result = evaluateOutputs outputs expected
   updateUserLastTest token result
   case result of
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)
diff --git a/lambda-calcul/haskell/src/Minilang/Lambda/DeBruijn.hs b/lambda-calcul/haskell/src/Minilang/Lambda/DeBruijn.hs
index 1e85ca6..1d2f9e8 100644
--- a/lambda-calcul/haskell/src/Minilang/Lambda/DeBruijn.hs
+++ b/lambda-calcul/haskell/src/Minilang/Lambda/DeBruijn.hs
@@ -3,6 +3,7 @@
 module Minilang.Lambda.DeBruijn where
 
 import Data.List (elemIndex)
+import qualified Data.Map.Strict as Map
 import Data.Text (Text)
 import qualified Data.Text
 import Minilang.Lambda.Eval (Term)
@@ -11,6 +12,7 @@ import qualified Minilang.Lambda.Eval as Eval
 data DeBruijn ann
   = FV Text
   | FNum Int
+  | FBuiltin Text          -- ^ a fully-applied or partial built-in operator
   | Var ann Int
   | Lam ann (DeBruijn ann)
   | App (DeBruijn ann) (DeBruijn ann)
@@ -21,13 +23,21 @@ type Env ann = [(Text, DeBruijn ann)]
 newEnv :: Env ann
 newEnv = []
 
+-- | An environment pre-seeded with every built-in operator name.
+-- Each entry maps the name to an 'FBuiltin' node so that 'eval\'' can
+-- recognise and reduce applications of those names.
+builtinDeBruijnEnv :: Env ann
+builtinDeBruijnEnv =
+  map (\name -> (name, FBuiltin name)) (Map.keys Eval.builtinArity)
+
 fromDeBruijn :: DeBruijn Text -> Term
 fromDeBruijn = \case
-  FV x -> Eval.Var x
-  FNum n -> Eval.Num n
-  Var s _ -> Eval.Var s
-  Lam s body -> Eval.Lam s (fromDeBruijn body)
-  App f a -> Eval.App (fromDeBruijn f) (fromDeBruijn a)
+  FV x        -> Eval.Var x
+  FNum n      -> Eval.Num n
+  FBuiltin b  -> Eval.Var b        -- reads back as a Var; eval recognises it
+  Var s _     -> Eval.Var s
+  Lam s body  -> Eval.Lam s (fromDeBruijn body)
+  App f a     -> Eval.App (fromDeBruijn f) (fromDeBruijn a)
 
 -- Convert a term with named variables to De Bruijn indices
 toDeBruijn :: Term -> DeBruijn Text
@@ -36,7 +46,7 @@ toDeBruijn term = go term []
     go (Eval.Var x) env =
       case elemIndex x env of
         Just idx -> Var x idx
-        Nothing -> FV x
+        Nothing  -> FV x
     go (Eval.Lam x body) env =
       Lam x (go body (x : env))
     go (Eval.App f a) env =
@@ -48,40 +58,119 @@ eval :: DeBruijn ann -> DeBruijn ann
 eval (App f a) =
   case eval f of
     Lam _ body -> eval (substitute [] 0 a body)
-    f' -> App f' a
+    f'         -> App f' a
 eval term = term
 
-eval' :: (Show ann, Eq ann) => Env ann -> DeBruijn ann -> DeBruijn ann
-eval' env (FV v) = case lookup v env of
-  Just term -> term
-  Nothing -> FV v
-eval' env (App f a) =
-  case eval' env f of
-    Lam _ body -> eval' env (substitute env 0 a body)
-    f' -> if f' /= f
-          then eval' env $ App f' a
-          else App f' a
-eval' _ term = term
+eval' :: Env Text -> DeBruijn Text -> DeBruijn Text
+eval' env = \case
+  FV v -> case lookup v env of
+    Just term -> term
+    Nothing   -> FV v
+  FBuiltin b -> FBuiltin b
+  App f a ->
+    let f' = eval' env f
+        a' = eval' env a
+    in case f' of
+      -- Beta-reduction
+      Lam _ body -> eval' env (substitute env 0 a' body)
+      -- Built-in: collect arguments and reduce when saturated
+      FBuiltin b -> evalBuiltin env b [a']
+      -- Left-spine is itself a partial builtin application
+      App g arg ->
+        case collectBuiltin (App g arg) of
+          Just (b, accumulated) -> evalBuiltin env b (accumulated ++ [a'])
+          Nothing ->
+            let applied = App f' a'
+            in if applied /= App f a
+               then eval' env applied
+               else applied
+      f'' ->
+        let applied = App f'' a'
+        in if applied /= App f a
+           then eval' env applied
+           else applied
+  term -> term
+
+-- | Walk a left-spine of 'App' nodes and check whether the root is an
+-- 'FBuiltin'.  If so, return the builtin name and the already-accumulated
+-- arguments (left-to-right order).
+collectBuiltin :: DeBruijn Text -> Maybe (Text, [DeBruijn Text])
+collectBuiltin = go []
+  where
+    go acc (App f arg) = go (arg : acc) f
+    go acc (FBuiltin b) = Just (b, acc)
+    go _ _ = Nothing
+
+-- | Attempt to reduce a built-in application once all required arguments
+-- are present.  Falls back to a neutral 'App' spine when the arity has not
+-- been reached yet or when the arguments are not integer literals.
+evalBuiltin :: Env Text -> Text -> [DeBruijn Text] -> DeBruijn Text
+evalBuiltin env b args =
+  case Map.lookup b Eval.builtinArity of
+    Nothing -> rebuild (FBuiltin b) args   -- unknown builtin; leave as-is
+    Just ar
+      | length args < ar ->
+          -- Still partial: return the spine as-is for now
+          rebuild (FBuiltin b) args
+      | length args == ar ->
+          case tryReduce b args of
+            Just result -> result
+            Nothing     -> rebuild (FBuiltin b) args
+      | otherwise ->
+          -- Over-applied: reduce with exactly `ar` args then apply the rest
+          let (sat, extra) = splitAt ar args
+          in case tryReduce b sat of
+               Just reduced -> foldl (\acc x -> eval' env (App acc x)) reduced extra
+               Nothing      -> rebuild (FBuiltin b) args
+
+-- | Church-encoded True as a DeBruijn term: lam f -> lam t -> t
+churchTrue :: DeBruijn Text
+churchTrue  = Lam "f" (Lam "t" (Var "t" 0))
+
+-- | Church-encoded False as a DeBruijn term: lam f -> lam t -> f
+churchFalse :: DeBruijn Text
+churchFalse = Lam "f" (Lam "t" (Var "f" 1))
+
+-- | Attempt a numeric reduction.  Returns 'Nothing' when either argument is
+-- not an 'FNum' (e.g. it is still a free variable).
+-- Comparison operators return Church booleans rather than integer flags.
+tryReduce :: Text -> [DeBruijn Text] -> Maybe (DeBruijn Text)
+tryReduce name args = case (name, args) of
+  ("+",   [FNum x, FNum y]) -> Just $ FNum (x + y)
+  ("-",   [FNum x, FNum y]) -> Just $ FNum (x - y)
+  ("*",   [FNum x, FNum y]) -> Just $ FNum (x * y)
+  ("div", [FNum x, FNum y]) | y /= 0 -> Just $ FNum (x `div` y)
+  ("mod", [FNum x, FNum y]) | y /= 0 -> Just $ FNum (x `mod` y)
+  ("=",   [FNum x, FNum y]) -> Just $ if x == y then churchTrue else churchFalse
+  ("<",   [FNum x, FNum y]) -> Just $ if x <  y then churchTrue else churchFalse
+  ("neg", [FNum x])         -> Just $ FNum (negate x)
+  _                         -> Nothing
+
+-- | Rebuild a left-spine application from a head and a list of arguments.
+rebuild :: DeBruijn Text -> [DeBruijn Text] -> DeBruijn Text
+rebuild = foldl App
 
 substitute :: Env ann -> Int -> DeBruijn ann -> DeBruijn ann -> DeBruijn ann
 substitute env n arg term = case term of
   FV x -> case lookup x env of
-    Just term -> term
+    Just t  -> t
     Nothing -> FV x
-  FNum _ -> term
+  FNum _     -> term
+  FBuiltin _ -> term
   Var t x
-    | x == n -> arg
+    | x == n    -> arg
     | otherwise -> Var t x
-  Lam x body -> Lam x (substitute env (n + 1) arg body)
-  App f a -> App (substitute env n arg f) (substitute env n arg a)
+  Lam x body  -> Lam x (substitute env (n + 1) arg body)
+  App f a     -> App (substitute env n arg f) (substitute env n arg a)
 
 pretty :: DeBruijn Text -> Text
 pretty = \case
-  FV x -> x
-  FNum n -> showNum n
-  Var s _ -> s
+  FV x       -> x
+  FNum n     -> showNum n
+  FBuiltin b -> b
+  Var s _    -> s
   Lam s body -> "(lam (" <> s <> ") " <> pretty body <> ")"
-  App f a -> "(" <> pretty f <> " " <> pretty a <> ")"
+  App f a    -> "(" <> pretty f <> " " <> pretty a <> ")"
 
 -- | Render an integer, using no space between '-' and digits for negative numbers.
 showNum :: Int -> Text
diff --git a/lambda-calcul/haskell/src/Minilang/Lambda/Eval.hs b/lambda-calcul/haskell/src/Minilang/Lambda/Eval.hs
index 650c4bd..324c881 100644
--- a/lambda-calcul/haskell/src/Minilang/Lambda/Eval.hs
+++ b/lambda-calcul/haskell/src/Minilang/Lambda/Eval.hs
@@ -4,6 +4,8 @@
 module Minilang.Lambda.Eval where
 
 import Data.Aeson (FromJSON, ToJSON)
+import Data.Map.Strict (Map)
+import qualified Data.Map.Strict as Map
 import Data.String (IsString (..))
 import Data.Text (Text, pack)
 import GHC.Generics (Generic)
@@ -18,7 +20,14 @@ data Term
 instance IsString Term where
   fromString = Var . pack
 
-data Value = Clos EnvValue Text Term | VNeut Neutral | VNum Int
+-- | A built-in arithmetic operator value.
+-- Carries its name, the number of arguments still needed, and the
+-- already-accumulated argument values (in order of application).
+data Value
+  = Clos EnvValue Text Term
+  | VNeut Neutral
+  | VNum Int
+  | Builtin Text Int [Value]
   deriving (Show, Read, Eq)
 
 data Neutral = NVar Text | NNum Int | NApp Neutral Value
@@ -31,15 +40,36 @@ type EnvValue = [(Text, Value)]
 newEnv :: Env
 newEnv = []
 
+-- | Arity table for every built-in operator.
+builtinArity :: Map Text Int
+builtinArity = Map.fromList
+  [ ("+",   2)
+  , ("-",   2)
+  , ("*",   2)
+  , ("div", 2)
+  , ("mod", 2)
+  , ("=",   2)
+  , ("<",   2)
+  , ("neg", 1)
+  ]
+
+-- | The set of built-in names, for fast membership testing.
+builtinNames :: Map Text Value
+builtinNames = Map.mapWithKey (\name ar -> Builtin name ar []) builtinArity
+
 normalise :: Term -> Term
-normalise term = readBack (eval [] term)
+normalise term = readBack (eval builtinEnvValue term)
+
+-- | An 'EnvValue' pre-seeded with all built-in operators.
+builtinEnvValue :: EnvValue
+builtinEnvValue = Map.toList builtinNames
 
 -- call-by-value evaluator
 -- from https://davidchristiansen.dk/tutorials/nbe/#%28part._untyped-eval%29
 eval :: EnvValue -> Term -> Value
 eval env = \case
   Var x -> case lookup x env of
-    Just term -> term
+    Just v  -> v
     Nothing -> VNeut (NVar x)
   Lam x body -> Clos env x body
   App f a ->
@@ -55,21 +85,59 @@ apply f a =
       let env' = (x, a) : closureEnv
        in eval env' body
     VNeut f' -> VNeut (NApp f' a)
-    VNum n -> VNeut (NApp (NNum n) a)
+    VNum n   -> VNeut (NApp (NNum n) a)
+    -- Last argument arrives: dispatch and reduce.
+    Builtin name 1 args -> dispatchBuiltin name (args ++ [a])
+    -- Still waiting for more arguments: accumulate.
+    Builtin name ar args -> Builtin name (ar - 1) (args ++ [a])
+
+-- | Church-encoded True: lam f t -> t
+churchTrue :: Value
+churchTrue = Clos builtinEnvValue "f" (Lam "t" (Var "t"))
+
+-- | Church-encoded False: lam f t -> f
+churchFalse :: Value
+churchFalse = Clos builtinEnvValue "f" (Lam "t" (Var "f"))
+
+-- | Reduce a fully-saturated built-in application.
+-- If the arguments are not both integers (free variables in function
+-- position), fall back to a stuck neutral term.
+-- Comparison operators (= and <) return Church booleans rather than integers.
+dispatchBuiltin :: Text -> [Value] -> Value
+dispatchBuiltin name args = case (name, args) of
+  ("+",   [VNum x, VNum y]) -> VNum (x + y)
+  ("-",   [VNum x, VNum y]) -> VNum (x - y)
+  ("*",   [VNum x, VNum y]) -> VNum (x * y)
+  ("div", [VNum x, VNum y])
+    | y /= 0   -> VNum (x `div` y)
+  ("mod", [VNum x, VNum y])
+    | y /= 0   -> VNum (x `mod` y)
+  ("=",   [VNum x, VNum y]) -> if x == y then churchTrue else churchFalse
+  ("<",   [VNum x, VNum y]) -> if x <  y then churchTrue else churchFalse
+  ("neg", [VNum x])         -> VNum (negate x)
+  -- Stuck: reconstruct a neutral application chain rooted at the builtin name.
+  _ -> foldl (\acc v -> VNeut (NApp (neutralOf acc) v)) (VNeut (NVar name)) args
+  where
+    neutralOf (VNeut n) = n
+    neutralOf v         = NApp (NVar name) v   -- shouldn't happen in practice
 
 readBack :: Value -> Term
 readBack = go []
   where
     go names = \case
       Clos env x body ->
-        let name = freshName x names
+        let name  = freshName x names
             names' = name : names
-            val' = eval ((x, VNeut (NVar name)) : env) body
+            val'  = eval ((x, VNeut (NVar name)) : env) body
          in Lam name (go names' val')
-      VNeut (NVar n) -> Var n
-      VNeut (NNum n) -> Num n
-      VNeut (NApp f a) -> App (go names (VNeut f)) (go names a)
-      VNum n -> Num n
+      VNeut (NVar n)    -> Var n
+      VNeut (NNum n)    -> Num n
+      VNeut (NApp f a)  -> App (go names (VNeut f)) (go names a)
+      VNum n            -> Num n
+      -- A partial builtin reads back as a chain of applications rooted at
+      -- the builtin name, e.g. Builtin "+" 1 [VNum 3]  →  App (Var "+") (Num 3)
+      Builtin bname _ accumulated ->
+        foldl (\acc v -> App acc (go names v)) (Var bname) accumulated
 
 freshName :: Text -> [Text] -> Text
 freshName x names
diff --git a/lambda-calcul/haskell/src/Minilang/REPL.hs b/lambda-calcul/haskell/src/Minilang/REPL.hs
index a8d3c77..7da2042 100644
--- a/lambda-calcul/haskell/src/Minilang/REPL.hs
+++ b/lambda-calcul/haskell/src/Minilang/REPL.hs
@@ -23,6 +23,8 @@ import Minilang.REPL.Pure
 import Minilang.REPL.Purer
 import Minilang.REPL.Run
 import Minilang.REPL.Types
+import System.Environment (lookupEnv)
+import Text.Read (readMaybe)
 import System.Console.Haskeline
   ( defaultBehavior,
     defaultSettings,
@@ -30,13 +32,32 @@ import System.Console.Haskeline
     runInputTBehavior,
     setComplete,
   )
-import System.IO (Handle)
+import System.IO (Handle, stderr)
+
+-- | Read the evaluator selection from the @MINILANG_EVAL@ environment variable.
+-- Returns 'DeBruijn' when the variable is absent or unrecognised.
+evaluatorFromEnv :: IO Evaluator
+evaluatorFromEnv =
+  lookupEnv "MINILANG_EVAL" >>= \case
+    Nothing  -> pure DeBruijn
+    Just raw -> case readMaybe raw of
+      Just ev -> pure ev
+      Nothing -> do
+        Text.hPutStrLn stderr $
+          "Warning: unknown MINILANG_EVAL value " <> Text.pack (show raw)
+          <> ", falling back to DeBruijn"
+        pure DeBruijn
+
+-- | Build the initial 'REPLEnv' using the given 'Evaluator'.
+replEnvWith :: Evaluator -> REPLEnv
+replEnvWith ev = initialREPL { evaluator = ev }
 
 -- * Haskeline REPL
 
-withTerminal :: IO ()
-withTerminal =
-  runInputTBehavior defaultBehavior settings $ evalStateT (runHaskeline runREPL) initialREPL
+withTerminal :: Evaluator -> IO ()
+withTerminal ev =
+  runInputTBehavior defaultBehavior settings $
+    evalStateT (runHaskeline runREPL) (replEnvWith ev)
   where
     settings = setComplete completion $ defaultSettings {historyFile = Just "~/.minilang.history"}
 
@@ -50,12 +71,12 @@ withHandles hin hout =
   evalStateT (runConsole runREPL) (IOEnv hin hout initialREPL)
 
 -- | Simple IO REPL, used to evaluate programs from stdin or file loading
-withIO :: Handle -> Handle -> IO ()
-withIO hin hout = do
+withIO :: Evaluator -> Handle -> Handle -> IO ()
+withIO ev hin hout = do
   programText <- parseProgram <$> Text.hGetContents hin
   case programText of
     Left err -> Text.hPutStrLn hout (Text.pack (show err))
-    Right prog -> case loadProgram Untyped newEnv newContext prog of
+    Right prog -> case loadProgram ev Untyped newEnv newContext prog of
       Right (results, _, _) -> mapM_ (Text.hPutStrLn hout . render) results
       Left err -> Text.hPutStrLn hout (Text.pack $ show err)
   where
diff --git a/lambda-calcul/haskell/src/Minilang/REPL/Run.hs b/lambda-calcul/haskell/src/Minilang/REPL/Run.hs
index 8b9b844..26f3cad 100644
--- a/lambda-calcul/haskell/src/Minilang/REPL/Run.hs
+++ b/lambda-calcul/haskell/src/Minilang/REPL/Run.hs
@@ -8,7 +8,7 @@ module Minilang.REPL.Run where
 
 import Control.Monad.Catch
 import Data.Text hiding (replicate)
-import Minilang.Lambda (loadProgram, evalInEnv)
+import Minilang.Lambda (loadProgram, evalInEnvWith)
 import Minilang.Lambda.Eval (newEnv)
 import Minilang.Lambda.Infer (extendContext, infer, newContext)
 import qualified Minilang.Lambda.Infer as Infer
@@ -34,11 +34,11 @@ handleUserInput ::
   Text ->
   m ()
 handleUserInput txt = do
-  repl@REPLEnv {language, env, context} <- getEnv
+  repl@REPLEnv {language, evaluator, env, context} <- getEnv
   case parse txt of
     Left err -> output (Msg $ pack $ show err)
     Right (Def ident body) -> do
-      let v = evalInEnv env body
+      let v = evalInEnvWith evaluator env body
       case language of
         Typed ->
           case infer v of
@@ -54,7 +54,7 @@ handleUserInput txt = do
           setEnv $ repl {env = (ident, v) : env}
           output (Defined ident (TyVar "<?>"))
     Right expr -> do
-      let v = evalInEnv env expr
+      let v = evalInEnvWith evaluator env expr
           ast = resugar v
       case language of
         Typed ->
@@ -86,6 +86,10 @@ handleCommand (Set (SelectLanguage lang)) =
   getEnv >>= \e ->
     setEnv (e {language = lang})
       >> output (Msg $ "Language set to " <> pack (show lang))
+handleCommand (Set (SelectEvaluator ev)) =
+  getEnv >>= \e ->
+    setEnv (e {evaluator = ev})
+      >> output (Msg $ "Evaluator set to " <> pack (show ev))
 handleCommand Help =
   output (Msg helpText)
 
@@ -94,11 +98,11 @@ loadProgramInEnv ::
   Text ->
   m ()
 loadProgramInEnv prog = do
-  repl@REPLEnv {env, context, language} <- getEnv
+  repl@REPLEnv {env, context, language, evaluator} <- getEnv
   case parseProgram prog of
     Left err -> output (Msg $ pack $ show err)
     Right exprs -> do
-      case loadProgram language env context exprs of
+      case loadProgram evaluator language env context exprs of
         Left typeError -> output (Msg $ pack $ show typeError)
         Right (results, env', context') -> do
           setEnv (repl {env = env', context = context'})
diff --git a/lambda-calcul/haskell/src/Minilang/REPL/Types.hs b/lambda-calcul/haskell/src/Minilang/REPL/Types.hs
index baa59ff..0b0472e 100644
--- a/lambda-calcul/haskell/src/Minilang/REPL/Types.hs
+++ b/lambda-calcul/haskell/src/Minilang/REPL/Types.hs
@@ -49,11 +49,12 @@ data REPLEnv = REPLEnv
     curIndent :: Int,
     stepTypeCheck :: Bool,
     debugParser :: Bool,
-    language :: Language
+    language :: Language,
+    evaluator :: Evaluator
   }
 
 initialREPL :: REPLEnv
-initialREPL = REPLEnv newEnv newContext 0 False False Untyped
+initialREPL = REPLEnv newEnv newContext 0 False False Untyped DeBruijn
 
 -- | Input
 data In
@@ -87,11 +88,22 @@ data Flag
   = StepTypeChecker Bool
   | DebugParser Bool
   | SelectLanguage Language
+  | SelectEvaluator Evaluator
   deriving (Eq, Show, Generic, ToJSON, FromJSON)
 
 data Language = Untyped | Typed
   deriving (Eq, Show, Read, Generic, ToJSON, FromJSON)
 
+-- | Which reduction strategy to use.
+--
+-- * 'DeBruijn' — call-by-value head reduction on De Bruijn-indexed terms
+--   (the original evaluator).
+-- * 'NbE' — Normalisation by Evaluation: eval to a 'Value' semantic domain,
+--   then read back to a 'Term'.  Reduces under lambda binders and therefore
+--   produces fully-normalised terms.
+data Evaluator = DeBruijn | NbE
+  deriving (Eq, Show, Read, Generic, ToJSON, FromJSON)
+
 -- | "Parse" given `Text` into some input for the REPL
 interpret ::
   Text -> In
@@ -113,6 +125,10 @@ interpret (unpack -> (':' : 'l' : 'a' : 'n' : 'g' : ' ' : lang)) =
   case readMaybe lang of
     Nothing -> Com Help
     Just l -> Com $ Set $ SelectLanguage l
+interpret (unpack -> (':' : 'e' : 'v' : 'a' : 'l' : ' ' : ev)) =
+  case readMaybe ev of
+    Nothing -> Com Help
+    Just e  -> Com $ Set $ SelectEvaluator e
 interpret t = In t
 
 helpText :: Text
@@ -128,6 +144,8 @@ helpText =
       "   :set <option>    : Set an option modifying the interpreter's behaviour",
       "   :unset <option>  : Remove an option that's been set previously",
       "   :l(oad) <file>   : load content of <file> into the interpreter, parsing and type-checking it",
+      "   :lang <Language> : Switch type-checking language (Untyped | Typed)",
+      "   :eval <Evaluator>: Switch reduction strategy (DeBruijn | NbE)",
       "",
       "Options: ",
       "   step             : Run the typechecker step-by-step, pausing at each rule application and",
diff --git a/lambda-calcul/haskell/src/Minilang/Server.hs b/lambda-calcul/haskell/src/Minilang/Server.hs
index 4252669..1b9fa25 100644
--- a/lambda-calcul/haskell/src/Minilang/Server.hs
+++ b/lambda-calcul/haskell/src/Minilang/Server.hs
@@ -26,6 +26,7 @@ import Data.Swagger (Swagger)
 import Data.Text (Text)
 import Minilang.API (Challenge, LambdaAPI, defaultChallenges)
 import Minilang.App (Env (..), lambdaApp, makeEnv, runApp)
+import Minilang.REPL.Types (Evaluator (..))
 import Minilang.Log
 import Minilang.OpenApi (lambdaSwagger)
 import Minilang.REPL.Net
@@ -45,16 +46,16 @@ data Server = Server
     serverPort :: Int
   }
 
--- | Starts HTTP server on given port.
+-- | Starts HTTP server on given port using the specified 'Evaluator'.
 --  This server serves static files from public/ directory and also
 --  exposes a WebSocket-based REPL under `/repl` path.
-startServer :: Int -> IO Server
-startServer serverPort = do
+startServer :: Int -> Evaluator -> IO Server
+startServer serverPort ev = do
   envs <- newTVarIO mempty
   logger <- newLog "minilang"
   loggerMiddleware <- runHTTPLog logger
   challenges <- readChallenges logger
-  env <- newStdGen >>= (`makeEnv` challenges)
+  env <- newStdGen >>= \g -> makeEnv g challenges ev
   let app =
         loggerMiddleware $
           runNetREPL logger envs (serveAPI env)