% space at the start of the frame.
\define[1]\example{
\framed[offset=1mm,align=right,strut=no,background=box,frame=off]{
- \setuptyping[option=LAM,style=sans,before=,after=]
+ \setuptyping[option=LAM,style=sans,before=,after=,strip=auto]
\typebuffer[#1]
- \setuptyping[option=none,style=\tttf]
+ \setuptyping[option=none,style=\tttf,strip=auto]
}
}
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{normal} = \italic{lambda}
\italic{lambda} = λvar.\italic{lambda} (representable(var))
| \italic{toplet}
- \italic{toplet} = let \italic{binding} in \italic{toplet}
- | letrec [\italic{binding}] in \italic{toplet}
- | var (representable(varvar))
+ \italic{toplet} = letrec [\italic{binding}...] in var (representable(varvar))
\italic{binding} = var = \italic{rhs} (representable(rhs))
-- State packing and unpacking by coercion
| var0 = var1 :: State ty (lvar(var1))
\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 (notation)}
+
\subsubsection{Other concepts}
A \emph{global variable} is any variable that is bound at the
top level of a program, or an external module. A \emph{local variable} is any
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.
this notation are still a bit fuzzy, so comments are welcom.
\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.
+
+ 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 normal
+ form.
\subsubsection{β-reduction}
β-reduction is a well known transformation from lambda calculus, where it is
sure that most lambda abstractions will eventually be reducable by
β-reduction.
- TODO: Define substitution syntax
-
\starttrans
(λx.E) M
-----------------
\transexample{β-reduction}{from}{to}
- \subsubsection{Application propagation}
- This transformation is meant to propagate application expressions downwards
- into expressions as far as possible. This allows partial applications inside
- expressions to become fully applied and exposes new transformation
- possibilities for other transformations (like β-reduction).
-
- \starttrans
- let binds in E) M
- -----------------
- let binds in E M
- \stoptrans
-
- % And an example
- \startbuffer[from]
- ( let
- val = 1
- in
- add val
- ) 3
- \stopbuffer
-
- \startbuffer[to]
- let
- val = 1
- in
- add val 3
- \stopbuffer
-
- \transexample{Application propagation for a let expression}{from}{to}
-
- \starttrans
- (case x of
- p1 -> E1
- \vdots
- pn -> En) M
- -----------------
- case x of
- p1 -> E1 M
- \vdots
- pn -> En M
- \stoptrans
-
- % And an example
- \startbuffer[from]
- ( case x of
- True -> id
- False -> neg
- ) 1
- \stopbuffer
-
- \startbuffer[to]
- case x of
- True -> id 1
- False -> neg 1
- \stopbuffer
-
- \transexample{Application propagation for a case expression}{from}{to}
-
\subsubsection{Empty let removal}
This transformation is simple: It removes recursive lets that have no bindings
- (which usually occurs when let derecursification removes the last binding from
- it).
+ (which usually occurs when unused let binding removal removes the last
+ binding from it).
\starttrans
letrec in M
M
\stoptrans
- \subsubsection{Simple let binding removal}
+ \todo{Example}
+
+ \subsubsection{Simple let binding removal}
This transformation inlines simple let bindings (\eg a = b).
This transformation is not needed to get into normal form, but makes the
resulting \small{VHDL} a lot shorter.
- \starttrans
- letnonrec
- a = b
- in
- M
- -----------------
- M[b/a]
- \stoptrans
-
\starttrans
letrec
+ a0 = E0
\vdots
- a = b
+ ai = b
\vdots
+ an = En
in
M
- -----------------
- let
- \vdots [b/a]
- \vdots [b/a]
+ ----------------------------- \lam{b} is a variable reference
+ letrec
+ a0 = E0 [b/ai]
+ \vdots
+ ai-1 = Ei-1 [b/ai]
+ ai+1 = Ei+1 [b/ai]
+ \vdots
+ an = En [b/ai]
in
- M[b/a]
+ M[b/ai]
\stoptrans
+ \todo{example}
+
\subsubsection{Unused let binding removal}
This transformation removes let bindings that are never used. Usually,
the desugarer introduces some unused let bindings.
This normalization pass should really be unneeded to get into normal form
- (since ununsed bindings are not forbidden by the normal form), but in practice
+ (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
- let a = E in M
- ---------------------------- \lam{a} does not occur free in \lam{M}
- M
- \stoptrans
-
\starttrans
letrec
+ a0 = E0
\vdots
- a = E
+ ai = Ei
\vdots
+ an = En
in
- M
- ---------------------------- \lam{a} does not occur free in \lam{M}
+ M \lam{a} does not occur free in \lam{M}
+ ---------------------------- \forall j, 0 <= j <= n, j ≠ i (\lam{a} does not occur free in \lam{Ej})
letrec
+ a0 = E0
\vdots
+ ai-1 = Ei-1
+ ai+1 = Ei+1
\vdots
+ an = En
in
M
\stoptrans
+ \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.
- \subsubsection{Compiler generated top level binding inlining}
- TODO
+ \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
+ \quote{wrapper} bindings, which are bound to just a variable
+ reference, or a partial application to constants or other variable
+ references.
+
+ Note that this transformation is completely optional. It is not
+ required to get any function into normal form, but it does help making
+ the resulting VHDL output easier to read (since it removes a bunch of
+ components that are really boring).
- \section{Program structure}
+ This transform takes any top level binding generated by the compiler,
+ whose normalized form contains only a single let binding.
+
+ \starttrans
+ x = λa0 ... λan.let y = E in y
+ ~
+ x
+ -------------------------------------- \lam{x} is generated by the compiler
+ λa0 ... λan.let y = E in y
+ \stoptrans
+
+ \startbuffer[from]
+ (+) :: Word -> Word -> Word
+ (+) = GHC.Num.(+) @Word $dNum
+ ~
+ (+) a b
+ \stopbuffer
+ \startbuffer[to]
+ GHC.Num.(+) @ Alu.Word $dNum a b
+ \stopbuffer
+
+ \transexample{Top level binding inlining}{from}{to}
+
+ Without this transformation, the (+) function would generate an
+ architecture 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 + is not 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 doesn't work}, so the entity would be called
+ \quote{w7aA7f} or something similarly unreadable and autogenerated).
+
+ \subsection{Program structure}
+ These transformations are aimed at normalizing the overall structure
+ into the intended form. This means ensuring there is a lambda abstraction
+ at the top for every argument (input port), putting all of the other
+ value definitions in let bindings and making the final return value a
+ simple variable reference.
\subsubsection{η-abstraction}
This transformation makes sure that all arguments of a function-typed
expression are named, by introducing lambda expressions. When combined with
- β-reduction and function inlining below, all function-typed expressions should
- be lambda abstractions or global identifiers.
+ β-reduction and non-representable binding inlining, all function-typed
+ expressions should be lambda abstractions or global identifiers.
\starttrans
E \lam{E :: a -> b}
\transexample{η-abstraction}{from}{to}
- \subsubsection{Let derecursification}
- This transformation is meant to make lets non-recursive whenever possible.
- This might allow other optimizations to do their work better. TODO: Why is
- this needed exactly?
+ \subsubsection{Application propagation}
+ This transformation is meant to propagate application expressions downwards
+ into expressions as far as possible. This allows partial applications inside
+ expressions to become fully applied and exposes new transformation
+ opportunities for other transformations (like β-reduction and
+ specialization).
+
+ \starttrans
+ (letrec binds in E) M
+ ------------------------
+ letrec binds in E M
+ \stoptrans
- \subsubsection{Let flattening}
- This transformation puts nested lets in the same scope, by lifting the
- binding(s) of the inner let into a new let around the outer let. Eventually,
- this will cause all let bindings to appear in the same scope (they will all be
- in scope for the function return value).
+ % And an example
+ \startbuffer[from]
+ ( letrec
+ val = 1
+ in
+ add val
+ ) 3
+ \stopbuffer
+
+ \startbuffer[to]
+ letrec
+ val = 1
+ in
+ add val 3
+ \stopbuffer
- Note that this transformation does not try to be smart when faced with
- recursive lets, it will just leave the lets recursive (possibly joining a
- recursive and non-recursive let into a single recursive let). The let
- rederecursification transformation will do this instead.
+ \transexample{Application propagation for a let expression}{from}{to}
\starttrans
- letnonrec x = (let bindings in M) in N
+ (case x of
+ p1 -> E1
+ \vdots
+ pn -> En) M
+ -----------------
+ case x of
+ p1 -> E1 M
+ \vdots
+ pn -> En M
+ \stoptrans
+
+ % And an example
+ \startbuffer[from]
+ ( case x of
+ True -> id
+ False -> neg
+ ) 1
+ \stopbuffer
+
+ \startbuffer[to]
+ case x of
+ True -> id 1
+ False -> neg 1
+ \stopbuffer
+
+ \transexample{Application propagation for a case expression}{from}{to}
+
+ \subsubsection{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
+ transformations simpler: They can simply assume all lets are
+ recursive.
+
+ \starttrans
+ let
+ a = E
+ in
+ M
------------------------------------------
- let bindings in (letnonrec x = M) in N
+ letrec
+ a = E
+ in
+ M
\stoptrans
+ \subsubsection{Let flattening}
+ This transformation puts nested lets in the same scope, by lifting the
+ binding(s) of the inner let into a new let around the outer let. Eventually,
+ this will cause all let bindings to appear in the same scope (they will all be
+ in scope for the function return value).
+
\starttrans
letrec
\vdots
- x = (let bindings in M)
+ x = (letrec bindings in M)
\vdots
in
N
\stoptrans
\startbuffer[from]
- let
+ letrec
a = letrec
x = 1
y = 2
in
x + y
in
- letrec
- b = let c = 3 in a + c
- d = 4
- in
- d + b
+ a
\stopbuffer
\startbuffer[to]
letrec
x = 1
y = 2
+ a = x + y
in
- let
- a = x + y
- in
- letrec
- c = 3
- b = a + c
- d = 4
- in
- d + b
+ a
\stopbuffer
\transexample{Let flattening}{from}{to}
\lam{E}, any \lam{E} can be transformed, while we only mean the \lam{E} that
is bound by \lam{x}. This might need some extra notes or something).
+ 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, of course. 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 representable 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
- let x = E in x
+ letrec x = E in x
\stoptrans
\starttrans
~ \lam{E} is representable
E \lam{E} is not a let expression
--------------------------- \lam{E} is not a local variable reference
- let x = E in x
+ letrec x = E in x
\stoptrans
\starttrans
~ \lam{E} is representable
E \lam{E} is not a local variable reference
---------------------------
- let x = E in x
+ letrec x = E in x
\stoptrans
\startbuffer[from]
\stopbuffer
\startbuffer[to]
- x = let x = add 1 2 in x
+ x = letrec x = add 1 2 in x
\stopbuffer
\transexample{Return value simplification}{from}{to}
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
\starttrans
M N
-------------------- \lam{N} is of a representable type
- let x = N in M x \lam{N} is not a local variable reference
+ letrec x = N in M x \lam{N} is not a local variable reference
\stoptrans
\startbuffer[from]
\stopbuffer
\startbuffer[to]
- let x = add a 1 in add x 1
+ letrec x = add a 1 in add x 1
\stopbuffer
\transexample{Argument extraction}{from}{to}
\starttrans
M N \lam{M} is a (partial aplication of a) builtin function.
--------------------- \lam{f0 ... fn} = free local variables of \lam{N}
- M x f0 ... fn \lam{N :: a -> b}
+ M (x f0 ... fn) \lam{N :: a -> b}
~ \lam{N} is not a (partial application of) a top level function
x = λf0 ... λfn.N
\stoptrans
\stopbuffer
\startbuffer[to]
- x0 = λb.λa.add a b
- ~
- map x0 xs
+ map (x0 b) xs
- x1 = λb.add b
map x1 ys
+ ~
+ x0 = λb.λa.add a b
+ x1 = λb.add b
\stopbuffer
\transexample{Function extraction}{from}{to}
+ 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}.
inc = λa.f a 1
\stoplambda
- we could {\em propagate} the constant argument 1, with the following
+ We could {\em propagate} the constant argument 1, with the following
result:
\startlambda
\stoptrans
- TODO: Example
+ \todo{Example}
\subsection{Case simplification}
\subsubsection{Scrutinee simplification}
case E of
alts
----------------- \lam{E} is not a local variable reference
- let x = E in
+ letrec x = E in
case E of
alts
\stoptrans
\stopbuffer
\startbuffer[to]
- let x = foo a in
+ letrec x = foo a in
case x of
True -> a
False -> b
\vdots
Cn vn,0 ... vn,m -> En
--------------------------------------------------- \forall i \forall j, 0 <= i <= n, 0 <= i < m (\lam{wi,j} is a wild (unused) binder)
- letnonrec
+ letrec
v0,0 = case x of C0 v0,0 .. v0,m -> v0,0
\vdots
v0,m = case x of C0 v0,0 .. v0,m -> v0,m
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
(,) b c -> add b c
\stopbuffer
\startbuffer[to]
- letnonrec
+ letrec
b = case a of (,) b c -> b
c = case a of (,) b c -> c
x0 = add b c
\transexample{Case removal}{from}{to}
- \subsection{Monomorphisation}
- TODO: Better name for this section
-
+ \subsection{Removing polymorphism}
Reference type-specialization (== argument propagation)
- \subsubsection{Defunctionalization}
+ Reference polymporphic binding inlining (== non-representable binding
+ inlining).
+
+ \subsection{Defunctionalization}
+ 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}
+
Reference higher-order-specialization (== argument propagation)
\subsubsection{Non-representable binding inlining}
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
- letnonrec a = E in M
- -------------------------- \lam{E} has a non-representable type.
- M[E/a]
- \stoptrans
\starttrans
letrec
+ a0 = E0
\vdots
- a = E
+ ai = Ei
\vdots
+ an = En
in
M
- -------------------------- \lam{E} has a non-representable type.
+ -------------------------- \lam{Ei} has a non-representable type.
letrec
- \vdots [E/a]
- \vdots [E/a]
+ a0 = E0 [Ei/ai]
+ \vdots
+ ai-1 = Ei-1 [Ei/ai]
+ ai+1 = Ei+1 [Ei/ai]
+ \vdots
+ an = En [Ei/ai]
in
- M[E/a]
+ M[Ei/ai]
\stoptrans
\startbuffer[from]
letrec
a = smallInteger 10
- inc = λa -> add a 1
+ inc = λb -> add b 1
inc' = add 1
x = fromInteger a
in
letrec
x = fromInteger (smallInteger 10)
in
- (λa -> add a 1) (add 1 x)
+ (λb -> add b 1) (add 1 x)
\stopbuffer
- \transexample{Let flattening}{from}{to}
+ \transexample{None representable binding inlining}{from}{to}
\section{Provable properties}
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