Inspringing, overbodige met, emptystore, babel fix

1 files changed, 36 insertions, 24 deletions

diff --git a/rulesexec.tex b/rulesexec.tex
index b4f5d1a..25db4d6 100644
--- a/rulesexec.tex
+++ b/rulesexec.tex
@@ -2,15 +2,20 @@
 \subsection{\texttt{Exec}}
 
 \begin{quote}
-	x - Executes the string at the top of the stack as a Smurf program. The stack and variable store are erased.
+	x - Executes the string at the top of the stack as a Smurf program. The stack
+	and variable store are erased.
 \end{quote}
 
-We halen een strings van de stack en gebruiken $\parsepgmop$ om dit in een programma om te zetten. Dit wordt 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.
+We halen een string van de stack en gebruiken $\parsepgmop$ om dit in een
+programma om te zetten. Dit wordt 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, \str')}
+		{\pgm'}{\ip}{(\Nil, \emptystore)}
 		{\ip'}{\op}{\st}
 	\justifies
 	\trans
@@ -20,40 +25,47 @@ $$
 	\qquad
 	\text{met\enspace
 		\parbox{36mm}{$(\var,\stk') = \pop{\stk}$,\\
-        $\pgm' = \parsepgm{\var'}$\\
-        $\str'~k = \lambda\forall k \in\String$.%tab tussen lambda en forall misschien mooier
-        }
+			$\pgm' = \parsepgm{\var'}$.}
 	}
 \end{prooftree}
 $$
 
-$\parsepgmop$ definiëren we als volgt, met hulpfunctie $\parsestrop$:
+\medskip
+$\parsepgmop$ definiëren we als volgt, met een hulpfunctie $\parsestrop$:
 
 $$
 	\parsepgm s =
 		\begin{cases}
-			\lambda & \text{als $s=\lambda$}\\
-            \parsepgm{s'} & \text{als $s=cs'$ met $c=$` `}\\
-            \parsestr{s'} & \text{als $s=cs'$ met $c=$`''`}\\
-            \StmCat:\parsepgm{s'} & \text{als $s=cs'$ met $c=$`+`}\\
-            \StmHead:\parsepgm{s'} & \text{als $s=cs'$ met $c=$`h`}\\
-            \StmTail:\parsepgm{s'} & \text{als $s=cs'$ met $c=$`t`}\\
-            \StmQuotify:\parsepgm{s'} & \text{als $s=cs'$ met $c=$`q`}\\
-            \StmPut:\parsepgm{s'} & \text{als $s=cs'$ met $c=$`p`}\\
-            \StmGet:\parsepgm{s'} & \text{als $s=cs'$ met $c=$`g`}\\
-            \StmInput:\parsepgm{s'} & \text{als $s=cs'$ met $c=$`i`}\\
-            \StmOutput:\parsepgm{s'} & \text{als $s=cs'$ met $c=$`o`}\\
-			\StmExec:\parsepgm{s'} & \text{als $s=cs'$ met $c=$`x`}\\
+			\lambda                   & \text{als $s=\lambda$}\\
+			\parsepgm{s'}             & \text{als $s=c~s'$ met $c$ whitespace}\\
+			\parsestr{s'}             & \text{als $s=\texttt{"}~s'$} \\
+			\StmCat:\parsepgm{s'}     & \text{als $s=\texttt{+}~s'$} \\
+			\StmHead:\parsepgm{s'}    & \text{als $s=\texttt{h}~s'$} \\
+			\StmTail:\parsepgm{s'}    & \text{als $s=\texttt{t}~s'$} \\
+			\StmQuotify:\parsepgm{s'} & \text{als $s=\texttt{q}~s'$} \\
+			\StmPut:\parsepgm{s'}     & \text{als $s=\texttt{p}~s'$} \\
+			\StmGet:\parsepgm{s'}     & \text{als $s=\texttt{g}~s'$} \\
+			\StmInput:\parsepgm{s'}   & \text{als $s=\texttt{i}~s'$} \\
+			\StmOutput:\parsepgm{s'}  & \text{als $s=\texttt{o}~s'$} \\
+			\StmExec:\parsepgm{s'}    & \text{als $s=\texttt{x}~s'$} \\
 		\end{cases}
 $$
-Het tweede geval van $\parsepgmop$ zorgt ervoor dat een programma-string spaties mag bevatten, die syntactisch zelf geen betekenis hebben. Dit is in overeenkomst met de specificatie, maar op zich niet nodig.
+
+Het tweede geval van $\parsepgmop$ zorgt ervoor dat een programma-string
+bijvoorbeeld spaties mag bevatten, die syntactisch zelf geen betekenis hebben.
+Dit is in overeenkomst met de specificatie, maar op zich niet nodig.
+
 $$
 	\parsestr s =
 		\begin{cases}
-			\lambda:\parsepgm{s'} & \text{als $s=cs'$ met $c=$'~'''}\\
-            `\backslash`~`''`~\parsestr{s'} & \text{als $s=cs'$ met $c=$`$\backslash$`~`''`}\\
-            c~\parsestr{s'} & \text{als $s=cs'$ met $c \in\Char$}\\
+			\lambda:\parsepgm{s'} & \text{als $s=\texttt{"}~s'$} \\
+			k~\parsestr{s'} & \text{als $s=\texttt{\textbackslash}~k~s'$ met
+				$k \in\Char$} \\
+			c~\parsestr{s'} & \text{als $s=c~s'$ met $c
+				\in\Char\setminus\{\texttt{"}\}$}\\
 		\end{cases}
 $$
-Het tweede geval van $\parsestrop$ zorgt ervoor dat ge-escapete aanhalingstekens de string niet beëindigen.
+
+Het tweede geval van $\parsestrop$ zorgt ervoor dat ge-escapete
+aanhalingstekens de string niet beëindigen.