(* ------------ set compiler output variable so we can see terms --------------*)
Compiler.Control.Print.printDepth := 50;

(* ------------ datatype of lambda terms and some sample terms ----------------*)
datatype term = 
     Var of int| 
     Const of int | 
     Lambda of int* term | 
     App of term * term |
     Plus of term * term;

val x = Var(1);
val y = Var(2);
val one = Const(1);
val two = Const(2);

val x_ = 1; (* to make lambda expressions easier to read *)
val y_ = 2;

val twice = Lambda(y_, Lambda(x_, App(y, App(y,x))));
val addx = Lambda(y_, Plus(y,x));
val test = App(twice,addx);

(* ------ substitution for free variable without renaming ---------*)

fun subst(t,x,Var(n)) = if x=n then t else Var(n)
|   subst(t,x,Const(n)) = Const(n)
|   subst(t,x,Lambda(n,t1)) = if x=n then (*-- missing part --*) 
                                     else (*-- missing part --*)
|   subst(t,x,App(t1,t2)) =  (*-- missing part --*)
|   subst(t,x,Plus(t1,t2)) = (*-- missing part --*)

(* ------ evaluation of expression using substitution -------------*)

fun ev(Var(n)) = Var(n)
|   ev(Const(n)) = Const(n)
|   ev(Lambda(n,t1)) = Lambda(n,ev(t1))
|   ev(App(t1,t2)) =  
        (case ev(t1) of
              Var(n) => App(Var(n),ev(t2))      |
            Const(n) => App(Const(n),ev(t2))    |
         Lambda(n,t) => (*-- missing part --*)  |
           App(t,t1) => App(App(t,t1),ev(t2))   |
          Plus(t,t1) => (*-- missing part --*)
|   ev(Plus(t1,t2)) =  
         case ev(t1) of
              Var(n) => Plus(Var(n),ev(t2))      |
            Const(n) => (case ev(t2) of
                        Var(m) => Plus(Const(n),Var(m))      |
                      Const(m) => (*-- missing part --*)     |
                   Lambda(m,t) =>  Plus(Const(n),Lambda(m,t))|
                     App(t3,t4) => (*-- missing part --*)    |
                    Plus(t3,t4) => Plus(Const(n),Plus(t3,t4)) )|
         Lambda(n,t) => Plus(Lambda(n,t),ev(t2)) |
           App(t,t1) => Plus(App(t,t1),ev(t2))   |  
          Plus(t,t1) => (*-- missing part --*)   ; 


(* ----- rename bound variables                         ----------*)

fun alpha(term) = ...

(* -------- define better eval function using renaming  ---------*)
          
fun eval(term) = ev(alpha(term));

ev test;
eval test;