Restructure the section structure of the Normalization chapter.

diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex
index 78854ac586e8901bf730287417294e3479a8a094..445c32389ad91ccd8f874ddbd49ebb8f7fa71682 100644 (file)
--- a/Chapters/Normalization.tex
+++ b/Chapters/Normalization.tex
@@ -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