\documentclass[12pt]{article}
\usepackage{code,verbatim,math-cmds,math-envs,latin-abbrevs,proof,amssymb,latexsym}

\input{defns}
\input{minml-defns}

\begin{document}

\begin{center}
{\Large CS 15-312 Assignment \#2 \\
\minml: New and Improved! \\
{\em or:} Products and Sums, Type Inference, \\
and the {\sf C} Machine \\}\nl \\
%Type Inference in an Expanded \minml \\}\nl \\
{\large Assigned: Friday, February 5 \\
Due: Friday, February 26, 4 PM \\} \nl \\
\end{center}


Greetings!  After having completed the first assignment, you should
all be experts in using ML to implement inductive definitions of the
static and dynamic semantics of a language, or at least those of
\minml.  In this assignment, we will expand \minml\ to include
product and sum types and related constructors and destructors of these
types.  We will then ask you to implement an algorithm to
perform type inference on untyped expressions in this expanded version of
\minml.  Lastly, you will be asked to implement the {\sf C} machine
in place of the SOS semantics as a way of evaluating expressions in
the language.
The written part of this assignment will involve extending the proof
of type safety of \minml\ to the new language constructs we introduce.

\section{What You Hand In}

The four source files you will be modifying are
{\tt cgen.sml}, {\tt csolve.sml}, {\tt cmachine.sml} and {\tt program.sml}.
The modules {\tt CGen}, {\tt CSolve}, {\tt CMachine} and {\tt Program},
defined in these files respectively, are used by the {\tt Top}
structure in {\tt top.sml} to create an ``implementation''
of this assignment.  We will provide the binaries for a structure
called {\tt Solution} containing our compiled implementations for these
four modules.  You can use our solution modules to test one or more
of the modules you've implemented in isolation by simply substituting
{\tt Solution.\mbox{{\em modulename}}} into the {\tt Top} structure in
the appropriate places.

In the files {\tt cgen-sig.sml}, {\tt csolve-sig.sml}, {\tt cmachine-sig.sml},
and {\tt program-sig.sml}, you will find the signatures your modules
must match (opaquely).
Note that not all the functions we ask you to implement
are used outside of the module in which they are defined, but we
have asked you to write them as a way of loosely structuring your code.
We will discuss the meaning of these signatures
in Section~3.

As always, we ask that your code be as simple and elegant
as possible, but not recklessly inefficient.  In other words, don't
optimize your code such that it is incomprehensible, but also be sure
not to perform redundant computations for the sake of readability.
In addition, please write a comment next to every function you write
describing the operation it performs and any notable aspects
of its implementation.  We {\em will} deduct points for insufficient
documentation.

While you are hacking, feel free to modify any of the files, but
make sure that the four files you hand in compile correctly with
the original versions of all those files, except for the {\tt Top}
structure which should obviously be instantiated to use the modules
you've written.
Then copy those four files into your handin directory:
\begin{code}
/afs/andrew/course/15/312/handin/<your-andrew-id>/ass2/
\end{code}
Hand in the written part of this assignment (described in Section 2.4)
to any of the TAs or Bob's secretary Jan Koehler.  Late assignments
submitted by Monday, February 29 at 4 PM, will be accepted with
a 25\% point deduction.

\section{Expanding \minml}

In this section, we present some extensions to \minml\, as well as provide
the necessary extensions to the static semantics, the dynamic semantics, 
the constraint generation judgment
and the {\sf C} machine.
We also state the written part
of the assignment.

\subsection{Products and Sums}

We begin by adding two new type constructors to \minml,
$\times$ and $+$, corresponding to product and sum types.
Think of products as ML tuples and sums as ML datatypes.
However, in our extension to \minml, we will only add
binary tuples (pairs) and binary datatypes, with \mathcd{inl}
and \mathcd{inr} (pronounced ``inleft'' and ``inright'')
as the datatype constructors.  For type destructors,
i.e.\ expressions that take apart a value of a certain type,
we introduce a \mathcd{bind} expression for products
that uses a limited form of pattern matching, and a \mathcd{case}
expression for sums.  The syntax for the extensions to the language
of types, typed expressions, untyped expressions and values is
given in Figure~1, as well as a new syntactic object, patterns.
\begin{figure}[t]
\[
\begin{array}{l@{\hspace{2em}}rcl}

\mbox{\em Types} & \tau & ::= & \dots \alt \Times{\tau_1}{\tau_2} \alt
        \Plus{\tau_1}{\tau_2} \\
\mbox{\em Typed Patterns} & p^t & ::= & \WildPat \alt \VarPat{x}{\tau} \alt \Pair{p_1^t}{p_2^t} \\
\mbox{\em Untyped Patterns} & p^u & ::= & \WildPat \alt x \alt \Pair{p_1^u}{p_2^u} \\
\mbox{\em Typed Expressions} & e & ::= & \dots \alt \Pair{e_1}{e_2} \alt \Bind{p^t}{e_1}{e_2} \alt \\
        &&& \qquad \InleftT{\tau_1}{\tau_2}{e} \alt \InrightT{\tau_1}{\tau_2}{e} \alt \\
        &&& \qquad \CaseT{e}{x_1}{\tau_1}{e_1}{x_2}{\tau_2}{e_2} \\
\mbox{\em Untyped Expressions} & u & ::= & \dots \alt \Pair{u_1}{u_2} \alt \Bind{p^u}{u_1}{u_2} \alt \\
        &&& \qquad \Inleft{u} \alt \Inright{u} \alt \\
        &&& \qquad \Case{u}{x_1}{u_1}{x_2}{u_2} \\
\mbox{\em Values} & v & ::= & \dots \alt \Pair{v_1}{v_2} \alt \InleftT{\tau_1}{\tau_2}{v} \alt \InrightT{\tau_1}{\tau_2}{v}
\end{array}
\]
\caption{Syntax for the extensions to \minml}
\end{figure}

\subsection{Static Semantics}
The specific meaning of these new extensions is best explained by
presenting the static and dynamic semantics for them.  In order
to do this, we need to define a new typing judgment on patterns
of the form $\Gamma\vdash p^t : \tau \gens \Gamma'$.  This
judgment will essentially
do pattern matching on $p$ to determine whether it can be given
type $\tau$, and if so, add the variables contained in $p$ to
the context $\Gamma$ with their respective types, producing $\Gamma'$.
We have three kinds of patterns: wild card patterns which
can take any type, variable patterns which can take only the specified
type, and pair patterns which take the product of the types of their
constituent patterns.  Hence,
the inductive rules for this judgment are as follows:
\[
\infer[\PWild]{\Gamma \vdash \WildPat : \tau \gens \Gamma}{} \qquad
\infer[\PVar]{\Gamma \vdash (x:\tau) : \tau \gens \Gamma[x:\tau]}{}
\]
\[
\infer[\PPair]{\typpatJ{\Gamma}{\Pair{p_1}{p_2}}{\Times{\tau_1}{\tau_2}}{\Gamma''}}
        {\typpatJ{\Gamma}{p_1}{\tau_1}{\Gamma'} \quad
         \typpatJ{\Gamma'}{p_2}{\tau_2}{\Gamma''}}
\]
Note that by definition of $\Gamma[x:\tau]$, $x$ cannot occur in
the domain of $\Gamma$.  This implies that a pattern which type-checks
cannot have duplicate variables in it.  This is important to remember
when you go to implement these typing rules for patterns
because if you want to use a ``shadowing'' technique
for adding variables to a context (which is perfectly acceptable
for this assignment), you will have to make sure that a pattern
has no duplicates {\em before} you check it.

Now that we have dealt with pattern checking, let's move on to the
new typing rules.  These are all fairly
straightforward.
\[
\infer[\TPair]{\typingJ{\Gamma}{\Pair{e_1}{e_2}}{\Times{\tau_1}{\tau_2}}}
        {\typingJ{\Gamma}{e_1}{\tau_1} \quad
        \typingJ{\Gamma}{e_2}{\tau_2}}
\]
\[
\infer[\TBind]{\typingJ{\Gamma}{\Bind{p}{e_1}{e_2}}{\tau}}
        {\typingJ{\Gamma}{e_1}{\tau_1} \quad
        \typpatJ{\Gamma}{p}{\tau_1}{\Gamma'} \quad
        \typingJ{\Gamma'}{e_2}{\tau}}
\]
\[
\infer[\TInl]{\typingJ{\Gamma}{\InleftT{\tau_1}{\tau_2}{e}}{\Plus{\tau_1}{\tau_2}}}
        {\typingJ{\Gamma}{e}{\tau_1}}
\qquad
\infer[\TInr]{\typingJ{\Gamma}{\InrightT{\tau_1}{\tau_2}{e}}{\Plus{\tau_1}{\tau_2}}}
        {\typingJ{\Gamma}{e}{\tau_2}}
\]
\[
\infer[\TCase]{\typingJ{\Gamma}{\CaseT{e}{x_1}{\tau_1}{e_1}{x_2}{\tau_2}{e_2}}{\tau}}
        {\typingJ{\Gamma}{e}{\Plus{\tau_1}{\tau_2}} \quad
        \typingJ{\Gamma[x_1:\tau_1]}{e_1}{\tau} \quad
        \typingJ{\Gamma[x_2:\tau_2]}{e_2}{\tau}}
\]
\subsection{Dynamic Semantics}
The evaluation rules are pretty sensible as well.  The only ones that
are a little tricky are those involving {\tt bind} because we need to do
pattern matching on the pattern in the {\tt bind} and, if it is a pair
pattern, break the expression into two nested {\tt bind}'s.
Aside from that, left-to-right evaluation prevails as usual.
\[
\infer[\EPairL]{\stepsJ{\Pair{e_1}{e_2}}{\Pair{e_1'}{e_2}}}
        {\stepsJ{e_1}{e_1'}}
\qquad
\infer[\EPairR]{\stepsJ{\Pair{v_1}{e_2}}{\Pair{v_1}{e_2'}}}
        {\stepsJ{e_2}{e_2'}}
\]
\[
\infer[\EBind]{\stepsJ{\Bind{p}{e_1}{e_2}}{\Bind{p}{e_1'}{e_2}}}
        {\stepsJ{e_1}{e_1'}}
\]
\[
\infer[\IBindW]{\stepsJ{\Bind{\WildPat}{v}{e}}{e}}{}
\qquad
\infer[\IBindV]{\stepsJ{\Bind{\VarPat{x}{\tau}}{v}{e}}{[v/x]e}}{}
\]
\[
\infer[\IBindP]{\stepsJ{\Bind{\Pair{p_1}{p_2}}{\Pair{v_1}{v_2}}{e}}
        {\Bind{p_1}{v_1}{\Bind{p_2}{v_2}{e}}}}{}
\]
\[
\infer[\EInl]{\stepsJ{\InleftT{\tau_1}{\tau_2}{e}}{\InleftT{\tau_1}{\tau_2}{e'}}}{\stepsJ{e}{e'}}
\qquad
\infer[\EInr]{\stepsJ{\InrightT{\tau_1}{\tau_2}{e}}{\InrightT{\tau_1}{\tau_2}{e'}}}{\stepsJ{e}{e'}}
\]
\[
\infer[\ICaseL]{\stepsJ{\CaseT{\InleftT{\tau_1}{\tau_2}{v}}{x_1}{\tau_1}{e_1}{x_2}{\tau_2}{e_2}}{[v/x_1]e_1}}{}
\]
\[
\infer[\ICaseR]{\stepsJ{\CaseT{\InrightT{\tau_1}{\tau_2}{v}}{x_1}{\tau_1}{e_1}{x_2}{\tau_2}{e_2}}{[v/x_2]e_2}}{}
\]
\[
\infer[\ECase]{\stepsbrJ{\CaseT{e}{x_1}{\tau_1}{e_1}{x_2}{\tau_2}{e_2}}{\CaseT{e'}{x_1}{\tau_1}{e_1}{x_2}{\tau_2}{e_2}}}{\stepsJ{e}{e'}}
\]
\subsection{Preservation and Progress}
Now that the extensions to \minml\ have been completely
specified, we can state the written part of this assignment as follows:
{\bf Prove type preservation and progress (the definitions of which are
given in the notes)
for the extended definition of \minml\ given here.}
This means presenting one new inductive
case of the theorems for each of the new rules here.
This is a great test of whether you really understand the proof
principles you have learned this term, and a number of the cases
are {\em not} tedious, so you won't be bored!

\subsection{Constraint Generation}

In this section we present the extensions to the constraint generation
judgment $\cgenJ{\Gamma^*}{u}{e^*}{\tau^*}{\phi}$, where $\phi$ is a 
constraint as defined in the notes, and the ${}^*$s indicate that
the types involved are really type schemes.
(For ease of presentation, we will omit the ${}^*$s from now on,
but in fact all the types discussed in this section are really type
schemes.  Likewise, in the code we have given you to work with,
the implementation of types, {\tt Typed.typ}, is really an
implementation of type schemes.)
In order to do this, however,
we need to form an auxiliary judgment to handle constraint generation
for patterns.  This auxiliary judgment takes the form
$\cgenpatJ{\Gamma}{p^u}{\Gamma'}{p^t}{\tau}$. This takes
the untyped pattern $p^u$, assigns fresh type variables to all
the variables in $p^u$, yielding an annotated pattern $p^t$, its type
$\tau$, and $\Gamma'$, the result of adding these variables and their
generated types to $\Gamma$.  Here are the rules defining this judgment:
\[
\infer{\cgenpatJ{\Gamma}{\WildPat}{\Gamma}{\WildPat}{\alpha}}
        {\alpha\ \mbox{is fresh}}
\qquad
\infer{\cgenpatJ{\Gamma}{x}{\Gamma[x:\alpha]}{x:\alpha}{\alpha}}
        {\alpha\ \mbox{is fresh}}
\]
\[
\infer{\cgenpatJ{\Gamma}{\Pair{p_1^u}{p_2^u}}{\Gamma''}{\Pair{p_1^t}{p_2^t}}{\Times{\tau_1}{\tau_2}}}
        {\cgenpatJ{\Gamma}{p_1^u}{\Gamma'}{p_1^t}{\tau_1} \quad
        \cgenpatJ{\Gamma'}{p_2^u}{\Gamma''}{p_2^t}{\tau_2}}
\]
Now that we've got that down, the new rules for the constraint generation
judgment are easy to present and follow the style
of the rules for core \minml.
\[
\infer{\cgenJ{\Gamma}{\Pair{u_1}{u_2}}{\Pair{e_1}{e_2}}{\Times{\tau_1}{\tau_2}}{\phi_1 \wedge \phi_2}}
        {\cgenJ{\Gamma}{u_1}{e_1}{\tau_1}{\phi_1} \quad
        \cgenJ{\Gamma}{u_2}{e_2}{\tau_2}{\phi_2}}
\]
\[
\infer{\cgenJ{\Gamma}{\Bind{p^u}{u_1}{u_2}}{\Bind{p^t}{e_1}{e_2}}{\tau}{\tau_p = \tau_1 \wedge \phi_1 \wedge \phi_2}}
        {\cgenJ{\Gamma}{u_1}{e_1}{\tau_1}{\phi_1} \quad
        \cgenpatJ{\Gamma}{p^u}{\Gamma'}{p^t}{\tau_p} \quad
        \cgenJ{\Gamma'}{u_2}{e_2}{\tau}{\phi_2}}
\]
\[
\infer{\cgenJ{\Gamma}{\Inleft{u}}{\InleftT{\tau}{\alpha}{e}}{\Plus{\tau}{\alpha}}{\phi}}
        {\cgenJ{\Gamma}{u}{e}{\tau}{\phi} \quad
        \alpha\ \mbox{is fresh}}
\qquad
\infer{\cgenJ{\Gamma}{\Inright{u}}{\InrightT{\alpha}{\tau}{e}}{\Plus{\alpha}{\tau}}{\phi}}
        {\cgenJ{\Gamma}{u}{e}{\tau}{\phi} \quad
        \alpha\ \mbox{is fresh}}
\]
\[
\infer{\cgenbrJ{\Gamma}{\Case{u}{x_1}{u_1}{x_2}{u_2}}{\CaseT{e}{x_1}{\alpha}{e_1}{x_2}{\beta}{e_2}}{\tau_1}{\tau = \Plus{\alpha}{\beta} \wedge \tau_1 = \tau_2 \wedge \phi \wedge \phi_1 \wedge \phi_2}}
        {\begin{array}{c}
        \cgenJ{\Gamma}{u}{e}{\tau}{\phi} \quad
        \alpha\ \mbox{is fresh}\quad\beta\ \mbox{is fresh} \\
        \cgenJ{\Gamma[x_1:\alpha]}{u_1}{e_1}{\tau_1}{\phi_1} \quad
        \cgenJ{\Gamma[x_2:\beta]}{u_2}{e_2}{\tau_2}{\phi_2}
        \end{array}}
\]

\subsection{The {\sf C} Machine}

Here we present the extensions to the {\sf C} machine.
First, we must define the new kinds of stack frames $f$ that arise
in the expanded \minml:
\[
\begin{array}{rcl}
f & ::= & \dots \alt \Pair{\hole}{e_2} \alt \Pair{v_1}{\hole} \alt \Bind{p}{\hole}{e} \\
&& \qquad \InleftT{\tau_1}{\tau_2}{\hole} \alt \InrightT{\tau_1}{\tau_2}{\hole} \\
&& \qquad \CaseT{\hole}{x_1}{\tau_1}{e_1}{x_2}{\tau_2}{e_2}
\end{array}
\]
Now we can give the new {\sf C} machine transition rules involving
products and sums.  We first give the rules that apply if the
$e$ in $(k,e)\Cstep(k',e')$ is a value, and then the rules that
apply if it is not.  Although the rules given in the notes were
not divided in this way, you may find it very useful to view them
this way for the purposes of your implementation.
\[
(\Pair{\hole}{e_2}\cons k, v_1) \Cstep (\Pair{v_1}{\hole}\cons k, e_2)
\qquad
(\Pair{v_1}{\hole}\cons k, v_2) \Cstep (k, \Pair{v_1}{v_2})
\]
\[
(\Bind{\WildPat}{\hole}{e} \cons k, v) \Cstep (k,e)
\]
\[
(\Bind{x:\tau}{\hole}{e} \cons k, v) \Cstep (k,[v/x]e)
\]
\[
(\Bind{\Pair{p_1}{p_2}}{\hole}{e}\ \cons\ k, \Pair{v_1}{v_2}) \Cstep
        (\Bind{p_1}{\hole}{\Bind{p_2}{v_2}{e}}\ \cons\ k, v_1)
\]
\[
(\InleftT{\tau_1}{\tau_2}{\hole} \cons k, v) \Cstep (k, \InleftT{\tau_1}{\tau_2}{v})
\]
\[
(\InrightT{\tau_1}{\tau_2}{\hole} \cons k, v) \Cstep (k, \InrightT{\tau_1}{\tau_2}{v})
\]
\[
(\CaseT{\hole}{x_1}{\tau_1}{e_1}{x_2}{\tau_2}{e_2}\ \cons\ k, \InleftT{\tau_1}{\tau_2}{v}) \Cstep (k, [v/x_1]e_1)
\]
\[
(\CaseT{\hole}{x_1}{\tau_1}{e_1}{x_2}{\tau_2}{e_2}\ \cons\ k, \InrightT{\tau_1}{\tau_2}{v}) \Cstep (k, [v/x_2]e_2)
\]
\newpage\noindent
Now if $e$ is not a value:
\[
(k,\Pair{e_1}{e_2}) \Cstep (\Pair{\hole}{e_2} \cons k, e_1)
\]
\[
(k,\Bind{p}{e_1}{e_2}) \Cstep (\Bind{p}{\hole}{e_2} \cons k, e_1)
\]
\[
(k,\InleftT{\tau_1}{\tau_2}{e}) \Cstep (\InleftT{\tau_1}{\tau_2}{\hole} \cons k, e)
\]
\[
(k,\InrightT{\tau_1}{\tau_2}{e}) \Cstep (\InrightT{\tau_1}{\tau_2}{\hole} \cons k, e)
\]
\[
\begin{array}{c}
(k,\CaseT{e}{x_1}{\tau_1}{e_1}{x_2}{\tau_2}{e_2}) \Cstep \\
        (\CaseT{\hole}{x_1}{\tau_1}{e_1}{x_2}{\tau_2}{e_2} \cons k, e)
\end{array}
\]

\section{Implementation}

As you know from Section~1, you are to complete the code in four modules
we have given you.  In {\tt CGen}, you will implement constraint
generation.  In {\tt CSolve}, you will
implement a constraint solver that is passed the constraints generated
in {\tt CGen} and asked to generate the principal solution of those
constraints in the form of a substitution.  In {\tt CMachine}, you will
implement the {\sf C} machine for expanded \minml.
Finally, in {\tt Program}, you will write code that executes
\minml\ ``programs''.  Whereas before a program was merely a series
of expressions to be evaluated, we will now allow a definition mechanism
at the top level which admits polymorphism.

You will note in the
signatures below references to types defined in {\tt Typed} and {\tt Untyped}.
They contain, respectively, the definitions of datatypes representing
the typed and untyped versions of \minml, but they also contain useful
functions for handling type variables, closed substitutions, etc.
See the code for more details.

\subsection{CGen}

The {\tt CGen} functor you are to implement in {\tt cgen.sml}
should match signature {\tt CGEN} defined as follows:
\begin{code}
signature CGEN =
sig
  type constraint
\nl
  type context = string -> Typed.typ
  val empty : context
  val ++ : context * (string * Typed.typ) -> context
\nl
  val pat2ctxt : context * Untyped.pat ->
                 context * Typed.pat * Typed.typ
\nl
  val cgen : context * Untyped.exp ->
             Typed.exp * Typed.typ * constraint
end
\end{code}
The reason {\tt CGen} is a functor is that it needs to use
the {\tt constraint} type and its related constructors that are
defined in {\tt CSolve}, so {\tt CSolve} is passed in as a parameter.
The {\tt context} type and its related operators {\tt empty}
and {\tt ++} should be familiar from the first assignment.
The key functions here are {\tt pat2ctxt} and {\tt cgen}.
The {\tt pat2ctxt} function should take a context $\Gamma$
and an untyped pattern $p^u$ and output a new context $\Gamma'$,
along with the annotated pattern $p^t$ and its type $\tau$
such that $\Gamma \vdash p^u \gens_C (\Gamma',p^t,\tau)$.
The {\tt cgen} function should take
a context $\Gamma$ and untyped expression $u$ and output
the annotated expression $e$ along with its type (scheme) $\tau$
and the generated constraints $\phi$ such that
$\Gamma \vdash u \leadsto_C e:\tau\,[\phi]$.

\subsection{CSolve}

The {\tt CSolve} structure you are to implement in {\tt csolve.sml}
should match signature {\tt CSOLVE} defined as follows:
\begin{code}
signature CSOLVE =
sig
  type constraint
  val True : constraint
  val == : Typed.typ * Typed.typ -> constraint
  val && : constraint * constraint -> constraint
\nl
  type singlesub = Typed.tyvar * Typed.typ
  val appsub : singlesub * Typed.typ -> Typed.typ
  val appsub2cs : singlesub * constraint -> constraint
\nl
  type multisub
  val emptysub : multisub
  val @@ : multisub * singlesub -> multisub
  val appsubs : multisub * Typed.typ -> Typed.typ
  val appsubs2exp : multisub * Typed.exp -> Typed.exp
\nl
  val occurscheck : Typed.tyvar * Typed.typ -> unit
  val csolve : multisub * constraint -> multisub
end
\end{code}
First, you should implement the type of constraints and its
constructors {\tt True}, {\tt ==} and {\tt \&\&}, corresponding
to $\top$, $=$ and $\wedge$ in the theory.  There are quite a few
ways to implement constraints, so we have left it up to you.
The reason we have the type of constraints defined in {\tt CSolve}
instead of {\tt CGen} is that here you will want to deconstruct
constraints in the process of constraint solving, whereas in
constraint generation you only need to build them up.

The {\tt singlesub} type is a pair containing a type variable
and the type to be substituted for it.  The {\tt appsub} function
should apply a {\tt singlesub} to a type.
The {\tt appsub2cs} function should apply a {\tt singlesub} to
all the types in a constraint.

The {\tt multisub} type is a substitution containing zero or more
type variables.  We have made the implementation of this abstract
because there are multiple ways of doing this, some more efficient
than others.  For instance, you might want to use functions to represent
substitutions, or perhaps lists of pairs, or binary maps.
The {\tt emptysub} is the identity substitution.
The {\tt @@} function can be used to compose a {\tt multisub} with
a {\tt onesub}.
The {\tt appsubs} function applies a {\tt multisub} to a type.
The {\tt appsubs2exp} function applies a {\tt multisub} to the
types within a typed expression.

The occurs-check (part of the constraint-solving algorithm) should
be implemented by the {\tt occurscheck} function, raising a
{\tt TypeError} if it fails, and returning unit otherwise.
Finally, {\tt csolve} should take an initial substitution $\theta$ and
a constraint $\phi$ and form the
substitution $\theta'$ such that $(\theta,\phi)\StepsTo_S^* (\theta',\top)$,
as defined by the constraint-solving algorithm in the notes.
Look in {\tt elab.sml} to see how this function and {\tt cgen}
are combined to perform type reconstruction on an untyped \minml\ term.

\subsection{CMachine}
The {\tt CMachine} structure you are to implement in {\tt cmachine.sml}
should match signature {\tt CMACHINE} defined as follows:
\begin{code}
signature CMACHINE =
sig
  exception Stuck
\nl
  type frame
  type stack
  type state = stack * Typed.exp
\nl
  val Cstep : state -> state
\nl
  val CstepOpt : state -> state option
  val CmultiStep : state -> state
  val eval : Typed.exp -> Typed.exp
end
\end{code}
The only function here that is not implemented is {\tt Cstep},
which as you might expect performs a single step of the
{\sf C} machine.  We have provided you with datatypes representing
the {\tt frame} and {\tt stack} types in {\tt cstep.sml} that
you are free to use or change, although we would prefer it if
you left them alone.  Note: the code for closed term substitutions
in typed expressions is provided for you in the {\tt Typed}
structure.  See that code for details.

\subsection{Program}
The {\tt Program} functor you are to implement in {\tt program.sml}
should match signature {\tt PROGRAM} defined as follows:
\begin{code}
signature PROGRAM =
sig
  exception Done
\nl
  val typing : Untyped.subst * Untyped.exp ->
               Untyped.exp * Typed.exp * Typed.typ
\nl
  val execute : Untyped.subst * Untyped.command ->
                Untyped.subst * string
end
\end{code}
To understand what to do here, we have to first define what
a \minml\ ``program'' is.  Before, programs were simply
sequences of expressions separated by semicolons.  In this
assignment, we will add the ability to make top-level definitions,
so now let us think of programs as sequences of commands, where
commands are defined as follows:
\[
\begin{array}{rcl}
C & ::= & \DefProg{x}{u} \alt \EvalProg{u} \alt \QuitProg
\end{array}
\]
Since programs in an interactive loop are really just streams of
commands, we will not try to write out a full semantics for
\minml\ programs, but instead just decide how to execute
a command within an environment that maps variables to
untyped expressions.  Given an environment
$E$ and a command $C$, the {\tt execute} function
returns an environment that might contain a
new binding (if $C$ were a {\tt def}), and also a string
containing \minml's response to the command (such as
``Type Error: Oy vey!'' or ``3 : int'').  How this is used
to ``execute'' a whole program we will not get into, but the
code for {\tt minml} is provided and you may want to figure out
what it's doing.  In any case, if the input $C$ to {\tt execute}
is of the form $\DefProg{x}{u}$ or $\EvalProg{u}$,
you should first apply the closed substitution represented by
the environment $E$ to $u$.  We have given you code for doing
closed substitutions on untyped terms in the {\tt Untyped} structure.
Then, the hopefully closed $u$
should be type-reconstructed to $e$ with type (scheme) $\tau$,
using the {\tt Elab.elaborate} function.
The execution up to this point should be encapsulated in the
{\tt typing} function, which returns the $u$ after substitution,
and the $e$ and $\tau$ from elaboration.

Then, in the case of a definition, do not evaluate the expression $e$,
but simply return $E$ with the addition of the pair $(x,u)$.
Note that using this new environment to execute the rest of the
program has the effect of making $x$ polymorphic: since we
will substitute $u$ for each free occurrence of $x$,
each such $x$ will not necessarily have the same type
(if $u$ could be reconstructed to multiple types).
In the case of an evaluation, evaluate $e$ to a value, and
return the old environment $E$.  It is up to you what kind of
messages you want to return in these different cases (hopefully
something useful), but make sure you handle a {\tt TypeError}
by producing an appropriate error message and continuing on,
not letting the error bubble up to the top level of SML.
(After all, if we don't like your user interface,
we can plug in our own!)  In the case of a quit command, just
raise the {\tt Done} exception.

\section{Checklist}

You think you've finished the assignment?  That would mean you've:
\begin{enumerate}
\item {\bf [25 points]} Proved type preservation and progress for expanded \minml
\item {\bf [25 points]} Implemented constraint generation in {\tt CGen}
\item {\bf [25 points]} Implemented constraint solving in {\tt CSolve}
\item {\bf [20 points]} Implemented the {\sf C} machine in {\tt CMachine}
\item {\bf [5 points]} Implemented the command semantics in {\tt Program}
\end{enumerate}

\end{document}
