\mainlanguage [en]
\setuppapersize[A4][A4]
-\setupbodyfont[10pt]
-%\usetypescript [lbr][ec]
-%\switchtotypeface [lbr] [10pt]
+% Define a custom typescript. We could also have put the \definetypeface's
+% directly in the script, without a typescript, but I guess this is more
+% elegant...
+\starttypescript[Custom]
+% This is a sans font that supports greek symbols
+\definetypeface [Custom] [ss] [sans] [iwona] [default]
+\definetypeface [Custom] [rm] [serif] [antykwa-torunska] [default]
+\definetypeface [Custom] [tt] [mono] [modern] [default]
+\definetypeface [Custom] [mm] [math] [modern] [default]
+\stoptypescript
+\usetypescript [Custom]
+
+% Use our custom typeface
+\switchtotypeface [Custom] [10pt]
% The function application operator, which expands to a space in math mode
\define[1]\expr{|#1|}
% A transformation
\definefloat[transformation][transformations]
\define[2]\transform{
+ \startframedtext[width=\textwidth]
+ #2
+ \stopframedtext
+}
+
+\define\conclusion{\blackrule[height=0.5pt,depth=0pt,width=.5\textwidth]}
+\define\nextrule{\vskip1cm}
+
+\define[2]\transformold{
%\placetransformation[here]{#1}
\startframedtext[width=\textwidth]
\startformula \startalign
\stopframedtext
}
+% A shortcut for italicized e.g.
+\define[0]\eg{{\em e.g.}}
+
+% Install the lambda calculus pretty-printer, as defined in pret-lam.lua.
+\installprettytype [LAM] [LAM]
+
+\definetyping[lambda][option=LAM,style=sans]
+\definetype[lam][option=LAM,style=sans]
+
+% An (invisible) frame to hold a lambda expression
+\define[1]\lamframe{
+ % Put a frame around lambda expressions, so they can have multiple
+ % lines and still appear inline.
+ % The align=right option really does left-alignment, but without the
+ % program will end up on a single line. The strut=no option prevents a
+ % bunch of empty space at the start of the frame.
+ \framed[offset=0mm,location=middle,strut=no,align=right,frame=off]{#1}
+}
+
+\define[2]\transbuf{
+ % Make \typebuffer uses the LAM pretty printer and a sans-serif font
+ % Also prevent any extra spacing above and below caused by the default
+ % before=\blank and after=\blank.
+ \setuptyping[option=LAM,style=sans,before=,after=]
+ % Prevent the arrow from ending up below the first frame (a \framed
+ % at the start of a line defaults to using vmode).
+ \dontleavehmode
+ % Put the elements in frames, so they can have multiple lines and be
+ % middle-aligned
+ \lamframe{\typebuffer[#1]}
+ \lamframe{\Rightarrow}
+ \lamframe{\typebuffer[#2]}
+ % Reset the typing settings to their defaults
+ \setuptyping[option=none,style=\tttf]
+}
+% This is the same as \transbuf above, but it accepts text directly instead
+% of through buffers. This only works for single lines, however.
+\define[2]\trans{
+ \dontleavehmode
+ \lamframe{\lam{#1}}
+ \lamframe{\Rightarrow}
+ \lamframe{\lam{#2}}
+}
+
+
% A helper to print a single example in the half the page width. The example
% text should be in a buffer whose name is given in an argument.
%
% The align=right option really does left-alignment, but without the program
% will end up on a single line. The strut=no option prevents a bunch of empty
% space at the start of the frame.
-\define[1]\example{\framed[frameoffset=2mm,align=right,strut=no]{\typebuffer[#1]}}
+\define[1]\example{
+ \framed[offset=1mm,align=right,strut=no]{
+ \setuptyping[option=LAM,style=sans,before=,after=]
+ \typebuffer[#1]
+ \setuptyping[option=none,style=\tttf]
+ }
+}
+
% A transformation example
\definefloat[example][examples]
}
\define[3]\transexampleh{
- \placeexample[here]{#1}
- \startcombination[1*2]
- {\example{#2}}{Original program}
- {\example{#3}}{Transformed program}
- \stopcombination
+% \placeexample[here]{#1}
+% \startcombination[1*2]
+% {\example{#2}}{Original program}
+% {\example{#3}}{Transformed program}
+% \stopcombination
}
% Define a custom description format for the builtinexprs below
\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" state, which is subsequently trivial to translate to
+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
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 postconditinos for
+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 ther exists some ordering of transformations for which the
+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.
\section{Goal}
The transformations described here have a well-defined goal: To bring the
-program in a well-defined program that is directly translatable to hardware,
+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
\starttyping
\x ->
let s = foo x
- in
- case s of
- (a, b) ->
- r = case a of
- High -> add
- Low -> let
- op' = case b of
- High -> sub
- Low -> \c d -> c
- in
- \c d -> op' d c
-\stoptyping
-
-\subsection{Argument extraction}
-This transformation makes sure that all of a bindings arguments are always
-bound to variables at the top level of the bound value. Formally, we can
-describe this transformation as follows.
-
-\transform{Argument extraction}
-{
-\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 :: a \xrightarrow b}} \NC = \expr{\lam{x}{\app{transform'}{\expr{(\app{expr}{x})}}}} \NR
-}
-
-When applying this transformation to our running example, we get the following
-program.
-
-\starttyping
- \x c d ->
- (let s = foo x
in
case s of
(a, b) ->
Low -> \c d -> c
in
\c d -> op' d c
- ) c d
\stoptyping
+\subsection{η-abstraction}
+This transformation makes sure that all arguments of a function-typed
+expression are named, by introducing lambda expressions. When combined with
+β-reduction and function inlining below, all function-typed expressions should
+be lambda abstractions or global identifiers.
+
+\transform{η-abstraction}
+{
+\lam{E :: * -> *}
+
+\lam{E} is not the first argument of an application.
+
+\lam{E} is not a lambda abstraction.
+
+\lam{x} is a variable that does not occur free in E.
+
+\conclusion
+
+\trans{E}{λx.E x}
+}
+
\startbuffer[from]
-foo = \x -> case x of True -> (\y -> mul y y); False -> id
+foo = λa -> case a of
+ True -> λb.mul b b
+ False -> id
\stopbuffer
+
\startbuffer[to]
-foo = \x z -> (case x of True -> (\y -> mul y y); False -> id) z
+foo = λa.λx -> (case a of
+ True -> λb.mul b b
+ False -> λy.id y) x
\stopbuffer
-\transexampleh{Argument extraction example}{from}{to}
+\transexample{η-abstraction}{from}{to}
-\subsection{Application propagation}
+\subsection{Extended β-reduction}
This transformation is meant to propagate application expressions downwards
-into expressions as far as possible. Formally, we can describe this
-transformation as follows.
+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).
+\startbuffer[from]
+(case x of
+ p1 -> E1
+ \vdots
+ pn -> En) M
+\stopbuffer
+\startbuffer[to]
+case x of
+ p1 -> E1 M
+ \vdots
+ pn -> En M
+\stopbuffer
-\transform{Application propagation}
+\transform{Extended β-reduction}
{
-\NC \app{transform}{\expr{\app{(\letexpr{binds}{expr})}{y}}} \NC = \expr{\letexpr{binds}{(\app{expr}{y})}}\NR
-\NC \app{transform}{\expr{\app{(\lam{x}{expr})}{y}}} \NC = \app{\app{subs}{x \xRightarrow y}}{\expr{expr}}\NR
-\NC \app{transform}{\expr{\app{(\case{x}{\alt{p}{e};...})}{y}}} \NC = \expr{\case{x}{\alt{p}{\app{e}{y}};...}}\;(for\;every\;alt)\NR
-}
+\conclusion
+\trans{(λx.E) M}{E[M/x]}
-When applying this transformation to our running example, we get the following
-program.
+\nextrule
+\conclusion
+\trans{(let binds in E) M}{let binds in E M}
-\starttyping
- \x c d ->
- 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
-\stoptyping
+\nextrule
+\conclusion
+\transbuf{from}{to}
+}
\startbuffer[from]
-foo = \x z -> (case x of True -> (\y -> mul y y); False -> id) z
+let a = (case x of
+ True -> id
+ False -> neg
+ ) 1
+ b = (let y = 3 in add y) 2
+in
+ (λz.add 1 z) 3
\stopbuffer
+
\startbuffer[to]
-foo = \x z -> case x of True -> mul z z; False -> id z
+let a = case x of
+ True -> id 1
+ False -> neg 1
+ b = let y = 3 in add y 2
+in
+ add 1 3
\stopbuffer
-\transexampleh{Application propagation example}{from}{to}
+\transexample{Extended β-reduction}{from}{to}
+
+\subsection{Argument simplification}
+The transforms in this section deal with simplifying application
+arguments into normal form. The goal here is to:
+
+\startitemize
+ \item Make all arguments of user-defined functions (\eg, of which
+ we have a function body) simple variable references of a runtime
+ representable type.
+ \item Make all arguments of builtin functions either:
+ \startitemize
+ \item A type argument.
+ \item A dictionary argument.
+ \item A type level expression.
+ \item A variable reference of a runtime representable type.
+ \item A variable reference or partial application of a function type.
+ \stopitemize
+\stopitemize
+
+\subsubsection{User-defined functions}
+We can divide the arguments of a user-defined function into two
+categories:
+\startitemize
+ \item Runtime representable typed arguments (\eg bits or vectors).
+ \item Non-runtime representable typed arguments.
+\stopitemize
+
+The next two transformations will deal with each of these two kinds of argument respectively.
+
+\subsubsubsection{Argument extraction}
+This transform deals with arguments to user-defined functions that
+are of a runtime representable type. These arguments can be preserved in
+the program, since they can be translated to input ports later on.
+However, since we can only connect signals to input ports, these
+arguments must be reduced to simple variables (for which signals will be
+produced).
+
+TODO: It seems we can map an expression to a port, not only a signal.
+Perhaps this makes this transformation not needed?
+TODO: Say something about dataconstructors (without arguments, like True
+or False), which are variable references of a runtime representable
+type, but do not result in a signal.
+
+To reduce a complex expression to a simple variable reference, we create
+a new let expression around the application, which binds the complex
+expression to a new variable. The original function is then applied to
+this variable.
+
+\transform{Argument extract}
+{
+\lam{X} is a (partial application of) a user-defined function
+
+\lam{Y} is of a hardware representable type
+
+\lam{Y} is not a variable referene
+
+\conclusion
+
+\trans{X Y}{let z = Y in X z}
+}
+\subsubsubsection{Argument propagation}
+This transform deals with arguments to user-defined functions that are
+not representable at runtime. This means these arguments cannot be
+preserved in the final form and most be {\em propagated}.
+
+Propagation means to create a specialized version of the called
+function, with the propagated argument already filled in. As a simple
+example, in the following program:
+
+\startlambda
+f = λa.λb.a + b
+inc = λa.f a 1
+\stoplambda
+
+we could {\em propagate} the constant argument 1, with the following
+result:
+
+\startlambda
+f' = λa.a + 1
+inc = λa.f' a
+\stoplambda
+
+Special care must be taken when the to-be-propagated expression has any
+free variables. If this is the case, the original argument should not be
+removed alltogether, but replaced by all the free variables of the
+expression. In this way, the original expression can still be evaluated
+inside the new function. Also, this brings us closer to our goal: All
+these free variables will be simple variable references.
+
+To prevent us from propagating the same argument over and over, a simple
+local variable reference is not propagated (since is has exactly one
+free variable, itself, we would only replace that argument with itself).
+
+This shows that any free local variables that are not runtime representable
+cannot be brought into normal form by this transform. We rely on an
+inlining transformation to replace such a variable with an expression we
+can propagate again.
+
+TODO: Move these definitions somewhere sensible.
+
+Definition: A global variable is any variable that is bound at the
+top level of a program. A local variable is any other variable.
+
+Definition: A 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.
+
+Definition: A 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.
+
+\transform{Argument propagation}
+{
+\lam{x} is a global variable, bound to a user-defined function
+
+\lam{x = E}
+
+\lam{Y_i} is not of a runtime representable type
+
+\lam{Y_i} is not a local variable reference
+
+\conclusion
+
+\lam{f0 ... fm} = free local vars of \lam{Y_i}
+
+\lam{x'} is a new global variable
+
+\lam{x' = λy0 ... yi-1 f0 ... fm yi+1 ... yn . E y0 ... yi-1 Yi yi+1 ... yn}
+
+\trans{x Y0 ... Yi ... Yn}{x' y0 ... yi-1 f0 ... fm Yi+1 ... Yn}
+}
+
+TODO: The above definition looks too complicated... Can we find
+something more concise?
+
+\subsubsection{Builtin functions}
+
+argument categories:
+
+function typed
+
+type / dictionary / other
+
+hardware representable
+
+TODO
\subsection{Introducing main scope}
This transformation is meant to introduce a single let expression that will be
Formally, we can describe the transformation as follows.
-\transform{Main scope introduction}
+\transformold{Main scope introduction}
{
\NC \app{transform}{\expr{\bind{f}{expr}}} \NC = \expr{\bind{f}{\app{transform'(expr)}}}\NR
\NR
Formally, we can describe the transformation as follows.
-\transform{Main scope introduction} { \NC \app{transform}{\expr{\bind{f}{expr}}} \NC = \expr{\bind{f}{\app{transform'(expr)}}}\NR
+\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
\item More builtin expressions should be added and these should be evaluated
by the compiler. For example, map, fold, +.
\stopitemize
+
+Initial example
+
+\startlambda
+ λ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
+\stoplambda
+
+After top-level η-abstraction:
+
+\startlambda
+ λx.λc.λd.
+ (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
+ ) c d
+\stoplambda
+
+After (extended) β-reduction:
+
+\startlambda
+ λx.λc.λd.
+ 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
+\stoplambda
+
+After return value extraction:
+
+\startlambda
+ λx.λc.λd.
+ let s = foo x
+ r = 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
+\stoplambda
+
+Scrutinee simplification does not apply.
+
+After case binder wildening:
+
+\startlambda
+ λx.λc.λd.
+ let s = foo x
+ a = case s of (a, _) -> a
+ b = case s of (_, b) -> b
+ r = case s of (_, _) ->
+ 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
+\stoplambda
+
+After case value simplification
+
+\startlambda
+ λx.λc.λd.
+ let s = foo x
+ a = case s of (a, _) -> a
+ b = case s of (_, b) -> b
+ r = case s of (_, _) -> r'
+ rh = add c d
+ rl = let rll = λc.λd.c
+ op' = case b of
+ High -> sub
+ Low -> rll
+ in
+ op' d c
+ r' = case a of
+ High -> rh
+ Low -> rl
+ in
+ r
+\stoplambda
+
+After let flattening:
+
+\startlambda
+ λx.λc.λd.
+ let s = foo x
+ a = case s of (a, _) -> a
+ b = case s of (_, b) -> b
+ r = case s of (_, _) -> r'
+ rh = add c d
+ rl = op' d c
+ rll = λc.λd.c
+ op' = case b of
+ High -> sub
+ Low -> rll
+ r' = case a of
+ High -> rh
+ Low -> rl
+ in
+ r
+\stoplambda
+
+After function inlining:
+
+\startlambda
+ λx.λc.λd.
+ let s = foo x
+ a = case s of (a, _) -> a
+ b = case s of (_, b) -> b
+ r = case s of (_, _) -> r'
+ rh = add c d
+ rl = (case b of
+ High -> sub
+ Low -> λc.λd.c) d c
+ r' = case a of
+ High -> rh
+ Low -> rl
+ in
+ r
+\stoplambda
+
+After (extended) β-reduction again:
+
+\startlambda
+ λx.λc.λd.
+ let s = foo x
+ a = case s of (a, _) -> a
+ b = case s of (_, b) -> b
+ r = case s of (_, _) -> r'
+ rh = add c d
+ rl = case b of
+ High -> sub d c
+ Low -> d
+ r' = case a of
+ High -> rh
+ Low -> rl
+ in
+ r
+\stoplambda
+
+After case value simplification again:
+
+\startlambda
+ λx.λc.λd.
+ let s = foo x
+ a = case s of (a, _) -> a
+ b = case s of (_, b) -> b
+ r = case s of (_, _) -> r'
+ rh = add c d
+ rlh = sub d c
+ rl = case b of
+ High -> rlh
+ Low -> d
+ r' = case a of
+ High -> rh
+ Low -> rl
+ in
+ r
+\stoplambda
+
+After case removal:
+
+\startlambda
+ λx.λc.λd.
+ let s = foo x
+ a = case s of (a, _) -> a
+ b = case s of (_, b) -> b
+ r = r'
+ rh = add c d
+ rlh = sub d c
+ rl = case b of
+ High -> rlh
+ Low -> d
+ r' = case a of
+ High -> rh
+ Low -> rl
+ in
+ r
+\stoplambda
+
+After let bind removal:
+
+\startlambda
+ λx.λc.λd.
+ let s = foo x
+ a = case s of (a, _) -> a
+ b = case s of (_, b) -> b
+ rh = add c d
+ rlh = sub d c
+ rl = case b of
+ High -> rlh
+ Low -> d
+ r' = case a of
+ High -> rh
+ Low -> rl
+ in
+ r'
+\stoplambda
+
+Application simplification is not applicable.
\stoptext
projects / matthijs / master-project / report.git / blobdiff