Add section on EDSLs.
[matthijs/master-project/report.git] / Chapters / Prototype.tex
index 139b93e56be69f2637efcffc785935e95bb77b9c..820327ce36008203deda81b3805af757464868f8 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
     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
       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 statements. 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: