datatype term = I of int | B of bool | Var of string
	      | Cond of term * term * term
              | Pair of term * term | Fst of term | Snd of term
              | Abs of string * term | App of term * term
              | Fix of string * term
              | Iszero of term | Succ of term | Pred of term;
		
local
fun member(x,nil) = false
   |member(x,y::ys) = x=y orelse member(x,ys);
fun merge(nil,ys) = ys
   |merge(xs,nil) = xs
   |merge(x::xs,ys) = if member(x,ys) then merge(xs,ys) else x::merge(xs,ys);
fun fr(Cxt, I n) = nil
   |fr(Cxt, B b) = nil
   |fr(Cxt,Var x) = if member(x,Cxt) then nil else x::nil
   |fr(Cxt, Cond(e1,e2,e3)) = merge(merge(fr(Cxt,e1),fr(Cxt,e2)),fr(Cxt,e3))
   |fr(Cxt, Pair(e1,e2)) = merge(fr(Cxt,e1),fr(Cxt,e2))
   |fr(Cxt, Fst(e1)) = fr(Cxt,e1)
   |fr(Cxt,Snd(e1)) = fr(Cxt,e1)
   |fr(Cxt,Abs(x,M)) = fr(x::Cxt,M)
   |fr(Cxt,App(M,N)) = merge(fr(Cxt,M),fr(Cxt,N))
   |fr(Cxt,Fix(x,M)) = fr(x::Cxt,M)
   |fr(Cxt,Iszero(e1)) = fr(Cxt,e1)
   |fr(Cxt,Succ(e1)) = fr(Cxt,e1)
   |fr(Cxt,Pred(e1)) = fr(Cxt,e1)


 val VarNames = ["x","y","z","u","v","w",
	         "x1","y1","z1","u1","v1","w1",
	         "x2","y2","z2","u2","v2","w2",
	         "x3","y3","z3","u3","v3","w3"];

 fun getfree(x::xs, L) = if not(member(x,L)) then x else getfree(xs,L)


  fun free M = fr(nil,M);

fun rename(M, x, y) =
  let fun ren(Var z) = if z=x then (Var y) else (Var z)
	 |ren(I n) = I n
	 |ren(B b) = B b
	 |ren(Cond(e1,e2,e3)) = Cond(ren e1, ren e2, ren e3)
	 |ren(Pair(e1,e2)) = Pair(ren e1, ren e2)
	 |ren(Fst e) = Fst(ren e)
	 |ren(Snd e) = Snd(ren e)
         |ren(Abs(z,M)) = if z=x then Abs(z,M) else Abs(z,ren M)
	 |ren(App(M,N)) = App(ren M, ren N)
         |ren(Fix(z,M)) = if z=x then Fix(z,M) else Fix(z,ren M)
	 |ren(Iszero e) = Iszero(ren e)
	 |ren(Succ e) = Succ(ren e)
	 |ren(Pred e) = Pred(ren e)
  in ren M end;


fun subst(M,N,x) =
  let fun sub(Var y) = if x=y then N else (Var y)
         |sub(I n) = I n
         |sub(B b) = B b
	 |sub(Cond(e1,e2,e3)) = Cond(sub e1, sub e2, sub e3)
	 |sub(Pair(e1,e2)) = Pair(sub e1, sub e2)
	 |sub(Fst e) = Fst(sub e)
	 |sub(Snd e) = Snd(sub e)
	 |sub(Abs(y,P)) = if x=y then Abs(y,P)
			  else if not(member(y,free(N)))
			       then Abs(y,sub(P))
			       else let val z=getfree(VarNames,free N @ free P)
				    in Abs(z,sub(rename(P,y,z)))
				    end
	 |sub(App(P,Q)) = App(sub P, sub Q)
	 |sub(Fix(y,P)) = if x=y then Fix(y,P)
			  else if not(member(y,free(N)))
			       then Fix(y,sub(P))
			       else let val z=getfree(VarNames,free N @ free P)
				    in Fix(z,sub(rename(P,y,z)))
				    end
	 |sub(Iszero e) = Iszero(sub e)
	 |sub(Succ e) = Succ(sub e)
	 |sub(Pred e) = Pred(sub e)
  in sub M end

in  (* local *)


(* Natural Semantics using Substitutions *)
		
fun eval (I n) = (I n)
   |eval (B b) = (B b)
   |eval (Cond(e1,e2,e3)) = 
      let val (B b) = eval e1
      in eval (if b then e2 else e3)
      end
   |eval (Pair(e1,e2)) = Pair(eval e1, eval e2)
   |eval (Fst e) =
      let val Pair(v1,v2) = eval e
      in v1 end
   |eval (Snd e) =
      let val Pair(v1,v2) = eval e
      in v2 end
   |eval (Abs(x,e)) = Abs(x,e)
   |eval (Fix(f,Abs(x,e))) = (Fix(f,Abs(x,e)))
   |eval (App(e1,e2)) =
      let  val v2 = eval e2
      in case (eval e1) of
         Abs(x,e') => eval (subst(e',v2,x))
        |Fix(f,Abs(x,e')) => eval (subst(subst(e',v2,x),Fix(f,Abs(x,e')),f))
      end
   |eval (Iszero e) =
      let val (I n) = eval e
      in B (n=0) end
   |eval (Succ e) =
      let val (I n) = eval e
      in  I(n+1) end
   |eval (Pred e) =
      let val (I n) = eval e
      in  I(n-1) end;
		

end; (* local *)