core can describe expressions that do not have a direct hardware
interpretation.
- \todo{Describe core properties not supported in \VHDL, and describe how the
- \VHDL we want to generate should look like.}
-
\section{Normal form}
- \todo{Refresh or refer to distinct hardware per application principle}
The transformations described here have a well-defined goal: To bring the
program in a well-defined form that is directly translatable to hardware,
while fully preserving the semantics of the program. We refer to this form as
In particular, we define no particular order of transformations. Since
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.
+ this leaves the implementation free to choose any application order that
+ results in an efficient implementation. Unfortunately this is not
+ entirely true for the current set of transformations. See
+ \in{section}[sec:normalization:non-determinism] for a discussion of this
+ problem.
When applying a single transformation, we try to apply it to every (sub)expression
in a function, not just the top level function body. This allows us to
In the following sections, we will be using a number of functions and
notations, which we will define here.
- \todo{Define substitution (notation)}
-
\subsubsection{Concepts}
A \emph{global variable} is any variable (binder) that is bound at the
top level of a program, or an external module. A \emph{local variable} is any
optimizations, but they are required to get our program into intended
normal form.
+ \placeintermezzo{}{
+ \defref{substitution notation}
+ \startframedtext[width=8cm,background=box,frame=no]
+ \startalignment[center]
+ {\tfa Substitution notation}
+ \stopalignment
+ \blank[medium]
+
+ In some of the transformations in this chapter, we need to perform
+ substitution on an expression. Substitution means replacing every
+ occurence of some expression (usually a variable reference) with
+ another expression.
+
+ There have been a lot of different notations used in literature for
+ specifying substitution. The notation that will be used in this report
+ is the following:
+
+ \startlambda
+ E[A=>B]
+ \stoplambda
+
+ This means expression \lam{E} with all occurences of \lam{A} replaced
+ with \lam{B}.
+ \stopframedtext
+ }
+
+ \defref{beta-reduction}
\subsubsection[sec:normalization:beta]{β-reduction}
- \defref{beta-reduction}
β-reduction is a well known transformation from lambda calculus, where it is
the main reduction step. It reduces applications of lambda abstractions,
removing both the lambda abstraction and the application.
This transformation is not needed to get an expression into intended
normal form (since these bindings are part of the intended normal
form), but makes the resulting \small{VHDL} a lot shorter.
-
+
+ \refdef{substitution notation}
\starttrans
letrec
a0 = E0
\transexample{apppropcase}{Application propagation for a case expression}{from}{to}
- \subsubsection{Let recursification}
+ \subsubsection[sec:normalization:letrecurse]{Let recursification}
This transformation makes all non-recursive lets recursive. In the
end, we want a single recursive let in our normalized program, so all
non-recursive lets can be converted. This also makes other
False -> b
\stopbuffer
- \transexample{letflat}{Let flattening}{from}{to}
+ \transexample{letflat}{Case normalisation}{from}{to}
\subsubsection{Case simplification}
solves (part of) the polymorphism, higher order values and
unrepresentable literals in an expression.
+ \refdef{substitution notation}
\starttrans
letrec
a0 = E0
let y = (a * b) in y + y
\stoplambda
- \subsection{Non-determinism}
+ \subsection[sec:normalization:non-determinism]{Non-determinism}
As an example, again consider the following expression:
\startlambda
projects / matthijs / master-project / report.git / blobdiff