XGitUrl: https://git.stderr.nl/gitweb?p=matthijs%2Fmasterproject%2Freport.git;a=blobdiff_plain;f=Core2Core.tex;h=1f258d31028dd4466749f542c9523ffabe2df490;hp=bc385a68324b210e435dbe1f42cbfed975099f8a;hb=204e3063cbdc2825e3f78ae0261dbf30d4cf38e0;hpb=95b1a682e51c47d635d5bafe75bd7096e8d4ec18
diff git a/Core2Core.tex b/Core2Core.tex
index bc385a6..1f258d3 100644
 a/Core2Core.tex
+++ b/Core2Core.tex
@@ 28,6 +28,15 @@
% A transformation
\definefloat[transformation][transformations]
\define[2]\transform{
+ \startframedtext[width=\textwidth]
+ #2
+ \stopframedtext
+}
+
+\define\conclusion{\blackrule[height=0.5pt,depth=0pt,width=.5\textwidth]}
+\define\nextrule{\vskip1cm}
+
+\define[2]\transformold{
%\placetransformation[here]{#1}
\startframedtext[width=\textwidth]
\startformula \startalign
@@ 36,16 +45,71 @@
\stopframedtext
}
+% A shortcut for italicized e.g. and i.e.
+\define[0]\eg{{\em e.g.}}
+\define[0]\ie{{\em i.e.}}
+
+\definedescription
+ [desc]
+ [location=hanging,hang=20,width=broad]
+ %command=\hskip1cm,margin=1cm]
+
% Install the lambda calculus prettyprinter, as defined in pretlam.lua.
\installprettytype [LAM] [LAM]
+\definetyping[lambda][option=LAM,style=sans]
+\definetype[lam][option=LAM,style=sans]
+
+% An (invisible) frame to hold a lambda expression
+\define[1]\lamframe{
+ % Put a frame around lambda expressions, so they can have multiple
+ % lines and still appear inline.
+ % The align=right option really does leftalignment, but without the
+ % program will end up on a single line. The strut=no option prevents a
+ % bunch of empty space at the start of the frame.
+ \framed[offset=0mm,location=middle,strut=no,align=right,frame=off]{#1}
+}
+
+\define[2]\transbuf{
+ % Make \typebuffer uses the LAM pretty printer and a sansserif font
+ % Also prevent any extra spacing above and below caused by the default
+ % before=\blank and after=\blank.
+ \setuptyping[option=LAM,style=sans,before=,after=]
+ % Prevent the arrow from ending up below the first frame (a \framed
+ % at the start of a line defaults to using vmode).
+ \dontleavehmode
+ % Put the elements in frames, so they can have multiple lines and be
+ % middlealigned
+ \lamframe{\typebuffer[#1]}
+ \lamframe{\Rightarrow}
+ \lamframe{\typebuffer[#2]}
+ % Reset the typing settings to their defaults
+ \setuptyping[option=none,style=\tttf]
+}
+% This is the same as \transbuf above, but it accepts text directly instead
+% of through buffers. This only works for single lines, however.
+\define[2]\trans{
+ \dontleavehmode
+ \lamframe{\lam{#1}}
+ \lamframe{\Rightarrow}
+ \lamframe{\lam{#2}}
+}
+
+
% A helper to print a single example in the half the page width. The example
% text should be in a buffer whose name is given in an argument.
%
% The align=right option really does leftalignment, but without the program
% will end up on a single line. The strut=no option prevents a bunch of empty
% space at the start of the frame.
\define[1]\example{\framed[frameoffset=2mm,align=right,strut=no]{\typebuffer[#1]}}
+\define[1]\example{
+ \framed[offset=1mm,align=right,strut=no]{
+ \setuptyping[option=LAM,style=sans,before=,after=]
+ \typebuffer[#1]
+ \setuptyping[option=none,style=\tttf]
+ }
+}
+
% A transformation example
\definefloat[example][examples]
@@ 60,11 +124,11 @@
}
\define[3]\transexampleh{
 \placeexample[here]{#1}
 \startcombination[1*2]
 {\example{#2}}{Original program}
 {\example{#3}}{Transformed program}
 \stopcombination
+% \placeexample[here]{#1}
+% \startcombination[1*2]
+% {\example{#2}}{Original program}
+% {\example{#3}}{Transformed program}
+% \stopcombination
}
% Define a custom description format for the builtinexprs below
@@ 76,42 +140,31 @@ Matthijs Kooijman
\section{Introduction}
As a new approach to translating Core to VHDL, we investigate a number of
transformations on our Core program, which should bring the program into a
welldefined "canonical" form, which is subsequently trivial to translate to
VHDL.

The transformations as presented here are far from complete, but are meant as
an exploration of possible transformations. In the running example below, we
apply each of the transformations exactly once, in sequence. As will be
apparent from the end result, there will be additional transformations needed
to fully reach our goal, and some transformations must be applied more than
once. How exactly to (efficiently) do this, has not been investigated.

Lastly, I hope to be able to state a number of pre and postconditions for
each transformation. If these can be proven for each transformation, and it
can be shown that there exists some ordering of transformations for which the
postcondition implies the canonical form, we can show that the transformations
do indeed transform any program (probably satisfying a number of
preconditions) to the canonical form.
+transforms on our Core program, which should bring the program into a
+welldefined {\em normal} form, which is subsequently trivial to
+translate to VHDL.
+
+The transforms as presented here are far from complete, but are meant as
+an exploration of possible transformations.
\section{Goal}
The transformations described here have a welldefined goal: To bring the
program in a welldefined form that is directly translatable to hardware,
while fully preserving the semantics of the program.
This {\em canonical form} is again a Core program, but with a very specific
structure. A function in canonical form has nested lambda's at the top, which
+This {\em normal form} is again a Core program, but with a very specific
+structure. A function in normal form has nested lambda's at the top, which
produce a let expression. This let expression binds every function application
in the function and produces either a simple identifier or a tuple of
identifiers. Every bound value in the let expression is either a simple
function application or a case expression to extract a single element from a
tuple returned by a function.
+in the function and produces a simple identifier. Every bound value in
+the let expression is either a simple function application or a case
+expression to extract a single element from a tuple returned by a
+function.
An example of a program in canonical form would be:
\starttyping
+\startlambda
 All arguments are an inital lambda
 \x c d >
+ Î»x.Î»c.Î»d.
 There is one let expression at the top level
let
 Calling some other userdefined function.
@@ 132,29 +185,21 @@ An example of a program in canonical form would be:
in
 The actual result
r
\stoptyping

In this and all following programs, the following definitions are assumed to
be available:

\starttyping
data Bit = Low  High

foo :: Int > (Bit, Bit)
add :: Int > Int > Int
sub :: Int > Int > Int
\stoptyping
+\stoplambda
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 are
the output ports. Each function application bound by the let expression
defines a component instantiation, where the input and output ports are mapped
to local signals or arguments. The tuple extracting case expressions don't map
to

\subsection{Canonical form definition}
Formally, the canonical form is a core program obeying the following
constraints.
+lambda's define the input ports. The value produced by the let expression is
+the output port. Most function applications bound by the let expression
+define a component instantiation, where the input and output ports are mapped
+to local signals or arguments. Some of the others use a builtin
+construction (\eg the \lam{case} statement) or call a builtin function
+(\eg \lam{add} or \lam{sub}). For these, a hardcoded VHDL translation is
+available.
+
+\subsection{Normal definition}
+Formally, the normal form is a core program obeying the following
+constraints. TODO: Update this section, this is probably not completely
+accurate or relevant anymore.
\startitemize[R,inmargin]
\item All top level binds must have the form $\expr{\bind{fun}{lamexpr}}$.
@@ 196,34 +241,376 @@ be any of $x_0$ to $x_n$. A case expression must have a $hardware\;type$.
\item TODO: Many more!
\stopitemize
\section{Transformation passes}
+\section{Transform passes}
+
+In this section we describe the actual transforms. Here we're using
+the core language in a notation that resembles lambda calculus.
+
+Each of these transforms is meant to be applied to every (sub)expression
+in a program, for as long as it applies. Only when none of the
+expressions can be applied anymore, the program is in normal form. We
+hope to be able to prove that this form will obey all of the constraints
+defined above, but this has yet to happen (though it seems likely that
+it will).
+
+Each of the transforms will be described informally first, explaining
+the need for and goal of the transform. Then, a formal definition is
+given, using a familiar syntax from the world of logic. Each transform
+is specified as a number of conditions (above the horizontal line) and a
+number of conclusions (below the horizontal line). The details of using
+this notation are still a bit fuzzy, so comments are welcom.
+
+\subsection{Î·abstraction}
+This transformation makes sure that all arguments of a functiontyped
+expression are named, by introducing lambda expressions. When combined with
+Î²reduction and function inlining below, all functiontyped expressions should
+be lambda abstractions or global identifiers.
+
+\transform{Î·abstraction}
+{
+\lam{E :: * > *}
+
+\lam{E} is not the first argument of an application.
+
+\lam{E} is not a lambda abstraction.
In this section we describe the actual transformations. Here we're using
mostly Corelike notation, with a few notable points.
+\lam{x} is a variable that does not occur free in E.
+
+\conclusion
+
+\trans{E}{Î»x.E x}
+}
+
+\startbuffer[from]
+foo = Î»a > case a of
+ True > Î»b.mul b b
+ False > id
+\stopbuffer
+
+\startbuffer[to]
+foo = Î»a.Î»x > (case a of
+ True > Î»b.mul b b
+ False > Î»y.id y) x
+\stopbuffer
+
+\transexample{Î·abstraction}{from}{to}
+
+\subsection{Extended Î²reduction}
+This transformation is meant to propagate application expressions downwards
+into expressions as far as possible. In lambda calculus, this reduction
+is known as Î²reduction, but it is of course only defined for
+applications of lambda abstractions. We extend this reduction to also
+work for the rest of core (case and let expressions).
+\startbuffer[from]
+(case x of
+ p1 > E1
+ \vdots
+ pn > En) M
+\stopbuffer
+\startbuffer[to]
+case x of
+ p1 > E1 M
+ \vdots
+ pn > En M
+\stopbuffer
+
+\transform{Extended Î²reduction}
+{
+\conclusion
+\trans{(Î»x.E) M}{E[M/x]}
+
+\nextrule
+\conclusion
+\trans{(let binds in E) M}{let binds in E M}
+
+\nextrule
+\conclusion
+\transbuf{from}{to}
+}
+
+\startbuffer[from]
+let a = (case x of
+ True > id
+ False > neg
+ ) 1
+ b = (let y = 3 in add y) 2
+in
+ (Î»z.add 1 z) 3
+\stopbuffer
+
+\startbuffer[to]
+let a = case x of
+ True > id 1
+ False > neg 1
+ b = let y = 3 in add y 2
+in
+ add 1 3
+\stopbuffer
+
+\transexample{Extended Î²reduction}{from}{to}
+
+\subsection{Argument simplification}
+The transforms in this section deal with simplifying application
+arguments into normal form. The goal here is to:
\startitemize
\item A core expression (in contrast with a transformation function, for
example), is enclosed in pipes. For example, $\app{transform}{\expr{\lam{z}{z+1}}}$
is the transform function applied to a lambda core expression.

Note that this notation might not be consistently applied everywhere. In
particular where a noncore function is used inside a core expression, things
get slightly confusing.
\item A bind is written as $\expr{\bind{x}{expr}}$. This means binding the identifier
$x$ to the expression $expr$.
\item In the core examples, the layout rule from Haskell is loosely applied.
It should be evident what was meant from indentation, even though it might nog
be strictly correct.
+ \item Make all arguments of userdefined functions (\eg, of which
+ we have a function body) simple variable references of a runtime
+ representable type.
+ \item Make all arguments of builtin functions either:
+ \startitemize
+ \item A type argument.
+ \item A dictionary argument.
+ \item A type level expression.
+ \item A variable reference of a runtime representable type.
+ \item A variable reference or partial application of a function type.
+ \stopitemize
\stopitemize
\subsection{Example}
In the descriptions of transformations below, the following (slightly
contrived) example program will be used as the running example. Note that this
the example for the canonical form given above is the same program, but in
canonical form.
+When looking at the arguments of a userdefined function, we can
+divide them into two categories:
+\startitemize
+ \item Arguments with a runtime representable type (\eg bits or vectors).
+
+ These arguments can be preserved in the program, since they can
+ be translated to input ports later on. However, since we can
+ only connect signals to input ports, these arguments must be
+ reduced to simple variables (for which signals will be
+ produced). This is taken care of by the argument extraction
+ transform.
+ \item Nonruntime representable typed arguments.
+
+ These arguments cannot be preserved in the program, since we
+ cannot represent them as input or output ports in the resulting
+ VHDL. To remove them, we create a specialized version of the
+ called function with these arguments filled in. This is done by
+ the argument propagation transform.
+\stopitemize
+
+When looking at the arguments of a builtin function, we can divide them
+into categories:
+
+\startitemize
+ \item Arguments with a runtime representable type.
+
+ As we have seen with userdefined functions, these arguments can
+ always be reduced to a simple variable reference, by the
+ argument extraction transform. Performing this transform for
+ builtin functions as well, means that the translation of builtin
+ functions can be limited to signal references, instead of
+ needing to support all possible expressions.
+
+ \item Arguments with a function type.
+
+ These arguments are functions passed to higher order builtins,
+ like \lam{map} and \lam{foldl}. Since implementing these
+ functions for arbitrary functiontyped expressions (\eg, lambda
+ expressions) is rather comlex, we reduce these arguments to
+ (partial applications of) global functions.
+
+ We can still support arbitrary expressions from the user code,
+ by creating a new global function containing that expression.
+ This way, we can simply replace the argument with a reference to
+ that new function. However, since the expression can contain any
+ number of free variables we also have to include partial
+ applications in our normal form.
+
+ This category of arguments is handled by the function extraction
+ transform.
+ \item Other unrepresentable arguments.
+
+ These arguments can take a few different forms:
+ \startdesc{Type arguments}
+ In the core language, type arguments can only take a single
+ form: A type wrapped in the Type constructor. Also, there is
+ nothing that can be done with type expressions, except for
+ applying functions to them, so we can simply leave type
+ arguments as they are.
+ \stopdesc
+ \startdesc{Dictionary arguments}
+ In the core language, dictionary arguments are used to find
+ operations operating on one of the type arguments (mostly for
+ finding class methods). Since we will not actually evaluatie
+ the function body for builtin functions and can generate
+ code for builtin functions by just looking at the type
+ arguments, these arguments can be ignored and left as they
+ are.
+ \stopdesc
+ \startdesc{Type level arguments}
+ Sometimes, we want to pass a value to a builtin function, but
+ we need to know the value at compile time. Additionally, the
+ value has an impact on the type of the function. This is
+ encoded using typelevel values, where the actual value of the
+ argument is not important, but the type encodes some integer,
+ for example. Since the value is not important, the actual form
+ of the expression does not matter either and we can leave
+ these arguments as they are.
+ \stopdesc
+ \startdesc{Other arguments}
+ Technically, there is still a wide array of arguments that can
+ be passed, but does not fall into any of the above categories.
+ However, none of the supported builtin functions requires such
+ an argument. This leaves use with passing unsupported types to
+ a function, such as calling \lam{head} on a list of functions.
+
+ In these cases, it would be impossible to generate hardware
+ for such a function call anyway, so we can ignore these
+ arguments.
+
+ The only way to generate hardware for builtin functions with
+ arguments like these, is to expand the function call into an
+ equivalent core expression (\eg, expand map into a series of
+ function applications). But for now, we choose to simply not
+ support expressions like these.
+ \stopdesc
+
+ From the above, we can conclude that we can simply ignore these
+ other unrepresentable arguments and focus on the first two
+ categories instead.
+\stopitemize
+
+\subsubsection{Argument extraction}
+This transform deals with arguments to functions that
+are of a runtime representable type.
+
+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
+or False), which are variable references of a runtime representable
+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
+expression to a new variable. The original function is then applied to
+this variable.
+
+\transform{Argument extract}
+{
+\lam{Y} is of a hardware representable type
+
+\lam{Y} is not a variable referene
+
+\conclusion
+
+\trans{X Y}{let z = Y in X z}
+}
+
+\subsubsection{Function extraction}
+This transform deals with functiontyped arguments to builtin functions.
+Since these arguments cannot be propagated, we choose to extract them
+into a new global function instead.
+
+Any free variables occuring in the extracted arguments will become
+parameters to the new global function. The original argument is replaced
+with a reference to the new function, applied to any free variables from
+the original argument.
+
+\transform{Function extraction}
+{
+\lam{X} is a (partial application of) a builtin function
+
+\lam{Y} is not an application
+
+\lam{Y} is not a variable reference
+
+\conclusion
+
+\lam{f0 ... fm} = free local vars of \lam{Y}
+
+\lam{y} is a new global variable
+
+\lam{y = Î»f0 ... fn.Y}
\starttyping
 \x >
+\trans{X Y}{X (y f0 ... fn)}
+}
+
+\subsubsection{Argument propagation}
+This transform deals with arguments to userdefined functions that are
+not representable at runtime. This means these arguments cannot be
+preserved in the final form and most be {\em propagated}.
+
+Propagation means to create a specialized version of the called
+function, with the propagated argument already filled in. As a simple
+example, in the following program:
+
+\startlambda
+f = Î»a.Î»b.a + b
+inc = Î»a.f a 1
+\stoplambda
+
+we could {\em propagate} the constant argument 1, with the following
+result:
+
+\startlambda
+f' = Î»a.a + 1
+inc = Î»a.f' a
+\stoplambda
+
+Special care must be taken when the tobepropagated expression has any
+free variables. If this is the case, the original argument should not be
+removed alltogether, but replaced by all the free variables of the
+expression. In this way, the original expression can still be evaluated
+inside the new function. Also, this brings us closer to our goal: All
+these free variables will be simple variable references.
+
+To prevent us from propagating the same argument over and over, a simple
+local variable reference is not propagated (since is has exactly one
+free variable, itself, we would only replace that argument with itself).
+
+This shows that any free local variables that are not runtime representable
+cannot be brought into normal form by this transform. We rely on an
+inlining transformation to replace such a variable with an expression we
+can propagate again.
+
+TODO: Move these definitions somewhere sensible.
+
+Definition: A global variable is any variable that is bound at the
+top level of a program. A local variable is any other variable.
+
+Definition: A hardware representable type is a type that we can generate
+a signal for in hardware. For example, a bit, a vector of bits, a 32 bit
+unsigned word, etc. Types that are not runtime representable notably
+include (but are not limited to): Types, dictionaries, functions.
+
+Definition: A builtin function is a function for which a builtin
+hardware translation is available, because its actual definition is not
+translatable. A userdefined function is any other function.
+
+\transform{Argument propagation}
+{
+\lam{x} is a global variable, bound to a userdefined function
+
+\lam{x = E}
+
+\lam{Y_i} is not of a runtime representable type
+
+\lam{Y_i} is not a local variable reference
+
+\conclusion
+
+\lam{f0 ... fm} = free local vars of \lam{Y_i}
+
+\lam{x'} is a new global variable
+
+\lam{x' = Î»y0 ... yi1 f0 ... fm yi+1 ... yn . E y0 ... yi1 Yi yi+1 ... yn}
+
+\trans{x Y0 ... Yi ... Yn}{x' y0 ... yi1 f0 ... fm Yi+1 ... Yn}
+}
+
+TODO: The above definition looks too complicated... Can we find
+something more concise?
+
+\subsection{Example sequence}
+
+This section lists an example expression, with a sequence of transforms
+applied to it. The exact transforms given here probably don't exactly
+match the transforms given above anymore, but perhaps this can clarify
+the big picture a bit.
+
+TODO: Update or remove this section.
+
+\startlambda
+ Î»x.
let s = foo x
in
case s of
@@ 233,29 +620,15 @@ canonical form.
Low > let
op' = case b of
High > sub
 Low > \c d > c
+ Low > Î»c.Î»d.c
in
 \c d > op' d c
\stoptyping

\subsection{Argument extraction}
This transformation makes sure that all of a bindings arguments are always
bound to variables at the top level of the bound value. Formally, we can
describe this transformation as follows.

\transform{Argument extraction}
{
\NC \app{transform}{\expr{\bind{f}{expr}}} \NC = \expr{\bind{f}{\app{transform'(expr)}}}\NR
\NR
\NC \app{transform'}{\expr{\lam{v}{expr}}} \NC = \expr{\lam{v}{\app{transform'}{expr}}}\NR
\NC \app{transform'}{\expr{expr :: a \xrightarrow b}} \NC = \expr{\lam{x}{\app{transform'}{\expr{(\app{expr}{x})}}}} \NR
}
+ Î»c.Î»d.op' d c
+\stoplambda
When applying this transformation to our running example, we get the following
program.
+After toplevel Î·abstraction:
\starttyping
 \x c d >
+\startlambda
+ Î»x.Î»c.Î»d.
(let s = foo x
in
case s of
@@ 265,38 +638,16 @@ program.
Low > let
op' = case b of
High > sub
 Low > \c d > c
+ Low > Î»c.Î»d.c
in
 \c d > op' d c
+ Î»c.Î»d.op' d c
) c d
\stoptyping

\startbuffer[from]
foo = \x > case x of True > (\y > mul y y); False > id
\stopbuffer
\startbuffer[to]
foo = \x z > (case x of True > (\y > mul y y); False > id) z
\stopbuffer

\transexampleh{Argument extraction example}{from}{to}

\subsection{Application propagation}
This transformation is meant to propagate application expressions downwards
into expressions as far as possible. Formally, we can describe this
transformation as follows.

\transform{Application propagation}
{
\NC \app{transform}{\expr{\app{(\letexpr{binds}{expr})}{y}}} \NC = \expr{\letexpr{binds}{(\app{expr}{y})}}\NR
\NC \app{transform}{\expr{\app{(\lam{x}{expr})}{y}}} \NC = \app{\app{subs}{x \xRightarrow y}}{\expr{expr}}\NR
\NC \app{transform}{\expr{\app{(\case{x}{\alt{p}{e};...})}{y}}} \NC = \expr{\case{x}{\alt{p}{\app{e}{y}};...}}\;(for\;every\;alt)\NR
}
+\stoplambda
When applying this transformation to our running example, we get the following
program.
+After (extended) Î²reduction:
\starttyping
 \x c d >
+\startlambda
+ Î»x.Î»c.Î»d.
let s = foo x
in
case s of
@@ 306,134 +657,190 @@ program.
Low > let
op' = case b of
High > sub
 Low > \c d > c
+ Low > Î»c.Î»d.c
in
op' d c
\stoptyping
+\stoplambda
\startbuffer[from]
foo = \x z > (case x of True > (\y > mul y y); False > id) z
\stopbuffer
\startbuffer[to]
foo = \x z > case x of True > mul z z; False > id z
\stopbuffer
+After return value extraction:
\transexampleh{Application propagation example}{from}{to}
+\startlambda
+ Î»x.Î»c.Î»d.
+ let s = foo x
+ r = case s of
+ (a, b) >
+ case a of
+ High > add c d
+ Low > let
+ op' = case b of
+ High > sub
+ Low > Î»c.Î»d.c
+ in
+ op' d c
+ in
+ r
+\stoplambda
\subsection{Introducing main scope}
This transformation is meant to introduce a single let expression that will be
the "main scope". This is the let expression as described under requirement
\ref[letexpr]. This let expression will contain only a single binding, which
binds the original expression to some identifier and then evalutes to just
this identifier (to comply with requirement \in[retexpr]).
+Scrutinee simplification does not apply.
Formally, we can describe the transformation as follows.
+After case binder wildening:
\transform{Main scope introduction}
{
\NC \app{transform}{\expr{\bind{f}{expr}}} \NC = \expr{\bind{f}{\app{transform'(expr)}}}\NR
\NR
\NC \app{transform'}{\expr{\lam{v}{expr}}} \NC = \expr{\lam{v}{\app{transform'}{expr}}}\NR
\NC \app{transform'}{\expr{expr}} \NC = \expr{\letexpr{\bind{x}{expr}}{x}} \NR
}
+\startlambda
+ Î»x.Î»c.Î»d.
+ let s = foo x
+ a = case s of (a, _) > a
+ b = case s of (_, b) > b
+ r = case s of (_, _) >
+ case a of
+ High > add c d
+ Low > let op' = case b of
+ High > sub
+ Low > Î»c.Î»d.c
+ in
+ op' d c
+ in
+ r
+\stoplambda
When applying this transformation to our running example, we get the following
program.
+After case value simplification
\starttyping
 \x c d >
 let r = (let s = foo x
 in
 case s of
 (a, b) >
 case a of
 High > add c d
 Low > let
 op' = case b of
 High > sub
 Low > \c d > c
 in
 op' d c
 )
+\startlambda
+ Î»x.Î»c.Î»d.
+ let s = foo x
+ a = case s of (a, _) > a
+ b = case s of (_, b) > b
+ r = case s of (_, _) > r'
+ rh = add c d
+ rl = let rll = Î»c.Î»d.c
+ op' = case b of
+ High > sub
+ Low > rll
+ in
+ op' d c
+ r' = case a of
+ High > rh
+ Low > rl
in
r
\stoptyping

\subsection{Scope flattening}
This transformation tries to flatten the topmost let expression in a bind,
{\em i.e.}, bind all identifiers in the same scope, and bind them to simple
expressions only (so simplify deeply nested expressions).

Formally, we can describe the transformation as follows.

\transform{Main scope introduction} { \NC \app{transform}{\expr{\bind{f}{expr}}} \NC = \expr{\bind{f}{\app{transform'(expr)}}}\NR
\NR
\NC \app{transform'}{\expr{\lam{v}{expr}}} \NC = \expr{\lam{v}{\app{transform'}{expr}}}\NR
\NC \app{transform'}{\expr{\letexpr{binds}{expr}}} \NC = \expr{\letexpr{\app{concat . map . flatten}{binds}}{expr}}\NR
\NR
\NC \app{flatten}{\expr{\bind{x}{\letexpr{binds}{expr}}}} \NC = (\app{concat . map . flatten}{binds}) \cup \{\app{flatten}{\expr{\bind{x}{expr}}}\}\NR
\NC \app{flatten}{\expr{\bind{x}{\case{s}{alts}}}} \NC = \app{concat}{binds'} \cup \{\bind{x}{\case{s}{alts'}}\}\NR
\NC \NC \where{(binds', alts')=\app{unzip.map.(flattenalt s)}{alts}}\NR
\NC \app{\app{flattenalt}{s}}{\expr{\alt{\app{con}{x_0\;..\;x_n}}{expr}}} \NC = (extracts \cup \{\app{flatten}{bind}\}, alt)\NR
\NC \NC \where{extracts =\{\expr{\case{s}{\alt{\app{con}{x_0\;..\;x_n}}{x_0}}},}\NR
\NC \NC \;..\;,\expr{\case{s}{\alt{\app{con}{x_0\;..\;x_n}}{x_n}}}\} \NR
\NC \NC bind = \expr{\bind{y}{expr}}\NR
\NC \NC alt = \expr{\alt{\app{con}{\_\;..\;\_}}{y}}\NR
}
+\stoplambda
When applying this transformation to our running example, we get the following
program.
+After let flattening:
\starttyping
 \x c d >
+\startlambda
+ Î»x.Î»c.Î»d.
let s = foo x
 r = case s of
 (_, _) > y
 a = case s of (a, b) > a
 b = case s of (a, b) > b
 y = case a of
 High > g
 Low > h
 g = add c d
 h = op' d c
+ a = case s of (a, _) > a
+ b = case s of (_, b) > b
+ r = case s of (_, _) > r'
+ rh = add c d
+ rl = op' d c
+ rll = Î»c.Î»d.c
op' = case b of
 High > i
 Low > j
 i = sub
 j = \c d > c
+ High > sub
+ Low > rll
+ r' = case a of
+ High > rh
+ Low > rl
in
r
\stoptyping
+\stoplambda
\subsection{More transformations}
As noted before, the above transformations are not complete. Other needed
transformations include:
\startitemize
\item Inlining of local identifiers with a function type. Since these cannot
be represented in hardware directly, they must be transformed into something
else. Inlining them should always be possible without loss of semantics (TODO:
How true is this?) and can expose new possibilities for other transformations
passes (such as application propagation when inlining {\tt j} above).
\item A variation on inlining local identifiers is the propagation of
function arguments with a function type. This will probably be initiated when
transforming the caller (and not the callee), but it will also deal with
identifiers with a function type that are unrepresentable in hardware.

Special care must be taken here, since the expression that is propagated into
the callee comes from a different scope. The function typed argument must thus
be replaced by any identifiers from the callers scope that the propagated
expression uses.

Note that propagating an argument will change both a function's interface and
implementation. For this to work, a new function should be created instead of
modifying the original function, so any other callers will not be broken.
\item Something similar should happen with return values with function types.
\item Polymorphism must be removed from all userdefined functions. This is
again similar to propagation function typed arguments, since this will also
create duplicates of functions (for a specific type). This is an operation
that is commonly known as "specialization" and already happens in GHC (since
nonpolymorph functions can be a lot faster than generic ones).
\item More builtin expressions should be added and these should be evaluated
by the compiler. For example, map, fold, +.
\stopitemize
+After function inlining:
+
+\startlambda
+ Î»x.Î»c.Î»d.
+ let s = foo x
+ a = case s of (a, _) > a
+ b = case s of (_, b) > b
+ r = case s of (_, _) > r'
+ rh = add c d
+ rl = (case b of
+ High > sub
+ Low > Î»c.Î»d.c) d c
+ r' = case a of
+ High > rh
+ Low > rl
+ in
+ r
+\stoplambda
+
+After (extended) Î²reduction again:
+
+\startlambda
+ Î»x.Î»c.Î»d.
+ let s = foo x
+ a = case s of (a, _) > a
+ b = case s of (_, b) > b
+ r = case s of (_, _) > r'
+ rh = add c d
+ rl = case b of
+ High > sub d c
+ Low > d
+ r' = case a of
+ High > rh
+ Low > rl
+ in
+ r
+\stoplambda
+
+After case value simplification again:
+
+\startlambda
+ Î»x.Î»c.Î»d.
+ let s = foo x
+ a = case s of (a, _) > a
+ b = case s of (_, b) > b
+ r = case s of (_, _) > r'
+ rh = add c d
+ rlh = sub d c
+ rl = case b of
+ High > rlh
+ Low > d
+ r' = case a of
+ High > rh
+ Low > rl
+ in
+ r
+\stoplambda
+
+After case removal:
+
+\startlambda
+ Î»x.Î»c.Î»d.
+ let s = foo x
+ a = case s of (a, _) > a
+ b = case s of (_, b) > b
+ r = r'
+ rh = add c d
+ rlh = sub d c
+ rl = case b of
+ High > rlh
+ Low > d
+ r' = case a of
+ High > rh
+ Low > rl
+ in
+ r
+\stoplambda
+
+After let bind removal:
+
+\startlambda
+ Î»x.Î»c.Î»d.
+ let s = foo x
+ a = case s of (a, _) > a
+ b = case s of (_, b) > b
+ rh = add c d
+ rlh = sub d c
+ rl = case b of
+ High > rlh
+ Low > d
+ r' = case a of
+ High > rh
+ Low > rl
+ in
+ r'
+\stoplambda
+
+Application simplification is not applicable.
\stoptext