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

Definition elimination for CoreProg? #118

Open conal opened 10 years ago

conal commented 10 years ago

Is there a transformation like letSubstR but for CoreProg instead of CoreExpr? Perhaps it would amount to a traversal with unfoldNameR, plus a transformation to remove unused definitions. I guess it'd have to include a check that the name is not exported.

xich commented 10 years ago

There isn't, but I think this would work:

{-# LANGUAGE ScopedTypeVariables #-}

progNonRecSubstR :: forall c m. Rewrite c m CoreProg
progNonRecSubstR = do
  ProgCons (NonRec v _) _ <- idR
  extractR (anybuR (promoteExprR (unfoldPredR (const . (==v))) :: Rewrite c m Core)) >>> progBindElimR

To handle recursive groups at the CoreProg level, you'd probably want a rewrite that breaks them into non-recursive bindings and SCC recursive groups. I believe GHC's occurAnalysePgm will do this (along with some other stuff), so you could lift it into a rewrite. Neil lifted the expression-level version in HERMIT.Dictionary.GHC.

conal commented 10 years ago

Thanks!