(*
This is an implementation of call-by-value evaluator
for the pure untyped lambda-calculus. It guarantees
that a free variable is always bound to a closure in
the environment when a CLOSED term is being evaluated.
*)
structure CallByValue =
struct
datatype lamexp =
One | Shift of lamexp | Abs of lamexp | App of lamexp * lamexp
typeref lamexp of int
with One <| {n:nat} lamexp(n+1)
| Shift <| {n:nat} lamexp(n) -> lamexp(n+1)
| Abs <| {n:nat} lamexp(n+1) -> lamexp(n)
| App <| {n:nat} lamexp(n) * lamexp(n) -> lamexp(n)
datatype closure = Closure of lamexp * closureList
and closureList = ClosureNil | ClosureCons of closure * closureList
typeref closureList of int
with ClosureNil <| closureList(0)
| ClosureCons <| {n:nat} closure * closureList(n) -> closureList(n+1)
| Closure <| {n:nat} lamexp(n) * closureList(n) -> closure
fun callbyvalue(exp) =
let
fun cbv(One, ClosureCons(clo, env)) = clo
| cbv(Shift(exp), ClosureCons(clo, env)) = cbv(exp, env)
| cbv(Abs(exp), env) = Closure(Abs(exp), env)
| cbv(App(fexp, exp), env) =
let
val Closure(Abs(body), env1) = cbv(fexp, env)
val clo = cbv(exp, env)
in
cbv(body, ClosureCons(clo, env1))
end
where cbv <| {n:nat} lamexp(n) * closureList(n) -> closure
in
cbv(exp, ClosureNil)
end
where callbyvalue <| lamexp(0) -> closure
end