(*
  Reducers (interpreters) for lambda-calculus.
*)

open Utils
open Parser


exception OutOfVariablesError


let possible_variables = List.map (fun x -> char_to_string (char_of_int x)) ((range 97 123) @ (range 65 91))


let fresh_var used_vars : string = 
  if StringSet.is_empty (StringSet.diff (string_set_from_list(possible_variables)) used_vars) 
  then raise (OutOfVariablesError)
  else StringSet.choose (StringSet.diff (string_set_from_list(possible_variables)) used_vars)


let rec fv = fun t -> match t with
   | Variable(x) -> let set = StringSet.empty in
          StringSet.add x set in set
   | Abstraction(x, t) -> let set = fv t in
       StringSet.remove x set in set
   | Application(t1, t2) -> let set1 = fv t1 in let set2 = fv t2 in let unite = StringSet.union t1 t2 in unite;;

let extract_some = function
  | Some x -> x 

let rec substitute x s = match s with
   | (s1, t) ->
    match t with
    | Variable(var) -> if x = var then s1 else t
    | Abstraction (var, t1) -> if x = var then t 
          else
        let set = fv s1 in
        if StringSet.mem var set then
         let term_to_string = format_term_conv t1 in
         let unite = StringSet.union set term_to_string in
         let fresh = fresh_var unite in
         Abstraction (fresh, substitute x (s1, Abstraction (fresh, substitute var (fresh, t1))))
        else
         Abstraction (var, substitute x (s1,t1))
    | Application(t1, t2) -> Application (substitue x (s1, t1), substitue x (s1, t2));;


let rec reduce_cbv = fun term ->
   match term with
   | Abstraction (x, t1) -> Some(term)
   | Application (t1, t2) -> match t2 with
       | Abstraction (var, t) -> reduce_cbn (substitute var (t2, t))
       | Application (term1, term2) -> reduce_cbn t2
   | _ -> None

let rec reduce_cbn =  fun term ->
   match term with
   | Abstraction (x, t1) -> Some(term)
   | Application (t1, t2) -> match t1 with
       | Abstraction (var, t) -> reduce_cbn (substitute var (t2, t))
       | Application (term1, term2) -> reduce_cbn t1
   | _ -> None