X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=code%2Funtyped_evaluator.ml;h=cf2a1b415f3dc1a822588c756af6acd98d0ba80d;hp=5323dcb91e801d05e3e092da9b34dd017fb3d668;hb=e62e212f2cbd9d7a3468d5531a15fa1023ec14a6;hpb=e1626ef4172d63a6bd74cbd8ab0fe56bb8ef8775 diff --git a/code/untyped_evaluator.ml b/code/untyped_evaluator.ml index 5323dcb9..cf2a1b41 100644 --- a/code/untyped_evaluator.ml +++ b/code/untyped_evaluator.ml @@ -2,23 +2,22 @@ This is a simplified version of the code at ... 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. + 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`, - 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 @@ -109,11 +113,11 @@ module V1 = struct | Var(var_ident) -> var_ident = ident | App(head, arg) -> - free_in ident head || free_in ident arg + (* COMPLETE THIS *) | Lambda(bound_ident, body) -> - bound_ident <> ident && free_in ident body + (* COMPLETE THIS *) | Let(bound_ident, arg, body) -> - free_in ident arg || (bound_ident <> ident && free_in ident body) + free_in ident arg || (* COMPLETE THIS *) | If(test, yes, no) -> free_in ident test || free_in ident yes || free_in ident no | Closure _ -> assert false @@ -201,7 +205,7 @@ module V1 = struct (match reduce_head_once arg env with | AlreadyResult _ -> (* if arg was not reducible, we can substitute *) - ReducedTo (substitute bound_var arg body) + (* COMPLETE THIS *) | StuckAt _ as outcome -> outcome (* propagate Stuck subterm *) | ReducedTo arg' -> ReducedTo (App(head, arg'))) @@ -210,13 +214,12 @@ module V1 = struct (match reduce_head_once head env with | AlreadyResult _ -> (* head was not reducible, was arg? *) (match reduce_head_once arg env with - | ReducedTo arg' -> ReducedTo (App(head, arg')) + | ReducedTo arg' -> (* COMPLETE THIS *) (* reducible cases of App(result, result) were caught above; so here we're stuck *) | AlreadyResult _ -> StuckAt term | StuckAt _ as outcome -> outcome) (* propagate Stuck subterm *) | StuckAt _ as outcome -> outcome (* propagate Stuck subterm *) - | ReducedTo head' -> ReducedTo (App(head', arg))) - + | ReducedTo head' -> (* COMPLETE THIS *)) @@ -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. *) | Some res -> res | None -> failwith ("Unbound variable `" ^ var ^ "`")) @@ -262,8 +265,7 @@ module V2 = struct bound to the result of evaluating arg under the current env *) let arg' = eval arg env in - let env' = push bound_var arg' env in - eval body env' + let env' = (* COMPLETE THIS *) | App(head, arg) -> (match eval head env with @@ -273,8 +275,7 @@ module V2 = struct (* evaluate body under saved_env to govern its free variables, except that we add a binding of bound_var to arg' *) - let saved_env' = push bound_var arg' saved_env in - eval body saved_env' + let saved_env' = (* COMPLETE THIS *) | head' -> raise (Stuck(App(head',arg)))) @@ -284,13 +285,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 -*)