summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--rules.tex6
-rw-r--r--rulescat.tex25
-rw-r--r--rulesquotify.tex28
-rw-r--r--smurf.sty8
4 files changed, 44 insertions, 23 deletions
diff --git a/rules.tex b/rules.tex
index 8b01508..1fee1d4 100644
--- a/rules.tex
+++ b/rules.tex
@@ -13,11 +13,11 @@ de rechterkant van transities toe te voegen), omdat dit het redeneren over
Smurfprogramma's makkelijker zal maken.
\input{ruleslambda}
-%\input{rulespush}
+\input{rulespush}
\input{ruleshead}
\input{rulestail}
-%\input{rulesquotify}
-%\input{rulescat}
+\input{rulesquotify}
+\input{rulescat}
\input{rulesget}
\input{rulesput}
\input{rulesinput}
diff --git a/rulescat.tex b/rulescat.tex
index d05e0e5..a54b508 100644
--- a/rulescat.tex
+++ b/rulescat.tex
@@ -4,12 +4,29 @@
\begin{quote}
+ - concatenates the top two strings on the stack. The string pushed earlier
- appears earlier in the resulting string, eg
- "Zork" "mid" +
- would result in the string "Zorkmid" being placed on the stack.
+ appears earlier in the resulting string, eg \smurfinline{"Zork" "mid" +}
+ would result in the string \texttt{Zorkmid} being placed on the stack.
\end{quote}
-De twee strings die als laatste op de stack zijn gezet worden dus samen gevoegd en terug op de stack gezet.
+De string bovenop de stack wordt toegevoegd aan de string hieronder. Het
+resultaat wordt op de stack gezet.
Dit geeft de volgende regel:
+$$
+\begin{prooftree}
+ \trans
+ {\pgm}{\ip}{(\push{s1~s2}{\stk''}, \str)}
+ {\ip'}{\op}{\st}
+ \justifies
+ \trans
+ {\StmCat:\pgm}{\ip}{(\stk,\str)}
+ {\ip'}{\op}{\st}
+ \using{\rcatns}
+ \qquad
+ \text{met\enspace
+ \parbox{36mm}{$(s_2,\stk') = \pop{\stk}$,\\$(s_1,\stk'') = \pop{\stk'}$.}
+ }
+\end{prooftree}
+$$
+
diff --git a/rulesquotify.tex b/rulesquotify.tex
index 0c0f09c..d218fd6 100644
--- a/rulesquotify.tex
+++ b/rulesquotify.tex
@@ -3,22 +3,22 @@
\label{sec:rules:quotify}
\begin{quote}
-q - "Quotifies" the string on top of the stack, so that it can be placed
- into a Smurf program as a literal string, eg
- Arthur "two-sheds" Jackson
- becomes
- "Arthur $\backslash$ "two-sheds $\backslash$ " Jackson"
+ q - "Quotifies" the string on top of the stack, so that it can be placed into
+ a Smurf program as a literal string, eg \texttt{Arthur "two-sheds" Jackson}
+ becomes \texttt{"Arthur $\backslash$"two-sheds$\backslash$" Jackson"}.
\end{quote}
-Er worden dus quotes om de string heen gezet. Als er in de oorspronkelijke string quotes stonden dan wordt voor iedere van deze quotes een "$\backslash$" geplaats.
-Om de backslashes te zetten word gebruik gemaakt van de hulpfunctie quo
+Er worden aanhalingstekens om de string bovenop de stack gezet. Als er in de
+oorspronkelijke string aanhalingstekens, backslashes of LF-karakters staan, dan
+wordt hier een \verb$\$ voor geplaatst. Hiervoor gebruiken we de hulpfunctie
+$\escapeop$.
Dit geeft de volgende regel:
$$
\begin{prooftree}
\trans
- {\pgm}{\ip}{(\push{"quo (c s)"}{\stk'}, \str) }
+ {\pgm}{\ip}{(\push{\texttt{"}\escape{s}\texttt{"}}{\stk'}, \str) }
{\ip}{\op}{\st}
\justifies
\trans
@@ -26,15 +26,15 @@ $$
{\ip}{\op}{\st}
\using{\rquotifyns}
\qquad
- \text{met (c s, stk') = pop (stk)
- }
+ \text{met $(s, stk') = \pop{\stk}$.}
\end{prooftree}
$$
$$
- \quo {c} {s} =
+ \escape{c~s} =
\begin{cases}
- \texttt{" c quo s} & \text{als $c=\texttt{"}$} \\
- \texttt{c quo s} & \text{anderszins}
+ \texttt{\textbackslash}~c~s & \text{als
+ $c\in\{\texttt{"},\texttt{\textbackslash},\text{het LF-karakter}\}$} \\
+ c~\escape{s} & \text{anderszins}
\end{cases}
-$$ \ No newline at end of file
+$$
diff --git a/smurf.sty b/smurf.sty
index 01d3d5b..8191582 100644
--- a/smurf.sty
+++ b/smurf.sty
@@ -11,8 +11,8 @@
\def\parsestr#1{\parsestrop\left(#1\right)}
\def\unescapeop{\mathit{unescape}}
\def\unescape#1{\unescapeop\left(#1\right)}
-\def\quo{\mathit{quo}}
-\def\quo#1{\quoop\left(#1\right)}
+\def\escapeop{\mathit{escape}}
+\def\escape#1{\escapeop\left(#1\right)}
% Types
\def\Pgm{\mathit{Pgm}}
@@ -61,7 +61,11 @@
% Rules
\def\rule#1#2{[\mbox{#1}_{\mbox{\footnotesize{#2}}}]}
\def\rlambdans{\rule{$\lambda$}{ns}}
+\def\rpushns{\rule{push}{ns}}
\def\rheadns{\rule{head}{ns}}
+\def\rtailns{\rule{tail}{ns}}
+\def\rquotifyns{\rule{quotify}{ns}}
+\def\rcatns{\rule{cat}{ns}}
\def\rgetns{\rule{get}{ns}}
\def\rputns{\rule{put}{ns}}
\def\rinputns{\rule{input}{ns}}