From f3a705e9d90ff0e54ef6bfec8db58947d7587704 Mon Sep 17 00:00:00 2001 From: Matthijs Kooijman Date: Mon, 2 Nov 2009 12:14:15 +0100 Subject: [PATCH] Reshuffle all transformations into categories. This changes no text, only ordering and indentation. Transformation are now put into a few categories (which still need an introductory text). --- Chapters/Normalization.tex | 1524 ++++++++++++++++++------------------ 1 file changed, 769 insertions(+), 755 deletions(-) diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex index 17a37c6..3356a4f 100644 --- a/Chapters/Normalization.tex +++ b/Chapters/Normalization.tex @@ -753,765 +753,779 @@ is specified as a number of conditions (above the horizontal line) and a number of conclusions (below the horizontal line). The details of using this notation are still a bit fuzzy, so comments are welcom. -\subsection{η-abstraction} -This transformation makes sure that all arguments of a function-typed -expression are named, by introducing lambda expressions. When combined with -β-reduction and function inlining below, all function-typed expressions should -be lambda abstractions or global identifiers. - -\starttrans -E \lam{E :: a -> b} --------------- \lam{E} is not the first argument of an application. -λx.E x \lam{E} is not a lambda abstraction. - \lam{x} is a variable that does not occur free in \lam{E}. -\stoptrans - -\startbuffer[from] -foo = λa.case a of - True -> λb.mul b b - False -> id -\stopbuffer - -\startbuffer[to] -foo = λa.λx.(case a of - True -> λb.mul b b - False -> λy.id y) x -\stopbuffer - -\transexample{η-abstraction}{from}{to} - -\subsection{β-reduction} -β-reduction is a well known transformation from lambda calculus, where it is -the main reduction step. It reduces applications of labmda abstractions, -removing both the lambda abstraction and the application. - -In our transformation system, this step helps to remove unwanted lambda -abstractions (basically all but the ones at the top level). Other -transformations (application propagation, non-representable inlining) make -sure that most lambda abstractions will eventually be reducable by -β-reduction. - -TODO: Define substitution syntax - -\starttrans -(λx.E) M ------------------ -E[M/x] -\stoptrans - -% And an example -\startbuffer[from] -(λa. 2 * a) (2 * b) -\stopbuffer - -\startbuffer[to] -2 * (2 * b) -\stopbuffer - -\transexample{β-reduction}{from}{to} - -\subsection{Application propagation} -This transformation is meant to propagate application expressions downwards -into expressions as far as possible. This allows partial applications inside -expressions to become fully applied and exposes new transformation -possibilities for other transformations (like β-reduction). - -\starttrans -let binds in E) M ------------------ -let binds in E M -\stoptrans - -% And an example -\startbuffer[from] -( let - val = 1 - in - add val -) 3 -\stopbuffer - -\startbuffer[to] -let - val = 1 -in - add val 3 -\stopbuffer - -\transexample{Application propagation for a let expression}{from}{to} - -\starttrans -(case x of - p1 -> E1 - \vdots - pn -> En) M ------------------ -case x of - p1 -> E1 M - \vdots - pn -> En M -\stoptrans - -% And an example -\startbuffer[from] -( case x of - True -> id - False -> neg -) 1 -\stopbuffer - -\startbuffer[to] -case x of - True -> id 1 - False -> neg 1 -\stopbuffer - -\transexample{Application propagation for a case expression}{from}{to} - -\subsection{Let derecursification} -This transformation is meant to make lets non-recursive whenever possible. -This might allow other optimizations to do their work better. TODO: Why is -this needed exactly? - -\subsection{Let flattening} -This transformation puts nested lets in the same scope, by lifting the -binding(s) of the inner let into a new let around the outer let. Eventually, -this will cause all let bindings to appear in the same scope (they will all be -in scope for the function return value). - -Note that this transformation does not try to be smart when faced with -recursive lets, it will just leave the lets recursive (possibly joining a -recursive and non-recursive let into a single recursive let). The let -rederecursification transformation will do this instead. - -\starttrans -letnonrec x = (let bindings in M) in N ------------------------------------------- -let bindings in (letnonrec x = M) in N -\stoptrans - -\starttrans -letrec - \vdots - x = (let bindings in M) - \vdots -in - N ------------------------------------------- -letrec - \vdots - bindings - x = M - \vdots -in - N -\stoptrans - -\startbuffer[from] -let - a = letrec - x = 1 - y = 2 - in - x + y -in - letrec - b = let c = 3 in a + c - d = 4 - in - d + b -\stopbuffer -\startbuffer[to] -letrec - x = 1 - y = 2 -in - let - a = x + y - in - letrec - c = 3 - b = a + c - d = 4 - in - d + b -\stopbuffer - -\transexample{Let flattening}{from}{to} - -\subsection{Empty let removal} -This transformation is simple: It removes recursive lets that have no bindings -(which usually occurs when let derecursification removes the last binding from -it). - -\starttrans -letrec in M --------------- -M -\stoptrans - -\subsection{Simple let binding removal} -This transformation inlines simple let bindings (\eg a = b). - -This transformation is not needed to get into normal form, but makes the -resulting \small{VHDL} a lot shorter. - -\starttrans -letnonrec - a = b -in - M ------------------ -M[b/a] -\stoptrans - -\starttrans -letrec - \vdots - a = b - \vdots -in - M ------------------ -let - \vdots [b/a] - \vdots [b/a] -in - M[b/a] -\stoptrans - -\subsection{Unused let binding removal} -This transformation removes let bindings that are never used. Usually, -the desugarer introduces some unused let bindings. - -This normalization pass should really be unneeded to get into normal form -(since ununsed bindings are not forbidden by the normal form), but in practice -the desugarer or simplifier emits some unused bindings that cannot be -normalized (e.g., calls to a \type{PatError} (TODO: Check this name)). Also, -this transformation makes the resulting \small{VHDL} a lot shorter. - -\starttrans -let a = E in M ----------------------------- \lam{a} does not occur free in \lam{M} -M -\stoptrans - -\starttrans -letrec - \vdots - a = E - \vdots -in - M ----------------------------- \lam{a} does not occur free in \lam{M} -letrec - \vdots - \vdots -in - M -\stoptrans - -\subsection{Non-representable binding inlining} -This transform inlines let bindings that have a non-representable type. Since -we can never generate a signal assignment for these bindings (we cannot -declare a signal assignment with a non-representable type, for obvious -reasons), we have no choice but to inline the binding to remove it. - -If the binding is non-representable because it is a lambda abstraction, it is -likely that it will inlined into an application and β-reduction will remove -the lambda abstraction and turn it into a representable expression at the -inline site. The same holds for partial applications, which can be turned into -full applications by inlining. - -Other cases of non-representable bindings we see in practice are primitive -Haskell types. In most cases, these will not result in a valid normalized -output, but then the input would have been invalid to start with. There is one -exception to this: When a builtin function is applied to a non-representable -expression, things might work out in some cases. For example, when you write a -literal \hs{SizedInt} in Haskell, like \hs{1 :: SizedInt D8}, this results in -the following core: \lam{fromInteger (smallInteger 10)}, where for example -\lam{10 :: GHC.Prim.Int\#} and \lam{smallInteger 10 :: Integer} have -non-representable types. TODO: This/these paragraph(s) should probably become a -separate discussion somewhere else. - -\starttrans -letnonrec a = E in M --------------------------- \lam{E} has a non-representable type. -M[E/a] -\stoptrans - -\starttrans -letrec - \vdots - a = E - \vdots -in - M --------------------------- \lam{E} has a non-representable type. -letrec - \vdots [E/a] - \vdots [E/a] -in - M[E/a] -\stoptrans - -\startbuffer[from] -letrec - a = smallInteger 10 - inc = λa -> add a 1 - inc' = add 1 - x = fromInteger a -in - inc (inc' x) -\stopbuffer - -\startbuffer[to] -letrec - x = fromInteger (smallInteger 10) -in - (λa -> add a 1) (add 1 x) -\stopbuffer - -\transexample{Let flattening}{from}{to} - -\subsection{Compiler generated top level binding inlining} -TODO - -\subsection{Scrutinee simplification} -This transform ensures that the scrutinee of a case expression is always -a simple variable reference. - -\starttrans -case E of - alts ------------------ \lam{E} is not a local variable reference -let x = E in - case E of - alts -\stoptrans - -\startbuffer[from] -case (foo a) of - True -> a - False -> b -\stopbuffer - -\startbuffer[to] -let x = foo a in - case x of - True -> a - False -> b -\stopbuffer - -\transexample{Let flattening}{from}{to} - - -\subsection{Case simplification} -This transformation ensures that all case expressions become normal form. This -means they will become one of: -\startitemize -\item An extractor case with a single alternative that picks a single field -from a datatype, \eg \lam{case x of (a, b) -> a}. -\item A selector case with multiple alternatives and only wild binders, that -makes a choice between expressions based on the constructor of another -expression, \eg \lam{case x of Low -> a; High -> b}. -\stopitemize - -\starttrans -case E of - C0 v0,0 ... v0,m -> E0 - \vdots - Cn vn,0 ... vn,m -> En ---------------------------------------------------- \forall i \forall j, 0 <= i <= n, 0 <= i < m (\lam{wi,j} is a wild (unused) binder) -letnonrec - v0,0 = case x of C0 v0,0 .. v0,m -> v0,0 - \vdots - v0,m = case x of C0 v0,0 .. v0,m -> v0,m - x0 = E0 - \dots - vn,m = case x of Cn vn,0 .. vn,m -> vn,m - xn = En -in - case E of - C0 w0,0 ... w0,m -> x0 - \vdots - Cn wn,0 ... wn,m -> xn -\stoptrans - -TODO: This transformation specified like this is complicated and misses -conditions to prevent looping with itself. Perhaps we should split it here for -discussion? - -\startbuffer[from] -case a of - True -> add b 1 - False -> add b 2 -\stopbuffer - -\startbuffer[to] -letnonrec - x0 = add b 1 - x1 = add b 2 -in - case a of - True -> x0 - False -> x1 -\stopbuffer - -\transexample{Selector case simplification}{from}{to} - -\startbuffer[from] -case a of - (,) b c -> add b c -\stopbuffer -\startbuffer[to] -letnonrec - b = case a of (,) b c -> b - c = case a of (,) b c -> c - x0 = add b c -in - case a of - (,) w0 w1 -> x0 -\stopbuffer - -\transexample{Extractor case simplification}{from}{to} - -\subsection{Case removal} -This transform removes any case statements with a single alternative and -only wild binders. - -These "useless" case statements are usually leftovers from case simplification -on extractor case (see the previous example). - -\starttrans -case x of - C v0 ... vm -> E ----------------------- \lam{\forall i, 0 <= i <= m} (\lam{vi} does not occur free in E) -E -\stoptrans - -\startbuffer[from] -case a of - (,) w0 w1 -> x0 -\stopbuffer - -\startbuffer[to] -x0 -\stopbuffer - -\transexample{Case removal}{from}{to} - -\subsection{Argument simplification} -The transforms in this section deal with simplifying application -arguments into normal form. The goal here is to: - -\startitemize - \item Make all arguments of user-defined functions (\eg, of which - we have a function body) simple variable references of a runtime - representable type. This is needed, since these applications will be turned - into component instantiations. - \item Make all arguments of builtin functions one of: - \startitemize - \item A type argument. - \item A dictionary argument. - \item A type level expression. - \item A variable reference of a runtime representable type. - \item A variable reference or partial application of a function type. - \stopitemize -\stopitemize - -When looking at the arguments of a user-defined function, we can -divide them into two categories: -\startitemize - \item Arguments of a runtime representable type (\eg bits or vectors). - - These arguments can be preserved in the program, since they can - be translated to input ports later on. However, since we can - only connect signals to input ports, these arguments must be - reduced to simple variables (for which signals will be - produced). This is taken care of by the argument extraction - transform. - \item Non-runtime representable typed arguments. - - These arguments cannot be preserved in the program, since we - cannot represent them as input or output ports in the resulting - \small{VHDL}. To remove them, we create a specialized version of the - called function with these arguments filled in. This is done by - the argument propagation transform. - - Typically, these arguments are type and dictionary arguments that are - used to make functions polymorphic. By propagating these arguments, we - are essentially doing the same which GHC does when it specializes - functions: Creating multiple variants of the same function, one for - each type for which it is used. Other common non-representable - arguments are functions, e.g. when calling a higher order function - with another function or a lambda abstraction as an argument. - - The reason for doing this is similar to the reasoning provided for - the inlining of non-representable let bindings above. In fact, this - argument propagation could be viewed as a form of cross-function - inlining. -\stopitemize - -TODO: Check the following itemization. - -When looking at the arguments of a builtin function, we can divide them -into categories: - -\startitemize - \item Arguments of a runtime representable type. - - As we have seen with user-defined functions, these arguments can - always be reduced to a simple variable reference, by the - argument extraction transform. Performing this transform for - builtin functions as well, means that the translation of builtin - functions can be limited to signal references, instead of - needing to support all possible expressions. - - \item Arguments of a function type. - - These arguments are functions passed to higher order builtins, - like \lam{map} and \lam{foldl}. Since implementing these - functions for arbitrary function-typed expressions (\eg, lambda - expressions) is rather comlex, we reduce these arguments to - (partial applications of) global functions. - - We can still support arbitrary expressions from the user code, - by creating a new global function containing that expression. - This way, we can simply replace the argument with a reference to - that new function. However, since the expression can contain any - number of free variables we also have to include partial - applications in our normal form. - - This category of arguments is handled by the function extraction - transform. - \item Other unrepresentable arguments. - - These arguments can take a few different forms: - \startdesc{Type arguments} - In the core language, type arguments can only take a single - form: A type wrapped in the Type constructor. Also, there is - nothing that can be done with type expressions, except for - applying functions to them, so we can simply leave type - arguments as they are. - \stopdesc - \startdesc{Dictionary arguments} - In the core language, dictionary arguments are used to find - operations operating on one of the type arguments (mostly for - finding class methods). Since we will not actually evaluatie - the function body for builtin functions and can generate - code for builtin functions by just looking at the type - arguments, these arguments can be ignored and left as they - are. - \stopdesc - \startdesc{Type level arguments} - Sometimes, we want to pass a value to a builtin function, but - we need to know the value at compile time. Additionally, the - value has an impact on the type of the function. This is - encoded using type-level values, where the actual value of the - argument is not important, but the type encodes some integer, - for example. Since the value is not important, the actual form - of the expression does not matter either and we can leave - these arguments as they are. - \stopdesc - \startdesc{Other arguments} - Technically, there is still a wide array of arguments that can - be passed, but does not fall into any of the above categories. - However, none of the supported builtin functions requires such - an argument. This leaves use with passing unsupported types to - a function, such as calling \lam{head} on a list of functions. - - In these cases, it would be impossible to generate hardware - for such a function call anyway, so we can ignore these - arguments. - - The only way to generate hardware for builtin functions with - arguments like these, is to expand the function call into an - equivalent core expression (\eg, expand map into a series of - function applications). But for now, we choose to simply not - support expressions like these. - \stopdesc - - From the above, we can conclude that we can simply ignore these - other unrepresentable arguments and focus on the first two - categories instead. -\stopitemize - -\subsubsection{Argument simplification} -This transform deals with arguments to functions that -are of a runtime representable type. It ensures that they will all become -references to global variables, or local signals in the resulting \small{VHDL}. - -TODO: It seems we can map an expression to a port, not only a signal. -Perhaps this makes this transformation not needed? -TODO: Say something about dataconstructors (without arguments, like True -or False), which are variable references of a runtime representable -type, but do not result in a signal. - -To reduce a complex expression to a simple variable reference, we create -a new let expression around the application, which binds the complex -expression to a new variable. The original function is then applied to -this variable. - -\starttrans -M N --------------------- \lam{N} is of a representable type -let x = N in M x \lam{N} is not a local variable reference -\stoptrans - -\startbuffer[from] -add (add a 1) 1 -\stopbuffer - -\startbuffer[to] -let x = add a 1 in add x 1 -\stopbuffer - -\transexample{Argument extraction}{from}{to} - -\subsubsection{Function extraction} -This transform deals with function-typed arguments to builtin functions. -Since these arguments cannot be propagated, we choose to extract them -into a new global function instead. - -Any free variables occuring in the extracted arguments will become -parameters to the new global function. The original argument is replaced -with a reference to the new function, applied to any free variables from -the original argument. - -This transformation is useful when applying higher order builtin functions -like \hs{map} to a lambda abstraction, for example. In this case, the code -that generates \small{VHDL} for \hs{map} only needs to handle top level functions and -partial applications, not any other expression (such as lambda abstractions or -even more complicated expressions). - -\starttrans -M N \lam{M} is a (partial aplication of a) builtin function. ---------------------- \lam{f0 ... fn} = free local variables of \lam{N} -M x f0 ... fn \lam{N :: a -> b} -~ \lam{N} is not a (partial application of) a top level function -x = λf0 ... λfn.N -\stoptrans - -\startbuffer[from] -map (λa . add a b) xs - -map (add b) ys -\stopbuffer - -\startbuffer[to] -x0 = λb.λa.add a b -~ -map x0 xs - -x1 = λb.add b -map x1 ys -\stopbuffer - -\transexample{Function extraction}{from}{to} - -\subsubsection{Argument propagation} -This transform deals with arguments to user-defined functions that are -not representable at runtime. This means these arguments cannot be -preserved in the final form and most be {\em propagated}. - -Propagation means to create a specialized version of the called -function, with the propagated argument already filled in. As a simple -example, in the following program: - -\startlambda -f = λa.λb.a + b -inc = λa.f a 1 -\stoplambda - -we could {\em propagate} the constant argument 1, with the following -result: - -\startlambda -f' = λa.a + 1 -inc = λa.f' a -\stoplambda - -Special care must be taken when the to-be-propagated expression has any -free variables. If this is the case, the original argument should not be -removed alltogether, but replaced by all the free variables of the -expression. In this way, the original expression can still be evaluated -inside the new function. Also, this brings us closer to our goal: All -these free variables will be simple variable references. - -To prevent us from propagating the same argument over and over, a simple -local variable reference is not propagated (since is has exactly one -free variable, itself, we would only replace that argument with itself). - -This shows that any free local variables that are not runtime representable -cannot be brought into normal form by this transform. We rely on an -inlining transformation to replace such a variable with an expression we -can propagate again. - -\starttrans -x = E -~ -x Y0 ... Yi ... Yn \lam{Yi} is not of a runtime representable type ---------------------------------------------- \lam{Yi} is not a local variable reference -x' y0 ... yi-1 f0 ... fm Yi+1 ... Yn \lam{f0 ... fm} = free local vars of \lam{Yi} -~ -x' = λy0 ... yi-1 f0 ... fm yi+1 ... yn . - E y0 ... yi-1 Yi yi+1 ... yn - -\stoptrans - -TODO: Example - -\subsection{Cast propagation / simplification} -This transform pushes casts down into the expression as far as possible. Since -its exact role and need is not clear yet, this transformation is not yet -specified. - -\subsection{Return value simplification} -This transformation ensures that the return value of a function is always a -simple local variable reference. - -Currently implemented using lambda simplification, let simplification, and -top simplification. Should change into something like the following, which -works only on the result of a function instead of any subexpression. This is -achieved by the contexts, like \lam{x = E}, though this is strictly not -correct (you could read this as "if there is any function \lam{x} that binds -\lam{E}, any \lam{E} can be transformed, while we only mean the \lam{E} that -is bound by \lam{x}. This might need some extra notes or something). - -\starttrans -x = E \lam{E} is representable -~ \lam{E} is not a lambda abstraction -E \lam{E} is not a let expression ---------------------------- \lam{E} is not a local variable reference -let x = E in x -\stoptrans - -\starttrans -x = λv0 ... λvn.E -~ \lam{E} is representable -E \lam{E} is not a let expression ---------------------------- \lam{E} is not a local variable reference -let x = E in x -\stoptrans + \subsection{General cleanup} + + \subsubsection{β-reduction} + β-reduction is a well known transformation from lambda calculus, where it is + the main reduction step. It reduces applications of labmda abstractions, + removing both the lambda abstraction and the application. + + In our transformation system, this step helps to remove unwanted lambda + abstractions (basically all but the ones at the top level). Other + transformations (application propagation, non-representable inlining) make + sure that most lambda abstractions will eventually be reducable by + β-reduction. + + TODO: Define substitution syntax + + \starttrans + (λx.E) M + ----------------- + E[M/x] + \stoptrans + + % And an example + \startbuffer[from] + (λa. 2 * a) (2 * b) + \stopbuffer + + \startbuffer[to] + 2 * (2 * b) + \stopbuffer + + \transexample{β-reduction}{from}{to} + + \subsubsection{Application propagation} + This transformation is meant to propagate application expressions downwards + into expressions as far as possible. This allows partial applications inside + expressions to become fully applied and exposes new transformation + possibilities for other transformations (like β-reduction). + + \starttrans + let binds in E) M + ----------------- + let binds in E M + \stoptrans + + % And an example + \startbuffer[from] + ( let + val = 1 + in + add val + ) 3 + \stopbuffer + + \startbuffer[to] + let + val = 1 + in + add val 3 + \stopbuffer + + \transexample{Application propagation for a let expression}{from}{to} + + \starttrans + (case x of + p1 -> E1 + \vdots + pn -> En) M + ----------------- + case x of + p1 -> E1 M + \vdots + pn -> En M + \stoptrans + + % And an example + \startbuffer[from] + ( case x of + True -> id + False -> neg + ) 1 + \stopbuffer + + \startbuffer[to] + case x of + True -> id 1 + False -> neg 1 + \stopbuffer + + \transexample{Application propagation for a case expression}{from}{to} + + \subsubsection{Empty let removal} + This transformation is simple: It removes recursive lets that have no bindings + (which usually occurs when let derecursification removes the last binding from + it). + + \starttrans + letrec in M + -------------- + M + \stoptrans + + \subsubsection{Simple let binding removal} + This transformation inlines simple let bindings (\eg a = b). + + This transformation is not needed to get into normal form, but makes the + resulting \small{VHDL} a lot shorter. + + \starttrans + letnonrec + a = b + in + M + ----------------- + M[b/a] + \stoptrans + + \starttrans + letrec + \vdots + a = b + \vdots + in + M + ----------------- + let + \vdots [b/a] + \vdots [b/a] + in + M[b/a] + \stoptrans + + \subsubsection{Unused let binding removal} + This transformation removes let bindings that are never used. Usually, + the desugarer introduces some unused let bindings. + + This normalization pass should really be unneeded to get into normal form + (since ununsed bindings are not forbidden by the normal form), but in practice + the desugarer or simplifier emits some unused bindings that cannot be + normalized (e.g., calls to a \type{PatError} (TODO: Check this name)). Also, + this transformation makes the resulting \small{VHDL} a lot shorter. + + \starttrans + let a = E in M + ---------------------------- \lam{a} does not occur free in \lam{M} + M + \stoptrans + + \starttrans + letrec + \vdots + a = E + \vdots + in + M + ---------------------------- \lam{a} does not occur free in \lam{M} + letrec + \vdots + \vdots + in + M + \stoptrans + + \subsubsection{Cast propagation / simplification} + This transform pushes casts down into the expression as far as possible. + Since its exact role and need is not clear yet, this transformation is + not yet specified. + + \subsubsection{Compiler generated top level binding inlining} + TODO + + \section{Program structure} + + \subsubsection{η-abstraction} + This transformation makes sure that all arguments of a function-typed + expression are named, by introducing lambda expressions. When combined with + β-reduction and function inlining below, all function-typed expressions should + be lambda abstractions or global identifiers. + + \starttrans + E \lam{E :: a -> b} + -------------- \lam{E} is not the first argument of an application. + λx.E x \lam{E} is not a lambda abstraction. + \lam{x} is a variable that does not occur free in \lam{E}. + \stoptrans + + \startbuffer[from] + foo = λa.case a of + True -> λb.mul b b + False -> id + \stopbuffer + + \startbuffer[to] + foo = λa.λx.(case a of + True -> λb.mul b b + False -> λy.id y) x + \stopbuffer + + \transexample{η-abstraction}{from}{to} + + \subsubsection{Let derecursification} + This transformation is meant to make lets non-recursive whenever possible. + This might allow other optimizations to do their work better. TODO: Why is + this needed exactly? + + \subsubsection{Let flattening} + This transformation puts nested lets in the same scope, by lifting the + binding(s) of the inner let into a new let around the outer let. Eventually, + this will cause all let bindings to appear in the same scope (they will all be + in scope for the function return value). + + Note that this transformation does not try to be smart when faced with + recursive lets, it will just leave the lets recursive (possibly joining a + recursive and non-recursive let into a single recursive let). The let + rederecursification transformation will do this instead. + + \starttrans + letnonrec x = (let bindings in M) in N + ------------------------------------------ + let bindings in (letnonrec x = M) in N + \stoptrans + + \starttrans + letrec + \vdots + x = (let bindings in M) + \vdots + in + N + ------------------------------------------ + letrec + \vdots + bindings + x = M + \vdots + in + N + \stoptrans + + \startbuffer[from] + let + a = letrec + x = 1 + y = 2 + in + x + y + in + letrec + b = let c = 3 in a + c + d = 4 + in + d + b + \stopbuffer + \startbuffer[to] + letrec + x = 1 + y = 2 + in + let + a = x + y + in + letrec + c = 3 + b = a + c + d = 4 + in + d + b + \stopbuffer + + \transexample{Let flattening}{from}{to} + + \subsubsection{Return value simplification} + This transformation ensures that the return value of a function is always a + simple local variable reference. + + Currently implemented using lambda simplification, let simplification, and + top simplification. Should change into something like the following, which + works only on the result of a function instead of any subexpression. This is + achieved by the contexts, like \lam{x = E}, though this is strictly not + correct (you could read this as "if there is any function \lam{x} that binds + \lam{E}, any \lam{E} can be transformed, while we only mean the \lam{E} that + is bound by \lam{x}. This might need some extra notes or something). + + \starttrans + x = E \lam{E} is representable + ~ \lam{E} is not a lambda abstraction + E \lam{E} is not a let expression + --------------------------- \lam{E} is not a local variable reference + let x = E in x + \stoptrans + + \starttrans + x = λv0 ... λvn.E + ~ \lam{E} is representable + E \lam{E} is not a let expression + --------------------------- \lam{E} is not a local variable reference + let x = E in x + \stoptrans + + \starttrans + x = λv0 ... λvn.let ... in E + ~ \lam{E} is representable + E \lam{E} is not a local variable reference + --------------------------- + let x = E in x + \stoptrans + + \startbuffer[from] + x = add 1 2 + \stopbuffer + + \startbuffer[to] + x = let x = add 1 2 in x + \stopbuffer + + \transexample{Return value simplification}{from}{to} + + \subsection{Argument simplification} + The transforms in this section deal with simplifying application + arguments into normal form. The goal here is to: + + \startitemize + \item Make all arguments of user-defined functions (\eg, of which + we have a function body) simple variable references of a runtime + representable type. This is needed, since these applications will be turned + into component instantiations. + \item Make all arguments of builtin functions one of: + \startitemize + \item A type argument. + \item A dictionary argument. + \item A type level expression. + \item A variable reference of a runtime representable type. + \item A variable reference or partial application of a function type. + \stopitemize + \stopitemize -\starttrans -x = λv0 ... λvn.let ... in E -~ \lam{E} is representable -E \lam{E} is not a local variable reference ---------------------------- -let x = E in x -\stoptrans + When looking at the arguments of a user-defined function, we can + divide them into two categories: + \startitemize + \item Arguments of a runtime representable type (\eg bits or vectors). + + These arguments can be preserved in the program, since they can + be translated to input ports later on. However, since we can + only connect signals to input ports, these arguments must be + reduced to simple variables (for which signals will be + produced). This is taken care of by the argument extraction + transform. + \item Non-runtime representable typed arguments. + + These arguments cannot be preserved in the program, since we + cannot represent them as input or output ports in the resulting + \small{VHDL}. To remove them, we create a specialized version of the + called function with these arguments filled in. This is done by + the argument propagation transform. + + Typically, these arguments are type and dictionary arguments that are + used to make functions polymorphic. By propagating these arguments, we + are essentially doing the same which GHC does when it specializes + functions: Creating multiple variants of the same function, one for + each type for which it is used. Other common non-representable + arguments are functions, e.g. when calling a higher order function + with another function or a lambda abstraction as an argument. + + The reason for doing this is similar to the reasoning provided for + the inlining of non-representable let bindings above. In fact, this + argument propagation could be viewed as a form of cross-function + inlining. + \stopitemize -\startbuffer[from] -x = add 1 2 -\stopbuffer + TODO: Check the following itemization. + + When looking at the arguments of a builtin function, we can divide them + into categories: + + \startitemize + \item Arguments of a runtime representable type. + + As we have seen with user-defined functions, these arguments can + always be reduced to a simple variable reference, by the + argument extraction transform. Performing this transform for + builtin functions as well, means that the translation of builtin + functions can be limited to signal references, instead of + needing to support all possible expressions. + + \item Arguments of a function type. + + These arguments are functions passed to higher order builtins, + like \lam{map} and \lam{foldl}. Since implementing these + functions for arbitrary function-typed expressions (\eg, lambda + expressions) is rather comlex, we reduce these arguments to + (partial applications of) global functions. + + We can still support arbitrary expressions from the user code, + by creating a new global function containing that expression. + This way, we can simply replace the argument with a reference to + that new function. However, since the expression can contain any + number of free variables we also have to include partial + applications in our normal form. + + This category of arguments is handled by the function extraction + transform. + \item Other unrepresentable arguments. + + These arguments can take a few different forms: + \startdesc{Type arguments} + In the core language, type arguments can only take a single + form: A type wrapped in the Type constructor. Also, there is + nothing that can be done with type expressions, except for + applying functions to them, so we can simply leave type + arguments as they are. + \stopdesc + \startdesc{Dictionary arguments} + In the core language, dictionary arguments are used to find + operations operating on one of the type arguments (mostly for + finding class methods). Since we will not actually evaluatie + the function body for builtin functions and can generate + code for builtin functions by just looking at the type + arguments, these arguments can be ignored and left as they + are. + \stopdesc + \startdesc{Type level arguments} + Sometimes, we want to pass a value to a builtin function, but + we need to know the value at compile time. Additionally, the + value has an impact on the type of the function. This is + encoded using type-level values, where the actual value of the + argument is not important, but the type encodes some integer, + for example. Since the value is not important, the actual form + of the expression does not matter either and we can leave + these arguments as they are. + \stopdesc + \startdesc{Other arguments} + Technically, there is still a wide array of arguments that can + be passed, but does not fall into any of the above categories. + However, none of the supported builtin functions requires such + an argument. This leaves use with passing unsupported types to + a function, such as calling \lam{head} on a list of functions. + + In these cases, it would be impossible to generate hardware + for such a function call anyway, so we can ignore these + arguments. + + The only way to generate hardware for builtin functions with + arguments like these, is to expand the function call into an + equivalent core expression (\eg, expand map into a series of + function applications). But for now, we choose to simply not + support expressions like these. + \stopdesc + + From the above, we can conclude that we can simply ignore these + other unrepresentable arguments and focus on the first two + categories instead. + \stopitemize -\startbuffer[to] -x = let x = add 1 2 in x -\stopbuffer + \subsubsection{Argument simplification} + This transform deals with arguments to functions that + are of a runtime representable type. It ensures that they will all become + references to global variables, or local signals in the resulting \small{VHDL}. + + TODO: It seems we can map an expression to a port, not only a signal. + Perhaps this makes this transformation not needed? + TODO: Say something about dataconstructors (without arguments, like True + or False), which are variable references of a runtime representable + type, but do not result in a signal. + + To reduce a complex expression to a simple variable reference, we create + a new let expression around the application, which binds the complex + expression to a new variable. The original function is then applied to + this variable. + + \starttrans + M N + -------------------- \lam{N} is of a representable type + let x = N in M x \lam{N} is not a local variable reference + \stoptrans + + \startbuffer[from] + add (add a 1) 1 + \stopbuffer + + \startbuffer[to] + let x = add a 1 in add x 1 + \stopbuffer + + \transexample{Argument extraction}{from}{to} + + \subsubsection{Function extraction} + This transform deals with function-typed arguments to builtin functions. + Since these arguments cannot be propagated, we choose to extract them + into a new global function instead. + + Any free variables occuring in the extracted arguments will become + parameters to the new global function. The original argument is replaced + with a reference to the new function, applied to any free variables from + the original argument. + + This transformation is useful when applying higher order builtin functions + like \hs{map} to a lambda abstraction, for example. In this case, the code + that generates \small{VHDL} for \hs{map} only needs to handle top level functions and + partial applications, not any other expression (such as lambda abstractions or + even more complicated expressions). + + \starttrans + M N \lam{M} is a (partial aplication of a) builtin function. + --------------------- \lam{f0 ... fn} = free local variables of \lam{N} + M x f0 ... fn \lam{N :: a -> b} + ~ \lam{N} is not a (partial application of) a top level function + x = λf0 ... λfn.N + \stoptrans + + \startbuffer[from] + map (λa . add a b) xs + + map (add b) ys + \stopbuffer + + \startbuffer[to] + x0 = λb.λa.add a b + ~ + map x0 xs + + x1 = λb.add b + map x1 ys + \stopbuffer + + \transexample{Function extraction}{from}{to} + + \subsubsection{Argument propagation} + This transform deals with arguments to user-defined functions that are + not representable at runtime. This means these arguments cannot be + preserved in the final form and most be {\em propagated}. + + Propagation means to create a specialized version of the called + function, with the propagated argument already filled in. As a simple + example, in the following program: + + \startlambda + f = λa.λb.a + b + inc = λa.f a 1 + \stoplambda + + we could {\em propagate} the constant argument 1, with the following + result: + + \startlambda + f' = λa.a + 1 + inc = λa.f' a + \stoplambda + + Special care must be taken when the to-be-propagated expression has any + free variables. If this is the case, the original argument should not be + removed alltogether, but replaced by all the free variables of the + expression. In this way, the original expression can still be evaluated + inside the new function. Also, this brings us closer to our goal: All + these free variables will be simple variable references. + + To prevent us from propagating the same argument over and over, a simple + local variable reference is not propagated (since is has exactly one + free variable, itself, we would only replace that argument with itself). + + This shows that any free local variables that are not runtime representable + cannot be brought into normal form by this transform. We rely on an + inlining transformation to replace such a variable with an expression we + can propagate again. + + \starttrans + x = E + ~ + x Y0 ... Yi ... Yn \lam{Yi} is not of a runtime representable type + --------------------------------------------- \lam{Yi} is not a local variable reference + x' y0 ... yi-1 f0 ... fm Yi+1 ... Yn \lam{f0 ... fm} = free local vars of \lam{Yi} + ~ + x' = λy0 ... yi-1 f0 ... fm yi+1 ... yn . + E y0 ... yi-1 Yi yi+1 ... yn + + \stoptrans + + TODO: Example + + \subsection{Case simplification} + \subsubsection{Scrutinee simplification} + This transform ensures that the scrutinee of a case expression is always + a simple variable reference. + + \starttrans + case E of + alts + ----------------- \lam{E} is not a local variable reference + let x = E in + case E of + alts + \stoptrans + + \startbuffer[from] + case (foo a) of + True -> a + False -> b + \stopbuffer + + \startbuffer[to] + let x = foo a in + case x of + True -> a + False -> b + \stopbuffer + + \transexample{Let flattening}{from}{to} + + + \subsubsection{Case simplification} + This transformation ensures that all case expressions become normal form. This + means they will become one of: + \startitemize + \item An extractor case with a single alternative that picks a single field + from a datatype, \eg \lam{case x of (a, b) -> a}. + \item A selector case with multiple alternatives and only wild binders, that + makes a choice between expressions based on the constructor of another + expression, \eg \lam{case x of Low -> a; High -> b}. + \stopitemize + + \starttrans + case E of + C0 v0,0 ... v0,m -> E0 + \vdots + Cn vn,0 ... vn,m -> En + --------------------------------------------------- \forall i \forall j, 0 <= i <= n, 0 <= i < m (\lam{wi,j} is a wild (unused) binder) + letnonrec + v0,0 = case x of C0 v0,0 .. v0,m -> v0,0 + \vdots + v0,m = case x of C0 v0,0 .. v0,m -> v0,m + x0 = E0 + \dots + vn,m = case x of Cn vn,0 .. vn,m -> vn,m + xn = En + in + case E of + C0 w0,0 ... w0,m -> x0 + \vdots + Cn wn,0 ... wn,m -> xn + \stoptrans + + TODO: This transformation specified like this is complicated and misses + conditions to prevent looping with itself. Perhaps we should split it here for + discussion? + + \startbuffer[from] + case a of + True -> add b 1 + False -> add b 2 + \stopbuffer + + \startbuffer[to] + letnonrec + x0 = add b 1 + x1 = add b 2 + in + case a of + True -> x0 + False -> x1 + \stopbuffer + + \transexample{Selector case simplification}{from}{to} + + \startbuffer[from] + case a of + (,) b c -> add b c + \stopbuffer + \startbuffer[to] + letnonrec + b = case a of (,) b c -> b + c = case a of (,) b c -> c + x0 = add b c + in + case a of + (,) w0 w1 -> x0 + \stopbuffer + + \transexample{Extractor case simplification}{from}{to} + + \subsubsection{Case removal} + This transform removes any case statements with a single alternative and + only wild binders. + + These "useless" case statements are usually leftovers from case simplification + on extractor case (see the previous example). + + \starttrans + case x of + C v0 ... vm -> E + ---------------------- \lam{\forall i, 0 <= i <= m} (\lam{vi} does not occur free in E) + E + \stoptrans + + \startbuffer[from] + case a of + (,) w0 w1 -> x0 + \stopbuffer + + \startbuffer[to] + x0 + \stopbuffer + + \transexample{Case removal}{from}{to} + +\subsection{Monomorphisation} + TODO: Better name for this section + + Reference type-specialization (== argument propagation) + +\subsubsection{Defunctionalization} + Reference higher-order-specialization (== argument propagation) + + \subsubsection{Non-representable binding inlining} + This transform inlines let bindings that have a non-representable type. Since + we can never generate a signal assignment for these bindings (we cannot + declare a signal assignment with a non-representable type, for obvious + reasons), we have no choice but to inline the binding to remove it. + + If the binding is non-representable because it is a lambda abstraction, it is + likely that it will inlined into an application and β-reduction will remove + the lambda abstraction and turn it into a representable expression at the + inline site. The same holds for partial applications, which can be turned into + full applications by inlining. + + Other cases of non-representable bindings we see in practice are primitive + Haskell types. In most cases, these will not result in a valid normalized + output, but then the input would have been invalid to start with. There is one + exception to this: When a builtin function is applied to a non-representable + expression, things might work out in some cases. For example, when you write a + literal \hs{SizedInt} in Haskell, like \hs{1 :: SizedInt D8}, this results in + the following core: \lam{fromInteger (smallInteger 10)}, where for example + \lam{10 :: GHC.Prim.Int\#} and \lam{smallInteger 10 :: Integer} have + non-representable types. TODO: This/these paragraph(s) should probably become a + separate discussion somewhere else. + + \starttrans + letnonrec a = E in M + -------------------------- \lam{E} has a non-representable type. + M[E/a] + \stoptrans + + \starttrans + letrec + \vdots + a = E + \vdots + in + M + -------------------------- \lam{E} has a non-representable type. + letrec + \vdots [E/a] + \vdots [E/a] + in + M[E/a] + \stoptrans + + \startbuffer[from] + letrec + a = smallInteger 10 + inc = λa -> add a 1 + inc' = add 1 + x = fromInteger a + in + inc (inc' x) + \stopbuffer + + \startbuffer[to] + letrec + x = fromInteger (smallInteger 10) + in + (λa -> add a 1) (add 1 x) + \stopbuffer + + \transexample{Let flattening}{from}{to} -\transexample{Return value simplification}{from}{to} \section{Provable properties} When looking at the system of transformations outlined above, there are a -- 2.30.2