projects
/
matthijs
/
master-project
/
report.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
Make pret-lam support superscripts.
[matthijs/master-project/report.git]
/
Core2Core.tex
diff --git
a/Core2Core.tex
b/Core2Core.tex
index 66612e12aac7933f782bf0e219266b6ed90821d7..051ddd6c12120cb5d216834d34583476cc5d2377 100644
(file)
--- 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]
% 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
% 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
Initial example
-\start
typing
- \x ->
+\start
lambda
+ λ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
-\stop
typing
+
λc.λd.
op' d c
+\stop
lambda
After top-level η-abstraction:
After top-level η-abstraction:
-\start
typing
- \x c d ->
+\start
lambda
+ λ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
-\stop
typing
+\stop
lambda
After (extended) β-reduction:
After (extended) β-reduction:
-\start
typing
- \x c d ->
+\start
lambda
+ λ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
-\stop
typing
+\stop
lambda
After return value extraction:
After return value extraction:
-\start
typing
- \x c d ->
+\start
lambda
+ λ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
-\stop
typing
+\stop
lambda
Scrutinee simplification does not apply.
After case binder wildening:
Scrutinee simplification does not apply.
After case binder wildening:
-\start
typing
- \x c d ->
+\start
lambda
+ λ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
-\stop
typing
+\stop
lambda
After case value simplification
After case value simplification
-\start
typing
- \x c d ->
+\start
lambda
+ λ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'
rh = add c d
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
r' = case a of
High -> rh
Low -> rl
in
r
-\stop
typing
+\stop
lambda
After let flattening:
After let flattening:
-\start
typing
- \x c d ->
+\start
lambda
+ λ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'
rh = add c d
rl = op' d c
rh = add c d
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
-\stop
typing
+\stop
lambda
After function inlining:
After function inlining:
-\start
typing
- \x c d ->
+\start
lambda
+ λ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'
rh = add c d
rl = (case b of
High -> sub
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
r' = case a of
-
High -> rh
-
Low -> rl
+ High -> rh
+ Low -> rl
in
r
in
r
-\stop
typing
+\stop
lambda
After (extended) β-reduction again:
After (extended) β-reduction again:
-\start
typing
- \x c d ->
+\start
lambda
+ λ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'
rh = add c d
rl = case b of
High -> sub d c
Low -> d
r' = case a of
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
in
r
-\stop
typing
+\stop
lambda
After case value simplification again:
After case value simplification again:
-\start
typing
- \x c d ->
+\start
lambda
+ λ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'
rh = add c d
rlh = sub d c
rl = case b of
High -> rlh
Low -> d
r' = case a of
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
in
r
-\stop
typing
+\stop
lambda
After case removal:
After case removal:
-\start
typing
- \x c d ->
+\start
lambda
+ λ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
-\stop
typing
+\stop
lambda
After let bind removal:
After let bind removal:
-\start
typing
- \x c d ->
+\start
lambda
+ λ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'
-\stop
typing
+\stop
lambda
Application simplification is not applicable.
\stoptext
Application simplification is not applicable.
\stoptext