X-Git-Url: https://git.stderr.nl/gitweb?p=matthijs%2Fmaster-project%2Freport.git;a=blobdiff_plain;f=Chapters%2FNormalization.tex;h=4b3a08c821404729476f02aefdba5af96c0c1585;hp=1f9f62be9bb633171419c7e4ab4a3c4a82c1d6f3;hb=600d280f5ab94fa48bc84fc13b7d485b868918d3;hpb=b1f08ad1bc712b096ea8330252e7a343955004f7

diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex
index 1f9f62b..4b3a08c 100644
--- a/Chapters/Normalization.tex
+++ b/Chapters/Normalization.tex
@@ -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
@@ -973,247 +1070,3 @@ x = let x = add 1 2 in x
 \stopbuffer
 
 \transexample{Return value simplification}{from}{to}
-
-\subsection{Example sequence}
-
-This section lists an example expression, with a sequence of transforms
-applied to it. The exact transforms given here probably don't exactly
-match the transforms given above anymore, but perhaps this can clarify
-the big picture a bit.
-
-TODO: Update or remove this section.
-
-\startlambda
-  λx.
-    let s = foo x
-    in
-      case s of
-        (a, b) ->
-          case a of
-            High -> add
-            Low -> let
-              op' = case b of
-                High -> sub
-                Low  -> λc.λd.c
-              in
-                λc.λd.op' d c
-\stoplambda
-
-After top-level η-abstraction:
-
-\startlambda
-  λx.λc.λd.
-    (let s = foo x
-    in
-      case s of
-        (a, b) ->
-          case a of
-            High -> add
-            Low -> let
-              op' = case b of
-                High -> sub
-                Low  -> λc.λd.c
-              in
-                λc.λd.op' d c
-    ) c d
-\stoplambda
-
-After (extended) β-reduction:
-
-\startlambda
-  λx.λc.λd.
-    let s = foo x
-    in
-      case s of
-        (a, b) ->
-          case a of
-            High -> add c d
-            Low -> let
-              op' = case b of
-                High -> sub
-                Low  -> λc.λd.c
-              in
-                op' d c
-\stoplambda
-
-After return value extraction:
-
-\startlambda
-  λx.λc.λd.
-    let s = foo x
-        r = case s of
-              (a, b) ->
-                case a of
-                  High -> add c d
-                  Low -> let
-                    op' = case b of
-                      High -> sub
-                      Low  -> λc.λd.c
-                    in
-                      op' d c
-    in
-      r
-\stoplambda
-
-Scrutinee simplification does not apply.
-
-After case binder wildening:
-
-\startlambda
-  λx.λc.λd.
-    let s = foo x
-        a = case s of (a, _) -> a
-        b = case s of (_, b) -> b
-        r = case s of (_, _) ->
-              case a of
-                High -> add c d
-                Low -> let op' = case b of
-                             High -> sub
-                             Low  -> λc.λd.c
-                       in
-                         op' d c
-    in
-      r
-\stoplambda
-
-After case value simplification
-
-\startlambda
-  λx.λc.λd.
-    let s = foo x
-        a = case s of (a, _) -> a
-        b = case s of (_, b) -> b
-        r = case s of (_, _) -> r'
-        rh = add c d
-        rl = let rll = λc.λd.c
-                 op' = case b of
-                   High -> sub
-                   Low  -> rll
-             in
-               op' d c
-        r' = case a of
-               High -> rh
-               Low -> rl
-    in
-      r
-\stoplambda
-
-After let flattening:
-
-\startlambda
-  λx.λc.λd.
-    let s = foo x
-        a = case s of (a, _) -> a
-        b = case s of (_, b) -> b
-        r = case s of (_, _) -> r'
-        rh = add c d
-        rl = op' d c
-        rll = λc.λd.c
-        op' = case b of
-          High -> sub
-          Low  -> rll
-        r' = case a of
-               High -> rh
-               Low -> rl
-    in
-      r
-\stoplambda
-
-After function inlining:
-
-\startlambda
-  λx.λc.λd.
-    let s = foo x
-        a = case s of (a, _) -> a
-        b = case s of (_, b) -> b
-        r = case s of (_, _) -> r'
-        rh = add c d
-        rl = (case b of
-          High -> sub
-          Low  -> λc.λd.c) d c
-        r' = case a of
-          High -> rh
-          Low -> rl
-    in
-      r
-\stoplambda
-
-After (extended) β-reduction again:
-
-\startlambda
-  λx.λc.λd.
-    let s = foo x
-        a = case s of (a, _) -> a
-        b = case s of (_, b) -> b
-        r = case s of (_, _) -> r'
-        rh = add c d
-        rl = case b of
-          High -> sub d c
-          Low  -> d
-        r' = case a of
-          High -> rh
-          Low -> rl
-    in
-      r
-\stoplambda
-
-After case value simplification again:
-
-\startlambda
-  λx.λc.λd.
-    let s = foo x
-        a = case s of (a, _) -> a
-        b = case s of (_, b) -> b
-        r = case s of (_, _) -> r'
-        rh = add c d
-        rlh = sub d c
-        rl = case b of
-          High -> rlh
-          Low  -> d
-        r' = case a of
-          High -> rh
-          Low -> rl
-    in
-      r
-\stoplambda
-
-After case removal:
-
-\startlambda
-  λx.λc.λd.
-    let s = foo x
-        a = case s of (a, _) -> a
-        b = case s of (_, b) -> b
-        r = r'
-        rh = add c d
-        rlh = sub d c
-        rl = case b of
-          High -> rlh
-          Low  -> d
-        r' = case a of
-          High -> rh
-          Low -> rl
-    in
-      r
-\stoplambda
-
-After let bind removal:
-
-\startlambda
-  λx.λc.λd.
-    let s = foo x
-        a = case s of (a, _) -> a
-        b = case s of (_, b) -> b
-        rh = add c d
-        rlh = sub d c
-        rl = case b of
-          High -> rlh
-          Low  -> d
-        r' = case a of
-          High -> rh
-          Low -> rl
-    in
-      r'
-\stoplambda
-
-Application simplification is not applicable.