-type term = I | S | K | FA of (term * term)
+type term = I | S | K | App of (term * term)
-let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))
-let test = FA (FA (K,I), skomega)
+let skomega = App (App (App (S,I), I), App (App (S,I), I))
+let test = App (App (K,I), skomega)
let reduce_one_step (t:term):term = match t with
- FA(I,a) -> a
- | FA(FA(K,a),b) -> a
- | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))
+ App(I,a) -> a
+ | App(App(K,a),b) -> a
+ | App(App(App(S,a),b),c) -> App(App(a,c),App(b,c))
| _ -> t
let is_redex (t:term):bool = not (t = reduce_one_step t)
-let rec reduce_eager (t:term):term = match t with
+let rec reduce (t:term):term = match t with
I -> I
| K -> K
| S -> S
- | FA (a, b) ->
- let t' = FA (reduce_eager a, reduce_eager b) in
- if (is_redex t') then reduce_eager (reduce_one_step t')
+ | App (a, b) ->
+ let t' = App (reduce a, reduce b) in
+ if (is_redex t') then reduce (reduce_one_step t')
else t'
let rec reduce_lazy (t:term):term = match t with
I -> I
| K -> K
| S -> S
- | FA (a, b) ->
- let t' = FA (reduce_lazy a, b) in
+ | App (a, b) ->
+ let t' = App (reduce_lazy a, b) in
if (is_redex t') then reduce_lazy (reduce_one_step t')
else t'