Safe Haskell	None

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

Typeable CertificationProblem
XmlContent CertificationProblem

data Origin Source

Constructors

ProofOrigin Tool

Instances

Typeable Origin
XmlContent Origin

data Tool Source

Constructors

Tool
Fields name :: String version :: String

Instances

Typeable Tool
XmlContent 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

Typeable CertificationProblemInput
XmlContent CertificationProblemInput

data Proof Source

Constructors

TrsTerminationProof TrsTerminationProof
TrsNonterminationProof TrsNonterminationProof
RelativeTerminationProof TrsTerminationProof
RelativeNonterminationProof TrsNonterminationProof
ComplexityProof ComplexityProof

Instances

Typeable Proof
XmlContent Proof

data DPS Source

Constructors

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

Instances

Typeable DPS
XmlContent DPS

data ComplexityProof Source

Constructors

ComplexityProofFIXME ()

Instances

Typeable ComplexityProof

data ComplexityMeasure Source

Constructors

DerivationalComplexity
RuntimeComplexity

Instances

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.atusersgeorgcbrcompetition/rules.php
Fields degree :: Int

Instances

Eq ComplexityClass
Typeable ComplexityClass

data TrsNonterminationProof Source

Constructors

TrsNonterminationProofFIXME ()

Instances

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

Typeable TrsTerminationProof
XmlContent TrsTerminationProof

data Model Source

Constructors

FiniteModel Int [Interpret]

Instances

Typeable Model
XmlContent 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

Typeable DpProof
XmlContent DpProof

data DepGraphComponent Source

Constructors

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

Instances

Typeable DepGraphComponent
XmlContent DepGraphComponent

data OrderingConstraintProof Source

Constructors

OCPRedPair RedPair

Instances

Typeable OrderingConstraintProof
XmlContent OrderingConstraintProof

data RedPair Source

Constructors

RPInterpretation Interpretation
RPPathOrder PathOrder

Instances

Typeable RedPair
XmlContent RedPair

data Interpretation Source

Constructors

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

Instances

Typeable Interpretation
XmlContent Interpretation

data Interpretation_Type Source

Constructors

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

Instances

Typeable Interpretation_Type
XmlContent Interpretation_Type

data Domain Source

Constructors

Naturals
Rationals Rational
Arctic Domain
Tropical Domain

Instances

Typeable Domain
XmlContent Domain

data Interpret Source

Constructors

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

Instances

Typeable Interpret
XmlContent Interpret

data Value Source

Constructors

Polynomial Polynomial
ArithFunction ArithFunction

Instances

Typeable Value
XmlContent Value

data Polynomial Source

Constructors

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

Instances

Typeable Polynomial
XmlContent Polynomial

data Symbol Source

Constructors

SymName Identifier
SymSharp Symbol
SymLabel Symbol Label

Instances

Typeable Symbol
XmlContent Symbol
XmlContent (TRS Identifier Symbol)

data Label Source

Constructors

LblNumber [Integer]
LblSymbol [Symbol]

Instances

Typeable Label
XmlContent Label

data Coefficient Source

Constructors

Vector [Coefficient]
Matrix [Coefficient]
forall a . XmlContent a => Coefficient_Coefficient a

Instances

Typeable Coefficient
XmlContent Coefficient

data Exotic Source

Constructors

Minus_Infinite
E_Integer Integer
E_Rational Rational
Plus_Infinite

Instances

Typeable Exotic
XmlContent Exotic

class ToExotic a whereSource

Methods

toExotic :: a -> Exotic Source

data PathOrder Source

Constructors

PathOrder [PrecedenceEntry] [ArgumentFilterEntry]

Instances

Typeable PathOrder
XmlContent PathOrder

data PrecedenceEntry Source

Constructors

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

Instances

Typeable PrecedenceEntry
XmlContent PrecedenceEntry

data ArgumentFilterEntry Source

Constructors

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

Instances

Typeable ArgumentFilterEntry
XmlContent ArgumentFilterEntry

data Identifier Source

Instances

Eq Identifier
Ord Identifier
Show Identifier
Typeable Identifier
XmlContent Identifier	FIXME: move to separate module
Hashable Identifier
Pretty Identifier
Reader 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)

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