X-Git-Url: https://git.stderr.nl/gitweb?p=matthijs%2Fmaster-project%2Freport.git;a=blobdiff_plain;f=Chapters%2FNormalization.tex;h=e609cb3d2874655ea38297c8c75637368b1fa2d7;hp=d36556beeb775495a399f554be7da5686313efad;hb=4521ef7f14ae52781329c17250f67d25d9a67dca;hpb=8821711ab53c9f3b9989262a11c003766011e96c

diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex
index d36556b..e609cb3 100644
--- 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
-  λ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
@@ -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).
-\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]
@@ -242,6 +291,34 @@ in
 
 \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:
@@ -472,69 +549,20 @@ translatable. A user-defined function is any other function.
 \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}
 
@@ -779,4 +807,3 @@ After let bind removal:
 \stoplambda
 
 Application simplification is not applicable.
-\stoptext