From 45bfd0c44c531bd94e00b5a11285691c48062157 Mon Sep 17 00:00:00 2001 From: Jim Date: Fri, 20 Mar 2015 19:32:22 -0400 Subject: [PATCH] provide gappy untyped_evaluator.ml --- code/untyped_evaluator.ml | 20 ++- code/untyped_evaluator_complete.ml | 292 +++++++++++++++++++++++++++++++++++++ 2 files changed, 301 insertions(+), 11 deletions(-) create mode 100644 code/untyped_evaluator_complete.ml diff --git a/code/untyped_evaluator.ml b/code/untyped_evaluator.ml index d820cce9..7af3eb43 100644 --- a/code/untyped_evaluator.ml +++ b/code/untyped_evaluator.ml @@ -2,7 +2,7 @@ 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. + 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`, @@ -113,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 @@ -205,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'))) @@ -214,12 +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 *)) @@ -265,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 @@ -276,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)))) diff --git a/code/untyped_evaluator_complete.ml b/code/untyped_evaluator_complete.ml new file mode 100644 index 00000000..90862058 --- /dev/null +++ b/code/untyped_evaluator_complete.ml @@ -0,0 +1,292 @@ +(* + 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 (* 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 `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 "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. +*) + +type identifier = string + +type term = + | Var of identifier + | App of term * 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) -> + if ident = sought_ident + then Some binding + else env sought_ident +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 `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. +*) +exception Stuck of term + +module V1 = struct + (* --------------------------------------------------------------- + Interpreter that reduces by substituting, using: + val reduce_head_once : term -> env -> reduceOutcome + val reduce : term -> env -> result + + reduce_head_once is similiar to reduce_if_redex in the + combinatory logic interpreter, except that the latter only + performed a reduction if its argument was exactly a redex. + It had to rely on its caller to detect cases where the term + was instead a longer sequence of applications that had a + redex at its head. In the present code, on the other hand, + we have reduce_head_once take care of this itself, by + calling itself recursively where appropriate. Still, it will + only perform at most one reduction per invocation. + *) + + + (* Search term and find a variable that isn't used in it, + either free or bound. We do this by appending primes to base + until we find an unused or "fresh" variable. *) + let fresh_var (base : identifier) (term : term) : identifier = + let rec aux term vars = + match term with + | Var(var_ident) -> + var_ident :: vars + | App(head, arg) -> + let vars' = aux head vars in + aux arg vars' + | Lambda(bound_ident, body) -> + aux body (bound_ident :: vars) + | Let(bound_ident, arg, body) -> + let vars' = aux arg vars in + aux body (bound_ident :: vars') + | If(test, yes, no) -> + let vars' = aux test vars in + let vars'' = aux yes vars' in + aux no vars'' + | Closure _ -> assert false in + let used_vars = aux term [] in + let rec check ident = + if List.mem ident used_vars + then check (ident ^ "'") + else ident in + check (base ^ "'") + + let rec free_in (ident : identifier) (term : term) : bool = + match term with + | Var(var_ident) -> + var_ident = ident + | App(head, arg) -> + free_in ident head || free_in ident arg + | Lambda(bound_ident, body) -> + bound_ident <> ident && free_in ident body + | Let(bound_ident, arg, body) -> + free_in ident arg || (bound_ident <> ident && free_in ident body) + | If(test, yes, no) -> + free_in ident test || free_in ident yes || free_in ident no + | Closure _ -> assert false + + let rec substitute (ident:identifier) (replacement : term) (original : term) = + match original with + | Var(var_ident) when var_ident = ident -> replacement + | Var _ as orig -> orig + | App(head, arg) -> + let head' = substitute ident replacement head in + let arg' = substitute ident replacement arg in + App(head', arg') + | Lambda(bound_ident, body) as orig + when bound_ident = ident || not (free_in ident body) -> + (* vacuous substitution *) + orig + | Lambda(bound_ident, body) + when not (free_in bound_ident replacement) -> + (* can substitute without renaming bound_ident *) + let body' = substitute ident replacement body in + Lambda(bound_ident, body') + | Lambda(bound_ident, body) -> + (* find a fresh variable unused in either body or + replacement (which we hack by specifying their App) *) + let bound_ident' = fresh_var bound_ident (App(body,replacement)) in + let body' = substitute bound_ident (Var bound_ident') body in + let body'' = substitute ident replacement body' in + Lambda(bound_ident', body'') + | Let(bound_ident, arg, body) + when bound_ident = ident || not (free_in ident body) -> + let arg' = substitute ident replacement arg in + Let(bound_ident, arg', body) + | Let(bound_ident, arg, body) + when not (free_in bound_ident replacement) -> + (* can substitute without renaming bound_ident *) + let body' = substitute ident replacement body in + let arg' = substitute ident replacement arg in + Let(bound_ident, arg', body') + | Let(bound_ident, arg, body) -> + (* find a fresh variable unused in either body or + replacement (which we hack by specifying their App) *) + let bound_ident' = fresh_var bound_ident (App(body,replacement)) in + let body' = substitute bound_ident (Var bound_ident') body in + let body'' = substitute ident replacement body' in + let arg' = substitute ident replacement arg in + Let(bound_ident', arg', body'') + | If(test, yes, no) -> + let test' = substitute ident replacement test in + let yes' = substitute ident replacement yes in + let no' = substitute ident replacement no in + If(test', yes', no') + | Closure _ -> assert false + + type reduceOutcome = AlreadyResult of result | StuckAt of term | ReducedTo of term + + let rec reduce_head_once (term : term) (env : env) : reduceOutcome = + match term with + | Lambda _ -> AlreadyResult term + + | Var var -> failwith ("Unbound variable `" ^ var ^ "`") + | Closure _ -> assert false (* no Closures in V1 *) + +(* In this simplified version there are no Bool Literals, so If terms are always stuck + | If(Literal(Bool true),yes,no) -> ReducedTo yes + | If(Literal(Bool false),yes,no) -> ReducedTo no +*) + | If(test,yes,no) -> + (match reduce_head_once test env with + | AlreadyResult _ -> StuckAt term (* if test was not reducible to a bool, the if-term is not reducible at all *) + | StuckAt _ as outcome -> outcome (* propagate Stuck subterm *) + | ReducedTo test' -> ReducedTo(If(test',yes,no))) + + (* notice we never evaluate the body except after substituting + and that happens only after arg is reduced to a result *) + | Let(bound_var,arg,body) -> + (match reduce_head_once arg env with + | AlreadyResult _ -> + (* if arg was not reducible, we can substitute *) + ReducedTo (substitute bound_var arg body) + | StuckAt _ as outcome -> outcome (* propagate Stuck subterm *) + | ReducedTo arg' -> ReducedTo (Let(bound_var,arg',body))) + + (* notice we only substitute after arg is reduced to a result *) + | App(Lambda(bound_var, body) as head, arg) -> + (match reduce_head_once arg env with + | AlreadyResult _ -> + (* if arg was not reducible, we can substitute *) + ReducedTo (substitute bound_var arg body) + | StuckAt _ as outcome -> outcome (* propagate Stuck subterm *) + | ReducedTo arg' -> ReducedTo (App(head, arg'))) + + (* first the head should be reduced, next the arg *) + | App(head, arg) -> + (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')) + (* 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))) + + + + let rec reduce (term : term) (env : env) = + match reduce_head_once term env with + | AlreadyResult res -> res + | StuckAt subterm -> raise (Stuck subterm) + | ReducedTo term' -> reduce term' env (* keep trying *) + +end (* module V1 *) + +module V2 = 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 + *) + + let rec eval (term : term) (env : env) : result = + match term with + | Closure _ -> term + + | Lambda(bound_var, body) -> Closure(bound_var, body, env) + + | 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 + | Some res -> res + | None -> failwith ("Unbound variable `" ^ var ^ "`")) + + | If(test, yes, no) -> + (match eval test env with +(* In this simplified version there are no Bool Literals, so If terms are always stuck + | Literal(Bool true) -> eval yes env + | Literal(Bool false) -> eval no env +*) + | res -> raise (Stuck(If(res,yes,no)))) + + | Let(bound_var, arg, body) -> + (* evaluate body under a new env where bound_var has been + 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' + + | App(head, arg) -> + (match eval head env with + | Closure(bound_var, body, saved_env) -> + (* argument gets evaluated in current env *) + let arg' = eval arg env in + (* 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' + | head' -> raise (Stuck(App(head',arg)))) + + + + 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 *) + +let reduce term = V1.reduce term empty +let evaluate term = V2.evaluate term empty + -- 2.11.0