(* Normalization by evaluation for untyped lambda terms
   AM Pitts 30/05/03
*)

(* syntax *)
type t;;
type var = t name;;
type term =
    Var of var
  | Lam of <<var>>term
  | App of term*term;;

(* semantics *)
type sem =
    L of ((unit -> sem) -> sem)
  | N of neu
and neu =
    V of var
  | A of neu*sem;;

(* reification reify : sem -> term *)
let rec reify d =
 match d with
     L f -> let x=fresh in Lam(<<x>>(reify(f(function () -> N(V x)))))
   | N n -> reifyn n
and reifyn n =
 match n with
     V x -> Var x
   | A(n',d') -> App(reifyn n', reify d');;

(* evals : (var * (unit->sem))list -> term -> sem *)
let rec evals env t  =
  match t with
      Var x -> (match env with
		    [] -> N(V x)
		  | (x',v)::env -> if x=x' then v() 
		                   else evals env (Var x))
    | Lam(<<x>>t) -> L(function v -> evals ((x,v)::env) t)
    | App(t1,t2) -> (match evals env t1 with
			 L f -> f(function () -> evals env t2)
		       | N n -> N(A(n,evals env t2)));;

(* evaluation eval : term -> sem *)
let rec eval t = evals [] t;;

(* normalisation norm:lam -> lam *)
let norm t = reify(eval t);;

(* equal : term * term -> bool
   Claim: equal(t1,t2)=true iff t1 and t2 are normalisable 
   and have the same normal form, up to alpha-equivalence 
*)
let equal(t1,t2) = ((norm t1)=(norm t2));;

(* examples *)
let a,b,c=fresh,fresh,fresh;;
let s = Lam(<<a>>(
          Lam(<<b>>(
           Lam(<<c>>(
            App(App(Var a,Var c),
                App(Var b,Var c))))))));;
let k = Lam(<<a>>(Lam(<<b>>(Var a))));;
let i  = Lam(<<a>>(Var a));;
let l = Lam(<<a>>i);;
let p  = Lam(<<a>>(
	  Lam(<<b>>(
	   Lam(<<c>>(
            App(App(Var c,Var a),Var b)))))));;
let p1 = Lam(<<c>>(App(Var c,k)));;
let p2 = Lam(<<c>>(App(Var c,l)));;
let omega = Lam(<<a>>(App(Var a, Var a)));;
let y  = Lam(<<a>>(
	  App(Lam(<<b>>(App(Var a,
                          App(Var b,Var b)))),
              Lam(<<b>>(App(Var a,
                          App(Var b,Var b)))))));;

(* tests *)
let t = App(App(App(s,k),k),i);; (* the normal form of this is i *)
(norm t) = i;; 
let i1 = App(p2,App(App(p,s),k));;(* the normal form of this is k *)
(norm i1) = k;;
let tm = App(l, App(omega,omega));; (* the normal form of this is i *)
(norm tm) = i;;
let loop = App(y,i);; (* fixpoint of the identity, has no normal form *)
(* so don't try this at home
norm loop;;
*)