For mini-project 1, you'll be building an interpreter for a small untyped subset of OCaml. This will mean building a parser and an evaluator. There will be no type checker for this project.
This mini-project is due on Thursday 4/03 by 8:00PM. It cannot be dropped. This is the "landing page" for the project, it does not contain any information about the project specification. The details of the project are given in the file assigns/interp1/spec.pdf.
To verify you're making progressing the mini-projects, you will be required to submit part of the mini-project, along with some written problems, by Thursday 03/27 8:00PM.
This time around, you must submit:
parse, 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.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.
The following is a variant of the toy-language from Assignment 6.
\begin{align*}
\textcolor{blue}{\texttt{<expr>}} &::= \textcolor{blue}{\texttt{<int>}} \\
&\hspace{3mm}| \hspace{2.5mm} \textcolor{red}{\texttt{true}} \\
&\hspace{3mm}| \hspace{2.5mm} \textcolor{red}{\texttt{false}} \\
&\hspace{3mm}| \hspace{2.5mm} \textcolor{red}{\texttt{(}} \ \textcolor{red}{\texttt{+}} \ \textcolor{blue}{\texttt{<expr>}} \ \textcolor{blue}{\texttt{<expr>}} \ \textcolor{red}{\texttt{)}} \\
&\hspace{3mm}| \hspace{2.5mm} \textcolor{red}{\texttt{(}} \ \textcolor{red}{\texttt{<}} \ \textcolor{blue}{\texttt{<expr>}} \ \textcolor{blue}{\texttt{<expr>}} \ \textcolor{red}{\texttt{)}} \\
&\hspace{3mm}| \hspace{2.5mm} \textcolor{red}{\texttt{(}} \ \textcolor{red}{\texttt{?}} \ \textcolor{blue}{\texttt{<expr>}} \ \textcolor{blue}{\texttt{<expr>}} \ \textcolor{blue}{\texttt{<expr>}} \ \textcolor{red}{\texttt{)}} \\
\end{align*}
Recall that values in small-step semantics must be part of the expression language itself. Here we take values in the big-step semantics to be integer and Boolean literals.
\frac
{n \text{ is an integer literal}}
{n \Downarrow n}
\qquad
\frac
{e_1 \Downarrow v_1 \qquad e_2 \Downarrow v_2 \qquad v_1 + v_2 = v}
{\texttt{(} \ \texttt{+} \ e_1 \ e_2 \ \texttt{)} \Downarrow v}
\qquad
\frac
{e_1 \Downarrow v_1 \qquad e_2 \Downarrow v_2 \qquad v_1 < v_2}
{\texttt{(} \ \texttt{<} \ e_1 \ e_2 \ \texttt{)} \Downarrow \texttt{true}}
\frac
{e_1 \Downarrow v_1 \qquad e_2 \Downarrow v_2 \qquad v_1 \geq v_2}
{\texttt{(} \ \texttt{<} \ e_1 \ e_2 \ \texttt{)} \Downarrow \texttt{false}}
\qquad
\frac
{e_1 \Downarrow \texttt{true} \qquad e_2 \Downarrow v_2}
{\texttt{(} \ \texttt{?} \ e_1 \ e_2 \ e_3 \ \texttt{)} \Downarrow v_2}
\qquad
\frac
{e_1 \Downarrow \texttt{false} \qquad e_3 \Downarrow v_3}
{\texttt{(} \ \texttt{?} \ e_1 \ e_2 \ e_3 \ \texttt{)} \Downarrow v_3}
Write down the small-step semantics (e \longrightarrow e') for this language so that it is equivalent to the big-step semantics given above. It should be the case that:
e \Downarrow v according to the big-step semantics above, then e \longrightarrow^* v according to the small-step semantics you give, where the reduction from e to v is unique.e is not evaluated with respect to the big-step semantics, then it should not be evaluated in the small-step semantics either (Hint. This is important for if-expressions).In technical parlance, \longrightarrow should be an adequate model of \Downarrow. As a hint, one rule of this system is the following.
\frac
{n \text{ is an integer literal} \qquad e \longrightarrow e'}
{\texttt{(} \ \texttt{<} \ n \ e \ \texttt{)}
\longrightarrow
\texttt{(} \ \texttt{<} \ n \ e' \ \texttt{)}}
The other rules will be similar.