-- 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.3.3

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 t] -> [Content t]
xfromstring :: Read a => CParser a
complain :: String -> CParser a
info :: Contents -> String
instance Data.Typeable.Internal.Typeable t => Text.XML.HaXml.TypeMapping.HTypeable t
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 a, Text.XML.HaXml.XmlContent.Parser.XmlContent a) => TPDB.Xml.XRead a

module TPDB.Pretty

-- | The abstract data type <tt>Doc</tt> represents pretty documents.
--   
--   <tt>Doc</tt> is an instance of the <a>Show</a> class. <tt>(show
--   doc)</tt> pretty prints document <tt>doc</tt> with a page width of 100
--   characters and a ribbon width of 40 characters.
--   
--   <pre>
--   show (text "hello" &lt;$&gt; text "world")
--   </pre>
--   
--   Which would return the string "hello\nworld", i.e.
--   
--   <pre>
--   hello
--   world
--   
--   </pre>
data Doc :: *

-- | The data type <tt>SimpleDoc</tt> represents rendered documents and is
--   used by the display functions.
--   
--   The <tt>Int</tt> in <tt>SText</tt> contains the length of the string.
--   The <tt>Int</tt> in <tt>SLine</tt> contains the indentation for that
--   line. The library provides two default display functions
--   <tt>displayS</tt> and <a>displayIO</a>. You can provide your own
--   display function by writing a function from a <tt>SimpleDoc</tt> to
--   your own output format.
data SimpleDoc :: *
render :: Doc -> String

-- | <tt>(renderCompact x)</tt> renders document <tt>x</tt> without adding
--   any indentation. Since no 'pretty' printing is involved, this renderer
--   is very fast. The resulting output contains fewer characters than a
--   pretty printed version and can be used for output that is read by
--   other programs.
renderCompact :: Doc -> SimpleDoc

-- | <tt>(displayIO handle simpleDoc)</tt> writes <tt>simpleDoc</tt> to the
--   file handle <tt>handle</tt>. This function is used for example by
--   <a>hPutDoc</a>:
--   
--   <pre>
--   hPutDoc handle doc = displayIO handle (renderPretty 0.4 100 doc)
--   </pre>
displayIO :: Handle -> SimpleDoc -> IO ()

-- | The member <tt>prettyList</tt> is only used to define the <tt>instance
--   Pretty a =&gt; Pretty [a]</tt>. In normal circumstances only the
--   <tt>pretty</tt> function is used.
class Pretty a
pretty :: a -> Doc
prettyList :: [a] -> Doc
fsep :: [Doc] -> Doc
sep :: [Doc] -> Doc
hsep :: [Doc] -> Doc
vsep :: [Doc] -> Doc
vcat :: [Doc] -> Doc
hcat :: [Doc] -> Doc
parens :: Doc -> Doc

-- | Document <tt>(brackets x)</tt> encloses document <tt>x</tt> in square
--   brackets, "[" and "]".
brackets :: Doc -> Doc

-- | Document <tt>(angles x)</tt> encloses document <tt>x</tt> in angles,
--   "&lt;" and "&gt;".
angles :: Doc -> Doc

-- | Document <tt>(braces x)</tt> encloses document <tt>x</tt> in braces,
--   "{" and "}".
braces :: Doc -> Doc

-- | The document <tt>(enclose l r x)</tt> encloses document <tt>x</tt>
--   between documents <tt>l</tt> and <tt>r</tt> using <tt>(&lt;&gt;)</tt>.
--   
--   <pre>
--   enclose l r x = l &lt;&gt; x &lt;&gt; r
--   </pre>
enclose :: Doc -> Doc -> Doc -> Doc

-- | <tt>(punctuate p xs)</tt> concatenates all documents in <tt>xs</tt>
--   with document <tt>p</tt> except for the last document.
--   
--   <pre>
--   someText = map text ["words","in","a","tuple"]
--   test = parens (align (cat (punctuate comma someText)))
--   </pre>
--   
--   This is laid out on a page width of 20 as:
--   
--   <pre>
--   (words,in,a,tuple)
--   
--   </pre>
--   
--   But when the page width is 15, it is laid out as:
--   
--   <pre>
--   (words,
--    in,
--    a,
--    tuple)
--   
--   </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 -> [Doc] -> [Doc]

-- | The document <tt>comma</tt> contains a comma, ",".
comma :: Doc

-- | The document <tt>(nest i x)</tt> renders document <tt>x</tt> with the
--   current indentation level increased by <tt>i</tt> (See also
--   <a>hang</a>, <a>align</a> and <a>indent</a>).
--   
--   <pre>
--   nest 2 (text "hello" &lt;$&gt; text "world") &lt;$&gt; text "!"
--   </pre>
--   
--   outputs as:
--   
--   <pre>
--   hello
--     world
--   !
--   
--   </pre>
nest :: Int -> Doc -> Doc

-- | The empty document is, indeed, empty. Although <tt>empty</tt> has no
--   content, it does have a 'height' of 1 and behaves exactly like
--   <tt>(text "")</tt> (and is therefore not a unit of
--   <tt>&lt;$&gt;</tt>).
empty :: Doc
text :: String -> Doc

-- | The document <tt>(x &lt;&gt; y)</tt> concatenates document <tt>x</tt>
--   and document <tt>y</tt>. It is an associative operation having
--   <a>empty</a> as a left and right unit. (infixr 6)
(<>) :: Doc -> Doc -> Doc
infixr 6 <>
(<+>) :: Doc -> Doc -> Doc
($$) :: Doc -> Doc -> Doc
instance (Text.PrettyPrint.Leijen.Text.Pretty a, Text.PrettyPrint.Leijen.Text.Pretty b, Text.PrettyPrint.Leijen.Text.Pretty c, Text.PrettyPrint.Leijen.Text.Pretty d) => Text.PrettyPrint.Leijen.Text.Pretty (a, b, c, d)
instance (Text.PrettyPrint.Leijen.Text.Pretty a, Text.PrettyPrint.Leijen.Text.Pretty b) => Text.PrettyPrint.Leijen.Text.Pretty (Data.Either.Either a b)


-- | 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

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 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.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 t => t -> [t] -> t
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 Text.PrettyPrint.Leijen.Text.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 t -> [(t, t)]
weak_rules :: RS s t -> [(t, t)]
equal_rules :: RS s t -> [(t, t)]
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 r] -> RS s r
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 Data.Hashable.Class.Hashable TPDB.Data.Identifier
instance GHC.Show.Show TPDB.Data.Identifier
instance GHC.Classes.Eq r => GHC.Classes.Eq (TPDB.Data.RS s r)
instance GHC.Base.Functor (TPDB.Data.RS s)

module TPDB.Data.Xml

-- | FIXME: move to separate module
no_sharp_name_HACK :: t -> t
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))

module TPDB.Convert
srs2trs :: SRS Identifier -> TRS 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)


-- | 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) (Maybe 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 t => t t1 Signature
getFuncsym :: ArrowXml t => t (NTree XNode) Funcsym
getRead :: (ArrowXml t1, Read t) => t1 XmlTree t
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]

module TPDB.XTC

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 t -> Bool
isMarked :: Marked t -> Bool
mark_top :: Term v a -> Term v (Marked a)
defined :: Ord a => RS s (Term t 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 Text.PrettyPrint.Leijen.Text.Pretty a => Text.PrettyPrint.Leijen.Text.Pretty (TPDB.DP.Transform.Marked a)

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.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 t c -> StateT Int Identity (Term Int c)


-- | 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
instance Text.PrettyPrint.Leijen.Text.Pretty TPDB.Data.Identifier
instance (Text.PrettyPrint.Leijen.Text.Pretty v, Text.PrettyPrint.Leijen.Text.Pretty s) => Text.PrettyPrint.Leijen.Text.Pretty (TPDB.Data.Term.Term v s)
instance TPDB.Plain.Write.PrettyTerm a => Text.PrettyPrint.Leijen.Text.Pretty (TPDB.Data.Rule.Rule a)
instance Text.PrettyPrint.Leijen.Text.Pretty s => TPDB.Plain.Write.PrettyTerm [s]
instance (Text.PrettyPrint.Leijen.Text.Pretty v, Text.PrettyPrint.Leijen.Text.Pretty s) => TPDB.Plain.Write.PrettyTerm (TPDB.Data.Term.Term v s)
instance (Text.PrettyPrint.Leijen.Text.Pretty s, TPDB.Plain.Write.PrettyTerm r) => Text.PrettyPrint.Leijen.Text.Pretty (TPDB.Data.RS s r)
instance (Text.PrettyPrint.Leijen.Text.Pretty s, Text.PrettyPrint.Leijen.Text.Pretty r) => Text.PrettyPrint.Leijen.Text.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 s => RS s1 [s] -> RS s [s]
make_srs :: Eq s => [Declaration [s]] -> SRS s
repair_signature_trs :: Ord s => RS s1 (Term v s) -> RS s (Term v s)
make_trs :: [Declaration (Term Identifier Identifier)] -> TRS Identifier Identifier
repair_variables :: (Foldable t1, Monad m, Eq s) => t1 s -> m (Rule (Term t 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)


-- | 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.DP.Graph

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

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

module TPDB.DP

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)]


-- | 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
data Proof
TrsTerminationProof :: TrsTerminationProof -> Proof
TrsNonterminationProof :: TrsNonterminationProof -> Proof
RelativeTerminationProof :: TrsTerminationProof -> Proof
RelativeNonterminationProof :: TrsNonterminationProof -> Proof
ComplexityProof :: ComplexityProof -> 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 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.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.Classes.Eq TPDB.CPF.Proof.Type.ComplexityClass
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.DPS
instance GHC.Classes.Eq TPDB.CPF.Proof.Type.Coefficient


-- | 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
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 -> t -> t1 (NTree XNode) t
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

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