+ As soon as all a functions own update state and output substate
+ variables have been joined together, the resulting
+ state-containing output variable can be packed into an output
+ state variable. Packing is done by casting into a state type.
+ \stopdesc
+
+ \startdesc{Output state variables can appear as (part of) a function result.}
+ \startlambda
+ avg = λi.λspacked.
+ let
+ \vdots
+ res = (spacked', o)
+ in
+ res
+ \stoplambda
+ When the output state is packed, it can be returned as a part
+ of the function result. Nothing else can be done with this
+ value (or any value that contains it).
+ \stopdesc
+
+ There is one final limitation that is hard to express in the above
+ itemization. Whenever substates are extracted from the input state
+ to be passed to functions, the corresponding output substates
+ should be inserted into the output state in the same way. In other
+ words, each pair of corresponding substates in the input and
+ output states should be passed / returned from the same called
+ function.
+
+ The prototype currently does not check much of the above
+ conditions. This means that if the conditions are violated,
+ sometimes a compile error is generated, but in other cases output
+ can be generated that is not valid \VHDL or at the very least does
+ not correspond to the input.
+
+ \subsection{Translating to \VHDL}
+ As noted above, the basic approach when generating \VHDL for stateful
+ functions is to generate a single register for every stateful function.
+ We look around the normal form to find the let binding that removes the
+ \lam{State} newtype (using a cast). We also find the let binding that
+ adds a \lam{State} type. These are connected to the output and the input
+ of the generated let binding respectively. This means that there can
+ only be one let binding that adds and one that removes the \lam{State}
+ type. It is easy to violate this constraint. This problem is detailed in
+ \in{section}[sec:normalization:stateproblems].
+
+ This approach seems simple enough, but will this also work for more
+ complex stateful functions involving substates? Observe that any
+ component of a function's state that is a substate, \ie passed on as
+ the state of another function, should have no influence on the
+ hardware generated for the calling function. Any state-specific
+ \small{VHDL} for this component can be generated entirely within the
+ called function. So, we can completely ignore substates when
+ generating \VHDL for a function.
+
+ From this observation, we might think to remove the substates from a
+ function's states alltogether, and leave only the state components
+ which are actual states of the current function. While doing this
+ would not remove any information needed to generate \small{VHDL} from
+ the function, it would cause the function definition to become invalid
+ (since we won't have any substate to pass to the functions anymore).
+ We could solve the syntactic problems by passing \type{undefined} for
+ state variables, but that would still break the code on the semantic
+ level (\ie, the function would no longer be semantically equivalent to
+ the original input).
+
+ To keep the function definition correct until the very end of the
+ process, we will not deal with (sub)states until we get to the
+ \small{VHDL} generation. Then, we are translating from Core to
+ \small{VHDL}, and we can simply ignore substates, effectively removing
+ the substate components alltogether.
+
+ But, how will we know what exactly is a substate? Since any state
+ argument or return value that represents state must be of the
+ \type{State} type, we can look at the type of a value. However, we
+ must be careful to ignore only \emph{substates}, and not a
+ function's own state.
+
+ In \in{example}[ex:AvgStateNorm] above, we should generate a register
+ connected with its output connected to \lam{s} and its input connected
+ to \lam{s'}. However, \lam{s'} is build up from both \lam{accs'} and
+ \lam{count'}, while only \lam{count'} should end up in the register.
+ \lam{accs'} is a substate for the \lam{acc} function, for which a
+ register will be created when generating \VHDL for the \lam{acc}
+ function.
+
+ Fortunately, the \lam{accs'} variable (and any other substate) has a
+ property that we can easily check: It has a \lam{State} type
+ annotation. This means that whenever \VHDL is generated for a tuple
+ (or other algebraic type), we can simply leave out all elements that
+ have a \lam{State} type. This will leave just the parts of the state
+ that do not have a \lam{State} type themselves, like \lam{count'},
+ which is exactly a function's own state. This approach also means that
+ the state part of the result is automatically excluded when generating
+ the output port, which is also required.
+
+ We can formalize this translation a bit, using the following
+ rules.