From 2790ccea19648fe307a85db7485ec8986e63e773 Mon Sep 17 00:00:00 2001 From: Matthijs Kooijman Date: Wed, 2 Dec 2009 12:16:47 +0100 Subject: [PATCH] Move some more stuff around in the Normalization chapter. --- Chapters/Normalization.tex | 343 +++++++++++++------------------------ Outline | 1 + 2 files changed, 122 insertions(+), 222 deletions(-) diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex index db743fc..d3b3700 100644 --- a/Chapters/Normalization.tex +++ b/Chapters/Normalization.tex @@ -328,41 +328,40 @@ \defref{intended normal form definition} \todo{Fix indentation} \startlambda - \italic{normal} = \italic{lambda} - \italic{lambda} = λvar.\italic{lambda} (representable(var)) + \italic{normal} := \italic{lambda} + \italic{lambda} := λvar.\italic{lambda} (representable(var)) | \italic{toplet} - \italic{toplet} = letrec [\italic{binding}...] in var (representable(var)) - \italic{binding} = var = \italic{rhs} (representable(rhs)) + \italic{toplet} := letrec [\italic{binding}...] in var (representable(var)) + \italic{binding} := var = \italic{rhs} (representable(rhs)) -- State packing and unpacking by coercion | var0 = var1 ▶ State ty (lvar(var1)) - | var0 = var1 ▶ ty (var1 :: State ty) (lvar(var1)) - \italic{rhs} = userapp + | var0 = var1 ▶ ty (var1 :: State ty ∧ lvar(var1)) + \italic{rhs} := userapp | builtinapp -- Extractor case | case var of C a0 ... an -> ai (lvar(var)) -- Selector case | case var of (lvar(var)) - DEFAULT -> var0 (lvar(var0)) - C w0 ... wn -> resvar (\forall{}i, wi \neq resvar, lvar(resvar)) - \italic{userapp} = \italic{userfunc} + [ DEFAULT -> var ] (lvar(var)) + C0 w0,0 ... w0,n -> var0 + \vdots + Cm wm,0 ... wm,n -> varm (\forall{}i \forall{}j, wi,j \neq vari, lvar(vari)) + \italic{userapp} := \italic{userfunc} | \italic{userapp} {userarg} - \italic{userfunc} = var (gvar(var)) - \italic{userarg} = var (lvar(var)) - \italic{builtinapp} = \italic{builtinfunc} + \italic{userfunc} := var (gvar(var)) + \italic{userarg} := var (lvar(var)) + \italic{builtinapp} := \italic{builtinfunc} | \italic{builtinapp} \italic{builtinarg} - \italic{builtinfunc} = var (bvar(var)) - \italic{builtinarg} = \italic{coreexpr} + \italic{builtinfunc} := var (bvar(var)) + \italic{builtinarg} := var (representable(var) ∧ lvar(var)) + | \italic{partapp} (partapp :: a -> b) + | \italic{coreexpr} (¬representable(coreexpr) ∧ ¬(coreexpr :: a -> b)) + \italic{partapp} := \italic{userapp} | \italic{builtinapp} \stoplambda - \todo{Limit builtinarg further} - \todo{There can still be other casts around (which the code can handle, e.g., ignore), which still need to be documented here} - \todo{Note about the selector case. It just supports Bit and Bool - currently, perhaps it should be generalized in the normal form? This is - no longer true, btw} - When looking at such a program from a hardware perspective, the top level lambda's define the input ports. The variable reference in the body of the recursive let expression is the output port. Most function @@ -1218,195 +1217,94 @@ \todo{More examples} - \subsection{Argument simplification} - The transforms in this section deal with simplifying application - arguments into normal form. The goal here is to: - - \todo{This section should only talk about representable arguments. Non - representable arguments are treated by specialization.} - - \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. \todo{Move this - bullet to specialization} - - 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{Move this itemization into a new section about builtin functions} - 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. + \subsection[sec:normalization:argsimpl]{Representable arguments simplification} + This section contains just a single transformation that deals with + representable arguments in applications. Non-representable arguments are + handled by the transformations in + \in{section}[sec:normalization:nonrep]. + + This transformation ensures that all representable arguments will become + references to local variables. This ensures they will become references + to local signals in the resulting \small{VHDL}, which is required due to + limitations in the component instantiation code in \VHDL (one can only + assign a signal or constant to an input port). By ensuring that all + arguments are always simple variable references, we always have a signal + available to map to the input ports. + + 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. + + \refdef{global variable} + Note that references to \emph{global variables} (like a top level + function without arguments, but also an argumentless dataconstructors + like \lam{True}) are also simplified. Only local variables generate + signals in the resulting architecture. Even though argumentless + dataconstructors generate constants in generated \VHDL code and could be + mapped to an input port directly, they are still simplified to make the + normal form more regular. + + \refdef{representable} + \starttrans + M N + -------------------- \lam{N} is representable + letrec x = N in M x \lam{N} is not a local variable reference + \stoptrans + \refdef{local variable} + + \startbuffer[from] + add (add a 1) 1 + \stopbuffer + + \startbuffer[to] + letrec x = add a 1 in add x 1 + \stopbuffer + + \transexample{argsimpl}{Argument simplification}{from}{to} + + \subsection[sec:normalization:builtins]{Builtin functions} + This section deals with (arguments to) builtin functions. In the + intended normal form definition\refdef{intended normal form definition} + we can see that there are three sorts of arguments a builtin function + can receive. + + \startitemize[KR] + \item A representable local variable reference. This is the most + common argument to any function. The argument simplification + transformation described in \in{section}[sec:normalization:argsimpl] + makes sure that \emph{any} representable argument to \emph{any} + function (including builtin functions) is turned into a local variable + reference. + \item (A partial application of) a top level function (either builtin on + user-defined). The function extraction transformation described in + this section takes care of turning every functiontyped argument into + (a partial application of) a top level function. + \item Any expression that is not representable and does not have a + function type. Since these can be any expression, there is no + transformation needed. Note that this category is exactly all + expressions that are not transformed by the transformations for the + previous two categories. This means that \emph{any} core expression + that is used as an argument to a builtin function will be either + transformed into one of the above categories, or end up in this + categorie. In any case, the result is in normal form. \stopitemize - \subsubsection[sec:normalization:argsimpl]{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}, which is required due to limitations in the component - instantiation code in \VHDL (one can only assign a signal or constant - to an input port). By ensuring that all arguments are always simple - variable references, we always have a signal available to assign to - input ports. - - \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. - - Note that a reference to a \emph{global variable} (like a top level - function without arguments, but also an argumentless dataconstructors - like \lam{True}) is also simplified. Only local variables generate - signals in the resulting architecture. + As noted, the argument simplification will handle any representable + arguments to a builtin function. The following transformation is needed + to handle non-representable arguments with a function type, all other + non-representable arguments don't need any special handling. - \refdef{representable} - \starttrans - M N - -------------------- \lam{N} is representable - letrec x = N in M x \lam{N} is not a local variable reference - \stoptrans - \refdef{local variable} - - \startbuffer[from] - add (add a 1) 1 - \stopbuffer - - \startbuffer[to] - letrec x = add a 1 in add x 1 - \stopbuffer - - \transexample{argextract}{Argument extraction}{from}{to} - \subsubsection[sec:normalization:funextract]{Function extraction} - \todo{Move to section about builtin functions} This transform deals with function-typed arguments to builtin - functions. Since builtin functions cannot be specialized to remove - the arguments, we choose to extract these arguments into a new global - function instead. This greatly simplifies the translation rules needed - for builtin functions. \todo{Should we talk about these? Reference - Christiaan?} + functions. + Since builtin functions cannot be specialized (see + \in{section}[sec:normalization:specialize]) to remove the arguments, + these arguments are extracted into a new global function instead. In + other words, we create a new top level function that has exactly the + extracted argument as its body. This greatly simplifies the + translation rules needed for builtin functions, since they only need + to handle (partial applications of) top level functions. Any free variables occuring in the extracted arguments will become parameters to the new global function. The original argument is replaced @@ -1427,27 +1325,20 @@ x = λf0 ... λfn.N \stoptrans - \todo{Split this example} \startbuffer[from] - map (λa . add a b) xs - - map (add b) ys + addList = λb.λxs.map (λa . add a b) xs \stopbuffer \startbuffer[to] - map (x0 b) xs - - map x1 ys + addList = λb.λxs.map (f b) xs ~ - x0 = λb.λa.add a b - x1 = λb.add b + f = λb.λa.add a b \stopbuffer \transexample{funextract}{Function extraction}{from}{to} - Note that \lam{x0} and {x1} will still need normalization after this. - - \todo{Fill the gap left by moving argument propagation away} + Note that the function \lam{f} will still need normalization after + this. \subsection{Case normalisation} \subsubsection{Scrutinee simplification} @@ -1591,14 +1482,22 @@ \transexample{caserem}{Case removal}{from}{to} - \subsection{Removing unrepresentable values} + \subsection[sec:normalization:nonrep]{Removing unrepresentable values} The transformations in this section are aimed at making all the values used in our expression representable. There are two main transformations that are applied to \emph{all} unrepresentable let - bindings and function arguments, but these are really meant to - address three different kinds of unrepresentable values: - Polymorphic values, higher order values and literals. Each of these - will be detailed below, followed by the actual transformations. + bindings and function arguments. These are meant to address three + different kinds of unrepresentable values: Polymorphic values, higher + order values and literals. The transformation are described generically: + They apply to all non-representable values. However, non-representable + values that don't fall into one of these three categories will be moved + around by these transformations but are unlikely to completely + disappear. They usually mean the program was not valid in the first + place, because unsupported types were used (for example, a program using + strings). + + Each of these three categories will be detailed below, followed by the + actual transformations. \subsubsection{Removing Polymorphism} As noted in \in{section}[sec:prototype:polymporphism], @@ -1939,7 +1838,7 @@ \transexample{nonrepinline}{Nonrepresentable binding inlining}{from}{to} - \subsubsection{Function specialization} + \subsubsection[sec:normalization:specialize]{Function specialization} This transform removes arguments to user-defined functions that are not representable at runtime. This is done by creating a \emph{specialized} version of the function that only works for one diff --git a/Outline b/Outline index 7a18303..2b32c29 100644 --- a/Outline +++ b/Outline @@ -61,3 +61,4 @@ TODO: core => Core TODO: \defref{beta-reduction} -> \defref{β-reduction} TODO: Make interaction links not bold TODO: Say something about implementation differences with transformation specs +TODO: Say something about the builtin functions somewhere (ref: christiaan) -- 2.30.2