evaluate terms when defining them

6 files changed, 33 insertions, 25 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
diff --git a/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs b/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs
index 89e86b9..3dbe3cd 100644
--- a/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs
+++ b/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs
@@ -2,7 +2,7 @@ module Minilang.Lambda.EvalSpec (spec) where
 
 import Control.Concurrent (threadDelay)
 import Control.Concurrent.Async (race_)
-import Minilang.Lambda.Eval (Term (..), eval, evalNeed)
+import Minilang.Lambda.Eval (Term (..), eval)
 import Test.Hspec (Spec, describe, it, pending, shouldBe)
 
 spec :: Spec
diff --git a/lambda-calcul/haskell/test/Minilang/REPL/NetSpec.hs b/lambda-calcul/haskell/test/Minilang/REPL/NetSpec.hs
index 7f77eeb..6a2b1ab 100644
--- a/lambda-calcul/haskell/test/Minilang/REPL/NetSpec.hs
+++ b/lambda-calcul/haskell/test/Minilang/REPL/NetSpec.hs
@@ -71,7 +71,7 @@ spec = around withServer $
       let inp = [Com (Set (SelectLanguage Typed)), In "((lam (x) x) y)"]
           expectedOutput =
             [ Right (Msg "Language set to Typed"),
-              Right $ Evaluated (AST.Sym "y") (Var "y") (TyVar "b")
+              Right $ Evaluated (AST.Sym "y") (Var "y") (TyVar "a")
             ]
       res <- runTestClient serverPort ".newenv1" inp
 
diff --git a/lambda-calcul/haskell/test/Minilang/REPLSpec.hs b/lambda-calcul/haskell/test/Minilang/REPLSpec.hs
index 74f6c29..bd64adf 100644
--- a/lambda-calcul/haskell/test/Minilang/REPLSpec.hs
+++ b/lambda-calcul/haskell/test/Minilang/REPLSpec.hs
@@ -51,7 +51,7 @@ spec = parallel $
 
       out
         `shouldBe` [ "Bye!",
-                     "y : c",
+                     "y : a",
                      "id : a -> a",
                      "Language set to Typed"
                    ]
@@ -80,7 +80,7 @@ spec = parallel $
 
       out
         `shouldBe` [ "Bye!",
-                     "Cannot unify type variable f with type (e -> f -> e) -> e due to circularity: The variable already occurs in the type.",
+                     "(lam (z s) (s ((lam (n z s) (s n)) (lam (z s) z)))) : a -> ((d -> ((g -> h -> g) -> f) -> f) -> j) -> j",
                      "Language set to Typed"
                    ]