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
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
|
module Minilang.Lambda where
import Data.Bifunctor (second)
import Minilang.Lambda.DeBruijn (builtinDeBruijnEnv, eval', fromDeBruijn, toDeBruijn)
import Minilang.Lambda.Eval (Env, Term, builtinEnvValue)
import qualified Minilang.Lambda.Eval as Eval
import Minilang.Lambda.Infer (Context, TypeError, extendContext, infer)
import Minilang.Lambda.Parser (AST (..), desugar)
import Minilang.Lambda.Unify (Type (..))
import Minilang.REPL.Types (Evaluator (..), 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 ::
Evaluator ->
Language ->
Env ->
Context ->
[AST] ->
Either TypeError ([(Term, Type)], Env, Context)
loadProgram evaluator 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 = evalInEnvWith evaluator 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 = evalInEnvWith evaluator 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)
-- | Evaluate an 'AST' in the given 'Env' using the De Bruijn CBV evaluator.
-- This is the default evaluator used by the server and REPL.
evalInEnv :: Env -> AST -> Term
evalInEnv = evalInEnvWith DeBruijn
-- | Evaluate an 'AST' using the selected 'Evaluator'.
evalInEnvWith :: Evaluator -> Env -> AST -> Term
evalInEnvWith DeBruijn env expr =
let term = desugar expr
-- User-defined bindings take precedence over builtins (rightmost wins
-- in a left-to-right lookup, so put user env first).
env' = (second toDeBruijn <$> env) ++ builtinDeBruijnEnv
in fromDeBruijn $ eval' env' (toDeBruijn term)
evalInEnvWith NbE env expr =
let term = desugar expr
-- Build an EnvValue from the user Env by evaluating each binding's
-- Term in the accumulated value env (builtins always available at the
-- bottom). foldl builds left-to-right so earlier bindings are visible
-- when evaluating later ones.
envV = foldl addBinding builtinEnvValue env
addBinding acc (name, t) = (name, Eval.eval acc t) : acc
in Eval.readBack (Eval.eval envV term)
|
