author Matthijs Kooijman Fri, 9 Oct 2009 09:15:13 +0000 (11:15 +0200) committer Matthijs Kooijman Fri, 9 Oct 2009 09:17:21 +0000 (11:17 +0200)

index 78854ac..445c323 100644 (file)
@@ -373,11 +373,7 @@ construction (\eg the \lam{case} statement) or call a builtin function
(\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.

@@ -588,7 +584,7 @@ alu = λopcode.λa.b. (case opcode of
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
@@ -604,6 +600,10 @@ When applying a single transformation, we try to apply it to every (sub)expressi
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
@@ -632,27 +632,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.

-\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.
-
\subsection{Binder uniqueness}
A common problem in transformation systems, is binder uniqueness. When not
considering this problem, it is easy to create transformations that mix up
@@ -747,6 +726,24 @@ binders is already unique, there is no way to introduce (incorrect) shadowing
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