Move some more stuff around in the Normalization chapter.
authorMatthijs Kooijman <matthijs@stdin.nl>
Wed, 2 Dec 2009 11:16:47 +0000 (12:16 +0100)
committerMatthijs Kooijman <matthijs@stdin.nl>
Wed, 2 Dec 2009 11:24:58 +0000 (12:24 +0100)
Chapters/Normalization.tex
Outline

index db743fc..d3b3700 100644 (file)
       \defref{intended normal form definition}
       \todo{Fix indentation}
       \startlambda
-      \italic{normal} = \italic{lambda}
-      \italic{lambda} = λvar.\italic{lambda} (representable(var))
+      \italic{normal} := \italic{lambda}
+      \italic{lambda} := λvar.\italic{lambda} (representable(var))
                       | \italic{toplet} 
-      \italic{toplet} = letrec [\italic{binding}...] in var (representable(var))
-      \italic{binding} = var = \italic{rhs} (representable(rhs))
+      \italic{toplet} := letrec [\italic{binding}...] in var (representable(var))
+      \italic{binding} := var = \italic{rhs} (representable(rhs))
                        -- State packing and unpacking by coercion
                        | var0 = var1 ▶ State ty (lvar(var1))
-                       | var0 = var1 ▶ ty (var1 :: State ty) (lvar(var1))
-      \italic{rhs} = userapp
+                       | var0 = var1 ▶ ty (var1 :: State ty ∧ lvar(var1))
+      \italic{rhs} := userapp
                    | builtinapp
                    -- Extractor case
                    | case var of C a0 ... an -> ai (lvar(var))
                    -- Selector case
                    | case var of (lvar(var))
-                      DEFAULT -> var0 (lvar(var0))
-                      C w0 ... wn -> resvar (\forall{}i, wi \neq resvar, lvar(resvar))
-      \italic{userapp} = \italic{userfunc}
+                      [ DEFAULT -> var ]  (lvar(var))
+                      C0 w0,0 ... w0,n -> var0
+                      \vdots
+                      Cm wm,0 ... wm,n -> varm       (\forall{}i \forall{}j, wi,j \neq vari, lvar(vari))
+      \italic{userapp} := \italic{userfunc}
                        | \italic{userapp} {userarg}
-      \italic{userfunc} = var (gvar(var))
-      \italic{userarg} = var (lvar(var))
-      \italic{builtinapp} = \italic{builtinfunc}
+      \italic{userfunc} := var (gvar(var))
+      \italic{userarg} := var (lvar(var))
+      \italic{builtinapp} := \italic{builtinfunc}
                           | \italic{builtinapp} \italic{builtinarg}
-      \italic{builtinfunc} = var (bvar(var))
-      \italic{builtinarg} = \italic{coreexpr}
+      \italic{builtinfunc} := var (bvar(var))
+      \italic{builtinarg} := var (representable(var) ∧ lvar(var))
+                          | \italic{partapp} (partapp :: a -> b)
+                          | \italic{coreexpr} (¬representable(coreexpr) ∧ ¬(coreexpr :: a -> b))
+      \italic{partapp} := \italic{userapp} | \italic{builtinapp}
       \stoplambda
 
-      \todo{Limit builtinarg further}
-
       \todo{There can still be other casts around (which the code can handle,
       e.g., ignore), which still need to be documented here}
 
-      \todo{Note about the selector case. It just supports Bit and Bool
-      currently, perhaps it should be generalized in the normal form? This is
-      no longer true, btw}
-
       When looking at such a program from a hardware perspective, the top level
       lambda's define the input ports. The variable reference in the body of
       the recursive let expression is the output port. Most function
         
         \todo{More examples}
 
-    \subsection{Argument simplification}
-      The transforms in this section deal with simplifying application
-      arguments into normal form. The goal here is to:
-
-      \todo{This section should only talk about representable arguments. Non
-      representable arguments are treated by specialization.}
-
-      \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. This is needed, since these applications will be turned
-       into component instantiations.
-       \item Make all arguments of builtin functions one of:
-         \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
-
-      When looking at the arguments of a user-defined function, we can
-      divide them into two categories:
-      \startitemize
-        \item Arguments of a runtime representable type (\eg bits or vectors).
-
-              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). This is taken care of by the argument extraction
-              transform.
-        \item Non-runtime representable typed arguments. \todo{Move this
-        bullet to specialization}
-              
-              These arguments cannot be preserved in the program, since we
-              cannot represent them as input or output ports in the resulting
-              \small{VHDL}. To remove them, we create a specialized version of the
-              called function with these arguments filled in. This is done by
-              the argument propagation transform.
-
-              Typically, these arguments are type and dictionary arguments that are
-              used to make functions polymorphic. By propagating these arguments, we
-              are essentially doing the same which GHC does when it specializes
-              functions: Creating multiple variants of the same function, one for
-              each type for which it is used. Other common non-representable
-              arguments are functions, e.g. when calling a higher order function
-              with another function or a lambda abstraction as an argument.
-
-              The reason for doing this is similar to the reasoning provided for
-              the inlining of non-representable let bindings above. In fact, this
-              argument propagation could be viewed as a form of cross-function
-              inlining.
-      \stopitemize
-
-      \todo{Move this itemization into a new section about builtin functions}
-      When looking at the arguments of a builtin function, we can divide them
-      into categories: 
-
-      \startitemize
-        \item Arguments of a runtime representable type.
-              
-              As we have seen with user-defined functions, these arguments can
-              always be reduced to a simple variable reference, by the
-              argument extraction transform. Performing this transform for
-              builtin functions as well, means that the translation of builtin
-              functions can be limited to signal references, instead of
-              needing to support all possible expressions.
-
-        \item Arguments of a function type.
-              
-              These arguments are functions passed to higher order builtins,
-              like \lam{map} and \lam{foldl}. Since implementing these
-              functions for arbitrary function-typed expressions (\eg, lambda
-              expressions) is rather comlex, we reduce these arguments to
-              (partial applications of) global functions.
-              
-              We can still support arbitrary expressions from the user code,
-              by creating a new global function containing that expression.
-              This way, we can simply replace the argument with a reference to
-              that new function. However, since the expression can contain any
-              number of free variables we also have to include partial
-              applications in our normal form.
-
-              This category of arguments is handled by the function extraction
-              transform.
-        \item Other unrepresentable arguments.
-              
-              These arguments can take a few different forms:
-              \startdesc{Type arguments}
-                In the core language, type arguments can only take a single
-                form: A type wrapped in the Type constructor. Also, there is
-                nothing that can be done with type expressions, except for
-                applying functions to them, so we can simply leave type
-                arguments as they are.
-              \stopdesc
-              \startdesc{Dictionary arguments}
-                In the core language, dictionary arguments are used to find
-                operations operating on one of the type arguments (mostly for
-                finding class methods). Since we will not actually evaluatie
-                the function body for builtin functions and can generate
-                code for builtin functions by just looking at the type
-                arguments, these arguments can be ignored and left as they
-                are.
-              \stopdesc
-              \startdesc{Type level arguments}
-                Sometimes, we want to pass a value to a builtin function, but
-                we need to know the value at compile time. Additionally, the
-                value has an impact on the type of the function. This is
-                encoded using type-level values, where the actual value of the
-                argument is not important, but the type encodes some integer,
-                for example. Since the value is not important, the actual form
-                of the expression does not matter either and we can leave
-                these arguments as they are.
-              \stopdesc
-              \startdesc{Other arguments}
-                Technically, there is still a wide array of arguments that can
-                be passed, but does not fall into any of the above categories.
-                However, none of the supported builtin functions requires such
-                an argument. This leaves use with passing unsupported types to
-                a function, such as calling \lam{head} on a list of functions.
-
-                In these cases, it would be impossible to generate hardware
-                for such a function call anyway, so we can ignore these
-                arguments.
-
-                The only way to generate hardware for builtin functions with
-                arguments like these, is to expand the function call into an
-                equivalent core expression (\eg, expand map into a series of
-                function applications). But for now, we choose to simply not
-                support expressions like these.
-              \stopdesc
-
-              From the above, we can conclude that we can simply ignore these
-              other unrepresentable arguments and focus on the first two
-              categories instead.
+    \subsection[sec:normalization:argsimpl]{Representable arguments simplification}
+      This section contains just a single transformation that deals with
+      representable arguments in applications. Non-representable arguments are
+      handled by the transformations in
+      \in{section}[sec:normalization:nonrep]. 
+      
+      This transformation ensures that all representable arguments will become
+      references to local variables. This ensures they will become references
+      to local signals in the resulting \small{VHDL}, which is required due to
+      limitations in the component instantiation code in \VHDL (one can only
+      assign a signal or constant to an input port). By ensuring that all
+      arguments are always simple variable references, we always have a signal
+      available to map to the input ports.
+
+      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.
+
+      \refdef{global variable}
+      Note that references to \emph{global variables} (like a top level
+      function without arguments, but also an argumentless dataconstructors
+      like \lam{True}) are also simplified. Only local variables generate
+      signals in the resulting architecture. Even though argumentless
+      dataconstructors generate constants in generated \VHDL code and could be
+      mapped to an input port directly, they are still simplified to make the
+      normal form more regular.
+
+      \refdef{representable}
+      \starttrans
+      M N
+      --------------------    \lam{N} is representable
+      letrec x = N in M x     \lam{N} is not a local variable reference
+      \stoptrans
+      \refdef{local variable}
+
+      \startbuffer[from]
+      add (add a 1) 1
+      \stopbuffer
+
+      \startbuffer[to]
+      letrec x = add a 1 in add x 1
+      \stopbuffer
+
+      \transexample{argsimpl}{Argument simplification}{from}{to}
+
+    \subsection[sec:normalization:builtins]{Builtin functions}
+      This section deals with (arguments to) builtin functions.  In the
+      intended normal form definition\refdef{intended normal form definition}
+      we can see that there are three sorts of arguments a builtin function
+      can receive.
+      
+      \startitemize[KR]
+        \item A representable local variable reference. This is the most
+        common argument to any function. The argument simplification
+        transformation described in \in{section}[sec:normalization:argsimpl]
+        makes sure that \emph{any} representable argument to \emph{any}
+        function (including builtin functions) is turned into a local variable
+        reference.
+        \item (A partial application of) a top level function (either builtin on
+        user-defined). The function extraction transformation described in
+        this section takes care of turning every functiontyped argument into
+        (a partial application of) a top level function.
+        \item Any expression that is not representable and does not have a
+        function type. Since these can be any expression, there is no
+        transformation needed. Note that this category is exactly all
+        expressions that are not transformed by the transformations for the
+        previous two categories. This means that \emph{any} core expression
+        that is used as an argument to a builtin function will be either
+        transformed into one of the above categories, or end up in this
+        categorie. In any case, the result is in normal form.
       \stopitemize
 
-      \subsubsection[sec:normalization:argsimpl]{Argument simplification}
-        This transform deals with arguments to functions that
-        are of a runtime representable type. It ensures that they will all become
-        references to global variables, or local signals in the resulting
-        \small{VHDL}, which is required due to limitations in the component
-        instantiation code in \VHDL (one can only assign a signal or constant
-        to an input port). By ensuring that all arguments are always simple
-        variable references, we always have a signal available to assign to
-        input ports.
-
-        \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.
-
-        Note that a reference to a \emph{global variable} (like a top level
-        function without arguments, but also an argumentless dataconstructors
-        like \lam{True}) is also simplified. Only local variables generate
-        signals in the resulting architecture. 
+      As noted, the argument simplification will handle any representable
+      arguments to a builtin function. The following transformation is needed
+      to handle non-representable arguments with a function type, all other
+      non-representable arguments don't need any special handling.
 
-        \refdef{representable}
-        \starttrans
-        M N
-        --------------------    \lam{N} is representable
-        letrec x = N in M x     \lam{N} is not a local variable reference
-        \stoptrans
-        \refdef{local variable}
-
-        \startbuffer[from]
-        add (add a 1) 1
-        \stopbuffer
-
-        \startbuffer[to]
-        letrec x = add a 1 in add x 1
-        \stopbuffer
-
-        \transexample{argextract}{Argument extraction}{from}{to}
-      
       \subsubsection[sec:normalization:funextract]{Function extraction}
-        \todo{Move to section about builtin functions}
         This transform deals with function-typed arguments to builtin
-        functions.  Since builtin functions cannot be specialized to remove
-        the arguments, we choose to extract these arguments into a new global
-        function instead. This greatly simplifies the translation rules needed
-        for builtin functions. \todo{Should we talk about these? Reference
-        Christiaan?}
+        functions. 
+        Since builtin functions cannot be specialized (see
+        \in{section}[sec:normalization:specialize]) to remove the arguments,
+        these arguments are extracted into a new global function instead. In
+        other words, we create a new top level function that has exactly the
+        extracted argument as its body. This greatly simplifies the
+        translation rules needed for builtin functions, since they only need
+        to handle (partial applications of) top level functions.
 
         Any free variables occuring in the extracted arguments will become
         parameters to the new global function. The original argument is replaced
         x = λf0 ... λfn.N
         \stoptrans
 
-        \todo{Split this example}
         \startbuffer[from]
-        map (λa . add a b) xs
-
-        map (add b) ys
+        addList = λb.λxs.map (λa . add a b) xs
         \stopbuffer
 
         \startbuffer[to]
-        map (x0 b) xs
-
-        map x1 ys
+        addList = λb.λxs.map (f b) xs
         ~
-        x0 = λb.λa.add a b
-        x1 = λb.add b
+        f = λb.λa.add a b
         \stopbuffer
 
         \transexample{funextract}{Function extraction}{from}{to}
 
-        Note that \lam{x0} and {x1} will still need normalization after this.
-
-      \todo{Fill the gap left by moving argument propagation away}
+        Note that the function \lam{f} will still need normalization after
+        this.
 
     \subsection{Case normalisation}
       \subsubsection{Scrutinee simplification}
 
         \transexample{caserem}{Case removal}{from}{to}
 
-    \subsection{Removing unrepresentable values}
+    \subsection[sec:normalization:nonrep]{Removing unrepresentable values}
       The transformations in this section are aimed at making all the
       values used in our expression representable. There are two main
       transformations that are applied to \emph{all} unrepresentable let
-      bindings and function arguments, but these are really meant to
-      address three different kinds of unrepresentable values:
-      Polymorphic values, higher order values and literals. Each of these
-      will be detailed below, followed by the actual transformations.
+      bindings and function arguments. These are meant to address three
+      different kinds of unrepresentable values: Polymorphic values, higher
+      order values and literals. The transformation are described generically:
+      They apply to all non-representable values. However, non-representable
+      values that don't fall into one of these three categories will be moved
+      around by these transformations but are unlikely to completely
+      disappear. They usually mean the program was not valid in the first
+      place, because unsupported types were used (for example, a program using
+      strings).
+     
+      Each of these three categories will be detailed below, followed by the
+      actual transformations.
 
       \subsubsection{Removing Polymorphism}
         As noted in \in{section}[sec:prototype:polymporphism],
 
         \transexample{nonrepinline}{Nonrepresentable binding inlining}{from}{to}
 
-      \subsubsection{Function specialization}
+      \subsubsection[sec:normalization:specialize]{Function specialization}
         This transform removes arguments to user-defined functions that are
         not representable at runtime. This is done by creating a
         \emph{specialized} version of the function that only works for one
diff --git a/Outline b/Outline
index 7a18303..2b32c29 100644 (file)
--- a/Outline
+++ b/Outline
@@ -61,3 +61,4 @@ TODO: core => Core
 TODO: \defref{beta-reduction} -> \defref{β-reduction}
 TODO: Make interaction links not bold
 TODO: Say something about implementation differences with transformation specs
+TODO: Say something about the builtin functions somewhere (ref: christiaan)