X-Git-Url: https://git.stderr.nl/gitweb?p=matthijs%2Fmaster-project%2Freport.git;a=blobdiff_plain;f=Chapters%2FNormalization.tex;h=427ab0a07e2dea01c68d704e9a31aa1b63fa17e0;hp=593a5f0f89f66814c2be5669a098aa31c014a3ef;hb=1b9665a243799137f9b3f2b04e13489ba6f66e5e;hpb=74f35b798121688576fa237ecc6b070b132d70ba diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex index 593a5f0..427ab0a 100644 --- a/Chapters/Normalization.tex +++ b/Chapters/Normalization.tex @@ -28,8 +28,8 @@ core can describe expressions that do not have a direct hardware interpretation. - TODO: Describe core properties not supported in \small{VHDL}, and describe how the - \small{VHDL} we want to generate should look like. + \todo{Describe core properties not supported in \VHDL, and describe how the + \VHDL we want to generate should look like.} \section{Normal form} The transformations described here have a well-defined goal: To bring the @@ -66,7 +66,7 @@ on the \quote{top level}. \stopitemize - TODO: Intermezzo: functions vs plain values + \todo{Intermezzo: functions vs plain values} A very simple example of a program in normal form is given in \in{example}[ex:MulSum]. As you can see, all arguments to the function (which @@ -340,13 +340,14 @@ \italic{builtinarg} = \italic{coreexpr} \stoplambda - -- TODO: Limit builtinarg further + \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{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? + \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 value produced by the let expression is @@ -576,9 +577,10 @@ the result of each transformation. In particular, we define no particular order of transformations. Since - transformation order should not influence the resulting normal form (see TODO - ref), this leaves the implementation free to choose any application order that - results in an efficient implementation. + transformation order should not influence the resulting normal form, + \todo{This is not really true, but would like it to be...} this leaves + the implementation free to choose any application order that results in + an efficient implementation. When applying a single transformation, we try to apply it to every (sub)expression in a function, not just the top level function. This allows us to keep the @@ -588,7 +590,7 @@ In the following sections, we will be using a number of functions and notations, which we will define here. - TODO: Define substitution + \todo{Define substitution (notation)} \subsubsection{Other concepts} A \emph{global variable} is any variable that is bound at the @@ -703,14 +705,14 @@ a single function} must be unique. To achieve this, we apply the following technique. - TODO: Define fresh binders and unique supplies + \todo{Define fresh binders and unique supplies} \startitemize \item Before starting normalization, all binders in the function are made unique. This is done by generating a fresh binder for every binder used. This also replaces binders that did not pose any conflict, but it does ensure that all binders within the function are generated by the same unique supply. See - (TODO: ref fresh binder). + \refdef{fresh binder} \item Whenever a new binder must be generated, we generate a fresh binder that is guaranteed to be different from \emph{all binders generated so far}. This can thus never introduce duplication and will maintain the invariant. @@ -793,7 +795,7 @@ M \stoptrans - TODO: Example + \todo{Example} \subsubsection{Simple let binding removal} This transformation inlines simple let bindings (\eg a = b). @@ -822,7 +824,7 @@ M[b/ai] \stoptrans - TODO: Example + \todo{example} \subsubsection{Unused let binding removal} This transformation removes let bindings that are never used. Usually, @@ -831,7 +833,7 @@ This normalization pass should really be unneeded to get into normal form (since unused 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, + normalized (e.g., calls to a \type{PatError} (\todo{Check this name}). Also, this transformation makes the resulting \small{VHDL} a lot shorter. \starttrans @@ -855,14 +857,14 @@ M \stoptrans - TODO: Example + \todo{Example} \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. - TODO: Cast propagation + \todo{Cast propagation} \subsubsection{Top level binding inlining} This transform takes simple top level bindings generated by the @@ -1171,7 +1173,7 @@ inlining. \stopitemize - TODO: Check the following itemization. + \todo{Check the following itemization.} When looking at the arguments of a builtin function, we can divide them into categories: @@ -1260,11 +1262,11 @@ 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. + \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 + \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. + 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 @@ -1331,6 +1333,10 @@ Note that \lam{x0} and {x1} will still need normalization after this. \subsubsection{Argument propagation} + \fxnote{This section should be generalized and describe + specialization, so other transformations can refer to this (since + specialization is really used in multiple categories).} + 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}. @@ -1380,7 +1386,7 @@ \stoptrans - TODO: Example + \todo{Example} \subsection{Case simplification} \subsubsection{Scrutinee simplification} @@ -1444,9 +1450,9 @@ 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? + \fxnote{This transformation specified like this is complicated and misses + conditions to prevent looping with itself. Perhaps it should be split here for + discussion?} \startbuffer[from] case a of @@ -1517,7 +1523,7 @@ These transformations remove most higher order expressions from our program, making it completely first-order (the only exception here is for arguments to builtin functions, since we can't specialize builtin - function. TODO: Talk more about this somewhere). + function. \todo{Talk more about this somewhere} Reference higher-order-specialization (== argument propagation) @@ -1541,8 +1547,8 @@ 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. + non-representable types. \todo{This/these paragraph(s) should probably become a + separate discussion somewhere else} \starttrans @@ -1680,7 +1686,7 @@ transformation system consists of β-reduction and η-reduction (solid edges) or β-reduction and η-reduction (dotted edges). - TODO: Define β-reduction and η-reduction? + \todo{Define β-reduction and η-reduction?} Note that the normal form of such a system consists of the set of nodes (expressions) without outgoing edges, since those are the expression to which