update homework
[lambda.git] / code / untyped_evaluator.ml
1 (*
2    This is a simplified version of the code at ...
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 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.
21 *)
22
23 type identifier = string
24   
25 type term =
26   | Var of identifier
27   | App of term * term
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
33
34 (* in the fuller code, we separate the term and result types *)
35 and result = term
36
37 (* This simplified code just provides a single implementation of environments;
38    but the fuller code provides more. *)
39 and env = identifier -> term option
40
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
46     then Some binding
47     else env sought_ident
48 let lookup sought_ident env = env sought_ident
49
50   
51 (*
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.
58
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.
62 *)
63 exception Stuck of term
64
65 module V1 = struct
66   (* ---------------------------------------------------------------
67      Interpreter that reduces by substituting, using:
68          val reduce_head_once : term -> env -> reduceOutcome
69          val reduce : term -> env -> result
70
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.
80   *)
81   
82
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 =
88     match term with
89     | Var(var_ident) ->
90         var_ident :: vars
91     | App(head, arg) ->
92         let vars' = aux head vars in
93         aux arg vars'
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
102         aux no vars''
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 ^ "'")
108       else ident in
109     check (base ^ "'")
110   
111   let rec free_in (ident : identifier) (term : term) : bool =
112     match term with
113     | Var(var_ident) ->
114         var_ident = ident
115     | App(head, arg) ->
116         (* COMPLETE THIS *)
117     | Lambda(bound_ident, body) ->
118         (* COMPLETE THIS *)
119     | Let(bound_ident, arg, body) ->
120         free_in ident arg || (* COMPLETE THIS *)
121     | If(test, yes, no) ->
122         free_in ident test || free_in ident yes || free_in ident no
123     | Closure _ -> assert false 
124   
125   let rec substitute (ident:identifier) (replacement : term) (original : term) =
126     match original with
127     | Var(var_ident) when var_ident = ident -> replacement
128     | Var _ as orig -> orig
129     | App(head, arg) ->
130         let head' = substitute ident replacement head in
131         let arg' = substitute ident replacement arg in
132         App(head', arg')
133     | Lambda(bound_ident, body) as orig
134       when bound_ident = ident || not (free_in ident body) ->
135         (* vacuous substitution *)
136         orig
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
171         If(test', yes', no')
172     | Closure _ -> assert false 
173  
174   type reduceOutcome = AlreadyResult of result | StuckAt of term | ReducedTo of term
175   
176   let rec reduce_head_once (term : term) (env : env) : reduceOutcome =
177     match term with
178     | Lambda _ -> AlreadyResult term
179   
180     | Var var -> failwith ("Unbound variable `" ^ var ^ "`")
181     | Closure _ -> assert false (* no Closures in V1 *)
182   
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
186 *)
187     | If(test,yes,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)))
192   
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
197         | AlreadyResult _ ->
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)))
202   
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
206         | AlreadyResult _ ->
207             (* if arg was not reducible, we can substitute *)
208             (* COMPLETE THIS *)
209         | StuckAt _ as outcome -> outcome (* propagate Stuck subterm *)
210         | ReducedTo arg' -> ReducedTo (App(head, arg')))
211   
212     (* first the head should be reduced, next the arg *)
213     | App(head, 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' -> (* COMPLETE THIS *)
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' -> (* COMPLETE THIS *))
223   
224
225
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 *)
231
232 end (* module V1 *)
233
234 module V2 = struct
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
240   *)
241
242   let rec eval (term : term) (env : env) : result =
243     match term with
244     | Closure _ -> term
245
246     | Lambda(bound_var, body) -> Closure(bound_var, body, env)
247
248     | Var var ->
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. *) CHECK
252         | Some res -> res
253         | None -> failwith ("Unbound variable `" ^ var ^ "`"))
254
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
260 *)
261         | res -> raise (Stuck(If(res,yes,no))))
262
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
266            current env *)
267         let arg' = eval arg env in
268         let env' = (* COMPLETE THIS *)
269
270     | App(head, arg) ->
271         (match eval head env with
272         | Closure(bound_var, body, saved_env) ->
273             (* argument gets evaluated in current env *)
274             let arg' = eval arg env in
275             (* evaluate body under saved_env to govern its free
276                variables, except that we add a binding of
277                bound_var to arg' *)
278             let saved_env' = (* COMPLETE THIS *)
279         | head' -> raise (Stuck(App(head',arg))))
280
281
282
283   let evaluate (term : term) (env : env) : result =
284     eval term env (* in the fuller code, this function catches the Stuck errors and prints them more nicely *)
285
286 end (* module V2 *)
287
288 let reduce term = V1.reduce term empty
289 let evaluate term = V2.evaluate term empty
290