Add and improve some transformations.

diff --git a/Core2Core.tex b/Core2Core.tex
index 051ddd6c12120cb5d216834d34583476cc5d2377..384c84d970e67cc232c2c0fd48b0eb2e2c31efe4 100644 (file)
--- a/Core2Core.tex
+++ b/Core2Core.tex
@@ -28,6 +28,15 @@
 % A transformation
 \definefloat[transformation][transformations]
 \define[2]\transform{
 % 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
   %\placetransformation[here]{#1}
   \startframedtext[width=\textwidth]
   \startformula \startalign


@@ -40,6 +49,7 @@
 \installprettytype [LAM] [LAM]
 
 \definetyping[lambda][option=LAM,style=sans]
 \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{
 
 % An (invisible) frame to hold a lambda expression
 \define[1]\lamframe{


@@ -51,7 +61,7 @@
         \framed[offset=0mm,location=middle,strut=no,align=right,frame=off]{#1}
 }
 
         \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.
         % 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.


@@ -67,6 +77,15 @@
         % Reset the typing settings to their defaults
         \setuptyping[option=none,style=\tttf]
 }
         % 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.
 
 % 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.


@@ -74,7 +93,14 @@
 % 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.
 % 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]
 
 % A transformation example
 \definefloat[example][examples]


@@ -89,11 +115,11 @@
 }
 
 \define[3]\transexampleh{
 }
 
 \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
 }
 
 % Define a custom description format for the builtinexprs below


@@ -267,87 +293,94 @@ canonical form.
                 \c d -> op' d c
 \stoptyping
 
                 \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]
 
 \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
 \stopbuffer

+

 \startbuffer[to]
 \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
 
 \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
 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]
 
 \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
 \stopbuffer

+

 \startbuffer[to]
 \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
 
 \stopbuffer
 

-\transexampleh{Application propagation example}{from}{to}
+\transexample{Extended β-reduction}{from}{to}

 
 \subsection{Introducing main scope}
 This transformation is meant to introduce a single let expression that will be
 
 \subsection{Introducing main scope}
 This transformation is meant to introduce a single let expression that will be


@@ -358,7 +391,7 @@ this identifier (to comply with requirement \in[retexpr]).
 
 Formally, we can describe the transformation as follows.
 
 
 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
 {
 \NC \app{transform}{\expr{\bind{f}{expr}}} \NC = \expr{\bind{f}{\app{transform'(expr)}}}\NR
 \NR


@@ -395,7 +428,7 @@ expressions only (so simplify deeply nested expressions).
 
 Formally, we can describe the transformation as follows.
 
 
 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
 \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