% 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} ::= [:] | \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*}