Move some more stuff around in the Normalization chapter.

diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex
index db743fc9a049d716c931747ca7cb09180723980a..d3b37003774e7f81abf3e6fc8661bf47811ce3f6 100644 (file)
--- a/Chapters/Normalization.tex
+++ b/Chapters/Normalization.tex
@@ -328,41 +328,40 @@
       \defref{intended normal form definition}
       \todo{Fix indentation}
       \startlambda
       \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} 

-      \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))
                        -- 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))
                    | 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{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{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
 
       \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{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
       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


@@ -1218,195 +1217,94 @@
         
         \todo{More examples}
 
         
         \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
 
       \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}
       \subsubsection[sec:normalization:funextract]{Function extraction}

-        \todo{Move to section about builtin functions}

         This transform deals with function-typed arguments to builtin
         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
 
         Any free variables occuring in the extracted arguments will become
         parameters to the new global function. The original argument is replaced


@@ -1427,27 +1325,20 @@
         x = λf0 ... λfn.N
         \stoptrans
 
         x = λf0 ... λfn.N
         \stoptrans
 

-        \todo{Split this example}

         \startbuffer[from]
         \startbuffer[from]

-        map (λa . add a b) xs
-
-        map (add b) ys
+        addList = λb.λxs.map (λa . add a b) xs

         \stopbuffer
 
         \startbuffer[to]
         \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}
 
         \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}
 
     \subsection{Case normalisation}
       \subsubsection{Scrutinee simplification}


@@ -1591,14 +1482,22 @@
 
         \transexample{caserem}{Case removal}{from}{to}
 
 
         \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
       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],
 
       \subsubsection{Removing Polymorphism}
         As noted in \in{section}[sec:prototype:polymporphism],


@@ -1939,7 +1838,7 @@
 
         \transexample{nonrepinline}{Nonrepresentable binding inlining}{from}{to}
 
 
         \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
         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 7a183037c745ea4973829301a57d82d4be8bc08a..2b32c29035d5f8298fa73af29b0edac97597b589 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: \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)