{-# language StandaloneDeriving #-}
{-# language ExistentialQuantification #-}
{-# language DeriveDataTypeable #-}
{-# language OverloadedStrings #-}
module TPDB.CPF.Proof.Type
( module TPDB.CPF.Proof.Type
, Identifier
, TES
)
where
import TPDB.Data
import TPDB.Plain.Write ()
import Data.Typeable
import TPDB.Pretty
import Data.Text
import TPDB.Xml (XmlContent)
data CertificationProblem =
CertificationProblem { input :: CertificationProblemInput
, cpfVersion :: Text
, proof :: Proof
, origin :: Origin
}
deriving ( Typeable, Eq )
data Origin = ProofOrigin { tool :: Tool }
deriving ( Typeable, Eq )
ignoredOrigin = ProofOrigin { tool = Tool "ignored" "ignored" }
data Tool = Tool { name :: Text
, version :: Text
}
deriving ( Typeable, Eq )
data CertificationProblemInput
= TrsInput { trsinput_trs :: TRS Identifier Identifier }
| ComplexityInput { trsinput_trs :: TRS Identifier Identifier
, complexityMeasure :: ComplexityMeasure
, complexityClass :: ComplexityClass
}
| ACRewriteSystem { trsinput_trs :: TRS Identifier Identifier
, asymbols :: [ Identifier ]
, csymbols :: [ Identifier ]
}
deriving ( Typeable, Eq )
instance Pretty CertificationProblemInput where
pretty cpi = case cpi of
TrsInput { } ->
"TrsInput" <+> vcat [ "trs" <+> pretty (trsinput_trs cpi) ]
ComplexityInput { } ->
"ComplexityInput" <+> vcat
[ "trs" <+> pretty (trsinput_trs cpi)
, "measure" <+> text (show $ complexityMeasure cpi )
, "class" <+> text (show $ complexityClass cpi )
]
ACRewriteSystem { } ->
"ACRewritesystem" <+> vcat
[ "trs" <+> pretty (trsinput_trs cpi)
, "asymbols" <+> text (show $ asymbols cpi )
, "csymbols" <+> text (show $ csymbols cpi )
]
data Proof = TrsTerminationProof TrsTerminationProof
| TrsNonterminationProof TrsNonterminationProof
| RelativeTerminationProof TrsTerminationProof
| RelativeNonterminationProof TrsNonterminationProof
| ComplexityProof ComplexityProof
| ACTerminationProof ACTerminationProof
deriving ( Typeable, Eq )
data DPS = forall s . ( XmlContent s ,
Typeable s, Eq s )
=> DPS [ Rule (Term Identifier s) ]
deriving ( Typeable )
instance Eq DPS where x == y = error "instance Eq DPS"
data ComplexityProof = ComplexityProofFIXME ()
deriving ( Typeable, Eq )
data ComplexityMeasure
= DerivationalComplexity
| RuntimeComplexity
deriving ( Typeable, Eq, Show )
data ComplexityClass =
ComplexityClassPolynomial { degree :: Int }
deriving ( Typeable, Eq, Show )
data TrsNonterminationProof = TrsNonterminationProofFIXME ()
deriving ( Typeable, Eq )
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
}
| Bounds { trs :: TRS Identifier Identifier
, bounds_type :: Bounds_Type
, bounds_bound :: Int
, bounds_finalStates :: [ State ]
, bounds_closedTreeAutomaton :: ClosedTreeAutomaton
}
deriving ( Typeable, Eq )
data Bounds_Type = Roof | Match
deriving ( Typeable, Eq )
data ClosedTreeAutomaton = ClosedTreeAutomaton
{ cta_treeAutomaton :: TreeAutomaton
, cta_criterion :: Criterion
}
deriving ( Typeable, Eq )
data Criterion = Compatibility
deriving ( Typeable, Eq )
data TreeAutomaton = TreeAutomaton
{ ta_finalStates :: [ State ]
, ta_transitions :: [ Transition ]
}
deriving ( Typeable, Eq )
data State = State Int
deriving ( Typeable, Eq )
data Transition = Transition
{ transition_lhs :: Transition_Lhs
, transition_rhs :: [ State ]
}
deriving ( Typeable, Eq )
data Transition_Lhs
= Transition_Symbol { tr_symbol :: Symbol
, tr_height :: Int
, tr_arguments :: [ State ]
}
| Transition_Epsilon State
deriving ( Typeable, Eq )
data Model = FiniteModel Int [Interpret]
deriving ( Typeable, Eq )
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
}
deriving ( Typeable, Eq )
data DepGraphComponent =
DepGraphComponent { dgcRealScc :: Bool
, dgcDps :: DPS
, dgcDpProof :: DpProof
}
deriving ( Typeable, Eq )
data OrderingConstraintProof = OCPRedPair RedPair
deriving ( Typeable, Eq )
data RedPair = RPInterpretation Interpretation
| RPPathOrder PathOrder
deriving ( Typeable, Eq )
data Interpretation =
Interpretation { interpretation_type :: Interpretation_Type
, interprets :: [ Interpret ]
}
deriving ( Typeable, Eq )
data Interpretation_Type =
Matrix_Interpretation { domain :: Domain, dimension :: Int
, strictDimension :: Int
}
deriving ( Typeable, Eq )
data Domain = Naturals
| Rationals Rational
| Arctic Domain
| Tropical Domain
deriving ( Typeable, Eq )
data Interpret = Interpret
{ symbol :: Symbol , arity :: Int , value :: Value }
deriving ( Typeable, Eq )
data Value = Polynomial Polynomial
| ArithFunction ArithFunction
deriving ( Typeable, Eq )
data Polynomial = Sum [ Polynomial ]
| Product [ Polynomial ]
| Polynomial_Coefficient Coefficient
| Polynomial_Variable Text
deriving ( Typeable, Eq )
data ArithFunction = AFNatural Integer
| AFVariable Integer
| AFSum [ArithFunction]
| AFProduct [ArithFunction]
| AFMin [ArithFunction]
| AFMax [ArithFunction]
| AFIfEqual ArithFunction ArithFunction ArithFunction ArithFunction
deriving ( Typeable, Eq )
data Symbol = SymName Identifier
| SymSharp Symbol
| SymLabel Symbol Label
deriving ( Typeable, Eq )
data Label = LblNumber [Integer]
| LblSymbol [Symbol]
deriving ( Typeable, Eq )
data Coefficient = Vector [ Coefficient ]
| Matrix [ Coefficient ]
| forall a . (Eq a , XmlContent a
) => Coefficient_Coefficient a
deriving ( Typeable )
instance Eq Coefficient where x == y = error "instance Eq Coefficient"
data Exotic = Minus_Infinite | E_Integer Integer | E_Rational Rational | Plus_Infinite
deriving ( Typeable, Eq )
class ToExotic a where toExotic :: a -> Exotic
data PathOrder = PathOrder [PrecedenceEntry] [ArgumentFilterEntry]
deriving ( Typeable, Eq )
data PrecedenceEntry = PrecedenceEntry { peSymbol :: Symbol
, peArity :: Int
, pePrecedence :: Integer
}
deriving ( Typeable, Eq )
data ArgumentFilterEntry =
ArgumentFilterEntry { afeSymbol :: Symbol
, afeArity :: Int
, afeFilter :: Either Int [Int]
}
deriving ( Typeable, Eq )
data ACTerminationProof = ACTerminationProofFIXME ()
deriving ( Typeable, Eq )