Add a new definition of the normal form.

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

diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex
index a8194decdf2826b8c9677989754dcd4e3c78fa25..b91eb40edda218c60ccb1fc951a2da436490af10 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
+
+\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
 
 \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


@@ -472,8 +518,8 @@ 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 .        \lam{f0 ... fm} = free local vars of \lam{Y_i}
       E y0 ... yi-1 Yi yi+1 ... yn   
 ~