\chapter[chap:normalization]{Normalization}
+ % 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 left-alignment, 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[offset=1mm,align=right,strut=no,background=box,frame=off]{
+ \setuptyping[option=LAM,style=sans,before=,after=,strip=auto]
+ \typebuffer[#1]
+ \setuptyping[option=none,style=\tttf,strip=auto]
+ }
+ }
-% 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 left-alignment, 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[offset=1mm,align=right,strut=no,background=box,frame=off]{
- \setuptyping[option=LAM,style=sans,before=,after=]
- \typebuffer[#1]
- \setuptyping[option=none,style=\tttf]
+ \define[4]\transexample{
+ \placeexample[here][ex:trans:#1]{#2}
+ \startcombination[2*1]
+ {\example{#3}}{Original program}
+ {\example{#4}}{Transformed program}
+ \stopcombination
}
-}
-
-
-\define[3]\transexample{
- \placeexample[here]{#1}
- \startcombination[2*1]
- {\example{#2}}{Original program}
- {\example{#3}}{Transformed program}
- \stopcombination
-}
-%
-%\define[3]\transexampleh{
-%% \placeexample[here]{#1}
-%% \startcombination[1*2]
-%% {\example{#2}}{Original program}
-%% {\example{#3}}{Transformed program}
-%% \stopcombination
-%}
-
-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 \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 \small{VHDL}, and describe how the
-\small{VHDL} we want to generate should look like.
-
-\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. 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
-alu = λa.λb.λc.
- let
- mul = (*) a b
- sum = (+) mul c
- in
- sum
-\stopbuffer
-
-\startuseMPgraphic{MulSum}
- save a, b, c, mul, add, sum;
-
- % I/O ports
- newCircle.a(btex $a$ etex) "framed(false)";
- newCircle.b(btex $b$ etex) "framed(false)";
- newCircle.c(btex $c$ etex) "framed(false)";
- newCircle.sum(btex $res$ etex) "framed(false)";
-
- % Components
- newCircle.mul(btex - etex);
- newCircle.add(btex + etex);
-
- a.c - b.c = (0cm, 2cm);
- b.c - c.c = (0cm, 2cm);
- add.c = c.c + (2cm, 0cm);
- mul.c = midpoint(a.c, b.c) + (2cm, 0cm);
- sum.c = add.c + (2cm, 0cm);
- c.c = origin;
-
- % Draw objects and lines
- drawObj(a, b, c, mul, add, sum);
-
- ncarc(a)(mul) "arcangle(15)";
- ncarc(b)(mul) "arcangle(-15)";
- ncline(c)(add);
- ncline(mul)(add);
- ncline(add)(sum);
-\stopuseMPgraphic
-
-\placeexample[here][ex:MulSum]{Simple architecture consisting of an adder and a
-subtractor.}
- \startcombination[2*1]
- {\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 opcode of
- Low -> res1
- High -> res2
- in
- res
-\stopbuffer
-
-\startuseMPgraphic{AddSubAlu}
- save opcode, a, b, add, sub, mux, res;
-
- % I/O ports
- newCircle.opcode(btex $opcode$ etex) "framed(false)";
- newCircle.a(btex $a$ etex) "framed(false)";
- newCircle.b(btex $b$ etex) "framed(false)";
- newCircle.res(btex $res$ etex) "framed(false)";
- % Components
- newCircle.add(btex + etex);
- newCircle.sub(btex - etex);
- newMux.mux;
-
- opcode.c - a.c = (0cm, 2cm);
- add.c - a.c = (4cm, 0cm);
- sub.c - b.c = (4cm, 0cm);
- a.c - b.c = (0cm, 3cm);
- mux.c = midpoint(add.c, sub.c) + (1.5cm, 0cm);
- res.c - mux.c = (1.5cm, 0cm);
- b.c = origin;
-
- % Draw objects and lines
- drawObj(opcode, a, b, res, add, sub, mux);
-
- ncline(a)(add) "posA(e)";
- ncline(b)(sub) "posA(e)";
- nccurve(a)(sub) "posA(e)", "angleA(0)";
- nccurve(b)(add) "posA(e)", "angleA(0)";
- nccurve(add)(mux) "posB(inpa)", "angleB(0)";
- nccurve(sub)(mux) "posB(inpb)", "angleB(0)";
- nccurve(opcode)(mux) "posB(n)", "angleA(0)", "angleB(-90)";
- ncline(mux)(res) "posA(out)";
-\stopuseMPgraphic
-
-\placeexample[here][ex:AddSubAlu]{Simple \small{ALU} supporting two operations.}
- \startcombination[2*1]
- {\typebufferlam{AddSubAlu}}{Core description in normal form.}
- {\boxedgraphic{AddSubAlu}}{The architecture described by the normal form.}
- \stopcombination
-
-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
- regbank = λa.λd.λsp.
- -- There are nested let expressions at top level
- let
- -- 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
- r2 = case s of (fst, snd) -> snd
- -- Calling some other user-defined function.
- d' = foo d
- -- Conditional connections
- out = case a of
- High -> r1
- Low -> r2
- r1' = case a of
- High -> d'
- Low -> r1
- r2' = case a of
- High -> r2
- Low -> d'
- -- Packing a tuple
- s' = (,) r1' r2'
- -- 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
-\stopbuffer
-
-\startuseMPgraphic{NormalComplete}
- save a, d, r, foo, muxr, muxout, out;
-
- % 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
-
-\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{Intended normal form definition}
-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.
-
-\startlambda
-\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{binding} = var = \italic{rhs} (representable(rhs))
- -- State packing and unpacking by coercion
- | var0 = var1 :: State ty (lvar(var1))
- | var0 = var1 :: ty (var0 :: State ty) (lvar(var1))
-\italic{rhs} = userapp
- | builtinapp
- -- Extractor case
- | case var of C a0 ... an -> ai (lvar(var))
- -- Selector case
- | case var of (lvar(var))
- DEFAULT -> var0 (lvar(var0))
- C w0 ... wn -> resvar (\forall{}i, wi \neq resvar, lvar(resvar))
-\italic{userapp} = \italic{userfunc}
- | \italic{userapp} {userarg}
-\italic{userfunc} = var (gvar(var))
-\italic{userarg} = var (lvar(var))
-\italic{builtinapp} = \italic{builtinfunc}
- | \italic{builtinapp} \italic{builtinarg}
-\italic{builtinfunc} = var (bvar(var))
-\italic{builtinarg} = \italic{coreexpr}
-\stoplambda
-
--- 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: Note about the selector case. It just supports Bit and Bool
-currently, perhaps it should be generalized in the normal form?
-
-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 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 \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.
-
-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
-transformations can be applied anymore, the program is in normal form (by
-definition). 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 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.
-
-\starttrans
-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}.
-\stoptrans
-
-\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{β-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. 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}
-
-\subsection{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?
-
-\subsection{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).
-
-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.
-
-\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)
- \vdots
-in
- N
-------------------------------------------
-letrec
- \vdots
- bindings
- x = M
- \vdots
-in
- N
-\stoptrans
-
-\startbuffer[from]
-let
- a = letrec
- x = 1
- y = 2
- in
- x + y
-in
- letrec
- b = let c = 3 in a + c
- d = 4
- in
- d + b
-\stopbuffer
-\startbuffer[to]
-letrec
- x = 1
- y = 2
-in
- let
- a = x + y
- in
- letrec
- c = 3
- b = a + c
- d = 4
- in
- d + b
-\stopbuffer
-
-\transexample{Let flattening}{from}{to}
-
-\subsection{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).
-
-\starttrans
-letrec in M
---------------
-M
-\stoptrans
-
-\subsection{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
- \vdots
- a = b
- \vdots
-in
- M
------------------
-let
- \vdots [b/a]
- \vdots [b/a]
-in
- M[b/a]
-\stoptrans
-
-\subsection{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
-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
- \vdots
- a = E
- \vdots
-in
- M
----------------------------- \lam{a} does not occur free in \lam{M}
-letrec
- \vdots
- \vdots
-in
- M
-\stoptrans
-
-\subsection{Non-representable binding inlining}
-This transform inlines let bindings that have a non-representable type. Since
-we can never generate a signal assignment for these bindings (we cannot
-declare a signal assignment with a non-representable type, for obvious
-reasons), we have no choice but to inline the binding to remove it.
-
-If the binding is non-representable because it is a lambda abstraction, it is
-likely that it will inlined into an application and β-reduction will remove
-the lambda abstraction and turn it into a representable expression at the
-inline site. The same holds for partial applications, which can be turned into
-full applications by inlining.
-
-Other cases of non-representable bindings we see in practice are primitive
-Haskell types. In most cases, these will not result in a valid normalized
-output, but then the input would have been invalid to start with. There is one
-exception to this: When a builtin function is applied to a non-representable
-expression, things might work out in some cases. For example, when you write a
-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.
-
-\starttrans
-letnonrec a = E in M
--------------------------- \lam{E} has a non-representable type.
-M[E/a]
-\stoptrans
-
-\starttrans
-letrec
- \vdots
- a = E
- \vdots
-in
- M
--------------------------- \lam{E} has a non-representable type.
-letrec
- \vdots [E/a]
- \vdots [E/a]
-in
- M[E/a]
-\stoptrans
-
-\startbuffer[from]
-letrec
- a = smallInteger 10
- inc = λa -> add a 1
- inc' = add 1
- x = fromInteger a
-in
- inc (inc' x)
-\stopbuffer
-
-\startbuffer[to]
-letrec
- x = fromInteger (smallInteger 10)
-in
- (λa -> add a 1) (add 1 x)
-\stopbuffer
-
-\transexample{Let flattening}{from}{to}
-
-\subsection{Compiler generated top level binding inlining}
-TODO
-
-\subsection{Scrutinee simplification}
-This transform ensures that the scrutinee of a case expression is always
-a simple variable reference.
-
-\starttrans
-case E of
- alts
------------------ \lam{E} is not a local variable reference
-let x = E in
- case E of
- alts
-\stoptrans
-
-\startbuffer[from]
-case (foo a) of
- True -> a
- False -> b
-\stopbuffer
-
-\startbuffer[to]
-let x = foo a in
- case x of
- True -> a
- False -> b
-\stopbuffer
-
-\transexample{Let flattening}{from}{to}
-
-
-\subsection{Case simplification}
-This transformation ensures that all case expressions become normal form. This
-means they will become one of:
-\startitemize
-\item An extractor case with a single alternative that picks a single field
-from a datatype, \eg \lam{case x of (a, b) -> a}.
-\item A selector case with multiple alternatives and only wild binders, that
-makes a choice between expressions based on the constructor of another
-expression, \eg \lam{case x of Low -> a; High -> b}.
-\stopitemize
-
-\starttrans
-case E of
- C0 v0,0 ... v0,m -> E0
- \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
- 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
- x0 = E0
- \dots
- vn,m = case x of Cn vn,0 .. vn,m -> vn,m
- xn = En
-in
- case E of
- C0 w0,0 ... w0,m -> x0
- \vdots
- 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?
-
-\startbuffer[from]
-case a of
- True -> add b 1
- False -> add b 2
-\stopbuffer
-
-\startbuffer[to]
-letnonrec
- x0 = add b 1
- x1 = add b 2
-in
- case a of
- True -> x0
- False -> x1
-\stopbuffer
-
-\transexample{Selector case simplification}{from}{to}
-
-\startbuffer[from]
-case a of
- (,) b c -> add b c
-\stopbuffer
-\startbuffer[to]
-letnonrec
- b = case a of (,) b c -> b
- c = case a of (,) b c -> c
- x0 = add b c
-in
- case a of
- (,) w0 w1 -> x0
-\stopbuffer
-
-\transexample{Extractor case simplification}{from}{to}
-
-\subsection{Case removal}
-This transform removes any case statements with a single alternative and
-only wild binders.
-
-These "useless" case statements are usually leftovers from case simplification
-on extractor case (see the previous example).
-
-\starttrans
-case x of
- C v0 ... vm -> E
----------------------- \lam{\forall i, 0 <= i <= m} (\lam{vi} does not occur free in E)
-E
-\stoptrans
-
-\startbuffer[from]
-case a of
- (,) w0 w1 -> x0
-\stopbuffer
-
-\startbuffer[to]
-x0
-\stopbuffer
-
-\transexample{Case removal}{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 Make all arguments of user-defined functions (\eg, of which
- we have a function body) simple variable references of a runtime
- representable type. This is needed, since these applications will be turned
- into component instantiations.
- \item Make all arguments of builtin functions one of:
- \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
-
-When looking at the arguments of a user-defined function, we can
-divide them into two categories:
-\startitemize
- \item Arguments of 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 Non-runtime representable typed arguments.
-
- These arguments cannot be preserved in the program, since we
- cannot represent them as input or output ports in the resulting
- \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.
-
- Typically, these arguments are type and dictionary arguments that are
- used to make functions polymorphic. By propagating these arguments, we
- are essentially doing the same which GHC does when it specializes
- functions: Creating multiple variants of the same function, one for
- each type for which it is used. Other common non-representable
- arguments are functions, e.g. when calling a higher order function
- with another function or a lambda abstraction as an argument.
-
- The reason for doing this is similar to the reasoning provided for
- the inlining of non-representable let bindings above. In fact, this
- argument propagation could be viewed as a form of cross-function
- inlining.
-\stopitemize
-
-TODO: Check the following itemization.
-
-When looking at the arguments of a builtin function, we can divide them
-into categories:
-
-\startitemize
- \item Arguments of a runtime representable type.
-
- As we have seen with user-defined 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 of a function type.
-
- These arguments are functions passed to higher order builtins,
- like \lam{map} and \lam{foldl}. Since implementing these
- functions for arbitrary function-typed 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 type-level 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 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 \small{VHDL}.
-
-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.
-
-\starttrans
-M N
--------------------- \lam{N} is of a representable type
-let x = N in M x \lam{N} is not a local variable reference
-\stoptrans
-
-\startbuffer[from]
-add (add a 1) 1
-\stopbuffer
-
-\startbuffer[to]
-let x = add a 1 in add x 1
-\stopbuffer
-
-\transexample{Argument extraction}{from}{to}
-
-\subsubsection{Function extraction}
-This transform deals with function-typed 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.
-
-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 \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).
-
-\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}
-~ \lam{N} is not a (partial application of) a top level function
-x = λf0 ... λfn.N
-\stoptrans
-
-\startbuffer[from]
-map (λa . add a b) xs
-
-map (add b) ys
-\stopbuffer
-
-\startbuffer[to]
-x0 = λb.λa.add a b
-~
-map x0 xs
-
-x1 = λb.add b
-map x1 ys
-\stopbuffer
-
-\transexample{Function extraction}{from}{to}
-
-\subsubsection{Argument propagation}
-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}.
-
-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 to-be-propagated 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.
-
-\starttrans
-x = E
-~
-x Y0 ... Yi ... Yn \lam{Yi} is not of a runtime representable type
---------------------------------------------- \lam{Yi} is not a local variable reference
-x' y0 ... yi-1 f0 ... fm Yi+1 ... Yn \lam{f0 ... fm} = free local vars of \lam{Yi}
-~
-x' = λy0 ... yi-1 f0 ... fm yi+1 ... yn .
- E y0 ... yi-1 Yi yi+1 ... yn
-
-\stoptrans
-
-TODO: Example
-
-\subsection{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.
-
-\subsection{Return value simplification}
-This transformation ensures that the return value of a function is always a
-simple local variable reference.
-
-Currently implemented using lambda simplification, let simplification, and
-top simplification. Should change into something like the following, which
-works only on the result of a function instead of any subexpression. This is
-achieved by the contexts, like \lam{x = E}, though this is strictly not
-correct (you could read this as "if there is any function \lam{x} that binds
-\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).
-
-\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
-\stoptrans
-
-\starttrans
-x = λv0 ... λvn.E
-~ \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
-\stoptrans
-
-\starttrans
-x = λv0 ... λvn.let ... in E
-~ \lam{E} is representable
-E \lam{E} is not a local variable reference
----------------------------
-let x = E in x
-\stoptrans
-
-\startbuffer[from]
-x = add 1 2
-\stopbuffer
-
-\startbuffer[to]
-x = let x = add 1 2 in x
-\stopbuffer
-
-\transexample{Return value simplification}{from}{to}
-
-\section{Provable properties}
- When looking at the system of transformations outlined above, there are a
- number of questions that we can ask ourselves. The main question is of course:
- \quote{Does our system work as intended?}. We can split this question into a
- number of subquestions:
-
- \startitemize[KR]
- \item[q:termination] Does our system \emph{terminate}? Since our system will
- keep running as long as transformations apply, there is an obvious risk that
- it will keep running indefinitely. One transformation produces a result that
- is transformed back to the original by another transformation, for example.
- \item[q:soundness] Is our system \emph{sound}? Since our transformations
- continuously modify the expression, there is an obvious risk that the final
- normal form will not be equivalent to the original program: Its meaning could
- have changed.
- \item[q:completeness] Is our system \emph{complete}? Since we have a complex
- system of transformations, there is an obvious risk that some expressions will
- not end up in our intended normal form, because we forgot some transformation.
- In other words: Does our transformation system result in our intended normal
- form for all possible inputs?
- \item[q:determinism] Is our system \emph{deterministic}? Since we have defined
- no particular order in which the transformation should be applied, there is an
- obvious risk that different transformation orderings will result in
- \emph{different} normal forms. They might still both be intended normal forms
- (if our system is \emph{complete}) and describe correct hardware (if our
- system is \emph{sound}), so this property is less important than the previous
- three: The translator would still function properly without it.
- \stopitemize
-
- \subsection{Graph representation}
- Before looking into how to prove these properties, we'll look at our
- transformation system from a graph perspective. The nodes of the graph are
- all possible Core expressions. The (directed) edges of the graph are
- transformations. When a transformation α applies to an expression \lam{A} to
- produce an expression \lam{B}, we add an edge from the node for \lam{A} to the
- node for \lam{B}, labeled α.
-
- \startuseMPgraphic{TransformGraph}
- save a, b, c, d;
-
- % Nodes
- newCircle.a(btex \lam{(λx.λy. (+) x y) 1} etex);
- newCircle.b(btex \lam{λy. (+) 1 y} etex);
- newCircle.c(btex \lam{(λx.(+) x) 1} etex);
- newCircle.d(btex \lam{(+) 1} etex);
-
- b.c = origin;
- c.c = b.c + (4cm, 0cm);
- a.c = midpoint(b.c, c.c) + (0cm, 4cm);
- d.c = midpoint(b.c, c.c) - (0cm, 3cm);
-
- % β-conversion between a and b
- ncarc.a(a)(b) "name(bred)";
- ObjLabel.a(btex $\xrightarrow[normal]{}{β}$ etex) "labpathname(bred)", "labdir(rt)";
- ncarc.b(b)(a) "name(bexp)", "linestyle(dashed withdots)";
- ObjLabel.b(btex $\xleftarrow[normal]{}{β}$ etex) "labpathname(bexp)", "labdir(lft)";
-
- % η-conversion between a and c
- ncarc.a(a)(c) "name(ered)";
- ObjLabel.a(btex $\xrightarrow[normal]{}{η}$ etex) "labpathname(ered)", "labdir(rt)";
- ncarc.c(c)(a) "name(eexp)", "linestyle(dashed withdots)";
- ObjLabel.c(btex $\xleftarrow[normal]{}{η}$ etex) "labpathname(eexp)", "labdir(lft)";
-
- % η-conversion between b and d
- ncarc.b(b)(d) "name(ered)";
- ObjLabel.b(btex $\xrightarrow[normal]{}{η}$ etex) "labpathname(ered)", "labdir(rt)";
- ncarc.d(d)(b) "name(eexp)", "linestyle(dashed withdots)";
- ObjLabel.d(btex $\xleftarrow[normal]{}{η}$ etex) "labpathname(eexp)", "labdir(lft)";
-
- % β-conversion between c and d
- ncarc.c(c)(d) "name(bred)";
- ObjLabel.c(btex $\xrightarrow[normal]{}{β}$ etex) "labpathname(bred)", "labdir(rt)";
- ncarc.d(d)(c) "name(bexp)", "linestyle(dashed withdots)";
- ObjLabel.d(btex $\xleftarrow[normal]{}{β}$ etex) "labpathname(bexp)", "labdir(lft)";
+
+ 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 \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.
+
+ \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. 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 and constants, not complete expressions). To make the \small{VHDL}
+ generation easy, a separate binder must be bound to ever application or
+ other expression.
+ \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 outer level.
+ This means that the body of the inner lambda abstraction is never a
+ function, but always a plain value.
+
+ As the body of the inner lambda abstraction, we see a single (recursive)
+ 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.
+
+ \todo{Add generated VHDL}
+
+ \startbuffer[MulSum]
+ alu :: Bit -> Word -> Word -> Word
+ alu = λa.λb.λc.
+ let
+ mul = (*) a b
+ sum = (+) mul c
+ in
+ sum
+ \stopbuffer
+
+ \startuseMPgraphic{MulSum}
+ save a, b, c, mul, add, sum;
+
+ % I/O ports
+ newCircle.a(btex $a$ etex) "framed(false)";
+ newCircle.b(btex $b$ etex) "framed(false)";
+ newCircle.c(btex $c$ etex) "framed(false)";
+ newCircle.sum(btex $res$ etex) "framed(false)";
+
+ % Components
+ newCircle.mul(btex * etex);
+ newCircle.add(btex + etex);
+
+ a.c - b.c = (0cm, 2cm);
+ b.c - c.c = (0cm, 2cm);
+ add.c = c.c + (2cm, 0cm);
+ mul.c = midpoint(a.c, b.c) + (2cm, 0cm);
+ sum.c = add.c + (2cm, 0cm);
+ c.c = origin;
% Draw objects and lines
- drawObj(a, b, c, d);
- \stopuseMPgraphic
+ drawObj(a, b, c, mul, add, sum);
- \placeexample[right][ex:TransformGraph]{Partial graph of a labmda calculus
- system with β and η reduction (solid lines) and expansion (dotted lines).}
- \boxedgraphic{TransformGraph}
+ ncarc(a)(mul) "arcangle(15)";
+ ncarc(b)(mul) "arcangle(-15)";
+ ncline(c)(add);
+ ncline(mul)(add);
+ ncline(add)(sum);
+ \stopuseMPgraphic
- Of course our graph is unbounded, since we can construct an infinite amount of
- Core expressions. Also, there might potentially be multiple edges between two
- given nodes (with different labels), though seems unlikely to actually happen
- in our system.
+ \placeexample[here][ex:MulSum]{Simple architecture consisting of a
+ multiplier and a subtractor.}
+ \startcombination[2*1]
+ {\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 components and
+ connections. 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 similar to \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 opcode of
+ Low -> res1
+ High -> res2
+ in
+ res
+ \stopbuffer
+
+ \startuseMPgraphic{AddSubAlu}
+ save opcode, a, b, add, sub, mux, res;
+
+ % I/O ports
+ newCircle.opcode(btex $opcode$ etex) "framed(false)";
+ newCircle.a(btex $a$ etex) "framed(false)";
+ newCircle.b(btex $b$ etex) "framed(false)";
+ newCircle.res(btex $res$ etex) "framed(false)";
+ % Components
+ newCircle.add(btex + etex);
+ newCircle.sub(btex - etex);
+ newMux.mux;
+
+ opcode.c - a.c = (0cm, 2cm);
+ add.c - a.c = (4cm, 0cm);
+ sub.c - b.c = (4cm, 0cm);
+ a.c - b.c = (0cm, 3cm);
+ mux.c = midpoint(add.c, sub.c) + (1.5cm, 0cm);
+ res.c - mux.c = (1.5cm, 0cm);
+ b.c = origin;
- See \in{example}[ex:TransformGraph] for the graph representation of a very
- simple lambda calculus that contains just the expressions \lam{(λx.λy. (+) x
- y) 1}, \lam{λy. (+) 1 y}, \lam{(λx.(+) x) 1} and \lam{(+) 1}. The
- transformation system consists of β-reduction and η-reduction (solid edges) or
- β-reduction and η-reduction (dotted edges).
+ % Draw objects and lines
+ drawObj(opcode, a, b, res, add, sub, mux);
+
+ ncline(a)(add) "posA(e)";
+ ncline(b)(sub) "posA(e)";
+ nccurve(a)(sub) "posA(e)", "angleA(0)";
+ nccurve(b)(add) "posA(e)", "angleA(0)";
+ nccurve(add)(mux) "posB(inpa)", "angleB(0)";
+ nccurve(sub)(mux) "posB(inpb)", "angleB(0)";
+ nccurve(opcode)(mux) "posB(n)", "angleA(0)", "angleB(-90)";
+ ncline(mux)(res) "posA(out)";
+ \stopuseMPgraphic
- TODO: Define β-reduction and η-reduction?
+ \placeexample[here][ex:AddSubAlu]{Simple \small{ALU} supporting two operations.}
+ \startcombination[2*1]
+ {\typebufferlam{AddSubAlu}}{Core description in normal form.}
+ {\boxedgraphic{AddSubAlu}}{The architecture described by the normal form.}
+ \stopcombination
+
+ 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
+ instead put some gates in front of the register's clock input, but we want
+ to show the architecture as close to the description as possible.
+
+ As you can see from the previous examples, the generation of the final
+ architecture from the normal form is straightforward. In each of the
+ examples, there is a direct match between the normal form structure,
+ the generated VHDL and the architecture shown in the images.
+
+ \startbuffer[NormalComplete]
+ regbank :: Bit
+ -> Word
+ -> State (Word, Word)
+ -> (State (Word, Word), Word)
+
+ -- All arguments are an inital lambda (address, data, packed state)
+ regbank = λa.λd.λsp.
+ -- There are nested let expressions at top level
+ let
+ -- 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 (a, b) -> a
+ r2 = case s of (a, b) -> b
+ -- Calling some other user-defined function.
+ d' = foo d
+ -- Conditional connections
+ out = case a of
+ High -> r1
+ Low -> r2
+ r1' = case a of
+ High -> d'
+ Low -> r1
+ r2' = case a of
+ High -> r2
+ Low -> d'
+ -- Packing a tuple
+ s' = (,) r1' r2'
+ -- 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
+ \stopbuffer
+
+ \startuseMPgraphic{NormalComplete}
+ save a, d, r, foo, muxr, muxout, out;
+
+ % 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
- 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
- no transformation applies anymore. We call this set of nodes the \emph{normal
- set}.
+ \todo{Don't split registers in this image?}
+ \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[sec:normalization:intendednormalform]{Intended normal form definition}
+ 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.
+
+ \defref{intended normal form definition}
+ \todo{Fix indentation}
+ \startlambda
+ \italic{normal} := \italic{lambda}
+ \italic{lambda} := λvar.\italic{lambda} (representable(var))
+ | \italic{toplet}
+ \italic{toplet} := letrec [\italic{binding}...] in var (representable(var))
+ \italic{binding} := var = \italic{rhs} (representable(rhs))
+ -- State packing and unpacking by coercion
+ | var0 = var1 ▶ State ty (lvar(var1))
+ | var0 = var1 ▶ ty (var1 :: State ty ∧ lvar(var1))
+ \italic{rhs} := userapp
+ | builtinapp
+ -- Extractor case
+ | case var of C a0 ... an -> ai (lvar(var))
+ -- Selector case
+ | case var of (lvar(var))
+ [ DEFAULT -> var ] (lvar(var))
+ C0 w0,0 ... w0,n -> var0
+ \vdots
+ Cm wm,0 ... wm,n -> varm (\forall{}i \forall{}j, wi,j \neq vari, lvar(vari))
+ \italic{userapp} := \italic{userfunc}
+ | \italic{userapp} {userarg}
+ \italic{userfunc} := var (gvar(var))
+ \italic{userarg} := var (lvar(var))
+ \italic{builtinapp} := \italic{builtinfunc}
+ | \italic{builtinapp} \italic{builtinarg}
+ \italic{builtinfunc} := var (bvar(var))
+ \italic{builtinarg} := var (representable(var) ∧ lvar(var))
+ | \italic{partapp} (partapp :: a -> b)
+ | \italic{coreexpr} (¬representable(coreexpr) ∧ ¬(coreexpr :: a -> b))
+ \italic{partapp} := \italic{userapp} | \italic{builtinapp}
+ \stoplambda
+
+ \todo{There can still be other casts around (which the code can handle,
+ e.g., ignore), which still need to be documented here}
+
+ When looking at such a program from a hardware perspective, the top level
+ lambda's define the input ports. The variable reference in the body of
+ the recursive 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} expression) or call a builtin function (\eg \lam{+} or
+ \lam{map}). For these, a hardcoded \small{VHDL} translation is
+ available.
+
+ \section[sec:normalization:transformation]{Transformation notation}
+ To be able to concisely present transformations, we use a specific format
+ for 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 letter (\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)} (binding \lam{a} to \lam{v} and \lam{B} to
+ \lam{(2 * w)}), but not \lam{(2 * w) + v}.
+ \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, commonly to prevent a transformation from
+ causing a loop with itself or another transformation.
+
+ Only if these conditions are \emph{all} true, the 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,
+ the 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 functions.
+
+ 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
+
+ η-abstraction is a well known transformation from lambda calculus. What
+ this transformation does, is take any expression that has a function type
+ and turn it into a lambda expression (giving an explicit name to the
+ argument). There are some extra conditions that ensure that this
+ transformation does not apply infinitely (which are not necessarily part
+ of the conventional definition of η-abstraction).
+
+ Consider the following function, which is a fairly obvious way to specify a
+ simple ALU (Note that \in{example}[ex:AddSubAlu] shows the normal form of this
+ function). The parentheses around the \lam{+} and \lam{-} operators are
+ commonly used in Haskell to show that the operators are used as normal
+ functions, instead of \emph{infix} operators (\eg, the operators appear
+ before their arguments, instead of in between).
+
+ \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
+ lambda 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 (which makes the second condition false). 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.
+
+ The first alternative is \lam{(+)}. This expression has a function type
+ (the operator still needs two arguments). It does not occur in function
+ position of an application and it is not a lambda expression, so the
+ transformation applies.
+
+ We look at the \lam{<original expression>} pattern, which is \lam{E}.
+ This means we bind \lam{E} to \lam{(+)}. We then replace the expression
+ with the \lam{<transformed expression>}, replacing all occurences of
+ \lam{E} with \lam{(+)}. In the \lam{<transformed expression>}, the This gives us the replacement expression:
+ \lam{λx.(+) x} (A lambda expression binding \lam{x}, with a body that
+ applies the addition operator to \lam{x}).
+
+ The complete function then becomes:
+ \startlambda
+ (case opcode of Low -> λa1.(+) a1; High -> (-)) a
+ \stoplambda
+
+ Now the transformation no longer applies to the complete first alternative
+ (since it is a lambda expression). It does not apply to the addition
+ operator again, since it is now in function position in an application. It
+ does, however, apply to the application of the addition operator, since
+ that is neither a lambda expression nor does it occur in function
+ position. This means after one more application of the transformation, the
+ function becomes:
+
+ \startlambda
+ (case opcode of Low -> λa1.λb1.(+) a1 b1; High -> (-)) a
+ \stoplambda
+
+ The other alternative is left as an exercise to the reader. The final
+ function, after applying η-abstraction until it does no longer apply is:
+
+ \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
+
+ \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,
+ this leaves the implementation free to choose any application order that
+ results in an efficient implementation. Unfortunately this is not
+ entirely true for the current set of transformations. See
+ \in{section}[sec:normalization:non-determinism] for a discussion of this
+ problem.
+
+ When applying a single transformation, we try to apply it to every (sub)expression
+ in a function, not just the top level function body. 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{Concepts}
+ A \emph{global variable} is any variable (binder) 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. Values 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{Predicates}
+ Here, we define a number of predicates 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[sec:normalization:uniq]{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 \in{section}[sec:normalization:beta]) 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, the following points can be
+ observed.
+
+ \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) within the same function (entity) 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
+ means 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 cause any conflict, but it does ensure that
+ all binders within the function are generated by the same unique supply.
+ \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.
+ \item Whenever (a 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.
+
+ Each transformation will be described informally first, explaining
+ the need for and goal of the transformation. Then, we will formally define
+ the transformation using the syntax introduced in
+ \in{section}[sec:normalization:transformation].
+
+ \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 intended
+ normal form.
+
+ \placeintermezzo{}{
+ \defref{substitution notation}
+ \startframedtext[width=8cm,background=box,frame=no]
+ \startalignment[center]
+ {\tfa Substitution notation}
+ \stopalignment
+ \blank[medium]
+
+ In some of the transformations in this chapter, we need to perform
+ substitution on an expression. Substitution means replacing every
+ occurence of some expression (usually a variable reference) with
+ another expression.
+
+ There have been a lot of different notations used in literature for
+ specifying substitution. The notation that will be used in this report
+ is the following:
+
+ \startlambda
+ E[A=>B]
+ \stoplambda
+
+ This means expression \lam{E} with all occurences of \lam{A} replaced
+ with \lam{B}.
+ \stopframedtext
+ }
+
+ \defref{beta-reduction}
+ \subsubsection[sec:normalization:beta]{β-reduction}
+ β-reduction is a well known transformation from lambda calculus, where it is
+ the main reduction step. It reduces applications of lambda 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.
+
+ Note that β-reduction also works on type lambda abstractions and type
+ applications as well. This means the substitution below also works on
+ type variables, in the case that the binder is a type variable and teh
+ expression applied to is a type.
+
+ \starttrans
+ (λx.E) M
+ -----------------
+ E[x=>M]
+ \stoptrans
+
+ % And an example
+ \startbuffer[from]
+ (λa. 2 * a) (2 * b)
+ \stopbuffer
+
+ \startbuffer[to]
+ 2 * (2 * b)
+ \stopbuffer
+
+ \transexample{beta}{β-reduction}{from}{to}
+
+ \startbuffer[from]
+ (λt.λa::t. a) @Int
+ \stopbuffer
+
+ \startbuffer[to]
+ (λa::Int. a)
+ \stopbuffer
+
+ \transexample{beta-type}{β-reduction for type abstractions}{from}{to}
+
+ \subsubsection{Empty let removal}
+ This transformation is simple: It removes recursive lets that have no bindings
+ (which usually occurs when unused let binding removal removes the last
+ binding from it).
+
+ Note that there is no need to define this transformation for
+ non-recursive lets, since they always contain exactly one binding.
+
+ \starttrans
+ letrec in M
+ --------------
+ M
+ \stoptrans
+
+ \todo{Example}
+
+ \subsubsection[sec:normalization:simplelet]{Simple let binding removal}
+ This transformation inlines simple let bindings, that bind some
+ binder to some other binder instead of a more complex expression (\ie
+ a = b).
+
+ This transformation is not needed to get an expression into intended
+ normal form (since these bindings are part of the intended normal
+ form), but makes the resulting \small{VHDL} a lot shorter.
+
+ \refdef{substitution notation}
+ \starttrans
+ letrec
+ a0 = E0
+ \vdots
+ ai = b
+ \vdots
+ an = En
+ in
+ M
+ ----------------------------- \lam{b} is a variable reference
+ letrec \lam{ai} ≠ \lam{b}
+ a0 = E0 [ai=>b]
+ \vdots
+ ai-1 = Ei-1 [ai=>b]
+ ai+1 = Ei+1 [ai=>b]
+ \vdots
+ an = En [ai=>b]
+ in
+ M[ai=>b]
+ \stoptrans
+
+ \todo{example}
+
+ \subsubsection{Unused let binding removal}
+ This transformation removes let bindings that are never used.
+ Occasionally, \GHC's desugarer introduces some unused let bindings.
+
+ This normalization pass should really be unneeded to get into intended normal form
+ (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.
+
+ \todo{Don't use old-style numerals in transformations}
+ \starttrans
+ letrec
+ a0 = E0
+ \vdots
+ ai = Ei
+ \vdots
+ an = En
+ in
+ M \lam{ai} does not occur free in \lam{M}
+ ---------------------------- \forall j, 0 ≤ j ≤ n, j ≠ i (\lam{ai} 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.
+
+ \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 intended 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{toplevelinline}{Top level binding inlining}{from}{to}
+
+ \in{Example}[ex:trans:toplevelinline] shows a typical application of
+ the addition operator generated by \GHC. The type and dictionary
+ arguments used here are described in
+ \in{Section}[section:prototype:polymorphism].
+
+ Without this transformation, there would be a \lam{(+)} entity
+ in the \VHDL 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 most
+ non-alphanumerics, like all characters in \lam{(+)}, are 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 or current state), putting all
+ of the other value definitions in let bindings and making the final
+ return value a simple variable reference.
+
+ \subsubsection[sec:normalization:eta]{η-abstraction}
+ This transformation makes sure that all arguments of a function-typed
+ expression are named, by introducing lambda expressions. When combined with
+ β-reduction and non-representable binding inlining, all function-typed
+ expressions should be lambda abstractions or global identifiers.
+
+ \starttrans
+ 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}.
+ \stoptrans
+
+ \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{eta}{η-abstraction}{from}{to}
+
+ \subsubsection[sec:normalization:appprop]{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).
+
+ Since all binders in our expression are unique (see
+ \in{section}[sec:normalization:uniq]), there is no risk that we will
+ introduce unintended shadowing by moving an expression into a lower
+ scope. Also, since only move expression into smaller scopes (down into
+ our expression), there is no risk of moving a variable reference out
+ of the scope in which it is defined.
+
+ \starttrans
+ (letrec binds in E) M
+ ------------------------
+ letrec binds in E M
+ \stoptrans
+
+ % And an example
+ \startbuffer[from]
+ ( letrec
+ val = 1
+ in
+ add val
+ ) 3
+ \stopbuffer
+
+ \startbuffer[to]
+ letrec
+ val = 1
+ in
+ add val 3
+ \stopbuffer
+
+ \transexample{appproplet}{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{apppropcase}{Application propagation for a case expression}{from}{to}
+
+ \subsubsection[sec:normalization:letrecurse]{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
+ binding(s) of the inner let into the outer let. Eventually, this will
+ cause all let bindings to appear in the same scope.
+
+ This transformation only applies to recursive lets, since all
+ non-recursive lets will be made recursive (see
+ \in{section}[sec:normalization:letrecurse]).
+
+ Since we are joining two scopes together, there is no risk of moving a
+ variable reference out of the scope where it is defined.
+
+ \starttrans
+ letrec
+ a0 = E0
+ \vdots
+ ai = (letrec bindings in M)
+ \vdots
+ an = En
+ in
+ N
+ ------------------------------------------
+ letrec
+ a0 = E0
+ \vdots
+ ai = M
+ \vdots
+ an = En
+ bindings
+ in
+ N
+ \stoptrans
+
+ \startbuffer[from]
+ letrec
+ a = 1
+ b = letrec
+ x = a
+ y = c
+ in
+ x + y
+ c = 2
+ in
+ b
+ \stopbuffer
+ \startbuffer[to]
+ letrec
+ a = 1
+ b = x + y
+ c = 2
+ x = a
+ y = c
+ in
+ b
+ \stopbuffer
+
+ \transexample{letflat}{Let flattening}{from}{to}
+
+ \subsubsection{Return value simplification}
+ This transformation ensures that the return value of a function is always a
+ simple local variable reference.
+
+ Currently implemented using lambda simplification, let simplification, and
+ top simplification. Should change into something like the following, which
+ works only on the result of a function instead of any subexpression. This is
+ achieved by the contexts, like \lam{x = E}, though this is strictly not
+ correct (you could read this as "if there is any function \lam{x} that binds
+ \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. 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 translatable 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
+ letrec x = E in x
+ \stoptrans
+
+ \starttrans
+ x = λv0 ... λvn.E
+ ~ \lam{E} is representable
+ E \lam{E} is not a let expression
+ --------------------------- \lam{E} is not a local variable reference
+ letrec x = E in x
+ \stoptrans
+
+ \starttrans
+ x = λv0 ... λvn.let ... in E
+ ~ \lam{E} is representable
+ E \lam{E} is not a local variable reference
+ -----------------------------
+ letrec x = E in x
+ \stoptrans
+
+ \startbuffer[from]
+ x = add 1 2
+ \stopbuffer
+
+ \startbuffer[to]
+ x = letrec x = add 1 2 in x
+ \stopbuffer
+
+ \transexample{retvalsimpl}{Return value simplification}{from}{to}
+
+ \todo{More examples}
+
+ \subsection[sec:normalization:argsimpl]{Representable arguments simplification}
+ This section contains just a single transformation that deals with
+ representable arguments in applications. Non-representable arguments are
+ handled by the transformations in
+ \in{section}[sec:normalization:nonrep].
+
+ This transformation ensures that all representable arguments will become
+ references to local variables. This ensures they will become references
+ to local signals in the resulting \small{VHDL}, which is required due to
+ limitations in the component instantiation code in \VHDL (one can only
+ assign a signal or constant to an input port). By ensuring that all
+ arguments are always simple variable references, we always have a signal
+ available to map to the input ports.
+
+ 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.
+
+ \refdef{global variable}
+ Note that references to \emph{global variables} (like a top level
+ function without arguments, but also an argumentless dataconstructors
+ like \lam{True}) are also simplified. Only local variables generate
+ signals in the resulting architecture. Even though argumentless
+ dataconstructors generate constants in generated \VHDL code and could be
+ mapped to an input port directly, they are still simplified to make the
+ normal form more regular.
+
+ \refdef{representable}
+ \starttrans
+ M N
+ -------------------- \lam{N} is representable
+ letrec x = N in M x \lam{N} is not a local variable reference
+ \stoptrans
+ \refdef{local variable}
+
+ \startbuffer[from]
+ add (add a 1) 1
+ \stopbuffer
+
+ \startbuffer[to]
+ letrec x = add a 1 in add x 1
+ \stopbuffer
+
+ \transexample{argsimpl}{Argument simplification}{from}{to}
+
+ \subsection[sec:normalization:builtins]{Builtin functions}
+ This section deals with (arguments to) builtin functions. In the
+ intended normal form definition\refdef{intended normal form definition}
+ we can see that there are three sorts of arguments a builtin function
+ can receive.
+
+ \startitemize[KR]
+ \item A representable local variable reference. This is the most
+ common argument to any function. The argument simplification
+ transformation described in \in{section}[sec:normalization:argsimpl]
+ makes sure that \emph{any} representable argument to \emph{any}
+ function (including builtin functions) is turned into a local variable
+ reference.
+ \item (A partial application of) a top level function (either builtin on
+ user-defined). The function extraction transformation described in
+ this section takes care of turning every functiontyped argument into
+ (a partial application of) a top level function.
+ \item Any expression that is not representable and does not have a
+ function type. Since these can be any expression, there is no
+ transformation needed. Note that this category is exactly all
+ expressions that are not transformed by the transformations for the
+ previous two categories. This means that \emph{any} core expression
+ that is used as an argument to a builtin function will be either
+ transformed into one of the above categories, or end up in this
+ categorie. In any case, the result is in normal form.
+ \stopitemize
+
+ As noted, the argument simplification will handle any representable
+ arguments to a builtin function. The following transformation is needed
+ to handle non-representable arguments with a function type, all other
+ non-representable arguments don't need any special handling.
+
+ \subsubsection[sec:normalization:funextract]{Function extraction}
+ This transform deals with function-typed arguments to builtin
+ functions.
+ Since builtin functions cannot be specialized (see
+ \in{section}[sec:normalization:specialize]) to remove the arguments,
+ these arguments are extracted into a new global function instead. In
+ other words, we create a new top level function that has exactly the
+ extracted argument as its body. This greatly simplifies the
+ translation rules needed for builtin functions, since they only need
+ to handle (partial applications of) top level functions.
+
+ 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.
+
+ 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 \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).
+
+ \starttrans
+ M N \lam{M} is (a partial aplication of) a builtin function.
+ --------------------- \lam{f0 ... fn} are all free local variables of \lam{N}
+ 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
+
+ \startbuffer[from]
+ addList = λb.λxs.map (λa . add a b) xs
+ \stopbuffer
+
+ \startbuffer[to]
+ addList = λb.λxs.map (f b) xs
+ ~
+ f = λb.λa.add a b
+ \stopbuffer
+
+ \transexample{funextract}{Function extraction}{from}{to}
+
+ Note that the function \lam{f} will still need normalization after
+ this.
+
+ \subsection{Case normalisation}
+ \subsubsection{Scrutinee simplification}
+ This transform ensures that the scrutinee of a case expression is always
+ a simple variable reference.
+
+ \starttrans
+ case E of
+ alts
+ ----------------- \lam{E} is not a local variable reference
+ letrec x = E in
+ case E of
+ alts
+ \stoptrans
+
+ \startbuffer[from]
+ case (foo a) of
+ True -> a
+ False -> b
+ \stopbuffer
+
+ \startbuffer[to]
+ letrec x = foo a in
+ case x of
+ True -> a
+ False -> b
+ \stopbuffer
+
+ \transexample{letflat}{Case normalisation}{from}{to}
+
+
+ \subsubsection{Case simplification}
+ This transformation ensures that all case expressions become normal form. This
+ means they will become one of:
+ \startitemize
+ \item An extractor case with a single alternative that picks a single field
+ from a datatype, \eg \lam{case x of (a, b) -> a}.
+ \item A selector case with multiple alternatives and only wild binders, that
+ makes a choice between expressions based on the constructor of another
+ expression, \eg \lam{case x of Low -> a; High -> b}.
+ \stopitemize
+
+ \defref{wild binder}
+ \starttrans
+ case E of
+ C0 v0,0 ... v0,m -> E0
+ \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)
+ letrec
+ v0,0 = case E of C0 v0,0 .. v0,m -> v0,0
+ \vdots
+ v0,m = case E of C0 v0,0 .. v0,m -> v0,m
+ \vdots
+ vn,m = case E of Cn vn,0 .. vn,m -> vn,m
+ x0 = E0
+ \vdots
+ xn = En
+ in
+ case E of
+ C0 w0,0 ... w0,m -> x0
+ \vdots
+ Cn wn,0 ... wn,m -> xn
+ \stoptrans
+ \todo{Check the subscripts of this transformation}
+
+ Note that this transformation applies to case statements with any
+ scrutinee. If the scrutinee is a complex expression, this might result
+ in duplicate hardware. An extra condition to only apply this
+ transformation when the scrutinee is already simple (effectively
+ causing this transformation to be only applied after the scrutinee
+ simplification transformation) might be in order.
+
+ \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
+ True -> add b 1
+ False -> add b 2
+ \stopbuffer
+
+ \startbuffer[to]
+ letnonrec
+ x0 = add b 1
+ x1 = add b 2
+ in
+ case a of
+ True -> x0
+ False -> x1
+ \stopbuffer
+
+ \transexample{selcasesimpl}{Selector case simplification}{from}{to}
+
+ \startbuffer[from]
+ case a of
+ (,) b c -> add b c
+ \stopbuffer
+ \startbuffer[to]
+ letrec
+ b = case a of (,) b c -> b
+ c = case a of (,) b c -> c
+ x0 = add b c
+ in
+ case a of
+ (,) w0 w1 -> x0
+ \stopbuffer
+
+ \transexample{excasesimpl}{Extractor case simplification}{from}{to}
+
+ \refdef{selector case}
+ In \in{example}[ex:trans:excasesimpl] the case expression is expanded
+ into multiple case expressions, including a pretty useless expression
+ (that is neither a selector or extractor case). This case can be
+ removed by the Case removal transformation in
+ \in{section}[sec:transformation:caseremoval].
+
+ \subsubsection[sec:transformation:caseremoval]{Case removal}
+ This transform removes any case statements with a single alternative and
+ only wild binders.
+
+ These "useless" case statements are usually leftovers from case simplification
+ on extractor case (see the previous example).
+
+ \starttrans
+ case x of
+ C v0 ... vm -> E
+ ---------------------- \lam{\forall i, 0 ≤ i ≤ m} (\lam{vi} does not occur free in E)
+ E
+ \stoptrans
+
+ \startbuffer[from]
+ case a of
+ (,) w0 w1 -> x0
+ \stopbuffer
+
+ \startbuffer[to]
+ x0
+ \stopbuffer
+
+ \transexample{caserem}{Case removal}{from}{to}
+
+ \subsection[sec:normalization:nonrep]{Removing unrepresentable values}
+ The transformations in this section are aimed at making all the
+ values used in our expression representable. There are two main
+ transformations that are applied to \emph{all} unrepresentable let
+ bindings and function arguments. These are meant to address three
+ different kinds of unrepresentable values: Polymorphic values, higher
+ order values and literals. The transformation are described generically:
+ They apply to all non-representable values. However, non-representable
+ values that don't fall into one of these three categories will be moved
+ around by these transformations but are unlikely to completely
+ disappear. They usually mean the program was not valid in the first
+ place, because unsupported types were used (for example, a program using
+ strings).
+
+ Each of these three categories will be detailed below, followed by the
+ actual transformations.
+
+ \subsubsection{Removing Polymorphism}
+ As noted in \in{section}[sec:prototype:polymporphism],
+ polymorphism is made explicit in Core through type and
+ dictionary arguments. To remove the polymorphism from a
+ function, we can simply specialize the polymorphic function for
+ the particular type applied to it. The same goes for dictionary
+ arguments. To remove polymorphism from let bound values, we
+ simply inline the let bindings that have a polymorphic type,
+ which should (eventually) make sure that the polymorphic
+ expression is applied to a type and/or dictionary, which can
+ then be removed by β-reduction (\in{section}[sec:normalization:beta]).
+
+ Since both type and dictionary arguments are not representable,
+ \refdef{representable}
+ the non-representable argument specialization and
+ non-representable let binding inlining transformations below
+ take care of exactly this.
+
+ There is one case where polymorphism cannot be completely
+ removed: Builtin functions are still allowed to be polymorphic
+ (Since we have no function body that we could properly
+ specialize). However, the code that generates \VHDL for builtin
+ functions knows how to handle this, so this is not a problem.
+
+ \subsubsection{Defunctionalization}
+ These transformations remove higher order expressions from our
+ program, making all values first-order.
+
+ Higher order values are always introduced by lambda abstractions, none
+ of the other Core expression elements can introduce a function type.
+ However, other expressions can \emph{have} a function type, when they
+ have a lambda expression in their body.
+
+ For example, the following expression is a higher order expression
+ that is not a lambda expression itself:
+
+ \refdef{id function}
+ \startlambda
+ case x of
+ High -> id
+ Low -> λx.x
+ \stoplambda
+
+ The reference to the \lam{id} function shows that we can introduce a
+ higher order expression in our program without using a lambda
+ expression directly. However, inside the definition of the \lam{id}
+ function, we can be sure that a lambda expression is present.
+
+ Looking closely at the definition of our normal form in
+ \in{section}[sec:normalization:intendednormalform], we can see that
+ there are three possibilities for higher order values to appear in our
+ intended normal form:
+
+ \startitemize[KR]
+ \item[item:toplambda] Lambda abstractions can appear at the highest level of a
+ top level function. These lambda abstractions introduce the
+ arguments (input ports / current state) of the function.
+ \item[item:builtinarg] (Partial applications of) top level functions can appear as an
+ argument to a builtin function.
+ \item[item:completeapp] (Partial applications of) top level functions can appear in
+ function position of an application. Since a partial application
+ cannot appear anywhere else (except as builtin function arguments),
+ all partial applications are applied, meaning that all applications
+ will become complete applications. However, since application of
+ arguments happens one by one, in the expression:
+ \startlambda
+ f 1 2
+ \stoplambda
+ the subexpression \lam{f 1} has a function type. But this is
+ allowed, since it is inside a complete application.
+ \stopitemize
+
+ We will take a typical function with some higher order values as an
+ example. The following function takes two arguments: a \lam{Bit} and a
+ list of numbers. Depending on the first argument, each number in the
+ list is doubled, or the list is returned unmodified. For the sake of
+ the example, no polymorphism is shown. In reality, at least map would
+ be polymorphic.
+
+ \startlambda
+ λy.let double = λx. x + x in
+ case y of
+ Low -> map double
+ High -> λz. z
+ \stoplambda
+
+ This example shows a number of higher order values that we cannot
+ translate to \VHDL directly. The \lam{double} binder bound in the let
+ expression has a function type, as well as both of the alternatives of
+ the case expression. The first alternative is a partial application of
+ the \lam{map} builtin function, whereas the second alternative is a
+ lambda abstraction.
+
+ To reduce all higher order values to one of the above items, a number
+ of transformations we've already seen are used. The η-abstraction
+ transformation from \in{section}[sec:normalization:eta] ensures all
+ function arguments are introduced by lambda abstraction on the highest
+ level of a function. These lambda arguments are allowed because of
+ \in{item}[item:toplambda] above. After η-abstraction, our example
+ becomes a bit bigger:
+
+ \startlambda
+ λy.λq.(let double = λx. x + x in
+ case y of
+ Low -> map double
+ High -> λz. z
+ ) q
+ \stoplambda
+
+ η-abstraction also introduces extra applications (the application of
+ the let expression to \lam{q} in the above example). These
+ applications can then propagated down by the application propagation
+ transformation (\in{section}[sec:normalization:appprop]). In our
+ example, the \lam{q} and \lam{r} variable will be propagated into the
+ let expression and then into the case expression:
+
+ \startlambda
+ λy.λq.let double = λx. x + x in
+ case y of
+ Low -> map double q
+ High -> (λz. z) q
+ \stoplambda
+
+ This propagation makes higher order values become applied (in
+ particular both of the alternatives of the case now have a
+ representable type). Completely applied top level functions (like the
+ first alternative) are now no longer invalid (they fall under
+ \in{item}[item:completeapp] above). (Completely) applied lambda
+ abstractions can be removed by β-abstraction. For our example,
+ applying β-abstraction results in the following:
+
+ \startlambda
+ λy.λq.let double = λx. x + x in
+ case y of
+ Low -> map double q
+ High -> q
+ \stoplambda
+
+ As you can see in our example, all of this moves applications towards
+ the higher order values, but misses higher order functions bound by
+ let expressions. The applications cannot be moved towards these values
+ (since they can be used in multiple places), so the values will have
+ to be moved towards the applications. This is achieved by inlining all
+ higher order values bound by let applications, by the
+ non-representable binding inlining transformation below. When applying
+ it to our example, we get the following:
+
+ \startlambda
+ λy.λq.case y of
+ Low -> map (λx. x + x) q
+ High -> q
+ \stoplambda
+
+ We've nearly eliminated all unsupported higher order values from this
+ expressions. The one that's remaining is the first argument to the
+ \lam{map} function. Having higher order arguments to a builtin
+ function like \lam{map} is allowed in the intended normal form, but
+ only if the argument is a (partial application) of a top level
+ function. This is easily done by introducing a new top level function
+ and put the lambda abstraction inside. This is done by the function
+ extraction transformation from
+ \in{section}[sec:normalization:funextract].
+
+ \startlambda
+ λy.λq.case y of
+ Low -> map func q
+ High -> q
+ \stoplambda
+
+ This also introduces a new function, that we have called \lam{func}:
+
+ \startlambda
+ func = λx. x + x
+ \stoplambda
+
+ Note that this does not actually remove the lambda, but now it is a
+ lambda at the highest level of a function, which is allowed in the
+ intended normal form.
+
+ There is one case that has not been discussed yet. What if the
+ \lam{map} function in the example above was not a builtin function
+ but a user-defined function? Then extracting the lambda expression
+ into a new function would not be enough, since user-defined functions
+ can never have higher order arguments. For example, the following
+ expression shows an example:
+
+ \startlambda
+ twice :: (Word -> Word) -> Word -> Word
+ twice = λf.λa.f (f a)
+
+ main = λa.app (λx. x + x) a
+ \stoplambda
+
+ This example shows a function \lam{twice} that takes a function as a
+ first argument and applies that function twice to the second argument.
+ Again, we've made the function monomorphic for clarity, even though
+ this function would be a lot more useful if it was polymorphic. The
+ function \lam{main} uses \lam{twice} to apply a lambda epression twice.
+
+ When faced with a user defined function, a body is available for that
+ function. This means we could create a specialized version of the
+ function that only works for this particular higher order argument
+ (\ie, we can just remove the argument and call the specialized
+ function without the argument). This transformation is detailed below.
+ Applying this transformation to the example gives:
+
+ \startlambda
+ twice' :: Word -> Word
+ twice' = λb.(λf.λa.f (f a)) (λx. x + x) b
+
+ main = λa.app' a
+ \stoplambda
+
+ The \lam{main} function is now in normal form, since the only higher
+ order value there is the top level lambda expression. The new
+ \lam{twice'} function is a bit complex, but the entire original body of
+ the original \lam{twice} function is wrapped in a lambda abstraction
+ and applied to the argument we've specialized for (\lam{λx. x + x})
+ and the other arguments. This complex expression can fortunately be
+ effectively reduced by repeatedly applying β-reduction:
+
+ \startlambda
+ twice' :: Word -> Word
+ twice' = λb.(b + b) + (b + b)
+ \stoplambda
+
+ This example also shows that the resulting normal form might not be as
+ efficient as we might hope it to be (it is calculating \lam{(b + b)}
+ twice). This is discussed in more detail in
+ \in{section}[sec:normalization:duplicatework].
+
+ \subsubsection{Literals}
+ There are a limited number of literals available in Haskell and Core.
+ \refdef{enumerated types} When using (enumerating) algebraic
+ datatypes, a literal is just a reference to the corresponding data
+ constructor, which has a representable type (the algebraic datatype)
+ and can be translated directly. This also holds for literals of the
+ \hs{Bool} Haskell type, which is just an enumerated type.
+
+ There is, however, a second type of literal that does not have a
+ representable type: Integer literals. Cλash supports using integer
+ literals for all three integer types supported (\hs{SizedWord},
+ \hs{SizedInt} and \hs{RangedWord}). This is implemented using
+ Haskell's \hs{Num} typeclass, which offers a \hs{fromInteger} method
+ that converts any \hs{Integer} to the Cλash datatypes.
+
+ When \GHC sees integer literals, it will automatically insert calls to
+ the \hs{fromInteger} method in the resulting Core expression. For
+ example, the following expression in Haskell creates a 32 bit unsigned
+ word with the value 1. The explicit type signature is needed, since
+ there is no context for \GHC to determine the type from otherwise.
+
+ \starthaskell
+ 1 :: SizedWord D32
+ \stophaskell
+
+ This Haskell code results in the following Core expression:
+
+ \startlambda
+ fromInteger @(SizedWord D32) \$dNum (smallInteger 10)
+ \stoplambda
+
+ The literal 10 will have the type \lam{GHC.Prim.Int\#}, which is
+ converted into an \lam{Integer} by \lam{smallInteger}. Finally, the
+ \lam{fromInteger} function will finally convert this into a
+ \lam{SizedWord D32}.
+
+ Both the \lam{GHC.Prim.Int\#} and \lam{Integer} types are not
+ representable, and cannot be translated directly. Fortunately, there
+ is no need to translate them, since \lam{fromInteger} is a builtin
+ function that knows how to handle these values. However, this does
+ require that the \lam{fromInteger} function is directly applied to
+ these non-representable literal values, otherwise errors will occur.
+ For example, the following expression is not in the intended normal
+ form, since one of the let bindings has an unrepresentable type
+ (\lam{Integer}):
+
+ \startlambda
+ let l = smallInteger 10 in fromInteger @(SizedWord D32) \$dNum l
+ \stoplambda
+
+ By inlining these let-bindings, we can ensure that unrepresentable
+ literals bound by a let binding end up in an application of the
+ appropriate builtin function, where they are allowed. Since it is
+ possible that the application of that function is in a different
+ function than the definition of the literal value, we will always need
+ to specialize away any unrepresentable literals that are used as
+ function arguments. The following two transformations do exactly this.
+
+ \subsubsection{Non-representable binding inlining}
+ This transform inlines let bindings that are bound to a
+ non-representable value. Since we can never generate a signal
+ assignment for these bindings (we cannot declare a signal assignment
+ with a non-representable type, for obvious reasons), we have no choice
+ but to inline the binding to remove it.
+
+ As we have seen in the previous sections, inlining these bindings
+ solves (part of) the polymorphism, higher order values and
+ unrepresentable literals in an expression.
+
+ \refdef{substitution notation}
+ \starttrans
+ letrec
+ a0 = E0
+ \vdots
+ ai = Ei
+ \vdots
+ an = En
+ in
+ M
+ -------------------------- \lam{Ei} has a non-representable type.
+ letrec
+ a0 = E0 [ai=>Ei] \vdots
+ ai-1 = Ei-1 [ai=>Ei]
+ ai+1 = Ei+1 [ai=>Ei]
+ \vdots
+ an = En [ai=>Ei]
+ in
+ M[ai=>Ei]
+ \stoptrans
+
+ \startbuffer[from]
+ letrec
+ a = smallInteger 10
+ inc = λb -> add b 1
+ inc' = add 1
+ x = fromInteger a
+ in
+ inc (inc' x)
+ \stopbuffer
+
+ \startbuffer[to]
+ letrec
+ x = fromInteger (smallInteger 10)
+ in
+ (λb -> add b 1) (add 1 x)
+ \stopbuffer
+
+ \transexample{nonrepinline}{Nonrepresentable binding inlining}{from}{to}
+
+ \subsubsection[sec:normalization:specialize]{Function specialization}
+ This transform removes arguments to user-defined functions that are
+ not representable at runtime. This is done by creating a
+ \emph{specialized} version of the function that only works for one
+ particular value of that argument (in other words, the argument can be
+ removed).
+
+ Specialization means to create a specialized version of the called
+ function, with one argument already filled in. As a simple example, in
+ the following program (this is not actual Core, since it directly uses
+ a literal with the unrepresentable type \lam{GHC.Prim.Int\#}).
+
+ \startlambda
+ f = λa.λb.a + b
+ inc = λa.f a 1
+ \stoplambda
+
+ We could specialize the function \lam{f} against the literal argument
+ 1, with the following result:
+
+ \startlambda
+ f' = λa.a + 1
+ inc = λa.f' a
+ \stoplambda
+
+ In some way, this transformation is similar to β-reduction, but it
+ operates across function boundaries. It is also similar to
+ non-representable let binding inlining above, since it sort of
+ \quote{inlines} an expression into a called function.
+
+ Special care must be taken when the argument has any free variables.
+ If this is the case, the original argument should not be removed
+ completely, but replaced by all the free variables of the expression.
+ In this way, the original expression can still be evaluated inside the
+ new function.
+
+ 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 or β-reduction transformation to replace such a
+ variable with an expression we can propagate again.
+
+ \starttrans
+ x = E
+ ~
+ x Y0 ... Yi ... Yn \lam{Yi} is not representable
+ --------------------------------------------- \lam{Yi} is not a local variable reference
+ x' y0 ... yi-1 f0 ... fm Yi+1 ... Yn \lam{f0 ... fm} are all free local vars of \lam{Yi}
+ ~ \lam{T0 ... Tn} are the types of \lam{Y0 ... Yn}
+ x' = λ(y0 :: T0) ... λ(yi-1 :: Ty-1). λf0 ... λfm. λ(yi+1 :: Ty+1) ... λ(yn :: Tn).
+ E y0 ... yi-1 Yi yi+1 ... yn
+ \stoptrans
+
+ This is a bit of a complex transformation. It transforms an
+ application of the function \lam{x}, where one of the arguments
+ (\lam{Y_i}) is not representable. A new
+ function \lam{x'} is created that wraps the body of the old function.
+ The body of the new function becomes a number of nested lambda
+ abstractions, one for each of the original arguments that are left
+ unchanged.
+
+ The ith argument is replaced with the free variables of
+ \lam{Y_i}. Note that we reuse the same binders as those used in
+ \lam{Y_i}, since we can then just use \lam{Y_i} inside the new
+ function body and have all of the variables it uses be in scope.
+
+ The argument that we are specializing for, \lam{Y_i}, is put inside
+ the new function body. The old function body is applied to it. Since
+ we use this new function only in place of an application with that
+ particular argument \lam{Y_i}, behaviour should not change.
+
+ Note that the types of the arguments of our new function are taken
+ from the types of the \emph{actual} arguments (\lam{T0 ... Tn}). This
+ means that any polymorphism in the arguments is removed, even when the
+ corresponding explicit type lambda is not removed
+ yet.\refdef{type lambda}
+
+ \todo{Examples. Perhaps reference the previous sections}
+
+ \section{Unsolved problems}
+ The above system of transformations has been implemented in the prototype
+ and seems to work well to compile simple and more complex examples of
+ hardware descriptions. \todo{Ref christiaan?} However, this normalization
+ system has not seen enough review and work to be complete and work for
+ every Core expression that is supplied to it. A number of problems
+ have already been identified and are discussed in this section.
+
+ \subsection[sec:normalization:duplicatework]{Work duplication}
+ A possible problem of β-reduction is that it could duplicate work.
+ When the expression applied is not a simple variable reference, but
+ requires calculation and the binder the lambda abstraction binds to
+ is used more than once, more hardware might be generated than strictly
+ needed.
+
+ As an example, consider the expression:
+
+ \startlambda
+ (λx. x + x) (a * b)
+ \stoplambda
+
+ When applying β-reduction to this expression, we get:
+
+ \startlambda
+ (a * b) + (a * b)
+ \stoplambda
+
+ which of course calculates \lam{(a * b)} twice.
+
+ A possible solution to this would be to use the following alternative
+ transformation, which is of course no longer normal β-reduction. The
+ followin transformation has not been tested in the prototype, but is
+ given here for future reference:
+
+ \starttrans
+ (λx.E) M
+ -----------------
+ letrec x = M in E
+ \stoptrans
+
+ This doesn't seem like much of an improvement, but it does get rid of
+ the lambda expression (and the associated higher order value), while
+ at the same time introducing a new let binding. Since the result of
+ every application or case expression must be bound by a let expression
+ in the intended normal form anyway, this is probably not a problem. If
+ the argument happens to be a variable reference, then simple let
+ binding removal (\in{section}[sec:normalization:simplelet]) will
+ remove it, making the result identical to that of the original
+ β-reduction transformation.
+
+ When also applying argument simplification to the above example, we
+ get the following expression:
+
+ \startlambda
+ let y = (a * b)
+ z = (a * b)
+ in y + z
+ \stoplambda
+
+ Looking at this, we could imagine an alternative approach: Create a
+ transformation that removes let bindings that bind identical values.
+ In the above expression, the \lam{y} and \lam{z} variables could be
+ merged together, resulting in the more efficient expression:
+
+ \startlambda
+ let y = (a * b) in y + y
+ \stoplambda
+
+ \subsection[sec:normalization:non-determinism]{Non-determinism}
+ As an example, again consider the following expression:
+
+ \startlambda
+ (λx. x + x) (a * b)
+ \stoplambda
+
+ We can apply both β-reduction (\in{section}[sec:normalization:beta])
+ as well as argument simplification
+ (\in{section}[sec:normalization:argsimpl]) to this expression.
+
+ When applying argument simplification first and then β-reduction, we
+ get the following expression:
+
+ \startlambda
+ let y = (a * b) in y + y
+ \stoplambda
+
+ When applying β-reduction first and then argument simplification, we
+ get the following expression:
+
+ \startlambda
+ let y = (a * b)
+ z = (a * b)
+ in y + z
+ \stoplambda
+
+ As you can see, this is a different expression. This means that the
+ order of expressions, does in fact change the resulting normal form,
+ which is something that we would like to avoid. In this particular
+ case one of the alternatives is even clearly more efficient, so we
+ would of course like the more efficient form to be the normal form.
+
+ For this particular problem, the solutions for duplication of work
+ seem from the previous section seem to fix the determinism of our
+ transformation system as well. However, it is likely that there are
+ other occurences of this problem.
+
+ \subsection{Casts}
+ We do not fully understand the use of cast expressions in Core, so
+ there are probably expressions involving cast expressions that cannot
+ be brought into intended normal form by this transformation system.
+
+ The uses of casts in the core system should be investigated more and
+ transformations will probably need updating to handle them in all
+ cases.
+
+ \subsection{Normalization of stateful descriptions}
+ Currently, the intended normal form definition\refdef{intended
+ normal form definition} offers enough freedom to describe all
+ valid stateful descriptions, but is not limiting enough. It is
+ possible to write descriptions which are in intended normal
+ form, but cannot be translated into \VHDL in a meaningful way
+ (\eg, a function that swaps two substates in its result, or a
+ function that changes a substate itself instead of passing it to
+ a subfunction).
+
+ It is now up to the programmer to not do anything funny with
+ these state values, whereas the normalization just tries not to
+ mess up the flow of state values. In practice, there are
+ situations where a Core program that \emph{could} be a valid
+ stateful description is not translateable by the prototype. This
+ most often happens when statefulness is mixed with pattern
+ matching, causing a state input to be unpacked multiple times or
+ be unpacked and repacked only in some of the code paths.
+
+ \todo{example?}
+
+ Without going into detail about the exact problems (of which
+ there are probably more than have shown up so far), it seems
+ unlikely that these problems can be solved entirely by just
+ improving the \VHDL state generation in the final stage. The
+ normalization stage seems the best place to apply the rewriting
+ needed to support more complex stateful descriptions. This does
+ of course mean that the intended normal form definition must be
+ extended as well to be more specific about how state handling
+ should look like in normal form.
+
+ \section[sec:normalization:properties]{Provable properties}
+ When looking at the system of transformations outlined above, there are a
+ number of questions that we can ask ourselves. The main question is of course:
+ \quote{Does our system work as intended?}. We can split this question into a
+ number of subquestions:
- From such a graph, we can derive some properties easily:
\startitemize[KR]
- \item A system will \emph{terminate} if there is no path of infinite length
- in the graph (this includes cycles).
- \item Soundness is not easily represented in the graph.
- \item A system is \emph{complete} if all of the nodes in the normal set have
- the intended normal form. The inverse (that all of the nodes outside of
- the normal set are \emph{not} in the intended normal form) is not
- strictly required.
- \item A system is deterministic if all paths from a node, which end in a node
- in the normal set, end at the same node.
+ \item[q:termination] Does our system \emph{terminate}? Since our system will
+ keep running as long as transformations apply, there is an obvious risk that
+ it will keep running indefinitely. This typically happens when one
+ transformation produces a result that is transformed back to the original
+ by another transformation, or when one or more transformations keep
+ expanding some expression.
+ \item[q:soundness] Is our system \emph{sound}? Since our transformations
+ continuously modify the expression, there is an obvious risk that the final
+ normal form will not be equivalent to the original program: Its meaning could
+ have changed.
+ \item[q:completeness] Is our system \emph{complete}? Since we have a complex
+ system of transformations, there is an obvious risk that some expressions will
+ not end up in our intended normal form, because we forgot some transformation.
+ In other words: Does our transformation system result in our intended normal
+ form for all possible inputs?
+ \item[q:determinism] Is our system \emph{deterministic}? Since we have defined
+ no particular order in which the transformation should be applied, there is an
+ obvious risk that different transformation orderings will result in
+ \emph{different} normal forms. They might still both be intended normal forms
+ (if our system is \emph{complete}) and describe correct hardware (if our
+ system is \emph{sound}), so this property is less important than the previous
+ three: The translator would still function properly without it.
\stopitemize
- When looking at the \in{example}[ex:TransformGraph], we see that the system
- terminates for both the reduction and expansion systems (but note that, for
- expansion, this is only true because we've limited the possible expressions!
- In comlete lambda calculus, there would be a path from \lam{(λx.λy. (+) x y)
- 1} to \lam{(λx.λy.(λz.(+) z) x y) 1} to \lam{(λx.λy.(λz.(λq.(+) q) z) x y) 1}
- etc.)
-
- If we would consider the system with both expansion and reduction, there would
- no longer be termination, since there would be cycles all over the place.
-
- The reduction and expansion systems have a normal set of containing just
- \lam{(+) 1} or \lam{(λx.λy. (+) x y) 1} respectively. Since all paths in
- either system end up in these normal forms, both systems are \emph{complete}.
- Also, since there is only one normal form, it must obviously be
- \emph{deterministic} as well.
-
- \subsection{Termination}
- Approach: Counting.
-
- Church-Rosser?
-
- \subsection{Soundness}
- Needs formal definition of semantics.
- Prove for each transformation seperately, implies soundness of the system.
-
- \subsection{Completeness}
- Show that any transformation applies to every Core expression that is not
- in normal form. To prove: no transformation applies => in intended form.
- Show the reverse: Not in intended form => transformation applies.
-
- \subsection{Determinism}
- How to prove this?
+ Unfortunately, the final transformation system has only been
+ developed in the final part of the research, leaving no more time
+ for verifying these properties. In fact, it is likely that the
+ current transformation system still violates some of these
+ properties in some cases and should be improved (or extra conditions
+ on the input hardware descriptions should be formulated).
+
+ This is most likely the case with the completeness and determinism
+ properties, perhaps als the termination property. The soundness
+ property probably holds, since it is easier to manually verify (each
+ transformation can be reviewed separately).
+
+ Even though no complete proofs have been made, some ideas for
+ possible proof strategies are shown below.
+
+ \subsection{Graph representation}
+ Before looking into how to prove these properties, we'll look at
+ transformation systems from a graph perspective. We will first define
+ the graph view and then illustrate it using a simple example from lambda
+ calculus (which is a different system than the Cλash normalization
+ system). The nodes of the graph are all possible Core expressions. The
+ (directed) edges of the graph are transformations. When a transformation
+ α applies to an expression \lam{A} to produce an expression \lam{B}, we
+ add an edge from the node for \lam{A} to the node for \lam{B}, labeled
+ α.
+
+ \startuseMPgraphic{TransformGraph}
+ save a, b, c, d;
+
+ % Nodes
+ newCircle.a(btex \lam{(λx.λy. (+) x y) 1} etex);
+ newCircle.b(btex \lam{λy. (+) 1 y} etex);
+ newCircle.c(btex \lam{(λx.(+) x) 1} etex);
+ newCircle.d(btex \lam{(+) 1} etex);
+
+ b.c = origin;
+ c.c = b.c + (4cm, 0cm);
+ a.c = midpoint(b.c, c.c) + (0cm, 4cm);
+ d.c = midpoint(b.c, c.c) - (0cm, 3cm);
+
+ % β-conversion between a and b
+ ncarc.a(a)(b) "name(bred)";
+ ObjLabel.a(btex $\xrightarrow[normal]{}{β}$ etex) "labpathname(bred)", "labdir(rt)";
+ ncarc.b(b)(a) "name(bexp)", "linestyle(dashed withdots)";
+ ObjLabel.b(btex $\xleftarrow[normal]{}{β}$ etex) "labpathname(bexp)", "labdir(lft)";
+
+ % η-conversion between a and c
+ ncarc.a(a)(c) "name(ered)";
+ ObjLabel.a(btex $\xrightarrow[normal]{}{η}$ etex) "labpathname(ered)", "labdir(rt)";
+ ncarc.c(c)(a) "name(eexp)", "linestyle(dashed withdots)";
+ ObjLabel.c(btex $\xleftarrow[normal]{}{η}$ etex) "labpathname(eexp)", "labdir(lft)";
+
+ % η-conversion between b and d
+ ncarc.b(b)(d) "name(ered)";
+ ObjLabel.b(btex $\xrightarrow[normal]{}{η}$ etex) "labpathname(ered)", "labdir(rt)";
+ ncarc.d(d)(b) "name(eexp)", "linestyle(dashed withdots)";
+ ObjLabel.d(btex $\xleftarrow[normal]{}{η}$ etex) "labpathname(eexp)", "labdir(lft)";
+
+ % β-conversion between c and d
+ ncarc.c(c)(d) "name(bred)";
+ ObjLabel.c(btex $\xrightarrow[normal]{}{β}$ etex) "labpathname(bred)", "labdir(rt)";
+ ncarc.d(d)(c) "name(bexp)", "linestyle(dashed withdots)";
+ ObjLabel.d(btex $\xleftarrow[normal]{}{β}$ etex) "labpathname(bexp)", "labdir(lft)";
+
+ % Draw objects and lines
+ drawObj(a, b, c, d);
+ \stopuseMPgraphic
+
+ \placeexample[right][ex:TransformGraph]{Partial graph of a lambda calculus
+ system with β and η reduction (solid lines) and expansion (dotted lines).}
+ \boxedgraphic{TransformGraph}
+
+ Of course the graph for Cλash is unbounded, since we can construct an
+ infinite amount of Core expressions. Also, there might potentially be
+ multiple edges between two given nodes (with different labels), though
+ seems unlikely to actually happen in our system.
+
+ See \in{example}[ex:TransformGraph] for the graph representation of a very
+ simple lambda calculus that contains just the expressions \lam{(λx.λy. (+) x
+ y) 1}, \lam{λy. (+) 1 y}, \lam{(λx.(+) x) 1} and \lam{(+) 1}. The
+ transformation system consists of β-reduction and η-reduction (solid edges) or
+ β-expansion and η-expansion (dotted edges).
+
+ \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
+ no transformation applies anymore. We call this set of nodes the \emph{normal
+ set}. The set of nodes containing expressions in intended normal
+ form \refdef{intended normal form} is called the \emph{intended
+ normal set}.
+
+ From such a graph, we can derive some properties easily:
+ \startitemize[KR]
+ \item A system will \emph{terminate} if there is no path of infinite length
+ in the graph (this includes cycles, but can also happen without cycles).
+ \item Soundness is not easily represented in the graph.
+ \item A system is \emph{complete} if all of the nodes in the normal set have
+ the intended normal form. The inverse (that all of the nodes outside of
+ the normal set are \emph{not} in the intended normal form) is not
+ strictly required. In other words, our normal set must be a
+ subset of the intended normal form, but they do not need to be
+ the same set.
+ form.
+ \item A system is deterministic if all paths starting at a particular
+ node, which end in a node in the normal set, end at the same node.
+ \stopitemize
+
+ When looking at the \in{example}[ex:TransformGraph], we see that the system
+ terminates for both the reduction and expansion systems (but note that, for
+ expansion, this is only true because we've limited the possible
+ expressions. In comlete lambda calculus, there would be a path from
+ \lam{(λx.λy. (+) x y) 1} to \lam{(λx.λy.(λz.(+) z) x y) 1} to
+ \lam{(λx.λy.(λz.(λq.(+) q) z) x y) 1} etc.)
+
+ If we would consider the system with both expansion and reduction, there
+ would no longer be termination either, since there would be cycles all
+ over the place.
+
+ The reduction and expansion systems have a normal set of containing just
+ \lam{(+) 1} or \lam{(λx.λy. (+) x y) 1} respectively. Since all paths in
+ either system end up in these normal forms, both systems are \emph{complete}.
+ Also, since there is only one node in the normal set, it must obviously be
+ \emph{deterministic} as well.
+
+ \subsection{Termination}
+ In general, proving termination of an arbitrary program is a very
+ hard problem. \todo{Ref about arbitrary termination} Fortunately,
+ we only have to prove termination for our specific transformation
+ system.
+
+ A common approach for these kinds of proofs is to associate a
+ measure with each possible expression in our system. If we can
+ show that each transformation strictly decreases this measure
+ (\ie, the expression transformed to has a lower measure than the
+ expression transformed from). \todo{ref about measure-based
+ termination proofs / analysis}
+
+ A good measure for a system consisting of just β-reduction would
+ be the number of lambda expressions in the expression. Since every
+ application of β-reduction removes a lambda abstraction (and there
+ is always a bounded number of lambda abstractions in every
+ expression) we can easily see that a transformation system with
+ just β-reduction will always terminate.
+
+ For our complete system, this measure would be fairly complex
+ (probably the sum of a lot of things). Since the (conditions on)
+ our transformations are pretty complex, we would need to include
+ both simple things like the number of let expressions as well as
+ more complex things like the number of case expressions that are
+ not yet in normal form.
+
+ No real attempt has been made at finding a suitable measure for
+ our system yet.
+
+ \subsection{Soundness}
+ Soundness is a property that can be proven for each transformation
+ separately. Since our system only runs separate transformations
+ sequentially, if each of our transformations leaves the
+ \emph{meaning} of the expression unchanged, then the entire system
+ will of course leave the meaning unchanged and is thus
+ \emph{sound}.
+
+ The current prototype has only been verified in an ad-hoc fashion
+ by inspecting (the code for) each transformation. A more formal
+ verification would be more appropriate.
+
+ To be able to formally show that each transformation properly
+ preserves the meaning of every expression, we require an exact
+ definition of the \emph{meaning} of every expression, so we can
+ compare them. Currently there seems to be no formal definition of
+ the meaning or semantics of \GHC's core language, only informal
+ descriptions are available.
+
+ It should be possible to have a single formal definition of
+ meaning for Core for both normal Core compilation by \GHC and for
+ our compilation to \VHDL. The main difference seems to be that in
+ hardware every expression is always evaluated, while in software
+ it is only evaluated if needed, but it should be possible to
+ assign a meaning to core expressions that assumes neither.
+
+ Since each of the transformations can be applied to any
+ subexpression as well, there is a constraint on our meaning
+ definition: The meaning of an expression should depend only on the
+ meaning of subexpressions, not on the expressions themselves. For
+ example, the meaning of the application in \lam{f (let x = 4 in
+ x)} should be the same as the meaning of the application in \lam{f
+ 4}, since the argument subexpression has the same meaning (though
+ the actual expression is different).
+
+ \subsection{Completeness}
+ Proving completeness is probably not hard, but it could be a lot
+ of work. We have seen above that to prove completeness, we must
+ show that the normal set of our graph representation is a subset
+ of the intended normal set.
+
+ However, it is hard to systematically generate or reason about the
+ normal set, since it is defined as any nodes to which no
+ transformation applies. To determine this set, each transformation
+ must be considered and when a transformation is added, the entire
+ set should be re-evaluated. This means it is hard to show that
+ each node in the normal set is also in the intended normal set.
+ Reasoning about our intended normal set is easier, since we know
+ how to generate it from its definition. \refdef{intended normal
+ form definition}.
+
+ Fortunately, we can also prove the complement (which is
+ equivalent, since $A \subseteq B \Leftrightarrow \overline{B}
+ \subseteq \overline{A}$): Show that the set of nodes not in
+ intended normal form is a subset of the set of nodes not in normal
+ form. In other words, show that for every expression that is not
+ in intended normal form, that there is at least one transformation
+ that applies to it (since that means it is not in normal form
+ either and since $A \subseteq C \Leftrightarrow \forall x (x \in A
+ \rightarrow x \in C)$).
+
+ By systematically reviewing the entire Core language definition
+ along with the intended normal form definition (both of which have
+ a similar structure), it should be possible to identify all
+ possible (sets of) core expressions that are not in intended
+ normal form and identify a transformation that applies to it.
+
+ This approach is especially useful for proving completeness of our
+ system, since if expressions exist to which none of the
+ transformations apply (\ie if the system is not yet complete), it
+ is immediately clear which expressions these are and adding
+ (or modifying) transformations to fix this should be relatively
+ easy.
+
+ As observed above, applying this approach is a lot of work, since
+ we need to check every (set of) transformation(s) separately.
+
+ \todo{Perhaps do a few steps of the proofs as proof-of-concept}
+
+% vim: set sw=2 sts=2 expandtab:
projects / matthijs / master-project / report.git / blobdiff