Add two transforms for argument simplification.

Also, add some text describing why the transforms are neccesary and how
they work.

diff --git a/Core2Core.tex b/Core2Core.tex
index 384c84d970e67cc232c2c0fd48b0eb2e2c31efe4..17d0ee262be8d02aea5a0639398d0394195d6f81 100644 (file)
--- a/Core2Core.tex
+++ b/Core2Core.tex
@@ -45,6 +45,9 @@
   \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]
 
@@ -382,6 +385,153 @@ in
 
 \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
 the "main scope". This is the let expression as described under requirement