Safe Haskell	Safe-Inferred
Language	Haskell2010

TPDB.CPF.Proof.Type

Description

internal representation of CPF termination proofs, see http://cl-informatik.uibk.ac.at/software/cpf/

Synopsis

data Symbol
- = SymName Identifier
- | SymSharp Symbol
- | SymLabel Symbol Label
data State = State Text
data Value
- = Polynomial Polynomial
- | ArithFunction ArithFunction
data Kind
- = Standard
- | Relative
data Substitution = Substitution [SubstEntry]
data CertificationProblem = CertificationProblem {
- input :: CertificationProblemInput
- cpfVersion :: Text
- proof :: Proof
- origin :: Origin
}
data CertificationProblemInput
- = TrsInput {
  - trsinput_trs :: Trs
  }
- | ComplexityInput {
  - trsinput_trs :: Trs
  - complexityMeasure :: ComplexityMeasure
  - complexityClass :: ComplexityClass
  }
- | ACRewriteSystem {
  - trsinput_trs :: Trs
  - asymbols :: [Symbol]
  - csymbols :: [Symbol]
  }
data Proof
- = TrsTerminationProof (TrsTerminationProof Standard)
- | TrsNonterminationProof (TrsNonterminationProof Standard)
- | RelativeTerminationProof (TrsTerminationProof Relative)
- | RelativeNonterminationProof (TrsNonterminationProof Relative)
- | ComplexityProof ComplexityProof
- | ACTerminationProof ACTerminationProof
data Origin = ProofOrigin {
- tool :: Tool
}
data Tool = Tool {
- name :: Text
- version :: Text
}
type Trs = TRS Identifier Symbol
data ComplexityMeasure
- = DerivationalComplexity
- | RuntimeComplexity
data ComplexityClass = ComplexityClassPolynomial {
- degree :: Int
}
data TrsTerminationProof (k :: Kind) where
- RIsEmpty :: TrsTerminationProof k
- SIsEmpty :: {..} -> TrsTerminationProof Relative
- RuleRemoval :: {..} -> TrsTerminationProof k
- EqualityRemoval :: {..} -> TrsTerminationProof Relative
- DpTrans :: {..} -> TrsTerminationProof Standard
- FlatContextClosure :: {..} -> TrsTerminationProof k
- Semlab :: {..} -> TrsTerminationProof k
- Split :: {..} -> TrsTerminationProof k
- StringReversal :: {..} -> TrsTerminationProof k
- Bounds :: {..} -> TrsTerminationProof Standard
data TrsNonterminationProof (k :: Kind)
- = VariableConditionViolated
- | TNP_RuleRemoval Trs (TrsNonterminationProof k)
- | TNP_StringReversal Trs (TrsNonterminationProof k)
- | Loop {
  - rewriteSequence :: RewriteSequence
  - substitution :: Substitution
  - context :: Context
  }
data ComplexityProof = ComplexityProofFIXME ()
data ACTerminationProof = ACTerminationProofFIXME ()
data DPS = DPS [Rule (Term Identifier Symbol)]
data RewriteSequence = RewriteSequence (Term Identifier Symbol) [RewriteStep]
data Context
- = Box
- | FunContext {
  - fc_symbol :: Symbol
  - fc_before :: [Term Identifier Symbol]
  - fc_here :: Context
  - fc_after :: [Term Identifier Symbol]
  }
data RewriteStep = RewriteStep {
- rs_position :: Position
- rs_rule :: Rule (Term Identifier Symbol)
- rs_term :: Term Identifier Symbol
}
data SubstEntry = SubstEntry Identifier (Term Identifier Symbol)
data OrderingConstraintProof = OCPRedPair RedPair
data DpProof
- = PIsEmpty
- | RedPairProc {
  - rppMono :: Mono
  - rppOrderingConstraintProof :: OrderingConstraintProof
  - rppDps :: DPS
  - rppTrs :: Maybe Trs
  - rppUsableRules :: Maybe DPS
  - rppDpProof :: DpProof
  }
- | DepGraphProc [DepGraphComponent]
- | SemLabProc {
  - slpModel :: Model
  - slpDps :: DPS
  - slpTrs :: DPS
  - slpDpProof :: DpProof
  }
- | UnlabProc {
  - ulpDps :: DPS
  - ulpTrs :: DPS
  - ulpDpProof :: DpProof
  }
data Model
- = FiniteModel Int [Interpret]
- | RootLabeling
data Bounds_Type
- = Roof
- | Match
data TreeAutomaton = TreeAutomaton {
- ta_finalStates :: [State]
- ta_transitions :: [Transition]
}
data Criterion = Compatibility
data Transition = Transition {
- transition_lhs :: Transition_Lhs
- transition_rhs :: State
}
data Transition_Lhs
- = Transition_Symbol {
  - tr_symbol :: Symbol
  - tr_height :: Int
  - tr_arguments :: [State]
  }
- | Transition_Epsilon State
data Interpret = Interpret {
- symbol :: Symbol
- arity :: Int
- value :: Value
}
data Mono
- = Weak
- | Strict
data DepGraphComponent = DepGraphComponent {
- dgcRealScc :: Bool
- dgcDps :: DPS
- dgcDpProof :: DpProof
}
data RedPair
- = RPInterpretation Interpretation
- | RPPathOrder PathOrder
data Interpretation = Interpretation {
- interpretation_type :: Interpretation_Type
- interprets :: [Interpret]
}
data PathOrder = PathOrder [PrecedenceEntry] [ArgumentFilterEntry]
data Interpretation_Type = Matrix_Interpretation {
- domain :: Domain
- dimension :: Int
- strictDimension :: Int
}
data Domain
- = Naturals
- | Rationals Rational
- | Arctic Domain
- | Tropical Domain
data Polynomial
- = Sum [Polynomial]
- | Product [Polynomial]
- | Polynomial_Coefficient Coefficient
- | Polynomial_Variable Text
data ArithFunction
- = AFNatural Integer
- | AFVariable Integer
- | AFSum [ArithFunction]
- | AFProduct [ArithFunction]
- | AFMin [ArithFunction]
- | AFMax [ArithFunction]
- | AFIfEqual ArithFunction ArithFunction ArithFunction ArithFunction
data Coefficient
- = Vector [Coefficient]
- | Matrix [Coefficient]
- | forall a.(Eq a, XmlContent a) => Coefficient_Coefficient a
data Label
- = LblNumber [Integer]
- | LblSymbol [Symbol]
data Exotic
- = Minus_Infinite
- | E_Integer Integer
- | E_Rational Rational
- | Plus_Infinite
class ToExotic a where
- toExotic :: a -> Exotic
data PrecedenceEntry = PrecedenceEntry {
- peSymbol :: Symbol
- peArity :: Int
- pePrecedence :: Integer
}
data ArgumentFilterEntry = ArgumentFilterEntry {
- afeSymbol :: Symbol
- afeArity :: Int
- afeFilter :: Either Int [Int]
}
ignoredOrigin :: Origin
data Identifier
type TES = TRS Identifier Identifier

Documentation

data Symbol Source #

Constructors

SymName Identifier
SymSharp Symbol
SymLabel Symbol Label

Instances

Instances details

Generic Symbol Source #
Instance details Defined in TPDB.CPF.Proof.Type Associated Types type Rep Symbol :: Type -> Type # Methods from :: Symbol -> Rep Symbol x # to :: Rep Symbol x -> Symbol #
Show Symbol Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods showsPrec :: Int -> Symbol -> ShowS # show :: Symbol -> String # showList :: [Symbol] -> ShowS #
Eq Symbol Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: Symbol -> Symbol -> Bool # (/=) :: Symbol -> Symbol -> Bool #
Ord Symbol Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods compare :: Symbol -> Symbol -> Ordering # (<) :: Symbol -> Symbol -> Bool # (<=) :: Symbol -> Symbol -> Bool # (>) :: Symbol -> Symbol -> Bool # (>=) :: Symbol -> Symbol -> Bool # max :: Symbol -> Symbol -> Symbol # min :: Symbol -> Symbol -> Symbol #
Hashable Symbol Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods hashWithSalt :: Int -> Symbol -> Int # hash :: Symbol -> Int #
Pretty Symbol Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods pretty :: Symbol -> Doc ann # prettyList :: [Symbol] -> Doc ann #
XmlContent Symbol Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: Symbol -> [Node] Source # parseContents :: Cursor -> [Symbol] Source #
XmlContent (TRS Identifier Symbol) Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: TRS Identifier Symbol -> [Node] Source # parseContents :: Cursor -> [TRS Identifier Symbol] Source #
type Rep Symbol Source #
Instance details Defined in TPDB.CPF.Proof.Type type Rep Symbol = D1 ('MetaData "Symbol" "TPDB.CPF.Proof.Type" "tpdb-2.7.3-CgDLIzMWhg29yaLLziq7QN" 'False) (C1 ('MetaCons "SymName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Identifier)) :+: (C1 ('MetaCons "SymSharp" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Symbol)) :+: C1 ('MetaCons "SymLabel" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Symbol) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Label))))

data State Source #

Constructors

State Text

Instances

Instances details

Generic State Source #
Instance details Defined in TPDB.CPF.Proof.Type Associated Types type Rep State :: Type -> Type # Methods from :: State -> Rep State x # to :: Rep State x -> State #
Eq State Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: State -> State -> Bool # (/=) :: State -> State -> Bool #
XmlContent State Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: State -> [Node] Source # parseContents :: Cursor -> [State] Source #
type Rep State Source #
Instance details Defined in TPDB.CPF.Proof.Type type Rep State = D1 ('MetaData "State" "TPDB.CPF.Proof.Type" "tpdb-2.7.3-CgDLIzMWhg29yaLLziq7QN" 'False) (C1 ('MetaCons "State" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Text)))

data Value Source #

Constructors

Polynomial Polynomial
ArithFunction ArithFunction

Instances

Instances details

Generic Value Source #
Instance details Defined in TPDB.CPF.Proof.Type Associated Types type Rep Value :: Type -> Type # Methods from :: Value -> Rep Value x # to :: Rep Value x -> Value #
Eq Value Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: Value -> Value -> Bool # (/=) :: Value -> Value -> Bool #
XmlContent Value Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: Value -> [Node] Source # parseContents :: Cursor -> [Value] Source #
type Rep Value Source #
Instance details Defined in TPDB.CPF.Proof.Type type Rep Value = D1 ('MetaData "Value" "TPDB.CPF.Proof.Type" "tpdb-2.7.3-CgDLIzMWhg29yaLLziq7QN" 'False) (C1 ('MetaCons "Polynomial" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Polynomial)) :+: C1 ('MetaCons "ArithFunction" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 ArithFunction)))

data Kind Source #

Constructors

Standard
Relative

Instances

Instances details

Generic Kind Source #
Instance details Defined in TPDB.CPF.Proof.Type Associated Types type Rep Kind :: Type -> Type # Methods from :: Kind -> Rep Kind x # to :: Rep Kind x -> Kind #
Eq Kind Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: Kind -> Kind -> Bool # (/=) :: Kind -> Kind -> Bool #
type Rep Kind Source #
Instance details Defined in TPDB.CPF.Proof.Type type Rep Kind = D1 ('MetaData "Kind" "TPDB.CPF.Proof.Type" "tpdb-2.7.3-CgDLIzMWhg29yaLLziq7QN" 'False) (C1 ('MetaCons "Standard" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Relative" 'PrefixI 'False) (U1 :: Type -> Type))

data Substitution Source #

Constructors

Substitution [SubstEntry]

Instances

Instances details

Generic Substitution Source #
Instance details Defined in TPDB.CPF.Proof.Type Associated Types type Rep Substitution :: Type -> Type # Methods from :: Substitution -> Rep Substitution x # to :: Rep Substitution x -> Substitution #
Eq Substitution Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: Substitution -> Substitution -> Bool # (/=) :: Substitution -> Substitution -> Bool #
XmlContent Substitution Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: Substitution -> [Node] Source # parseContents :: Cursor -> [Substitution] Source #
type Rep Substitution Source #
Instance details Defined in TPDB.CPF.Proof.Type type Rep Substitution = D1 ('MetaData "Substitution" "TPDB.CPF.Proof.Type" "tpdb-2.7.3-CgDLIzMWhg29yaLLziq7QN" 'False) (C1 ('MetaCons "Substitution" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 [SubstEntry])))

data CertificationProblem Source #

Constructors

CertificationProblem
Fields input :: CertificationProblemInput cpfVersion :: Text proof :: Proof origin :: Origin

Instances

Instances details

Generic CertificationProblem Source #
Instance details Defined in TPDB.CPF.Proof.Type Associated Types type Rep CertificationProblem :: Type -> Type # Methods from :: CertificationProblem -> Rep CertificationProblem x # to :: Rep CertificationProblem x -> CertificationProblem #
Eq CertificationProblem Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: CertificationProblem -> CertificationProblem -> Bool # (/=) :: CertificationProblem -> CertificationProblem -> Bool #
XmlContent CertificationProblem Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: CertificationProblem -> [Node] Source # parseContents :: Cursor -> [CertificationProblem] Source #
type Rep CertificationProblem Source #
Instance details Defined in TPDB.CPF.Proof.Type type Rep CertificationProblem = D1 ('MetaData "CertificationProblem" "TPDB.CPF.Proof.Type" "tpdb-2.7.3-CgDLIzMWhg29yaLLziq7QN" 'False) (C1 ('MetaCons "CertificationProblem" 'PrefixI 'True) ((S1 ('MetaSel ('Just "input") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 CertificationProblemInput) :: S1 ('MetaSel ('Just "cpfVersion") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Text)) :: (S1 ('MetaSel ('Just "proof") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Proof) :*: S1 ('MetaSel ('Just "origin") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Origin))))

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
ComplexityInput
Fields trsinput_trs :: Trs complexityMeasure :: ComplexityMeasure complexityClass :: ComplexityClass
ACRewriteSystem
Fields trsinput_trs :: Trs asymbols :: [Symbol] csymbols :: [Symbol]

Instances

Instances details

Generic CertificationProblemInput Source #
Instance details Defined in TPDB.CPF.Proof.Type Associated Types type Rep CertificationProblemInput :: Type -> Type # Methods from :: CertificationProblemInput -> Rep CertificationProblemInput x # to :: Rep CertificationProblemInput x -> CertificationProblemInput #
Eq CertificationProblemInput Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: CertificationProblemInput -> CertificationProblemInput -> Bool # (/=) :: CertificationProblemInput -> CertificationProblemInput -> Bool #
Pretty CertificationProblemInput Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods pretty :: CertificationProblemInput -> Doc ann # prettyList :: [CertificationProblemInput] -> Doc ann #
XmlContent CertificationProblemInput Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: CertificationProblemInput -> [Node] Source # parseContents :: Cursor -> [CertificationProblemInput] Source #
type Rep CertificationProblemInput Source #
Instance details Defined in TPDB.CPF.Proof.Type type Rep CertificationProblemInput = D1 ('MetaData "CertificationProblemInput" "TPDB.CPF.Proof.Type" "tpdb-2.7.3-CgDLIzMWhg29yaLLziq7QN" 'False) (C1 ('MetaCons "TrsInput" 'PrefixI 'True) (S1 ('MetaSel ('Just "trsinput_trs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Trs)) :+: (C1 ('MetaCons "ComplexityInput" 'PrefixI 'True) (S1 ('MetaSel ('Just "trsinput_trs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Trs) :: (S1 ('MetaSel ('Just "complexityMeasure") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 ComplexityMeasure) :: S1 ('MetaSel ('Just "complexityClass") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 ComplexityClass))) :+: C1 ('MetaCons "ACRewriteSystem" 'PrefixI 'True) (S1 ('MetaSel ('Just "trsinput_trs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Trs) :: (S1 ('MetaSel ('Just "asymbols") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 [Symbol]) :: S1 ('MetaSel ('Just "csymbols") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 [Symbol])))))

data Proof Source #

Constructors

TrsTerminationProof (TrsTerminationProof Standard)
TrsNonterminationProof (TrsNonterminationProof Standard)
RelativeTerminationProof (TrsTerminationProof Relative)
RelativeNonterminationProof (TrsNonterminationProof Relative)
ComplexityProof ComplexityProof
ACTerminationProof ACTerminationProof

Instances

Instances details

Generic Proof Source #
Instance details Defined in TPDB.CPF.Proof.Type Associated Types type Rep Proof :: Type -> Type # Methods from :: Proof -> Rep Proof x # to :: Rep Proof x -> Proof #
Eq Proof Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: Proof -> Proof -> Bool # (/=) :: Proof -> Proof -> Bool #
XmlContent Proof Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: Proof -> [Node] Source # parseContents :: Cursor -> [Proof] Source #
type Rep Proof Source #
Instance details Defined in TPDB.CPF.Proof.Type type Rep Proof = D1 ('MetaData "Proof" "TPDB.CPF.Proof.Type" "tpdb-2.7.3-CgDLIzMWhg29yaLLziq7QN" 'False) ((C1 ('MetaCons "TrsTerminationProof" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 (TrsTerminationProof 'Standard))) :+: (C1 ('MetaCons "TrsNonterminationProof" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 (TrsNonterminationProof 'Standard))) :+: C1 ('MetaCons "RelativeTerminationProof" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 (TrsTerminationProof 'Relative))))) :+: (C1 ('MetaCons "RelativeNonterminationProof" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 (TrsNonterminationProof 'Relative))) :+: (C1 ('MetaCons "ComplexityProof" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 ComplexityProof)) :+: C1 ('MetaCons "ACTerminationProof" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 ACTerminationProof)))))

data Origin Source #

Constructors

ProofOrigin
Fields tool :: Tool

Instances

Instances details

Generic Origin Source #
Instance details Defined in TPDB.CPF.Proof.Type Associated Types type Rep Origin :: Type -> Type # Methods from :: Origin -> Rep Origin x # to :: Rep Origin x -> Origin #
Eq Origin Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: Origin -> Origin -> Bool # (/=) :: Origin -> Origin -> Bool #
XmlContent Origin Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: Origin -> [Node] Source # parseContents :: Cursor -> [Origin] Source #
type Rep Origin Source #
Instance details Defined in TPDB.CPF.Proof.Type type Rep Origin = D1 ('MetaData "Origin" "TPDB.CPF.Proof.Type" "tpdb-2.7.3-CgDLIzMWhg29yaLLziq7QN" 'False) (C1 ('MetaCons "ProofOrigin" 'PrefixI 'True) (S1 ('MetaSel ('Just "tool") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Tool)))

data Tool Source #

Constructors

Tool
Fields name :: Text version :: Text

Instances

Instances details

Generic Tool Source #
Instance details Defined in TPDB.CPF.Proof.Type Associated Types type Rep Tool :: Type -> Type # Methods from :: Tool -> Rep Tool x # to :: Rep Tool x -> Tool #
Eq Tool Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: Tool -> Tool -> Bool # (/=) :: Tool -> Tool -> Bool #
XmlContent Tool Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: Tool -> [Node] Source # parseContents :: Cursor -> [Tool] Source #
type Rep Tool Source #
Instance details Defined in TPDB.CPF.Proof.Type type Rep Tool = D1 ('MetaData "Tool" "TPDB.CPF.Proof.Type" "tpdb-2.7.3-CgDLIzMWhg29yaLLziq7QN" 'False) (C1 ('MetaCons "Tool" 'PrefixI 'True) (S1 ('MetaSel ('Just "name") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Text) :*: S1 ('MetaSel ('Just "version") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Text)))

type Trs = TRS Identifier Symbol Source #

use this type throughout. Variables are plain identifiers but signature can use sharped, and labelled symbols.

data ComplexityMeasure Source #

Constructors

DerivationalComplexity
RuntimeComplexity

Instances

Instances details

Generic ComplexityMeasure Source #
Instance details Defined in TPDB.CPF.Proof.Type Associated Types type Rep ComplexityMeasure :: Type -> Type # Methods from :: ComplexityMeasure -> Rep ComplexityMeasure x # to :: Rep ComplexityMeasure x -> ComplexityMeasure #
Show ComplexityMeasure Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods showsPrec :: Int -> ComplexityMeasure -> ShowS # show :: ComplexityMeasure -> String # showList :: [ComplexityMeasure] -> ShowS #
Eq ComplexityMeasure Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: ComplexityMeasure -> ComplexityMeasure -> Bool # (/=) :: ComplexityMeasure -> ComplexityMeasure -> Bool #
type Rep ComplexityMeasure Source #
Instance details Defined in TPDB.CPF.Proof.Type type Rep ComplexityMeasure = D1 ('MetaData "ComplexityMeasure" "TPDB.CPF.Proof.Type" "tpdb-2.7.3-CgDLIzMWhg29yaLLziq7QN" 'False) (C1 ('MetaCons "DerivationalComplexity" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RuntimeComplexity" 'PrefixI 'False) (U1 :: Type -> Type))

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

Instances details

Generic ComplexityClass Source #
Instance details Defined in TPDB.CPF.Proof.Type Associated Types type Rep ComplexityClass :: Type -> Type # Methods from :: ComplexityClass -> Rep ComplexityClass x # to :: Rep ComplexityClass x -> ComplexityClass #
Show ComplexityClass Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods showsPrec :: Int -> ComplexityClass -> ShowS # show :: ComplexityClass -> String # showList :: [ComplexityClass] -> ShowS #
Eq ComplexityClass Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: ComplexityClass -> ComplexityClass -> Bool # (/=) :: ComplexityClass -> ComplexityClass -> Bool #
type Rep ComplexityClass Source #
Instance details Defined in TPDB.CPF.Proof.Type type Rep ComplexityClass = D1 ('MetaData "ComplexityClass" "TPDB.CPF.Proof.Type" "tpdb-2.7.3-CgDLIzMWhg29yaLLziq7QN" 'False) (C1 ('MetaCons "ComplexityClassPolynomial" 'PrefixI 'True) (S1 ('MetaSel ('Just "degree") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Int)))

data TrsTerminationProof (k :: Kind) where Source #

Constructors

RIsEmpty :: TrsTerminationProof k
SIsEmpty
Fields :: { trsTerminationProof_Standard :: !(TrsTerminationProof Standard) } -> TrsTerminationProof Relative
RuleRemoval
Fields :: { rr_orderingConstraintProof :: !OrderingConstraintProof , trs :: !Trs , trsTerminationProof :: !(TrsTerminationProof k) } -> TrsTerminationProof k
EqualityRemoval
Fields :: { trsTerminationProof_Relative :: !(TrsTerminationProof Relative) } -> TrsTerminationProof Relative
DpTrans
Fields :: { dptrans_dps :: DPS , markedSymbols :: Bool , dptrans_dpProof :: DpProof } -> TrsTerminationProof Standard
FlatContextClosure
Fields :: { flatContexts :: ![Context] , trs :: !Trs , trsTerminationProof :: !(TrsTerminationProof k) } -> TrsTerminationProof k
Semlab
Fields :: { model :: !Model , trs :: !Trs , trsTerminationProof :: !(TrsTerminationProof k) } -> TrsTerminationProof k
Split
Fields :: { trs :: !Trs , remove :: !(TrsTerminationProof Relative) , remain :: !(TrsTerminationProof k) } -> TrsTerminationProof k
StringReversal
Fields :: { trs :: !Trs , trsTerminationProof :: !(TrsTerminationProof k) } -> TrsTerminationProof k
Bounds
Fields :: { bounds_type :: Bounds_Type , bounds_bound :: Int , bounds_finalStates :: [State] , bounds_closedTreeAutomaton :: TreeAutomaton , bounds_criterion :: Criterion } -> TrsTerminationProof Standard

Instances

Instances details

Eq (TrsTerminationProof k) Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: TrsTerminationProof k -> TrsTerminationProof k -> Bool # (/=) :: TrsTerminationProof k -> TrsTerminationProof k -> Bool #
XmlContent (TrsTerminationProof 'Relative) Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: TrsTerminationProof 'Relative -> [Node] Source # parseContents :: Cursor -> [TrsTerminationProof 'Relative] Source #
XmlContent (TrsTerminationProof 'Standard) Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: TrsTerminationProof 'Standard -> [Node] Source # parseContents :: Cursor -> [TrsTerminationProof 'Standard] Source #

data TrsNonterminationProof (k :: Kind) Source #

Constructors

VariableConditionViolated
TNP_RuleRemoval Trs (TrsNonterminationProof k)
TNP_StringReversal Trs (TrsNonterminationProof k)
Loop
Fields rewriteSequence :: RewriteSequence substitution :: Substitution context :: Context

Instances

Instances details

Generic (TrsNonterminationProof k) Source #
Instance details Defined in TPDB.CPF.Proof.Type Associated Types type Rep (TrsNonterminationProof k) :: Type -> Type # Methods from :: TrsNonterminationProof k -> Rep (TrsNonterminationProof k) x # to :: Rep (TrsNonterminationProof k) x -> TrsNonterminationProof k #
Eq (TrsNonterminationProof k) Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: TrsNonterminationProof k -> TrsNonterminationProof k -> Bool # (/=) :: TrsNonterminationProof k -> TrsNonterminationProof k -> Bool #
XmlContent (TrsNonterminationProof 'Relative) Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: TrsNonterminationProof 'Relative -> [Node] Source # parseContents :: Cursor -> [TrsNonterminationProof 'Relative] Source #
XmlContent (TrsNonterminationProof 'Standard) Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: TrsNonterminationProof 'Standard -> [Node] Source # parseContents :: Cursor -> [TrsNonterminationProof 'Standard] Source #
type Rep (TrsNonterminationProof k) Source #
Instance details Defined in TPDB.CPF.Proof.Type type Rep (TrsNonterminationProof k) = D1 ('MetaData "TrsNonterminationProof" "TPDB.CPF.Proof.Type" "tpdb-2.7.3-CgDLIzMWhg29yaLLziq7QN" 'False) ((C1 ('MetaCons "VariableConditionViolated" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TNP_RuleRemoval" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Trs) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 (TrsNonterminationProof k)))) :+: (C1 ('MetaCons "TNP_StringReversal" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Trs) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 (TrsNonterminationProof k))) :+: C1 ('MetaCons "Loop" 'PrefixI 'True) (S1 ('MetaSel ('Just "rewriteSequence") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 RewriteSequence) :: (S1 ('MetaSel ('Just "substitution") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Substitution) :: S1 ('MetaSel ('Just "context") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Context)))))

data ComplexityProof Source #

Constructors

ComplexityProofFIXME ()

Instances

Instances details

Generic ComplexityProof Source #
Instance details Defined in TPDB.CPF.Proof.Type Associated Types type Rep ComplexityProof :: Type -> Type # Methods from :: ComplexityProof -> Rep ComplexityProof x # to :: Rep ComplexityProof x -> ComplexityProof #
Eq ComplexityProof Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: ComplexityProof -> ComplexityProof -> Bool # (/=) :: ComplexityProof -> ComplexityProof -> Bool #
type Rep ComplexityProof Source #
Instance details Defined in TPDB.CPF.Proof.Type type Rep ComplexityProof = D1 ('MetaData "ComplexityProof" "TPDB.CPF.Proof.Type" "tpdb-2.7.3-CgDLIzMWhg29yaLLziq7QN" 'False) (C1 ('MetaCons "ComplexityProofFIXME" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 ())))

data ACTerminationProof Source #

Constructors

ACTerminationProofFIXME ()

Instances

Instances details

Generic ACTerminationProof Source #
Instance details Defined in TPDB.CPF.Proof.Type Associated Types type Rep ACTerminationProof :: Type -> Type # Methods from :: ACTerminationProof -> Rep ACTerminationProof x # to :: Rep ACTerminationProof x -> ACTerminationProof #
Eq ACTerminationProof Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: ACTerminationProof -> ACTerminationProof -> Bool # (/=) :: ACTerminationProof -> ACTerminationProof -> Bool #
type Rep ACTerminationProof Source #
Instance details Defined in TPDB.CPF.Proof.Type type Rep ACTerminationProof = D1 ('MetaData "ACTerminationProof" "TPDB.CPF.Proof.Type" "tpdb-2.7.3-CgDLIzMWhg29yaLLziq7QN" 'False) (C1 ('MetaCons "ACTerminationProofFIXME" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 ())))

data DPS Source #

Constructors

DPS [Rule (Term Identifier Symbol)]

Instances

Instances details

Eq DPS Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: DPS -> DPS -> Bool # (/=) :: DPS -> DPS -> Bool #
XmlContent DPS Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: DPS -> [Node] Source # parseContents :: Cursor -> [DPS] Source #

data RewriteSequence Source #

Constructors

RewriteSequence (Term Identifier Symbol) [RewriteStep]

Instances

Instances details

Generic RewriteSequence Source #
Instance details Defined in TPDB.CPF.Proof.Type Associated Types type Rep RewriteSequence :: Type -> Type # Methods from :: RewriteSequence -> Rep RewriteSequence x # to :: Rep RewriteSequence x -> RewriteSequence #
Eq RewriteSequence Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: RewriteSequence -> RewriteSequence -> Bool # (/=) :: RewriteSequence -> RewriteSequence -> Bool #
XmlContent RewriteSequence Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: RewriteSequence -> [Node] Source # parseContents :: Cursor -> [RewriteSequence] Source #
type Rep RewriteSequence Source #
Instance details Defined in TPDB.CPF.Proof.Type type Rep RewriteSequence = D1 ('MetaData "RewriteSequence" "TPDB.CPF.Proof.Type" "tpdb-2.7.3-CgDLIzMWhg29yaLLziq7QN" 'False) (C1 ('MetaCons "RewriteSequence" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 (Term Identifier Symbol)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 [RewriteStep])))

data Context Source #

Constructors

Box
FunContext
Fields fc_symbol :: Symbol fc_before :: [Term Identifier Symbol] fc_here :: Context fc_after :: [Term Identifier Symbol]

Instances

Instances details

Generic Context Source #
Instance details Defined in TPDB.CPF.Proof.Type Associated Types type Rep Context :: Type -> Type # Methods from :: Context -> Rep Context x # to :: Rep Context x -> Context #
Eq Context Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: Context -> Context -> Bool # (/=) :: Context -> Context -> Bool #
XmlContent Context Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: Context -> [Node] Source # parseContents :: Cursor -> [Context] Source #
type Rep Context Source #
Instance details Defined in TPDB.CPF.Proof.Type type Rep Context = D1 ('MetaData "Context" "TPDB.CPF.Proof.Type" "tpdb-2.7.3-CgDLIzMWhg29yaLLziq7QN" 'False) (C1 ('MetaCons "Box" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FunContext" 'PrefixI 'True) ((S1 ('MetaSel ('Just "fc_symbol") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Symbol) :: S1 ('MetaSel ('Just "fc_before") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 [Term Identifier Symbol])) :: (S1 ('MetaSel ('Just "fc_here") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Context) :*: S1 ('MetaSel ('Just "fc_after") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 [Term Identifier Symbol]))))

data RewriteStep Source #

Constructors

RewriteStep
Fields rs_position :: Position rs_rule :: Rule (Term Identifier Symbol) rs_term :: Term Identifier Symbol

Instances

Instances details

Generic RewriteStep Source #
Instance details Defined in TPDB.CPF.Proof.Type Associated Types type Rep RewriteStep :: Type -> Type # Methods from :: RewriteStep -> Rep RewriteStep x # to :: Rep RewriteStep x -> RewriteStep #
Eq RewriteStep Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: RewriteStep -> RewriteStep -> Bool # (/=) :: RewriteStep -> RewriteStep -> Bool #
XmlContent RewriteStep Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: RewriteStep -> [Node] Source # parseContents :: Cursor -> [RewriteStep] Source #
type Rep RewriteStep Source #
Instance details Defined in TPDB.CPF.Proof.Type type Rep RewriteStep = D1 ('MetaData "RewriteStep" "TPDB.CPF.Proof.Type" "tpdb-2.7.3-CgDLIzMWhg29yaLLziq7QN" 'False) (C1 ('MetaCons "RewriteStep" 'PrefixI 'True) (S1 ('MetaSel ('Just "rs_position") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Position) :: (S1 ('MetaSel ('Just "rs_rule") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 (Rule (Term Identifier Symbol))) :: S1 ('MetaSel ('Just "rs_term") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 (Term Identifier Symbol)))))

data SubstEntry Source #

Constructors

SubstEntry Identifier (Term Identifier Symbol)

Instances

Instances details

Generic SubstEntry Source #
Instance details Defined in TPDB.CPF.Proof.Type Associated Types type Rep SubstEntry :: Type -> Type # Methods from :: SubstEntry -> Rep SubstEntry x # to :: Rep SubstEntry x -> SubstEntry #
Eq SubstEntry Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: SubstEntry -> SubstEntry -> Bool # (/=) :: SubstEntry -> SubstEntry -> Bool #
XmlContent SubstEntry Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: SubstEntry -> [Node] Source # parseContents :: Cursor -> [SubstEntry] Source #
type Rep SubstEntry Source #
Instance details Defined in TPDB.CPF.Proof.Type type Rep SubstEntry = D1 ('MetaData "SubstEntry" "TPDB.CPF.Proof.Type" "tpdb-2.7.3-CgDLIzMWhg29yaLLziq7QN" 'False) (C1 ('MetaCons "SubstEntry" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Identifier) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 (Term Identifier Symbol))))

data OrderingConstraintProof Source #

Constructors

OCPRedPair RedPair

Instances

Instances details

Generic OrderingConstraintProof Source #
Instance details Defined in TPDB.CPF.Proof.Type Associated Types type Rep OrderingConstraintProof :: Type -> Type # Methods from :: OrderingConstraintProof -> Rep OrderingConstraintProof x # to :: Rep OrderingConstraintProof x -> OrderingConstraintProof #
Eq OrderingConstraintProof Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: OrderingConstraintProof -> OrderingConstraintProof -> Bool # (/=) :: OrderingConstraintProof -> OrderingConstraintProof -> Bool #
XmlContent OrderingConstraintProof Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: OrderingConstraintProof -> [Node] Source # parseContents :: Cursor -> [OrderingConstraintProof] Source #
type Rep OrderingConstraintProof Source #
Instance details Defined in TPDB.CPF.Proof.Type type Rep OrderingConstraintProof = D1 ('MetaData "OrderingConstraintProof" "TPDB.CPF.Proof.Type" "tpdb-2.7.3-CgDLIzMWhg29yaLLziq7QN" 'False) (C1 ('MetaCons "OCPRedPair" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 RedPair)))

data DpProof Source #

Constructors

PIsEmpty
RedPairProc
Fields rppMono :: Mono rppOrderingConstraintProof :: OrderingConstraintProof rppDps :: DPS rppTrs :: Maybe Trs 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

Instances details

Generic DpProof Source #
Instance details Defined in TPDB.CPF.Proof.Type Associated Types type Rep DpProof :: Type -> Type # Methods from :: DpProof -> Rep DpProof x # to :: Rep DpProof x -> DpProof #
Eq DpProof Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: DpProof -> DpProof -> Bool # (/=) :: DpProof -> DpProof -> Bool #
XmlContent DpProof Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: DpProof -> [Node] Source # parseContents :: Cursor -> [DpProof] Source #
type Rep DpProof Source #
Instance details Defined in TPDB.CPF.Proof.Type type Rep DpProof = D1 ('MetaData "DpProof" "TPDB.CPF.Proof.Type" "tpdb-2.7.3-CgDLIzMWhg29yaLLziq7QN" 'False) ((C1 ('MetaCons "PIsEmpty" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RedPairProc" 'PrefixI 'True) ((S1 ('MetaSel ('Just "rppMono") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Mono) :: (S1 ('MetaSel ('Just "rppOrderingConstraintProof") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 OrderingConstraintProof) :: S1 ('MetaSel ('Just "rppDps") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 DPS))) :: (S1 ('MetaSel ('Just "rppTrs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 (Maybe Trs)) :: (S1 ('MetaSel ('Just "rppUsableRules") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 (Maybe DPS)) :: S1 ('MetaSel ('Just "rppDpProof") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 DpProof))))) :+: (C1 ('MetaCons "DepGraphProc" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 [DepGraphComponent])) :+: (C1 ('MetaCons "SemLabProc" 'PrefixI 'True) ((S1 ('MetaSel ('Just "slpModel") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Model) :: S1 ('MetaSel ('Just "slpDps") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 DPS)) :: (S1 ('MetaSel ('Just "slpTrs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 DPS) :: S1 ('MetaSel ('Just "slpDpProof") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 DpProof))) :+: C1 ('MetaCons "UnlabProc" 'PrefixI 'True) (S1 ('MetaSel ('Just "ulpDps") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 DPS) :: (S1 ('MetaSel ('Just "ulpTrs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 DPS) :: S1 ('MetaSel ('Just "ulpDpProof") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 DpProof))))))

data Model Source #

Constructors

FiniteModel Int [Interpret]
RootLabeling

Instances

Instances details

Generic Model Source #
Instance details Defined in TPDB.CPF.Proof.Type Associated Types type Rep Model :: Type -> Type # Methods from :: Model -> Rep Model x # to :: Rep Model x -> Model #
Eq Model Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: Model -> Model -> Bool # (/=) :: Model -> Model -> Bool #
XmlContent Model Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: Model -> [Node] Source # parseContents :: Cursor -> [Model] Source #
type Rep Model Source #
Instance details Defined in TPDB.CPF.Proof.Type type Rep Model = D1 ('MetaData "Model" "TPDB.CPF.Proof.Type" "tpdb-2.7.3-CgDLIzMWhg29yaLLziq7QN" 'False) (C1 ('MetaCons "FiniteModel" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 [Interpret])) :+: C1 ('MetaCons "RootLabeling" 'PrefixI 'False) (U1 :: Type -> Type))

data Bounds_Type Source #

Constructors

Roof
Match

Instances

Instances details

Generic Bounds_Type Source #
Instance details Defined in TPDB.CPF.Proof.Type Associated Types type Rep Bounds_Type :: Type -> Type # Methods from :: Bounds_Type -> Rep Bounds_Type x # to :: Rep Bounds_Type x -> Bounds_Type #
Eq Bounds_Type Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: Bounds_Type -> Bounds_Type -> Bool # (/=) :: Bounds_Type -> Bounds_Type -> Bool #
XmlContent Bounds_Type Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: Bounds_Type -> [Node] Source # parseContents :: Cursor -> [Bounds_Type] Source #
type Rep Bounds_Type Source #
Instance details Defined in TPDB.CPF.Proof.Type type Rep Bounds_Type = D1 ('MetaData "Bounds_Type" "TPDB.CPF.Proof.Type" "tpdb-2.7.3-CgDLIzMWhg29yaLLziq7QN" 'False) (C1 ('MetaCons "Roof" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Match" 'PrefixI 'False) (U1 :: Type -> Type))

data TreeAutomaton Source #

Constructors

TreeAutomaton
Fields ta_finalStates :: [State] ta_transitions :: [Transition]

Instances

Instances details

Generic TreeAutomaton Source #
Instance details Defined in TPDB.CPF.Proof.Type Associated Types type Rep TreeAutomaton :: Type -> Type # Methods from :: TreeAutomaton -> Rep TreeAutomaton x # to :: Rep TreeAutomaton x -> TreeAutomaton #
Eq TreeAutomaton Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: TreeAutomaton -> TreeAutomaton -> Bool # (/=) :: TreeAutomaton -> TreeAutomaton -> Bool #
XmlContent TreeAutomaton Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: TreeAutomaton -> [Node] Source # parseContents :: Cursor -> [TreeAutomaton] Source #
type Rep TreeAutomaton Source #
Instance details Defined in TPDB.CPF.Proof.Type type Rep TreeAutomaton = D1 ('MetaData "TreeAutomaton" "TPDB.CPF.Proof.Type" "tpdb-2.7.3-CgDLIzMWhg29yaLLziq7QN" 'False) (C1 ('MetaCons "TreeAutomaton" 'PrefixI 'True) (S1 ('MetaSel ('Just "ta_finalStates") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 [State]) :*: S1 ('MetaSel ('Just "ta_transitions") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 [Transition])))

data Criterion Source #

Constructors

Compatibility

Instances

Instances details

Generic Criterion Source #
Instance details Defined in TPDB.CPF.Proof.Type Associated Types type Rep Criterion :: Type -> Type # Methods from :: Criterion -> Rep Criterion x # to :: Rep Criterion x -> Criterion #
Eq Criterion Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: Criterion -> Criterion -> Bool # (/=) :: Criterion -> Criterion -> Bool #
XmlContent Criterion Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: Criterion -> [Node] Source # parseContents :: Cursor -> [Criterion] Source #
type Rep Criterion Source #
Instance details Defined in TPDB.CPF.Proof.Type type Rep Criterion = D1 ('MetaData "Criterion" "TPDB.CPF.Proof.Type" "tpdb-2.7.3-CgDLIzMWhg29yaLLziq7QN" 'False) (C1 ('MetaCons "Compatibility" 'PrefixI 'False) (U1 :: Type -> Type))

data Transition Source #

Constructors

Transition
Fields transition_lhs :: Transition_Lhs transition_rhs :: State

Instances

Instances details

Generic Transition Source #
Instance details Defined in TPDB.CPF.Proof.Type Associated Types type Rep Transition :: Type -> Type # Methods from :: Transition -> Rep Transition x # to :: Rep Transition x -> Transition #
Eq Transition Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: Transition -> Transition -> Bool # (/=) :: Transition -> Transition -> Bool #
XmlContent Transition Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: Transition -> [Node] Source # parseContents :: Cursor -> [Transition] Source #
type Rep Transition Source #
Instance details Defined in TPDB.CPF.Proof.Type type Rep Transition = D1 ('MetaData "Transition" "TPDB.CPF.Proof.Type" "tpdb-2.7.3-CgDLIzMWhg29yaLLziq7QN" 'False) (C1 ('MetaCons "Transition" 'PrefixI 'True) (S1 ('MetaSel ('Just "transition_lhs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Transition_Lhs) :*: S1 ('MetaSel ('Just "transition_rhs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 State)))

data Transition_Lhs Source #

Constructors

Transition_Symbol
Fields tr_symbol :: Symbol tr_height :: Int tr_arguments :: [State]
Transition_Epsilon State

Instances

Instances details

Generic Transition_Lhs Source #
Instance details Defined in TPDB.CPF.Proof.Type Associated Types type Rep Transition_Lhs :: Type -> Type # Methods from :: Transition_Lhs -> Rep Transition_Lhs x # to :: Rep Transition_Lhs x -> Transition_Lhs #
Eq Transition_Lhs Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: Transition_Lhs -> Transition_Lhs -> Bool # (/=) :: Transition_Lhs -> Transition_Lhs -> Bool #
XmlContent Transition_Lhs Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: Transition_Lhs -> [Node] Source # parseContents :: Cursor -> [Transition_Lhs] Source #
type Rep Transition_Lhs Source #
Instance details Defined in TPDB.CPF.Proof.Type type Rep Transition_Lhs = D1 ('MetaData "Transition_Lhs" "TPDB.CPF.Proof.Type" "tpdb-2.7.3-CgDLIzMWhg29yaLLziq7QN" 'False) (C1 ('MetaCons "Transition_Symbol" 'PrefixI 'True) (S1 ('MetaSel ('Just "tr_symbol") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Symbol) :: (S1 ('MetaSel ('Just "tr_height") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Int) :: S1 ('MetaSel ('Just "tr_arguments") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 [State]))) :+: C1 ('MetaCons "Transition_Epsilon" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 State)))

data Interpret Source #

Constructors

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

Instances

Instances details

Generic Interpret Source #
Instance details Defined in TPDB.CPF.Proof.Type Associated Types type Rep Interpret :: Type -> Type # Methods from :: Interpret -> Rep Interpret x # to :: Rep Interpret x -> Interpret #
Eq Interpret Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: Interpret -> Interpret -> Bool # (/=) :: Interpret -> Interpret -> Bool #
XmlContent Interpret Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: Interpret -> [Node] Source # parseContents :: Cursor -> [Interpret] Source #
type Rep Interpret Source #
Instance details Defined in TPDB.CPF.Proof.Type type Rep Interpret = D1 ('MetaData "Interpret" "TPDB.CPF.Proof.Type" "tpdb-2.7.3-CgDLIzMWhg29yaLLziq7QN" 'False) (C1 ('MetaCons "Interpret" 'PrefixI 'True) (S1 ('MetaSel ('Just "symbol") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Symbol) :: (S1 ('MetaSel ('Just "arity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Int) :: S1 ('MetaSel ('Just "value") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Value))))

data Mono Source #

Constructors

Weak
Strict

Instances

Instances details

Generic Mono Source #
Instance details Defined in TPDB.CPF.Proof.Type Associated Types type Rep Mono :: Type -> Type # Methods from :: Mono -> Rep Mono x # to :: Rep Mono x -> Mono #
Eq Mono Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: Mono -> Mono -> Bool # (/=) :: Mono -> Mono -> Bool #
type Rep Mono Source #
Instance details Defined in TPDB.CPF.Proof.Type type Rep Mono = D1 ('MetaData "Mono" "TPDB.CPF.Proof.Type" "tpdb-2.7.3-CgDLIzMWhg29yaLLziq7QN" 'False) (C1 ('MetaCons "Weak" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Strict" 'PrefixI 'False) (U1 :: Type -> Type))

data DepGraphComponent Source #

Constructors

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

Instances

Instances details

Generic DepGraphComponent Source #
Instance details Defined in TPDB.CPF.Proof.Type Associated Types type Rep DepGraphComponent :: Type -> Type # Methods from :: DepGraphComponent -> Rep DepGraphComponent x # to :: Rep DepGraphComponent x -> DepGraphComponent #
Eq DepGraphComponent Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: DepGraphComponent -> DepGraphComponent -> Bool # (/=) :: DepGraphComponent -> DepGraphComponent -> Bool #
XmlContent DepGraphComponent Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: DepGraphComponent -> [Node] Source # parseContents :: Cursor -> [DepGraphComponent] Source #
type Rep DepGraphComponent Source #
Instance details Defined in TPDB.CPF.Proof.Type type Rep DepGraphComponent = D1 ('MetaData "DepGraphComponent" "TPDB.CPF.Proof.Type" "tpdb-2.7.3-CgDLIzMWhg29yaLLziq7QN" 'False) (C1 ('MetaCons "DepGraphComponent" 'PrefixI 'True) (S1 ('MetaSel ('Just "dgcRealScc") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Bool) :: (S1 ('MetaSel ('Just "dgcDps") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 DPS) :: S1 ('MetaSel ('Just "dgcDpProof") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 DpProof))))

data RedPair Source #

Constructors

RPInterpretation Interpretation
RPPathOrder PathOrder

Instances

Instances details

Generic RedPair Source #
Instance details Defined in TPDB.CPF.Proof.Type Associated Types type Rep RedPair :: Type -> Type # Methods from :: RedPair -> Rep RedPair x # to :: Rep RedPair x -> RedPair #
Eq RedPair Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: RedPair -> RedPair -> Bool # (/=) :: RedPair -> RedPair -> Bool #
XmlContent RedPair Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: RedPair -> [Node] Source # parseContents :: Cursor -> [RedPair] Source #
type Rep RedPair Source #
Instance details Defined in TPDB.CPF.Proof.Type type Rep RedPair = D1 ('MetaData "RedPair" "TPDB.CPF.Proof.Type" "tpdb-2.7.3-CgDLIzMWhg29yaLLziq7QN" 'False) (C1 ('MetaCons "RPInterpretation" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Interpretation)) :+: C1 ('MetaCons "RPPathOrder" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 PathOrder)))

data Interpretation Source #

Constructors

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

Instances

Instances details

Generic Interpretation Source #
Instance details Defined in TPDB.CPF.Proof.Type Associated Types type Rep Interpretation :: Type -> Type # Methods from :: Interpretation -> Rep Interpretation x # to :: Rep Interpretation x -> Interpretation #
Eq Interpretation Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: Interpretation -> Interpretation -> Bool # (/=) :: Interpretation -> Interpretation -> Bool #
XmlContent Interpretation Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: Interpretation -> [Node] Source # parseContents :: Cursor -> [Interpretation] Source #
type Rep Interpretation Source #
Instance details Defined in TPDB.CPF.Proof.Type type Rep Interpretation = D1 ('MetaData "Interpretation" "TPDB.CPF.Proof.Type" "tpdb-2.7.3-CgDLIzMWhg29yaLLziq7QN" 'False) (C1 ('MetaCons "Interpretation" 'PrefixI 'True) (S1 ('MetaSel ('Just "interpretation_type") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Interpretation_Type) :*: S1 ('MetaSel ('Just "interprets") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 [Interpret])))

data PathOrder Source #

Constructors

PathOrder [PrecedenceEntry] [ArgumentFilterEntry]

Instances

Instances details

Generic PathOrder Source #
Instance details Defined in TPDB.CPF.Proof.Type Associated Types type Rep PathOrder :: Type -> Type # Methods from :: PathOrder -> Rep PathOrder x # to :: Rep PathOrder x -> PathOrder #
Eq PathOrder Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: PathOrder -> PathOrder -> Bool # (/=) :: PathOrder -> PathOrder -> Bool #
XmlContent PathOrder Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: PathOrder -> [Node] Source # parseContents :: Cursor -> [PathOrder] Source #
type Rep PathOrder Source #
Instance details Defined in TPDB.CPF.Proof.Type type Rep PathOrder = D1 ('MetaData "PathOrder" "TPDB.CPF.Proof.Type" "tpdb-2.7.3-CgDLIzMWhg29yaLLziq7QN" 'False) (C1 ('MetaCons "PathOrder" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 [PrecedenceEntry]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 [ArgumentFilterEntry])))

data Interpretation_Type Source #

Constructors

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

Instances

Instances details

Generic Interpretation_Type Source #
Instance details Defined in TPDB.CPF.Proof.Type Associated Types type Rep Interpretation_Type :: Type -> Type # Methods from :: Interpretation_Type -> Rep Interpretation_Type x # to :: Rep Interpretation_Type x -> Interpretation_Type #
Eq Interpretation_Type Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: Interpretation_Type -> Interpretation_Type -> Bool # (/=) :: Interpretation_Type -> Interpretation_Type -> Bool #
XmlContent Interpretation_Type Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: Interpretation_Type -> [Node] Source # parseContents :: Cursor -> [Interpretation_Type] Source #
type Rep Interpretation_Type Source #
Instance details Defined in TPDB.CPF.Proof.Type type Rep Interpretation_Type = D1 ('MetaData "Interpretation_Type" "TPDB.CPF.Proof.Type" "tpdb-2.7.3-CgDLIzMWhg29yaLLziq7QN" 'False) (C1 ('MetaCons "Matrix_Interpretation" 'PrefixI 'True) (S1 ('MetaSel ('Just "domain") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Domain) :: (S1 ('MetaSel ('Just "dimension") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Int) :: S1 ('MetaSel ('Just "strictDimension") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Int))))

data Domain Source #

Constructors

Naturals
Rationals Rational
Arctic Domain
Tropical Domain

Instances

Instances details

Generic Domain Source #
Instance details Defined in TPDB.CPF.Proof.Type Associated Types type Rep Domain :: Type -> Type # Methods from :: Domain -> Rep Domain x # to :: Rep Domain x -> Domain #
Eq Domain Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: Domain -> Domain -> Bool # (/=) :: Domain -> Domain -> Bool #
XmlContent Domain Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: Domain -> [Node] Source # parseContents :: Cursor -> [Domain] Source #
type Rep Domain Source #
Instance details Defined in TPDB.CPF.Proof.Type type Rep Domain = D1 ('MetaData "Domain" "TPDB.CPF.Proof.Type" "tpdb-2.7.3-CgDLIzMWhg29yaLLziq7QN" 'False) ((C1 ('MetaCons "Naturals" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Rationals" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Rational))) :+: (C1 ('MetaCons "Arctic" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Domain)) :+: C1 ('MetaCons "Tropical" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Domain))))

data Polynomial Source #

Constructors

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

Instances

Instances details

Generic Polynomial Source #
Instance details Defined in TPDB.CPF.Proof.Type Associated Types type Rep Polynomial :: Type -> Type # Methods from :: Polynomial -> Rep Polynomial x # to :: Rep Polynomial x -> Polynomial #
Eq Polynomial Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: Polynomial -> Polynomial -> Bool # (/=) :: Polynomial -> Polynomial -> Bool #
XmlContent Polynomial Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: Polynomial -> [Node] Source # parseContents :: Cursor -> [Polynomial] Source #
type Rep Polynomial Source #
Instance details Defined in TPDB.CPF.Proof.Type type Rep Polynomial = D1 ('MetaData "Polynomial" "TPDB.CPF.Proof.Type" "tpdb-2.7.3-CgDLIzMWhg29yaLLziq7QN" 'False) ((C1 ('MetaCons "Sum" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 [Polynomial])) :+: C1 ('MetaCons "Product" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 [Polynomial]))) :+: (C1 ('MetaCons "Polynomial_Coefficient" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Coefficient)) :+: C1 ('MetaCons "Polynomial_Variable" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Text))))

data ArithFunction Source #

Constructors

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

Instances

Instances details

Generic ArithFunction Source #
Instance details Defined in TPDB.CPF.Proof.Type Associated Types type Rep ArithFunction :: Type -> Type # Methods from :: ArithFunction -> Rep ArithFunction x # to :: Rep ArithFunction x -> ArithFunction #
Eq ArithFunction Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: ArithFunction -> ArithFunction -> Bool # (/=) :: ArithFunction -> ArithFunction -> Bool #
XmlContent ArithFunction Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: ArithFunction -> [Node] Source # parseContents :: Cursor -> [ArithFunction] Source #
type Rep ArithFunction Source #
Instance details Defined in TPDB.CPF.Proof.Type type Rep ArithFunction = D1 ('MetaData "ArithFunction" "TPDB.CPF.Proof.Type" "tpdb-2.7.3-CgDLIzMWhg29yaLLziq7QN" 'False) ((C1 ('MetaCons "AFNatural" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Integer)) :+: (C1 ('MetaCons "AFVariable" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Integer)) :+: C1 ('MetaCons "AFSum" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 [ArithFunction])))) :+: ((C1 ('MetaCons "AFProduct" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 [ArithFunction])) :+: C1 ('MetaCons "AFMin" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 [ArithFunction]))) :+: (C1 ('MetaCons "AFMax" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 [ArithFunction])) :+: C1 ('MetaCons "AFIfEqual" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 ArithFunction) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 ArithFunction)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 ArithFunction) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 ArithFunction))))))

data Coefficient Source #

Constructors

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

Instances

Instances details

Eq Coefficient Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: Coefficient -> Coefficient -> Bool # (/=) :: Coefficient -> Coefficient -> Bool #
XmlContent Coefficient Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: Coefficient -> [Node] Source # parseContents :: Cursor -> [Coefficient] Source #

data Label Source #

Constructors

LblNumber [Integer]
LblSymbol [Symbol]

Instances

Instances details

Generic Label Source #
Instance details Defined in TPDB.CPF.Proof.Type Associated Types type Rep Label :: Type -> Type # Methods from :: Label -> Rep Label x # to :: Rep Label x -> Label #
Eq Label Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: Label -> Label -> Bool # (/=) :: Label -> Label -> Bool #
Ord Label Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods compare :: Label -> Label -> Ordering # (<) :: Label -> Label -> Bool # (<=) :: Label -> Label -> Bool # (>) :: Label -> Label -> Bool # (>=) :: Label -> Label -> Bool # max :: Label -> Label -> Label # min :: Label -> Label -> Label #
Hashable Label Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods hashWithSalt :: Int -> Label -> Int # hash :: Label -> Int #
Pretty Label Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods pretty :: Label -> Doc ann # prettyList :: [Label] -> Doc ann #
XmlContent Label Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: Label -> [Node] Source # parseContents :: Cursor -> [Label] Source #
type Rep Label Source #
Instance details Defined in TPDB.CPF.Proof.Type type Rep Label = D1 ('MetaData "Label" "TPDB.CPF.Proof.Type" "tpdb-2.7.3-CgDLIzMWhg29yaLLziq7QN" 'False) (C1 ('MetaCons "LblNumber" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 [Integer])) :+: C1 ('MetaCons "LblSymbol" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 [Symbol])))

data Exotic Source #

Constructors

Minus_Infinite
E_Integer Integer
E_Rational Rational
Plus_Infinite

Instances

Instances details

Generic Exotic Source #
Instance details Defined in TPDB.CPF.Proof.Type Associated Types type Rep Exotic :: Type -> Type # Methods from :: Exotic -> Rep Exotic x # to :: Rep Exotic x -> Exotic #
Eq Exotic Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: Exotic -> Exotic -> Bool # (/=) :: Exotic -> Exotic -> Bool #
XmlContent Exotic Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: Exotic -> [Node] Source # parseContents :: Cursor -> [Exotic] Source #
type Rep Exotic Source #
Instance details Defined in TPDB.CPF.Proof.Type type Rep Exotic = D1 ('MetaData "Exotic" "TPDB.CPF.Proof.Type" "tpdb-2.7.3-CgDLIzMWhg29yaLLziq7QN" 'False) ((C1 ('MetaCons "Minus_Infinite" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "E_Integer" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Integer))) :+: (C1 ('MetaCons "E_Rational" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Rational)) :+: C1 ('MetaCons "Plus_Infinite" 'PrefixI 'False) (U1 :: Type -> Type)))

class ToExotic a where Source #

Methods

toExotic :: a -> Exotic Source #

data PrecedenceEntry Source #

Constructors

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

Instances

Instances details

Generic PrecedenceEntry Source #
Instance details Defined in TPDB.CPF.Proof.Type Associated Types type Rep PrecedenceEntry :: Type -> Type # Methods from :: PrecedenceEntry -> Rep PrecedenceEntry x # to :: Rep PrecedenceEntry x -> PrecedenceEntry #
Eq PrecedenceEntry Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: PrecedenceEntry -> PrecedenceEntry -> Bool # (/=) :: PrecedenceEntry -> PrecedenceEntry -> Bool #
XmlContent PrecedenceEntry Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: PrecedenceEntry -> [Node] Source # parseContents :: Cursor -> [PrecedenceEntry] Source #
type Rep PrecedenceEntry Source #
Instance details Defined in TPDB.CPF.Proof.Type type Rep PrecedenceEntry = D1 ('MetaData "PrecedenceEntry" "TPDB.CPF.Proof.Type" "tpdb-2.7.3-CgDLIzMWhg29yaLLziq7QN" 'False) (C1 ('MetaCons "PrecedenceEntry" 'PrefixI 'True) (S1 ('MetaSel ('Just "peSymbol") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Symbol) :: (S1 ('MetaSel ('Just "peArity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Int) :: S1 ('MetaSel ('Just "pePrecedence") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Integer))))

data ArgumentFilterEntry Source #

Constructors

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

Instances

Instances details

Generic ArgumentFilterEntry Source #
Instance details Defined in TPDB.CPF.Proof.Type Associated Types type Rep ArgumentFilterEntry :: Type -> Type # Methods from :: ArgumentFilterEntry -> Rep ArgumentFilterEntry x # to :: Rep ArgumentFilterEntry x -> ArgumentFilterEntry #
Eq ArgumentFilterEntry Source #
Instance details Defined in TPDB.CPF.Proof.Type Methods (==) :: ArgumentFilterEntry -> ArgumentFilterEntry -> Bool # (/=) :: ArgumentFilterEntry -> ArgumentFilterEntry -> Bool #
XmlContent ArgumentFilterEntry Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: ArgumentFilterEntry -> [Node] Source # parseContents :: Cursor -> [ArgumentFilterEntry] Source #
type Rep ArgumentFilterEntry Source #
Instance details Defined in TPDB.CPF.Proof.Type type Rep ArgumentFilterEntry = D1 ('MetaData "ArgumentFilterEntry" "TPDB.CPF.Proof.Type" "tpdb-2.7.3-CgDLIzMWhg29yaLLziq7QN" 'False) (C1 ('MetaCons "ArgumentFilterEntry" 'PrefixI 'True) (S1 ('MetaSel ('Just "afeSymbol") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Symbol) :: (S1 ('MetaSel ('Just "afeArity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Int) :: S1 ('MetaSel ('Just "afeFilter") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 (Either Int [Int])))))

ignoredOrigin :: Origin Source #

data Identifier Source #

Instances

Instances details

Show Identifier Source #
Instance details Defined in TPDB.Data.Identifier Methods showsPrec :: Int -> Identifier -> ShowS # show :: Identifier -> String # showList :: [Identifier] -> ShowS #
Eq Identifier Source #
Instance details Defined in TPDB.Data.Identifier Methods (==) :: Identifier -> Identifier -> Bool # (/=) :: Identifier -> Identifier -> Bool #
Ord Identifier Source #
Instance details Defined in TPDB.Data.Identifier Methods compare :: Identifier -> Identifier -> Ordering # (<) :: Identifier -> Identifier -> Bool # (<=) :: Identifier -> Identifier -> Bool # (>) :: Identifier -> Identifier -> Bool # (>=) :: Identifier -> Identifier -> Bool # max :: Identifier -> Identifier -> Identifier # min :: Identifier -> Identifier -> Identifier #
Hashable Identifier Source #
Instance details Defined in TPDB.Data.Identifier Methods hashWithSalt :: Int -> Identifier -> Int # hash :: Identifier -> Int #
Pretty Identifier Source #
Instance details Defined in TPDB.Plain.Write Methods pretty :: Identifier -> Doc ann # prettyList :: [Identifier] -> Doc ann #
Reader Identifier Source #
Instance details Defined in TPDB.Plain.Read Methods reader :: Parser Identifier Source #
XmlContent Identifier Source #	FIXME: move to separate module
Instance details Defined in TPDB.Data.Xml Methods toContents :: Identifier -> [Node] Source # parseContents :: Cursor -> [Identifier] Source #
Reader (SRS Identifier) Source #
Instance details Defined in TPDB.Plain.Read Methods reader :: Parser (SRS Identifier) Source #
Reader (TRS Identifier Identifier) Source #
Instance details Defined in TPDB.Plain.Read Methods reader :: Parser (TRS Identifier Identifier) Source #
(TermC v Identifier, Reader v) => Reader (Term v Identifier) Source #
Instance details Defined in TPDB.Plain.Read Methods reader :: Parser (Term v Identifier) Source #
XmlContent (TRS Identifier Symbol) Source #
Instance details Defined in TPDB.CPF.Proof.Write Methods toContents :: TRS Identifier Symbol -> [Node] Source # parseContents :: Cursor -> [TRS Identifier Symbol] Source #

type TES = TRS Identifier Identifier Source #

legacy stuff (used in matchbox)