{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}

-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Comp.Multi.Strategic
-- Copyright   :  James Koppel, 2013
-- License     :  BSD-style (see the LICENSE file in the distribution)
--
-- Strategy combinators for cubix-compdata. Older versions of this package were built for vanilla compdata.
--
-- Strategy combinators are functions that build more complicated traversals
-- out of smaller (perhaps single-node) traversals. The name comes from the idea of a
-- rewriting strategy, an algorithm for choosing how to apply a set of rewrite rules.
-- For a tutorial introduction to strategy combinators, see:
--
-- * \"The Essence of Strategic Programming\", Ralf Lämmel et al, online
--    at https://eelcovisser.org/publications/2002/LaemmelVV02.pdf
--
-- Functions in this module have a particular naming schema:
--
--
-- * Suffix @R@ (e.g.: `anybuR`): Short for \"rewrite\". It means the function is type-preserving
--   (rewrites a term to another term of the same sort).
--
-- * Suffix @T@ (e.g.: `onetdT`): Short for \"translate\". It means the function rewrites a tree to a fixed type.
--
-- * Suffix @F@ (e.g.: `promoteTF`): Short for \"failable\". This denotes combinators whose result is a rewrite in the
--   `Maybe` monad.
--
-- * @td@ (e.g.: `crushtdT`): Short for \"top-down traversal\"
--
-- * @bu@ (e.g.: `anybuR`): Short for \"bottom-up traversal\"
--
-- The design (and naming system) of `compstrat` is heavily inspired by an older library of strategy combinators,
-- KURE, https://hackage.haskell.org/package/kure
--
-----------------------------------------------------------------------------

module Data.Comp.Multi.Strategic
  (
    -- * Rewrites
    -- ** Core types
    RewriteM
  , Rewrite
  , GRewriteM
  , GRewrite

  -- ** Rewrite combinators for failure
  , addFail
  , tryR
  , failR

  -- ** Rewrite combinators for sorts
  , dynamicR
  , promoteR
  , promoteRF

  -- ** Sequential combination of rewrites
  , (>+>)
  , (<+)

  -- ** One-level traversal combinators
  , allR
  , revAllR
  , anyR
  , oneR
  , allStateR
  , allIdxR

  -- ** Whole-term traversals
  , alltdR
  , allbuR
  , anytdR
  , anybuR
  , revAllbuR
  , prunetdRF
  , prunetdR
  , onetdR
  , onebuR

  , idR
  , traceR
  , isSortR

    -- * Translations
    -- ** Core types
  , Translate
  , TranslateM
  , GTranslateM

    -- ** Conditions
  , guardBoolT
  , guardedT

    -- ** Traversals
  , 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

--------------------------------------------------------------------------------

-- Porting from the old type-equality library to the new base Data.Type.Equality
-- Haven't yet looked into rewriting with gcastWith instead

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 = withStrategy (htraverse id)
evalPar :: f l :-> f l
evalPar = f l i -> f l i
forall a. a -> a
id

--------------------------------------------------------------------------------

-- | The basic type of rewrites. A @RewriteM m f l@ rewrites a term
--   of signature @f@, sort @l@, to another such term, with effects in monad @m@
--
-- @Rewrite m f l@ is equivalent to @`TranslateM` m f l (f l)@.
type RewriteM m f l = f l -> m (f l)

-- | A rewrite with no effects
type Rewrite f l = RewriteM Identity f l

-- | An effectful rewrite that runs on terms of any sort
type GRewriteM m f = forall l. RewriteM m f l

-- | A rewrite that runs on terms of any sort and has no effects
type GRewrite f = GRewriteM Identity f

--------------------------------------------------------------------------------
-- Rewrites
--------------------------------------------------------------------------------

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

--------------------------------------------------------------------------------

-- | Turns a rewrite that runs on a single sort to one that runs on any sort,
--   failing for all other sorts.
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

-- | Turns a rewrite that may fail into one that unconditionally succeeds, replacing
--   failures with identity.
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)

-- | The rewrite that always fails
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

-- | Turns a failable rewrite on one sort @l@ into a rewrite that always succeeds, and runs on any sort,
--   performing the identity rewrite on terms of sort other than @l@. Defined @`tryR` . `dynamicR`@
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

-- | Turns a rewrite that runs on a single sort to one that runs on any sort,
--   failing for all other sorts. Equivalent to `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

-- | Applies a rewrite to all immediate subterms of the current term.
--   Ignores holes.
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
--allR f t = liftA Term $ evalPar $ htraverse f $ unTerm t

-- Ignores holes
-- | Like `allR`, but runs on the children in reverse order
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

-- | Runs a stateful computation on all immediate children of the current term.
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)) -- ^ A stateful computation
            -> s                                                  -- ^ The start state
            -> 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'


-- | Let @f@ be a rewrite with an extra `Int` parameter, intended to be called @f i t@, where @t@
--   is a term and @i@ is the index of @t@ among its parent's children. Then @allIdxR f x@ runs
--   @f@ on all children of @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


-- | Applies two rewrites in suceesion, succeeding if one or both succeed
(>+>) :: (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)

-- | Left-biased choice -- (f <+ g) runs f, and, if it fails, then runs 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

-- | Applies a rewrite to all immediate subterms of the current term, succeeding if any succeed
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 -- not point-free because of type inference

-- | Applies a rewrite to the first immediate subterm of the current term where it can succeed
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 -- not point-free because of type inference

-- | Runs a rewrite in a bottom-up traversal. Defined:
--   @
--       allbuR f = `allR` (allbuR f) >=> 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


-- | Like `allbuR`, but runs in right-to-left order
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

-- | Runs a rewrite in a top-down traversal Defined:
--   @
--       alltdR f = f >=> allR (alltdR 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)

-- | Runs a rewrite in a bottom-up traversal, succeeding if any succeed. Defined:
--    @
--      anybuR f = anyR (anybuR f) >+> 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

-- | Runs a rewrite in a top-down traversal, succeeding if any succeed. Defined:
--    @
--      anytdR f = f >+> anyR (anytdR 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)

-- | Runs a rewrite in a top-down traversal, succeeding if any succeed, and pruning below successes. Defined:
--    @
--       prunetdRF f = f <+ anyR (prunetdRF 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)

-- | Like `prunetdRF`, but the outer level always succeeds. Defined @`tryR` . `prunetdRF`@
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)

-- | Applies a rewrite to the first node where it can succeed in a bottom-up traversal. Defined:
--    @
--      onebuR f = oneR (onebuR f) <+ 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

-- | Applies a rewrite to the first node where it can succeed in a top-down traversal. Defined:
--    @
--      onetdR f = f <+ oneR (onetdR 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)

-- | The identity rewrite
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

-- | Wraps a rewrite with one that performs a debug-print of each visited node
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 (Proxy :: Proxy l)@ performs the identity rewrite at terms of sort @l@,
--   and fails for all other terms.
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

--------------------------------------------------------------------------------
-- Translations
--------------------------------------------------------------------------------

-- | A single-sorted translation in the Identity monad
type Translate f l t = TranslateM Identity f l t

-- | A monadic translation for a single sort
type TranslateM m f l t = f l -> m t

-- | A monadic translation for all sorts
type GTranslateM m f t = forall l. TranslateM m f l t

-- | @f <+> g@ runs @f@ and @g@ in sequence, ignoring the output of @f@, and returning the output of @g@.
(+>>) :: (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 (Proxy :: Proxy l)@ is the translate that succeeds for terms of sort @l@, and fails elsewhere
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

-- | Takes a boolean function of a term, and converts `False` values to failure in the monad
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

-- | Guarded choice: @guardedT g t e@ runs @t@ (\"then branch\") on its input if @g@ succeeds, and otherwise runs @e@
--   (\"else branch\")
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)

-- | The translation that always fails
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

-- FIXME: This is apparently broken
-- | Takes a translation, and replaces success with failure, and replaces failure with the identity rewrite
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

-- | Allows a one-sorted translation to be applied to any sort, failing at sorts
--   different form the original
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

-- | Lifts a translation into the Maybe monad, allowing it to fail
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
. )

-- | Runs a failable computation, replacing failure with `mempty`
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

-- | Runs a translation in a top-down manner, combining its effects. Succeeds if any succeeds.
--   When run using MaybeT, returns its result for the last node where it succeded
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

-- | Runs a translation on each node which returns a value in some monoid, and combines the results.
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

-- | Fold a tree in a top-down manner. Includes some rudimentary parallelism.
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)

-- | An always successful top-down fold, replacing failures with `mempty`.
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