2 This is a simplified version of the code at ...
3 You can use this code as follows:
5 1. First, use a text editor to fill in the uncompleted portions.
6 2. Then see if OCaml will compile it, by typing `ocamlc -c simple.ml` in a Terminal.
7 3. If it doesn't work, go back to step 1.
8 4. If it does work, then you can start up the OCaml toplevel using `ocaml -I DIRECTORY`,
9 where DIRECTORY is the name of the folder that contains your `simple.ml` file.
10 (Alternatively, if OCaml is already started, you can type `#directory "DIRECTORY";;`
11 5. Then once OCaml is started, you can either: (a) type `#load "simple.cmo";;`, then type
12 `open Simple;;` (this has to be on a separate line from step (a), it seems);
13 or (b) instead you can type `#use "simple.ml";;`
14 6. Now you can try commands like `interpret (App(Lambda("x",Var "x"),Lambda("y",Var "y"))) empty`
15 Or V1.reduce (App(Lambda("x",Var "x"),Lambda("y",Var "y"))) empty`
16 Or V1.evaluate (App(Lambda("x",Var "x"),Lambda("y",Var "y"))) empty`
18 The environments play absolutely no role in this simplified V1 interpreter. In the
19 fuller code, they have a limited role in the V1 interpreter. In the V2 interpreter,
20 the environments are essential. This simplified code just provides a single
21 implementation of environments; but the fuller code provides more.
24 type identifier = string
29 | Lambda of identifier * term
30 | Let of identifier * term * term
31 | If of term * term * term
32 | Closure of identifier * term * env
36 and env = identifier -> term option
38 let empty = fun _ -> None
39 let push (ident : identifier) binding env =
40 fun (sought_ident : identifier) ->
41 if ident = sought_ident
44 let lookup sought_ident env = env sought_ident
48 eval raises this exception when it fails to reduce/evaluate
49 a term, because it has components for which no
50 reduction/evaluation is defined, such as `succ false`. The
51 reduction-based interpreter just signaled this with a normal
52 return value; but the environment- based interpreter uses an
53 exception to abort prematurely.
55 In this simplified version of the code, we also use this
56 exception to report a failed term in V1, since we lack
57 the resources to print the term instead, as the full code does.
59 exception Stuck of term
62 (* ---------------------------------------------------------------
63 Interpreter that reduces by substituting, using:
64 val reduce_head_once : term -> env -> reduceOutcome
65 val reduce : term -> env -> result
67 reduce_head_once is similiar to reduce_if_redex in the
68 combinatory logic interpreter, except that the latter only
69 performed a reduction if its argument was exactly a redex.
70 It had to rely on its caller to detect cases where the term
71 was instead a longer sequence of applications that had a
72 redex at its head. In the present code, on the other hand,
73 we have reduce_head_once take care of this itself, by
74 calling itself recursively where appropriate. Still, it will
75 only perform at most one reduction per invocation.
79 (* Search term and find a variable that isn't used in it,
80 either free or bound. We do this by appending primes to base
81 until we find an unused or "fresh" variable. *)
82 let fresh_var (base : identifier) (term : term) : identifier =
83 let rec aux term vars =
88 let vars' = aux head vars in
90 | Lambda(bound_ident, body) ->
91 aux body (bound_ident :: vars)
92 | Let(bound_ident, arg, body) ->
93 let vars' = aux arg vars in
94 aux body (bound_ident :: vars')
95 | If(test, yes, no) ->
96 let vars' = aux test vars in
97 let vars'' = aux yes vars' in
99 | Closure _ -> assert false in
100 let used_vars = aux term [] in
101 let rec check ident =
102 if List.mem ident used_vars
103 then check (ident ^ "'")
107 let rec free_in (ident : identifier) (term : term) : bool =
112 free_in ident head || free_in ident arg
113 | Lambda(bound_ident, body) ->
114 bound_ident <> ident && free_in ident body
115 | Let(bound_ident, arg, body) ->
116 free_in ident arg || (bound_ident <> ident && free_in ident body)
117 | If(test, yes, no) ->
118 free_in ident test || free_in ident yes || free_in ident no
119 | Closure _ -> assert false
121 let rec substitute (ident:identifier) (replacement : term) (original : term) =
123 | Var(var_ident) when var_ident = ident -> replacement
124 | Var _ as orig -> orig
126 let head' = substitute ident replacement head in
127 let arg' = substitute ident replacement arg in
129 | Lambda(bound_ident, body) as orig
130 when bound_ident = ident || not (free_in ident body) ->
131 (* vacuous substitution *)
133 | Lambda(bound_ident, body)
134 when not (free_in bound_ident replacement) ->
135 (* can substitute without renaming bound_ident *)
136 let body' = substitute ident replacement body in
137 Lambda(bound_ident, body')
138 | Lambda(bound_ident, body) ->
139 (* find a fresh variable unused in either body or
140 replacement (which we hack by specifying their App) *)
141 let bound_ident' = fresh_var bound_ident (App(body,replacement)) in
142 let body' = substitute bound_ident (Var bound_ident') body in
143 let body'' = substitute ident replacement body' in
144 Lambda(bound_ident', body'')
145 | Let(bound_ident, arg, body)
146 when bound_ident = ident || not (free_in ident body) ->
147 let arg' = substitute ident replacement arg in
148 Let(bound_ident, arg', body)
149 | Let(bound_ident, arg, body)
150 when not (free_in bound_ident replacement) ->
151 (* can substitute without renaming bound_ident *)
152 let body' = substitute ident replacement body in
153 let arg' = substitute ident replacement arg in
154 Let(bound_ident, arg', body')
155 | Let(bound_ident, arg, body) ->
156 (* find a fresh variable unused in either body or
157 replacement (which we hack by specifying their App) *)
158 let bound_ident' = fresh_var bound_ident (App(body,replacement)) in
159 let body' = substitute bound_ident (Var bound_ident') body in
160 let body'' = substitute ident replacement body' in
161 let arg' = substitute ident replacement arg in
162 Let(bound_ident', arg', body'')
163 | If(test, yes, no) ->
164 let test' = substitute ident replacement test in
165 let yes' = substitute ident replacement yes in
166 let no' = substitute ident replacement no in
168 | Closure _ -> assert false
170 type reduceOutcome = AlreadyResult of result | StuckAt of term | ReducedTo of term
172 let rec reduce_head_once (term : term) (env : env) : reduceOutcome =
174 | Lambda _ -> AlreadyResult term
176 | Var var -> failwith ("Unbound variable `" ^ var ^ "`")
177 | Closure _ -> assert false (* no Closures in V1 *)
179 (* In this simplified version there are no Bool Literals, so If terms are always stuck
180 | If(Literal(Bool true),yes,no) -> ReducedTo yes
181 | If(Literal(Bool false),yes,no) -> ReducedTo no
184 (match reduce_head_once test env with
185 | AlreadyResult _ -> StuckAt term (* if test was not reducible to a bool, the if-term is not reducible at all *)
186 | StuckAt _ as outcome -> outcome (* propagate Stuck subterm *)
187 | ReducedTo test' -> ReducedTo(If(test',yes,no)))
189 (* notice we never evaluate the body except after substituting
190 and that happens only after arg is reduced to a result *)
191 | Let(bound_var,arg,body) ->
192 (match reduce_head_once arg env with
194 (* if arg was not reducible, we can substitute *)
195 ReducedTo (substitute bound_var arg body)
196 | StuckAt _ as outcome -> outcome (* propagate Stuck subterm *)
197 | ReducedTo arg' -> ReducedTo (Let(bound_var,arg',body)))
199 (* notice we only substitute after arg is reduced to a result *)
200 | App(Lambda(bound_var, body) as head, arg) ->
201 (match reduce_head_once arg env with
203 (* if arg was not reducible, we can substitute *)
204 ReducedTo (substitute bound_var arg body)
205 | StuckAt _ as outcome -> outcome (* propagate Stuck subterm *)
206 | ReducedTo arg' -> ReducedTo (App(head, arg')))
208 (* first the head should be reduced, next the arg *)
210 (match reduce_head_once head env with
211 | AlreadyResult _ -> (* head was not reducible, was arg? *)
212 (match reduce_head_once arg env with
213 | ReducedTo arg' -> ReducedTo (App(head, arg'))
214 (* reducible cases of App(result, result) were caught above; so here we're stuck *)
215 | AlreadyResult _ -> StuckAt term
216 | StuckAt _ as outcome -> outcome) (* propagate Stuck subterm *)
217 | StuckAt _ as outcome -> outcome (* propagate Stuck subterm *)
218 | ReducedTo head' -> ReducedTo (App(head', arg)))
223 let rec reduce (term : term) (env : env) =
224 match reduce_head_once term env with
225 | AlreadyResult res -> res
226 | StuckAt subterm -> raise (Stuck subterm)
227 | ReducedTo term' -> reduce term' env (* keep trying *)
232 (* ---------------------------------------------------------------
233 Interpreter that employs an "environment" or assignment
234 function of results, using:
235 val eval term -> env -> result, or may raise (Stuck term)
236 val evaluate term -> env -> result
237 Now `env` contains local as well as toplevel bindings.
240 let rec eval (term : term) (env : env) : result =
244 | Lambda(bound_var, body) -> Closure(bound_var, body, env)
247 (match lookup var env with
248 (* the first case is different from V1.reduce_head_once *)
250 | None -> failwith ("Unbound variable `" ^ var ^ "`"))
252 | If(test, yes, no) ->
253 (match eval test env with
254 (* In this simplified version there are no Bool Literals, so If terms are always stuck
255 | Literal(Bool true) -> eval yes env
256 | Literal(Bool false) -> eval no env
258 | res -> raise (Stuck(If(res,yes,no))))
260 | Let(bound_var, arg, body) ->
261 (* evaluate body under a new env where bound_var has been
262 bound to the result of evaluating arg under the
264 let arg' = eval arg env in
265 let env' = push bound_var arg' env in
269 (match eval head env with
270 | Closure(bound_var, body, saved_env) ->
271 (* argument gets evaluated in current env *)
272 let arg' = eval arg env in
273 (* evaluate body under saved_env to govern its free
274 variables, except that we add a binding of
276 let saved_env' = push bound_var arg' saved_env in
278 | head' -> raise (Stuck(App(head',arg))))
282 let evaluate (term : term) (env : env) : result =
283 eval term env (* in the fuller code, this function catches the Stuck errors and prints them more nicely *)
288 (* Put comment (* *)s around exactly one of the following two pairs of lines. *)
290 let version = "version 1 (reduce by substituting)"
291 let interpret = V1.reduce
294 let version = "version 2 (use environment for local bindings)"
295 let interpret = V2.evaluate