From 70ce03a503dc915067321c2b321038ab0ce43586 Mon Sep 17 00:00:00 2001 From: Matthijs Kooijman Date: Tue, 30 Jun 2009 19:38:07 +0200 Subject: [PATCH] Add two transforms for argument simplification. Also, add some text describing why the transforms are neccesary and how they work. --- Core2Core.tex | 150 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 150 insertions(+) diff --git a/Core2Core.tex b/Core2Core.tex index 384c84d..17d0ee2 100644 --- 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 -- 2.30.2