X-Git-Url: https://git.stderr.nl/gitweb?p=matthijs%2Fmaster-project%2Freport.git;a=blobdiff_plain;f=Chapters%2FNormalization.tex;h=37895b3a5543f6c189625da9b4645ae9d418bccc;hp=03f379244e0299b787ae294c90e4db2c07eab829;hb=b01be2e1ed672b31da67a7a24228f8442d918f9a;hpb=68e92ccd2b456b9ce81b0617417bc8abdaff6fa3

diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex
index 03f3792..37895b3 100644
--- a/Chapters/Normalization.tex
+++ b/Chapters/Normalization.tex
@@ -28,11 +28,7 @@
   core can describe expressions that do not have a direct hardware
   interpretation.
 
-  \todo{Describe core properties not supported in \VHDL, and describe how the
-  \VHDL we want to generate should look like.}
-
   \section{Normal form}
-    \todo{Refresh or refer to distinct hardware per application principle}
     The transformations described here have a well-defined goal: To bring the
     program in a well-defined form that is directly translatable to hardware,
     while fully preserving the semantics of the program. We refer to this form as
@@ -629,9 +625,11 @@
 
       In particular, we define no particular order of transformations. Since
       transformation order should not influence the resulting normal form,
-      \todo{This is not really true, but would like it to be...} this leaves
-      the implementation free to choose any application order that results in
-      an efficient implementation.
+      this leaves the implementation free to choose any application order that
+      results in an efficient implementation. Unfortunately this is not
+      entirely true for the current set of transformations. See
+      \in{section}[sec:normalization:non-determinism] for a discussion of this
+      problem.
 
       When applying a single transformation, we try to apply it to every (sub)expression
       in a function, not just the top level function body. This allows us to
@@ -798,6 +796,7 @@
        normal form.
 
         \placeintermezzo{}{
+          \defref{substitution notation}
           \startframedtext[width=8cm,background=box,frame=no]
           \startalignment[center]
             {\tfa Substitution notation}
@@ -890,7 +889,8 @@
         This transformation is not needed to get an expression into intended
         normal form (since these bindings are part of the intended normal
         form), but makes the resulting \small{VHDL} a lot shorter.
-        
+       
+        \refdef{substitution notation}
         \starttrans
         letrec
           a0 = E0
@@ -1647,7 +1647,7 @@
         
         This propagation makes higher order values become applied (in
         particular both of the alternatives of the case now have a
-        representable type. Completely applied top level functions (like the
+        representable type). Completely applied top level functions (like the
         first alternative) are now no longer invalid (they fall under
         \in{item}[item:completeapp] above). (Completely) applied lambda
         abstractions can be removed by β-abstraction. For our example,
@@ -1822,6 +1822,7 @@
         solves (part of) the polymorphism, higher order values and
         unrepresentable literals in an expression.
 
+        \refdef{substitution notation}
         \starttrans
         letrec 
           a0 = E0
@@ -1944,7 +1945,6 @@
 
         \todo{Examples. Perhaps reference the previous sections}
 
-
   \section{Unsolved problems}
     The above system of transformations has been implemented in the prototype
     and seems to work well to compile simple and more complex examples of
@@ -2013,7 +2013,7 @@
         let y = (a * b) in y + y
         \stoplambda
 
-      \subsection{Non-determinism}
+      \subsection[sec:normalization:non-determinism]{Non-determinism}
         As an example, again consider the following expression:
 
         \startlambda
@@ -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: