(* 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. *) | 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