hw2: remove extra stuff from semantics
This commit is contained in:
Binary file not shown.
@@ -45,8 +45,9 @@ you will implement the semantics for a small imperative language, named WHILE.
|
||||
\newcommand{\false}{\mbox{\tt false}}
|
||||
\newcommand{\note}[1]{\mbox{\tt not}~{#1}}
|
||||
|
||||
\begin{figure}\label{fig:lang}
|
||||
\begin{figure}[H]
|
||||
\caption{The WHILE language}
|
||||
\label{fig:lang}
|
||||
\[
|
||||
\begin{array}{llr}
|
||||
\mydefhead{e ::=\qquad\qquad\qquad\qquad}{Expressions}
|
||||
@@ -58,7 +59,7 @@ you will implement the semantics for a small imperative language, named WHILE.
|
||||
\mydefcase{\ife e e e}{conditional expressions}
|
||||
\mydefcase{\whilee e e}{while expressions}
|
||||
\mydefcase{e ~boolop~ e}{boolean binary operations}
|
||||
\mydefcase{\not e}{negation}
|
||||
\mydefcase{\note e}{negation}
|
||||
\\
|
||||
\mydefhead{v ::=\qquad\qquad\qquad\qquad}{Values}
|
||||
\mydefcase{i}{integer values}
|
||||
@@ -81,41 +82,8 @@ Once we have mutable references, other language constructs become more useful,
|
||||
such as sequencing operations ($e_1;e_2$).
|
||||
|
||||
|
||||
|
||||
%---------
|
||||
\section{Small-step semantics}
|
||||
|
||||
\newcommand{\ssrule}[3]{
|
||||
\rel{#1} &
|
||||
\frac{\strut\begin{array}{@{}c@{}} #2 \end{array}}
|
||||
{\strut\begin{array}{@{}c@{}} #3 \end{array}}
|
||||
\\~\\
|
||||
}
|
||||
%\newcommand{\sstep}[4]{\ctxt[{#1}],{#2} \rightarrow \ctxt[{#3}],{#4}}
|
||||
%\newcommand{\sstepraw}[4]{{#1},{#2} \rightarrow {#3},{#4}}
|
||||
\newcommand{\sstep}[4]{{#1},{#2} \rightarrow {#3},{#4}}
|
||||
\newcommand{\ctxt}{C}
|
||||
|
||||
The small-step semantics for WHILE are given in Figure~\ref{fig:smallstep}.
|
||||
%For the sake of brevity, these rules use \emph{evaluation contexts} ($\ctxt$),
|
||||
%which specify which \emph{redex} will be evaluated next.
|
||||
%The evaluation rules then apply to the ``hole'' ($\bullet$) in this context.
|
||||
%
|
||||
Most of these rules are fairly straightforward, but there are a couple of points
|
||||
to note with the $\rel{ss-while}$ rule.
|
||||
First of all, this is the only rule that makes a more complex expression
|
||||
when it has finished.
|
||||
(This rule is much cleaner when specified with the big-step operational semantics.)
|
||||
|
||||
Secondly, note the final value of this expression once the while loop completes.
|
||||
It will \emph{always} be {\false} when it completes.
|
||||
We could have created a special value, such as {\tt null},
|
||||
or we could have made the while loop a statement that returns no value.
|
||||
Both choices, however, would complicate our language needlessly.
|
||||
|
||||
|
||||
%--------------
|
||||
\section{YOUR ASSIGNMENT}
|
||||
\section{Semantics}
|
||||
\newcommand{\bstep}[4]{{#1},{#2} \Downarrow {#3},{#4}}
|
||||
|
||||
% Format for a big-step evaluation rule.
|
||||
@@ -129,183 +97,9 @@ Both choices, however, would complicate our language needlessly.
|
||||
\\~\\
|
||||
}
|
||||
|
||||
\noindent
|
||||
{\bf Part 1:}
|
||||
Rewrite the operational semantic rules for WHILE in \LaTeX\
|
||||
to use big-step operational semantics instead.
|
||||
Submit both your \LaTeX\ source and the generated PDF file.
|
||||
|
||||
Extend your semantics with features to handle boolean values.
|
||||
{\bf Do not treat these a binary operators.}
|
||||
Specifically, add support for:
|
||||
\begin{compactitem}
|
||||
\item {\tt and}
|
||||
\item {\tt or}
|
||||
\item {\tt not}
|
||||
\end{compactitem}
|
||||
|
||||
The exact behavior of these new features is up to you,
|
||||
but should seem reasonable to most programmers.
|
||||
|
||||
\bigskip
|
||||
\noindent
|
||||
{\bf Part 2:}
|
||||
Once you have your semantics defined,
|
||||
download {\tt WhileInterp.hs} and implement the {\tt evaluate} function,
|
||||
as well as any additional functions you need.
|
||||
Your implementation must be consistent with your operational semantics,
|
||||
{\it including your extensions for {\tt and}, {\tt or}, and {\tt not}}.
|
||||
Also, you may not change any type signatures provided in the file.
|
||||
|
||||
Finally, implement the interpreter to match your semantics.
|
||||
|
||||
\bigskip
|
||||
\noindent
|
||||
{\bf Zip all files together into {\tt hw2.zip} and submit to Canvas.}
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
%\begin{figure}[H]\label{fig:smallstep}
|
||||
%\caption{Small-step semantics for WHILE}
|
||||
%{\bf Runtime Syntax:}
|
||||
%\[
|
||||
%\begin{array}{rclcl}
|
||||
% \ctxt & \in & {Context} \quad & ::= & \quad \ctxt; e
|
||||
% ~|~ \ctxt ~op~ e
|
||||
% ~|~ v ~op~ \ctxt
|
||||
% ~|~ \assign{x}{\ctxt}
|
||||
% ~|~ \ife{\ctxt}{e_1}{e_2}
|
||||
% ~|~ \bullet \\
|
||||
% \sigma & \in & {Store} \quad & = & \quad {variable} ~\rightarrow ~v \\
|
||||
% \\
|
||||
%\end{array}
|
||||
%\]
|
||||
%{\bf Evaluation Rules:~~~ \fbox{$\sstepraw{e}{\sigma}{e'}{\sigma'}$}} \\
|
||||
%\[
|
||||
%\begin{array}{cc}
|
||||
%\begin{array}{r@{\qquad}l}
|
||||
%\ssrule{ss-var}{
|
||||
% x \in domain(\sigma) \qquad \sigma(x)=v
|
||||
%}{
|
||||
% \sstep{x}{\sigma}{v}{\sigma}
|
||||
%}
|
||||
%\ssrule{ss-assign}{
|
||||
%}{
|
||||
% \sstep{\assign{x}{v}}{\sigma}{v}{\sigma[x:=v]}
|
||||
%}
|
||||
%\ssrule{ss-op}{
|
||||
% v = v_1 ~op~ v_2
|
||||
%}{
|
||||
% \sstep{v_1~op~v_2}{\sigma}{v}{\sigma}
|
||||
%}
|
||||
%\end{array}
|
||||
% &
|
||||
%\begin{array}{r@{\qquad}l}
|
||||
%\ssrule{ss-seq}{
|
||||
%}{
|
||||
% \sstep{v;e}{\sigma}{e}{\sigma}
|
||||
%}
|
||||
%\ssrule{ss-iftrue}{
|
||||
%}{
|
||||
% \sstep{\ife{\true}{e_1}{e_2}}{\sigma}{e_1}{\sigma}
|
||||
%}
|
||||
%\ssrule{ss-iffalse}{
|
||||
%}{
|
||||
% \sstep{\ife{\false}{e_1}{e_2}}{\sigma}{e_2}{\sigma}
|
||||
%}
|
||||
%\ssrule{ss-while}{
|
||||
%}{
|
||||
% \sstep{\whilee{e_1}{e_2}}{\sigma}{\ife{e_1}{e_2;\whilee{e_1}{e_2}}{\false}}{\sigma}
|
||||
%}
|
||||
%\end{array}
|
||||
%\end{array}
|
||||
%\]
|
||||
%\end{figure}
|
||||
%
|
||||
|
||||
\begin{figure}[H]\label{fig:smallstep}
|
||||
\caption{Small-step semantics for WHILE}
|
||||
{\bf Runtime Syntax:}
|
||||
\[
|
||||
\begin{array}{rclcl}
|
||||
\sigma & \in & {Store} \quad & = & \quad {variable} ~\rightarrow ~v \\
|
||||
\\
|
||||
\end{array}
|
||||
\]
|
||||
{\bf Evaluation Rules:~~~ \fbox{$\sstep{e}{\sigma}{e'}{\sigma'}$}} \\
|
||||
\[
|
||||
%\begin{array}{cc}
|
||||
\begin{array}{r@{\qquad}l}
|
||||
\ssrule{ss-seqctx}{
|
||||
\sstep{e_1}{\sigma}{e_1'}{\sigma'}
|
||||
}{
|
||||
\sstep{e_1;e_2}{\sigma}{e_1';e_2}{\sigma'}
|
||||
}
|
||||
\ssrule{ss-seq}{
|
||||
}{
|
||||
\sstep{v;e}{\sigma}{e}{\sigma}
|
||||
}
|
||||
\ssrule{ss-opctx1}{
|
||||
\sstep{e_1}{\sigma}{e_1'}{\sigma'}
|
||||
}{
|
||||
\sstep{e_1~op~e_2}{\sigma}{e_1'~op~e_2}{\sigma'}
|
||||
}
|
||||
\ssrule{ss-opctx2}{
|
||||
\sstep{e_2}{\sigma}{e_2'}{\sigma'}
|
||||
}{
|
||||
\sstep{v_1~op~e_2}{\sigma}{v_1~op~e_2'}{\sigma'}
|
||||
}
|
||||
\ssrule{ss-op}{
|
||||
v = v_1 ~op~ v_2
|
||||
}{
|
||||
\sstep{v_1~op~v_2}{\sigma}{v}{\sigma}
|
||||
}
|
||||
\end{array}
|
||||
\begin{array}{r@{\qquad}l}
|
||||
\ssrule{ss-var}{
|
||||
x \in domain(\sigma) \qquad \sigma(x)=v
|
||||
}{
|
||||
\sstep{x}{\sigma}{v}{\sigma}
|
||||
}
|
||||
\ssrule{ss-assignctx}{
|
||||
\sstep{e_1}{\sigma}{e_1'}{\sigma'}
|
||||
}{
|
||||
\sstep{\assign{x}{e}}{\sigma}{\assign{x}{e'}}{\sigma'}
|
||||
}
|
||||
\ssrule{ss-assign}{
|
||||
}{
|
||||
\sstep{\assign{x}{v}}{\sigma}{v}{\sigma[x:=v]}
|
||||
}
|
||||
\ssrule{ss-iftrue}{
|
||||
}{
|
||||
\sstep{\ife{\true}{e_1}{e_2}}{\sigma}{e_1}{\sigma}
|
||||
}
|
||||
\ssrule{ss-iffalse}{
|
||||
}{
|
||||
\sstep{\ife{\false}{e_1}{e_2}}{\sigma}{e_2}{\sigma}
|
||||
}
|
||||
\end{array}
|
||||
\]
|
||||
\[
|
||||
\begin{array}{r@{\qquad}l}
|
||||
\ssrule{ss-ifctx}{
|
||||
\sstep{e_1}{\sigma}{e_1'}{\sigma'}
|
||||
}{
|
||||
\sstep{\ife{e_1}{e_2}{e_3}}{\sigma}{\ife{e_1'}{e_2}{e_3}}{\sigma'}
|
||||
}
|
||||
\ssrule{ss-while}{
|
||||
}{
|
||||
\sstep{\whilee{e_1}{e_2}}{\sigma}{\ife{e_1}{e_2;\whilee{e_1}{e_2}}{\false}}{\sigma}
|
||||
}
|
||||
\end{array}
|
||||
\]
|
||||
\end{figure}
|
||||
|
||||
|
||||
\begin{figure}[H]\label{fig:bigstep}
|
||||
\begin{figure}[H]
|
||||
\caption{Big-step semantics for WHILE}
|
||||
\label{fig:bigstep}
|
||||
{\bf Runtime Syntax:}
|
||||
\[
|
||||
\begin{array}{rclcl}
|
||||
|
||||
Reference in New Issue
Block a user