From 204e3063cbdc2825e3f78ae0261dbf30d4cf38e0 Mon Sep 17 00:00:00 2001 From: Matthijs Kooijman Date: Wed, 1 Jul 2009 16:51:35 +0200 Subject: [PATCH 1/1] Update and/or remove older text. --- Core2Core.tex | 248 ++++++++++---------------------------------------- 1 file changed, 48 insertions(+), 200 deletions(-) diff --git a/Core2Core.tex b/Core2Core.tex index ae9c189..1f258d3 100644 --- a/Core2Core.tex +++ b/Core2Core.tex @@ -140,42 +140,31 @@ Matthijs Kooijman \section{Introduction} As a new approach to translating Core to VHDL, we investigate a number of -transformations on our Core program, which should bring the program into a -well-defined "canonical" form, which is subsequently trivial to translate to -VHDL. - -The transformations as presented here are far from complete, but are meant as -an exploration of possible transformations. In the running example below, we -apply each of the transformations exactly once, in sequence. As will be -apparent from the end result, there will be additional transformations needed -to fully reach our goal, and some transformations must be applied more than -once. How exactly to (efficiently) do this, has not been investigated. - -Lastly, I hope to be able to state a number of pre- and postconditions for -each transformation. If these can be proven for each transformation, and it -can be shown that there exists some ordering of transformations for which the -postcondition implies the canonical form, we can show that the transformations -do indeed transform any program (probably satisfying a number of -preconditions) to the canonical form. +transforms on our Core program, which should bring the program into a +well-defined {\em normal} form, which is subsequently trivial to +translate to VHDL. + +The transforms as presented here are far from complete, but are meant as +an exploration of possible transformations. \section{Goal} The transformations described here have a well-defined goal: To bring the program in a well-defined form that is directly translatable to hardware, while fully preserving the semantics of the program. -This {\em canonical form} is again a Core program, but with a very specific -structure. A function in canonical form has nested lambda's at the top, which +This {\em normal form} is again a Core program, but with a very specific +structure. A function in normal form has nested lambda's at the top, which produce a let expression. This let expression binds every function application -in the function and produces either a simple identifier or a tuple of -identifiers. Every bound value in the let expression is either a simple -function application or a case expression to extract a single element from a -tuple returned by a function. +in the function and produces a simple identifier. Every bound value in +the let expression is either a simple function application or a case +expression to extract a single element from a tuple returned by a +function. An example of a program in canonical form would be: -\starttyping +\startlambda -- All arguments are an inital lambda - \x c d -> + λx.λc.λd. -- There is one let expression at the top level let -- Calling some other user-defined function. @@ -196,29 +185,21 @@ An example of a program in canonical form would be: in -- The actual result r -\stoptyping - -In this and all following programs, the following definitions are assumed to -be available: - -\starttyping -data Bit = Low | High - -foo :: Int -> (Bit, Bit) -add :: Int -> Int -> Int -sub :: Int -> Int -> Int -\stoptyping +\stoplambda When looking at such a program from a hardware perspective, the top level -lambda's define the input ports. The value produced by the let expression are -the output ports. Each function application bound by the let expression -defines a component instantiation, where the input and output ports are mapped -to local signals or arguments. The tuple extracting case expressions don't map -to - -\subsection{Canonical form definition} -Formally, the canonical form is a core program obeying the following -constraints. +lambda's define the input ports. The value produced by the let expression is +the output port. Most function applications bound by the let expression +define a component instantiation, where the input and output ports are mapped +to local signals or arguments. Some of the others use a builtin +construction (\eg the \lam{case} statement) or call a builtin function +(\eg \lam{add} or \lam{sub}). For these, a hardcoded VHDL translation is +available. + +\subsection{Normal definition} +Formally, the normal form is a core program obeying the following +constraints. TODO: Update this section, this is probably not completely +accurate or relevant anymore. \startitemize[R,inmargin] \item All top level binds must have the form $\expr{\bind{fun}{lamexpr}}$. @@ -260,47 +241,24 @@ be any of $x_0$ to $x_n$. A case expression must have a $hardware\;type$. \item TODO: Many more! \stopitemize -\section{Transformation passes} +\section{Transform passes} -In this section we describe the actual transformations. Here we're using -mostly Core-like notation, with a few notable points. - -\startitemize -\item A core expression (in contrast with a transformation function, for -example), is enclosed in pipes. For example, $\app{transform}{\expr{\lam{z}{z+1}}}$ -is the transform function applied to a lambda core expression. - -Note that this notation might not be consistently applied everywhere. In -particular where a non-core function is used inside a core expression, things -get slightly confusing. -\item A bind is written as $\expr{\bind{x}{expr}}$. This means binding the identifier -$x$ to the expression $expr$. -\item In the core examples, the layout rule from Haskell is loosely applied. -It should be evident what was meant from indentation, even though it might nog -be strictly correct. -\stopitemize +In this section we describe the actual transforms. Here we're using +the core language in a notation that resembles lambda calculus. -\subsection{Example} -In the descriptions of transformations below, the following (slightly -contrived) example program will be used as the running example. Note that this -the example for the canonical form given above is the same program, but in -canonical form. +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 +expressions can be applied anymore, the program is in normal form. 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). -\starttyping - \x -> - let s = foo x - in - case s of - (a, b) -> - case a of - High -> add - Low -> let - op' = case b of - High -> sub - Low -> \c d -> c - in - \c d -> op' d c -\stoptyping +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 @@ -642,124 +600,14 @@ translatable. A user-defined function is any other function. TODO: The above definition looks too complicated... Can we find something more concise? -\subsection{Introducing main scope} -This transformation is meant to introduce a single let expression that will be -the "main scope". This is the let expression as described under requirement -\ref[letexpr]. This let expression will contain only a single binding, which -binds the original expression to some identifier and then evalutes to just -this identifier (to comply with requirement \in[retexpr]). - -Formally, we can describe the transformation as follows. - -\transformold{Main scope introduction} -{ -\NC \app{transform}{\expr{\bind{f}{expr}}} \NC = \expr{\bind{f}{\app{transform'(expr)}}}\NR -\NR -\NC \app{transform'}{\expr{\lam{v}{expr}}} \NC = \expr{\lam{v}{\app{transform'}{expr}}}\NR -\NC \app{transform'}{\expr{expr}} \NC = \expr{\letexpr{\bind{x}{expr}}{x}} \NR -} - -When applying this transformation to our running example, we get the following -program. - -\starttyping - \x c d -> - let r = (let s = foo x - in - case s of - (a, b) -> - case a of - High -> add c d - Low -> let - op' = case b of - High -> sub - Low -> \c d -> c - in - op' d c - ) - in - r -\stoptyping - -\subsection{Scope flattening} -This transformation tries to flatten the topmost let expression in a bind, -{\em i.e.}, bind all identifiers in the same scope, and bind them to simple -expressions only (so simplify deeply nested expressions). - -Formally, we can describe the transformation as follows. - -\transformold{Main scope introduction} { \NC \app{transform}{\expr{\bind{f}{expr}}} \NC = \expr{\bind{f}{\app{transform'(expr)}}}\NR -\NR -\NC \app{transform'}{\expr{\lam{v}{expr}}} \NC = \expr{\lam{v}{\app{transform'}{expr}}}\NR -\NC \app{transform'}{\expr{\letexpr{binds}{expr}}} \NC = \expr{\letexpr{\app{concat . map . flatten}{binds}}{expr}}\NR -\NR -\NC \app{flatten}{\expr{\bind{x}{\letexpr{binds}{expr}}}} \NC = (\app{concat . map . flatten}{binds}) \cup \{\app{flatten}{\expr{\bind{x}{expr}}}\}\NR -\NC \app{flatten}{\expr{\bind{x}{\case{s}{alts}}}} \NC = \app{concat}{binds'} \cup \{\bind{x}{\case{s}{alts'}}\}\NR -\NC \NC \where{(binds', alts')=\app{unzip.map.(flattenalt s)}{alts}}\NR -\NC \app{\app{flattenalt}{s}}{\expr{\alt{\app{con}{x_0\;..\;x_n}}{expr}}} \NC = (extracts \cup \{\app{flatten}{bind}\}, alt)\NR -\NC \NC \where{extracts =\{\expr{\case{s}{\alt{\app{con}{x_0\;..\;x_n}}{x_0}}},}\NR -\NC \NC \;..\;,\expr{\case{s}{\alt{\app{con}{x_0\;..\;x_n}}{x_n}}}\} \NR -\NC \NC bind = \expr{\bind{y}{expr}}\NR -\NC \NC alt = \expr{\alt{\app{con}{\_\;..\;\_}}{y}}\NR -} - -When applying this transformation to our running example, we get the following -program. - -\starttyping - \x c d -> - let s = foo x - r = case s of - (_, _) -> y - a = case s of (a, b) -> a - b = case s of (a, b) -> b - y = case a of - High -> g - Low -> h - g = add c d - h = op' d c - op' = case b of - High -> i - Low -> j - i = sub - j = \c d -> c - in - r -\stoptyping +\subsection{Example sequence} -\subsection{More transformations} -As noted before, the above transformations are not complete. Other needed -transformations include: -\startitemize -\item Inlining of local identifiers with a function type. Since these cannot -be represented in hardware directly, they must be transformed into something -else. Inlining them should always be possible without loss of semantics (TODO: -How true is this?) and can expose new possibilities for other transformations -passes (such as application propagation when inlining {\tt j} above). -\item A variation on inlining local identifiers is the propagation of -function arguments with a function type. This will probably be initiated when -transforming the caller (and not the callee), but it will also deal with -identifiers with a function type that are unrepresentable in hardware. - -Special care must be taken here, since the expression that is propagated into -the callee comes from a different scope. The function typed argument must thus -be replaced by any identifiers from the callers scope that the propagated -expression uses. - -Note that propagating an argument will change both a function's interface and -implementation. For this to work, a new function should be created instead of -modifying the original function, so any other callers will not be broken. -\item Something similar should happen with return values with function types. -\item Polymorphism must be removed from all user-defined functions. This is -again similar to propagation function typed arguments, since this will also -create duplicates of functions (for a specific type). This is an operation -that is commonly known as "specialization" and already happens in GHC (since -non-polymorph functions can be a lot faster than generic ones). -\item More builtin expressions should be added and these should be evaluated -by the compiler. For example, map, fold, +. -\stopitemize +This section lists an example expression, with a sequence of transforms +applied to it. The exact transforms given here probably don't exactly +match the transforms given above anymore, but perhaps this can clarify +the big picture a bit. -Initial example +TODO: Update or remove this section. \startlambda λx. -- 2.30.2