(* This is an implementation of a call-by-value evaluator for pure
 * simply typed lambda calculus. We verify that the implementation
 * preserves the type of the term being evaluated: a term of a given
 * type is evaluated to a closure of the same type.
 *)

datatype simple_type = Base of int | Fun of simple_type * simple_type

datatype lambda_exp =
  One | Shift of lambda_exp |
  Abs of simple_type * lambda_exp |
  App of lambda_exp * lambda_exp

datatype context = CTXempty | CTXcons of simple_type * context

typeref lambda_exp of simple_type * context
with One <| {t,ctx} lambda_exp(t,CTXcons(t,ctx))
   | Shift <| {ta,tb,ctx} lambda_exp(ta,ctx) -> lambda_exp(ta,CTXcons(tb,ctx))
   | Abs <| {ta,tb,ctx} simple_type * lambda_exp(tb,CTXcons(ta,ctx)) ->
                          lambda_exp(Fun(ta,tb),ctx)
   | App <| {ta,tb,ctx} lambda_exp(Fun(ta,tb),ctx) * lambda_exp(ta,ctx) ->
                          lambda_exp(tb,ctx)

datatype closure = Closure of lambda_exp * environment
and environment = ENVempty | ENVcons of closure * environment

typeref closure of simple_type
with Closure <| {t,ctx} lambda_exp(t,ctx) * environment(ctx) -> closure(t)
and environment of simple_type * context
with ENVempty <| environment(CTXempty)
   | ENVcons <| {t,ctx}
                  closure(t) * environment(ctx) -> environment(CTXcons(t,ctx))

fun call_by_value(lam) =
  let
    fun cbv(One, ENVcons(clo, env)) = clo
      | cbv(Shift(lam), ENVcons(clo, env)) = cbv(lam, env)
      | cbv(Abs(sim, lam), env) = Closure(Abs(sim, lam), env)
      | cbv(App(flam, lam), env) =
        let
          val Closure(Abs(sim, body), fenv) = cbv(flam, env)
          val clo = cbv(lam, env)
        in
          cbv(body, ENVcons(clo, fenv))
        end
    where cbv <|{t,ctx} lambda_exp(t,ctx) * environment(ctx) -> closure(t)
  in
    cbv(lam, ENVempty)
  end
where call_by_value <| {t:simple_type} lambda_exp(t, CTXempty) -> closure(t)