X-Git-Url: https://git.stderr.nl/gitweb?p=matthijs%2Fmaster-project%2Freport.git;a=blobdiff_plain;f=Chapters%2FNormalization.tex;h=71e71eb33ae78160d51b1fa9981847d233d3fd58;hp=e609cb3d2874655ea38297c8c75637368b1fa2d7;hb=77f079684a01c329d10d1cd00cf5e4ee1d05377f;hpb=4521ef7f14ae52781329c17250f67d25d9a67dca

diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex
index e609cb3..71e71eb 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]
@@ -35,37 +35,200 @@
 %%  \stopcombination
 %}
 
-The first step in the core to VHDL translation process, is normalization. We
+The first step in the core to \small{VHDL} translation process, is normalization. We
 aim to bring the core description into a simpler form, which we can
-subsequently translate into VHDL easily. This normal form is needed because
-the full core language is more expressive than VHDL in some areas and because
+subsequently translate into \small{VHDL} easily. This normal form is needed because
+the full core language is more expressive than \small{VHDL} in some areas and because
 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.
+TODO: Describe core properties not supported in \small{VHDL}, and describe how the
+\small{VHDL} we want to generate should look like.
 
-\section{Goal}
+\section{Normal form}
 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.
+while fully preserving the semantics of the program. We refer to this form as
+the \emph{normal form} of the program. The formal definition of this normal
+form is quite simple:
 
-This {\em normal form} is again a Core program, but with a very specific
-structure. A function in normal form has nested lambda's at the top, which
-produce a let expression. This let expression binds every function application
-in the function and produces a simple identifier. Every bound value in
-the let expression is either a simple function application or a case
-expression to extract a single element from a tuple returned by a
-function.
+\placedefinition{}{A program is in \emph{normal form} if none of the
+transformations from this chapter apply.}
 
-An example of a program in canonical form would be:
+Of course, this is an \quote{easy} definition of the normal form, since our
+program will end up in normal form automatically. The more interesting part is
+to see if this normal form actually has the properties we would like it to
+have.
+
+But, before getting into more definitions and details about this normal form,
+let's try to get a feeling for it first. The easiest way to do this is by
+describing the things we want to not have in a normal form.
+
+\startitemize
+  \item Any \emph{polymorphism} must be removed. When laying down hardware, we
+  can't generate any signals that can have multiple types. All types must be
+  completely known to generate hardware.
+  
+  \item Any \emph{higher order} constructions must be removed. We can't
+  generate a hardware signal that contains a function, so all values,
+  arguments and returns values used must be first order.
+
+  \item Any complex \emph{nested scopes} must be removed. In the \small{VHDL}
+  description, every signal is in a single scope. Also, full expressions are
+  not supported everywhere (in particular port maps can only map signal names,
+  not expressions). To make the \small{VHDL} generation easy, all values must be bound
+  on the \quote{top level}.
+\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 final hardware) are at the top. This means that
+the body of the final lambda abstraction is never a function, but always a
+plain value.
+
+After the lambda abstractions, we see a single let expression, that binds two
+variables (\lam{mul} and \lam{sum}). These variables will be signals in the
+final hardware, 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.
+
+\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[here][ex:MulSum]{Simple architecture consisting of an adder and a
+subtractor.}
+  \startcombination[2*1]
+    {\typebufferlam{MulSum}}{Core description in normal form.}
+    {\boxedgraphic{MulSum}}{The architecture described by the normal form.}
+  \stopcombination
+
+The previous example described composing an architecture by calling other
+functions (operators), resulting in a simple architecture with component and
+connection. There is of course also some mechanism for choice in the normal
+form. In a normal Core program, the \emph{case} expression can be used in a
+few different ways to describe choice. In normal form, this is limited to a
+very specific form.
+
+\in{Example}[ex:AddSubAlu] shows an example describing a
+simple \small{ALU}, which chooses between two operations based on an opcode
+bit. The main structure is the same as in \in{example}[ex:MulSum], but this
+time the \lam{res} variable is bound to a case expression. This case
+expression scrutinizes the variable \lam{opcode} (and scrutinizing more
+complex expressions is not supported). The case expression can select a
+different variable based on the constructor of \lam{opcode}.
+
+\startbuffer[AddSubAlu]
+alu :: Bit -> Word -> Word -> Word
+alu = λopcode.λa.λb.
+    let
+      res1 = (+) a b
+      res2 = (-) a b
+      res = case opcode 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[here][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.}
+  \stopcombination
+
+As a more complete example, consider \in{example}[ex:NormalComplete]. This
+example contains everything that is supported in normal form, with the
+exception of builtin higher order functions.
+
+\startbuffer[NormalComplete]
+  regbank :: Bit 
+             -> Word 
+             -> State (Word, Word) 
+             -> (State (Word, Word), Word)
 
-\startlambda
   -- All arguments are an inital lambda
-  λa.λd.λsp.
+  regbank = λa.λd.λsp.
   -- There are nested let expressions at top level
   let
-    -- Unpack the state by coercion
+    -- Unpack the state by coercion (\eg, cast from
+    -- State (Word, Word) to (Word, Word))
     s = sp :: (Word, Word)
     -- Extract both registers from the state
     r1 = case s of (fst, snd) -> fst
@@ -77,52 +240,116 @@ An example of a program in canonical form would be:
       High -> r1
       Low -> r2
     r1' = case a of
-      High -> d
+      High -> d'
       Low -> r1
     r2' = case a of
       High -> r2
-      Low -> d
+      Low -> d'
     -- Packing a tuple
     s' = (,) r1' r2'
-    -- Packing the state by coercion
+    -- pack the state by coercion (\eg, cast from
+    -- (Word, Word) to State (Word, Word))
     sp' = s' :: State (Word, Word)
     -- Pack our return value
     res = (,) sp' out
   in
     -- The actual result
     res
-\stoplambda
+\stopbuffer
+
+\startuseMPgraphic{NormalComplete}
+  save a, d, r, foo, muxr, muxout, out;
+
+  % I/O ports
+  newCircle.a(btex \lam{a} etex) "framed(false)";
+  newCircle.d(btex \lam{d} etex) "framed(false)";
+  newCircle.out(btex \lam{out} etex) "framed(false)";
+  % Components
+  %newCircle.add(btex + etex);
+  newBox.foo(btex \lam{foo} etex);
+  newReg.r1(btex $\lam{r1}$ etex) "dx(4mm)", "dy(6mm)";
+  newReg.r2(btex $\lam{r2}$ etex) "dx(4mm)", "dy(6mm)", "reflect(true)";
+  newMux.muxr1;
+  % Reflect over the vertical axis
+  reflectObj(muxr1)((0,0), (0,1));
+  newMux.muxr2;
+  newMux.muxout;
+  rotateObj(muxout)(-90);
+
+  d.c               = foo.c + (0cm, 1.5cm); 
+  a.c               = (xpart r2.c + 2cm, ypart d.c - 0.5cm);
+  foo.c             = midpoint(muxr1.c, muxr2.c) + (0cm, 2cm);
+  muxr1.c           = r1.c + (0cm, 2cm);
+  muxr2.c           = r2.c + (0cm, 2cm);
+  r2.c              = r1.c + (4cm, 0cm);
+  r1.c              = origin;
+  muxout.c          = midpoint(r1.c, r2.c) - (0cm, 2cm);
+  out.c             = muxout.c - (0cm, 1.5cm);
+
+%  % Draw objects and lines
+  drawObj(a, d, foo, r1, r2, muxr1, muxr2, muxout, out);
+  
+  ncline(d)(foo);
+  nccurve(foo)(muxr1) "angleA(-90)", "posB(inpa)", "angleB(180)";
+  nccurve(foo)(muxr2) "angleA(-90)", "posB(inpb)", "angleB(0)";
+  nccurve(muxr1)(r1) "posA(out)", "angleA(180)", "posB(d)", "angleB(0)";
+  nccurve(r1)(muxr1) "posA(out)", "angleA(0)", "posB(inpb)", "angleB(180)";
+  nccurve(muxr2)(r2) "posA(out)", "angleA(0)", "posB(d)", "angleB(180)";
+  nccurve(r2)(muxr2) "posA(out)", "angleA(180)", "posB(inpa)", "angleB(0)";
+  nccurve(r1)(muxout) "posA(out)", "angleA(0)", "posB(inpb)", "angleB(-90)";
+  nccurve(r2)(muxout) "posA(out)", "angleA(180)", "posB(inpa)", "angleB(-90)";
+  % Connect port a
+  nccurve(a)(muxout) "angleA(-90)", "angleB(180)", "posB(sel)";
+  nccurve(a)(muxr1) "angleA(180)", "angleB(-90)", "posB(sel)";
+  nccurve(a)(muxr2) "angleA(180)", "angleB(-90)", "posB(sel)";
+  ncline(muxout)(out) "posA(out)";
+\stopuseMPgraphic
+
+\placeexample[here][ex:NormalComplete]{Simple architecture consisting of an adder and a
+subtractor.}
+  \startcombination[2*1]
+    {\typebufferlam{NormalComplete}}{Core description in normal form.}
+    {\boxedgraphic{NormalComplete}}{The architecture described by the normal form.}
+  \stopcombination
+
+\subsection{Normal form definition}
+Now we have some intuition for the normal form, we can describe how we want
+the normal form to look like in a slightly more formal manner. The following
+EBNF-like description completely captures the intended structure (and
+generates a subset of GHC's core format).
+
+Some clauses have an expression listed in parentheses. These are conditions
+that need to apply to the clause.
 
 \startlambda
 \italic{normal} = \italic{lambda}
-\italic{lambda} = λvar.\italic{lambda} (representable(typeof(var)))
+\italic{lambda} = λvar.\italic{lambda} (representable(var))
                 | \italic{toplet} 
 \italic{toplet} = let \italic{binding} in \italic{toplet} 
                 | letrec [\italic{binding}] in \italic{toplet}
-                | var (representable(typeof(var)), fvar(var))
-\italic{binding} = var = \italic{rhs} (representable(typeof(rhs)))
+                | var (representable(varvar))
+\italic{binding} = var = \italic{rhs} (representable(rhs))
                  -- State packing and unpacking by coercion
-                 | var0 = var1 :: State ty (fvar(var1))
-                 | var0 = var1 :: ty (var0 :: State ty) (fvar(var1))
+                 | var0 = var1 :: State ty (lvar(var1))
+                 | var0 = var1 :: ty (var0 :: State ty) (lvar(var1))
 \italic{rhs} = userapp
              | builtinapp
              -- Extractor case
-             | case var of C a0 ... an -> ai (fvar(var))
+             | case var of C a0 ... an -> ai (lvar(var))
              -- Selector case
-             | case var of (fvar(var))
-                DEFAULT -> var0 (fvar(var0))
-                C w0 ... wn -> resvar (\forall{}i, wi \neq resvar, fvar(resvar))
+             | case var of (lvar(var))
+                DEFAULT -> var0 (lvar(var0))
+                C w0 ... wn -> resvar (\forall{}i, wi \neq resvar, lvar(resvar))
 \italic{userapp} = \italic{userfunc}
                  | \italic{userapp} {userarg}
-\italic{userfunc} = var (tvar(var))
-\italic{userarg} = var (fvar(var))
+\italic{userfunc} = var (gvar(var))
+\italic{userarg} = var (lvar(var))
 \italic{builtinapp} = \italic{builtinfunc}
                     | \italic{builtinapp} \italic{builtinarg}
 \italic{builtinfunc} = var (bvar(var))
 \italic{builtinarg} = \italic{coreexpr}
 \stoplambda
 
--- TODO: Define tvar, fvar, typeof, representable
 -- TODO: Limit builtinarg further
 
 -- TODO: There can still be other casts around (which the code can handle,
@@ -137,65 +364,90 @@ the output port. Most function applications bound by the let expression
 define a component instantiation, where the input and output ports are mapped
 to local signals or arguments. Some of the others use a builtin
 construction (\eg the \lam{case} statement) or call a builtin function
-(\eg \lam{add} or \lam{sub}). For these, a hardcoded VHDL translation is
+(\eg \lam{add} or \lam{sub}). For these, a hardcoded \small{VHDL} translation is
 available.
 
-\subsection{Normal definition}
-Formally, the normal form is a core program obeying the following
-constraints. TODO: Update this section, this is probably not completely
-accurate or relevant anymore.
-
-\startitemize[R,inmargin]
-%\item All top level binds must have the form $\expr{\bind{fun}{lamexpr}}$.
-%$fun$ is an identifier that will be bound as a global identifier.
-%\item A $lamexpr$ has the form $\expr{\lam{arg}{lamexpr}}$ or
-%$\expr{letexpr}$. $arg$ is an identifier which will be bound as an $argument$.
-%\item[letexpr] A $letexpr$ has the form $\expr{\letexpr{letbinds}{retexpr}}$.
-%\item $letbinds$ is a list with elements of the form
-%$\expr{\bind{res}{appexpr}}$ or $\expr{\bind{res}{builtinexpr}}$, where $res$ is
-%an identifier that will be bound as local identifier. The type of the bound
-%value must be a $hardware\;type$.
-%\item[builtinexpr] A $builtinexpr$ is an expression that can be mapped to an
-%equivalent VHDL expression. Since there are many supported forms for this,
-%these are defined in a separate table.
-%\item An $appexpr$ has the form $\expr{fun}$ or $\expr{\app{appexpr}{x}}$,
-%where $fun$ is a global identifier and $x$ is a local identifier.
-%\item[retexpr] A $retexpr$ has the form $\expr{x}$ or $\expr{tupexpr}$, where $x$ is a local identifier that is bound as an $argument$ or $result$.  A $retexpr$ must
-%be of a $hardware\;type$.
-%\item A $tupexpr$ has the form $\expr{con}$ or $\expr{\app{tupexpr}{x}}$,
-%where $con$ is a tuple constructor ({\em e.g.} $(,)$ or $(,,,)$) and $x$ is
-%a local identifier.
-%\item A $hardware\;type$ is a type that can be directly translated to
-%hardware. This includes the types $Bit$, $SizedWord$, tuples containing
-%elements of $hardware\;type$s, and will include others. This explicitely
-%excludes function types.
-\stopitemize
+\subsection{Definitions}
+In the following sections, we will be using a number of functions and
+notations, which we will define here.
+
+\subsubsection{Transformations}
+The most important notation is the one for transformation, which looks like
+the following:
 
-TODO: Say something about uniqueness of identifiers
+\starttrans
+context conditions
+~
+from
+------------------------            expression conditions
+to
+~
+context additions
+\stoptrans
 
-\subsection{Builtin expressions}
-A $builtinexpr$, as defined at \in[builtinexpr] can have any of the following forms.
+Here, we describe a transformation. The most import parts are \lam{from} and
+\lam{to}, which describe the Core expresssion that should be matched and the
+expression that it should be replaced with. This matching can occur anywhere
+in function that is being normalized, so it applies to any subexpression as
+well.
 
-\startitemize[m,inmargin]
-%\item
-%$tuple\_extract=\expr{\case{t}{\alt{\app{con}{x_0\;x_1\;..\;x_n}}{x_i}}}$,
-%where $t$ can be any local identifier, $con$ is a tuple constructor ({\em
-%e.g.} $(,)$ or $(,,,)$), $x_0$ to $x_n$ can be any identifier, and $x_i$ can
-%be any of $x_0$ to $x_n$. A case expression must have a $hardware\;type$.
-%\item TODO: Many more!
-\stopitemize
+The \lam{expression conditions} list a number of conditions on the \lam{from}
+expression that must hold for the transformation to apply.
 
-\section{Transform passes}
+Furthermore, there is some way to look into the environment (\eg, other top
+level bindings).  The \lam{context conditions} part specifies any number of
+top level bindings that must be present for the transformation to apply.
+Usually, this lists a top level binding that binds an identfier that is also
+used in the \lam{from} expression, allowing us to "access" the value of a top
+level binding in the \lam{to} expression (\eg, for inlining).
+
+Finally, there is a way to influence the environment. The \lam{context
+additions} part lists any number of new top level bindings that should be
+added.
+
+If there are no \lam{context conditions} or \lam{context additions}, they can
+be left out alltogether, along with the separator \lam{~}.
+
+TODO: Example
 
+\subsubsection{Other concepts}
+A \emph{global variable} is any variable that is bound at the
+top level of a program, or an external module. A local variable is any other
+variable (\eg, variables local to a function, which can be bound by lambda
+abstractions, let expressions and case expressions).
+
+A \emph{hardware representable} type is a type that we can generate
+a signal for in hardware. For example, a bit, a vector of bits, a 32 bit
+unsigned word, etc. Types that are not runtime representable notably
+include (but are not limited to): Types, dictionaries, functions.
+
+A \emph{builtin function} is a function for which a builtin
+hardware translation is available, because its actual definition is not
+translatable. A user-defined function is any other function.
+
+\subsubsection{Functions}
+Here, we define a number of functions that can be used below to concisely
+specify conditions.
+
+\emph{gvar(expr)} is true when \emph{expr} is a variable that references a
+global variable. It is false when it references a local variable.
+
+\emph{lvar(expr)} is the inverse of \emph{gvar}; it is true when \emph{expr}
+references a local variable, false when it references a global variable.
+
+\emph{representable(expr)} or \emph{representable(var)} is true when
+\emph{expr} or \emph{var} has a type that is representable at runtime.
+
+\section{Transform passes}
 In this section we describe the actual transforms. Here we're using
 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
@@ -221,13 +473,13 @@ E                 \lam{E :: * -> *}
 \stoptrans
 
 \startbuffer[from]
-foo = λa -> case a of 
+foo = λa.case a of 
   True -> λb.mul b b
   False -> id
 \stopbuffer
 
 \startbuffer[to]
-foo = λa.λx -> (case a of 
+foo = λa.λx.(case a of 
     True -> λb.mul b b
     False -> λy.id y) x
 \stopbuffer
@@ -292,33 +544,338 @@ in
 \transexample{Extended β-reduction}{from}{to}
 
 \subsection{Let derecursification}
+This transformation is meant to make lets non-recursive whenever possible.
+This might allow other optimizations to do their work better. TODO: Why is
+this needed exactly?
 
 \subsection{Let flattening}
-This transform turns two nested lets (\lam{let x = (let ... in ...) in
-...}) into a single let.
+This transformation puts nested lets in the same scope, by lifting the
+binding(s) of the inner let into a new let around the outer let. Eventually,
+this will cause all let bindings to appear in the same scope (they will all be
+in scope for the function return value).
+
+Note that this transformation does not try to be smart when faced with
+recursive lets, it will just leave the lets recursive (possibly joining a
+recursive and non-recursive let into a single recursive let). The let
+rederursification transformation will do this instead.
+
+\starttrans
+letnonrec x = (let bindings in M) in N
+------------------------------------------
+let bindings in (letnonrec x = M) in N
+\stoptrans
+
+\starttrans
+letrec 
+  \vdots
+  x = (let bindings in M)
+  \vdots
+in
+  N
+------------------------------------------
+letrec
+  \vdots
+  bindings
+  x = M
+  \vdots
+in
+  N
+\stoptrans
+
+\startbuffer[from]
+let
+  a = letrec
+    x = 1
+    y = 2
+  in
+    x + y
+in
+  letrec
+    b = let c = 3 in a + c
+    d = 4
+  in
+    d + b
+\stopbuffer
+\startbuffer[to]
+letrec
+  x = 1
+  y = 2
+in
+  let
+    a = x + y
+  in
+    letrec
+      c = 3
+      b = a + c
+      d = 4
+    in
+      d + b
+\stopbuffer
+
+\transexample{Let flattening}{from}{to}
 
 \subsection{Empty let removal}
+This transformation is simple: It removes recursive lets that have no bindings
+(which usually occurs when let derecursification removes the last binding from
+it).
+
+\starttrans
+letrec in M
+--------------
+M
+\stoptrans
 
 \subsection{Simple let binding removal}
-This transforms inlines simple let bindings (\eg a = b).
+This transformation inlines simple let bindings (\eg a = b).
+
+This transformation is not needed to get into normal form, but makes the
+resulting \small{VHDL} a lot shorter.
+
+\starttrans
+letnonrec
+  a = b
+in
+  M
+-----------------
+M[b/a]
+\stoptrans
+
+\starttrans
+letrec
+  \vdots
+  a = b
+  \vdots
+in
+  M
+-----------------
+let
+  \vdots [b/a]
+  \vdots [b/a]
+in
+  M[b/a]
+\stoptrans
 
 \subsection{Unused let binding removal}
+This transformation removes let bindings that are never used. Usually,
+the desugarer introduces some unused let bindings.
+
+This normalization pass should really be unneeded to get into normal form
+(since ununsed bindings are not forbidden by the normal form), but in practice
+the desugarer or simplifier emits some unused bindings that cannot be
+normalized (e.g., calls to a \type{PatError} (TODO: Check this name)). Also,
+this transformation makes the resulting \small{VHDL} a lot shorter.
+
+\starttrans
+let a = E in M
+----------------------------    \lam{a} does not occur free in \lam{M}
+M
+\stoptrans
+
+\starttrans
+letrec
+  \vdots
+  a = E
+  \vdots
+in
+  M
+----------------------------    \lam{a} does not occur free in \lam{M}
+letrec
+  \vdots
+  \vdots
+in
+  M
+\stoptrans
 
 \subsection{Non-representable binding inlining}
-This transform inlines let bindings of a funtion type. TODO: This should
-be generelized to anything that is non representable at runtime, or
-something like that.
+This transform inlines let bindings that have a non-representable type. Since
+we can never generate a signal assignment for these bindings (we cannot
+declare a signal assignment with a non-representable type, for obvious
+reasons), we have no choice but to inline the binding to remove it.
+
+If the binding is non-representable because it is a lambda abstraction, it is
+likely that it will inlined into an application and β-reduction will remove
+the lambda abstraction and turn it into a representable expression at the
+inline site. The same holds for partial applications, which can be turned into
+full applications by inlining.
+
+Other cases of non-representable bindings we see in practice are primitive
+Haskell types. In most cases, these will not result in a valid normalized
+output, but then the input would have been invalid to start with. There is one
+exception to this: When a builtin function is applied to a non-representable
+expression, things might work out in some cases. For example, when you write a
+literal \hs{SizedInt} in Haskell, like \hs{1 :: SizedInt D8}, this results in
+the following core: \lam{fromInteger (smallInteger 10)}, where for example
+\lam{10 :: GHC.Prim.Int\#} and \lam{smallInteger 10 :: Integer} have
+non-representable types. TODO: This/these paragraph(s) should probably become a
+separate discussion somewhere else.
+
+\starttrans
+letnonrec a = E in M
+--------------------------    \lam{E} has a non-representable type.
+M[E/a]
+\stoptrans
+
+\starttrans
+letrec 
+  \vdots
+  a = E
+  \vdots
+in
+  M
+--------------------------    \lam{E} has a non-representable type.
+letrec
+  \vdots [E/a]
+  \vdots [E/a]
+in
+  M[E/a]
+\stoptrans
+
+\startbuffer[from]
+letrec
+  a = smallInteger 10
+  inc = λa -> add a 1
+  inc' = add 1
+  x = fromInteger a 
+in
+  inc (inc' x)
+\stopbuffer
+
+\startbuffer[to]
+letrec
+  x = fromInteger (smallInteger 10)
+in
+  (λa -> add a 1) (add 1 x)
+\stopbuffer
+
+\transexample{Let flattening}{from}{to}
+
+\subsection{Compiler generated top level binding inlining}
+TODO
 
 \subsection{Scrutinee simplification}
 This transform ensures that the scrutinee of a case expression is always
 a simple variable reference.
 
+\starttrans
+case E of
+  alts
+-----------------        \lam{E} is not a local variable reference
+let x = E in 
+  case E of
+    alts
+\stoptrans
+
+\startbuffer[from]
+case (foo a) of
+  True -> a
+  False -> b
+\stopbuffer
+
+\startbuffer[to]
+let x = foo a in
+  case x of
+    True -> a
+    False -> b
+\stopbuffer
+
+\transexample{Let flattening}{from}{to}
+
+
 \subsection{Case simplification}
+This transformation ensures that all case expressions become normal form. This
+means they will become one of:
+\startitemize
+\item An extractor case with a single alternative that picks a single field
+from a datatype, \eg \lam{case x of (a, b) -> a}.
+\item A selector case with multiple alternatives and only wild binders, that
+makes a choice between expressions based on the constructor of another
+expression, \eg \lam{case x of Low -> a; High -> b}.
+\stopitemize
+
+\starttrans
+case E of
+  C0 v0,0 ... v0,m -> E0
+  \vdots
+  Cn vn,0 ... vn,m -> En
+--------------------------------------------------- \forall i \forall j, 0 <= i <= n, 0 <= i < m (\lam{wi,j} is a wild (unused) binder)
+letnonrec
+  v0,0 = case x of C0 v0,0 .. v0,m -> v0,0
+  \vdots
+  v0,m = case x of C0 v0,0 .. v0,m -> v0,m
+  x0 = E0
+  \dots
+  vn,m = case x of Cn vn,0 .. vn,m -> vn,m
+  xn = En
+in
+  case E of
+    C0 w0,0 ... w0,m -> x0
+    \vdots
+    Cn wn,0 ... wn,m -> xn
+\stoptrans
+
+TODO: This transformation specified like this is complicated and misses
+conditions to prevent looping with itself. Perhaps we should split it here for
+discussion?
+
+\startbuffer[from]
+case a of
+  True -> add b 1
+  False -> add b 2
+\stopbuffer
+
+\startbuffer[to]
+letnonrec
+  x0 = add b 1
+  x1 = add b 2
+in
+  case a of
+    True -> x0
+    False -> x1
+\stopbuffer
+
+\transexample{Selector case simplification}{from}{to}
+
+\startbuffer[from]
+case a of
+  (,) b c -> add b c
+\stopbuffer
+\startbuffer[to]
+letnonrec
+  b = case a of (,) b c -> b
+  c = case a of (,) b c -> c
+  x0 = add b c
+in
+  case a of
+    (,) w0 w1 -> x0
+\stopbuffer
+
+\transexample{Extractor case simplification}{from}{to}
 
 \subsection{Case removal}
 This transform removes any case statements with a single alternative and
 only wild binders.
 
+These "useless" case statements are usually leftovers from case simplification
+on extractor case (see the previous example).
+
+\starttrans
+case x of
+  C v0 ... vm -> E
+----------------------     \lam{\forall i, 0 <= i <= m} (\lam{vi} does not occur free in E)
+E
+\stoptrans
+
+\startbuffer[from]
+case a of
+  (,) w0 w1 -> x0
+\stopbuffer
+
+\startbuffer[to]
+x0
+\stopbuffer
+
+\transexample{Case removal}{from}{to}
+
 \subsection{Argument simplification}
 The transforms in this section deal with simplifying application
 arguments into normal form. The goal here is to:
@@ -326,8 +883,9 @@ arguments into normal form. The goal here is to:
 \startitemize
  \item Make all arguments of user-defined functions (\eg, of which
  we have a function body) simple variable references of a runtime
- representable type.
- \item Make all arguments of builtin functions either:
+ representable type. This is needed, since these applications will be turned
+ into component instantiations.
+ \item Make all arguments of builtin functions one of:
    \startitemize
     \item A type argument.
     \item A dictionary argument.
@@ -340,7 +898,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
@@ -352,16 +910,31 @@ divide them into two categories:
         
         These arguments cannot be preserved in the program, since we
         cannot represent them as input or output ports in the resulting
-        VHDL. To remove them, we create a specialized version of the
+        \small{VHDL}. To remove them, we create a specialized version of the
         called function with these arguments filled in. This is done by
         the argument propagation transform.
+
+        Typically, these arguments are type and dictionary arguments that are
+        used to make functions polymorphic. By propagating these arguments, we
+        are essentially doing the same which GHC does when it specializes
+        functions: Creating multiple variants of the same function, one for
+        each type for which it is used. Other common non-representable
+        arguments are functions, e.g. when calling a higher order function
+        with another function or a lambda abstraction as an argument.
+
+        The reason for doing this is similar to the reasoning provided for
+        the inlining of non-representable let bindings above. In fact, this
+        argument propagation could be viewed as a form of cross-function
+        inlining.
 \stopitemize
 
+TODO: Check the following itemization.
+
 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
@@ -370,7 +943,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
@@ -439,9 +1012,10 @@ into categories:
         categories instead.
 \stopitemize
 
-\subsubsection{Argument extraction}
+\subsubsection{Argument simplification}
 This transform deals with arguments to functions that
-are of a runtime representable type. 
+are of a runtime representable type. It ensures that they will all become
+references to global variables, or local signals in the resulting \small{VHDL}. 
 
 TODO: It seems we can map an expression to a port, not only a signal.
 Perhaps this makes this transformation not needed?
@@ -454,16 +1028,21 @@ a new let expression around the application, which binds the complex
 expression to a new variable. The original function is then applied to
 this variable.
 
-%\transform{Argument extract}
-%{
-%\lam{Y} is of a hardware representable type
-%
-%\lam{Y} is not a variable referene
-%
-%\conclusion
-%
-%\trans{X Y}{let z = Y in X z}
-%}
+\starttrans
+M N
+--------------------    \lam{N} is of a representable type
+let x = N in M x        \lam{N} is not a local variable reference
+\stoptrans
+
+\startbuffer[from]
+add (add a 1) 1
+\stopbuffer
+
+\startbuffer[to]
+let x = add a 1 in add x 1
+\stopbuffer
+
+\transexample{Argument extraction}{from}{to}
 
 \subsubsection{Function extraction}
 This transform deals with function-typed arguments to builtin functions.
@@ -475,24 +1054,36 @@ parameters to the new global function. The original argument is replaced
 with a reference to the new function, applied to any free variables from
 the original argument.
 
-%\transform{Function extraction}
-%{
-%\lam{X} is a (partial application of) a builtin function
-%
-%\lam{Y} is not an application
-%
-%\lam{Y} is not a variable reference
-%
-%\conclusion
-%
-%\lam{f0 ... fm} = free local vars of \lam{Y}
-%
-%\lam{y} is a new global variable
-%
-%\lam{y = λf0 ... fn.Y}
-%
-%\trans{X Y}{X (y f0 ... fn)}
-%}
+This transformation is useful when applying higher order builtin functions
+like \hs{map} to a lambda abstraction, for example. In this case, the code
+that generates \small{VHDL} for \hs{map} only needs to handle top level functions and
+partial applications, not any other expression (such as lambda abstractions or
+even more complicated expressions).
+
+\starttrans
+M N                     \lam{M} is a (partial aplication of a) builtin function.
+---------------------   \lam{f0 ... fn} = free local variables of \lam{N}
+M x f0 ... fn           \lam{N :: a -> b}
+~                       \lam{N} is not a (partial application of) a top level function
+x = λf0 ... λfn.N
+\stoptrans
+
+\startbuffer[from]
+map (λa . add a b) xs
+
+map (add b) ys
+\stopbuffer
+
+\startbuffer[to]
+x0 = λb.λa.add a b
+~
+map x0 xs
+
+x1 = λb.add b
+map x1 ys
+\stopbuffer
+
+\transexample{Function extraction}{from}{to}
 
 \subsubsection{Argument propagation}
 This transform deals with arguments to user-defined functions that are
@@ -532,278 +1123,67 @@ cannot be brought into normal form by this transform. We rely on an
 inlining transformation to replace such a variable with an expression we
 can propagate again.
 
-TODO: Move these definitions somewhere sensible.
-
-Definition: A global variable is any variable that is bound at the
-top level of a program. A local variable is any other variable.
-
-Definition: A hardware representable type is a type that we can generate
-a signal for in hardware. For example, a bit, a vector of bits, a 32 bit
-unsigned word, etc. Types that are not runtime representable notably
-include (but are not limited to): Types, dictionaries, functions.
-
-Definition: A builtin function is a function for which a builtin
-hardware translation is available, because its actual definition is not
-translatable. A user-defined function is any other function.
-
 \starttrans
 x = E
 ~
 x Y0 ... Yi ... Yn                               \lam{Yi} is not of a runtime representable type
 ---------------------------------------------    \lam{Yi} is not a local variable reference
-x' = λy0 ... yi-1 f0 ... fm yi+1 ... yn .        \lam{f0 ... fm} = free local vars of \lam{Y_i}
-      E y0 ... yi-1 Yi yi+1 ... yn   
+x' y0 ... yi-1 f0 ...  fm Yi+1 ... Yn            \lam{f0 ... fm} = free local vars of \lam{Yi}
 ~
-x' y0 ... yi-1 f0 ...  fm Yi+1 ... Yn
+x' = λy0 ... yi-1 f0 ... fm yi+1 ... yn .       
+      E y0 ... yi-1 Yi yi+1 ... yn   
+
 \stoptrans
 
+TODO: Example
+
 \subsection{Cast propagation / simplification}
-This transform pushes casts down into the expression as far as possible.
+This transform pushes casts down into the expression as far as possible. Since
+its exact role and need is not clear yet, this transformation is not yet
+specified.
 
 \subsection{Return value simplification}
-Currently implemented using lambda simplification, let simplification, and
-top simplification. Should change.
-
-\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:
+This transformation ensures that the return value of a function is always a
+simple local variable reference.
 
-\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:
+Currently implemented using lambda simplification, let simplification, and
+top simplification. Should change into something like the following, which
+works only on the result of a function instead of any subexpression. This is
+achieved by the contexts, like \lam{x = E}, though this is strictly not
+correct (you could read this as "if there is any function \lam{x} that binds
+\lam{E}, any \lam{E} can be transformed, while we only mean the \lam{E} that
+is bound by \lam{x}. This might need some extra notes or something).
 
-\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
+\starttrans
+x = 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
+let x = E in x
+\stoptrans
 
-After case removal:
+\starttrans
+x = λv0 ... λvn.E
+~                                \lam{E} is representable
+E                                \lam{E} is not a let expression
+---------------------------      \lam{E} is not a local variable reference
+let x = E in x
+\stoptrans
 
-\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
+\starttrans
+x = λv0 ... λvn.let ... in E
+~                                \lam{E} is representable
+E                                \lam{E} is not a local variable reference
+---------------------------
+let x = E in x
+\stoptrans
 
-After let bind removal:
+\startbuffer[from]
+x = add 1 2
+\stopbuffer
 
-\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
+\startbuffer[to]
+x = let x = add 1 2 in x
+\stopbuffer
 
-Application simplification is not applicable.
+\transexample{Return value simplification}{from}{to}