hw6

[lambda.git] / code / ski_evaluator.hs

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'