Merge branch 'working'
[lambda.git] / topics / week7_untyped_evaluator.mdwn
1 [[!toc levels=2]]
2
3 Datatypes and complications
4 ---------------------------
5
6 Let's start with an OCaml datatype for untyped lambda terms:
7
8     type identifier = string
9     type term =
10       | Var of identifier
11       | App of term * term
12       | Lambda of identifier * term
13
14 Some examples of `term`s are:
15
16     Var "x"
17     App(Var "x", Var "y")
18     App(Lambda("x",Var "x"), Var "y")
19
20 We're going to want to design an _interpreter_ program that will reduce or evaluate the final term down to:
21
22     Var "y"
23
24 It would be nice if it also knew how to display that in the more user-friendly format:
25
26     y
27
28 And it would be doubly-specially nice if we didn't have to type our input in the long explicit OCaml notation, but could instead just write:
29
30     (\x.x) y
31
32 and behind the scenes that got converted into:
33
34     App(Lambda("x",Var "x"), Var "y")
35
36 which is what the functions of our interpreter program have to deal with.
37
38 As long as we're at it, why don't we make out language a bit more full-featured. We could throw in `let`-terms and `if-then`-terms, too:
39
40     type term =
41       | Var of identifier
42       | App of term * term
43       | Lambda of identifier * term
44       | Let of identifier * term * term
45       | LetRec of (identifier * term) list * term
46       | If of term * term * term
47
48 We're not actually going to implement `LetRec` in this exercise; that's just there as a placeholder for later. 
49
50 Perhaps also some boolean and number constants:
51
52     type literal = Bool of bool | Num of int
53     type term =
54       ...
55       | Literal of literal
56
57 But then once we have those, we are going to want to have some primitive operations to deal with them. Otherwise they'll just be black boxes that we can only pass around, without ever inspecting or making differentiated use of. Thus we might want operations like `zero?` and `pred` for numbers, `not` for negation, and so on. Long story short, we are going to want some *primitive functions*, some *constructors* (like `cons` and `[]` were for lists), and some *deconstructors* or operations appropriate to those constructors (these were `head` and `tail` for lists). Thus our fleshed-out datatype might look like this:
58
59     type term =
60       | Var of identifier
61       | App of term * term
62       | Lambda of identifier * term
63       | Let of identifier * term * term
64       | LetRec of (identifier * term) list * term
65       | If of term * term * term
66       (* Constants, functional and otherwise *)
67       | Primfun of primfun
68       | Constructor of constructor
69       | Destructor of destructor
70       | Literal of literal
71
72 The official term for operations like `head` and `tail` is "deconstructor", not "destructor", but the latter is shorter and more fun to type.
73
74 We're going to explore how to implement the interpreter using two different methods. One is a translation of the method Chris demonstrated for combinatory logic over to the lambda calculus. You check if any part of a term is reducible, if so perform the appropriate substitutions, and then keep repeating single-step reductions until you can't find any more eligible redexes. This involves substituting the argument of a redex into any free occurrences of the variable bound in the head. The second method works a bit differently. You can begin by thinking of it an improvement on the first method, that tries to get by without having to do all the laborious substitutions that reducing again and again would entail. But its virtues will be more than merely ones of efficiency. It will also start to look a lot more like the kinds of semantics, using assignment functions, that we're more familiar with as formal semanticists. In programming circles, assignment functions are called "environments" and we'll use that terminology here. So the two methods we're going to look at will be, first, a substitute-and-repeat interpreter; and second, an environment-based one.
75
76 The code of this interpreter is based on source code accompanying Pierce's excellent book _Types and Programming Languages_. (In particular, the files here <http://www.cis.upenn.edu/~bcpierce/tapl/checkers/fulluntyped/>.) We aggressively modified that code to suit our somewhat different needs (and taste). Notably, Pierce's code only provides a substitute-and-repeat interpreter; so part of our refactoring was to make it easier to switch back and forth between that and an environment-based interpreter.
77
78 We provided you with a [[homework assignment|/exercises/assignment7]] that is a simplified version of the code of our interpreter. After getting that to work, you may be interested to play around with the fuller version, which adds literal  numbers and booleans, and user-friendly input and printing of results.
79
80 But these benefits come at a price. The code has some complexity to it. 
81
82 Now part of the complexity can be factored out into extra files that you might just ignore, and we've tried to organize the code to maximize that. But sadly, some of the complexity inevitably ends up polluting our nice simple datatype. We're going to explain where this pollution comes from, in the hope that then you'll be able to see through it to the simple underlying form, that we displayed above.
83
84 A **first source of complexity** is that we want to get friendlier error messages, for example if we run the interpreter on a file `./input` that contains:
85
86     let x = 3 in x + y
87
88 The interpreter will complain:
89
90     ./input:1.17: Unbound variable `y`
91
92 What this means is that while processing the file `./input`, after character 17 on line 1, something gave the interpreter indigestion, and its particular complaint is that it encountered an ``Unbound variable `y` ``. When the code you're feeding the interpreter is non-trivial, it's very helpful to get this kind of information about where in the file the error originated from. But to keep track of that, our datatype has to get messier. We'll have some extra information (we'll call it `info`, don't worry about its internal structure) associated with each term (and subterm) that we're handling. And so our datatypes will look instead like this:
93
94     type bare_term =
95       | Var of identifier
96       ...
97     type term = info * bare_term
98
99 And when we pattern match on the (full, annotated) terms, our code will look like this:
100
101     match term with
102     | _,Var ident -> ...
103     ...
104
105 with the extra `_,` at the start of the pattern to catch and discard the extra information about where the term came from. In some cases we need to retain that information instead of discarding it, so the code will instead look like this:
106
107     match term with
108     | fi,Var ident -> ...
109     ...
110
111 using the variable `fi` for the "source file info".
112
113 A **second complication** has to do with the distinction between `term`s in general and what we want to count as `result`s of our computations.
114
115 In these exercises, unlike the combinatory logic ones, we are only going to work with "call-by-value" interpreters. That is, we will only apply functions (whether primitives or those expressed by Lambdas) to what we deem as "value"s or "result"s. At a minimum, these must be terms that it is not possible to reduce further. So `1` and `\x. x` count as values. But we will also legislate that terms like `1 (\x. x)`, though non-reducible (our booleans and numbers won't be Church functions, but rather will be non-functional atoms), count as "stuck" and so aren't results either. (As suggested in class, you can think of "stuck" terms as representing or being crashed computations.)
116
117 As a result of never applying functions to non-results, non-results will never get bound to any variables, either.
118
119 Now in the VA/substitute-and-repeat part of the exercise, results will simply be a proper subset of our terms. They will be abstracts, plus literals and all the other primitives. They won't include free/unbound variables. We'll count those as "stuck" or crashed computations, too. (But _bound_ variables are okay, because they'll always be bound to results.)
120
121 However, when we move to the VB/environment-based interpreter, we will need to introduce some results that aren't (just) terms, called `Closure`s. We'll discuss these later; but the upshot is that we're going to need eventually to work with code where the result datatype and the term datatype may be partly disjoint. So we are going to need two parallel datatypes:
122
123     type bare_term =
124       | TermVar of identifier
125       | TermApp of term * term
126       | TermLambda of identifier * term
127       | TermLet of identifier * term * term
128       | TermLetRec of (identifier * term) list * term
129       | TermIf of term * term * term
130       (* Constants, functional and otherwise *)
131       | TermPrimfun of primfun
132       | TermConstructor of constructor
133       | TermDestructor of destructor
134       | TermLiteral of literal
135     type term = info * bare_term
136
137     type bare_result =
138     (*| Symbol of ... *)
139     (*| Closure of ... *)
140       | ResLambda of identifier * term
141       | ResPrimfun of primfun
142       | ResConstructor of constructor
143       | ResDestructor of destructor
144       | ResLiteral of literal
145     type result = info * bare_result
146
147
148 We'll explain the `Symbol` and `Closure` variants on the `bare_result` datatype below.
149
150 Having these two parallel datatypes is rather annoying, and requires us to insert some translation functions `term_of_result` and `result_of_term` at a few places in the program. But the core, non-fancy parts of OCaml don't supply any more elegant way to specify that one datatype overlaps or is a subtype of another, so this is what works best.
151
152 A **third complication** has to do with environments. On the one hand, we don't have any really compelling need for environments in the first phase of the exercise, when we're just making a substitute-and-repeat interpreter. They don't play any role in the fundamental task we're focusing on. But on the other hand, weaving environments into the system when we *will* need them, for the second phase of the exercise, is not simple and would require lots of code changes. So that is a reason to include them from the beginning, just off to the side not doing any important work until we want them.
153
154 And as long as we've got them at the party, we might just as well give them _something_ to do. Pierce's original code takes a source file as input, which it expects to contain a sequence of terms or other toplevel declarations separated by semicolons, and prints out the result of maximally reducing each of the terms. Note I said "or other toplevel declarations." In addition to terms like this:
155
156     1 + 2;
157     let x = 1 in x + 2
158
159 that code also accepted toplevel declarations like this:
160
161     let y = 1 + 2 end
162
163 which means that we should reduce the rhs `1 + 2`, and *save* the result to be used for any locally-unbound occurrences of `y` in later terms. If the interpreter encounters *other* locally-unbound variables, where no such toplevel binding has been established, it will fail with an error. Thus:
164
165     let y = 1 + 2 end;
166     let x = 0 in (x,y)
167
168 will evaluate to `(0,3)`, but:
169
170     let y = 1 + 2 end;
171     let x = 0 in (x,w)
172
173 will crash, because `w` has no result bound to it. Note that you can locally rebind variables like `y` that have toplevel bindings. Thus:
174
175     let y = 1 + 2 end;
176     (y, (let y = 0 in y))
177
178 evaluates to `(3,0)`. (You have to enclose the `let y = 0 in y` in parentheses in order to embed it in terms like the pair construction `(_, _)`.)
179
180 Note that what I'm writing above isn't the syntax parsed by Pierce's original code. He uses a syntax that would be unfamiliar to you, so we've translated his code into a more local dialect; and the above examples are expressed using that dialect.
181
182 Pierce's code had a second kind of toplevel declaration, too, which looks like this (in our dialect, not his):
183
184     symbol w;
185     let x = 0 in (x,w)
186
187 Now that won't crash, but will instead evaluate to `(0,w)`. The code now treats unbound occurrences of `w` as atomic uninterpreted symbols, like Scheme's `'w`. And these symbols do count as results. (They are also available to be rebound; that is, you are allowed to say `symbol w; let w = 0 in ...`. But perhaps we should prohibit that.)
188
189 So these two kinds of toplevel declarations are already handled by Pierce's code, in a form, and it seemed neatest just to clean them up to our taste and leave them in place. And environments are needed, even in the VA/substitute-and-repeat interpreter (which is all Pierce's code provides), to implement those toplevel declarations. But as I said before, you can for now just think of the environments as sitting in the sidelines. They aren't used in any way for interpreting terms like:
190
191     let y = 1 + 2 in
192     let x = y + 10 in
193     (x, y)
194
195 Okay, that **completes our survey of the complications**.
196
197 The VA/reducuction-based interpreter
198 ------------------------------------
199
200 For one part of the homework, we had you complete a `reduce_head_once` function that converts OCaml values like:
201
202     TermApp(TermApp(TermLambda("x", TermApp(Var "x", Var "y")), TermLambda("w", Var "w")), ...)
203
204 to:
205
206     TermApp(TermApp(TermLambda("w", Var "w"), Var "y"), ...)
207
208 The further reduction, to:
209
210     TermApp(Var "y", ...)
211
212 has to come from a subsequent re-invocation of the function.
213
214 Let's think about how we should detect that the term has been reduced as far as we can take it. In the substitute-and-repeat interpreter Chris demonstrated for combinatory logic, we had the `reduce_if_redex` function perform a single reduction *if it could*, and then it was up to the caller to compare the result to the original term to see whether any reduction took place. That worked for the example we had. But it has some disadvantages. One is that it's inefficient. Another is that it's sensitive to the idiosyncrasies of how your programming language handles equality comparisons on complex structures; and these details turn out to be very complex and vary from language to language (and even across different versions of different implementations of a single language). We'd be glad to discuss these subtleties offline, but if you're not prepared to master them, it would be smart to foster an ingrained hesitation to blindly applying a language's `=` operator to complex structures. (Some problem cases: large numbers, set structures, structures that contain functions, cyclic structures.) A third difficulty is that it's sensitive to the particular combinators we took as basic. With `S` and `K` and `I`, it can never happen that a term has been reduced, but the output is identical to the input. That can happen in the lambda calculus, though (remember `ω ω`); and it can happen in combinatory logic if other terms are chosen as primitive (`W W1 W2` reduces to `W1 W2 W2`, so let them all just be plain `W`s).
215
216 So let's consider different strategies for how to detect that the term cannot be reduced any further. One possibility is to write a function that traverses the term ahead of time, and just reports whether it's already a result, without trying to perform any reductions itself. Another strategy is to "raise an exception" or error when we ask the `reduce_head_once` function to reduce an irreducible term; then we can use OCaml's error-handling facilities to "catch" the error at an earlier point in our code and we'll know then that we're finished. Pierce's code used a mix of these two strategies.
217
218 What we're going to do instead is to have our `reduce_head_once` function wrap up its output in a special datatype, that describes how that output was reached. That type looks like this:
219
220       type reduceOutcome = AlreadyResult of result | StuckAt of term | ReducedTo of term
221
222 That is, one possible outcome is that the term supplied is already a result, and so can't be reduced further for that reason. In that case, we use the first variant. We could omit the `of result` parameter, since the code that called `reduce_head_once` already knows what term it was trying to reduce; but in some cases it's a bit more convenient to have `reduce_head_once`  tell us explicitly what the result was, so we make that accompany the `AlreadyResult` tag. A second outcome is that the term is "stuck" and so for that reason also can't be reduced further. In this case, we want to supply the stuck subterm, and propagate that upward through the recursive calls to `reduce_head_once`, so that the callers can see specifically what subterm it was that caused the trouble. Finally, there is also the possibility that we *were* able to reduce the term by one step, in which case we return `ReducedTo newly_reduced_term`.
223
224 The structure of our `reduce_head_once` function, then, will look like this:
225
226     let rec reduce_head_once (term : term) (env : env) : reduceOutcome =
227       match term with
228       | _,TermLambda _
229       | _,TermPrimfun _
230       | _,TermConstructor _
231       | _,TermDestructor _
232       | _,TermLiteral _ -> AlreadyResult (result_of_term term)
233
234       | fi,TermVar var -> ...
235
236       (* notice we never evaluate a yes/no branch until it is chosen *)
237       | _,TermIf((_,TermLiteral(Bool true)),yes,no) ->
238           ReducedTo yes
239       | _,TermIf((_,TermLiteral(Bool false)),yes,no) ->
240           ReducedTo no
241       | fi,TermIf(test,yes,no) ->
242           (match reduce_head_once test env with
243           | AlreadyResult _ -> StuckAt term (* if test was not reducible to a bool, the if-term is not reducible at all *)
244           | StuckAt _ as outcome -> outcome (* propagate Stuck subterm *)
245           | ReducedTo test' -> ReducedTo(fi,TermIf(test',yes,no)))
246
247       | ...
248   
249
250 The homework asked you to fill in some of the gaps in this function. As mentioned before, the only role that environments play in this function is to see if variables are associated with any toplevel bindings. (If you're willing to forego those, you can select an implementation `Env0` of the environments that is guaranteed to do nothing.)
251
252 Now, some function needs to call the `reduce_head_once` function repeatedly and figure out when it's appropriate to stop. This is done by the `reduce` function, which looks like this:
253
254     let rec reduce (term : term) (env : env) : result =
255       match reduce_head_once term with
256       | AlreadyResult res -> res
257       | StuckAt subterm -> die_with_stuck_term subterm
258       | ReducedTo term' -> reduce term' env (* keep trying *)
259
260 This recursively calls `reduce_head_once` until it gets a result or gets stuck. In the latter case, it calls a function that prints an error message and quits the program. If it did get a result, it returns that to the caller.
261
262 The structure of these two functions, `reduce_head_once` and `reduce`, is similar to the functions `reduce_if_redex` and `reduce_try2` in the [[combinatory evaluator|/code/ski_evaluator.ml]]. The only difference is that `reduce_if_redex` only
263 performed a reduction if its argument was exactly a redex. It had to rely on its caller to detect cases where the term was instead a longer sequence of applications that had a redex at its head.  In the present code, on the other hand, we have `reduce_head_once` take care of this itself, by calling itself recursively where appropriate. Still, it will only perform at most one reduction per invocation.
264
265 One of the helper functions used by `reduce_head_once` is a `substitute` function, which begins:
266
267     let rec substitute (ident : identifier) (replacement : term) (original : term) =
268       match original with ...
269
270 This makes sure to substitute the replacement for any free occurrences of `Var ident` in the original, renaming bound variables in the original as needed so that no terms free in the replacement become captured by binding `Lambda`s or `Let`s in the original. This function is tricky to write correctly; so we supplied it for you.
271
272 However, one of the helper functions that *it* calls is `free_in (ident : identifier) (term : term) : bool`, and this was a function that you did [[write for an earlier homework|/exercises/assignment5/#occurs_free]]. Hence we asked you to adapt your implementation of that to the term datatype used in this interpreter. Here is a skeleton of this function:
273
274     let rec free_in (ident : identifier) (term : term) : bool =
275       match term with
276       | _,TermVar(var_ident) -> var_ident = ident
277       | _,TermApp(head, arg) ->
278           ...
279       | _,TermLambda(bound_ident, body) ->
280           ...
281       | _,TermLet(bound_ident, arg, body) ->
282           ...
283       | _,TermLetRec _ -> failwith "letrec not implemented"
284       | _,TermIf(test, yes, no) ->
285           ...
286       | _,TermPrimfun _ | _,TermConstructor _ | _,TermDestructor | _,TermLiteral _ -> false
287
288
289 That is, `Var ident` occurs free in `Var var_ident` iff the identifiers `ident` and `var_ident` are the same. The last four cases are easy: primitive functions, constructors, destructors, and literals contain no bindable variables so variables never occur free in them. These values may contain *results*, for instance if we partially apply the primitive function `+` to `3`, what we'll get back is another primitive function that remembers it has already been applied to `3`. But our interpreter is set up to make sure that this only happens when the argument (`3`) is already a result, and in our design that means it doesn't contain any bindable variables.
290
291 But now what about the cases for `App`, `Lambda`, `Let`, and `If`? Think about what the code for these should look like. It's just an adaptation/extension of what you did in the previous week's homework. In the assignment, we supplied some of the code for these, and asked you to complete the rest.
292
293 We also asked you to fill in some gaps in the `reduce_head_once` function.
294
295
296 Moving to the VB/environment-based interpreter
297 ----------------------------------------------
298
299 The previous interpreter strategy is nice because it corresponds so closely to the reduction rules we give when specifying our lambda calculus. (Including specifying evaluation order, which redexes it's allowed to reduce, and so on.) But keeping track of free and bound variables, computing fresh variables when needed, that's all a pain.
300
301 Here's a better strategy. Instead of keeping all of the information about which variables have been bound or are still free implicitly inside of the terms, we'll keep a separate scorecard, which we will call an "environment". This is a familiar strategy for philosophers of language and for linguists, since it amounts to evaluating terms relative to an assignment function. The difference between the substitute-and-repeat approach above, and this approach, is one huge step towards monads.
302
303 [[Read this page explaining about the need for Closures in this interpreter strategy.|/topics/week7_environments_and_closures]].
304
305 Now `Closure`s are not a new kind of lambda _term_: the syntax for our language doesn't have any constituents that get parsed into `Closure`s. `Closure`s are only created _during the course of evaluating_ terms: specifically, when a variable gets bound to an abstract, which may itself contain variables that are locally free (not bound by the abstract itself). This is why we have separate datatypes for _terms_ and for the _results_ that terms can evaluate to. `Closure`s are results, but they aren't terms. `App`s are terms, but not results. Our boolean and number literals, as well as our primitive functions, constructors, and destructors, are both.
306
307 In later weeks, we will see more examples of results that aren't terms, but can only be generated during the course of a computation. (I'm thinking of mutable reference cells. Arguably, partially applied constructors are yet another example, that we're already familiar with.)
308
309
310 Getting, reading, and compiling the source code
311 -----------------------------------------------
312
313 You can download the source code for the intepreter [[here|/code/untyped_full-1.7.tgz]]. That link will always give you the latest version. We will update it as we find any issues. Let us know about any difficulties you experience.
314
315 When you unpack the downloaded source code, you will get a folder with the following contents, sorted here by logical order rather than alphabetically.
316
317     interface.mli
318     types.ml
319     engine.ml
320     main.ml
321     primitives.ml
322     hilevel.ml
323     lolevel.ml
324     lexer.mll
325     parser.mly
326     types.mli
327     engine.mli
328     primitives.mli
329     hilevel.mli
330     lolevel.mli
331     Makefile
332     test.f
333     .depend
334
335 The first three files in this list are the ones you should focus on.
336
337 An `.mli` file like `interface.mli` specifies types for OCaml, in a way that gets published for other files in the same program to see. This `interface.mli` file contains the basic datatypes the program works with. And even this file (necessarily) has some complexity you can ignore. All you really need to pay attention to at first are the datatypes we described before.
338
339 The second file, `types.ml`, contains different implementations for the environments. If you like, you can look at how these work. The common interface these implementations have to supply is declared in the previous file:
340
341     module type ENV = sig
342       type env
343       val empty : env
344       val shift : identifier -> binding -> env -> env
345       val lookup : identifier -> env -> binding option
346       val version : string
347     end (* ENV *)
348
349 Each implementation of that interface is itself pretty simple, though the file `types.ml` does need to have some trickery in it to work around constraints imposed by OCaml. (The trickery is marked as such.)
350
351 OCaml's terminology for the _abstract interfaces_ is `module type S = sig ... end`, and its terminology for the _concrete implementations_ of these is `module M = struct ... end`. (By the way, the `*.mli` files get compiled into the former of these, and the `*.ml` files get compiled into the latter.) The implementations have to define (at least) all the types and values declared in the abstract interface. Notice that in the `ENV` interface, we just said `type env`. That means there _has to be_ some type `env`; but different implementations can define it differently. Also, when other parts of the code _use_ the interface, the details of how the `env` type is implemented won't be exposed to them. They have to interact with the `env`s via the declared `shift` and `lookup` functions, and the `empty` environment that every implementation is obliged to provide.
352
353 What the function `lookup` does is take an identifier like `"x"` and an existing `env`, and try to return the `result` that this `env` associates with that identifier, if any. Else it returns `None`. (There are some complications, in that we don't really return a `result option`, but rather a `binding option`, where the `binding` type is a small wrapper around a type `bound`, which is identified with the type `result`. The point of the `binding` wrapper is to help handle the toplevel declarations. But you can ignore that and just think of the `binding`s as `bound`/`result`s. The point of having the two identified types `bound` and `result` is to prepare for later developments. The `result` is what a term like `Var "x"` evaluates to (in a context where it's not free). The `bound` is what the environment binds the identifier `"x"` to. In our present system, these are of course the same. But later when we introduce mutable state into our system, they may come apart, depending on design choices we make.)
354
355 What the function `shift` does is take an `env` and add a new binding for a given identifier. It returns an `env` with this new binding. The identifier may or may not have already had a binding in the original `env`; but in any case, the new `env` will only return the supplied new `binding` when you `lookup` the `ident`.
356
357 As we've said, there are different ways to implement these environments. That's what's in the `types.ml` file. The `Env0` implementation provides the demanded interface, but doesn't do anything. It won't remember any new bindings. You can select this for the VA interpreter, if you like, to demonstrate that the `env`s are inessential to that interpretation strategy. (Though in that case the toplevel declarations won't be remembered.) `Env1` implements the environments as a list of pairs of identifiers and bindings. `Env2` implements the environments instead as functions from identifiers to `Some binding` or to `None`, if the identifier has no binding in that environment. At the end of the file `types.ml` is the line:
358
359     include Env1
360
361 You can change that to whichever of these implementations you'd like to use.
362
363 The third file, `engine.ml`, is where the action is. Most of the homework assignment was just a simplified version of this file. At the bottom of the file are also instructions on how to shift the interpreter between using the VA or the VB functions:
364
365     (* Put comment (* *)s around exactly one of the following two pairs of lines. *)
366
367     let version = "A (reduce by substituting; " ^ version ^ ")"
368     let interpret = VA.reduce
369
370     (*
371     let version = "B (use environment for local bindings; " ^ version ^ ")"
372     let interpret = VB.evaluate
373     *)
374
375
376 You can try building and running the interpreter like this. First, make sure you're in a Terminal and that your working directory is the folder that the source code unpacked to. Then just type `make`. That should take care of everything. If you see errors that you don't think are your fault, let us know about them.
377
378 Possibly some Windows computers that _do_ have OCaml on them might nonetheless fail to have the `make` program. (It isn't OCaml-specific, and will be found by default on Macs and many Linux systems.) In that case, you can try entering the following sequence of commands by hand:
379
380     ocamllex lexer.mll
381     ocamlyacc -v parser.mly
382     ocamlc -c lolevel.mli
383     ocamlc -c lolevel.ml
384     ocamlc -c interface.mli
385     ocamlc -c types.mli
386     ocamlc -c types.ml
387     ocamlc -c hilevel.mli
388     ocamlc -c hilevel.ml
389     ocamlc -c primitives.mli
390     ocamlc -w -8 -c primitives.ml
391     ocamlc -c engine.mli
392     ocamlc -c engine.ml
393     ocamlc -c parser.mli
394     ocamlc -c parser.ml
395     ocamlc -c lexer.ml
396     ocamlc -c main.ml
397     ocamlc -o interp.exe lolevel.cmo types.cmo hilevel.cmo primitives.cmo \
398       engine.cmo parser.cmo lexer.cmo main.cmo 
399
400
401 OK, I built the interpeter. How can I use it?
402 ---------------------------------------------
403
404 The interpreter you built is called `interp` (or on Windows, `interp.exe`). You can see its help message by running `./interp --help`.
405
406 The interpreter takes input that you feed it, by any of various methods, and passes it through a _parser_. The parser expects the input to contain a sequence of terms (plus possibly the other toplevel declarations we described before), separated by semicolons. It's optional whether to have a semicolon after the last term.
407
408 If the input doesn't parse correctly, you will get a "Syntax error." If it does parse, then the parser hands the result off to your interpretation functions (either `reduce`/`reduce_head_once` in VA of the interpreter, or `eval`/`evaluate`, in VB). If they are able to reduce/evaluate each term to a result, they will print those results in a user-friendly format, and then move to the next result. If they ever encounter a stuck term or unbound variable, they will instead fail with an error.
409
410 So how do you supply the interpreter with input. Suppose the file `./input` contains:
411
412     let x = 3 in
413     (x, 0);
414     5*2 - 1;
415     \x. x
416
417 Then here is a demonstration of three methods for supplying input. These will all give equivalent results:
418
419  *  `./interp input`
420  *  `echo 'let x = 3 in (x, 0); 5*2 - 1; \x. x' | ./interp -`
421  *  `./interp -e 'let x = 3 in (x, 0)' -e '5*2 - 1' -e '\x. x'`
422
423 In the last method, the different `-e` elements are concatenated with `;`s; and then it works just like the preceding methods.
424
425 The format the parser accepts should look somewhat familiar to you. Lambda expressions work as normal, except that they must always be "dotted" (that is, use `\x.x` not `\x x`). You can also use some infix operators in the ways you can in Kapulet and Haskell:
426
427     2-1
428     (-) 2 1
429     (2-) 1
430     (-1) 2 /* this works as in Kapulet not Haskell; it means 2-1 */
431     flip (-) 1 2
432
433 All giving the same result.
434
435 As an experiment, the parser accepts two kinds of numeric input. Numbers like `0`, `1`, and so on are handled as native OCaml numbers; whereas numbers like `0.`, `1.` and so on are handled as abbreviations for `Zero`, `Succ Zero` and so on, with the implied OCaml datatype:
436
437     type dotted_number = Zero | Succ of dotted_number
438
439 The supplied primitives `pred`, `succ`, and `zero?` work only on the dotted numbers; whereas the supplied infix primitives `+`, `-`, and `*` work only on the undotted numbers. There are also `<` and `<=` and `==` for the undotted numbers. (The parser will also accept `>` and `>=`, but will translate them into the corresponding uses of `<` and `<=`.)
440
441 This version of the interpreter doesn't come pre-equipped with any Church numbers (or booleans or tuples or lists), but you can code them manually if you like. You can also code a fixed point combinator manually if you like. But be sure to use [[Θ′ or Y′|topics/week4_fixed_point_combinators/#primed]], since the unprimed fixed point combinators we introduced you to won't terminate in a call-by-value interpreter, like this one. (The [[lambda evaluator on the website|/code/lambda_evaluator]], by contrast, uses a normal order evaluation strategy.)
442
443 Here is some more sample inputs, each of which the parser is happy with:
444
445     /* these are comments */
446     if zero? x then 1 else pred x
447     zero? 0. /* zero? and pred and succ work with dotted numbers */
448     x == 0 /* the infix comparison operators and + - * work with undotted numbers */
449     /* both of the following get translated into if-terms */
450     x and y
451     x or y
452     lambda x. x
453     \x. x
454     \x y. y (x y)
455     let x = 1 + 2 in 2 * x
456     let x = 1 + 2; y = x+1 in y
457     let f = \x.x+1 in f 0
458     let f x = x + 1 in f 0
459     true
460     (false,1)
461     (,1) true
462     (,) true 1
463     (,,) x y z /* but only up to triples, there are no bigger tuples */
464     box 1 /* this is a 1-tuple */
465     /* it won't be clear yet why it's useful, but wait for later weeks */
466     fst (1,2) /* evaluates to 1 */
467     /* you can use fst on boxes, pairs, and triples */
468     /*   snd also on pairs and triples */
469     /*   and trd on triples */
470     id x
471     const x y /* our friend the K combinator */
472     flip f x y /* gives f y x */
473     g o f /* `o` is an infix composition operator */
474     f x $ g y $ h z /* as in Haskell, this is f x (g y (h z)) */
475     /* note that it's not f x (g y) (h z) */
476     "strings" /* you can input these and pass them around, but can't perform any operations on them */
477
478 Predefined combinators include: `S`, `K` (same as `const`), `I` (same as `id`), `B` (same as `(o)`, occurring in prefix not infix position), `C` (same as `flip`), `T` (same as `flip ($)`), `V` (the Church pairing combinator), `W`, `M` (better known as `ω`), and `L`.
479
480 The parser also accepts `letrec ... in ...` terms, but currently there is no implementation for how to reduce/interpret these (that's for a later assignment), so you'll just get an error.
481
482 As explained before, you can also include toplevel declarations like:
483
484     let y = ... end;
485
486 Calling them "toplevel" means they can't be embedded inside terms. The above declaration interprets the rhs as a term, and then binds the variable `y` to the result, making it available in later terms where `y` hasn't been locally rebound. Thus:
487
488     let y = 1 + 2 end;
489     let x = 0 in (x,y)
490
491 gets interpreted as `(0,3)`.
492
493 Another toplevel declaration `symbol w` tells the interpreter that you want to specially designate `w` as okay to appear uninterpreted in terms you use.
494
495 If the interpreter encounters other locally-unbound variables, where no toplevel declaration has already been given, it will fail with an error.
496