X-Git-Url: https://git.stderr.nl/gitweb?p=matthijs%2Fmaster-project%2Freport.git;a=blobdiff_plain;f=Chapters%2FNormalization.tex;h=77dd977c8e87f7175c5f16bdc375c2fa95717eda;hp=a811bfef339e1d613fc6aa25496ab68c92a3ef61;hb=28b745e6faf774843ecdfbce67bdd22b8b4fc550;hpb=898bdb75483e570effe1a926592fc938419d83e9 diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex index a811bfe..77dd977 100644 --- a/Chapters/Normalization.tex +++ b/Chapters/Normalization.tex @@ -21,12 +21,12 @@ \stopcombination } - The first step in the core to \small{VHDL} translation process, is normalization. We - aim to bring the core description into a simpler form, which we can + The first step in the Core to \small{VHDL} translation process, is normalization. We + aim to bring the Core description into a simpler form, which we can subsequently translate into \small{VHDL} easily. This normal form is needed because - the full core language is more expressive than \small{VHDL} in some + the full Core language is more expressive than \small{VHDL} in some areas (higher-order expressions, limited polymorphism using type - classes, etc.) and because core can describe expressions that do not + classes, etc.) and because Core can describe expressions that do not have a direct hardware interpretation. \section{Normal form} @@ -224,7 +224,8 @@ -> State (Word, Word) -> (State (Word, Word), Word) - -- All arguments are an inital lambda (address, data, packed state) + -- All arguments are an inital lambda + -- (address, data, packed state) regbank = λa.λd.λsp. -- There are nested let expressions at top level let @@ -320,7 +321,7 @@ Now we have some intuition for the normal form, we can describe how we want the normal form to look like in a slightly more formal manner. The EBNF-like description in \in{definition}[def:IntendedNormal] captures - most of the intended structure (and generates a subset of \GHC's core + most of the intended structure (and generates a subset of \GHC's Core format). There are two things missing from this definition: cast expressions are @@ -712,7 +713,7 @@ \subsection[sec:normalization:uniq]{Binder uniqueness} A common problem in transformation systems, is binder uniqueness. When not considering this problem, it is easy to create transformations that mix up - bindings and cause name collisions. Take for example, the following core + bindings and cause name collisions. Take for example, the following Core expression: \startlambda @@ -796,7 +797,6 @@ unique. This is done by generating a fresh binder for every binder used. This also replaces binders that did not cause any conflict, but it does ensure that all binders within the function are generated by the same unique supply. - \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. @@ -1078,7 +1078,7 @@ \in{Example}[ex:trans:toplevelinline] shows a typical application of the addition operator generated by \GHC. The type and dictionary arguments used here are described in - \in{Section}[section:prototype:polymorphism]. + \in{Section}[sec:prototype:coretypes]. Without this transformation, there would be a \lam{(+)} entity in the \VHDL\ which would just add its inputs. This generates a @@ -1430,7 +1430,7 @@ 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 + previous two categories. This means that \emph{any} Core expression that is used as an argument to a built-in 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. @@ -1586,10 +1586,12 @@ \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}.\defref{extractor case} \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}.\defref{selector case} \stopitemize For an arbitrary case, that has \lam{n} alternatives, with @@ -1717,7 +1719,7 @@ actual transformations. \subsubsection{Removing Polymorphism} - As noted in \in{section}[sec:prototype:polymporphism], + As noted in \in{section}[sec:prototype:coretypes], polymorphism is made explicit in Core through type and dictionary arguments. To remove the polymorphism from a function, we can simply specialize the polymorphic function for @@ -2255,7 +2257,7 @@ there are probably expressions involving cast expressions that cannot be brought into intended normal form by this transformation system. - The uses of casts in the core system should be investigated more and + The uses of casts in the Core system should be investigated more and transformations will probably need updating to handle them in all cases. @@ -2413,7 +2415,7 @@ outgoing edges (meaning no transformation applies to it). The set of nodes without outgoing edges is called the \emph{normal set}. Similarly, the set of nodes containing expressions in intended normal form - \refdef{intended normal form} is called the \emph{intended normal set}. + \refdef{intended normal form definition} is called the \emph{intended normal set}. From such a graph, we can derive some properties easily: \startitemize[KR] @@ -2503,7 +2505,7 @@ 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 - assign a meaning to core expressions that assumes neither. + assign a meaning to Core expressions that assumes neither. Since each of the transformations can be applied to any subexpression as well, there is a constraint on our meaning @@ -2543,7 +2545,7 @@ By systematically reviewing the entire Core language definition along with the intended normal form definition (both of which have a similar structure), it should be possible to identify all - possible (sets of) core expressions that are not in intended + possible (sets of) Core expressions that are not in intended normal form and identify a transformation that applies to it. This approach is especially useful for proving completeness of our