WWSplitTactic.hss

-- this is a (pretty general) ww tactic
-- it transforms:
--
-- rec g = body                                 (where body mentions g)
--
-- into:
--
-- g = let f = \g -> body                       (f is not recursive)
--         rec work = unwrap (f (wrap work))
--     in wrap work
--
-- Note: inlining f (and bashing) would result in the same code
--       achieved in the reverse example by applying the "ww" rule.
--
-- The original function g is now a non-recursive wrapping of the worker.
-- The worker makes use of the original body, and is recursive.
--
-- So what have we gained doing it this way? Mainly, the noise of the
-- original body is all tidily hidden in f, and we can focus on manipulating
-- the wrap and unwrap functions, which is what we want to do.
--
-- I've tested this on reverse, and it also works, so I think the
-- next step is to formulate it as an actual rewrite, or otherwise
-- bundle it up as a one-liner.
--
-- TODO: this relies on a RULES pragmas:
--
--  {-# RULES "ww" forall work . fix work = wrap (fix (unwrap . work . wrap)) #-}
--
-- We either need to provide this somehow, or implement it as a rewrite.
--
-- BEGIN: ww tactic
{
fix-intro
consider lam
let-intro 'f
up
let-float-arg
1
apply-rule ww
simplify
{ 1; let-intro 'w }
let-float-arg
{ rhs-of 'w
  unfold 'fix ; alpha-let 'work
  simplify
}
let-subst
let-float-arg
}
-- END: ww tactic