%% \stopcombination
%}
-The first step in the core to VHDL translation process, is normalization. We
+The first step in the core to \small{VHDL} translation process, is normalization. We
aim to bring the core description into a simpler form, which we can
-subsequently translate into VHDL easily. This normal form is needed because
-the full core language is more expressive than VHDL in some areas and because
+subsequently translate into \small{VHDL} easily. This normal form is needed because
+the full core language is more expressive than \small{VHDL} in some areas and because
core can describe expressions that do not have a direct hardware
interpretation.
-TODO: Describe core properties not supported in VHDL, and describe how the
-VHDL we want to generate should look like.
+TODO: Describe core properties not supported in \small{VHDL}, and describe how the
+\small{VHDL} we want to generate should look like.
-\section{Goal}
+\section{Normal form}
The transformations described here have a well-defined goal: To bring the
program in a well-defined form that is directly translatable to hardware,
-while fully preserving the semantics of the program.
-
-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 number of nested let expressions. These let expressions binds a
-number of simple expressions in the function and produces a simple identifier.
-Every bound value in the let expression is either a simple function
-application, a case expression to extract a single element from a tuple
-returned by a function or a case expression to choose between two signals
-based on some other signal.
-
-This structure is easy to translate to VHDL, since each top level lambda will
-be an input port, every bound value will become a concurrent statement (such
-as a component instantiation or conditional signal assignment) and the result
-variable will become the output port.
+while fully preserving the semantics of the program. We refer to this form as
+the \emph{normal form} of the program. The formal definition of this normal
+form is quite simple:
+
+\placedefinition{}{A program is in \emph{normal form} if none of the
+transformations from this chapter apply.}
+
+Of course, this is an \quote{easy} definition of the normal form, since our
+program will end up in normal form automatically. The more interesting part is
+to see if this normal form actually has the properties we would like it to
+have.
+
+But, before getting into more definitions and details about this normal form,
+let's try to get a feeling for it first. The easiest way to do this is by
+describing the things we want to not have in a normal form.
+
+\startitemize
+ \item Any \emph{polymorphism} must be removed. When laying down hardware, we
+ can't generate any signals that can have multiple types. All types must be
+ completely known to generate hardware.
+
+ \item Any \emph{higher order} constructions must be removed. We can't
+ generate a hardware signal that contains a function, so all values,
+ arguments and returns values used must be first order.
+
+ \item Any complex \emph{nested scopes} must be removed. In the \small{VHDL}
+ description, every signal is in a single scope. Also, full expressions are
+ not supported everywhere (in particular port maps can only map signal names,
+ not expressions). To make the \small{VHDL} generation easy, all values must be bound
+ on the \quote{top level}.
+\stopitemize
+
+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
+will become input ports in the final hardware) are at the top. This means that
+the body of the final lambda abstraction is never a function, but always a
+plain value.
+
+After the lambda abstractions, we see a single let expression, that binds two
+variables (\lam{mul} and \lam{sum}). These variables will be signals in the
+final hardware, bound to the output port of the \lam{*} and \lam{+}
+components.
+
+The final line (the \quote{return value} of the function) selects the
+\lam{sum} signal to be the output port of the function. This \quote{return
+value} can always only be a variable reference, never a more complex
+expression.
\startbuffer[MulSum]
alu :: Bit -> Word -> Word -> Word
ncline(add)(sum);
\stopuseMPgraphic
-\placeexample[ex:MulSum]{\small{ALU} described in normal form}
+\placeexample[here][ex:MulSum]{Simple architecture consisting of an adder and a
+subtractor.}
\startcombination[2*1]
- {\typebufferlam{MulSum}}{Description in normal form}
- {\boxedgraphic{MulSum}}{Described architecture}
+ {\typebufferlam{MulSum}}{Core description in normal form.}
+ {\boxedgraphic{MulSum}}{The architecture described by the normal form.}
\stopcombination
+The previous example described composing an architecture by calling other
+functions (operators), resulting in a simple architecture with component and
+connection. There is of course also some mechanism for choice in the normal
+form. In a normal Core program, the \emph{case} expression can be used in a
+few different ways to describe choice. In normal form, this is limited to a
+very specific form.
+
+\in{Example}[ex:AddSubAlu] shows an example describing a
+simple \small{ALU}, which chooses between two operations based on an opcode
+bit. The main structure is the same as in \in{example}[ex:MulSum], but this
+time the \lam{res} variable is bound to a case expression. This case
+expression scrutinizes the variable \lam{opcode} (and scrutinizing more
+complex expressions is not supported). The case expression can select a
+different variable based on the constructor of \lam{opcode}.
+
\startbuffer[AddSubAlu]
alu :: Bit -> Word -> Word -> Word
alu = λopcode.λa.λb.
let
res1 = (+) a b
res2 = (-) a b
- res = case op of
+ res = case opcode of
Low -> res1
High -> res2
in
ncline(mux)(res) "posA(out)";
\stopuseMPgraphic
-\placeexample[ex:AddSubAlu]{\small{ALU} described in normal form}
+\placeexample[here][ex:AddSubAlu]{Simple \small{ALU} supporting two operations.}
\startcombination[2*1]
- {\typebufferlam{AddSubAlu}}{Description in normal form}
- {\boxedgraphic{AddSubAlu}}{Described architecture}
+ {\typebufferlam{AddSubAlu}}{Core description in normal form.}
+ {\boxedgraphic{AddSubAlu}}{The architecture described by the normal form.}
\stopcombination
-\startlambda
+As a more complete example, consider \in{example}[ex:NormalComplete]. This
+example contains everything that is supported in normal form, with the
+exception of builtin higher order functions. The graphical version of the
+architecture contains a slightly simplified version, since the state tuple
+packing and unpacking have been left out. Instead, two seperate registers are
+drawn. Also note that most synthesis tools will further optimize this
+architecture by removing the multiplexers at the register input and replace
+them with some logic in the clock inputs, but we want to show the architecture
+as close to the description as possible.
+
+\startbuffer[NormalComplete]
+ regbank :: Bit
+ -> Word
+ -> State (Word, Word)
+ -> (State (Word, Word), Word)
+
-- All arguments are an inital lambda
- λa.λd.λsp.
+ regbank = λa.λd.λsp.
-- There are nested let expressions at top level
let
- -- Unpack the state by coercion
+ -- Unpack the state by coercion (\eg, cast from
+ -- State (Word, Word) to (Word, Word))
s = sp :: (Word, Word)
-- Extract both registers from the state
r1 = case s of (fst, snd) -> fst
High -> r1
Low -> r2
r1' = case a of
- High -> d
+ High -> d'
Low -> r1
r2' = case a of
High -> r2
- Low -> d
+ Low -> d'
-- Packing a tuple
s' = (,) r1' r2'
- -- Packing the state by coercion
+ -- pack the state by coercion (\eg, cast from
+ -- (Word, Word) to State (Word, Word))
sp' = s' :: State (Word, Word)
-- Pack our return value
res = (,) sp' out
in
-- The actual result
res
-\stoplambda
-
-\subsection{Definitions}
-In the following sections, we will be using a number of functions and
-notations, which we will define here.
-
-\subsubsection{Transformations}
-The most important notation is the one for transformation, which looks like
-the following:
-
-\starttrans
-context conditions
-~
-from
------------------------- expression conditions
-to
-~
-context additions
-\stoptrans
-
-Here, we describe a transformation. The most import parts are \lam{from} and
-\lam{to}, which describe the Core expresssion that should be matched and the
-expression that it should be replaced with. This matching can occur anywhere
-in function that is being normalized, so it applies to any subexpression as
-well.
-
-The \lam{expression conditions} list a number of conditions on the \lam{from}
-expression that must hold for the transformation to apply.
-
-Furthermore, there is some way to look into the environment (\eg, other top
-level bindings). The \lam{context conditions} part specifies any number of
-top level bindings that must be present for the transformation to apply.
-Usually, this lists a top level binding that binds an identfier that is also
-used in the \lam{from} expression, allowing us to "access" the value of a top
-level binding in the \lam{to} expression (\eg, for inlining).
-
-Finally, there is a way to influence the environment. The \lam{context
-additions} part lists any number of new top level bindings that should be
-added.
-
-If there are no \lam{context conditions} or \lam{context additions}, they can
-be left out alltogether, along with the separator \lam{~}.
-
-TODO: Example
-
-\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 local variable is any other
-variable (\eg, variables local to a function, which can be bound by lambda
-abstractions, let expressions and case expressions).
-
-A \emph{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.
-
-A \emph{builtin function} is a function for which a builtin
-hardware translation is available, because its actual definition is not
-translatable. A user-defined function is any other function.
+\stopbuffer
-\subsubsection{Functions}
-Here, we define a number of functions that can be used below to concisely
-specify conditions.
+\startuseMPgraphic{NormalComplete}
+ save a, d, r, foo, muxr, muxout, out;
-\emph{gvar(expr)} is true when \emph{expr} is a variable that references a
-global variable. It is false when it references a local variable.
-
-\emph{lvar(expr)} is the inverse of \emph{gvar}; it is true when \emph{expr}
-references a local variable, false when it references a global variable.
+ % I/O ports
+ newCircle.a(btex \lam{a} etex) "framed(false)";
+ newCircle.d(btex \lam{d} etex) "framed(false)";
+ newCircle.out(btex \lam{out} etex) "framed(false)";
+ % Components
+ %newCircle.add(btex + etex);
+ newBox.foo(btex \lam{foo} etex);
+ newReg.r1(btex $\lam{r1}$ etex) "dx(4mm)", "dy(6mm)";
+ newReg.r2(btex $\lam{r2}$ etex) "dx(4mm)", "dy(6mm)", "reflect(true)";
+ newMux.muxr1;
+ % Reflect over the vertical axis
+ reflectObj(muxr1)((0,0), (0,1));
+ newMux.muxr2;
+ newMux.muxout;
+ rotateObj(muxout)(-90);
+
+ d.c = foo.c + (0cm, 1.5cm);
+ a.c = (xpart r2.c + 2cm, ypart d.c - 0.5cm);
+ foo.c = midpoint(muxr1.c, muxr2.c) + (0cm, 2cm);
+ muxr1.c = r1.c + (0cm, 2cm);
+ muxr2.c = r2.c + (0cm, 2cm);
+ r2.c = r1.c + (4cm, 0cm);
+ r1.c = origin;
+ muxout.c = midpoint(r1.c, r2.c) - (0cm, 2cm);
+ out.c = muxout.c - (0cm, 1.5cm);
+
+% % Draw objects and lines
+ drawObj(a, d, foo, r1, r2, muxr1, muxr2, muxout, out);
+
+ ncline(d)(foo);
+ nccurve(foo)(muxr1) "angleA(-90)", "posB(inpa)", "angleB(180)";
+ nccurve(foo)(muxr2) "angleA(-90)", "posB(inpb)", "angleB(0)";
+ nccurve(muxr1)(r1) "posA(out)", "angleA(180)", "posB(d)", "angleB(0)";
+ nccurve(r1)(muxr1) "posA(out)", "angleA(0)", "posB(inpb)", "angleB(180)";
+ nccurve(muxr2)(r2) "posA(out)", "angleA(0)", "posB(d)", "angleB(180)";
+ nccurve(r2)(muxr2) "posA(out)", "angleA(180)", "posB(inpa)", "angleB(0)";
+ nccurve(r1)(muxout) "posA(out)", "angleA(0)", "posB(inpb)", "angleB(-90)";
+ nccurve(r2)(muxout) "posA(out)", "angleA(180)", "posB(inpa)", "angleB(-90)";
+ % Connect port a
+ nccurve(a)(muxout) "angleA(-90)", "angleB(180)", "posB(sel)";
+ nccurve(a)(muxr1) "angleA(180)", "angleB(-90)", "posB(sel)";
+ nccurve(a)(muxr2) "angleA(180)", "angleB(-90)", "posB(sel)";
+ ncline(muxout)(out) "posA(out)";
+\stopuseMPgraphic
-\emph{representable(expr)} or \emph{representable(var)} is true when
-\emph{expr} or \emph{var} has a type that is representable at runtime.
+\placeexample[here][ex:NormalComplete]{Simple architecture consisting of an adder and a
+subtractor.}
+ \startcombination[2*1]
+ {\typebufferlam{NormalComplete}}{Core description in normal form.}
+ {\boxedgraphic{NormalComplete}}{The architecture described by the normal form.}
+ \stopcombination
\subsection{Normal form definition}
-We can describe this normal form in a slightly more formal manner. The
-following EBNF-like description completely captures the intended structure
-(and generates a subset of GHC's core format).
+Now we have some intuition for the normal form, we can describe how we want
+the normal form to look like in a slightly more formal manner. The following
+EBNF-like description completely captures the intended structure (and
+generates a subset of GHC's core format).
Some clauses have an expression listed in parentheses. These are conditions
that need to apply to the clause.
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
+(\eg \lam{add} or \lam{sub}). For these, a hardcoded \small{VHDL} translation is
available.
+\section{Transformation notation}
+To be able to concisely present transformations, we use a specific format to
+them. It is a simple format, similar to one used in logic reasoning.
+
+Such a transformation description looks like the following.
+
+\starttrans
+<context conditions>
+~
+<original expression>
+-------------------------- <expression conditions>
+<transformed expresssion>
+~
+<context additions>
+\stoptrans
+
+This format desribes a transformation that applies to \lam{original
+expresssion} and transforms it into \lam{transformed expression}, assuming
+that all conditions apply. In this format, there are a number of placeholders
+in pointy brackets, most of which should be rather obvious in their meaning.
+Nevertheless, we will more precisely specify their meaning below:
+
+ \startdesc{<original expression>} The expression pattern that will be matched
+ against (subexpressions of) the expression to be transformed. We call this a
+ pattern, because it can contain \emph{placeholders} (variables), which match
+ any expression or binder. Any such placeholder is said to be \emph{bound} to
+ the expression it matches. It is convention to use an uppercase latter (\eg
+ \lam{M} or \lam{E} to refer to any expression (including a simple variable
+ reference) and lowercase letters (\eg \lam{v} or \lam{b}) to refer to
+ (references to) binders.
+
+ For example, the pattern \lam{a + B} will match the expression
+ \lam{v + (2 * w)} (and bind \lam{a} to \lam{v} and \lam{B} to
+ \lam{(2 * 2)}), but not \lam{v + (2 * w)}.
+ \stopdesc
+
+ \startdesc{<expression conditions>}
+ These are extra conditions on the expression that is matched. These
+ conditions can be used to further limit the cases in which the
+ transformation applies, in particular to prevent a transformation from
+ causing a loop with itself or another transformation.
+
+ Only if these if these conditions are \emph{all} true, this transformation
+ applies.
+ \stopdesc
+
+ \startdesc{<context conditions>}
+ These are a number of extra conditions on the context of the function. In
+ particular, these conditions can require some other top level function to be
+ present, whose value matches the pattern given here. The format of each of
+ these conditions is: \lam{binder = <pattern>}.
+
+ Typically, the binder is some placeholder bound in the \lam{<original
+ expression>}, while the pattern contains some placeholders that are used in
+ the \lam{transformed expression}.
+
+ Only if a top level binder exists that matches each binder and pattern, this
+ transformation applies.
+ \stopdesc
+
+ \startdesc{<transformed expression>}
+ This is the expression template that is the result of the transformation. If, looking
+ at the above three items, the transformation applies, the \lam{original
+ expression} is completely replaced with the \lam{<transformed expression>}.
+ We call this a template, because it can contain placeholders, referring to
+ any placeholder bound by the \lam{<original expression>} or the
+ \lam{<context conditions>}. The resulting expression will have those
+ placeholders replaced by the values bound to them.
+
+ Any binder (lowercase) placeholder that has no value bound to it yet will be
+ bound to (and replaced with) a fresh binder.
+ \stopdesc
+
+ \startdesc{<context additions>}
+ These are templates for new functions to add to the context. This is a way
+ to have a transformation create new top level functiosn.
+
+ Each addition has the form \lam{binder = template}. As above, any
+ placeholder in the addition is replaced with the value bound to it, and any
+ binder placeholder that has no value bound to it yet will be bound to (and
+ replaced with) a fresh binder.
+ \stopdesc
+
+ As an example, we'll look at η-abstraction:
+
+\starttrans
+E \lam{E :: a -> b}
+-------------- \lam{E} does not occur on a function position in an application
+λx.E x \lam{E} is not a lambda abstraction.
+\stoptrans
+
+ Consider the following function, which is a fairly obvious way to specify a
+ simple ALU (Note \at{example}[ex:AddSubAlu] is the normal form of this
+ function):
+
+\startlambda
+alu :: Bit -> Word -> Word -> Word
+alu = λopcode. case opcode of
+ Low -> (+)
+ High -> (-)
+\stoplambda
+
+ There are a few subexpressions in this function to which we could possibly
+ apply the transformation. Since the pattern of the transformation is only
+ the placeholder \lam{E}, any expression will match that. Whether the
+ transformation applies to an expression is thus solely decided by the
+ conditions to the right of the transformation.
+
+ We will look at each expression in the function in a top down manner. The
+ first expression is the entire expression the function is bound to.
+
+\startlambda
+λopcode. case opcode of
+ Low -> (+)
+ High -> (-)
+\stoplambda
+
+ As said, the expression pattern matches this. The type of this expression is
+ \lam{Bit -> Word -> Word -> Word}, which matches \lam{a -> b} (Note that in
+ this case \lam{a = Bit} and \lam{b = Word -> Word -> Word}).
+
+ Since this expression is at top level, it does not occur at a function
+ position of an application. However, The expression is a lambda abstraction,
+ so this transformation does not apply.
+
+ The next expression we could apply this transformation to, is the body of
+ the lambda abstraction:
+
+\startlambda
+case opcode of
+ Low -> (+)
+ High -> (-)
+\stoplambda
+
+ The type of this expression is \lam{Word -> Word -> Word}, which again
+ matches \lam{a -> b}. The expression is the body of a lambda expression, so
+ it does not occur at a function position of an application. Finally, the
+ expression is not a lambda abstraction but a case expression, so all the
+ conditions match. There are no context conditions to match, so the
+ transformation applies.
+
+ By now, the placeholder \lam{E} is bound to the entire expression. The
+ placeholder \lam{x}, which occurs in the replacement template, is not bound
+ yet, so we need to generate a fresh binder for that. Let's use the binder
+ \lam{a}. This results in the following replacement expression:
+
+\startlambda
+λa.(case opcode of
+ Low -> (+)
+ High -> (-)) a
+\stoplambda
+
+ Continuing with this expression, we see that the transformation does not
+ apply again (it is a lambda expression). Next we look at the body of this
+ labmda abstraction:
+
+\startlambda
+(case opcode of
+ Low -> (+)
+ High -> (-)) a
+\stoplambda
+
+ Here, the transformation does apply, binding \lam{E} to the entire
+ expression and \lam{x} to the fresh binder \lam{b}, resulting in the
+ replacement:
+
+\startlambda
+λb.(case opcode of
+ Low -> (+)
+ High -> (-)) a b
+\stoplambda
+
+ Again, the transformation does not apply to this lambda abstraction, so we
+ look at its body. For brevity, we'll put the case statement on one line from
+ now on.
+
+\startlambda
+(case opcode of Low -> (+); High -> (-)) a b
+\stoplambda
+
+ The type of this expression is \lam{Word}, so it does not match \lam{a -> b}
+ and the transformation does not apply. Next, we have two options for the
+ next expression to look at: The function position and argument position of
+ the application. The expression in the argument position is \lam{b}, which
+ has type \lam{Word}, so the transformation does not apply. The expression in
+ the function position is:
+
+\startlambda
+(case opcode of Low -> (+); High -> (-)) a
+\stoplambda
+
+ Obviously, the transformation does not apply here, since it occurs in
+ function position. In the same way the transformation does not apply to both
+ components of this expression (\lam{case opcode of Low -> (+); High -> (-)}
+ and \lam{a}), so we'll skip to the components of the case expression: The
+ scrutinee and both alternatives. Since the opcode is not a function, it does
+ not apply here, and we'll leave both alternatives as an exercise to the
+ reader. The final function, after all these transformations becomes:
+
+\startlambda
+alu :: Bit -> Word -> Word -> Word
+alu = λopcode.λa.b. (case opcode of
+ Low -> λa1.λb1 (+) a1 b1
+ High -> λa2.λb2 (-) a2 b2) a b
+\stoplambda
+
+ In this case, the transformation does not apply anymore, though this might
+ not always be the case (e.g., the application of a transformation on a
+ subexpression might open up possibilities to apply the transformation
+ further up in the expression).
+
+\subsection{Transformation application}
+In this chapter we define a number of transformations, but how will we apply
+these? As stated before, our normal form is reached as soon as no
+transformation applies anymore. This means our application strategy is to
+simply apply any transformation that applies, and continuing to do that with
+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.
+
+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
+transformation descriptions concise and powerful.
+
+\subsection{Definitions}
+In the following sections, we will be using a number of functions and
+notations, which we will define here.
+
+\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
+other variable (\eg, variables local to a function, which can be bound by
+lambda abstractions, let expressions and pattern matches of case
+alternatives). Note that this is a slightly different notion of global versus
+local than what \small{GHC} uses internally.
+\defref{global variable} \defref{local variable}
+
+A \emph{hardware representable} (or just \emph{representable}) type or value
+is (a value of) 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.
+\defref{representable}
+
+A \emph{builtin function} is a function supplied by the Cλash framework, whose
+implementation is not valid Cλash. The implementation is of course valid
+Haskell, for simulation, but it is not expressable in Cλash.
+\defref{builtin function} \defref{user-defined function}
+
+For these functions, Cλash has a \emph{builtin hardware translation}, so calls
+to these functions can still be translated. These are functions like
+\lam{map}, \lam{hwor} and \lam{length}.
+
+A \emph{user-defined} function is a function for which we do have a Cλash
+implementation available.
+
+\subsubsection{Functions}
+Here, we define a number of functions that can be used below to concisely
+specify conditions.
+
+\refdef{global variable}\emph{gvar(expr)} is true when \emph{expr} is a variable that references a
+global variable. It is false when it references a local variable.
+
+\refdef{local variable}\emph{lvar(expr)} is the complement of \emph{gvar}; it is true when \emph{expr}
+references a local variable, false when it references a global variable.
+
+\refdef{representable}\emph{representable(expr)} or \emph{representable(var)} is true when
+\emph{expr} or \emph{var} is \emph{representable}.
+
+\subsection{Binder uniqueness}
+A common problem in transformation systems, is binder uniqueness. When not
+considering this problem, it is easy to create transformations that mix up
+bindings and cause name collisions. Take for example, the following core
+expression:
+
+\startlambda
+(λa.λb.λc. a * b * c) x c
+\stoplambda
+
+By applying β-reduction (see below) once, we can simplify this expression to:
+
+\startlambda
+(λb.λc. x * b * c) c
+\stoplambda
+
+Now, we have replaced the \lam{a} binder with a reference to the \lam{x}
+binder. No harm done here. But note that we see multiple occurences of the
+\lam{c} binder. The first is a binding occurence, to which the second refers.
+The last, however refers to \emph{another} instance of \lam{c}, which is
+bound somewhere outside of this expression. Now, if we would apply beta
+reduction without taking heed of binder uniqueness, we would get:
+
+\startlambda
+λc. x * c * c
+\stoplambda
+
+This is obviously not what was supposed to happen! The root of this problem is
+the reuse of binders: Identical binders can be bound in different scopes, such
+that only the inner one is \quote{visible} in the inner expression. In the example
+above, the \lam{c} binder was bound outside of the expression and in the inner
+lambda expression. Inside that lambda expression, only the inner \lam{c} is
+visible.
+
+There are a number of ways to solve this. \small{GHC} has isolated this
+problem to their binder substitution code, which performs \emph{deshadowing}
+during its expression traversal. This means that any binding that shadows
+another binding on a higher level is replaced by a new binder that does not
+shadow any other binding. This non-shadowing invariant is enough to prevent
+binder uniqueness problems in \small{GHC}.
+
+In our transformation system, maintaining this non-shadowing invariant is
+a bit harder to do (mostly due to implementation issues, the prototype doesn't
+use \small{GHC}'s subsitution code). Also, we can observe the following
+points.
+
+\startitemize
+\item Deshadowing does not guarantee overall uniqueness. For example, the
+following (slightly contrived) expression shows the identifier \lam{x} bound in
+two seperate places (and to different values), even though no shadowing
+occurs.
+
+\startlambda
+(let x = 1 in x) + (let x = 2 in x)
+\stoplambda
+
+\item In our normal form (and the resulting \small{VHDL}), all binders
+(signals) will end up in the same scope. To allow this, all binders within the
+same function should be unique.
+
+\item When we know that all binders in an expression are unique, moving around
+or removing a subexpression will never cause any binder conflicts. If we have
+some way to generate fresh binders, introducing new subexpressions will not
+cause any problems either. The only way to cause conflicts is thus to
+duplicate an existing subexpression.
+\stopitemize
+
+Given the above, our prototype maintains a unique binder invariant. This
+meanst that in any given moment during normalization, all binders \emph{within
+a single function} must be unique. To achieve this, we apply the following
+technique.
+
+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).
+\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.
+\item Whenever (part of) an expression is duplicated (for example when
+inlining), all binders in the expression are replaced with fresh binders
+(using the same method as at the start of normalization). These fresh binders
+can never introduce duplication, so this will maintain the invariant.
+\item Whenever we move part of an expression around within the function, there
+is no need to do anything special. There is obviously no way to introduce
+duplication by moving expressions around. Since we know that each of the
+binders is already unique, there is no way to introduce (incorrect) shadowing
+either.
+\stopitemize
+
\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.
number of conclusions (below the horizontal line). The details of using
this notation are still a bit fuzzy, so comments are welcom.
-TODO: Formally describe the "apply to every (sub)expression" in terms of
-rules with full transformations in the conditions.
-
\subsection{η-abstraction}
This transformation makes sure that all arguments of a function-typed
expression are named, by introducing lambda expressions. When combined with
be lambda abstractions or global identifiers.
\starttrans
-E \lam{E :: * -> *}
+E \lam{E :: a -> b}
-------------- \lam{E} is not the first argument of an application.
λx.E x \lam{E} is not a lambda abstraction.
\lam{x} is a variable that does not occur free in \lam{E}.
\transexample{η-abstraction}{from}{to}
-\subsection{Extended β-reduction}
+\subsection{β-reduction}
+β-reduction is a well known transformation from lambda calculus, where it is
+the main reduction step. It reduces applications of labmda abstractions,
+removing both the lambda abstraction and the application.
+
+In our transformation system, this step helps to remove unwanted lambda
+abstractions (basically all but the ones at the top level). Other
+transformations (application propagation, non-representable inlining) make
+sure that most lambda abstractions will eventually be reducable by
+β-reduction.
+
+TODO: Define substitution syntax
+
+\starttrans
+(λx.E) M
+-----------------
+E[M/x]
+\stoptrans
+
+% And an example
+\startbuffer[from]
+(λa. 2 * a) (2 * b)
+\stopbuffer
+
+\startbuffer[to]
+2 * (2 * b)
+\stopbuffer
+
+\transexample{β-reduction}{from}{to}
+
+\subsection{Application propagation}
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).
+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).
-For let expressions:
\starttrans
let binds in E) M
-----------------
let binds in E M
\stoptrans
-For case statements:
+% 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
pn -> En M
\stoptrans
-For lambda expressions:
-\starttrans
-(λx.E) M
------------------
-E[M/x]
-\stoptrans
-
% And an example
\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
+( case x of
+ True -> id
+ False -> neg
+) 1
\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
+case x of
+ True -> id 1
+ False -> neg 1
\stopbuffer
-\transexample{Extended β-reduction}{from}{to}
+\transexample{Application propagation for a case expression}{from}{to}
\subsection{Let derecursification}
This transformation is meant to make lets non-recursive whenever possible.
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
-rederursification transformation will do this instead.
+rederecursification transformation will do this instead.
\starttrans
letnonrec x = (let bindings in M) in N
This transformation inlines simple let bindings (\eg a = b).
This transformation is not needed to get into normal form, but makes the
-resulting VHDL a lot shorter.
+resulting \small{VHDL} a lot shorter.
\starttrans
letnonrec
(since ununsed 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 VHDL a lot shorter.
+this transformation makes the resulting \small{VHDL} a lot shorter.
\starttrans
let a = E in M
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
+ \small{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.
\subsubsection{Argument simplification}
This transform deals with arguments to functions that
are of a runtime representable type. It ensures that they will all become
-references to global variables, or local signals in the resulting VHDL.
+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.
Perhaps this makes this transformation not needed?
This transformation is useful when applying higher order builtin functions
like \hs{map} to a lambda abstraction, for example. In this case, the code
-that generates VHDL for \hs{map} only needs to handle top level functions and
+that generates \small{VHDL} for \hs{map} only needs to handle top level functions and
partial applications, not any other expression (such as lambda abstractions or
even more complicated expressions).
projects / matthijs / master-project / report.git / blobdiff