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
M
\stoptrans
- \subsubsection{Simple let binding removal}
+ \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
TODO
\section{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{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
+ (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{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
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.
+ dederecursification transformation will do this instead.
\starttrans
letnonrec x = (let bindings in M) in N
\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
\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}
projects / matthijs / master-project / report.git / commitdiff