\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}
+
+\subsection{Let flattening}
+This transform turns two nested lets (\lam{let x = (let ... in ...) in
+...}) into a single let.
+
+\subsection{Empty let removal}
+
+\subsection{Simple let binding removal}
+This transforms inlines simple let bindings (\eg a = b).
+
+\subsection{Unused let binding removal}
+
+\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}
\stoplambda
Application simplification is not applicable.
-\stoptext