diff options
| -rw-r--r-- | rules.tex | 2 | ||||
| -rw-r--r-- | ruleshead.tex | 29 | ||||
| -rw-r--r-- | smurf.sty | 1 |
3 files changed, 31 insertions, 1 deletions
@@ -13,7 +13,7 @@ de rechterkant van transities toe te voegen), omdat dit het redeneren over Smurfprogramma's makkelijker zal maken. %\input{rulespush} -%\input{ruleshead} +\input{ruleshead} %\input{rulestail} %\input{rulesquotify} %\input{rulescat} diff --git a/ruleshead.tex b/ruleshead.tex new file mode 100644 index 0000000..70d15ab --- /dev/null +++ b/ruleshead.tex @@ -0,0 +1,29 @@ +% vim: set spelllang=nl: +\subsection{\texttt{Head}} + +\begin{quote} + h - Pops a string from the stack, and pushes its head, ie the first + character. This causes an error if used on the empty string. +\end{quote} + +In plaats van het geven van een error kiezen we ervoor te voorkomen dat we een +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{s}{\stk'}, \str)} + {\ip'}{\op}{\st} + \justifies + \trans + {\StmHead:\pgm}{\ip}{(\stk,\str)} + {\ip'}{\op}{\st} + \using{\rheadns} + \qquad + \text{met $(c~s,\stk') = \pop{\stk}$.} +\end{prooftree} +$$ + @@ -57,6 +57,7 @@ % Rules \def\rule#1#2{[\mbox{#1}_{\mbox{\footnotesize{#2}}}]} +\def\rheadns{\rule{head}{ns}} \def\rgetns{\rule{get}{ns}} \def\rputns{\rule{put}{ns}} \def\rinputns{\rule{input}{ns}} |