# type term = Var of string 
            | Abs of (string * term) 
            | App of term * term;;

# let id = Abs("x",Var "x");;
# let k = Abs("x",Abs("y",Var "x"));;
# let omega = App(Abs("x",App(Var "x",Var "x")),Abs("x",App(Var "x",Var "x")));;
# let const z = Abs("x",Var z);;

# let rec string_of_term t = match t with
    Var x -> x
  | Abs (x,t') -> "\\" ^ x ^ "." ^ string_of_term t'
  | App (t0,t1) -> "(" ^ (string_of_term t0) ^ " " ^ (string_of_term t1) ^ ")";;

# print_string (string_of_term id);;
# print_string (string_of_term k);;
# print_string (string_of_term omega);;

# type 'a set = Set of 'a list;;
 
# let emptyset = Set [];;
 
# let rec member x s = match s with
    Set [] -> false
  | Set (y::s') -> x=y or (member x (Set s'));;
 
# let rec union s t = match s with
    Set [] -> t
  | Set (x::s') -> (match union (Set s') t with Set t' ->
      if member x t then Set t' else Set (x::t'));;
 
# let rec diff s x = match s with
    Set [] -> s
  | Set (y::s') -> (match diff (Set s') x with Set t' ->
      if x=y then Set s' else Set (y::t'));;

# let rec fv t = match t with
    Var x -> Set [x]
  | App(t0,t1) -> union (fv t0) (fv t1)
  | Abs(x,t0) -> diff (fv t0) x;;

# fv omega;;
# fv (const "z");;
# fv (Abs ("x", App(Var "x",Var "y")));;

# let count = ref(-1);;
# let gensym = fun () -> count := !count +1; "x" ^ string_of_int (!count);;
 
# let rec subst x t' t = match t with
    Var y -> if x=y then t' else Var y
  | App(t0,t1) -> App(subst x t' t0, subst x t' t1)
  | Abs(y,t0) when y=x -> Abs(x,t0)
  | Abs(y,t0) when y!=x && not (member y (fv t')) -> Abs(y, subst x t' t0)
  | Abs(y,t0) when y!=x && member y (fv t') -> 
      let z = gensym() in Abs(z,subst x t' (subst z (Var y) t0));;

# let isredex t = match t with 
    App(Abs(x,t0),t1) -> true
  | _ -> false;;
 
# let rec hasredex t = match t with 
    Var x -> false
  | Abs(x,t') -> hasredex t'
  | App(t0,t1) -> isredex t or hasredex t0 or hasredex t1;;
 
# exception Error;;
 
# let rec reduce1 t = if not (hasredex t) then t else match t with
    Abs(x,t') -> Abs(x,reduce1 t')
  | App(Abs(x,t0),t1) -> subst x t1 t0 
  | App(t0,t1) -> if hasredex t0 then App(reduce1 t0,t1) else App(t0,reduce1 t1);;
 
# let rec reduce t k = if k=0 then t else let t' = reduce1 t in reduce t' (k-1);;
 
# let rec reducefix t = let t' = reduce1 t in if t'=t then t' else reducefix t';;
 
# reduce (App((const "z"),omega)) 1;;