evaluate terms when defining them

3 files changed, 29 insertions, 21 deletions

diff --git a/lambda-calcul/haskell/src/Minilang/Lambda.hs b/lambda-calcul/haskell/src/Minilang/Lambda.hs
index d223658..ff636ce 100644
--- a/lambda-calcul/haskell/src/Minilang/Lambda.hs
+++ b/lambda-calcul/haskell/src/Minilang/Lambda.hs
@@ -3,7 +3,7 @@ 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.Infer (Context, TypeError, infer)
+import Minilang.Lambda.Infer (Context, TypeError, extendContext, infer)
 import Minilang.Lambda.Parser (AST (..), desugar)
 import Minilang.Lambda.Unify (Type (..))
 import Minilang.REPL.Types (Language (..))
@@ -38,24 +38,28 @@ loadProgram language env context exprs =
         exprs
 
     runExpr language (Def ident body) env context =
-      let term = desugar body
+      let term = evalInEnv env body
        in case language of
             Typed ->
               case infer term of
                 Left typeError -> Left typeError
                 Right typ ->
-                  Right (Nothing, (ident, term) : env, context)
+                  Right (Nothing, (ident, term) : env, extendContext ident typ context)
             Untyped ->
               Right (Nothing, (ident, term) : env, context)
     runExpr language expr env context =
-      let term = desugar expr
-          env' = second toDeBruijn <$> env
-          v = fromDeBruijn $ eval' env' (toDeBruijn term)
+      let v = evalInEnv env expr
        in case language of
             Typed ->
-              case infer term of
+              case infer v of
                 Left typeError -> Left typeError
                 Right typ ->
                   Right (Just (v, typ), env, context)
             Untyped ->
               Right (Just (v, TyVar "<?>"), env, context)
+
+evalInEnv :: Env -> AST -> Term
+evalInEnv env expr =
+  let term = desugar expr
+      env' = second toDeBruijn <$> env
+   in fromDeBruijn $ eval' env' (toDeBruijn term)
diff --git a/lambda-calcul/haskell/src/Minilang/Lambda/Infer.hs b/lambda-calcul/haskell/src/Minilang/Lambda/Infer.hs
index ab590c6..2052398 100644
--- a/lambda-calcul/haskell/src/Minilang/Lambda/Infer.hs
+++ b/lambda-calcul/haskell/src/Minilang/Lambda/Infer.hs
@@ -61,6 +61,10 @@ data Context = Context
   }
   deriving (Eq, Show, Generic, ToJSON, FromJSON)
 
+extendContext :: Text -> Type -> Context -> Context
+extendContext x ty (Context n env) =
+  Context n (Map.insert x ty env)
+
 annotate :: Eval.Term -> Either TypeError (ATerm Type)
 annotate t =
   evalStateT (go (fromTerm t) []) newContext
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