X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=code%2Fski_evaluator.ml;h=4d6f9a122aef7da22ab444970690c03f7bc9f6e7;hp=10d130e08f9e9d3006a846bffacbdcb2b2cb4fae;hb=9c4caef33bf49319c09bf0b39a29ba43f8be1a10;hpb=c802743d4972249bbeb4648717784250bc5b1360 diff --git a/code/ski_evaluator.ml b/code/ski_evaluator.ml index 10d130e0..4d6f9a12 100644 --- a/code/ski_evaluator.ml +++ b/code/ski_evaluator.ml @@ -1,30 +1,30 @@ -type term = I | S | K | FA of (term * term) +type term = I | S | K | App of (term * term) -let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I)) -let test = FA (FA (K,I), skomega) +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 - FA(I,a) -> a - | FA(FA(K,a),b) -> a - | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c)) + 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_eager (t:term):term = match t with +let rec reduce (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') + | 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 - | FA (a, b) -> - let t' = FA (reduce_lazy a, b) in + | App (a, b) -> + let t' = App (reduce_lazy a, b) in if (is_redex t') then reduce_lazy (reduce_one_step t') else t'