From c802743d4972249bbeb4648717784250bc5b1360 Mon Sep 17 00:00:00 2001 From: Chris Date: Sat, 14 Mar 2015 08:24:35 -0400 Subject: [PATCH] added code --- code/ski_evaluator.hs | 24 ++++++++++++++++++++++++ code/ski_evaluator.ml | 30 ++++++++++++++++++++++++++++++ 2 files changed, 54 insertions(+) create mode 100644 code/ski_evaluator.hs create mode 100644 code/ski_evaluator.ml 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' diff --git a/code/ski_evaluator.ml b/code/ski_evaluator.ml new file mode 100644 index 00000000..10d130e0 --- /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' -- 2.11.0