-- A type of pruners.
{-# OPTIONS_HADDOCK hide #-}
{-# LANGUAGE FunctionalDependencies, GeneralizedNewtypeDeriving, FlexibleInstances, UndecidableInstances, DefaultSignatures, GADTs, TypeOperators, DeriveFunctor, DeriveTraversable #-}
module QuickSpec.Internal.Pruning where

import QuickSpec.Internal.Prop
import QuickSpec.Internal.Testing
import QuickSpec.Internal.Type(Type)
import Twee.Pretty
import Control.Monad.Trans.Class
import Control.Monad.IO.Class
import Control.Monad.Trans.State.Strict
import Control.Monad.Trans.Reader
import Data.Maybe

data Theorem norm =
  Theorem {
    forall norm. Theorem norm -> Prop norm
prop :: Prop norm,
    forall norm. Theorem norm -> [(Prop norm, [Prop norm])]
axiomsUsed :: [(Prop norm, [Prop norm])] }
  deriving (forall a b. a -> Theorem b -> Theorem a
forall a b. (a -> b) -> Theorem a -> Theorem b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Theorem b -> Theorem a
$c<$ :: forall a b. a -> Theorem b -> Theorem a
fmap :: forall a b. (a -> b) -> Theorem a -> Theorem b
$cfmap :: forall a b. (a -> b) -> Theorem a -> Theorem b
Functor, forall a. Eq a => a -> Theorem a -> Bool
forall a. Num a => Theorem a -> a
forall a. Ord a => Theorem a -> a
forall m. Monoid m => Theorem m -> m
forall a. Theorem a -> Bool
forall a. Theorem a -> Int
forall a. Theorem a -> [a]
forall a. (a -> a -> a) -> Theorem a -> a
forall m a. Monoid m => (a -> m) -> Theorem a -> m
forall b a. (b -> a -> b) -> b -> Theorem a -> b
forall a b. (a -> b -> b) -> b -> Theorem a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: forall a. Num a => Theorem a -> a
$cproduct :: forall a. Num a => Theorem a -> a
sum :: forall a. Num a => Theorem a -> a
$csum :: forall a. Num a => Theorem a -> a
minimum :: forall a. Ord a => Theorem a -> a
$cminimum :: forall a. Ord a => Theorem a -> a
maximum :: forall a. Ord a => Theorem a -> a
$cmaximum :: forall a. Ord a => Theorem a -> a
elem :: forall a. Eq a => a -> Theorem a -> Bool
$celem :: forall a. Eq a => a -> Theorem a -> Bool
length :: forall a. Theorem a -> Int
$clength :: forall a. Theorem a -> Int
null :: forall a. Theorem a -> Bool
$cnull :: forall a. Theorem a -> Bool
toList :: forall a. Theorem a -> [a]
$ctoList :: forall a. Theorem a -> [a]
foldl1 :: forall a. (a -> a -> a) -> Theorem a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Theorem a -> a
foldr1 :: forall a. (a -> a -> a) -> Theorem a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Theorem a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> Theorem a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Theorem a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Theorem a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Theorem a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Theorem a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Theorem a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Theorem a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Theorem a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> Theorem a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Theorem a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Theorem a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Theorem a -> m
fold :: forall m. Monoid m => Theorem m -> m
$cfold :: forall m. Monoid m => Theorem m -> m
Foldable, Functor Theorem
Foldable Theorem
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Theorem (m a) -> m (Theorem a)
forall (f :: * -> *) a.
Applicative f =>
Theorem (f a) -> f (Theorem a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Theorem a -> m (Theorem b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Theorem a -> f (Theorem b)
sequence :: forall (m :: * -> *) a. Monad m => Theorem (m a) -> m (Theorem a)
$csequence :: forall (m :: * -> *) a. Monad m => Theorem (m a) -> m (Theorem a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Theorem a -> m (Theorem b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Theorem a -> m (Theorem b)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Theorem (f a) -> f (Theorem a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
Theorem (f a) -> f (Theorem a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Theorem a -> f (Theorem b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Theorem a -> f (Theorem b)
Traversable)

instance Pretty norm => Pretty (Theorem norm) where
  pPrint :: Theorem norm -> Doc
pPrint Theorem norm
thm =
    (String -> Doc
text String
"prop =" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pPrint (forall norm. Theorem norm -> Prop norm
prop Theorem norm
thm)) Doc -> Doc -> Doc
$$
    (String -> Doc
text String
"axioms used =" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pPrint (forall norm. Theorem norm -> [(Prop norm, [Prop norm])]
axiomsUsed Theorem norm
thm))

class Monad m => MonadPruner term norm m | m -> term norm where
  normaliser :: m (term -> norm)
  add :: Prop term -> m Bool
  decodeNormalForm :: (Type -> Maybe term) -> norm -> m (Maybe term)
  normTheorems :: m [Theorem norm]

  default normaliser :: (MonadTrans t, MonadPruner term norm m', m ~ t m') => m (term -> norm)
  normaliser = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall term norm (m :: * -> *).
MonadPruner term norm m =>
m (term -> norm)
normaliser

  default add :: (MonadTrans t, MonadPruner term norm m', m ~ t m') => Prop term -> m Bool
  add = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall term norm (m :: * -> *).
MonadPruner term norm m =>
Prop term -> m Bool
add

  default normTheorems :: (MonadTrans t, MonadPruner term' norm m', m ~ t m') => m [Theorem norm]
  normTheorems = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall term norm (m :: * -> *).
MonadPruner term norm m =>
m [Theorem norm]
normTheorems

  default decodeNormalForm :: (MonadTrans t, MonadPruner term norm m', m ~ t m') => (Type -> Maybe term) -> norm -> m (Maybe term)
  decodeNormalForm Type -> Maybe term
hole norm
t = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (forall term norm (m :: * -> *).
MonadPruner term norm m =>
(Type -> Maybe term) -> norm -> m (Maybe term)
decodeNormalForm Type -> Maybe term
hole norm
t)

decodeTheorem :: MonadPruner term norm m => (Type -> Maybe term) -> Theorem norm -> m (Maybe (Theorem term))
decodeTheorem :: forall term norm (m :: * -> *).
MonadPruner term norm m =>
(Type -> Maybe term) -> Theorem norm -> m (Maybe (Theorem term))
decodeTheorem Type -> Maybe term
hole Theorem norm
thm = Theorem (Maybe term) -> Maybe (Theorem term)
elimMaybeThm forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall term norm (m :: * -> *).
MonadPruner term norm m =>
(Type -> Maybe term) -> norm -> m (Maybe term)
decodeNormalForm Type -> Maybe term
hole) Theorem norm
thm
  where
    elimMaybeThm :: Theorem (Maybe term) -> Maybe (Theorem term)
elimMaybeThm (Theorem Prop (Maybe term)
prop [(Prop (Maybe term), [Prop (Maybe term)])]
axs) =
      case forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence Prop (Maybe term)
prop of
        Maybe (Prop term)
Nothing -> forall a. Maybe a
Nothing
        Just Prop term
prop -> forall a. a -> Maybe a
Just (forall norm.
Prop norm -> [(Prop norm, [Prop norm])] -> Theorem norm
Theorem Prop term
prop (forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Prop (Maybe term), [Prop (Maybe term)])
-> Maybe (Prop term, [Prop term])
elimMaybeAx [(Prop (Maybe term), [Prop (Maybe term)])]
axs))
    elimMaybeAx :: (Prop (Maybe term), [Prop (Maybe term)])
-> Maybe (Prop term, [Prop term])
elimMaybeAx (Prop (Maybe term)
ax, [Prop (Maybe term)]
insts) =
      case forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence Prop (Maybe term)
ax of
        Maybe (Prop term)
Nothing -> forall a. Maybe a
Nothing
        Just Prop term
ax -> forall a. a -> Maybe a
Just (Prop term
ax, forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe forall {a}. Prop (Maybe a) -> Maybe (Prop a)
elimMaybeInst [Prop (Maybe term)]
insts)
    elimMaybeInst :: Prop (Maybe a) -> Maybe (Prop a)
elimMaybeInst = forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence

theorems :: MonadPruner term norm m => (Type -> Maybe term) -> m [Theorem term]
theorems :: forall term norm (m :: * -> *).
MonadPruner term norm m =>
(Type -> Maybe term) -> m [Theorem term]
theorems Type -> Maybe term
hole = do
  [Theorem norm]
thms <- forall term norm (m :: * -> *).
MonadPruner term norm m =>
m [Theorem norm]
normTheorems
  forall a. [Maybe a] -> [a]
catMaybes forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall term norm (m :: * -> *).
MonadPruner term norm m =>
(Type -> Maybe term) -> Theorem norm -> m (Maybe (Theorem term))
decodeTheorem Type -> Maybe term
hole) [Theorem norm]
thms

instance MonadPruner term norm m => MonadPruner term norm (StateT s m)
instance MonadPruner term norm m => MonadPruner term norm (ReaderT r m)

normalise :: MonadPruner term norm m => term -> m norm
normalise :: forall term norm (m :: * -> *).
MonadPruner term norm m =>
term -> m norm
normalise term
t = do
  term -> norm
norm <- forall term norm (m :: * -> *).
MonadPruner term norm m =>
m (term -> norm)
normaliser
  forall (m :: * -> *) a. Monad m => a -> m a
return (term -> norm
norm term
t)

newtype ReadOnlyPruner m a = ReadOnlyPruner { forall (m :: * -> *) a. ReadOnlyPruner m a -> m a
withReadOnlyPruner :: m a }
  deriving (forall a b. a -> ReadOnlyPruner m b -> ReadOnlyPruner m a
forall a b. (a -> b) -> ReadOnlyPruner m a -> ReadOnlyPruner m b
forall (m :: * -> *) a b.
Functor m =>
a -> ReadOnlyPruner m b -> ReadOnlyPruner m a
forall (m :: * -> *) a b.
Functor m =>
(a -> b) -> ReadOnlyPruner m a -> ReadOnlyPruner m b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> ReadOnlyPruner m b -> ReadOnlyPruner m a
$c<$ :: forall (m :: * -> *) a b.
Functor m =>
a -> ReadOnlyPruner m b -> ReadOnlyPruner m a
fmap :: forall a b. (a -> b) -> ReadOnlyPruner m a -> ReadOnlyPruner m b
$cfmap :: forall (m :: * -> *) a b.
Functor m =>
(a -> b) -> ReadOnlyPruner m a -> ReadOnlyPruner m b
Functor, forall a. a -> ReadOnlyPruner m a
forall a b.
ReadOnlyPruner m a -> ReadOnlyPruner m b -> ReadOnlyPruner m a
forall a b.
ReadOnlyPruner m a -> ReadOnlyPruner m b -> ReadOnlyPruner m b
forall a b.
ReadOnlyPruner m (a -> b)
-> ReadOnlyPruner m a -> ReadOnlyPruner m b
forall a b c.
(a -> b -> c)
-> ReadOnlyPruner m a -> ReadOnlyPruner m b -> ReadOnlyPruner m c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
forall {m :: * -> *}. Applicative m => Functor (ReadOnlyPruner m)
forall (m :: * -> *) a. Applicative m => a -> ReadOnlyPruner m a
forall (m :: * -> *) a b.
Applicative m =>
ReadOnlyPruner m a -> ReadOnlyPruner m b -> ReadOnlyPruner m a
forall (m :: * -> *) a b.
Applicative m =>
ReadOnlyPruner m a -> ReadOnlyPruner m b -> ReadOnlyPruner m b
forall (m :: * -> *) a b.
Applicative m =>
ReadOnlyPruner m (a -> b)
-> ReadOnlyPruner m a -> ReadOnlyPruner m b
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> c)
-> ReadOnlyPruner m a -> ReadOnlyPruner m b -> ReadOnlyPruner m c
<* :: forall a b.
ReadOnlyPruner m a -> ReadOnlyPruner m b -> ReadOnlyPruner m a
$c<* :: forall (m :: * -> *) a b.
Applicative m =>
ReadOnlyPruner m a -> ReadOnlyPruner m b -> ReadOnlyPruner m a
*> :: forall a b.
ReadOnlyPruner m a -> ReadOnlyPruner m b -> ReadOnlyPruner m b
$c*> :: forall (m :: * -> *) a b.
Applicative m =>
ReadOnlyPruner m a -> ReadOnlyPruner m b -> ReadOnlyPruner m b
liftA2 :: forall a b c.
(a -> b -> c)
-> ReadOnlyPruner m a -> ReadOnlyPruner m b -> ReadOnlyPruner m c
$cliftA2 :: forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> c)
-> ReadOnlyPruner m a -> ReadOnlyPruner m b -> ReadOnlyPruner m c
<*> :: forall a b.
ReadOnlyPruner m (a -> b)
-> ReadOnlyPruner m a -> ReadOnlyPruner m b
$c<*> :: forall (m :: * -> *) a b.
Applicative m =>
ReadOnlyPruner m (a -> b)
-> ReadOnlyPruner m a -> ReadOnlyPruner m b
pure :: forall a. a -> ReadOnlyPruner m a
$cpure :: forall (m :: * -> *) a. Applicative m => a -> ReadOnlyPruner m a
Applicative, forall a. a -> ReadOnlyPruner m a
forall a b.
ReadOnlyPruner m a -> ReadOnlyPruner m b -> ReadOnlyPruner m b
forall a b.
ReadOnlyPruner m a
-> (a -> ReadOnlyPruner m b) -> ReadOnlyPruner m b
forall {m :: * -> *}. Monad m => Applicative (ReadOnlyPruner m)
forall (m :: * -> *) a. Monad m => a -> ReadOnlyPruner m a
forall (m :: * -> *) a b.
Monad m =>
ReadOnlyPruner m a -> ReadOnlyPruner m b -> ReadOnlyPruner m b
forall (m :: * -> *) a b.
Monad m =>
ReadOnlyPruner m a
-> (a -> ReadOnlyPruner m b) -> ReadOnlyPruner m b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: forall a. a -> ReadOnlyPruner m a
$creturn :: forall (m :: * -> *) a. Monad m => a -> ReadOnlyPruner m a
>> :: forall a b.
ReadOnlyPruner m a -> ReadOnlyPruner m b -> ReadOnlyPruner m b
$c>> :: forall (m :: * -> *) a b.
Monad m =>
ReadOnlyPruner m a -> ReadOnlyPruner m b -> ReadOnlyPruner m b
>>= :: forall a b.
ReadOnlyPruner m a
-> (a -> ReadOnlyPruner m b) -> ReadOnlyPruner m b
$c>>= :: forall (m :: * -> *) a b.
Monad m =>
ReadOnlyPruner m a
-> (a -> ReadOnlyPruner m b) -> ReadOnlyPruner m b
Monad, forall a. IO a -> ReadOnlyPruner m a
forall (m :: * -> *).
Monad m -> (forall a. IO a -> m a) -> MonadIO m
forall {m :: * -> *}. MonadIO m => Monad (ReadOnlyPruner m)
forall (m :: * -> *) a. MonadIO m => IO a -> ReadOnlyPruner m a
liftIO :: forall a. IO a -> ReadOnlyPruner m a
$cliftIO :: forall (m :: * -> *) a. MonadIO m => IO a -> ReadOnlyPruner m a
MonadIO, MonadTester testcase term)

instance MonadTrans ReadOnlyPruner where
  lift :: forall (m :: * -> *) a. Monad m => m a -> ReadOnlyPruner m a
lift = forall (m :: * -> *) a. m a -> ReadOnlyPruner m a
ReadOnlyPruner

instance MonadPruner term norm m => MonadPruner term norm (ReadOnlyPruner m) where
  normaliser :: ReadOnlyPruner m (term -> norm)
normaliser = forall (m :: * -> *) a. m a -> ReadOnlyPruner m a
ReadOnlyPruner forall term norm (m :: * -> *).
MonadPruner term norm m =>
m (term -> norm)
normaliser
  add :: Prop term -> ReadOnlyPruner m Bool
add Prop term
_ = forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True

newtype WatchPruner term m a = WatchPruner (StateT [Prop term] m a)
  deriving (forall a b. a -> WatchPruner term m b -> WatchPruner term m a
forall a b.
(a -> b) -> WatchPruner term m a -> WatchPruner term m b
forall term (m :: * -> *) a b.
Functor m =>
a -> WatchPruner term m b -> WatchPruner term m a
forall term (m :: * -> *) a b.
Functor m =>
(a -> b) -> WatchPruner term m a -> WatchPruner term m b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> WatchPruner term m b -> WatchPruner term m a
$c<$ :: forall term (m :: * -> *) a b.
Functor m =>
a -> WatchPruner term m b -> WatchPruner term m a
fmap :: forall a b.
(a -> b) -> WatchPruner term m a -> WatchPruner term m b
$cfmap :: forall term (m :: * -> *) a b.
Functor m =>
(a -> b) -> WatchPruner term m a -> WatchPruner term m b
Functor, forall a. a -> WatchPruner term m a
forall a b.
WatchPruner term m a
-> WatchPruner term m b -> WatchPruner term m a
forall a b.
WatchPruner term m a
-> WatchPruner term m b -> WatchPruner term m b
forall a b.
WatchPruner term m (a -> b)
-> WatchPruner term m a -> WatchPruner term m b
forall a b c.
(a -> b -> c)
-> WatchPruner term m a
-> WatchPruner term m b
-> WatchPruner term m c
forall {term} {m :: * -> *}.
Monad m =>
Functor (WatchPruner term m)
forall term (m :: * -> *) a. Monad m => a -> WatchPruner term m a
forall term (m :: * -> *) a b.
Monad m =>
WatchPruner term m a
-> WatchPruner term m b -> WatchPruner term m a
forall term (m :: * -> *) a b.
Monad m =>
WatchPruner term m a
-> WatchPruner term m b -> WatchPruner term m b
forall term (m :: * -> *) a b.
Monad m =>
WatchPruner term m (a -> b)
-> WatchPruner term m a -> WatchPruner term m b
forall term (m :: * -> *) a b c.
Monad m =>
(a -> b -> c)
-> WatchPruner term m a
-> WatchPruner term m b
-> WatchPruner term m c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: forall a b.
WatchPruner term m a
-> WatchPruner term m b -> WatchPruner term m a
$c<* :: forall term (m :: * -> *) a b.
Monad m =>
WatchPruner term m a
-> WatchPruner term m b -> WatchPruner term m a
*> :: forall a b.
WatchPruner term m a
-> WatchPruner term m b -> WatchPruner term m b
$c*> :: forall term (m :: * -> *) a b.
Monad m =>
WatchPruner term m a
-> WatchPruner term m b -> WatchPruner term m b
liftA2 :: forall a b c.
(a -> b -> c)
-> WatchPruner term m a
-> WatchPruner term m b
-> WatchPruner term m c
$cliftA2 :: forall term (m :: * -> *) a b c.
Monad m =>
(a -> b -> c)
-> WatchPruner term m a
-> WatchPruner term m b
-> WatchPruner term m c
<*> :: forall a b.
WatchPruner term m (a -> b)
-> WatchPruner term m a -> WatchPruner term m b
$c<*> :: forall term (m :: * -> *) a b.
Monad m =>
WatchPruner term m (a -> b)
-> WatchPruner term m a -> WatchPruner term m b
pure :: forall a. a -> WatchPruner term m a
$cpure :: forall term (m :: * -> *) a. Monad m => a -> WatchPruner term m a
Applicative, forall a. a -> WatchPruner term m a
forall a b.
WatchPruner term m a
-> WatchPruner term m b -> WatchPruner term m b
forall a b.
WatchPruner term m a
-> (a -> WatchPruner term m b) -> WatchPruner term m b
forall term (m :: * -> *).
Monad m =>
Applicative (WatchPruner term m)
forall term (m :: * -> *) a. Monad m => a -> WatchPruner term m a
forall term (m :: * -> *) a b.
Monad m =>
WatchPruner term m a
-> WatchPruner term m b -> WatchPruner term m b
forall term (m :: * -> *) a b.
Monad m =>
WatchPruner term m a
-> (a -> WatchPruner term m b) -> WatchPruner term m b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: forall a. a -> WatchPruner term m a
$creturn :: forall term (m :: * -> *) a. Monad m => a -> WatchPruner term m a
>> :: forall a b.
WatchPruner term m a
-> WatchPruner term m b -> WatchPruner term m b
$c>> :: forall term (m :: * -> *) a b.
Monad m =>
WatchPruner term m a
-> WatchPruner term m b -> WatchPruner term m b
>>= :: forall a b.
WatchPruner term m a
-> (a -> WatchPruner term m b) -> WatchPruner term m b
$c>>= :: forall term (m :: * -> *) a b.
Monad m =>
WatchPruner term m a
-> (a -> WatchPruner term m b) -> WatchPruner term m b
Monad, forall term (m :: * -> *) a. Monad m => m a -> WatchPruner term m a
forall (m :: * -> *) a. Monad m => m a -> WatchPruner term m a
forall (t :: (* -> *) -> * -> *).
(forall (m :: * -> *) a. Monad m => m a -> t m a) -> MonadTrans t
lift :: forall (m :: * -> *) a. Monad m => m a -> WatchPruner term m a
$clift :: forall term (m :: * -> *) a. Monad m => m a -> WatchPruner term m a
MonadTrans, forall a. IO a -> WatchPruner term m a
forall {term} {m :: * -> *}.
MonadIO m =>
Monad (WatchPruner term m)
forall term (m :: * -> *) a.
MonadIO m =>
IO a -> WatchPruner term m a
forall (m :: * -> *).
Monad m -> (forall a. IO a -> m a) -> MonadIO m
liftIO :: forall a. IO a -> WatchPruner term m a
$cliftIO :: forall term (m :: * -> *) a.
MonadIO m =>
IO a -> WatchPruner term m a
MonadIO, MonadTester testcase term)

instance MonadPruner term norm m => MonadPruner term norm (WatchPruner term m) where
  normaliser :: WatchPruner term m (term -> norm)
normaliser = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall term norm (m :: * -> *).
MonadPruner term norm m =>
m (term -> norm)
normaliser
  add :: Prop term -> WatchPruner term m Bool
add Prop term
prop = do
    Bool
res <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (forall term norm (m :: * -> *).
MonadPruner term norm m =>
Prop term -> m Bool
add Prop term
prop)
    forall term (m :: * -> *) a.
StateT [Prop term] m a -> WatchPruner term m a
WatchPruner (forall (m :: * -> *) s. Monad m => (s -> s) -> StateT s m ()
modify (Prop term
propforall a. a -> [a] -> [a]
:))
    forall (m :: * -> *) a. Monad m => a -> m a
return Bool
res

watchPruner :: Monad m => WatchPruner term m a -> m (a, [Prop term])
watchPruner :: forall (m :: * -> *) term a.
Monad m =>
WatchPruner term m a -> m (a, [Prop term])
watchPruner (WatchPruner StateT [Prop term] m a
mx) = do
  (a
x, [Prop term]
props) <- forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT StateT [Prop term] m a
mx []
  forall (m :: * -> *) a. Monad m => a -> m a
return (a
x, forall a. [a] -> [a]
reverse [Prop term]
props)