From: Matthijs Kooijman Date: Wed, 4 Nov 2009 11:47:34 +0000 (+0100) Subject: Make the normal form use only recursive lets again. X-Git-Tag: final-thesis~175 X-Git-Url: https://git.stderr.nl/gitweb?a=commitdiff_plain;h=4703461b0093f5c9a83876fad9d21a34c7a28eb4;p=matthijs%2Fmaster-project%2Freport.git Make the normal form use only recursive lets again. Previously, both recursive and non-recursive lets were allowed, which made a lot of transformations a lot more complex. Now, all lets are made recursive again, which makes things simpler. Also do some other miscellaneous fixes in the Normalization chapter. --- diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex index 5647ae0..f1b53df 100644 --- a/Chapters/Normalization.tex +++ b/Chapters/Normalization.tex @@ -317,9 +317,7 @@ \italic{normal} = \italic{lambda} \italic{lambda} = λvar.\italic{lambda} (representable(var)) | \italic{toplet} - \italic{toplet} = let \italic{binding} in \italic{toplet} - | letrec [\italic{binding}] in \italic{toplet} - | var (representable(varvar)) + \italic{toplet} = letrec [\italic{binding}...] in var (representable(varvar)) \italic{binding} = var = \italic{rhs} (representable(rhs)) -- State packing and unpacking by coercion | var0 = var1 :: State ty (lvar(var1)) @@ -590,6 +588,8 @@ In the following sections, we will be using a number of functions and notations, which we will define here. + TODO: Define substitution + \subsubsection{Other concepts} A \emph{global variable} is any variable that is bound at the top level of a program, or an external module. A \emph{local variable} is any @@ -784,8 +784,8 @@ \subsubsection{Empty let removal} This transformation is simple: It removes recursive lets that have no bindings - (which usually occurs when let derecursification removes the last binding from - it). + (which usually occurs when unused let binding removal removes the last + binding from it). \starttrans letrec in M @@ -793,67 +793,70 @@ M \stoptrans + TODO: Example + \subsubsection{Simple let binding removal} This transformation inlines simple let bindings (\eg a = b). This transformation is not needed to get into normal form, but makes the resulting \small{VHDL} a lot shorter. - \starttrans - letnonrec - a = b - in - M - ----------------- - M[b/a] - \stoptrans - \starttrans letrec + a0 = E0 \vdots - a = b + ai = b \vdots + an = En in M - ----------------- - let - \vdots [b/a] - \vdots [b/a] + ----------------------------- \lam{b} is a variable reference + letrec + a0 = E0 [b/ai] + \vdots + ai-1 = Ei-1 [b/ai] + ai+1 = Ei+1 [b/ai] + \vdots + an = En [b/ai] in - M[b/a] + M[b/ai] \stoptrans + TODO: Example + \subsubsection{Unused let binding removal} This transformation removes let bindings that are never used. Usually, the desugarer introduces some unused let bindings. This normalization pass should really be unneeded to get into normal form - (since ununsed bindings are not forbidden by the normal form), but in practice + (since unused bindings are not forbidden by the normal form), but in practice the desugarer or simplifier emits some unused bindings that cannot be normalized (e.g., calls to a \type{PatError} (TODO: Check this name)). Also, this transformation makes the resulting \small{VHDL} a lot shorter. - \starttrans - let a = E in M - ---------------------------- \lam{a} does not occur free in \lam{M} - M - \stoptrans - \starttrans letrec + a0 = E0 \vdots - a = E + ai = Ei \vdots + an = En in - M - ---------------------------- \lam{a} does not occur free in \lam{M} + M \lam{a} does not occur free in \lam{M} + ---------------------------- \forall j, 0 <= j <= n, j ≠ i (\lam{a} does not occur free in \lam{Ej}) letrec + a0 = E0 \vdots + ai-1 = Ei-1 + ai+1 = Ei+1 \vdots + an = En in M \stoptrans + TODO: Example + \subsubsection{Cast propagation / simplification} This transform pushes casts down into the expression as far as possible. Since its exact role and need is not clear yet, this transformation is @@ -862,7 +865,7 @@ \subsubsection{Compiler generated top level binding inlining} TODO - \section{Program structure} + \subsection{Program structure} These transformations are aimed at normalizing the overall structure into the intended form. This means ensuring there is a lambda abstraction at the top for every argument (input port), putting all of the other @@ -904,14 +907,14 @@ specialization). \starttrans - (let binds in E) M + (letrec binds in E) M ----------------- - let binds in E M + letrec binds in E M \stoptrans % And an example \startbuffer[from] - ( let + ( letrec val = 1 in add val @@ -919,7 +922,7 @@ \stopbuffer \startbuffer[to] - let + letrec val = 1 in add val 3 @@ -955,10 +958,24 @@ \transexample{Application propagation for a case expression}{from}{to} - \subsubsection{Let derecursification} - This transformation is meant to make lets non-recursive whenever possible. - This might allow other optimizations to do their work better. TODO: Why is - this needed exactly? + \subsubsection{Let recursification} + This transformation makes all non-recursive lets recursive. In the + end, we want a single recursive let in our normalized program, so all + non-recursive lets can be converted. This also makes other + transformations simpler: They can simply assume all lets are + recursive. + + \starttrans + let + a = E + in + M + ------------------------------------------ + letrec + a = E + in + M + \stoptrans \subsubsection{Let flattening} This transformation puts nested lets in the same scope, by lifting the @@ -966,21 +983,10 @@ this will cause all let bindings to appear in the same scope (they will all be in scope for the function return value). - Note that this transformation does not try to be smart when faced with - recursive lets, it will just leave the lets recursive (possibly joining a - recursive and non-recursive let into a single recursive let). The let - dederecursification transformation will do this instead. - - \starttrans - letnonrec x = (let bindings in M) in N - ------------------------------------------ - let bindings in (letnonrec x = M) in N - \stoptrans - \starttrans letrec \vdots - x = (let bindings in M) + x = (letrec bindings in M) \vdots in N @@ -995,33 +1001,22 @@ \stoptrans \startbuffer[from] - let + letrec a = letrec x = 1 y = 2 in x + y in - letrec - b = let c = 3 in a + c - d = 4 - in - d + b + a \stopbuffer \startbuffer[to] letrec x = 1 y = 2 + a = x + y in - let - a = x + y - in - letrec - c = 3 - b = a + c - d = 4 - in - d + b + a \stopbuffer \transexample{Let flattening}{from}{to} @@ -1051,7 +1046,7 @@ ~ \lam{E} is not a lambda abstraction E \lam{E} is not a let expression --------------------------- \lam{E} is not a local variable reference - let x = E in x + letrec x = E in x \stoptrans \starttrans @@ -1059,7 +1054,7 @@ ~ \lam{E} is representable E \lam{E} is not a let expression --------------------------- \lam{E} is not a local variable reference - let x = E in x + letrec x = E in x \stoptrans \starttrans @@ -1067,7 +1062,7 @@ ~ \lam{E} is representable E \lam{E} is not a local variable reference --------------------------- - let x = E in x + letrec x = E in x \stoptrans \startbuffer[from] @@ -1075,7 +1070,7 @@ \stopbuffer \startbuffer[to] - x = let x = add 1 2 in x + x = letrec x = add 1 2 in x \stopbuffer \transexample{Return value simplification}{from}{to} @@ -1235,7 +1230,7 @@ \starttrans M N -------------------- \lam{N} is of a representable type - let x = N in M x \lam{N} is not a local variable reference + letrec x = N in M x \lam{N} is not a local variable reference \stoptrans \startbuffer[from] @@ -1243,7 +1238,7 @@ \stopbuffer \startbuffer[to] - let x = add a 1 in add x 1 + letrec x = add a 1 in add x 1 \stopbuffer \transexample{Argument extraction}{from}{to} @@ -1267,7 +1262,7 @@ \starttrans M N \lam{M} is a (partial aplication of a) builtin function. --------------------- \lam{f0 ... fn} = free local variables of \lam{N} - M x f0 ... fn \lam{N :: a -> b} + M (x f0 ... fn) \lam{N :: a -> b} ~ \lam{N} is not a (partial application of) a top level function x = λf0 ... λfn.N \stoptrans @@ -1279,16 +1274,18 @@ \stopbuffer \startbuffer[to] - x0 = λb.λa.add a b - ~ - map x0 xs + map (x0 b) xs - x1 = λb.add b map x1 ys + ~ + x0 = λb.λa.add a b + x1 = λb.add b \stopbuffer \transexample{Function extraction}{from}{to} + Note that \lam{x0} and {x1} will still need normalization after this. + \subsubsection{Argument propagation} This transform deals with arguments to user-defined functions that are not representable at runtime. This means these arguments cannot be @@ -1303,7 +1300,7 @@ inc = λa.f a 1 \stoplambda - we could {\em propagate} the constant argument 1, with the following + We could {\em propagate} the constant argument 1, with the following result: \startlambda @@ -1350,7 +1347,7 @@ case E of alts ----------------- \lam{E} is not a local variable reference - let x = E in + letrec x = E in case E of alts \stoptrans @@ -1362,7 +1359,7 @@ \stopbuffer \startbuffer[to] - let x = foo a in + letrec x = foo a in case x of True -> a False -> b @@ -1388,7 +1385,7 @@ \vdots Cn vn,0 ... vn,m -> En --------------------------------------------------- \forall i \forall j, 0 <= i <= n, 0 <= i < m (\lam{wi,j} is a wild (unused) binder) - letnonrec + letrec v0,0 = case x of C0 v0,0 .. v0,m -> v0,0 \vdots v0,m = case x of C0 v0,0 .. v0,m -> v0,m @@ -1430,7 +1427,7 @@ (,) b c -> add b c \stopbuffer \startbuffer[to] - letnonrec + letrec b = case a of (,) b c -> b c = case a of (,) b c -> c x0 = add b c @@ -1503,31 +1500,32 @@ non-representable types. TODO: This/these paragraph(s) should probably become a separate discussion somewhere else. - \starttrans - letnonrec a = E in M - -------------------------- \lam{E} has a non-representable type. - M[E/a] - \stoptrans \starttrans letrec + a0 = E0 \vdots - a = E + ai = Ei \vdots + an = En in M - -------------------------- \lam{E} has a non-representable type. + -------------------------- \lam{Ei} has a non-representable type. letrec - \vdots [E/a] - \vdots [E/a] + a0 = E0 [Ei/ai] + \vdots + ai-1 = Ei-1 [Ei/ai] + ai+1 = Ei+1 [Ei/ai] + \vdots + an = En [Ei/ai] in - M[E/a] + M[Ei/ai] \stoptrans \startbuffer[from] letrec a = smallInteger 10 - inc = λa -> add a 1 + inc = λb -> add b 1 inc' = add 1 x = fromInteger a in @@ -1538,10 +1536,10 @@ letrec x = fromInteger (smallInteger 10) in - (λa -> add a 1) (add 1 x) + (λb -> add b 1) (add 1 x) \stopbuffer - \transexample{Let flattening}{from}{to} + \transexample{None representable binding inlining}{from}{to} \section{Provable properties}