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 2acd1c8a14296539507ef8e153c19ff79a9498f5..b91eb40edda218c60ccb1fc951a2da436490af10 100644 (file)
--- a/Chapters/Normalization.tex
+++ b/Chapters/Normalization.tex
@@ -93,6 +93,44 @@ An example of a program in canonical form would be:
     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
@@ -480,8 +518,8 @@ 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   
 ~