{-# LANGUAGE AllowAmbiguousTypes #-} -- For isSortR and isSortT
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# 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
  , pruningCrushtdTF
  , pruningCrushtdT
  , maximalSubterms

  , (+>>)
  , 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, runIdentity )
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.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 :: forall a b (f :: * -> *). (a :~: b) -> f a -> f b
subst a :~: b
Refl f a
x = f a
f b
x

subst2 :: (a :~: b) -> f (g a) -> f (g b)
subst2 :: forall a b (f :: * -> *) (g :: * -> *).
(a :~: b) -> f (g a) -> f (g b)
subst2 a :~: b
Refl f (g a)
x = f (g a)
f (g b)
x

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

evalPar :: (HTraversable f) => f l :-> f l
--evalPar = withStrategy (htraverse id)
evalPar :: forall (f :: (* -> *) -> * -> *) (l :: * -> *).
HTraversable f =>
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 :: forall (m :: * -> *) (f :: * -> *) l.
MonadPlus m =>
RewriteM m f l -> RewriteM (AnyR m) f l
wrapAnyR RewriteM m f l
f f l
t = (m (f l) -> WriterT Any m (f l)
forall (m :: * -> *) a. Monad m => m a -> WriterT Any m a
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 a b. WriterT Any m a -> WriterT Any m b -> WriterT Any m a
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 a. WriterT Any m a -> WriterT Any m a -> WriterT Any m a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` f l -> WriterT Any m (f l)
forall a. a -> WriterT Any m a
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 :: forall (m :: * -> *) (f :: * -> *) l.
MonadPlus m =>
RewriteM (AnyR m) f l -> RewriteM m f l
unwrapAnyR RewriteM (AnyR m) f l
f f l
t = do (f l
t', Any 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
                      f l -> m (f l)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return f l
t'
                     else
                      m (f l)
forall a. m a
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 :: forall (m :: * -> *) (f :: * -> *) l.
MonadPlus m =>
RewriteM m f l -> RewriteM (OneR m) f l
wrapOneR RewriteM m f l
f f l
t = do Bool
b <- StateT Bool m Bool
forall s (m :: * -> *). MonadState s m => m s
get
                  if Bool
b then
                    f l -> OneR m (f l)
forall a. a -> StateT Bool m a
forall (m :: * -> *) a. Monad m => a -> m a
return f l
t
                   else
                    (m (f l) -> OneR m (f l)
forall (m :: * -> *) a. Monad m => m a -> StateT Bool m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (RewriteM m f l
f f l
t) OneR m (f l) -> StateT Bool m () -> OneR m (f l)
forall a b. StateT Bool m a -> StateT Bool m b -> StateT Bool m a
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) OneR m (f l) -> OneR m (f l) -> OneR m (f l)
forall a. StateT Bool m a -> StateT Bool m a -> StateT Bool m a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` f l -> OneR m (f l)
forall a. a -> StateT Bool m a
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 :: forall (m :: * -> *) (f :: * -> *) l.
MonadPlus m =>
RewriteM (OneR m) f l -> RewriteM m f l
unwrapOneR RewriteM (OneR m) f l
f f l
t = do (f l
t', 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
                      f l -> m (f l)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return f l
t'
                     else
                      m (f l)
forall a. m a
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 :: forall (f :: * -> *) l (m :: * -> *).
(DynCase f l, MonadPlus m) =>
RewriteM m f l -> GRewriteM m f
dynamicR RewriteM m f l
f f l
t = case f l -> Maybe (l :~: l)
forall b. f b -> Maybe (b :~: l)
forall (f :: * -> *) a b. DynCase f a => f b -> Maybe (b :~: a)
dyncase f l
t of
                 Just 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)
                 Maybe (l :~: l)
Nothing -> m (f l)
forall a. m a
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 :: forall (m :: * -> *) (f :: * -> *) l.
Monad m =>
RewriteM (MaybeT m) f l -> RewriteM m f l
tryR RewriteM (MaybeT m) f l
f 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 :: forall (m :: * -> *) (f :: * -> *) l. MonadPlus m => RewriteM m f l
failR = m (f l) -> f l -> m (f l)
forall a b. a -> b -> a
const m (f l)
forall a. m a
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 :: forall (f :: * -> *) l (m :: * -> *).
(DynCase f l, Monad m) =>
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
RewriteM (MaybeT m) f l -> GRewriteM (MaybeT m) f
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 :: forall (f :: * -> *) l (m :: * -> *).
(DynCase f l, Monad m) =>
RewriteM (MaybeT m) f l -> GRewriteM (MaybeT m) f
promoteRF = RewriteM (MaybeT m) f l -> RewriteM (MaybeT m) f l
RewriteM (MaybeT m) f l -> GRewriteM (MaybeT m) f
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 :: 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)
f h :: Cxt h f a l
h@(Hole a l
_) = Cxt h f a l -> m (Cxt h f a l)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Cxt h f a l
h
allR GRewriteM m (Cxt h f a)
f   (Term 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 (f :: * -> *) (a :: * -> *) (b :: * -> *).
Applicative f =>
NatM f a b -> NatM f (f a) (f b)
forall (t :: (* -> *) -> * -> *) (f :: * -> *) (a :: * -> *)
       (b :: * -> *).
(HTraversable t, Applicative f) =>
NatM f a b -> NatM f (t a) (t b)
htraverse RewriteM m (Cxt h f a) i
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 :: 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)
f h :: Cxt h f a l
h@(Hole a l
_) = Cxt h f a l -> m (Cxt h f a l)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Cxt h f a l
h
revAllR GRewriteM m (Cxt h f a)
f   (Term 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 (f :: * -> *) (a :: * -> *) (b :: * -> *).
Applicative f =>
NatM f a b -> NatM f (f a) (f b)
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 (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)
f s
s h :: Cxt h f a l
h@(Hole a l
_) = Cxt h f a l -> m (Cxt h f a l)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Cxt h f a l
h
allStateR forall i. s -> Cxt h f a i -> m (Cxt h f a i, s)
f s
s   (Term 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)
-> NatM (StateT s m) (f (Cxt h f a)) (f (Cxt h f a))
forall (f :: * -> *) (a :: * -> *) (b :: * -> *).
Applicative f =>
NatM f a b -> NatM f (f a) (f b)
forall (t :: (* -> *) -> * -> *) (f :: * -> *) (a :: * -> *)
       (b :: * -> *).
(HTraversable t, Applicative f) =>
NatM f a b -> NatM f (t a) (t b)
htraverse RewriteM (StateT s m) (Cxt h f a) i
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' :: NatM (StateT s m) (Cxt h f a) (Cxt h f a)
f' Cxt h f a l
x = do s
st <- StateT s m s
forall s (m :: * -> *). MonadState s m => m s
get
              (Cxt h f a l
x', s
st') <- m (Cxt h f a l, s) -> StateT s m (Cxt h f a l, s)
forall (m :: * -> *) a. Monad m => m a -> StateT s m a
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'
              Cxt h f a l -> StateT s m (Cxt h f a l)
forall a. a -> StateT s m a
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 :: forall (m :: * -> *) (f :: (* -> *) -> * -> *) h (a :: * -> *) l.
(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)
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 (\Int
n 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 -> 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 a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Int -> m Int
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)) Int
0


-- | Applies two rewrites in suceesion, succeeding if one or both succeed
(>+>) :: (MonadPlus m) => GRewriteM m f -> GRewriteM m f -> GRewriteM m f
GRewriteM m f
f >+> :: forall (m :: * -> *) (f :: * -> *).
MonadPlus m =>
GRewriteM m f -> GRewriteM m f -> GRewriteM m f
>+> GRewriteM m f
g = RewriteM (WriterT Any 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 (WriterT Any 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 (WriterT Any m) f l
-> RewriteM (WriterT Any m) f l -> RewriteM (WriterT Any m) f l
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> RewriteM m f l -> RewriteM (WriterT Any 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) => TranslateM m f l t -> TranslateM m f l t -> TranslateM m f l t
<+ :: forall (m :: * -> *) (f :: * -> *) l t.
Alternative m =>
TranslateM m f l t -> TranslateM m f l t -> TranslateM m f l t
(<+) TranslateM m f l t
f TranslateM m f l t
g f l
x = TranslateM m f l t
f f l
x m t -> m t -> m t
forall a. m a -> m a -> m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> TranslateM m f l t
g f l
x

-- | Applies a rewrite to all immediate subterms of the current term, succeeding if any succeed
--   Ignores holes.
anyR :: (MonadPlus m, HTraversable f) => GRewriteM m (Cxt h f a) -> RewriteM m (Cxt h f a) l
anyR :: 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)
f = RewriteM (WriterT Any 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 (WriterT Any m) (Cxt h f a) l
 -> RewriteM m (Cxt h f a) l)
-> RewriteM (WriterT Any m) (Cxt h f a) l
-> RewriteM m (Cxt h f a) l
forall a b. (a -> b) -> a -> b
$ GRewriteM (WriterT Any m) (Cxt h f a)
-> RewriteM (WriterT Any 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 (WriterT Any m) (Cxt h f a)
 -> RewriteM (WriterT Any m) (Cxt h f a) l)
-> GRewriteM (WriterT Any m) (Cxt h f a)
-> RewriteM (WriterT Any m) (Cxt h f a) l
forall a b. (a -> b) -> a -> b
$ RewriteM m (Cxt h f a) l -> RewriteM (WriterT Any 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
--   Ignores holes.
oneR :: (MonadPlus m, HTraversable f) => GRewriteM m (Cxt h f a) -> RewriteM m (Cxt h f a) l
oneR :: 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)
f = RewriteM (StateT Bool 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 (StateT Bool m) (Cxt h f a) l
 -> RewriteM m (Cxt h f a) l)
-> RewriteM (StateT Bool m) (Cxt h f a) l
-> RewriteM m (Cxt h f a) l
forall a b. (a -> b) -> a -> b
$ GRewriteM (StateT Bool m) (Cxt h f a)
-> RewriteM (StateT Bool 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 (StateT Bool m) (Cxt h f a)
 -> RewriteM (StateT Bool m) (Cxt h f a) l)
-> GRewriteM (StateT Bool m) (Cxt h f a)
-> RewriteM (StateT Bool m) (Cxt h f a) l
forall a b. (a -> b) -> a -> b
$ RewriteM m (Cxt h f a) l -> RewriteM (StateT Bool 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
--   @
--   Ignores holes.
allbuR :: (Monad m, HTraversable f) => GRewriteM m (Cxt h f a) -> GRewriteM m (Cxt h f a)
allbuR :: 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 = 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 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
>=> 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 :: 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 = 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 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
>=> 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)
--   @
--
--   Ignores holes.
alltdR :: (Monad m, HTraversable f) => GRewriteM m (Cxt h f a) -> GRewriteM m (Cxt h f a)
alltdR :: 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 = 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 RewriteM m (Cxt h f a) l
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
--    @
--
--   Ignores holes.
anybuR :: (MonadPlus m, HTraversable f) => GRewriteM m (Cxt h f a) -> GRewriteM m (Cxt h f a)
anybuR :: 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) -> 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 RewriteM m (Cxt h f a) l
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
>+> RewriteM m (Cxt h f a) l
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 :: 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 = RewriteM m (Cxt h f a) l
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 RewriteM m (Cxt h f a) l
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)
--    @
--
--   Ignores holes.
prunetdRF :: (MonadPlus m, HTraversable f) => GRewriteM m (Cxt h f a) -> GRewriteM m (Cxt h f a)
prunetdRF :: 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 = 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 t.
Alternative m =>
TranslateM m f l t -> TranslateM m f l t -> TranslateM m f l t
<+ 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 RewriteM m (Cxt h f a) l
GRewriteM m (Cxt h f a)
f)

-- | Like `prunetdRF`, but the outer level always succeeds. Defined @`tryR` . `prunetdRF`@
--   Ignores holes.
prunetdR :: (Monad m, HTraversable f) => GRewriteM (MaybeT m) (Cxt h f a) -> GRewriteM m (Cxt h f a)
prunetdR :: forall (m :: * -> *) (f :: (* -> *) -> * -> *) h (a :: * -> *).
(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)
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 RewriteM (MaybeT m) (Cxt h f a) l
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
--    @
--
--   Ignores holes.
onebuR :: (MonadPlus m, HTraversable f) => GRewriteM m (Cxt h f a) -> GRewriteM m (Cxt h f a)
onebuR :: 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 = 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 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 t.
Alternative m =>
TranslateM m f l t -> TranslateM m f l t -> TranslateM m f l t
<+ 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)
--    @
-- 
--   Ignores holes.
onetdR :: (MonadPlus m, HTraversable f) => GRewriteM m (Cxt h f a) -> GRewriteM m (Cxt h f a)
onetdR :: 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 = 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 t.
Alternative m =>
TranslateM m f l t -> TranslateM m f l t -> TranslateM m f l t
<+ 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 RewriteM m (Cxt h f a) l
GRewriteM m (Cxt h f a)
f)

-- | The identity rewrite
idR :: (Applicative m) => RewriteM m f l
idR :: forall (m :: * -> *) (f :: * -> *) l.
Applicative m =>
RewriteM m f l
idR = f l -> m (f l)
forall a. a -> m a
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 :: forall (f :: (* -> *) -> * -> *) (a :: * -> *) (m :: * -> *) h l.
(ShowHF f, KShow a, HTraversable f, Monad m) =>
RewriteM m (Cxt h f a) l
traceR 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
  Cxt h f a l -> m (Cxt h f a l)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Cxt h f a l
x

-- | @isSortR \@l@ performs the identity rewrite at terms of sort @l@,
--   and fails for all other terms.
isSortR :: forall l l' f m. (MonadPlus m, DynCase f l) => RewriteM m f l'
isSortR :: forall l l' (f :: * -> *) (m :: * -> *).
(MonadPlus m, DynCase f l) =>
RewriteM m f l'
isSortR = TranslateM m f l' ()
-> TranslateM m f l' (f l')
-> TranslateM m f l' (f l')
-> TranslateM m f l' (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 (forall l l' (f :: * -> *) (m :: * -> *).
(DynCase f l, Applicative m) =>
TranslateM m f l' Bool
isSortT @l)) TranslateM m f l' (f l')
forall (m :: * -> *) (f :: * -> *) l.
Applicative m =>
RewriteM m f l
idR TranslateM m f l' (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
+>> :: forall (m :: * -> *) (f :: * -> *) l t u.
Monad m =>
TranslateM m f l t -> TranslateM m f l u -> TranslateM m f l u
(+>>) TranslateM m f l t
f TranslateM m f l u
g f l
t = TranslateM m f l t
f f l
t m t -> m u -> m u
forall a b. m a -> m b -> m b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> TranslateM m f l u
g f l
t

-- | @isSortT \@l@ is the translate that succeeds for terms of sort @l@, and fails elsewhere
isSortT :: forall l l' f m. (DynCase f l, Applicative m) => TranslateM m f l' Bool
isSortT :: forall l l' (f :: * -> *) (m :: * -> *).
(DynCase f l, Applicative m) =>
TranslateM m f l' Bool
isSortT = Bool -> m Bool
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> m Bool) -> (f l' -> Bool) -> f l' -> m Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l (e :: * -> *) i. DynCase e l => e i -> Bool
isSort @l

-- | 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 :: forall (m :: * -> *) (f :: * -> *) l.
MonadPlus m =>
TranslateM m f l Bool -> TranslateM m f l ()
guardBoolT TranslateM m f l Bool
t f l
x = TranslateM m f l Bool
t f l
x m Bool -> (Bool -> m ()) -> m ()
forall a b. m a -> (a -> m b) -> m b
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 :: 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
g TranslateM m f l u
t TranslateM m f l u
e f l
x = (TranslateM m f l t
g f l
x m t -> m u -> m u
forall a b. m a -> m b -> m b
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 a. m a -> m a -> m a
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 :: forall (m :: * -> *) (f :: * -> *) l t.
Alternative m =>
TranslateM m f l t
failT = m t -> f l -> m t
forall a b. a -> b -> a
const m t
forall a. m a
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 :: forall (m :: * -> *) (f :: * -> *) l t.
Alternative m =>
TranslateM m f l t -> RewriteM m f l
notT TranslateM m f l t
t = TranslateM m f l t
-> TranslateM m f l (f l)
-> TranslateM m f l (f l)
-> TranslateM m f l (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 TranslateM m f l (f l)
forall (m :: * -> *) (f :: * -> *) l t.
Alternative m =>
TranslateM m f l t
failT TranslateM m f l (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 :: forall (f :: * -> *) l (m :: * -> *) t.
(DynCase f l, Alternative m) =>
TranslateM m f l t -> GTranslateM m f t
promoteTF TranslateM m f l t
f f l
t = case f l -> Maybe (l :~: l)
forall b. f b -> Maybe (b :~: l)
forall (f :: * -> *) a b. DynCase f a => f b -> Maybe (b :~: a)
dyncase f l
t of
                  Just 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)
                  Maybe (l :~: l)
Nothing -> m t
forall a. m a
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 :: forall (m :: * -> *) (f :: * -> *) l t.
Monad m =>
TranslateM m f l t -> TranslateM (MaybeT m) f l t
addFail = (m t -> MaybeT m t
forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m t -> MaybeT m t) -> (f l -> m t) -> f l -> MaybeT m t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. )

-- | Runs a failable computation, replacing failure with `mempty`
mtryM :: (Applicative m, Monoid a) => MaybeT m a -> m a
mtryM :: forall (m :: * -> *) a.
(Applicative m, Monoid a) =>
MaybeT m a -> m a
mtryM = (Maybe a -> a) -> m (Maybe a) -> m a
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (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 :: forall (m :: * -> *) (f :: (* -> *) -> * -> *) t.
(MonadPlus m, HFoldable f) =>
GTranslateM m (HFix f) t -> GTranslateM m (HFix f) t
onetdT GTranslateM m (HFix f) t
t = GTranslateM m (HFix f) t
-> (m t -> m t -> m t) -> GTranslateM m (HFix f) t
forall (f :: (* -> *) -> * -> *) h (a :: * -> *) r.
HFoldable f =>
(Cxt h f a :=> r) -> (r -> r -> r) -> Cxt h f a :=> r
query TranslateM m (HFix f) i t
GTranslateM m (HFix f) t
t m t -> m t -> m t
forall a. m a -> m a -> m a
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 :: forall r (f :: (* -> *) -> * -> *).
HFoldable f =>
(HFix f :=> r) -> (r -> r -> r) -> HFix f :=> r
parQuery HFix f :=> r
q r -> r -> r
c 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 :=> Eval r
rec Int
8 HFix f i
tree
  where
    rec :: Int -> HFix f :=> Eval r
    rec :: Int -> HFix f :=> Eval r
rec Int
0 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 :=> r
forall (f :: (* -> *) -> * -> *) h (a :: * -> *) r.
HFoldable f =>
(Cxt h f a :=> r) -> (r -> r -> r) -> Cxt h f a :=> r
query HFix f i -> r
HFix f :=> r
q r -> r -> r
c HFix f i
i
    rec Int
depth i :: HFix f i
i@(Term f (HFix f) i
t) = (Eval r -> HFix f :=> Eval r) -> Eval r -> f (HFix f) :=> Eval r
forall b (a :: * -> *). (b -> a :=> b) -> b -> f a :=> b
forall (h :: (* -> *) -> * -> *) b (a :: * -> *).
HFoldable h =>
(b -> a :=> b) -> b -> h a :=> b
hfoldl (\Eval r
s 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 -> HFix f :=> Eval r
rec (Int
depthInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
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 :: forall (f :: (* -> *) -> * -> *) t (m :: * -> *) l.
(HFoldable f, Monoid t, Applicative m) =>
GTranslateM m (HFix f) t -> TranslateM m (HFix f) l t
foldT GTranslateM m (HFix f) t
t (Term f (HFix f) l
tree) = (m t -> GTranslateM m (HFix f) t) -> m t -> f (HFix f) :=> m t
forall b (a :: * -> *). (b -> a :=> b) -> b -> f a :=> b
forall (h :: (* -> *) -> * -> *) b (a :: * -> *).
HFoldable h =>
(b -> a :=> b) -> b -> h a :=> b
hfoldl (\m t
s Cxt NoHole f (K ()) i
x -> (t -> t -> t) -> m t -> m t -> m t
forall a b c. (a -> b -> c) -> m a -> m b -> m c
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 (Cxt NoHole f (K ()) i -> m t
GTranslateM m (HFix f) t
t Cxt NoHole f (K ()) i
x)) (t -> m t
forall a. a -> m a
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 :: 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
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 TranslateM m (HFix f) i t
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 :: forall (f :: (* -> *) -> * -> *) t (m :: * -> *).
(HFoldable f, Monoid t, Monad m) =>
GTranslateM (MaybeT m) (HFix f) t -> GTranslateM m (HFix f) t
crushtdT GTranslateM (MaybeT m) (HFix f) t
f = GTranslateM m (HFix f) t -> GTranslateM m (HFix f) 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 -> GTranslateM m (HFix f) t)
-> GTranslateM m (HFix f) t -> GTranslateM m (HFix f) t
forall a b. (a -> b) -> a -> b
$ MaybeT m t -> m t
forall (m :: * -> *) a.
(Applicative 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

-- | Similar to crushtdT, except it never recurses below successes
pruningCrushtdTF :: (HFoldable f, Monoid t, Alternative m) => GTranslateM m (HFix f) t -> GTranslateM m (HFix f) t
pruningCrushtdTF :: forall (f :: (* -> *) -> * -> *) t (m :: * -> *).
(HFoldable f, Monoid t, Alternative m) =>
GTranslateM m (HFix f) t -> GTranslateM m (HFix f) t
pruningCrushtdTF GTranslateM m (HFix f) t
f = TranslateM m (HFix f) l t
GTranslateM m (HFix f) t
f TranslateM m (HFix f) l t
-> TranslateM m (HFix f) l t -> TranslateM m (HFix f) l t
forall (m :: * -> *) (f :: * -> *) l t.
Alternative m =>
TranslateM m f l t -> TranslateM m f l t -> TranslateM m f l t
<+ (\(Term f (HFix f) l
t) -> (m t -> GTranslateM m (HFix f) t) -> m t -> f (HFix f) :=> m t
forall b (a :: * -> *). (b -> a :=> b) -> b -> f a :=> b
forall (h :: (* -> *) -> * -> *) b (a :: * -> *).
HFoldable h =>
(b -> a :=> b) -> b -> h a :=> b
hfoldl (\m t
s Cxt NoHole f (K ()) i
x -> (t -> t -> t) -> m t -> m t -> m t
forall a b c. (a -> b -> c) -> m a -> m b -> m c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 t -> t -> t
forall a. Semigroup a => a -> a -> a
(<>) m t
s (m t -> m t) -> m t -> m t
forall a b. (a -> b) -> a -> b
$ GTranslateM m (HFix f) t -> GTranslateM m (HFix f) t
forall (f :: (* -> *) -> * -> *) t (m :: * -> *).
(HFoldable f, Monoid t, Alternative m) =>
GTranslateM m (HFix f) t -> GTranslateM m (HFix f) t
pruningCrushtdTF TranslateM m (HFix f) l t
GTranslateM m (HFix f) t
f Cxt NoHole f (K ()) i
x) (t -> m t
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure t
forall a. Monoid a => a
mempty) f (HFix f) l
t)

-- Monad instead of Applicative, because the Applicative instance for MaybeT requires Monad
-- | pruningCrushtdTF, replacing top-level failure with mempty
pruningCrushtdT :: (HFoldable f, Monoid t, Monad m) => GTranslateM (MaybeT m) (HFix f) t -> GTranslateM m (HFix f) t
pruningCrushtdT :: forall (f :: (* -> *) -> * -> *) t (m :: * -> *).
(HFoldable f, Monoid t, Monad m) =>
GTranslateM (MaybeT m) (HFix f) t -> GTranslateM m (HFix f) t
pruningCrushtdT GTranslateM (MaybeT m) (HFix f) t
f = MaybeT m t -> m t
forall (m :: * -> *) a.
(Applicative 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
. GTranslateM (MaybeT m) (HFix f) t
-> GTranslateM (MaybeT m) (HFix f) t
forall (f :: (* -> *) -> * -> *) t (m :: * -> *).
(HFoldable f, Monoid t, Alternative m) =>
GTranslateM m (HFix f) t -> GTranslateM m (HFix f) t
pruningCrushtdTF TranslateM (MaybeT m) (HFix f) l t
GTranslateM (MaybeT m) (HFix f) t
f

-- | Gives all subterms of any given sort of a term which are not contained in another term of that sort
maximalSubterms :: forall f l l'. (DynCase (HFix f) l, HFoldable f) => HFix f l' -> [HFix f l]
maximalSubterms :: forall (f :: (* -> *) -> * -> *) l l'.
(DynCase (HFix f) l, HFoldable f) =>
HFix f l' -> [HFix f l]
maximalSubterms = Identity [HFix f l] -> [HFix f l]
forall a. Identity a -> a
runIdentity (Identity [HFix f l] -> [HFix f l])
-> (HFix f l' -> Identity [HFix f l]) -> HFix f l' -> [HFix f l]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GTranslateM (MaybeT Identity) (HFix f) [HFix f l]
-> GTranslateM Identity (HFix f) [HFix f l]
forall (f :: (* -> *) -> * -> *) t (m :: * -> *).
(HFoldable f, Monoid t, Monad m) =>
GTranslateM (MaybeT m) (HFix f) t -> GTranslateM m (HFix f) t
pruningCrushtdT (TranslateM (MaybeT Identity) (HFix f) l [HFix f l]
-> GTranslateM (MaybeT Identity) (HFix f) [HFix f l]
forall (f :: * -> *) l (m :: * -> *) t.
(DynCase f l, Alternative m) =>
TranslateM m f l t -> GTranslateM m f t
promoteTF TranslateM (MaybeT Identity) (HFix f) l [HFix f l]
idOnTargetSort)
  where
    idOnTargetSort :: TranslateM (MaybeT Identity) (HFix f) l [HFix f l]
    idOnTargetSort :: TranslateM (MaybeT Identity) (HFix f) l [HFix f l]
idOnTargetSort HFix f l
x = [HFix f l] -> MaybeT Identity [HFix f l]
forall a. a -> MaybeT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return [HFix f l
x]