\documentclass[11pt]{article}
\usepackage{palatino}
\usepackage{fullpage}
\usepackage{latexsym}
\usepackage{verbatim}
\usepackage{amsmath,proof,amsthm,amssymb,enumerate}

\newcommand{\question}[2]
  {\bigskip \noindent
   {\bf Question #1} (#2 points).}

\newcommand{\task}[2]
  {\bigskip
   \noindent{\large\bf Task: #1 (#2 points)\newline}
  }


\newcommand{\extracreditquestion}[1]
  {\bigskip \noindent
   {\bf Question #1} (EXTRA CREDIT).}

\newcommand{\definition}[2]
  {\bigskip
   \begin{tabular}{p{1.5in}p{4.0in}}
        \textbf{#1} & #2 \\
        \end{tabular}
  }

\long\def\dummy#1\enddummy{}
\def\implies{\Rightarrow}

\def\hash{\texttt{\char"23}}
\newcommand{\arrayenv}[1]{\renewcommand{\arraystretch}{1}  \begin{array}[t]{@{}c@{}}#1\end{array}} 
\newcommand{\debruijn}[1]{\hash\ensuremath{#1}}
\newcommand{\subst}[3]{\{#1/#2\}#3}
% \newcommand{\shift}[2]{\ensuremath{\uparrow_{#1}(#2)}}
% \newcommand{\tr}[2]{\texttt{Tr}(#1, #2)}
% \def\db1{\debruijn{1}}
% \newcommand{\lookup}[2]{\texttt{lookup}(#1,#2)}


\title{Assignment 2: \\
       Implementing MinML}
\author{15-312: Foundations of Programming Languages \\
        Kevin Watkins ({\tt kw@cmu.edu})}
\date{Out: Thursday, 27 Jan 2004\\
Due: Thursday, 10 February 2004 (11:59 PM) \\[1em]
100 points total}

\begin{document}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}[theorem]{Lemma}

\maketitle

\section{Introduction}

This is our first programming assignment. For this assignment you will implement a typechecker and evaluator for
MinML in SML.

The code for
this assignment can be found in
$$\texttt{/afs/andrew/scs/cs/15-312/handout/2/}$$

In the assignment folder you'll find several files with
support code; you will only need to fill in the missing code in
\texttt{translate.sml}, \texttt{typing.sml}, and \texttt{eval.sml}.

\subsection{Handins}

This assignment must be turned in
electronically by 11:59 pm on Thursday, 10 February 2004. The files \texttt{translate.sml}, \texttt{typing.sml}, and
\texttt{eval.sml} must be handed in to
$$\texttt{/afs/andrew/scs/cs/15-312/handin/<yourid>/2/}$$

Your code must compile with the original versions of the other files,
so don't change them.
%Never change signatures, even in the files you
%modify, unless we ask you to.
If your code does not compile and
type-check, you will receive little or no credit. Note that only the three files listed above will actually be copied out of your directory, so don't do anything like adding more files to {\tt sources.cm}.

Also, please turn in any test cases you'd like us to use by copying
them to your handin directory.  To ensure that our scripts notice the
files, make sure they have the suffix {\tt .mml}.

Immediately after the deadline, we will run a script to sweep
through all the handin directories and copy your files elsewhere. We
will also sweep 24, 48, and 72 hours after the deadline, for anyone
using late days on this assignment. It is {\bf not} a good idea to work
on your code in the handin directory, because if you happen to be working
when a sweep happens, it might pick up a broken version of your code.
Instead, work on your code somewhere else, and copy it into your handin
directory whenever you have a working version. Note that your handin
directory may briefly be write-protected while a sweep is actually
happening.

You can write into your handin directory as often as you like. The last
distinct version picked up by the sweeps will be graded. If you would
rather have an earlier version graded (perhaps because you want to save on
late days) you {\bf must} tell Kevin Watkins before the expiration of the three
day late handin period.

If you work on your code in AFS, you are responsible for keeping your
working code inaccessible to other students in the class using AFS permissions. 
If you have world-readable code for an assignment in your AFS directory and
some other student ends up submitting code identical to yours, you will have
no way of defending yourself against charges of unacceptable
collaboration.

For more information on handing in code, refer to
$$\texttt{http://www.cs.cmu.edu/\char"7Ecrary/312/assignments.html}$$

\subsection{Grading}

Code for this assignment is graded on correctness and clarity. Don't
try to make your code more efficient if it costs clarity, because you
are not being graded on efficiency. For your reference, the sample solution
to this assignment has the following line counts:
\begin{center}\begin{tabular}{lr}
  \texttt{translate.sml} & 30 \\
  \texttt{typing.sml}    & 52 \\
  \texttt{eval.sml}      & 63 \\
\end{tabular}\end{center}
If you find yourself writing a lot more code than this, you may want to
rethink your approach.

\section{Overview of the supplied code}

Before you begin, you may wish to read through the provided code
(especially the signatures) to gain an understanding of the setup.
All of the necessary SML files are listed in the \texttt{sources.cm}
file, and you can build the project in SML/NJ by typing
\texttt{CM.make()}. The following files are included:
\begin{center}\begin{tabular}{ll}
  \texttt{minml.sml} & Abstract syntax of MinML \\[1ex]
  \texttt{stream.sml} & Lazy streams \\
  \texttt{input.sml} & Input as a lazy stream of characters \\
  \texttt{lexer.sml} & Lexical analysis \\
  \texttt{parse.sml} & Parsing concrete syntax into abstract syntax \\
  \texttt{print.sml} & Printing abstract syntax as concrete syntax \\[1ex]
  \texttt{translate.sig} & Signature for translation from named to de Bruijn form \\
  \texttt{translate.sml} & (To be filled in by you) \\
  \texttt{typing.sig} & Signature for type checker \\
  \texttt{typing.sml} & (To be filled in by you) \\
  \texttt{eval.sig} & Signature for evaluator \\
  \texttt{eval.sml} & (To be filled in by you) \\[1ex]
  \texttt{loop.sml} & Combinators for the top-level loop \\
  \texttt{top.sml} & The top-level loop \\
\end{tabular}\end{center}

\subsection{Abstract syntax}

\begin{figure}[tb]
\[\begin{array}{rcl}
k &::= & \texttt{0\ } | \texttt{\ 1\ } | \texttt{\ }... \\
\\
o &::=& \texttt{+ } | \texttt{ - } | \texttt{ * } | \texttt{ = } | \texttt{ < } | \texttt{ \~{} } \\
\\
\tau &::=& \texttt{int\ } | \texttt{\ bool\ } |   \texttt{\ }\tau_1 \to \tau_2\\
\\
e &::=& \texttt{num}(k) \,\,|\,\, \texttt{true} \,\,|\,\, \texttt{false}
        \,\,|\,\, x 
        \,\,|\,\, \texttt{fun}(\tau_1,\tau_2,f\,.\,x\,.\,e)\\
&    |& \texttt{}o(e_1,...,e_n) \,\,|\,\,
 \texttt{if}(e_1,e_2,e_3) \,\,|\,\,
 \texttt{apply}(e_1,e_2) \,\,|\,\,
 \texttt{let}(e_1,x\,.\,e_2)\\


\end{array} \]
\caption{Abstract syntax for MinML} \label{fig:absyn}
\end{figure}

The named-style abstract syntax of MinML is shown in Figure~\ref{fig:absyn}. 
For this assignment we will work with both named and de Bruijn-form
abstract syntax. In {\tt minml.sml} there are signatures and structures for
each. The {\em primitive operators} of MinML such as $+$ or $<$ are all represented
by a single SML constructor {\tt Primop}. Code in {\tt minml.sml} indicates
the types of each primitive operator and how they evaluate. The abstract
syntax groups binders with their scopes, in higher-order abstract syntax
style.

\subsection{Parsing}

The parser provided to you is based on lazy memoizing streams, which should
be familiar from 15-212. The code implementing streams is in {\tt stream.sml}.
Parsing itself happens in three stages.

\begin{itemize}
\item
First, a lazy stream of characters is
constructed. Forcing this stream causes the user to be prompted for input, or
characters to be read from a file, depending on what the current input source
is. This input code is in {\tt input.sml}.

\begin{figure}[tb]
\centering
\begin{tabular}{llllll}
\textbf{Symbol} & \textbf{Token} & \textbf{Symbol} & \textbf{Token} &
\textbf{Symbol} & \textbf{Token} \\
\hline
\verb+int+ & \texttt{INT} &
\verb+bool+ & \texttt{BOOL} &
\verb+->+ & \texttt{ARROW} \\
\verb+true+ & \texttt{TRUE} &
\verb+false+ & \texttt{FALSE} &
\verb+fun+ & \texttt{FUN} \\
\verb+is+ & \texttt{IS} &
\verb+end+ & \texttt{END} &
\verb+if+ & \texttt{IF} \\
\verb+then+ & \texttt{THEN} &
\verb+else+ & \texttt{ELSE} &
\verb+let+ & \texttt{LET} \\
\verb+in+ & \texttt{IN} &
\verb+(+ & \texttt{LPAREN} &
\verb+)+ & \texttt{RPAREN} \\
\verb+;+ & \texttt{SEMICOLON} &
\Large{\texttt{\char"7E}} & \texttt{NEGATE} &
\verb+=+ & \texttt{EQUALS} \\
\verb+<+ & \texttt{LESSTHAN} &
\verb+*+ & \texttt{TIMES} &
\verb+-+ & \texttt{MINUS} \\
\verb-+- & \texttt{PLUS} &
\verb+:+ & \texttt{COLON} \\[1ex]
$k$ & \texttt{NUMBER(}$k$\texttt{)} \\
$x$ & \texttt{VAR(}$x$\texttt{)} \\
\end{tabular}
\caption{MinML tokens} \label{fig:tokens}
\end{figure}

\item
Next, the stream of characters is transformed into a stream of {\em tokens}
by a lexical analyzer in {\tt lexer.sml}. The concrete syntax of tokens is shown in Figure~\ref{fig:tokens}. Each sort of token has a constructor in the SML datatype
{\tt Lexer.token}.

\begin{figure}[tb]
\centering
\begin{tabular}{rcl}
  \textit{program} &::=& \textit{exp}$_0$ \verb+;+ \\[1ex]
  \textit{exp}$_0$ &::=& \textit{exp}$_0$ \verb+=+ \textit{exp}$_1$
                         $\,|\,$ \textit{exp}$_0$ \verb+<+ \textit{exp}$_1$
                         $\,|\,$ \textit{exp}$_1$ \\
  \textit{exp}$_1$ &::=& \textit{exp}$_1$ \verb-+- \textit{exp}$_2$
                         $\,|\,$ \textit{exp}$_1$ \verb+-+ \textit{exp}$_2$
                         $\,|\,$ \textit{exp}$_2$ \\
  \textit{exp}$_2$ &::=& \textit{exp}$_2$ \verb+*+ \textit{exp}$_3$
                         $\,|\,$ \textit{exp}$_3$ \\
  \textit{exp}$_3$ &::=& {\Large{\texttt{\char"7E}}} \textit{exp}$_\infty$
                         $\,|\,$ \textit{exp}$_4$ \\
  \textit{exp}$_4$ &::=& \textit{exp}$_4$ \textit{exp}$_\infty$
                         $\,|\,$ \textit{exp}$_\infty$ \\
  \textit{exp}$_\infty$ &::=&
    \verb+(+ \textit{exp}$_0$ \verb+)+ $\,|\,$
    $k$ $\,|\,$
    $x$ $\,|\,$
    \verb+true+ $\,|\,$
    \verb+false+ \\
    &$|$&
    \verb+if+ \textit{exp}$_0$ \verb+then+ \textit{exp}$_0$
                               \verb+else+ \textit{exp}$_0$ \verb+end+ \\
    &$|$&
    \verb+let+ $x$ \verb+=+ \textit{exp}$_0$ \verb+in+
               \textit{exp}$_0$ \verb+end+ \\
    &$|$&
    \verb+fun+ $f$ \verb+(+ $x$ \verb+:+ \textit{type}$_0$ \verb+)+
       \verb+:+ \textit{type}$_0$ \verb+is+ \textit{exp}$_0$ \verb+end+ \\[1ex]
  \textit{type}$_0$ &::=& \textit{type}$_\infty$ \verb+->+ \textit{type}$_0$
                $\,|\,$ \textit{type}$_\infty$ \\
  \textit{type}$_\infty$ &::=& \verb+(+ \textit{type}$_0$ \verb+)+
                $\,|\,$ \verb+int+ $\,|\,$ \verb+bool+ \\
\end{tabular}
\caption{MinML concrete syntax} \label{fig:grammar}
\end{figure}

\item
Finally, the stream of tokens is transformed into a stream of expressions
by the parser in {\tt parse.sml}. The parser accepts the concrete grammar shown
in Figure~\ref{fig:grammar}. Note that the expressions produced by the
parser are in named form {\tt MinML.exp}, not de Bruijn form {\tt DBMinML.exp}.
\end{itemize}

The grammar should be mostly self-explanatory. Primitive operations have the
same precedences as in SML, and are left-associative. Application is shown
by writing the function $e_1$ and the argument $e_2$ next to each other as in
SML: $e_1\,e_2$. Function types are written $\tau_1 \rightarrow \tau_2$, where $\rightarrow$ is right-associative, as in SML. Some examples of MinML syntax at each of the three stages of parsing are shown in Figure~\ref{fig:parsing}.

\begin{figure}[tb]
\begin{tabular}{p{1.5in}p{2.0in}p{2.0in}}
\textbf{Concrete syntax} & \textbf{Lexer tokens} & \textbf{Abstract syntax} \\
\hline
\texttt{true} & \texttt{TRUE} & \texttt{Bool(true)} \\
 & & \\
\texttt{1} & \texttt{NUMBER(1)} & \texttt{Int(1)} \\
 & & \\
\texttt{if true then 4 else 5 end} & \texttt{IF TRUE THEN NUMBER(4) ELSE NUMBER(5) END}
     & \texttt{If(Bool(true), Int(4), Int(5))} \\
 & & \\
\texttt{f 3} & \texttt{VAR("f") NUMBER(3)} & \texttt{Apply(Var("f"), Int(3))} \\
 & & \\
\texttt{1 + 2} & \texttt{NUMBER(1) PLUS NUMBER(2)} & \texttt{Primop(Plus, [Int(1), Int(2)])} \\
 & & \\
\texttt{1 + g 2 * 3} & \texttt{NUMBER(1) PLUS VAR("g") NUMBER(2) TIMES NUMBER(3)} & \texttt{Primop(Plus, [Int(1), Primop(Times, [Apply(Var("g"), Int(2)), Int(3)])])} \\
 & & \\
\texttt{fun f(g :\ int -> bool -> int) :\ bool is true end}
  & \texttt{FUN VAR("f") LPAREN VAR("g") COLON INT ARROW BOOL ARROW INT RPAREN COLON BOOL IS TRUE END}
  & \texttt{Fun(ARROW(INT, ARROW(BOOL, INT)), BOOL, ("f", "g", Bool(true)))} \\
 & & \\
\end{tabular}
\label{fig:parsing}
\caption{Examples of MinML parsing}
\end{figure}

\subsection{Printing}

Code for printing both named- and de Bruijn-style abstract syntax is provided
for you in {\tt print.sml}.  The printer tries to eliminate redundant
parentheses where possible.

\subsection{Top-level loop}

The files {\tt loop.sml} and {\tt top.sml} implement a top-level loop for
MinML similar to SML/NJ's. The top-level loop reads
expressions one at a time, and performs some action on each one. Using
the combinators in {\tt loop.sml} you can set up a top-level loop that
performs actions like type-checking and stepwise evaluation. Some
useful top-level loops are already defined in {\tt top.sml}.

\subsection{Test cases}

We've also provided a few test cases in files of the form {\em foo}{\tt .mml}.

\bigskip

\begin{tabular}{llp{1.5in}}
\textbf{Filename} & \textbf{Expected Result} & \textbf{Description} \\
\hline
\texttt{if.mml} & \verb+3 : int+ & Simple test of \texttt{if} \\
 & & \\
\texttt{fun.mml} & \arrayenv{\texttt{fun ident(x :\ int) :\ int is } \\
                                       \texttt{x  end : int -> int}} & Simple test of \texttt{fun} \\
 & & \\
\texttt{factorial.mml} & \verb+120 : int+ & The factorial function \\
 & & \\
\texttt{self.mml} & \textit{ill-typed} & Ill-typed function \\
 & & \\
\texttt{hof.mml} & \verb+7 : int+ & Simulates pairs using functions \\
\end{tabular}

\bigskip

These can be run using the functions {\tt Top.file\_}{\em something} in
{\tt top.sml}. These test files are (obviously) not exhaustive, so part of
this assignment is developing your own test files in order to test each case
in your code thoroughly. Remember, however, that passing test cases only
helps you make your code {\em correct}; you will also be graded on {\em clarity}.

You are encouraged to submit your test cases to us. After everyone's
homework is submitted, we will collect all the test cases together with
some of our own, and test your code with all of them. The results of these
tests will be factored into the correctness part of your grade. So,
although you will not receive extra points directly for submitting
test cases, it is still in your interest to make up some that your
code handles correctly, since they will tend to improve your grade. See
the beginning of the assignment for instructions on how to submit your
test cases.

To play around with the parser and become familiar with MinML, type
$$\verb+Top.loop_print_noDB ();+$$
or
$$\verb+Top.file_print_noDB "+\textit{test\_file}\verb+.mml";+$$
These will print the program (with some redundant parentheses) in the
named-variable form.

\section{Your tasks}

\subsection{Variables and binding}

In this part of the assignment, you will translate MinML terms from the
named representation to a de Bruijn representation. To get started, read
Section 5.4 of Robert Harper's notes, then think about how
to translate the abstract syntax.  Most cases are very straightforward;
variables, \texttt{let}, and \texttt{fun} require a little thought.  For
\texttt{fun}, which binds {\it two} variables at once (the function and
its argument), use the convention that the de Bruijn index
$\debruijn{1}$ refers to the argument and the de Bruijn index
$\debruijn{2}$ to the function itself. For example:

\bigskip

\noindent
\begin{tabular}{|p{0.45\textwidth}|p{0.5\textwidth}|}
\hline
\textbf{Named} & \textbf{de Bruijn} \\
\hline
\texttt{fun fact (x :\ int) :\ int is \newline 
~~if x=0 then 1 else x*fact(x-1) end \newline
end} &
\texttt{fun }$\lambda$\texttt{ (}$\lambda$\texttt{ :\ int) :\ int is \newline
if \debruijn{1}=0 then 1 else \debruijn{1}*\debruijn{2}(\debruijn{1}-1) end \newline
end} \\
\hline
\end{tabular}

\task{Translation to de Bruijn form}{20}

In file \texttt{translate.sml}, complete the implementation of
function \verb+Translate.translate+.  When completed, it should
translate a closed MinML expression in the named variable
representation (type \verb+MinML.exp+) to a closed
expression in the de Bruijn representation (type \verb+DBMinML.exp+).
Your implementation of \verb+Translate.translate+ should satisfy the
following specification:
\begin{quote}
If $e$ is a closed named-form term, then $\texttt{Translate.translate(}e\texttt{)} = e'$, where $e'$ is its de Bruijn-form counterpart.

If $e$ is not closed, then $\texttt{Translate.translate(}e\texttt{)} = \texttt{raise Translate.Error(}s\texttt{)}$ for some informative string $s$.
\end{quote}

In the translator, you will need to maintain an environment of variable names.  Use the
simplest representation possible; don't worry about efficiency.

\subsection{Static semantics}

Next, you will implement a typechecker for MinML in de Bruijn form. The static
semantics for MinML, given in Figure \ref{typingrules}, has the property that
every expression has at most one type. Your typechecker
will return the unique type for an expression if it is well-typed, or
raise the exception \texttt{Typing.Error}($s$) with some informative
string $s$ otherwise.

\def\G{\Gamma}
\def\int{\texttt{int}}
\def\bool{\texttt{bool}}
\newcommand{\entails}{\vdash}

\begin{figure}[tbp]
\centering
\renewcommand{\arraystretch}{3}
\begin{tabular}{r l}
% \infer[\textit{VarTyp1}]{\G;\tau \entails \debruijn{1} : \tau}{}
%
% \\
%
% \infer[\textit{VarTypK}]{\G;\tau' \entails \debruijn{k + 1} : \tau}
%        {\G \entails \debruijn{k} : \tau}
%
% \\
\infer[\textit{VarTyp}]{\G \entails x : \tau}{\G(x) = \tau}

\\

\infer[\textit{NumTyp}]{\G \entails k : \int}{}

\\

\infer[\textit{TrueTyp}]{\G \entails \texttt{true} : \bool}{}
&
% \infer[\textit{IfTyp}]{\G \entails \texttt{if}\, e_c \,\texttt{then}\, e_t \,\texttt{else}\, e_f \,\texttt{fi} : \tau}{\G \entails e_c : \bool & \G \entails e_t : \tau & \G \entails e_f : \tau}

\infer[\textit{IfTyp}]{\G \entails \texttt{if}(e, e_1, e_2) : \tau}
      {\G \entails e : \bool & \G \entails e_1 : \tau & \G \entails e_2 : \tau}

\\

\infer[\textit{FalseTyp}]{\G \entails \texttt{false} : \bool}{}

\\
%\infer[\textit{FunTyp}]{\G \entails \texttt{fun}\, f (x : \tau_1) : \tau_2 \,\texttt{is}\, e \,\texttt{end} : \tau_1 \to \tau_2}
%        {\G;(\tau_1 \to \tau_2);\tau_1 \entails e : \tau_2}
\infer[\textit{FunTyp}]{\G \entails \texttt{fun}(\tau_1, \tau_2, f.x.e) : \tau_1 \to \tau_2}
  {\G, f{:}\tau_1 \to \tau_2, x{:}\tau_1 \entails e : \tau_2}

&
\infer[\textit{AppTyp}]{\G \entails \texttt{apply}(e_1, e_2) : \tau}{\G \entails e_1 : \tau_2 \to \tau & \G \entails e_2 : \tau_2}


\\

\infer[\textit{OpTyp}]{\G \entails o(e_1, \ldots, e_n) : \tau_o}{\G \entails e_1 : \tau_{o1} & ... & \G \entails e_n : \tau_{on}}
\\
% \infer[\textit{LetTyp}]{\G \entails \texttt{let}\,x\: \texttt{=}\:e_1
%                              \:\texttt{in}\: e_2 \:\texttt{end} : \tau_2}{\G \entails e_1 : \tau_1 & \G; \tau_1 \entails e_2 : \tau_2}
\infer[\textit{LetTyp}]{\G \entails \texttt{let}(e_1, x.e_2) : \tau_2}
 {\G \entails e_1 : \tau_1 & \G, x{:}\tau_1 \entails e_2 : \tau_2}
\end{tabular}
\renewcommand{\arraystretch}{1}

\caption{Static semantics for MinML} \label{typingrules}

\end{figure}

Recall that the specification of MinML uses a \emph{typing judgment}
to classify MinML expressions as ill- or well-typed. The typing
judgment is defined inductively by the inference rules. Therefore, in
order to decide whether a given expression has a type, we need to
search for a derivation using the typing rules.

In general, we cannot assume that an expression matches only one
typing rule and thus, the search strategy for a derivation can be
\emph{non-deterministic}. Fortunately, the search strategy for MinML
is \emph{syntax directed}: the form of expression we are typing
determines uniquely which rule to apply. Therefore, if the typechecker
finds that no rule can be applied to an expression, it knows that the
expression is ill-typed and can raise an exception immediately. Otherwise,
the typechecker can apply the (unique) appropriate typing rule.
Your code will probably have one function clause for
each constructor of the datatype \texttt{DBMinML.exp}.

We provide a function \texttt{MinML.typeOfPrimop}
that returns the domain and range types for a primop. These correspond
to the types $\tau_{oi}$ and $\tau_o$ in the rule {\em OpTyp}. Your
typechecker should use this function. It should remain correct even if
the language were later extended with additional primops (potentially having zero or more than two arguments).

\task{Typechecker}{35}

Complete the code in \texttt{typing.sml} to produce a structure
\texttt{Typing :> TYPING} which implements the behavior specified. You
should not modify any other files. Remember that the expression to be 
typechecked will be in de Bruijn form. Your function \texttt{Typing.typeOf}
should have the following property.
\begin{quote}
  If $\cdot\vdash e : \tau$ for some (unique) $\tau$, then
  $\texttt{Typing.typeOf(}e\texttt{)} = \tau$.

  If $\cdot\vdash e : \tau$ does not hold for any $\tau$, then
  $\texttt{Typing.typeOf(}e\texttt{)} = \texttt{raise Typing.Error(}s\texttt{)}$
  for some $s$.
\end{quote}

Be sure that you implement this specification \emph{exactly}.

You can test your typechecker at this point before going on.
Run \verb+Top.loop_type ()+ or \verb+Top.file_type "+\textit{test\_file}\verb+.mml"+.

\subsection{Dynamic semantics}

Finally, you'll implement the MinML dynamic semantics in the file
\texttt{eval.sml}. The dynamic semantics is given in Figure
\ref{evalrules} as a relation ``$\mapsto$'' for single-step
evaluation. There are many more efficient ways of evaluating MinML
programs (as we'll see later in the class), but we require that you
strictly follow the specified semantics for this assignment.
Before reading the figure, you should decide what MinML expressions
should be values.

\begin{figure}[tb]
\centering
\renewcommand{\arraystretch}{3}
\begin{tabular}{r}
\infer[\textit{OpArg}]{o(v_1, \ldots, e_i, \ldots, e_n) \mapsto o(v_1, \ldots, e_i', \ldots, e_n)}{e_i \mapsto e_i'}
\\
\infer[\textit{OpVals}]{o(v_1, \ldots, v_n) \mapsto v}{(\mbox{by primop $o$})}
\\
% \infer[\textit{IfCond}]{\texttt{if } e_c \texttt{ then } e_t \texttt{ else } e_f \texttt{ fi} \mapsto \texttt{if } e_c' \texttt{ then } e_t \texttt{ else } e_f \texttt{ fi}}{e_c \mapsto e_c'}
\infer[\textit{IfCond}]{\texttt{if}(e, e_1, e_2) \mapsto \texttt{if}(e', e_1, e_2)}
 {e \mapsto e'}
\\
%\infer[\textit{IfTrue}]{\texttt{if true then } e_t \texttt{ else } e_f \texttt{~fi} \mapsto e_t}{}
\infer[\textit{IfTrue}]{\texttt{if}(\texttt{true}, e_1, e_2) \mapsto e_1}{}
\\
%\infer[\textit{IfFalse}]{\texttt{if false then } e_t \texttt{ else } e_f \texttt{~fi} \mapsto e_f}{}
\infer[\textit{IfFalse}]{\texttt{if}(\texttt{false}, e_1, e_2) \mapsto e_2}{}
\\
\infer[\textit{AppFun}]{\texttt{apply}(e_1, e_2) \mapsto \texttt{apply}(e_1', e_2)}{e_1 \mapsto e_1'}
\\
\infer[\textit{AppArg}]{\texttt{apply}(v_1, e_2) \mapsto \texttt{apply}(v_1, e_2')}{e_2 \mapsto e_2'}
\\
\infer[\textit{CallFun}]{\texttt{apply}(v_2, v_1) \mapsto \subst{v_2}{f}{\subst{v_1}{x}{e}}}
        {v_2 = \texttt{fun}(\tau_1,\tau_2,f.x.e)}
\\
\infer[\textit{LetArg}]{\texttt{let}(e_1, x.e_2) \mapsto \texttt{let}(e_1', x.e_2)}
        {e_1 \mapsto e_1'}
\\
\infer[\textit{Let}]{\texttt{let}(v_1, x.e_2) \mapsto \subst{v_1}{x}{e_2}}{}
\end{tabular}

\caption{Dynamic semantics for MinML: $v$, $v_i$, etc. denote 
expressions that are values} \label{evalrules}

\end{figure}

The evaluation algorithm is straightforward. First it will use the
``compatibility rules'' \textit{OpArg}, \textit{IfCond}, \textit{AppFun},
\textit{AppArg}, and \textit{LetArg} to recursively scan the input
expression for the proper subexpression to modify. Once the proper
subexpression has been located, one of the ``reduction rules''
\textit{OpVals}, \textit{IfTrue}, \textit{IfFalse}, \textit{CallFun},
\textit{Let} can be applied. If no rule applies (as might happen if
the expression is already fully evaluated, or is ill-typed), the
evaluator will raise an exception.

For example, on the expression $e_1\,\, e_2$, the evaluator will try
to apply an evaluation step to the function expression $e_1$. If it is
already a value, the evaluator will try to apply a step to the
argument expression $e_2$. If it is already a value as well, the
evaluator will try to use the reduction rule for application,
\textit{CallFun}.

You should use the function \verb+MinML.evalPrimop+ to compute the
result of the rule \textit{OpVals}.

Since the \textit{CallFun} and \textit{Let} rules involve
substitutions, you will also need to properly implement substitutions.
You may find your notes from the recitation on de Bruijn indices helpful
for this part.

\task{Evaluator}{45}

In \texttt{eval.sml}, fill in the structure \texttt{Eval :> EVAL} to
implement the behavior specified. You should not modify any other
files. You should implement the function \texttt{Eval.isValue} according
to the following specification:
\begin{quote}
  Suppose $e$ is a closed de Bruijn term.

  If $e$ is a value, then $\texttt{Eval.isValue(}e\texttt{)} = \texttt{true}$.

  If $e$ is not a value, then $\texttt{Eval.isValue(}e\texttt{)} = \texttt{false}$.

  If $e$ is not closed, then $\texttt{Eval.isValue(}e\texttt{)}$ can do anything.
\end{quote}
You should implement the function \texttt{Eval.step} according to
the following specification:
\begin{quote}
  Suppose $e$ is a closed de Bruijn term.

  If $e \mapsto e'$ for some (unique) $e'$, then $\texttt{Eval.step(}e\texttt{)} = e'$.

  If $e \mapsto e'$ does not hold for any $e'$, then
  $\texttt{Eval.step(}e\texttt{)} = \texttt{raise Eval.NoStep}$.

  If $e$ is not closed, then $\texttt{Eval.step(}e\texttt{)}$ can do anything.
\end{quote}

Be careful to implement these specifications \emph{exactly} according to the
definitions of the judgments. It is easy to get some corner cases wrong.

You can test your evaluator by running \verb+Top.loop_eval ()+ or
\verb+Top.file_eval "+\textit{test\_file}\verb+.mml"+. You can use
the functions \verb+Top.loop_step+ and \verb+Top.file_step+ to
see the individual evaluation steps until a value or stuck state is
reached.

\end{document}
