+ \subsubsection{Example}
+ As an example of the used approach, there is a simple averaging circuit in
+ \in{example}[ex:AvgState]. This circuit lets the accumulation of the
+ inputs be done by a subcomponent, \hs{acc}, but keeps a count of value
+ accumulated in its own state.\footnote{Currently, the prototype
+ is not able to compile this example, since the built-in function
+ for division has not been added.}
+
+ \startbuffer[AvgState]
+ -- The state type annotation
+ newtype State s = State s
+
+ -- The accumulator state type
+ type AccState = State Word
+ -- The accumulator
+ acc :: Word -> AccState -> (AccState, Word)
+ acc i (State s) = let sum = s + i in (State sum, sum)
+
+ -- The averaging circuit state type
+ type AvgState = State (AccState, Word)
+ -- The averaging circuit
+ avg :: Word -> AvgState -> (AvgState, Word)
+ avg i (State s) = (State s', o)
+ where
+ (accs, count) = s
+ -- Pass our input through the accumulator, which outputs a sum
+ (accs', sum) = acc i accs
+ -- Increment the count (which will be our new state)
+ count' = count + 1
+ -- Compute the average
+ o = sum / count'
+ s' = (accs', count')
+ \stopbuffer
+
+ \placeexample[here][ex:AvgState]{Simple stateful averaging circuit.}
+ %\startcombination[2*1]
+ {\typebufferhs{AvgState}}%{Haskell description using function applications.}
+ % {\boxedgraphic{AvgState}}{The architecture described by the Haskell description.}
+ %\stopcombination
+ \todo{Picture}
+
+ \section{Implementing state}
+ Now its clear how to put state annotations in the Haskell source,
+ there is the question of how to implement this state translation. As
+ we have seen in \in{section}[sec:prototype:design], the translation to
+ \VHDL\ happens as a simple, final step in the compilation process.
+ This step works on a core expression in normal form. The specifics
+ of normal form will be explained in
+ \in{chapter}[chap:normalization], but the examples given should be
+ easy to understand using the definitin of Core given above.
+
+ \startbuffer[AvgStateNormal]
+ acc = λi.λspacked.
+ let
+ -- Remove the State newtype
+ s = spacked ▶ Word
+ s' = s + i
+ o = s + i
+ -- Add the State newtype again
+ spacked' = s' ▶ State Word
+ res = (spacked', o)
+ in
+ res
+
+ avg = λi.λspacked.
+ let
+ s = spacked ▶ (AccState, Word)
+ accs = case s of (accs, _) -> accs
+ count = case s of (_, count) -> count
+ accres = acc i accs
+ accs' = case accres of (accs', _) -> accs'
+ sum = case accres of (_, sum) -> sum
+ count' = count + 1
+ o = sum / count'
+ s' = (accs', count')
+ spacked' = s' ▶ State (AccState, Word)
+ res = (spacked', o)
+ in
+ res
+ \stopbuffer
+
+ \placeexample[here][ex:AvgStateNormal]{Normalized version of \in{example}[ex:AvgState]}
+ {\typebufferlam{AvgStateNormal}}
+
+ \subsection[sec:prototype:statelimits]{State in normal form}
+ Before describing how to translate state from normal form to
+ \VHDL, we will first see how state handling looks in normal form.
+ What limitations are there on their use to guarantee that proper
+ \VHDL\ can be generated?
+
+ We will try to formulate a number of rules about what operations are
+ allowed with state variables. These rules apply to the normalized Core
+ representation, but will in practice apply to the original Haskell
+ hardware description as well. Ideally, these rules would become part
+ of the intended normal form definition \refdef{intended normal form
+ definition}, but this is not the case right now. This can cause some
+ problems, which are detailed in
+ \in{section}[sec:normalization:stateproblems].
+
+ In these rules we use the terms \emph{state variable} to refer to any
+ variable that has a \lam{State} type. A \emph{state-containing
+ variable} is any variable whose type contains a \lam{State} type,
+ but is not one itself (like \lam{(AccState, Word)} in the example,
+ which is a tuple type, but contains \lam{AccState}, which is again
+ equal to \lam{State Word}).
+
+ We also use a distinction between \emph{input} and \emph{output
+ (state) variables} and \emph{substate variables}, which will be
+ defined in the rules themselves.
+
+ \startdesc{State variables can appear as an argument.}
+ \startlambda
+ avg = λi.λspacked. ...
+ \stoplambda