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

XmlContent CertificationProblem
Typeable * CertificationProblem

data Origin Source

Constructors

ProofOrigin Tool

Instances

XmlContent Origin
Typeable * Origin

data Tool Source

Constructors

Tool
Fields name :: String version :: String

Instances

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

Instances

XmlContent CertificationProblemInput
Typeable * CertificationProblemInput

data Proof Source

Constructors

TrsTerminationProof TrsTerminationProof

Instances

XmlContent Proof
Typeable * Proof

data Sharp i Source

Constructors

Sharp i
Plain i

Instances

Eq i => Eq (Sharp i)
Ord i => Ord (Sharp i)
(Typeable * i, XmlContent i) => XmlContent (Sharp i)
Typeable (* -> *) Sharp

data DPS Source

Constructors

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

Instances

XmlContent DPS
Typeable * DPS

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

XmlContent TrsTerminationProof
Typeable * TrsTerminationProof

data Model Source

Constructors

FiniteModel
Fields carrierSize :: Int

Instances

Typeable * Model

data DpProof Source

Constructors

PIsEmpty
RedPairProc
Fields dp_orderingConstraintProof :: OrderingConstraintProof red_pair_dps :: DPS redpairproc_dpProof :: DpProof

Instances

XmlContent DpProof
Typeable * DpProof

data OrderingConstraintProof Source

Constructors

RedPair
Fields interpretation :: Interpretation

Instances

XmlContent OrderingConstraintProof
Typeable * OrderingConstraintProof

data Interpretation Source

Constructors

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

Instances

XmlContent Interpretation
Typeable * Interpretation

data Interpretation_Type Source

Constructors

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

Instances

XmlContent Interpretation_Type
Typeable * Interpretation_Type

data Domain Source

Constructors

Naturals
Rationals Rational
Arctic Domain
Tropical Domain

Instances

XmlContent Domain
Typeable * Domain

data Interpret Source

Constructors

forall s . XmlContent s => Interpret
Fields symbol :: s arity :: Int value :: Value

Instances

XmlContent Interpret
Typeable * Interpret

data Value Source

Constructors

Polynomial Polynomial

Instances

XmlContent Value
Typeable * Value

data Polynomial Source

Constructors

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

Instances

XmlContent Polynomial
Typeable * Polynomial

data Coefficient Source

Constructors

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

Instances

XmlContent Coefficient
Typeable * Coefficient

data Exotic Source

Constructors

Minus_Infinite
E_Integer Integer
E_Rational Rational
Plus_Infinite

Instances

XmlContent Exotic
Typeable * Exotic

class ToExotic a where Source

Methods

toExotic :: a -> Exotic Source

Instances

ToExotic Integer
ToExotic MinPlus
ToExotic MaxPlus
ToExotic a => ToExotic (Xml_As_String a)

data Identifier Source

Instances

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

type TES = TRS Identifier Identifier Source

legaca stuff (used in matchbox)