Various small fixes following from Bert's commentaar.
[matthijs/master-project/report.git] / Chapters / Prototype.tex
index ac4cc93e29023e8d319b54537cfa2a0f45eb968f..48c69b9d0f50bdfb1dd71c95994f13ff504e9457 100644 (file)
       development.
     \stopitemize
 
-    \todo{Sidenote: No EDSL}
 
+    \placeintermezzo{}{
+      \startframedtext[width=8cm,background=box,frame=no]
+      \startalignment[center]
+        {\tfa No \small{EDSL} or Template Haskell}
+      \stopalignment
+      \blank[medium]
+
+      Note that in this consideration, embedded domain-specific
+      languages (\small{EDSL}) and Template Haskell (\small{TH})
+      approaches have not been included. As we've seen in
+      \in{section}[sec:context:fhdls], these approaches have all kinds
+      of limitations on the description language that we would like to
+      avoid.
+      \stopframedtext
+    }
     Considering that we required a prototype which should be working quickly,
     and that implementing parsers, semantic checkers and especially
     typcheckers is not exactly the core of this research (but it is lots and
@@ -51,8 +65,6 @@
     primary compiler, \GHC, provides a high level API to its internals, made
     Haskell an obvious choice.
 
-    \note{There should be evaluation of the choice of Haskell and \VHDL}
-
   \section[sec:prototype:output]{Output format}
     The second important question is: What will be our output format? Since
     our prototype won't be able to program FPGA's directly, we'll have to have
@@ -68,8 +80,7 @@
     However, \small{EDIF} is not completely tool-independent. It specifies a
     meta-format, but the hardware components that can be used vary between
     various tool and hardware vendors, as well as the interpretation of the
-    \small{EDIF} standard. \todo{Is this still true? Reference:
-    http://delivery.acm.org/10.1145/80000/74534/p803-li.pdf?key1=74534\&key2=8370537521\&coll=GUIDE\&dl=GUIDE\&CFID=61207158\&CFTOKEN=61908473}
+    \small{EDIF} standard. \cite[li89]
    
     This means that when working with \small{EDIF}, our prototype would become
     technology dependent (\eg only work with \small{FPGA}s of a specific
     switch to \small{EDIF} in the future, with minimal changes to the
     prototype.
 
-  \section{Prototype design}
+  \section[sec:prototype:design]{Prototype design}
     As suggested above, we will use the Glasgow Haskell Compiler (\small{GHC}) to
     implement our prototype compiler. To understand the design of the
     compiler, we will first dive into the \small{GHC} compiler a bit. It's
       \startlambda
       λbndr.body
       \stoplambda
-      This is the basic lambda abstraction, as it occurs in labmda calculus.
+      This is the basic lambda abstraction, as it occurs in lambda calculus.
       It consists of a binder part and a body part.  A lambda abstraction
       creates a function, that can be applied to an argument. The binder is
       usually a value binder, but it can also be a \emph{type binder} (or
       binder, even when strictness was involved.  Nonetheless, the prototype
       handles this binder as expected.
 
-      Note that these case statements are less powerful than the full Haskell
-      case statements. In particular, they do not support complex patterns like
+      Note that these case expressions are less powerful than the full Haskell
+      case expressions. In particular, they do not support complex patterns like
       in Haskell. Only the constructor of an expression can be matched,
       complex patterns are implemented using multiple nested case expressions.
 
-      Case statements are also used for unpacking of algebraic datatypes, even
+      Case expressions are also used for unpacking of algebraic datatypes, even
       when there is only a single constructor. For examples, to add the elements
       of a tuple, the following Core is generated:
 
         instance declaration. This dictionary, as well as the binder
         introduced by a lambda that introduces a dictionary, have the
         predicate type as their type. These binders are usually named starting
-        with a \lam{$}. Usually the name of the type concerned is not
+        with a \lam{\$}. Usually the name of the type concerned is not
         reflected in the name of the dictionary, but the name of the type
         class is. The Haskell expression \hs{show True} thus becomes:
 
         \startlambda
-        show @Bool $dShow True
+        show @Bool \$dShow True
         \stoplambda
       \stopdesc
 
       here)}.
         
   \section[sec:prototype:statetype]{State annotations in Haskell}
-      \fxnote{This entire section on state annotations should be reviewed}
-
-      Ideal: Type synonyms, since there is no additional code overhead for
-      packing and unpacking. Downside: there is no explicit conversion in Core
-      either, so type synonyms tend to get lost in expressions (they can be
-      preserved in binders, but this makes implementation harder, since that
-      statefulness of a value must be manually tracked).
-
-      Less ideal: Newtype. Requires explicit packing and unpacking of function
-      arguments. If you don't unpack substates, there is no overhead for
-      (un)packing substates. This will result in many nested State constructors
-      in a nested state type. \eg: 
+    As noted in \in{section}[sec:description:stateann], Cλash needs some
+    way to let the programmer explicitly specify which of a function's
+    arguments and which part of a function's result represent the
+    function's state.
+
+    Using the Haskell type systems, there are a few ways we can tackle this.
+
+    \subsection{Type synonyms}
+      Haskell provides type synonyms as a way to declare a new type that is
+      equal to an existing type (or rather, a new name for an existing type).
+      This allows both the original type and the synonym to be used
+      interchangedly in a Haskell program. This means no explicit conversion
+      is needed either. For example, a simple accumulator would become:
+
+      \starthaskell
+      type State s = s
+      acc :: Word -> State Word -> (State Word, Word)
+      acc i s = let sum = s + i in (sum, sum)
+      \stophaskell
+
+      This looks nice in Haskell, but turns out to be hard to implement. There
+      are no explicit conversion in Haskell, but not in Core either. This
+      means the type of a value might be show as \hs{AccState} in some places,
+      but \hs{Word} in others (and this can even change due to
+      transformations). Since every binder has an explicit type associated
+      with it, the type of every function type will be properly preserved and
+      could be used to track down the statefulness of each value by the
+      compiler. However, this makes the implementation a lot more complicated
+      than it currently is using \hs{newtypes}.
+
+    % Use \type instead of \hs here, since the latter breaks inside
+    % section headings.
+    \subsection{Type renaming (\type{newtype})}
+      Haskell also supports type renamings as a way to declare a new type that
+      has the same (runtime) representation as an existing type (but is in
+      fact a different type to the typechecker). With type renaming, an
+      explicit conversion between values of the two types is needed. The
+      accumulator would then become:
+
+      \starthaskell
+      newtype State s = State s
+      acc :: Word -> State Word -> (State Word, Word)
+      acc i (State s) = let sum = s + i in (State sum, sum)
+      \stophaskell
+
+      The \hs{newtype} line declares a new type \hs{State} that has one type
+      argument, \hs{s}. This type contains one \quote{constructor} \hs{State}
+      with a single argument of type \hs{s}. It is customary to name the
+      constructor the same as the type, which is allowed (since types can
+      never cause name collisions with values). The difference with the type
+      synonym example is in the explicit conversion between the \hs{State
+      Word} and \hs{Word} types by pattern matching and by using the explicit
+      the \hs{State constructor}.
+
+      This explicit conversion makes the \VHDL generation easier: Whenever we
+      remove (unpack) the \hs{State} type, this means we are accessing the
+      current state (\eg, accessing the register output). Whenever we are a
+      adding (packing) the \hs{State} type, we are producing a new value for
+      the state (\eg, providing the register input).
+
+      When dealing with nested states (a stateful function that calls stateful
+      functions, which might call stateful functions, etc.) the state type
+      could quickly grow complex because of all the \hs{State} type constructors
+      needed. For example, consider the following state type (this is just the
+      state type, not the entire function type):
 
       \starttyping
       State (State Bit, State (State Word, Bit), Word)
       \stoptyping
 
-      Alternative: Provide different newtypes for input and output state. This
-      makes the code even more explicit, and typechecking can find even more
-      errors. However, this requires defining two type synomyms for each
-      stateful function instead of just one. \eg:
-
-      \starttyping
-      type AccumStateIn = StateIn Bit
-      type AccumStateOut = StateOut Bit
-      \stoptyping
+      We cannot leave all these \hs{State} type constructors out, since that
+      would change the type (unlike when using type synonyms). However, when
+      using type synonyms to hide away substates (see
+      \in{section}[sec:prototype:substatesynonyms] below), this
+      disadvantage should be limited.
+
+      \subsubsection{Different input and output types}
+        An alternative could be to use different types for input and output
+        state (\ie current and updated state). The accumulator example would
+        then become something like:
+
+        \starthaskell
+        newtype StateIn s = StateIn s
+        newtype StateOut s = StateOut s
+        acc :: Word -> StateIn Word -> (StateIn Word, Word)
+        acc i (StateIn s) = let sum = s + i in (StateIn sum, sum)
+        \stophaskell
+        
+        This could make the implementation easier and the hardware
+        descriptions less errorprone (you can no longer \quote{forget} to
+        unpack and repack a state variable and just return it directly, which
+        can be a problem in the current prototype). However, it also means we
+        need twice as many type synonyms to hide away substates, making this
+        approach a bit cumbersome. It also makes it harder to copmare input
+        and output state types, possible reducing the type safety of the
+        descriptions.
+
+    \subsection[sec:prototype:substatesynonyms]{Type synonyms for substates}
+      As noted above, when using nested (hierarchical) states, the state types
+      of the \quote{upper} functions (those that call other functions, which
+      call other functions, etc.) quickly becomes complicated. Also, when the
+      state type of one of the \quote{lower} functions changes, the state
+      types of all the upper functions changes as well. If the state type for
+      each function is explicitly and completely specified, this means that a
+      lot of code needs updating whenever a state type changes.
+
+      To prevent this, it is recommended (but not enforced) to use a type
+      synonym for the state type of every function. Every function calling
+      other functions will then use the state type synonym of the called
+      functions in its own type, requiring no code changes when the state type
+      of a called function changes. This approach is used in
+      \in{example}[ex:AvgState] below. The \hs{AccState} and \hs{AvgState}
+      are examples of such state type synonyms.
+
+    \subsection{Chosen approach}
+      To keep implementation simple, the current prototype uses the type
+      renaming approach, with a single type for both input and output
+      states. In the future, it might be worthwhile to revisit this
+      approach if more complicated flow analysis is implemented for
+      state variables. This analysis is needed to add proper error
+      checking anyway and might allow the use of type synonyms without
+      losing any expressivity.
 
-      This also increases the possibility of having different input and output
-      states. Checking for identical input and output state types is also
-      harder, since each element in the state must be unpacked and compared
-      separately.
+      \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 builtin 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've 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
 
-      Alternative: Provide a type for the entire result type of a stateful
-      function, not just the state part. \eg:
+        Any lambda that binds a variable with a state type, creates a new
+        input state variable.
+      \stopdesc
 
-      \starttyping
-      newtype Result state result = Result (state, result)
-      \stoptyping
-      
-      This makes it easy to say "Any stateful function must return a
-      \type{Result} type, without having to sort out result from state. However,
-      this either requires a second type for input state (similar to
-      \type{StateIn} / \type{StateOut} above), or requires the compiler to
-      select the right argument for input state by looking at types (which works
-      for complex states, but when that state has the same type as an argument,
-      things get ambiguous) or by selecting a fixed (\eg, the last) argument,
-      which might be limiting.
+      \startdesc{Input state variables can be unpacked.}
+        \startlambda
+          s = spacked ▶ (AccState, Word)
+        \stoplambda
 
-      \subsubsection{Example}
-      As an example of the used approach, a simple averaging circuit, that lets
-      the accumulation of the inputs be done by a subcomponent.
+        An input state variable may be unpacked using a cast operation. This
+        removes the \lam{State} type renaming and the result has no longer a
+        \lam{State} type.
+
+        If the result of this unpacking does not have a state type and does
+        not contain state variables, there are no limitations on its use.
+        Otherwise if it does not have a state type but does contain
+        substates, we refer to it as a \emph{state-containing input
+        variable} and the limitations below apply. If it has a state type
+        itself, we refer to it as an \emph{input substate variable} and the
+        below limitations apply as well.
+
+        It may seem strange to consider a variable that still has a state
+        type directly after unpacking, but consider the case where a
+        function does not have any state of its own, but does call a single
+        stateful function. This means it must have a state argument that
+        contains just a substate. The function signature of such a function
+        could look like:
+
+        \starthaskell
+          type FooState = State AccState
+        \stophaskell
+
+        Which is of course equivalent to \lam{State (State Word)}.
+      \stopdesc
 
-      \starttyping
-        newtype State s = State s
-
-        type AccumState = State Bit
-        accum :: Word -> AccumState -> (AccumState, Word)
-        accum i (State s) = (State (s + i), s + i)
-
-        type AvgState = (AccumState, Word)
-        avg :: Word -> AvgState -> (AvgState, Word)
-        avg i (State s) = (State s', o)
-          where
-            (accums, count) = s
-            -- Pass our input through the accumulator, which outputs a sum
-            (accums', sum) = accum i accums
-            -- Increment the count (which will be our new state)
-            count' = count + 1
-            -- Compute the average
-            o = sum / count'
-            s' = (accums', count')
-      \stoptyping
+      \startdesc{Variables can be extracted from state-containing input variables.}
+        \startlambda
+          accs = case s of (accs, _) -> accs
+        \stoplambda
 
-      And the normalized, core-like versions:
+        A state-containing input variable is typically a tuple containing
+        multiple elements (like the current function's state, substates or
+        more tuples containing substates). All of these can be extracted
+        from an input variable using an extractor case (or possibly
+        multiple, when the input variable is nested).
+
+        If the result has no state type and does not contain any state
+        variables either, there are no further limitations on its use. If
+        the result has no state type but does contain state variables we
+        refer to it as a \emph{state-containing input variable} and this
+        limitation keeps applying. If the variable has a state type itself,
+        we refer to it as an \emph{input substate variable} and below
+        limitations apply.
+
+      \startdesc{Input substate variables can be passed to functions.} 
+        \startlambda
+          accres = acc i accs
+          accs' = case accres of (accs', _) -> accs'
+        \stoplambda
+        
+        An input substate variable can (only) be passed to a function.
+        Additionally, every input substate variable must be used in exactly
+        \emph{one} application, no more and no less.
 
-      \starttyping
-        accum i spacked = res
-          where
-            s = case spacked of (State s) -> s
-            s' = s + i
-            spacked' = State s'
-            o = s + i
-            res = (spacked', o)
-
-        avg i spacked = res
-          where
-            s = case spacked of (State s) -> s
-            accums = case s of (accums, \_) -> accums
-            count = case s of (\_, count) -> count
-            accumres = accum i accums
-            accums' = case accumres of (accums', \_) -> accums'
-            sum = case accumres of (\_, sum) -> sum
-            count' = count + 1
-            o = sum / count'
-            s' = (accums', count')
-            spacked' = State s'
-            res = (spacked', o)
-      \stoptyping
+        The function result should contain exactly one state variable, which
+        can be extracted using (multiple) case expressions. The extracted
+        state variable is referred to the \emph{output substate}
 
+        The type of this output substate must be identical to the type of
+        the input substate passed to the function.
+      \stopdesc
 
+      \startdesc{Variables can be inserted into a state-containing output variable.}
+        \startlambda
+          s' = (accs', count')
+        \stoplambda
+        
+        A function's output state is usually a tuple containing its own
+        updated state variables and all output substates. This result is
+        built up using any single-constructor algebraic datatype.
 
-      As noted above, any component of a function's state that is a substate,
-      \eg 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 leave out substates from any 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.
-      Here, we are translating from Core to \small{VHDL}, and we can simply not generate
-      \small{VHDL} for substates, effectively removing the substate components
-      alltogether.
-
-      There are a few important points when ignore substates.
-
-      First, we have to have some definition of "substate". Since any state
-      argument or return value that represents state must be of the \type{State}
-      type, we can simply look at its type. However, we must be careful to
-      ignore only {\em substates}, and not a function's own state.
-
-      In the example above, this means we should remove \type{accums'} from
-      \type{s'}, but not throw away \type{s'} entirely. We should, however,
-      remove \type{s'} from the output port of the function, since the state
-      will be handled by a \small{VHDL} procedure within the function.
-
-      When looking at substates, these can appear in two places: As part of an
-      argument and as part of a return value. As noted above, these substates
-      can only be used in very specific ways.
-
-      \desc{State variables can appear as an argument.} When generating \small{VHDL}, we
-      completely ignore the argument and generate no input port for it.
-
-      \desc{State variables can be extracted from other state variables.} When
-      extracting a state variable from another state variable, this always means
-      we're extracting a substate, which we can ignore. So, we simply generate no
-      \small{VHDL} for any extraction operation that has a state variable as a result.
-
-      \desc{State variables can be passed to functions.} When passing a
-      state variable to a function, this always means we're passing a substate
-      to a subcomponent. The entire argument can simply be ingored in the
-      resulting port map.
-
-      \desc{State variables can be returned from functions.} When returning a
-      state variable from a function (probably as a part of an algebraic
-      datatype), this always mean we're returning a substate from a
-      subcomponent. The entire state variable should be ignored in the resulting
-      port map. The type binder of the binder that the function call is bound
-      to should not include the state type either.
-
-      \startdesc{State variables can be inserted into other variables.} When inserting
-      a state variable into another variable (usually by constructing that new
-      variable using its constructor), we can identify two cases: 
+        The result of these expressions is referred to as a
+        \emph{state-containing output variable}, which are subject to these
+        limitations.
+      \stopdesc
 
-      \startitemize
-        \item The state is inserted into another state variable. In this case,
-        the inserted state is a substate, and can be safely left out of the
-        constructed variable.
-        \item The state is inserted into a non-state variable. This happens when
-        building up the return value of a function, where you put state and
-        retsult variables together in an algebraic type (usually a tuple). In
-        this case, we should leave the state variable out as well, since we
-        don't want it to be included as an output port.
-      \stopitemize
+      \startdesc{State containing output variables can be packed.}
+        \startlambda
+          spacked' = s' ▶ State (AccState, Word)
+        \stoplambda
 
-      So, in both cases, we can simply leave out the state variable from the
-      resulting value. In the latter case, however, we should generate a state
-      proc instead, which assigns the state variable to the input state variable
-      at each clock tick.
+        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
-      
-      \desc{State variables can appear as (part of) a function result.} When
-      generating \small{VHDL}, we can completely ignore any part of a function result
-      that has a state type. If the entire result is a state type, this will
-      mean the entity will not have an output port. Otherwise, the state
-      elements will be removed from the type of the output port.
 
+      \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
 
-      Now, we know how to handle each use of a state variable separately. If we
-      look at the whole, we can conclude the following:
+      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.
 
       \startitemize
-        \item A state unpack operation should not generate any \small{VHDL}. The binder
-        to which the unpacked state is bound should still be declared, this signal
-        will become the register and will hold the current state.
-        \item A state pack operation should not generate any \small{VHDL}. The binder th
-        which the packed state is bound should not be declared. The binder that is
-        packed is the signal that will hold the new state.
-        \item Any values of a State type should not be translated to \small{VHDL}. In
-        particular, State elements should be removed from tuples (and other
-        datatypes) and arguments with a state type should not generate ports.
-        \item To make the state actually work, a simple \small{VHDL} proc should be
-        generated. This proc updates the state at every clockcycle, by assigning
-        the new state to the current state. This will be recognized by synthesis
-        tools as a register specification.
+        \item A state unpack operation should not generate any \small{VHDL}.
+        The binder to which the unpacked state is bound should still be
+        declared, this signal will become the register and will hold the
+        current state.
+        \item A state pack operation should not generate any \small{VHDL}.
+        The binder to which the packed state is bound should not be
+        declared. The binder that is packed is the signal that will hold the
+        new state.
+        \item Any values of a State type should not be translated to
+        \small{VHDL}. In particular, State elements should be removed from
+        tuples (and other datatypes) and arguments with a state type should
+        not generate ports.
+        \item To make the state actually work, a simple \small{VHDL} proc
+        should be generated. This proc updates the state at every
+        clockcycle, by assigning the new state to the current state. This
+        will be recognized by synthesis tools as a register specification.
       \stopitemize
 
-
-      When applying these rules to the example program (in normal form), we will
-      get the following result. All the parts that don't generate any value are
-      crossed out, leaving some very boring assignments here and there.
+      When applying these rules to the description in
+      \in{example}[ex:AvgStateNormal], we be left with the description
+      in \in{example}[ex:AvgStateRemoved]. All the parts that don't
+      generate any \VHDL directly are crossed out, leaving just the
+      actual flow of values in the final hardware.
       
-    
-  \starthaskell
-    avg i --spacked-- = res
-      where
-        s = --case spacked of (State s) -> s--
-        --accums = case s of (accums, \_) -> accums--
-        count = case s of (--\_,-- count) -> count
-        accumres = accum i --accums--
-        --accums' = case accumres of (accums', \_) -> accums'--
-        sum = case accumres of (--\_,-- sum) -> sum
-        count' = count + 1
-        o = sum / count'
-        s' = (--accums',-- count')
-        --spacked' = State s'--
-        res = (--spacked',-- o)
-  \stophaskell
-          
+      \startlambda
+        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
+      \stoplambda
+              
       When we would really leave out the crossed out parts, we get a slightly
-      weird program: There is a variable \type{s} which has no value, and there
-      is a variable \type{s'} that is never used. Together, these two will form
-      the state proc of the function. \type{s} contains the "current" state,
-      \type{s'} is assigned the "next" state. So, at the end of each clock
-      cycle, \type{s'} should be assigned to \type{s}.
-
-      Note that the definition of \type{s'} is not removed, even though one
-      might think it as having a state type. Since the state type has a single
-      argument constructor \type{State}, some type that should be the resulting
-      state should always be explicitly packed with the State constructor,
-      allowing us to remove the packed version, but still generate \small{VHDL} for the
-      unpacked version (of course with any substates removed).
-      
-      As you can see, the definition of \type{s'} is still present, since it
-      does not have a state type (The State constructor. The \type{accums'} substate has been removed,
-      leaving us just with the state of \type{avg} itself.
-    \subsection{Initial state}
-      How to specify the initial state? Cannot be done inside a hardware
-      function, since the initial state is its own state argument for the first
-      call (unless you add an explicit, synchronous reset port).
-
-      External init state is natural for simulation.
-
-      External init state works for hardware generation as well.
-
-      Implementation issues: state splitting, linking input to output state,
-      checking usage constraints on state variables.
-
-      \todo{Implementation issues: Separate compilation, simplified core.}
-
+      weird program: There is a variable \lam{s} which has no value, and there
+      is a variable \lam{s'} that is never used. Together, these two will form
+      the state proc of the function. \lam{s} contains the "current" state,
+      \lam{s'} is assigned the "next" state. So, at the end of each clock
+      cycle, \lam{s'} should be assigned to \lam{s}.
+
+      As you can see, the definition of \lam{s'} is still present, since
+      it does not have a state type. The \lam{accums'} substate has been
+      removed, leaving us just with the state of \lam{avg} itself.
+
+      As an illustration of the result of this function,
+      \in{example}[ex:AccStateVHDL] and \in{example}[ex:AvgStateVHDL] show the the \VHDL that is
+      generated from the examples is this section.
+
+      \startbuffer[AvgStateVHDL]
+        entity avgComponent_0 is
+             port (\izAlE2\ : in \unsigned_31\;
+                   \foozAo1zAo12\ : out \(,)unsigned_31\;
+                   clock : in std_logic;
+                   resetn : in std_logic);
+        end entity avgComponent_0;
+
+
+        architecture structural of avgComponent_0 is
+             signal \szAlG2\ : \(,)unsigned_31\;
+             signal \countzAlW2\ : \unsigned_31\;
+             signal \dszAm62\ : \(,)unsigned_31\;
+             signal \sumzAmk3\ : \unsigned_31\;
+             signal \reszAnCzAnM2\ : \unsigned_31\;
+             signal \foozAnZzAnZ2\ : \unsigned_31\;
+             signal \reszAnfzAnj3\ : \unsigned_31\;
+             signal \s'zAmC2\ : \(,)unsigned_31\;
+        begin
+             \countzAlW2\ <= \szAlG2\.A;
+
+             \comp_ins_dszAm62\ : entity accComponent_1
+                                       port map (\izAob3\ => \izAlE2\,
+                                                 \foozAoBzAoB2\ => \dszAm62\,
+                                                 clock => clock,
+                                                 resetn => resetn);
+
+             \sumzAmk3\ <= \dszAm62\.A;
+
+             \reszAnCzAnM2\ <= to_unsigned(1, 32);
+
+             \foozAnZzAnZ2\ <= \countzAlW2\ + \reszAnCzAnM2\;
+
+             \reszAnfzAnj3\ <= \sumzAmk3\ * \foozAnZzAnZ2\;
+
+             \s'zAmC2\.A <= \foozAnZzAnZ2\;
+
+             \foozAo1zAo12\.A <= \reszAnfzAnj3\;
+
+             state : process (clock, resetn)
+             begin
+                  if resetn = '0' then
+                  elseif rising_edge(clock) then
+                       \szAlG2\ <= \s'zAmC2\;
+                  end if;
+             end process state;
+        end architecture structural;
+      \stopbuffer
+      \startbuffer[AccStateVHDL]
+        entity accComponent_1 is
+             port (\izAob3\ : in \unsigned_31\;
+                   \foozAoBzAoB2\ : out \(,)unsigned_31\;
+                   clock : in std_logic;
+                   resetn : in std_logic);
+        end entity accComponent_1;
+
+
+        architecture structural of accComponent_1 is
+             signal \szAod3\ : \unsigned_31\;
+             signal \reszAonzAor3\ : \unsigned_31\;
+        begin
+             \reszAonzAor3\ <= \szAod3\ + \izAob3\;
+             
+             \foozAoBzAoB2\.A <= \reszAonzAor3\;
+             
+             state : process (clock, resetn)
+             begin
+                  if resetn = '0' then
+                  elseif rising_edge(clock) then
+                       \szAod3\ <= \reszAonzAor3\;
+                  end if;
+             end process state;
+        end architecture structural;
+      \stopbuffer 
+    
+      \placeexample[][ex:AccStateVHDL]{\VHDL generated for acc from \in{example}[ex:AvgState]}
+          {\typebuffer[AccStateVHDL]}
+      \placeexample[][ex:AvgStateVHDL]{\VHDL generated for avg from \in{example}[ex:AvgState]}
+          {\typebuffer[AvgStateVHDL]}
+%    \subsection{Initial state}
+%      How to specify the initial state? Cannot be done inside a hardware
+%      function, since the initial state is its own state argument for the first
+%      call (unless you add an explicit, synchronous reset port).
+%
+%      External init state is natural for simulation.
+%
+%      External init state works for hardware generation as well.
+%
+%      Implementation issues: state splitting, linking input to output state,
+%      checking usage constraints on state variables.
+%
+%      \todo{Implementation issues: Separate compilation, simplified core.}
+%
 % vim: set sw=2 sts=2 expandtab: