From 35ce834593526d613598a431723cd5be7fe440af Mon Sep 17 00:00:00 2001 From: Matthijs Kooijman Date: Fri, 9 Oct 2009 11:15:13 +0200 Subject: [PATCH] Restructure the section structure of the Normalization chapter. --- Chapters/Normalization.tex | 51 ++++++++++++++++++-------------------- 1 file changed, 24 insertions(+), 27 deletions(-) diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex index 78854ac..445c323 100644 --- 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 -- 2.30.2