X-Git-Url: https://git.stderr.nl/gitweb?p=matthijs%2Fmaster-project%2Freport.git;a=blobdiff_plain;f=Core2Core.tex;h=17d0ee262be8d02aea5a0639398d0394195d6f81;hp=bc385a68324b210e435dbe1f42cbfed975099f8a;hb=0028507a3d326add5d45d20cfe750ef964d9b3f0;hpb=95b1a682e51c47d635d5bafe75bd7096e8d4ec18

diff --git a/Core2Core.tex b/Core2Core.tex
index bc385a6..17d0ee2 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,65 @@
   \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]
@@ -60,11 +118,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 +296,241 @@ 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
+
+\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
@@ -329,7 +541,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 +578,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 +648,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