-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | An equational theorem prover
--   
--   Twee is an experimental equational theorem prover based on
--   Knuth-Bendix completion.
--   
--   Given a set of equational axioms and a set of equational conjectures
--   it will try to prove the conjectures. It will terminate if the
--   conjectures are true but normally fail to terminate if they are false.
--   
--   The input problem should be in TPTP format (see http://www.tptp.org).
--   You can use types and quantifiers, but apart from that the problem
--   must be equational.
@package twee
@version 0.1


-- | Miscellaneous utility functions.
module Twee.Utils
repeatM :: Monad m => m a -> m [a]
partitionBy :: Ord b => (a -> b) -> [a] -> [[a]]
collate :: Ord a => ([b] -> c) -> [(a, b)] -> [(a, c)]
isSorted :: Ord a => [a] -> Bool
isSortedBy :: Ord b => (a -> b) -> [a] -> Bool
usort :: Ord a => [a] -> [a]
usortBy :: (a -> a -> Ordering) -> [a] -> [a]
sortBy' :: Ord b => (a -> b) -> [a] -> [a]
usortBy' :: Ord b => (a -> b) -> [a] -> [a]
orElse :: Ordering -> Ordering -> Ordering
unbuffered :: IO a -> IO a
newtype Max a
Max :: Maybe a -> Max a
[getMax] :: Max a -> Maybe a
getMaxWith :: Ord a => a -> Max a -> a
newtype Min a
Min :: Maybe a -> Min a
[getMin] :: Min a -> Maybe a
getMinWith :: Ord a => a -> Min a -> a
labelM :: Monad m => (a -> m b) -> [a] -> m [(a, b)]
instance GHC.Classes.Ord a => GHC.Base.Monoid (Twee.Utils.Max a)
instance GHC.Classes.Ord a => GHC.Base.Monoid (Twee.Utils.Min a)

module Twee.Term.Core
data Symbol
Symbol :: Bool -> Int -> Int -> Symbol
[isFun] :: Symbol -> Bool
[index] :: Symbol -> Int
[size] :: Symbol -> Int
toSymbol :: Int64 -> Symbol
fromSymbol :: Symbol -> Int64
data TermList f
TermList :: {-# UNPACK #-} !Int -> {-# UNPACK #-} !Int -> {-# UNPACK #-} !ByteArray -> TermList f
[low] :: TermList f -> {-# UNPACK #-} !Int
[high] :: TermList f -> {-# UNPACK #-} !Int
[array] :: TermList f -> {-# UNPACK #-} !ByteArray
at :: Int -> TermList f -> Term f
lenList :: TermList f -> Int
data Term f
Term :: {-# UNPACK #-} !Int64 -> {-# UNPACK #-} !(TermList f) -> Term f
[root] :: Term f -> {-# UNPACK #-} !Int64
[termlist] :: Term f -> {-# UNPACK #-} !(TermList f)
unsafePatHead :: TermList f -> Maybe (Term f, TermList f, TermList f)
patHead :: TermList f -> Maybe (Term f, TermList f, TermList f)
newtype Fun f
MkFun :: Int -> Fun f
newtype Var
MkVar :: Int -> Var
patRoot :: Int64 -> Either Var (Fun f)
patNext :: TermList f -> TermList f
singleton :: Term f -> TermList f
eqSameLength :: TermList f -> TermList f -> Bool
compareContents :: TermList f -> TermList f -> Ordering
newtype Builder f
Builder :: (forall s. Builder1 s) -> Builder f
[unBuilder] :: Builder f -> forall s. Builder1 s
type Builder1 s = State# s -> MutableByteArray# s -> Int# -> Int# -> (# State# s, Int# #)
buildTermList :: Builder f -> TermList f
getArray :: (MutableByteArray s -> Builder1 s) -> Builder1 s
getSize :: (Int -> Builder1 s) -> Builder1 s
getIndex :: (Int -> Builder1 s) -> Builder1 s
putIndex :: Int -> Builder1 s
liftST :: ST s () -> Builder1 s
built :: Builder1 s
then_ :: Builder1 s -> Builder1 s -> Builder1 s
checked :: Int -> Builder1 s -> Builder1 s
emitSymbolBuilder :: Symbol -> Builder f -> Builder f
emitFun :: Fun f -> Builder f -> Builder f
emitVar :: Var -> Builder f
emitTermList :: TermList f -> Builder f
instance GHC.Enum.Enum Twee.Term.Core.Var
instance GHC.Classes.Ord Twee.Term.Core.Var
instance GHC.Classes.Eq Twee.Term.Core.Var
instance GHC.Classes.Eq (Twee.Term.Core.Fun f)
instance GHC.Show.Show Twee.Term.Core.Symbol
instance GHC.Classes.Eq (Twee.Term.Core.Term f)
instance GHC.Classes.Ord (Twee.Term.Core.Term f)
instance GHC.Show.Show (Twee.Term.Core.Fun f)
instance GHC.Show.Show Twee.Term.Core.Var
instance GHC.Classes.Eq (Twee.Term.Core.TermList f)
instance GHC.Classes.Ord (Twee.Term.Core.TermList f)
instance GHC.Base.Monoid (Twee.Term.Core.Builder f)

module Twee.Term
class Build f a | a -> f
builder :: Build f a => a -> Builder f
build :: Build f a => a -> Term f
buildList :: Build f a => a -> TermList f
con :: Fun f -> Builder f
fun :: Build f a => Fun f -> a -> Builder f
var :: Var -> Builder f
listSubstList :: Subst f -> [(Var, TermList f)]
listSubst :: Subst f -> [(Var, Term f)]
foldSubst :: (Var -> TermList f -> b -> b) -> b -> Subst f -> b
allSubst :: (Var -> TermList f -> Bool) -> Subst f -> Bool
forMSubst_ :: Monad m => Subst f -> (Var -> TermList f -> m ()) -> m ()
class Substitution f s | s -> f
evalSubst :: Substitution f s => s -> Var -> Builder f
subst :: Substitution f s => s -> Term f -> Builder f
substList :: Substitution f s => s -> TermList f -> Builder f
newtype Subst f
Subst :: IntMap (TermList f) -> Subst f
[unSubst] :: Subst f -> IntMap (TermList f)
substSize :: Subst f -> Int
lookupList :: Var -> Subst f -> Maybe (TermList f)
extendList :: Var -> TermList f -> Subst f -> Maybe (Subst f)
retract :: Var -> Subst f -> Subst f
unsafeExtendList :: Var -> TermList f -> Subst f -> Subst f
substCompose :: Substitution f s => Subst f -> s -> Subst f
substCompatible :: Subst f -> Subst f -> Bool
substUnion :: Subst f -> Subst f -> Subst f
idempotent :: Subst f -> Bool
idempotentOn :: Subst f -> TermList f -> Bool
close :: TriangleSubst f -> Subst f
canonicalise :: [TermList f] -> Subst f
emptySubst :: Subst f
flattenSubst :: [(Var, Term f)] -> Maybe (Subst f)
match :: Term f -> Term f -> Maybe (Subst f)
matchList :: TermList f -> TermList f -> Maybe (Subst f)
newtype TriangleSubst f
Triangle :: Subst f -> TriangleSubst f
[unTriangle] :: TriangleSubst f -> Subst f
substTri :: Subst f -> Var -> Builder f
unify :: Term f -> Term f -> Maybe (Subst f)
unifyList :: TermList f -> TermList f -> Maybe (Subst f)
unifyTri :: Term f -> Term f -> Maybe (TriangleSubst f)
unifyListTri :: TermList f -> TermList f -> Maybe (TriangleSubst f)
children :: Term f -> TermList f
fromTermList :: TermList f -> [Term f]
lookup :: Var -> Subst f -> Maybe (Term f)
extend :: Var -> Term f -> Subst f -> Maybe (Subst f)
len :: Term f -> Int
emitTerm :: Term f -> Builder f
bound :: Term f -> Int
boundList :: TermList f -> Int
occurs :: Var -> Term f -> Bool
occursList :: Var -> TermList f -> Bool
termListToList :: TermList f -> [Term f]
emptyTermList :: TermList f
subtermsList :: TermList f -> [Term f]
subterms :: Term f -> [Term f]
properSubtermsList :: TermList f -> [Term f]
properSubterms :: Term f -> [Term f]
isFun :: Term f -> Bool
isVar :: Term f -> Bool
isInstanceOf :: Term f -> Term f -> Bool
isVariantOf :: Term f -> Term f -> Bool
mapFun :: (Fun f -> Fun g) -> Term f -> Builder g
mapFunList :: (Fun f -> Fun g) -> TermList f -> Builder g
class Numbered f
fromInt :: Numbered f => Int -> f
toInt :: Numbered f => f -> Int
fromFun :: Numbered f => Fun f -> f
toFun :: Numbered f => f -> Fun f
app :: Numbered a => a -> [Term a] -> Term a
data Term f
data TermList f
at :: Int -> TermList f -> Term f
lenList :: TermList f -> Int
newtype Fun f
MkFun :: Int -> Fun f
newtype Var
MkVar :: Int -> Var
singleton :: Term f -> TermList f
data Builder f
instance GHC.Show.Show (Twee.Term.TriangleSubst f)
instance Twee.Term.Build f (Twee.Term.Core.Builder f)
instance Twee.Term.Build f (Twee.Term.Core.Term f)
instance Twee.Term.Build f (Twee.Term.Core.TermList f)
instance Twee.Term.Build f a => Twee.Term.Build f [a]
instance (Twee.Term.Build f a, v ~ Twee.Term.Core.Var) => Twee.Term.Substitution f (v -> a)
instance Twee.Term.Substitution f (Twee.Term.Subst f)
instance Twee.Term.Substitution f (Twee.Term.TriangleSubst f)
instance GHC.Show.Show (Twee.Term.Core.Term f)
instance GHC.Show.Show (Twee.Term.Core.TermList f)
instance GHC.Show.Show (Twee.Term.Subst f)
instance (GHC.Classes.Ord f, Twee.Term.Numbered f) => GHC.Classes.Ord (Twee.Term.Core.Fun f)


-- | Pretty-printing of terms and assorted other values.
module Twee.Pretty
prettyPrint :: Pretty a => a -> IO ()
pPrintParen :: Bool -> Doc -> Doc
pPrintTuple :: [Doc] -> Doc
pPrintSet :: [Doc] -> Doc

-- | Generate a list of candidate names for pretty-printing.
supply :: [String] -> [String]

-- | A class for customising the printing of function symbols.
class Pretty f => PrettyTerm f where termStyle _ = curried
termStyle :: PrettyTerm f => f -> TermStyle

-- | Defines how to print out a function symbol.
newtype TermStyle
TermStyle :: (forall a. Pretty a => PrettyLevel -> Rational -> Doc -> [a] -> Doc) -> TermStyle

-- | Takes the pretty-printing level, precedence, pretty-printed function
--   symbol and list of arguments and prints the term.
[pPrintTerm] :: TermStyle -> forall a. Pretty a => PrettyLevel -> Rational -> Doc -> [a] -> Doc

-- | For operators like <tt>$</tt> that should be printed as a blank space.
invisible :: TermStyle

-- | For functions that should be printed curried.
curried :: TermStyle

-- | For functions that should be printed uncurried.
uncurried :: TermStyle

-- | For prefix operators.
prefix :: TermStyle

-- | For postfix operators.
postfix :: TermStyle

-- | A helper function that deals with under- and oversaturated
--   applications.
fixedArity :: Int -> TermStyle -> TermStyle

-- | A helper function that drops a certain number of arguments.
implicitArguments :: Int -> TermStyle -> TermStyle

-- | For infix operators.
infixStyle :: Int -> TermStyle

-- | For tuples.
tupleStyle :: TermStyle

-- | Pretty printing class. The precedence level is used in a similar way
--   as in the <a>Show</a> class. Minimal complete definition is either
--   <a>pPrintPrec</a> or <a>pPrint</a>.
class Pretty a
pPrintPrec :: Pretty a => PrettyLevel -> Rational -> a -> Doc
pPrint :: Pretty a => a -> Doc
pPrintList :: Pretty a => PrettyLevel -> [a] -> Doc
instance Text.PrettyPrint.HughesPJClass.Pretty Text.PrettyPrint.HughesPJ.Doc
instance Text.PrettyPrint.HughesPJClass.Pretty a => Text.PrettyPrint.HughesPJClass.Pretty (Data.Set.Base.Set a)
instance Text.PrettyPrint.HughesPJClass.Pretty Twee.Term.Core.Var
instance (Text.PrettyPrint.HughesPJClass.Pretty k, Text.PrettyPrint.HughesPJClass.Pretty v) => Text.PrettyPrint.HughesPJClass.Pretty (Data.Map.Base.Map k v)
instance (GHC.Classes.Eq a, GHC.Real.Integral a, Text.PrettyPrint.HughesPJClass.Pretty a) => Text.PrettyPrint.HughesPJClass.Pretty (GHC.Real.Ratio a)
instance (Twee.Term.Numbered f, Text.PrettyPrint.HughesPJClass.Pretty f) => Text.PrettyPrint.HughesPJClass.Pretty (Twee.Term.Core.Fun f)
instance (Twee.Term.Numbered f, Twee.Pretty.PrettyTerm f) => Text.PrettyPrint.HughesPJClass.Pretty (Twee.Term.Core.Term f)
instance (Twee.Term.Numbered f, Twee.Pretty.PrettyTerm f) => Text.PrettyPrint.HughesPJClass.Pretty (Twee.Term.Core.TermList f)
instance (Twee.Term.Numbered f, Twee.Pretty.PrettyTerm f) => Text.PrettyPrint.HughesPJClass.Pretty (Twee.Term.Subst f)


-- | Assignment of unique IDs to values. Inspired by the <tt>intern</tt>
--   package.
module Twee.Label
class Ord a => Labelled a where initialId _ = 0
cache :: Labelled a => Cache a
initialId :: Labelled a => a -> Int
type Cache a = IORef (CacheState a)
data CacheState a
CacheState :: {-# UNPACK #-} !Int -> !(IntMap a) -> !(Map a Int) -> CacheState a
[nextId] :: CacheState a -> {-# UNPACK #-} !Int
[to] :: CacheState a -> !(IntMap a)
[from] :: CacheState a -> !(Map a Int)
mkCache :: forall a. Labelled a => Cache a
label :: Labelled a => a -> Int
find :: Labelled a => Int -> Maybe a
instance GHC.Show.Show a => GHC.Show.Show (Twee.Label.CacheState a)

module Twee.Constraints
data Atom f
Constant :: (Fun f) -> Atom f
Variable :: Var -> Atom f
atoms :: Term f -> [Atom f]
toTerm :: Atom f -> Term f
fromTerm :: Term f -> Maybe (Atom f)
data Formula f
Less :: (Atom f) -> (Atom f) -> Formula f
LessEq :: (Atom f) -> (Atom f) -> Formula f
And :: [Formula f] -> Formula f
Or :: [Formula f] -> Formula f
negateFormula :: Formula f -> Formula f
conj :: (Foldable t, Numbered f, Ord f) => t (Formula f) -> Formula f
disj :: (Foldable t, Numbered f, Ord f) => t (Formula f) -> Formula f
(&&&) :: (Ord f, Numbered f) => Formula f -> Formula f -> Formula f
(|||) :: (Ord f, Numbered f) => Formula f -> Formula f -> Formula f
true :: Formula f
false :: Formula f
data Branch f
Branch :: [Fun f] -> [(Atom f, Atom f)] -> [(Atom f, Atom f)] -> Branch f
[funs] :: Branch f -> [Fun f]
[less] :: Branch f -> [(Atom f, Atom f)]
[equals] :: Branch f -> [(Atom f, Atom f)]
trueBranch :: Branch f
norm :: Eq f => Branch f -> Atom f -> Atom f
contradictory :: (Numbered f, Minimal f, Ord f) => Branch f -> Bool
formAnd :: (Numbered f, Minimal f, Ord f) => Formula f -> [Branch f] -> [Branch f]
branches :: (Numbered f, Minimal f, Ord f) => Formula f -> [Branch f]
addLess :: (Numbered f, Minimal f, Ord f) => Atom f -> Atom f -> Branch f -> [Branch f]
addEquals :: (Numbered f, Minimal f, Ord f) => Atom f -> Atom f -> Branch f -> [Branch f]
addTerm :: (Numbered f, Minimal f, Ord f) => Atom f -> Branch f -> Branch f
newtype Model f
Model :: (Map (Atom f) (Int, Int)) -> Model f
modelToLiterals :: Model f -> [Formula f]
modelFromOrder :: (Numbered f, Minimal f, Ord f) => [Atom f] -> Model f
weakenModel :: Ord (Fun f) => Model f -> [Model f]
varInModel :: (Numbered f, Minimal f, Ord f) => Model f -> Var -> Bool
varGroups :: (Numbered f, Minimal f, Ord f) => Model f -> [(Fun f, [Var], Maybe (Fun f))]
class Minimal a
minimal :: Minimal a => a
lessEqInModel :: (Numbered f, Minimal f, Ord f) => Model f -> Atom f -> Atom f -> Maybe Strictness
solve :: (Numbered f, Minimal f, Ord f, PrettyTerm f) => [Atom f] -> Branch f -> Either (Model f) (Subst f)
class Ord f => Ordered f where orientTerms t u | t == u = Just EQ | lessEq t u = Just LT | lessEq u t = Just GT | otherwise = Nothing
orientTerms :: Ordered f => Term f -> Term f -> Maybe Ordering
lessEq :: Ordered f => Term f -> Term f -> Bool
lessIn :: Ordered f => Model f -> Term f -> Term f -> Maybe Strictness
data Strictness
Strict :: Strictness
Nonstrict :: Strictness
instance GHC.Show.Show Twee.Constraints.Strictness
instance GHC.Classes.Eq Twee.Constraints.Strictness
instance GHC.Show.Show (Twee.Constraints.Model f)
instance GHC.Show.Show (Twee.Constraints.Formula f)
instance GHC.Show.Show (Twee.Constraints.Atom f)
instance GHC.Classes.Eq (Twee.Term.Core.Fun f) => GHC.Classes.Eq (Twee.Constraints.Atom f)
instance GHC.Classes.Ord (Twee.Term.Core.Fun f) => GHC.Classes.Ord (Twee.Constraints.Atom f)
instance GHC.Classes.Eq (Twee.Term.Core.Fun f) => GHC.Classes.Eq (Twee.Constraints.Formula f)
instance GHC.Classes.Ord (Twee.Term.Core.Fun f) => GHC.Classes.Ord (Twee.Constraints.Formula f)
instance GHC.Classes.Eq (Twee.Term.Core.Fun f) => GHC.Classes.Eq (Twee.Constraints.Branch f)
instance GHC.Classes.Ord (Twee.Term.Core.Fun f) => GHC.Classes.Ord (Twee.Constraints.Branch f)
instance (Twee.Term.Numbered f, Twee.Pretty.PrettyTerm f) => Text.PrettyPrint.HughesPJClass.Pretty (Twee.Constraints.Atom f)
instance (Twee.Term.Numbered f, Twee.Pretty.PrettyTerm f) => Text.PrettyPrint.HughesPJClass.Pretty (Twee.Constraints.Formula f)
instance (Twee.Term.Numbered f, Twee.Pretty.PrettyTerm f) => Text.PrettyPrint.HughesPJClass.Pretty (Twee.Constraints.Branch f)
instance (Twee.Term.Numbered f, Twee.Pretty.PrettyTerm f) => Text.PrettyPrint.HughesPJClass.Pretty (Twee.Constraints.Model f)
instance (Twee.Term.Numbered f, Twee.Constraints.Minimal f) => Twee.Constraints.Minimal (Twee.Term.Core.Fun f)

module Twee.Base
class Symbolic a where type ConstantOf a where {
    type family ConstantOf a;
}
term :: Symbolic a => a -> TermOf a
termsDL :: Symbolic a => a -> DList (TermListOf a)
replace :: Symbolic a => (TermListOf a -> BuilderOf a) -> a -> a
terms :: Symbolic a => a -> [TermListOf a]
subst :: (Symbolic a, Substitution (ConstantOf a) s) => s -> a -> a
type TermOf a = Term (ConstantOf a)
type TermListOf a = TermList (ConstantOf a)
type SubstOf a = Subst (ConstantOf a)
type BuilderOf a = Builder (ConstantOf a)
type FunOf a = Fun (ConstantOf a)
vars :: Symbolic a => a -> [Var]
isGround :: Symbolic a => a -> Bool
funs :: Symbolic a => a -> [FunOf a]
occ :: Symbolic a => FunOf a -> a -> Int
canonicalise :: Symbolic a => a -> a
class Minimal a
minimal :: Minimal a => a
minimalTerm :: (Numbered f, Minimal f) => Term f
isMinimal :: (Numbered f, Minimal f) => Term f -> Bool
class Skolem f
skolem :: Skolem f => Var -> f
class Arity f
arity :: Arity f => f -> Int
class Sized a
size :: Sized a => a -> Int
class Ord f => Ordered f where orientTerms t u | t == u = Just EQ | lessEq t u = Just LT | lessEq u t = Just GT | otherwise = Nothing
orientTerms :: Ordered f => Term f -> Term f -> Maybe Ordering
lessEq :: Ordered f => Term f -> Term f -> Bool
lessIn :: Ordered f => Model f -> Term f -> Term f -> Maybe Strictness
data Strictness
Strict :: Strictness
Nonstrict :: Strictness
class (Numbered f, Ordered f, Arity f, Sized f, Minimal f, Skolem f, PrettyTerm f) => Function f
data Extended f
Minimal :: Extended f
Skolem :: Int -> Extended f
Function :: f -> Extended f
extended :: Numbered f => TermList f -> Builder (Extended f)
unextended :: Numbered f => TermList (Extended f) -> Builder f
instance GHC.Base.Functor Twee.Base.Extended
instance GHC.Show.Show f => GHC.Show.Show (Twee.Base.Extended f)
instance GHC.Classes.Ord f => GHC.Classes.Ord (Twee.Base.Extended f)
instance GHC.Classes.Eq f => GHC.Classes.Eq (Twee.Base.Extended f)
instance Twee.Base.Symbolic (Twee.Term.Core.Term f)
instance Twee.Base.Symbolic (Twee.Term.Core.TermList f)
instance (Twee.Base.ConstantOf a ~ Twee.Base.ConstantOf b, Twee.Base.Symbolic a, Twee.Base.Symbolic b) => Twee.Base.Symbolic (a, b)
instance (Twee.Base.ConstantOf a ~ Twee.Base.ConstantOf b, Twee.Base.ConstantOf a ~ Twee.Base.ConstantOf c, Twee.Base.Symbolic a, Twee.Base.Symbolic b, Twee.Base.Symbolic c) => Twee.Base.Symbolic (a, b, c)
instance Twee.Base.Symbolic a => Twee.Base.Symbolic [a]
instance (Twee.Term.Numbered f, Twee.Base.Skolem f) => Twee.Base.Skolem (Twee.Term.Core.Fun f)
instance (Twee.Term.Numbered f, Twee.Base.Arity f) => Twee.Base.Arity (Twee.Term.Core.Fun f)
instance (Twee.Base.Sized f, Twee.Term.Numbered f) => Twee.Base.Sized (Twee.Term.Core.Fun f)
instance (Twee.Base.Sized f, Twee.Term.Numbered f) => Twee.Base.Sized (Twee.Term.Core.TermList f)
instance (Twee.Base.Sized f, Twee.Term.Numbered f) => Twee.Base.Sized (Twee.Term.Core.Term f)
instance (Twee.Term.Numbered f, Twee.Constraints.Ordered f, Twee.Base.Arity f, Twee.Base.Sized f, Twee.Constraints.Minimal f, Twee.Base.Skolem f, Twee.Pretty.PrettyTerm f) => Twee.Base.Function f
instance Twee.Constraints.Minimal (Twee.Base.Extended f)
instance Twee.Base.Skolem (Twee.Base.Extended f)
instance Twee.Term.Numbered f => Twee.Term.Numbered (Twee.Base.Extended f)
instance Text.PrettyPrint.HughesPJClass.Pretty f => Text.PrettyPrint.HughesPJClass.Pretty (Twee.Base.Extended f)
instance Twee.Pretty.PrettyTerm f => Twee.Pretty.PrettyTerm (Twee.Base.Extended f)
instance Twee.Base.Sized f => Twee.Base.Sized (Twee.Base.Extended f)
instance Twee.Base.Arity f => Twee.Base.Arity (Twee.Base.Extended f)

module Twee.KBO
lessEq :: Function f => Term f -> Term f -> Bool
lessIn :: Function f => Model f -> Term f -> Term f -> Maybe Strictness
sizeLessIn :: Function f => Model f -> Term f -> Term f -> Maybe Strictness
minimumIn :: Function f => Model f -> Map Var Int -> Maybe Int
lexLessIn :: Function f => Model f -> Term f -> Term f -> Maybe Strictness

module Twee.LPO
lessEq :: Function f => Term f -> Term f -> Bool
lessIn :: Function f => Model f -> Term f -> Term f -> Maybe Strictness

module Twee.Queue
class Heuristic h where reinsert = insert members = unfoldr remove
insert :: (Heuristic h, Ord a) => a -> h a -> h a
remove :: (Heuristic h, Ord a) => h a -> Maybe (a, h a)
reinsert :: (Heuristic h, Ord a) => a -> h a -> h a
members :: (Heuristic h, Ord a) => h a -> [a]
emptyHeap :: Heap a
data FIFO a
FIFO :: [a] -> [a] -> FIFO a
emptyFIFO :: FIFO a
data Either1 h1 h2 a
Left1 :: (h1 a) -> Either1 h1 h2 a
Right1 :: (h2 a) -> Either1 h1 h2 a
data Mix h a
Mix :: {-# UNPACK #-} !Int -> {-# UNPACK #-} !Int -> {-# UNPACK #-} !Int -> !(h a) -> !(h a) -> Mix h a
[takeLeft] :: Mix h a -> {-# UNPACK #-} !Int
[takeRight] :: Mix h a -> {-# UNPACK #-} !Int
[takeNext] :: Mix h a -> {-# UNPACK #-} !Int
[left] :: Mix h a -> !(h a)
[right] :: Mix h a -> !(h a)
emptyMix :: Int -> Int -> h a -> h a -> Mix h a
data Queue h a
Queue :: !(h a) -> h a -> Set Label -> Label -> Queue h a
[queue] :: Queue h a -> !(h a)
[emptyQueue] :: Queue h a -> h a
[queueLabels] :: Queue h a -> Set Label
[nextLabel] :: Queue h a -> Label
class Ord a => Labels a
labels :: Labels a => a -> [Label]
empty :: h a -> Queue h a
emptyFrom :: Queue q a -> Queue q a
enqueue :: (Heuristic h, Labels a) => a -> Queue h a -> Queue h a
reenqueue :: (Heuristic h, Labels a) => a -> Queue h a -> Queue h a
dequeue :: (Heuristic h, Labels a) => Queue h a -> Maybe (a, Queue h a)
queueSize :: (Heuristic h, Labels a) => Queue h a -> Int
toList :: (Heuristic h, Labels a) => Queue h a -> [a]
newtype Label
Label :: Int -> Label
noLabel :: Label
newLabel :: Queue h a -> (Label, Queue h a)
deleteLabel :: Label -> Queue h a -> Queue h a
data Labelled a
Labelled :: Label -> a -> Labelled a
[labelOf] :: Labelled a -> Label
[peel] :: Labelled a -> a
moveLabel :: Functor f => Labelled (f a) -> f (Labelled a)
unlabelled :: a -> Labelled a

-- | A min-heap of values of type <tt>a</tt>.
data Heap a :: * -> *
instance GHC.Base.Functor Twee.Queue.Labelled
instance GHC.Show.Show a => GHC.Show.Show (Twee.Queue.Labelled a)
instance GHC.Show.Show (h a) => GHC.Show.Show (Twee.Queue.Queue h a)
instance GHC.Real.Real Twee.Queue.Label
instance GHC.Enum.Enum Twee.Queue.Label
instance GHC.Real.Integral Twee.Queue.Label
instance GHC.Show.Show Twee.Queue.Label
instance GHC.Num.Num Twee.Queue.Label
instance GHC.Classes.Ord Twee.Queue.Label
instance GHC.Classes.Eq Twee.Queue.Label
instance GHC.Show.Show (h a) => GHC.Show.Show (Twee.Queue.Mix h a)
instance (GHC.Show.Show (h2 a), GHC.Show.Show (h1 a)) => GHC.Show.Show (Twee.Queue.Either1 h1 h2 a)
instance GHC.Show.Show a => GHC.Show.Show (Twee.Queue.FIFO a)
instance Twee.Queue.Heuristic Data.Heap.Heap
instance Twee.Queue.Heuristic Twee.Queue.FIFO
instance (Twee.Queue.Heuristic h1, Twee.Queue.Heuristic h2) => Twee.Queue.Heuristic (Twee.Queue.Either1 h1 h2)
instance Twee.Queue.Heuristic h => Twee.Queue.Heuristic (Twee.Queue.Mix h)
instance GHC.Classes.Eq (Twee.Queue.Labelled a)
instance GHC.Classes.Ord (Twee.Queue.Labelled a)
instance Twee.Base.Symbolic a => Twee.Base.Symbolic (Twee.Queue.Labelled a)
instance Text.PrettyPrint.HughesPJClass.Pretty a => Text.PrettyPrint.HughesPJClass.Pretty (Twee.Queue.Labelled a)

module Twee.Array
data Array a
Array :: {-# UNPACK #-} !Int -> {-# UNPACK #-} !(Array a) -> Array a
[arraySize] :: Array a -> {-# UNPACK #-} !Int
[arrayContents] :: Array a -> {-# UNPACK #-} !(Array a)
class Default a
def :: Default a => a
toList :: Array a -> [(Int, a)]
newArray :: Default a => Array a
(!) :: Default a => Array a -> Int -> a
update :: Default a => Int -> a -> Array a -> Array a
instance GHC.Show.Show a => GHC.Show.Show (Twee.Array.Array a)

module Twee.Index
data Index a
Index :: {-# UNPACK #-} !Int -> [Entry a] -> {-# UNPACK #-} !(Array (Index a)) -> !(Index a) -> Index a
[size] :: Index a -> {-# UNPACK #-} !Int
[here] :: Index a -> [Entry a]
[fun] :: Index a -> {-# UNPACK #-} !(Array (Index a))
[var] :: Index a -> !(Index a)
Singleton :: {-# UNPACK #-} !(TermListOf a) -> {-# UNPACK #-} !(Entry a) -> Index a
[key] :: Index a -> {-# UNPACK #-} !(TermListOf a)
[value] :: Index a -> {-# UNPACK #-} !(Entry a)
Nil :: Index a
data Entry a
Entry :: {-# UNPACK #-} !(TermOf a) -> a -> Entry a
[e_key] :: Entry a -> {-# UNPACK #-} !(TermOf a)
[e_value] :: Entry a -> a
null :: Index a -> Bool
singleton :: Symbolic a => a -> Index a
insert :: Symbolic a => a -> Index a -> Index a
expand :: TermListOf a -> Entry a -> Index a
delete :: (Eq a, Symbolic a) => a -> Index a -> Index a
elem :: (Eq a, Symbolic a) => a -> Index a -> Bool
data Match a
Match :: a -> SubstOf a -> Match a
[matchResult] :: Match a -> a
[matchSubst] :: Match a -> SubstOf a
newtype Frozen a
Frozen :: (TermListOf a -> [Match a]) -> Frozen a
[matchesList_] :: Frozen a -> TermListOf a -> [Match a]
matchesList :: TermListOf a -> Frozen a -> [Match a]
lookup :: Symbolic a => TermOf a -> Frozen a -> [a]
matches :: TermOf a -> Frozen a -> [Match a]
freeze :: Index a -> Frozen a
find :: TermListOf a -> Index a -> [Match a] -> [Match a]
elems :: Index a -> [a]
map :: (ConstantOf a ~ ConstantOf b) => (a -> b) -> Frozen a -> Frozen b
filter :: (a -> Bool) -> Frozen a -> Frozen a
union :: Frozen a -> Frozen a -> Frozen a
instance GHC.Show.Show a => GHC.Show.Show (Twee.Index.Index a)
instance GHC.Show.Show a => GHC.Show.Show (Twee.Index.Entry a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Twee.Index.Entry a)
instance Twee.Array.Default (Twee.Index.Index a)

module Twee.Indexes
class Rated a
rating :: Rated a => a -> Int
maxRating :: Rated a => a -> Int
newtype Indexes a
Indexes :: Array Int (Index a) -> Indexes a
[unIndexes] :: Indexes a -> Array Int (Index a)
empty :: forall a. Rated a => Indexes a
singleton :: (Symbolic a, Rated a) => a -> Indexes a
insert :: forall a. (Symbolic a, Rated a) => a -> Indexes a -> Indexes a
delete :: forall a. (Eq a, Symbolic a, Rated a) => a -> Indexes a -> Indexes a
freeze :: Int -> Indexes a -> Frozen a
elems :: forall a. Rated a => Indexes a -> [a]
instance GHC.Show.Show a => GHC.Show.Show (Twee.Indexes.Indexes a)

module Twee.Rule
data Rule f
Rule :: Orientation f -> Term f -> Term f -> Rule f
[orientation] :: Rule f -> Orientation f
[lhs] :: Rule f -> Term f
[rhs] :: Rule f -> Term f
data Orientation f
Oriented :: Orientation f
WeaklyOriented :: [Term f] -> Orientation f
Permutative :: [(Term f, Term f)] -> Orientation f
Unoriented :: Orientation f
oriented :: Orientation f -> Bool
pPrintRule :: (Numbered f, PrettyTerm f) => Term f -> Term f -> Doc
data Equation f
(:=:) :: Term f -> Term f -> Equation f
type EquationOf a = Equation (ConstantOf a)
order :: Function f => Equation f -> Equation f
unorient :: Rule f -> Equation f
orient :: Function f => Equation f -> [Rule f]
rule :: Function f => Term f -> Term f -> Rule f
bothSides :: (Term f -> Term f') -> Equation f -> Equation f'
trivial :: Eq f => Equation f -> Bool
type Strategy f = Term f -> [Reduction f]
data Reduction f
Step :: (Rule f) -> (Subst f) -> Reduction f
Trans :: (Reduction f) -> (Reduction f) -> Reduction f
Parallel :: [(Int, Reduction f)] -> (Term f) -> Reduction f
result :: Reduction f -> Term f
pPrintReduction :: (Numbered f, PrettyTerm f) => Reduction f -> Doc
steps :: Reduction f -> [(Rule f, Subst f)]
anywhere1 :: (Numbered f, PrettyTerm f) => Strategy f -> Reduction f -> Maybe (Reduction f)
normaliseWith :: (Numbered f, PrettyTerm f) => Strategy f -> Term f -> Reduction f
normalForms :: Function f => Strategy f -> [Term f] -> Set (Term f)
anywhere :: Strategy f -> Strategy f
nested :: Strategy f -> Strategy f
rewrite :: Function f => String -> (Rule f -> Subst f -> Bool) -> Frozen (Rule f) -> Strategy f
tryRule :: Function f => (Rule f -> Subst f -> Bool) -> Rule f -> Strategy f
simplifies :: Function f => Rule f -> Subst f -> Bool
reducesWith :: Function f => (Term f -> Term f -> Bool) -> Rule f -> Subst f -> Bool
reduces :: Function f => Rule f -> Subst f -> Bool
reducesInModel :: Function f => Model f -> Rule f -> Subst f -> Bool
reducesSkolem :: Function f => Rule f -> Subst f -> Bool
reducesSub :: Function f => Term f -> Rule f -> Subst f -> Bool
instance GHC.Show.Show (Twee.Rule.Reduction f)
instance GHC.Show.Show (Twee.Rule.Equation f)
instance GHC.Classes.Ord (Twee.Rule.Equation f)
instance GHC.Classes.Eq (Twee.Rule.Equation f)
instance GHC.Show.Show (Twee.Rule.Rule f)
instance GHC.Classes.Ord (Twee.Rule.Rule f)
instance GHC.Classes.Eq (Twee.Rule.Rule f)
instance GHC.Show.Show (Twee.Rule.Orientation f)
instance GHC.Classes.Eq (Twee.Rule.Orientation f)
instance GHC.Classes.Ord (Twee.Rule.Orientation f)
instance Twee.Base.Symbolic (Twee.Rule.Rule f)
instance Twee.Base.Symbolic (Twee.Rule.Orientation f)
instance (Twee.Term.Numbered f, Twee.Pretty.PrettyTerm f) => Text.PrettyPrint.HughesPJClass.Pretty (Twee.Rule.Rule f)
instance Twee.Base.Symbolic (Twee.Rule.Equation f)
instance (Twee.Term.Numbered f, Twee.Pretty.PrettyTerm f) => Text.PrettyPrint.HughesPJClass.Pretty (Twee.Rule.Equation f)
instance (Twee.Term.Numbered f, Twee.Base.Sized f) => Twee.Base.Sized (Twee.Rule.Equation f)
instance (Twee.Term.Numbered f, Twee.Pretty.PrettyTerm f) => Text.PrettyPrint.HughesPJClass.Pretty (Twee.Rule.Reduction f)

module Twee
data Twee f
Twee :: Maybe Int -> {-# UNPACK #-} !(Indexes (Labelled (Modelled (Critical (Rule f))))) -> {-# UNPACK #-} !(Indexes (Rule f)) -> !(Index (Labelled (CancellationRule f))) -> [Set (Term f)] -> Int -> Int -> Int -> Int -> Int -> !(Queue (Mix (Either1 FIFO Heap)) (Passive f)) -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Maybe Int -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Int -> Int -> Map JoinReason Int -> Twee f
[maxSize] :: Twee f -> Maybe Int
[labelledRules] :: Twee f -> {-# UNPACK #-} !(Indexes (Labelled (Modelled (Critical (Rule f)))))
[extraRules] :: Twee f -> {-# UNPACK #-} !(Indexes (Rule f))
[cancellationRules] :: Twee f -> !(Index (Labelled (CancellationRule f)))
[goals] :: Twee f -> [Set (Term f)]
[totalCPs] :: Twee f -> Int
[processedCPs] :: Twee f -> Int
[renormaliseAt] :: Twee f -> Int
[minimumCPSetSize] :: Twee f -> Int
[cpSplits] :: Twee f -> Int
[queue] :: Twee f -> !(Queue (Mix (Either1 FIFO Heap)) (Passive f))
[useGeneralSuperpositions] :: Twee f -> Bool
[useGroundJoining] :: Twee f -> Bool
[useConnectedness] :: Twee f -> Bool
[useSetJoining] :: Twee f -> Bool
[useSetJoiningForGoals] :: Twee f -> Bool
[useCancellation] :: Twee f -> Bool
[maxCancellationSize] :: Twee f -> Maybe Int
[atomicCancellation] :: Twee f -> Bool
[unifyConstantsInCancellation] :: Twee f -> Bool
[useInterreduction] :: Twee f -> Bool
[useUnsafeInterreduction] :: Twee f -> Bool
[skipCompositeSuperpositions] :: Twee f -> Bool
[tracing] :: Twee f -> Bool
[moreTracing] :: Twee f -> Bool
[lhsWeight] :: Twee f -> Int
[rhsWeight] :: Twee f -> Int
[joinStatistics] :: Twee f -> Map JoinReason Int
initialState :: Int -> Int -> Twee f
addGoals :: [Set (Term f)] -> Twee f -> Twee f
report :: Function f => Twee f -> String
enqueueM :: Function f => Passive f -> State (Twee f) ()
reenqueueM :: Function f => Passive f -> State (Twee f) ()
dequeueM :: Function f => State (Twee f) (Maybe (Passive f))
newLabelM :: State (Twee f) Label
data Modelled a
Modelled :: Model (ConstantOf a) -> [Int] -> a -> Modelled a
[model] :: Modelled a -> Model (ConstantOf a)
[positions] :: Modelled a -> [Int]
[modelled] :: Modelled a -> a
rulesFor :: Function f => Int -> Twee f -> Frozen (Rule f)
easyRules :: Function f => Twee f -> Frozen (Rule f)
rules :: Function f => Twee f -> Frozen (Rule f)
allRules :: Function f => Twee f -> Frozen (Rule f)
normaliseQuickly :: Function f => Twee f -> Term f -> Reduction f
normalise :: Function f => Twee f -> Term f -> Reduction f
normaliseIn :: Function f => Twee f -> Model f -> Term f -> Reduction f
normaliseSub :: Function f => Twee f -> Term f -> Term f -> Reduction f
normaliseSkolem :: Function f => Twee f -> Term f -> Reduction f
reduceCP :: Function f => Twee f -> JoinStage -> (Term f -> Term f) -> Critical (Equation f) -> Either JoinReason (Critical (Equation f))
data JoinStage
Initial :: JoinStage
Simplification :: JoinStage
Reducing :: JoinStage
Subjoining :: JoinStage
data JoinReason
Trivial :: JoinStage -> JoinReason
Subsumed :: JoinStage -> JoinReason
SetJoining :: JoinReason
GroundJoined :: JoinReason
normaliseCPQuickly :: Function f => Twee f -> Critical (Equation f) -> Either JoinReason (Critical (Equation f))
normaliseCPReducing :: Function f => Twee f -> Critical (Equation f) -> Either JoinReason (Critical (Equation f))
normaliseCP :: Function f => Twee f -> Critical (Equation f) -> Either JoinReason (Critical (Equation f))
complete :: Function f => State (Twee f) ()
complete1 :: Function f => State (Twee f) Bool
renormaliseGoals :: Function f => State (Twee f) ()
normaliseCPs :: forall f. Function f => State (Twee f) ()
consider :: Function f => Int -> Label -> Label -> Critical (Equation f) -> State (Twee f) Bool
groundJoinableEq :: Function f => Twee f -> Equation f -> Bool
groundJoinable :: Function f => Twee f -> Critical (Equation f) -> Bool
groundJoin :: Function f => Twee f -> [Branch f] -> Critical (Equation f) -> Either (Model f) [Critical (Equation f)]
valid :: Function f => Model f -> Reduction f -> Bool
optimise :: a -> (a -> [a]) -> (a -> Bool) -> a
addRule :: Function f => Modelled (Critical (Rule f)) -> State (Twee f) Label
addExtraRule :: Function f => Rule f -> State (Twee f) ()
extraRuleSafe :: Function f => Twee f -> Rule f -> Bool
deleteRule :: Function f => Label -> Modelled (Critical (Rule f)) -> State (Twee f) ()
data Simplification f
Simplify :: (Model f) -> (Modelled (Critical (Rule f))) -> Simplification f
Reorient :: (Modelled (Critical (Rule f))) -> Simplification f
interreduce :: Function f => Rule f -> State (Twee f) ()
reduceWith :: Function f => Twee f -> Label -> Rule f -> Modelled (Critical (Rule f)) -> Maybe (Simplification f)
simplifyRule :: Function f => Label -> Model f -> Modelled (Critical (Rule f)) -> State (Twee f) ()
newEquation :: Function f => Equation f -> State (Twee f) ()
noCritInfo :: Function f => CritInfo f
data CancellationRule f
CancellationRule :: [[Term f]] -> {-# UNPACK #-} !(Rule f) -> CancellationRule f
[cr_unified] :: CancellationRule f -> [[Term f]]
[cr_rule] :: CancellationRule f -> {-# UNPACK #-} !(Rule f)
toCancellationRule :: Function f => Twee f -> Rule f -> Maybe (CancellationRule f)
addCancellationRule :: Function f => Label -> Rule f -> Twee f -> Twee f
deleteCancellationRule :: Function f => Label -> Rule f -> Twee f -> Twee f
data Critical a
Critical :: CritInfo (ConstantOf a) -> a -> Critical a
[critInfo] :: Critical a -> CritInfo (ConstantOf a)
[critical] :: Critical a -> a
data CritInfo f
CritInfo :: Term f -> Int -> CritInfo f
[top] :: CritInfo f -> Term f
[overlap] :: CritInfo f -> Int
data CPInfo
CPInfo :: {-# UNPACK #-} !Int -> {-# UNPACK #-} !Int -> {-# UNPACK #-} !Label -> {-# UNPACK #-} !Label -> CPInfo
[cpWeight] :: CPInfo -> {-# UNPACK #-} !Int
[cpWeight2] :: CPInfo -> {-# UNPACK #-} !Int
[cpAge1] :: CPInfo -> {-# UNPACK #-} !Label
[cpAge2] :: CPInfo -> {-# UNPACK #-} !Label
data CP f
CP :: {-# UNPACK #-} !CPInfo -> {-# UNPACK #-} !(Critical (Equation f)) -> {-# UNPACK #-} !Label -> {-# UNPACK #-} !Label -> CP f
[info] :: CP f -> {-# UNPACK #-} !CPInfo
[cp] :: CP f -> {-# UNPACK #-} !(Critical (Equation f))
[l1] :: CP f -> {-# UNPACK #-} !Label
[l2] :: CP f -> {-# UNPACK #-} !Label
data CPs f
CPs :: {-# UNPACK #-} !CPInfo -> {-# UNPACK #-} !Label -> {-# UNPACK #-} !Label -> {-# UNPACK #-} !Label -> {-# UNPACK #-} !Int -> {-# UNPACK #-} !(Labelled (Rule f)) -> CPs f
[best] :: CPs f -> {-# UNPACK #-} !CPInfo
[label] :: CPs f -> {-# UNPACK #-} !Label
[lower] :: CPs f -> {-# UNPACK #-} !Label
[upper] :: CPs f -> {-# UNPACK #-} !Label
[count] :: CPs f -> {-# UNPACK #-} !Int
[from] :: CPs f -> {-# UNPACK #-} !(Labelled (Rule f))
data Passive f
SingleCP :: {-# UNPACK #-} !(CP f) -> Passive f
ManyCPs :: {-# UNPACK #-} !(CPs f) -> Passive f
passiveCount :: Passive f -> Int
data InitialCP f
InitialCP :: (Term f, Label) -> Bool -> Labelled (Critical (Equation f)) -> InitialCP f
[cpId] :: InitialCP f -> (Term f, Label)
[cpOK] :: InitialCP f -> Bool
[cpCP] :: InitialCP f -> Labelled (Critical (Equation f))
criticalPairs :: Function f => Twee f -> Label -> Label -> Rule f -> [Labelled (Critical (Equation f))]
ruleOverlaps :: Twee f -> Term f -> [Int]
overlaps :: [Int] -> Term f -> Term f -> [(Subst f, Int)]
emitReplacement :: Int -> Term f -> TermList f -> Builder f
criticalPairs1 :: Function f => Twee f -> [Int] -> Rule f -> [Labelled (Rule f)] -> [Labelled (Critical (Equation f))]
queueCP :: Function f => (Passive f -> State (Twee f) ()) -> (Equation f -> Bool) -> Label -> Label -> Critical (Equation f) -> State (Twee f) ()
queueCPs :: (Function f, Ord a) => (Passive f -> State (Twee f) ()) -> Label -> Label -> (Label -> a) -> Labelled (Rule f) -> State (Twee f) ()
queueCPsSplit :: Function f => (Passive f -> State (Twee f) ()) -> Label -> Label -> Labelled (Rule f) -> State (Twee f) ()
toCPs :: Function f => Twee f -> Label -> Label -> Labelled (Rule f) -> [CP f]
toCP :: Function f => Twee f -> Label -> Label -> (Equation f -> Bool) -> Critical (Equation f) -> Maybe (CP f)
cancelledWeight :: Function f => Twee f -> (Equation f -> Bool) -> Equation f -> Int
bestCancellation :: Function f => Twee f -> (Equation f -> Bool) -> Equation f -> (Int, Equation f)
weight :: Function f => Twee f -> Equation f -> Int
weight' :: Function f => Twee f -> Equation f -> Int
cancellations :: Function f => Twee f -> (Equation f -> Bool) -> Equation f -> [Equation f]
data Event f
NewRule :: (Rule f) -> Event f
ExtraRule :: (Rule f) -> Event f
NewCP :: (Passive f) -> Event f
Reduce :: (Simplification f) -> (Rule f) -> Event f
Consider :: (Critical (Equation f)) -> Event f
Joined :: (Critical (Equation f)) -> JoinReason -> Event f
Delay :: (Critical (Equation f)) -> Event f
Cancel :: (Critical (Equation f)) -> (Equation f) -> Event f
Discharge :: (Critical (Equation f)) -> (Model f) -> Event f
NormaliseCPs :: (Twee f) -> Event f
trace :: Function f => Twee f -> Event f -> a -> a
traceM :: Function f => Event f -> State (Twee f) ()
traceIf :: Bool -> Doc -> a -> a
instance GHC.Show.Show f => GHC.Show.Show (Twee.Twee f)
instance GHC.Show.Show f => GHC.Show.Show (Twee.Passive f)
instance GHC.Classes.Eq (Twee.Passive f)
instance GHC.Show.Show (Twee.CPs f)
instance GHC.Show.Show f => GHC.Show.Show (Twee.CP f)
instance GHC.Show.Show Twee.CPInfo
instance GHC.Classes.Ord Twee.CPInfo
instance GHC.Classes.Eq Twee.CPInfo
instance GHC.Show.Show f => GHC.Show.Show (Twee.Simplification f)
instance GHC.Show.Show (Twee.CancellationRule f)
instance GHC.Show.Show Twee.JoinReason
instance GHC.Classes.Ord Twee.JoinReason
instance GHC.Classes.Eq Twee.JoinReason
instance GHC.Show.Show Twee.JoinStage
instance GHC.Classes.Ord Twee.JoinStage
instance GHC.Classes.Eq Twee.JoinStage
instance (GHC.Show.Show a, GHC.Show.Show (Twee.Base.ConstantOf a)) => GHC.Show.Show (Twee.Modelled a)
instance (GHC.Show.Show a, GHC.Show.Show (Twee.Base.ConstantOf a)) => GHC.Show.Show (Twee.Critical a)
instance GHC.Show.Show f => GHC.Show.Show (Twee.CritInfo f)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Twee.Modelled a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Twee.Modelled a)
instance (Twee.Pretty.PrettyTerm (Twee.Base.ConstantOf a), Text.PrettyPrint.HughesPJClass.Pretty a) => Text.PrettyPrint.HughesPJClass.Pretty (Twee.Modelled a)
instance Twee.Base.Symbolic a => Twee.Base.Symbolic (Twee.Modelled a)
instance Twee.Indexes.Rated a => Twee.Indexes.Rated (Twee.Queue.Labelled a)
instance Twee.Indexes.Rated a => Twee.Indexes.Rated (Twee.Modelled a)
instance Twee.Indexes.Rated a => Twee.Indexes.Rated (Twee.Critical a)
instance Twee.Indexes.Rated (Twee.Rule.Rule f)
instance Text.PrettyPrint.HughesPJClass.Pretty Twee.JoinStage
instance Text.PrettyPrint.HughesPJClass.Pretty Twee.JoinReason
instance (Twee.Term.Numbered f, Twee.Pretty.PrettyTerm f) => Text.PrettyPrint.HughesPJClass.Pretty (Twee.Simplification f)
instance (Twee.Term.Numbered f, Twee.Pretty.PrettyTerm f) => Text.PrettyPrint.HughesPJClass.Pretty (Twee.CancellationRule f)
instance Twee.Base.Symbolic (Twee.CancellationRule f)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Twee.Critical a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Twee.Critical a)
instance (Twee.Pretty.PrettyTerm (Twee.Base.ConstantOf a), Text.PrettyPrint.HughesPJClass.Pretty a) => Text.PrettyPrint.HughesPJClass.Pretty (Twee.Critical a)
instance Twee.Base.Symbolic a => Twee.Base.Symbolic (Twee.Critical a)
instance Twee.Base.Symbolic (Twee.CritInfo f)
instance GHC.Classes.Eq (Twee.CP f)
instance GHC.Classes.Ord (Twee.CP f)
instance Twee.Queue.Labels (Twee.CP f)
instance (Twee.Term.Numbered f, Twee.Pretty.PrettyTerm f) => Text.PrettyPrint.HughesPJClass.Pretty (Twee.CP f)
instance GHC.Classes.Eq (Twee.CPs f)
instance GHC.Classes.Ord (Twee.CPs f)
instance Twee.Queue.Labels (Twee.CPs f)
instance (Twee.Term.Numbered f, Twee.Pretty.PrettyTerm f) => Text.PrettyPrint.HughesPJClass.Pretty (Twee.CPs f)
instance GHC.Classes.Ord (Twee.Passive f)
instance Twee.Queue.Labels (Twee.Passive f)
instance (Twee.Term.Numbered f, Twee.Pretty.PrettyTerm f) => Text.PrettyPrint.HughesPJClass.Pretty (Twee.Passive f)