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

diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex
index 059ba43..1f9f62b 100644
--- a/Chapters/Normalization.tex
+++ b/Chapters/Normalization.tex
@@ -52,11 +52,17 @@ 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
-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:
 
@@ -93,36 +99,114 @@ An example of a program in canonical form would be:
     res
 \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(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,
@@ -140,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.
 
-\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}
-
 In this section we describe the actual transforms. Here we're using
 the core language in a notation that resembles lambda calculus.
 
@@ -221,13 +259,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
@@ -397,8 +435,8 @@ in
   M
 -----------------
 let
-  \vdots
-  \vdots
+  \vdots [b/a]
+  \vdots [b/a]
 in
   M[b/a]
 \stoptrans
@@ -435,20 +473,195 @@ in
 \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:
@@ -456,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
- 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.
@@ -485,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.
+
+        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: 
 
@@ -569,9 +798,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 VHDL. 
 
 TODO: It seems we can map an expression to a port, not only a signal.
 Perhaps this makes this transformation not needed?
@@ -584,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.
 
-%\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.
@@ -605,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.
 
-%\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
@@ -662,37 +909,70 @@ 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}
+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.
+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{Example sequence}