-- A pruner that uses twee. Supports types and background axioms.
{-# OPTIONS_HADDOCK hide #-}
{-# LANGUAGE RecordWildCards, FlexibleContexts, FlexibleInstances, GADTs, PatternSynonyms, GeneralizedNewtypeDeriving, MultiParamTypeClasses, UndecidableInstances #-}
module QuickSpec.Internal.Pruning.Twee(Config(..), module QuickSpec.Internal.Pruning.Twee) where

import QuickSpec.Internal.Testing
import QuickSpec.Internal.Pruning
import QuickSpec.Internal.Term
import QuickSpec.Internal.Terminal
import qualified QuickSpec.Internal.Pruning.Types as Types
import QuickSpec.Internal.Pruning.Types(Tagged)
import qualified QuickSpec.Internal.Pruning.PartialApplication as PartialApplication
import QuickSpec.Internal.Pruning.PartialApplication(PartiallyApplied)
import qualified QuickSpec.Internal.Pruning.Background as Background
import Control.Monad.Trans.Class
import Control.Monad.IO.Class
import qualified QuickSpec.Internal.Pruning.UntypedTwee as Untyped
import QuickSpec.Internal.Pruning.UntypedTwee(Config(..))
import Data.Typeable

newtype Pruner fun m a =
  Pruner (PartialApplication.Pruner fun (Types.Pruner (PartiallyApplied fun) (Background.Pruner (Tagged (PartiallyApplied fun)) (Untyped.Pruner (Tagged (PartiallyApplied fun)) m))) a)
  deriving (forall a b. a -> Pruner fun m b -> Pruner fun m a
forall a b. (a -> b) -> Pruner fun m a -> Pruner fun m b
forall fun (m :: * -> *) a b.
Functor m =>
a -> Pruner fun m b -> Pruner fun m a
forall fun (m :: * -> *) a b.
Functor m =>
(a -> b) -> Pruner fun m a -> Pruner fun 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 -> Pruner fun m b -> Pruner fun m a
$c<$ :: forall fun (m :: * -> *) a b.
Functor m =>
a -> Pruner fun m b -> Pruner fun m a
fmap :: forall a b. (a -> b) -> Pruner fun m a -> Pruner fun m b
$cfmap :: forall fun (m :: * -> *) a b.
Functor m =>
(a -> b) -> Pruner fun m a -> Pruner fun m b
Functor, forall a. a -> Pruner fun m a
forall a b. Pruner fun m a -> Pruner fun m b -> Pruner fun m a
forall a b. Pruner fun m a -> Pruner fun m b -> Pruner fun m b
forall a b.
Pruner fun m (a -> b) -> Pruner fun m a -> Pruner fun m b
forall a b c.
(a -> b -> c) -> Pruner fun m a -> Pruner fun m b -> Pruner fun m c
forall {fun} {m :: * -> *}. Monad m => Functor (Pruner fun m)
forall fun (m :: * -> *) a. Monad m => a -> Pruner fun m a
forall fun (m :: * -> *) a b.
Monad m =>
Pruner fun m a -> Pruner fun m b -> Pruner fun m a
forall fun (m :: * -> *) a b.
Monad m =>
Pruner fun m a -> Pruner fun m b -> Pruner fun m b
forall fun (m :: * -> *) a b.
Monad m =>
Pruner fun m (a -> b) -> Pruner fun m a -> Pruner fun m b
forall fun (m :: * -> *) a b c.
Monad m =>
(a -> b -> c) -> Pruner fun m a -> Pruner fun m b -> Pruner fun 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. Pruner fun m a -> Pruner fun m b -> Pruner fun m a
$c<* :: forall fun (m :: * -> *) a b.
Monad m =>
Pruner fun m a -> Pruner fun m b -> Pruner fun m a
*> :: forall a b. Pruner fun m a -> Pruner fun m b -> Pruner fun m b
$c*> :: forall fun (m :: * -> *) a b.
Monad m =>
Pruner fun m a -> Pruner fun m b -> Pruner fun m b
liftA2 :: forall a b c.
(a -> b -> c) -> Pruner fun m a -> Pruner fun m b -> Pruner fun m c
$cliftA2 :: forall fun (m :: * -> *) a b c.
Monad m =>
(a -> b -> c) -> Pruner fun m a -> Pruner fun m b -> Pruner fun m c
<*> :: forall a b.
Pruner fun m (a -> b) -> Pruner fun m a -> Pruner fun m b
$c<*> :: forall fun (m :: * -> *) a b.
Monad m =>
Pruner fun m (a -> b) -> Pruner fun m a -> Pruner fun m b
pure :: forall a. a -> Pruner fun m a
$cpure :: forall fun (m :: * -> *) a. Monad m => a -> Pruner fun m a
Applicative, forall a. a -> Pruner fun m a
forall a b. Pruner fun m a -> Pruner fun m b -> Pruner fun m b
forall a b.
Pruner fun m a -> (a -> Pruner fun m b) -> Pruner fun m b
forall fun (m :: * -> *). Monad m => Applicative (Pruner fun m)
forall fun (m :: * -> *) a. Monad m => a -> Pruner fun m a
forall fun (m :: * -> *) a b.
Monad m =>
Pruner fun m a -> Pruner fun m b -> Pruner fun m b
forall fun (m :: * -> *) a b.
Monad m =>
Pruner fun m a -> (a -> Pruner fun m b) -> Pruner fun 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 -> Pruner fun m a
$creturn :: forall fun (m :: * -> *) a. Monad m => a -> Pruner fun m a
>> :: forall a b. Pruner fun m a -> Pruner fun m b -> Pruner fun m b
$c>> :: forall fun (m :: * -> *) a b.
Monad m =>
Pruner fun m a -> Pruner fun m b -> Pruner fun m b
>>= :: forall a b.
Pruner fun m a -> (a -> Pruner fun m b) -> Pruner fun m b
$c>>= :: forall fun (m :: * -> *) a b.
Monad m =>
Pruner fun m a -> (a -> Pruner fun m b) -> Pruner fun m b
Monad, forall a. IO a -> Pruner fun m a
forall {fun} {m :: * -> *}. MonadIO m => Monad (Pruner fun m)
forall fun (m :: * -> *) a. MonadIO m => IO a -> Pruner fun m a
forall (m :: * -> *).
Monad m -> (forall a. IO a -> m a) -> MonadIO m
liftIO :: forall a. IO a -> Pruner fun m a
$cliftIO :: forall fun (m :: * -> *) a. MonadIO m => IO a -> Pruner fun m a
MonadIO, MonadTester testcase term,
            MonadPruner (Term fun) (Untyped.Norm (Tagged (PartiallyApplied fun))), String -> Pruner fun m ()
forall {fun} {m :: * -> *}. MonadTerminal m => Monad (Pruner fun m)
forall fun (m :: * -> *).
MonadTerminal m =>
String -> Pruner fun m ()
forall (m :: * -> *).
Monad m
-> (String -> m ())
-> (String -> m ())
-> (String -> m ())
-> MonadTerminal m
putTemp :: String -> Pruner fun m ()
$cputTemp :: forall fun (m :: * -> *).
MonadTerminal m =>
String -> Pruner fun m ()
putLine :: String -> Pruner fun m ()
$cputLine :: forall fun (m :: * -> *).
MonadTerminal m =>
String -> Pruner fun m ()
putText :: String -> Pruner fun m ()
$cputText :: forall fun (m :: * -> *).
MonadTerminal m =>
String -> Pruner fun m ()
MonadTerminal)

instance MonadTrans (Pruner fun) where
  lift :: forall (m :: * -> *) a. Monad m => m a -> Pruner fun m a
lift = forall fun (m :: * -> *) a.
Pruner
  fun
  (Pruner
     (PartiallyApplied fun)
     (Pruner
        (Tagged (PartiallyApplied fun))
        (Pruner (Tagged (PartiallyApplied fun)) m)))
  a
-> Pruner fun m a
Pruner forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift

run :: (Sized fun, Typeable fun, Ord fun, Monad m) => Config -> Pruner fun m a -> m a
run :: forall fun (m :: * -> *) a.
(Sized fun, Typeable fun, Ord fun, Monad m) =>
Config -> Pruner fun m a -> m a
run Config
config (Pruner Pruner
  fun
  (Pruner
     (PartiallyApplied fun)
     (Pruner
        (Tagged (PartiallyApplied fun))
        (Pruner (Tagged (PartiallyApplied fun)) m)))
  a
x) =
  forall fun (m :: * -> *) a.
(Typeable fun, Ord fun, Sized fun, Monad m) =>
Config -> Pruner fun m a -> m a
Untyped.run Config
config (forall (m :: * -> *) fun a. Monad m => Pruner fun m a -> m a
Background.run (forall fun (pruner :: * -> *) a. Pruner fun pruner a -> pruner a
Types.run (forall fun (pruner :: * -> *) a. Pruner fun pruner a -> pruner a
PartialApplication.run Pruner
  fun
  (Pruner
     (PartiallyApplied fun)
     (Pruner
        (Tagged (PartiallyApplied fun))
        (Pruner (Tagged (PartiallyApplied fun)) m)))
  a
x)))