(*
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 (* 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 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 (* 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
(* This simplified code just provides a single implementation of environments;
but the fuller code provides more. *)
and env = (identifier * term) list
(* 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 `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 VA, since we lack
the resources to print the term instead, as the full code does.
*)
exception Stuck of term
module VA = 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 VA *)
(* 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 VA *)
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
*)
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
(* 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 ^ "`"))
| 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' = shift 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' = shift 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 VB *)
let reduce term = VA.reduce term empty
let evaluate term = VB.evaluate term empty