author Matthijs Kooijman Wed, 10 Jun 2009 11:43:51 +0000 (13:43 +0200) committer Matthijs Kooijman Wed, 10 Jun 2009 11:43:51 +0000 (13:43 +0200)
 Core2Core.tex patch | blob | history

index 66612e1..051ddd6 100644 (file)
@@ -39,6 +39,8 @@
% Install the lambda calculus pretty-printer, as defined in pret-lam.lua.
\installprettytype [LAM] [LAM]

% 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\lamframe{
% Put a frame around lambda expressions, so they can have multiple
% An (invisible) frame to hold a lambda expression
\define\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

Initial example

-\starttyping
-  \x ->
+\startlambda
+  λx.
let s = foo x
in
case s of
let s = foo x
in
case s of
@@ -477,15 +479,15 @@ Initial example
Low -> let
op' = case b of
High -> sub
Low -> let
op' = case b of
High -> sub
-                Low  -> \c d -> c
+                Low  -> λc.λd.c
in
in
-                \c d -> op' d c
-\stoptyping
+                λc.λd.op' d c
+\stoplambda

After top-level η-abstraction:

After top-level η-abstraction:

-\starttyping
-  \x c d ->
+\startlambda
+  λx.λc.λd.
(let s = foo x
in
case s of
(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 -> let
op' = case b of
High -> sub
-                Low  -> \c d -> c
+                Low  -> λc.λd.c
in
in
-                \c d -> op' d c
+                λc.λd.op' d c
) c d
) c d
-\stoptyping
+\stoplambda

After (extended) β-reduction:

After (extended) β-reduction:

-\starttyping
-  \x c d ->
+\startlambda
+  λx.λc.λd.
let s = foo x
in
case s of
let s = foo x
in
case s of
@@ -514,15 +516,15 @@ After (extended) β-reduction:
Low -> let
op' = case b of
High -> sub
Low -> let
op' = case b of
High -> sub
-                Low  -> \c d -> c
+                Low  -> λc.λd.c
in
op' d c
in
op' d c
-\stoptyping
+\stoplambda

After return value extraction:

After return value extraction:

-\starttyping
-  \x c d ->
+\startlambda
+  λx.λc.λd.
let s = foo x
r = case s of
(a, b) ->
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 -> let
op' = case b of
High -> sub
-                      Low  -> \c d -> c
+                      Low  -> λc.λd.c
in
op' d c
in
r
in
op' d c
in
r
-\stoptyping
+\stoplambda

Scrutinee simplification does not apply.

After case binder wildening:

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
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
in
r
-\stoptyping
+\stoplambda

After case value simplification

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
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'
-        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
r' = case a of
High -> rh
Low -> rl
in
r
-\stoptyping
+\stoplambda

After let flattening:

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
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'
rl = op' d c
rl = op' d c
-        rll = \c d -> c
+        rll = λc.λd.c
op' = case b of
High -> sub
Low  -> rll
op' = case b of
High -> sub
Low  -> rll
@@ -605,73 +602,70 @@ After let flattening:
Low -> rl
in
r
Low -> rl
in
r
-\stoptyping
+\stoplambda

After function inlining:

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
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'
rl = (case b of
High -> sub
rl = (case b of
High -> sub
-          Low  -> \c d -> c) d c
+          Low  -> λc.λd.c) d c
r' = case a of
r' = case a of
-               High -> rh
-               Low -> rl
+          High -> rh
+          Low -> rl
in
r
in
r
-\stoptyping
+\stoplambda

After (extended) β-reduction again:

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
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'
rl = case b of
High -> sub d c
Low  -> d
r' = case a of
rl = case b of
High -> sub d c
Low  -> d
r' = case a of
-               High -> rh
-               Low -> rl
+          High -> rh
+          Low -> rl
in
r
in
r
-\stoptyping
+\stoplambda

After case value simplification again:

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
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'
rlh = sub d c
rl = case b of
High -> rlh
Low  -> d
r' = case a of
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
in
r
-\stoptyping
+\stoplambda

After case removal:

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
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 -> rlh
Low  -> d
r' = case a of
-               High -> rh
-               Low -> rl
+          High -> rh
+          Low -> rl
in
r
in
r
-\stoptyping
+\stoplambda

After let bind removal:

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
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 -> rlh
Low  -> d
r' = case a of
-               High -> rh
-               Low -> rl
+          High -> rh
+          Low -> rl
in
r'
in
r'
-\stoptyping
+\stoplambda

Application simplification is not applicable.
\stoptext

Application simplification is not applicable.
\stoptext