Safe Haskell | None |
---|---|
Language | Haskell98 |
internal representation of CPF termination proofs, see http://cl-informatik.uibk.ac.at/software/cpf/
Synopsis
- data ACTerminationProof = ACTerminationProofFIXME ()
- data ArgumentFilterEntry = ArgumentFilterEntry {}
- data PrecedenceEntry = PrecedenceEntry {}
- data PathOrder = PathOrder [PrecedenceEntry] [ArgumentFilterEntry]
- class ToExotic a where
- data Exotic
- data Coefficient
- = Vector [Coefficient]
- | Matrix [Coefficient]
- | (Eq a, XmlContent a) => Coefficient_Coefficient a
- data Label
- data Symbol
- data ArithFunction
- data Polynomial
- data Value
- data Interpret = Interpret {}
- data Domain
- data Interpretation_Type = Matrix_Interpretation {}
- data Interpretation = Interpretation {}
- data RedPair
- data OrderingConstraintProof = OCPRedPair RedPair
- data DepGraphComponent = DepGraphComponent {
- dgcRealScc :: Bool
- dgcDps :: DPS
- dgcDpProof :: DpProof
- data DpProof
- = PIsEmpty
- | RedPairProc { }
- | DepGraphProc [DepGraphComponent]
- | SemLabProc { }
- | UnlabProc { }
- data Model = FiniteModel Int [Interpret]
- data Transition_Lhs
- data Transition = Transition {}
- data State = State Int
- data TreeAutomaton = TreeAutomaton {
- ta_finalStates :: [State]
- ta_transitions :: [Transition]
- data Criterion = Compatibility
- data ClosedTreeAutomaton = ClosedTreeAutomaton {}
- data Bounds_Type
- data TrsTerminationProof
- = RIsEmpty
- | RuleRemoval { }
- | DpTrans { }
- | Semlab { }
- | Unlab { }
- | StringReversal { }
- | Bounds { }
- data TrsNonterminationProof = TrsNonterminationProofFIXME ()
- data ComplexityClass = ComplexityClassPolynomial {}
- data ComplexityMeasure
- data ComplexityProof = ComplexityProofFIXME ()
- data DPS = (XmlContent s, Typeable s, Eq s) => DPS [Rule (Term Identifier s)]
- data Proof
- data CertificationProblemInput
- = TrsInput { }
- | ComplexityInput { }
- | ACRewriteSystem {
- trsinput_trs :: TRS Identifier Identifier
- asymbols :: [Identifier]
- csymbols :: [Identifier]
- data Tool = Tool {}
- data Origin = ProofOrigin {}
- data CertificationProblem = CertificationProblem {}
- ignoredOrigin :: Origin
- data Identifier
- type TES = TRS Identifier Identifier
Documentation
data ACTerminationProof Source #
Instances
Eq ACTerminationProof Source # | |
Defined in TPDB.CPF.Proof.Type (==) :: ACTerminationProof -> ACTerminationProof -> Bool # (/=) :: ACTerminationProof -> ACTerminationProof -> Bool # |
data ArgumentFilterEntry Source #
Instances
Eq ArgumentFilterEntry Source # | |
Defined in TPDB.CPF.Proof.Type (==) :: ArgumentFilterEntry -> ArgumentFilterEntry -> Bool # (/=) :: ArgumentFilterEntry -> ArgumentFilterEntry -> Bool # | |
XmlContent ArgumentFilterEntry Source # | |
Defined in TPDB.CPF.Proof.Write toContents :: ArgumentFilterEntry -> [Node] Source # parseContents :: Cursor -> [ArgumentFilterEntry] Source # |
data PrecedenceEntry Source #
Instances
Eq PrecedenceEntry Source # | |
Defined in TPDB.CPF.Proof.Type (==) :: PrecedenceEntry -> PrecedenceEntry -> Bool # (/=) :: PrecedenceEntry -> PrecedenceEntry -> Bool # | |
XmlContent PrecedenceEntry Source # | |
Defined in TPDB.CPF.Proof.Write toContents :: PrecedenceEntry -> [Node] Source # parseContents :: Cursor -> [PrecedenceEntry] Source # |
data Coefficient Source #
Vector [Coefficient] | |
Matrix [Coefficient] | |
(Eq a, XmlContent a) => Coefficient_Coefficient a |
Instances
Eq Coefficient Source # | |
Defined in TPDB.CPF.Proof.Type (==) :: Coefficient -> Coefficient -> Bool # (/=) :: Coefficient -> Coefficient -> Bool # | |
XmlContent Coefficient Source # | |
Defined in TPDB.CPF.Proof.Write toContents :: Coefficient -> [Node] Source # parseContents :: Cursor -> [Coefficient] Source # |
Instances
Eq Symbol Source # | |
XmlContent Symbol Source # | |
Defined in TPDB.CPF.Proof.Write toContents :: Symbol -> [Node] Source # parseContents :: Cursor -> [Symbol] Source # | |
XmlContent (TRS Identifier Symbol) Source # | |
Defined in TPDB.CPF.Proof.Write toContents :: TRS Identifier Symbol -> [Node] Source # parseContents :: Cursor -> [TRS Identifier Symbol] Source # |
data ArithFunction Source #
AFNatural Integer | |
AFVariable Integer | |
AFSum [ArithFunction] | |
AFProduct [ArithFunction] | |
AFMin [ArithFunction] | |
AFMax [ArithFunction] | |
AFIfEqual ArithFunction ArithFunction ArithFunction ArithFunction |
Instances
Eq ArithFunction Source # | |
Defined in TPDB.CPF.Proof.Type (==) :: ArithFunction -> ArithFunction -> Bool # (/=) :: ArithFunction -> ArithFunction -> Bool # | |
XmlContent ArithFunction Source # | |
Defined in TPDB.CPF.Proof.Write toContents :: ArithFunction -> [Node] Source # parseContents :: Cursor -> [ArithFunction] Source # |
data Polynomial Source #
Instances
Eq Polynomial Source # | |
Defined in TPDB.CPF.Proof.Type (==) :: Polynomial -> Polynomial -> Bool # (/=) :: Polynomial -> Polynomial -> Bool # | |
XmlContent Polynomial Source # | |
Defined in TPDB.CPF.Proof.Write toContents :: Polynomial -> [Node] Source # parseContents :: Cursor -> [Polynomial] Source # |
data Interpretation_Type Source #
Instances
Eq Interpretation_Type Source # | |
Defined in TPDB.CPF.Proof.Type (==) :: Interpretation_Type -> Interpretation_Type -> Bool # (/=) :: Interpretation_Type -> Interpretation_Type -> Bool # | |
XmlContent Interpretation_Type Source # | |
Defined in TPDB.CPF.Proof.Write toContents :: Interpretation_Type -> [Node] Source # parseContents :: Cursor -> [Interpretation_Type] Source # |
data Interpretation Source #
Instances
Eq Interpretation Source # | |
Defined in TPDB.CPF.Proof.Type (==) :: Interpretation -> Interpretation -> Bool # (/=) :: Interpretation -> Interpretation -> Bool # | |
XmlContent Interpretation Source # | |
Defined in TPDB.CPF.Proof.Write toContents :: Interpretation -> [Node] Source # parseContents :: Cursor -> [Interpretation] Source # |
data OrderingConstraintProof Source #
Instances
Eq OrderingConstraintProof Source # | |
Defined in TPDB.CPF.Proof.Type | |
XmlContent OrderingConstraintProof Source # | |
Defined in TPDB.CPF.Proof.Write toContents :: OrderingConstraintProof -> [Node] Source # parseContents :: Cursor -> [OrderingConstraintProof] Source # |
data DepGraphComponent Source #
DepGraphComponent | |
|
Instances
Eq DepGraphComponent Source # | |
Defined in TPDB.CPF.Proof.Type (==) :: DepGraphComponent -> DepGraphComponent -> Bool # (/=) :: DepGraphComponent -> DepGraphComponent -> Bool # | |
XmlContent DepGraphComponent Source # | |
Defined in TPDB.CPF.Proof.Write toContents :: DepGraphComponent -> [Node] Source # parseContents :: Cursor -> [DepGraphComponent] Source # |
data Transition_Lhs Source #
Instances
Eq Transition_Lhs Source # | |
Defined in TPDB.CPF.Proof.Type (==) :: Transition_Lhs -> Transition_Lhs -> Bool # (/=) :: Transition_Lhs -> Transition_Lhs -> Bool # | |
XmlContent Transition_Lhs Source # | |
Defined in TPDB.CPF.Proof.Write toContents :: Transition_Lhs -> [Node] Source # parseContents :: Cursor -> [Transition_Lhs] Source # |
data Transition Source #
Instances
Eq Transition Source # | |
Defined in TPDB.CPF.Proof.Type (==) :: Transition -> Transition -> Bool # (/=) :: Transition -> Transition -> Bool # | |
XmlContent Transition Source # | |
Defined in TPDB.CPF.Proof.Write toContents :: Transition -> [Node] Source # parseContents :: Cursor -> [Transition] Source # |
data TreeAutomaton Source #
TreeAutomaton | |
|
Instances
Eq TreeAutomaton Source # | |
Defined in TPDB.CPF.Proof.Type (==) :: TreeAutomaton -> TreeAutomaton -> Bool # (/=) :: TreeAutomaton -> TreeAutomaton -> Bool # | |
XmlContent TreeAutomaton Source # | |
Defined in TPDB.CPF.Proof.Write toContents :: TreeAutomaton -> [Node] Source # parseContents :: Cursor -> [TreeAutomaton] Source # |
data ClosedTreeAutomaton Source #
Instances
Eq ClosedTreeAutomaton Source # | |
Defined in TPDB.CPF.Proof.Type (==) :: ClosedTreeAutomaton -> ClosedTreeAutomaton -> Bool # (/=) :: ClosedTreeAutomaton -> ClosedTreeAutomaton -> Bool # | |
XmlContent ClosedTreeAutomaton Source # | |
Defined in TPDB.CPF.Proof.Write toContents :: ClosedTreeAutomaton -> [Node] Source # parseContents :: Cursor -> [ClosedTreeAutomaton] Source # |
data Bounds_Type Source #
Instances
Eq Bounds_Type Source # | |
Defined in TPDB.CPF.Proof.Type (==) :: Bounds_Type -> Bounds_Type -> Bool # (/=) :: Bounds_Type -> Bounds_Type -> Bool # | |
XmlContent Bounds_Type Source # | |
Defined in TPDB.CPF.Proof.Write toContents :: Bounds_Type -> [Node] Source # parseContents :: Cursor -> [Bounds_Type] Source # |
data TrsTerminationProof Source #
RIsEmpty | |
RuleRemoval | |
DpTrans | |
| |
Semlab | |
Unlab | |
StringReversal | |
Bounds | |
Instances
Eq TrsTerminationProof Source # | |
Defined in TPDB.CPF.Proof.Type (==) :: TrsTerminationProof -> TrsTerminationProof -> Bool # (/=) :: TrsTerminationProof -> TrsTerminationProof -> Bool # | |
XmlContent TrsTerminationProof Source # | |
Defined in TPDB.CPF.Proof.Write toContents :: TrsTerminationProof -> [Node] Source # parseContents :: Cursor -> [TrsTerminationProof] Source # |
data TrsNonterminationProof Source #
Instances
Eq TrsNonterminationProof Source # | |
Defined in TPDB.CPF.Proof.Type |
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 |
Instances
Eq ComplexityClass Source # | |
Defined in TPDB.CPF.Proof.Type (==) :: ComplexityClass -> ComplexityClass -> Bool # (/=) :: ComplexityClass -> ComplexityClass -> Bool # | |
Show ComplexityClass Source # | |
Defined in TPDB.CPF.Proof.Type showsPrec :: Int -> ComplexityClass -> ShowS # show :: ComplexityClass -> String # showList :: [ComplexityClass] -> ShowS # |
data ComplexityMeasure Source #
Instances
Eq ComplexityMeasure Source # | |
Defined in TPDB.CPF.Proof.Type (==) :: ComplexityMeasure -> ComplexityMeasure -> Bool # (/=) :: ComplexityMeasure -> ComplexityMeasure -> Bool # | |
Show ComplexityMeasure Source # | |
Defined in TPDB.CPF.Proof.Type showsPrec :: Int -> ComplexityMeasure -> ShowS # show :: ComplexityMeasure -> String # showList :: [ComplexityMeasure] -> ShowS # |
data ComplexityProof Source #
Instances
Eq ComplexityProof Source # | |
Defined in TPDB.CPF.Proof.Type (==) :: ComplexityProof -> ComplexityProof -> Bool # (/=) :: ComplexityProof -> ComplexityProof -> Bool # |
(XmlContent s, Typeable s, Eq s) => DPS [Rule (Term Identifier s)] |
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 | |
ACRewriteSystem | |
|
Instances
Eq CertificationProblemInput Source # | |
Defined in TPDB.CPF.Proof.Type | |
Pretty CertificationProblemInput Source # | |
Defined in TPDB.CPF.Proof.Type pretty :: CertificationProblemInput -> Doc ann # prettyList :: [CertificationProblemInput] -> Doc ann # | |
XmlContent CertificationProblemInput Source # | |
Defined in TPDB.CPF.Proof.Write |
data CertificationProblem Source #
CertificationProblem | |
|
Instances
Eq CertificationProblem Source # | |
Defined in TPDB.CPF.Proof.Type (==) :: CertificationProblem -> CertificationProblem -> Bool # (/=) :: CertificationProblem -> CertificationProblem -> Bool # | |
XmlContent CertificationProblem Source # | |
Defined in TPDB.CPF.Proof.Write toContents :: CertificationProblem -> [Node] Source # parseContents :: Cursor -> [CertificationProblem] Source # |
data Identifier Source #
Instances
type TES = TRS Identifier Identifier Source #
legacy stuff (used in matchbox)