X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=code%2Funtyped_evaluator.ml;h=5ccecb50296b578f490b590f10dc97f85ec984a4;hp=7af3eb43424db407a1bf24720841dbe67378efc1;hb=061c0095bf19d1c00b53cd25d6b03a9b07ee2365;hpb=45bfd0c44c531bd94e00b5a11285691c48062157

diff --git a/code/untyped_evaluator.ml b/code/untyped_evaluator.ml
index 7af3eb43..5ccecb50 100644
--- a/code/untyped_evaluator.ml
+++ b/code/untyped_evaluator.ml
@@ -1,8 +1,8 @@
 (*
-   This is a simplified version of the code at ...
+   This is a simplified version of the code at http://lambda.jimpryor.net/code/untyped_full-1.7.tgz
    You can use this code as follows:
 
-   1. First, use a text editor to fill in the (* COMPLETE THIS *) portions
+   1. First, use a text editor to fill in the (* COMPLETE THIS *) portions.
    2. Then see if OCaml will compile it, by typing `ocamlc -c untyped_evaluator.ml` in a Terminal.
    3. If it doesn't work, go back to step 1.
    4. If it does work, then you can start up the OCaml toplevel using `ocaml -I DIRECTORY`,
@@ -15,9 +15,29 @@
       `reduce (App(Lambda("x",Var "x"),Lambda("y",Var "y")))`
       `evaluate (App(Lambda("x",Var "x"),Lambda("y",Var "y")))`
 
-   The environments play absolutely no role in this simplified V1 interpreter. In the
-   fuller code, they have a limited role in the V1 interpreter. In the V2 interpreter,
-   the environments are essential.
+   The two interpreters presented below are (VersionA) a substitute-and-repeat
+   interpreter, and (VersionB) an environment-based interpreter. We discuss the
+   differences between these in the course notes.
+
+   The implementeations we provide make both of these call-by-value. When given
+   a term `App(head, arg)`, the steps are: first, reduce or evaluate
+   `head`---it might involve further `App`s itself. Second, reduce or evaluate
+   `arg`.  Third, only _when_ `arg` reduces or evaluates to a result value, then
+   "perform" the application. What this last step amounts to is different in
+   the two interpreters. Call-by-name interpreters would "perform" the
+   application regardless, and without even trying to reduce or evaluate arg to
+   a result value beforehand.
+
+   Additionally, these implementations assume that free variables are "stuck"
+   terms rather than result values. That is a bit inconvenient with this
+   simplified program: it means that Lambdas (or Closures, in VB) are the only
+   result values. But in the fuller code from which this is simplified, it
+   makes more sense, because there we also have literal number and boolean
+   values as results, too.
+
+   The environments play absolutely no role in the simplified VA interpreter
+   presented here. In the fuller code, they have a limited role in the VA
+   interpreter. In the VB interpreter, the environments are essential.
 *)
 
 type identifier = string
@@ -25,10 +45,10 @@ type identifier = string
 type term =
   | Var of identifier
   | App of term * term
-  | Lambda of identifier * term (* in V2, never used as a result *)
+  | Lambda of identifier * term (* in VB, never used as a result *)
   | Let of identifier * term * term
   | If of term * term * term
-  (* the following variant is never used as a term, only as a V2 result *)
+  (* the following variant is never used as a term, only as a VB result *)
   | Closure of identifier * term * env
 
 (* in the fuller code, we separate the term and result types *)
@@ -36,33 +56,33 @@ and result = term
 
 (* This simplified code just provides a single implementation of environments;
    but the fuller code provides more. *)
-and env = identifier -> term option
+and env = (identifier * term) list
 
 (* Operations for environments *)
-let empty = fun _ -> None
-let push (ident : identifier) binding env =
-  fun (sought_ident : identifier) ->
-    if ident = sought_ident
-    then Some binding
-    else env sought_ident
-let lookup sought_ident env = env sought_ident
+let empty = []
+let shift (ident : identifier) binding env = (ident,binding) :: env
+let rec lookup (sought_ident : identifier) (env : env) : term option =
+  match env with
+  | [] -> None
+  | (ident, binding) :: _ when ident = sought_ident -> Some binding
+  | _ :: env' -> lookup sought_ident env'
 
   
 (*
    eval raises this exception when it fails to reduce/evaluate
    a term, because it has components for which no
    reduction/evaluation is defined, such as `x y`. The
-   reduction-based interpreter just signals this with a normal
+   substitute-and-repeat interpreter just signals this with a normal
    return value; but the environment-based interpreter uses an
    exception to abort prematurely.
 
    In this simplified version of the code, we also use this
-   exception to report a failed term in V1, since we lack
+   exception to report a failed term in VA, since we lack
    the resources to print the term instead, as the full code does.
 *)
 exception Stuck of term
 
-module V1 = struct
+module VA = struct
   (* ---------------------------------------------------------------
      Interpreter that reduces by substituting, using:
          val reduce_head_once : term -> env -> reduceOutcome
@@ -178,7 +198,7 @@ module V1 = struct
     | Lambda _ -> AlreadyResult term
   
     | Var var -> failwith ("Unbound variable `" ^ var ^ "`")
-    | Closure _ -> assert false (* no Closures in V1 *)
+    | Closure _ -> assert false (* no Closures in VA *)
   
 (* In this simplified version there are no Bool Literals, so If terms are always stuck
     | If(Literal(Bool true),yes,no) -> ReducedTo yes
@@ -229,9 +249,9 @@ module V1 = struct
     | StuckAt subterm -> raise (Stuck subterm)
     | ReducedTo term' -> reduce term' env (* keep trying *)
 
-end (* module V1 *)
+end (* module VA *)
 
-module V2 = struct
+module VB = struct
   (* ---------------------------------------------------------------
      Interpreter that employs an "environment" or assignment
      function of results, using:
@@ -247,8 +267,9 @@ module V2 = struct
 
     | Var var ->
         (match lookup var env with
-        (* Free variables will never be pushed to the env, so we can be
-	   sure this is a result. *) CHECK
+	(* In this call-by-value design, only results get
+	   saved in the environment, so we can be sure this
+	   is a result. *)
         | Some res -> res
         | None -> failwith ("Unbound variable `" ^ var ^ "`"))
 
@@ -283,8 +304,8 @@ module V2 = struct
   let evaluate (term : term) (env : env) : result =
     eval term env (* in the fuller code, this function catches the Stuck errors and prints them more nicely *)
 
-end (* module V2 *)
+end (* module VB *)
 
-let reduce term = V1.reduce term empty
-let evaluate term = V2.evaluate term empty
+let reduce term = VA.reduce term empty
+let evaluate term = VB.evaluate term empty