2 This is a simplified version of the code at http://lambda.jimpryor.net/code/untyped_full-1.7.tgz
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 two interpreters presented below are (VersionA) a substitute-and-repeat
19 interpreter, and (VersionB) an environment-based interpreter. We discuss the
20 differences between these in the course notes.
22 The implementeations we provide make both of these call-by-value. When given
23 a term `App(head, arg)`, the steps are: first, reduce or evaluate
24 `head`---it might involve further `App`s itself. Second, reduce or evaluate
25 `arg`. Third, only _when_ `arg` reduces or evaluates to a result value, then
26 "perform" the application. What this last step amounts to is different in
27 the two interpreters. Call-by-name interpreters would "perform" the
28 application regardless, and without even trying to reduce or evaluate arg to
29 a result value beforehand.
31 Additionally, these implementations assume that free variables are "stuck"
32 terms rather than result values. That is a bit inconvenient with this
33 simplified program: it means that Lambdas (or Closures, in VB) are the only
34 result values. But in the fuller code from which this is simplified, it
35 makes more sense, because there we also have literal number and boolean
36 values as results, too.
38 The environments play absolutely no role in the simplified VA interpreter
39 presented here. In the fuller code, they have a limited role in the VA
40 interpreter. In the VB interpreter, the environments are essential.
43 type identifier = string
48 | Lambda of identifier * term (* in VB, never used as a result *)
49 | Let of identifier * term * term
50 | If of term * term * term
51 (* the following variant is never used as a term, only as a VB result *)
52 | Closure of identifier * term * env
54 (* in the fuller code, we separate the term and result types *)
57 (* This simplified code just provides a single implementation of environments;
58 but the fuller code provides more. *)
59 and env = (identifier * term) list
61 (* Operations for environments *)
63 let shift (ident : identifier) binding env = (ident,binding) :: env
64 let rec lookup (sought_ident : identifier) (env : env) : term option =
67 | (ident, binding) :: _ when ident = sought_ident -> Some binding
68 | _ :: env' -> lookup sought_ident env'
72 eval raises this exception when it fails to reduce/evaluate
73 a term, because it has components for which no
74 reduction/evaluation is defined, such as `x y`. The
75 substitute-and-repeat interpreter just signals this with a normal
76 return value; but the environment-based interpreter uses an
77 exception to abort prematurely.
79 In this simplified version of the code, we also use this
80 exception to report a failed term in VA, since we lack
81 the resources to print the term instead, as the full code does.
83 exception Stuck of term
86 (* ---------------------------------------------------------------
87 Interpreter that reduces by substituting, using:
88 val reduce_head_once : term -> env -> reduceOutcome
89 val reduce : term -> env -> result
91 reduce_head_once is similiar to reduce_if_redex in the
92 combinatory logic interpreter, except that the latter only
93 performed a reduction if its argument was exactly a redex.
94 It had to rely on its caller to detect cases where the term
95 was instead a longer sequence of applications that had a
96 redex at its head. In the present code, on the other hand,
97 we have reduce_head_once take care of this itself, by
98 calling itself recursively where appropriate. Still, it will
99 only perform at most one reduction per invocation.
103 (* Search term and find a variable that isn't used in it,
104 either free or bound. We do this by appending primes to base
105 until we find an unused or "fresh" variable. *)
106 let fresh_var (base : identifier) (term : term) : identifier =
107 let rec aux term vars =
112 let vars' = aux head vars in
114 | Lambda(bound_ident, body) ->
115 aux body (bound_ident :: vars)
116 | Let(bound_ident, arg, body) ->
117 let vars' = aux arg vars in
118 aux body (bound_ident :: vars')
119 | If(test, yes, no) ->
120 let vars' = aux test vars in
121 let vars'' = aux yes vars' in
123 | Closure _ -> assert false in
124 let used_vars = aux term [] in
125 let rec check ident =
126 if List.mem ident used_vars
127 then check (ident ^ "'")
131 let rec free_in (ident : identifier) (term : term) : bool =
136 free_in ident head || free_in ident arg
137 | Lambda(bound_ident, body) ->
138 bound_ident <> ident && free_in ident body
139 | Let(bound_ident, arg, body) ->
140 free_in ident arg || (bound_ident <> ident && free_in ident body)
141 | If(test, yes, no) ->
142 free_in ident test || free_in ident yes || free_in ident no
143 | Closure _ -> assert false
145 let rec substitute (ident:identifier) (replacement : term) (original : term) =
147 | Var(var_ident) when var_ident = ident -> replacement
148 | Var _ as orig -> orig
150 let head' = substitute ident replacement head in
151 let arg' = substitute ident replacement arg in
153 | Lambda(bound_ident, body) as orig
154 when bound_ident = ident || not (free_in ident body) ->
155 (* vacuous substitution *)
157 | Lambda(bound_ident, body)
158 when not (free_in bound_ident replacement) ->
159 (* can substitute without renaming bound_ident *)
160 let body' = substitute ident replacement body in
161 Lambda(bound_ident, body')
162 | Lambda(bound_ident, body) ->
163 (* find a fresh variable unused in either body or
164 replacement (which we hack by specifying their App) *)
165 let bound_ident' = fresh_var bound_ident (App(body,replacement)) in
166 let body' = substitute bound_ident (Var bound_ident') body in
167 let body'' = substitute ident replacement body' in
168 Lambda(bound_ident', body'')
169 | Let(bound_ident, arg, body)
170 when bound_ident = ident || not (free_in ident body) ->
171 let arg' = substitute ident replacement arg in
172 Let(bound_ident, arg', body)
173 | Let(bound_ident, arg, body)
174 when not (free_in bound_ident replacement) ->
175 (* can substitute without renaming bound_ident *)
176 let body' = substitute ident replacement body in
177 let arg' = substitute ident replacement arg in
178 Let(bound_ident, arg', body')
179 | Let(bound_ident, arg, body) ->
180 (* find a fresh variable unused in either body or
181 replacement (which we hack by specifying their App) *)
182 let bound_ident' = fresh_var bound_ident (App(body,replacement)) in
183 let body' = substitute bound_ident (Var bound_ident') body in
184 let body'' = substitute ident replacement body' in
185 let arg' = substitute ident replacement arg in
186 Let(bound_ident', arg', body'')
187 | If(test, yes, no) ->
188 let test' = substitute ident replacement test in
189 let yes' = substitute ident replacement yes in
190 let no' = substitute ident replacement no in
192 | Closure _ -> assert false
194 type reduceOutcome = AlreadyResult of result | StuckAt of term | ReducedTo of term
196 let rec reduce_head_once (term : term) (env : env) : reduceOutcome =
198 | Lambda _ -> AlreadyResult term
200 | Var var -> failwith ("Unbound variable `" ^ var ^ "`")
201 | Closure _ -> assert false (* no Closures in VA *)
203 (* In this simplified version there are no Bool Literals, so If terms are always stuck
204 | If(Literal(Bool true),yes,no) -> ReducedTo yes
205 | If(Literal(Bool false),yes,no) -> ReducedTo no
208 (match reduce_head_once test env with
209 | AlreadyResult _ -> StuckAt term (* if test was not reducible to a bool, the if-term is not reducible at all *)
210 | StuckAt _ as outcome -> outcome (* propagate Stuck subterm *)
211 | ReducedTo test' -> ReducedTo(If(test',yes,no)))
213 (* notice we never evaluate the body except after substituting
214 and that happens only after arg is reduced to a result *)
215 | Let(bound_var,arg,body) ->
216 (match reduce_head_once arg env with
218 (* if arg was not reducible, we can substitute *)
219 ReducedTo (substitute bound_var arg body)
220 | StuckAt _ as outcome -> outcome (* propagate Stuck subterm *)
221 | ReducedTo arg' -> ReducedTo (Let(bound_var,arg',body)))
223 (* notice we only substitute after arg is reduced to a result *)
224 | App(Lambda(bound_var, body) as head, arg) ->
225 (match reduce_head_once arg env with
227 (* if arg was not reducible, we can substitute *)
228 ReducedTo (substitute bound_var arg body)
229 | StuckAt _ as outcome -> outcome (* propagate Stuck subterm *)
230 | ReducedTo arg' -> ReducedTo (App(head, arg')))
232 (* first the head should be reduced, next the arg *)
234 (match reduce_head_once head env with
235 | AlreadyResult _ -> (* head was not reducible, was arg? *)
236 (match reduce_head_once arg env with
237 | ReducedTo arg' -> ReducedTo (App(head, arg'))
238 (* reducible cases of App(result, result) were caught above; so here we're stuck *)
239 | AlreadyResult _ -> StuckAt term
240 | StuckAt _ as outcome -> outcome) (* propagate Stuck subterm *)
241 | StuckAt _ as outcome -> outcome (* propagate Stuck subterm *)
242 | ReducedTo head' -> ReducedTo (App(head', arg)))
246 let rec reduce (term : term) (env : env) =
247 match reduce_head_once term env with
248 | AlreadyResult res -> res
249 | StuckAt subterm -> raise (Stuck subterm)
250 | ReducedTo term' -> reduce term' env (* keep trying *)
255 (* ---------------------------------------------------------------
256 Interpreter that employs an "environment" or assignment
257 function of results, using:
258 val eval term -> env -> result, or may raise (Stuck term)
259 val evaluate term -> env -> result
262 let rec eval (term : term) (env : env) : result =
266 | Lambda(bound_var, body) -> Closure(bound_var, body, env)
269 (match lookup var env with
270 (* In this call-by-value design, only results get
271 saved in the environment, so we can be sure this
274 | None -> failwith ("Unbound variable `" ^ var ^ "`"))
276 | If(test, yes, no) ->
277 (match eval test env with
278 (* In this simplified version there are no Bool Literals, so If terms are always stuck
279 | Literal(Bool true) -> eval yes env
280 | Literal(Bool false) -> eval no env
282 | res -> raise (Stuck(If(res,yes,no))))
284 | Let(bound_var, arg, body) ->
285 (* evaluate body under a new env where bound_var has been
286 bound to the result of evaluating arg under the
288 let arg' = eval arg env in
289 let env' = shift bound_var arg' env in
293 (match eval head env with
294 | Closure(bound_var, body, saved_env) ->
295 (* argument gets evaluated in current env *)
296 let arg' = eval arg env in
297 (* evaluate body under saved_env to govern its free
298 variables, except that we add a binding of
300 let saved_env' = shift bound_var arg' saved_env in
302 | head' -> raise (Stuck(App(head',arg))))
306 let evaluate (term : term) (env : env) : result =
307 eval term env (* in the fuller code, this function catches the Stuck errors and prints them more nicely *)
311 let reduce term = VA.reduce term empty
312 let evaluate term = VB.evaluate term empty