% vim: set spelllang=nl:
\subsection{Input en output}
\label{sec:def:io}

Allereerst definiëren we het type $\Stack{a}$, omdat stacks we veel met stacks
doen in onze semantiek regels. Een $\Stack{a}$ (lees: een stack van elementen
van type $a$) is een simpel datatype met de volgende syntax:

\def\inbrackets#1{$\mathrm{[}#1\mathrm{]}$}
\def\bracka{\inbrackets{a}}
\begin{grammar}
	<Stack \bracka> ::= [<a>:<Stack \bracka>] | \Nil
\end{grammar}

Op een stack zijn twee instructies gedefinieerd:
\begin{gather*}
	\pushop : a \times \Stack{a} \to \Stack{a} \\
	\push{e}{\stk} \isdef [e:\stk] \\[1em]
	\popop : \Stack{a} \hookrightarrow a \times \Stack{a} \\
	\pop{[e:\stk]} \isdef (e,\stk) \\
\end{gather*}

$\popop$ is een partiële functie omdat $\pop\Nil$ niet gebruikt mag worden in
onze semantiekregels. %todo waarom niet?

\medskip
We zullen de input en output beide als $\Stack{\String}$ modelleren. In feite
zal zelfs blijken dat we op $\Input$ de operatie $\pushop$ niet nodig hebben,
en op $\Output$ de operatie $\popop$ niet zullen gebruiken. Informeel
beschouwen we $\Input$ als een `bron' van $\String$s en $\Output$ als een `put'
van $\String$s. Formeel:
\begin{align*}
	\Input &\isdef \Stack{\String} \\ \Output &\isdef \Stack{\String}
\end{align*}