Fib.hss

flatten-module
consider 'fib

{

ww-split [| wrap |] [| unwrap |]
consider 'work ; remember origwork

-- work = unwrap (f (wrap work))

0 ; eta-expand 'n

-- work n = unwrap (f (wrap work)) n

any-call (unfold 'unwrap)

-- work n = (f (wrap work) n, f (wrap work) (n+1))

0 ; case-split-inline 'n

-- work 0     = (f (wrap work) 0, f (wrap work) 1)
-- work (n+1) = (f (wrap work) (n+1), f (wrap work) (n+2))

{ 1 ; any-call (unfold 'f) }
{ 2 ; 0 ; 1 ; any-call (unfold 'f) }
simplify

-- work 0     = (0, 1)
-- work (n+1) = (f (wrap work) (n+1), wrap work (n+1) + wrap work n)

2 ; 0 ; { 1 ; any-call (unfold origwork) }

-- work 0     = (0, 1)
-- work (n+1) = (f (wrap work) (n+1), wrap (unwrap (f (wrap work))) (n+1) + wrap (unwrap (f (wrap work))) n)

any-bu (foreward (ww-assumption-A [| wrap |] [| unwrap |]))

-- work 0     = (0, 1)
-- work (n+1) = (f (wrap work) (n+1), f (wrap work) (n+1) + f (wrap work) n)

{ 1 ; 1 ; let-intro 'x }
{ 0 ; 1 ; let-intro 'y }
innermost let-float
try (reorder-lets ['x,'y])
one-td (fold 'y)
let-tuple 'xy

-- work 0     = (0, 1)
-- work (n+1) = let (x,y) = (f (wrap work) n, f (wrap work) (n+1)) in (y,x+y)

one-td (fold 'unwrap)

-- work 0     = (0, 1)
-- work (n+1) = let (x,y) = unwrap (f (wrap work)) n in (y,x+y)

one-td (fold origwork)

-- work 0     = (0, 1)
-- work (n+1) = let (x,y) = work n in (y,x+y)

}

innermost dead-let-elimination
any-call (unfold 'wrap)
simplify