summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--defio.tex4
-rw-r--r--defstate.tex13
-rw-r--r--rules.tex2
-rw-r--r--rulesget.tex16
-rw-r--r--rulesput.tex23
-rw-r--r--smurf.sty8
6 files changed, 58 insertions, 8 deletions
diff --git a/defio.tex b/defio.tex
index c9b1f95..fb92e20 100644
--- a/defio.tex
+++ b/defio.tex
@@ -15,10 +15,12 @@ Op een stack zijn twee instructies gedefinieerd:
\begin{gather*}
\pushop : a \times \Stack{a} \to \Stack{a} \\
\push{e}{s} \isdef [e:s] \\[1em]
- \popop : \Stack{a} \to a \times \Stack{a} \\
+ \popop : \Stack{a} \hookrightarrow a \times \Stack{a} \\
\pop{[e:s]} \isdef (e,s) \\
\end{gather*}
+$\popop$ is een partiële functie omdat $\pop\Nil$ niet gedefinieerd is.
+
\medskip
We zullen de input en output beide als $\Stack{\String}$ modelleren. In feite
zal zelfs blijken dat we op $\Input$ de operatie $\pushop$ niet nodig hebben,
diff --git a/defstate.tex b/defstate.tex
index 3ff1a79..4dee41e 100644
--- a/defstate.tex
+++ b/defstate.tex
@@ -16,3 +16,16 @@ $\lambda$ in overeenstemming met de documentatie \cite{safalra}:
variable values are initially set to the empty string.
\end{quote}
+Om de waarde van een key $k$ uit store $\str$ te halen gebruiken we simpelweg
+$\str~k$. Vervolgens definiëren we $\putop:\SynString \times \SynString \times
+(\String\to\String) \to (\String\to\String)$ die gegeven een variabelenaam, een
+waarde en een oude store een nieuwe store oplevert:
+
+$$
+ \put{\var}{\val}{\str} k =
+ \begin{cases}
+ \val & \text{als $k=\var$} \\
+ \str~k & \text{als $k\ne\var$}
+ \end{cases}
+$$
+
diff --git a/rules.tex b/rules.tex
index fd145e4..e77286d 100644
--- a/rules.tex
+++ b/rules.tex
@@ -17,8 +17,8 @@ Smurfprogramma's makkelijker zal maken.
%\input{rulestail}
%\input{rulesquotify}
%\input{rulescat}
-%\input{rulesput}
\input{rulesget}
+\input{rulesput}
%\input{rulesinput}
%\input{rulesoutput}
%\input{rulesexec}
diff --git a/rulesget.tex b/rulesget.tex
index b61b764..f8810a7 100644
--- a/rulesget.tex
+++ b/rulesget.tex
@@ -1,19 +1,27 @@
% vim: set spelllang=nl:
\subsection{\texttt{Get}}
-$\StmGet$ neemt het bovenste element van de stack en gebruikt dit als
-variabelenaam om in de variable store te zoeken.
+\begin{quote}
+ g - Pops a variable name from the stack, and pushes the value of the
+ variable.
+\end{quote}
+
+De regel voor dit statement spreekt voor zich. In het geval dat $\stk$ leeg is,
+is $\pop\stk$ niet gedefinieerd en kunnen we de regel dus niet toepassen. Omdat
+$\StmGet$ geen IO gebruikt kunnen we $\ip$, $\ip'$ en $\op$ direct doorgeven.
$$
\begin{prooftree}
\trans
- {\pgm}{\ip}{([\str~\var:\stk], \str)}
+ {\pgm}{\ip}{(\push{\str~\var}{\stk}, \str)}
{\ip'}{\op}{\st}
\justifies
\trans
- {\StmGet:\pgm}{\ip}{([\var:\stk],\str)}
+ {\StmGet:\pgm}{\ip}{(\stk,\str)}
{\ip'}{\op}{\st}
\using{\rgetns}
+ \qquad
+ \text{met $(\var,\stk') = \pop{\stk}$.}
\end{prooftree}
$$
diff --git a/rulesput.tex b/rulesput.tex
index ce3c624..1691a5b 100644
--- a/rulesput.tex
+++ b/rulesput.tex
@@ -1,9 +1,30 @@
% vim: set spelllang=nl:
\subsection{\texttt{Put}}
+\begin{quote}
+ p - Pops a variable name from the stack, pops a value from the stack, and
+ assigns that value to the variable name.
+\end{quote}
+
+We halen twee strings van de stack en gebruiken $\putop$ om een nieuwe variable
+store te krijgen. Hiermee wordt de rest van het programma uitgevoerd. Als er
+minder dan twee elementen op de stack staan kan deze regel niet worden
+toegepast, aangezien $\popop$ een partiële functie is.
+
$$
\begin{prooftree}
- hallo
+ \trans
+ {\pgm}{\ip}{(\stk'', \put\var\val\str)}
+ {\ip'}{\op}{\st}
+ \justifies
+ \trans
+ {\StmPut:\pgm}{\ip}{(\stk,\str)}
+ {\ip'}{\op}{\st}
+ \using{\rputns}
+ \qquad
+ \text{met\enspace
+ \parbox{36mm}{$(\var,\stk') = \pop{\stk}$,\\$(\val,\stk'') = \pop{\stk'}$.}
+ }
\end{prooftree}
$$
diff --git a/smurf.sty b/smurf.sty
index 6bc6fde..bd10d7e 100644
--- a/smurf.sty
+++ b/smurf.sty
@@ -10,7 +10,7 @@
\def\String{\mathit{String}}
\def\Char{\mathit{Char}}
-% Stacks
+% Stack
\def\Stack#1{\mathbf{Stack}\left[\mathit{#1}\right]}
\def\Nil{\texttt{Nil}}
\def\pushop{\mathit{push}}
@@ -18,6 +18,10 @@
\def\push#1#2{\pushop\left(#1, #2\right)}
\def\pop#1{\popop\left(#1\right)}
+% Store
+\def\putop{\mathit{put}}
+\def\put#1#2#3{\putop\left(#1, #2, #3\right)}
+
% Syntax
\def\SynPgm{\langle\Pgm\rangle}
\def\SynStm{\langle\Stm\rangle}
@@ -43,6 +47,7 @@
% Rules
\def\rule#1#2{[\mbox{#1}_{\mbox{\footnotesize{#2}}}]}
\def\rgetns{\rule{get}{ns}}
+\def\rputns{\rule{put}{ns}}
% Common names
\def\stk{\mathit{stk}}
@@ -53,4 +58,5 @@
\def\stm{\mathit{stm}}
\def\st{\mathit{st}}
\def\var{\mathit{var}}
+\def\val{\mathit{val}}