-- 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.
--   
--   This package contains only the library part of twee.
@package twee-lib
@version 2.1.2


-- | Assignment of unique IDs to values. Inspired by the <tt>intern</tt>
--   package.
module Twee.Label

-- | A value of type <tt>a</tt> which has been given a unique ID.
data Label a

-- | Construct a <tt><a>Label</a> a</tt> from its unique ID, which must be
--   the <a>labelNum</a> of an already existing <a>Label</a>. Extremely
--   unsafe!
unsafeMkLabel :: Int32 -> Label a

-- | The unique ID of a label.
labelNum :: Label a -> Int32

-- | Assign a label to a value.
label :: forall a. (Typeable a, Ord a) => a -> Label a

-- | Recover the underlying value from a label.
find :: Label a -> a
instance GHC.Show.Show (Twee.Label.Label a)
instance GHC.Classes.Ord (Twee.Label.Label a)
instance GHC.Classes.Eq (Twee.Label.Label a)


-- | A module which can run housekeeping tasks every so often.
module Twee.Task

-- | A task which runs in the monad <tt>m</tt> and produces a value of type
--   <tt>a</tt>.
data Task m a

-- | Create a new task that should be run a certain proportion of the time.
--   The first argument is how often in seconds the task should run, at
--   most. The second argument is the maximum percentage of time that
--   should be spent on the task.
newTask :: MonadIO m => Double -> Double -> m a -> m (Task m a)

-- | Run a task if it's time to run it.
checkTask :: MonadIO m => Task m a -> m (Maybe a)


-- | Terms and substitutions.
--   
--   Terms in twee are represented as arrays rather than as an algebraic
--   data type. This module defines pattern synonyms (<a>App</a>,
--   <a>Var</a>, <a>Cons</a>, <a>Empty</a>) which means that pattern
--   matching on terms works just as normal. The pattern synonyms can not
--   be used to create new terms; for that you have to use a builder
--   interface (<a>Build</a>).
--   
--   This module also provides:
--   
--   <ul>
--   <li>pattern synonyms for iterating through a term one symbol at a time
--   (<a>ConsSym</a>);</li>
--   <li>substitutions (<a>Substitution</a>, <a>Subst</a>,
--   <a>subst</a>);</li>
--   <li>unification (<a>unify</a>) and matching (<a>match</a>);</li>
--   <li>miscellaneous useful functions on terms.</li>
--   </ul>
module Twee.Term

-- | <tt><a>Term</a> f</tt> is a term whose function symbols have type
--   <tt>f</tt>. It is either a <a>Var</a> or an <a>App</a>.
data Term f

-- | Matches a variable.

-- | Matches a function application.

-- | Check if a term is a function application.
isApp :: Term f -> Bool

-- | Check if a term is a variable
isVar :: Term f -> Bool

-- | Convert a term to a termlist.
singleton :: Term f -> TermList f

-- | Find the length of a term.
len :: Term f -> Int

-- | <tt><a>TermList</a> f</tt> is a list of terms whose function symbols
--   have type <tt>f</tt>. It is either a <a>Cons</a> or an <a>Empty</a>.
--   You can turn it into a <tt>[<a>Term</a> f]</tt> with <a>unpack</a>.
data TermList f

-- | Matches the empty termlist.

-- | Matches a non-empty termlist, unpacking it into head and tail.

-- | Matches a non-empty termlist, unpacking it into head and <i>everything
--   except the root symbol of the head</i>. Useful for iterating through
--   terms one symbol at a time.
--   
--   For example, if <tt>ts</tt> is the termlist <tt>[f(x,y), g(z)]</tt>,
--   then <tt>let ConsSym u us = ts</tt> results in the following bindings:
--   
--   <pre>
--   u  = f(x,y)
--   us = [x, y, g(z)]
--   </pre>

-- | Like <a>Cons</a>, but does not check that the termlist is non-empty.
--   Use only if you are sure the termlist is non-empty.

-- | Like <a>ConsSym</a>, but does not check that the termlist is
--   non-empty. Use only if you are sure the termlist is non-empty.

-- | The empty termlist.
empty :: forall f. TermList f

-- | Convert a termlist into an ordinary list of terms.
unpack :: TermList f -> [Term f]

-- | The length of (number of symbols in) a termlist.
lenList :: TermList f -> Int

-- | A function symbol. <tt>f</tt> is the underlying type of function
--   symbols defined by the user; <tt><a>Fun</a> f</tt> is an <tt>f</tt>
--   together with an automatically-generated unique number.
data Fun f

-- | Construct a <a>Fun</a> from a function symbol.
fun :: (Ord f, Typeable f) => f -> Fun f

-- | The unique number of a <a>Fun</a>.
fun_id :: Fun f -> Int

-- | The underlying function symbol of a <a>Fun</a>.
fun_value :: Fun f -> f

-- | A pattern which extracts the <a>fun_value</a> from a <a>Fun</a>.

-- | A variable.
newtype Var
V :: Int -> Var

-- | The variable's number. Don't use huge variable numbers: they will be
--   truncated to 32 bits when stored in a term.
[var_id] :: Var -> Int

-- | Instances of <a>Build</a> can be turned into terms using <a>build</a>
--   or <a>buildList</a>, and turned into term builders using
--   <a>builder</a>. Has instances for terms, termlists, builders, and
--   Haskell lists.
class Build a where {
    type family BuildFun a;
}

-- | Convert a value into a <a>Builder</a>.
builder :: Build a => a -> Builder (BuildFun a)

-- | A monoid for building terms. <a>mempty</a> represents the empty
--   termlist, while <a>mappend</a> appends two termlists.
data Builder f

-- | Build a term. The given builder must produce exactly one term.
build :: Build a => a -> Term (BuildFun a)

-- | Build a termlist.
buildList :: Build a => a -> TermList (BuildFun a)

-- | Build a constant (a function with no arguments).
con :: Fun f -> Builder f

-- | Build a function application.
app :: Build a => Fun (BuildFun a) -> a -> Builder (BuildFun a)

-- | Build a variable.
var :: Var -> Builder f

-- | Get the children (direct subterms) of a term.
children :: Term f -> TermList f

-- | Find all proper subterms of a term.
properSubterms :: Term f -> [Term f]

-- | Find all subterms of a termlist.
subtermsList :: TermList f -> [Term f]

-- | Find all subterms of a term.
subterms :: Term f -> [Term f]

-- | Check if a variable occurs in a term.
occurs :: Var -> Term f -> Bool

-- | Is a term a subterm of another one?
isSubtermOf :: Term f -> Term f -> Bool

-- | Is a term contained as a subterm in a given termlist?
isSubtermOfList :: Term f -> TermList f -> Bool

-- | Index into a termlist.
at :: Int -> TermList f -> Term f

-- | A class for values which act as substitutions.
--   
--   Instances include <a>Subst</a> as well as functions from variables to
--   terms.
class Substitution s where {
    type family SubstFun s;
}

-- | Apply the substitution to a variable.
evalSubst :: Substitution s => s -> Var -> Builder (SubstFun s)

-- | Apply the substitution to a termlist.
substList :: Substitution s => s -> TermList (SubstFun s) -> Builder (SubstFun s)

-- | Apply a substitution to a term.
subst :: Substitution s => s -> Term (SubstFun s) -> Builder (SubstFun s)

-- | A substitution which maps variables to terms of type <tt><a>Term</a>
--   f</tt>.
newtype Subst f
Subst :: IntMap (TermList f) -> Subst f
[unSubst] :: Subst f -> IntMap (TermList f)

-- | The empty substitution.
emptySubst :: () => Subst f

-- | Construct a substitution from a list. Returns <tt>Nothing</tt> if a
--   variable is bound to several different terms.
listToSubst :: [(Var, Term f)] -> Maybe (Subst f)

-- | Convert a substitution to a list of bindings.
substToList :: Subst f -> [(Var, Term f)]

-- | Look up a variable in a substitution.
lookup :: Var -> Subst f -> Maybe (Term f)

-- | Look up a variable in a substitution, returning a termlist.
lookupList :: Var -> Subst f -> Maybe (TermList f)

-- | Add a new binding to a substitution.
extend :: Var -> Term f -> Subst f -> Maybe (Subst f)

-- | Add a new binding to a substitution, giving a termlist.
extendList :: Var -> TermList f -> Subst f -> Maybe (Subst f)

-- | Add a new binding to a substitution. Overwrites any existing binding.
unsafeExtendList :: Var -> TermList f -> Subst f -> Subst f

-- | Remove a binding from a substitution.
retract :: Var -> Subst f -> Subst f

-- | Fold a function over a substitution.
foldSubst :: (Var -> TermList f -> b -> b) -> b -> Subst f -> b

-- | Check if all bindings of a substitution satisfy a given property.
allSubst :: (Var -> TermList f -> Bool) -> Subst f -> Bool

-- | Compute the set of variables bound by a substitution.
substDomain :: Subst f -> [Var]

-- | Return the highest-number variable in a substitution plus 1.
substSize :: Subst f -> Int

-- | Compose two substitutions.
substCompose :: Substitution s => Subst (SubstFun s) -> s -> Subst (SubstFun s)

-- | Check if two substitutions are compatible (they do not send the same
--   variable to different terms).
substCompatible :: Subst f -> Subst f -> Bool

-- | Take the union of two substitutions. The substitutions must be
--   compatible, which is not checked.
substUnion :: Subst f -> Subst f -> Subst f

-- | Check if a substitution is idempotent (applying it twice has the same
--   effect as applying it once).
idempotent :: Subst f -> Bool

-- | Check if a substitution has no effect on a given term.
idempotentOn :: Subst f -> TermList f -> Bool

-- | Return a substitution which renames the variables of a list of terms
--   to put them in a canonical order.
canonicalise :: [TermList f] -> Subst f

-- | <tt><a>match</a> pat t</tt> matches the term <tt>t</tt> against the
--   pattern <tt>pat</tt>.
match :: Term f -> Term f -> Maybe (Subst f)

-- | A variant of <a>match</a> which extends an existing substitution.
matchIn :: Subst f -> Term f -> Term f -> Maybe (Subst f)

-- | A variant of <a>match</a> which works on termlists.
matchList :: TermList f -> TermList f -> Maybe (Subst f)

-- | A variant of <a>match</a> which works on termlists and extends an
--   existing substitution.
matchListIn :: Subst f -> TermList f -> TermList f -> Maybe (Subst f)

-- | <tt>t `'isInstanceOf'\` pat</tt> checks if <tt>t</tt> is an instance
--   of <tt>pat</tt>.
isInstanceOf :: Term f -> Term f -> Bool

-- | Check if two terms are renamings of one another.
isVariantOf :: Term f -> Term f -> Bool

-- | Unify two terms.
unify :: Term f -> Term f -> Maybe (Subst f)

-- | Unify two termlists.
unifyList :: TermList f -> TermList f -> Maybe (Subst f)

-- | Unify two terms, returning a triangle substitution. This is slightly
--   faster than <a>unify</a>.
unifyTri :: Term f -> Term f -> Maybe (TriangleSubst f)

-- | Unify two termlists, returning a triangle substitution. This is
--   slightly faster than <a>unify</a>.
unifyListTri :: TermList f -> TermList f -> Maybe (TriangleSubst f)

-- | A triangle substitution is one in which variables can be defined in
--   terms of each other, though not in a circular way.
--   
--   The main use of triangle substitutions is in unification;
--   <a>unifyTri</a> returns one. A triangle substitution can be converted
--   to an ordinary substitution with <a>close</a>, or used directly using
--   its <a>Substitution</a> instance.
newtype TriangleSubst f
Triangle :: Subst f -> TriangleSubst f
[unTriangle] :: TriangleSubst f -> Subst f

-- | Iterate a triangle substitution to make it idempotent.
close :: TriangleSubst f -> Subst f

-- | Convert a position in a term, expressed as a single number, into a
--   path.
positionToPath :: Term f -> Int -> [Int]

-- | Convert a path in a term into a position.
pathToPosition :: Term f -> [Int] -> Int

-- | Replace the term at a given position in a term with a different term.
replacePosition :: (Build a, BuildFun a ~ f) => Int -> a -> TermList f -> Builder f

-- | Replace the term at a given position in a term with a different term,
--   while simultaneously applying a substitution. Useful for building
--   critical pairs.
replacePositionSub :: (Substitution sub, SubstFun sub ~ f) => sub -> Int -> TermList f -> TermList f -> Builder f

-- | Return the lowest- and highest-numbered variables in a term.
bound :: Term f -> (Var, Var)

-- | Return the lowest- and highest-numbered variables in a termlist.
boundList :: TermList f -> (Var, Var)

-- | Return the lowest- and highest-numbered variables in a list of
--   termlists.
boundLists :: [TermList f] -> (Var, Var)

-- | Map a function over the function symbols in a term.
mapFun :: (Fun f -> Fun g) -> Term f -> Builder g

-- | Map a function over the function symbols in a termlist.
mapFunList :: (Fun f -> Fun g) -> TermList f -> Builder g

-- | Compare the <a>fun_value</a>s of two <a>Fun</a>s.
(<<) :: Ord f => Fun f -> Fun f -> Bool
instance GHC.Show.Show (Twee.Term.TriangleSubst f)
instance GHC.Classes.Eq (Twee.Term.Subst f)
instance Twee.Term.Substitution (Twee.Term.TriangleSubst f)
instance Twee.Term.Substitution (Twee.Term.Subst f)
instance GHC.Show.Show (Twee.Term.Subst f)
instance (Twee.Term.Build a, v ~ Twee.Term.Core.Var) => Twee.Term.Substitution (v -> a)
instance Twee.Term.Build (Twee.Term.Core.Builder f)
instance Twee.Term.Build (Twee.Term.Core.Term f)
instance Twee.Term.Build (Twee.Term.Core.TermList f)
instance Twee.Term.Build a => Twee.Term.Build [a]
instance GHC.Show.Show (Twee.Term.Core.Term f)
instance GHC.Show.Show (Twee.Term.Core.TermList f)


-- | Pretty-printing of terms and assorted other values.
module Twee.Pretty

-- | Print a value to the console.
prettyPrint :: Pretty a => a -> IO ()

-- | The empty document. Used to avoid name clashes with <a>empty</a>.
pPrintEmpty :: Doc

-- | Print a tuple of values.
pPrintTuple :: [Doc] -> Doc

-- | Print a set of vlaues.
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

-- | The style of the function symbol. Defaults to <a>curried</a>.
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

-- | Renders a function application. Takes the following arguments in this
--   order: Pretty-printing level, current precedence, pretty-printed
--   function symbol and list of arguments to the function.
[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 Twee.Pretty.PrettyTerm f => Twee.Pretty.PrettyTerm (Twee.Term.Core.Fun f)
instance Twee.Pretty.PrettyTerm f => Text.PrettyPrint.HughesPJClass.Pretty (Twee.Term.Core.Term f)
instance Twee.Pretty.PrettyTerm f => Text.PrettyPrint.HughesPJClass.Pretty (Twee.Term.Core.TermList f)
instance Twee.Pretty.PrettyTerm f => Text.PrettyPrint.HughesPJClass.Pretty (Twee.Term.Subst f)
instance Text.PrettyPrint.HughesPJClass.Pretty Text.PrettyPrint.HughesPJ.Doc
instance Text.PrettyPrint.HughesPJClass.Pretty a => Text.PrettyPrint.HughesPJClass.Pretty (Data.Set.Internal.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.Internal.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 Text.PrettyPrint.HughesPJClass.Pretty f => Text.PrettyPrint.HughesPJClass.Pretty (Twee.Term.Core.Fun f)


-- | 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)]
fixpoint :: Eq a => (a -> a) -> a -> a
intMin :: Int -> Int -> Int
intMax :: Int -> Int -> Int
splitInterval :: Integral a => a -> (a, a) -> [(a, a)]
instance GHC.Classes.Ord a => GHC.Base.Monoid (Twee.Utils.Min a)
instance GHC.Classes.Ord a => GHC.Base.Monoid (Twee.Utils.Max a)


-- | A queue of passive critical pairs, using a memory-efficient
--   representation.
module Twee.PassiveQueue

-- | A datatype representing all the type parameters of the queue.
class (Eq (Id params), Integral (Id params), Ord (Score params), Unbox (PackedScore params), Unbox (PackedId params)) => Params params where {
    type family Score params;
    type family Id params;
    type family PackedScore params;
    type family PackedId params;
}

-- | Pack a <a>Score</a>.
packScore :: Params params => proxy params -> Score params -> PackedScore params

-- | Unpack a <a>PackedScore</a>.
unpackScore :: Params params => proxy params -> PackedScore params -> Score params

-- | Pack an <a>Id</a>.
packId :: Params params => proxy params -> Id params -> PackedId params

-- | Unpack a <a>PackedId</a>.
unpackId :: Params params => proxy params -> PackedId params -> Id params

-- | A critical pair queue.
data Queue params

-- | A queued critical pair.
data Passive params
Passive :: !(Score params) -> !(Id params) -> !(Id params) -> {-# UNPACK #-} !Int -> Passive params

-- | The score of this critical pair.
[passive_score] :: Passive params -> !(Score params)

-- | The rule which does the outermost rewrite in this critical pair.
[passive_rule1] :: Passive params -> !(Id params)

-- | The rule which does the innermost rewrite in this critical pair.
[passive_rule2] :: Passive params -> !(Id params)

-- | The position of the overlap. See <a>overlap_pos</a>.
[passive_pos] :: Passive params -> {-# UNPACK #-} !Int

-- | The empty queue.
empty :: Queue params

-- | Add a set of <a>Passive</a>s to the queue.
insert :: Params params => Id params -> [Passive params] -> Queue params -> Queue params

-- | Remove the minimum <a>Passive</a> from the queue.
removeMin :: Params params => Queue params -> Maybe (Passive params, Queue params)

-- | Map a function over all <a>Passive</a>s.
mapMaybe :: Params params => (Passive params -> Maybe (Passive params)) -> Queue params -> Queue params
instance Twee.PassiveQueue.Params params => GHC.Classes.Eq (Twee.PassiveQueue.PassiveSet params)
instance Twee.PassiveQueue.Params params => GHC.Classes.Ord (Twee.PassiveQueue.PassiveSet params)
instance Twee.PassiveQueue.Params params => GHC.Classes.Eq (Twee.PassiveQueue.Passive params)
instance Twee.PassiveQueue.Params params => GHC.Classes.Ord (Twee.PassiveQueue.Passive params)


-- | Solving constraints on variable ordering.
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 => t Formula f -> Formula f
disj :: Foldable t => t Formula f -> Formula f
(&&&) :: () => Formula f -> Formula f -> Formula 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 :: (Minimal f, Ord f) => Branch f -> Bool
formAnd :: (Minimal f, Ordered f) => Formula f -> [Branch f] -> [Branch f]
branches :: (Minimal f, Ordered f) => Formula f -> [Branch f]
addLess :: (Minimal f, Ordered f) => Atom f -> Atom f -> Branch f -> [Branch f]
addEquals :: (Minimal f, Ordered f) => Atom f -> Atom f -> Branch f -> [Branch f]
addTerm :: (Minimal f, Ordered f) => Atom f -> Branch f -> Branch f
newtype Model f
Model :: (Map (Atom f) (Int, Int)) -> Model f
modelToLiterals :: Model f -> [Formula f]
modelFromOrder :: (Minimal f, Ord f) => [Atom f] -> Model f
weakenModel :: Model f -> [Model f]
varInModel :: (Minimal f, Ord f) => Model f -> Var -> Bool
varGroups :: (Minimal f, Ord f) => Model f -> [(Fun f, [Var], Maybe (Fun f))]
class Minimal f
minimal :: Minimal f => Fun f
lessEqInModel :: (Minimal f, Ordered f) => Model f -> Atom f -> Atom f -> Maybe Strictness
solve :: (Minimal f, Ordered f, PrettyTerm f) => [Atom f] -> Branch f -> Either (Model f) (Subst f)
class Ord f => Ordered f

-- | Return <a>True</a> if the first term is less than or equal to the
--   second, in the term ordering.
lessEq :: Ordered f => Term f -> Term f -> Bool

-- | Check if the first term is less than or equal to the second in the
--   given model, and decide whether the inequality is strict or nonstrict.
lessIn :: Ordered f => Model f -> Term f -> Term f -> Maybe Strictness

-- | Describes whether an inequality is strict or nonstrict.
data Strictness

-- | The first term is strictly less than the second.
Strict :: Strictness

-- | The first term is less than or equal to the second.
Nonstrict :: Strictness

-- | Return <a>True</a> if the first argument is strictly less than the
--   second, in the term ordering.
lessThan :: Ordered f => Term f -> Term f -> Bool

-- | Return the direction in which the terms are oriented according to the
--   term ordering, or <a>Nothing</a> if they cannot be oriented. A result
--   of <tt><a>Just</a> <a>LT</a></tt> means that the first term is less
--   than <i>or equal to</i> the second.
orientTerms :: Ordered f => Term f -> Term f -> Maybe Ordering
instance GHC.Show.Show Twee.Constraints.Strictness
instance GHC.Classes.Eq Twee.Constraints.Strictness
instance GHC.Show.Show (Twee.Constraints.Model f)
instance GHC.Classes.Eq (Twee.Constraints.Model f)
instance GHC.Classes.Ord (Twee.Constraints.Branch f)
instance GHC.Classes.Eq (Twee.Constraints.Branch f)
instance GHC.Show.Show (Twee.Constraints.Formula f)
instance GHC.Classes.Ord (Twee.Constraints.Formula f)
instance GHC.Classes.Eq (Twee.Constraints.Formula f)
instance GHC.Classes.Ord (Twee.Constraints.Atom f)
instance GHC.Classes.Eq (Twee.Constraints.Atom f)
instance GHC.Show.Show (Twee.Constraints.Atom f)
instance Twee.Pretty.PrettyTerm f => Text.PrettyPrint.HughesPJClass.Pretty (Twee.Constraints.Model f)
instance Twee.Pretty.PrettyTerm f => Text.PrettyPrint.HughesPJClass.Pretty (Twee.Constraints.Branch f)
instance Twee.Pretty.PrettyTerm f => Text.PrettyPrint.HughesPJClass.Pretty (Twee.Constraints.Formula f)
instance Twee.Pretty.PrettyTerm f => Text.PrettyPrint.HughesPJClass.Pretty (Twee.Constraints.Atom f)


-- | Useful operations on terms and similar. Also re-exports some generally
--   useful modules such as <a>Term</a> and <a>Pretty</a>.
module Twee.Base

-- | Generalisation of term functionality to things that contain terms
--   (e.g., rewrite rules and equations).
class Symbolic a where {
    type family ConstantOf a;
}

-- | Compute a <a>DList</a> of all terms which appear in the argument (used
--   for e.g. computing free variables). See also <a>terms</a>.
termsDL :: Symbolic a => a -> DList (TermListOf a)

-- | Apply a substitution. When using the <a>Symbolic</a> type class, you
--   can use <a>subst</a> instead.
subst_ :: Symbolic a => (Var -> BuilderOf a) -> a -> a

-- | Apply a substitution.
subst :: (Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) => s -> a -> a

-- | Find all terms occuring in the argument.
terms :: Symbolic a => a -> [TermListOf a]

-- | A term compatible with a given <a>Symbolic</a>.
type TermOf a = Term (ConstantOf a)

-- | A termlist compatible with a given <a>Symbolic</a>.
type TermListOf a = TermList (ConstantOf a)

-- | A substitution compatible with a given <a>Symbolic</a>.
type SubstOf a = Subst (ConstantOf a)

-- | A triangle substitution compatible with a given <a>Symbolic</a>.
type TriangleSubstOf a = TriangleSubst (ConstantOf a)

-- | A builder compatible with a given <a>Symbolic</a>.
type BuilderOf a = Builder (ConstantOf a)

-- | The underlying type of function symbols of a given <a>Symbolic</a>.
type FunOf a = Fun (ConstantOf a)

-- | Find the variables occurring in the argument.
vars :: Symbolic a => a -> [Var]

-- | Test if the argument is ground.
isGround :: Symbolic a => a -> Bool

-- | Find the function symbols occurring in the argument.
funs :: Symbolic a => a -> [FunOf a]

-- | Count how many times a function symbol occurs in the argument.
occ :: Symbolic a => FunOf a -> a -> Int

-- | Count how many times a variable occurs in the argument.
occVar :: Symbolic a => Var -> a -> Int

-- | Rename the argument so that variables are introduced in a canonical
--   order (starting with V0, then V1 and so on).
canonicalise :: Symbolic a => a -> a

-- | Rename the second argument so that it does not mention any variable
--   which occurs in the first.
renameAvoiding :: (Symbolic a, Symbolic b) => a -> b -> b

-- | Represents a unique identifier (e.g., for a rule).
newtype Id
Id :: Int32 -> Id
[unId] :: Id -> Int32

-- | An instance <tt><a>Has</a> a b</tt> indicates that a value of type
--   <tt>a</tt> contains a value of type <tt>b</tt> which is somehow part
--   of the meaning of the <tt>a</tt>.
--   
--   A number of functions use <a>Has</a> constraints to work in a more
--   general setting. For example, the functions in <a>CP</a> operate on
--   rewrite rules, but actually accept any <tt>a</tt> satisfying
--   <tt><a>Has</a> a (<a>Rule</a> f)</tt>.
--   
--   Use taste when definining <a>Has</a> instances; don't do it
--   willy-nilly.
class Has a b

-- | Get at the thing.
the :: Has a b => a -> b
class Minimal f
minimal :: Minimal f => Fun f

-- | Build the minimal constant as a term.
minimalTerm :: Minimal f => Term f

-- | Check if a term is the minimal constant.
isMinimal :: Minimal f => Term f -> Bool

-- | Erase a given set of variables from the argument, replacing them with
--   the minimal constant.
erase :: (Symbolic a, ConstantOf a ~ f, Minimal f) => [Var] -> a -> a

-- | Construction of Skolem constants.
class Skolem f

-- | Turn a variable into a Skolem constant.
skolem :: Skolem f => Var -> Fun f

-- | For types which have a notion of arity.
class Arity f

-- | Measure the arity.
arity :: Arity f => f -> Int

-- | For types which have a notion of size.
class Sized a

-- | Compute the size.
size :: Sized a => a -> Int
class Ord f => Ordered f

-- | Return <a>True</a> if the first term is less than or equal to the
--   second, in the term ordering.
lessEq :: Ordered f => Term f -> Term f -> Bool

-- | Check if the first term is less than or equal to the second in the
--   given model, and decide whether the inequality is strict or nonstrict.
lessIn :: Ordered f => Model f -> Term f -> Term f -> Maybe Strictness

-- | Return <a>True</a> if the first argument is strictly less than the
--   second, in the term ordering.
lessThan :: Ordered f => Term f -> Term f -> Bool

-- | Return the direction in which the terms are oriented according to the
--   term ordering, or <a>Nothing</a> if they cannot be oriented. A result
--   of <tt><a>Just</a> <a>LT</a></tt> means that the first term is less
--   than <i>or equal to</i> the second.
orientTerms :: Ordered f => Term f -> Term f -> Maybe Ordering

-- | A hack for encoding Horn clauses. See <a>Score</a>. The default
--   implementation of <a>hasEqualsBonus</a> should work OK.
class EqualsBonus f
hasEqualsBonus :: EqualsBonus f => f -> Bool
isEquals, isTrue, isFalse :: EqualsBonus f => f -> Bool
isEquals, isTrue, isFalse :: EqualsBonus f => f -> Bool
isEquals, isTrue, isFalse :: EqualsBonus f => f -> Bool

-- | Describes whether an inequality is strict or nonstrict.
data Strictness

-- | The first term is strictly less than the second.
Strict :: Strictness

-- | The first term is less than or equal to the second.
Nonstrict :: Strictness

-- | The collection of constraints which the type of function symbols must
--   satisfy in order to be used by twee.
type Function f = (Ordered f, Arity f, Sized f, Minimal f, Skolem f, PrettyTerm f, EqualsBonus f)

-- | A function symbol extended with a minimal constant and Skolem
--   functions. Comes equipped with <a>Minimal</a> and <a>Skolem</a>
--   instances.
data Extended f

-- | The minimal constant.
Minimal :: Extended f

-- | A Skolem function.
Skolem :: Var -> Extended f

-- | An ordinary function symbol.
Function :: f -> Extended 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 GHC.Real.Integral Twee.Base.Id
instance GHC.Real.Real Twee.Base.Id
instance GHC.Num.Num Twee.Base.Id
instance GHC.Enum.Bounded Twee.Base.Id
instance GHC.Enum.Enum Twee.Base.Id
instance GHC.Show.Show Twee.Base.Id
instance GHC.Classes.Ord Twee.Base.Id
instance GHC.Classes.Eq Twee.Base.Id
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)
instance (Data.Typeable.Internal.Typeable f, GHC.Classes.Ord f) => Twee.Constraints.Minimal (Twee.Base.Extended f)
instance (Data.Typeable.Internal.Typeable f, GHC.Classes.Ord f) => Twee.Base.Skolem (Twee.Base.Extended f)
instance Twee.Base.EqualsBonus f => Twee.Base.EqualsBonus (Twee.Base.Extended f)
instance Twee.Base.EqualsBonus f => Twee.Base.EqualsBonus (Twee.Term.Core.Fun f)
instance Twee.Base.Sized f => Twee.Base.Sized (Twee.Term.Core.Fun f)
instance Twee.Base.Sized f => Twee.Base.Sized (Twee.Term.Core.TermList f)
instance Twee.Base.Sized f => Twee.Base.Sized (Twee.Term.Core.Term f)
instance Twee.Base.Arity f => Twee.Base.Arity (Twee.Term.Core.Fun f)
instance Twee.Base.Has a a
instance Twee.Base.Symbolic (Twee.Term.Core.Term f)
instance Twee.Base.Symbolic (Twee.Term.Core.TermList f)
instance Twee.Base.Symbolic (Twee.Term.Subst 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.Base.Symbolic a => Twee.Base.Symbolic (GHC.Base.Maybe a)
instance Text.PrettyPrint.HughesPJClass.Pretty Twee.Base.Id


-- | An implementation of Knuth-Bendix ordering.
module Twee.KBO

-- | Check if one term is less than another in KBO.
lessEq :: Function f => Term f -> Term f -> Bool

-- | Check if one term is less than another in a given model.
lessIn :: Function f => Model f -> Term f -> Term f -> Maybe Strictness


-- | A term index to accelerate matching. An index is a multimap from terms
--   to arbitrary values.
--   
--   The type of query supported is: given a search term, find all keys
--   such that the search term is an instance of the key, and return the
--   corresponding values.
module Twee.Index

-- | A term index: a multimap from <tt><a>Term</a> f</tt> to <tt>a</tt>.
data Index f a

-- | An empty index.
empty :: Index f a

-- | Is the index empty?
null :: Index f a -> Bool

-- | An index with one entry.
singleton :: Term f -> a -> Index f a

-- | Insert an entry into the index.
insert :: Term f -> a -> Index f a -> Index f a

-- | Delete an entry from the index.
delete :: Eq a => Term f -> a -> Index f a -> Index f a

-- | Look up a term in the index. Finds all key-value such that the search
--   term is an instance of the key, and returns an instance of the the
--   value which makes the search term exactly equal to the key.
lookup :: (Has a b, Symbolic b, Has b (TermOf b)) => TermOf b -> Index (ConstantOf b) a -> [b]

-- | Look up a term in the index. Like <a>lookup</a>, but returns the exact
--   value that was inserted into the index, not an instance. Also returns
--   a substitution which when applied to the value gives you the matching
--   instance.
matches :: Has a (Term f) => Term f -> Index f a -> [(Subst f, a)]

-- | Look up a term in the index, possibly returning spurious extra
--   results.
approxMatches :: Term f -> Index f a -> [a]

-- | Return all elements of the index.
elems :: Index f a -> [a]
instance GHC.Show.Show a => GHC.Show.Show (Twee.Index.Index f a)
instance Data.DynamicArray.Default (Twee.Index.Index f a)


-- | Equations.
module Twee.Equation
data Equation f
(:=:) :: {-# UNPACK #-} !(Term f) -> {-# UNPACK #-} !(Term f) -> Equation f
[eqn_lhs] :: Equation f -> {-# UNPACK #-} !(Term f)
[eqn_rhs] :: Equation f -> {-# UNPACK #-} !(Term f)
type EquationOf a = Equation (ConstantOf a)

-- | Order an equation roughly left-to-right. However, there is no
--   guarantee that the result is oriented.
order :: Function f => Equation f -> Equation f

-- | Apply a function to both sides of an equation.
bothSides :: (Term f -> Term f') -> Equation f -> Equation f'

-- | Is an equation of the form t = t?
trivial :: Eq f => Equation f -> Bool
simplerThan :: Function f => Equation f -> Equation f -> Bool
instance GHC.Show.Show (Twee.Equation.Equation f)
instance GHC.Classes.Ord (Twee.Equation.Equation f)
instance GHC.Classes.Eq (Twee.Equation.Equation f)
instance Twee.Base.Symbolic (Twee.Equation.Equation f)
instance Twee.Pretty.PrettyTerm f => Text.PrettyPrint.HughesPJClass.Pretty (Twee.Equation.Equation f)
instance Twee.Base.Sized f => Twee.Base.Sized (Twee.Equation.Equation f)


-- | Equational proofs which are checked for correctedness.
module Twee.Proof

-- | A checked proof. If you have a value of type <tt>Proof f</tt>, it
--   should jolly well represent a valid proof!
--   
--   The only way to construct a <tt>Proof f</tt> is by using
--   <a>certify</a>.
data Proof f

-- | A derivation is an unchecked proof. It might be wrong! The way to
--   check it is to call <a>certify</a> to turn it into a <a>Proof</a>.
data Derivation f

-- | Apply an existing rule (with proof!) to the root of a term
UseLemma :: {-# UNPACK #-} !(Lemma f) -> !(Subst f) -> Derivation f

-- | Apply an axiom to the root of a term
UseAxiom :: {-# UNPACK #-} !(Axiom f) -> !(Subst f) -> Derivation f

-- | Reflexivity. <tt><a>Refl</a> t</tt> proves <tt>t = t</tt>.
Refl :: !(Term f) -> Derivation f

-- | Symmetry
Symm :: !(Derivation f) -> Derivation f

-- | Transivitity
Trans :: !(Derivation f) -> !(Derivation f) -> Derivation f

-- | Congruence. Parallel, i.e., takes a function symbol and one derivation
--   for each argument of that function.
Cong :: {-# UNPACK #-} !(Fun f) -> ![Derivation f] -> Derivation f

-- | A lemma, which includes a proof.
data Lemma f
Lemma :: {-# UNPACK #-} !Id -> !(Proof f) -> Lemma f

-- | The id number of the lemma. Has no semantic meaning; for convenience
--   only.
[lemma_id] :: Lemma f -> {-# UNPACK #-} !Id

-- | A proof of the lemma.
[lemma_proof] :: Lemma f -> !(Proof f)
data Axiom f
Axiom :: {-# UNPACK #-} !Int -> !String -> !(Equation f) -> Axiom f

-- | The number of the axiom. Has no semantic meaning; for convenience
--   only.
[axiom_number] :: Axiom f -> {-# UNPACK #-} !Int

-- | A description of the axiom. Has no semantic meaning; for convenience
--   only.
[axiom_name] :: Axiom f -> !String

-- | The equation which the axiom asserts.
[axiom_eqn] :: Axiom f -> !(Equation f)

-- | Checks a <a>Derivation</a> and, if it is correct, returns a certified
--   <a>Proof</a>.
--   
--   If the <a>Derivation</a> is incorrect, throws an exception.
certify :: PrettyTerm f => Derivation f -> Proof f
equation :: Proof f -> (Equation f)
derivation :: Proof f -> (Derivation f)
lemma :: Lemma f -> Subst f -> Derivation f
axiom :: Axiom f -> Derivation f
symm :: Derivation f -> Derivation f
trans :: Derivation f -> Derivation f -> Derivation f
cong :: Fun f -> [Derivation f] -> Derivation f

-- | Applies a derivation at a particular path in a term.
congPath :: [Int] -> Term f -> Derivation f -> Derivation f

-- | Simplify a derivation.
--   
--   After simplification, a derivation has the following properties:
--   
--   <ul>
--   <li><a>Symm</a> is pushed down next to <a>Lemma</a> and
--   <a>Axiom</a></li>
--   <li><a>Refl</a> only occurs inside <a>Cong</a> or at the top
--   level</li>
--   <li><a>Trans</a> is right-associated and is pushed inside <a>Cong</a>
--   if possible</li>
--   </ul>
simplify :: Minimal f => (Lemma f -> Maybe (Derivation f)) -> Derivation f -> Derivation f

-- | Find all lemmas which are used in a derivation.
usedLemmas :: Derivation f -> [Lemma f]

-- | Find all axioms which are used in a derivation.
usedAxioms :: Derivation f -> [Axiom f]

-- | Find all lemmas which are used in a derivation, together with the
--   substitutions used.
usedLemmasAndSubsts :: Derivation f -> [(Lemma f, Subst f)]

-- | Find all axioms which are used in a derivation, together with the
--   substitutions used.
usedAxiomsAndSubsts :: Derivation f -> [(Axiom f, Subst f)]

-- | Options for proof presentation.
data Config
Config :: !Bool -> !Bool -> !Bool -> Config

-- | Never inline lemmas.
[cfg_all_lemmas] :: Config -> !Bool

-- | Inline all lemmas.
[cfg_no_lemmas] :: Config -> !Bool

-- | Print out explicit substitutions.
[cfg_show_instances] :: Config -> !Bool

-- | The default configuration.
defaultConfig :: Config

-- | A proof, with all axioms and lemmas explicitly listed.
data Presentation f
Presentation :: [Axiom f] -> [Lemma f] -> [ProvedGoal f] -> Presentation f

-- | The used axioms.
[pres_axioms] :: Presentation f -> [Axiom f]

-- | The used lemmas.
[pres_lemmas] :: Presentation f -> [Lemma f]

-- | The goals proved.
[pres_goals] :: Presentation f -> [ProvedGoal f]
data ProvedGoal f
ProvedGoal :: Int -> String -> Proof f -> Equation f -> Subst f -> ProvedGoal f
[pg_number] :: ProvedGoal f -> Int
[pg_name] :: ProvedGoal f -> String
[pg_proof] :: ProvedGoal f -> Proof f
[pg_goal_hint] :: ProvedGoal f -> Equation f
[pg_witness_hint] :: ProvedGoal f -> Subst f

-- | Construct a <tt>ProvedGoal</tt>.
provedGoal :: Int -> String -> Proof f -> ProvedGoal f

-- | Check that pg_goal/pg_witness match up with pg_proof.
checkProvedGoal :: Function f => ProvedGoal f -> ProvedGoal f

-- | Print a presented proof.
pPrintPresentation :: forall f. Function f => Config -> Presentation f -> Doc

-- | Simplify and present a proof.
present :: Function f => Config -> [ProvedGoal f] -> Presentation f

-- | Format an equation nicely.
--   
--   Used both here and in the main file.
describeEquation :: PrettyTerm f => String -> String -> Maybe String -> Equation f -> Doc
instance GHC.Show.Show (Twee.Proof.Presentation f)
instance GHC.Show.Show (Twee.Proof.ProvedGoal f)
instance GHC.Show.Show (Twee.Proof.Proof f)
instance GHC.Classes.Eq (Twee.Proof.Proof f)
instance GHC.Show.Show (Twee.Proof.Lemma f)
instance GHC.Show.Show (Twee.Proof.Derivation f)
instance GHC.Classes.Eq (Twee.Proof.Derivation f)
instance GHC.Show.Show (Twee.Proof.Axiom f)
instance GHC.Classes.Ord (Twee.Proof.Axiom f)
instance GHC.Classes.Eq (Twee.Proof.Axiom f)
instance Twee.Base.Function f => Text.PrettyPrint.HughesPJClass.Pretty (Twee.Proof.Presentation f)
instance GHC.Classes.Eq (Twee.Proof.Lemma f)
instance GHC.Classes.Ord (Twee.Proof.Lemma f)
instance Twee.Base.Symbolic (Twee.Proof.Derivation f)
instance Twee.Base.Function f => Text.PrettyPrint.HughesPJClass.Pretty (Twee.Proof.Proof f)
instance Twee.Pretty.PrettyTerm f => Text.PrettyPrint.HughesPJClass.Pretty (Twee.Proof.Derivation f)
instance Twee.Pretty.PrettyTerm f => Text.PrettyPrint.HughesPJClass.Pretty (Twee.Proof.Lemma f)
instance Twee.Pretty.PrettyTerm f => Text.PrettyPrint.HughesPJClass.Pretty (Twee.Proof.Axiom f)


-- | Term rewriting.
module Twee.Rule

-- | A rewrite rule.
data Rule f
Rule :: !(Orientation f) -> {-# UNPACK #-} !(Term f) -> {-# UNPACK #-} !(Term f) -> Rule f

-- | Information about whether and how the rule is oriented.
[orientation] :: Rule f -> !(Orientation f)

-- | The left-hand side of the rule.
[lhs] :: Rule f -> {-# UNPACK #-} !(Term f)

-- | The right-hand side of the rule.
[rhs] :: Rule f -> {-# UNPACK #-} !(Term f)
type RuleOf a = Rule (ConstantOf a)

-- | A rule's orientation.
--   
--   <a>Oriented</a> and <a>WeaklyOriented</a> rules are used only
--   left-to-right. <a>Permutative</a> and <a>Unoriented</a> rules are used
--   bidirectionally.
data Orientation f

-- | An oriented rule.
Oriented :: Orientation f

-- | A weakly oriented rule. The first argument is the minimal constant,
--   the second argument is a list of terms which are weakly oriented in
--   the rule.
--   
--   A rule with orientation <tt><a>WeaklyOriented</a> k ts</tt> can be
--   used unless all terms in <tt>ts</tt> are equal to <tt>k</tt>.
WeaklyOriented :: {-# UNPACK #-} !(Fun f) -> [Term f] -> Orientation f

-- | A permutative rule.
--   
--   A rule with orientation <tt><a>Permutative</a> ts</tt> can be used if
--   <tt>map fst ts</tt> is lexicographically greater than <tt>map snd
--   ts</tt>.
Permutative :: [(Term f, Term f)] -> Orientation f

-- | An unoriented rule.
Unoriented :: Orientation f

-- | Is a rule oriented or weakly oriented?
oriented :: Orientation f -> Bool

-- | Is a rule weakly oriented?
weaklyOriented :: Orientation f -> Bool

-- | Turn a rule into an equation.
unorient :: Rule f -> Equation f

-- | Turn an equation t :=: u into a rule t -&gt; u by computing the
--   orientation info (e.g. oriented, permutative or unoriented).
--   
--   Crashes if t -&gt; u is not a valid rule, for example if there is a
--   variable in <tt>u</tt> which is not in <tt>t</tt>. To prevent this
--   happening, combine with <a>split</a>.
orient :: Function f => Equation f -> Rule f

-- | Flip an unoriented rule so that it goes right-to-left.
backwards :: Rule f -> Rule f

-- | Compute the normal form of a term wrt only oriented rules.
simplify :: (Function f, Has a (Rule f)) => Index f a -> Term f -> Term f
simplify1 :: (Function f, Has a (Rule f)) => Index f a -> Term f -> Term f

-- | Check if a term can be simplified.
canSimplify :: (Function f, Has a (Rule f)) => Index f a -> Term f -> Bool
canSimplifyList :: (Function f, Has a (Rule f)) => Index f a -> TermList f -> Bool

-- | Find a simplification step that applies to a term.
simpleRewrite :: (Function f, Has a (Rule f)) => Index f a -> Term f -> Maybe (Rule f, Subst f)

-- | A strategy gives a set of possible reductions for a term.
type Strategy f = Term f -> [Reduction f]

-- | A multi-step rewrite proof <tt>t -&gt;* u</tt>
data Reduction f

-- | Apply a single rewrite rule to the root of a term
Step :: {-# UNPACK #-} !(Lemma f) -> !(Rule f) -> !(Subst f) -> Reduction f

-- | Reflexivity
Refl :: {-# UNPACK #-} !(Term f) -> Reduction f

-- | Transivitity
Trans :: !(Reduction f) -> !(Reduction f) -> Reduction f

-- | Congruence
Cong :: {-# UNPACK #-} !(Fun f) -> ![Reduction f] -> Reduction f

-- | A smart constructor for Trans which simplifies Refl.
trans :: Reduction f -> Reduction f -> Reduction f

-- | A smart constructor for Cong which simplifies Refl.
cong :: Fun f -> [Reduction f] -> Reduction f

-- | The list of all rewrite rules used in a rewrite proof.
steps :: Reduction f -> [Reduction f]

-- | Turn a reduction into a proof.
reductionProof :: Reduction f -> Derivation f

-- | Construct a basic rewrite step.
step :: (Has a (Rule f), Has a (Lemma f)) => a -> Subst f -> Reduction f

-- | A rewrite proof with the final term attached. Has an <tt>Ord</tt>
--   instance which compares the final term.
data Resulting f
Resulting :: {-# UNPACK #-} !(Term f) -> !(Reduction f) -> Resulting f
[result] :: Resulting f -> {-# UNPACK #-} !(Term f)
[reduction] :: Resulting f -> !(Reduction f)

-- | Construct a <a>Resulting</a> from a <a>Reduction</a>.
reduce :: Reduction f -> Resulting f

-- | Normalise a term wrt a particular strategy.
normaliseWith :: Function f => (Term f -> Bool) -> Strategy f -> Term f -> Resulting f

-- | Compute all normal forms of a set of terms wrt a particular strategy.
normalForms :: Function f => Strategy f -> [Resulting f] -> Set (Resulting f)

-- | Compute all successors of a set of terms (a successor of a term
--   <tt>t</tt> is a term <tt>u</tt> such that <tt>t -&gt;* u</tt>).
successors :: Function f => Strategy f -> [Resulting f] -> Set (Resulting f)
successorsAndNormalForms :: Function f => Strategy f -> [Resulting f] -> (Set (Resulting f), Set (Resulting f))

-- | Apply a strategy anywhere in a term.
anywhere :: Strategy f -> Strategy f

-- | Apply a strategy to some child of the root function.
nested :: Strategy f -> Strategy f

-- | Apply a strategy in parallel in as many places as possible. Takes only
--   the first rewrite of each strategy.
parallel :: PrettyTerm f => Strategy f -> Strategy f

-- | A strategy which rewrites using an index.
rewrite :: (Function f, Has a (Rule f), Has a (Lemma f)) => (Rule f -> Subst f -> Bool) -> Index f a -> Strategy f

-- | A strategy which applies one rule only.
tryRule :: (Function f, Has a (Rule f), Has a (Lemma f)) => (Rule f -> Subst f -> Bool) -> a -> Strategy f

-- | Check if a rule can be applied, given an ordering &lt;= on terms.
reducesWith :: Function f => (Term f -> Term f -> Bool) -> Rule f -> Subst f -> Bool

-- | Check if a rule can be applied normally.
reduces :: Function f => Rule f -> Subst f -> Bool

-- | Check if a rule can be applied and is oriented.
reducesOriented :: Function f => Rule f -> Subst f -> Bool

-- | Check if a rule can be applied in a particular model.
reducesInModel :: Function f => Model f -> Rule f -> Subst f -> Bool

-- | Check if a rule can be applied to the Skolemised version of a term.
reducesSkolem :: Function f => Rule f -> Subst f -> Bool
instance GHC.Show.Show (Twee.Rule.Resulting f)
instance GHC.Show.Show (Twee.Rule.Reduction 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.Resulting f)
instance GHC.Classes.Ord (Twee.Rule.Resulting f)
instance Twee.Base.Symbolic (Twee.Rule.Resulting f)
instance Twee.Base.Function f => Text.PrettyPrint.HughesPJClass.Pretty (Twee.Rule.Resulting f)
instance Twee.Base.Symbolic (Twee.Rule.Reduction f)
instance Twee.Base.Function f => Text.PrettyPrint.HughesPJClass.Pretty (Twee.Rule.Reduction f)
instance Twee.Base.Symbolic (Twee.Rule.Rule f)
instance f ~ g => Twee.Base.Has (Twee.Rule.Rule f) (Twee.Term.Core.Term g)
instance Twee.Pretty.PrettyTerm f => Text.PrettyPrint.HughesPJClass.Pretty (Twee.Rule.Rule f)
instance GHC.Classes.Eq (Twee.Rule.Orientation f)
instance GHC.Classes.Ord (Twee.Rule.Orientation f)
instance Twee.Base.Symbolic (Twee.Rule.Orientation f)

module Twee.Rule.Index
data RuleIndex f a
RuleIndex :: !(Index f a) -> !(Index f a) -> !(Index f a) -> RuleIndex f a
[index_oriented] :: RuleIndex f a -> !(Index f a)
[index_weak] :: RuleIndex f a -> !(Index f a)
[index_all] :: RuleIndex f a -> !(Index f a)
empty :: RuleIndex f a
insert :: forall f a. Has a (Rule f) => Term f -> a -> RuleIndex f a -> RuleIndex f a
delete :: forall f a. (Eq a, Has a (Rule f)) => Term f -> a -> RuleIndex f a -> RuleIndex f a

-- | Look up a term in the index, possibly returning spurious extra
--   results.
approxMatches :: Term f -> Index f a -> [a]

-- | Look up a term in the index. Like <a>lookup</a>, but returns the exact
--   value that was inserted into the index, not an instance. Also returns
--   a substitution which when applied to the value gives you the matching
--   instance.
matches :: Has a (Term f) => Term f -> Index f a -> [(Subst f, a)]

-- | Look up a term in the index. Finds all key-value such that the search
--   term is an instance of the key, and returns an instance of the the
--   value which makes the search term exactly equal to the key.
lookup :: (Has a b, Symbolic b, Has b (TermOf b)) => TermOf b -> Index (ConstantOf b) a -> [b]
instance GHC.Show.Show a => GHC.Show.Show (Twee.Rule.Index.RuleIndex f a)


-- | Critical pair generation.
module Twee.CP

-- | The set of positions at which a term can have critical overlaps.
data Positions f
NilP :: Positions f
ConsP :: {-# UNPACK #-} !Int -> !(Positions f) -> Positions f
type PositionsOf a = Positions (ConstantOf a)

-- | Calculate the set of positions for a term.
positions :: Term f -> Positions f
positionsChurch :: Positions f -> ChurchList Int

-- | A critical overlap of one rule with another.
data Overlap f
Overlap :: {-# UNPACK #-} !Depth -> {-# UNPACK #-} !(Term f) -> {-# UNPACK #-} !(Term f) -> {-# UNPACK #-} !Int -> {-# UNPACK #-} !(Equation f) -> Overlap f

-- | The depth (1 for CPs of axioms, 2 for CPs whose rules have depth 1,
--   etc.)
[overlap_depth] :: Overlap f -> {-# UNPACK #-} !Depth

-- | The critical term.
[overlap_top] :: Overlap f -> {-# UNPACK #-} !(Term f)

-- | The part of the critical term which the inner rule rewrites.
[overlap_inner] :: Overlap f -> {-# UNPACK #-} !(Term f)

-- | The position in the critical term which is rewritten.
[overlap_pos] :: Overlap f -> {-# UNPACK #-} !Int

-- | The critical pair itself.
[overlap_eqn] :: Overlap f -> {-# UNPACK #-} !(Equation f)
type OverlapOf a = Overlap (ConstantOf a)

-- | Represents the depth of a critical pair.
newtype Depth
Depth :: Int -> Depth

-- | Compute all overlaps of a rule with a set of rules.
overlaps :: (Function f, Has a (Rule f), Has a (Positions f), Has a Depth) => Depth -> Index f a -> [a] -> a -> [(a, a, Overlap f)]
overlapsChurch :: forall f a. (Function f, Has a (Rule f), Has a (Positions f), Has a Depth) => Depth -> Index f a -> [a] -> a -> ChurchList (a, a, Overlap f)
asymmetricOverlaps :: (Function f, Has a (Rule f), Has a Depth) => Index f a -> Depth -> Positions f -> Rule f -> Rule f -> ChurchList (Overlap f)

-- | Create an overlap at a particular position in a term. Doesn't simplify
--   the overlap.
overlapAt :: Int -> Depth -> Rule f -> Rule f -> Maybe (Overlap f)

-- | Simplify an overlap and remove it if it's trivial.
simplifyOverlap :: (Function f, Has a (Rule f)) => Index f a -> Overlap f -> Maybe (Overlap f)
buildReplacePositionSub :: TriangleSubst f -> Int -> TermList f -> TermList f -> Term f
termSubst :: TriangleSubst f -> Term f -> Term f

-- | The configuration for the critical pair weighting heuristic.
data Config
Config :: !Int -> !Int -> !Int -> !Int -> !Int -> !Int -> !Int -> Config
[cfg_lhsweight] :: Config -> !Int
[cfg_rhsweight] :: Config -> !Int
[cfg_funweight] :: Config -> !Int
[cfg_varweight] :: Config -> !Int
[cfg_depthweight] :: Config -> !Int
[cfg_dupcost] :: Config -> !Int
[cfg_dupfactor] :: Config -> !Int

-- | The default heuristic configuration.
defaultConfig :: Config

-- | Compute a score for a critical pair.
score :: Function f => Config -> Overlap f -> Int

-- | A critical pair together with information about how it was derived
data CriticalPair f
CriticalPair :: {-# UNPACK #-} !(Equation f) -> {-# UNPACK #-} !Depth -> !(Maybe (Term f)) -> !(Derivation f) -> CriticalPair f

-- | The critical pair itself.
[cp_eqn] :: CriticalPair f -> {-# UNPACK #-} !(Equation f)

-- | The depth of the critical pair.
[cp_depth] :: CriticalPair f -> {-# UNPACK #-} !Depth

-- | The critical term, if there is one. (Axioms do not have a critical
--   term.)
[cp_top] :: CriticalPair f -> !(Maybe (Term f))

-- | A derivation of the critical pair from the axioms.
[cp_proof] :: CriticalPair f -> !(Derivation f)

-- | Split a critical pair so that it can be turned into rules.
--   
--   The resulting critical pairs have the property that no variable
--   appears on the right that is not on the left.
split :: Function f => CriticalPair f -> [CriticalPair f]

-- | Make a critical pair from two rules and an overlap.
makeCriticalPair :: (Has a (Rule f), Has a (Lemma f), Has a Id, Function f) => a -> a -> Overlap f -> Maybe (CriticalPair f)

-- | Return a proof for a critical pair.
overlapProof :: forall a f. (Has a (Rule f), Has a (Lemma f), Has a Id) => a -> a -> Overlap f -> Derivation f
instance GHC.Show.Show (Twee.CP.Overlap f)
instance GHC.Show.Show Twee.CP.Depth
instance GHC.Real.Integral Twee.CP.Depth
instance GHC.Enum.Enum Twee.CP.Depth
instance GHC.Real.Real Twee.CP.Depth
instance GHC.Num.Num Twee.CP.Depth
instance GHC.Classes.Ord Twee.CP.Depth
instance GHC.Classes.Eq Twee.CP.Depth
instance Twee.Base.Symbolic (Twee.CP.CriticalPair f)
instance Twee.Pretty.PrettyTerm f => Text.PrettyPrint.HughesPJClass.Pretty (Twee.CP.CriticalPair f)
instance GHC.Show.Show (Twee.CP.Positions f)


-- | Tactics for joining critical pairs.
module Twee.Join
data Config
Config :: !Bool -> !Bool -> !Bool -> Config
[cfg_ground_join] :: Config -> !Bool
[cfg_use_connectedness] :: Config -> !Bool
[cfg_set_join] :: Config -> !Bool
defaultConfig :: Config
joinCriticalPair :: (Function f, Has a (Rule f), Has a (Lemma f)) => Config -> Index f (Equation f) -> RuleIndex f a -> Maybe (Model f) -> CriticalPair f -> Either (CriticalPair f, Model f) (Maybe (CriticalPair f), [CriticalPair f])
step1 :: (Function f, Has a (Rule f), Has a (Lemma f)) => Config -> Index f (Equation f) -> RuleIndex f a -> CriticalPair f -> Maybe (CriticalPair f)
step2 :: (Function f, Has a (Rule f), Has a (Lemma f)) => Config -> Index f (Equation f) -> RuleIndex f a -> CriticalPair f -> Maybe (CriticalPair f)
step3 :: (Function f, Has a (Rule f), Has a (Lemma f)) => Config -> Index f (Equation f) -> RuleIndex f a -> CriticalPair f -> Maybe (CriticalPair f)
allSteps :: (Function f, Has a (Rule f), Has a (Lemma f)) => Config -> Index f (Equation f) -> RuleIndex f a -> CriticalPair f -> Maybe (CriticalPair f)
joinWith :: (Has a (Rule f), Has a (Lemma f)) => Index f (Equation f) -> RuleIndex f a -> (Term f -> Term f -> Resulting f) -> CriticalPair f -> Maybe (CriticalPair f)
subsumed :: (Has a (Rule f), Has a (Lemma f)) => Index f (Equation f) -> RuleIndex f a -> Equation f -> Bool
groundJoin :: (Function f, Has a (Rule f), Has a (Lemma f)) => Config -> Index f (Equation f) -> RuleIndex f a -> [Branch f] -> CriticalPair f -> Either (Model f) [CriticalPair f]
groundJoinFrom :: (Function f, Has a (Rule f), Has a (Lemma f)) => Config -> Index f (Equation f) -> RuleIndex f a -> Model f -> [Branch f] -> CriticalPair f -> Either (Model f) [CriticalPair f]
groundJoinFromMaybe :: (Function f, Has a (Rule f), Has a (Lemma f)) => Config -> Index f (Equation f) -> RuleIndex f a -> Maybe (Model f) -> [Branch f] -> CriticalPair f -> Either (Model f) [CriticalPair f]
valid :: Function f => Model f -> Reduction f -> Bool
optimise :: a -> (a -> [a]) -> (a -> Bool) -> a


-- | The main prover loop.
module Twee

-- | The prover configuration.
data Config
Config :: Int -> Int64 -> Int -> Bool -> Int -> Config -> Config -> Config -> Config
[cfg_max_term_size] :: Config -> Int
[cfg_max_critical_pairs] :: Config -> Int64
[cfg_max_cp_depth] :: Config -> Int
[cfg_simplify] :: Config -> Bool
[cfg_renormalise_percent] :: Config -> Int
[cfg_critical_pairs] :: Config -> Config
[cfg_join] :: Config -> Config
[cfg_proof_presentation] :: Config -> Config

-- | The prover state.
data State f
State :: !(RuleIndex f (ActiveRule f)) -> !(IntMap (Active f)) -> !(IntMap (ActiveRule f)) -> !(Index f (Equation f)) -> ![Goal f] -> !(Queue Params) -> {-# UNPACK #-} !Id -> {-# UNPACK #-} !RuleId -> {-# UNPACK #-} !Int64 -> ![Message f] -> State f
[st_rules] :: State f -> !(RuleIndex f (ActiveRule f))
[st_active_ids] :: State f -> !(IntMap (Active f))
[st_rule_ids] :: State f -> !(IntMap (ActiveRule f))
[st_joinable] :: State f -> !(Index f (Equation f))
[st_goals] :: State f -> ![Goal f]
[st_queue] :: State f -> !(Queue Params)
[st_next_active] :: State f -> {-# UNPACK #-} !Id
[st_next_rule] :: State f -> {-# UNPACK #-} !RuleId
[st_considered] :: State f -> {-# UNPACK #-} !Int64
[st_messages_rev] :: State f -> ![Message f]

-- | The default prover configuration.
defaultConfig :: Config

-- | Does this configuration run the prover in a complete mode?
configIsComplete :: Config -> Bool

-- | The initial state.
initialState :: State f

-- | A message which is produced by the prover when something interesting
--   happens.
data Message f

-- | A new rule.
NewActive :: !(Active f) -> Message f

-- | A new joinable equation.
NewEquation :: !(Equation f) -> Message f

-- | A rule was deleted.
DeleteActive :: !(Active f) -> Message f

-- | The CP queue was simplified.
SimplifyQueue :: Message f

-- | The rules were reduced wrt each other.
Interreduce :: Message f

-- | Emit a message.
message :: PrettyTerm f => Message f -> State f -> State f

-- | Forget about all emitted messages.
clearMessages :: State f -> State f

-- | Get all emitted messages.
messages :: State f -> [Message f]
data Params

-- | Compute all critical pairs from a rule.
makePassives :: Function f => Config -> State f -> ActiveRule f -> [Passive Params]

-- | Turn a Passive back into an overlap. Doesn't try to simplify it.
findPassive :: forall f. Function f => Config -> State f -> Passive Params -> Maybe (ActiveRule f, ActiveRule f, Overlap f)

-- | Renormalise a queued Passive.
simplifyPassive :: Function f => Config -> State f -> Passive Params -> Maybe (Passive Params)

-- | Renormalise the entire queue.
simplifyQueue :: Function f => Config -> State f -> State f

-- | Enqueue a set of critical pairs.
enqueue :: Function f => State f -> RuleId -> [Passive Params] -> State f

-- | Dequeue a critical pair.
--   
--   Also takes care of:
--   
--   <ul>
--   <li>removing any orphans from the head of the queue</li>
--   <li>ignoring CPs that are too big</li>
--   </ul>
dequeue :: Function f => Config -> State f -> (Maybe (CriticalPair f, ActiveRule f, ActiveRule f), State f)
data Active f
Active :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Depth -> {-# UNPACK #-} !(Rule f) -> !(Maybe (Term f)) -> {-# UNPACK #-} !(Proof f) -> !(Model f) -> ![ActiveRule f] -> Active f
[active_id] :: Active f -> {-# UNPACK #-} !Id
[active_depth] :: Active f -> {-# UNPACK #-} !Depth
[active_rule] :: Active f -> {-# UNPACK #-} !(Rule f)
[active_top] :: Active f -> !(Maybe (Term f))
[active_proof] :: Active f -> {-# UNPACK #-} !(Proof f)
[active_model] :: Active f -> !(Model f)
[active_rules] :: Active f -> ![ActiveRule f]
active_cp :: Active f -> CriticalPair f
data ActiveRule f
ActiveRule :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !RuleId -> {-# UNPACK #-} !Depth -> {-# UNPACK #-} !(Rule f) -> {-# UNPACK #-} !(Proof f) -> !(Positions f) -> ActiveRule f
[rule_active] :: ActiveRule f -> {-# UNPACK #-} !Id
[rule_rid] :: ActiveRule f -> {-# UNPACK #-} !RuleId
[rule_depth] :: ActiveRule f -> {-# UNPACK #-} !Depth
[rule_rule] :: ActiveRule f -> {-# UNPACK #-} !(Rule f)
[rule_proof] :: ActiveRule f -> {-# UNPACK #-} !(Proof f)
[rule_positions] :: ActiveRule f -> !(Positions f)
newtype RuleId
RuleId :: Id -> RuleId
addActive :: Function f => Config -> State f -> (Id -> RuleId -> RuleId -> Active f) -> State f
addActiveOnly :: Function f => State f -> Active f -> State f
deleteActive :: Function f => State f -> Active f -> State f
consider :: Function f => Config -> State f -> CriticalPair f -> State f
considerUsing :: Function f => RuleIndex f (ActiveRule f) -> Config -> State f -> CriticalPair f -> State f
addCP :: Function f => Config -> Model f -> State f -> CriticalPair f -> State f
addAxiom :: Function f => Config -> State f -> Axiom f -> State f
addJoinable :: Function f => State f -> Equation f -> State f
data Goal f
Goal :: String -> Int -> Equation f -> Set (Resulting f) -> Set (Resulting f) -> Goal f
[goal_name] :: Goal f -> String
[goal_number] :: Goal f -> Int
[goal_eqn] :: Goal f -> Equation f
[goal_lhs] :: Goal f -> Set (Resulting f)
[goal_rhs] :: Goal f -> Set (Resulting f)
addGoal :: Function f => Config -> State f -> Goal f -> State f
normaliseGoals :: Function f => State f -> State f
goal :: Int -> String -> Equation f -> Goal f
interreduce :: Function f => Config -> State f -> State f
interreduce1 :: Function f => Config -> State f -> Active f -> State f
data Output m f
Output :: (Message f -> m ()) -> Output m f
[output_message] :: Output m f -> Message f -> m ()
complete :: (Function f, MonadIO m) => Output m f -> Config -> State f -> m (State f)
complete1 :: Function f => Config -> State f -> (Bool, State f)
solved :: Function f => State f -> Bool
solutions :: Function f => State f -> [ProvedGoal f]
rules :: Function f => State f -> [Rule f]
completePure :: Function f => Config -> State f -> State f
normaliseTerm :: Function f => State f -> Term f -> Resulting f
normalForms :: Function f => State f -> Term f -> Set (Resulting f)
simplifyTerm :: Function f => State f -> Term f -> Term f
instance GHC.Enum.Enum Twee.RuleId
instance GHC.Real.Integral Twee.RuleId
instance GHC.Real.Real Twee.RuleId
instance GHC.Num.Num Twee.RuleId
instance GHC.Show.Show Twee.RuleId
instance GHC.Classes.Ord Twee.RuleId
instance GHC.Classes.Eq Twee.RuleId
instance Twee.Base.Function f => Text.PrettyPrint.HughesPJClass.Pretty (Twee.Message f)
instance GHC.Classes.Eq (Twee.Active f)
instance Twee.Base.Function f => Text.PrettyPrint.HughesPJClass.Pretty (Twee.Active f)
instance Twee.Pretty.PrettyTerm f => Twee.Base.Symbolic (Twee.ActiveRule f)
instance GHC.Classes.Eq (Twee.ActiveRule f)
instance Twee.Base.Has (Twee.ActiveRule f) Twee.Base.Id
instance Twee.Base.Has (Twee.ActiveRule f) Twee.RuleId
instance Twee.Base.Has (Twee.ActiveRule f) Twee.CP.Depth
instance f ~ g => Twee.Base.Has (Twee.ActiveRule f) (Twee.Rule.Rule g)
instance f ~ g => Twee.Base.Has (Twee.ActiveRule f) (Twee.Proof.Proof g)
instance f ~ g => Twee.Base.Has (Twee.ActiveRule f) (Twee.Proof.Lemma g)
instance f ~ g => Twee.Base.Has (Twee.ActiveRule f) (Twee.CP.Positions g)
instance Twee.PassiveQueue.Params Twee.Params