{-# 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 { CertificationProblem -> CertificationProblemInput
input :: CertificationProblemInput
, CertificationProblem -> Text
cpfVersion :: Text
, CertificationProblem -> Proof
proof :: Proof
, CertificationProblem -> Origin
origin :: Origin
}
deriving ( Typeable, CertificationProblem -> CertificationProblem -> Bool
(CertificationProblem -> CertificationProblem -> Bool)
-> (CertificationProblem -> CertificationProblem -> Bool)
-> Eq CertificationProblem
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CertificationProblem -> CertificationProblem -> Bool
$c/= :: CertificationProblem -> CertificationProblem -> Bool
== :: CertificationProblem -> CertificationProblem -> Bool
$c== :: CertificationProblem -> CertificationProblem -> Bool
Eq )
data Origin = ProofOrigin { Origin -> Tool
tool :: Tool }
deriving ( Typeable, Origin -> Origin -> Bool
(Origin -> Origin -> Bool)
-> (Origin -> Origin -> Bool) -> Eq Origin
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Origin -> Origin -> Bool
$c/= :: Origin -> Origin -> Bool
== :: Origin -> Origin -> Bool
$c== :: Origin -> Origin -> Bool
Eq )
ignoredOrigin :: Origin
ignoredOrigin = ProofOrigin :: Tool -> Origin
ProofOrigin { tool :: Tool
tool = Text -> Text -> Tool
Tool Text
"ignored" Text
"ignored" }
data Tool = Tool { Tool -> Text
name :: Text
, Tool -> Text
version :: Text
}
deriving ( Typeable, Tool -> Tool -> Bool
(Tool -> Tool -> Bool) -> (Tool -> Tool -> Bool) -> Eq Tool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Tool -> Tool -> Bool
$c/= :: Tool -> Tool -> Bool
== :: Tool -> Tool -> Bool
$c== :: Tool -> Tool -> Bool
Eq )
data CertificationProblemInput
= TrsInput { CertificationProblemInput -> TRS Identifier Identifier
trsinput_trs :: TRS Identifier Identifier }
| ComplexityInput { trsinput_trs :: TRS Identifier Identifier
, CertificationProblemInput -> ComplexityMeasure
complexityMeasure :: ComplexityMeasure
, CertificationProblemInput -> ComplexityClass
complexityClass :: ComplexityClass
}
| ACRewriteSystem { trsinput_trs :: TRS Identifier Identifier
, CertificationProblemInput -> [Identifier]
asymbols :: [ Identifier ]
, CertificationProblemInput -> [Identifier]
csymbols :: [ Identifier ]
}
deriving ( Typeable, CertificationProblemInput -> CertificationProblemInput -> Bool
(CertificationProblemInput -> CertificationProblemInput -> Bool)
-> (CertificationProblemInput -> CertificationProblemInput -> Bool)
-> Eq CertificationProblemInput
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CertificationProblemInput -> CertificationProblemInput -> Bool
$c/= :: CertificationProblemInput -> CertificationProblemInput -> Bool
== :: CertificationProblemInput -> CertificationProblemInput -> Bool
$c== :: CertificationProblemInput -> CertificationProblemInput -> Bool
Eq )
instance Pretty CertificationProblemInput where
pretty :: CertificationProblemInput -> Doc ann
pretty CertificationProblemInput
cpi = case CertificationProblemInput
cpi of
TrsInput { } ->
Doc ann
"TrsInput" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat [ Doc ann
"trs" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> TRS Identifier Identifier -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (CertificationProblemInput -> TRS Identifier Identifier
trsinput_trs CertificationProblemInput
cpi) ]
ComplexityInput { } ->
Doc ann
"ComplexityInput" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat
[ Doc ann
"trs" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> TRS Identifier Identifier -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (CertificationProblemInput -> TRS Identifier Identifier
trsinput_trs CertificationProblemInput
cpi)
, Doc ann
"measure" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> String -> Doc ann
forall ann. String -> Doc ann
text (ComplexityMeasure -> String
forall a. Show a => a -> String
show (ComplexityMeasure -> String) -> ComplexityMeasure -> String
forall a b. (a -> b) -> a -> b
$ CertificationProblemInput -> ComplexityMeasure
complexityMeasure CertificationProblemInput
cpi )
, Doc ann
"class" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> String -> Doc ann
forall ann. String -> Doc ann
text (ComplexityClass -> String
forall a. Show a => a -> String
show (ComplexityClass -> String) -> ComplexityClass -> String
forall a b. (a -> b) -> a -> b
$ CertificationProblemInput -> ComplexityClass
complexityClass CertificationProblemInput
cpi )
]
ACRewriteSystem { } ->
Doc ann
"ACRewritesystem" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat
[ Doc ann
"trs" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> TRS Identifier Identifier -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (CertificationProblemInput -> TRS Identifier Identifier
trsinput_trs CertificationProblemInput
cpi)
, Doc ann
"asymbols" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> String -> Doc ann
forall ann. String -> Doc ann
text ([Identifier] -> String
forall a. Show a => a -> String
show ([Identifier] -> String) -> [Identifier] -> String
forall a b. (a -> b) -> a -> b
$ CertificationProblemInput -> [Identifier]
asymbols CertificationProblemInput
cpi )
, Doc ann
"csymbols" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> String -> Doc ann
forall ann. String -> Doc ann
text ([Identifier] -> String
forall a. Show a => a -> String
show ([Identifier] -> String) -> [Identifier] -> String
forall a b. (a -> b) -> a -> b
$ CertificationProblemInput -> [Identifier]
csymbols CertificationProblemInput
cpi )
]
data Proof = TrsTerminationProof TrsTerminationProof
| TrsNonterminationProof TrsNonterminationProof
| RelativeTerminationProof TrsTerminationProof
| RelativeNonterminationProof TrsNonterminationProof
| ComplexityProof ComplexityProof
| ACTerminationProof ACTerminationProof
deriving ( Typeable, Proof -> Proof -> Bool
(Proof -> Proof -> Bool) -> (Proof -> Proof -> Bool) -> Eq Proof
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Proof -> Proof -> Bool
$c/= :: Proof -> Proof -> Bool
== :: Proof -> Proof -> Bool
$c== :: Proof -> Proof -> Bool
Eq )
data DPS = forall s . ( XmlContent s ,
Typeable s, Eq s )
=> DPS [ Rule (Term Identifier s) ]
deriving ( Typeable )
instance Eq DPS where DPS
x == :: DPS -> DPS -> Bool
== DPS
y = String -> Bool
forall a. HasCallStack => String -> a
error String
"instance Eq DPS"
data ComplexityProof = ComplexityProofFIXME ()
deriving ( Typeable, ComplexityProof -> ComplexityProof -> Bool
(ComplexityProof -> ComplexityProof -> Bool)
-> (ComplexityProof -> ComplexityProof -> Bool)
-> Eq ComplexityProof
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ComplexityProof -> ComplexityProof -> Bool
$c/= :: ComplexityProof -> ComplexityProof -> Bool
== :: ComplexityProof -> ComplexityProof -> Bool
$c== :: ComplexityProof -> ComplexityProof -> Bool
Eq )
data ComplexityMeasure
= DerivationalComplexity
| RuntimeComplexity
deriving ( Typeable, ComplexityMeasure -> ComplexityMeasure -> Bool
(ComplexityMeasure -> ComplexityMeasure -> Bool)
-> (ComplexityMeasure -> ComplexityMeasure -> Bool)
-> Eq ComplexityMeasure
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ComplexityMeasure -> ComplexityMeasure -> Bool
$c/= :: ComplexityMeasure -> ComplexityMeasure -> Bool
== :: ComplexityMeasure -> ComplexityMeasure -> Bool
$c== :: ComplexityMeasure -> ComplexityMeasure -> Bool
Eq, Int -> ComplexityMeasure -> ShowS
[ComplexityMeasure] -> ShowS
ComplexityMeasure -> String
(Int -> ComplexityMeasure -> ShowS)
-> (ComplexityMeasure -> String)
-> ([ComplexityMeasure] -> ShowS)
-> Show ComplexityMeasure
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ComplexityMeasure] -> ShowS
$cshowList :: [ComplexityMeasure] -> ShowS
show :: ComplexityMeasure -> String
$cshow :: ComplexityMeasure -> String
showsPrec :: Int -> ComplexityMeasure -> ShowS
$cshowsPrec :: Int -> ComplexityMeasure -> ShowS
Show )
data ComplexityClass =
ComplexityClassPolynomial { ComplexityClass -> Int
degree :: Int }
deriving ( Typeable, ComplexityClass -> ComplexityClass -> Bool
(ComplexityClass -> ComplexityClass -> Bool)
-> (ComplexityClass -> ComplexityClass -> Bool)
-> Eq ComplexityClass
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ComplexityClass -> ComplexityClass -> Bool
$c/= :: ComplexityClass -> ComplexityClass -> Bool
== :: ComplexityClass -> ComplexityClass -> Bool
$c== :: ComplexityClass -> ComplexityClass -> Bool
Eq, Int -> ComplexityClass -> ShowS
[ComplexityClass] -> ShowS
ComplexityClass -> String
(Int -> ComplexityClass -> ShowS)
-> (ComplexityClass -> String)
-> ([ComplexityClass] -> ShowS)
-> Show ComplexityClass
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ComplexityClass] -> ShowS
$cshowList :: [ComplexityClass] -> ShowS
show :: ComplexityClass -> String
$cshow :: ComplexityClass -> String
showsPrec :: Int -> ComplexityClass -> ShowS
$cshowsPrec :: Int -> ComplexityClass -> ShowS
Show )
data TrsNonterminationProof = TrsNonterminationProofFIXME ()
deriving ( Typeable, TrsNonterminationProof -> TrsNonterminationProof -> Bool
(TrsNonterminationProof -> TrsNonterminationProof -> Bool)
-> (TrsNonterminationProof -> TrsNonterminationProof -> Bool)
-> Eq TrsNonterminationProof
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TrsNonterminationProof -> TrsNonterminationProof -> Bool
$c/= :: TrsNonterminationProof -> TrsNonterminationProof -> Bool
== :: TrsNonterminationProof -> TrsNonterminationProof -> Bool
$c== :: TrsNonterminationProof -> TrsNonterminationProof -> Bool
Eq )
data TrsTerminationProof
= RIsEmpty
| RuleRemoval { TrsTerminationProof -> OrderingConstraintProof
rr_orderingConstraintProof :: OrderingConstraintProof
, TrsTerminationProof -> TRS Identifier Identifier
trs :: TRS Identifier Identifier
, TrsTerminationProof -> TrsTerminationProof
trsTerminationProof :: TrsTerminationProof
}
| DpTrans { TrsTerminationProof -> DPS
dptrans_dps :: DPS
, TrsTerminationProof -> Bool
markedSymbols :: Bool , TrsTerminationProof -> DpProof
dptrans_dpProof :: DpProof }
| Semlab { TrsTerminationProof -> Model
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
, TrsTerminationProof -> Bounds_Type
bounds_type :: Bounds_Type
, TrsTerminationProof -> Int
bounds_bound :: Int
, TrsTerminationProof -> [State]
bounds_finalStates :: [ State ]
, TrsTerminationProof -> ClosedTreeAutomaton
bounds_closedTreeAutomaton :: ClosedTreeAutomaton
}
deriving ( Typeable, TrsTerminationProof -> TrsTerminationProof -> Bool
(TrsTerminationProof -> TrsTerminationProof -> Bool)
-> (TrsTerminationProof -> TrsTerminationProof -> Bool)
-> Eq TrsTerminationProof
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TrsTerminationProof -> TrsTerminationProof -> Bool
$c/= :: TrsTerminationProof -> TrsTerminationProof -> Bool
== :: TrsTerminationProof -> TrsTerminationProof -> Bool
$c== :: TrsTerminationProof -> TrsTerminationProof -> Bool
Eq )
data Bounds_Type = Roof | Match
deriving ( Typeable, Bounds_Type -> Bounds_Type -> Bool
(Bounds_Type -> Bounds_Type -> Bool)
-> (Bounds_Type -> Bounds_Type -> Bool) -> Eq Bounds_Type
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Bounds_Type -> Bounds_Type -> Bool
$c/= :: Bounds_Type -> Bounds_Type -> Bool
== :: Bounds_Type -> Bounds_Type -> Bool
$c== :: Bounds_Type -> Bounds_Type -> Bool
Eq )
data ClosedTreeAutomaton = ClosedTreeAutomaton
{ ClosedTreeAutomaton -> TreeAutomaton
cta_treeAutomaton :: TreeAutomaton
, ClosedTreeAutomaton -> Criterion
cta_criterion :: Criterion
}
deriving ( Typeable, ClosedTreeAutomaton -> ClosedTreeAutomaton -> Bool
(ClosedTreeAutomaton -> ClosedTreeAutomaton -> Bool)
-> (ClosedTreeAutomaton -> ClosedTreeAutomaton -> Bool)
-> Eq ClosedTreeAutomaton
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ClosedTreeAutomaton -> ClosedTreeAutomaton -> Bool
$c/= :: ClosedTreeAutomaton -> ClosedTreeAutomaton -> Bool
== :: ClosedTreeAutomaton -> ClosedTreeAutomaton -> Bool
$c== :: ClosedTreeAutomaton -> ClosedTreeAutomaton -> Bool
Eq )
data Criterion = Compatibility
deriving ( Typeable, Criterion -> Criterion -> Bool
(Criterion -> Criterion -> Bool)
-> (Criterion -> Criterion -> Bool) -> Eq Criterion
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Criterion -> Criterion -> Bool
$c/= :: Criterion -> Criterion -> Bool
== :: Criterion -> Criterion -> Bool
$c== :: Criterion -> Criterion -> Bool
Eq )
data TreeAutomaton = TreeAutomaton
{ TreeAutomaton -> [State]
ta_finalStates :: [ State ]
, TreeAutomaton -> [Transition]
ta_transitions :: [ Transition ]
}
deriving ( Typeable, TreeAutomaton -> TreeAutomaton -> Bool
(TreeAutomaton -> TreeAutomaton -> Bool)
-> (TreeAutomaton -> TreeAutomaton -> Bool) -> Eq TreeAutomaton
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TreeAutomaton -> TreeAutomaton -> Bool
$c/= :: TreeAutomaton -> TreeAutomaton -> Bool
== :: TreeAutomaton -> TreeAutomaton -> Bool
$c== :: TreeAutomaton -> TreeAutomaton -> Bool
Eq )
data State = State Int
deriving ( Typeable, State -> State -> Bool
(State -> State -> Bool) -> (State -> State -> Bool) -> Eq State
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: State -> State -> Bool
$c/= :: State -> State -> Bool
== :: State -> State -> Bool
$c== :: State -> State -> Bool
Eq )
data Transition = Transition
{ Transition -> Transition_Lhs
transition_lhs :: Transition_Lhs
, Transition -> [State]
transition_rhs :: [ State ]
}
deriving ( Typeable, Transition -> Transition -> Bool
(Transition -> Transition -> Bool)
-> (Transition -> Transition -> Bool) -> Eq Transition
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Transition -> Transition -> Bool
$c/= :: Transition -> Transition -> Bool
== :: Transition -> Transition -> Bool
$c== :: Transition -> Transition -> Bool
Eq )
data Transition_Lhs
= Transition_Symbol { Transition_Lhs -> Symbol
tr_symbol :: Symbol
, Transition_Lhs -> Int
tr_height :: Int
, Transition_Lhs -> [State]
tr_arguments :: [ State ]
}
| Transition_Epsilon State
deriving ( Typeable, Transition_Lhs -> Transition_Lhs -> Bool
(Transition_Lhs -> Transition_Lhs -> Bool)
-> (Transition_Lhs -> Transition_Lhs -> Bool) -> Eq Transition_Lhs
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Transition_Lhs -> Transition_Lhs -> Bool
$c/= :: Transition_Lhs -> Transition_Lhs -> Bool
== :: Transition_Lhs -> Transition_Lhs -> Bool
$c== :: Transition_Lhs -> Transition_Lhs -> Bool
Eq )
data Model = FiniteModel Int [Interpret]
deriving ( Typeable, Model -> Model -> Bool
(Model -> Model -> Bool) -> (Model -> Model -> Bool) -> Eq Model
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Model -> Model -> Bool
$c/= :: Model -> Model -> Bool
== :: Model -> Model -> Bool
$c== :: Model -> Model -> Bool
Eq )
data DpProof = PIsEmpty
| RedPairProc { DpProof -> OrderingConstraintProof
rppOrderingConstraintProof :: OrderingConstraintProof
, DpProof -> DPS
rppDps :: DPS
, DpProof -> Maybe DPS
rppUsableRules :: Maybe DPS
, DpProof -> DpProof
rppDpProof :: DpProof
}
| DepGraphProc [ DepGraphComponent ]
| SemLabProc { DpProof -> Model
slpModel :: Model
, DpProof -> DPS
slpDps :: DPS
, DpProof -> DPS
slpTrs :: DPS
, DpProof -> DpProof
slpDpProof :: DpProof
}
| UnlabProc { DpProof -> DPS
ulpDps :: DPS
, DpProof -> DPS
ulpTrs :: DPS
, DpProof -> DpProof
ulpDpProof :: DpProof
}
deriving ( Typeable, DpProof -> DpProof -> Bool
(DpProof -> DpProof -> Bool)
-> (DpProof -> DpProof -> Bool) -> Eq DpProof
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DpProof -> DpProof -> Bool
$c/= :: DpProof -> DpProof -> Bool
== :: DpProof -> DpProof -> Bool
$c== :: DpProof -> DpProof -> Bool
Eq )
data DepGraphComponent =
DepGraphComponent { DepGraphComponent -> Bool
dgcRealScc :: Bool
, DepGraphComponent -> DPS
dgcDps :: DPS
, DepGraphComponent -> DpProof
dgcDpProof :: DpProof
}
deriving ( Typeable, DepGraphComponent -> DepGraphComponent -> Bool
(DepGraphComponent -> DepGraphComponent -> Bool)
-> (DepGraphComponent -> DepGraphComponent -> Bool)
-> Eq DepGraphComponent
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DepGraphComponent -> DepGraphComponent -> Bool
$c/= :: DepGraphComponent -> DepGraphComponent -> Bool
== :: DepGraphComponent -> DepGraphComponent -> Bool
$c== :: DepGraphComponent -> DepGraphComponent -> Bool
Eq )
data OrderingConstraintProof = OCPRedPair RedPair
deriving ( Typeable, OrderingConstraintProof -> OrderingConstraintProof -> Bool
(OrderingConstraintProof -> OrderingConstraintProof -> Bool)
-> (OrderingConstraintProof -> OrderingConstraintProof -> Bool)
-> Eq OrderingConstraintProof
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: OrderingConstraintProof -> OrderingConstraintProof -> Bool
$c/= :: OrderingConstraintProof -> OrderingConstraintProof -> Bool
== :: OrderingConstraintProof -> OrderingConstraintProof -> Bool
$c== :: OrderingConstraintProof -> OrderingConstraintProof -> Bool
Eq )
data RedPair = RPInterpretation Interpretation
| RPPathOrder PathOrder
deriving ( Typeable, RedPair -> RedPair -> Bool
(RedPair -> RedPair -> Bool)
-> (RedPair -> RedPair -> Bool) -> Eq RedPair
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: RedPair -> RedPair -> Bool
$c/= :: RedPair -> RedPair -> Bool
== :: RedPair -> RedPair -> Bool
$c== :: RedPair -> RedPair -> Bool
Eq )
data Interpretation =
Interpretation { Interpretation -> Interpretation_Type
interpretation_type :: Interpretation_Type
, Interpretation -> [Interpret]
interprets :: [ Interpret ]
}
deriving ( Typeable, Interpretation -> Interpretation -> Bool
(Interpretation -> Interpretation -> Bool)
-> (Interpretation -> Interpretation -> Bool) -> Eq Interpretation
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Interpretation -> Interpretation -> Bool
$c/= :: Interpretation -> Interpretation -> Bool
== :: Interpretation -> Interpretation -> Bool
$c== :: Interpretation -> Interpretation -> Bool
Eq )
data Interpretation_Type =
Matrix_Interpretation { Interpretation_Type -> Domain
domain :: Domain, Interpretation_Type -> Int
dimension :: Int
, Interpretation_Type -> Int
strictDimension :: Int
}
deriving ( Typeable, Interpretation_Type -> Interpretation_Type -> Bool
(Interpretation_Type -> Interpretation_Type -> Bool)
-> (Interpretation_Type -> Interpretation_Type -> Bool)
-> Eq Interpretation_Type
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Interpretation_Type -> Interpretation_Type -> Bool
$c/= :: Interpretation_Type -> Interpretation_Type -> Bool
== :: Interpretation_Type -> Interpretation_Type -> Bool
$c== :: Interpretation_Type -> Interpretation_Type -> Bool
Eq )
data Domain = Naturals
| Rationals Rational
| Arctic Domain
| Tropical Domain
deriving ( Typeable, Domain -> Domain -> Bool
(Domain -> Domain -> Bool)
-> (Domain -> Domain -> Bool) -> Eq Domain
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Domain -> Domain -> Bool
$c/= :: Domain -> Domain -> Bool
== :: Domain -> Domain -> Bool
$c== :: Domain -> Domain -> Bool
Eq )
data Interpret = Interpret
{ Interpret -> Symbol
symbol :: Symbol , Interpret -> Int
arity :: Int , Interpret -> Value
value :: Value }
deriving ( Typeable, Interpret -> Interpret -> Bool
(Interpret -> Interpret -> Bool)
-> (Interpret -> Interpret -> Bool) -> Eq Interpret
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Interpret -> Interpret -> Bool
$c/= :: Interpret -> Interpret -> Bool
== :: Interpret -> Interpret -> Bool
$c== :: Interpret -> Interpret -> Bool
Eq )
data Value = Polynomial Polynomial
| ArithFunction ArithFunction
deriving ( Typeable, Value -> Value -> Bool
(Value -> Value -> Bool) -> (Value -> Value -> Bool) -> Eq Value
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Value -> Value -> Bool
$c/= :: Value -> Value -> Bool
== :: Value -> Value -> Bool
$c== :: Value -> Value -> Bool
Eq )
data Polynomial = Sum [ Polynomial ]
| Product [ Polynomial ]
| Polynomial_Coefficient Coefficient
| Polynomial_Variable Text
deriving ( Typeable, Polynomial -> Polynomial -> Bool
(Polynomial -> Polynomial -> Bool)
-> (Polynomial -> Polynomial -> Bool) -> Eq Polynomial
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Polynomial -> Polynomial -> Bool
$c/= :: Polynomial -> Polynomial -> Bool
== :: Polynomial -> Polynomial -> Bool
$c== :: Polynomial -> Polynomial -> Bool
Eq )
data ArithFunction = AFNatural Integer
| AFVariable Integer
| AFSum [ArithFunction]
| AFProduct [ArithFunction]
| AFMin [ArithFunction]
| AFMax [ArithFunction]
| AFIfEqual ArithFunction ArithFunction ArithFunction ArithFunction
deriving ( Typeable, ArithFunction -> ArithFunction -> Bool
(ArithFunction -> ArithFunction -> Bool)
-> (ArithFunction -> ArithFunction -> Bool) -> Eq ArithFunction
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ArithFunction -> ArithFunction -> Bool
$c/= :: ArithFunction -> ArithFunction -> Bool
== :: ArithFunction -> ArithFunction -> Bool
$c== :: ArithFunction -> ArithFunction -> Bool
Eq )
data Symbol = SymName Identifier
| SymSharp Symbol
| SymLabel Symbol Label
deriving ( Typeable, Symbol -> Symbol -> Bool
(Symbol -> Symbol -> Bool)
-> (Symbol -> Symbol -> Bool) -> Eq Symbol
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Symbol -> Symbol -> Bool
$c/= :: Symbol -> Symbol -> Bool
== :: Symbol -> Symbol -> Bool
$c== :: Symbol -> Symbol -> Bool
Eq )
data Label = LblNumber [Integer]
| LblSymbol [Symbol]
deriving ( Typeable, Label -> Label -> Bool
(Label -> Label -> Bool) -> (Label -> Label -> Bool) -> Eq Label
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Label -> Label -> Bool
$c/= :: Label -> Label -> Bool
== :: Label -> Label -> Bool
$c== :: Label -> Label -> Bool
Eq )
data Coefficient = Vector [ Coefficient ]
| Matrix [ Coefficient ]
| forall a . (Eq a , XmlContent a
) => Coefficient_Coefficient a
deriving ( Typeable )
instance Eq Coefficient where Coefficient
x == :: Coefficient -> Coefficient -> Bool
== Coefficient
y = String -> Bool
forall a. HasCallStack => String -> a
error String
"instance Eq Coefficient"
data Exotic = Minus_Infinite | E_Integer Integer | E_Rational Rational | Plus_Infinite
deriving ( Typeable, Exotic -> Exotic -> Bool
(Exotic -> Exotic -> Bool)
-> (Exotic -> Exotic -> Bool) -> Eq Exotic
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Exotic -> Exotic -> Bool
$c/= :: Exotic -> Exotic -> Bool
== :: Exotic -> Exotic -> Bool
$c== :: Exotic -> Exotic -> Bool
Eq )
class ToExotic a where toExotic :: a -> Exotic
data PathOrder = PathOrder [PrecedenceEntry] [ArgumentFilterEntry]
deriving ( Typeable, PathOrder -> PathOrder -> Bool
(PathOrder -> PathOrder -> Bool)
-> (PathOrder -> PathOrder -> Bool) -> Eq PathOrder
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PathOrder -> PathOrder -> Bool
$c/= :: PathOrder -> PathOrder -> Bool
== :: PathOrder -> PathOrder -> Bool
$c== :: PathOrder -> PathOrder -> Bool
Eq )
data PrecedenceEntry = PrecedenceEntry { PrecedenceEntry -> Symbol
peSymbol :: Symbol
, PrecedenceEntry -> Int
peArity :: Int
, PrecedenceEntry -> Integer
pePrecedence :: Integer
}
deriving ( Typeable, PrecedenceEntry -> PrecedenceEntry -> Bool
(PrecedenceEntry -> PrecedenceEntry -> Bool)
-> (PrecedenceEntry -> PrecedenceEntry -> Bool)
-> Eq PrecedenceEntry
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PrecedenceEntry -> PrecedenceEntry -> Bool
$c/= :: PrecedenceEntry -> PrecedenceEntry -> Bool
== :: PrecedenceEntry -> PrecedenceEntry -> Bool
$c== :: PrecedenceEntry -> PrecedenceEntry -> Bool
Eq )
data ArgumentFilterEntry =
ArgumentFilterEntry { ArgumentFilterEntry -> Symbol
afeSymbol :: Symbol
, ArgumentFilterEntry -> Int
afeArity :: Int
, ArgumentFilterEntry -> Either Int [Int]
afeFilter :: Either Int [Int]
}
deriving ( Typeable, ArgumentFilterEntry -> ArgumentFilterEntry -> Bool
(ArgumentFilterEntry -> ArgumentFilterEntry -> Bool)
-> (ArgumentFilterEntry -> ArgumentFilterEntry -> Bool)
-> Eq ArgumentFilterEntry
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ArgumentFilterEntry -> ArgumentFilterEntry -> Bool
$c/= :: ArgumentFilterEntry -> ArgumentFilterEntry -> Bool
== :: ArgumentFilterEntry -> ArgumentFilterEntry -> Bool
$c== :: ArgumentFilterEntry -> ArgumentFilterEntry -> Bool
Eq )
data ACTerminationProof = ACTerminationProofFIXME ()
deriving ( Typeable, ACTerminationProof -> ACTerminationProof -> Bool
(ACTerminationProof -> ACTerminationProof -> Bool)
-> (ACTerminationProof -> ACTerminationProof -> Bool)
-> Eq ACTerminationProof
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ACTerminationProof -> ACTerminationProof -> Bool
$c/= :: ACTerminationProof -> ACTerminationProof -> Bool
== :: ACTerminationProof -> ACTerminationProof -> Bool
$c== :: ACTerminationProof -> ACTerminationProof -> Bool
Eq )