X-Git-Url: https://git.stderr.nl/gitweb?p=matthijs%2Fmaster-project%2Freport.git;a=blobdiff_plain;f=Chapters%2FNormalization.tex;h=61170088d4b13a23166d7a7683628629f7442351;hp=f9a10157970ad68d646a6d5948f697f516af8f23;hb=f276067e08b153e130b305242a4e2ef87e84960a;hpb=4b177f0eea59d8cc3e9da21a078583260d9f79c9

diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex
index f9a1015..6117008 100644
--- a/Chapters/Normalization.tex
+++ b/Chapters/Normalization.tex
@@ -2060,6 +2060,37 @@
         transformations will probably need updating to handle them in all
         cases.
 
+      \subsection{Normalization of stateful descriptions}
+        Currently, the intended normal form definition\refdef{intended
+        normal form definition} offers enough freedom to describe all
+        valid stateful descriptions, but is not limiting enough. It is
+        possible to write descriptions which are in intended normal
+        form, but cannot be translated into \VHDL in a meaningful way
+        (\eg, a function that swaps two substates in its result, or a
+        function that changes a substate itself instead of passing it to
+        a subfunction).
+
+        It is now up to the programmer to not do anything funny with
+        these state values, whereas the normalization just tries not to
+        mess up the flow of state values. In practice, there are
+        situations where a Core program that \emph{could} be a valid
+        stateful description is not translateable by the prototype. This
+        most often happens when statefulness is mixed with pattern
+        matching, causing a state input to be unpacked multiple times or
+        be unpacked and repacked only in some of the code paths.
+
+        \todo{example?}
+
+        Without going into detail about the exact problems (of which
+        there are probably more than have shown up so far), it seems
+        unlikely that these problems can be solved entirely by just
+        improving the \VHDL state generation in the final stage. The
+        normalization stage seems the best place to apply the rewriting
+        needed to support more complex stateful descriptions. This does
+        of course mean that the intended normal form definition must be
+        extended as well to be more specific about how state handling
+        should look like in normal form.
+
   \section[sec:normalization:properties]{Provable properties}
     When looking at the system of transformations outlined above, there are a
     number of questions that we can ask ourselves. The main question is of course:
@@ -2213,7 +2244,6 @@
       Also, since there is only one node in the normal set, it must obviously be
       \emph{deterministic} as well.
 
-    \todo{Add content to these sections}
     \subsection{Termination}
       In general, proving termination of an arbitrary program is a very
       hard problem. \todo{Ref about arbitrary termination} Fortunately,