add Juli8-v1.3
[lambda.git] / code / untyped_evaluator_complete.ml
1 (*
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:
4
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")))`
17
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.
21
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.
30
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.
37
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.
41 *)
42
43 type identifier = string
44   
45 type term =
46   | Var of identifier
47   | App of term * term
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
53
54 (* in the fuller code, we separate the term and result types *)
55 and result = term
56
57 (* This simplified code just provides a single implementation of environments;
58    but the fuller code provides more. *)
59 and env = (identifier * term) list
60
61 (* Operations for environments *)
62 let empty = []
63 let shift (ident : identifier) binding env = (ident,binding) :: env
64 let rec lookup (sought_ident : identifier) (env : env) : term option =
65   match env with
66   | [] -> None
67   | (ident, binding) :: _ when ident = sought_ident -> Some binding
68   | _ :: env' -> lookup sought_ident env'
69
70   
71 (*
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.
78
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.
82 *)
83 exception Stuck of term
84
85 module VA = struct
86   (* ---------------------------------------------------------------
87      Interpreter that reduces by substituting, using:
88          val reduce_head_once : term -> env -> reduceOutcome
89          val reduce : term -> env -> result
90
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.
100   *)
101   
102
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 =
108     match term with
109     | Var(var_ident) ->
110         var_ident :: vars
111     | App(head, arg) ->
112         let vars' = aux head vars in
113         aux arg vars'
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
122         aux no vars''
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 ^ "'")
128       else ident in
129     check (base ^ "'")
130   
131   let rec free_in (ident : identifier) (term : term) : bool =
132     match term with
133     | Var(var_ident) ->
134         var_ident = ident
135     | App(head, arg) ->
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 
144   
145   let rec substitute (ident:identifier) (replacement : term) (original : term) =
146     match original with
147     | Var(var_ident) when var_ident = ident -> replacement
148     | Var _ as orig -> orig
149     | App(head, arg) ->
150         let head' = substitute ident replacement head in
151         let arg' = substitute ident replacement arg in
152         App(head', arg')
153     | Lambda(bound_ident, body) as orig
154       when bound_ident = ident || not (free_in ident body) ->
155         (* vacuous substitution *)
156         orig
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
191         If(test', yes', no')
192     | Closure _ -> assert false 
193  
194   type reduceOutcome = AlreadyResult of result | StuckAt of term | ReducedTo of term
195   
196   let rec reduce_head_once (term : term) (env : env) : reduceOutcome =
197     match term with
198     | Lambda _ -> AlreadyResult term
199   
200     | Var var -> failwith ("Unbound variable `" ^ var ^ "`")
201     | Closure _ -> assert false (* no Closures in VA *)
202   
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
206 *)
207     | If(test,yes,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)))
212   
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
217         | AlreadyResult _ ->
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)))
222   
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
226         | AlreadyResult _ ->
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')))
231   
232     (* first the head should be reduced, next the arg *)
233     | App(head, 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)))
243   
244
245
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 *)
251
252 end (* module VA *)
253
254 module VB = struct
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
260   *)
261
262   let rec eval (term : term) (env : env) : result =
263     match term with
264     | Closure _ -> term
265
266     | Lambda(bound_var, body) -> Closure(bound_var, body, env)
267
268     | Var var ->
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
272            is a result. *)
273         | Some res -> res
274         | None -> failwith ("Unbound variable `" ^ var ^ "`"))
275
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
281 *)
282         | res -> raise (Stuck(If(res,yes,no))))
283
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
287            current env *)
288         let arg' = eval arg env in
289         let env' = shift bound_var arg' env in
290         eval body env'
291
292     | App(head, arg) ->
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
299                bound_var to arg' *)
300             let saved_env' = shift bound_var arg' saved_env in
301             eval body saved_env'
302         | head' -> raise (Stuck(App(head',arg))))
303
304
305
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 *)
308
309 end (* module VB *)
310
311 let reduce term = VA.reduce term empty
312 let evaluate term = VB.evaluate term empty
313