- 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}
+ 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). This is a slightly different notion of global versus
+ local than what \small{GHC} uses internally, but for our purposes
+ the distinction \GHC\ makes is not useful.
+ \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{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}
+
+ These are functions like \lam{map}, \lam{hwor}, \lam{+} and \lam{length}.
+
+ 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}