module Data.Comp.Multi.Strategic
(
RewriteM
, Rewrite
, GRewriteM
, GRewrite
, addFail
, tryR
, promoteR
, promoteRF
, allR
, (>+>)
, (+>)
, anyR
, oneR
, alltdR
, allbuR
, anytdR
, anybuR
, prunetdR
, onetdR
, onebuR
, Translate
, TranslateM
, GTranslateM
, promoteTF
, mtryM
, onetdT
, foldtdT
, crushtdT
) where
import Control.Applicative ( Applicative, (<*) )
import Control.Monad ( MonadPlus(..), liftM, liftM2, (>=>) )
import Control.Monad.Identity ( Identity )
import Control.Monad.Trans ( lift )
import Control.Monad.Trans.Maybe ( MaybeT, runMaybeT )
import Control.Monad.State ( StateT, runStateT, get, put )
import Control.Monad.Writer ( WriterT, runWriterT, tell )
import Data.Comp.Multi ( Cxt(..), Term, unTerm )
import Data.Comp.Multi.Generic ( query )
import Data.Comp.Multi.HFoldable ( HFoldable )
import Data.Comp.Multi.HTraversable ( HTraversable, hmapM )
import Data.Monoid ( Monoid, mappend, mempty, Any(..) )
import Data.Type.Equality ( (:~:)(..), sym )
import Data.Comp.Multi.Strategy.Classification
subst :: (a :~: b) -> f a -> f b
subst Refl x = x
subst2 :: (a :~: b) -> f (g a) -> f (g b)
subst2 Refl x = x
type RewriteM m f l = f l -> m (f l)
type Rewrite f l = RewriteM Identity f l
type GRewriteM m f = forall l. RewriteM m f l
type GRewrite f = GRewriteM Identity f
type AnyR m = WriterT Any m
wrapAnyR :: (Applicative m, MonadPlus m) => RewriteM m f l -> RewriteM (AnyR m) f l
wrapAnyR f t = (lift (f t) <* tell (Any True)) `mplus` return t
unwrapAnyR :: MonadPlus m => RewriteM (AnyR m) f l -> RewriteM m f l
unwrapAnyR f t = do (t', Any b) <- runWriterT (f t)
if b then
return t'
else
mzero
type OneR m = StateT Bool m
wrapOneR :: (Applicative m, MonadPlus m) => RewriteM m f l -> RewriteM (OneR m) f l
wrapOneR f t = do b <- get
if b then
return t
else
(lift (f t) <* put True) `mplus` return t
unwrapOneR :: MonadPlus m => RewriteM (OneR m) f l -> RewriteM m f l
unwrapOneR f t = do (t', b) <- runStateT (f t) False
if b then
return t'
else
mzero
dynamicR :: (DynCase f l, MonadPlus m) => RewriteM m f l -> GRewriteM m f
dynamicR f t = case dyncase t of
Just p -> subst2 (sym p) $ f (subst p t)
Nothing -> mzero
tryR :: (Monad m) => RewriteM (MaybeT m) f l -> RewriteM m f l
tryR f t = liftM (maybe t id) $ runMaybeT (f t)
promoteR :: (DynCase f l, Monad m) => RewriteM (MaybeT m) f l -> GRewriteM m f
promoteR = tryR . dynamicR
promoteRF :: (DynCase f l, Monad m) => RewriteM (MaybeT m) f l -> GRewriteM (MaybeT m) f
promoteRF = dynamicR
allR :: (Monad m, HTraversable f) => GRewriteM m (Term f) -> RewriteM m (Term f) l
allR f t = liftM Term $ hmapM f $ unTerm t
(>+>) :: (Applicative m, MonadPlus m) => GRewriteM m f -> GRewriteM m f -> GRewriteM m f
f >+> g = unwrapAnyR (wrapAnyR f >=> wrapAnyR g)
(+>) :: (MonadPlus m) => RewriteM m f l -> RewriteM m f l -> RewriteM m f l
(+>) f g x = f x `mplus` g x
anyR :: (Applicative m, MonadPlus m, HTraversable f) => GRewriteM m (Term f) -> RewriteM m (Term f) l
anyR f = unwrapAnyR $ allR $ wrapAnyR f
oneR :: (Applicative m, MonadPlus m, HTraversable f) => GRewriteM m (Term f) -> RewriteM m (Term f) l
oneR f = unwrapOneR $ allR $ wrapOneR f
allbuR :: (Monad m, HTraversable f) => GRewriteM m (Term f) -> GRewriteM m (Term f)
allbuR f = allR (allbuR f) >=> f
alltdR :: (Monad m, HTraversable f) => GRewriteM m (Term f) -> GRewriteM m (Term f)
alltdR f = f >=> allR (alltdR f)
anybuR :: (Applicative m, MonadPlus m, HTraversable f) => GRewriteM m (Term f) -> GRewriteM m (Term f)
anybuR f = anyR (anybuR f) >+> f
anytdR :: (Applicative m, MonadPlus m, HTraversable f) => GRewriteM m (Term f) -> GRewriteM m (Term f)
anytdR f = f >+> anyR (anytdR f)
prunetdR :: (Applicative m, MonadPlus m, HTraversable f) => GRewriteM m (Term f) -> GRewriteM m (Term f)
prunetdR f = f +> anyR (prunetdR f)
onebuR :: (Applicative m, MonadPlus m, HTraversable f) => GRewriteM m (Term f) -> GRewriteM m (Term f)
onebuR f = oneR (onebuR f) +> f
onetdR :: (Applicative m, MonadPlus m, HTraversable f) => GRewriteM m (Term f) -> GRewriteM m (Term f)
onetdR f = f +> oneR (onetdR f)
type Translate f l t = TranslateM Identity f l t
type TranslateM m f l t = f l -> m t
type GTranslateM m f t = forall l. TranslateM m f l t
promoteTF :: (DynCase f l, MonadPlus m) => TranslateM m f l t -> GTranslateM m f t
promoteTF f t = case dyncase t of
Just p -> f (subst p t)
Nothing -> mzero
addFail :: Monad m => TranslateM m f l t -> TranslateM (MaybeT m) f l t
addFail = (lift . )
mtryM :: (Monad m, Monoid a) => MaybeT m a -> m a
mtryM = liftM (maybe mempty id) . runMaybeT
onetdT :: (MonadPlus m, HFoldable f) => GTranslateM m (Term f) t -> GTranslateM m (Term f) t
onetdT t = query t mplus
foldtdT :: (HFoldable f, Monoid t, Monad m) => GTranslateM m (Term f) t -> GTranslateM m (Term f) t
foldtdT t = query t (liftM2 mappend)
crushtdT :: (HFoldable f, Monoid t, Monad m) => GTranslateM (MaybeT m) (Term f) t -> GTranslateM m (Term f) t
crushtdT f = foldtdT $ mtryM . f