## Substitution model warmup For this lab, you may find it useful to refer to the table of substitution model rules given in these [notes on a core subset of OCaml](core-ocaml.html). 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.