Reshuffle all transformations into categories.
authorMatthijs Kooijman <matthijs@stdin.nl>
Mon, 2 Nov 2009 11:14:15 +0000 (12:14 +0100)
committerMatthijs Kooijman <matthijs@stdin.nl>
Mon, 2 Nov 2009 11:26:21 +0000 (12:26 +0100)
This changes no text, only ordering and indentation. Transformation are
now put into a few categories (which still need an introductory text).

Chapters/Normalization.tex

index 17a37c6..3356a4f 100644 (file)
@@ -753,765 +753,779 @@ is specified as a number of conditions (above the horizontal line) and a
 number of conclusions (below the horizontal line). The details of using
 this notation are still a bit fuzzy, so comments are welcom.
 
-\subsection{η-abstraction}
-This transformation makes sure that all arguments of a function-typed
-expression are named, by introducing lambda expressions. When combined with
-β-reduction and function inlining below, all function-typed expressions should
-be lambda abstractions or global identifiers.
-
-\starttrans
-E                 \lam{E :: a -> b}
---------------    \lam{E} is not the first argument of an application.
-λx.E x            \lam{E} is not a lambda abstraction.
-                  \lam{x} is a variable that does not occur free in \lam{E}.
-\stoptrans
-
-\startbuffer[from]
-foo = λa.case a of 
-  True -> λb.mul b b
-  False -> id
-\stopbuffer
-
-\startbuffer[to]
-foo = λa.λx.(case a of 
-    True -> λb.mul b b
-    False -> λy.id y) x
-\stopbuffer
-
-\transexample{η-abstraction}{from}{to}
-
-\subsection{β-reduction}
-β-reduction is a well known transformation from lambda calculus, where it is
-the main reduction step. It reduces applications of labmda abstractions,
-removing both the lambda abstraction and the application.
-
-In our transformation system, this step helps to remove unwanted lambda
-abstractions (basically all but the ones at the top level). Other
-transformations (application propagation, non-representable inlining) make
-sure that most lambda abstractions will eventually be reducable by
-β-reduction.
-
-TODO: Define substitution syntax
-
-\starttrans
-(λx.E) M
------------------
-E[M/x]
-\stoptrans
-
-% And an example
-\startbuffer[from]
-(λa. 2 * a) (2 * b)
-\stopbuffer
-
-\startbuffer[to]
-2 * (2 * b)
-\stopbuffer
-
-\transexample{β-reduction}{from}{to}
-
-\subsection{Application propagation}
-This transformation is meant to propagate application expressions downwards
-into expressions as far as possible. This allows partial applications inside
-expressions to become fully applied and exposes new transformation
-possibilities for other transformations (like β-reduction).
-
-\starttrans
-let binds in E) M
------------------
-let binds in E M
-\stoptrans
-
-% And an example
-\startbuffer[from]
-( let 
-    val = 1
-  in 
-    add val
-) 3
-\stopbuffer
-
-\startbuffer[to]
-let 
-  val = 1
-in 
-  add val 3
-\stopbuffer
-
-\transexample{Application propagation for a let expression}{from}{to}
-
-\starttrans
-(case x of
-  p1 -> E1
-  \vdots
-  pn -> En) M
------------------
-case x of
-  p1 -> E1 M
-  \vdots
-  pn -> En M
-\stoptrans
-
-% And an example
-\startbuffer[from]
-( case x of 
-    True -> id
-    False -> neg
-) 1
-\stopbuffer
-
-\startbuffer[to]
-case x of 
-  True -> id 1
-  False -> neg 1
-\stopbuffer
-
-\transexample{Application propagation for a case expression}{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 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
-rederecursification 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 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 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:
-
-\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. 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.
-    \item A type level expression.
-    \item A variable reference of a runtime representable type.
-    \item A variable reference or partial application of a function type.
-   \stopitemize
-\stopitemize
-
-When looking at the arguments of a user-defined function, we can
-divide them into two categories:
-\startitemize
-  \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
-        only connect signals to input ports, these arguments must be
-        reduced to simple variables (for which signals will be
-        produced). This is taken care of by the argument extraction
-        transform.
-  \item Non-runtime representable typed arguments.
-        
-        These arguments cannot be preserved in the program, since we
-        cannot represent them as input or output ports in the resulting
-        \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 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
-        argument extraction transform. Performing this transform for
-        builtin functions as well, means that the translation of builtin
-        functions can be limited to signal references, instead of
-        needing to support all possible expressions.
-
-  \item Arguments of a function type.
-        
-        These arguments are functions passed to higher order builtins,
-        like \lam{map} and \lam{foldl}. Since implementing these
-        functions for arbitrary function-typed expressions (\eg, lambda
-        expressions) is rather comlex, we reduce these arguments to
-        (partial applications of) global functions.
-        
-        We can still support arbitrary expressions from the user code,
-        by creating a new global function containing that expression.
-        This way, we can simply replace the argument with a reference to
-        that new function. However, since the expression can contain any
-        number of free variables we also have to include partial
-        applications in our normal form.
-
-        This category of arguments is handled by the function extraction
-        transform.
-  \item Other unrepresentable arguments.
-        
-        These arguments can take a few different forms:
-        \startdesc{Type arguments}
-          In the core language, type arguments can only take a single
-          form: A type wrapped in the Type constructor. Also, there is
-          nothing that can be done with type expressions, except for
-          applying functions to them, so we can simply leave type
-          arguments as they are.
-        \stopdesc
-        \startdesc{Dictionary arguments}
-          In the core language, dictionary arguments are used to find
-          operations operating on one of the type arguments (mostly for
-          finding class methods). Since we will not actually evaluatie
-          the function body for builtin functions and can generate
-          code for builtin functions by just looking at the type
-          arguments, these arguments can be ignored and left as they
-          are.
-        \stopdesc
-        \startdesc{Type level arguments}
-          Sometimes, we want to pass a value to a builtin function, but
-          we need to know the value at compile time. Additionally, the
-          value has an impact on the type of the function. This is
-          encoded using type-level values, where the actual value of the
-          argument is not important, but the type encodes some integer,
-          for example. Since the value is not important, the actual form
-          of the expression does not matter either and we can leave
-          these arguments as they are.
-        \stopdesc
-        \startdesc{Other arguments}
-          Technically, there is still a wide array of arguments that can
-          be passed, but does not fall into any of the above categories.
-          However, none of the supported builtin functions requires such
-          an argument. This leaves use with passing unsupported types to
-          a function, such as calling \lam{head} on a list of functions.
-
-          In these cases, it would be impossible to generate hardware
-          for such a function call anyway, so we can ignore these
-          arguments.
-
-          The only way to generate hardware for builtin functions with
-          arguments like these, is to expand the function call into an
-          equivalent core expression (\eg, expand map into a series of
-          function applications). But for now, we choose to simply not
-          support expressions like these.
-        \stopdesc
-
-        From the above, we can conclude that we can simply ignore these
-        other unrepresentable arguments and focus on the first two
-        categories instead.
-\stopitemize
-
-\subsubsection{Argument simplification}
-This transform deals with arguments to functions that
-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?
-TODO: Say something about dataconstructors (without arguments, like True
-or False), which are variable references of a runtime representable
-type, but do not result in a signal.
-
-To reduce a complex expression to a simple variable reference, we create
-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.
-
-\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.
-Since these arguments cannot be propagated, we choose to extract them
-into a new global function instead.
-
-Any free variables occuring in the extracted arguments will become
-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.
-
-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
-not representable at runtime. This means these arguments cannot be
-preserved in the final form and most be {\em propagated}.
-
-Propagation means to create a specialized version of the called
-function, with the propagated argument already filled in. As a simple
-example, in the following program:
-
-\startlambda
-f = λa.λb.a + b
-inc = λa.f a 1
-\stoplambda
-
-we could {\em propagate} the constant argument 1, with the following
-result:
-
-\startlambda
-f' = λa.a + 1
-inc = λa.f' a
-\stoplambda
-
-Special care must be taken when the to-be-propagated expression has any
-free variables. If this is the case, the original argument should not be
-removed alltogether, but replaced by all the free variables of the
-expression. In this way, the original expression can still be evaluated
-inside the new function. Also, this brings us closer to our goal: All
-these free variables will be simple variable references.
-
-To prevent us from propagating the same argument over and over, a simple
-local variable reference is not propagated (since is has exactly one
-free variable, itself, we would only replace that argument with itself).
-
-This shows that any free local variables that are not runtime representable
-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.
-
-\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{Yi}
-~
-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. Since
-its exact role and need is not clear yet, this transformation is not yet
-specified.
-
-\subsection{Return value simplification}
-This transformation ensures that the return value of a function is always a
-simple local variable reference.
-
-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).
-
-\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
-
-\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
+  \subsection{General cleanup}
+
+    \subsubsection{β-reduction}
+      β-reduction is a well known transformation from lambda calculus, where it is
+      the main reduction step. It reduces applications of labmda abstractions,
+      removing both the lambda abstraction and the application.
+
+      In our transformation system, this step helps to remove unwanted lambda
+      abstractions (basically all but the ones at the top level). Other
+      transformations (application propagation, non-representable inlining) make
+      sure that most lambda abstractions will eventually be reducable by
+      β-reduction.
+
+      TODO: Define substitution syntax
+
+      \starttrans
+      (λx.E) M
+      -----------------
+      E[M/x]
+      \stoptrans
+
+      % And an example
+      \startbuffer[from]
+      (λa. 2 * a) (2 * b)
+      \stopbuffer
+
+      \startbuffer[to]
+      2 * (2 * b)
+      \stopbuffer
+
+      \transexample{β-reduction}{from}{to}
+
+    \subsubsection{Application propagation}
+      This transformation is meant to propagate application expressions downwards
+      into expressions as far as possible. This allows partial applications inside
+      expressions to become fully applied and exposes new transformation
+      possibilities for other transformations (like β-reduction).
+
+      \starttrans
+      let binds in E) M
+      -----------------
+      let binds in E M
+      \stoptrans
+
+      % And an example
+      \startbuffer[from]
+      ( let 
+          val = 1
+        in 
+          add val
+      ) 3
+      \stopbuffer
+
+      \startbuffer[to]
+      let 
+        val = 1
+      in 
+        add val 3
+      \stopbuffer
+
+      \transexample{Application propagation for a let expression}{from}{to}
+
+      \starttrans
+      (case x of
+        p1 -> E1
+        \vdots
+        pn -> En) M
+      -----------------
+      case x of
+        p1 -> E1 M
+        \vdots
+        pn -> En M
+      \stoptrans
+
+      % And an example
+      \startbuffer[from]
+      ( case x of 
+          True -> id
+          False -> neg
+      ) 1
+      \stopbuffer
+
+      \startbuffer[to]
+      case x of 
+        True -> id 1
+        False -> neg 1
+      \stopbuffer
+
+      \transexample{Application propagation for a case expression}{from}{to}
+
+    \subsubsection{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
+
+      \subsubsection{Simple let binding removal}
+      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
+
+    \subsubsection{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
+
+    \subsubsection{Cast propagation / simplification}
+      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.
+
+    \subsubsection{Compiler generated top level binding inlining}
+      TODO
+
+  \section{Program structure}
+
+    \subsubsection{η-abstraction}
+      This transformation makes sure that all arguments of a function-typed
+      expression are named, by introducing lambda expressions. When combined with
+      β-reduction and function inlining below, all function-typed expressions should
+      be lambda abstractions or global identifiers.
+
+      \starttrans
+      E                 \lam{E :: a -> b}
+      --------------    \lam{E} is not the first argument of an application.
+      λx.E x            \lam{E} is not a lambda abstraction.
+                        \lam{x} is a variable that does not occur free in \lam{E}.
+      \stoptrans
+
+      \startbuffer[from]
+      foo = λa.case a of 
+        True -> λb.mul b b
+        False -> id
+      \stopbuffer
+
+      \startbuffer[to]
+      foo = λa.λx.(case a of 
+          True -> λb.mul b b
+          False -> λy.id y) x
+      \stopbuffer
+
+      \transexample{η-abstraction}{from}{to}
+
+    \subsubsection{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?
+
+    \subsubsection{Let flattening}
+      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
+      rederecursification 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}
+
+    \subsubsection{Return value simplification}
+      This transformation ensures that the return value of a function is always a
+      simple local variable reference.
+
+      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).
+
+      \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
+
+      \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
+
+      \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
+
+      \startbuffer[from]
+      x = add 1 2
+      \stopbuffer
+
+      \startbuffer[to]
+      x = let x = add 1 2 in x
+      \stopbuffer
+
+      \transexample{Return value simplification}{from}{to}
+
+  \subsection{Argument simplification}
+    The transforms in this section deal with simplifying application
+    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. 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.
+        \item A type level expression.
+        \item A variable reference of a runtime representable type.
+        \item A variable reference or partial application of a function type.
+       \stopitemize
+    \stopitemize
 
-\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
+    When looking at the arguments of a user-defined function, we can
+    divide them into two categories:
+    \startitemize
+      \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
+            only connect signals to input ports, these arguments must be
+            reduced to simple variables (for which signals will be
+            produced). This is taken care of by the argument extraction
+            transform.
+      \item Non-runtime representable typed arguments.
+            
+            These arguments cannot be preserved in the program, since we
+            cannot represent them as input or output ports in the resulting
+            \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
 
-\startbuffer[from]
-x = add 1 2
-\stopbuffer
+    TODO: Check the following itemization.
+
+    When looking at the arguments of a builtin function, we can divide them
+    into categories: 
+
+    \startitemize
+      \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
+            argument extraction transform. Performing this transform for
+            builtin functions as well, means that the translation of builtin
+            functions can be limited to signal references, instead of
+            needing to support all possible expressions.
+
+      \item Arguments of a function type.
+            
+            These arguments are functions passed to higher order builtins,
+            like \lam{map} and \lam{foldl}. Since implementing these
+            functions for arbitrary function-typed expressions (\eg, lambda
+            expressions) is rather comlex, we reduce these arguments to
+            (partial applications of) global functions.
+            
+            We can still support arbitrary expressions from the user code,
+            by creating a new global function containing that expression.
+            This way, we can simply replace the argument with a reference to
+            that new function. However, since the expression can contain any
+            number of free variables we also have to include partial
+            applications in our normal form.
+
+            This category of arguments is handled by the function extraction
+            transform.
+      \item Other unrepresentable arguments.
+            
+            These arguments can take a few different forms:
+            \startdesc{Type arguments}
+              In the core language, type arguments can only take a single
+              form: A type wrapped in the Type constructor. Also, there is
+              nothing that can be done with type expressions, except for
+              applying functions to them, so we can simply leave type
+              arguments as they are.
+            \stopdesc
+            \startdesc{Dictionary arguments}
+              In the core language, dictionary arguments are used to find
+              operations operating on one of the type arguments (mostly for
+              finding class methods). Since we will not actually evaluatie
+              the function body for builtin functions and can generate
+              code for builtin functions by just looking at the type
+              arguments, these arguments can be ignored and left as they
+              are.
+            \stopdesc
+            \startdesc{Type level arguments}
+              Sometimes, we want to pass a value to a builtin function, but
+              we need to know the value at compile time. Additionally, the
+              value has an impact on the type of the function. This is
+              encoded using type-level values, where the actual value of the
+              argument is not important, but the type encodes some integer,
+              for example. Since the value is not important, the actual form
+              of the expression does not matter either and we can leave
+              these arguments as they are.
+            \stopdesc
+            \startdesc{Other arguments}
+              Technically, there is still a wide array of arguments that can
+              be passed, but does not fall into any of the above categories.
+              However, none of the supported builtin functions requires such
+              an argument. This leaves use with passing unsupported types to
+              a function, such as calling \lam{head} on a list of functions.
+
+              In these cases, it would be impossible to generate hardware
+              for such a function call anyway, so we can ignore these
+              arguments.
+
+              The only way to generate hardware for builtin functions with
+              arguments like these, is to expand the function call into an
+              equivalent core expression (\eg, expand map into a series of
+              function applications). But for now, we choose to simply not
+              support expressions like these.
+            \stopdesc
+
+            From the above, we can conclude that we can simply ignore these
+            other unrepresentable arguments and focus on the first two
+            categories instead.
+    \stopitemize
 
-\startbuffer[to]
-x = let x = add 1 2 in x
-\stopbuffer
+    \subsubsection{Argument simplification}
+      This transform deals with arguments to functions that
+      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?
+      TODO: Say something about dataconstructors (without arguments, like True
+      or False), which are variable references of a runtime representable
+      type, but do not result in a signal.
+
+      To reduce a complex expression to a simple variable reference, we create
+      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.
+
+      \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.
+      Since these arguments cannot be propagated, we choose to extract them
+      into a new global function instead.
+
+      Any free variables occuring in the extracted arguments will become
+      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.
+
+      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
+      not representable at runtime. This means these arguments cannot be
+      preserved in the final form and most be {\em propagated}.
+
+      Propagation means to create a specialized version of the called
+      function, with the propagated argument already filled in. As a simple
+      example, in the following program:
+
+      \startlambda
+      f = λa.λb.a + b
+      inc = λa.f a 1
+      \stoplambda
+
+      we could {\em propagate} the constant argument 1, with the following
+      result:
+
+      \startlambda
+      f' = λa.a + 1
+      inc = λa.f' a
+      \stoplambda
+
+      Special care must be taken when the to-be-propagated expression has any
+      free variables. If this is the case, the original argument should not be
+      removed alltogether, but replaced by all the free variables of the
+      expression. In this way, the original expression can still be evaluated
+      inside the new function. Also, this brings us closer to our goal: All
+      these free variables will be simple variable references.
+
+      To prevent us from propagating the same argument over and over, a simple
+      local variable reference is not propagated (since is has exactly one
+      free variable, itself, we would only replace that argument with itself).
+
+      This shows that any free local variables that are not runtime representable
+      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.
+
+      \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{Yi}
+      ~
+      x' = λy0 ... yi-1 f0 ... fm yi+1 ... yn .       
+            E y0 ... yi-1 Yi yi+1 ... yn   
+
+      \stoptrans
+
+      TODO: Example
+
+  \subsection{Case simplification}
+    \subsubsection{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}
+
+
+    \subsubsection{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}
+
+    \subsubsection{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{Monomorphisation}
+  TODO: Better name for this section
+
+  Reference type-specialization (== argument propagation)
+
+\subsubsection{Defunctionalization}
+  Reference higher-order-specialization (== argument propagation)
+
+    \subsubsection{Non-representable binding inlining}
+      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}
 
-\transexample{Return value simplification}{from}{to}
 
 \section{Provable properties}
   When looking at the system of transformations outlined above, there are a