<. These rules extend the rules you've
seen in lecture to support pairs, simple variants, and anonymous
functions.
**Exercise**: evaluate the following expressions using the substitution model.
Double check that the values that you produce match those produced by OCaml.
- `(3 + 5) * 2` (2 steps)
- `if 2 + 3 < 4 then 1 + 1 else 2 + 2` (4 steps)
- `let x = 2 + 2 in x + x` (3 steps)
- `let x = 1 in let x = x + x in x + x` (4 steps)
### Pairs
In OCaml, a pair of values `(v1,v2)` is a value. OCaml does not specify whether
pairs of expressions are evaluated from left to right or from right to left, but
the evaluation rules we've given for the core OCaml semantics above evaluate
from left to right (this is actually different from what the current implementation
of OCaml does, but since it's unspecified, it's bad to rely on one order or
the other!)
The syntax extension and evaluation rules are here:
```
e ::= ... | (e1,e2) | fst e | snd e
v ::= ... | (v1,v2)
(e1,e2) --> (e1',e2)
if e1 --> e1'
(v1,e2) --> (v1,e2')
if e2 --> e2'
fst e --> fst e'
if e --> e'
snd e --> snd e'
if e --> e'
fst (v1,v2) --> v1
snd (v1,v2) --> v2
```
**Exercise**: Evaluate the following expressions using the substitution model.
- `(3 + 5, 2 + 4)` (2 steps)
- `(fst (3,4), snd (3,4))` (2 steps)
- `((if fst (true, 3) then snd (1,2) else 3), if snd (3,false) then snd (1,2) else 3)` (5 steps)
### Functions
Function evaluation in the substitution model is very similar to the evaluation
of `let` expressions. Anonymous functions are values, and do
not evaluate any further. To evaluate a function application,
we first evaluate the function being applied, then we evaluate
the argument, then we substitute the argument into the body of
the function. Again, as with pairs, this order is unspecified for OCaml, and
is different in the current implementation of OCaml, so don't rely on the order!
Here are the syntax and evaluation rules for functions:
```
e ::= ... | e1 e2 | fun x -> e
v ::= fun x -> e
e1 e2 --> e1' e2
if e1 --> e1'
v1 e2 --> v1 e2'
if e2 --> e2'
(fun x -> e) v --> e{v/x}
```
**Exercise**: Evaluate the following expressions using the substitution model.
- `(fun x -> 3 + x) 2` (2 steps)
- `let f = (fun x -> x + x) in (f 3) + (f 3)` (6 steps)
- `let f = (fun x -> fun y -> x + y) in let g = f 3 in g 1 + (f 2 3)` (9 steps)
- `let f = fun x -> x + x in let x = 1 in let g = fun y -> x + f y in g 3` (7 steps)
### Pattern matching
The rules for pattern matching in the core OCaml notes above are not as general
as the `match` statement you've grown to know and love.
In the core OCaml notes, there are only two patterns: `Left x` and `Right x`.
Recall that a pattern in full OCaml can be any non-function value with any
subexpression replaced by variables.
**Exercise**: use this definition to write a BNF grammar for patterns (since
patterns are syntactically like values, you may want to refer to the BNF
grammar for values).
```
p ::=
```
Using the syntax for patterns, we can extend the BNF for expressions to include
match expressions. Unfortunately both the syntax and the meta-syntax use the
`|` symbol; be aware that the entire `match` line is a single syntactic form
that happens to include some `|` characters in it; I've written parentheses to
clarify:
```
e ::= ... | (match e with | p1 -> e1 | p2 -> e2 | ... | pn -> en)
```
How do we evaluate match statements? We start by evaluating the expression
being matched down to a value. We then consider each pattern one-by-one; if
the value matches the pattern, we evaluate to the body, but if it doesn't match
we move onto the next pattern.
**Exercise**: complete the first evaluation rule for `match`, indicating that we
start by evaluating the value being matched:
```
match e with | p1 -> e1 | p2 -> e2 | ... | pn -> en --> ???
if ???
```
**Exercise**: complete an evaluation rule for `match` that indicates that we move
on to the next pattern if the first one doesn't match:
```
match v with | p1 -> e1 | p2 -> e2 | ... | pn -> en --> ???
if v does not match p1
```
What does it mean for `v` to match `p`? Recall that `p` is a value with some
variables in place of subexpressions. `v` matches `p` if there are values we
can substitute into those variables to make `v` and `p` the same.
**Exercise**: complete an evaluation rule for `match` expressions for when the
value does match the first pattern:
```
match v with | p1 -> e1 | p2 -> e2 | ... | pn -> en --> ???
if v = ???
```
**Exercise**: double check your rules by evaluating the following expression:
- `match (1 + 2, 3) with | (1,0) -> 4 | (1,x) -> x | (x,y) -> x + y` (5 steps)
## Interpreter
In the [provided code](rec-code.zip) we have provided an interpreter for a
subset of OCaml using the substitution model. For clarity, we'll refer to this
subset of OCaml as OCalf. The provided code contains the following:
- `ast.ml` and `ast.mli`: the abstract syntax tree type for OCalf
- `eval.ml`: a partially completed interpreter using the substitution model
- `lexer.mll`. `parser.mly`, and `main.ml`: a grammar for OCalf
- `printer.ml` and `printer.mli`: functions for printing out ASTs nicely
- `top.ml`: configuration for the toplevel; you should `#use` this file.
- `.ocamlinit`: causes `utop` to automatically `#use "top.ml"` when you start
utop.
As in the previous recitation, you can build everything by running
```
ocamlbuild -use-menhir main.byte
```
at the command line.
The provided code differs from the interpreter you developed in class in a few
ways.
- Instead of just `+` and `&&`, we have a large
number of binary operators. These are all represented by a `BinOp` node in
the abstract syntax tree.
- We've added syntax for `let rec`, pairs, anonymous functions, variants, and
pattern matching.
- The `Eval.multistep` function prints the expression at each stage of evaluation:
```
utop # Eval.multistep (parse_expr "(3 + 5) * 2");;
(3 + 5) * 2
--> 8 * 2
--> 16
- : Ast.expr = 16
```
**Exercise**: Use `Eval.multistep` to check your answers to the first exercise
in this recitation.
**Exercise**: Complete the implementation of the `subst` function by writing
the substitution rules for pairs and functions.
**Exercise**: Complete the implementation of `step` by filling in the `If`,
`Pair`, `Fun` and `App` cases.
## Let rec (\*)
The evaluation rule for `let` is
```
let x = v in e --> e { v / x }
```
**Exercise**: This rule doesn't work properly for `let rec` expressions. Explain
what happens when you try to use it on the following expression:
```
let rec fact = fun x ->
if x <= 1 then 1 else x * (fact (x - 1)) in
fact 3
```
To solve this problem, when evaluating let rec statements in the substitution
model, you need to perform two substitutions: when evaluating
`let rec f = e1 in e2`, you need to first "unfold" f in the body of `e1` by
substituting the entire let rec statement in for f. Then you can substitute
this unfolded `f` into `e2`. Formally:
```
let rec f = v in e --> e{v{(let rec f = v in f)/f} / f}
```
**Exercise (\*)**: use this rule to evaluate the following expression (16 steps).
You may want to simplify your life by writing "F" in place of `(let rec fact =
fun x -> if x <= 1 then 1 else x * (fact (x-1)) in fact)`
```
let rec fact = fun x ->
if x <= 1 then 1 else x * (fact (x - 1)) in
fact 3
```
**Exercise (\*)**: Complete the `let rec` case in the interpreter. Use it to
double check your answer to the previous exercise.
]]>