Move some examples around.
[matthijs/master-project/report.git] / Chapters / Normalization.tex
index fba2c4a47d22b6fb09527fbd4f94ff40e87fd162..e1a96ff0c396a10239ec8b8330fc5f62064844d5 100644 (file)
@@ -36,7 +36,7 @@
     to this form as the \emph{normal form} of the program. The formal
     definition of this normal form is quite simple:
 
-    \placedefinition{}{\startboxed A program is in \emph{normal form} if none of the
+    \placedefinition[force]{}{\startboxed A program is in \emph{normal form} if none of the
     transformations from this chapter apply.\stopboxed}
 
     Of course, this is an \quote{easy} definition of the normal form, since our
       other expression.
     \stopitemize
 
-    \todo{Intermezzo: functions vs plain values}
-
-    A very simple example of a program in normal form is given in
-    \in{example}[ex:MulSum]. As you can see, all arguments to the function (which
-    will become input ports in the generated \VHDL) are at the outer level.
-    This means that the body of the inner lambda abstraction is never a
-    function, but always a plain value.
-
-    As the body of the inner lambda abstraction, we see a single (recursive)
-    let expression, that binds two variables (\lam{mul} and \lam{sum}). These
-    variables will be signals in the generated \VHDL, bound to the output port
-    of the \lam{*} and \lam{+} components.
-
-    The final line (the \quote{return value} of the function) selects the
-    \lam{sum} signal to be the output port of the function. This \quote{return
-    value} can always only be a variable reference, never a more complex
-    expression.
-
-    \todo{Add generated VHDL}
-
     \startbuffer[MulSum]
     alu :: Bit -> Word -> Word -> Word
     alu = λa.λb.λc.
       ncline(add)(sum);
     \stopuseMPgraphic
 
-    \placeexample[here][ex:MulSum]{Simple architecture consisting of a
+    \placeexample[][ex:MulSum]{Simple architecture consisting of a
     multiplier and a subtractor.}
       \startcombination[2*1]
         {\typebufferlam{MulSum}}{Core description in normal form.}
         {\boxedgraphic{MulSum}}{The architecture described by the normal form.}
       \stopcombination
 
+    \todo{Intermezzo: functions vs plain values}
+
+    A very simple example of a program in normal form is given in
+    \in{example}[ex:MulSum]. As you can see, all arguments to the function (which
+    will become input ports in the generated \VHDL) are at the outer level.
+    This means that the body of the inner lambda abstraction is never a
+    function, but always a plain value.
+
+    As the body of the inner lambda abstraction, we see a single (recursive)
+    let expression, that binds two variables (\lam{mul} and \lam{sum}). These
+    variables will be signals in the generated \VHDL, bound to the output port
+    of the \lam{*} and \lam{+} components.
+
+    The final line (the \quote{return value} of the function) selects the
+    \lam{sum} signal to be the output port of the function. This \quote{return
+    value} can always only be a variable reference, never a more complex
+    expression.
+
+    \todo{Add generated VHDL}
+
     \in{Example}[ex:MulSum] showed a function that just applied two
     other functions (multiplication and addition), resulting in a simple
     architecture with two components and some connections.  There is of
       ncline(mux)(res) "posA(out)";
     \stopuseMPgraphic
 
-    \placeexample[here][ex:AddSubAlu]{Simple \small{ALU} supporting two operations.}
+    \placeexample[][ex:AddSubAlu]{Simple \small{ALU} supporting two operations.}
       \startcombination[2*1]
         {\typebufferlam{AddSubAlu}}{Core description in normal form.}
         {\boxedgraphic{AddSubAlu}}{The architecture described by the normal form.}
     \stopuseMPgraphic
 
     \todo{Don't split registers in this image?}
-    \placeexample[here][ex:NormalComplete]{Simple architecture consisting of an adder and a
+    \placeexample[][ex:NormalComplete]{Simple architecture consisting of an adder and a
     subtractor.}
       \startcombination[2*1]
         {\typebufferlam{NormalComplete}}{Core description in normal form.}
         \stoptrans
 
         \starttrans
-        x = λv0 ... λvn.E
-        ~                                \lam{E} is representable
+        x = λv0 ... λvn.E                \lam{E} is representable
+        ~                                \lam{E} is not a lambda abstraction
         E                                \lam{E} is not a let expression
         ---------------------------      \lam{E} is not a local variable reference
         letrec x = E in x