Restructure the introduction of the Normalization chapter.
authorMatthijs Kooijman <matthijs@stdin.nl>
Mon, 5 Oct 2009 12:17:07 +0000 (14:17 +0200)
committerMatthijs Kooijman <matthijs@stdin.nl>
Mon, 5 Oct 2009 12:17:07 +0000 (14:17 +0200)
It now builds up to the formal definition using smaller examples, which
should make the chapter more easy to understand.

Chapters/Normalization.tex

index 4b3a08c821404729476f02aefdba5af96c0c1585..f64f7909aab0fbedf59e4d5c5a0c7d2777a5f927 100644 (file)
@@ -45,24 +45,58 @@ interpretation.
 TODO: Describe core properties not supported in VHDL, and describe how the
 VHDL we want to generate should look like.
 
-\section{Goal}
+\section{Normal form}
 The transformations described here have a well-defined goal: To bring the
 program in a well-defined form that is directly translatable to hardware,
-while fully preserving the semantics of the program.
-
-This {\em normal form} is again a Core program, but with a very specific
-structure. A function in normal form has nested lambda's at the top, which
-produce a number of nested let expressions. These let expressions binds a
-number of simple expressions in the function and produces a simple identifier.
-Every bound value in the let expression is either a simple function
-application, a case expression to extract a single element from a tuple
-returned by a function or a case expression to choose between two signals
-based on some other signal.
-
-This structure is easy to translate to VHDL, since each top level lambda will
-be an input port, every bound value will become a concurrent statement (such
-as a component instantiation or conditional signal assignment) and the result
-variable will become the output port.
+while fully preserving the semantics of the program. We refer to this form as
+the \emph{normal form} of the program. The formal definition of this normal
+form is quite simple:
+
+\placedefinition{}{A program is in \emph{normal form} if none of the
+transformations from this chapter apply.}
+
+Of course, this is an \quote{easy} definition of the normal form, since our
+program will end up in normal form automatically. The more interesting part is
+to see if this normal form actually has the properties we would like it to
+have.
+
+But, before getting into more definitions and details about this normal form,
+let's try to get a feeling for it first. The easiest way to do this is by
+describing the things we want to not have in a normal form.
+
+\startitemize
+  \item Any \emph{polymorphism} must be removed. When laying down hardware, we
+  can't generate any signals that can have multiple types. All types must be
+  completely known to generate hardware.
+  
+  \item Any \emph{higher order} constructions must be removed. We can't
+  generate a hardware signal that contains a function, so all values,
+  arguments and returns values used must be first order.
+
+  \item Any complex \emph{nested scopes} must be removed. In the 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 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
@@ -104,19 +138,35 @@ alu = λa.λb.λc.
   ncline(add)(sum);
 \stopuseMPgraphic
 
-\placeexample[ex:MulSum]{\small{ALU} described in normal form}
+\placeexample[here][ex:MulSum]{Simple architecture consisting of an adder and a
+subtractor.}
   \startcombination[2*1]
-    {\typebufferlam{MulSum}}{Description in normal form}
-    {\boxedgraphic{MulSum}}{Described architecture}
+    {\typebufferlam{MulSum}}{Core description in normal form.}
+    {\boxedgraphic{MulSum}}{The architecture described by the normal form.}
   \stopcombination
 
+The previous example described composing an architecture by calling other
+functions (operators), resulting in a simple architecture with component and
+connection. There is of course also some mechanism for choice in the normal
+form. In a normal Core program, the \emph{case} expression can be used in a
+few different ways to describe choice. In normal form, this is limited to a
+very specific form.
+
+\in{Example}[ex:AddSubAlu] shows an example describing a
+simple \small{ALU}, which chooses between two operations based on an opcode
+bit. The main structure is the same as in \in{example}[ex:MulSum], but this
+time the \lam{res} variable is bound to a case expression. This case
+expression scrutinizes the variable \lam{opcode} (and scrutinizing more
+complex expressions is not supported). The case expression can select a
+different variable based on the constructor of \lam{opcode}.
+
 \startbuffer[AddSubAlu]
 alu :: Bit -> Word -> Word -> Word
 alu = λopcode.λa.λb.
     let
       res1 = (+) a b
       res2 = (-) a b
-      res = case op of
+      res = case opcode of
         Low -> res1
         High -> res2
     in
@@ -157,18 +207,28 @@ alu = λopcode.λa.λb.
   ncline(mux)(res) "posA(out)";
 \stopuseMPgraphic
 
-\placeexample[ex:AddSubAlu]{\small{ALU} described in normal form}
+\placeexample[here][ex:AddSubAlu]{Simple \small{ALU} supporting two operations.}
   \startcombination[2*1]
-    {\typebufferlam{AddSubAlu}}{Description in normal form}
-    {\boxedgraphic{AddSubAlu}}{Described architecture}
+    {\typebufferlam{AddSubAlu}}{Core description in normal form.}
+    {\boxedgraphic{AddSubAlu}}{The architecture described by the normal form.}
   \stopcombination
 
-\startlambda
+As a more complete example, consider \in{example}[ex:NormalComplete]. This
+example contains everything that is supported in normal form, with the
+exception of builtin higher order functions.
+
+\startbuffer[NormalComplete]
+  regbank :: Bit 
+             -> Word 
+             -> State (Word, Word) 
+             -> (State (Word, Word), Word)
+
   -- All arguments are an inital lambda
-  λa.λd.λsp.
+  regbank = λa.λd.λsp.
   -- There are nested let expressions at top level
   let
-    -- Unpack the state by coercion
+    -- Unpack the state by coercion (\eg, cast from
+    -- State (Word, Word) to (Word, Word))
     s = sp :: (Word, Word)
     -- Extract both registers from the state
     r1 = case s of (fst, snd) -> fst
@@ -180,22 +240,133 @@ alu = λopcode.λa.λb.
       High -> r1
       Low -> r2
     r1' = case a of
-      High -> d
+      High -> d'
       Low -> r1
     r2' = case a of
       High -> r2
-      Low -> d
+      Low -> d'
     -- Packing a tuple
     s' = (,) r1' r2'
-    -- Packing the state by coercion
+    -- pack the state by coercion (\eg, cast from
+    -- (Word, Word) to State (Word, Word))
     sp' = s' :: State (Word, Word)
     -- Pack our return value
     res = (,) sp' out
   in
     -- The actual result
     res
+\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{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 VHDL translation is
+available.
+
 \subsection{Definitions}
 In the following sections, we will be using a number of functions and
 notations, which we will define here.
@@ -267,60 +438,6 @@ references a local variable, false when it references a global variable.
 \emph{representable(expr)} or \emph{representable(var)} is true when
 \emph{expr} or \emph{var} has a type that is representable at runtime.
 
-\subsection{Normal form definition}
-We can describe this normal form in a slightly more formal manner. The
-following EBNF-like description completely captures the intended structure
-(and generates a subset of GHC's core format).
-
-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 VHDL translation is
-available.
-
 \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.