From 02d40af51b0bf6ea346adf5856de5173a1540de1 Mon Sep 17 00:00:00 2001 From: Jim Date: Fri, 20 Mar 2015 19:27:57 -0400 Subject: [PATCH] refine untyped_evaluator --- code/untyped_evaluator.ml | 54 ++++++++++++++++++++++------------------------- 1 file changed, 25 insertions(+), 29 deletions(-) diff --git a/code/untyped_evaluator.ml b/code/untyped_evaluator.ml index 5323dcb9..d820cce9 100644 --- a/code/untyped_evaluator.ml +++ b/code/untyped_evaluator.ml @@ -3,22 +3,21 @@ You can use this code as follows: 1. First, use a text editor to fill in the uncompleted portions. - 2. Then see if OCaml will compile it, by typing `ocamlc -c simple.ml` in a Terminal. + 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`, - where DIRECTORY is the name of the folder that contains your `simple.ml` file. + where DIRECTORY is the name of the folder that contains your `untyped_evaluator.ml` file. (Alternatively, if OCaml is already started, you can type `#directory "DIRECTORY";;` - 5. Then once OCaml is started, you can either: (a) type `#load "simple.cmo";;`, then type - `open Simple;;` (this has to be on a separate line from step (a), it seems); - or (b) instead you can type `#use "simple.ml";;` - 6. Now you can try commands like `interpret (App(Lambda("x",Var "x"),Lambda("y",Var "y"))) empty` - Or V1.reduce (App(Lambda("x",Var "x"),Lambda("y",Var "y"))) empty` - Or V1.evaluate (App(Lambda("x",Var "x"),Lambda("y",Var "y"))) empty` + 5. Then once OCaml is started, you can either: (a) type `#load "untyped_evaluator.cmo";;`, then type + `open Untyped_evaluator;;` (this has to be on a separate line from step (a), it seems); + or (b) instead you can type `#use "untyped_evaluator.ml";;` + 6. Now you can try commands like: + `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. This simplified code just provides a single - implementation of environments; but the fuller code provides more. + the environments are essential. *) type identifier = string @@ -26,15 +25,20 @@ type identifier = string type term = | Var of identifier | App of term * term - | Lambda of identifier * term + | Lambda of identifier * term (* in V2, 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 *) | Closure of identifier * term * env +(* in the fuller code, we separate the term and result types *) and result = term +(* This simplified code just provides a single implementation of environments; + but the fuller code provides more. *) and env = identifier -> term option +(* Operations for environments *) let empty = fun _ -> None let push (ident : identifier) binding env = fun (sought_ident : identifier) -> @@ -47,14 +51,14 @@ let lookup sought_ident env = env sought_ident (* 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 `succ false`. The - reduction-based interpreter just signaled this with a normal - return value; but the environment- based interpreter uses an + reduction/evaluation is defined, such as `x y`. The + reduction-based 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 - the resources to print the term instead, as the full code does. + In this simplified version of the code, we also use this + exception to report a failed term in V1, since we lack + the resources to print the term instead, as the full code does. *) exception Stuck of term @@ -217,7 +221,6 @@ module V1 = struct | StuckAt _ as outcome -> outcome (* propagate Stuck subterm *) | ReducedTo head' -> ReducedTo (App(head', arg))) - let rec reduce (term : term) (env : env) = @@ -234,7 +237,6 @@ module V2 = struct function of results, using: val eval term -> env -> result, or may raise (Stuck term) val evaluate term -> env -> result - Now `env` contains local as well as toplevel bindings. *) let rec eval (term : term) (env : env) : result = @@ -245,7 +247,8 @@ module V2 = struct | Var var -> (match lookup var env with - (* the first case is different from V1.reduce_head_once *) + (* Free variables will never be pushed to the env, so we can be + sure this is a result. *) CHECK | Some res -> res | None -> failwith ("Unbound variable `" ^ var ^ "`")) @@ -284,13 +287,6 @@ module V2 = struct end (* module V2 *) +let reduce term = V1.reduce term empty +let evaluate term = V2.evaluate term empty -(* Put comment (* *)s around exactly one of the following two pairs of lines. *) - -let version = "version 1 (reduce by substituting)" -let interpret = V1.reduce - -(* -let version = "version 2 (use environment for local bindings)" -let interpret = V2.evaluate -*) -- 2.11.0