(\eg \lam{add} or \lam{sub}). For these, a hardcoded \small{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.
-
-\subsubsection{Transformation notation}
+\section{Transformation notation}
To be able to concisely present transformations, we use a specific format to
them. It is a simple format, similar to one used in logic reasoning.
subexpression might open up possibilities to apply the transformation
further up in the expression).
-\subsubsection{Transformation application}
+\subsection{Transformation application}
In this chapter we define a number of transformations, but how will we apply
these? As stated before, our normal form is reached as soon as no
transformation applies anymore. This means our application strategy is to
in a function, not just the top level function. This allows us to keep the
transformation descriptions concise and powerful.
+\subsection{Definitions}
+In the following sections, we will be using a number of functions and
+notations, which we will define here.
+
\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.
+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. Types 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{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
+\refdef{global variable}\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}
+\refdef{local variable}\emph{lvar(expr)} is the complement 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.
-
-\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.
-
-Each of these transforms is meant to be applied to every (sub)expression
-in a program, for as long as it applies. Only when none of the
-transformations can be applied anymore, the program is in normal form (by
-definition). We hope to be able to prove that this form will obey all of the
-constraints defined above, but this has yet to happen (though it seems likely
-that it will).
-
-Each of the transforms will be described informally first, explaining
-the need for and goal of the transform. Then, a formal definition is
-given, using a familiar syntax from the world of logic. Each transform
-is specified as a number of conditions (above the horizontal line) and a
-number of conclusions (below the horizontal line). The details of using
-this notation are still a bit fuzzy, so comments are welcom.
-
-TODO: Formally describe the "apply to every (sub)expression" in terms of
-rules with full transformations in the conditions.
+\refdef{representable}\emph{representable(expr)} or \emph{representable(var)} is true when
+\emph{expr} or \emph{var} is \emph{representable}.
\subsection{Binder uniqueness}
A common problem in transformation systems, is binder uniqueness. When not
either.
\stopitemize
+\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.
+
+Each of these transforms is meant to be applied to every (sub)expression
+in a program, for as long as it applies. Only when none of the
+transformations can be applied anymore, the program is in normal form (by
+definition). We hope to be able to prove that this form will obey all of the
+constraints defined above, but this has yet to happen (though it seems likely
+that it will).
+
+Each of the transforms will be described informally first, explaining
+the need for and goal of the transform. Then, a formal definition is
+given, using a familiar syntax from the world of logic. Each transform
+is specified as a number of conditions (above the horizontal line) and a
+number of conclusions (below the horizontal line). The details of using
+this notation are still a bit fuzzy, so comments are welcom.
+
\subsection{η-abstraction}
This transformation makes sure that all arguments of a function-typed
expression are named, by introducing lambda expressions. When combined with
\transexample{η-abstraction}{from}{to}
-\subsection{Extended β-reduction}
+\subsection{β-reduction}
+β-reduction is a well known transformation from lambda calculus, where it is
+the main reduction step. It reduces applications of labmda abstractions,
+removing both the lambda abstraction and the application.
+
+In our transformation system, this step helps to remove unwanted lambda
+abstractions (basically all but the ones at the top level). Other
+transformations (application propagation, non-representable inlining) make
+sure that most lambda abstractions will eventually be reducable by
+β-reduction.
+
+TODO: Define substitution syntax
+
+\starttrans
+(λx.E) M
+-----------------
+E[M/x]
+\stoptrans
+
+% And an example
+\startbuffer[from]
+(λa. 2 * a) (2 * b)
+\stopbuffer
+
+\startbuffer[to]
+2 * (2 * b)
+\stopbuffer
+
+\transexample{β-reduction}{from}{to}
+
+\subsection{Application propagation}
This transformation is meant to propagate application expressions downwards
-into expressions as far as possible. In lambda calculus, this reduction
-is known as β-reduction, but it is of course only defined for
-applications of lambda abstractions. We extend this reduction to also
-work for the rest of core (case and let expressions).
+into expressions as far as possible. This allows partial applications inside
+expressions to become fully applied and exposes new transformation
+possibilities for other transformations (like β-reduction).
-For let expressions:
\starttrans
let binds in E) M
-----------------
let binds in E M
\stoptrans
-For case statements:
+% And an example
+\startbuffer[from]
+( let
+ val = 1
+ in
+ add val
+) 3
+\stopbuffer
+
+\startbuffer[to]
+let
+ val = 1
+in
+ add val 3
+\stopbuffer
+
+\transexample{Application propagation for a let expression}{from}{to}
+
\starttrans
(case x of
p1 -> E1
pn -> En M
\stoptrans
-For lambda expressions:
-\starttrans
-(λx.E) M
------------------
-E[M/x]
-\stoptrans
-
% And an example
\startbuffer[from]
-( let a = (case x of
- True -> id
- False -> neg
- ) 1
- b = (let y = 3 in add y) 2
- in
- (λz.add 1 z)
-) 3
+( case x of
+ True -> id
+ False -> neg
+) 1
\stopbuffer
\startbuffer[to]
-let a = case x of
- True -> id 1
- False -> neg 1
- b = let y = 3 in add y 2
-in
- add 1 3
+case x of
+ True -> id 1
+ False -> neg 1
\stopbuffer
-\transexample{Extended β-reduction}{from}{to}
+\transexample{Application propagation for a case expression}{from}{to}
\subsection{Let derecursification}
This transformation is meant to make lets non-recursive whenever possible.
Note that this transformation does not try to be smart when faced with
recursive lets, it will just leave the lets recursive (possibly joining a
recursive and non-recursive let into a single recursive let). The let
-rederursification transformation will do this instead.
+rederecursification transformation will do this instead.
\starttrans
letnonrec x = (let bindings in M) in N
projects / matthijs / master-project / report.git / blobdiff