X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=code%2Fski_evaluator.ml;h=742d63d17b45d39bd3d9b1ec4c400e300cd0c320;hp=5e23ff9af0eb0d1f86271e13d31ef32e59801ae2;hb=d2cd63fe26f3777ee6fb7a6005bf28e30c0381f0;hpb=ad7fea353514a45be62c56bbc9f8df266db0266b diff --git a/code/ski_evaluator.ml b/code/ski_evaluator.ml index 5e23ff9a..742d63d1 100644 --- a/code/ski_evaluator.ml +++ b/code/ski_evaluator.ml @@ -1,30 +1,32 @@ -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 (t:term):term = match t with - 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' +type term = I | S | K | App of (term * term) -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' +let skomega = App (App (App (S,I), I), App (App (S,I), I)) +let test = App (App (K,I), skomega) + +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_try3 (t:term):term = match t with + | I -> I + | K -> K + | S -> S + | App (a, b) -> + let t' = App (reduce_try3 a, b) in + if (is_redex t') then let t'' = reduce_if_redex t' + in reduce_try3 t'' + else t'