(* Deductive Systems: An evaluator for Mini-ML using HOAS *)
(* Author: Carsten Schuermann *)

datatype exp
  = Z
  | S of exp
  | Case of exp * exp * (exp -> exp)
  | Lam of (exp -> exp)
  | App of exp * exp
  | Pair of exp * exp
  | Fst of exp
  | Snd of exp
  | Fix of (exp -> exp)
  | Let of exp * (exp -> exp)


(* Invariant:  
   eval E = V     <=>  e evalsto v
*)

fun eval Z = Z
  | eval (S e) = S (eval e)
  | eval (Case (e, e1, e2)) = 
    (case (eval e) of
       Z => eval e1
     | (S v') => eval (e2 v'))
  | eval (Lam e) = Lam e
  | eval (App (e1, e2)) = 
    (case (eval e1) of 
       (Lam e1') => eval (e1' (eval e2)))
  | eval (Pair (e1, e2)) = Pair (eval e1, eval e2)
  | eval (Fst e) = 
    (case eval e of
       Pair (v1, v2) => v1)
  | eval (Snd e) = 
    (case eval e of
       Pair (v1, v2) => v2)
  | eval (Fix e) = eval (e (Fix e)) 
  | eval (Let (e1, e2)) = eval (e2 (eval e1))
	  

(* Example run:
eval (App (Fix (fn f => Lam (fn x => Case (x, Z, fn x' => S (S (App (f,  x')))))), S (S Z)));
val it = S (S (S (S Z))) : exp
*)