47 lines
963 B
Plaintext
47 lines
963 B
Plaintext
# Helpers
|
|
datatype 'a list {
|
|
Cons ('a, 'a list),
|
|
Empty,
|
|
}
|
|
|
|
datatype 'a maybe {
|
|
Just 'a,
|
|
Nothing,
|
|
}
|
|
|
|
# Lambda calculus term, nameless representation
|
|
datatype term {
|
|
Var int
|
|
Int int
|
|
Abs term
|
|
App (term, term)
|
|
}
|
|
|
|
# Result of the evaluation
|
|
datatype value {
|
|
Int int
|
|
Closure (env, term)
|
|
}
|
|
|
|
alias env = value list
|
|
|
|
typecheck add_binding : value -> env -> env
|
|
def add_binding v env = Cons v env
|
|
|
|
typecheck lookup : int -> env -> value maybe
|
|
def lookup _ <Empty> = Nothing
|
|
| lookup 0 <Cons x xs> = Just x
|
|
| lookup n <Cons x xs> = lookup (subtract n 1) xs
|
|
|
|
typecheck eval : env -> term -> value
|
|
def eval e <Var idx> = match lookup idx e {
|
|
case <Just v> -> v
|
|
case <Nothing> -> abort "Variable out of scope"
|
|
}
|
|
|
|
| eval e <Int x> = Int x
|
|
| eval e <Abs t> = Closure e t
|
|
| eval e <App t1 t2> =
|
|
let def new_env = add_binding (eval e t2) e
|
|
in eval new_env t1
|