From b87d5b45110cd7efe7109dd6d4e9c19ef28522aa Mon Sep 17 00:00:00 2001
From: Arnaud Bailly <arnaud@pankzsoft.com>
Date: Thu, 6 Nov 2025 08:35:36 +0100
Subject: evaluate terms when defining them

---
 lambda-calcul/haskell/src/Minilang/REPL/Run.hs | 28 +++++++++++++-------------
 1 file changed, 14 insertions(+), 14 deletions(-)

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

diff --git a/lambda-calcul/haskell/src/Minilang/REPL/Run.hs b/lambda-calcul/haskell/src/Minilang/REPL/Run.hs
index bf28b23..8b9b844 100644
--- a/lambda-calcul/haskell/src/Minilang/REPL/Run.hs
+++ b/lambda-calcul/haskell/src/Minilang/REPL/Run.hs
@@ -7,14 +7,12 @@
 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, eval', fromDeBruijn, toDeBruijn)
+import Minilang.Lambda (loadProgram, evalInEnv)
 import Minilang.Lambda.Eval (newEnv)
-import Minilang.Lambda.Infer (infer, newContext)
+import Minilang.Lambda.Infer (extendContext, infer, newContext)
 import qualified Minilang.Lambda.Infer as Infer
-import Minilang.Lambda.Parser (AST (..), desugar, parse, parseProgram, resugar)
+import Minilang.Lambda.Parser (AST (..), parse, parseProgram, resugar)
 import Minilang.Lambda.Unify (Type (TyVar))
 import Minilang.REPL.Types
 
@@ -36,29 +34,31 @@ handleUserInput ::
   Text ->
   m ()
 handleUserInput txt = do
-  repl@REPLEnv {language, env} <- getEnv
+  repl@REPLEnv {language, env, context} <- getEnv
   case parse txt of
     Left err -> output (Msg $ pack $ show err)
     Right (Def ident body) -> do
-      let term = desugar body
+      let v = evalInEnv env body
       case language of
         Typed ->
-          case infer term of
+          case infer v of
             Left typeError -> output (Msg $ Infer.render typeError)
             Right typ -> do
-              setEnv $ repl {env = (ident, term) : env}
+              setEnv $
+                repl
+                  { env = (ident, v) : env,
+                    context = extendContext ident typ context
+                  }
               output (Defined ident typ)
         Untyped -> do
-          setEnv $ repl {env = (ident, term) : env}
+          setEnv $ repl {env = (ident, v) : env}
           output (Defined ident (TyVar "<?>"))
     Right expr -> do
-      let term = desugar expr
-          env' = second toDeBruijn <$> env
-          v = fromDeBruijn $ eval' env' (toDeBruijn term)
+      let v = evalInEnv env expr
           ast = resugar v
       case language of
         Typed ->
-          case infer term of
+          case infer v of
             Left typeError -> output (Msg $ Infer.render typeError)
             Right typ -> do
               let
-- 
cgit v1.3.1