X-Git-Url: https://git.stderr.nl/gitweb?p=matthijs%2Fmaster-project%2Freport.git;a=blobdiff_plain;f=Chapters%2FNormalization.tex;h=03cafcf23ed1ac11d908b283a9300328429a16e7;hp=5252c0fe71bca473d5ff2deb71482a7bbeed2d2a;hb=2ff5f767f17203c764a8ec9ef6711b234c1deb6d;hpb=1f7da57279ce037054198cb09402dcc5f1ac913e diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex index 5252c0f..03cafcf 100644 --- a/Chapters/Normalization.tex +++ b/Chapters/Normalization.tex @@ -913,7 +913,6 @@ either. To prevent the \VHDL\ generation from breaking on these artifacts, this transformation removes them. - \todo{Do not use old-style numerals in transformations} \starttrans letrec a0 = E0 @@ -1952,7 +1951,7 @@ twice). This is discussed in more detail in \in{section}[sec:normalization:duplicatework]. - \subsubsection{Literals} + \subsubsection[sec:normalization:literals]{Literals} There are a limited number of literals available in Haskell and Core. \refdef{enumerated types} When using (enumerating) algebraic data-types, a literal is just a reference to the corresponding data @@ -2149,7 +2148,7 @@ \section{Unsolved problems} The above system of transformations has been implemented in the prototype and seems to work well to compile simple and more complex examples of - hardware descriptions. \todo{Ref christiaan?} However, this normalization + hardware descriptions \cite[baaij09]. However, this normalization system has not seen enough review and work to be complete and work for every Core expression that is supplied to it. A number of problems have already been identified and are discussed in this section. @@ -2568,9 +2567,8 @@ {\lam{\forall A, B, C \exists D (A ->> B ∧ A ->> C => B ->> D ∧ C ->> D)}} Here, \lam{A ->> B} means \lam{A} \emph{reduces to} \lam{B}. In - other words, there is a set of transformations that can be applied - to transform \lam{A} to \lam{B}. \lam{=>} is used to mean - \emph{implies}. + other words, there is a set of transformations that can transform + \lam{A} to \lam{B}. \lam{=>} is used to mean \emph{implies}. For a transformation system holding the Church-Rosser property, it is easy to show that it is in fact deterministic. Showing that this