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.
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}
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
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
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}
\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
\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
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.
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.
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.
\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
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
\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).
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}
\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
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
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).
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
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).
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
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}
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.
projects / matthijs / master-project / report.git / blobdiff