(* C-Machine Implementation for MinML *)
(* 15-312 Foundations of Programming Languages *)
(* Frank Pfenning, Fall'02 *)

structure CMach : 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))

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

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

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

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

    | eval (Let(e1, ((), e2))) k =
	eval e1 (fn v1 => letFrame (v1, ((), e2)) k)

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

  and ifFrame (Bool(true), e2, e3) k = eval e2 k
    | ifFrame (Bool(false), e2, e3) k = eval e3 k
    (* other expressions impossible by MinML typing *)

  and applyFrame1 (v1, e2) k = eval e2 (fn v2 => applyFrame2 (v1, v2) k)
  and applyFrame2 (v1 as Fun(_, _, ((), (), e1')), v2) k =
         eval (Subst.subst (v1, 2, Subst.subst (v2, 1, e1'))) k
    (* other expressions impossible by MinML typing *)

  and letFrame (v1, ((), e2)) k = eval (Subst.subst (v1, 1, e2)) k

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

  and listFrame (v::es) k = evals es (fn vs => returns (v::vs) k)

  and return v k = k v
  and returns vs k = k vs

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

end;  (* structure CMach *)