M
-----------------
let
- \vdots
- \vdots
+ \vdots [b/a]
+ \vdots [b/a]
in
M[b/a]
\stoptrans
\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:
\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.
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:
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?
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.
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
~
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}
projects / matthijs / master-project / report.git / commitdiff