X-Git-Url: https://git.stderr.nl/gitweb?p=matthijs%2Fmaster-project%2Freport.git;a=blobdiff_plain;f=Chapters%2FNormalization.tex;h=d564d231405a00ab7f31622ef525b15f987c2218;hp=5a3fecb802f5833565eefe87df5e9601d910c1a8;hb=d92aa4307ca45f07c6ae50056e08ffc874839756;hpb=788930024f24adb36067d90b246621b2fa528328 diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex index 5a3fecb..d564d23 100644 --- a/Chapters/Normalization.tex +++ b/Chapters/Normalization.tex @@ -324,7 +324,7 @@ There are two things missing: Cast expressions are sometimes allowed by the prototype, but not specified here and the below - definition allows uses of state that cannot be translated to \VHDL + definition allows uses of state that cannot be translated to \VHDL\ properly. These two problems are discussed in \in{section}[sec:normalization:castproblems] and \in{section}[sec:normalization:stateproblems] respectively. @@ -383,8 +383,8 @@ Most function applications bound by the let expression define a component instantiation, where the input and output ports are mapped to local signals or arguments. Some of the others use a - built-in construction (\eg the \lam{case} expression) or call a - built-in function (\eg \lam{+} or \lam{map}). For these, a + built-in construction (\eg\ the \lam{case} expression) or call a + built-in function (\eg\ \lam{+} or \lam{map}). For these, a hardcoded \small{VHDL} translation is available. \section[sec:normalization:transformation]{Transformation notation} @@ -413,9 +413,9 @@ against (subexpressions of) the expression to be transformed. We call this a pattern, because it can contain \emph{placeholders} (variables), which match any expression or binder. Any such placeholder is said to be \emph{bound} to - the expression it matches. It is convention to use an uppercase letter (\eg + the expression it matches. It is convention to use an uppercase letter (\eg\ \lam{M} or \lam{E}) to refer to any expression (including a simple variable - reference) and lowercase letters (\eg \lam{v} or \lam{b}) to refer to + reference) and lowercase letters (\eg\ \lam{v} or \lam{b}) to refer to (references to) binders. For example, the pattern \lam{a + B} will match the expression @@ -666,7 +666,7 @@ lambda abstractions, let expressions and pattern matches of case alternatives). This is a slightly different notion of global versus local than what \small{GHC} uses internally, but for our purposes - the distinction \GHC makes is not useful. + the distinction \GHC\ makes is not useful. \defref{global variable} \defref{local variable} A \emph{hardware representable} (or just \emph{representable}) type or value @@ -901,7 +901,7 @@ desugarer or simplifier emits some bindings that cannot be normalized (e.g., calls to a \hs{Control.Exception.Base.patError}) but are not used anywhere - either. To prevent the \VHDL generation from breaking on these + either. To prevent the \VHDL\ generation from breaking on these artifacts, this transformation removes them. \todo{Do not use old-style numerals in transformations} @@ -971,7 +971,7 @@ \subsubsection[sec:normalization:simplelet]{Simple let binding removal} This transformation inlines simple let bindings, that bind some - binder to some other binder instead of a more complex expression (\ie + binder to some other binder instead of a more complex expression (\ie\ a = b). This transformation is not needed to get an expression into intended @@ -1072,11 +1072,11 @@ \in{Section}[section:prototype:polymorphism]. Without this transformation, there would be a \lam{(+)} entity - in the \VHDL which would just add its inputs. This generates a + in the \VHDL\ which would just add its inputs. This generates a lot of overhead in the \VHDL, which is particularly annoying when browsing the generated RTL schematic (especially since most non-alphanumerics, like all characters in \lam{(+)}, are not - allowed in \VHDL architecture names\footnote{Technically, it is + allowed in \VHDL\ architecture names\footnote{Technically, it is allowed to use non-alphanumerics when using extended identifiers, but it seems that none of the tooling likes extended identifiers in filenames, so it effectively does not @@ -1326,7 +1326,7 @@ 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 + 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. @@ -1341,7 +1341,7 @@ 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 + 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. @@ -1441,6 +1441,9 @@ this. \subsection{Case normalisation} + The transformations in this section ensure that case statements end up + in normal form. + \subsubsection{Scrutinee simplification} This transform ensures that the scrutinee of a case expression is always a simple variable reference. @@ -1470,16 +1473,37 @@ \transexample{letflat}{Case normalisation}{from}{to} + \placeintermezzo{}{ + \defref{wild binders} + \startframedtext[width=7cm,background=box,frame=no] + \startalignment[center] + {\tfa Wild binders} + \stopalignment + \blank[medium] + In a functional expression, a \emph{wild binder} refers to any + binder that is never referenced. This means that even though it + will be bound to a particular value, that value is never used. + + The Haskell syntax offers the underscore as a wild binder that + cannot even be referenced (It can be seen as introducing a new, + anonymous, binder everytime it is used). + + In these transformations, the term wild binder will sometimes be + used to indicate that a binder must not be referenced. + \stopframedtext + } + \subsubsection{Case normalization} This transformation ensures that all case expressions get a form that is allowed by the intended normal form. This means they - will become one of: \refdef{intended normal form definition} + will become one of: + \startitemize \item An extractor case with a single alternative that picks a field - from a datatype, \eg \lam{case x of (a, b) -> a}. + 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}. + expression, \eg\ \lam{case x of Low -> a; High -> b}. \stopitemize For an arbitrary case, that has \lam{n} alternatives, with @@ -1515,7 +1539,6 @@ Cn wn,0 ... wn,m -> yn \stoptrans - \refdef{wild binder} Note that this transformation applies to case expressions with any scrutinee. If the scrutinee is a complex expression, this might result in duplication of work (hardware). An extra condition to @@ -1567,7 +1590,7 @@ \subsubsection[sec:transformation:caseremoval]{Case removal} This transform removes any case expression with a single alternative and - only wild binders.\refdef{wild binder} + only wild binders.\refdef{wild binders} These "useless" case expressions are usually leftovers from case simplification on extractor case (see the previous example). @@ -1628,7 +1651,7 @@ There is one case where polymorphism cannot be completely removed: Built-in functions are still allowed to be polymorphic (Since we have no function body that we could properly - specialize). However, the code that generates \VHDL for built-in + specialize). However, the code that generates \VHDL\ for built-in functions knows how to handle this, so this is not a problem. \subsubsection[sec:normalization:defunctionalization]{Defunctionalization} @@ -1697,7 +1720,7 @@ \stoplambda This example shows a number of higher-order values that we cannot - translate to \VHDL directly. The \lam{double} binder bound in the let + translate to \VHDL\ directly. The \lam{double} binder bound in the let expression has a function type, as well as both of the alternatives of the case expression. The first alternative is a partial application of the \lam{map} built-in function, whereas the second alternative is a @@ -1856,11 +1879,11 @@ Haskell's \hs{Num} type class, which offers a \hs{fromInteger} method that converts any \hs{Integer} to the Cλash datatypes. - When \GHC sees integer literals, it will automatically insert calls to + When \GHC\ sees integer literals, it will automatically insert calls to the \hs{fromInteger} method in the resulting Core expression. For example, the following expression in Haskell creates a 32 bit unsigned word with the value 1. The explicit type signature is needed, since - there is no context for \GHC to determine the type from otherwise. + there is no context for \GHC\ to determine the type from otherwise. \starthaskell 1 :: SizedWord D32 @@ -2155,7 +2178,7 @@ normal form definition} offers enough freedom to describe all valid stateful descriptions, but is not limiting enough. It is possible to write descriptions which are in intended normal - form, but cannot be translated into \VHDL in a meaningful way + form, but cannot be translated into \VHDL\ in a meaningful way (\eg, a function that swaps two substates in its result, or a function that changes a substate itself instead of passing it to a subfunction). @@ -2172,7 +2195,7 @@ Without going into detail about the exact problems (of which there are probably more than have shown up so far), it seems unlikely that these problems can be solved entirely by just - improving the \VHDL state generation in the final stage. The + improving the \VHDL\ state generation in the final stage. The normalization stage seems the best place to apply the rewriting needed to support more complex stateful descriptions. This does of course mean that the intended normal form definition must be @@ -2217,11 +2240,13 @@ developed in the final part of the research, leaving no more time for verifying these properties. In fact, it is likely that the current transformation system still violates some of these - properties in some cases and should be improved (or extra conditions - on the input hardware descriptions should be formulated). + properties in some cases (see + \in{section}[sec:normalization:non-determinism] and + \in{section}[sec:normalization:stateproblems]) and should be improved (or + extra conditions on the input hardware descriptions should be formulated). This is most likely the case with the completeness and determinism - properties, perhaps als the termination property. The soundness + properties, perhaps also the termination property. The soundness property probably holds, since it is easier to manually verify (each transformation can be reviewed separately). @@ -2389,7 +2414,7 @@ sufficient for our goals (but it is a good start). It should be possible to have a single formal definition of - meaning for Core for both normal Core compilation by \GHC and for + meaning for Core for both normal Core compilation by \GHC\ and for our compilation to \VHDL. The main difference seems to be that in hardware every expression is always evaluated, while in software it is only evaluated if needed, but it should be possible to @@ -2418,7 +2443,7 @@ each node in the normal set is also in the intended normal set. Reasoning about our intended normal set is easier, since we know how to generate it from its definition. \refdef{intended normal - form definition}. + form definition} Fortunately, we can also prove the complement (which is equivalent, since $A \subseteq B \Leftrightarrow \overline{B} @@ -2438,7 +2463,7 @@ This approach is especially useful for proving completeness of our system, since if expressions exist to which none of the - transformations apply (\ie if the system is not yet complete), it + transformations apply (\ie\ if the system is not yet complete), it is immediately clear which expressions these are and adding (or modifying) transformations to fix this should be relatively easy.