X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=code%2Fski_evaluator.ml;h=11e8dd4ebd85a4794317052a7c39f8eaa3387eb6;hp=f0b4d1669e045bc2c7fee82ef0503ccc9e532be2;hb=0cb89c90973c0c5c74d7c3cfd929ca95946d44e4;hpb=6ee4185debd7b5401900080ace6d0445c08853f5

diff --git a/code/ski_evaluator.ml b/code/ski_evaluator.ml
index f0b4d166..11e8dd4e 100644
--- a/code/ski_evaluator.ml
+++ b/code/ski_evaluator.ml
@@ -21,12 +21,108 @@ let rec reduce_try2 (t:term):term = match t with
                             in reduce_try2 t''
                        else t'
 
-let rec reduce_lazy (t:term):term = match t with
+let rec reduce_try3 (t:term):term = match t with
   | I -> I
   | K -> K
   | S -> S
   | App (a, b) ->
-      let t' = App (reduce_lazy a, b) in
+      let t' = App (reduce_try3 a, b) in
       if (is_redex t') then let t'' = reduce_if_redex t'
-                            in reduce_lazy 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_try3 a, reduce_try 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 pattern-matching in the `reduce_head_once`
+    function.  Otherwise, the code now structurally parallels the
+    VA/substitute-and-repeat 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.
+
+*)