Reorder and complete the list of transformations.

[matthijs/master-project/report.git] / Chapters / Normalization.tex

diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex
index d36556beeb775495a399f554be7da5686313efad..e609cb3d2874655ea38297c8c75637368b1fa2d7 100644 (file)
--- a/Chapters/Normalization.tex
+++ b/Chapters/Normalization.tex
@@ -62,29 +62,75 @@ An example of a program in canonical form would be:
 
 \startlambda
   -- All arguments are an inital lambda
 
 \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
   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.
     -- 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
     -- 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
       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
   in
     -- The actual result

-    r
+    res

 \stoplambda
 
 \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
 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


@@ -194,41 +240,44 @@ into expressions as far as possible. In lambda calculus, this reduction
 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).
 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
 (case x of
   p1 -> E1
   \vdots
   pn -> En) M

-\stopbuffer
-\startbuffer[to]
+-----------------

 case x of
   p1 -> E1 M
   \vdots
   pn -> En M
 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]
 \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]
 \stopbuffer
 
 \startbuffer[to]


@@ -242,6 +291,34 @@ in
 
 \transexample{Extended β-reduction}{from}{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:
 \subsection{Argument simplification}
 The transforms in this section deal with simplifying application
 arguments into normal form. The goal here is to:


@@ -472,69 +549,20 @@ translatable. A user-defined function is any other function.
 \starttrans
 x = E
 ~
 \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
 
 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.
 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}
 
 
 \subsection{Example sequence}
 


@@ -779,4 +807,3 @@ After let bind removal:
 \stoplambda
 
 Application simplification is not applicable.
 \stoplambda
 
 Application simplification is not applicable.

-\stoptext