X-Git-Url: https://git.stderr.nl/gitweb?p=matthijs%2Fmaster-project%2Freport.git;a=blobdiff_plain;f=Core2Core.tex;h=051ddd6c12120cb5d216834d34583476cc5d2377;hp=1b1a7826577f1418cfc8d4a281dc1e1dc9f24d6e;hb=b5c7b3b79746ee07210d1b5b93bd0ce83b8e6d29;hpb=51cc0f0087211d281ad8e364e299569b6d135416

diff --git a/Core2Core.tex b/Core2Core.tex
index 1b1a782..051ddd6 100644
--- a/Core2Core.tex
+++ b/Core2Core.tex
@@ -39,6 +39,8 @@
 % Install the lambda calculus pretty-printer, as defined in pret-lam.lua.
 \installprettytype [LAM] [LAM]
 
+\definetyping[lambda][option=LAM,style=sans]
+
 % An (invisible) frame to hold a lambda expression
 \define[1]\lamframe{
         % Put a frame around lambda expressions, so they can have multiple
@@ -463,4 +465,241 @@ 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
+
+\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 top-level η-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.
 \stoptext