From: Matthijs Kooijman <m.kooijman@student.utwente.nl>
Date: Wed, 10 Jun 2009 11:43:51 +0000 (+0200)
Subject: Format the example sequence as lambda calculus.
X-Git-Tag: final-thesis~327
X-Git-Url: https://git.stderr.nl/gitweb?p=matthijs%2Fmaster-project%2Freport.git;a=commitdiff_plain;h=acb73f97bc84ec0445f364edf8264734c9413e9d

Format the example sequence as lambda calculus.
---

diff --git a/Core2Core.tex b/Core2Core.tex
index 66612e1..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
@@ -466,8 +468,8 @@ by the compiler. For example, map, fold, +.
 
 Initial example
 
-\starttyping
-  \x -> 
+\startlambda
+  λx.
     let s = foo x
     in
       case s of
@@ -477,15 +479,15 @@ Initial example
             Low -> let
               op' = case b of
                 High -> sub
-                Low  -> \c d -> c
+                Low  -> λc.λd.c
               in
-                \c d -> op' d c
-\stoptyping
+                λc.λd.op' d c
+\stoplambda
 
 After top-level η-abstraction:
 
-\starttyping
-  \x c d -> 
+\startlambda
+  λx.λc.λd.
     (let s = foo x
     in
       case s of
@@ -495,16 +497,16 @@ After top-level η-abstraction:
             Low -> let
               op' = case b of
                 High -> sub
-                Low  -> \c d -> c
+                Low  -> λc.λd.c
               in
-                \c d -> op' d c
+                λc.λd.op' d c
     ) c d
-\stoptyping
+\stoplambda
 
 After (extended) β-reduction:
 
-\starttyping
-  \x c d -> 
+\startlambda
+  λx.λc.λd.
     let s = foo x
     in
       case s of
@@ -514,15 +516,15 @@ After (extended) β-reduction:
             Low -> let
               op' = case b of
                 High -> sub
-                Low  -> \c d -> c
+                Low  -> λc.λd.c
               in
                 op' d c
-\stoptyping
+\stoplambda
 
 After return value extraction:
 
-\starttyping
-  \x c d -> 
+\startlambda
+  λx.λc.λd.
     let s = foo x
         r = case s of
               (a, b) ->
@@ -531,72 +533,67 @@ After return value extraction:
                   Low -> let
                     op' = case b of
                       High -> sub
-                      Low  -> \c d -> c
+                      Low  -> λc.λd.c
                     in
                       op' d c
     in
       r
-\stoptyping
+\stoplambda
 
 Scrutinee simplification does not apply.
 
 After case binder wildening:
 
-\starttyping
-  \x c d -> 
+\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
+        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
+\stoplambda
 
 After case value simplification
 
-\starttyping
-  \x c d -> 
+\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'
+        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
+        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
+\stoplambda
 
 After let flattening:
 
-\starttyping
-  \x c d -> 
+\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'
+        r = case s of (_, _) -> r'
         rh = add c d
         rl = op' d c
-        rll = \c d -> c
+        rll = λc.λd.c
         op' = case b of
           High -> sub
           Low  -> rll
@@ -605,73 +602,70 @@ After let flattening:
                Low -> rl
     in
       r
-\stoptyping
+\stoplambda
 
 After function inlining:
 
-\starttyping
-  \x c d -> 
+\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'
+        r = case s of (_, _) -> r'
         rh = add c d
         rl = (case b of
           High -> sub
-          Low  -> \c d -> c) d c
+          Low  -> λc.λd.c) d c
         r' = case a of
-               High -> rh
-               Low -> rl
+          High -> rh
+          Low -> rl
     in
       r
-\stoptyping
+\stoplambda
 
 After (extended) β-reduction again:
 
-\starttyping
-  \x c d -> 
+\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'
+        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
+          High -> rh
+          Low -> rl
     in
       r
-\stoptyping
+\stoplambda
 
 After case value simplification again:
 
-\starttyping
-  \x c d -> 
+\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'
+        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
+          High -> rh
+          Low -> rl
     in
       r
-\stoptyping
+\stoplambda
 
 After case removal:
 
-\starttyping
-  \x c d -> 
+\startlambda
+  λx.λc.λd.
     let s = foo x
         a = case s of (a, _) -> a
         b = case s of (_, b) -> b
@@ -682,16 +676,16 @@ After case removal:
           High -> rlh
           Low  -> d
         r' = case a of
-               High -> rh
-               Low -> rl
+          High -> rh
+          Low -> rl
     in
       r
-\stoptyping
+\stoplambda
 
 After let bind removal:
 
-\starttyping
-  \x c d -> 
+\startlambda
+  λx.λc.λd.
     let s = foo x
         a = case s of (a, _) -> a
         b = case s of (_, b) -> b
@@ -701,11 +695,11 @@ After let bind removal:
           High -> rlh
           Low  -> d
         r' = case a of
-               High -> rh
-               Low -> rl
+          High -> rh
+          Low -> rl
     in
       r'
-\stoptyping
+\stoplambda
 
 Application simplification is not applicable.
 \stoptext