+ \subsubsection{Example}
+ As an example of the used approach, a simple averaging circuit
+ is shown in \in{example}[ex:AvgState]. This circuit lets the
+ accumulation of the inputs be done by a sub-component, \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 there is no built-in function for division.}
+
+ \startbuffer[AvgState]
+ -- This type renaming would become part of Cλash, it is shown
+ -- here just for clarity
+ 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{\VHDL\ generation for 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 definition of Core given above. The
+ conversion to and from the \hs{State} type is done using the cast
+ operator, \lam{▶}.
+
+ \startbuffer[AvgStateNormal]
+ acc = λi.λspacked.
+ let
+ -- Remove the State newtype
+ s = spacked ▶ Word
+ sum = s + i
+ -- Add the State newtype again
+ spacked' = sum ▶ State Word
+ res = (spacked', sum)
+ in
+ res
+
+ avg = λi.λspacked.
+ let
+ s = spacked ▶ (AccState, Word)
+ accs = case s of (a, b) -> a
+ count = case s of (c, d) -> d
+ accres = acc i accs
+ accs' = case accres of (e, f) -> e
+ sum = case accres of (g, h) -> h
+ 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.
+ How must their use be limited to guarantee that proper \VHDL\ can
+ be generated?
+
+ We will 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{sub-state variables}, which will be
+ defined in the rules themselves.
+
+ These rules describe everything that can be done with state
+ variables and state-containing variables. Everything else is
+ invalid. For every rule, the corresponding part of
+ \in{example}[ex:AvgStateNormal] is shown.
+
+ \startdesc{State variables can appear as an argument.}
+ \startlambda
+ avg = λi.λspacked. ...
+ \stoplambda