+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.
+
+\startbuffer[NormalComplete]
+ regbank :: Bit
+ -> Word
+ -> State (Word, Word)
+ -> (State (Word, Word), Word)