Safe Haskell | None |
---|---|
Language | Haskell98 |
internal representation of CPF termination proofs, see http://cl-informatik.uibk.ac.at/software/cpf/
- data CertificationProblem = CertificationProblem {}
- data Origin = ProofOrigin {}
- ignoredOrigin :: Origin
- data Tool = Tool {}
- data CertificationProblemInput
- data Proof
- data DPS = (XmlContent s, Typeable s, Eq s) => DPS [Rule (Term Identifier s)]
- data ComplexityProof = ComplexityProofFIXME ()
- data ComplexityMeasure
- data ComplexityClass = ComplexityClassPolynomial {}
- data TrsNonterminationProof = TrsNonterminationProofFIXME ()
- data TrsTerminationProof
- = RIsEmpty
- | RuleRemoval { }
- | DpTrans { }
- | Semlab { }
- | Unlab { }
- | StringReversal { }
- | Bounds { }
- data Bounds_Type
- data ClosedTreeAutomaton = ClosedTreeAutomaton {}
- data Criterion = Compatibility
- data TreeAutomaton = TreeAutomaton {
- ta_finalStates :: [State]
- ta_transitions :: [Transition]
- data State = State Int
- data Transition = Transition {}
- data Transition_Lhs
- data Model = FiniteModel Int [Interpret]
- data DpProof
- = PIsEmpty
- | RedPairProc { }
- | DepGraphProc [DepGraphComponent]
- | SemLabProc { }
- | UnlabProc { }
- data DepGraphComponent = DepGraphComponent {
- dgcRealScc :: Bool
- dgcDps :: DPS
- dgcDpProof :: DpProof
- data OrderingConstraintProof = OCPRedPair RedPair
- data RedPair
- data Interpretation = Interpretation {}
- data Interpretation_Type = Matrix_Interpretation {}
- data Domain
- data Interpret = Interpret {}
- data Value
- data Polynomial
- data ArithFunction
- data Symbol
- data Label
- data Coefficient
- = Vector [Coefficient]
- | Matrix [Coefficient]
- | (Eq a, XmlContent a) => Coefficient_Coefficient a
- data Exotic
- class ToExotic a where
- data PathOrder = PathOrder [PrecedenceEntry] [ArgumentFilterEntry]
- data PrecedenceEntry = PrecedenceEntry {}
- data ArgumentFilterEntry = ArgumentFilterEntry {}
- data Identifier
- type TES = TRS Identifier Identifier
Documentation
data CertificationProblem Source #
data CertificationProblemInput Source #
TrsInput | 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) |
ComplexityInput | |
data ComplexityMeasure Source #
data ComplexityClass Source #
ComplexityClassPolynomial | it seems the degree must always be given in CPF, although the category spec also allows POLY http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/rules.php |
data TrsTerminationProof Source #
data ClosedTreeAutomaton Source #
data TreeAutomaton Source #
TreeAutomaton | |
|
data Transition Source #
data DepGraphComponent Source #
DepGraphComponent | |
|
data Interpretation Source #
data Interpretation_Type Source #
data Polynomial Source #
data ArithFunction Source #
data Coefficient Source #
Vector [Coefficient] | |
Matrix [Coefficient] | |
(Eq a, XmlContent a) => Coefficient_Coefficient a |
data ArgumentFilterEntry Source #
data Identifier Source #
type TES = TRS Identifier Identifier Source #
legacy stuff (used in matchbox)