{-# language StandaloneDeriving #-}
{-# language DataKinds, KindSignatures, GADTs, StandaloneDeriving #-}
{-# language ExistentialQuantification #-}
{-# language DeriveDataTypeable, DeriveGeneric #-}
{-# language OverloadedStrings #-}
{-# language FlexibleContexts #-}
{-# language StrictData #-}

-- | 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 (Text)
import qualified Data.Text as T
import TPDB.Xml (XmlContent)
import GHC.Generics
import Data.Hashable
import Data.Kind
import qualified Data.Text.Lazy as TL

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
$c== :: CertificationProblem -> CertificationProblem -> Bool
== :: CertificationProblem -> CertificationProblem -> Bool
$c/= :: CertificationProblem -> CertificationProblem -> Bool
/= :: CertificationProblem -> CertificationProblem -> Bool
Eq, (forall x. CertificationProblem -> Rep CertificationProblem x)
-> (forall x. Rep CertificationProblem x -> CertificationProblem)
-> Generic CertificationProblem
forall x. Rep CertificationProblem x -> CertificationProblem
forall x. CertificationProblem -> Rep CertificationProblem x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. CertificationProblem -> Rep CertificationProblem x
from :: forall x. CertificationProblem -> Rep CertificationProblem x
$cto :: forall x. Rep CertificationProblem x -> CertificationProblem
to :: forall x. Rep CertificationProblem x -> CertificationProblem
Generic )

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
$c== :: Origin -> Origin -> Bool
== :: Origin -> Origin -> Bool
$c/= :: Origin -> Origin -> Bool
/= :: Origin -> Origin -> Bool
Eq, (forall x. Origin -> Rep Origin x)
-> (forall x. Rep Origin x -> Origin) -> Generic Origin
forall x. Rep Origin x -> Origin
forall x. Origin -> Rep Origin x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Origin -> Rep Origin x
from :: forall x. Origin -> Rep Origin x
$cto :: forall x. Rep Origin x -> Origin
to :: forall x. Rep Origin x -> Origin
Generic )

ignoredOrigin :: Origin
ignoredOrigin = 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
$c== :: Tool -> Tool -> Bool
== :: Tool -> Tool -> Bool
$c/= :: Tool -> Tool -> Bool
/= :: Tool -> Tool -> Bool
Eq, (forall x. Tool -> Rep Tool x)
-> (forall x. Rep Tool x -> Tool) -> Generic Tool
forall x. Rep Tool x -> Tool
forall x. Tool -> Rep Tool x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Tool -> Rep Tool x
from :: forall x. Tool -> Rep Tool x
$cto :: forall x. Rep Tool x -> Tool
to :: forall x. Rep Tool x -> Tool
Generic )

-- | use this type throughout.
-- Variables are plain identifiers
-- but signature can use sharped, and labelled symbols.
type Trs = TRS Identifier Symbol

data CertificationProblemInput 
    = TrsInput { CertificationProblemInput -> Trs
trsinput_trs :: Trs }
      -- ^ 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
                      , CertificationProblemInput -> ComplexityMeasure
complexityMeasure :: ComplexityMeasure
                      , CertificationProblemInput -> ComplexityClass
complexityClass :: ComplexityClass      
                      }
    | ACRewriteSystem { trsinput_trs :: Trs
                      , CertificationProblemInput -> [Symbol]
asymbols :: [ Symbol ]
                      , CertificationProblemInput -> [Symbol]
csymbols :: [ Symbol ]
                      }
   deriving ( Typeable, CertificationProblemInput -> CertificationProblemInput -> Bool
(CertificationProblemInput -> CertificationProblemInput -> Bool)
-> (CertificationProblemInput -> CertificationProblemInput -> Bool)
-> Eq CertificationProblemInput
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: CertificationProblemInput -> CertificationProblemInput -> Bool
== :: CertificationProblemInput -> CertificationProblemInput -> Bool
$c/= :: CertificationProblemInput -> CertificationProblemInput -> Bool
/= :: CertificationProblemInput -> CertificationProblemInput -> Bool
Eq, (forall x.
 CertificationProblemInput -> Rep CertificationProblemInput x)
-> (forall x.
    Rep CertificationProblemInput x -> CertificationProblemInput)
-> Generic CertificationProblemInput
forall x.
Rep CertificationProblemInput x -> CertificationProblemInput
forall x.
CertificationProblemInput -> Rep CertificationProblemInput x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x.
CertificationProblemInput -> Rep CertificationProblemInput x
from :: forall x.
CertificationProblemInput -> Rep CertificationProblemInput x
$cto :: forall x.
Rep CertificationProblemInput x -> CertificationProblemInput
to :: forall x.
Rep CertificationProblemInput x -> CertificationProblemInput
Generic  )

instance Pretty CertificationProblemInput where
  pretty :: forall ann. 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 -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Trs -> Doc ann
pretty (CertificationProblemInput -> Trs
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 -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Trs -> Doc ann
pretty (CertificationProblemInput -> Trs
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 -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Trs -> Doc ann
pretty (CertificationProblemInput -> Trs
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 ([Symbol] -> String
forall a. Show a => a -> String
show ([Symbol] -> String) -> [Symbol] -> String
forall a b. (a -> b) -> a -> b
$ CertificationProblemInput -> [Symbol]
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 ([Symbol] -> String
forall a. Show a => a -> String
show ([Symbol] -> String) -> [Symbol] -> String
forall a b. (a -> b) -> a -> b
$ CertificationProblemInput -> [Symbol]
csymbols CertificationProblemInput
cpi )
         ]

data Kind = Standard | Relative
   deriving ( Typeable, Kind -> Kind -> Bool
(Kind -> Kind -> Bool) -> (Kind -> Kind -> Bool) -> Eq Kind
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Kind -> Kind -> Bool
== :: Kind -> Kind -> Bool
$c/= :: Kind -> Kind -> Bool
/= :: Kind -> Kind -> Bool
Eq, (forall x. Kind -> Rep Kind x)
-> (forall x. Rep Kind x -> Kind) -> Generic Kind
forall x. Rep Kind x -> Kind
forall x. Kind -> Rep Kind x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Kind -> Rep Kind x
from :: forall x. Kind -> Rep Kind x
$cto :: forall x. Rep Kind x -> Kind
to :: forall x. Rep Kind x -> Kind
Generic  )

data Proof = TrsTerminationProof (TrsTerminationProof Standard)
           | TrsNonterminationProof (TrsNonterminationProof Standard)
           | RelativeTerminationProof (TrsTerminationProof Relative)
           | RelativeNonterminationProof (TrsNonterminationProof Relative)
           | 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
$c== :: Proof -> Proof -> Bool
== :: Proof -> Proof -> Bool
$c/= :: Proof -> Proof -> Bool
/= :: Proof -> Proof -> Bool
Eq, (forall x. Proof -> Rep Proof x)
-> (forall x. Rep Proof x -> Proof) -> Generic Proof
forall x. Rep Proof x -> Proof
forall x. Proof -> Rep Proof x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Proof -> Rep Proof x
from :: forall x. Proof -> Rep Proof x
$cto :: forall x. Rep Proof x -> Proof
to :: forall x. Rep Proof x -> Proof
Generic  )

data DPS = DPS [ Rule (Term Identifier Symbol) ]
   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
$c== :: ComplexityProof -> ComplexityProof -> Bool
== :: ComplexityProof -> ComplexityProof -> Bool
$c/= :: ComplexityProof -> ComplexityProof -> Bool
/= :: ComplexityProof -> ComplexityProof -> Bool
Eq, (forall x. ComplexityProof -> Rep ComplexityProof x)
-> (forall x. Rep ComplexityProof x -> ComplexityProof)
-> Generic ComplexityProof
forall x. Rep ComplexityProof x -> ComplexityProof
forall x. ComplexityProof -> Rep ComplexityProof x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ComplexityProof -> Rep ComplexityProof x
from :: forall x. ComplexityProof -> Rep ComplexityProof x
$cto :: forall x. Rep ComplexityProof x -> ComplexityProof
to :: forall x. Rep ComplexityProof x -> ComplexityProof
Generic  )

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
$c== :: ComplexityMeasure -> ComplexityMeasure -> Bool
== :: ComplexityMeasure -> ComplexityMeasure -> Bool
$c/= :: ComplexityMeasure -> ComplexityMeasure -> Bool
/= :: ComplexityMeasure -> ComplexityMeasure -> Bool
Eq, (forall x. ComplexityMeasure -> Rep ComplexityMeasure x)
-> (forall x. Rep ComplexityMeasure x -> ComplexityMeasure)
-> Generic ComplexityMeasure
forall x. Rep ComplexityMeasure x -> ComplexityMeasure
forall x. ComplexityMeasure -> Rep ComplexityMeasure x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ComplexityMeasure -> Rep ComplexityMeasure x
from :: forall x. ComplexityMeasure -> Rep ComplexityMeasure x
$cto :: forall x. Rep ComplexityMeasure x -> ComplexityMeasure
to :: forall x. Rep ComplexityMeasure x -> ComplexityMeasure
Generic , 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
$cshowsPrec :: Int -> ComplexityMeasure -> ShowS
showsPrec :: Int -> ComplexityMeasure -> ShowS
$cshow :: ComplexityMeasure -> String
show :: ComplexityMeasure -> String
$cshowList :: [ComplexityMeasure] -> ShowS
showList :: [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
$c== :: ComplexityClass -> ComplexityClass -> Bool
== :: ComplexityClass -> ComplexityClass -> Bool
$c/= :: ComplexityClass -> ComplexityClass -> Bool
/= :: ComplexityClass -> ComplexityClass -> Bool
Eq, (forall x. ComplexityClass -> Rep ComplexityClass x)
-> (forall x. Rep ComplexityClass x -> ComplexityClass)
-> Generic ComplexityClass
forall x. Rep ComplexityClass x -> ComplexityClass
forall x. ComplexityClass -> Rep ComplexityClass x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ComplexityClass -> Rep ComplexityClass x
from :: forall x. ComplexityClass -> Rep ComplexityClass x
$cto :: forall x. Rep ComplexityClass x -> ComplexityClass
to :: forall x. Rep ComplexityClass x -> ComplexityClass
Generic , 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
$cshowsPrec :: Int -> ComplexityClass -> ShowS
showsPrec :: Int -> ComplexityClass -> ShowS
$cshow :: ComplexityClass -> String
show :: ComplexityClass -> String
$cshowList :: [ComplexityClass] -> ShowS
showList :: [ComplexityClass] -> ShowS
Show )

data TrsNonterminationProof (k :: Kind)
  = VariableConditionViolated
  | TNP_RuleRemoval Trs (TrsNonterminationProof k)
  | TNP_StringReversal Trs (TrsNonterminationProof k)
  | Loop
  { forall (k :: Kind). TrsNonterminationProof k -> RewriteSequence
rewriteSequence :: RewriteSequence
  , forall (k :: Kind). TrsNonterminationProof k -> Substitution
substitution :: Substitution
  , forall (k :: Kind). TrsNonterminationProof k -> Context
context :: Context
  }
    deriving ( Typeable, TrsNonterminationProof k -> TrsNonterminationProof k -> Bool
(TrsNonterminationProof k -> TrsNonterminationProof k -> Bool)
-> (TrsNonterminationProof k -> TrsNonterminationProof k -> Bool)
-> Eq (TrsNonterminationProof k)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (k :: Kind).
TrsNonterminationProof k -> TrsNonterminationProof k -> Bool
$c== :: forall (k :: Kind).
TrsNonterminationProof k -> TrsNonterminationProof k -> Bool
== :: TrsNonterminationProof k -> TrsNonterminationProof k -> Bool
$c/= :: forall (k :: Kind).
TrsNonterminationProof k -> TrsNonterminationProof k -> Bool
/= :: TrsNonterminationProof k -> TrsNonterminationProof k -> Bool
Eq, (forall x.
 TrsNonterminationProof k -> Rep (TrsNonterminationProof k) x)
-> (forall x.
    Rep (TrsNonterminationProof k) x -> TrsNonterminationProof k)
-> Generic (TrsNonterminationProof k)
forall x.
Rep (TrsNonterminationProof k) x -> TrsNonterminationProof k
forall x.
TrsNonterminationProof k -> Rep (TrsNonterminationProof k) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (k :: Kind) x.
Rep (TrsNonterminationProof k) x -> TrsNonterminationProof k
forall (k :: Kind) x.
TrsNonterminationProof k -> Rep (TrsNonterminationProof k) x
$cfrom :: forall (k :: Kind) x.
TrsNonterminationProof k -> Rep (TrsNonterminationProof k) x
from :: forall x.
TrsNonterminationProof k -> Rep (TrsNonterminationProof k) x
$cto :: forall (k :: Kind) x.
Rep (TrsNonterminationProof k) x -> TrsNonterminationProof k
to :: forall x.
Rep (TrsNonterminationProof k) x -> TrsNonterminationProof k
Generic  )

data RewriteSequence = RewriteSequence (Term Identifier Symbol) [ RewriteStep ]
    deriving ( Typeable, RewriteSequence -> RewriteSequence -> Bool
(RewriteSequence -> RewriteSequence -> Bool)
-> (RewriteSequence -> RewriteSequence -> Bool)
-> Eq RewriteSequence
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: RewriteSequence -> RewriteSequence -> Bool
== :: RewriteSequence -> RewriteSequence -> Bool
$c/= :: RewriteSequence -> RewriteSequence -> Bool
/= :: RewriteSequence -> RewriteSequence -> Bool
Eq, (forall x. RewriteSequence -> Rep RewriteSequence x)
-> (forall x. Rep RewriteSequence x -> RewriteSequence)
-> Generic RewriteSequence
forall x. Rep RewriteSequence x -> RewriteSequence
forall x. RewriteSequence -> Rep RewriteSequence x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. RewriteSequence -> Rep RewriteSequence x
from :: forall x. RewriteSequence -> Rep RewriteSequence x
$cto :: forall x. Rep RewriteSequence x -> RewriteSequence
to :: forall x. Rep RewriteSequence x -> RewriteSequence
Generic  )

data RewriteStep = RewriteStep
  { RewriteStep -> Position
rs_position :: Position
  , RewriteStep -> Rule (Term Identifier Symbol)
rs_rule :: Rule (Term Identifier Symbol)
  , RewriteStep -> Term Identifier Symbol
rs_term :: Term Identifier Symbol
  }
    deriving ( Typeable, RewriteStep -> RewriteStep -> Bool
(RewriteStep -> RewriteStep -> Bool)
-> (RewriteStep -> RewriteStep -> Bool) -> Eq RewriteStep
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: RewriteStep -> RewriteStep -> Bool
== :: RewriteStep -> RewriteStep -> Bool
$c/= :: RewriteStep -> RewriteStep -> Bool
/= :: RewriteStep -> RewriteStep -> Bool
Eq, (forall x. RewriteStep -> Rep RewriteStep x)
-> (forall x. Rep RewriteStep x -> RewriteStep)
-> Generic RewriteStep
forall x. Rep RewriteStep x -> RewriteStep
forall x. RewriteStep -> Rep RewriteStep x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. RewriteStep -> Rep RewriteStep x
from :: forall x. RewriteStep -> Rep RewriteStep x
$cto :: forall x. Rep RewriteStep x -> RewriteStep
to :: forall x. Rep RewriteStep x -> RewriteStep
Generic  )

data Substitution = Substitution [ SubstEntry ]
    deriving ( Typeable, Substitution -> Substitution -> Bool
(Substitution -> Substitution -> Bool)
-> (Substitution -> Substitution -> Bool) -> Eq Substitution
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Substitution -> Substitution -> Bool
== :: Substitution -> Substitution -> Bool
$c/= :: Substitution -> Substitution -> Bool
/= :: Substitution -> Substitution -> Bool
Eq, (forall x. Substitution -> Rep Substitution x)
-> (forall x. Rep Substitution x -> Substitution)
-> Generic Substitution
forall x. Rep Substitution x -> Substitution
forall x. Substitution -> Rep Substitution x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Substitution -> Rep Substitution x
from :: forall x. Substitution -> Rep Substitution x
$cto :: forall x. Rep Substitution x -> Substitution
to :: forall x. Rep Substitution x -> Substitution
Generic  )

data SubstEntry = SubstEntry Identifier (Term Identifier Symbol)
    deriving ( Typeable, SubstEntry -> SubstEntry -> Bool
(SubstEntry -> SubstEntry -> Bool)
-> (SubstEntry -> SubstEntry -> Bool) -> Eq SubstEntry
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: SubstEntry -> SubstEntry -> Bool
== :: SubstEntry -> SubstEntry -> Bool
$c/= :: SubstEntry -> SubstEntry -> Bool
/= :: SubstEntry -> SubstEntry -> Bool
Eq, (forall x. SubstEntry -> Rep SubstEntry x)
-> (forall x. Rep SubstEntry x -> SubstEntry) -> Generic SubstEntry
forall x. Rep SubstEntry x -> SubstEntry
forall x. SubstEntry -> Rep SubstEntry x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. SubstEntry -> Rep SubstEntry x
from :: forall x. SubstEntry -> Rep SubstEntry x
$cto :: forall x. Rep SubstEntry x -> SubstEntry
to :: forall x. Rep SubstEntry x -> SubstEntry
Generic  )

data Context = Box
   | FunContext { Context -> Symbol
fc_symbol :: Symbol
                , Context -> [Term Identifier Symbol]
fc_before :: [Term Identifier Symbol ]
                , Context -> Context
fc_here :: Context
                , Context -> [Term Identifier Symbol]
fc_after  :: [Term Identifier Symbol ]
                }
    deriving ( Typeable, Context -> Context -> Bool
(Context -> Context -> Bool)
-> (Context -> Context -> Bool) -> Eq Context
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Context -> Context -> Bool
== :: Context -> Context -> Bool
$c/= :: Context -> Context -> Bool
/= :: Context -> Context -> Bool
Eq, (forall x. Context -> Rep Context x)
-> (forall x. Rep Context x -> Context) -> Generic Context
forall x. Rep Context x -> Context
forall x. Context -> Rep Context x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Context -> Rep Context x
from :: forall x. Context -> Rep Context x
$cto :: forall x. Rep Context x -> Context
to :: forall x. Rep Context x -> Context
Generic  )

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

deriving instance Typeable (TrsTerminationProof k)
deriving instance Eq (TrsTerminationProof k)
-- deriving instance Generic (TrsTerminationProof k)

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
$c== :: Bounds_Type -> Bounds_Type -> Bool
== :: Bounds_Type -> Bounds_Type -> Bool
$c/= :: Bounds_Type -> Bounds_Type -> Bool
/= :: Bounds_Type -> Bounds_Type -> Bool
Eq, (forall x. Bounds_Type -> Rep Bounds_Type x)
-> (forall x. Rep Bounds_Type x -> Bounds_Type)
-> Generic Bounds_Type
forall x. Rep Bounds_Type x -> Bounds_Type
forall x. Bounds_Type -> Rep Bounds_Type x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Bounds_Type -> Rep Bounds_Type x
from :: forall x. Bounds_Type -> Rep Bounds_Type x
$cto :: forall x. Rep Bounds_Type x -> Bounds_Type
to :: forall x. Rep Bounds_Type x -> Bounds_Type
Generic  )

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
$c== :: Criterion -> Criterion -> Bool
== :: Criterion -> Criterion -> Bool
$c/= :: Criterion -> Criterion -> Bool
/= :: Criterion -> Criterion -> Bool
Eq, (forall x. Criterion -> Rep Criterion x)
-> (forall x. Rep Criterion x -> Criterion) -> Generic Criterion
forall x. Rep Criterion x -> Criterion
forall x. Criterion -> Rep Criterion x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Criterion -> Rep Criterion x
from :: forall x. Criterion -> Rep Criterion x
$cto :: forall x. Rep Criterion x -> Criterion
to :: forall x. Rep Criterion x -> Criterion
Generic  )

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
$c== :: TreeAutomaton -> TreeAutomaton -> Bool
== :: TreeAutomaton -> TreeAutomaton -> Bool
$c/= :: TreeAutomaton -> TreeAutomaton -> Bool
/= :: TreeAutomaton -> TreeAutomaton -> Bool
Eq, (forall x. TreeAutomaton -> Rep TreeAutomaton x)
-> (forall x. Rep TreeAutomaton x -> TreeAutomaton)
-> Generic TreeAutomaton
forall x. Rep TreeAutomaton x -> TreeAutomaton
forall x. TreeAutomaton -> Rep TreeAutomaton x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. TreeAutomaton -> Rep TreeAutomaton x
from :: forall x. TreeAutomaton -> Rep TreeAutomaton x
$cto :: forall x. Rep TreeAutomaton x -> TreeAutomaton
to :: forall x. Rep TreeAutomaton x -> TreeAutomaton
Generic  )

data State = State Text -- Int -- Ha! Wrong.
   deriving ( Typeable, State -> State -> Bool
(State -> State -> Bool) -> (State -> State -> Bool) -> Eq State
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: State -> State -> Bool
== :: State -> State -> Bool
$c/= :: State -> State -> Bool
/= :: State -> State -> Bool
Eq, (forall x. State -> Rep State x)
-> (forall x. Rep State x -> State) -> Generic State
forall x. Rep State x -> State
forall x. State -> Rep State x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. State -> Rep State x
from :: forall x. State -> Rep State x
$cto :: forall x. Rep State x -> State
to :: forall x. Rep State x -> State
Generic  )

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
$c== :: Transition -> Transition -> Bool
== :: Transition -> Transition -> Bool
$c/= :: Transition -> Transition -> Bool
/= :: Transition -> Transition -> Bool
Eq, (forall x. Transition -> Rep Transition x)
-> (forall x. Rep Transition x -> Transition) -> Generic Transition
forall x. Rep Transition x -> Transition
forall x. Transition -> Rep Transition x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Transition -> Rep Transition x
from :: forall x. Transition -> Rep Transition x
$cto :: forall x. Rep Transition x -> Transition
to :: forall x. Rep Transition x -> Transition
Generic  )

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
$c== :: Transition_Lhs -> Transition_Lhs -> Bool
== :: Transition_Lhs -> Transition_Lhs -> Bool
$c/= :: Transition_Lhs -> Transition_Lhs -> Bool
/= :: Transition_Lhs -> Transition_Lhs -> Bool
Eq, (forall x. Transition_Lhs -> Rep Transition_Lhs x)
-> (forall x. Rep Transition_Lhs x -> Transition_Lhs)
-> Generic Transition_Lhs
forall x. Rep Transition_Lhs x -> Transition_Lhs
forall x. Transition_Lhs -> Rep Transition_Lhs x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Transition_Lhs -> Rep Transition_Lhs x
from :: forall x. Transition_Lhs -> Rep Transition_Lhs x
$cto :: forall x. Rep Transition_Lhs x -> Transition_Lhs
to :: forall x. Rep Transition_Lhs x -> Transition_Lhs
Generic  )

data Model
  = FiniteModel Int [Interpret]
  | RootLabeling
   deriving ( Typeable, Model -> Model -> Bool
(Model -> Model -> Bool) -> (Model -> Model -> Bool) -> Eq Model
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Model -> Model -> Bool
== :: Model -> Model -> Bool
$c/= :: Model -> Model -> Bool
/= :: Model -> Model -> Bool
Eq, (forall x. Model -> Rep Model x)
-> (forall x. Rep Model x -> Model) -> Generic Model
forall x. Rep Model x -> Model
forall x. Model -> Rep Model x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Model -> Rep Model x
from :: forall x. Model -> Rep Model x
$cto :: forall x. Rep Model x -> Model
to :: forall x. Rep Model x -> Model
Generic  )

data Mono = Weak | Strict
   deriving ( Typeable, Mono -> Mono -> Bool
(Mono -> Mono -> Bool) -> (Mono -> Mono -> Bool) -> Eq Mono
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Mono -> Mono -> Bool
== :: Mono -> Mono -> Bool
$c/= :: Mono -> Mono -> Bool
/= :: Mono -> Mono -> Bool
Eq, (forall x. Mono -> Rep Mono x)
-> (forall x. Rep Mono x -> Mono) -> Generic Mono
forall x. Rep Mono x -> Mono
forall x. Mono -> Rep Mono x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Mono -> Rep Mono x
from :: forall x. Mono -> Rep Mono x
$cto :: forall x. Rep Mono x -> Mono
to :: forall x. Rep Mono x -> Mono
Generic  )

data DpProof = PIsEmpty  
             | RedPairProc { DpProof -> Mono
rppMono :: Mono
                           , DpProof -> OrderingConstraintProof
rppOrderingConstraintProof :: OrderingConstraintProof
                           , DpProof -> DPS
rppDps                     :: DPS
                           , DpProof -> Maybe Trs
rppTrs :: Maybe Trs
                           , 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
$c== :: DpProof -> DpProof -> Bool
== :: DpProof -> DpProof -> Bool
$c/= :: DpProof -> DpProof -> Bool
/= :: DpProof -> DpProof -> Bool
Eq, (forall x. DpProof -> Rep DpProof x)
-> (forall x. Rep DpProof x -> DpProof) -> Generic DpProof
forall x. Rep DpProof x -> DpProof
forall x. DpProof -> Rep DpProof x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. DpProof -> Rep DpProof x
from :: forall x. DpProof -> Rep DpProof x
$cto :: forall x. Rep DpProof x -> DpProof
to :: forall x. Rep DpProof x -> DpProof
Generic  )

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
$c== :: DepGraphComponent -> DepGraphComponent -> Bool
== :: DepGraphComponent -> DepGraphComponent -> Bool
$c/= :: DepGraphComponent -> DepGraphComponent -> Bool
/= :: DepGraphComponent -> DepGraphComponent -> Bool
Eq, (forall x. DepGraphComponent -> Rep DepGraphComponent x)
-> (forall x. Rep DepGraphComponent x -> DepGraphComponent)
-> Generic DepGraphComponent
forall x. Rep DepGraphComponent x -> DepGraphComponent
forall x. DepGraphComponent -> Rep DepGraphComponent x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. DepGraphComponent -> Rep DepGraphComponent x
from :: forall x. DepGraphComponent -> Rep DepGraphComponent x
$cto :: forall x. Rep DepGraphComponent x -> DepGraphComponent
to :: forall x. Rep DepGraphComponent x -> DepGraphComponent
Generic  )

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
$c== :: OrderingConstraintProof -> OrderingConstraintProof -> Bool
== :: OrderingConstraintProof -> OrderingConstraintProof -> Bool
$c/= :: OrderingConstraintProof -> OrderingConstraintProof -> Bool
/= :: OrderingConstraintProof -> OrderingConstraintProof -> Bool
Eq, (forall x.
 OrderingConstraintProof -> Rep OrderingConstraintProof x)
-> (forall x.
    Rep OrderingConstraintProof x -> OrderingConstraintProof)
-> Generic OrderingConstraintProof
forall x. Rep OrderingConstraintProof x -> OrderingConstraintProof
forall x. OrderingConstraintProof -> Rep OrderingConstraintProof x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. OrderingConstraintProof -> Rep OrderingConstraintProof x
from :: forall x. OrderingConstraintProof -> Rep OrderingConstraintProof x
$cto :: forall x. Rep OrderingConstraintProof x -> OrderingConstraintProof
to :: forall x. Rep OrderingConstraintProof x -> OrderingConstraintProof
Generic  )

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
$c== :: RedPair -> RedPair -> Bool
== :: RedPair -> RedPair -> Bool
$c/= :: RedPair -> RedPair -> Bool
/= :: RedPair -> RedPair -> Bool
Eq, (forall x. RedPair -> Rep RedPair x)
-> (forall x. Rep RedPair x -> RedPair) -> Generic RedPair
forall x. Rep RedPair x -> RedPair
forall x. RedPair -> Rep RedPair x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. RedPair -> Rep RedPair x
from :: forall x. RedPair -> Rep RedPair x
$cto :: forall x. Rep RedPair x -> RedPair
to :: forall x. Rep RedPair x -> RedPair
Generic  )

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
$c== :: Interpretation -> Interpretation -> Bool
== :: Interpretation -> Interpretation -> Bool
$c/= :: Interpretation -> Interpretation -> Bool
/= :: Interpretation -> Interpretation -> Bool
Eq, (forall x. Interpretation -> Rep Interpretation x)
-> (forall x. Rep Interpretation x -> Interpretation)
-> Generic Interpretation
forall x. Rep Interpretation x -> Interpretation
forall x. Interpretation -> Rep Interpretation x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Interpretation -> Rep Interpretation x
from :: forall x. Interpretation -> Rep Interpretation x
$cto :: forall x. Rep Interpretation x -> Interpretation
to :: forall x. Rep Interpretation x -> Interpretation
Generic  )

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
$c== :: Interpretation_Type -> Interpretation_Type -> Bool
== :: Interpretation_Type -> Interpretation_Type -> Bool
$c/= :: Interpretation_Type -> Interpretation_Type -> Bool
/= :: Interpretation_Type -> Interpretation_Type -> Bool
Eq, (forall x. Interpretation_Type -> Rep Interpretation_Type x)
-> (forall x. Rep Interpretation_Type x -> Interpretation_Type)
-> Generic Interpretation_Type
forall x. Rep Interpretation_Type x -> Interpretation_Type
forall x. Interpretation_Type -> Rep Interpretation_Type x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Interpretation_Type -> Rep Interpretation_Type x
from :: forall x. Interpretation_Type -> Rep Interpretation_Type x
$cto :: forall x. Rep Interpretation_Type x -> Interpretation_Type
to :: forall x. Rep Interpretation_Type x -> Interpretation_Type
Generic  )

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
$c== :: Domain -> Domain -> Bool
== :: Domain -> Domain -> Bool
$c/= :: Domain -> Domain -> Bool
/= :: Domain -> Domain -> Bool
Eq, (forall x. Domain -> Rep Domain x)
-> (forall x. Rep Domain x -> Domain) -> Generic Domain
forall x. Rep Domain x -> Domain
forall x. Domain -> Rep Domain x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Domain -> Rep Domain x
from :: forall x. Domain -> Rep Domain x
$cto :: forall x. Rep Domain x -> Domain
to :: forall x. Rep Domain x -> Domain
Generic  )

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
$c== :: Interpret -> Interpret -> Bool
== :: Interpret -> Interpret -> Bool
$c/= :: Interpret -> Interpret -> Bool
/= :: Interpret -> Interpret -> Bool
Eq, (forall x. Interpret -> Rep Interpret x)
-> (forall x. Rep Interpret x -> Interpret) -> Generic Interpret
forall x. Rep Interpret x -> Interpret
forall x. Interpret -> Rep Interpret x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Interpret -> Rep Interpret x
from :: forall x. Interpret -> Rep Interpret x
$cto :: forall x. Rep Interpret x -> Interpret
to :: forall x. Rep Interpret x -> Interpret
Generic  )

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
$c== :: Value -> Value -> Bool
== :: Value -> Value -> Bool
$c/= :: Value -> Value -> Bool
/= :: Value -> Value -> Bool
Eq, (forall x. Value -> Rep Value x)
-> (forall x. Rep Value x -> Value) -> Generic Value
forall x. Rep Value x -> Value
forall x. Value -> Rep Value x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Value -> Rep Value x
from :: forall x. Value -> Rep Value x
$cto :: forall x. Rep Value x -> Value
to :: forall x. Rep Value x -> Value
Generic  )

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
$c== :: Polynomial -> Polynomial -> Bool
== :: Polynomial -> Polynomial -> Bool
$c/= :: Polynomial -> Polynomial -> Bool
/= :: Polynomial -> Polynomial -> Bool
Eq, (forall x. Polynomial -> Rep Polynomial x)
-> (forall x. Rep Polynomial x -> Polynomial) -> Generic Polynomial
forall x. Rep Polynomial x -> Polynomial
forall x. Polynomial -> Rep Polynomial x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Polynomial -> Rep Polynomial x
from :: forall x. Polynomial -> Rep Polynomial x
$cto :: forall x. Rep Polynomial x -> Polynomial
to :: forall x. Rep Polynomial x -> Polynomial
Generic  )

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
$c== :: ArithFunction -> ArithFunction -> Bool
== :: ArithFunction -> ArithFunction -> Bool
$c/= :: ArithFunction -> ArithFunction -> Bool
/= :: ArithFunction -> ArithFunction -> Bool
Eq, (forall x. ArithFunction -> Rep ArithFunction x)
-> (forall x. Rep ArithFunction x -> ArithFunction)
-> Generic ArithFunction
forall x. Rep ArithFunction x -> ArithFunction
forall x. ArithFunction -> Rep ArithFunction x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ArithFunction -> Rep ArithFunction x
from :: forall x. ArithFunction -> Rep ArithFunction x
$cto :: forall x. Rep ArithFunction x -> ArithFunction
to :: forall x. Rep ArithFunction x -> ArithFunction
Generic  )

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
$c== :: Symbol -> Symbol -> Bool
== :: Symbol -> Symbol -> Bool
$c/= :: Symbol -> Symbol -> Bool
/= :: Symbol -> Symbol -> Bool
Eq, Eq Symbol
Eq Symbol =>
(Symbol -> Symbol -> Ordering)
-> (Symbol -> Symbol -> Bool)
-> (Symbol -> Symbol -> Bool)
-> (Symbol -> Symbol -> Bool)
-> (Symbol -> Symbol -> Bool)
-> (Symbol -> Symbol -> Symbol)
-> (Symbol -> Symbol -> Symbol)
-> Ord Symbol
Symbol -> Symbol -> Bool
Symbol -> Symbol -> Ordering
Symbol -> Symbol -> Symbol
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Symbol -> Symbol -> Ordering
compare :: Symbol -> Symbol -> Ordering
$c< :: Symbol -> Symbol -> Bool
< :: Symbol -> Symbol -> Bool
$c<= :: Symbol -> Symbol -> Bool
<= :: Symbol -> Symbol -> Bool
$c> :: Symbol -> Symbol -> Bool
> :: Symbol -> Symbol -> Bool
$c>= :: Symbol -> Symbol -> Bool
>= :: Symbol -> Symbol -> Bool
$cmax :: Symbol -> Symbol -> Symbol
max :: Symbol -> Symbol -> Symbol
$cmin :: Symbol -> Symbol -> Symbol
min :: Symbol -> Symbol -> Symbol
Ord, (forall x. Symbol -> Rep Symbol x)
-> (forall x. Rep Symbol x -> Symbol) -> Generic Symbol
forall x. Rep Symbol x -> Symbol
forall x. Symbol -> Rep Symbol x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Symbol -> Rep Symbol x
from :: forall x. Symbol -> Rep Symbol x
$cto :: forall x. Rep Symbol x -> Symbol
to :: forall x. Rep Symbol x -> Symbol
Generic )
instance Hashable Symbol

instance Pretty Symbol where
  pretty :: forall ann. Symbol -> Doc ann
pretty Symbol
s = case Symbol
s of
    SymName Identifier
n -> Identifier -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Identifier -> Doc ann
pretty Identifier
n
    SymSharp Symbol
s -> Symbol -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Symbol -> Doc ann
pretty Symbol
s Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
"#"
    SymLabel Symbol
s Label
l -> Symbol -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Symbol -> Doc ann
pretty Symbol
s Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
"_" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Label -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Label -> Doc ann
pretty Label
l

instance Show Symbol where show :: Symbol -> String
show = Text -> String
TL.unpack (Text -> String) -> (Symbol -> Text) -> Symbol -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc Any -> Text
forall {ann}. Doc ann -> Text
render (Doc Any -> Text) -> (Symbol -> Doc Any) -> Symbol -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Symbol -> Doc ann
pretty


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
$c== :: Label -> Label -> Bool
== :: Label -> Label -> Bool
$c/= :: Label -> Label -> Bool
/= :: Label -> Label -> Bool
Eq, Eq Label
Eq Label =>
(Label -> Label -> Ordering)
-> (Label -> Label -> Bool)
-> (Label -> Label -> Bool)
-> (Label -> Label -> Bool)
-> (Label -> Label -> Bool)
-> (Label -> Label -> Label)
-> (Label -> Label -> Label)
-> Ord Label
Label -> Label -> Bool
Label -> Label -> Ordering
Label -> Label -> Label
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Label -> Label -> Ordering
compare :: Label -> Label -> Ordering
$c< :: Label -> Label -> Bool
< :: Label -> Label -> Bool
$c<= :: Label -> Label -> Bool
<= :: Label -> Label -> Bool
$c> :: Label -> Label -> Bool
> :: Label -> Label -> Bool
$c>= :: Label -> Label -> Bool
>= :: Label -> Label -> Bool
$cmax :: Label -> Label -> Label
max :: Label -> Label -> Label
$cmin :: Label -> Label -> Label
min :: Label -> Label -> Label
Ord, (forall x. Label -> Rep Label x)
-> (forall x. Rep Label x -> Label) -> Generic Label
forall x. Rep Label x -> Label
forall x. Label -> Rep Label x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Label -> Rep Label x
from :: forall x. Label -> Rep Label x
$cto :: forall x. Rep Label x -> Label
to :: forall x. Rep Label x -> Label
Generic )
instance Hashable Label

instance Pretty Label where
  pretty :: forall ann. Label -> Doc ann
pretty (LblNumber [Integer]
xs) = [Integer] -> Doc ann
forall ann. [Integer] -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty [Integer]
xs
  pretty (LblSymbol [Symbol]
xs) = [Symbol] -> Doc ann
forall ann. [Symbol] -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty [Symbol]
xs

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
$c== :: Exotic -> Exotic -> Bool
== :: Exotic -> Exotic -> Bool
$c/= :: Exotic -> Exotic -> Bool
/= :: Exotic -> Exotic -> Bool
Eq, (forall x. Exotic -> Rep Exotic x)
-> (forall x. Rep Exotic x -> Exotic) -> Generic Exotic
forall x. Rep Exotic x -> Exotic
forall x. Exotic -> Rep Exotic x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Exotic -> Rep Exotic x
from :: forall x. Exotic -> Rep Exotic x
$cto :: forall x. Rep Exotic x -> Exotic
to :: forall x. Rep Exotic x -> Exotic
Generic  )

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
$c== :: PathOrder -> PathOrder -> Bool
== :: PathOrder -> PathOrder -> Bool
$c/= :: PathOrder -> PathOrder -> Bool
/= :: PathOrder -> PathOrder -> Bool
Eq, (forall x. PathOrder -> Rep PathOrder x)
-> (forall x. Rep PathOrder x -> PathOrder) -> Generic PathOrder
forall x. Rep PathOrder x -> PathOrder
forall x. PathOrder -> Rep PathOrder x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. PathOrder -> Rep PathOrder x
from :: forall x. PathOrder -> Rep PathOrder x
$cto :: forall x. Rep PathOrder x -> PathOrder
to :: forall x. Rep PathOrder x -> PathOrder
Generic  )

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
$c== :: PrecedenceEntry -> PrecedenceEntry -> Bool
== :: PrecedenceEntry -> PrecedenceEntry -> Bool
$c/= :: PrecedenceEntry -> PrecedenceEntry -> Bool
/= :: PrecedenceEntry -> PrecedenceEntry -> Bool
Eq, (forall x. PrecedenceEntry -> Rep PrecedenceEntry x)
-> (forall x. Rep PrecedenceEntry x -> PrecedenceEntry)
-> Generic PrecedenceEntry
forall x. Rep PrecedenceEntry x -> PrecedenceEntry
forall x. PrecedenceEntry -> Rep PrecedenceEntry x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. PrecedenceEntry -> Rep PrecedenceEntry x
from :: forall x. PrecedenceEntry -> Rep PrecedenceEntry x
$cto :: forall x. Rep PrecedenceEntry x -> PrecedenceEntry
to :: forall x. Rep PrecedenceEntry x -> PrecedenceEntry
Generic  )

data ArgumentFilterEntry = 
     ArgumentFilterEntry { ArgumentFilterEntry -> Symbol
afeSymbol :: Symbol
                         , ArgumentFilterEntry -> Int
afeArity  :: Int
                         , ArgumentFilterEntry -> Either Int Position
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
$c== :: ArgumentFilterEntry -> ArgumentFilterEntry -> Bool
== :: ArgumentFilterEntry -> ArgumentFilterEntry -> Bool
$c/= :: ArgumentFilterEntry -> ArgumentFilterEntry -> Bool
/= :: ArgumentFilterEntry -> ArgumentFilterEntry -> Bool
Eq, (forall x. ArgumentFilterEntry -> Rep ArgumentFilterEntry x)
-> (forall x. Rep ArgumentFilterEntry x -> ArgumentFilterEntry)
-> Generic ArgumentFilterEntry
forall x. Rep ArgumentFilterEntry x -> ArgumentFilterEntry
forall x. ArgumentFilterEntry -> Rep ArgumentFilterEntry x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ArgumentFilterEntry -> Rep ArgumentFilterEntry x
from :: forall x. ArgumentFilterEntry -> Rep ArgumentFilterEntry x
$cto :: forall x. Rep ArgumentFilterEntry x -> ArgumentFilterEntry
to :: forall x. Rep ArgumentFilterEntry x -> ArgumentFilterEntry
Generic  )

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
$c== :: ACTerminationProof -> ACTerminationProof -> Bool
== :: ACTerminationProof -> ACTerminationProof -> Bool
$c/= :: ACTerminationProof -> ACTerminationProof -> Bool
/= :: ACTerminationProof -> ACTerminationProof -> Bool
Eq, (forall x. ACTerminationProof -> Rep ACTerminationProof x)
-> (forall x. Rep ACTerminationProof x -> ACTerminationProof)
-> Generic ACTerminationProof
forall x. Rep ACTerminationProof x -> ACTerminationProof
forall x. ACTerminationProof -> Rep ACTerminationProof x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ACTerminationProof -> Rep ACTerminationProof x
from :: forall x. ACTerminationProof -> Rep ACTerminationProof x
$cto :: forall x. Rep ACTerminationProof x -> ACTerminationProof
to :: forall x. Rep ACTerminationProof x -> ACTerminationProof
Generic  )