{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
module Data.Comp.Multi.Strategic
(
RewriteM
, Rewrite
, GRewriteM
, GRewrite
, addFail
, tryR
, failR
, dynamicR
, promoteR
, promoteRF
, (>+>)
, (<+)
, allR
, revAllR
, anyR
, oneR
, allStateR
, allIdxR
, alltdR
, allbuR
, anytdR
, anybuR
, revAllbuR
, prunetdRF
, prunetdR
, onetdR
, onebuR
, idR
, traceR
, isSortR
, Translate
, TranslateM
, GTranslateM
, guardBoolT
, guardedT
, foldtdT
, crushtdT
, onetdT
, (+>>)
, isSortT
, failT
, notT
, promoteTF
, mtryM
, foldT
) where
import Control.Applicative ( Applicative, (<*), liftA, liftA2, Alternative(..) )
import Control.Applicative.Backwards ( Backwards(..) )
import Control.Monad ( MonadPlus(..), liftM, liftM2, (>=>), guard )
import Control.Monad.Identity ( Identity )
import Control.Monad.Trans ( lift )
import Control.Monad.Trans.Maybe ( MaybeT, runMaybeT )
import Control.Monad.State ( StateT, runStateT, evalStateT, get, put )
import Control.Monad.Writer ( WriterT, runWriterT, tell )
import Control.Parallel.Strategies ( withStrategy, rparWith, rpar, Eval, runEval )
import Debug.Trace ( traceM )
import Data.Comp.Multi ( Cxt(..), HFix, unTerm, (:->), (:=>) )
import Data.Comp.Multi.Generic ( query )
import Data.Comp.Multi.HFoldable ( HFoldable(..) )
import Data.Comp.Multi.HTraversable ( HTraversable(..) )
import Data.Comp.Multi.Show ( KShow, ShowHF )
import Data.Monoid ( Monoid, mappend, mempty, Any(..) )
import Data.Proxy ( Proxy(..) )
import Data.Type.Equality ( (:~:)(..), sym )
import Data.Comp.Multi.Strategy.Classification
subst :: (a :~: b) -> f a -> f b
subst :: (a :~: b) -> f a -> f b
subst Refl x :: f a
x = f a
f b
x
subst2 :: (a :~: b) -> f (g a) -> f (g b)
subst2 :: (a :~: b) -> f (g a) -> f (g b)
subst2 Refl x :: f (g a)
x = f (g a)
f (g b)
x
evalPar :: (HTraversable f) => f l :-> f l
evalPar :: f l :-> f l
evalPar = f l i -> f l i
forall a. a -> a
id
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 :: (MonadPlus m) => RewriteM m f l -> RewriteM (AnyR m) f l
wrapAnyR :: RewriteM m f l -> RewriteM (AnyR m) f l
wrapAnyR f :: RewriteM m f l
f t :: f l
t = (m (f l) -> WriterT Any m (f l)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (RewriteM m f l
f f l
t) WriterT Any m (f l) -> WriterT Any m () -> WriterT Any m (f l)
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Any -> WriterT Any m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (Bool -> Any
Any Bool
True)) WriterT Any m (f l) -> WriterT Any m (f l) -> WriterT Any m (f l)
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` RewriteM (AnyR m) f l
forall (m :: * -> *) a. Monad m => a -> m a
return f l
t
unwrapAnyR :: MonadPlus m => RewriteM (AnyR m) f l -> RewriteM m f l
unwrapAnyR :: RewriteM (AnyR m) f l -> RewriteM m f l
unwrapAnyR f :: RewriteM (AnyR m) f l
f t :: f l
t = do (t' :: f l
t', Any b :: Bool
b) <- WriterT Any m (f l) -> m (f l, Any)
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT (RewriteM (AnyR m) f l
f f l
t)
if Bool
b then
RewriteM m f l
forall (m :: * -> *) a. Monad m => a -> m a
return f l
t'
else
m (f l)
forall (m :: * -> *) a. MonadPlus m => m a
mzero
type OneR m = StateT Bool m
wrapOneR :: (MonadPlus m) => RewriteM m f l -> RewriteM (OneR m) f l
wrapOneR :: RewriteM m f l -> RewriteM (OneR m) f l
wrapOneR f :: RewriteM m f l
f t :: f l
t = do Bool
b <- StateT Bool m Bool
forall s (m :: * -> *). MonadState s m => m s
get
if Bool
b then
RewriteM (OneR m) f l
forall (m :: * -> *) a. Monad m => a -> m a
return f l
t
else
(m (f l) -> StateT Bool m (f l)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (RewriteM m f l
f f l
t) StateT Bool m (f l) -> StateT Bool m () -> StateT Bool m (f l)
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Bool -> StateT Bool m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put Bool
True) StateT Bool m (f l) -> StateT Bool m (f l) -> StateT Bool m (f l)
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` RewriteM (OneR m) f l
forall (m :: * -> *) a. Monad m => a -> m a
return f l
t
unwrapOneR :: MonadPlus m => RewriteM (OneR m) f l -> RewriteM m f l
unwrapOneR :: RewriteM (OneR m) f l -> RewriteM m f l
unwrapOneR f :: RewriteM (OneR m) f l
f t :: f l
t = do (t' :: f l
t', b :: Bool
b) <- StateT Bool m (f l) -> Bool -> m (f l, Bool)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (RewriteM (OneR m) f l
f f l
t) Bool
False
if Bool
b then
RewriteM m f l
forall (m :: * -> *) a. Monad m => a -> m a
return f l
t'
else
m (f l)
forall (m :: * -> *) a. MonadPlus m => m a
mzero
dynamicR :: (DynCase f l, MonadPlus m) => RewriteM m f l -> GRewriteM m f
dynamicR :: RewriteM m f l -> GRewriteM m f
dynamicR f :: RewriteM m f l
f t :: f l
t = case f l -> Maybe (l :~: l)
forall (f :: * -> *) a b. DynCase f a => f b -> Maybe (b :~: a)
dyncase f l
t of
Just p :: l :~: l
p -> (l :~: l) -> m (f l) -> m (f l)
forall a b (f :: * -> *) (g :: * -> *).
(a :~: b) -> f (g a) -> f (g b)
subst2 ((l :~: l) -> l :~: l
forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
sym l :~: l
p) (m (f l) -> m (f l)) -> m (f l) -> m (f l)
forall a b. (a -> b) -> a -> b
$ RewriteM m f l
f ((l :~: l) -> f l -> f l
forall a b (f :: * -> *). (a :~: b) -> f a -> f b
subst l :~: l
p f l
t)
Nothing -> m (f l)
forall (m :: * -> *) a. MonadPlus m => m a
mzero
tryR :: (Monad m) => RewriteM (MaybeT m) f l -> RewriteM m f l
tryR :: RewriteM (MaybeT m) f l -> RewriteM m f l
tryR f :: RewriteM (MaybeT m) f l
f t :: f l
t = (Maybe (f l) -> f l) -> m (Maybe (f l)) -> m (f l)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (f l -> (f l -> f l) -> Maybe (f l) -> f l
forall b a. b -> (a -> b) -> Maybe a -> b
maybe f l
t f l -> f l
forall a. a -> a
id) (m (Maybe (f l)) -> m (f l)) -> m (Maybe (f l)) -> m (f l)
forall a b. (a -> b) -> a -> b
$ MaybeT m (f l) -> m (Maybe (f l))
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (RewriteM (MaybeT m) f l
f f l
t)
failR :: (MonadPlus m) => RewriteM m f l
failR :: RewriteM m f l
failR = m (f l) -> RewriteM m f l
forall a b. a -> b -> a
const m (f l)
forall (m :: * -> *) a. MonadPlus m => m a
mzero
promoteR :: (DynCase f l, Monad m) => RewriteM (MaybeT m) f l -> GRewriteM m f
promoteR :: RewriteM (MaybeT m) f l -> GRewriteM m f
promoteR = RewriteM (MaybeT m) f l -> RewriteM m f l
forall (m :: * -> *) (f :: * -> *) l.
Monad m =>
RewriteM (MaybeT m) f l -> RewriteM m f l
tryR (RewriteM (MaybeT m) f l -> RewriteM m f l)
-> (RewriteM (MaybeT m) f l -> RewriteM (MaybeT m) f l)
-> RewriteM (MaybeT m) f l
-> RewriteM m f l
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RewriteM (MaybeT m) f l -> RewriteM (MaybeT m) f l
forall (f :: * -> *) l (m :: * -> *).
(DynCase f l, MonadPlus m) =>
RewriteM m f l -> GRewriteM m f
dynamicR
promoteRF :: (DynCase f l, Monad m) => RewriteM (MaybeT m) f l -> GRewriteM (MaybeT m) f
promoteRF :: RewriteM (MaybeT m) f l -> GRewriteM (MaybeT m) f
promoteRF = RewriteM (MaybeT m) f l -> RewriteM (MaybeT m) f l
forall (f :: * -> *) l (m :: * -> *).
(DynCase f l, MonadPlus m) =>
RewriteM m f l -> GRewriteM m f
dynamicR
allR :: (Applicative m, HTraversable f) => GRewriteM m (Cxt h f a) -> RewriteM m (Cxt h f a) l
allR :: GRewriteM m (Cxt h f a) -> RewriteM m (Cxt h f a) l
allR f :: GRewriteM m (Cxt h f a)
f h :: Cxt h f a l
h@(Hole _) = RewriteM m (Cxt h f a) l
forall (f :: * -> *) a. Applicative f => a -> f a
pure Cxt h f a l
h
allR f :: GRewriteM m (Cxt h f a)
f (Term t :: f (Cxt h f a) l
t) = (f (Cxt h f a) l -> Cxt h f a l)
-> m (f (Cxt h f a) l) -> m (Cxt h f a l)
forall (f :: * -> *) a b. Applicative f => (a -> b) -> f a -> f b
liftA f (Cxt h f a) l -> Cxt h f a l
forall (f :: (* -> *) -> * -> *) h (a :: * -> *) i.
f (Cxt h f a) i -> Cxt h f a i
Term (m (f (Cxt h f a) l) -> m (Cxt h f a l))
-> m (f (Cxt h f a) l) -> m (Cxt h f a l)
forall a b. (a -> b) -> a -> b
$ GRewriteM m (Cxt h f a) -> NatM m (f (Cxt h f a)) (f (Cxt h f a))
forall (t :: (* -> *) -> * -> *) (f :: * -> *) (a :: * -> *)
(b :: * -> *).
(HTraversable t, Applicative f) =>
NatM f a b -> NatM f (t a) (t b)
htraverse GRewriteM m (Cxt h f a)
f (f (Cxt h f a) l -> m (f (Cxt h f a) l))
-> f (Cxt h f a) l -> m (f (Cxt h f a) l)
forall a b. (a -> b) -> a -> b
$ f (Cxt h f a) l
t
revAllR :: (Applicative m, HTraversable f) => GRewriteM m (Cxt h f a) -> RewriteM m (Cxt h f a) l
revAllR :: GRewriteM m (Cxt h f a) -> RewriteM m (Cxt h f a) l
revAllR f :: GRewriteM m (Cxt h f a)
f h :: Cxt h f a l
h@(Hole _) = RewriteM m (Cxt h f a) l
forall (f :: * -> *) a. Applicative f => a -> f a
pure Cxt h f a l
h
revAllR f :: GRewriteM m (Cxt h f a)
f (Term t :: f (Cxt h f a) l
t) = (f (Cxt h f a) l -> Cxt h f a l)
-> m (f (Cxt h f a) l) -> m (Cxt h f a l)
forall (f :: * -> *) a b. Applicative f => (a -> b) -> f a -> f b
liftA f (Cxt h f a) l -> Cxt h f a l
forall (f :: (* -> *) -> * -> *) h (a :: * -> *) i.
f (Cxt h f a) i -> Cxt h f a i
Term (m (f (Cxt h f a) l) -> m (Cxt h f a l))
-> m (f (Cxt h f a) l) -> m (Cxt h f a l)
forall a b. (a -> b) -> a -> b
$ Backwards m (f (Cxt h f a) l) -> m (f (Cxt h f a) l)
forall k (f :: k -> *) (a :: k). Backwards f a -> f a
forwards (Backwards m (f (Cxt h f a) l) -> m (f (Cxt h f a) l))
-> Backwards m (f (Cxt h f a) l) -> m (f (Cxt h f a) l)
forall a b. (a -> b) -> a -> b
$ NatM (Backwards m) (Cxt h f a) (Cxt h f a)
-> NatM (Backwards m) (f (Cxt h f a)) (f (Cxt h f a))
forall (t :: (* -> *) -> * -> *) (f :: * -> *) (a :: * -> *)
(b :: * -> *).
(HTraversable t, Applicative f) =>
NatM f a b -> NatM f (t a) (t b)
htraverse (m (Cxt h f a i) -> Backwards m (Cxt h f a i)
forall k (f :: k -> *) (a :: k). f a -> Backwards f a
Backwards (m (Cxt h f a i) -> Backwards m (Cxt h f a i))
-> (Cxt h f a i -> m (Cxt h f a i))
-> Cxt h f a i
-> Backwards m (Cxt h f a i)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cxt h f a i -> m (Cxt h f a i)
GRewriteM m (Cxt h f a)
f) (f (Cxt h f a) l -> Backwards m (f (Cxt h f a) l))
-> f (Cxt h f a) l -> Backwards m (f (Cxt h f a) l)
forall a b. (a -> b) -> a -> b
$ f (Cxt h f a) l
t
allStateR :: forall m f s h a l.
(Monad m, HTraversable f)
=> (forall i. s -> Cxt h f a i -> m (Cxt h f a i, s))
-> s
-> RewriteM m (Cxt h f a) l
allStateR :: (forall i. s -> Cxt h f a i -> m (Cxt h f a i, s))
-> s -> RewriteM m (Cxt h f a) l
allStateR f :: forall i. s -> Cxt h f a i -> m (Cxt h f a i, s)
f s :: s
s h :: Cxt h f a l
h@(Hole _) = RewriteM m (Cxt h f a) l
forall (f :: * -> *) a. Applicative f => a -> f a
pure Cxt h f a l
h
allStateR f :: forall i. s -> Cxt h f a i -> m (Cxt h f a i, s)
f s :: s
s (Term t :: f (Cxt h f a) l
t) = (f (Cxt h f a) l -> Cxt h f a l)
-> m (f (Cxt h f a) l) -> m (Cxt h f a l)
forall (f :: * -> *) a b. Applicative f => (a -> b) -> f a -> f b
liftA f (Cxt h f a) l -> Cxt h f a l
forall (f :: (* -> *) -> * -> *) h (a :: * -> *) i.
f (Cxt h f a) i -> Cxt h f a i
Term (m (f (Cxt h f a) l) -> m (Cxt h f a l))
-> m (f (Cxt h f a) l) -> m (Cxt h f a l)
forall a b. (a -> b) -> a -> b
$ StateT s m (f (Cxt h f a) l) -> s -> m (f (Cxt h f a) l)
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (NatM (StateT s m) (Cxt h f a) (Cxt h f a)
-> f (Cxt h f a) l -> StateT s m (f (Cxt h f a) l)
forall (t :: (* -> *) -> * -> *) (f :: * -> *) (a :: * -> *)
(b :: * -> *).
(HTraversable t, Applicative f) =>
NatM f a b -> NatM f (t a) (t b)
htraverse NatM (StateT s m) (Cxt h f a) (Cxt h f a)
f' f (Cxt h f a) l
t) s
s
where
f' :: GRewriteM (StateT s m) (Cxt h f a)
f' :: RewriteM (StateT s m) (Cxt h f a) l
f' x :: Cxt h f a l
x = do s
st <- StateT s m s
forall s (m :: * -> *). MonadState s m => m s
get
(x' :: Cxt h f a l
x', st' :: s
st') <- m (Cxt h f a l, s) -> StateT s m (Cxt h f a l, s)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (Cxt h f a l, s) -> StateT s m (Cxt h f a l, s))
-> m (Cxt h f a l, s) -> StateT s m (Cxt h f a l, s)
forall a b. (a -> b) -> a -> b
$ s -> Cxt h f a l -> m (Cxt h f a l, s)
forall i. s -> Cxt h f a i -> m (Cxt h f a i, s)
f s
st Cxt h f a l
x
s -> StateT s m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put s
st'
RewriteM (StateT s m) (Cxt h f a) l
forall (m :: * -> *) a. Monad m => a -> m a
return Cxt h f a l
x'
allIdxR :: (Monad m, HTraversable f) => (Int -> GRewriteM m (Cxt h f a)) -> RewriteM m (Cxt h f a) l
allIdxR :: (Int -> GRewriteM m (Cxt h f a)) -> RewriteM m (Cxt h f a) l
allIdxR f :: Int -> GRewriteM m (Cxt h f a)
f = (forall i. Int -> Cxt h f a i -> m (Cxt h f a i, Int))
-> Int -> RewriteM m (Cxt h f a) l
forall (m :: * -> *) (f :: (* -> *) -> * -> *) s h (a :: * -> *) l.
(Monad m, HTraversable f) =>
(forall i. s -> Cxt h f a i -> m (Cxt h f a i, s))
-> s -> RewriteM m (Cxt h f a) l
allStateR (\n :: Int
n x :: Cxt h f a i
x -> (,) (Cxt h f a i -> Int -> (Cxt h f a i, Int))
-> m (Cxt h f a i) -> m (Int -> (Cxt h f a i, Int))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> RewriteM m (Cxt h f a) i
Int -> GRewriteM m (Cxt h f a)
f Int
n Cxt h f a i
x m (Int -> (Cxt h f a i, Int)) -> m Int -> m (Cxt h f a i, Int)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Int -> m Int
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1)) 0
(>+>) :: (MonadPlus m) => GRewriteM m f -> GRewriteM m f -> GRewriteM m f
f :: GRewriteM m f
f >+> :: GRewriteM m f -> GRewriteM m f -> GRewriteM m f
>+> g :: GRewriteM m f
g = RewriteM (AnyR m) f l -> RewriteM m f l
forall (m :: * -> *) (f :: * -> *) l.
MonadPlus m =>
RewriteM (AnyR m) f l -> RewriteM m f l
unwrapAnyR (RewriteM m f l -> RewriteM (AnyR m) f l
forall (m :: * -> *) (f :: * -> *) l.
MonadPlus m =>
RewriteM m f l -> RewriteM (AnyR m) f l
wrapAnyR RewriteM m f l
GRewriteM m f
f RewriteM (AnyR m) f l
-> RewriteM (AnyR m) f l -> RewriteM (AnyR m) f l
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> RewriteM m f l -> RewriteM (AnyR m) f l
forall (m :: * -> *) (f :: * -> *) l.
MonadPlus m =>
RewriteM m f l -> RewriteM (AnyR m) f l
wrapAnyR RewriteM m f l
GRewriteM m f
g)
(<+) :: (Alternative m) => RewriteM m f l -> RewriteM m f l -> RewriteM m f l
<+ :: RewriteM m f l -> RewriteM m f l -> RewriteM m f l
(<+) f :: RewriteM m f l
f g :: RewriteM m f l
g x :: f l
x = RewriteM m f l
f f l
x m (f l) -> m (f l) -> m (f l)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> RewriteM m f l
g f l
x
anyR :: (MonadPlus m, HTraversable f) => GRewriteM m (Cxt h f a) -> RewriteM m (Cxt h f a) l
anyR :: GRewriteM m (Cxt h f a) -> RewriteM m (Cxt h f a) l
anyR f :: GRewriteM m (Cxt h f a)
f = RewriteM (AnyR m) (Cxt h f a) l -> RewriteM m (Cxt h f a) l
forall (m :: * -> *) (f :: * -> *) l.
MonadPlus m =>
RewriteM (AnyR m) f l -> RewriteM m f l
unwrapAnyR (RewriteM (AnyR m) (Cxt h f a) l -> RewriteM m (Cxt h f a) l)
-> RewriteM (AnyR m) (Cxt h f a) l -> RewriteM m (Cxt h f a) l
forall a b. (a -> b) -> a -> b
$ GRewriteM (AnyR m) (Cxt h f a) -> RewriteM (AnyR m) (Cxt h f a) l
forall (m :: * -> *) (f :: (* -> *) -> * -> *) h (a :: * -> *) l.
(Applicative m, HTraversable f) =>
GRewriteM m (Cxt h f a) -> RewriteM m (Cxt h f a) l
allR (GRewriteM (AnyR m) (Cxt h f a) -> RewriteM (AnyR m) (Cxt h f a) l)
-> GRewriteM (AnyR m) (Cxt h f a)
-> RewriteM (AnyR m) (Cxt h f a) l
forall a b. (a -> b) -> a -> b
$ RewriteM m (Cxt h f a) l -> RewriteM (AnyR m) (Cxt h f a) l
forall (m :: * -> *) (f :: * -> *) l.
MonadPlus m =>
RewriteM m f l -> RewriteM (AnyR m) f l
wrapAnyR RewriteM m (Cxt h f a) l
GRewriteM m (Cxt h f a)
f
oneR :: (MonadPlus m, HTraversable f) => GRewriteM m (Cxt h f a) -> RewriteM m (Cxt h f a) l
oneR :: GRewriteM m (Cxt h f a) -> RewriteM m (Cxt h f a) l
oneR f :: GRewriteM m (Cxt h f a)
f = RewriteM (OneR m) (Cxt h f a) l -> RewriteM m (Cxt h f a) l
forall (m :: * -> *) (f :: * -> *) l.
MonadPlus m =>
RewriteM (OneR m) f l -> RewriteM m f l
unwrapOneR (RewriteM (OneR m) (Cxt h f a) l -> RewriteM m (Cxt h f a) l)
-> RewriteM (OneR m) (Cxt h f a) l -> RewriteM m (Cxt h f a) l
forall a b. (a -> b) -> a -> b
$ GRewriteM (OneR m) (Cxt h f a) -> RewriteM (OneR m) (Cxt h f a) l
forall (m :: * -> *) (f :: (* -> *) -> * -> *) h (a :: * -> *) l.
(Applicative m, HTraversable f) =>
GRewriteM m (Cxt h f a) -> RewriteM m (Cxt h f a) l
allR (GRewriteM (OneR m) (Cxt h f a) -> RewriteM (OneR m) (Cxt h f a) l)
-> GRewriteM (OneR m) (Cxt h f a)
-> RewriteM (OneR m) (Cxt h f a) l
forall a b. (a -> b) -> a -> b
$ RewriteM m (Cxt h f a) l -> RewriteM (OneR m) (Cxt h f a) l
forall (m :: * -> *) (f :: * -> *) l.
MonadPlus m =>
RewriteM m f l -> RewriteM (OneR m) f l
wrapOneR RewriteM m (Cxt h f a) l
GRewriteM m (Cxt h f a)
f
allbuR :: (Monad m, HTraversable f) => GRewriteM m (Cxt h f a) -> GRewriteM m (Cxt h f a)
allbuR :: GRewriteM m (Cxt h f a) -> GRewriteM m (Cxt h f a)
allbuR f :: GRewriteM m (Cxt h f a)
f = GRewriteM m (Cxt h f a) -> RewriteM m (Cxt h f a) l
forall (m :: * -> *) (f :: (* -> *) -> * -> *) h (a :: * -> *) l.
(Applicative m, HTraversable f) =>
GRewriteM m (Cxt h f a) -> RewriteM m (Cxt h f a) l
allR (GRewriteM m (Cxt h f a) -> GRewriteM m (Cxt h f a)
forall (m :: * -> *) (f :: (* -> *) -> * -> *) h (a :: * -> *).
(Monad m, HTraversable f) =>
GRewriteM m (Cxt h f a) -> GRewriteM m (Cxt h f a)
allbuR GRewriteM m (Cxt h f a)
f) RewriteM m (Cxt h f a) l
-> RewriteM m (Cxt h f a) l -> RewriteM m (Cxt h f a) l
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> RewriteM m (Cxt h f a) l
GRewriteM m (Cxt h f a)
f
revAllbuR :: (Monad m, HTraversable f) => GRewriteM m (Cxt h f a) -> GRewriteM m (Cxt h f a)
revAllbuR :: GRewriteM m (Cxt h f a) -> GRewriteM m (Cxt h f a)
revAllbuR f :: GRewriteM m (Cxt h f a)
f = GRewriteM m (Cxt h f a) -> RewriteM m (Cxt h f a) l
forall (m :: * -> *) (f :: (* -> *) -> * -> *) h (a :: * -> *) l.
(Applicative m, HTraversable f) =>
GRewriteM m (Cxt h f a) -> RewriteM m (Cxt h f a) l
revAllR (GRewriteM m (Cxt h f a) -> GRewriteM m (Cxt h f a)
forall (m :: * -> *) (f :: (* -> *) -> * -> *) h (a :: * -> *).
(Monad m, HTraversable f) =>
GRewriteM m (Cxt h f a) -> GRewriteM m (Cxt h f a)
revAllbuR GRewriteM m (Cxt h f a)
f) RewriteM m (Cxt h f a) l
-> RewriteM m (Cxt h f a) l -> RewriteM m (Cxt h f a) l
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> RewriteM m (Cxt h f a) l
GRewriteM m (Cxt h f a)
f
alltdR :: (Monad m, HTraversable f) => GRewriteM m (Cxt h f a) -> GRewriteM m (Cxt h f a)
alltdR :: GRewriteM m (Cxt h f a) -> GRewriteM m (Cxt h f a)
alltdR f :: GRewriteM m (Cxt h f a)
f = RewriteM m (Cxt h f a) l
GRewriteM m (Cxt h f a)
f RewriteM m (Cxt h f a) l
-> RewriteM m (Cxt h f a) l -> RewriteM m (Cxt h f a) l
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> GRewriteM m (Cxt h f a) -> RewriteM m (Cxt h f a) l
forall (m :: * -> *) (f :: (* -> *) -> * -> *) h (a :: * -> *) l.
(Applicative m, HTraversable f) =>
GRewriteM m (Cxt h f a) -> RewriteM m (Cxt h f a) l
allR (GRewriteM m (Cxt h f a) -> GRewriteM m (Cxt h f a)
forall (m :: * -> *) (f :: (* -> *) -> * -> *) h (a :: * -> *).
(Monad m, HTraversable f) =>
GRewriteM m (Cxt h f a) -> GRewriteM m (Cxt h f a)
alltdR GRewriteM m (Cxt h f a)
f)
anybuR :: (MonadPlus m, HTraversable f) => GRewriteM m (Cxt h f a) -> GRewriteM m (Cxt h f a)
anybuR :: GRewriteM m (Cxt h f a) -> GRewriteM m (Cxt h f a)
anybuR f :: GRewriteM m (Cxt h f a)
f = GRewriteM m (Cxt h f a) -> RewriteM m (Cxt h f a) l
forall (m :: * -> *) (f :: (* -> *) -> * -> *) h (a :: * -> *) l.
(MonadPlus m, HTraversable f) =>
GRewriteM m (Cxt h f a) -> RewriteM m (Cxt h f a) l
anyR (GRewriteM m (Cxt h f a) -> GRewriteM m (Cxt h f a)
forall (m :: * -> *) (f :: (* -> *) -> * -> *) h (a :: * -> *).
(MonadPlus m, HTraversable f) =>
GRewriteM m (Cxt h f a) -> GRewriteM m (Cxt h f a)
anybuR GRewriteM m (Cxt h f a)
f) GRewriteM m (Cxt h f a)
-> GRewriteM m (Cxt h f a) -> GRewriteM m (Cxt h f a)
forall (m :: * -> *) (f :: * -> *).
MonadPlus m =>
GRewriteM m f -> GRewriteM m f -> GRewriteM m f
>+> GRewriteM m (Cxt h f a)
f
anytdR :: (MonadPlus m, HTraversable f) => GRewriteM m (Cxt h f a) -> GRewriteM m (Cxt h f a)
anytdR :: GRewriteM m (Cxt h f a) -> GRewriteM m (Cxt h f a)
anytdR f :: GRewriteM m (Cxt h f a)
f = GRewriteM m (Cxt h f a)
f GRewriteM m (Cxt h f a)
-> GRewriteM m (Cxt h f a) -> GRewriteM m (Cxt h f a)
forall (m :: * -> *) (f :: * -> *).
MonadPlus m =>
GRewriteM m f -> GRewriteM m f -> GRewriteM m f
>+> GRewriteM m (Cxt h f a) -> RewriteM m (Cxt h f a) l
forall (m :: * -> *) (f :: (* -> *) -> * -> *) h (a :: * -> *) l.
(MonadPlus m, HTraversable f) =>
GRewriteM m (Cxt h f a) -> RewriteM m (Cxt h f a) l
anyR (GRewriteM m (Cxt h f a) -> GRewriteM m (Cxt h f a)
forall (m :: * -> *) (f :: (* -> *) -> * -> *) h (a :: * -> *).
(MonadPlus m, HTraversable f) =>
GRewriteM m (Cxt h f a) -> GRewriteM m (Cxt h f a)
anytdR GRewriteM m (Cxt h f a)
f)
prunetdRF :: (MonadPlus m, HTraversable f) => GRewriteM m (Cxt h f a) -> GRewriteM m (Cxt h f a)
prunetdRF :: GRewriteM m (Cxt h f a) -> GRewriteM m (Cxt h f a)
prunetdRF f :: GRewriteM m (Cxt h f a)
f = RewriteM m (Cxt h f a) l
GRewriteM m (Cxt h f a)
f RewriteM m (Cxt h f a) l
-> RewriteM m (Cxt h f a) l -> RewriteM m (Cxt h f a) l
forall (m :: * -> *) (f :: * -> *) l.
Alternative m =>
RewriteM m f l -> RewriteM m f l -> RewriteM m f l
<+ GRewriteM m (Cxt h f a) -> RewriteM m (Cxt h f a) l
forall (m :: * -> *) (f :: (* -> *) -> * -> *) h (a :: * -> *) l.
(MonadPlus m, HTraversable f) =>
GRewriteM m (Cxt h f a) -> RewriteM m (Cxt h f a) l
anyR (GRewriteM m (Cxt h f a) -> GRewriteM m (Cxt h f a)
forall (m :: * -> *) (f :: (* -> *) -> * -> *) h (a :: * -> *).
(MonadPlus m, HTraversable f) =>
GRewriteM m (Cxt h f a) -> GRewriteM m (Cxt h f a)
prunetdRF GRewriteM m (Cxt h f a)
f)
prunetdR :: (Monad m, HTraversable f) => GRewriteM (MaybeT m) (Cxt h f a) -> GRewriteM m (Cxt h f a)
prunetdR :: GRewriteM (MaybeT m) (Cxt h f a) -> GRewriteM m (Cxt h f a)
prunetdR f :: GRewriteM (MaybeT m) (Cxt h f a)
f = RewriteM (MaybeT m) (Cxt h f a) l -> RewriteM m (Cxt h f a) l
forall (m :: * -> *) (f :: * -> *) l.
Monad m =>
RewriteM (MaybeT m) f l -> RewriteM m f l
tryR (GRewriteM (MaybeT m) (Cxt h f a)
-> GRewriteM (MaybeT m) (Cxt h f a)
forall (m :: * -> *) (f :: (* -> *) -> * -> *) h (a :: * -> *).
(MonadPlus m, HTraversable f) =>
GRewriteM m (Cxt h f a) -> GRewriteM m (Cxt h f a)
prunetdRF GRewriteM (MaybeT m) (Cxt h f a)
f)
onebuR :: (MonadPlus m, HTraversable f) => GRewriteM m (Cxt h f a) -> GRewriteM m (Cxt h f a)
onebuR :: GRewriteM m (Cxt h f a) -> GRewriteM m (Cxt h f a)
onebuR f :: GRewriteM m (Cxt h f a)
f = GRewriteM m (Cxt h f a) -> RewriteM m (Cxt h f a) l
forall (m :: * -> *) (f :: (* -> *) -> * -> *) h (a :: * -> *) l.
(MonadPlus m, HTraversable f) =>
GRewriteM m (Cxt h f a) -> RewriteM m (Cxt h f a) l
oneR (GRewriteM m (Cxt h f a) -> GRewriteM m (Cxt h f a)
forall (m :: * -> *) (f :: (* -> *) -> * -> *) h (a :: * -> *).
(MonadPlus m, HTraversable f) =>
GRewriteM m (Cxt h f a) -> GRewriteM m (Cxt h f a)
onebuR GRewriteM m (Cxt h f a)
f) RewriteM m (Cxt h f a) l
-> RewriteM m (Cxt h f a) l -> RewriteM m (Cxt h f a) l
forall (m :: * -> *) (f :: * -> *) l.
Alternative m =>
RewriteM m f l -> RewriteM m f l -> RewriteM m f l
<+ RewriteM m (Cxt h f a) l
GRewriteM m (Cxt h f a)
f
onetdR :: (MonadPlus m, HTraversable f) => GRewriteM m (Cxt h f a) -> GRewriteM m (Cxt h f a)
onetdR :: GRewriteM m (Cxt h f a) -> GRewriteM m (Cxt h f a)
onetdR f :: GRewriteM m (Cxt h f a)
f = RewriteM m (Cxt h f a) l
GRewriteM m (Cxt h f a)
f RewriteM m (Cxt h f a) l
-> RewriteM m (Cxt h f a) l -> RewriteM m (Cxt h f a) l
forall (m :: * -> *) (f :: * -> *) l.
Alternative m =>
RewriteM m f l -> RewriteM m f l -> RewriteM m f l
<+ GRewriteM m (Cxt h f a) -> RewriteM m (Cxt h f a) l
forall (m :: * -> *) (f :: (* -> *) -> * -> *) h (a :: * -> *) l.
(MonadPlus m, HTraversable f) =>
GRewriteM m (Cxt h f a) -> RewriteM m (Cxt h f a) l
oneR (GRewriteM m (Cxt h f a) -> GRewriteM m (Cxt h f a)
forall (m :: * -> *) (f :: (* -> *) -> * -> *) h (a :: * -> *).
(MonadPlus m, HTraversable f) =>
GRewriteM m (Cxt h f a) -> GRewriteM m (Cxt h f a)
onetdR GRewriteM m (Cxt h f a)
f)
idR :: (Applicative m) => RewriteM m f l
idR :: RewriteM m f l
idR = RewriteM m f l
forall (f :: * -> *) a. Applicative f => a -> f a
pure
traceR :: (ShowHF f, KShow a, HTraversable f, Monad m) => RewriteM m (Cxt h f a) l
traceR :: RewriteM m (Cxt h f a) l
traceR x :: Cxt h f a l
x = do
String -> m ()
forall (f :: * -> *). Applicative f => String -> f ()
traceM (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ Cxt h f a l -> String
forall a. Show a => a -> String
show Cxt h f a l
x
RewriteM m (Cxt h f a) l
forall (m :: * -> *) a. Monad m => a -> m a
return Cxt h f a l
x
isSortR :: (MonadPlus m, DynCase f l) => Proxy l -> RewriteM m f l'
isSortR :: Proxy l -> RewriteM m f l'
isSortR p :: Proxy l
p = TranslateM m f l' ()
-> RewriteM m f l' -> RewriteM m f l' -> RewriteM m f l'
forall (m :: * -> *) (f :: * -> *) l t u.
Alternative m =>
TranslateM m f l t
-> TranslateM m f l u -> TranslateM m f l u -> TranslateM m f l u
guardedT (TranslateM m f l' Bool -> TranslateM m f l' ()
forall (m :: * -> *) (f :: * -> *) l.
MonadPlus m =>
TranslateM m f l Bool -> TranslateM m f l ()
guardBoolT (Proxy l -> TranslateM m f l' Bool
forall (f :: * -> *) l (m :: * -> *) l'.
(DynCase f l, Applicative m) =>
Proxy l -> TranslateM m f l' Bool
isSortT Proxy l
p)) RewriteM m f l'
forall (m :: * -> *) (f :: * -> *) l.
Applicative m =>
RewriteM m f l
idR RewriteM m f l'
forall (m :: * -> *) (f :: * -> *) l. MonadPlus m => RewriteM m f l
failR
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
(+>>) :: (Monad m) => TranslateM m f l t -> TranslateM m f l u -> TranslateM m f l u
+>> :: TranslateM m f l t -> TranslateM m f l u -> TranslateM m f l u
(+>>) f :: TranslateM m f l t
f g :: TranslateM m f l u
g t :: f l
t = TranslateM m f l t
f f l
t m t -> m u -> m u
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> TranslateM m f l u
g f l
t
isSortT :: (DynCase f l, Applicative m) => Proxy l -> TranslateM m f l' Bool
isSortT :: Proxy l -> TranslateM m f l' Bool
isSortT p :: Proxy l
p = Bool -> m Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> m Bool) -> (f l' -> Bool) -> TranslateM m f l' Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy l -> forall i. f i -> Bool
forall (e :: * -> *) l.
DynCase e l =>
Proxy l -> forall i. e i -> Bool
isSort Proxy l
p
guardBoolT :: (MonadPlus m) => TranslateM m f l Bool -> TranslateM m f l ()
guardBoolT :: TranslateM m f l Bool -> TranslateM m f l ()
guardBoolT t :: TranslateM m f l Bool
t x :: f l
x = TranslateM m f l Bool
t f l
x m Bool -> (Bool -> m ()) -> m ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Bool -> m ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard
guardedT :: (Alternative m) => TranslateM m f l t -> TranslateM m f l u -> TranslateM m f l u -> TranslateM m f l u
guardedT :: TranslateM m f l t
-> TranslateM m f l u -> TranslateM m f l u -> TranslateM m f l u
guardedT g :: TranslateM m f l t
g t :: TranslateM m f l u
t e :: TranslateM m f l u
e x :: f l
x = (TranslateM m f l t
g f l
x m t -> m u -> m u
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> TranslateM m f l u
t f l
x) m u -> m u -> m u
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (TranslateM m f l u
e f l
x)
failT :: (Alternative m) => TranslateM m f l t
failT :: TranslateM m f l t
failT = m t -> TranslateM m f l t
forall a b. a -> b -> a
const m t
forall (f :: * -> *) a. Alternative f => f a
empty
notT :: (Alternative m) => TranslateM m f l t -> RewriteM m f l
notT :: TranslateM m f l t -> RewriteM m f l
notT t :: TranslateM m f l t
t = TranslateM m f l t
-> RewriteM m f l -> RewriteM m f l -> RewriteM m f l
forall (m :: * -> *) (f :: * -> *) l t u.
Alternative m =>
TranslateM m f l t
-> TranslateM m f l u -> TranslateM m f l u -> TranslateM m f l u
guardedT TranslateM m f l t
t RewriteM m f l
forall (m :: * -> *) (f :: * -> *) l t.
Alternative m =>
TranslateM m f l t
failT RewriteM m f l
forall (m :: * -> *) (f :: * -> *) l.
Applicative m =>
RewriteM m f l
idR
promoteTF :: (DynCase f l, Alternative m) => TranslateM m f l t -> GTranslateM m f t
promoteTF :: TranslateM m f l t -> GTranslateM m f t
promoteTF f :: TranslateM m f l t
f t :: f l
t = case f l -> Maybe (l :~: l)
forall (f :: * -> *) a b. DynCase f a => f b -> Maybe (b :~: a)
dyncase f l
t of
Just p :: l :~: l
p -> TranslateM m f l t
f ((l :~: l) -> f l -> f l
forall a b (f :: * -> *). (a :~: b) -> f a -> f b
subst l :~: l
p f l
t)
Nothing -> m t
forall (f :: * -> *) a. Alternative f => f a
empty
addFail :: Monad m => TranslateM m f l t -> TranslateM (MaybeT m) f l t
addFail :: TranslateM m f l t -> TranslateM (MaybeT m) f l t
addFail = (m t -> MaybeT m t
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m t -> MaybeT m t)
-> TranslateM m f l t -> TranslateM (MaybeT m) f l t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. )
mtryM :: (Monad m, Monoid a) => MaybeT m a -> m a
mtryM :: MaybeT m a -> m a
mtryM = (Maybe a -> a) -> m (Maybe a) -> m a
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (a -> (a -> a) -> Maybe a -> a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe a
forall a. Monoid a => a
mempty a -> a
forall a. a -> a
id) (m (Maybe a) -> m a)
-> (MaybeT m a -> m (Maybe a)) -> MaybeT m a -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MaybeT m a -> m (Maybe a)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT
onetdT :: (MonadPlus m, HFoldable f) => GTranslateM m (HFix f) t -> GTranslateM m (HFix f) t
onetdT :: GTranslateM m (HFix f) t -> GTranslateM m (HFix f) t
onetdT t :: GTranslateM m (HFix f) t
t = GTranslateM m (HFix f) t
-> (m t -> m t -> m t) -> GTranslateM m (HFix f) t
forall (f :: (* -> *) -> * -> *) r.
HFoldable f =>
(HFix f :=> r) -> (r -> r -> r) -> HFix f :=> r
query GTranslateM m (HFix f) t
t m t -> m t -> m t
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus
parQuery :: forall r f. HFoldable f => (HFix f :=> r) -> (r -> r -> r) -> HFix f :=> r
parQuery :: (HFix f :=> r) -> (r -> r -> r) -> HFix f :=> r
parQuery q :: HFix f :=> r
q c :: r -> r -> r
c tree :: HFix f i
tree = Eval r -> r
forall a. Eval a -> a
runEval (Eval r -> r) -> Eval r -> r
forall a b. (a -> b) -> a -> b
$ Int -> HFix f i -> Eval r
Int -> HFix f :=> Eval r
rec 8 HFix f i
tree
where
rec :: Int -> HFix f :=> Eval r
rec :: Int -> HFix f :=> Eval r
rec 0 i :: HFix f i
i = Strategy r
forall a. Strategy a
rpar Strategy r -> Strategy r
forall a b. (a -> b) -> a -> b
$ (HFix f :=> r) -> (r -> r -> r) -> HFix f i -> r
forall (f :: (* -> *) -> * -> *) r.
HFoldable f =>
(HFix f :=> r) -> (r -> r -> r) -> HFix f :=> r
query HFix f :=> r
q r -> r -> r
c HFix f i
i
rec depth :: Int
depth i :: HFix f i
i@(Term t :: f (HFix f) i
t) = (Eval r -> HFix f :=> Eval r) -> Eval r -> f (HFix f) i -> Eval r
forall (h :: (* -> *) -> * -> *) b (a :: * -> *).
HFoldable h =>
(b -> a :=> b) -> b -> h a :=> b
hfoldl (\s :: Eval r
s x :: Cxt NoHole f (K ()) i
x -> (r -> r -> r) -> Eval r -> Eval r -> Eval r
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 r -> r -> r
c Eval r
s (Int -> Cxt NoHole f (K ()) i -> Eval r
Int -> HFix f :=> Eval r
rec (Int
depthInt -> Int -> Int
forall a. Num a => a -> a -> a
-1) Cxt NoHole f (K ()) i
x)) (Strategy r
forall a. Strategy a
rpar Strategy r -> Strategy r
forall a b. (a -> b) -> a -> b
$ HFix f i -> r
HFix f :=> r
q HFix f i
i) f (HFix f) i
t
foldT :: (HFoldable f, Monoid t, Applicative m) => GTranslateM m (HFix f) t -> TranslateM m (HFix f) l t
foldT :: GTranslateM m (HFix f) t -> TranslateM m (HFix f) l t
foldT t :: GTranslateM m (HFix f) t
t (Term tree :: f (HFix f) l
tree) = (m t -> GTranslateM m (HFix f) t) -> m t -> f (HFix f) l -> m t
forall (h :: (* -> *) -> * -> *) b (a :: * -> *).
HFoldable h =>
(b -> a :=> b) -> b -> h a :=> b
hfoldl (\s :: m t
s x :: Cxt NoHole f (K ()) i
x -> (t -> t -> t) -> m t -> m t -> m t
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 t -> t -> t
forall a. Monoid a => a -> a -> a
mappend m t
s (TranslateM m (HFix f) i t
GTranslateM m (HFix f) t
t Cxt NoHole f (K ()) i
x)) (t -> m t
forall (f :: * -> *) a. Applicative f => a -> f a
pure t
forall a. Monoid a => a
mempty) f (HFix f) l
tree
foldtdT :: (HFoldable f, Monoid t, Monad m) => GTranslateM m (HFix f) t -> GTranslateM m (HFix f) t
foldtdT :: GTranslateM m (HFix f) t -> GTranslateM m (HFix f) t
foldtdT t :: GTranslateM m (HFix f) t
t = GTranslateM m (HFix f) t
-> (m t -> m t -> m t) -> GTranslateM m (HFix f) t
forall r (f :: (* -> *) -> * -> *).
HFoldable f =>
(HFix f :=> r) -> (r -> r -> r) -> HFix f :=> r
parQuery GTranslateM m (HFix f) t
t ((t -> t -> t) -> m t -> m t -> m t
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 t -> t -> t
forall a. Monoid a => a -> a -> a
mappend)
crushtdT :: (HFoldable f, Monoid t, Monad m) => GTranslateM (MaybeT m) (HFix f) t -> GTranslateM m (HFix f) t
crushtdT :: GTranslateM (MaybeT m) (HFix f) t -> GTranslateM m (HFix f) t
crushtdT f :: GTranslateM (MaybeT m) (HFix f) t
f = GTranslateM m (HFix f) t -> TranslateM m (HFix f) l t
forall (f :: (* -> *) -> * -> *) t (m :: * -> *).
(HFoldable f, Monoid t, Monad m) =>
GTranslateM m (HFix f) t -> GTranslateM m (HFix f) t
foldtdT (GTranslateM m (HFix f) t -> TranslateM m (HFix f) l t)
-> GTranslateM m (HFix f) t -> TranslateM m (HFix f) l t
forall a b. (a -> b) -> a -> b
$ MaybeT m t -> m t
forall (m :: * -> *) a. (Monad m, Monoid a) => MaybeT m a -> m a
mtryM (MaybeT m t -> m t) -> (HFix f l -> MaybeT m t) -> HFix f l -> m t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HFix f l -> MaybeT m t
GTranslateM (MaybeT m) (HFix f) t
f