-- 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 1.5.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.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.Show.Show TPDB.Data.Rule.Relation
instance GHC.Classes.Ord TPDB.Data.Rule.Relation
instance GHC.Classes.Eq TPDB.Data.Rule.Relation
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 s, GHC.Show.Show v) => GHC.Show.Show (TPDB.Data.Term.Term v s)
instance (GHC.Classes.Ord s, GHC.Classes.Ord v) => GHC.Classes.Ord (TPDB.Data.Term.Term v s)
instance (GHC.Classes.Eq s, GHC.Classes.Eq v) => 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 ann -> SimpleDocStream ann
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 indentation level 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 <a>hang</a>, <a>align</a> and <a>indent</a>.
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
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> with
--   <tt>i</tt> spaces, 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 indentation level 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 <a>hang</a>, <a>align</a> and <a>indent</a>.
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 (Data.Text.Prettyprint.Doc.Internal.Pretty a, Data.Text.Prettyprint.Doc.Internal.Pretty b, Data.Text.Prettyprint.Doc.Internal.Pretty c, Data.Text.Prettyprint.Doc.Internal.Pretty d) => Data.Text.Prettyprint.Doc.Internal.Pretty (a, b, c, d)
instance (Data.Text.Prettyprint.Doc.Internal.Pretty a, Data.Text.Prettyprint.Doc.Internal.Pretty b) => Data.Text.Prettyprint.Doc.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 Data.Text.Prettyprint.Doc.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
data Identifier
Identifier :: !Int -> !String -> Int -> Identifier
[_identifier_hash] :: Identifier -> !Int
[name] :: Identifier -> !String
[arity] :: Identifier -> Int
mk :: Int -> String -> Identifier

-- | according to XTC spec
data Funcsym
Funcsym :: String -> Int -> Maybe Theory -> Maybe Replacementmap -> Funcsym

-- | should be Text
[fs_name] :: Funcsym -> String
[fs_arity] :: Funcsym -> Int
[fs_theory] :: Funcsym -> Maybe Theory
[fs_replacementmap] :: Funcsym -> Maybe Replacementmap
data Signature
Signature :: [Funcsym] -> Signature
HigherOrderSignature :: Signature
data Replacementmap
Replacementmap :: [Int] -> Replacementmap
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
strict_rules :: () => RS s b -> [(b, b)]
weak_rules :: () => RS s b -> [(b, b)]
equal_rules :: () => RS s b -> [(b, b)]
type TRS v s = RS s (Term v s)
type SRS s = RS s [s]
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
data Type
Termination :: Type
Complexity :: Type
data Strategy
Full :: Strategy
Innermost :: Strategy
Outermost :: Strategy

-- | 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 Theory
A :: Theory
C :: Theory
AC :: Theory
data Startterm
Startterm_Constructor_based :: Startterm
Startterm_Full :: Startterm

-- | legacy stuff (used in matchbox)
type TES = TRS Identifier Identifier
type SES = SRS Identifier
mknullary :: String -> Identifier
mkunary :: String -> Identifier
from_strict_rules :: Bool -> [(t, t)] -> RS i t
with_rules :: () => RS s r1 -> [Rule r2] -> RS s r2
instance GHC.Show.Show TPDB.Data.Startterm
instance GHC.Show.Show TPDB.Data.Signature
instance GHC.Show.Show TPDB.Data.Funcsym
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.Strategy
instance GHC.Show.Show TPDB.Data.Type
instance GHC.Show.Show TPDB.Data.Replacementmap
instance GHC.Classes.Ord TPDB.Data.Identifier
instance GHC.Classes.Eq TPDB.Data.Identifier
instance GHC.Classes.Eq r => GHC.Classes.Eq (TPDB.Data.RS s r)
instance GHC.Base.Functor (TPDB.Data.RS s)
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 => Data.Text.Prettyprint.Doc.Internal.Pretty (TPDB.Data.Rule.Rule a)
instance Data.Text.Prettyprint.Doc.Internal.Pretty s => TPDB.Plain.Write.PrettyTerm [s]
instance (Data.Text.Prettyprint.Doc.Internal.Pretty v, Data.Text.Prettyprint.Doc.Internal.Pretty s) => TPDB.Plain.Write.PrettyTerm (TPDB.Data.Term.Term v s)
instance (Data.Text.Prettyprint.Doc.Internal.Pretty s, TPDB.Plain.Write.PrettyTerm r) => Data.Text.Prettyprint.Doc.Internal.Pretty (TPDB.Data.RS s r)
instance Data.Text.Prettyprint.Doc.Internal.Pretty TPDB.Data.Identifier
instance (Data.Text.Prettyprint.Doc.Internal.Pretty v, Data.Text.Prettyprint.Doc.Internal.Pretty s) => Data.Text.Prettyprint.Doc.Internal.Pretty (TPDB.Data.Term.Term v s)
instance (Data.Text.Prettyprint.Doc.Internal.Pretty s, Data.Text.Prettyprint.Doc.Internal.Pretty r) => Data.Text.Prettyprint.Doc.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 :: ByteString -> Either String (TRS Identifier Identifier)
srs :: ByteString -> Either String (SRS Identifier)
class Reader a
reader :: Reader a => Parser a

-- | warning: by definition, {}[] may appear in identifiers
lexer :: GenTokenParser ByteString () 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 ByteString () 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 :: (Eq s, Foldable t, Monad m) => 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 :: (Eq c, Ord v) => 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 Data.Text.Prettyprint.Doc.Internal.Pretty a => Data.Text.Prettyprint.Doc.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 :: (Eq c, Ord a) => 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 b, Ord a) => RS Marked a Term b Marked a -> [Either Rule Term b Marked a RS Marked a Term b Marked a]

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

module TPDB.DP


-- | internal representation of CPF termination proofs, see
--   <a>http://cl-informatik.uibk.ac.at/software/cpf/</a>
module TPDB.CPF.Proof.Type
data CertificationProblem
CertificationProblem :: CertificationProblemInput -> String -> Proof -> Origin -> CertificationProblem
[input] :: CertificationProblem -> CertificationProblemInput
[cpfVersion] :: CertificationProblem -> String
[proof] :: CertificationProblem -> Proof
[origin] :: CertificationProblem -> Origin
data Origin
ProofOrigin :: Tool -> Origin
[tool] :: Origin -> Tool
ignoredOrigin :: Origin
data Tool
Tool :: String -> String -> Tool
[name] :: Tool -> String
[version] :: Tool -> String
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 Proof
TrsTerminationProof :: TrsTerminationProof -> Proof
TrsNonterminationProof :: TrsNonterminationProof -> Proof
RelativeTerminationProof :: TrsTerminationProof -> Proof
RelativeNonterminationProof :: TrsNonterminationProof -> Proof
ComplexityProof :: ComplexityProof -> Proof
ACTerminationProof :: ACTerminationProof -> Proof
data DPS
DPS :: [Rule (Term Identifier s)] -> DPS
data ComplexityProof
ComplexityProofFIXME :: () -> ComplexityProof
data ComplexityMeasure
DerivationalComplexity :: ComplexityMeasure
RuntimeComplexity :: ComplexityMeasure
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 TrsNonterminationProof
TrsNonterminationProofFIXME :: () -> TrsNonterminationProof
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 Bounds_Type
Roof :: Bounds_Type
Match :: Bounds_Type
data ClosedTreeAutomaton
ClosedTreeAutomaton :: TreeAutomaton -> Criterion -> ClosedTreeAutomaton
[cta_treeAutomaton] :: ClosedTreeAutomaton -> TreeAutomaton
[cta_criterion] :: ClosedTreeAutomaton -> Criterion
data Criterion
Compatibility :: Criterion
data TreeAutomaton
TreeAutomaton :: [State] -> [Transition] -> TreeAutomaton
[ta_finalStates] :: TreeAutomaton -> [State]
[ta_transitions] :: TreeAutomaton -> [Transition]
data State
State :: Int -> State
data Transition
Transition :: Transition_Lhs -> [State] -> Transition
[transition_lhs] :: Transition -> Transition_Lhs
[transition_rhs] :: Transition -> [State]
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 Model
FiniteModel :: Int -> [Interpret] -> Model
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 DepGraphComponent
DepGraphComponent :: Bool -> DPS -> DpProof -> DepGraphComponent
[dgcRealScc] :: DepGraphComponent -> Bool
[dgcDps] :: DepGraphComponent -> DPS
[dgcDpProof] :: DepGraphComponent -> DpProof
data OrderingConstraintProof
OCPRedPair :: RedPair -> OrderingConstraintProof
data RedPair
RPInterpretation :: Interpretation -> RedPair
RPPathOrder :: PathOrder -> RedPair
data Interpretation
Interpretation :: Interpretation_Type -> [Interpret] -> Interpretation
[interpretation_type] :: Interpretation -> Interpretation_Type
[interprets] :: Interpretation -> [Interpret]
data Interpretation_Type
Matrix_Interpretation :: Domain -> Int -> Int -> Interpretation_Type
[domain] :: Interpretation_Type -> Domain
[dimension] :: Interpretation_Type -> Int
[strictDimension] :: Interpretation_Type -> Int
data Domain
Naturals :: Domain
Rationals :: Rational -> Domain
Arctic :: Domain -> Domain
Tropical :: Domain -> Domain
data Interpret
Interpret :: Symbol -> Int -> Value -> Interpret
[symbol] :: Interpret -> Symbol
[arity] :: Interpret -> Int
[value] :: Interpret -> Value
data Value
Polynomial :: Polynomial -> Value
ArithFunction :: ArithFunction -> Value
data Polynomial
Sum :: [Polynomial] -> Polynomial
Product :: [Polynomial] -> Polynomial
Polynomial_Coefficient :: Coefficient -> Polynomial
Polynomial_Variable :: String -> Polynomial
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 Symbol
SymName :: Identifier -> Symbol
SymSharp :: Symbol -> Symbol
SymLabel :: Symbol -> Label -> Symbol
data Label
LblNumber :: [Integer] -> Label
LblSymbol :: [Symbol] -> Label
data Coefficient
Vector :: [Coefficient] -> Coefficient
Matrix :: [Coefficient] -> Coefficient
Coefficient_Coefficient :: a -> Coefficient
data Exotic
Minus_Infinite :: Exotic
E_Integer :: Integer -> Exotic
E_Rational :: Rational -> Exotic
Plus_Infinite :: Exotic
class ToExotic a
toExotic :: ToExotic a => a -> Exotic
data PathOrder
PathOrder :: [PrecedenceEntry] -> [ArgumentFilterEntry] -> PathOrder
data PrecedenceEntry
PrecedenceEntry :: Symbol -> Int -> Integer -> PrecedenceEntry
[peSymbol] :: PrecedenceEntry -> Symbol
[peArity] :: PrecedenceEntry -> Int
[pePrecedence] :: PrecedenceEntry -> Integer
data ArgumentFilterEntry
ArgumentFilterEntry :: Symbol -> Int -> Either Int [Int] -> ArgumentFilterEntry
[afeSymbol] :: ArgumentFilterEntry -> Symbol
[afeArity] :: ArgumentFilterEntry -> Int
[afeFilter] :: ArgumentFilterEntry -> Either Int [Int]
data ACTerminationProof
ACTerminationProofFIXME :: () -> ACTerminationProof
data Identifier

-- | legacy stuff (used in matchbox)
type TES = TRS Identifier Identifier
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.CertificationProblem
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.Proof
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.ACTerminationProof
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.TrsTerminationProof
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.OrderingConstraintProof
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.RedPair
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.PathOrder
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.ArgumentFilterEntry
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.PrecedenceEntry
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.Exotic
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.Model
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.Interpretation
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.Interpret
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.Value
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.Polynomial
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.ClosedTreeAutomaton
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.TreeAutomaton
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.Transition
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.Transition_Lhs
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.ArithFunction
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.Interpretation_Type
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.Domain
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.State
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.Criterion
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.Bounds_Type
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.TrsNonterminationProof
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.CertificationProblemInput
instance GHC.Show.Show TPDB.CPF.Proof.Type.ComplexityClass
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.ComplexityClass
instance GHC.Show.Show TPDB.CPF.Proof.Type.ComplexityMeasure
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.ComplexityMeasure
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.ComplexityProof
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.Origin
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.Tool
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.Coefficient
instance Data.Text.Prettyprint.Doc.Internal.Pretty TPDB.CPF.Proof.Type.CertificationProblemInput
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.DPS

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


-- | construct data object from XML tree.
module TPDB.XTC.Read
atTag :: ArrowXml a => String -> a NTree XNode XmlTree
getTerm :: ArrowXml a => a XmlTree Term Identifier Identifier
getVar :: ArrowXml t => t XmlTree Term Identifier s
getFunApp :: ArrowXml a => a XmlTree Term Identifier Identifier
gotoChild :: ArrowXml t => String -> t NTree XNode NTree XNode
getChild :: ArrowXml t => String -> t NTree XNode XmlTree
getProblem :: ArrowXml cat => cat NTree XNode Problem Identifier Identifier
getType :: Arrow t => t [Char] Type
getStrategy :: ArrowXml t => t NTree XNode Maybe Strategy
getStartterm :: ArrowXml a => a NTree XNode Startterm
getTRS :: ArrowXml t => t NTree XNode RS Identifier Term Identifier Identifier
getSignature :: ArrowXml a => a NTree XNode Signature
getFOSignature :: ArrowXml t => t NTree XNode Signature
getHOSignature :: Arrow t1 => t1 t2 Signature
getFuncsym :: ArrowXml t => t NTree XNode Funcsym
getRead :: (Read t2, ArrowXml t1) => t1 XmlTree t2
getRules :: ArrowXml t => Relation -> t NTree XNode [Rule Term Identifier Identifier]
getRule :: ArrowXml t => Relation -> t NTree XNode Rule Term Identifier Identifier
readProblems :: FilePath -> IO [Problem Identifier Identifier]
readProblemsBS :: ByteString -> IO [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 -> ByteString -> 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
mkel :: Name -> [Content ()] -> Content ()
rmkel :: Monad m => Name -> [Content ()] -> m Content ()
nospaceString :: String -> Content ()
escape :: [Char] -> [Char]
type Contents = [Content Posn]
data CParser a
CParser :: (Contents -> Maybe (a, Contents)) -> CParser a
[unCParser] :: CParser a -> Contents -> Maybe (a, Contents)
must_succeed :: CParser a -> CParser a
class Typeable a => XRead a
xread :: XRead a => CParser a
wrap :: forall a. Typeable a => CParser a -> Parser (Content Posn) a
errmsg :: () => [Content i] -> String
orelse :: CParser a -> CParser a -> CParser a
many :: CParser a -> CParser [a]
element :: () => Name -> CParser a -> CParser a
element0 :: () => QName -> CParser a -> CParser a
strip :: () => [Content i] -> [Content i]
xfromstring :: Read a => CParser a
complain :: String -> CParser a
info :: Contents -> String
instance (Data.Typeable.Internal.Typeable a, Text.XML.HaXml.XmlContent.Parser.XmlContent a) => TPDB.Xml.XRead a
instance GHC.Base.Functor TPDB.Xml.CParser
instance GHC.Base.Applicative TPDB.Xml.CParser
instance GHC.Base.Monad TPDB.Xml.CParser
instance Data.Typeable.Internal.Typeable t => Text.XML.HaXml.TypeMapping.HTypeable t

module TPDB.Data.Xml

-- | FIXME: move to separate module
no_sharp_name_HACK :: () => p -> p
sharp_name_HACK :: Monad m => [Content ()] -> m Content ()
instance Text.XML.HaXml.XmlContent.Parser.XmlContent TPDB.Data.Identifier
instance (Data.Typeable.Internal.Typeable (TPDB.Data.Term.Term v c), Text.XML.HaXml.XmlContent.Parser.XmlContent v, Text.XML.HaXml.XmlContent.Parser.XmlContent c) => Text.XML.HaXml.XmlContent.Parser.XmlContent (TPDB.Data.Term.Term v c)
instance Text.XML.HaXml.TypeMapping.HTypeable (TPDB.Data.Rule.Rule (TPDB.Data.Term.Term v c))
instance (Text.XML.HaXml.TypeMapping.HTypeable (TPDB.Data.Rule.Rule (TPDB.Data.Term.Term v c)), Text.XML.HaXml.XmlContent.Parser.XmlContent (TPDB.Data.Term.Term v c)) => Text.XML.HaXml.XmlContent.Parser.XmlContent (TPDB.Data.Rule.Rule (TPDB.Data.Term.Term v c))


-- | 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 Text.XML.HaXml.XmlContent.Parser.XmlContent TPDB.CPF.Proof.Type.CertificationProblem
instance Text.XML.HaXml.XmlContent.Parser.XmlContent TPDB.CPF.Proof.Type.Origin
instance Text.XML.HaXml.XmlContent.Parser.XmlContent TPDB.CPF.Proof.Type.Tool
instance Text.XML.HaXml.XmlContent.Parser.XmlContent TPDB.CPF.Proof.Type.CertificationProblemInput
instance Text.XML.HaXml.XmlContent.Parser.XmlContent (TPDB.Data.TRS TPDB.Data.Identifier TPDB.CPF.Proof.Type.Symbol)
instance (Data.Typeable.Internal.Typeable t, Text.XML.HaXml.XmlContent.Parser.XmlContent t) => Text.XML.HaXml.XmlContent.Parser.XmlContent (TPDB.Data.Rule.Rule t)
instance Text.XML.HaXml.XmlContent.Parser.XmlContent TPDB.CPF.Proof.Type.Proof
instance Text.XML.HaXml.XmlContent.Parser.XmlContent TPDB.CPF.Proof.Type.DPS
instance Text.XML.HaXml.XmlContent.Parser.XmlContent TPDB.CPF.Proof.Type.TrsTerminationProof
instance Text.XML.HaXml.XmlContent.Parser.XmlContent TPDB.CPF.Proof.Type.Bounds_Type
instance Text.XML.HaXml.XmlContent.Parser.XmlContent TPDB.CPF.Proof.Type.State
instance Text.XML.HaXml.XmlContent.Parser.XmlContent TPDB.CPF.Proof.Type.ClosedTreeAutomaton
instance Text.XML.HaXml.XmlContent.Parser.XmlContent TPDB.CPF.Proof.Type.Criterion
instance Text.XML.HaXml.XmlContent.Parser.XmlContent TPDB.CPF.Proof.Type.TreeAutomaton
instance Text.XML.HaXml.XmlContent.Parser.XmlContent TPDB.CPF.Proof.Type.Transition
instance Text.XML.HaXml.XmlContent.Parser.XmlContent TPDB.CPF.Proof.Type.Transition_Lhs
instance Text.XML.HaXml.XmlContent.Parser.XmlContent TPDB.CPF.Proof.Type.Model
instance Text.XML.HaXml.XmlContent.Parser.XmlContent TPDB.CPF.Proof.Type.DpProof
instance Text.XML.HaXml.XmlContent.Parser.XmlContent TPDB.CPF.Proof.Type.DepGraphComponent
instance Text.XML.HaXml.XmlContent.Parser.XmlContent TPDB.CPF.Proof.Type.OrderingConstraintProof
instance Text.XML.HaXml.XmlContent.Parser.XmlContent TPDB.CPF.Proof.Type.RedPair
instance Text.XML.HaXml.XmlContent.Parser.XmlContent TPDB.CPF.Proof.Type.Interpretation
instance Text.XML.HaXml.XmlContent.Parser.XmlContent TPDB.CPF.Proof.Type.Interpretation_Type
instance Text.XML.HaXml.XmlContent.Parser.XmlContent TPDB.CPF.Proof.Type.Domain
instance Text.XML.HaXml.XmlContent.Parser.XmlContent GHC.Real.Rational
instance Text.XML.HaXml.XmlContent.Parser.XmlContent TPDB.CPF.Proof.Type.Interpret
instance Text.XML.HaXml.XmlContent.Parser.XmlContent TPDB.CPF.Proof.Type.Value
instance Text.XML.HaXml.XmlContent.Parser.XmlContent TPDB.CPF.Proof.Type.Polynomial
instance Text.XML.HaXml.XmlContent.Parser.XmlContent TPDB.CPF.Proof.Type.ArithFunction
instance Text.XML.HaXml.XmlContent.Parser.XmlContent TPDB.CPF.Proof.Type.Coefficient
instance Text.XML.HaXml.XmlContent.Parser.XmlContent TPDB.CPF.Proof.Type.Exotic
instance Text.XML.HaXml.XmlContent.Parser.XmlContent TPDB.CPF.Proof.Type.Symbol
instance Text.XML.HaXml.XmlContent.Parser.XmlContent TPDB.CPF.Proof.Type.Label
instance Text.XML.HaXml.XmlContent.Parser.XmlContent TPDB.CPF.Proof.Type.PathOrder
instance Text.XML.HaXml.XmlContent.Parser.XmlContent TPDB.CPF.Proof.Type.PrecedenceEntry
instance Text.XML.HaXml.XmlContent.Parser.XmlContent TPDB.CPF.Proof.Type.ArgumentFilterEntry

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 :: String -> IO [CertificationProblem]
readCP_with_tracelevel :: Int -> String -> IO [CertificationProblem]
getCP :: ArrowXml cat => cat NTree XNode CertificationProblem
getInput :: ArrowXml a => a XmlTree CertificationProblemInput
getTerminationInput :: ArrowXml cat => cat XmlTree CertificationProblemInput
getACTerminationInput :: ArrowXml cat => cat XmlTree CertificationProblemInput
getSymbol :: ArrowXml t => t NTree XNode Identifier
getComplexityInput :: ArrowXml cat => cat XmlTree CertificationProblemInput
getComplexityMeasure :: ArrowXml a => a NTree XNode ComplexityMeasure
getComplexityClass :: ArrowXml t => t NTree XNode ComplexityClass
getTrsInput :: ArrowXml t => t NTree XNode [Rule Term Identifier Identifier]
getTrs :: ArrowXml t => t NTree XNode [Rule Term Identifier Identifier]
getTrsWith :: ArrowXml t => Relation -> t NTree XNode [Rule Term Identifier Identifier]
getProof :: ArrowXml a => a NTree XNode Proof
getDummy :: ArrowXml t1 => String -> t2 -> t1 NTree XNode t2
getRules :: ArrowXml t => Relation -> t NTree XNode [Rule Term Identifier Identifier]
getRule :: ArrowXml t => Relation -> t NTree XNode Rule Term Identifier Identifier
getTerm :: ArrowXml a => a XmlTree Term Identifier Identifier
getVar :: ArrowXml t => t XmlTree Term Identifier s
getFunApp :: ArrowXml a => a XmlTree Term Identifier Identifier
gotoChild :: ArrowXml t => String -> t NTree XNode NTree XNode
getChild :: ArrowXml t => String -> t NTree XNode XmlTree

module TPDB.CPF.Proof.Xml


-- | original author: Malcolm Wallace, license: LGPL
--   <a>http://hackage.haskell.org/packages/archive/HaXml/1.23.3/doc/html/Text-XML-HaXml-Pretty.html</a>
--   
--   modified by Johannes Waldmann to use a different pretty-printer
--   back-end.
--   
--   This is a pretty-printer for turning the internal representation of
--   generic structured XML documents into the Doc type (which can later be
--   rendered using Text.PrettyPrint.HughesPJ.render). Essentially there is
--   one pp function for each type in Text.Xml.HaXml.Types, so you can
--   pretty-print as much or as little of the document as you wish.
module TPDB.Xml.Pretty
document :: Document i -> Doc
content :: Content i -> Doc
element :: Element i -> Doc
doctypedecl :: DocTypeDecl -> Doc
prolog :: Prolog -> Doc
cp :: CP -> Doc