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 (* COMPLETE THIS *) portions.
6 2. Then see if OCaml will compile it, by typing `ocamlc -c untyped_evaluator.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 `untyped_evaluator.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 "untyped_evaluator.cmo";;`, then type
12 `open Untyped_evaluator;;` (this has to be on a separate line from step (a), it seems);
13 or (b) instead you can type `#use "untyped_evaluator.ml";;`
14 6. Now you can try commands like:
15 `reduce (App(Lambda("x",Var "x"),Lambda("y",Var "y")))`
16 `evaluate (App(Lambda("x",Var "x"),Lambda("y",Var "y")))`
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.
23 type identifier = string
28 | Lambda of identifier * term (* in V2, never used as a result *)
29 | Let of identifier * term * term
30 | If of term * term * term
31 (* the following variant is never used as a term, only as a V2 result *)
32 | Closure of identifier * term * env
34 (* in the fuller code, we separate the term and result types *)
37 (* This simplified code just provides a single implementation of environments;
38 but the fuller code provides more. *)
39 and env = identifier -> term option
41 (* Operations for environments *)
42 let empty = fun _ -> None
43 let push (ident : identifier) binding env =
44 fun (sought_ident : identifier) ->
45 if ident = sought_ident
48 let lookup sought_ident env = env sought_ident
52 eval raises this exception when it fails to reduce/evaluate
53 a term, because it has components for which no
54 reduction/evaluation is defined, such as `x y`. The
55 reduction-based interpreter just signals this with a normal
56 return value; but the environment-based interpreter uses an
57 exception to abort prematurely.
59 In this simplified version of the code, we also use this
60 exception to report a failed term in V1, since we lack
61 the resources to print the term instead, as the full code does.
63 exception Stuck of term
66 (* ---------------------------------------------------------------
67 Interpreter that reduces by substituting, using:
68 val reduce_head_once : term -> env -> reduceOutcome
69 val reduce : term -> env -> result
71 reduce_head_once is similiar to reduce_if_redex in the
72 combinatory logic interpreter, except that the latter only
73 performed a reduction if its argument was exactly a redex.
74 It had to rely on its caller to detect cases where the term
75 was instead a longer sequence of applications that had a
76 redex at its head. In the present code, on the other hand,
77 we have reduce_head_once take care of this itself, by
78 calling itself recursively where appropriate. Still, it will
79 only perform at most one reduction per invocation.
83 (* Search term and find a variable that isn't used in it,
84 either free or bound. We do this by appending primes to base
85 until we find an unused or "fresh" variable. *)
86 let fresh_var (base : identifier) (term : term) : identifier =
87 let rec aux term vars =
92 let vars' = aux head vars in
94 | Lambda(bound_ident, body) ->
95 aux body (bound_ident :: vars)
96 | Let(bound_ident, arg, body) ->
97 let vars' = aux arg vars in
98 aux body (bound_ident :: vars')
99 | If(test, yes, no) ->
100 let vars' = aux test vars in
101 let vars'' = aux yes vars' in
103 | Closure _ -> assert false in
104 let used_vars = aux term [] in
105 let rec check ident =
106 if List.mem ident used_vars
107 then check (ident ^ "'")
111 let rec free_in (ident : identifier) (term : term) : bool =
116 free_in ident head || free_in ident arg
117 | Lambda(bound_ident, body) ->
118 bound_ident <> ident && free_in ident body
119 | Let(bound_ident, arg, body) ->
120 free_in ident arg || (bound_ident <> ident && free_in ident body)
121 | If(test, yes, no) ->
122 free_in ident test || free_in ident yes || free_in ident no
123 | Closure _ -> assert false
125 let rec substitute (ident:identifier) (replacement : term) (original : term) =
127 | Var(var_ident) when var_ident = ident -> replacement
128 | Var _ as orig -> orig
130 let head' = substitute ident replacement head in
131 let arg' = substitute ident replacement arg in
133 | Lambda(bound_ident, body) as orig
134 when bound_ident = ident || not (free_in ident body) ->
135 (* vacuous substitution *)
137 | Lambda(bound_ident, body)
138 when not (free_in bound_ident replacement) ->
139 (* can substitute without renaming bound_ident *)
140 let body' = substitute ident replacement body in
141 Lambda(bound_ident, body')
142 | Lambda(bound_ident, body) ->
143 (* find a fresh variable unused in either body or
144 replacement (which we hack by specifying their App) *)
145 let bound_ident' = fresh_var bound_ident (App(body,replacement)) in
146 let body' = substitute bound_ident (Var bound_ident') body in
147 let body'' = substitute ident replacement body' in
148 Lambda(bound_ident', body'')
149 | Let(bound_ident, arg, body)
150 when bound_ident = ident || not (free_in ident body) ->
151 let arg' = substitute ident replacement arg in
152 Let(bound_ident, arg', body)
153 | Let(bound_ident, arg, body)
154 when not (free_in bound_ident replacement) ->
155 (* can substitute without renaming bound_ident *)
156 let body' = substitute ident replacement body in
157 let arg' = substitute ident replacement arg in
158 Let(bound_ident, arg', body')
159 | Let(bound_ident, arg, body) ->
160 (* find a fresh variable unused in either body or
161 replacement (which we hack by specifying their App) *)
162 let bound_ident' = fresh_var bound_ident (App(body,replacement)) in
163 let body' = substitute bound_ident (Var bound_ident') body in
164 let body'' = substitute ident replacement body' in
165 let arg' = substitute ident replacement arg in
166 Let(bound_ident', arg', body'')
167 | If(test, yes, no) ->
168 let test' = substitute ident replacement test in
169 let yes' = substitute ident replacement yes in
170 let no' = substitute ident replacement no in
172 | Closure _ -> assert false
174 type reduceOutcome = AlreadyResult of result | StuckAt of term | ReducedTo of term
176 let rec reduce_head_once (term : term) (env : env) : reduceOutcome =
178 | Lambda _ -> AlreadyResult term
180 | Var var -> failwith ("Unbound variable `" ^ var ^ "`")
181 | Closure _ -> assert false (* no Closures in V1 *)
183 (* In this simplified version there are no Bool Literals, so If terms are always stuck
184 | If(Literal(Bool true),yes,no) -> ReducedTo yes
185 | If(Literal(Bool false),yes,no) -> ReducedTo no
188 (match reduce_head_once test env with
189 | AlreadyResult _ -> StuckAt term (* if test was not reducible to a bool, the if-term is not reducible at all *)
190 | StuckAt _ as outcome -> outcome (* propagate Stuck subterm *)
191 | ReducedTo test' -> ReducedTo(If(test',yes,no)))
193 (* notice we never evaluate the body except after substituting
194 and that happens only after arg is reduced to a result *)
195 | Let(bound_var,arg,body) ->
196 (match reduce_head_once arg env with
198 (* if arg was not reducible, we can substitute *)
199 ReducedTo (substitute bound_var arg body)
200 | StuckAt _ as outcome -> outcome (* propagate Stuck subterm *)
201 | ReducedTo arg' -> ReducedTo (Let(bound_var,arg',body)))
203 (* notice we only substitute after arg is reduced to a result *)
204 | App(Lambda(bound_var, body) as head, arg) ->
205 (match reduce_head_once arg env with
207 (* if arg was not reducible, we can substitute *)
208 ReducedTo (substitute bound_var arg body)
209 | StuckAt _ as outcome -> outcome (* propagate Stuck subterm *)
210 | ReducedTo arg' -> ReducedTo (App(head, arg')))
212 (* first the head should be reduced, next the arg *)
214 (match reduce_head_once head env with
215 | AlreadyResult _ -> (* head was not reducible, was arg? *)
216 (match reduce_head_once arg env with
217 | ReducedTo arg' -> ReducedTo (App(head, arg'))
218 (* reducible cases of App(result, result) were caught above; so here we're stuck *)
219 | AlreadyResult _ -> StuckAt term
220 | StuckAt _ as outcome -> outcome) (* propagate Stuck subterm *)
221 | StuckAt _ as outcome -> outcome (* propagate Stuck subterm *)
222 | ReducedTo head' -> ReducedTo (App(head', arg)))
226 let rec reduce (term : term) (env : env) =
227 match reduce_head_once term env with
228 | AlreadyResult res -> res
229 | StuckAt subterm -> raise (Stuck subterm)
230 | ReducedTo term' -> reduce term' env (* keep trying *)
235 (* ---------------------------------------------------------------
236 Interpreter that employs an "environment" or assignment
237 function of results, using:
238 val eval term -> env -> result, or may raise (Stuck term)
239 val evaluate term -> env -> result
242 let rec eval (term : term) (env : env) : result =
246 | Lambda(bound_var, body) -> Closure(bound_var, body, env)
249 (match lookup var env with
250 (* Free variables will never be pushed to the env, so we can be
251 sure this is a result. *)
253 | None -> failwith ("Unbound variable `" ^ var ^ "`"))
255 | If(test, yes, no) ->
256 (match eval test env with
257 (* In this simplified version there are no Bool Literals, so If terms are always stuck
258 | Literal(Bool true) -> eval yes env
259 | Literal(Bool false) -> eval no env
261 | res -> raise (Stuck(If(res,yes,no))))
263 | Let(bound_var, arg, body) ->
264 (* evaluate body under a new env where bound_var has been
265 bound to the result of evaluating arg under the
267 let arg' = eval arg env in
268 let env' = push bound_var arg' env in
272 (match eval head env with
273 | Closure(bound_var, body, saved_env) ->
274 (* argument gets evaluated in current env *)
275 let arg' = eval arg env in
276 (* evaluate body under saved_env to govern its free
277 variables, except that we add a binding of
279 let saved_env' = push bound_var arg' saved_env in
281 | head' -> raise (Stuck(App(head',arg))))
285 let evaluate (term : term) (env : env) : result =
286 eval term env (* in the fuller code, this function catches the Stuck errors and prints them more nicely *)
290 let reduce term = V1.reduce term empty
291 let evaluate term = V2.evaluate term empty