exx
[lambda.git] / code / ski_evaluator.ml
index 5e23ff9..4d6f9a1 100644 (file)
@@ -1,12 +1,12 @@
-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)        
@@ -15,8 +15,8 @@ let rec reduce (t:term):term = match t with
     I -> I                                                     
   | K -> K                                                     
   | S -> S                                                     
-  | FA (a, b) ->                                                   
-      let t' = FA (reduce a, reduce b) in                      
+  | App (a, b) ->                                                   
+      let t' = App (reduce a, reduce b) in                      
         if (is_redex t') then reduce (reduce_one_step t')     
                          else t'                               
 
@@ -24,7 +24,7 @@ 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'