X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?a=blobdiff_plain;ds=sidebyside;f=code%2Fski_evaluator.hs;fp=code%2Fski_evaluator.hs;h=845d6dad8bd17ac613d13b2b30b50bce8ecc81a6;hb=6eb94b1b0c2bd030c11a3da469e769faa5ada8d9;hp=0000000000000000000000000000000000000000;hpb=fce00a47baedac4f4b00119179c8e04e5dd708ac;p=lambda.git

diff --git a/code/ski_evaluator.hs b/code/ski_evaluator.hs
new file mode 100644
index 00000000..845d6dad
--- /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'