X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=code%2Funtyped_evaluator.ml;h=5ccecb50296b578f490b590f10dc97f85ec984a4;hp=5323dcb91e801d05e3e092da9b34dd017fb3d668;hb=061c0095bf19d1c00b53cd25d6b03a9b07ee2365;hpb=46af41468d114dba7d89b800df78fafcabe796dc diff --git a/code/untyped_evaluator.ml b/code/untyped_evaluator.ml index 5323dcb9..5ccecb50 100644 --- a/code/untyped_evaluator.ml +++ b/code/untyped_evaluator.ml @@ -1,24 +1,43 @@ (* - 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 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 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 @@ -26,39 +45,44 @@ type identifier = string type term = | Var of identifier | App of term * term - | Lambda of identifier * term + | 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 VB result *) | Closure of identifier * term * env +(* in the fuller code, we separate the term and result types *) and result = term -and env = identifier -> term option +(* This simplified code just provides a single implementation of environments; + but the fuller code provides more. *) +and env = (identifier * term) list -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 +(* Operations for environments *) +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 `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 + 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 - 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 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 @@ -109,11 +133,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 @@ -174,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 @@ -201,7 +225,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 +234,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 *)) @@ -226,15 +249,14 @@ 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: 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 +267,9 @@ module V2 = struct | Var var -> (match lookup var env with - (* the first case is different from V1.reduce_head_once *) + (* 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 ^ "`")) @@ -262,8 +286,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 +296,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)))) @@ -282,15 +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 = VA.reduce term empty +let evaluate term = VB.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 -*)