\documentclass{article}
\usepackage{fullpage}
\usepackage{listings}
\usepackage{color}
\usepackage{amsmath,amssymb,amsthm}
\usepackage{tocloft}

\definecolor{mygreen}{rgb}{0,0.6,0}
\definecolor{mygray}{rgb}{0.5,0.5,0.5}
\definecolor{mymauve}{rgb}{0.58,0,0.82}

\lstset{ %
  backgroundcolor=\color{white},   % choose the background color; you must add \usepackage{color} or \usepackage{xcolor}
  basicstyle=\tt,                  % the size of the fonts that are used for the code
  breakatwhitespace=false,         % sets if automatic breaks should only happen at whitespace
  breaklines=true,                 % sets automatic line breaking
  captionpos=b,                    % sets the caption-position to bottom
  commentstyle=\color{mygreen},    % comment style
  deletekeywords={...},            % if you want to delete keywords from the given language
  escapeinside={\%*}{*)},          % if you want to add LaTeX within your code
  extendedchars=true,              % lets you use non-ASCII characters; for 8-bits encodings only, does not work with UTF-8
  frame=single,                    % adds a frame around the code
  keepspaces=true,                 % keeps spaces in text, useful for keeping indentation of code (possibly needs columns=flexible)
  keywordstyle=\color{blue},       % keyword style
  morekeywords={*,...},            % if you want to add more keywords to the set
  numbers=left,                    % where to put the line-numbers; possible values are (none, left, right)
  numbersep=9pt,                   % how far the line-numbers are from the code
  numberstyle=\tiny\color{mygray}, % the style that is used for the line-numbers
  rulecolor=\color{black},         % if not set, the frame-color may be changed on line-breaks within not-black text (e.g. comments (green here))
  showspaces=false,                % show spaces everywhere adding particular underscores; it overrides 'showstringspaces'
  showstringspaces=false,          % underline spaces within strings only
  showtabs=false,                  % show tabs within strings adding particular underscores
  stepnumber=1,                    % the step between two line-numbers. If it's 1, each line will be numbered
  stringstyle=\color{mymauve},     % string literal style
  tabsize=2,                       % sets default tabsize to 2 spaces
  title=\lstname                   % show the filename of files included with \lstinputlisting; also try caption instead of title
}

\usepackage{fourier}                % set math font
%\usepackage[no-math]{fontspec}      % to load non-Latex fonts (keep math font)
%\setsansfont{Optima}                % set sans-serif font
%\usepackage{sectsty}                % to override section fonts
%\allsectionsfont{\fontspec{Optima}} % set header font

\usepackage{stmaryrd} % for double brackets

\title{
  \textbf{CSE3302 Programming Language Project Specification} \\
  }
\author{
  \normalsize
  \begin{tabular}{rcl}
    Course Instructor: & Kenny Zhu & \texttt{kenny.zhu@uta.edu} \\
    Teaching Assistant: & Peter (Weiran) Zhang & \texttt{wxz9630@mavs.uta.edu} \\
  \end{tabular}
}

\newcommand{\btt}{\mathbf{tt}}
\newcommand{\bff}{\mathbf{ff}}
\newcommand{\To}{\ \textcolor{blue}{\Downarrow}\ }
\newcommand{\result}[1]{\textcolor{blue}{\texttt{#1}}}

\renewcommand{\cftsecfont}{\bfseries} % Bold section titles in ToC
\renewcommand{\cftsecpagefont}{\bfseries} % Bold page numbers for sections
\renewcommand{\cftsecleader}{\cftdotfill{\cftdotsep}} % Add dots between section title and page number
\setlength{\cftbeforesecskip}{0.5em} % Adjust vertical spacing before sections
\setlength{\cftsecindent}{1.5em} % Indent section titles
\date{Due Date: April 27, 2026, 11:59 PM}

\begin{document}

\maketitle

\section{Introduction}

In this project, you are required to implement an \emph{interpreter} for the
programming language SimPL (pronounced \emph{simple}).  SimPL is a simplified
dialect of ML, which can be used for both \emph{functional} and
\emph{imperative} programming.  This specification presents a definition of
SimPL and provides guidelines to help you implement the interpreter.

\section{Lexical Definition}

The lexical definition of SimPL consists of four aspects: comments, atoms, keywords, and operators.

\subsection{Comments}

\begin{itemize}
  \item Comments in SimPL are enclosed by pairs of \texttt{(*} and \texttt{*)}.
  \item Comments are nestable, e.g. \texttt{(*  (*  *)  *)} is a valid comment, while \texttt{(*  (*  *)} is invalid.
  \item A comment can spread over multiple lines.
  \item Comments and whitespaces (spaces, tabs, newlines) should be ignored and not evaluated.
\end{itemize}

\subsection{Atoms}

\begin{itemize}
  \item Atoms are either integer literals or identifiers.
  \item Integer literals are matched by regular expression \texttt{[0-9]+}.
  \item Integer literals only represent non-negative integers less than $2^{31}$.
  \item Integer literals are in decimal format, and leading zeros are insignificant, e.g. both \texttt{0123} and \texttt{000123} represent the integer $123$.
  \item Identifiers are matched by regular expression \texttt{[\_a-z][\_a-zA-Z0-9']*}.
\end{itemize}

\subsection{Keywords}

All the following identifiers are keywords.
Related keywords are grouped in the same line for better readability.
Keywords cannot be bound to anything.

\begin{itemize}
  \item \texttt{nil}
  \item \texttt{ref}
  \item \texttt{fn \ rec}
  \item \texttt{let \ in \ end}
  \item \texttt{if \ then \ else}
  \item \texttt{while \ do}
  \item \texttt{true \ false}
  \item \texttt{not \ andalso \ orelse}
\end{itemize}

\subsection{Operators}

\begin{itemize}
  \item \texttt{+ \ - \ * \ / \ \% \ \~}
  \item \texttt{= \ <> \ < \ <= \ > \ >=}
  \item \texttt{:: \ () \ =>}
  \item \texttt{:= \ !}
  \item \texttt{, \ ; \ ( \ )}
\end{itemize}

\section{Syntax}

\begin{itemize}
  \item All SimPL programs are expressions.  $\mathbf{Exp}$ is the set of all expressions.
  \item Names are non-keyword identifiers.  $\mathbf{Var}$ is the set of all names.
  \item Expressions, names, and integer literals are denoted by meta variables $e$, $x$, and $n$.
  \item Unary operator $uop \in \{ \texttt{\textasciitilde}, \texttt{not}, \texttt{!} \}$
  \item Binary operator $bop \in \{ \texttt{+}, \texttt{-}, \texttt{*}, \texttt{/}, \texttt{\%}, \texttt{=}, \texttt{<>}, \texttt{<}, \texttt{<=}, \texttt{>}, \texttt{>=}, \texttt{andalso}, \texttt{orelse}, \texttt{::}, \texttt{:=}, \texttt{;} \}$
\end{itemize}

\[\begin{array}{rcll}
  \mbox{Expression}\ e
    & ::= & n & \mbox{integer literal} \\
    &  |  & x & \mbox{name} \\
    &  |  & \texttt{true} & \mbox{true value} \\
    &  |  & \texttt{false} & \mbox{false value} \\
    &  |  & \texttt{nil} & \mbox{empty list} \\
    &  |  & \texttt{ref} \ e & \mbox{reference creation} \\
    &  |  & \texttt{fn} \ x \ \texttt{=>} \ e & \mbox{function} \\
    &  |  & \texttt{rec} \ x \ \texttt{=>} \ e & \mbox{recursion} \\
    &  |  & \texttt{(} e \texttt{,}\ e \texttt{)} & \mbox{pair construction} \\
    &  |  & uop\ e & \mbox{unary operation} \\
    &  |  & e\ bop\ e & \mbox{binary operation} \\
    &  |  & e\ e & \mbox{application} \\
    &  |  & \texttt{let}\ x\ \texttt{=}\ e\ \texttt{in}\ e\ \texttt{end} & \mbox{binding} \\
    &  |  & \texttt{if}\ e\ \texttt{then}\ e\ \texttt{else}\ e & \mbox{conditional} \\
    &  |  & \texttt{while}\ e\ \texttt{do}\ e & \mbox{loop} \\
    &  |  & \texttt{()} & \mbox{unit} \\
    &  |  & \texttt{(} e \texttt{)} & \mbox{grouping} \\
\end{array}\]

\subsection{Operator Precedence}

\begin{center}
\begin{tabular}{cll}
  \hline
  Priority & Operator(s) & Associativity \\
  \hline
  1 & \texttt{;} & left \\
  2 & \texttt{:=} & none \\
  3 & \texttt{orelse} & right \\
  4 & \texttt{andalso} & right \\
  5 & \texttt{= \ <> \ < \ <= \ > \ >=} & none \\
  6 & \texttt{::} & right \\
  7 & \texttt{+ \ -} & left \\
  8 & \texttt{* \ / \ \%} & left \\
  9 & (application) & left \\
  10 & \texttt{\textasciitilde\ \ not \ !} & right \\
  \hline
\end{tabular}
\end{center}

\section{Typing}

\subsection{Definition}

\begin{figure}[h]
\begin{minipage}{0.5\textwidth}
\[\begin{array}{rcl}
  \mbox{Arbitrary type}\ t
    & ::= & \texttt{int} \\
    &  |  & \texttt{bool} \\
    &  |  & \texttt{unit} \\
    &  |  & t\ \texttt{list} \\
    &  |  & t\ \texttt{ref} \\
    &  |  & t \times t \\
    &  |  & t \rightarrow t \\
\end{array}\]
\end{minipage}
\begin{minipage}{0.5\textwidth}
\[\begin{array}{rcl}
  \mbox{Equality type}\ \alpha
    & ::= & \texttt{int} \\
    &  |  & \texttt{bool} \\
    &  |  & \alpha\ \texttt{list} \\
    &  |  & t\ \texttt{ref} \\
    &  |  & \alpha \times \alpha \\
\end{array}\]
\end{minipage}
\end{figure}

The set of all types $\mathbf{Typ}$ is the smallest set satisfying the following rules.
\begin{itemize}
  \item $\texttt{int}\in\mathbf{Typ}$, $\texttt{bool}\in\mathbf{Typ}$, $\texttt{unit}\in\mathbf{Typ}$
  \item $\forall t\in\mathbf{Typ}, t\ \texttt{list}\in\mathbf{Typ}$
  \item $\forall t\in\mathbf{Typ}, t\ \texttt{ref}\in\mathbf{Typ}$
  \item $\forall t_1,t_2\in\mathbf{Typ}, t_1\times t_2\in\mathbf{Typ}$
  \item $\forall t_1,t_2\in\mathbf{Typ}, t_1\rightarrow t_2\in\mathbf{Typ}$
\end{itemize}

Type environment $\Gamma:\mathbf{Var}\rightarrow \mathbf{Typ}$ is a mapping from names to arbitrary types.
The replacement of $x$ with $t$ in $\Gamma$, i.e. $\Gamma[x:t]$, is defined as follows.
\[
\Gamma[x:t](y) =
  \begin{cases}
    t & \text{if}\ x=y \\
    \Gamma(y) & \text{otherwise}
  \end{cases}
\]

Typing rules:

\begin{figure}[htb]\fbox{
		\begin{minipage}{0.33\textwidth}
			\begin{align*}
			\tag{\sc T-Int}
			\frac{}{\Gamma\vdash n : \texttt{int}}
			\\
			\tag{\sc T-Name}
			\frac{\Gamma(x) = t}{\Gamma\vdash x:t}
			\\
			\tag{\sc T-Fn}
			\frac{\Gamma[x:t_1]\vdash e:t_2}{\Gamma\vdash \texttt{fn}\ x\ \texttt{=>}\ e : t_1\rightarrow t_2}
			\\
			\tag{\sc T-Rec}
			\frac{\Gamma[x:t]\vdash e:t}{\Gamma\vdash \texttt{rec}\ x\ \texttt{=>}\ e : t}
			\end{align*}
		\end{minipage}
		\begin{minipage}{0.33\textwidth}
			\begin{align*}
			\tag{\sc T-True}
			\frac{}{\Gamma\vdash \texttt{true} : \texttt{bool}}
			\\
			\tag{\sc T-False}
			\frac{}{\Gamma\vdash \texttt{false} : \texttt{bool}}
			\\
			\tag{\sc T-Neg}
			\frac{\Gamma\vdash e:\texttt{int}}{\Gamma\vdash \texttt{\textasciitilde} e:\texttt{int}}
			\\
			\tag{\sc T-Not}
			\frac{\Gamma\vdash e:\texttt{bool}}{\Gamma\vdash \texttt{not}\ e:\texttt{bool}}
			\end{align*}
		\end{minipage}
		\begin{minipage}{0.33\textwidth}
			\begin{align*}
			\tag{\sc T-Nil}
			\frac{}{\Gamma\vdash \texttt{nil} : \alpha\ \texttt{list}}
			\\
			\tag{\sc T-Unit}
			\frac{}{\Gamma\vdash \texttt{()} : \texttt{unit}}
			\\
			\tag{\sc T-Group}
			\frac{\Gamma\vdash e:t}{\Gamma\vdash \texttt{(} e \texttt{)} : t}
			\\
			\tag{\sc T-Seq}
			\frac{\Gamma\vdash e_1:unit \quad \Gamma\vdash e_2:t_2}
			{\Gamma\vdash e_1 \texttt{;} e_2 : t_2}
			\end{align*}
	\end{minipage}}
\end{figure}

\begin{figure}[htb]\fbox{
		\begin{minipage}{0.4\textwidth}
			\begin{align*}
			\tag{\sc T-Ref}
			\frac{\Gamma\vdash e : t}{\Gamma\vdash \texttt{ref}\ e : t\ \texttt{ref}}
			\\
			\tag{\sc T-Assign}
			\frac{\Gamma\vdash e_1:t\ \texttt{ref} \quad \Gamma\vdash e_2:t}
			{\Gamma\vdash e_1\ \texttt{:=}\ e_2 : \texttt{unit}}
			\\\\
			\tag{\sc T-Deref}
			\frac{\Gamma\vdash e:t\ \texttt{ref}}{\Gamma\vdash \texttt{!} e:t}
			\\\\
			\tag{\sc T-Pair}
			\frac{\Gamma\vdash e_1:t_1 \quad \Gamma\vdash e_2:t_2}{\Gamma\vdash \texttt{(}e_1\texttt{,}\ e_2\texttt{)} : t_1\times t_2}
			\\\\
			\tag{\sc T-Cons}
			\frac{\Gamma\vdash e_1:t \quad \Gamma\vdash e_2:t\ \texttt{list}}
			{\Gamma\vdash e_1\ \texttt{::}\ e_2 : t\ \texttt{list}}
			\\\\
			\tag{\sc T-App}
			\frac{\Gamma\vdash e_1:t_2\rightarrow t_1 \quad \Gamma\vdash e_2:t_2}
			{\Gamma\vdash e_1\ e_2 : t_1}
			\\\\
			\tag{\sc T-Let}
			\frac{\Gamma\vdash e_1:t_1 \quad \Gamma[x:t_1]\vdash e_2:t_2}
			{\Gamma\vdash \texttt{let}\ x\ \texttt{=}\ e_1\ \texttt{in}\ e_2\ \texttt{end} : t_2}
			\\
			\end{align*}
		\end{minipage}
		\begin{minipage}{0.6\textwidth}
			\begin{align*}
			\tag{\sc T-Arith}
			\frac{\Gamma\vdash e_1:\texttt{int} \quad \Gamma\vdash e_2:\texttt{int} \quad bop\in\{\texttt{+}, \texttt{-}, \texttt{*}, \texttt{/}, \texttt{\%}\}}
			{\Gamma\vdash e_1\ bop\ e_2 : \texttt{int}}
			\\
			\tag{\sc T-Rel}
			\frac{\Gamma\vdash e_1:\texttt{int} \quad \Gamma\vdash e_2:\texttt{int} \quad bop\in\{\texttt{<}, \texttt{<=}, \texttt{>}, \texttt{>=}\}}
			{\Gamma\vdash e_1\ bop\ e_2 : \texttt{bool}}
			\\\\
			\tag{\sc T-Eq}
			\frac{\Gamma\vdash e_1:\alpha \quad \Gamma\vdash e_2:\alpha \quad bop\in\{\texttt{=}, \texttt{<>}\}}
			{\Gamma\vdash e_1\ bop\ e_2 : \texttt{bool}}
			\\\\
			\tag{\sc T-AndAlso}
			\frac{\Gamma\vdash e_1:\texttt{bool} \quad \Gamma\vdash e_2:\texttt{bool}}
			{\Gamma\vdash e_1\ \texttt{andalso}\ e_2 : \texttt{bool}}
			\\\\
			\tag{\sc T-OrElse}
			\frac{\Gamma\vdash e_1:\texttt{bool} \quad \Gamma\vdash e_2:\texttt{bool}}
			{\Gamma\vdash e_1\ \texttt{orelse}\ e_2 : \texttt{bool}}
			\\\\
			\tag{\sc T-Cond}
			\frac{\Gamma\vdash e_1:\texttt{bool} \quad \Gamma\vdash e_2:t \quad \Gamma\vdash e_3:t}
			{\Gamma\vdash \texttt{if}\ e_1\ \texttt{then}\ e_2\ \texttt{else}\ e_3 : t}
			\\\\
			\tag{\sc T-Loop}
			\frac{\Gamma\vdash e_1:\texttt{bool} \quad \Gamma\vdash e_2:unit}
			{\Gamma\vdash \texttt{while}\ e_1\ \texttt{do}\ e_2 : \texttt{unit}}
			\\
			\end{align*}
	\end{minipage}}
\end{figure}

\newpage

\subsection{Polymorphism}

There is no explicit type annotations in SimPL. So principal type inference is necessary.
~\\~\\
1. Some constraint typing rules:

\begin{figure}[htb]\fbox{
		\begin{minipage}{0.4\textwidth}
			\begin{align*}
			\tag{\sc CT-Int}
			\frac{}{\Gamma\vdash n : \texttt{int},\{\}}
			\\\\
			\tag{\sc CT-Name}
			\frac{\Gamma(x) = t}{\Gamma\vdash x:t,\{\}}
			\\\\
			\tag{\sc CT-True}
			\frac{}{\Gamma\vdash \texttt{true} : \texttt{bool},\{\}}
			\\\\
			\tag{\sc CT-False}
			\frac{}{\Gamma\vdash \texttt{false} : \texttt{bool},\{\}}
			\\
			\end{align*}
		\end{minipage}
		\begin{minipage}{0.6\textwidth}
			\begin{align*}
			\tag{\sc CT-Arith}
			\frac{\Gamma\vdash e_1:t_1,q_1 \quad \Gamma\vdash e_2:t_2,q_2 \quad bop\in\{\texttt{+}, \texttt{-}, \texttt{*}, \texttt{/}, \texttt{\%}\}}
			{\Gamma\vdash e_1\ bop\ e_2 : \texttt{int}, q_1\cup q_2 \cup \{t_1=int, t_2=int\}}
			\\\\
			\tag{\sc CT-Rel}
			\frac{\Gamma\vdash e_1:t_1,q_1 \quad \Gamma\vdash e_2:t_2,q_2 \quad bop\in\{\texttt{<}, \texttt{<=}, \texttt{>}, \texttt{>=}\}}
			{\Gamma\vdash e_1\ bop\ e_2 : \texttt{bool}, q_1\cup q_2 \cup \{t_1=int, t_2=int\}}
			\\\\
			\tag{\sc CT-Fn}
			\frac{\Gamma,x:a\vdash e:t,q}{\Gamma\vdash \texttt{fn}\ x:a\ \texttt{=>}\ e:b : a\rightarrow b,q\cup \{t=b\}}
			\\
			\end{align*}
	\end{minipage}}
\end{figure}

\newpage

You need to think of how to deal with other cases.

~\\

2. Unification algorithm:

\begin{align*}
	&\frac{}{(S,\{int=int\}\cup q)->(S,q)}\\
	&\frac{}{(S,\{bool=bool\}\cup q)->(S,q)}\\
	&\frac{}{(S,\{a=a\}\cup q)->(S,q)}\\
	&\frac{}{(S,\{s_{11}->s_{12}=s_{21}->s_{22}\}\cup q)->(S,\{s_{11} = s_{21}, s_{12}=s_{22}\}\cup q)}\\
	&\frac{}{(S,\{a=s\}\cup q)->([a=s]\circ S,q[s/a])}(a\ not\ in\ FV(s))\\
	&\frac{}{(S,\{s=a\}\cup q)->([a=s]\circ S,q[s/a])}(a\ not\ in\ FV(s))\\
\end{align*}

3. Let-Polymorphism is also needed.

\begin{align*}
	&\frac{\Gamma \vdash e_2[e_1/x]:t_2 \quad \Gamma \vdash e_1:t_1}
	{\Gamma\vdash \texttt{let}\ x\ \texttt{=}\ e_1\ \texttt{in}\ e_2\ \texttt{end} : t_2} &(T-LetPoly)\\
	&\frac{\Gamma \vdash e_2[e_1/x]:t_2,q_1 \quad \Gamma \vdash e_1:t_1}
	{\Gamma\vdash \texttt{let}\ x\ \texttt{=}\ e_1\ \texttt{in}\ e_2\ \texttt{end} : t_2, q_1}&(CT-LetPoly)\\
\end{align*}
\newpage

\section{Semantics}

\subsection{State}

A state $s\in\mathbf{State}$ is a triple $(E,M,p)$ where
$E\in\mathbf{Env}$ is the environment,
$M\in\mathbf{Mem}$ is the memory, and
$p\in\mathbb{N}$ is the memory pointer.
\begin{align*}
\mathbf{State} &= \mathbf{Env} \times \mathbf{Mem} \times \mathbb{N} \\
  \mathbf{Env} &= \mathbf{Var} \rightarrow \mathbf{Val}\cup\mathbf{Rec} \\
  \mathbf{Mem} &= \mathbb{N} \rightarrow \mathbf{Val}
\end{align*}

Both the environment and the memory are updateable mappings.
Given an updateable mapping $f:X\rightarrow Y$, the updated mapping $f[x\mapsto y]$,
where $x\in X, y\in Y$, is defined as \[f[x\mapsto y](x') = \begin{cases}
  y & \text{if}\ x=x' \\
  f(x) & \text{otherwise.}
\end{cases}\]

$\mathbf{Val}$ consists of integers, booleans, lists, references, pairs, and functions.  $\mathbf{Rec}$ is the set of recursions.
\begin{align*}
  \mathbf{Val} &= \bigcup_{t\in\mathbf{Typ}}\mathcal{V}_t \\
  \mathcal{V}_\texttt{unit} &= \{ \texttt{unit} \} \\
  \mathcal{V}_\texttt{int} &= \mathbb{Z} = \{\cdots,-3,-2,-1,0,1,2,3,\cdots\}\\
  \mathcal{V}_\texttt{bool} &= \mathbb{B} = \{\btt,\bff\} \\
  \mathcal{V}_{t\ \texttt{list}} &= \bigcup_{i=0}^{\infty}\mathcal{V}_{t\ \texttt{list}}^{(i)} \\
  \mathcal{V}_{t\ \texttt{list}}^{(0)} &= \{ \texttt{nil} \} \\
  \mathcal{V}_{t\ \texttt{list}}^{(i+1)} &= \{\texttt{cons}\}\times\mathcal{V}_t\times\mathcal{V}_{t\ \texttt{list}}^{(i)} \\
  \mathcal{V}_{t\ \texttt{ref}} &= \{\texttt{ref}\}\times\mathbb{N} \\
  \mathcal{V}_{t_1\times t_2} &= \{\texttt{pair}\}\times\mathcal{V}_{t_1}\times\mathcal{V}_{t_2} \\
  \mathcal{V}_{t_1\rightarrow t_2} &= \textcolor{red}{{\mathcal{V}_{t_1}}^{\mathcal{V}_{t_2}}} \subseteq \{\texttt{fun}\}\times\mathbf{Env}\times\mathbf{Var}\times\mathbf{Exp} \\
  \mathbf{Rec} &= \{\texttt{rec}\}\times\mathbf{Env}\times\mathbf{Var}\times\mathbf{Exp}
\end{align*}

\subsection{Rules}

Judgement form: $E,M,p;e\To M',p';v$ where $E\in\mathbf{Env}, M,M'\in\mathbf{Mem}, p\in\mathbb{N}, e\in\mathbf{Exp}, v\in\mathbf{Val}$

\begin{align*}
\tag{\sc E-Int}
\frac{\mathbf{n}=\mathcal{N}\llbracket n\rrbracket}
{E,M,p;n\To M,p;\mathbf{n}}
\\
\tag{\sc E-Name1}
\frac{E(x)=(\texttt{rec},E_1,x_1,e_1) \quad E_1,M,p;\texttt{rec}\ x_1\ \texttt{=>}\ e_1\To M',p';v}
{E,M,p;x\To M',p';v}
\\
\tag{\sc E-Name2}
\frac{E(x)=v}
{E,M,p;x\To M,p;v}
\\
\tag{\sc E-True}
\frac{}
{E,M,p;\texttt{true}\To M,p;\btt}
\\
\tag{\sc E-False}
\frac{}
{E,M,p;\texttt{false}\To M,p;\bff}
\\
\tag{\sc E-Nil}
\frac{}
{E,M,p;\texttt{nil}\To M,p;\texttt{nil}}
\\
\tag{\sc E-Unit}
\frac{}
{E,M,p;\texttt{()}\To M,p;\texttt{unit}}
\\
\tag{\sc E-Group}
\frac{E,M,p;e\To M,p;v}
{E,M,p;\texttt{(}e\texttt{)}\To M,p;v}
\end{align*}

\begin{align*}
\tag{\sc E-Ref}
\frac{E,M,p+1;e\To M'',p';v \quad M'=M''[p\mapsto v]}
{E,M,p;\texttt{ref}\ e\To M',p';(\texttt{ref},p)}
\\
\tag{\sc E-Assign}
\frac{E,M,p;e_1\To M',p';(\texttt{ref},p_1) \quad E,M',p';e_2\To M''',p'';v \quad M''=M'''[p_1\mapsto v]}
{E,M,p;e_1\ \texttt{:=}\ e_2\To M'',p'';\texttt{unit}}
\\
\tag{\sc E-Deref}
\frac{E,M,p;e\To M',p';(\texttt{ref},p_1) \quad v=M'(p_1)}
{E,M,p;\texttt{!}e\To M',p';v}
\end{align*}

\begin{align*}
\tag{\sc E-Fn}
\frac{}
{E,M,p;\texttt{fn}\ x\ \texttt{=>}\ e\To M,p;(\texttt{fun},E,x,e)}
\\
\tag{\sc E-Rec}
\frac{E[x\mapsto(\texttt{rec},E,x,e)],M,p;e\To M',p';v}
{E,M,p;\texttt{rec}\ x\ \texttt{=>}\ e\To M',p';v}
\\
\tag{\sc E-App}
\frac{E,M,p;e_1\To M',p';(\texttt{fun},E_1,x,e) \quad E,M',p';e_2\To M'',p'';v_2 \quad E_1[x\mapsto v_2],M'',p'';e\To M''',p''';v}
{E,M,p;e_1\ e_2\To M''',p''',v}
\end{align*}

\begin{align*}
\tag{\sc E-Pair}
\frac{E,M,p;e_1\To M',p';v_1 \quad E,M',p';e_2\To M'',p'';v_2}
{E,M,p;\texttt{(}e_1\texttt{,}\ e_2\texttt{)}\To M'',p'';(\texttt{pair},v_1,v_2)}
\\
\tag{\sc E-Cons}
\frac{E,M,p;e_1\To M',p';v_1 \quad E,M',p';e_2\To M'',p'';v_2}
{E,M,p;e_1\ \texttt{::}\ e_2\To M'',p'';(\texttt{cons},v_1,v_2)}
\end{align*}

\begin{align*}
\tag{\sc E-Neg}
\frac{E,M,p;e\To M',p';v \quad v'=-v}
{E,M,p;\texttt{\textasciitilde}e\To M',p';v'}
\\
\tag{\sc E-Add}
\frac{E,M,p;e_1\To M',p';v_1 \quad E,M',p';e_2\To M'',p'';v_2 \quad v=v_1+v_2}
{E,M,p;e_1\ \texttt{+}\ e_2\To M'',p'';v}
\\
\tag{\sc E-Sub}
\frac{E,M,p;e_1\To M',p';v_1 \quad E,M',p';e_2\To M'',p'';v_2 \quad v=v_1-v_2}
{E,M,p;e_1\ \texttt{-}\ e_2\To M'',p'';v}
\\
\tag{\sc E-Mul}
\frac{E,M,p;e_1\To M',p';v_1 \quad E,M',p';e_2\To M'',p'';v_2 \quad v=v_1 v_2}
{E,M,p;e_1\ \texttt{*}\ e_2\To M'',p'';v}
\\
\tag{\sc E-Div}
\frac{E,M,p;e_1\To M',p';v_1 \quad E,M',p';e_2\To M'',p'';v_2 \quad v_2\ne 0 \quad v=v_1\ \mathtt{div}\ v_2}
{E,M,p;e_1\ \texttt{/}\ e_2\To M'',p'';v}
\\
\tag{\sc E-Mod}
\frac{E,M,p;e_1\To M',p';v_1 \quad E,M',p';e_2\To M'',p'';v_2 \quad v_2\ne 0 \quad v=v_1\ \mathtt{mod}\ v_2}
{E,M,p;e_1\ \texttt{\%}\ e_2\To M'',p'';v}
\end{align*}

\begin{align*}
\tag{\sc E-Less1}
\frac{E,M,p;e_1\To M',p';v_1 \quad E,M',p';e_2\To M'',p'';v_2 \quad v_1<v_2}
{E,M,p;e_1\ \texttt{<}\ e_2\To M'',p'';\btt}
\\
\tag{\sc E-Less2}
\frac{E,M,p;e_1\To M',p';v_1 \quad E,M',p';e_2\To M'',p'';v_2 \quad v_1\ge v_2}
{E,M,p;e_1\ \texttt{<}\ e_2\To M'',p'';\bff}
\\
\tag{\sc E-LessEq1}
\frac{E,M,p;e_1\To M',p';v_1 \quad E,M',p';e_2\To M'',p'';v_2 \quad v_1\le v_2}
{E,M,p;e_1\ \texttt{<=}\ e_2\To M'',p'';\btt}
\\
\tag{\sc E-LessEq2}
\frac{E,M,p;e_1\To M',p';v_1 \quad E,M',p';e_2\To M'',p'';v_2 \quad v_1>v_2}
{E,M,p;e_1\ \texttt{<=}\ e_2\To M'',p'';\bff}
\\
\tag{\sc E-Greater1}
\frac{E,M,p;e_1\To M',p';v_1 \quad E,M',p';e_2\To M'',p'';v_2 \quad v_1>v_2}
{E,M,p;e_1\ \texttt{>}\ e_2\To M'',p'';\btt}
\\
\tag{\sc E-Greater2}
\frac{E,M,p;e_1\To M',p';v_1 \quad E,M',p';e_2\To M'',p'';v_2 \quad v_1\le v_2}
{E,M,p;e_1\ \texttt{>}\ e_2\To M'',p'';\bff}
\\
\tag{\sc E-GreaterEq1}
\frac{E,M,p;e_1\To M',p';v_1 \quad E,M',p';e_2\To M'',p'';v_2 \quad v_1\ge v_2}
{E,M,p;e_1\ \texttt{>=}\ e_2\To M'',p'';\btt}
\\
\tag{\sc E-GreaterEq2}
\frac{E,M,p;e_1\To M',p';v_1 \quad E,M',p';e_2\To M'',p'';v_2 \quad v_1<v_2}
{E,M,p;e_1\ \texttt{>=}\ e_2\To M'',p'';\bff}
\\
\tag{\sc E-Eq1}
\frac{E,M,p;e_1\To M',p';v_1 \quad E,M',p';e_2\To M'',p'';v_2 \quad v_1=v_2}
{E,M,p;e_1\ \texttt{=}\ e_2\To M'',p'';\btt}
\\
\tag{\sc E-Eq2}
\frac{E,M,p;e_1\To M',p';v_1 \quad E,M',p';e_2\To M'',p'';v_2 \quad v_1\ne v_2}
{E,M,p;e_1\ \texttt{=}\ e_2\To M'',p'';\bff}
\\
\tag{\sc E-Neq1}
\frac{E,M,p;e_1\To M',p';v_1 \quad E,M',p';e_2\To M'',p'';v_2 \quad v_1\ne v_2}
{E,M,p;e_1\ \texttt{<>}\ e_2\To M'',p'';\btt}
\\
\tag{\sc E-Neq2}
\frac{E,M,p;e_1\To M',p';v_1 \quad E,M',p';e_2\To M'',p'';v_2 \quad v_1=v_2}
{E,M,p;e_1\ \texttt{<>}\ e_2\To M'',p'';\bff}
\end{align*}

\begin{align*}
\tag{\sc E-Not1}
\frac{E,M,p;e\To M',p';\btt}
{E,M,p;\texttt{not}\ e\To M',p';\bff}
\\
\tag{\sc E-Not2}
\frac{E,M,p;e\To M',p';\bff}
{E,M,p;\texttt{not}\ e\To M',p';\btt}
\\
\tag{\sc E-AndAlso1}
\frac{E,M,p;e_1\To M',p';\btt \quad E,M',p';e_2\To M'',p'';v}
{E,M,p;e_1\ \texttt{andalso}\ e_2\To M'',p'';v}
\\
\tag{\sc E-AndAlso2}
\frac{E,M,p;e_1\To M',p';\bff}
{E,M,p;e_1\ \texttt{andalso}\ e_2\To M',p';\bff}
\\
\tag{\sc E-OrElse1}
\frac{E,M,p;e_1\To M',p';\btt}
{E,M,p;e_1\ \texttt{orelse}\ e_2\To M',p';\btt}
\\
\tag{\sc E-OrElse2}
\frac{E,M,p;e_1\To M',p';\bff \quad E,M',p';e_2\To M'',p'';v}
{E,M,p;e_1\ \texttt{orelse}\ e_2\To M'',p'';v}
\end{align*}

\begin{align*}
\tag{\sc E-Seq}
\frac{E,M,p;e_1\To M',p';v_1 \quad E,M',p';e_2\To M'',p'';v_2}
{E,M,p;e_1 \texttt{;} e_2\To M'',p'';v_2}
\\
\tag{\sc E-Let}
\frac{E,M,p;e_1\To M',p';v_1 \quad E[x\mapsto v_1],M',p';e_2\To M'',p'';v_2}
{E,M,p;\texttt{let}\ x\ \texttt{=}\ e_1\ \texttt{in}\ e_2\ \texttt{end}\To M'',p'';v_2}
\\
\tag{\sc E-Cond1}
\frac{E,M,p;e_1\To M',p';\btt \quad E,M',p';e_2\To M'',p'';v}
{E,M,p;\texttt{if}\ e_1\ \texttt{then}\ e_2\ \texttt{else}\ e_3\To M'',p'';v}
\\
\tag{\sc E-Cond2}
\frac{E,M,p;e_1\To M',p';\bff \quad E,M',p';e_3\To M'',p'';v}
{E,M,p;\texttt{if}\ e_1\ \texttt{then}\ e_2\ \texttt{else}\ e_3\To M'',p'';v}
\\
\tag{\sc E-Loop1}
\frac{E,M,p;e_1\To M',p';\btt \quad E,M',p';e_2\ \texttt{;}\ \texttt{while}\ e_1\ \texttt{do}\ e_2\To M'',p'';v}
{E,M,p;\texttt{while}\ e_1\ \texttt{do}\ e_2\To M'',p'';v}
\\
\tag{\sc E-Loop2}
\frac{E,M,p;e_1\To M',p';\bff}
{E,M,p;\texttt{while}\ e_1\ \texttt{do}\ e_2\To M',p';\texttt{unit}}
\end{align*}

\subsection{Supplementary Details}

\begin{itemize}
  \item $\mathcal{N}\llbracket n\rrbracket$ is the value of $n$, e.g. $\mathcal{N}\llbracket\texttt{123}\rrbracket = 123$.
  \item If $a$ and $d$ are integers, with $d$ non-zero, then a remainder $a\ \texttt{mod}\ d$ is an integer $r$ such that $a = qd + r$ for some integer $q$, and with $|r| < |d|$.  $a\ \texttt{div}\ d = q$ is the quotient.
  \item Equality comparisons ($=$ and $\ne$) work for any equality type.
  \begin{itemize}
    \item $\forall n\in\mathbb{Z}, n=n$
    \item $\btt=\btt, \bff=\bff$
    \item $\texttt{nil}=\texttt{nil}$
    \item $(\texttt{cons},h_1,t_1)=(\texttt{cons},h_2,t_2) \iff h_1=h_2\land t_1=t_2$
    \item $(\texttt{ref},p_1)=(\texttt{ref},p_2) \iff p_1=p_2$
    \item $(\texttt{pair},a_1,b_1)=(\texttt{pair},a_2,b_2) \iff a_1=a_2\land b_1=b_2$
    \item $v_1\ne v_2 \iff \lnot(v_1=v_2)$
  \end{itemize}
\end{itemize}

\section{Examples}

\begin{lstlisting}[language=ML]
let add = fn x => fn y => x + y
in  add 1 2
end
(* ==> 3 *)
\end{lstlisting}

\begin{lstlisting}[language=ML]
let fact = rec f => fn x => if x=1 then 1 else x * (f (x-1))
in  fact 4
end
(* ==> 24 *)
\end{lstlisting}

\begin{lstlisting}[language=ML]
let gcd = rec g => fn a => fn b =>
            if b=0 then a else g b (a % b)
in  gcd 34986 3087
end
(* ==> 1029 *)
\end{lstlisting}

\begin{lstlisting}[language=ML]
let gcd = fn x => fn y =>
            let a = ref x in
              let b = ref y in
                let c = ref 0 in
                  (while !b <> 0 do c := !a; a := !b; b := !c % !b);
                  !a
                end
              end
            end
in  gcd 34986 3087
end
(* ==> 1029 *)
\end{lstlisting}

\begin{lstlisting}[language=ML]
let
  sum = rec sum =>
  		fn a => if a=nil
                then 0
                else hd a + sum (tl a)
in
  sum (1::2::3::nil)
end
(* ==> 6 *)
\end{lstlisting}

\section{Implementation}

\subsection{Command-line Interface}

You are required to implement the SimPL interpreter in Java, and submit a runnable JAR file, say \texttt{SimPL.jar}.  Your interpreter should accept exactly one command-line argument, which is the path of the SimPL program, and then read the program file for execution.  Your interpreter should output the result of the execution to the standard output (\texttt{System.out}).
\begin{itemize}
  \item Your interpreter is started by using \texttt{java -jar SimPL.jar \emph{program}.spl}.
  \item If there is a syntax error, output \result{syntax error}.
  \item If there is a type error, output \result{type error}.
  \item If there is a runtime error, output \result{runtime error}.
  \item If the result is an integer, output its value.
  \item If the result is $\btt$, output \result{true}.
  \item If the result is $\bff$, output \result{false}.
  \item If the result is \texttt{nil}, output \result{nil}.
  \item If the result is \texttt{unit}, output \result{unit}.
  \item If the result is a list, output \result{list@} followed by its length.
  \item If the result is a reference, output \result{ref@} followed by its content.
  \item If the result is a pair, output \result{pair@$v_1$@$v_2$} where $v_i$ is $i$-th element of the pair.
  \item If the result is a function, output \result{fun}.
  \item Spaces in the output are insignificant.
  \item For any test program, your interpreter has up to 5 seconds to execute it.
  \item Your interpreter is started in a sandbox environment and can only read the current test program.
\end{itemize}

\subsection{Predefined Functions}

\begin{align*}
  fst &: t_1\times t_2\to t_1 \\
  snd &: t_1\times t_2\to t_2 \\
  hd &: t\ \texttt{list}\to t \\
  tl &: t\ \texttt{list}\to t\ \texttt{list} \\
  fst(\texttt{pair},v_1,v_2) &= v_1 \\
  snd(\texttt{pair},v_1,v_2) &= v_2 \\
  hd(\texttt{cons},v_1,v_2) &= v_1 \\
  tl(\texttt{cons},v_1,v_2) &= v_2 \\
  hd(\texttt{nil}) &= \textcolor{red}{\tt error} \\
  tl(\texttt{nil}) &= \textcolor{red}{\tt error}
\end{align*}

\texttt{fst}, \texttt{snd}, \texttt{hd}, and \texttt{tl} are not keywords.
They are predefined names in the topmost environment, work in the same way as user-defined functions, and can be bound to other values.

\section{Bonus}

\begin{itemize}
  \item Mutually recursive combinator
  \item Infinite streams
  \item Garbage collection (of ref cells)
  \item Tail recursion
  \item Lazy evaluation
  \item Other features or optimizations
\end{itemize}

\section{Deliverables}
\begin{itemize}
  \item A single zip file (\texttt{LastName\_StudentId\_SimPL.zip}) containing the complete project, including the runnable JAR file specified in Section 7.1, with all \texttt{TODO} items and other missing implementations properly completed. While \texttt{Interpreter.java} may be temporarily modified during development for convenience (e.g., testing), the submitted version must be restored to the original skeleton version. Your submission will be evaluated based on both the existing test cases (which must be left unchanged) and additional hidden test cases that will not be provided in advance.
  \item A single PDF report that clearly explains your implementation (via code snippets of the classes) and includes explanations of:
    \begin{itemize}
      \item One library function from \texttt{src/simpl/interpreter/lib}
      \item One function from \texttt{src/simpl/interpreter/pcf}
      \item Three values from \texttt{src/simpl/interpreter}
      \item Four expressions from \texttt{src/simpl/parser/ast}, including at least two from pure lambda calculus
      \item Four types from \texttt{src/simpl/typing}
    \end{itemize}
The report should clearly demonstrate your comprehension of each component and should be straightforward to complete given your work in the project. Include any bonus features implemented, along with relevant code snippets for context.

  \item Any instances of plagiarism, either among submissions or from online sources, will result in a score of zero.

\end{itemize}



\end{document}
