Mini-Project 2: The Environment Model

One-Week Check-in

For the one-week check-in, you must submit:

• An implementation of desugar, as detailed in the mini-project specification. You should be able to leave your implementations of the other functions partial or empty as long as your code builds.
• Solutions to the written problems below.

Note. We will not re-test parts of the mini-project from the one-week check-in. To recieve full credit on the mini-project, you must successfully submit both the one-week check-in and the complete mini-project.

Written Problems

Desugaring

let foo (x : int) (y : int) : int =
  let bar (z : bool) : bool = z || x = y in
  bar true

let baz (x : unit) : int = foo 1 2

let biz : int = baz ()

Desugar the above program according to the desugaring rules given in the mini-project 2 specification (please use reasonable indentation to make it easier on our graders).

Closures

let x : int = 2 + 3 in
let g : int -> int = fun (x : int) -> x + x in
let f : int -> int = fun (y : int) -> g x in
let x : int -> int = g in
f

Determine the closure which the above expression evaluates to according to the semantic rules given in the mini-project 2 specification.

Semantic Derivation

let rec f : bool -> bool = fun (x : bool) -> x || f true in f false

Let e be the expression above. In the derivation of the judgment \langle \ \varnothing \ , \ e \ \rangle \ \Downarrow \top (according to the semantics rules given in the mini-project 2 specification) there are two places at which you need to derive a judgment of the form \langle \ \mathcal E \ , \ \texttt{x || f true} \ \rangle \Downarrow \top for some dynamic environment \mathcal E. Write down what that environment is in each of the two cases. To be clear, you don't need to write down the entire derivation of \langle \ \varnothing \ , \ e \ \rangle \ \Downarrow \top. You just need to write two judgments of the form:

\begin{align*}
\langle \ \mathcal E_1 \ , \ \texttt{x || f true} \ \rangle
&\Downarrow \top \\
\langle \ \mathcal E_2 \ , \ \texttt{x || f true} \ \rangle
&\Downarrow \top
\end{align*}

Both of which are derived within a derivation of \langle \ \varnothing \ , \ e \ \rangle \ \Downarrow \top.