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

Documentation

data CertificationProblem Source #

Constructors

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

Instances

Eq CertificationProblem Source #
Methods (==) :: CertificationProblem -> CertificationProblem -> Bool # (/=) :: CertificationProblem -> CertificationProblem -> Bool #

data Origin Source #

Constructors

ProofOrigin
Fields tool :: Tool

Instances

Eq Origin Source #
Methods (==) :: Origin -> Origin -> Bool # (/=) :: Origin -> Origin -> Bool #

ignoredOrigin :: Origin Source #

data Tool Source #

Constructors

Tool
Fields name :: Text version :: Text

Instances

Eq Tool Source #
Methods (==) :: Tool -> Tool -> Bool # (/=) :: Tool -> Tool -> Bool #

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 #
Methods (==) :: CertificationProblemInput -> CertificationProblemInput -> Bool # (/=) :: CertificationProblemInput -> CertificationProblemInput -> Bool #
Pretty CertificationProblemInput Source #
Methods pretty :: CertificationProblemInput -> Doc ann # prettyList :: [CertificationProblemInput] -> Doc ann #

data Proof Source #

Constructors

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

Instances

Eq Proof Source #
Methods (==) :: Proof -> Proof -> Bool # (/=) :: Proof -> Proof -> Bool #

data DPS Source #

Constructors

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

Instances

Eq DPS Source #
Methods (==) :: DPS -> DPS -> Bool # (/=) :: DPS -> DPS -> Bool #

data ComplexityProof Source #

Constructors

ComplexityProofFIXME ()

Instances

Eq ComplexityProof Source #
Methods (==) :: ComplexityProof -> ComplexityProof -> Bool # (/=) :: ComplexityProof -> ComplexityProof -> Bool #

data ComplexityMeasure Source #

Constructors

DerivationalComplexity
RuntimeComplexity

Instances

Eq ComplexityMeasure Source #
Methods (==) :: ComplexityMeasure -> ComplexityMeasure -> Bool # (/=) :: ComplexityMeasure -> ComplexityMeasure -> Bool #
Show ComplexityMeasure Source #
Methods showsPrec :: Int -> ComplexityMeasure -> ShowS # show :: ComplexityMeasure -> String # showList :: [ComplexityMeasure] -> ShowS #

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 #
Methods (==) :: ComplexityClass -> ComplexityClass -> Bool # (/=) :: ComplexityClass -> ComplexityClass -> Bool #
Show ComplexityClass Source #
Methods showsPrec :: Int -> ComplexityClass -> ShowS # show :: ComplexityClass -> String # showList :: [ComplexityClass] -> ShowS #

data TrsNonterminationProof Source #

Constructors

TrsNonterminationProofFIXME ()

Instances

Eq TrsNonterminationProof Source #
Methods (==) :: TrsNonterminationProof -> TrsNonterminationProof -> Bool # (/=) :: TrsNonterminationProof -> TrsNonterminationProof -> Bool #

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 #
Methods (==) :: TrsTerminationProof -> TrsTerminationProof -> Bool # (/=) :: TrsTerminationProof -> TrsTerminationProof -> Bool #

data Bounds_Type Source #

Constructors

Roof
Match

Instances

Eq Bounds_Type Source #
Methods (==) :: Bounds_Type -> Bounds_Type -> Bool # (/=) :: Bounds_Type -> Bounds_Type -> Bool #

data ClosedTreeAutomaton Source #

Constructors

ClosedTreeAutomaton
Fields cta_treeAutomaton :: TreeAutomaton cta_criterion :: Criterion

Instances

Eq ClosedTreeAutomaton Source #
Methods (==) :: ClosedTreeAutomaton -> ClosedTreeAutomaton -> Bool # (/=) :: ClosedTreeAutomaton -> ClosedTreeAutomaton -> Bool #

data Criterion Source #

Constructors

Compatibility

Instances

Eq Criterion Source #
Methods (==) :: Criterion -> Criterion -> Bool # (/=) :: Criterion -> Criterion -> Bool #

data TreeAutomaton Source #

Constructors

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

Instances

Eq TreeAutomaton Source #
Methods (==) :: TreeAutomaton -> TreeAutomaton -> Bool # (/=) :: TreeAutomaton -> TreeAutomaton -> Bool #

data State Source #

Constructors

State Int

Instances

Eq State Source #
Methods (==) :: State -> State -> Bool # (/=) :: State -> State -> Bool #

data Transition Source #

Constructors

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

Instances

Eq Transition Source #
Methods (==) :: Transition -> Transition -> Bool # (/=) :: Transition -> Transition -> Bool #

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 #
Methods (==) :: Transition_Lhs -> Transition_Lhs -> Bool # (/=) :: Transition_Lhs -> Transition_Lhs -> Bool #

data Model Source #

Constructors

FiniteModel Int [Interpret]

Instances

Eq Model Source #
Methods (==) :: Model -> Model -> Bool # (/=) :: Model -> Model -> Bool #

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 #
Methods (==) :: DpProof -> DpProof -> Bool # (/=) :: DpProof -> DpProof -> Bool #

data DepGraphComponent Source #

Constructors

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

Instances

Eq DepGraphComponent Source #
Methods (==) :: DepGraphComponent -> DepGraphComponent -> Bool # (/=) :: DepGraphComponent -> DepGraphComponent -> Bool #

data OrderingConstraintProof Source #

Constructors

OCPRedPair RedPair

Instances

Eq OrderingConstraintProof Source #
Methods (==) :: OrderingConstraintProof -> OrderingConstraintProof -> Bool # (/=) :: OrderingConstraintProof -> OrderingConstraintProof -> Bool #

data RedPair Source #

Constructors

RPInterpretation Interpretation
RPPathOrder PathOrder

Instances

Eq RedPair Source #
Methods (==) :: RedPair -> RedPair -> Bool # (/=) :: RedPair -> RedPair -> Bool #

data Interpretation Source #

Constructors

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

Instances

Eq Interpretation Source #
Methods (==) :: Interpretation -> Interpretation -> Bool # (/=) :: Interpretation -> Interpretation -> Bool #

data Interpretation_Type Source #

Constructors

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

Instances

Eq Interpretation_Type Source #
Methods (==) :: Interpretation_Type -> Interpretation_Type -> Bool # (/=) :: Interpretation_Type -> Interpretation_Type -> Bool #

data Domain Source #

Constructors

Naturals
Rationals Rational
Arctic Domain
Tropical Domain

Instances

Eq Domain Source #
Methods (==) :: Domain -> Domain -> Bool # (/=) :: Domain -> Domain -> Bool #

data Interpret Source #

Constructors

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

Instances

Eq Interpret Source #
Methods (==) :: Interpret -> Interpret -> Bool # (/=) :: Interpret -> Interpret -> Bool #

data Value Source #

Constructors

Polynomial Polynomial
ArithFunction ArithFunction

Instances

Eq Value Source #
Methods (==) :: Value -> Value -> Bool # (/=) :: Value -> Value -> Bool #

data Polynomial Source #

Constructors

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

Instances

Eq Polynomial Source #
Methods (==) :: Polynomial -> Polynomial -> Bool # (/=) :: Polynomial -> Polynomial -> Bool #

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 #
Methods (==) :: ArithFunction -> ArithFunction -> Bool # (/=) :: ArithFunction -> ArithFunction -> Bool #

data Symbol Source #

Constructors

SymName Identifier
SymSharp Symbol
SymLabel Symbol Label

Instances

Eq Symbol Source #
Methods (==) :: Symbol -> Symbol -> Bool # (/=) :: Symbol -> Symbol -> Bool #

data Label Source #

Constructors

LblNumber [Integer]
LblSymbol [Symbol]

Instances

Eq Label Source #
Methods (==) :: Label -> Label -> Bool # (/=) :: Label -> Label -> Bool #

data Coefficient Source #

Constructors

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

Instances

Eq Coefficient Source #
Methods (==) :: Coefficient -> Coefficient -> Bool # (/=) :: Coefficient -> Coefficient -> Bool #

data Exotic Source #

Constructors

Minus_Infinite
E_Integer Integer
E_Rational Rational
Plus_Infinite

Instances

Eq Exotic Source #
Methods (==) :: Exotic -> Exotic -> Bool # (/=) :: Exotic -> Exotic -> Bool #

class ToExotic a where Source #

Minimal complete definition

toExotic

Methods

toExotic :: a -> Exotic Source #

data PathOrder Source #

Constructors

PathOrder [PrecedenceEntry] [ArgumentFilterEntry]

Instances

Eq PathOrder Source #
Methods (==) :: PathOrder -> PathOrder -> Bool # (/=) :: PathOrder -> PathOrder -> Bool #

data PrecedenceEntry Source #

Constructors

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

Instances

Eq PrecedenceEntry Source #
Methods (==) :: PrecedenceEntry -> PrecedenceEntry -> Bool # (/=) :: PrecedenceEntry -> PrecedenceEntry -> Bool #

data ArgumentFilterEntry Source #

Constructors

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

Instances

Eq ArgumentFilterEntry Source #
Methods (==) :: ArgumentFilterEntry -> ArgumentFilterEntry -> Bool # (/=) :: ArgumentFilterEntry -> ArgumentFilterEntry -> Bool #

data ACTerminationProof Source #

Constructors

ACTerminationProofFIXME ()

Instances

Eq ACTerminationProof Source #
Methods (==) :: ACTerminationProof -> ACTerminationProof -> Bool # (/=) :: ACTerminationProof -> ACTerminationProof -> Bool #

data Identifier Source #

Instances

Eq Identifier Source #
Methods (==) :: Identifier -> Identifier -> Bool # (/=) :: Identifier -> Identifier -> Bool #
Ord Identifier Source #
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 #
Methods showsPrec :: Int -> Identifier -> ShowS # show :: Identifier -> String # showList :: [Identifier] -> ShowS #
Hashable Identifier Source #
Methods hashWithSalt :: Int -> Identifier -> Int # hash :: Identifier -> Int #
Reader Identifier Source #
Methods reader :: Parser Identifier Source #
Reader (SRS Identifier) Source #
Methods reader :: Parser (SRS Identifier) Source #
Reader v => Reader (Term v Identifier) Source #
Methods reader :: Parser (Term v Identifier) Source #
Reader (TRS Identifier Identifier) Source #
Methods reader :: Parser (TRS Identifier Identifier) Source #

type TES = TRS Identifier Identifier Source #

legacy stuff (used in matchbox)