Add a sequence of examples for the new transformations.

The transformations themselves are not in the document yet, but this was
an exploration of the possibilities.

diff --git a/Core2Core.tex b/Core2Core.tex
index 1b1a7826577f1418cfc8d4a281dc1e1dc9f24d6e..66612e12aac7933f782bf0e219266b6ed90821d7 100644 (file)
--- a/Core2Core.tex
+++ b/Core2Core.tex
@@ -463,4 +463,249 @@ non-polymorph functions can be a lot faster than generic ones).
 \item More builtin expressions should be added and these should be evaluated
 by the compiler. For example, map, fold, +.
 \stopitemize
+
+Initial example
+
+\starttyping
+  \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
+\stoptyping
+
+After top-level η-abstraction:
+
+\starttyping
+  \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
+\stoptyping
+
+After (extended) β-reduction:
+
+\starttyping
+  \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
+\stoptyping
+
+After return value extraction:
+
+\starttyping
+  \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
+\stoptyping
+
+Scrutinee simplification does not apply.
+
+After case binder wildening:
+
+\starttyping
+  \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
+\stoptyping
+
+After case value simplification
+
+\starttyping
+  \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
+\stoptyping
+
+After let flattening:
+
+\starttyping
+  \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
+\stoptyping
+
+After function inlining:
+
+\starttyping
+  \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
+\stoptyping
+
+After (extended) β-reduction again:
+
+\starttyping
+  \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
+\stoptyping
+
+After case value simplification again:
+
+\starttyping
+  \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
+\stoptyping
+
+After case removal:
+
+\starttyping
+  \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
+\stoptyping
+
+After let bind removal:
+
+\starttyping
+  \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'
+\stoptyping
+
+Application simplification is not applicable.
 \stoptext