1. (*
2.   Reducers (interpreters) for lambda-calculus.
3. *)
4.  
5. open Utils
6. open Parser
7.  
8.  
9. exception OutOfVariablesError
10.  
11.  
12. let possible_variables = List.map (fun x -> char_to_string (char_of_int x)) ((range 97 123) @ (range 65 91))
13.  
14.  
15. let fresh_var used_vars : string =
16.   if StringSet.is_empty (StringSet.diff (string_set_from_list(possible_variables)) used_vars)
17.   then raise (OutOfVariablesError)
18.   else StringSet.choose (StringSet.diff (string_set_from_list(possible_variables)) used_vars)
19.  
20.  
21. let rec fv = fun t -> match t with
22.    | Variable(x) -> let set = StringSet.empty in
23.           StringSet.add x set in set
24.    | Abstraction(x, t) -> let set = fv t in
25.        StringSet.remove x set in set
26.    | Application(t1, t2) -> let set1 = fv t1 in let set2 = fv t2 in let unite = StringSet.union t1 t2 in unite;;
27.  
28. let extract_some = function
29.   | Some x -> x
30.  
31. let rec substitute x s = match s with
32.    | (s1, t) ->
33.     match t with
34.     | Variable(var) -> if x = var then s1 else t
35.     | Abstraction (var, t1) -> if x = var then t
36.           else
37.         let set = fv s1 in
38.         if StringSet.mem var set then
39.          let term_to_string = format_term_conv t1 in
40.          let unite = StringSet.union set term_to_string in
41.          let fresh = fresh_var unite in
42.          Abstraction (fresh, substitute x (s1, Abstraction (fresh, substitute var (fresh, t1))))
43.         else
44.          Abstraction (var, substitute x (s1,t1))
45.     | Application(t1, t2) -> Application (substitue x (s1, t1), substitue x (s1, t2));;
46.  
47.  
48. let rec reduce_cbv = fun term ->
49.    match term with
50.    | Abstraction (x, t1) -> Some(term)
51.    | Application (t1, t2) -> match t2 with
52.        | Abstraction (var, t) -> reduce_cbn (substitute var (t2, t))
53.        | Application (term1, term2) -> reduce_cbn t2
54.    | _ -> None
55.  
56. let rec reduce_cbn =  fun term ->
57.    match term with
58.    | Abstraction (x, t1) -> Some(term)
59.    | Application (t1, t2) -> match t1 with
60.        | Abstraction (var, t) -> reduce_cbn (substitute var (t2, t))
61.        | Application (term1, term2) -> reduce_cbn t1
62.    | _ -> None