summaryrefslogtreecommitdiff
path: root/lambda-calcul/haskell/src/Minilang/REPL/Run.hs
diff options
context:
space:
mode:
authorArnaud Bailly <arnaud@pankzsoft.com>2025-11-06 08:35:36 +0100
committerArnaud Bailly <arnaud@pankzsoft.com>2025-11-06 08:35:36 +0100
commitb87d5b45110cd7efe7109dd6d4e9c19ef28522aa (patch)
tree2fd831c479523b8a77d6a721e00ec5b610a7b111 /lambda-calcul/haskell/src/Minilang/REPL/Run.hs
parent6d35fd9630238375cc28a282780f597421107469 (diff)
downloadlambda-nantes-b87d5b45110cd7efe7109dd6d4e9c19ef28522aa.tar.gz
evaluate terms when defining them
Diffstat (limited to 'lambda-calcul/haskell/src/Minilang/REPL/Run.hs')
-rw-r--r--lambda-calcul/haskell/src/Minilang/REPL/Run.hs28
1 files changed, 14 insertions, 14 deletions
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