From 4fed459d89b6b3abcce8028b19af806b48a38bd7 Mon Sep 17 00:00:00 2001
From: Arnaud Bailly <arnaud@pankzsoft.com>
Date: Sun, 22 Mar 2026 13:16:21 +0100
Subject: Add builtin arithmetic operators
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

* also allow choosing evaluator
* ensures equivalence of evaluators up-to α-renaming
* checks server accepts answers from challenge
---
 lambda-calcul/haskell/src/Minilang/REPL/Run.hs   | 16 ++++++++++------
 lambda-calcul/haskell/src/Minilang/REPL/Types.hs | 22 ++++++++++++++++++++--
 2 files changed, 30 insertions(+), 8 deletions(-)

(limited to 'lambda-calcul/haskell/src/Minilang/REPL')

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",
-- 
cgit v1.3.1