From ae59f17cb3d58de7afca7f441d8bcf9a718e024c Mon Sep 17 00:00:00 2001
From: Arnaud Bailly <arnaud@pankzsoft.com>
Date: Wed, 5 Nov 2025 09:15:46 +0100
Subject: handle defitions in untyped language

---
 lambda-calcul/haskell/src/Minilang/REPL/Pure.hs    |  1 +
 lambda-calcul/haskell/src/Minilang/REPL/Run.hs     | 22 ++++++++++++++++++----
 lambda-calcul/haskell/src/Minilang/REPL/Types.hs   |  6 +++---
 .../haskell/test/Minilang/Lambda/ParserSpec.hs     | 10 +++++-----
 lambda-calcul/haskell/test/Minilang/REPLSpec.hs    | 11 +++++++++++
 5 files changed, 38 insertions(+), 12 deletions(-)

diff --git a/lambda-calcul/haskell/src/Minilang/REPL/Pure.hs b/lambda-calcul/haskell/src/Minilang/REPL/Pure.hs
index 7ca0c85..8250152 100644
--- a/lambda-calcul/haskell/src/Minilang/REPL/Pure.hs
+++ b/lambda-calcul/haskell/src/Minilang/REPL/Pure.hs
@@ -42,6 +42,7 @@ render :: Out -> Text
 render = \case
   Msg t -> t
   Evaluated ast _term typ -> pretty ast <> " : " <> Type.pretty typ
+  Defined ident typ -> ident <> " : " <> Type.pretty typ
   Bye -> "Bye!"
   other -> pack (show other)
 
diff --git a/lambda-calcul/haskell/src/Minilang/REPL/Run.hs b/lambda-calcul/haskell/src/Minilang/REPL/Run.hs
index bc552cb..a98ff41 100644
--- a/lambda-calcul/haskell/src/Minilang/REPL/Run.hs
+++ b/lambda-calcul/haskell/src/Minilang/REPL/Run.hs
@@ -7,13 +7,14 @@
 module Minilang.REPL.Run where
 
 import Control.Monad.Catch
+import Data.Bifunctor (second)
 import Data.Text hiding (replicate)
 import Minilang.Lambda (loadProgram)
-import Minilang.Lambda.DeBruijn (eval, fromDeBruijn, toDeBruijn)
+import Minilang.Lambda.DeBruijn (eval, eval', fromDeBruijn, toDeBruijn)
 import Minilang.Lambda.Eval (newEnv)
 import Minilang.Lambda.Infer (infer, newContext)
 import qualified Minilang.Lambda.Infer as Infer
-import Minilang.Lambda.Parser (desugar, parse, resugar)
+import Minilang.Lambda.Parser (AST (..), desugar, parse, resugar)
 import Minilang.Lambda.Unify (Type (TyVar))
 import Minilang.REPL.Types
 
@@ -35,12 +36,25 @@ handleUserInput ::
   Text ->
   m ()
 handleUserInput txt = do
-  REPLEnv {language} <- getEnv
+  repl@REPLEnv {language, env} <- getEnv
   case parse txt of
     Left err -> output (Msg $ pack $ show err)
+    Right (Def ident body) -> do
+      let term = desugar body
+      case language of
+        Typed ->
+          case infer term of
+            Left typeError -> output (Msg $ Infer.render typeError)
+            Right typ -> do
+              setEnv $ repl {env = (ident, term) : env}
+              output (Defined ident typ)
+        Untyped -> do
+          setEnv $ repl {env = (ident, term) : env}
+          output (Defined ident (TyVar "<?>"))
     Right expr -> do
       let term = desugar expr
-          v = fromDeBruijn $ eval (toDeBruijn term)
+          env' = second toDeBruijn <$> env
+          v = fromDeBruijn $ eval' env' (toDeBruijn term)
           ast = resugar v
       case language of
         Typed ->
diff --git a/lambda-calcul/haskell/src/Minilang/REPL/Types.hs b/lambda-calcul/haskell/src/Minilang/REPL/Types.hs
index b7a324b..baa59ff 100644
--- a/lambda-calcul/haskell/src/Minilang/REPL/Types.hs
+++ b/lambda-calcul/haskell/src/Minilang/REPL/Types.hs
@@ -7,11 +7,11 @@ import Control.Exception (Exception)
 import Data.Aeson (FromJSON, ToJSON)
 import Data.Text as Text hiding (replicate)
 import GHC.Generics
-import Minilang.Lambda.Eval (Env, Term, newEnv)
+import Minilang.Lambda.Eval (Term, Env, newEnv)
 import Minilang.Lambda.Infer (Context, newContext)
+import Minilang.Lambda.Parser (AST)
 import Minilang.Lambda.Unify (Type)
 import Text.Read (readMaybe)
-import Minilang.Lambda.Parser (AST)
 
 class (Monad m) => MonadREPL m where
   -- | Returns the current environment for this session
@@ -76,7 +76,7 @@ data Content
   deriving (Eq, Show, Generic, ToJSON, FromJSON)
 
 data Out
-  = Defined Text Term
+  = Defined Text Type
   | Evaluated AST Term Type
   | CurrentEnv Env Context Language
   | Msg Text
diff --git a/lambda-calcul/haskell/test/Minilang/Lambda/ParserSpec.hs b/lambda-calcul/haskell/test/Minilang/Lambda/ParserSpec.hs
index e7816c6..e6f05b9 100644
--- a/lambda-calcul/haskell/test/Minilang/Lambda/ParserSpec.hs
+++ b/lambda-calcul/haskell/test/Minilang/Lambda/ParserSpec.hs
@@ -98,14 +98,14 @@ spec = parallel $ do
                 )
                 `shouldSatisfy` isRight
 
-  it "parses a definition" $ do
-    let defStr = "(def id (lam (x) x))"
-        expectedAST = Def "id" (Abs ["x"] (Sym "x"))
-    parse defStr `shouldBe` Right expectedAST
+  prop "parses a definition" $
+    forAll (genDef 5) $ \ast ->
+      let text = pretty ast
+       in parse text `shouldBe` Right ast
 
 spine :: AST -> Int
 spine = \case
-  App x y rest -> 1 + spine x + length rest
+  App x _ rest -> 1 + spine x + length rest
   _ -> 0
 
 arity :: AST -> Int
diff --git a/lambda-calcul/haskell/test/Minilang/REPLSpec.hs b/lambda-calcul/haskell/test/Minilang/REPLSpec.hs
index cf6ef01..81ac25c 100644
--- a/lambda-calcul/haskell/test/Minilang/REPLSpec.hs
+++ b/lambda-calcul/haskell/test/Minilang/REPLSpec.hs
@@ -23,6 +23,17 @@ spec = parallel $
                      "y : <?>"
                    ]
 
+    it "evaluates untyped MiniLang terms with definitions" $ do
+      let out =
+            withInput
+              ["(def id (lam (x) x))", "(id y)"]
+
+      out
+        `shouldBe` [ "Bye!",
+                     "y : <?>",
+                     "id : <?>"
+                   ]
+
     it "defaults untyped terms" $ do
       let out =
             withInput
-- 
cgit v1.3.1