Safe Haskell	None
Language	Haskell98

TPDB.CPF.Proof.Type

Description

internal representation of CPF termination proofs, see http://cl-informatik.uibk.ac.at/software/cpf/

Synopsis

data ACTerminationProof = ACTerminationProofFIXME ()
data ArgumentFilterEntry = ArgumentFilterEntry {
- afeSymbol :: Symbol
- afeArity :: Int
- afeFilter :: Either Int [Int]
}
data PrecedenceEntry = PrecedenceEntry {
- peSymbol :: Symbol
- peArity :: Int
- pePrecedence :: Integer
}
data PathOrder = PathOrder [PrecedenceEntry] [ArgumentFilterEntry]
class ToExotic a where
data Exotic
- = Minus_Infinite
- | E_Integer Integer
- | E_Rational Rational
- | Plus_Infinite
data Coefficient
- = Vector [Coefficient]
- | Matrix [Coefficient]
- | (Eq a, XmlContent a) => Coefficient_Coefficient a
data Label
- = LblNumber [Integer]
- | LblSymbol [Symbol]
data Symbol
- = SymName Identifier
- | SymSharp Symbol
- | SymLabel Symbol Label
data ArithFunction
- = AFNatural Integer
- | AFVariable Integer
- | AFSum [ArithFunction]
- | AFProduct [ArithFunction]
- | AFMin [ArithFunction]
- | AFMax [ArithFunction]
- | AFIfEqual ArithFunction ArithFunction ArithFunction ArithFunction
data Polynomial
- = Sum [Polynomial]
- | Product [Polynomial]
- | Polynomial_Coefficient Coefficient
- | Polynomial_Variable Text
data Value
- = Polynomial Polynomial
- | ArithFunction ArithFunction
data Interpret = Interpret {
- symbol :: Symbol
- arity :: Int
- value :: Value
}
data Domain
- = Naturals
- | Rationals Rational
- | Arctic Domain
- | Tropical Domain
data Interpretation_Type = Matrix_Interpretation {
- domain :: Domain
- dimension :: Int
- strictDimension :: Int
}
data Interpretation = Interpretation {
- interpretation_type :: Interpretation_Type
- interprets :: [Interpret]
}
data RedPair
- = RPInterpretation Interpretation
- | RPPathOrder PathOrder
data OrderingConstraintProof = OCPRedPair RedPair
data DepGraphComponent = DepGraphComponent {
- dgcRealScc :: Bool
- dgcDps :: DPS
- dgcDpProof :: DpProof
}
data DpProof
- = PIsEmpty
- | RedPairProc {
  - rppOrderingConstraintProof :: OrderingConstraintProof
  - rppDps :: DPS
  - rppUsableRules :: Maybe DPS
  - rppDpProof :: DpProof
  }
- | DepGraphProc [DepGraphComponent]
- | SemLabProc {
  - slpModel :: Model
  - slpDps :: DPS
  - slpTrs :: DPS
  - slpDpProof :: DpProof
  }
- | UnlabProc {
  - ulpDps :: DPS
  - ulpTrs :: DPS
  - ulpDpProof :: DpProof
  }
data Model = FiniteModel Int [Interpret]
data Transition_Lhs
- = Transition_Symbol {
  - tr_symbol :: Symbol
  - tr_height :: Int
  - tr_arguments :: [State]
  }
- | Transition_Epsilon State
data Transition = Transition {
- transition_lhs :: Transition_Lhs
- transition_rhs :: [State]
}
data State = State Int
data TreeAutomaton = TreeAutomaton {
- ta_finalStates :: [State]
- ta_transitions :: [Transition]
}
data Criterion = Compatibility
data ClosedTreeAutomaton = ClosedTreeAutomaton {
- cta_treeAutomaton :: TreeAutomaton
- cta_criterion :: Criterion
}
data Bounds_Type
- = Roof
- | Match
data TrsTerminationProof
- = RIsEmpty
- | RuleRemoval {
  }
- | DpTrans {
  - dptrans_dps :: DPS
  - markedSymbols :: Bool
  - dptrans_dpProof :: DpProof
  }
- | Semlab {
  - model :: Model
  - trs :: TRS Identifier Identifier
  - trsTerminationProof :: TrsTerminationProof
  }
- | Unlab {
  - trs :: TRS Identifier Identifier
  - trsTerminationProof :: TrsTerminationProof
  }
- | StringReversal {
  - trs :: TRS Identifier Identifier
  - trsTerminationProof :: TrsTerminationProof
  }
- | Bounds {
  - trs :: TRS Identifier Identifier
  - bounds_type :: Bounds_Type
  - bounds_bound :: Int
  - bounds_finalStates :: [State]
  - bounds_closedTreeAutomaton :: ClosedTreeAutomaton
  }
data TrsNonterminationProof = TrsNonterminationProofFIXME ()
data ComplexityClass = ComplexityClassPolynomial {
- degree :: Int
}
data ComplexityMeasure
- = DerivationalComplexity
- | RuntimeComplexity
data ComplexityProof = ComplexityProofFIXME ()
data DPS = (XmlContent s, Typeable s, Eq s) => DPS [Rule (Term Identifier s)]
data Proof
- = TrsTerminationProof TrsTerminationProof
- | TrsNonterminationProof TrsNonterminationProof
- | RelativeTerminationProof TrsTerminationProof
- | RelativeNonterminationProof TrsNonterminationProof
- | ComplexityProof ComplexityProof
- | ACTerminationProof ACTerminationProof
data CertificationProblemInput
- = TrsInput {
  - trsinput_trs :: TRS Identifier Identifier
  }
- | ComplexityInput {
  }
- | ACRewriteSystem {
  - trsinput_trs :: TRS Identifier Identifier
  - asymbols :: [Identifier]
  - csymbols :: [Identifier]
  }
data Tool = Tool {
- name :: Text
- version :: Text
}
data Origin = ProofOrigin {
- tool :: Tool
}
data CertificationProblem = CertificationProblem {
- input :: CertificationProblemInput
- cpfVersion :: Text
- proof :: Proof
- origin :: Origin
}
ignoredOrigin :: Origin
data Identifier
type TES = TRS Identifier Identifier

Documentation

data ACTerminationProof Source #

Constructors

ACTerminationProofFIXME ()

Instances

Eq ACTerminationProof Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: ACTerminationProof -> ACTerminationProof -> Bool # (/=) :: ACTerminationProof -> ACTerminationProof -> Bool #

data ArgumentFilterEntry Source #

Constructors

ArgumentFilterEntry
Fields afeSymbol :: Symbol afeArity :: Int afeFilter :: Either Int [Int]

Instances

Eq ArgumentFilterEntry Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: ArgumentFilterEntry -> ArgumentFilterEntry -> Bool # (/=) :: ArgumentFilterEntry -> ArgumentFilterEntry -> Bool #
XmlContent ArgumentFilterEntry Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: ArgumentFilterEntry -> [Node] Source # parseContents :: Cursor -> [ArgumentFilterEntry] Source #

data PrecedenceEntry Source #

Constructors

PrecedenceEntry
Fields peSymbol :: Symbol peArity :: Int pePrecedence :: Integer

Instances

Eq PrecedenceEntry Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: PrecedenceEntry -> PrecedenceEntry -> Bool # (/=) :: PrecedenceEntry -> PrecedenceEntry -> Bool #
XmlContent PrecedenceEntry Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: PrecedenceEntry -> [Node] Source # parseContents :: Cursor -> [PrecedenceEntry] Source #

data PathOrder Source #

Constructors

PathOrder [PrecedenceEntry] [ArgumentFilterEntry]

Instances

Eq PathOrder Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: PathOrder -> PathOrder -> Bool # (/=) :: PathOrder -> PathOrder -> Bool #
XmlContent PathOrder Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: PathOrder -> [Node] Source # parseContents :: Cursor -> [PathOrder] Source #

class ToExotic a where Source #

Minimal complete definition

toExotic

Methods

toExotic :: a -> Exotic Source #

data Exotic Source #

Constructors

Minus_Infinite
E_Integer Integer
E_Rational Rational
Plus_Infinite

Instances

Eq Exotic Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: Exotic -> Exotic -> Bool # (/=) :: Exotic -> Exotic -> Bool #
XmlContent Exotic Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: Exotic -> [Node] Source # parseContents :: Cursor -> [Exotic] Source #

data Coefficient Source #

Constructors

Vector [Coefficient]
Matrix [Coefficient]
(Eq a, XmlContent a) => Coefficient_Coefficient a

Instances

Eq Coefficient Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: Coefficient -> Coefficient -> Bool # (/=) :: Coefficient -> Coefficient -> Bool #
XmlContent Coefficient Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: Coefficient -> [Node] Source # parseContents :: Cursor -> [Coefficient] Source #

data Label Source #

Constructors

LblNumber [Integer]
LblSymbol [Symbol]

Instances

Eq Label Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: Label -> Label -> Bool # (/=) :: Label -> Label -> Bool #
XmlContent Label Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: Label -> [Node] Source # parseContents :: Cursor -> [Label] Source #

data Symbol Source #

Constructors

SymName Identifier
SymSharp Symbol
SymLabel Symbol Label

Instances

Eq Symbol Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: Symbol -> Symbol -> Bool # (/=) :: Symbol -> Symbol -> Bool #
XmlContent Symbol Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: Symbol -> [Node] Source # parseContents :: Cursor -> [Symbol] Source #
XmlContent (TRS Identifier Symbol) Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: TRS Identifier Symbol -> [Node] Source # parseContents :: Cursor -> [TRS Identifier Symbol] Source #

data ArithFunction Source #

Constructors

AFNatural Integer
AFVariable Integer
AFSum [ArithFunction]
AFProduct [ArithFunction]
AFMin [ArithFunction]
AFMax [ArithFunction]
AFIfEqual ArithFunction ArithFunction ArithFunction ArithFunction

Instances

Eq ArithFunction Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: ArithFunction -> ArithFunction -> Bool # (/=) :: ArithFunction -> ArithFunction -> Bool #
XmlContent ArithFunction Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: ArithFunction -> [Node] Source # parseContents :: Cursor -> [ArithFunction] Source #

data Polynomial Source #

Constructors

Sum [Polynomial]
Product [Polynomial]
Polynomial_Coefficient Coefficient
Polynomial_Variable Text

Instances

Eq Polynomial Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: Polynomial -> Polynomial -> Bool # (/=) :: Polynomial -> Polynomial -> Bool #
XmlContent Polynomial Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: Polynomial -> [Node] Source # parseContents :: Cursor -> [Polynomial] Source #

data Value Source #

Constructors

Polynomial Polynomial
ArithFunction ArithFunction

Instances

Eq Value Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: Value -> Value -> Bool # (/=) :: Value -> Value -> Bool #
XmlContent Value Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: Value -> [Node] Source # parseContents :: Cursor -> [Value] Source #

data Interpret Source #

Constructors

Interpret
Fields symbol :: Symbol arity :: Int value :: Value

Instances

Eq Interpret Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: Interpret -> Interpret -> Bool # (/=) :: Interpret -> Interpret -> Bool #
XmlContent Interpret Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: Interpret -> [Node] Source # parseContents :: Cursor -> [Interpret] Source #

data Domain Source #

Constructors

Naturals
Rationals Rational
Arctic Domain
Tropical Domain

Instances

Eq Domain Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: Domain -> Domain -> Bool # (/=) :: Domain -> Domain -> Bool #
XmlContent Domain Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: Domain -> [Node] Source # parseContents :: Cursor -> [Domain] Source #

data Interpretation_Type Source #

Constructors

Matrix_Interpretation
Fields domain :: Domain dimension :: Int strictDimension :: Int

Instances

Eq Interpretation_Type Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: Interpretation_Type -> Interpretation_Type -> Bool # (/=) :: Interpretation_Type -> Interpretation_Type -> Bool #
XmlContent Interpretation_Type Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: Interpretation_Type -> [Node] Source # parseContents :: Cursor -> [Interpretation_Type] Source #

data Interpretation Source #

Constructors

Interpretation
Fields interpretation_type :: Interpretation_Type interprets :: [Interpret]

Instances

Eq Interpretation Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: Interpretation -> Interpretation -> Bool # (/=) :: Interpretation -> Interpretation -> Bool #
XmlContent Interpretation Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: Interpretation -> [Node] Source # parseContents :: Cursor -> [Interpretation] Source #

data RedPair Source #

Constructors

RPInterpretation Interpretation
RPPathOrder PathOrder

Instances

Eq RedPair Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: RedPair -> RedPair -> Bool # (/=) :: RedPair -> RedPair -> Bool #
XmlContent RedPair Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: RedPair -> [Node] Source # parseContents :: Cursor -> [RedPair] Source #

data OrderingConstraintProof Source #

Constructors

OCPRedPair RedPair

Instances

Eq OrderingConstraintProof Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: OrderingConstraintProof -> OrderingConstraintProof -> Bool # (/=) :: OrderingConstraintProof -> OrderingConstraintProof -> Bool #
XmlContent OrderingConstraintProof Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: OrderingConstraintProof -> [Node] Source # parseContents :: Cursor -> [OrderingConstraintProof] Source #

data DepGraphComponent Source #

Constructors

DepGraphComponent
Fields dgcRealScc :: Bool dgcDps :: DPS dgcDpProof :: DpProof

Instances

Eq DepGraphComponent Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: DepGraphComponent -> DepGraphComponent -> Bool # (/=) :: DepGraphComponent -> DepGraphComponent -> Bool #
XmlContent DepGraphComponent Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: DepGraphComponent -> [Node] Source # parseContents :: Cursor -> [DepGraphComponent] Source #

data DpProof Source #

Constructors

PIsEmpty
RedPairProc
Fields rppOrderingConstraintProof :: OrderingConstraintProof rppDps :: DPS rppUsableRules :: Maybe DPS rppDpProof :: DpProof
DepGraphProc [DepGraphComponent]
SemLabProc
Fields slpModel :: Model slpDps :: DPS slpTrs :: DPS slpDpProof :: DpProof
UnlabProc
Fields ulpDps :: DPS ulpTrs :: DPS ulpDpProof :: DpProof

Instances

Eq DpProof Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: DpProof -> DpProof -> Bool # (/=) :: DpProof -> DpProof -> Bool #
XmlContent DpProof Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: DpProof -> [Node] Source # parseContents :: Cursor -> [DpProof] Source #

data Model Source #

Constructors

FiniteModel Int [Interpret]

Instances

Eq Model Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: Model -> Model -> Bool # (/=) :: Model -> Model -> Bool #
XmlContent Model Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: Model -> [Node] Source # parseContents :: Cursor -> [Model] Source #

data Transition_Lhs Source #

Constructors

Transition_Symbol
Fields tr_symbol :: Symbol tr_height :: Int tr_arguments :: [State]
Transition_Epsilon State

Instances

Eq Transition_Lhs Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: Transition_Lhs -> Transition_Lhs -> Bool # (/=) :: Transition_Lhs -> Transition_Lhs -> Bool #
XmlContent Transition_Lhs Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: Transition_Lhs -> [Node] Source # parseContents :: Cursor -> [Transition_Lhs] Source #

data Transition Source #

Constructors

Transition
Fields transition_lhs :: Transition_Lhs transition_rhs :: [State]

Instances

Eq Transition Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: Transition -> Transition -> Bool # (/=) :: Transition -> Transition -> Bool #
XmlContent Transition Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: Transition -> [Node] Source # parseContents :: Cursor -> [Transition] Source #

data State Source #

Constructors

State Int

Instances

Eq State Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: State -> State -> Bool # (/=) :: State -> State -> Bool #
XmlContent State Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: State -> [Node] Source # parseContents :: Cursor -> [State] Source #

data TreeAutomaton Source #

Constructors

TreeAutomaton
Fields ta_finalStates :: [State] ta_transitions :: [Transition]

Instances

Eq TreeAutomaton Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: TreeAutomaton -> TreeAutomaton -> Bool # (/=) :: TreeAutomaton -> TreeAutomaton -> Bool #
XmlContent TreeAutomaton Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: TreeAutomaton -> [Node] Source # parseContents :: Cursor -> [TreeAutomaton] Source #

data Criterion Source #

Constructors

Compatibility

Instances

Eq Criterion Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: Criterion -> Criterion -> Bool # (/=) :: Criterion -> Criterion -> Bool #
XmlContent Criterion Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: Criterion -> [Node] Source # parseContents :: Cursor -> [Criterion] Source #

data ClosedTreeAutomaton Source #

Constructors

ClosedTreeAutomaton
Fields cta_treeAutomaton :: TreeAutomaton cta_criterion :: Criterion

Instances

Eq ClosedTreeAutomaton Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: ClosedTreeAutomaton -> ClosedTreeAutomaton -> Bool # (/=) :: ClosedTreeAutomaton -> ClosedTreeAutomaton -> Bool #
XmlContent ClosedTreeAutomaton Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: ClosedTreeAutomaton -> [Node] Source # parseContents :: Cursor -> [ClosedTreeAutomaton] Source #

data Bounds_Type Source #

Constructors

Roof
Match

Instances

Eq Bounds_Type Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: Bounds_Type -> Bounds_Type -> Bool # (/=) :: Bounds_Type -> Bounds_Type -> Bool #
XmlContent Bounds_Type Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: Bounds_Type -> [Node] Source # parseContents :: Cursor -> [Bounds_Type] Source #

data TrsTerminationProof Source #

Constructors

RIsEmpty
RuleRemoval
Fields rr_orderingConstraintProof :: OrderingConstraintProof trs :: TRS Identifier Identifier trsTerminationProof :: TrsTerminationProof
DpTrans
Fields dptrans_dps :: DPS markedSymbols :: Bool dptrans_dpProof :: DpProof
Semlab
Fields model :: Model trs :: TRS Identifier Identifier trsTerminationProof :: TrsTerminationProof
Unlab
Fields trs :: TRS Identifier Identifier trsTerminationProof :: TrsTerminationProof
StringReversal
Fields trs :: TRS Identifier Identifier trsTerminationProof :: TrsTerminationProof
Bounds
Fields trs :: TRS Identifier Identifier bounds_type :: Bounds_Type bounds_bound :: Int bounds_finalStates :: [State] bounds_closedTreeAutomaton :: ClosedTreeAutomaton

Instances

Eq TrsTerminationProof Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: TrsTerminationProof -> TrsTerminationProof -> Bool # (/=) :: TrsTerminationProof -> TrsTerminationProof -> Bool #
XmlContent TrsTerminationProof Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: TrsTerminationProof -> [Node] Source # parseContents :: Cursor -> [TrsTerminationProof] Source #

data TrsNonterminationProof Source #

Constructors

TrsNonterminationProofFIXME ()

Instances

Eq TrsNonterminationProof Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: TrsNonterminationProof -> TrsNonterminationProof -> Bool # (/=) :: TrsNonterminationProof -> TrsNonterminationProof -> Bool #

data ComplexityClass Source #

Constructors

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
Fields degree :: Int

Instances

Eq ComplexityClass Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: ComplexityClass -> ComplexityClass -> Bool # (/=) :: ComplexityClass -> ComplexityClass -> Bool #
Show ComplexityClass Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods showsPrec :: Int -> ComplexityClass -> ShowS # show :: ComplexityClass -> String # showList :: [ComplexityClass] -> ShowS #

data ComplexityMeasure Source #

Constructors

DerivationalComplexity
RuntimeComplexity

Instances

Eq ComplexityMeasure Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: ComplexityMeasure -> ComplexityMeasure -> Bool # (/=) :: ComplexityMeasure -> ComplexityMeasure -> Bool #
Show ComplexityMeasure Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods showsPrec :: Int -> ComplexityMeasure -> ShowS # show :: ComplexityMeasure -> String # showList :: [ComplexityMeasure] -> ShowS #

data ComplexityProof Source #

Constructors

ComplexityProofFIXME ()

Instances

Eq ComplexityProof Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: ComplexityProof -> ComplexityProof -> Bool # (/=) :: ComplexityProof -> ComplexityProof -> Bool #

data DPS Source #

Constructors

(XmlContent s, Typeable s, Eq s) => DPS [Rule (Term Identifier s)]

Instances

Eq DPS Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: DPS -> DPS -> Bool # (/=) :: DPS -> DPS -> Bool #
XmlContent DPS Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: DPS -> [Node] Source # parseContents :: Cursor -> [DPS] Source #

data Proof Source #

Constructors

TrsTerminationProof TrsTerminationProof
TrsNonterminationProof TrsNonterminationProof
RelativeTerminationProof TrsTerminationProof
RelativeNonterminationProof TrsNonterminationProof
ComplexityProof ComplexityProof
ACTerminationProof ACTerminationProof

Instances

Eq Proof Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: Proof -> Proof -> Bool # (/=) :: Proof -> Proof -> Bool #
XmlContent Proof Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: Proof -> [Node] Source # parseContents :: Cursor -> [Proof] Source #

data CertificationProblemInput Source #

Constructors

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)
Fields trsinput_trs :: TRS Identifier Identifier
ComplexityInput
Fields trsinput_trs :: TRS Identifier Identifier complexityMeasure :: ComplexityMeasure complexityClass :: ComplexityClass
ACRewriteSystem
Fields trsinput_trs :: TRS Identifier Identifier asymbols :: [Identifier] csymbols :: [Identifier]

Instances

Eq CertificationProblemInput Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: CertificationProblemInput -> CertificationProblemInput -> Bool # (/=) :: CertificationProblemInput -> CertificationProblemInput -> Bool #
Pretty CertificationProblemInput Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods pretty :: CertificationProblemInput -> Doc ann # prettyList :: [CertificationProblemInput] -> Doc ann #
XmlContent CertificationProblemInput Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: CertificationProblemInput -> [Node] Source # parseContents :: Cursor -> [CertificationProblemInput] Source #

data Tool Source #

Constructors

Tool
Fields name :: Text version :: Text

Instances

Eq Tool Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: Tool -> Tool -> Bool # (/=) :: Tool -> Tool -> Bool #
XmlContent Tool Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: Tool -> [Node] Source # parseContents :: Cursor -> [Tool] Source #

data Origin Source #

Constructors

ProofOrigin
Fields tool :: Tool

Instances

Eq Origin Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: Origin -> Origin -> Bool # (/=) :: Origin -> Origin -> Bool #
XmlContent Origin Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: Origin -> [Node] Source # parseContents :: Cursor -> [Origin] Source #

data CertificationProblem Source #

Constructors

CertificationProblem
Fields input :: CertificationProblemInput cpfVersion :: Text proof :: Proof origin :: Origin

Instances

Eq CertificationProblem Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: CertificationProblem -> CertificationProblem -> Bool # (/=) :: CertificationProblem -> CertificationProblem -> Bool #
XmlContent CertificationProblem Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: CertificationProblem -> [Node] Source # parseContents :: Cursor -> [CertificationProblem] Source #

ignoredOrigin :: Origin Source #

data Identifier Source #

Instances

Eq Identifier Source #
Instance details Defined in TPDB.Data Methods (==) :: Identifier -> Identifier -> Bool # (/=) :: Identifier -> Identifier -> Bool #
Ord Identifier Source #
Instance details Defined in TPDB.Data Methods compare :: Identifier -> Identifier -> Ordering # (<) :: Identifier -> Identifier -> Bool # (<=) :: Identifier -> Identifier -> Bool # (>) :: Identifier -> Identifier -> Bool # (>=) :: Identifier -> Identifier -> Bool # max :: Identifier -> Identifier -> Identifier # min :: Identifier -> Identifier -> Identifier #
Show Identifier Source #
Instance details Defined in TPDB.Data Methods showsPrec :: Int -> Identifier -> ShowS # show :: Identifier -> String # showList :: [Identifier] -> ShowS #
Hashable Identifier Source #
Instance details Defined in TPDB.Data Methods hashWithSalt :: Int -> Identifier -> Int # hash :: Identifier -> Int #
Pretty Identifier #
Instance details Defined in TPDB.Plain.Write Methods pretty :: Identifier -> Doc ann # prettyList :: [Identifier] -> Doc ann #
Reader Identifier Source #
Instance details Defined in TPDB.Plain.Read Methods reader :: Parser Identifier Source #
XmlContent Identifier Source #	FIXME: move to separate module
Instance details Defined in TPDB.Data.Xml Methods toContents :: Identifier -> [Node] Source # parseContents :: Cursor -> [Identifier] Source #
Reader (SRS Identifier) Source #
Instance details Defined in TPDB.Plain.Read Methods reader :: Parser (SRS Identifier) Source #
Reader v => Reader (Term v Identifier) Source #
Instance details Defined in TPDB.Plain.Read Methods reader :: Parser (Term v Identifier) Source #
Reader (TRS Identifier Identifier) Source #
Instance details Defined in TPDB.Plain.Read Methods reader :: Parser (TRS Identifier Identifier) Source #
XmlContent (TRS Identifier Symbol) Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: TRS Identifier Symbol -> [Node] Source # parseContents :: Cursor -> [TRS Identifier Symbol] Source #

type TES = TRS Identifier Identifier Source #

legacy stuff (used in matchbox)