From: Matthijs Kooijman
Date: Wed, 2 Sep 2009 09:17:18 +0000 (+0200)
Subject: Remove the example sequence, it was completely out of date.
XGitTag: finalthesis~264
XGitUrl: https://git.stderr.nl/gitweb?p=matthijs%2Fmasterproject%2Freport.git;a=commitdiff_plain;h=689ceb49f2969d573c77d6f279b5ea90592cd6ca
Remove the example sequence, it was completely out of date.

diff git a/Chapters/Normalization.tex b/Chapters/Normalization.tex
index 1f9f62b..68d48d4 100644
 a/Chapters/Normalization.tex
+++ b/Chapters/Normalization.tex
@@ 973,247 +973,3 @@ x = let x = add 1 2 in x
\stopbuffer
\transexample{Return value simplification}{from}{to}

\subsection{Example sequence}

This section lists an example expression, with a sequence of transforms
applied to it. The exact transforms given here probably don't exactly
match the transforms given above anymore, but perhaps this can clarify
the big picture a bit.

TODO: Update or remove this section.

\startlambda
 Î»x.
 let s = foo x
 in
 case s of
 (a, b) >
 case a of
 High > add
 Low > let
 op' = case b of
 High > sub
 Low > Î»c.Î»d.c
 in
 Î»c.Î»d.op' d c
\stoplambda

After toplevel Î·abstraction:

\startlambda
 Î»x.Î»c.Î»d.
 (let s = foo x
 in
 case s of
 (a, b) >
 case a of
 High > add
 Low > let
 op' = case b of
 High > sub
 Low > Î»c.Î»d.c
 in
 Î»c.Î»d.op' d c
 ) c d
\stoplambda

After (extended) Î²reduction:

\startlambda
 Î»x.Î»c.Î»d.
 let s = foo x
 in
 case s of
 (a, b) >
 case a of
 High > add c d
 Low > let
 op' = case b of
 High > sub
 Low > Î»c.Î»d.c
 in
 op' d c
\stoplambda

After return value extraction:

\startlambda
 Î»x.Î»c.Î»d.
 let s = foo x
 r = case s of
 (a, b) >
 case a of
 High > add c d
 Low > let
 op' = case b of
 High > sub
 Low > Î»c.Î»d.c
 in
 op' d c
 in
 r
\stoplambda

Scrutinee simplification does not apply.

After case binder wildening:

\startlambda
 Î»x.Î»c.Î»d.
 let s = foo x
 a = case s of (a, _) > a
 b = case s of (_, b) > b
 r = case s of (_, _) >
 case a of
 High > add c d
 Low > let op' = case b of
 High > sub
 Low > Î»c.Î»d.c
 in
 op' d c
 in
 r
\stoplambda

After case value simplification

\startlambda
 Î»x.Î»c.Î»d.
 let s = foo x
 a = case s of (a, _) > a
 b = case s of (_, b) > b
 r = case s of (_, _) > r'
 rh = add c d
 rl = let rll = Î»c.Î»d.c
 op' = case b of
 High > sub
 Low > rll
 in
 op' d c
 r' = case a of
 High > rh
 Low > rl
 in
 r
\stoplambda

After let flattening:

\startlambda
 Î»x.Î»c.Î»d.
 let s = foo x
 a = case s of (a, _) > a
 b = case s of (_, b) > b
 r = case s of (_, _) > r'
 rh = add c d
 rl = op' d c
 rll = Î»c.Î»d.c
 op' = case b of
 High > sub
 Low > rll
 r' = case a of
 High > rh
 Low > rl
 in
 r
\stoplambda

After function inlining:

\startlambda
 Î»x.Î»c.Î»d.
 let s = foo x
 a = case s of (a, _) > a
 b = case s of (_, b) > b
 r = case s of (_, _) > r'
 rh = add c d
 rl = (case b of
 High > sub
 Low > Î»c.Î»d.c) d c
 r' = case a of
 High > rh
 Low > rl
 in
 r
\stoplambda

After (extended) Î²reduction again:

\startlambda
 Î»x.Î»c.Î»d.
 let s = foo x
 a = case s of (a, _) > a
 b = case s of (_, b) > b
 r = case s of (_, _) > r'
 rh = add c d
 rl = case b of
 High > sub d c
 Low > d
 r' = case a of
 High > rh
 Low > rl
 in
 r
\stoplambda

After case value simplification again:

\startlambda
 Î»x.Î»c.Î»d.
 let s = foo x
 a = case s of (a, _) > a
 b = case s of (_, b) > b
 r = case s of (_, _) > r'
 rh = add c d
 rlh = sub d c
 rl = case b of
 High > rlh
 Low > d
 r' = case a of
 High > rh
 Low > rl
 in
 r
\stoplambda

After case removal:

\startlambda
 Î»x.Î»c.Î»d.
 let s = foo x
 a = case s of (a, _) > a
 b = case s of (_, b) > b
 r = r'
 rh = add c d
 rlh = sub d c
 rl = case b of
 High > rlh
 Low > d
 r' = case a of
 High > rh
 Low > rl
 in
 r
\stoplambda

After let bind removal:

\startlambda
 Î»x.Î»c.Î»d.
 let s = foo x
 a = case s of (a, _) > a
 b = case s of (_, b) > b
 rh = add c d
 rlh = sub d c
 rl = case b of
 High > rlh
 Low > d
 r' = case a of
 High > rh
 Low > rl
 in
 r'
\stoplambda

Application simplification is not applicable.