{-# language StandaloneDeriving #-}
{-# language ExistentialQuantification #-}
{-# language DeriveDataTypeable #-}
{-# language OverloadedStrings #-}

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

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 }
      -- ^ 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)
    | 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 } 
     -- ^ 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
    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 )