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
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
\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
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
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
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.
M
\stoptrans
- TODO: Example
+ \todo{Example}
\subsubsection{Simple let binding removal}
This transformation inlines simple let bindings (\eg a = b).
M[b/ai]
\stoptrans
- TODO: Example
+ \todo{example}
\subsubsection{Unused let binding removal}
This transformation removes let bindings that are never used. Usually,
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
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}
+
\subsubsection{Top level binding inlining}
This transform takes simple top level bindings generated by the
\small{GHC} compiler. \small{GHC} sometimes generates very simple
\starttrans
(letrec binds in E) M
- -----------------
+ ------------------------
letrec binds in E M
\stoptrans
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:
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
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}.
\stoptrans
- TODO: Example
+ \todo{Example}
\subsection{Case simplification}
\subsubsection{Scrutinee simplification}
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
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)
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
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
projects / matthijs / master-project / report.git / blobdiff