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


-- | Data Type for Rewriting Systems
--   
@package tpdb
@version 0.8.4

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 c, Pretty d) => Pretty (a, b, c, d)


-- | 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.Xml
mkel :: Name -> [Content ()] -> Content ()
rmkel :: Monad m => Name -> [Content ()] -> m (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]

-- | 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 Typeable 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 Typeable Rule
instance Typeable 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 Show Identifier
instance Hashable Identifier

module TPDB.Data.Xml

-- | FIXME: move to separate module
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
data Marked a
Original :: a -> Marked a
Marked :: a -> Marked a
Auxiliary :: a -> Marked a
dp :: Ord a => RS s1 (Term v a) -> RS s (Term v (Marked a))
instance Eq a => Eq (Marked a)
instance Ord a => Ord (Marked a)
instance Pretty a => Pretty (Marked a)
instance Hashable a => Hashable (Marked a)


-- | 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 (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 :: (Monad m, Eq s) => [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.
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)


-- | 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
data Proof
TrsTerminationProof :: TrsTerminationProof -> Proof
data Sharp i
Sharp :: i -> Sharp i
Plain :: i -> Sharp i
data DPS
DPS :: [Rule (Term Identifier s)] -> DPS
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 -> Model
carrierSize :: Model -> Int
data DpProof
PIsEmpty :: DpProof
RedPairProc :: OrderingConstraintProof -> DPS -> DpProof -> DpProof
dp_orderingConstraintProof :: DpProof -> OrderingConstraintProof
red_pair_dps :: DpProof -> DPS
redpairproc_dpProof :: DpProof -> DpProof
data OrderingConstraintProof
RedPair :: Interpretation -> OrderingConstraintProof
interpretation :: OrderingConstraintProof -> Interpretation
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 :: s -> Int -> Value -> Interpret
symbol :: Interpret -> s
arity :: Interpret -> Int
value :: Interpret -> Value
data Value
Polynomial :: Polynomial -> Value
data Polynomial
Sum :: [Polynomial] -> Polynomial
Product :: [Polynomial] -> Polynomial
Polynomial_Coefficient :: Coefficient -> Polynomial
Polynomial_Variable :: String -> Polynomial
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 Identifier

-- | legaca stuff (used in matchbox)
type TES = TRS Identifier Identifier
instance Typeable Tool
instance Typeable Origin
instance Typeable CertificationProblemInput
instance Typeable Sharp
instance Typeable DPS
instance Typeable Model
instance Typeable Domain
instance Typeable Interpretation_Type
instance Typeable Coefficient
instance Typeable Polynomial
instance Typeable Value
instance Typeable Interpret
instance Typeable Interpretation
instance Typeable OrderingConstraintProof
instance Typeable DpProof
instance Typeable TrsTerminationProof
instance Typeable Proof
instance Typeable CertificationProblem
instance Typeable Exotic
instance Eq i => Eq (Sharp i)
instance Ord i => Ord (Sharp i)


-- | internal representation of Rainbow termination proofs, see
--   <a>http://color.loria.fr/</a> this file is modelled after
--   rainbow/proof.ml it omits constructors not needed for matrix
--   interpretations (for the moment)
module TPDB.Rainbow.Proof.Type
data Vector a
Vector :: [a] -> Vector a
data Matrix a
Matrix :: [Vector a] -> Matrix a
data MaxPlus
MinusInfinite :: MaxPlus
MaxPlusFinite :: Integer -> MaxPlus
data MinPlus
MinPlusFinite :: Integer -> MinPlus
PlusInfinite :: MinPlus
data Mi_Fun a
Mi_Fun :: Vector a -> [Matrix a] -> Mi_Fun a
mi_const :: Mi_Fun a -> Vector a
mi_args :: Mi_Fun a -> [Matrix a]
data Poly_Fun a
Poly_Fun :: [a] -> Poly_Fun a
coefficients :: Poly_Fun a -> [a]
type Matrix_Int = Interpretation Mi_Fun
type Polynomial_Int = Interpretation Poly_Fun
data Interpretation f
Interpretation :: Domain -> Integer -> NominalDiffTime -> UTCTime -> UTCTime -> [(k, f a)] -> Interpretation f
mi_domain :: Interpretation f -> Domain
mi_dim :: Interpretation f -> Integer

-- | this is an extension
mi_duration :: Interpretation f -> NominalDiffTime
mi_start :: Interpretation f -> UTCTime
mi_end :: Interpretation f -> UTCTime
mi_int :: Interpretation f -> [(k, f a)]
data Domain
Natural :: Domain
Arctic :: Domain
Arctic_Below_Zero :: Domain
Tropical :: Domain
data Red_Ord
Red_Ord_Matrix_Int :: Matrix_Int -> Red_Ord
Red_Ord_Polynomial_Int :: Polynomial_Int -> Red_Ord
Red_Ord_Simple_Projection :: Simple_Projection -> Red_Ord
Red_Ord_Usable_Rules :: Usable_Rules -> Red_Ord
data Usable_Rules
Usable_Rules :: [Identifier] -> Usable_Rules
data Simple_Projection
Simple_Projection :: [(Identifier, Int)] -> Simple_Projection
data Claim
Claim :: TRS Identifier Identifier -> Property -> Claim
system :: Claim -> TRS Identifier Identifier
property :: Claim -> Property
data Proof
Proof :: Claim -> Reason -> Proof
claim :: Proof -> Claim
reason :: Proof -> Reason
data Property
Termination :: Property
Top_Termination :: Property
Complexity :: (Function, Function) -> Property

-- | see specification:
--   <a>http://termination-portal.org/wiki/Complexity</a>
data Function
Unknown :: Function
Polynomial :: Maybe Int -> Function
degree :: Function -> Maybe Int
Exponential :: Function
data Reason
Trivial :: Reason
MannaNess :: Red_Ord -> Proof -> Reason
MarkSymb :: Proof -> Reason
DP :: Proof -> Reason
Reverse :: Proof -> Reason
As_TRS :: Proof -> Reason
As_SRS :: Proof -> Reason

-- | proposed extension
SCC :: [Proof] -> Reason

-- | experimental (not in Rainbow)
RFC :: Proof -> Reason

-- | experimental (not in Rainbow)
Undo_RFC :: Proof -> Reason

-- | TODO add more info
Bounded_Matrix_Interpretation :: Proof -> Reason
data Over_Graph
HDE :: Over_Graph
HDE_Marked :: Over_Graph
data Marked a
Hd_Mark :: a -> Marked a
Int_Mark :: a -> Marked a
instance Typeable Vector
instance Typeable Matrix
instance Typeable MaxPlus
instance Typeable MinPlus
instance Typeable Mi_Fun
instance Typeable Poly_Fun
instance Typeable Domain
instance Typeable Interpretation
instance Typeable Usable_Rules
instance Typeable Simple_Projection
instance Typeable Red_Ord
instance Typeable Function
instance Typeable Property
instance Typeable Claim
instance Typeable Reason
instance Typeable Proof
instance Typeable Over_Graph
instance Typeable Marked
instance Show MaxPlus
instance Read MaxPlus
instance Show MinPlus
instance Read MinPlus
instance Show Domain
instance Eq Domain
instance Ord Domain
instance Show Over_Graph
instance Eq a => Eq (Marked a)
instance Ord a => Ord (Marked a)
instance ToExotic MinPlus
instance ToExotic MaxPlus
instance ToExotic Integer
instance Pretty Function
instance Show Function
instance Pretty Property
instance Show Property
instance Pretty Simple_Projection
instance Pretty Usable_Rules
instance Pretty UTCTime
instance Pretty NominalDiffTime
instance Pretty Domain


-- | from internal representation to XML, and back
module TPDB.Rainbow.Proof.Xml
tox :: Proof -> Document ()
toplevel :: XmlContent a => a -> Element ()

-- | for some types, e.g. Integer , do not use XmlContent instance for
--   element type but show them (as string). reason: the XmlContent module
--   contains an instance for integer that produces <a>value="42"/</a> and
--   there is no way to turn this off.
data Xml_As_String a
Xml_As_String :: a -> Xml_As_String a

-- | FIXME this is broken because the keys could be Identifier or Marked
--   Identifier
mai :: (Typeable a, XmlContent a, ToExotic a) => String -> Domain -> a -> CParser Matrix_Int
externalize :: [Identifier] -> Rule (Term Identifier Identifier) -> Rule (Term Identifier (Marked Identifier))

-- | super ugly risky: name mangling
unP :: Identifier -> Identifier
instance [incoherent] Typeable Xml_As_String
instance [incoherent] XRead Identifier
instance [incoherent] (Typeable a, XmlContent a) => XRead (Marked a)
instance [incoherent] (Typeable a, XmlContent a) => XmlContent (Marked a)
instance [incoherent] XmlContent Over_Graph
instance [incoherent] XRead Proof
instance [incoherent] XmlContent Proof
instance [incoherent] HTypeable Proof
instance [incoherent] XRead Red_Ord
instance [incoherent] XRead Simple_Projection
instance [incoherent] XmlContent Simple_Projection
instance [incoherent] XmlContent Red_Ord
instance [incoherent] XRead Matrix_Int
instance [incoherent] XmlContent Matrix_Int
instance [incoherent] XmlContent Domain
instance [incoherent] ToExotic a => ToExotic (Xml_As_String a)
instance [incoherent] XRead a => XRead (Mi_Fun a)
instance [incoherent] (Typeable a, XmlContent a) => XmlContent (Mi_Fun a)
instance [incoherent] XRead a => XRead (Matrix a)
instance [incoherent] (Typeable a, XmlContent a) => XmlContent (Matrix a)
instance [incoherent] (Typeable a, Show a, Read a) => XmlContent (Xml_As_String a)
instance [incoherent] XmlContent MaxPlus
instance [incoherent] XRead a => XRead (Vector a)
instance [incoherent] (Typeable a, XmlContent a) => XmlContent (Vector a)


-- | from internal representation to XML, and back
module TPDB.CPF.Proof.Xml
tox :: CertificationProblem -> Document ()
instance [incoherent] XmlContent Exotic
instance [incoherent] XmlContent Coefficient
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 OrderingConstraintProof
instance [incoherent] XmlContent DpProof
instance [incoherent] XmlContent TrsTerminationProof
instance [incoherent] XmlContent DPS
instance [incoherent] (Typeable i, XmlContent i) => XmlContent (Sharp i)
instance [incoherent] XmlContent Proof
instance [incoherent] (Typeable t, XmlContent t) => XmlContent (Rule t)
instance [incoherent] (Typeable v, Typeable c, XmlContent v, XmlContent c) => XmlContent (TRS v c)
instance [incoherent] XmlContent CertificationProblemInput
instance [incoherent] XmlContent Tool
instance [incoherent] XmlContent Origin
instance [incoherent] XmlContent CertificationProblem