(*
- 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
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
| 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
| 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
(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')))
(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 *))
| 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 =
| 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 ^ "`"))
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
(* 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))))
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
-*)