Add two new simple normal form examples.

[matthijs/master-project/report.git] / Chapters / Normalization.tex

diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex
index 1f9f62be9bb633171419c7e4ab4a3c4a82c1d6f3..4b3a08c821404729476f02aefdba5af96c0c1585 100644 (file)
--- 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.
 
 % 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{
 % 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]
     \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.
 
 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
 
 \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
 
 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
 
 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
 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
 
         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
 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
         
         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.
 
         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
         
         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}
 \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.