X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=code%2Funtyped_evaluator.ml;h=5ccecb50296b578f490b590f10dc97f85ec984a4;hp=d820cce91b40a7b3faee9e0d3e1f80fa584d3f88;hb=061c0095bf19d1c00b53cd25d6b03a9b07ee2365;hpb=02d40af51b0bf6ea346adf5856de5173a1540de1 diff --git a/code/untyped_evaluator.ml b/code/untyped_evaluator.ml index d820cce9..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 uncompleted 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 @@ -113,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 @@ -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 @@ -205,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'))) @@ -214,12 +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 *)) @@ -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 ^ "`")) @@ -265,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 @@ -276,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)))) @@ -285,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