\startlambda
-- All arguments are an inital lambda
- λx.λc.λd.
- -- There is one let expression at the top level
+ λa.λd.λsp.
+ -- There are nested let expressions at top level
let
+ -- Unpack the state by coercion
+ s = sp :: (Word, Word)
+ -- Extract both registers from the state
+ r1 = case s of (fst, snd) -> fst
+ r2 = case s of (fst, snd) -> snd
-- Calling some other user-defined function.
- s = foo x
- -- Extracting result values from a tuple
- a = case s of (a, b) -> a
- b = case s of (a, b) -> b
- -- Some builtin expressions
- rh = add c d
- rhh = sub d c
+ d' = foo d
-- Conditional connections
- rl = case b of
- High -> rhh
+ out = case a of
+ High -> r1
+ Low -> r2
+ r1' = case a of
+ High -> d
+ Low -> r1
+ r2' = case a of
+ High -> r2
Low -> d
- r = case a of
- High -> rh
- Low -> rl
+ -- Packing a tuple
+ s' = (,) r1' r2'
+ -- Packing the state by coercion
+ sp' = s' :: State (Word, Word)
+ -- Pack our return value
+ res = (,) sp' out
in
-- The actual result
- r
+ res
\stoplambda
+\startlambda
+\italic{normal} = \italic{lambda}
+\italic{lambda} = λvar.\italic{lambda} (representable(typeof(var)))
+ | \italic{toplet}
+\italic{toplet} = let \italic{binding} in \italic{toplet}
+ | letrec [\italic{binding}] in \italic{toplet}
+ | var (representable(typeof(var)), fvar(var))
+\italic{binding} = var = \italic{rhs} (representable(typeof(rhs)))
+ -- State packing and unpacking by coercion
+ | var0 = var1 :: State ty (fvar(var1))
+ | var0 = var1 :: ty (var0 :: State ty) (fvar(var1))
+\italic{rhs} = userapp
+ | builtinapp
+ -- Extractor case
+ | case var of C a0 ... an -> ai (fvar(var))
+ -- Selector case
+ | case var of (fvar(var))
+ DEFAULT -> var0 (fvar(var0))
+ C w0 ... wn -> resvar (\forall{}i, wi \neq resvar, fvar(resvar))
+\italic{userapp} = \italic{userfunc}
+ | \italic{userapp} {userarg}
+\italic{userfunc} = var (tvar(var))
+\italic{userarg} = var (fvar(var))
+\italic{builtinapp} = \italic{builtinfunc}
+ | \italic{builtinapp} \italic{builtinarg}
+\italic{builtinfunc} = var (bvar(var))
+\italic{builtinarg} = \italic{coreexpr}
+\stoplambda
+
+-- TODO: Define tvar, fvar, typeof, representable
+-- 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?
+
When looking at such a program from a hardware perspective, the top level
lambda's define the input ports. The value produced by the let expression is
the output port. Most function applications bound by the let expression
is known as β-reduction, but it is of course only defined for
applications of lambda abstractions. We extend this reduction to also
work for the rest of core (case and let expressions).
-\startbuffer[from]
+
+For let expressions:
+\starttrans
+let binds in E) M
+-----------------
+let binds in E M
+\stoptrans
+
+For case statements:
+\starttrans
(case x of
p1 -> E1
\vdots
pn -> En) M
-\stopbuffer
-\startbuffer[to]
+-----------------
case x of
p1 -> E1 M
\vdots
pn -> En M
-\stopbuffer
+\stoptrans
-%\transform{Extended β-reduction}
-%{
-%\conclusion
-%\trans{(λx.E) M}{E[M/x]}
-%
-%\nextrule
-%\conclusion
-%\trans{(let binds in E) M}{let binds in E M}
-%
-%\nextrule
-%\conclusion
-%\transbuf{from}{to}
-%}
+For lambda expressions:
+\starttrans
+(λx.E) M
+-----------------
+E[M/x]
+\stoptrans
+% And an example
\startbuffer[from]
-let a = (case x of
- True -> id
- False -> neg
- ) 1
- b = (let y = 3 in add y) 2
-in
- (λz.add 1 z) 3
+( let a = (case x of
+ True -> id
+ False -> neg
+ ) 1
+ b = (let y = 3 in add y) 2
+ in
+ (λz.add 1 z)
+) 3
\stopbuffer
\startbuffer[to]
\transexample{Extended β-reduction}{from}{to}
+\subsection{Let derecursification}
+This transformation is meant to make lets non-recursive whenever possible.
+This might allow other optimizations to do their work better. TODO: Why is
+this needed exactly?
+
+\subsection{Let flattening}
+This transformation puts nested lets in the same scope, by lifting the
+binding(s) of the inner let into a new let around the outer let. Eventually,
+this will cause all let bindings to appear in the same scope (they will all be
+in scope for the function return value).
+
+Note that this transformation does not try to be smart when faced with
+recursive lets, it will just leave the lets recursive (possibly joining a
+recursive and non-recursive let into a single recursive let). The let
+rederursification transformation will do this instead.
+
+\starttrans
+letnonrec x = (let bindings in M) in N
+------------------------------------------
+let bindings in (letnonrec x = M) in N
+\stoptrans
+
+\starttrans
+letrec
+ \vdots
+ x = (let bindings in M)
+ \vdots
+in
+ N
+------------------------------------------
+letrec
+ \vdots
+ bindings
+ x = M
+ \vdots
+in
+ N
+\stoptrans
+
+\startbuffer[from]
+let
+ a = letrec
+ x = 1
+ y = 2
+ in
+ x + y
+in
+ letrec
+ b = let c = 3 in a + c
+ d = 4
+ in
+ d + b
+\stopbuffer
+\startbuffer[to]
+letrec
+ x = 1
+ y = 2
+in
+ let
+ a = x + y
+ in
+ letrec
+ c = 3
+ b = a + c
+ d = 4
+ in
+ d + b
+\stopbuffer
+
+\transexample{Let flattening}{from}{to}
+
+\subsection{Empty let removal}
+This transformation is simple: It removes recursive lets that have no bindings
+(which usually occurs when let derecursification removes the last binding from
+it).
+
+\starttrans
+letrec in M
+--------------
+M
+\stoptrans
+
+\subsection{Simple let binding removal}
+This transformation inlines simple let bindings (\eg a = b).
+
+This transformation is not needed to get into normal form, but makes the
+resulting VHDL a lot shorter.
+
+\starttrans
+letnonrec
+ a = b
+in
+ M
+-----------------
+M[b/a]
+\stoptrans
+
+\starttrans
+letrec
+ \vdots
+ a = b
+ \vdots
+in
+ M
+-----------------
+let
+ \vdots
+ \vdots
+in
+ M[b/a]
+\stoptrans
+
+\subsection{Unused let binding removal}
+This transformation removes let bindings that are never used. Usually,
+the desugarer introduces some unused let bindings.
+
+This normalization pass should really be unneeded to get into normal form
+(since ununsed bindings are not forbidden by the normal form), but in practice
+the desugarer or simplifier emits some unused bindings that cannot be
+normalized (e.g., calls to a \type{PatError} (TODO: Check this name)). Also,
+this transformation makes the resulting VHDL a lot shorter.
+
+\starttrans
+let a = E in M
+---------------------------- \lam{a} does not occur free in \lam{M}
+M
+\stoptrans
+
+\starttrans
+letrec
+ \vdots
+ a = E
+ \vdots
+in
+ M
+---------------------------- \lam{a} does not occur free in \lam{M}
+letrec
+ \vdots
+ \vdots
+in
+ M
+\stoptrans
+
+\subsection{Non-representable binding inlining}
+This transform inlines let bindings of a funtion type. TODO: This should
+be generelized to anything that is non representable at runtime, or
+something like that.
+
+\subsection{Scrutinee simplification}
+This transform ensures that the scrutinee of a case expression is always
+a simple variable reference.
+
+\subsection{Case simplification}
+
+\subsection{Case removal}
+This transform removes any case statements with a single alternative and
+only wild binders.
+
\subsection{Argument simplification}
The transforms in this section deal with simplifying application
arguments into normal form. The goal here is to:
\starttrans
x = E
~
-x Y0 ... Yi ... Yn \lam{Y_i} is not of a runtime representable type
---------------------------------------------- \lam{Y_i} is not a local variable reference
+x Y0 ... Yi ... Yn \lam{Yi} is not of a runtime representable type
+--------------------------------------------- \lam{Yi} is not a local variable reference
x' = λy0 ... yi-1 f0 ... fm yi+1 ... yn . \lam{f0 ... fm} = free local vars of \lam{Y_i}
E y0 ... yi-1 Yi yi+1 ... yn
~
x' y0 ... yi-1 f0 ... fm Yi+1 ... Yn
\stoptrans
-%\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?
-
-\subsection{Cast propagation}
+\subsection{Cast propagation / simplification}
This transform pushes casts down into the expression as far as possible.
-\subsection{Let recursification}
-This transform makes all lets recursive.
-\subsection{Let simplification}
-This transform makes the result value of all let expressions a simple
-variable reference.
-\subsection{Let flattening}
-This transform turns two nested lets (\lam{let x = (let ... in ...) in
-...}) into a single let.
-\subsection{Simple let binding removal}
-This transforms inlines simple let bindings (\eg a = b).
-\subsection{Function inlining}
-This transform inlines let bindings of a funtion type. TODO: This should
-be generelized to anything that is non representable at runtime, or
-something like that.
-\subsection{Scrutinee simplification}
-This transform ensures that the scrutinee of a case expression is always
-a simple variable reference.
-\subsection{Case binder wildening}
-This transform replaces all binders of a each case alternative with a
-wild binder (\ie, one that is never referred to). This will possibly
-introduce a number of new "selector" case statements, that only select
-one element from an algebraic datatype and bind it to a variable.
-\subsection{Case value simplification}
-This transform simplifies the result value of each case alternative by
-binding the value in a let expression and replacing the value by a
-simple variable reference.
-\subsection{Case removal}
-This transform removes any case statements with a single alternative and
-only wild binders.
+
+\subsection{Return value simplification}
+Currently implemented using lambda simplification, let simplification, and
+top simplification. Should change.
\subsection{Example sequence}
projects / matthijs / master-project / report.git / blobdiff