From: Matthijs Kooijman Date: Fri, 28 Aug 2009 19:41:15 +0000 (+0200) Subject: Add a new definition of the normal form. X-Git-Tag: final-thesis~273 X-Git-Url: https://git.stderr.nl/gitweb?a=commitdiff_plain;h=66f5758c343546733f7cda281ccff7eafedd6b73;p=matthijs%2Fmaster-project%2Freport.git Add a new definition of the normal form. This definition uses a sort of EBNF. --- diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex index cbef2c0..b91eb40 100644 --- 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