(* Values and Environments *)
datatype value = VI of int | VB of bool | VPair of value * value
               | closure of env * term
and      env   = empty | bnd of env * string * value;
    
exception  unbound_variable;

(* Lookup the value of a variable in the environment *)
fun lookup(x,empty) = raise unbound_variable
   |lookup(x,bnd(rho,y,v)) = if x=y then v else lookup(x,rho)
		
(* eval1 evaluates a term with respect to an environment *)
fun eval1 (rho, I n) = (VI n)
   |eval1 (rho, B b) = (VB b)
   |eval1 (rho, Var x) = lookup(x,rho)
   |eval1 (rho, Cond(e1,e2,e3)) = 
      let val (VB b) = eval1 (rho,e1)
      in eval1 (rho, if b then e2 else e3)
      end
   |eval1 (rho, Pair(e1,e2)) = VPair(eval1(rho,e1), eval1(rho,e2))
   |eval1 (rho, Fst e) =
      let val VPair(v1,v2) = eval1 (rho,e)
      in v1 end
   |eval1 (rho, Snd e) =
      let val VPair(v1,v2) = eval1 (rho,e)
      in v2 end
   |eval1 (rho,Abs(x,e)) = closure(rho,Abs(x,e))
   |eval1 (rho,Fix(f,Abs(x,e))) = closure(rho,(Fix(f,Abs(x,e))))
   |eval1 (rho,App(e1,e2)) =
      let  val v2 = eval1 (rho,e2)
      in case (eval1 (rho,e1)) of
         closure(rho',Abs(y,e')) => eval1 (bnd(rho',y,v2),e')
        |closure(rho',Fix(f,Abs(x,e'))) 
             => eval1 (bnd(bnd(rho',x,v2),f,closure(rho',Fix(f,Abs(x,e')))),e')
      end
   |eval1 (rho, Iszero e) =
      let val (VI n) = eval1 (rho,e)
      in VB (n=0) end
   |eval1 (rho,Succ e) =
      let val (VI n) = eval1 (rho,e)
      in  VI(n+1) end
   |eval1 (rho,Pred e) =
      let val (VI n) = eval1 (rho,e)
      in  VI(n-1) end;