\stopdesc
To understand this notation better, the step by step application of
- the η-abstraction transformation to a simple \small{ALU} will be
- shown. Consider η-abstraction, which is a common transformation from
+ the η-expansion transformation to a simple \small{ALU} will be
+ shown. Consider η-expansion, which is a common transformation from
labmda calculus, described using above notation as follows:
\starttrans
λx.E x \lam{E} is not a lambda abstraction.
\stoptrans
- η-abstraction is a well known transformation from lambda calculus. What
+ η-expansion is a well known transformation from lambda calculus. What
this transformation does, is take any expression that has a function type
and turn it into a lambda expression (giving an explicit name to the
argument). There are some extra conditions that ensure that this
transformation does not apply infinitely (which are not necessarily part
- of the conventional definition of η-abstraction).
+ of the conventional definition of η-expansion).
Consider the following function, in Core notation, which is a fairly obvious way to specify a
simple \small{ALU} (Note that it is not yet in normal form, but
\stoplambda
The other alternative is left as an exercise to the reader. The final
- function, after applying η-abstraction until it does no longer apply is:
+ function, after applying η-expansion until it does no longer apply is:
\startlambda
alu :: Bit -> Word -> Word -> Word
\in{section}[sec:normalization:transformation].
\subsection{General cleanup}
- These transformations are general cleanup transformations, that aim to
- make expressions simpler. These transformations usually clean up the
- mess left behind by other transformations or clean up expressions to
- expose new transformation opportunities for other transformations.
+ \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:
- Most of these transformations are standard optimizations in other
- compilers as well. However, in our compiler, most of these are not just
- 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.
+ \startlambda
+ E[A=>B]
+ \stoplambda
- 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:
+ This means expression \lam{E} with all occurences of \lam{A} replaced
+ with \lam{B}.
+ \stopframedtext
+ }
- \startlambda
- E[A=>B]
- \stoplambda
+ These transformations are general cleanup transformations, that aim to
+ make expressions simpler. These transformations usually clean up the
+ mess left behind by other transformations or clean up expressions to
+ expose new transformation opportunities for other transformations.
- This means expression \lam{E} with all occurences of \lam{A} replaced
- with \lam{B}.
- \stopframedtext
- }
+ Most of these transformations are standard optimizations in other
+ compilers as well. However, in our compiler, most of these are not just
+ optimizations, but they are required to get our program into intended
+ normal form.
\subsubsection[sec:normalization:beta]{β-reduction}
β-reduction is a well known transformation from lambda calculus, where it is
of the other value definitions in let bindings and making the final
return value a simple variable reference.
- \subsubsection[sec:normalization:eta]{η-abstraction}
+ \subsubsection[sec:normalization:eta]{η-expansion}
This transformation makes sure that all arguments of a function-typed
expression are named, by introducing lambda expressions. When combined with
β-reduction and non-representable binding inlining, all function-typed
False -> λy.id y) x
\stopbuffer
- \transexample{eta}{η-abstraction}{from}{to}
+ \transexample{eta}{η-expansion}{from}{to}
\subsubsection[sec:normalization:appprop]{Application propagation}
This transformation is meant to propagate application expressions downwards
This transformation ensures that the return value of a function is always a
simple local variable reference.
- This transformation only applies to the entire body of a
- function instead of any subexpression in a function. This is
- achieved by the contexts, like \lam{x = E}, though this is
- strictly not correct (you could read this as "if there is any
- function \lam{x} that binds \lam{E}, any \lam{E} can be
- transformed, while we only mean the \lam{E} that is bound by
- \lam{x}).
-
- Note that the return value is not simplified if its not
- representable. Otherwise, this would cause a direct loop with
- the inlining of unrepresentable bindings. If the return value is
- not representable because it has a function type, η-abstraction
- should make sure that this transformation will eventually apply.
- If the value is not representable for other reasons, the
- function result itself is not representable, meaning this
- function is not translatable anyway.
+ The basic idea of this transformation is to take the body of a
+ function and bind it with a let expression (so the body of that let
+ expression becomes a variable reference that can be used as the output
+ port). If the body of the function happens to have lambda abstractions
+ at the top level (which is allowed by the intended normal
+ form\refdef{intended normal form definition}), we take the body of the
+ inner lambda instead. If that happens to be a let expression already
+ (which is allowed by the intended normal form), we take the body of
+ that let (which is not allowed to be anything but a variable reference
+ according the the intended normal form).
+
+ This transformation uses the context conditions in a special way.
+ These contexts, like \lam{x = λv1 ... λvn.E}, are above the dotted
+ line and provide a condition on the environment (\ie\ they require a
+ certain top level binding to be present). These ensure that
+ expressions are only transformed when they are in the functions
+ \quote{return value} directly. This means the context conditions have
+ to interpreted in the right way: not \quote{if there is any function
+ \lam{x} that binds \lam{E}, any \lam{E} can be transformed}, but we
+ mean only the \lam{E} that is bound by \lam{x}).
+
+ Be careful when reading the transformations: Not the entire function
+ from the context is transformed, just a part of it.
+
+ Note that the return value is not simplified if it is not representable.
+ Otherwise, this would cause a loop with the inlining of
+ unrepresentable bindings in
+ \in{section}[sec:normalization:nonrepinline]. If the return value is
+ not representable because it has a function type, η-expansion should
+ make sure that this transformation will eventually apply. If the
+ value is not representable for other reasons, the function result
+ itself is not representable, meaning this function is not translatable
+ anyway.
\starttrans
- x = E \lam{E} is representable
- ~ \lam{E} is not a lambda abstraction
- E \lam{E} is not a let expression
- --------------------------- \lam{E} is not a local variable reference
- letrec x = E in x
+ x = λv1 ... λvn.E \lam{n} can be zero
+ ~ \lam{E} is representable
+ E \lam{E} is not a lambda abstraction
+ --------------------------- \lam{E} is not a let expression
+ letrec y = E in y \lam{E} is not a local variable reference
\stoptrans
\starttrans
- x = λv0 ... λvn.E \lam{E} is representable
- ~ \lam{E} is not a lambda abstraction
- E \lam{E} is not a let expression
- --------------------------- \lam{E} is not a local variable reference
- letrec x = E in x
- \stoptrans
-
- \starttrans
- x = λv0 ... λvn.let ... in E
- ~ \lam{E} is representable
- E \lam{E} is not a local variable reference
- -----------------------------
- letrec x = E in x
+ x = λv1 ... λvn.letrec binds in E \lam{n} can be zero
+ ~ \lam{E} is representable
+ letrec binds in E \lam{E} is not a local variable reference
+ ------------------------------------
+ letrec binds; y = E in y
\stoptrans
\startbuffer[from]
\stopbuffer
\startbuffer[to]
- x = letrec x = add 1 2 in x
+ x = letrec y = add 1 2 in y
\stopbuffer
\transexample{retvalsimpl}{Return value simplification}{from}{to}
+
+ \startbuffer[from]
+ x = λa. add 1 a
+ \stopbuffer
+
+ \startbuffer[to]
+ x = λa. letrec
+ y = add 1 a
+ in
+ y
+ \stopbuffer
+
+ \transexample{retvalsimpllam}{Return value simplification with a lambda abstraction}{from}{to}
- \todo{More examples}
+ \startbuffer[from]
+ x = letrec
+ a = add 1 2
+ in
+ add a 3
+ \stopbuffer
+
+ \startbuffer[to]
+ x = letrec
+ a = add 1 2
+ y = add a 3
+ in
+ y
+ \stopbuffer
+
+ \transexample{retvalsimpllet}{Return value simplification with a let expression}{from}{to}
\subsection[sec:normalization:argsimpl]{Representable arguments simplification}
This section contains just a single transformation that deals with
\stopframedtext
}
+ \subsubsection{Scrutinee binder removal}
+ This transformation removes (or rather, makes wild) the binder to
+ which the scrutinee is bound after evaluation. This is done by
+ replacing the bndr with the scrutinee in all alternatives. To prevent
+ duplication of work, this transformation is only applied when the
+ scrutinee is already a simple variable reference (but the previous
+ transformation ensures this will eventually be the case). The
+ scrutinee binder itself is replaced by a wild binder (which is no
+ longer displayed).
+
+ Note that one could argue that this transformation can change the
+ meaning of the Core expression. In the regular Core semantics, a case
+ expression forces the evaluation of its scrutinee and can be used to
+ implement strict evaluation. However, in the generated \VHDL,
+ evaluation is always strict. So the semantics we assign to the Core
+ expression (which differ only at this particular point), this
+ transformation is completely valid.
+
+ \starttrans
+ case x of bndr
+ alts
+ ----------------- \lam{x} is a local variable reference
+ case x of
+ alts[bndr=>x]
+ \stoptrans
+
+ \startbuffer[from]
+ case x of y
+ True -> y
+ False -> not y
+ \stopbuffer
+
+ \startbuffer[to]
+ case x of
+ True -> x
+ False -> not x
+ \stopbuffer
+
+ \transexample{scrutbndrremove}{Scrutinee binder removal}{from}{to}
+
\subsubsection{Case normalization}
This transformation ensures that all case expressions get a form
that is allowed by the intended normal form. This means they
lambda abstraction.
To reduce all higher-order values to one of the above items, a number
- of transformations we have already seen are used. The η-abstraction
+ of transformations we have already seen are used. The η-expansion
transformation from \in{section}[sec:normalization:eta] ensures all
function arguments are introduced by lambda abstraction on the highest
level of a function. These lambda arguments are allowed because of
- \in{item}[item:toplambda] above. After η-abstraction, our example
+ \in{item}[item:toplambda] above. After η-expansion, our example
becomes a bit bigger:
\startlambda
) q
\stoplambda
- η-abstraction also introduces extra applications (the application of
+ η-expansion also introduces extra applications (the application of
the let expression to \lam{q} in the above example). These
applications can then propagated down by the application propagation
transformation (\in{section}[sec:normalization:appprop]). In our
representable type). Completely applied top level functions (like the
first alternative) are now no longer invalid (they fall under
\in{item}[item:completeapp] above). (Completely) applied lambda
- abstractions can be removed by β-abstraction. For our example,
- applying β-abstraction results in the following:
+ abstractions can be removed by β-expansion. For our example,
+ applying β-expansion results in the following:
\startlambda
λy.λq.let double = λx. x + x in
to specialize away any unrepresentable literals that are used as
function arguments. The following two transformations do exactly this.
- \subsubsection{Non-representable binding inlining}
+ \subsubsection[sec:normalization:nonrepinline]{Non-representable binding inlining}
This transform inlines let bindings that are bound to a
non-representable value. Since we can never generate a signal
assignment for these bindings (we cannot declare a signal assignment
projects / matthijs / master-project / report.git / blobdiff