added code

diff --git a/code/ski_evaluator.hs b/code/ski_evaluator.hs
new file mode 100644 (file)
index 0000000..845d6da
--- /dev/null
+++ b/code/ski_evaluator.hs
@@ -0,0 +1,24 @@
+data Term = I | S | K | FA Term Term deriving (Eq, Show)      
+                                                              
+skomega = (FA (FA (FA S I) I) (FA (FA S I) I))                      
+test = (FA (FA K I) skomega)
+                                                              
+reduce_one_step :: Term -> Term                                      
+reduce_one_step t = case t of                                      
+  FA I a -> a                                                      
+  FA (FA K a) b -> a                                              
+  FA (FA (FA S a) b) c -> FA (FA a c) (FA b c)                      
+  _ -> t                                                      
+                                                              
+is_redex :: Term -> Bool                                      
+is_redex t = not (t == reduce_one_step t)                      
+                                                              
+reduce :: Term -> Term                                              
+reduce t = case t of                                              
+  I -> I                                                      
+  K -> K                                                      
+  S -> S                                                      
+  FA a b ->                                                       
+    let t' = FA (reduce a) (reduce b) in                      
+      if (is_redex t') then reduce (reduce_one_step t')      
+                       else t'                                

diff --git a/code/ski_evaluator.ml b/code/ski_evaluator.ml
new file mode 100644 (file)
index 0000000..10d130e
--- /dev/null
+++ b/code/ski_evaluator.ml
@@ -0,0 +1,30 @@
+type term = I | S | K | FA of (term * term)                    
+                                                               
+let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))                
+let test = FA (FA (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))                       
+  | _ -> t                                                     
+                                                               
+let is_redex (t:term):bool = not (t = reduce_one_step t)        
+                                                                      
+let rec reduce_eager (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')     
+                         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                      
+        if (is_redex t') then reduce_lazy (reduce_one_step t')     
+                         else t'