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 :: String proof :: Proof origin :: Origin

Instances

Eq CertificationProblem
XmlContent CertificationProblem
Typeable * CertificationProblem

data Origin Source

Constructors

ProofOrigin
Fields tool :: Tool

Instances

Eq Origin
XmlContent Origin
Typeable * Origin

ignoredOrigin :: Origin Source

data Tool Source

Constructors

Tool
Fields name :: String version :: String

Instances

Eq Tool
XmlContent Tool
Typeable * Tool

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

Instances

Eq CertificationProblemInput
XmlContent CertificationProblemInput
Typeable * CertificationProblemInput

data Proof Source

Constructors

TrsTerminationProof TrsTerminationProof
TrsNonterminationProof TrsNonterminationProof
RelativeTerminationProof TrsTerminationProof
RelativeNonterminationProof TrsNonterminationProof
ComplexityProof ComplexityProof

Instances

Eq Proof
XmlContent Proof
Typeable * Proof

data DPS Source

Constructors

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

Instances

Eq DPS
XmlContent DPS
Typeable * DPS

data ComplexityProof Source

Constructors

ComplexityProofFIXME ()

Instances

Eq ComplexityProof
Typeable * ComplexityProof

data ComplexityMeasure Source

Constructors

DerivationalComplexity
RuntimeComplexity

Instances

Eq ComplexityMeasure
Typeable * ComplexityMeasure

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
Typeable * ComplexityClass

data TrsNonterminationProof Source

Constructors

TrsNonterminationProofFIXME ()

Instances

Eq TrsNonterminationProof
Typeable * TrsNonterminationProof

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

Instances

Eq TrsTerminationProof
XmlContent TrsTerminationProof
Typeable * TrsTerminationProof

data Model Source

Constructors

FiniteModel Int [Interpret]

Instances

Eq Model
XmlContent Model
Typeable * Model

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
XmlContent DpProof
Typeable * DpProof

data DepGraphComponent Source

Constructors

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

Instances

Eq DepGraphComponent
XmlContent DepGraphComponent
Typeable * DepGraphComponent

data OrderingConstraintProof Source

Constructors

OCPRedPair RedPair

Instances

Eq OrderingConstraintProof
XmlContent OrderingConstraintProof
Typeable * OrderingConstraintProof

data RedPair Source

Constructors

RPInterpretation Interpretation
RPPathOrder PathOrder

Instances

Eq RedPair
XmlContent RedPair
Typeable * RedPair

data Interpretation Source

Constructors

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

Instances

Eq Interpretation
XmlContent Interpretation
Typeable * Interpretation

data Interpretation_Type Source

Constructors

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

Instances

Eq Interpretation_Type
XmlContent Interpretation_Type
Typeable * Interpretation_Type

data Domain Source

Constructors

Naturals
Rationals Rational
Arctic Domain
Tropical Domain

Instances

Eq Domain
XmlContent Domain
Typeable * Domain

data Interpret Source

Constructors

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

Instances

Eq Interpret
XmlContent Interpret
Typeable * Interpret

data Value Source

Constructors

Polynomial Polynomial
ArithFunction ArithFunction

Instances

Eq Value
XmlContent Value
Typeable * Value

data Polynomial Source

Constructors

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

Instances

Eq Polynomial
XmlContent Polynomial
Typeable * Polynomial

data ArithFunction Source

Constructors

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

Instances

Eq ArithFunction
XmlContent ArithFunction
Typeable * ArithFunction

data Symbol Source

Constructors

SymName Identifier
SymSharp Symbol
SymLabel Symbol Label

Instances

Eq Symbol
XmlContent Symbol
Typeable * Symbol
XmlContent (TRS Identifier Symbol)

data Label Source

Constructors

LblNumber [Integer]
LblSymbol [Symbol]

Instances

Eq Label
XmlContent Label
Typeable * Label

data Coefficient Source

Constructors

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

Instances

Eq Coefficient
XmlContent Coefficient
Typeable * Coefficient

data Exotic Source

Constructors

Minus_Infinite
E_Integer Integer
E_Rational Rational
Plus_Infinite

Instances

Eq Exotic
XmlContent Exotic
Typeable * Exotic

class ToExotic a where Source

Methods

toExotic :: a -> Exotic Source

data PathOrder Source

Constructors

PathOrder [PrecedenceEntry] [ArgumentFilterEntry]

Instances

Eq PathOrder
XmlContent PathOrder
Typeable * PathOrder

data PrecedenceEntry Source

Constructors

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

Instances

Eq PrecedenceEntry
XmlContent PrecedenceEntry
Typeable * PrecedenceEntry

data ArgumentFilterEntry Source

Constructors

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

Instances

Eq ArgumentFilterEntry
XmlContent ArgumentFilterEntry
Typeable * ArgumentFilterEntry

data Identifier Source

Instances

Eq Identifier
Ord Identifier
Show Identifier
XmlContent Identifier	FIXME: move to separate module
Hashable Identifier
Pretty Identifier
Reader Identifier
Typeable * Identifier
Reader (SRS Identifier)
XmlContent (TRS Identifier Symbol)
Reader v => Reader (Term v Identifier)
Reader (TRS Identifier Identifier)

type TES = TRS Identifier Identifier Source

legaca stuff (used in matchbox)