X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=code%2Fski_evaluator.ml;h=742d63d17b45d39bd3d9b1ec4c400e300cd0c320;hp=4d6f9a122aef7da22ab444970690c03f7bc9f6e7;hb=d2cd63fe26f3777ee6fb7a6005bf28e30c0381f0;hpb=ff5b3f5a76fb744b332bc5d0fb3ef5632ce02879

diff --git a/code/ski_evaluator.ml b/code/ski_evaluator.ml
index 4d6f9a12..742d63d1 100644
--- a/code/ski_evaluator.ml
+++ b/code/ski_evaluator.ml
@@ -1,30 +1,32 @@
-type term = I | S | K | App of (term * term)                    
-                                                               
-let skomega = App (App (App (S,I), I), App (App (S,I), I))                
+type term = I | S | K | App of (term * term)
+
+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                    
-    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 (t:term):term = match t with                        
-    I -> I                                                     
-  | K -> K                                                     
-  | S -> S                                                     
-  | 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                                                     
-  | App (a, b) ->                                                   
-      let t' = App (reduce_lazy a, b) in                      
-        if (is_redex t') then reduce_lazy (reduce_one_step t')     
-                         else t'                               
+let reduce_if_redex (t:term):term = match t with
+  | 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_if_redex t)
+
+let rec reduce_try2 (t:term):term = match t with
+  | I -> I
+  | K -> K
+  | S -> S
+  | App (a, b) ->
+      let t' = App (reduce_try2 a, reduce_try2 b) in
+      if (is_redex t') then let t'' = reduce_if_redex t'
+                            in reduce_try2 t''
+                       else t'
+
+let rec reduce_try3 (t:term):term = match t with
+  | I -> I
+  | K -> K
+  | S -> S
+  | App (a, b) ->
+      let t' = App (reduce_try3 a, b) in
+      if (is_redex t') then let t'' = reduce_if_redex t'
+                            in reduce_try3 t''
+                       else t'