module Tip.Pass.CSEMatch where
import Tip.Core
import Tip.Fresh
data CSEMatchOpts =
CSEMatchOpts {
cse_nullary :: Bool
}
cseMatchNormal, cseMatchWhy3 :: CSEMatchOpts
cseMatchNormal = CSEMatchOpts False
cseMatchWhy3 = CSEMatchOpts True
cseMatch :: Name a => CSEMatchOpts -> Theory a -> Theory a
cseMatch CSEMatchOpts{..} =
transformExprIn $ \e ->
case e of
Match (Lcl x) pats ->
Match (Lcl x) (map (replaceWith x) pats)
_ -> e
where
replaceWith x (Case (ConPat con args) body)
| length args > 0 || cse_nullary =
Case (ConPat con args) $
flip transformExpr body $ \e ->
if e == Gbl con :@: map Lcl args
then Lcl x
else e
replaceWith x case_ = case_