From b87d5b45110cd7efe7109dd6d4e9c19ef28522aa Mon Sep 17 00:00:00 2001 From: Arnaud Bailly Date: Thu, 6 Nov 2025 08:35:36 +0100 Subject: evaluate terms when defining them --- lambda-calcul/haskell/src/Minilang/Lambda.hs | 18 ++++++++------ lambda-calcul/haskell/src/Minilang/Lambda/Infer.hs | 4 ++++ lambda-calcul/haskell/src/Minilang/REPL/Run.hs | 28 +++++++++++----------- .../haskell/test/Minilang/Lambda/EvalSpec.hs | 2 +- .../haskell/test/Minilang/REPL/NetSpec.hs | 2 +- lambda-calcul/haskell/test/Minilang/REPLSpec.hs | 4 ++-- 6 files changed, 33 insertions(+), 25 deletions(-) (limited to 'lambda-calcul/haskell') 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" ] -- cgit v1.3.1