Add a section on research goals and an outline.

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

diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex
index a8194decdf2826b8c9677989754dcd4e3c78fa25..68d48d4eeebf1511647d7939726d16dfa856cf60 100644 (file)
--- a/Chapters/Normalization.tex
+++ b/Chapters/Normalization.tex
@@ -52,39 +52,169 @@ while fully preserving the semantics of the program.
 
 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
 
 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.
+produce a number of nested let expressions. These let expressions binds a
+number of simple expressions in the function and produces a simple identifier.
+Every bound value in the let expression is either a simple function
+application, a case expression to extract a single element from a tuple
+returned by a function or a case expression to choose between two signals
+based on some other signal.
+
+This structure is easy to translate to VHDL, since each top level lambda will
+be an input port, every bound value will become a concurrent statement (such
+as a component instantiation or conditional signal assignment) and the result
+variable will become the output port.

 
 An example of a program in canonical form would be:
 
 \startlambda
   -- All arguments are an inital lambda
 
 An example of a program in canonical form would be:
 
 \startlambda
   -- All arguments are an inital lambda

-  λx.λc.λd.
-  -- There is one let expression at the top level
+  λa.λd.λsp.
+  -- There are nested let expressions at top level

   let
   let

+    -- Unpack the state by coercion
+    s = sp :: (Word, Word)
+    -- Extract both registers from the state
+    r1 = case s of (fst, snd) -> fst
+    r2 = case s of (fst, snd) -> snd

     -- Calling some other user-defined function.
     -- Calling some other user-defined function.

-    s = foo x
-    -- Extracting result values from a tuple
-    a = case s of (a, b) -> a
-    b = case s of (a, b) -> b
-    -- Some builtin expressions
-    rh = add c d
-    rhh = sub d c
+    d' = foo d

     -- Conditional connections
     -- Conditional connections

-    rl = case b of
-      High -> rhh
+    out = case a of
+      High -> r1
+      Low -> r2
+    r1' = case a of
+      High -> d
+      Low -> r1
+    r2' = case a of
+      High -> r2

       Low -> d
       Low -> d

-    r = case a of
-      High -> rh
-      Low -> rl
+    -- Packing a tuple
+    s' = (,) r1' r2'
+    -- Packing the state by coercion
+    sp' = s' :: State (Word, Word)
+    -- Pack our return value
+    res = (,) sp' out

   in
     -- The actual result
   in
     -- The actual result

-    r
+    res

 \stoplambda
 
 \stoplambda
 

+\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:
+
+\starttrans
+context conditions
+~
+from
+------------------------            expression conditions
+to
+~
+context additions
+\stoptrans
+
+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.
+
+The \lam{expression conditions} list a number of conditions on the \lam{from}
+expression that must hold for the transformation to apply.
+
+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.
+
+\subsection{Normal form definition}
+We can describe this normal form 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(var))
+                | \italic{toplet} 
+\italic{toplet} = let \italic{binding} in \italic{toplet} 
+                | letrec [\italic{binding}] in \italic{toplet}
+                | var (representable(varvar))
+\italic{binding} = var = \italic{rhs} (representable(rhs))
+                 -- State packing and unpacking by coercion
+                 | 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 (lvar(var))
+             -- Selector case
+             | 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 (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: Limit builtinarg further
+
+-- TODO: There can still be other casts around (which the code can handle,
+e.g., ignore), which still need to be documented here.
+
+-- TODO: Note about the selector case. It just supports Bit and Bool
+currently, perhaps it should be generalized in the normal form?
+

 When looking at such a program from a hardware perspective, the top level
 lambda's define the input ports. The value produced by the let expression is
 the output port. Most function applications bound by the let expression
 When looking at such a program from a hardware perspective, the top level
 lambda's define the input ports. The value produced by the let expression is
 the output port. Most function applications bound by the let expression


@@ -94,53 +224,7 @@ construction (\eg the \lam{case} statement) or call a builtin function
 (\eg \lam{add} or \lam{sub}). For these, a hardcoded VHDL translation is
 available.
 
 (\eg \lam{add} or \lam{sub}). For these, a hardcoded 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
-
-TODO: Say something about uniqueness of identifiers
-
-\subsection{Builtin expressions}
-A $builtinexpr$, as defined at \in[builtinexpr] can have any of the following forms.
-
-\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
-

 \section{Transform passes}
 \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.
 
 In this section we describe the actual transforms. Here we're using
 the core language in a notation that resembles lambda calculus.
 


@@ -175,13 +259,13 @@ E                 \lam{E :: * -> *}
 \stoptrans
 
 \startbuffer[from]
 \stoptrans
 
 \startbuffer[from]

-foo = λa -> case a of 
+foo = λa.case a of 

   True -> λb.mul b b
   False -> id
 \stopbuffer
 
 \startbuffer[to]
   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
     True -> λb.mul b b
     False -> λy.id y) x
 \stopbuffer


@@ -194,41 +278,44 @@ into expressions as far as possible. In lambda calculus, this reduction
 is known as β-reduction, but it is of course only defined for
 applications of lambda abstractions. We extend this reduction to also
 work for the rest of core (case and let expressions).
 is known as β-reduction, but it is of course only defined for
 applications of lambda abstractions. We extend this reduction to also
 work for the rest of core (case and let expressions).

-\startbuffer[from]
+
+For let expressions:
+\starttrans
+let binds in E) M
+-----------------
+let binds in E M
+\stoptrans
+
+For case statements:
+\starttrans

 (case x of
   p1 -> E1
   \vdots
   pn -> En) M
 (case x of
   p1 -> E1
   \vdots
   pn -> En) M

-\stopbuffer
-\startbuffer[to]
+-----------------

 case x of
   p1 -> E1 M
   \vdots
   pn -> En M
 case x of
   p1 -> E1 M
   \vdots
   pn -> En M

-\stopbuffer
+\stoptrans

 
 

-%\transform{Extended β-reduction}
-%{
-%\conclusion
-%\trans{(λx.E) M}{E[M/x]}
-%
-%\nextrule
-%\conclusion
-%\trans{(let binds in E) M}{let binds in E M}
-%
-%\nextrule
-%\conclusion
-%\transbuf{from}{to}
-%}
+For lambda expressions:
+\starttrans
+(λx.E) M
+-----------------
+E[M/x]
+\stoptrans

 
 

+% And an example

 \startbuffer[from]
 \startbuffer[from]

-let a = (case x of 
-           True -> id
-           False -> neg
-        ) 1
-    b = (let y = 3 in add y) 2
-in
-  (λz.add 1 z) 3
+( let a = (case x of 
+            True -> id
+            False -> neg
+          ) 1
+      b = (let y = 3 in add y) 2
+  in
+    (λz.add 1 z)
+) 3

 \stopbuffer
 
 \startbuffer[to]
 \stopbuffer
 
 \startbuffer[to]


@@ -242,6 +329,339 @@ in
 
 \transexample{Extended β-reduction}{from}{to}
 
 
 \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 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 transformation inlines simple let bindings (\eg a = b).
+
+This transformation is not needed to get into normal form, but makes the
+resulting 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 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:
 \subsection{Argument simplification}
 The transforms in this section deal with simplifying application
 arguments into normal form. The goal here is to:


@@ -249,8 +669,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
 \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.
    \startitemize
     \item A type argument.
     \item A dictionary argument.


@@ -278,8 +699,23 @@ divide them into two categories:
         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.
         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
 
 \stopitemize
 

+TODO: Check the following itemization.
+

 When looking at the arguments of a builtin function, we can divide them
 into categories: 
 
 When looking at the arguments of a builtin function, we can divide them
 into categories: 
 


@@ -362,9 +798,10 @@ into categories:
         categories instead.
 \stopitemize
 
         categories instead.
 \stopitemize
 

-\subsubsection{Argument extraction}
+\subsubsection{Argument simplification}

 This transform deals with arguments to functions that
 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 VHDL. 

 
 TODO: It seems we can map an expression to a port, not only a signal.
 Perhaps this makes this transformation not needed?
 
 TODO: It seems we can map an expression to a port, not only a signal.
 Perhaps this makes this transformation not needed?


@@ -377,16 +814,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.
 
 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.
 
 \subsubsection{Function extraction}
 This transform deals with function-typed arguments to builtin functions.


@@ -398,24 +840,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.
 
 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 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
 
 \subsubsection{Argument propagation}
 This transform deals with arguments to user-defined functions that are


@@ -455,327 +909,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.
 
 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
 ~
 \starttrans
 x = E
 ~

-x Y0 ... Yi ... Yn                               \lam{Y_i} is not of a runtime representable type
----------------------------------------------    \lam{Y_i} 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 ... 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
-\stoptrans
-
-%\transform{Argument propagation}
-%{
-%\lam{x} is a global variable, bound to a user-defined function
-%
-%\lam{x = E}
-%
-%\lam{Y_i} is not of a runtime representable type
-%
-%\lam{Y_i} is not a local variable reference
-%
-%\conclusion
-%
-%\lam{f0 ... fm} = free local vars of \lam{Y_i}
-%
-%\lam{x'} is a new global variable
-%
-%\lam{x' = λy0 ... yi-1 f0 ... fm yi+1 ... yn . E y0 ... yi-1 Yi yi+1 ... yn}
-%
-%\trans{x Y0 ... Yi ... Yn}{x' y0 ... yi-1 f0 ... fm Yi+1 ... Yn}
-%}
-%
-%TODO: The above definition looks too complicated... Can we find
-%something more concise?
-
-\subsection{Cast propagation}
-This transform pushes casts down into the expression as far as possible.
-\subsection{Let recursification}
-This transform makes all lets recursive.
-\subsection{Let simplification}
-This transform makes the result value of all let expressions a simple
-variable reference.
-\subsection{Let flattening}
-This transform turns two nested lets (\lam{let x = (let ... in ...) in
-...}) into a single let.
-\subsection{Simple let binding removal}
-This transforms inlines simple let bindings (\eg a = b).
-\subsection{Function 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.
-\subsection{Scrutinee simplification}
-This transform ensures that the scrutinee of a case expression is always
-a simple variable reference.
-\subsection{Case binder wildening}
-This transform replaces all binders of a each case alternative with a
-wild binder (\ie, one that is never referred to). This will possibly
-introduce a number of new "selector" case statements, that only select
-one element from an algebraic datatype and bind it to a variable.
-\subsection{Case value simplification}
-This transform simplifies the result value of each case alternative by
-binding the value in a let expression and replacing the value by a
-simple variable reference.
-\subsection{Case removal}
-This transform removes any case statements with a single alternative and
-only wild binders.
-
-\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
+x' = λy0 ... yi-1 f0 ... fm yi+1 ... yn .       
+      E y0 ... yi-1 Yi yi+1 ... yn   

 
 

-After function inlining:
+\stoptrans

 
 

-\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
+TODO: Example

 
 

-After (extended) β-reduction again:
+\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.

 
 

-\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
+\subsection{Return value simplification}
+This transformation ensures that the return value of a function is always a
+simple local variable reference.

 
 

-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}