Fib.hss

flatten-module
consider 'fib

{

load "../WWSplitTactic.hss"
consider 'work ; remember origwork

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

down ; 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))

down ; 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 (unfold-rule precondition)

-- 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-arg <+ let-float-app)
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