From a69989b9a23856c1962a14dd4ae11a3bd63645a7 Mon Sep 17 00:00:00 2001
From: Camil Staps
Date: Thu, 28 Apr 2016 15:52:22 +0200
Subject: Head regel

---
 rules.tex     |  2 +-
 ruleshead.tex | 29 +++++++++++++++++++++++++++++
 smurf.sty     |  1 +
 3 files changed, 31 insertions(+), 1 deletion(-)
 create mode 100644 ruleshead.tex

diff --git a/rules.tex b/rules.tex
index 03a274e..b6acb25 100644
--- a/rules.tex
+++ b/rules.tex
@@ -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}
+$$
+
diff --git a/smurf.sty b/smurf.sty
index 0bf2f53..78d1bbd 100644
--- a/smurf.sty
+++ b/smurf.sty
@@ -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}}
-- 
cgit v1.2.3