\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
projects / matthijs / master-project / report.git / blobdiff