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
|
module Minilang.Lambda where
import Minilang.Lambda.DeBruijn (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.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
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)
|
