summaryrefslogtreecommitdiff
path: root/lambda-calcul/haskell/src/Minilang/Lambda.hs
diff options
context:
space:
mode:
authorArnaud Bailly <arnaud@pankzsoft.com>2025-11-05 12:02:23 +0100
committerArnaud Bailly <arnaud@pankzsoft.com>2025-11-05 12:02:23 +0100
commit99e2ce71faa82e7b99574895e0fe24183ba9f6c3 (patch)
tree10538bb91d187a3c1d281a87a3974a6036f2ad2f /lambda-calcul/haskell/src/Minilang/Lambda.hs
parent438e3f8c5dcdfeead15a6a9a1760f7c254fc54b2 (diff)
downloadlambda-nantes-99e2ce71faa82e7b99574895e0fe24183ba9f6c3.tar.gz
can parse whole programs and load them
Diffstat (limited to 'lambda-calcul/haskell/src/Minilang/Lambda.hs')
-rw-r--r--lambda-calcul/haskell/src/Minilang/Lambda.hs69
1 files changed, 49 insertions, 20 deletions
diff --git a/lambda-calcul/haskell/src/Minilang/Lambda.hs b/lambda-calcul/haskell/src/Minilang/Lambda.hs
index d2df56f..2372578 100644
--- a/lambda-calcul/haskell/src/Minilang/Lambda.hs
+++ b/lambda-calcul/haskell/src/Minilang/Lambda.hs
@@ -1,32 +1,61 @@
module Minilang.Lambda where
-import Minilang.Lambda.DeBruijn (eval, fromDeBruijn, toDeBruijn)
+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.Parser (AST, desugar)
+import Minilang.Lambda.Parser (AST (..), desugar)
import Minilang.Lambda.Unify (Type (..))
import Minilang.REPL.Types (Language (..))
-- | Top-level evaluator
--- Load an AST into given `Env` and `Context`, returning an extended
--- `Env` and `Context` with declarations bound
+-- Load a list of expressions into given `Env` and `Context`, returning an extended
+-- `Env` and `Context` with declarations bound and the list of evaluated top-level
+-- terms along with their types.
loadProgram ::
Language ->
- AST ->
Env ->
Context ->
- Either TypeError (Term, Type, Env, Context)
--- loadProgram (Let d r) ρ γ = do
--- (ρ', γ') <- checkD 0 d ρ γ
--- loadProgram r ρ' γ'
-loadProgram language expr env context =
- let term = desugar expr
- v = fromDeBruijn $ eval (toDeBruijn term)
- in case language of
- Typed ->
- case infer term of
- Left typeError -> Left typeError
- Right typ ->
- Right (v, typ, env, context)
- Untyped ->
- Right (v, TyVar "<?>", env, context)
+ [AST] ->
+ Either TypeError ([(Term, Type)], Env, Context)
+loadProgram language env context exprs =
+ fmap (\(res, e, c) -> (reverse res, e, c)) result
+ where
+ result =
+ foldr
+ ( \expr acc ->
+ case acc of
+ Left typeError -> Left typeError
+ Right (results, env', context') ->
+ case runExpr language expr env' context' of
+ Left typeError -> Left typeError
+ Right (Nothing, env'', context'') ->
+ Right (results, env'', context'')
+ Right (Just res, env'', context'') ->
+ Right (res : results, env'', context'')
+ )
+ (Right ([], env, context))
+ exprs
+
+ runExpr language (Def ident body) env context =
+ let term = desugar body
+ in case language of
+ Typed ->
+ case infer term of
+ Left typeError -> Left typeError
+ Right typ ->
+ Right (Nothing, (ident, term) : env, 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)
+ in case language of
+ Typed ->
+ case infer term of
+ Left typeError -> Left typeError
+ Right typ ->
+ Right (Just (v, typ), env, context)
+ Untyped ->
+ Right (Just (v, TyVar "<?>"), env, context)