(*
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.
2. Then see if OCaml will compile it, by typing `ocamlc -c simple.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.
(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`
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.
*)
type identifier = string
type term =
| Var of identifier
| App of term * term
| Lambda of identifier * term
| Let of identifier * term * term
| If of term * term * term
| Closure of identifier * term * env
and result = term
and env = identifier -> term option
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 `succ false`. The
reduction-based interpreter just signaled 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
Now `env` contains local as well as toplevel bindings.
*)
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
(* the first case is different from V1.reduce_head_once *)
| 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 *)
(* 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
*)