Add some more transformations.
[matthijs/master-project/report.git] / Core2Core.tex
index 051ddd6..ae9c189 100644 (file)
 % 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. 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{
@@ -51,7 +70,7 @@
         \framed[offset=0mm,location=middle,strut=no,align=right,frame=off]{#1}
 }
 
-\define[2]\trans{
+\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.
         % 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
@@ -267,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
@@ -358,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
@@ -395,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