From 7ea03edf218ad5b63cd7ee0faa33391e1f3893ae Mon Sep 17 00:00:00 2001 From: Jim Date: Wed, 18 Mar 2015 23:41:12 -0400 Subject: [PATCH 1/1] update ski_evaluators --- code/ski_evaluator.hs | 46 ++++++++++++++++++++-------------------- code/ski_evaluator.ml | 58 ++++++++++++++++++++++++++------------------------- 2 files changed, 53 insertions(+), 51 deletions(-) diff --git a/code/ski_evaluator.hs b/code/ski_evaluator.hs index 26f1c0e6..348b216f 100644 --- a/code/ski_evaluator.hs +++ b/code/ski_evaluator.hs @@ -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) - -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' diff --git a/code/ski_evaluator.ml b/code/ski_evaluator.ml index 4d6f9a12..15ee4a77 100644 --- a/code/ski_evaluator.ml +++ b/code/ski_evaluator.ml @@ -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 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' -- 2.11.0