% -*- Mode: LaTeX -*-

\section{A Lazy Interpreter for the Kernel Language}
\label{sec:interp2}

\subsection{Changes to Abstract Machine}
\[\begin{array}{lclcl}
\store      & \in & \bx{Store} & = & \bx{Location} \rightarrow \{\ftag{\val}\mid
\ttag{\thunk}\mid\dtag{\susps}\} \\
\thunk      & \in & \bx{Thunk} & = & \bx{Code} \times \bx{Environments}
\end{array}\]

\subsection{Additional Instructions}

\begin{center}
\begin{tabular}{l@{\hm::\hm}p{4.5in}}
\setenv{\envs} & Set the environment stack to $\envs$
\end{tabular}
\end{center}

\subsection{Changes to Evaluation Rules}

\subsubsection*{Identifiers}

\noindent\begin{tabular}{@{}lc}
\fbx{eval} identifier (\fbx{thunk}): & \\
& \inference{\state{\_}{\eval{x}:\insts}{\envs[x\mapsto\loc_{x}]}{\works}%
                   {\store[\loc_{x}\mapsto\ttag{(\insts',\envs')}]}{}}%
            {\state{\_}{\insts'\append(\setenv{\envs}:\insts)}{\envs'}{\works}{\store'}{}}\\
\multicolumn{2}{l}{where $\store' = \store[\loc_{x}\mapsto\dtag{[\;]}]$}
\end{tabular}

\subsubsection*{Non-Strict Primitive Functions}

\noindent\begin{tabular}{@{}lc}
\fbx{eval} \tbx{Cons}: & \\
& \inference{\state{\_}{\eval{\tbx{Cons}(x_{1},x_{2})}:\insts}{\envs}{\works}{\store}{}}%
            {\state{\loc}{\insts}{\envs}{\works}{\store'}{}}\\ \\
\multicolumn{2}{l}{where $\begin{array}[t]{l}
\store'=\store+\{\;\loc\mapsto\ttag{\thunk_{1}},(\loc+1)\mapsto\ttag{\thunk_{2}}\;\} \\
\thunk_{1}=([\eval{x_{1}}:\update{\loc}], \envs) \\
\thunk_{2}=([\eval{x_{2}}:\update{\loc+1}], \envs)
\end{array}$}
\end{tabular}

\subsubsection*{Block Expression}

\noindent\begin{tabular}{@{}lc}
\fbx{eval} block: & \\
& \inference{\state{\_}{\eval{\{\;x_{1}=E_{1};\ldots;x_{n}=E_{n}\;\tbx{in}\;X\;\}}:\insts}%
                   {\envs}{\works}{\store}{}}%
            {\state{\_}{\eval{X}:\popenv:\insts}{\env:\envs}%
                   {\works \append \works'}{\store'}{}}\\ \\
\multicolumn{2}{l}{where $\begin{array}[t]{l}
\env = \{\;x_{1}\mapsto\loc_{1}\ldots{}x_{n}\mapsto\loc_{n}\;\}\\
\store' = \store+\{\;\loc_{1}\mapsto\ttag{\thunk_{1}}\ldots\loc_{n}\mapsto\ttag{\thunk_{n}}\;\}\\
\thunk_{1} = ([\eval{E_{1}}:\update{\loc_{1}}], \env:\envs)\\
\cdots \\
\thunk_{n} = ([\eval{E_{n}}:\update{\loc_{n}}], \env:\envs) \\
\works' = [(\_, [\eval{x_{1}}:\sched], \env:\envs):\ldots:(\_, [\eval{x_{n}}:\sched], \env:\envs)]
\end{array}$}
\end{tabular}

\subsubsection*{Primitive Functions}

\noindent\begin{tabular}{@{}lc}
\tbx{I-fetch} (\fbx{thunk}): & \\
& \inference{\state{\_}{\primapp{\tbx{I-fetch}}{x_{1},x_{2}}:\insts}%
                   {\envs[x_{1}\mapsto\loc_{1},x_{2}\mapsto\loc_{2}]}{\works}{\store}{}}%
            {\state{\_}{\insts'\append(\setenv{\envs}:\insts)}{\envs'}{\works}{\store'}{}}\\
\multicolumn{2}{l}{where $\begin{array}[t]{l}
\store[\loc_{1}\mapsto\ftag{\loc},\loc_{2}\mapsto\ftag{\ul{i}},
(\loc+i)\mapsto\ttag{(\insts',\envs')}]\\
\store'=\store[(\loc+i)\mapsto\dtag{[\;]}]
\end{array}$}
\end{tabular}

\noindent\begin{tabular}{@{}lc}
\tbx{I-store} (\fbx{thunk}): & \\
& \inference{\state{\_}{\primapp{\tbx{I-store}}{x_{1},x_{2},x_{3}}:\insts}%
                   {\envs[x_{1}\mapsto\loc_{1},x_{2}\mapsto\loc_{2},x_{3}\mapsto\loc_{3}]}%
                   {\works}{\store}{}}%
            {\state{\tbx{err}}{[\;]}{\envs}{[\;]}{\store}{}}\\
\multicolumn{2}{l}{where $\store[\loc_{1}\mapsto\ftag{\loc},\loc_{2}\mapsto\ftag{\ul{i}},
\loc_{3}\mapsto\ftag{\val},(\loc+i)\mapsto\ttag{\thunk}]$}
\end{tabular}

\noindent\begin{tabular}{@{}lc}
\tbx{M-take} (\fbx{thunk}): & \\
& \inference{\state{\_}{\primapp{\tbx{M-take}}{x_{1},x_{2}}:\insts}%
                   {\envs[x_{1}\mapsto\loc_{1},x_{2}\mapsto\loc_{2}]}{\works}{\store}{}}%
            {\state{\tbx{err}}{[\;]}{\envs}{[\;]}{\store}{}}\\
\multicolumn{2}{l}{where $\store[\loc_{1}\mapsto\ftag{\loc},\loc_{2}\mapsto\ftag{\ul{i}},
(\loc+i)\mapsto\ttag{\thunk}]$}
\end{tabular}

\noindent\begin{tabular}{@{}lc}
\tbx{M-put} (\fbx{thunk}): & \\
& \inference{\state{\_}{\primapp{\tbx{M-put}}{x_{1},x_{2},x_{3}}:\insts}%
                   {\envs[x_{1}\mapsto\loc_{1},x_{2}\mapsto\loc_{2},x_{3}\mapsto\loc_{3}]}%
                   {\works}{\store}{}}%
            {\state{\tbx{err}}{[\;]}{\envs}{[\;]}{\store}{}}\\
\multicolumn{2}{l}{where $\store[\loc_{1}\mapsto\ftag{\loc},\loc_{2}\mapsto\ftag{\ul{i}},
\loc_{3}\mapsto\ftag{\val},(\loc+i)\mapsto\ttag{\thunk}]$}
\end{tabular}

