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


-- | Data Type for Rewriting Systems
--   
--   The package defines data types and parsers for rewriting systems and
--   termination proofs, as used in the Termination Competitions. For
--   syntax and semantics specification, see
--   <a>http://www.termination-portal.org/wiki/TPDB</a>
@package tpdb
@version 2.2.2

module TPDB.Data.Rule
data Relation
Strict :: Relation
Weak :: Relation
Equal :: Relation
data Rule a
Rule :: a -> a -> Relation -> Bool -> Rule a
[lhs] :: Rule a -> a
[rhs] :: Rule a -> a
[relation] :: Rule a -> Relation
[top] :: Rule a -> Bool
strict :: Rule a -> Bool
weak :: Rule a -> Bool
equal :: Rule a -> Bool
instance GHC.Show.Show TPDB.Data.Rule.Relation
instance GHC.Classes.Ord TPDB.Data.Rule.Relation
instance GHC.Classes.Eq TPDB.Data.Rule.Relation
instance GHC.Classes.Ord a => GHC.Classes.Ord (TPDB.Data.Rule.Rule a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (TPDB.Data.Rule.Rule a)
instance GHC.Base.Functor TPDB.Data.Rule.Rule

module TPDB.Data.Term
data Term v s
Var :: v -> Term v s
Node :: s -> [Term v s] -> Term v s
vmap :: (v -> u) -> Term v s -> Term u s
type Position = [Int]
positions :: Term v c -> [(Position, Term v c)]
size :: Term v c -> Int
depth :: Term v c -> Int

-- | all positions
pos :: Term v c -> [Position]

-- | non-variable positions
sympos :: Term v c -> [Position]

-- | variable positions
varpos :: Term v c -> [Position]

-- | leaf positions (= nullary symbols)
leafpos :: Term v c -> [Position]
subterms :: Term v c -> [Term v c]
strict_subterms :: Term v c -> [Term v c]
isSubtermOf :: (Eq v, Eq c) => Term v c -> Term v c -> Bool
isStrictSubtermOf :: (Eq v, Eq c) => Term v c -> Term v c -> Bool

-- | compute new symbol at position, giving the position
pmap :: (Position -> c -> d) -> Term v c -> Term v d

-- | compute new symbol from *reverse* position and previous symbol this is
--   more efficient (no reverse needed)
rpmap :: (Position -> c -> d) -> Term v c -> Term v d
peek :: Term v c -> Position -> Term v c
peek_symbol :: Term v c -> Position -> c

-- | warning: don't check arity
poke_symbol :: Term v c -> (Position, c) -> Term v c
poke :: Term v c -> (Position, Term v c) -> Term v c
pokes :: Term v c -> [(Position, Term v c)] -> Term v c

-- | in preorder
symsl :: Term v c -> [c]
syms :: Ord c => Term v c -> Set c
lsyms :: Ord c => Term v c -> [c]
vars :: Ord v => Term v c -> Set v
isvar :: Term v c -> Bool

-- | list of variables (each occurs once, unspecified ordering)
lvars :: Ord v => Term v c -> [v]

-- | list of variables (in pre-order, with duplicates)
voccs :: Term v c -> [v]
instance (GHC.Show.Show v, GHC.Show.Show s) => GHC.Show.Show (TPDB.Data.Term.Term v s)
instance (GHC.Classes.Ord v, GHC.Classes.Ord s) => GHC.Classes.Ord (TPDB.Data.Term.Term v s)
instance (GHC.Classes.Eq v, GHC.Classes.Eq s) => GHC.Classes.Eq (TPDB.Data.Term.Term v s)
instance GHC.Base.Functor (TPDB.Data.Term.Term v)

module TPDB.Pretty

-- | The abstract data type <tt><a>Doc</a> ann</tt> represents pretty
--   documents that have been annotated with data of type <tt>ann</tt>.
--   
--   More specifically, a value of type <tt><a>Doc</a></tt> represents a
--   non-empty set of possible layouts of a document. The layout functions
--   select one of these possibilities, taking into account things like the
--   width of the output document.
--   
--   The annotation is an arbitrary piece of data associated with (part of)
--   a document. Annotations may be used by the rendering backends in order
--   to display output differently, such as
--   
--   <ul>
--   <li>color information (e.g. when rendering to the terminal)</li>
--   <li>mouseover text (e.g. when rendering to rich HTML)</li>
--   <li>whether to show something or not (to allow simple or detailed
--   versions)</li>
--   </ul>
--   
--   The simplest way to display a <a>Doc</a> is via the <a>Show</a> class.
--   
--   <pre>
--   &gt;&gt;&gt; putStrLn (show (vsep ["hello", "world"]))
--   hello
--   world
--   </pre>
data Doc ann

-- | Overloaded conversion to <a>Doc</a>.
--   
--   Laws:
--   
--   <ol>
--   <li>output should be pretty. :-)</li>
--   </ol>
class Pretty a

-- | <pre>
--   &gt;&gt;&gt; pretty 1 &lt;+&gt; pretty "hello" &lt;+&gt; pretty 1.234
--   1 hello 1.234
--   </pre>
pretty :: Pretty a => a -> Doc ann

-- | <tt><a>prettyList</a></tt> is only used to define the <tt>instance
--   <a>Pretty</a> a =&gt; <a>Pretty</a> [a]</tt>. In normal circumstances
--   only the <tt><a>pretty</a></tt> function is used.
--   
--   <pre>
--   &gt;&gt;&gt; prettyList [1, 23, 456]
--   [1, 23, 456]
--   </pre>
prettyList :: Pretty a => [a] -> Doc ann
render :: Doc ann -> Text
renderWide :: Doc ann -> SimpleDocStream ann
renderCompact :: Doc ann1 -> SimpleDocStream ann2
renderPretty :: Doc ann -> SimpleDocStream ann
displayIO :: Handle -> SimpleDocStream ann -> IO ()
fsep :: [Doc ann] -> Doc ann
sep :: [Doc ann] -> Doc ann
hsep :: [Doc ann] -> Doc ann
vsep :: [Doc ann] -> Doc ann
vcat :: [Doc ann] -> Doc ann
hcat :: [Doc ann] -> Doc ann

-- | <pre>
--   &gt;&gt;&gt; parens "·"
--   (·)
--   </pre>
parens :: Doc ann -> Doc ann

-- | <pre>
--   &gt;&gt;&gt; brackets "·"
--   [·]
--   </pre>
brackets :: Doc ann -> Doc ann

-- | <pre>
--   &gt;&gt;&gt; angles "·"
--   &lt;·&gt;
--   </pre>
angles :: Doc ann -> Doc ann

-- | <pre>
--   &gt;&gt;&gt; braces "·"
--   {·}
--   </pre>
braces :: Doc ann -> Doc ann

-- | <tt>(<a>enclose</a> l r x)</tt> encloses document <tt>x</tt> between
--   documents <tt>l</tt> and <tt>r</tt> using <tt><a>&lt;&gt;</a></tt>.
--   
--   <pre>
--   &gt;&gt;&gt; enclose "A" "Z" "·"
--   A·Z
--   </pre>
--   
--   <pre>
--   <a>enclose</a> l r x = l <a>&lt;&gt;</a> x <a>&lt;&gt;</a> r
--   </pre>
enclose :: Doc ann -> Doc ann -> Doc ann -> Doc ann

-- | <tt>(<a>encloseSep</a> l r sep xs)</tt> concatenates the documents
--   <tt>xs</tt> separated by <tt>sep</tt>, and encloses the resulting
--   document by <tt>l</tt> and <tt>r</tt>.
--   
--   The documents are laid out horizontally if that fits the page:
--   
--   <pre>
--   &gt;&gt;&gt; let doc = "list" &lt;+&gt; align (encloseSep lbracket rbracket comma (map pretty [1,20,300,4000]))
--   
--   &gt;&gt;&gt; putDocW 80 doc
--   list [1,20,300,4000]
--   </pre>
--   
--   If there is not enough space, then the input is split into lines
--   entry-wise therwise they are laid out vertically, with separators put
--   in the front:
--   
--   <pre>
--   &gt;&gt;&gt; putDocW 10 doc
--   list [1
--        ,20
--        ,300
--        ,4000]
--   </pre>
--   
--   Note that <tt>doc</tt> contains an explicit call to <a>align</a> so
--   that the list items are aligned vertically.
--   
--   For putting separators at the end of entries instead, have a look at
--   <a>punctuate</a>.
encloseSep :: Doc ann -> Doc ann -> Doc ann -> [Doc ann] -> Doc ann

-- | <tt>(<a>punctuate</a> p xs)</tt> appends <tt>p</tt> to all but the
--   last document in <tt>xs</tt>.
--   
--   <pre>
--   &gt;&gt;&gt; let docs = punctuate comma (Util.words "lorem ipsum dolor sit amet")
--   
--   &gt;&gt;&gt; putDocW 80 (hsep docs)
--   lorem, ipsum, dolor, sit, amet
--   </pre>
--   
--   The separators are put at the end of the entries, which we can see if
--   we position the result vertically:
--   
--   <pre>
--   &gt;&gt;&gt; putDocW 20 (vsep docs)
--   lorem,
--   ipsum,
--   dolor,
--   sit,
--   amet
--   </pre>
--   
--   If you want put the commas in front of their elements instead of at
--   the end, you should use <a>tupled</a> or, in general,
--   <a>encloseSep</a>.
punctuate :: Doc ann -> [Doc ann] -> [Doc ann]

-- | <pre>
--   &gt;&gt;&gt; comma
--   ,
--   </pre>
comma :: Doc ann

-- | <tt>(<a>nest</a> i x)</tt> lays out the document <tt>x</tt> with the
--   current nesting level (indentation of the following lines) increased
--   by <tt>i</tt>. Negative values are allowed, and decrease the nesting
--   level accordingly.
--   
--   <pre>
--   &gt;&gt;&gt; vsep [nest 4 (vsep ["lorem", "ipsum", "dolor"]), "sit", "amet"]
--   lorem
--       ipsum
--       dolor
--   sit
--   amet
--   </pre>
--   
--   See also
--   
--   <ul>
--   <li><a>hang</a> (<a>nest</a> relative to current cursor position
--   instead of current nesting level)</li>
--   <li><a>align</a> (set nesting level to current cursor position)</li>
--   <li><a>indent</a> (increase indentation on the spot, padding with
--   spaces).</li>
--   </ul>
nest :: Int -> Doc ann -> Doc ann

-- | Haskell-inspired variant of <a>encloseSep</a> with braces and comma as
--   separator.
--   
--   <pre>
--   &gt;&gt;&gt; let doc = list (map pretty [1,20,300,4000])
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; putDocW 80 doc
--   [1, 20, 300, 4000]
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; putDocW 10 doc
--   [ 1
--   , 20
--   , 300
--   , 4000 ]
--   </pre>
list :: [Doc ann] -> Doc ann

-- | Haskell-inspired variant of <a>encloseSep</a> with parentheses and
--   comma as separator.
--   
--   <pre>
--   &gt;&gt;&gt; let doc = tupled (map pretty [1,20,300,4000])
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; putDocW 80 doc
--   (1, 20, 300, 4000)
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; putDocW 10 doc
--   ( 1
--   , 20
--   , 300
--   , 4000 )
--   </pre>
tupled :: [Doc ann] -> Doc ann

-- | An associative operation.
--   
--   <pre>
--   &gt;&gt;&gt; [1,2,3] &lt;&gt; [4,5,6]
--   [1,2,3,4,5,6]
--   </pre>
(<>) :: Semigroup a => a -> a -> a
infixr 6 <>

-- | Identity of <a>mappend</a>
--   
--   <pre>
--   &gt;&gt;&gt; "Hello world" &lt;&gt; mempty
--   "Hello world"
--   </pre>
mempty :: Monoid a => a
empty :: Doc ann
text :: String -> Doc ann
(<+>) :: Doc ann -> Doc ann -> Doc ann
($$) :: Doc ann -> Doc ann -> Doc ann

-- | <tt>(<a>indent</a> i x)</tt> indents document <tt>x</tt> by <tt>i</tt>
--   columns, starting from the current cursor position.
--   
--   <pre>
--   &gt;&gt;&gt; let doc = reflow "The indent function indents these words!"
--   
--   &gt;&gt;&gt; putDocW 24 ("prefix" &lt;&gt; indent 4 doc)
--   prefix    The indent
--             function
--             indents these
--             words!
--   </pre>
--   
--   <pre>
--   <a>indent</a> i d = <a>hang</a> i ({i spaces} &lt;&gt; d)
--   </pre>
indent :: Int -> Doc ann -> Doc ann

-- | <tt>(<a>nest</a> i x)</tt> lays out the document <tt>x</tt> with the
--   current nesting level (indentation of the following lines) increased
--   by <tt>i</tt>. Negative values are allowed, and decrease the nesting
--   level accordingly.
--   
--   <pre>
--   &gt;&gt;&gt; vsep [nest 4 (vsep ["lorem", "ipsum", "dolor"]), "sit", "amet"]
--   lorem
--       ipsum
--       dolor
--   sit
--   amet
--   </pre>
--   
--   See also
--   
--   <ul>
--   <li><a>hang</a> (<a>nest</a> relative to current cursor position
--   instead of current nesting level)</li>
--   <li><a>align</a> (set nesting level to current cursor position)</li>
--   <li><a>indent</a> (increase indentation on the spot, padding with
--   spaces).</li>
--   </ul>
nest :: Int -> Doc ann -> Doc ann

-- | <tt>(<a>hang</a> i x)</tt> lays out the document <tt>x</tt> with a
--   nesting level set to the <i>current column</i> plus <tt>i</tt>.
--   Negative values are allowed, and decrease the nesting level
--   accordingly.
--   
--   <pre>
--   &gt;&gt;&gt; let doc = reflow "Indenting these words with hang"
--   
--   &gt;&gt;&gt; putDocW 24 ("prefix" &lt;+&gt; hang 4 doc)
--   prefix Indenting these
--              words with
--              hang
--   </pre>
--   
--   This differs from <a>nest</a>, which is based on the <i>current
--   nesting level</i> plus <tt>i</tt>. When you're not sure, try the more
--   efficient <a>nest</a> first. In our example, this would yield
--   
--   <pre>
--   &gt;&gt;&gt; let doc = reflow "Indenting these words with nest"
--   
--   &gt;&gt;&gt; putDocW 24 ("prefix" &lt;+&gt; nest 4 doc)
--   prefix Indenting these
--       words with nest
--   </pre>
--   
--   <pre>
--   <a>hang</a> i doc = <a>align</a> (<a>nest</a> i doc)
--   </pre>
hang :: Int -> Doc ann -> Doc ann
instance (Prettyprinter.Internal.Pretty a, Prettyprinter.Internal.Pretty b, Prettyprinter.Internal.Pretty c, Prettyprinter.Internal.Pretty d) => Prettyprinter.Internal.Pretty (a, b, c, d)
instance (Prettyprinter.Internal.Pretty a, Prettyprinter.Internal.Pretty b) => Prettyprinter.Internal.Pretty (Data.Either.Either a b)

module TPDB.Data.Attributes
data Attributes
Attributes :: Int -> Int -> Int -> Int -> Int -> Bool -> Bool -> Bool -> Int -> Int -> Attributes
[size_of_signature] :: Attributes -> Int
[max_arity] :: Attributes -> Int
[total_term_size] :: Attributes -> Int
[max_term_size] :: Attributes -> Int
[max_term_depth] :: Attributes -> Int
[left_linear] :: Attributes -> Bool
[right_linear] :: Attributes -> Bool
[linear] :: Attributes -> Bool
[max_var_count] :: Attributes -> Int

-- | value is meaningless if the system has no variables
[max_var_depth] :: Attributes -> Int
compute_attributes :: (Ord v, Ord c) => [Rule (Term v c)] -> Attributes
safe_maximum :: Ord p => p -> [p] -> p
varcount :: Ord v => Rule (Term v c) -> Map v (Int, Int)
varcount_term :: Ord v => Term v c -> Map v Int
instance GHC.Show.Show TPDB.Data.Attributes.Attributes
instance Prettyprinter.Internal.Pretty TPDB.Data.Attributes.Attributes


-- | Data types for rewrite systems and termination problems. A "bare" term
--   rewrite system (list of rules and relative rules) is <tt>TRS v s</tt>.
--   A termination problem is <tt>Problem v s</tt>. This contains a rewrite
--   system plus extra information (strategy, theory, etc.)
module TPDB.Data
type SES = SRS Identifier

-- | legacy stuff (used in matchbox)
type TES = TRS Identifier Identifier
data Startterm
Startterm_Constructor_based :: Startterm
Startterm_Full :: Startterm
data Theory
A :: Theory
C :: Theory
AC :: Theory

-- | this is modelled after
--   <a>https://www.lri.fr/~marche/tpdb/format.html</a>
data Theorydecl v s

-- | example: "(AC plus)"
Property :: Theory -> [s] -> Theorydecl v s
Equations :: [Rule (Term v s)] -> Theorydecl v s
data Strategy
Full :: Strategy
Innermost :: Strategy
Outermost :: Strategy
data Type
Termination :: Type
Complexity :: Type
data Problem v s
Problem :: Type -> TRS v s -> Maybe Strategy -> Signature -> Maybe Startterm -> Attributes -> Problem v s
[type_] :: Problem v s -> Type
[trs] :: Problem v s -> TRS v s
[strategy] :: Problem v s -> Maybe Strategy
[full_signature] :: Problem v s -> Signature
[startterm] :: Problem v s -> Maybe Startterm
[attributes] :: Problem v s -> Attributes
type SRS s = RS s [s]
type TRS v s = RS s (Term v s)
data RS s r
RS :: [s] -> [Rule r] -> Bool -> RS s r

-- | better keep order in signature (?)
[signature] :: RS s r -> [s]
[rules] :: RS s r -> [Rule r]

-- | if True, write comma between rules
[separate] :: RS s r -> Bool
data Replacementmap
Replacementmap :: [Int] -> Replacementmap
data Signature
Signature :: [Funcsym] -> Signature
HigherOrderSignature :: Signature

-- | according to XTC spec
data Funcsym
Funcsym :: Text -> Int -> Maybe Theory -> Maybe Replacementmap -> Funcsym
[fs_name] :: Funcsym -> Text
[fs_arity] :: Funcsym -> Int
[fs_theory] :: Funcsym -> Maybe Theory
[fs_replacementmap] :: Funcsym -> Maybe Replacementmap
class Ord (Var t) => Variables t where {
    type family Var t;
}
variables :: Variables t => t -> Set (Var t)
data Identifier
Identifier :: !Int -> !Text -> Int -> Identifier
[_identifier_hash] :: Identifier -> !Int
[name] :: Identifier -> !Text
[arity] :: Identifier -> Int
mk :: Int -> Text -> Identifier
strict_rules :: RS s b -> [(b, b)]
weak_rules :: RS s b -> [(b, b)]
equal_rules :: RS s b -> [(b, b)]
mknullary :: Text -> Identifier
mkunary :: Text -> Identifier
from_strict_rules :: Bool -> [(t, t)] -> RS i t
with_rules :: RS s r1 -> [Rule r2] -> RS s r2
instance GHC.Classes.Ord TPDB.Data.Identifier
instance GHC.Classes.Eq TPDB.Data.Identifier
instance GHC.Show.Show TPDB.Data.Replacementmap
instance GHC.Show.Show TPDB.Data.Type
instance GHC.Show.Show TPDB.Data.Strategy
instance GHC.Show.Show TPDB.Data.Theory
instance GHC.Read.Read TPDB.Data.Theory
instance GHC.Classes.Ord TPDB.Data.Theory
instance GHC.Classes.Eq TPDB.Data.Theory
instance GHC.Show.Show TPDB.Data.Funcsym
instance GHC.Show.Show TPDB.Data.Signature
instance GHC.Show.Show TPDB.Data.Startterm
instance TPDB.Data.Variables (TPDB.Data.SRS s)
instance GHC.Classes.Ord v => TPDB.Data.Variables (TPDB.Data.TRS v s)
instance GHC.Classes.Eq r => GHC.Classes.Eq (TPDB.Data.RS s r)
instance GHC.Base.Functor (TPDB.Data.RS s)
instance GHC.Classes.Ord v => TPDB.Data.Variables (TPDB.Data.Term.Term v c)
instance TPDB.Data.Variables [c]
instance TPDB.Data.Variables r => TPDB.Data.Variables (TPDB.Data.Rule.Rule r)
instance Data.Hashable.Class.Hashable TPDB.Data.Identifier
instance GHC.Show.Show TPDB.Data.Identifier


-- | the "old" TPDB format cf.
--   <a>http://www.lri.fr/~marche/tpdb/format.html</a>
module TPDB.Plain.Write
class PrettyTerm a
prettyTerm :: PrettyTerm a => a -> Doc ann
instance TPDB.Plain.Write.PrettyTerm a => Prettyprinter.Internal.Pretty (TPDB.Data.Rule.Rule a)
instance Prettyprinter.Internal.Pretty s => TPDB.Plain.Write.PrettyTerm [s]
instance (Prettyprinter.Internal.Pretty v, Prettyprinter.Internal.Pretty s) => TPDB.Plain.Write.PrettyTerm (TPDB.Data.Term.Term v s)
instance (Prettyprinter.Internal.Pretty s, TPDB.Plain.Write.PrettyTerm r, TPDB.Data.Variables (TPDB.Data.RS s r), Prettyprinter.Internal.Pretty (TPDB.Data.Var (TPDB.Data.RS s r))) => Prettyprinter.Internal.Pretty (TPDB.Data.RS s r)
instance Prettyprinter.Internal.Pretty TPDB.Data.Identifier
instance (Prettyprinter.Internal.Pretty v, Prettyprinter.Internal.Pretty s) => Prettyprinter.Internal.Pretty (TPDB.Data.Term.Term v s)
instance (Prettyprinter.Internal.Pretty s, Prettyprinter.Internal.Pretty r, TPDB.Data.Variables (TPDB.Data.Term.Term s r)) => Prettyprinter.Internal.Pretty (TPDB.Data.Problem s r)


-- | textual input, cf. <a>http://www.lri.fr/~marche/tpdb/format.html</a>
module TPDB.Plain.Read
trs :: Text -> Either String (TRS Identifier Identifier)
srs :: Text -> Either String (SRS Identifier)
class Reader a
reader :: Reader a => Parser a

-- | warning: by definition, {}[] may appear in identifiers
lexer :: GenTokenParser Text () Identity
data Declaration u
Var_Declaration :: [Identifier] -> Declaration u
Theory_Declaration :: Declaration u
Strategy_Declaration :: Declaration u
Rules_Declaration :: [Rule u] -> Declaration u

-- | this is super-ugly: a parenthesized, possibly nested, possibly
--   comma-separated, list of identifiers or strings
Unknown_Declaration :: Declaration u
declaration :: Reader u => Bool -> Parser (Declaration u)
anylist :: ParsecT Text () Identity ()
repair_signature_srs :: Eq s1 => RS s2 [s1] -> RS s1 [s1]
make_srs :: Eq s => [Declaration [s]] -> SRS s
repair_signature_trs :: Ord s1 => RS s2 (Term v s1) -> RS s1 (Term v s1)
make_trs :: [Declaration (Term Identifier Identifier)] -> TRS Identifier Identifier
repair_variables :: (Monad m, Foldable t, Eq s) => t s -> m (Rule (Term v s)) -> m (Rule (Term s s))
instance TPDB.Plain.Read.Reader TPDB.Data.Identifier
instance TPDB.Plain.Read.Reader s => TPDB.Plain.Read.Reader [s]
instance TPDB.Plain.Read.Reader v => TPDB.Plain.Read.Reader (TPDB.Data.Term.Term v TPDB.Data.Identifier)
instance TPDB.Plain.Read.Reader u => TPDB.Plain.Read.Reader (TPDB.Data.Rule.Rule u)
instance TPDB.Plain.Read.Reader (TPDB.Data.SRS TPDB.Data.Identifier)
instance TPDB.Plain.Read.Reader (TPDB.Data.TRS TPDB.Data.Identifier TPDB.Data.Identifier)

module TPDB.DP.Unify

-- | naive implementation (worst case exponential)
mgu :: (Ord v, Eq c) => Term v c -> Term v c -> Maybe (Map v (Term v c))

-- | will only bind variables in the left side
match :: (Ord v, Ord w, Eq c) => Term v c -> Term w c -> Maybe (Map v (Term w c))
unifies :: (Ord v, Eq c) => Term v c -> Term v c -> Bool
apply :: Ord k => Term k s -> Map k (Term k s) -> Term k s
times :: Ord v => Substitution v c -> Substitution v c -> Substitution v c

module TPDB.Convert
srs2trs :: SRS Identifier -> TRS Identifier Identifier
set_arity :: Int -> Identifier -> Identifier
convert_srs_rule :: Rule [Identifier] -> Rule (Term Identifier Identifier)
trs2srs :: Eq v => TRS v s -> Maybe (SRS s)
convert_trs_rule :: Eq a => Rule (Term a s) -> Maybe (Rule [s])
unspine :: v -> [s] -> Term v s

-- | success iff term consists of unary symbols and the lowest node is a
--   variable
spine :: Term v s -> Maybe ([s], v)

module TPDB.Mirror

-- | if input is SRS, reverse lhs and rhs of each rule
mirror :: TRS Identifier s -> Maybe (TRS Identifier s)

module TPDB.DP.Transform
data Marked a
Original :: a -> Marked a
Marked :: a -> Marked a
Auxiliary :: a -> Marked a
isOriginal :: Marked a -> Bool
isMarked :: Marked a -> Bool
mark_top :: Term v a -> Term v (Marked a)
defined :: Ord a => RS s (Term v a) -> Set a

-- | compute the DP transformed system.
dp :: (Ord v, Ord s) => RS s (Term v s) -> RS (Marked s) (Term v (Marked s))
instance GHC.Generics.Generic (TPDB.DP.Transform.Marked a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (TPDB.DP.Transform.Marked a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (TPDB.DP.Transform.Marked a)
instance GHC.Show.Show a => GHC.Show.Show (TPDB.DP.Transform.Marked a)
instance Data.Hashable.Class.Hashable a => Data.Hashable.Class.Hashable (TPDB.DP.Transform.Marked a)
instance Prettyprinter.Internal.Pretty a => Prettyprinter.Internal.Pretty (TPDB.DP.Transform.Marked a)

module TPDB.DP.TCap

-- | This function keeps only those parts of the input term which cannot be
--   reduced, even if the term is instantiated. All other parts are
--   replaced by fresh variables. Def 4.4 in
--   <a>http://cl-informatik.uibk.ac.at/users/griff/publications/Sternagel-Thiemann-RTA10.pdf</a>
tcap :: (Ord v, Ord c) => TRS v c -> Term v c -> Term Int c
fresh_var :: State Int (Term Int c)
walk :: (Ord a, Eq c) => RS s (Term a c) -> Term v c -> StateT Int Identity (Term Int c)

module TPDB.DP.Usable

-- | DANGER: this ignores the CE condition
restrict :: (Ord c, Ord v) => RS c (Term v c) -> RS c (Term v c)

-- | computes the least closed set of usable rules, cf. Def 4.5
--   <a>http://cl-informatik.uibk.ac.at/users/griff/publications/Sternagel-Thiemann-RTA10.pdf</a>
usable :: (Ord v, Ord c) => TRS v c -> Set (Rule (Term v c))
fixpoint :: Eq t => (t -> t) -> t -> t
required :: (Ord v, Ord c) => TRS v c -> Set (Rule (Term v c)) -> Set (Rule (Term v c))
needed :: (Ord v, Ord c) => TRS v c -> Term v c -> [Rule (Term v c)]

module TPDB.DP.Graph

-- | DP problems for strongly connected components, topologically sorted,
--   with CyclicComponents in Right, others in Left.
components :: (Ord v, Ord a) => RS (Marked a) (Term v (Marked a)) -> [Either (Rule (Term v (Marked a))) (RS (Marked a) (Term v (Marked a)))]

-- | edges of the estimated dependency graph
edges :: (Ord v, Ord a) => RS (Marked a) (Term v (Marked a)) -> [(Rule (Term v (Marked a)), Rule (Term v (Marked a)))]
check :: [(Rule (Term Identifier (Marked Identifier)), Rule (Term Identifier (Marked Identifier)))]
sys :: TRS Identifier Identifier

module TPDB.DP


-- | construct data object from XML tree.
module TPDB.XTC.Read
readProblemF :: FilePath -> IO (Problem Identifier Identifier)
readProblemT :: Text -> Either SomeException (Problem Identifier Identifier)


-- | read benchmark from in-memory data (e.g., from a ByteString)
module TPDB.Input.Memory

-- | first argument is file name, second argument is file contents. first
--   arg. is needed to pick the proper parser (SRS, TRS, XTC)
get :: String -> Text -> IO (Either String (Either (TRS Identifier Identifier) (SRS Identifier)))

module TPDB.Input.File

-- | read input from file with given name. can have extension .srs, .trs,
--   .xml. unknown extension is considered as .xml, because of
--   <a>http://starexec.forumotion.com/t60-restore-file-extension-for-renamed-benchmarks</a>
get :: FilePath -> IO (Either (TRS Identifier Identifier) (SRS Identifier))
getE :: FilePath -> IO (Either String (Either (TRS Identifier Identifier) (SRS Identifier)))
get_trs :: FilePath -> IO (TRS Identifier Identifier)
getE_trs :: FilePath -> IO (Either String (TRS Identifier Identifier))
get_srs :: FilePath -> IO (SRS Identifier)


-- | <i>Deprecated: use TPDB.INput.File instead</i>
module TPDB.Input

module TPDB.XTC.Write
document :: Problem Identifier Identifier -> Document
writeFile :: RenderSettings -> FilePath -> Document -> IO ()
renderLBS :: RenderSettings -> Document -> ByteString
renderText :: RenderSettings -> Document -> Text

-- | The default value for this type.
def :: Default a => a

module TPDB.XTC

module TPDB.Xml
class XmlContent a
toContents :: XmlContent a => a -> [Node]
parseContents :: XmlContent a => Cursor -> [a]
mkel :: Name -> [Node] -> Node
rmkel :: Monad m => Name -> [Node] -> m Node

-- | Select only text nodes, and directly give the <tt>Content</tt> values.
--   XPath: <i>The node test text() is true for any text node.</i>
--   
--   Note that this is not strictly an <a>Axis</a>, but will work with most
--   combinators.
content :: Cursor -> [Text]

-- | Apply a function to the result of an axis.
(&|) :: (Cursor node -> [a]) -> (a -> b) -> Cursor node -> [b]
infixr 1 &|
escape :: [Char] -> [Char]
nospaceString :: Text -> Node
instance TPDB.Xml.XmlContent GHC.Types.Int
instance TPDB.Xml.XmlContent GHC.Integer.Type.Integer
instance TPDB.Xml.XmlContent GHC.Types.Bool

module TPDB.Data.Xml
no_sharp_name_HACK :: p -> p
instance TPDB.Xml.XmlContent TPDB.Data.Identifier
instance (GHC.Show.Show v, TPDB.Xml.XmlContent v, TPDB.Xml.XmlContent c) => TPDB.Xml.XmlContent (TPDB.Data.Term.Term v c)
instance TPDB.Xml.XmlContent (TPDB.Data.Term.Term v c) => TPDB.Xml.XmlContent (TPDB.Data.Rule.Rule (TPDB.Data.Term.Term v c))


-- | internal representation of CPF termination proofs, see
--   <a>http://cl-informatik.uibk.ac.at/software/cpf/</a>
module TPDB.CPF.Proof.Type
data ACTerminationProof
ACTerminationProofFIXME :: () -> ACTerminationProof
data ArgumentFilterEntry
ArgumentFilterEntry :: Symbol -> Int -> Either Int [Int] -> ArgumentFilterEntry
[afeSymbol] :: ArgumentFilterEntry -> Symbol
[afeArity] :: ArgumentFilterEntry -> Int
[afeFilter] :: ArgumentFilterEntry -> Either Int [Int]
data PrecedenceEntry
PrecedenceEntry :: Symbol -> Int -> Integer -> PrecedenceEntry
[peSymbol] :: PrecedenceEntry -> Symbol
[peArity] :: PrecedenceEntry -> Int
[pePrecedence] :: PrecedenceEntry -> Integer
data PathOrder
PathOrder :: [PrecedenceEntry] -> [ArgumentFilterEntry] -> PathOrder
class ToExotic a
toExotic :: ToExotic a => a -> Exotic
data Exotic
Minus_Infinite :: Exotic
E_Integer :: Integer -> Exotic
E_Rational :: Rational -> Exotic
Plus_Infinite :: Exotic
data Coefficient
Vector :: [Coefficient] -> Coefficient
Matrix :: [Coefficient] -> Coefficient
Coefficient_Coefficient :: a -> Coefficient
data Label
LblNumber :: [Integer] -> Label
LblSymbol :: [Symbol] -> Label
data Symbol
SymName :: Identifier -> Symbol
SymSharp :: Symbol -> Symbol
SymLabel :: Symbol -> Label -> Symbol
data ArithFunction
AFNatural :: Integer -> ArithFunction
AFVariable :: Integer -> ArithFunction
AFSum :: [ArithFunction] -> ArithFunction
AFProduct :: [ArithFunction] -> ArithFunction
AFMin :: [ArithFunction] -> ArithFunction
AFMax :: [ArithFunction] -> ArithFunction
AFIfEqual :: ArithFunction -> ArithFunction -> ArithFunction -> ArithFunction -> ArithFunction
data Polynomial
Sum :: [Polynomial] -> Polynomial
Product :: [Polynomial] -> Polynomial
Polynomial_Coefficient :: Coefficient -> Polynomial
Polynomial_Variable :: Text -> Polynomial
data Value
Polynomial :: Polynomial -> Value
ArithFunction :: ArithFunction -> Value
data Interpret
Interpret :: Symbol -> Int -> Value -> Interpret
[symbol] :: Interpret -> Symbol
[arity] :: Interpret -> Int
[value] :: Interpret -> Value
data Domain
Naturals :: Domain
Rationals :: Rational -> Domain
Arctic :: Domain -> Domain
Tropical :: Domain -> Domain
data Interpretation_Type
Matrix_Interpretation :: Domain -> Int -> Int -> Interpretation_Type
[domain] :: Interpretation_Type -> Domain
[dimension] :: Interpretation_Type -> Int
[strictDimension] :: Interpretation_Type -> Int
data Interpretation
Interpretation :: Interpretation_Type -> [Interpret] -> Interpretation
[interpretation_type] :: Interpretation -> Interpretation_Type
[interprets] :: Interpretation -> [Interpret]
data RedPair
RPInterpretation :: Interpretation -> RedPair
RPPathOrder :: PathOrder -> RedPair
data OrderingConstraintProof
OCPRedPair :: RedPair -> OrderingConstraintProof
data DepGraphComponent
DepGraphComponent :: Bool -> DPS -> DpProof -> DepGraphComponent
[dgcRealScc] :: DepGraphComponent -> Bool
[dgcDps] :: DepGraphComponent -> DPS
[dgcDpProof] :: DepGraphComponent -> DpProof
data DpProof
PIsEmpty :: DpProof
RedPairProc :: OrderingConstraintProof -> DPS -> Maybe DPS -> DpProof -> DpProof
[rppOrderingConstraintProof] :: DpProof -> OrderingConstraintProof
[rppDps] :: DpProof -> DPS
[rppUsableRules] :: DpProof -> Maybe DPS
[rppDpProof] :: DpProof -> DpProof
DepGraphProc :: [DepGraphComponent] -> DpProof
SemLabProc :: Model -> DPS -> DPS -> DpProof -> DpProof
[slpModel] :: DpProof -> Model
[slpDps] :: DpProof -> DPS
[slpTrs] :: DpProof -> DPS
[slpDpProof] :: DpProof -> DpProof
UnlabProc :: DPS -> DPS -> DpProof -> DpProof
[ulpDps] :: DpProof -> DPS
[ulpTrs] :: DpProof -> DPS
[ulpDpProof] :: DpProof -> DpProof
data Model
FiniteModel :: Int -> [Interpret] -> Model
data Transition_Lhs
Transition_Symbol :: Symbol -> Int -> [State] -> Transition_Lhs
[tr_symbol] :: Transition_Lhs -> Symbol
[tr_height] :: Transition_Lhs -> Int
[tr_arguments] :: Transition_Lhs -> [State]
Transition_Epsilon :: State -> Transition_Lhs
data Transition
Transition :: Transition_Lhs -> [State] -> Transition
[transition_lhs] :: Transition -> Transition_Lhs
[transition_rhs] :: Transition -> [State]
data State
State :: Int -> State
data TreeAutomaton
TreeAutomaton :: [State] -> [Transition] -> TreeAutomaton
[ta_finalStates] :: TreeAutomaton -> [State]
[ta_transitions] :: TreeAutomaton -> [Transition]
data Criterion
Compatibility :: Criterion
data ClosedTreeAutomaton
ClosedTreeAutomaton :: TreeAutomaton -> Criterion -> ClosedTreeAutomaton
[cta_treeAutomaton] :: ClosedTreeAutomaton -> TreeAutomaton
[cta_criterion] :: ClosedTreeAutomaton -> Criterion
data Bounds_Type
Roof :: Bounds_Type
Match :: Bounds_Type
data TrsTerminationProof
RIsEmpty :: TrsTerminationProof
RuleRemoval :: OrderingConstraintProof -> TRS Identifier Identifier -> TrsTerminationProof -> TrsTerminationProof
[rr_orderingConstraintProof] :: TrsTerminationProof -> OrderingConstraintProof
[trs] :: TrsTerminationProof -> TRS Identifier Identifier
[trsTerminationProof] :: TrsTerminationProof -> TrsTerminationProof
DpTrans :: DPS -> Bool -> DpProof -> TrsTerminationProof
[dptrans_dps] :: TrsTerminationProof -> DPS
[markedSymbols] :: TrsTerminationProof -> Bool
[dptrans_dpProof] :: TrsTerminationProof -> DpProof
Semlab :: Model -> TRS Identifier Identifier -> TrsTerminationProof -> TrsTerminationProof
[model] :: TrsTerminationProof -> Model
[trs] :: TrsTerminationProof -> TRS Identifier Identifier
[trsTerminationProof] :: TrsTerminationProof -> TrsTerminationProof
Unlab :: TRS Identifier Identifier -> TrsTerminationProof -> TrsTerminationProof
[trs] :: TrsTerminationProof -> TRS Identifier Identifier
[trsTerminationProof] :: TrsTerminationProof -> TrsTerminationProof
StringReversal :: TRS Identifier Identifier -> TrsTerminationProof -> TrsTerminationProof
[trs] :: TrsTerminationProof -> TRS Identifier Identifier
[trsTerminationProof] :: TrsTerminationProof -> TrsTerminationProof
Bounds :: TRS Identifier Identifier -> Bounds_Type -> Int -> [State] -> ClosedTreeAutomaton -> TrsTerminationProof
[trs] :: TrsTerminationProof -> TRS Identifier Identifier
[bounds_type] :: TrsTerminationProof -> Bounds_Type
[bounds_bound] :: TrsTerminationProof -> Int
[bounds_finalStates] :: TrsTerminationProof -> [State]
[bounds_closedTreeAutomaton] :: TrsTerminationProof -> ClosedTreeAutomaton
data TrsNonterminationProof
TrsNonterminationProofFIXME :: () -> TrsNonterminationProof
data ComplexityClass

-- | it seems the degree must always be given in CPF, although the category
--   spec also allows <a>POLY</a>
--   <a>http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/rules.php</a>
ComplexityClassPolynomial :: Int -> ComplexityClass
[degree] :: ComplexityClass -> Int
data ComplexityMeasure
DerivationalComplexity :: ComplexityMeasure
RuntimeComplexity :: ComplexityMeasure
data ComplexityProof
ComplexityProofFIXME :: () -> ComplexityProof
data DPS
DPS :: [Rule (Term Identifier s)] -> DPS
data Proof
TrsTerminationProof :: TrsTerminationProof -> Proof
TrsNonterminationProof :: TrsNonterminationProof -> Proof
RelativeTerminationProof :: TrsTerminationProof -> Proof
RelativeNonterminationProof :: TrsNonterminationProof -> Proof
ComplexityProof :: ComplexityProof -> Proof
ACTerminationProof :: ACTerminationProof -> Proof
data CertificationProblemInput

-- | this is actually not true, since instead of copying from XTC, CPF
--   format repeats the definition of TRS, and it's a different one
--   (relative rules are extra)
TrsInput :: TRS Identifier Identifier -> CertificationProblemInput
[trsinput_trs] :: CertificationProblemInput -> TRS Identifier Identifier
ComplexityInput :: TRS Identifier Identifier -> ComplexityMeasure -> ComplexityClass -> CertificationProblemInput
[trsinput_trs] :: CertificationProblemInput -> TRS Identifier Identifier
[complexityMeasure] :: CertificationProblemInput -> ComplexityMeasure
[complexityClass] :: CertificationProblemInput -> ComplexityClass
ACRewriteSystem :: TRS Identifier Identifier -> [Identifier] -> [Identifier] -> CertificationProblemInput
[trsinput_trs] :: CertificationProblemInput -> TRS Identifier Identifier
[asymbols] :: CertificationProblemInput -> [Identifier]
[csymbols] :: CertificationProblemInput -> [Identifier]
data Tool
Tool :: Text -> Text -> Tool
[name] :: Tool -> Text
[version] :: Tool -> Text
data Origin
ProofOrigin :: Tool -> Origin
[tool] :: Origin -> Tool
data CertificationProblem
CertificationProblem :: CertificationProblemInput -> Text -> Proof -> Origin -> CertificationProblem
[input] :: CertificationProblem -> CertificationProblemInput
[cpfVersion] :: CertificationProblem -> Text
[proof] :: CertificationProblem -> Proof
[origin] :: CertificationProblem -> Origin
ignoredOrigin :: Origin
data Identifier

-- | legacy stuff (used in matchbox)
type TES = TRS Identifier Identifier
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.Tool
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.Origin
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.ComplexityProof
instance GHC.Show.Show TPDB.CPF.Proof.Type.ComplexityMeasure
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.ComplexityMeasure
instance GHC.Show.Show TPDB.CPF.Proof.Type.ComplexityClass
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.ComplexityClass
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.CertificationProblemInput
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.TrsNonterminationProof
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.Bounds_Type
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.Criterion
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.State
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.Domain
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.Interpretation_Type
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.ArithFunction
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.Symbol
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.Label
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.Transition_Lhs
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.Transition
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.TreeAutomaton
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.ClosedTreeAutomaton
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.Polynomial
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.Value
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.Interpret
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.Interpretation
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.Model
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.Exotic
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.PrecedenceEntry
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.ArgumentFilterEntry
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.PathOrder
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.RedPair
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.OrderingConstraintProof
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.DepGraphComponent
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.DpProof
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.TrsTerminationProof
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.ACTerminationProof
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.Proof
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.CertificationProblem
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.Coefficient
instance Prettyprinter.Internal.Pretty TPDB.CPF.Proof.Type.CertificationProblemInput
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.DPS


-- | from internal representation to XML, and back
module TPDB.CPF.Proof.Write
tox :: CertificationProblem -> Document
symbolize :: Functor f => RS Identifier (f Identifier) -> RS Symbol (f Symbol)
instance TPDB.Xml.XmlContent TPDB.CPF.Proof.Type.CertificationProblem
instance TPDB.Xml.XmlContent TPDB.CPF.Proof.Type.Origin
instance TPDB.Xml.XmlContent TPDB.CPF.Proof.Type.Tool
instance TPDB.Xml.XmlContent TPDB.CPF.Proof.Type.CertificationProblemInput
instance TPDB.Xml.XmlContent (TPDB.Data.TRS TPDB.Data.Identifier TPDB.CPF.Proof.Type.Symbol)
instance (Data.Typeable.Internal.Typeable t, TPDB.Xml.XmlContent t) => TPDB.Xml.XmlContent (TPDB.Data.Rule.Rule t)
instance TPDB.Xml.XmlContent TPDB.CPF.Proof.Type.Proof
instance TPDB.Xml.XmlContent TPDB.CPF.Proof.Type.DPS
instance TPDB.Xml.XmlContent TPDB.CPF.Proof.Type.TrsTerminationProof
instance TPDB.Xml.XmlContent TPDB.CPF.Proof.Type.Bounds_Type
instance TPDB.Xml.XmlContent TPDB.CPF.Proof.Type.State
instance TPDB.Xml.XmlContent TPDB.CPF.Proof.Type.ClosedTreeAutomaton
instance TPDB.Xml.XmlContent TPDB.CPF.Proof.Type.Criterion
instance TPDB.Xml.XmlContent TPDB.CPF.Proof.Type.TreeAutomaton
instance TPDB.Xml.XmlContent TPDB.CPF.Proof.Type.Transition
instance TPDB.Xml.XmlContent TPDB.CPF.Proof.Type.Transition_Lhs
instance TPDB.Xml.XmlContent TPDB.CPF.Proof.Type.Model
instance TPDB.Xml.XmlContent TPDB.CPF.Proof.Type.DpProof
instance TPDB.Xml.XmlContent TPDB.CPF.Proof.Type.DepGraphComponent
instance TPDB.Xml.XmlContent TPDB.CPF.Proof.Type.OrderingConstraintProof
instance TPDB.Xml.XmlContent TPDB.CPF.Proof.Type.RedPair
instance TPDB.Xml.XmlContent TPDB.CPF.Proof.Type.Interpretation
instance TPDB.Xml.XmlContent TPDB.CPF.Proof.Type.Interpretation_Type
instance TPDB.Xml.XmlContent TPDB.CPF.Proof.Type.Domain
instance TPDB.Xml.XmlContent GHC.Real.Rational
instance TPDB.Xml.XmlContent TPDB.CPF.Proof.Type.Interpret
instance TPDB.Xml.XmlContent TPDB.CPF.Proof.Type.Value
instance TPDB.Xml.XmlContent TPDB.CPF.Proof.Type.Polynomial
instance TPDB.Xml.XmlContent TPDB.CPF.Proof.Type.ArithFunction
instance TPDB.Xml.XmlContent TPDB.CPF.Proof.Type.Coefficient
instance TPDB.Xml.XmlContent TPDB.CPF.Proof.Type.Exotic
instance TPDB.Xml.XmlContent TPDB.CPF.Proof.Type.Symbol
instance TPDB.Xml.XmlContent TPDB.CPF.Proof.Type.Label
instance TPDB.Xml.XmlContent TPDB.CPF.Proof.Type.PathOrder
instance TPDB.Xml.XmlContent TPDB.CPF.Proof.Type.PrecedenceEntry
instance TPDB.Xml.XmlContent TPDB.CPF.Proof.Type.ArgumentFilterEntry

module TPDB.CPF.Proof.Util
fromMarkedIdentifier :: Marked Identifier -> Symbol
sortVariables :: Rule (Term Identifier s) -> Rule (Term Identifier s)

module TPDB.CPF.Proof.Read

-- | dangerous: not all constructor arguments will be set. the function
--   produces something like
--   
--   CertificationProblem { input = CertificationProblemInput , proof =
--   TrsTerminationProof undefined }
readCP :: Text -> Either SomeException [CertificationProblem]
readFile :: FilePath -> IO CertificationProblem
element1 :: Name -> Cursor -> [Cursor]
fromDoc :: Cursor -> [CertificationProblem]
getInput :: Cursor Node -> [CertificationProblemInput]
getTerminationInput :: Cursor Node -> [CertificationProblemInput]
getACTerminationInput :: Cursor -> [CertificationProblemInput]
getSymbol :: Cursor Node -> [Identifier]
getComplexityInput :: Cursor -> [CertificationProblemInput]
getComplexityMeasure :: Cursor -> [ComplexityMeasure]
getComplexityClass :: Cursor Node -> [ComplexityClass]
getTrsInput :: Cursor Node -> [[Rule (Term Identifier Identifier)]]
getRulesWith :: Relation -> Cursor -> [[Rule (Term Identifier Identifier)]]
getRule :: Relation -> Cursor -> [Rule (Term Identifier Identifier)]
getProof :: Cursor -> [Proof]
getDummy :: Name -> b -> Cursor -> [b]
getTerm :: Cursor -> [Term Identifier Identifier]
getVar :: Cursor -> [Term Identifier Identifier]
getFunApp :: Cursor -> [Term Identifier Identifier]

module TPDB.CPF.Proof.Xml