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

Instances

Typeable CertificationProblemInput
XmlContent CertificationProblemInput

data Proof Source

Constructors

TrsTerminationProof TrsTerminationProof

Instances

Typeable Proof
XmlContent Proof

data Sharp i Source

Constructors

Sharp i
Plain i

Instances

Typeable1 Sharp
Eq i => Eq (Sharp i)
Ord i => Ord (Sharp i)
(Typeable i, XmlContent i) => XmlContent (Sharp i)

data DPS Source

Constructors

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

Instances

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

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

Typeable DpProof
XmlContent DpProof

data OrderingConstraintProof Source

Constructors

RedPair
Fields interpretation :: Interpretation

Instances

Typeable OrderingConstraintProof
XmlContent OrderingConstraintProof

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

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

Instances

Typeable Interpret
XmlContent Interpret

data Value Source

Constructors

Polynomial Polynomial

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 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

Instances

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

data Identifier Source

Instances

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