-\chapter{Normalization}
+\chapter[chap:normalization]{Normalization}
% A helper to print a single example in the half the page width. The example
% text should be in a buffer whose name is given in an argument.
% will end up on a single line. The strut=no option prevents a bunch of empty
% space at the start of the frame.
\define[1]\example{
- \framed[offset=1mm,align=right,strut=no]{
+ \framed[offset=1mm,align=right,strut=no,background=box,frame=off]{
\setuptyping[option=LAM,style=sans,before=,after=]
\typebuffer[#1]
\setuptyping[option=none,style=\tttf]
\stopbuffer
\transexample{Return value simplification}{from}{to}
-
-\subsection{Example sequence}
-
-This section lists an example expression, with a sequence of transforms
-applied to it. The exact transforms given here probably don't exactly
-match the transforms given above anymore, but perhaps this can clarify
-the big picture a bit.
-
-TODO: Update or remove this section.
-
-\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.
projects / matthijs / master-project / report.git / blobdiff