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
projects / matthijs / master-project / report.git / commitdiff