author Jim Thu, 19 Mar 2015 03:41:12 +0000 (23:41 -0400) committer Jim Thu, 19 Mar 2015 03:41:12 +0000 (23:41 -0400)
 code/ski_evaluator.hs patch | blob | history code/ski_evaluator.ml patch | blob | history

index 26f1c0e..348b216 100644 (file)
@@ -1,24 +1,24 @@
-data Term = I | S | K | App Term Term deriving (Eq, Show)
-
-skomega = (App (App (App S I) I) (App (App S I) I))
+data Term = I | S | K | App Term Term deriving (Eq, Show)
+
+skomega = (App (App (App S I) I) (App (App S I) I))
test = (App (App K I) skomega)
test = (App (App K I) skomega)
-
-reduce_one_step :: Term -> Term
-reduce_one_step t = case t of
-  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
-
-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
-  App a b ->
-    let t' = App (reduce a) (reduce b) in
-      if (is_redex t') then reduce (reduce_one_step t')
-                       else t'
+
+reduce_if_redex :: Term -> Term
+reduce_if_redex t = case t of
+  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
+
+is_redex :: Term -> Bool
+is_redex t = not (t == reduce_if_redex t)
+
+reduce_try2 :: Term -> Term
+reduce_try2 t = case t of
+  I -> I
+  K -> K
+  S -> S
+  App a b ->
+    let t' = App (reduce_try2 a) (reduce_try2 b) in
+      if (is_redex t') then reduce_try2 (reduce_if_redex t')
+                       else t'
index 4d6f9a1..15ee4a7 100644 (file)
@@ -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 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_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 let t'' = reduce_if_redex t'
+                            in reduce_lazt t''
+                       else t'