{\defref{intended normal form definition}
\typebufferlam{IntendedNormal}}
- When looking at such a program from a hardware perspective, the
- top level lambda abstractions define the input ports. Lambda
- abstractions cannot appear anywhere else. 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
- built-in construction (\eg\ the \lam{case} expression) or call a
- built-in function (\eg\ \lam{+} or \lam{map}). For these, a
- hardcoded \small{VHDL} translation is available.
+ When looking at such a program from a hardware perspective, the top
+ level lambda abstractions (\italic{lambda}) define the input ports.
+ Lambda abstractions cannot appear anywhere else. The variable reference
+ in the body of the recursive let expression (\italic{toplet}) is the
+ output port. Most binders bound by the let expression define a
+ component instantiation (\italic{userapp}), where the input and output
+ ports are mapped to local signals (\italic{userarg}). Some of the others
+ use a built-in construction (\eg\ the \lam{case} expression) or call a
+ built-in function (\italic{builtinapp}) such as \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
dictionaries, functions.
\defref{representable}
- A \emph{built-in 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{built-in function} \defref{user-defined function}
+ A \emph{built-in function} is a function supplied by the Cλash
+ framework, whose implementation is not used to generate \VHDL. This is
+ either because it is no valid Cλash (like most list functions that need
+ recursion) or because a Cλash implementation would be unwanted (for the
+ addition operator, for example, we would rather use the \VHDL addition
+ operator to let the synthesis tool decide what kind of adder to use
+ instead of explicitly describing one in Cλash). \defref{built-in
+ function}
- For these functions, Cλash has a \emph{built-in hardware translation}, so calls
- to these functions can still be translated. These are functions like
- \lam{map}, \lam{hwor} and \lam{length}.
+ These are functions like \lam{map}, \lam{hwor}, \lam{+} and \lam{length}.
- A \emph{user-defined} function is a function for which we do have a Cλash
- implementation available.
+ For these functions, Cλash has a \emph{built-in hardware translation},
+ so calls to these functions can still be translated. Built-in functions
+ must have a valid Haskell implementation, of course, to allow
+ simulation.
+
+ A \emph{user-defined} function is a function for which no built-in
+ translation is available and whose definition will thus need to be
+ translated to Cλash. \defref{user-defined function}
\subsubsection[sec:normalization:predicates]{Predicates}
Here, we define a number of predicates that can be used below to concisely
\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 expressions 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}.
+ In such a graph a node (expression) is in normal form if it has no
+ outgoing edges (meaning no transformation applies to it). The set of
+ nodes without outgoing edges is called the \emph{normal set}. Similarly,
+ 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]