+\subsection{Definitions}
+In the following sections, we will be using a number of functions and
+notations, which we will define here.
+
+\subsubsection{Transformations}
+The most important notation is the one for transformation, which looks like
+the following:
+
+\starttrans
+context conditions
+~
+from
+------------------------ expression conditions
+to
+~
+context additions
+\stoptrans
+
+Here, we describe a transformation. The most import parts are \lam{from} and
+\lam{to}, which describe the Core expresssion that should be matched and the
+expression that it should be replaced with. This matching can occur anywhere
+in function that is being normalized, so it applies to any subexpression as
+well.
+
+The \lam{expression conditions} list a number of conditions on the \lam{from}
+expression that must hold for the transformation to apply.
+
+Furthermore, there is some way to look into the environment (\eg, other top
+level bindings). The \lam{context conditions} part specifies any number of
+top level bindings that must be present for the transformation to apply.
+Usually, this lists a top level binding that binds an identfier that is also
+used in the \lam{from} expression, allowing us to "access" the value of a top
+level binding in the \lam{to} expression (\eg, for inlining).
+
+Finally, there is a way to influence the environment. The \lam{context
+additions} part lists any number of new top level bindings that should be
+added.
+
+If there are no \lam{context conditions} or \lam{context additions}, they can
+be left out alltogether, along with the separator \lam{~}.
+
+TODO: Example
+
+\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 local variable is any other
+variable (\eg, variables local to a function, which can be bound by lambda
+abstractions, let expressions and case expressions).
+
+A \emph{hardware representable} type is 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.
+
+A \emph{builtin function} is a function for which a builtin
+hardware translation is available, because its actual definition is not
+translatable. A user-defined function is any other function.
+
+\subsubsection{Functions}
+Here, we define a number of functions that can be used below to concisely
+specify conditions.
+
+\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.
+
+\emph{lvar(expr)} is the inverse of \emph{gvar}; it is true when \emph{expr}
+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.
+
projects / matthijs / master-project / report.git / blobdiff