ku-fpg / hermit

Haskell Equational Reasoning Model-to-Implementation Tunnel
http://www.ittc.ku.edu/csdl/fpg/Tools/HERMIT
BSD 2-Clause "Simplified" License
49 stars 8 forks source link

let-float from case alternative #113

Closed conal closed 10 years ago

conal commented 10 years ago

Is there a let-float variation for when the let binding is in a case alternative? Something like the following:

case foo of { p -> let x = u in v ; ... }  ==>
let x = u in case foo of { p -> v ; ... }

where no variable in p occurs in u and where x is not one of the variables in p.

If HERMIT doesn't have such a rewrite, is it because the need hasn't arisen?

conal commented 10 years ago

Here's my current working version. Feedback, please.

-- | case foo of { ... ; p -> let x = u in v ; ... }  ==>
--   let x = u in case foo of { ... ; p -> v ; ... }
-- 
-- where no variable in `p` occurs freely in `u`, and where `x` is not one of
-- the variables in `p`.
letFloatCaseAltR :: ReExpr
letFloatCaseAltR =
  do Case scrut w ty alts <- id
     (b,alts') <- letFloatOneAltR alts
     return $ Let b (Case scrut w ty alts')

-- Perform the first safe let-floating out of a case alternative
letFloatOneAltR :: [CoreAlt] -> TransformH x (CoreBind,[CoreAlt])
letFloatOneAltR [] = fail "no alternatives safe to let-float"
letFloatOneAltR (alt:rest) =
  (do (bind,alt') <- letFloatAltR alt
      return (bind,alt':rest))
  <+
  (second (alt :) <$> letFloatOneAltR rest)

-- (p -> let bind in e) ==>  (bind, p -> e)
letFloatAltR :: CoreAlt -> TransformH x (CoreBind,CoreAlt)
letFloatAltR (con,vs,Let bind@(NonRec x a) body)
  | isEmptyVarSet (vset `intersectVarSet` freeVarsExpr a)
    && not (x `elemVarSet` vset)
  = return (bind,(con,vs,body))
 where
   vset = mkVarSet vs
letFloatAltR _ = fail "letFloatAltR: not applicable"

-- TODO: consider variable occurrence conditions more carefully
xich commented 10 years ago

I've added this in b799ed8bb5fee861cad0707a16bd9d37b8a22f87

Thanks for the starting point. I adapted your code in a couple ways:

  1. It now handles recursive binding groups (though will not split them).
  2. There is an external that allows you to specify a specific alternative you want to float from.
  3. Added some cases to the unbound/capture checks... I think I covered everything possible.