TPDB.CPF.Proof.Type

Description

Synopsis

• data CertificationProblem = CertificationProblem {
  • input :: CertificationProblemInput
  • cpfVersion :: String
  • proof :: Proof
  • origin :: Origin
  }
• data Origin = ProofOrigin {
  • tool :: Tool
  }
• ignoredOrigin :: Origin
• data Tool = Tool {
  • name :: String
  • version :: String
  }
• data CertificationProblemInput
  • = TrsInput {
    • trsinput_trs :: TRS Identifier Identifier
    }
  • | ComplexityInput {
    • trsinput_trs :: TRS Identifier Identifier
    • complexityMeasure :: ComplexityMeasure
    • complexityClass :: ComplexityClass
    }
• data Proof
  • = TrsTerminationProof TrsTerminationProof
  • | TrsNonterminationProof TrsNonterminationProof
  • | RelativeTerminationProof TrsTerminationProof
  • | RelativeNonterminationProof TrsNonterminationProof
  • | ComplexityProof ComplexityProof
• data DPS = forall s . (XmlContent s, Typeable s, Eq s) => DPS [Rule (Term Identifier s)]
• data ComplexityProof = ComplexityProofFIXME ()
• data ComplexityMeasure
  • = DerivationalComplexity
  • | RuntimeComplexity
• data ComplexityClass = ComplexityClassPolynomial {
  • degree :: Int
  }
• data TrsNonterminationProof = TrsNonterminationProofFIXME ()
• data TrsTerminationProof
  • = RIsEmpty
  • | RuleRemoval {
    • rr_orderingConstraintProof :: OrderingConstraintProof
    • trs :: TRS Identifier Identifier
    • trsTerminationProof :: TrsTerminationProof
    }
  • | DpTrans {
    • dptrans_dps :: DPS
    • markedSymbols :: Bool
    • dptrans_dpProof :: DpProof
    }
  • | Semlab {
    • model :: Model
    • trs :: TRS Identifier Identifier
    • trsTerminationProof :: TrsTerminationProof
    }
  • | Unlab {
    • trs :: TRS Identifier Identifier
    • trsTerminationProof :: TrsTerminationProof
    }
  • | StringReversal {
    • trs :: TRS Identifier Identifier
    • trsTerminationProof :: TrsTerminationProof
    }
• data Model = FiniteModel Int [Interpret]
• data DpProof
  • = PIsEmpty
  • | RedPairProc {
    • rppOrderingConstraintProof :: OrderingConstraintProof
    • rppDps :: DPS
    • rppUsableRules :: Maybe DPS
    • rppDpProof :: DpProof
    }
  • | DepGraphProc [DepGraphComponent]
  • | SemLabProc {
    • slpModel :: Model
    • slpDps :: DPS
    • slpTrs :: DPS
    • slpDpProof :: DpProof
    }
  • | UnlabProc {
    • ulpDps :: DPS
    • ulpTrs :: DPS
    • ulpDpProof :: DpProof
    }
• data DepGraphComponent = DepGraphComponent {
  • dgcRealScc :: Bool
  • dgcDps :: DPS
  • dgcDpProof :: DpProof
  }
• data OrderingConstraintProof = OCPRedPair RedPair
• data RedPair
  • = RPInterpretation Interpretation
  • | RPPathOrder PathOrder
• data Interpretation = Interpretation {
  • interpretation_type :: Interpretation_Type
  • interprets :: [Interpret]
  }
• data Interpretation_Type = Matrix_Interpretation {
  • domain :: Domain
  • dimension :: Int
  • strictDimension :: Int
  }
• data Domain
  • = Naturals
  • | Rationals Rational
  • | Arctic Domain
  • | Tropical Domain
• data Interpret = Interpret {
  • symbol :: Symbol
  • arity :: Int
  • value :: Value
  }
• data Value
  • = Polynomial Polynomial
  • | ArithFunction ArithFunction
• data Polynomial
  • = Sum [Polynomial]
  • | Product [Polynomial]
  • | Polynomial_Coefficient Coefficient
  • | Polynomial_Variable String
• data ArithFunction
  • = AFNatural Integer
  • | AFVariable Integer
  • | AFSum [ArithFunction]
  • | AFProduct [ArithFunction]
  • | AFMin [ArithFunction]
  • | AFMax [ArithFunction]
  • | AFIfEqual ArithFunction ArithFunction ArithFunction ArithFunction
• data Symbol
  • = SymName Identifier
  • | SymSharp Symbol
  • | SymLabel Symbol Label
• data Label
  • = LblNumber [Integer]
  • | LblSymbol [Symbol]
• data Coefficient
  • = Vector [Coefficient]
  • | Matrix [Coefficient]
  • | forall a . (Eq a, XmlContent a) => Coefficient_Coefficient a
• data Exotic
  • = Minus_Infinite
  • | E_Integer Integer
  • | E_Rational Rational
  • | Plus_Infinite
• class ToExotic a where
  • toExotic :: a -> Exotic
• data PathOrder = PathOrder [PrecedenceEntry] [ArgumentFilterEntry]
• data PrecedenceEntry = PrecedenceEntry {
  • peSymbol :: Symbol
  • peArity :: Int
  • pePrecedence :: Integer
  }
• data ArgumentFilterEntry = ArgumentFilterEntry {
  • afeSymbol :: Symbol
  • afeArity :: Int
  • afeFilter :: Either Int [Int]
  }
• data Identifier
• type TES = TRS Identifier Identifier

Documentation