X-Git-Url: https://git.stderr.nl/gitweb?p=matthijs%2Fmaster-project%2Freport.git;a=blobdiff_plain;f=Core2Core.tex;h=ae9c18976ba51daade3248d58c98b835ddba2a42;hp=bc385a68324b210e435dbe1f42cbfed975099f8a;hb=f3d8c0e61d2df140a1c6b83e720629383162e78c;hpb=95b1a682e51c47d635d5bafe75bd7096e8d4ec18 diff --git a/Core2Core.tex b/Core2Core.tex index bc385a6..ae9c189 100644 --- a/Core2Core.tex +++ b/Core2Core.tex @@ -28,6 +28,15 @@ % 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 @@ -36,16 +45,71 @@ \stopframedtext } +% A shortcut for italicized e.g. and i.e. +\define[0]\eg{{\em e.g.}} +\define[0]\ie{{\em i.e.}} + +\definedescription + [desc] + [location=hanging,hang=20,width=broad] + %command=\hskip-1cm,margin=1cm] + % 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] @@ -60,11 +124,11 @@ } \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 @@ -238,87 +302,345 @@ canonical form. \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. +\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{Argument extraction} +\transform{η-abstraction} { -\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 -} +\lam{E :: * -> *} -When applying this transformation to our running example, we get the following -program. +\lam{E} is not the first argument of an application. -\starttyping - \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 -\stoptyping +\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 + +When looking at the arguments of a user-defined function, we can +divide them into two categories: +\startitemize + \item Arguments with a runtime representable type (\eg bits or vectors). + + 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). This is taken care of by the argument extraction + transform. + \item Non-runtime representable typed arguments. + + These arguments cannot be preserved in the program, since we + cannot represent them as input or output ports in the resulting + VHDL. To remove them, we create a specialized version of the + called function with these arguments filled in. This is done by + the argument propagation transform. +\stopitemize + +When looking at the arguments of a builtin function, we can divide them +into categories: + +\startitemize + \item Arguments with a runtime representable type. + + As we have seen with user-defined functions, these arguments can + always be reduced to a simple variable reference, by the + argument extraction transform. Performing this transform for + builtin functions as well, means that the translation of builtin + functions can be limited to signal references, instead of + needing to support all possible expressions. + + \item Arguments with a function type. + + These arguments are functions passed to higher order builtins, + like \lam{map} and \lam{foldl}. Since implementing these + functions for arbitrary function-typed expressions (\eg, lambda + expressions) is rather comlex, we reduce these arguments to + (partial applications of) global functions. + + We can still support arbitrary expressions from the user code, + by creating a new global function containing that expression. + This way, we can simply replace the argument with a reference to + that new function. However, since the expression can contain any + number of free variables we also have to include partial + applications in our normal form. + + This category of arguments is handled by the function extraction + transform. + \item Other unrepresentable arguments. + + These arguments can take a few different forms: + \startdesc{Type arguments} + In the core language, type arguments can only take a single + form: A type wrapped in the Type constructor. Also, there is + nothing that can be done with type expressions, except for + applying functions to them, so we can simply leave type + arguments as they are. + \stopdesc + \startdesc{Dictionary arguments} + In the core language, dictionary arguments are used to find + operations operating on one of the type arguments (mostly for + finding class methods). Since we will not actually evaluatie + the function body for builtin functions and can generate + code for builtin functions by just looking at the type + arguments, these arguments can be ignored and left as they + are. + \stopdesc + \startdesc{Type level arguments} + Sometimes, we want to pass a value to a builtin function, but + we need to know the value at compile time. Additionally, the + value has an impact on the type of the function. This is + encoded using type-level values, where the actual value of the + argument is not important, but the type encodes some integer, + for example. Since the value is not important, the actual form + of the expression does not matter either and we can leave + these arguments as they are. + \stopdesc + \startdesc{Other arguments} + Technically, there is still a wide array of arguments that can + be passed, but does not fall into any of the above categories. + However, none of the supported builtin functions requires such + an argument. This leaves use with passing unsupported types to + a function, such as calling \lam{head} on a list of functions. + + In these cases, it would be impossible to generate hardware + for such a function call anyway, so we can ignore these + arguments. + + The only way to generate hardware for builtin functions with + arguments like these, is to expand the function call into an + equivalent core expression (\eg, expand map into a series of + function applications). But for now, we choose to simply not + support expressions like these. + \stopdesc + + From the above, we can conclude that we can simply ignore these + other unrepresentable arguments and focus on the first two + categories instead. +\stopitemize + +\subsubsection{Argument extraction} +This transform deals with arguments to functions that +are of a runtime representable type. + +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{Y} is of a hardware representable type + +\lam{Y} is not a variable referene + +\conclusion + +\trans{X Y}{let z = Y in X z} +} + +\subsubsection{Function extraction} +This transform deals with function-typed arguments to builtin functions. +Since these arguments cannot be propagated, we choose to extract them +into a new global function instead. + +Any free variables occuring in the extracted arguments will become +parameters to the new global function. The original argument is replaced +with a reference to the new function, applied to any free variables from +the original argument. + +\transform{Function extraction} +{ +\lam{X} is a (partial application of) a builtin function + +\lam{Y} is not an application + +\lam{Y} is not a variable reference + +\conclusion + +\lam{f0 ... fm} = free local vars of \lam{Y} + +\lam{y} is a new global variable + +\lam{y = λf0 ... fn.Y} + +\trans{X Y}{X (y f0 ... fn)} +} + +\subsubsection{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? \subsection{Introducing main scope} This transformation is meant to introduce a single let expression that will be @@ -329,7 +651,7 @@ this identifier (to comply with requirement \in[retexpr]). 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 @@ -366,7 +688,7 @@ expressions only (so simplify deeply nested expressions). 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 @@ -436,4 +758,241 @@ 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 + +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