(* Continuation-Passing Style Interpreter for MinML *)
(* 15-312 Foundations of Programming Languages *)
(* Frank Pfenning, Fall'02 *)

structure CPS : EVAL =
struct

  open T
  open P
  open DBMinML

  (* cannot type-check this easily in ML in this style *)
  type value = exp

  (**** Auxiliary Functions ****)

  (* applyPrimop : primop * value list -> exp *)
  fun applyPrimop (p, vs) = valOf (evalPrimop (p, vs))

  (* applyIf : value * exp * exp -> exp *)
  fun applyIf (Bool(true), e2, e3) = e2
    | applyIf (Bool(false), e2, e3) = e3
    (* other expressions impossible by MinML typing *)

  (* applyFun : value * value -> exp *)
  fun applyFun (v1 as Fun(_, _, ((), (), e1')), v2) =
	Subst.subst (v1, 2, Subst.subst (v2, 1, e1'))
    (* other expressions impossible by MinML typing *)

  (**** Evaluation ****)
  (* eval : exp -> (value -> value) -> value *)
  (* evals : exp list -> (value list -> value) -> value *)

  fun eval (v as Int _) k = k v
    | eval (Primop(p, es)) k = evals es (fn vs => k (applyPrimop (p, vs)))

    | eval (v as Bool _) k = k v
    | eval (If(e1, e2, e3)) k =
        eval e1 (fn v1 => eval (applyIf (v1, e2, e3)) k)

    | eval (v as Fun _) k = k v
    | eval (Apply(e1, e2)) k =
	eval e1 (fn v1 => eval e2 (fn v2 => eval (applyFun (v1, v2)) k))

    | eval (Let(e1, ((), e2))) k =
	eval e1 (fn v1 => eval (Subst.subst (v1, 1, e2)) k)

    (* eval (Var _) k impossible by MinML typing *)

  and evals (nil) k = k (nil)
    | evals (e::es) k = eval e (fn v => evals es (fn vs => k (v:: vs)))

  fun evaluate e = eval e (fn v => v)

end;  (* structure CPS *)