(* Increase the print depth to see deeply nested
   structure *)

Control.Print.printDepth := 100; 

infixr -->


datatype type_exp = integer | boolean | listtype of type_exp | 
                     --> of type_exp * type_exp | typevar of string



datatype exp = constant_int of int  | 
               constant_bool of bool  |
               variable of string  | 
               alist of exp list  |
               lambda of string * exp  | 
               letdef of (string * exp) list * exp | 
               cond of exp * exp * exp  |
               application of exp * exp 


type substitution = (string * type_exp) list

fun replace_var v [] = typevar v
 |  replace_var v ((x,value)::rest) = if v = x then value
				       else replace_var v rest

fun apply_sub theta (typevar v) = replace_var v theta
 |  apply_sub theta (listtype t) = listtype (apply_sub theta t)
 |  apply_sub theta (t1 --> t2) = (apply_sub theta t1) --> (apply_sub theta t2)
 |  apply_sub _ exp = exp


fun substitute v new (typevar q) = if v = q then new else (typevar q)
 |  substitute v new  (listtype t) = listtype (substitute v new t)
 |  substitute v new  (t1 --> t2) = (substitute v new t1) -->
                                    (substitute v new t2)
 |  substitute _ _ t = t

fun member v (typevar w) = if v = w then true else false
 |  member v (p --> q) = member v p orelse member v q
 |  member v (listtype t) = member v t
 |  member _ _ = false

exception unify_failure

fun unify [] theta = theta 
  | unify ((typevar(v),exp)::rest) theta =
      if exp = typevar(v) then unify rest theta
      else if member v exp then
         raise unify_failure 
      else 
       let val new_rest = 
             map (fn (l,r) =>(substitute v exp l, substitute v exp r)) rest
           val new_theta = 
	     map (fn (name,def) => (name,substitute v exp def)) theta
       in
         unify new_rest ((v,exp)::new_theta)
       end	
  | unify ((exp,typevar(v))::rest)theta = unify((typevar(v),exp)::rest) theta
  | unify ((t1-->t2,t3-->t4)::rest) theta =
      unify ((t1,t3)::(t2,t4)::rest) theta
  | unify ((listtype t1, listtype t2)::rest) theta =
        unify ((t1,t2)::rest) theta
  | unify ((t1,t2)::rest) theta = if t1 = t2 then unify rest theta
                                  else raise unify_failure