diff options
| -rw-r--r-- | rulesexec.tex | 59 | ||||
| -rw-r--r-- | smurf.sty | 8 |
2 files changed, 67 insertions, 0 deletions
diff --git a/rulesexec.tex b/rulesexec.tex new file mode 100644 index 0000000..b4f5d1a --- /dev/null +++ b/rulesexec.tex @@ -0,0 +1,59 @@ +% vim: set spelllang=nl: +\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. +\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. + +$$ +\begin{prooftree} + \trans + {\pgm'}{\ip}{(\Nil, \str')} + {\ip'}{\op}{\st} + \justifies + \trans + {\StmExec:\pgm}{\ip}{(\stk,\str)} + {\ip'}{\op}{\st} + \using{\rexecns} + \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 + } + } +\end{prooftree} +$$ + +$\parsepgmop$ definiëren we als volgt, met 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`}\\ + \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. +$$ + \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$}\\ + \end{cases} +$$ +Het tweede geval van $\parsestrop$ zorgt ervoor dat ge-escapete aanhalingstekens de string niet beëindigen. + @@ -1,6 +1,12 @@ % General \def\isdef{\stackrel{\text{def}}{=}} +\def\parsepgmop{\mathit{Parse}} +\def\parsepgm#1{\parsepgmop\left(#1\right)} + +\def\parsestrop{\mathit{ParseStr}} +\def\parsestr#1{\parsestrop\left(#1\right)} + % Types \def\Pgm{\mathit{Pgm}} \def\Stm{\mathit{Stm}} @@ -18,6 +24,7 @@ \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)} @@ -48,6 +55,7 @@ \def\rule#1#2{[\mbox{#1}_{\mbox{\footnotesize{#2}}}]} \def\rgetns{\rule{get}{ns}} \def\rputns{\rule{put}{ns}} +\def\rexecns{\rule{exec}{ns}} % Common names \def\stk{\mathit{stk}} |