% 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]
}
}
\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))
In the following sections, we will be using a number of functions and
notations, which we will define here.
+ TODO: Define substitution
+
\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
\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
+ 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,
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
+ \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.
- \section{Program structure}
+ 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).
+
+ 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
specialization).
\starttrans
- (let binds in E) M
- -----------------
- let binds in E M
+ (letrec binds in E) M
+ ------------------------
+ letrec binds in E M
\stoptrans
% And an example
\startbuffer[from]
- ( let
+ ( letrec
val = 1
in
add val
\stopbuffer
\startbuffer[to]
- let
+ letrec
val = 1
in
add val 3
\transexample{Application propagation for a case expression}{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{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
+ ------------------------------------------
+ letrec
+ a = E
+ in
+ M
+ \stoptrans
\subsubsection{Let flattening}
This transformation puts nested lets in the same scope, by lifting the
this will cause all let bindings to appear in the same scope (they will all be
in scope for the function return value).
- 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
- dederecursification transformation will do this instead.
-
- \starttrans
- letnonrec x = (let bindings in M) in N
- ------------------------------------------
- let bindings in (letnonrec x = M) in N
- \stoptrans
-
\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} 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}
\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}
This transform deals with arguments to user-defined functions that are
not representable at runtime. This means these arguments cannot be
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
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
(,) 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
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}
projects / matthijs / master-project / report.git / blobdiff