XGitUrl: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=code%2Fski_evaluator.ml;h=727a84a5f2c084c5b2efbb6eee6fed231a0a93a1;hp=5e23ff9af0eb0d1f86271e13d31ef32e59801ae2;hb=15cd3aa71d183a77137b122f09d6f0a023d1043c;hpb=4aea3a471f66d67fccff34189186f8cdb561dd68
diff git a/code/ski_evaluator.ml b/code/ski_evaluator.ml
index 5e23ff9a..727a84a5 100644
 a/code/ski_evaluator.ml
+++ b/code/ski_evaluator.ml
@@ 1,30 +1,128 @@
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'

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'
+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_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'
+
+(* To make this closer to the untyped lambda interpreter, we'd need to:
+
+1. Change the method by which we detect/report if a term is reducible, as
+ follows:
+
+ (* Since there's no Stuck variant, and we don't return anything with
+ the Already... variant, this type is isomorphic to `None  Some
+ term`, and we could just use that. However, we'll use this custom
+ type to emphasize the parallels with the untyped interpreter. *)
+ type reduceOutcome = AlreadyReduced  ReducedTo of term
+
+ let reduce_if_redex (t : term) : reduceOutcome = match t with
+  App(I,a) > ReducedTo a
+  App(App(K,a),b) > ReducedTo a
+  App(App(App(S,a),b),c) > ReducedTo (App(App(a,c),App(b,c)))
+  _ > AlreadyReduced
+
+ let rec reduce_try4 (t : term) : term = match t with
+  I > I
+  K > K
+  S > S
+  App(a, b) >
+ let t' = App(reduce_try4 a, reduce_try4 b) in
+ (match reduce_if_redex t' with
+  ReducedTo t'' > reduce_try4 t''
+  AlreadyReduced > t')
+
+2. Shift the responsibilities between the looping function `reduce` and the
+ reducing function, so that the latter now calls itself recursively trying
+ to find a suitable redex, until it can perform one reduction.
+
+ type reduceOutcome = AlreadyReduced  ReducedTo of term
+
+ let rec reduce_once (t : term) : reduceOutcome = match t with
+  App(a, b) > (match reduce_once a with
+  ReducedTo a' > ReducedTo (App(a',b))
+  AlreadyReduced > (match reduce_once b with
+  ReducedTo b' > ReducedTo (App(a,b'))
+  AlreadyReduced >
+ (* here we have the old functionality of reduce_if_redex *)
+ (match t with
+  App(I,a) > ReducedTo a
+  App(App(K,a),b) > ReducedTo a
+  App(App(App(S,a),b),c) > ReducedTo (App(App(a,c),App(b,c)))
+  _ > AlreadyReduced)))
+  _ > AlreadyReduced
+
+ let rec reduce_try5 (t : term) : term = match reduce_once t with
+  ReducedTo t'> reduce_try5 t'
+  AlreadyReduced > t
+
+3. Finally, the untyped interpreter only performs reductions in (possibly
+ embedded) _head_ positions. By contrast, the (eager) combinatory
+ interpeters above wlll reduce `K (I I)` to `K I`. To make these
+ interpreters also (eagerly) reduce only head redexes, let's bring back an
+ `is_redex` function:
+
+ type reduceOutcome = AlreadyReduced  ReducedTo of term
+
+ let is_redex (t : term) : bool = match t with
+  App(I,_) > true
+  App(App(K,_),_) > true
+  App(App(App(S,_),_),_) > true
+  _ > false
+
+ let rec reduce_head_once (t : term) : reduceOutcome = match t with
+  App(a, b) > (match reduce_head_once a with
+  ReducedTo a' > ReducedTo (App(a',b))
+ (* now we only try to reduce b when App(a,b) is a redex *)
+  AlreadyReduced when is_redex t > (match reduce_head_once b with
+  ReducedTo b' > ReducedTo (App(a,b'))
+  AlreadyReduced >
+ (* old functionality of reduce_if_redex *)
+ (match t with
+  App(I,a) > ReducedTo a
+  App(App(K,a),b) > ReducedTo a
+  App(App(App(S,a),b),c) > ReducedTo (App(App(a,c),App(b,c)))
+  _ > AlreadyReduced))
+ (* else leave b as it is *)
+  _ > AlreadyReduced)
+  _ > AlreadyReduced
+
+ let rec reduce_try6 (t : term) : term = match reduce_head_once t with
+  ReducedTo t'> reduce_try6 t'
+  AlreadyReduced > t
+
+4. In the untyped interpreter, there is no separate `is_redex` function. That
+ check is embedded into the patternmatching in the `reduce_head_once`
+ function. Otherwise, the code now structurally parallels the
+ VA/substituteandrepeat strategy of the untyped interpreter. The remaining
+ differences have to do with the shift from combinatory logic to the lambda
+ calculus, tracking free variables, the complexities of substitution, and so
+ on.
+
+*)