1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
|
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, extendContext, infer)
import Minilang.Lambda.Parser (AST (..), desugar)
import Minilang.Lambda.Unify (Type (..))
import Minilang.REPL.Types (Language (..))
-- | Top-level evaluator
-- 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 ->
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 =
foldl
( \acc expr ->
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 = evalInEnv env body
in case language of
Typed ->
case infer term of
Left typeError -> Left typeError
Right typ ->
Right (Nothing, (ident, term) : env, extendContext ident typ context)
Untyped ->
Right (Nothing, (ident, term) : env, context)
runExpr language expr env context =
let v = evalInEnv env expr
in case language of
Typed ->
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)
|
