X-Git-Url: https://git.stderr.nl/gitweb?p=matthijs%2Fmaster-project%2Freport.git;a=blobdiff_plain;f=Core2Core.tex;h=5df24873befeb7b28d0cf018dfb0924cc3efd85a;hp=1f258d31028dd4466749f542c9523ffabe2df490;hb=32d52cda513c45334ab256c9f42d41ed6938fc48;hpb=204e3063cbdc2825e3f78ae0261dbf30d4cf38e0

diff --git a/Core2Core.tex b/Core2Core.tex
index 1f258d3..5df2487 100644
--- a/Core2Core.tex
+++ b/Core2Core.tex
@@ -60,6 +60,9 @@
 \definetyping[lambda][option=LAM,style=sans]
 \definetype[lam][option=LAM,style=sans]
 
+\installprettytype [TRANS] [TRANS]
+\definetyping[trans][option=TRANS,style=normal,before=,after=]
+
 % An (invisible) frame to hold a lambda expression
 \define[1]\lamframe{
         % Put a frame around lambda expressions, so they can have multiple
@@ -260,26 +263,21 @@ is specified as a number of conditions (above the horizontal line) and a
 number of conclusions (below the horizontal line). The details of using
 this notation are still a bit fuzzy, so comments are welcom.
 
+TODO: Formally describe the "apply to every (sub)expression" in terms of
+rules with full transformations in the conditions.
+
 \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}
-}
+\starttrans
+E                 \lam{E :: * -> *}
+--------------    \lam{E} is not the first argument of an application.
+λx.E x            \lam{E} is not a lambda abstraction.
+                  \lam{x} is a variable that does not occur free in \lam{E}.
+\stoptrans
 
 \startbuffer[from]
 foo = λa -> case a of 
@@ -576,6 +574,17 @@ 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.
 
+\starttrans
+x = E
+~
+x Y0 ... Yi ... Yn                               \lam{Y_i} is not of a runtime representable type
+---------------------------------------------    \lam{Y_i} is not a local variable reference
+x' = λy0 ... yi-1 f0 ... fm yi+1 ... yn .        \lam{f0 ... fm} = free local vars of \lam{Y_i}
+      E y0 ... yi-1 Yi yi+1 ... yn   
+~
+x' y0 ... yi-1 f0 ...  fm Yi+1 ... Yn
+\stoptrans
+
 \transform{Argument propagation}
 {
 \lam{x} is a global variable, bound to a user-defined function
@@ -600,6 +609,38 @@ translatable. A user-defined function is any other function.
 TODO: The above definition looks too complicated... Can we find
 something more concise?
 
+\subsection{Cast propagation}
+This transform pushes casts down into the expression as far as possible.
+\subsection{Let recursification}
+This transform makes all lets recursive.
+\subsection{Let simplification}
+This transform makes the result value of all let expressions a simple
+variable reference.
+\subsection{Let flattening}
+This transform turns two nested lets (\lam{let x = (let ... in ...) in
+...}) into a single let.
+\subsection{Simple let binding removal}
+This transforms inlines simple let bindings (\eg a = b).
+\subsection{Function inlining}
+This transform inlines let bindings of a funtion type. TODO: This should
+be generelized to anything that is non representable at runtime, or
+something like that.
+\subsection{Scrutinee simplification}
+This transform ensures that the scrutinee of a case expression is always
+a simple variable reference.
+\subsection{Case binder wildening}
+This transform replaces all binders of a each case alternative with a
+wild binder (\ie, one that is never referred to). This will possibly
+introduce a number of new "selector" case statements, that only select
+one element from an algebraic datatype and bind it to a variable.
+\subsection{Case value simplification}
+This transform simplifies the result value of each case alternative by
+binding the value in a let expression and replacing the value by a
+simple variable reference.
+\subsection{Case removal}
+This transform removes any case statements with a single alternative and
+only wild binders.
+
 \subsection{Example sequence}
 
 This section lists an example expression, with a sequence of transforms