Appendix met regels

15 files changed, 222 insertions, 174 deletions

diff --git a/app-rules.tex b/app-rules.tex
new file mode 100644
index 0000000..2503c64
--- /dev/null
+++ b/app-rules.tex
@@ -0,0 +1,30 @@
+% vim: set spelllang=nl:
+\newgeometry{left=25mm,right=25mm}
+\section{Semantiekregels}
+\label{sec:app:rules}
+
+Een overzicht van de gedefinieerde regels voor de natuurlijke semantiek van
+Smurf:
+
+\FrameSep0pt
+\begin{framed}
+	\printrulefalse
+	\setlength{\extrarowheight}{20pt}
+	\begin{tabular}{l l}
+		$\rlambdans$  & \therlambdans{} \\
+		$\rcatns$     & \thercatns{} \\
+		$\rexecns$    & \therexecns{} \\
+		$\rgetns$     & \thergetns{} \\
+		$\rheadns$    & \therheadns{} \\
+		$\rinputns$   & \therinputns{} \\
+		$\routputns$  & \theroutputns{} \\
+		$\rpushns$    & \therpushns{} \\
+		$\rputns$     & \therputns{} \\
+		$\rquotifyns$ & \therquotifyns{} \\
+		$\rtailns$    & \thertailns{} \\
+	\end{tabular}
+	\vspace{1cm}
+	\printruletrue
+\end{framed}
+
+\restoregeometry
diff --git a/rule-defs.tex b/rule-defs.tex
new file mode 100644
index 0000000..d77cff8
--- /dev/null
+++ b/rule-defs.tex
@@ -0,0 +1,167 @@
+\newif\ifprintrule
+\printruletrue
+
+\long\def\printrule#1#2#3{$$
+	\begin{prooftree}
+		#1
+		\ifprintrule
+			\using#2
+		\else
+			\using{}
+		\fi
+		\qquad\text{#3}
+	\end{prooftree}
+$$}
+
+\def\rcatnstree{
+	\trans
+		{\pgm}{\ip}{(\push{s_1~s_2}{\stk''}, \str)}
+		{\ip'}{\op}{\st}
+	\justifies
+	\trans
+		{\StmCat:\pgm}{\ip}{(\stk,\str)}
+		{\ip'}{\op}{\st}
+}
+
+\long\def\thercatns{
+	\printrule\rcatnstree\rcatns{met\enspace
+	\parbox{36mm}{$\pop{\stk} = (s_2,\stk') $,\\$ \pop{\stk'} = (s_1,\stk'')$.}}
+}
+
+\def\rexecnstree{
+	\trans
+		{\pgm'}{\ip}{(\Nil, \emptystore)}
+		{\ip'}{\op}{\st}
+	\justifies
+	\trans
+		{\StmExec:\pgm}{\ip}{(\stk,\str)}
+		{\ip'}{\op}{\st}
+}
+
+\long\def\therexecns{
+	\printrule\rexecnstree\rexecns{met\enspace
+		\parbox{36mm}{$ \pop{\stk} =(\var,\stk')$,\\
+			$\pgm' = \parsepgm{\var'}$.}
+	}
+}
+
+\def\rgetnstree{
+	\trans
+		{\pgm}{\ip}{(\push{\str~\var}{\stk'}, \str)}
+		{\ip'}{\op}{\st}
+	\justifies
+	\trans
+		{\StmGet:\pgm}{\ip}{(\stk,\str)}
+		{\ip'}{\op}{\st}
+}
+
+\long\def\thergetns{
+	\printrule\rgetnstree\rgetns{met $\pop{\stk}= (\var,\stk')$.}
+}
+
+\def\rheadnstree{
+	\trans
+		{\pgm}{\ip}{(\push{c}{\stk'}, \str)}
+		{\ip'}{\op}{\st}
+	\justifies
+	\trans
+		{\StmHead:\pgm}{\ip}{(\stk,\str)}
+		{\ip'}{\op}{\st}
+}
+
+\long\def\therheadns{
+	\printrule\rheadnstree\rheadns{met $\pop{\stk} = (c~s,\stk')$.}
+}
+
+\def\rinputnstree{
+	\trans
+		{\pgm}{\ip'}{(\push\val\stk, \str)}
+		{\ip''}{\op}{\st}
+	\justifies
+	\trans
+		{\StmInput:\pgm}{\ip}{(\stk,\str)}
+		{\ip''}{\op}{\st}
+}
+
+\long\def\therinputns{
+	\printrule\rinputnstree\rinputns{met $\pop\ip = (\val,\ip')$.}
+}
+
+\def\rlambdanstree{
+	\axjustifies
+	\trans
+		{\lambda}{\ip}{\st}
+		{\ip}{\Nil}{\st}
+}
+
+\long\def\therlambdans{\printrule\rlambdanstree\rlambdans{}}
+
+\def\routputnstree{
+	\trans
+		{\pgm}{\ip}{(\stk',\str)}
+		{\ip'}{\op}{\st}
+	\justifies
+	\trans
+		{\StmOutput:\pgm}{\ip}{(\stk,\str)}
+		{\ip'}{\push{s}{\op}}{\st}
+}
+
+\long\def\theroutputns{
+	\printrule\routputnstree\routputns{met $\pop{\stk} = (s,\stk') $,}
+}
+
+\def\rpushnstree{
+	\trans
+		{\pgm}{\ip}{(\push{s}{\stk}), \str)}
+		{\ip'}{\op}{\st}
+	\justifies
+	\trans
+		{\StmPush~s:\pgm}{\ip}{(\stk,\str)}
+		{\ip'}{\op}{\st}
+}
+
+\long\def\therpushns{\printrule\rpushnstree\rpushns{}}
+
+\def\rputnstree{
+	\trans
+		{\pgm}{\ip}{(\stk'', \put\var\val\str)}
+		{\ip'}{\op}{\st}
+	\justifies
+	\trans
+		{\StmPut:\pgm}{\ip}{(\stk,\str)}
+		{\ip'}{\op}{\st}
+}
+
+\long\def\therputns{
+	\printrule\rputnstree\rputns{met\enspace
+		\parbox{36mm}{$\pop{\stk} = (\var,\stk')$,
+		\\$\pop{\stk'}= (\val,\stk'')$.}}
+}
+
+\def\rquotifynstree{
+	\trans
+		{\pgm}{\ip}{(\push{\texttt{"}\escape{s}\texttt{"}}{\stk'}, \str) }
+		{\ip'}{\op}{\st}
+	\justifies
+	\trans
+		{\StmQuotify:\pgm}{\ip}{(\stk,\str)}
+		{\ip'}{\op}{\st}
+}
+
+\long\def\therquotifyns{
+	\printrule\rquotifynstree\rquotifyns{met $\pop{\stk} = (s, stk')$.}
+}
+
+\def\rtailnstree{
+	\trans
+		{\pgm}{\ip}{(\push{s}{\stk'}, \str)}
+		{\ip'}{\op}{\st}
+	\justifies
+	\trans
+		{\StmTail:\pgm}{\ip}{(\stk,\str)}
+		{\ip'}{\op}{\st}
+}
+
+\long\def\thertailns{
+	\printrule\rtailnstree\rtailns{met $ \pop{\stk} = (c~s,\stk') $.}
+}
diff --git a/rules.tex b/rules.tex
index b4f8fd9..a82e3a7 100644
--- a/rules.tex
+++ b/rules.tex
@@ -1,5 +1,5 @@
 % vim: set spelllang=nl:
-\section{Regels} %todo working title
+\section{Regels in de natuurlijke semantiek}
 \label{sec:rules}
 
 We zullen nu ieder syntaxelement nader specificeren. Ook zullen regels voor de
@@ -16,6 +16,12 @@ maken (in tegenstelling tot bijvoorbeeld een errorstatus aan de rechterkant van
 transities toe te voegen), omdat dit het redeneren over Smurfprogramma's
 makkelijker zal maken.
 
+Hieronder worden de regels gedefinieerd en beargumenteerd. We zullen eerst
+regels bekijken die de stack manipuleren. Daarna laten we de regels die de
+variable store gebruiken zien. Vervolgens bekijken we regels die input en
+output gebruiken. We sluiten af met de regel voor $\StmExec$. In
+\autoref{sec:app:rules} is een alfabetisch overzicht van de regels te vinden.
+
 \input{ruleslambda}
 \input{rulespush}
 \input{ruleshead}
@@ -27,4 +33,3 @@ makkelijker zal maken.
 \input{rulesinput}
 \input{rulesoutput}
 \input{rulesexec}
-
diff --git a/rulescat.tex b/rulescat.tex
index f36f0ec..863ba96 100644
--- a/rulescat.tex
+++ b/rulescat.tex
@@ -12,20 +12,4 @@ 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{s_1~s_2}{\stk''}, \str)}
-		{\ip'}{\op}{\st}
-	\justifies
-	\trans
-		{\StmCat:\pgm}{\ip}{(\stk,\str)}
-		{\ip'}{\op}{\st}
-	\using{\rcatns}
-	\qquad
-	\text{met\enspace
-	\parbox{36mm}{$\pop{\stk} = (s_2,\stk') $,\\$ \pop{\stk'} = (s_1,\stk'')$.}}
-\end{prooftree}
-$$
-
+\thercatns
diff --git a/rulesexec.tex b/rulesexec.tex
index 9f4a60a..0ac3e10 100644
--- a/rulesexec.tex
+++ b/rulesexec.tex
@@ -13,24 +13,7 @@ het nieuwe programma om uitgevoerd te worden.  Als de $\stk$ leeg is is deze
 regel niet toepasbaar, omdat $\pop\stk$ dan niet gedefinieerd is. Ook is deze
 regel niet toepasbaar als de gepopte string zelf geen geldig Smurf-programma
 is, omdat $\parsepgmop$ dan niet gedefinieerd is.
-
-$$
-\begin{prooftree}
-	\trans
-		{\pgm'}{\ip}{(\Nil, \emptystore)}
-		{\ip'}{\op}{\st}
-	\justifies
-	\trans
-		{\StmExec:\pgm}{\ip}{(\stk,\str)}
-		{\ip'}{\op}{\st}
-	\using{\rexecns}
-	\qquad
-	\text{met\enspace
-		\parbox{36mm}{$ \pop{\stk} =(\var,\stk')$,\\
-			$\pgm' = \parsepgm{\var'}$.}
-	}
-\end{prooftree}
-$$
+\therexecns%
 
 \medskip
 $\parsepgmop$ definiëren we als volgt, met een hulpfunctie $\parsestrop$:
diff --git a/rulesget.tex b/rulesget.tex
index 44daa5f..ac0464a 100644
--- a/rulesget.tex
+++ b/rulesget.tex
@@ -8,19 +8,5 @@
 \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. 
-$$
-\begin{prooftree}
-	\trans
-		{\pgm}{\ip}{(\push{\str~\var}{\stk'}, \str)}
-		{\ip'}{\op}{\st}
-	\justifies
-	\trans
-		{\StmGet:\pgm}{\ip}{(\stk,\str)}
-		{\ip'}{\op}{\st}
-	\using{\rgetns}
-	\qquad
-	\text{met $\pop{\stk}= (\var,\stk')$.}
-\end{prooftree}
-$$
-
+is $\pop\stk$ niet gedefinieerd en kunnen we de regel dus niet toepassen.
+\thergetns%
diff --git a/ruleshead.tex b/ruleshead.tex
index ba3d99a..3931619 100644
--- a/ruleshead.tex
+++ b/ruleshead.tex
@@ -12,19 +12,4 @@ afleidingsboom kunnen maken wanneer $\StmHead$ wordt uitgevoerd op het moment
 dat het element bovenop de stack de lege string is.
 
 Dit geeft de volgende regel:
-
-$$
-\begin{prooftree}
-	\trans
-		{\pgm}{\ip}{(\push{c}{\stk'}, \str)}
-		{\ip'}{\op}{\st}
-	\justifies
-	\trans
-		{\StmHead:\pgm}{\ip}{(\stk,\str)}
-		{\ip'}{\op}{\st}
-	\using{\rheadns}
-	\qquad
-	\text{met $\pop{\stk} = (c~s,\stk')$.}
-\end{prooftree}
-$$
-
+\therheadns%
diff --git a/rulesinput.tex b/rulesinput.tex
index 9d8985c..004c764 100644
--- a/rulesinput.tex
+++ b/rulesinput.tex
@@ -25,19 +25,4 @@ gedefinieerd is. Geeft de gebruiker niet genoeg input, dan hoeven we dus geen
 afleidingsboom te maken (en we zullen dit ook onmogelijk maken).
 
 Dit geeft de volgende regel:
-
-$$
-\begin{prooftree}
-	\trans
-		{\pgm}{\ip'}{(\push\val\stk, \str)}
-		{\ip''}{\op}{\st}
-	\justifies
-	\trans
-		{\StmInput:\pgm}{\ip}{(\stk,\str)}
-		{\ip''}{\op}{\st}
-	\using{\rinputns}
-	\qquad
-	\text{met $\pop\ip = (\val,\ip')$.}
-\end{prooftree}
-$$
-
+\therinputns%
diff --git a/ruleslambda.tex b/ruleslambda.tex
index 5612872..161fa2b 100644
--- a/ruleslambda.tex
+++ b/ruleslambda.tex
@@ -5,14 +5,4 @@
 We hebben één axioma nodig om het basisgeval van het lege programma af te
 handelen. Deze regel geeft aan dat het lege programma niets doet: het gebruikt
 geen input, geeft geen output, en verandert de state niet.
-
-$$
-\begin{prooftree}
-	\axjustifies
-	\trans
-		{\lambda}{\ip}{\st}
-		{\ip}{\Nil}{\st}
-	\using{\rlambdans}
-\end{prooftree}
-$$
-
+\therlambdans%
diff --git a/rulesoutput.tex b/rulesoutput.tex
index d4bb487..257be28 100644
--- a/rulesoutput.tex
+++ b/rulesoutput.tex
@@ -10,24 +10,9 @@ We houden gedurende het hele programma een stack van strings, genaamd $\Output$
 bij waar het programma zijn output naar wegschrijft.
 
 Dit geeft de volgende regel:
-
-$$
-\prooftree
-        \trans
-        {\pgm}{\ip}{(\stk',\str)}
-        	{\ip'}{\op}{\st}
-	\justifies
-        \trans
-        {\StmOutput:\pgm}{\ip}{(\stk,\str)}
-            {\ip'}{\push{s}{\op}}{\st}
-	\using{\routputns}
-	\qquad
-	\text{met $\pop{\stk} = (s,\stk') $,}
-\endprooftree
-$$
+\theroutputns%
 
 waarbij $\op$ in de bovenste regel de gehele outputstack weergeeft. Merk op
 dat eenzelfde regel waar $s$ niet voor op de stack wordt gezet maar achter,
 even geldig is. Geen van beide opties is beter dan de ander omdat we geen
 aannames doen over hoe de $\Output$-stack wordt verwerkt.
-
diff --git a/rulespush.tex b/rulespush.tex
index 324601e..21f332d 100644
--- a/rulespush.tex
+++ b/rulespush.tex
@@ -17,19 +17,7 @@ zoals het commentaar op de specificatie~\cite{safalra} aangeeft, niet
 gedefinieerd wat er met ongeldige escape sequences gebeurt.
 
 Dit geeft de volgende regel:
-
-$$
-\begin{prooftree}
-	\trans
-		{\pgm}{\ip}{(\push{s}{\stk}), \str)}
-		{\ip'}{\op}{\st}
-	\justifies
-	\trans
-		{\StmPush~s:\pgm}{\ip}{(\stk,\str)}
-		{\ip'}{\op}{\st}
-	\using{\rpushns}
-\end{prooftree}
-$$
+\therpushns%
 
 De definitie van $\unescapeop$ is als volgt:
 
@@ -54,4 +42,3 @@ het commentaar op de specificatie en met de Perl interpreter: %todo referentie
 	should not rely on this behaviour and should always ensure valid escape
 	sequences are used.
 \end{quote}
- 
diff --git a/rulesput.tex b/rulesput.tex
index 3a8fd05..371cae6 100644
--- a/rulesput.tex
+++ b/rulesput.tex
@@ -11,21 +11,4 @@ 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}
-	\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}{$\pop{\stk} = (\var,\stk')$,
-		\\$\pop{\stk'}= (\val,\stk'')$.}}
-\end{prooftree}
-$$
-
+\therputns%
diff --git a/rulesquotify.tex b/rulesquotify.tex
index 8ebe567..27c34a3 100644
--- a/rulesquotify.tex
+++ b/rulesquotify.tex
@@ -15,26 +15,13 @@ wordt hier een \verb$\$ voor geplaatst. Hiervoor gebruiken we de hulpfunctie
 $\escapeop$.
 
 Dit geeft de volgende regel:
-$$
-\begin{prooftree}
-	\trans
-		{\pgm}{\ip}{(\push{\texttt{"}\escape{s}\texttt{"}}{\stk'}, \str) }
-		{\ip'}{\op}{\st}
-	\justifies
-	\trans
-		{\StmQuotify:\pgm}{\ip}{(\stk,\str)}
-		{\ip'}{\op}{\st}
-	\using{\rquotifyns}
-	\qquad
-	\text{met $\pop{\stk} = (s, stk')$.}
-\end{prooftree}
-$$
+\therquotifyns%
 
 $$
 	\escape{c~s} =
 		\begin{cases}
 			\texttt{\textbackslash}~c~\escape{s} & \text{als
 				$c\in\{\texttt{"},\texttt{\textbackslash},\text{het LF-karakter}\}$} \\
-			c~\escape{s}                & \text{anderszins}
+			c~\escape{s} & \text{anderszins}
 		\end{cases}
 $$
diff --git a/rulestail.tex b/rulestail.tex
index dc93a3b..8ed1c58 100644
--- a/rulestail.tex
+++ b/rulestail.tex
@@ -11,18 +11,4 @@ afleidingsboom kunnen maken wanneer $\StmTail$ wordt uitgevoerd op het moment
 dat het element bovenop de stack de lege string is.
 
 Dit geeft de volgende regel:
-
-$$
-\begin{prooftree}
-	\trans
-		{\pgm}{\ip}{(\push{s}{\stk'}, \str)}
-		{\ip'}{\op}{\st}
-	\justifies
-	\trans
-		{\StmTail:\pgm}{\ip}{(\stk,\str)}
-		{\ip'}{\op}{\st}
-	\using{\rtailns}
-	\qquad
-	\text{met $ \pop{\stk} = (c~s,\stk') $.}
-\end{prooftree}
-$$
\ No newline at end of file
+\thertailns%
diff --git a/werkstuk.tex b/werkstuk.tex
index 5920a4c..eafa592 100644
--- a/werkstuk.tex
+++ b/werkstuk.tex
@@ -19,12 +19,15 @@
 \usepackage{stackrel}
 \usepackage{syntax}
 \usepackage{thmtools}
+\usepackage{framed}
+\usepackage{array}
 
 \usepackage{clean}
 \lstset{language=Clean,breaklines,tabsize=2,xleftmargin=\parindent}
 
 % Eigen packages
 \usepackage{smurf}
+\input{rule-defs}
 
 % Settings, fixes
 \setlist{itemsep=0pt}
@@ -56,7 +59,9 @@
 \input{analyse}
 \input{refs}
 
+\clearpage
 \appendix
+\input{app-rules.tex}
 \input{app-trees.tex}
 
 \end{document}