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

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 :: Pretty a => a -> Doc
prettyList :: Pretty a => [a] -> Doc
fsep :: [Doc] -> Doc

-- | The document <tt>(hsep xs)</tt> concatenates all documents <tt>xs</tt>
--   horizontally with <tt>(&lt;+&gt;)</tt>.
hsep :: [Doc] -> Doc

-- | The document <tt>(vsep xs)</tt> concatenates all documents <tt>xs</tt>
--   vertically with <tt>(&lt;$&gt;)</tt>. If a <a>group</a> undoes the
--   line breaks inserted by <tt>vsep</tt>, all documents are separated
--   with a space.
--   
--   <pre>
--   someText = map text (words ("text to lay out"))
--   
--   test = text "some" &lt;+&gt; vsep someText
--   </pre>
--   
--   This is laid out as:
--   
--   <pre>
--   some text
--   to
--   lay
--   out
--   </pre>
--   
--   The <a>align</a> combinator can be used to align the documents under
--   their first element
--   
--   <pre>
--   test = text "some" &lt;+&gt; align (vsep someText)
--   </pre>
--   
--   Which is printed as:
--   
--   <pre>
--   some text
--        to
--        lay
--        out
--   </pre>
vsep :: [Doc] -> Doc
vcat :: [Doc] -> Doc

-- | The document <tt>(hcat xs)</tt> concatenates all documents <tt>xs</tt>
--   horizontally with <tt>(&lt;&gt;)</tt>.
hcat :: [Doc] -> Doc

-- | Document <tt>(parens x)</tt> encloses document <tt>x</tt> in
--   parenthesis, "(" and ")".
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
(<+>) :: Doc -> Doc -> Doc
($$) :: Doc -> Doc -> Doc
instance (Pretty a, Pretty b) => Pretty (Either a b)
instance (Pretty a, Pretty b, Pretty c, Pretty d) => Pretty (a, b, c, d)


-- | original author: Malcolm Wallace, license: LGPL
--   http:<i></i>hackage.haskell.org<i>packages</i>archive<i>HaXml</i>1.23.3<i>doc</i>html/Text-XML-HaXml-Pretty.html
--   
--   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.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 :: 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 [incoherent] (Typeable a, XmlContent a) => XRead a
instance [incoherent] Monad CParser
instance [incoherent] Functor CParser
instance [incoherent] Typeable t => HTypeable t

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

-- | 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 Typeable2 Term
instance (Eq v, Eq s) => Eq (Term v s)
instance (Ord v, Ord s) => Ord (Term v s)
instance (Show v, Show s) => Show (Term v s)
instance Functor (Term v)

module TPDB.Data
data Identifier
Identifier :: Int -> String -> Int -> Identifier
_identifier_hash :: Identifier -> Int
name :: Identifier -> String
arity :: Identifier -> Int
mk :: Int -> String -> Identifier
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
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 -> Maybe Startterm -> Problem v s
type_ :: Problem v s -> Type
trs :: Problem v s -> TRS v s
strategy :: Problem v s -> Maybe Strategy
startterm :: Problem v s -> Maybe Startterm
data Type
Termination :: Type
Complexity :: Type
data Strategy
Full :: Strategy
Innermost :: Strategy
Outermost :: Strategy
data Startterm
Startterm_Constructor_based :: Startterm
Startterm_Full :: Startterm

-- | legaca 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 t -> [Rule r] -> RS s r
instance Typeable Identifier
instance Typeable Relation
instance Typeable1 Rule
instance Typeable2 RS
instance Eq Identifier
instance Ord Identifier
instance Eq Relation
instance Ord Relation
instance Show Relation
instance Eq a => Eq (Rule a)
instance Ord a => Ord (Rule a)
instance Show Type
instance Show Strategy
instance Show Startterm
instance Eq r => Eq (RS s r)
instance Functor Rule
instance Functor (RS s)
instance Show Identifier
instance Hashable Identifier

module TPDB.Data.Xml
no_sharp_name_HACK :: t -> t
sharp_name_HACK :: Monad m => [Content ()] -> m (Content ())
instance (HTypeable (Rule (Term v c)), XmlContent (Term v c)) => XmlContent (Rule (Term v c))
instance HTypeable (Rule (Term v c))
instance (Typeable (Term v c), XmlContent v, XmlContent c) => XmlContent (Term v c)
instance XmlContent Identifier

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 t => t (NTree XNode) [Identifier]
getFuncsym :: ArrowXml t => t (NTree XNode) Identifier
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]

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 Show a => Show (Marked a)
instance Eq a => Eq (Marked a)
instance Ord a => Ord (Marked a)
instance Generic (Marked a)
instance Datatype D1Marked
instance Constructor C1_0Marked
instance Constructor C1_1Marked
instance Constructor C1_2Marked
instance Pretty a => Pretty (Marked a)
instance Hashable a => Hashable (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))
unifies :: (Eq c, Ord v) => Term v c -> Term v c -> Bool
apply :: Ord v => Term v s -> Map v (Term v s) -> Term v 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
--   http:<i></i>cl-informatik.uibk.ac.at<i>users</i>griff<i>publications</i>Sternagel-Thiemann-RTA10.pdf
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 v) => RS s (Term v c) -> Term t c -> StateT Int Identity (Term Int c)


-- | the <a>old</a> 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 (Pretty s, Pretty r) => Pretty (Problem s r)
instance (Pretty s, PrettyTerm r) => Pretty (RS s r)
instance (Pretty v, Pretty s) => PrettyTerm (Term v s)
instance Pretty s => PrettyTerm [s]
instance PrettyTerm a => Pretty (Rule a)
instance (Pretty v, Pretty s) => Pretty (Term v s)
instance Pretty Identifier


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

-- | warning: by definition, {}[] may appear in identifiers
lexer :: GenTokenParser String u 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 String u Identity ()
repair_signature_srs :: Eq s => RS t [s] -> RS s [s]
make_srs :: Eq s => [Declaration [s]] -> SRS s
repair_signature_trs :: Ord s => RS t (Term v s) -> RS s (Term v s)
make_trs :: [Declaration (Term Identifier Identifier)] -> TRS Identifier Identifier
repair_variables :: (Eq s, Monad m) => [s] -> m (Rule (Term t s)) -> m (Rule (Term s s))
instance Reader (TRS Identifier Identifier)
instance Reader (SRS Identifier)
instance Reader u => Reader (Rule u)
instance Reader v => Reader (Term v Identifier)
instance Reader s => Reader [s]
instance Reader Identifier

module TPDB.Input

-- | read input from file with given name. can have extension .srs, .trs,
--   .xml. unknown extension is considered as .xml, because of
--   http:<i></i>starexec.forumotion.com/t60-restore-file-extension-for-renamed-benchmarks
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)

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 t, Ord b) => 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
--   http:<i></i>cl-informatik.uibk.ac.at<i>users</i>griff<i>publications</i>Sternagel-Thiemann-RTA10.pdf
usable :: (Ord v, Ord c) => TRS v c -> Set (Rule (Term v c))
fixpoint :: Eq a => (a -> a) -> a -> a
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
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>
--   http:<i></i>cl-informatik.uibk.ac.at<i>users</i>georg<i>cbr</i>competition/rules.php
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
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

-- | legaca stuff (used in matchbox)
type TES = TRS Identifier Identifier
instance Typeable Tool
instance Typeable Origin
instance Typeable DPS
instance Typeable ComplexityProof
instance Typeable ComplexityMeasure
instance Typeable ComplexityClass
instance Typeable CertificationProblemInput
instance Typeable TrsNonterminationProof
instance Typeable Domain
instance Typeable Interpretation_Type
instance Typeable ArithFunction
instance Typeable Label
instance Typeable Symbol
instance Typeable Coefficient
instance Typeable Polynomial
instance Typeable Value
instance Typeable Interpret
instance Typeable Interpretation
instance Typeable Model
instance Typeable Exotic
instance Typeable PrecedenceEntry
instance Typeable ArgumentFilterEntry
instance Typeable PathOrder
instance Typeable RedPair
instance Typeable OrderingConstraintProof
instance Typeable DpProof
instance Typeable DepGraphComponent
instance Typeable TrsTerminationProof
instance Typeable Proof
instance Typeable CertificationProblem
instance Eq ComplexityClass


-- | 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 [incoherent] XmlContent ArgumentFilterEntry
instance [incoherent] XmlContent PrecedenceEntry
instance [incoherent] XmlContent PathOrder
instance [incoherent] XmlContent Label
instance [incoherent] XmlContent Symbol
instance [incoherent] XmlContent Exotic
instance [incoherent] XmlContent Coefficient
instance [incoherent] XmlContent ArithFunction
instance [incoherent] XmlContent Polynomial
instance [incoherent] XmlContent Value
instance [incoherent] XmlContent Interpret
instance [incoherent] XmlContent Rational
instance [incoherent] XmlContent Domain
instance [incoherent] XmlContent Interpretation_Type
instance [incoherent] XmlContent Interpretation
instance [incoherent] XmlContent RedPair
instance [incoherent] XmlContent OrderingConstraintProof
instance [incoherent] XmlContent DepGraphComponent
instance [incoherent] XmlContent DpProof
instance [incoherent] XmlContent Model
instance [incoherent] XmlContent TrsTerminationProof
instance [incoherent] XmlContent DPS
instance [incoherent] XmlContent Proof
instance [incoherent] (Typeable t, XmlContent t) => XmlContent (Rule t)
instance [incoherent] XmlContent (TRS Identifier Symbol)
instance [incoherent] XmlContent CertificationProblemInput
instance [incoherent] XmlContent Tool
instance [incoherent] XmlContent Origin
instance [incoherent] XmlContent CertificationProblem

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]
getCP :: ArrowXml cat => cat (NTree XNode) CertificationProblem
getInput :: ArrowXml a => a (NTree XNode) CertificationProblemInput
getTerminationInput :: ArrowXml cat => cat (NTree XNode) CertificationProblemInput
getComplexityInput :: ArrowXml cat => cat (NTree XNode) 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 cat => String -> c -> cat (NTree XNode) c
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
atTag :: ArrowXml a => String -> a (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)