(*
   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.
*)

(*
 * We also verify that the pattern matching in the definition
 * of function cbv is EXHAUSITIVE.
 *)

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
	    
        exception Unreachable

	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
                  | cbv _ = raise Unreachable (* we can indeed verify that this is unreachable *)
		where cbv <| {n:nat} lamexp(n) * closureList(n) -> closure
	    in
		cbv(exp, ClosureNil)
	    end
	where callbyvalue <| lamexp(0) -> closure
    end