Add two new simple normal form examples.
[matthijs/master-project/report.git] / Chapters / Normalization.tex
index 68d48d4eeebf1511647d7939726d16dfa856cf60..4b3a08c821404729476f02aefdba5af96c0c1585 100644 (file)
@@ -1,4 +1,4 @@
-\chapter{Normalization}
+\chapter[chap:normalization]{Normalization}
 
 % A helper to print a single example in the half the page width. The example
 % text should be in a buffer whose name is given in an argument.
@@ -7,7 +7,7 @@
 % will end up on a single line. The strut=no option prevents a bunch of empty
 % space at the start of the frame.
 \define[1]\example{
-  \framed[offset=1mm,align=right,strut=no]{
+  \framed[offset=1mm,align=right,strut=no,background=box,frame=off]{
     \setuptyping[option=LAM,style=sans,before=,after=]
     \typebuffer[#1]
     \setuptyping[option=none,style=\tttf]
@@ -64,7 +64,104 @@ be an input port, every bound value will become a concurrent statement (such
 as a component instantiation or conditional signal assignment) and the result
 variable will become the output port.
 
-An example of a program in canonical form would be:
+\startbuffer[MulSum]
+alu :: Bit -> Word -> Word -> Word
+alu = λa.λb.λc.
+    let
+      mul = (*) a b
+      sum = (+) mul c
+    in
+      sum
+\stopbuffer
+
+\startuseMPgraphic{MulSum}
+  save a, b, c, mul, add, sum;
+
+  % I/O ports
+  newCircle.a(btex $a$ etex) "framed(false)";
+  newCircle.b(btex $b$ etex) "framed(false)";
+  newCircle.c(btex $c$ etex) "framed(false)";
+  newCircle.sum(btex $res$ etex) "framed(false)";
+
+  % Components
+  newCircle.mul(btex - etex);
+  newCircle.add(btex + etex);
+
+  a.c      - b.c   = (0cm, 2cm);
+  b.c      - c.c   = (0cm, 2cm);
+  add.c            = c.c + (2cm, 0cm);
+  mul.c            = midpoint(a.c, b.c) + (2cm, 0cm);
+  sum.c            = add.c + (2cm, 0cm);
+  c.c              = origin;
+
+  % Draw objects and lines
+  drawObj(a, b, c, mul, add, sum);
+
+  ncarc(a)(mul) "arcangle(15)";
+  ncarc(b)(mul) "arcangle(-15)";
+  ncline(c)(add);
+  ncline(mul)(add);
+  ncline(add)(sum);
+\stopuseMPgraphic
+
+\placeexample[ex:MulSum]{\small{ALU} described in normal form}
+  \startcombination[2*1]
+    {\typebufferlam{MulSum}}{Description in normal form}
+    {\boxedgraphic{MulSum}}{Described architecture}
+  \stopcombination
+
+\startbuffer[AddSubAlu]
+alu :: Bit -> Word -> Word -> Word
+alu = λopcode.λa.λb.
+    let
+      res1 = (+) a b
+      res2 = (-) a b
+      res = case op of
+        Low -> res1
+        High -> res2
+    in
+      res
+\stopbuffer
+
+\startuseMPgraphic{AddSubAlu}
+  save opcode, a, b, add, sub, mux, res;
+
+  % I/O ports
+  newCircle.opcode(btex $opcode$ etex) "framed(false)";
+  newCircle.a(btex $a$ etex) "framed(false)";
+  newCircle.b(btex $b$ etex) "framed(false)";
+  newCircle.res(btex $res$ etex) "framed(false)";
+  % Components
+  newCircle.add(btex + etex);
+  newCircle.sub(btex - etex);
+  newMux.mux;
+
+  opcode.c - a.c   = (0cm, 2cm);
+  add.c    - a.c   = (4cm, 0cm);
+  sub.c    - b.c   = (4cm, 0cm);
+  a.c      - b.c   = (0cm, 3cm);
+  mux.c            = midpoint(add.c, sub.c) + (1.5cm, 0cm);
+  res.c    - mux.c = (1.5cm, 0cm);
+  b.c              = origin;
+
+  % Draw objects and lines
+  drawObj(opcode, a, b, res, add, sub, mux);
+
+  ncline(a)(add) "posA(e)";
+  ncline(b)(sub) "posA(e)";
+  nccurve(a)(sub) "posA(e)", "angleA(0)";
+  nccurve(b)(add) "posA(e)", "angleA(0)";
+  nccurve(add)(mux) "posB(inpa)", "angleB(0)";
+  nccurve(sub)(mux) "posB(inpb)", "angleB(0)";
+  nccurve(opcode)(mux) "posB(n)", "angleA(0)", "angleB(-90)";
+  ncline(mux)(res) "posA(out)";
+\stopuseMPgraphic
+
+\placeexample[ex:AddSubAlu]{\small{ALU} described in normal form}
+  \startcombination[2*1]
+    {\typebufferlam{AddSubAlu}}{Description in normal form}
+    {\boxedgraphic{AddSubAlu}}{Described architecture}
+  \stopcombination
 
 \startlambda
   -- All arguments are an inital lambda
@@ -230,10 +327,10 @@ the core language in a notation that resembles lambda calculus.
 
 Each of these transforms is meant to be applied to every (sub)expression
 in a program, for as long as it applies. Only when none of the
-expressions can be applied anymore, the program is in normal form. We
-hope to be able to prove that this form will obey all of the constraints
-defined above, but this has yet to happen (though it seems likely that
-it will).
+transformations can be applied anymore, the program is in normal form (by
+definition). We hope to be able to prove that this form will obey all of the
+constraints defined above, but this has yet to happen (though it seems likely
+that it will).
 
 Each of the transforms will be described informally first, explaining
 the need for and goal of the transform. Then, a formal definition is
@@ -684,7 +781,7 @@ arguments into normal form. The goal here is to:
 When looking at the arguments of a user-defined function, we can
 divide them into two categories:
 \startitemize
-  \item Arguments with a runtime representable type (\eg bits or vectors).
+  \item Arguments of a runtime representable type (\eg bits or vectors).
 
         These arguments can be preserved in the program, since they can
         be translated to input ports later on.  However, since we can
@@ -720,7 +817,7 @@ When looking at the arguments of a builtin function, we can divide them
 into categories: 
 
 \startitemize
-  \item Arguments with a runtime representable type.
+  \item Arguments of a runtime representable type.
         
         As we have seen with user-defined functions, these arguments can
         always be reduced to a simple variable reference, by the
@@ -729,7 +826,7 @@ into categories:
         functions can be limited to signal references, instead of
         needing to support all possible expressions.
 
-  \item Arguments with a function type.
+  \item Arguments of a function type.
         
         These arguments are functions passed to higher order builtins,
         like \lam{map} and \lam{foldl}. Since implementing these