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, Maybe 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 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 (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 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, Just typ), env', context')
Untyped ->
Right (Just (v, Nothing), 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)
|
