-- |
-- - Module      : Language.SMT2.Syntax
-- - Description : SMT language parser
-- - Maintainer  : ubikium@gmail.com
-- - Stability   : experimental
module Language.SMT2.Syntax where

import Data.List.NonEmpty (NonEmpty)
import qualified Data.Text as T
import Text.Parsec.Text (GenParser)

-- * Lexicons (Sec. 3.1)

--
-- Note: semantics should be provided by specific theories.
-- See Remark 1 of the refrence.

type Numeral = T.Text

type Decimal = T.Text

type Hexadecimal = T.Text

type Binary = T.Text

type StringLiteral = T.Text

type ReservedWord = T.Text

type Symbol = T.Text

type Keyword = T.Text

-- * S-expressions (Sec. 3.2)

data SpecConstant
  = SCNumeral Numeral
  | SCDecimal Decimal
  | SCHexadecimal Hexadecimal
  | SCBinary Binary
  | SCString StringLiteral
  deriving (SpecConstant -> SpecConstant -> Bool
(SpecConstant -> SpecConstant -> Bool)
-> (SpecConstant -> SpecConstant -> Bool) -> Eq SpecConstant
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SpecConstant -> SpecConstant -> Bool
$c/= :: SpecConstant -> SpecConstant -> Bool
== :: SpecConstant -> SpecConstant -> Bool
$c== :: SpecConstant -> SpecConstant -> Bool
Eq, Int -> SpecConstant -> ShowS
[SpecConstant] -> ShowS
SpecConstant -> String
(Int -> SpecConstant -> ShowS)
-> (SpecConstant -> String)
-> ([SpecConstant] -> ShowS)
-> Show SpecConstant
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SpecConstant] -> ShowS
$cshowList :: [SpecConstant] -> ShowS
show :: SpecConstant -> String
$cshow :: SpecConstant -> String
showsPrec :: Int -> SpecConstant -> ShowS
$cshowsPrec :: Int -> SpecConstant -> ShowS
Show)

data SExpr
  = SEConstant SpecConstant
  | SEReservedWord ReservedWord
  | SESymbol Symbol
  | SEKeyword Keyword
  | SEList SList
  deriving (SExpr -> SExpr -> Bool
(SExpr -> SExpr -> Bool) -> (SExpr -> SExpr -> Bool) -> Eq SExpr
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SExpr -> SExpr -> Bool
$c/= :: SExpr -> SExpr -> Bool
== :: SExpr -> SExpr -> Bool
$c== :: SExpr -> SExpr -> Bool
Eq, Int -> SExpr -> ShowS
[SExpr] -> ShowS
SExpr -> String
(Int -> SExpr -> ShowS)
-> (SExpr -> String) -> ([SExpr] -> ShowS) -> Show SExpr
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SExpr] -> ShowS
$cshowList :: [SExpr] -> ShowS
show :: SExpr -> String
$cshow :: SExpr -> String
showsPrec :: Int -> SExpr -> ShowS
$cshowsPrec :: Int -> SExpr -> ShowS
Show)

type SList = [SExpr]

-- * Identifiers (Sec 3.3)

data Index
  = IxNumeral Numeral
  | IxSymbol Symbol
  deriving (Index -> Index -> Bool
(Index -> Index -> Bool) -> (Index -> Index -> Bool) -> Eq Index
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Index -> Index -> Bool
$c/= :: Index -> Index -> Bool
== :: Index -> Index -> Bool
$c== :: Index -> Index -> Bool
Eq, Int -> Index -> ShowS
[Index] -> ShowS
Index -> String
(Int -> Index -> ShowS)
-> (Index -> String) -> ([Index] -> ShowS) -> Show Index
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Index] -> ShowS
$cshowList :: [Index] -> ShowS
show :: Index -> String
$cshow :: Index -> String
showsPrec :: Int -> Index -> ShowS
$cshowsPrec :: Int -> Index -> ShowS
Show)

data Identifier
  = IdSymbol Symbol
  | IdIndexed Symbol (NonEmpty Index)
  deriving (Identifier -> Identifier -> Bool
(Identifier -> Identifier -> Bool)
-> (Identifier -> Identifier -> Bool) -> Eq Identifier
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Identifier -> Identifier -> Bool
$c/= :: Identifier -> Identifier -> Bool
== :: Identifier -> Identifier -> Bool
$c== :: Identifier -> Identifier -> Bool
Eq, Int -> Identifier -> ShowS
[Identifier] -> ShowS
Identifier -> String
(Int -> Identifier -> ShowS)
-> (Identifier -> String)
-> ([Identifier] -> ShowS)
-> Show Identifier
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Identifier] -> ShowS
$cshowList :: [Identifier] -> ShowS
show :: Identifier -> String
$cshow :: Identifier -> String
showsPrec :: Int -> Identifier -> ShowS
$cshowsPrec :: Int -> Identifier -> ShowS
Show)

-- * Attributes (Sec. 3.4)

data AttributeValue
  = AttrValSpecConstant SpecConstant
  | AttrValSymbol Symbol
  | AttrValSList SList
  deriving (AttributeValue -> AttributeValue -> Bool
(AttributeValue -> AttributeValue -> Bool)
-> (AttributeValue -> AttributeValue -> Bool) -> Eq AttributeValue
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: AttributeValue -> AttributeValue -> Bool
$c/= :: AttributeValue -> AttributeValue -> Bool
== :: AttributeValue -> AttributeValue -> Bool
$c== :: AttributeValue -> AttributeValue -> Bool
Eq, Int -> AttributeValue -> ShowS
[AttributeValue] -> ShowS
AttributeValue -> String
(Int -> AttributeValue -> ShowS)
-> (AttributeValue -> String)
-> ([AttributeValue] -> ShowS)
-> Show AttributeValue
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [AttributeValue] -> ShowS
$cshowList :: [AttributeValue] -> ShowS
show :: AttributeValue -> String
$cshow :: AttributeValue -> String
showsPrec :: Int -> AttributeValue -> ShowS
$cshowsPrec :: Int -> AttributeValue -> ShowS
Show)

data Attribute
  = AttrKey Keyword
  | AttrKeyValue Keyword AttributeValue
  deriving (Attribute -> Attribute -> Bool
(Attribute -> Attribute -> Bool)
-> (Attribute -> Attribute -> Bool) -> Eq Attribute
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Attribute -> Attribute -> Bool
$c/= :: Attribute -> Attribute -> Bool
== :: Attribute -> Attribute -> Bool
$c== :: Attribute -> Attribute -> Bool
Eq, Int -> Attribute -> ShowS
[Attribute] -> ShowS
Attribute -> String
(Int -> Attribute -> ShowS)
-> (Attribute -> String)
-> ([Attribute] -> ShowS)
-> Show Attribute
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Attribute] -> ShowS
$cshowList :: [Attribute] -> ShowS
show :: Attribute -> String
$cshow :: Attribute -> String
showsPrec :: Int -> Attribute -> ShowS
$cshowsPrec :: Int -> Attribute -> ShowS
Show)

-- * Sorts (Sec 3.5)

data Sort
  = SortSymbol Identifier
  | SortParameter Identifier (NonEmpty Sort)
  deriving (Sort -> Sort -> Bool
(Sort -> Sort -> Bool) -> (Sort -> Sort -> Bool) -> Eq Sort
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Sort -> Sort -> Bool
$c/= :: Sort -> Sort -> Bool
== :: Sort -> Sort -> Bool
$c== :: Sort -> Sort -> Bool
Eq, Int -> Sort -> ShowS
[Sort] -> ShowS
Sort -> String
(Int -> Sort -> ShowS)
-> (Sort -> String) -> ([Sort] -> ShowS) -> Show Sort
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Sort] -> ShowS
$cshowList :: [Sort] -> ShowS
show :: Sort -> String
$cshow :: Sort -> String
showsPrec :: Int -> Sort -> ShowS
$cshowsPrec :: Int -> Sort -> ShowS
Show)

-- * Terms and Formulas (Sec 3.6)

data QualIdentifier
  = Unqualified Identifier
  | Qualified Identifier Sort
  deriving (QualIdentifier -> QualIdentifier -> Bool
(QualIdentifier -> QualIdentifier -> Bool)
-> (QualIdentifier -> QualIdentifier -> Bool) -> Eq QualIdentifier
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: QualIdentifier -> QualIdentifier -> Bool
$c/= :: QualIdentifier -> QualIdentifier -> Bool
== :: QualIdentifier -> QualIdentifier -> Bool
$c== :: QualIdentifier -> QualIdentifier -> Bool
Eq, Int -> QualIdentifier -> ShowS
[QualIdentifier] -> ShowS
QualIdentifier -> String
(Int -> QualIdentifier -> ShowS)
-> (QualIdentifier -> String)
-> ([QualIdentifier] -> ShowS)
-> Show QualIdentifier
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [QualIdentifier] -> ShowS
$cshowList :: [QualIdentifier] -> ShowS
show :: QualIdentifier -> String
$cshow :: QualIdentifier -> String
showsPrec :: Int -> QualIdentifier -> ShowS
$cshowsPrec :: Int -> QualIdentifier -> ShowS
Show)

data VarBinding = VarBinding Symbol Term
  deriving (VarBinding -> VarBinding -> Bool
(VarBinding -> VarBinding -> Bool)
-> (VarBinding -> VarBinding -> Bool) -> Eq VarBinding
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: VarBinding -> VarBinding -> Bool
$c/= :: VarBinding -> VarBinding -> Bool
== :: VarBinding -> VarBinding -> Bool
$c== :: VarBinding -> VarBinding -> Bool
Eq, Int -> VarBinding -> ShowS
[VarBinding] -> ShowS
VarBinding -> String
(Int -> VarBinding -> ShowS)
-> (VarBinding -> String)
-> ([VarBinding] -> ShowS)
-> Show VarBinding
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [VarBinding] -> ShowS
$cshowList :: [VarBinding] -> ShowS
show :: VarBinding -> String
$cshow :: VarBinding -> String
showsPrec :: Int -> VarBinding -> ShowS
$cshowsPrec :: Int -> VarBinding -> ShowS
Show)

data SortedVar = SortedVar Symbol Sort
  deriving (SortedVar -> SortedVar -> Bool
(SortedVar -> SortedVar -> Bool)
-> (SortedVar -> SortedVar -> Bool) -> Eq SortedVar
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SortedVar -> SortedVar -> Bool
$c/= :: SortedVar -> SortedVar -> Bool
== :: SortedVar -> SortedVar -> Bool
$c== :: SortedVar -> SortedVar -> Bool
Eq, Int -> SortedVar -> ShowS
[SortedVar] -> ShowS
SortedVar -> String
(Int -> SortedVar -> ShowS)
-> (SortedVar -> String)
-> ([SortedVar] -> ShowS)
-> Show SortedVar
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SortedVar] -> ShowS
$cshowList :: [SortedVar] -> ShowS
show :: SortedVar -> String
$cshow :: SortedVar -> String
showsPrec :: Int -> SortedVar -> ShowS
$cshowsPrec :: Int -> SortedVar -> ShowS
Show)

data MatchPattern
  = MPVariable Symbol
  | MPConstructor Symbol (NonEmpty Symbol)
  deriving (MatchPattern -> MatchPattern -> Bool
(MatchPattern -> MatchPattern -> Bool)
-> (MatchPattern -> MatchPattern -> Bool) -> Eq MatchPattern
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: MatchPattern -> MatchPattern -> Bool
$c/= :: MatchPattern -> MatchPattern -> Bool
== :: MatchPattern -> MatchPattern -> Bool
$c== :: MatchPattern -> MatchPattern -> Bool
Eq, Int -> MatchPattern -> ShowS
[MatchPattern] -> ShowS
MatchPattern -> String
(Int -> MatchPattern -> ShowS)
-> (MatchPattern -> String)
-> ([MatchPattern] -> ShowS)
-> Show MatchPattern
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [MatchPattern] -> ShowS
$cshowList :: [MatchPattern] -> ShowS
show :: MatchPattern -> String
$cshow :: MatchPattern -> String
showsPrec :: Int -> MatchPattern -> ShowS
$cshowsPrec :: Int -> MatchPattern -> ShowS
Show)

data MatchCase = MatchCase MatchPattern Term
  deriving (MatchCase -> MatchCase -> Bool
(MatchCase -> MatchCase -> Bool)
-> (MatchCase -> MatchCase -> Bool) -> Eq MatchCase
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: MatchCase -> MatchCase -> Bool
$c/= :: MatchCase -> MatchCase -> Bool
== :: MatchCase -> MatchCase -> Bool
$c== :: MatchCase -> MatchCase -> Bool
Eq, Int -> MatchCase -> ShowS
[MatchCase] -> ShowS
MatchCase -> String
(Int -> MatchCase -> ShowS)
-> (MatchCase -> String)
-> ([MatchCase] -> ShowS)
-> Show MatchCase
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [MatchCase] -> ShowS
$cshowList :: [MatchCase] -> ShowS
show :: MatchCase -> String
$cshow :: MatchCase -> String
showsPrec :: Int -> MatchCase -> ShowS
$cshowsPrec :: Int -> MatchCase -> ShowS
Show)

data Term
  = TermSpecConstant SpecConstant
  | TermQualIdentifier QualIdentifier
  | TermApplication QualIdentifier (NonEmpty Term)
  | TermLet (NonEmpty VarBinding) Term
  | TermForall (NonEmpty SortedVar) Term
  | TermExists (NonEmpty SortedVar) Term
  | TermMatch Term (NonEmpty MatchCase)
  | TermAnnotation Term (NonEmpty Attribute)
  deriving (Term -> Term -> Bool
(Term -> Term -> Bool) -> (Term -> Term -> Bool) -> Eq Term
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Term -> Term -> Bool
$c/= :: Term -> Term -> Bool
== :: Term -> Term -> Bool
$c== :: Term -> Term -> Bool
Eq, Int -> Term -> ShowS
[Term] -> ShowS
Term -> String
(Int -> Term -> ShowS)
-> (Term -> String) -> ([Term] -> ShowS) -> Show Term
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Term] -> ShowS
$cshowList :: [Term] -> ShowS
show :: Term -> String
$cshow :: Term -> String
showsPrec :: Int -> Term -> ShowS
$cshowsPrec :: Int -> Term -> ShowS
Show)

-- * Theory declarations (Sec 3.7)

data SortSymbolDecl = SortSymbolDecl Identifier Numeral [Attribute]
  deriving (SortSymbolDecl -> SortSymbolDecl -> Bool
(SortSymbolDecl -> SortSymbolDecl -> Bool)
-> (SortSymbolDecl -> SortSymbolDecl -> Bool) -> Eq SortSymbolDecl
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SortSymbolDecl -> SortSymbolDecl -> Bool
$c/= :: SortSymbolDecl -> SortSymbolDecl -> Bool
== :: SortSymbolDecl -> SortSymbolDecl -> Bool
$c== :: SortSymbolDecl -> SortSymbolDecl -> Bool
Eq, Int -> SortSymbolDecl -> ShowS
[SortSymbolDecl] -> ShowS
SortSymbolDecl -> String
(Int -> SortSymbolDecl -> ShowS)
-> (SortSymbolDecl -> String)
-> ([SortSymbolDecl] -> ShowS)
-> Show SortSymbolDecl
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SortSymbolDecl] -> ShowS
$cshowList :: [SortSymbolDecl] -> ShowS
show :: SortSymbolDecl -> String
$cshow :: SortSymbolDecl -> String
showsPrec :: Int -> SortSymbolDecl -> ShowS
$cshowsPrec :: Int -> SortSymbolDecl -> ShowS
Show)

data MetaSpecConstant = MSC_NUMERAL | MSC_DECIMAL | MSC_STRING
  deriving (MetaSpecConstant -> MetaSpecConstant -> Bool
(MetaSpecConstant -> MetaSpecConstant -> Bool)
-> (MetaSpecConstant -> MetaSpecConstant -> Bool)
-> Eq MetaSpecConstant
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: MetaSpecConstant -> MetaSpecConstant -> Bool
$c/= :: MetaSpecConstant -> MetaSpecConstant -> Bool
== :: MetaSpecConstant -> MetaSpecConstant -> Bool
$c== :: MetaSpecConstant -> MetaSpecConstant -> Bool
Eq, Int -> MetaSpecConstant -> ShowS
[MetaSpecConstant] -> ShowS
MetaSpecConstant -> String
(Int -> MetaSpecConstant -> ShowS)
-> (MetaSpecConstant -> String)
-> ([MetaSpecConstant] -> ShowS)
-> Show MetaSpecConstant
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [MetaSpecConstant] -> ShowS
$cshowList :: [MetaSpecConstant] -> ShowS
show :: MetaSpecConstant -> String
$cshow :: MetaSpecConstant -> String
showsPrec :: Int -> MetaSpecConstant -> ShowS
$cshowsPrec :: Int -> MetaSpecConstant -> ShowS
Show)

data FunSymbolDecl
  = FunConstant SpecConstant Sort [Attribute]
  | FunMeta MetaSpecConstant Sort [Attribute]
  | -- | potentially overloaded
    FunIdentifier Identifier (NonEmpty Sort) [Attribute]
  deriving (FunSymbolDecl -> FunSymbolDecl -> Bool
(FunSymbolDecl -> FunSymbolDecl -> Bool)
-> (FunSymbolDecl -> FunSymbolDecl -> Bool) -> Eq FunSymbolDecl
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: FunSymbolDecl -> FunSymbolDecl -> Bool
$c/= :: FunSymbolDecl -> FunSymbolDecl -> Bool
== :: FunSymbolDecl -> FunSymbolDecl -> Bool
$c== :: FunSymbolDecl -> FunSymbolDecl -> Bool
Eq, Int -> FunSymbolDecl -> ShowS
[FunSymbolDecl] -> ShowS
FunSymbolDecl -> String
(Int -> FunSymbolDecl -> ShowS)
-> (FunSymbolDecl -> String)
-> ([FunSymbolDecl] -> ShowS)
-> Show FunSymbolDecl
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [FunSymbolDecl] -> ShowS
$cshowList :: [FunSymbolDecl] -> ShowS
show :: FunSymbolDecl -> String
$cshow :: FunSymbolDecl -> String
showsPrec :: Int -> FunSymbolDecl -> ShowS
$cshowsPrec :: Int -> FunSymbolDecl -> ShowS
Show)

data ParFunSymbolDecl
  = -- | non-parametric
    NonPar FunSymbolDecl
  | -- | parametric
    Par (NonEmpty Symbol) Identifier (NonEmpty Sort) [Attribute]
  deriving (ParFunSymbolDecl -> ParFunSymbolDecl -> Bool
(ParFunSymbolDecl -> ParFunSymbolDecl -> Bool)
-> (ParFunSymbolDecl -> ParFunSymbolDecl -> Bool)
-> Eq ParFunSymbolDecl
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ParFunSymbolDecl -> ParFunSymbolDecl -> Bool
$c/= :: ParFunSymbolDecl -> ParFunSymbolDecl -> Bool
== :: ParFunSymbolDecl -> ParFunSymbolDecl -> Bool
$c== :: ParFunSymbolDecl -> ParFunSymbolDecl -> Bool
Eq, Int -> ParFunSymbolDecl -> ShowS
[ParFunSymbolDecl] -> ShowS
ParFunSymbolDecl -> String
(Int -> ParFunSymbolDecl -> ShowS)
-> (ParFunSymbolDecl -> String)
-> ([ParFunSymbolDecl] -> ShowS)
-> Show ParFunSymbolDecl
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ParFunSymbolDecl] -> ShowS
$cshowList :: [ParFunSymbolDecl] -> ShowS
show :: ParFunSymbolDecl -> String
$cshow :: ParFunSymbolDecl -> String
showsPrec :: Int -> ParFunSymbolDecl -> ShowS
$cshowsPrec :: Int -> ParFunSymbolDecl -> ShowS
Show)

data TheoryAttribute
  = TASorts (NonEmpty SortSymbolDecl)
  | TAFuns (NonEmpty ParFunSymbolDecl)
  | TASortsDescription StringLiteral
  | TAFunsDescription StringLiteral
  | TADefinition StringLiteral
  | TAValues StringLiteral
  | TANotes StringLiteral
  | TAAttr Attribute
  deriving (TheoryAttribute -> TheoryAttribute -> Bool
(TheoryAttribute -> TheoryAttribute -> Bool)
-> (TheoryAttribute -> TheoryAttribute -> Bool)
-> Eq TheoryAttribute
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TheoryAttribute -> TheoryAttribute -> Bool
$c/= :: TheoryAttribute -> TheoryAttribute -> Bool
== :: TheoryAttribute -> TheoryAttribute -> Bool
$c== :: TheoryAttribute -> TheoryAttribute -> Bool
Eq, Int -> TheoryAttribute -> ShowS
[TheoryAttribute] -> ShowS
TheoryAttribute -> String
(Int -> TheoryAttribute -> ShowS)
-> (TheoryAttribute -> String)
-> ([TheoryAttribute] -> ShowS)
-> Show TheoryAttribute
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TheoryAttribute] -> ShowS
$cshowList :: [TheoryAttribute] -> ShowS
show :: TheoryAttribute -> String
$cshow :: TheoryAttribute -> String
showsPrec :: Int -> TheoryAttribute -> ShowS
$cshowsPrec :: Int -> TheoryAttribute -> ShowS
Show)

data TheoryDecl = TheoryDecl Symbol (NonEmpty TheoryAttribute)
  deriving (TheoryDecl -> TheoryDecl -> Bool
(TheoryDecl -> TheoryDecl -> Bool)
-> (TheoryDecl -> TheoryDecl -> Bool) -> Eq TheoryDecl
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TheoryDecl -> TheoryDecl -> Bool
$c/= :: TheoryDecl -> TheoryDecl -> Bool
== :: TheoryDecl -> TheoryDecl -> Bool
$c== :: TheoryDecl -> TheoryDecl -> Bool
Eq, Int -> TheoryDecl -> ShowS
[TheoryDecl] -> ShowS
TheoryDecl -> String
(Int -> TheoryDecl -> ShowS)
-> (TheoryDecl -> String)
-> ([TheoryDecl] -> ShowS)
-> Show TheoryDecl
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TheoryDecl] -> ShowS
$cshowList :: [TheoryDecl] -> ShowS
show :: TheoryDecl -> String
$cshow :: TheoryDecl -> String
showsPrec :: Int -> TheoryDecl -> ShowS
$cshowsPrec :: Int -> TheoryDecl -> ShowS
Show)

-- * Logic Declarations (Sec 3.8)

data LogicAttribute
  = LATheories (NonEmpty Symbol)
  | LALanguage StringLiteral
  | LAExtensions StringLiteral
  | LAValues StringLiteral
  | LANotes StringLiteral
  | LAAttr Attribute
  deriving (LogicAttribute -> LogicAttribute -> Bool
(LogicAttribute -> LogicAttribute -> Bool)
-> (LogicAttribute -> LogicAttribute -> Bool) -> Eq LogicAttribute
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: LogicAttribute -> LogicAttribute -> Bool
$c/= :: LogicAttribute -> LogicAttribute -> Bool
== :: LogicAttribute -> LogicAttribute -> Bool
$c== :: LogicAttribute -> LogicAttribute -> Bool
Eq, Int -> LogicAttribute -> ShowS
[LogicAttribute] -> ShowS
LogicAttribute -> String
(Int -> LogicAttribute -> ShowS)
-> (LogicAttribute -> String)
-> ([LogicAttribute] -> ShowS)
-> Show LogicAttribute
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [LogicAttribute] -> ShowS
$cshowList :: [LogicAttribute] -> ShowS
show :: LogicAttribute -> String
$cshow :: LogicAttribute -> String
showsPrec :: Int -> LogicAttribute -> ShowS
$cshowsPrec :: Int -> LogicAttribute -> ShowS
Show)

data Logic = Logic Symbol (NonEmpty LogicAttribute)
  deriving (Logic -> Logic -> Bool
(Logic -> Logic -> Bool) -> (Logic -> Logic -> Bool) -> Eq Logic
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Logic -> Logic -> Bool
$c/= :: Logic -> Logic -> Bool
== :: Logic -> Logic -> Bool
$c== :: Logic -> Logic -> Bool
Eq, Int -> Logic -> ShowS
[Logic] -> ShowS
Logic -> String
(Int -> Logic -> ShowS)
-> (Logic -> String) -> ([Logic] -> ShowS) -> Show Logic
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Logic] -> ShowS
$cshowList :: [Logic] -> ShowS
show :: Logic -> String
$cshow :: Logic -> String
showsPrec :: Int -> Logic -> ShowS
$cshowsPrec :: Int -> Logic -> ShowS
Show)

-- * Scripts (Sec 3.9)

data SortDec = SortDec Symbol Numeral
  deriving (SortDec -> SortDec -> Bool
(SortDec -> SortDec -> Bool)
-> (SortDec -> SortDec -> Bool) -> Eq SortDec
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SortDec -> SortDec -> Bool
$c/= :: SortDec -> SortDec -> Bool
== :: SortDec -> SortDec -> Bool
$c== :: SortDec -> SortDec -> Bool
Eq, Int -> SortDec -> ShowS
[SortDec] -> ShowS
SortDec -> String
(Int -> SortDec -> ShowS)
-> (SortDec -> String) -> ([SortDec] -> ShowS) -> Show SortDec
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SortDec] -> ShowS
$cshowList :: [SortDec] -> ShowS
show :: SortDec -> String
$cshow :: SortDec -> String
showsPrec :: Int -> SortDec -> ShowS
$cshowsPrec :: Int -> SortDec -> ShowS
Show)

data SelectorDec = SelectorDec Symbol Sort
  deriving (SelectorDec -> SelectorDec -> Bool
(SelectorDec -> SelectorDec -> Bool)
-> (SelectorDec -> SelectorDec -> Bool) -> Eq SelectorDec
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SelectorDec -> SelectorDec -> Bool
$c/= :: SelectorDec -> SelectorDec -> Bool
== :: SelectorDec -> SelectorDec -> Bool
$c== :: SelectorDec -> SelectorDec -> Bool
Eq, Int -> SelectorDec -> ShowS
[SelectorDec] -> ShowS
SelectorDec -> String
(Int -> SelectorDec -> ShowS)
-> (SelectorDec -> String)
-> ([SelectorDec] -> ShowS)
-> Show SelectorDec
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SelectorDec] -> ShowS
$cshowList :: [SelectorDec] -> ShowS
show :: SelectorDec -> String
$cshow :: SelectorDec -> String
showsPrec :: Int -> SelectorDec -> ShowS
$cshowsPrec :: Int -> SelectorDec -> ShowS
Show)

data ConstructorDec = ConstructorDec Symbol [SelectorDec]
  deriving (ConstructorDec -> ConstructorDec -> Bool
(ConstructorDec -> ConstructorDec -> Bool)
-> (ConstructorDec -> ConstructorDec -> Bool) -> Eq ConstructorDec
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ConstructorDec -> ConstructorDec -> Bool
$c/= :: ConstructorDec -> ConstructorDec -> Bool
== :: ConstructorDec -> ConstructorDec -> Bool
$c== :: ConstructorDec -> ConstructorDec -> Bool
Eq, Int -> ConstructorDec -> ShowS
[ConstructorDec] -> ShowS
ConstructorDec -> String
(Int -> ConstructorDec -> ShowS)
-> (ConstructorDec -> String)
-> ([ConstructorDec] -> ShowS)
-> Show ConstructorDec
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ConstructorDec] -> ShowS
$cshowList :: [ConstructorDec] -> ShowS
show :: ConstructorDec -> String
$cshow :: ConstructorDec -> String
showsPrec :: Int -> ConstructorDec -> ShowS
$cshowsPrec :: Int -> ConstructorDec -> ShowS
Show)

data DatatypeDec
  = DDNonparametric (NonEmpty ConstructorDec)
  | DDParametric (NonEmpty Symbol) (NonEmpty ConstructorDec)
  deriving (DatatypeDec -> DatatypeDec -> Bool
(DatatypeDec -> DatatypeDec -> Bool)
-> (DatatypeDec -> DatatypeDec -> Bool) -> Eq DatatypeDec
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DatatypeDec -> DatatypeDec -> Bool
$c/= :: DatatypeDec -> DatatypeDec -> Bool
== :: DatatypeDec -> DatatypeDec -> Bool
$c== :: DatatypeDec -> DatatypeDec -> Bool
Eq, Int -> DatatypeDec -> ShowS
[DatatypeDec] -> ShowS
DatatypeDec -> String
(Int -> DatatypeDec -> ShowS)
-> (DatatypeDec -> String)
-> ([DatatypeDec] -> ShowS)
-> Show DatatypeDec
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DatatypeDec] -> ShowS
$cshowList :: [DatatypeDec] -> ShowS
show :: DatatypeDec -> String
$cshow :: DatatypeDec -> String
showsPrec :: Int -> DatatypeDec -> ShowS
$cshowsPrec :: Int -> DatatypeDec -> ShowS
Show)

data FunctionDec = FunctionDec Symbol [SortedVar] Sort
  deriving (FunctionDec -> FunctionDec -> Bool
(FunctionDec -> FunctionDec -> Bool)
-> (FunctionDec -> FunctionDec -> Bool) -> Eq FunctionDec
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: FunctionDec -> FunctionDec -> Bool
$c/= :: FunctionDec -> FunctionDec -> Bool
== :: FunctionDec -> FunctionDec -> Bool
$c== :: FunctionDec -> FunctionDec -> Bool
Eq, Int -> FunctionDec -> ShowS
[FunctionDec] -> ShowS
FunctionDec -> String
(Int -> FunctionDec -> ShowS)
-> (FunctionDec -> String)
-> ([FunctionDec] -> ShowS)
-> Show FunctionDec
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [FunctionDec] -> ShowS
$cshowList :: [FunctionDec] -> ShowS
show :: FunctionDec -> String
$cshow :: FunctionDec -> String
showsPrec :: Int -> FunctionDec -> ShowS
$cshowsPrec :: Int -> FunctionDec -> ShowS
Show)

data FunctionDef = FunctionDef Symbol [SortedVar] Sort Term
  deriving (FunctionDef -> FunctionDef -> Bool
(FunctionDef -> FunctionDef -> Bool)
-> (FunctionDef -> FunctionDef -> Bool) -> Eq FunctionDef
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: FunctionDef -> FunctionDef -> Bool
$c/= :: FunctionDef -> FunctionDef -> Bool
== :: FunctionDef -> FunctionDef -> Bool
$c== :: FunctionDef -> FunctionDef -> Bool
Eq, Int -> FunctionDef -> ShowS
[FunctionDef] -> ShowS
FunctionDef -> String
(Int -> FunctionDef -> ShowS)
-> (FunctionDef -> String)
-> ([FunctionDef] -> ShowS)
-> Show FunctionDef
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [FunctionDef] -> ShowS
$cshowList :: [FunctionDef] -> ShowS
show :: FunctionDef -> String
$cshow :: FunctionDef -> String
showsPrec :: Int -> FunctionDef -> ShowS
$cshowsPrec :: Int -> FunctionDef -> ShowS
Show)

data PropLiteral
  = PLPositive Symbol
  | PLNegative Symbol
  deriving (PropLiteral -> PropLiteral -> Bool
(PropLiteral -> PropLiteral -> Bool)
-> (PropLiteral -> PropLiteral -> Bool) -> Eq PropLiteral
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PropLiteral -> PropLiteral -> Bool
$c/= :: PropLiteral -> PropLiteral -> Bool
== :: PropLiteral -> PropLiteral -> Bool
$c== :: PropLiteral -> PropLiteral -> Bool
Eq, Int -> PropLiteral -> ShowS
[PropLiteral] -> ShowS
PropLiteral -> String
(Int -> PropLiteral -> ShowS)
-> (PropLiteral -> String)
-> ([PropLiteral] -> ShowS)
-> Show PropLiteral
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PropLiteral] -> ShowS
$cshowList :: [PropLiteral] -> ShowS
show :: PropLiteral -> String
$cshow :: PropLiteral -> String
showsPrec :: Int -> PropLiteral -> ShowS
$cshowsPrec :: Int -> PropLiteral -> ShowS
Show)

data Command
  = Assert Term
  | CheckSat
  | CheckSatAssuming [PropLiteral]
  | DeclareConst Symbol Sort
  | DeclareDatatype Symbol DatatypeDec
  | -- | same number
    DeclareDatatypes (NonEmpty SortDec) (NonEmpty DatatypeDec)
  | DeclareFun Symbol [Sort] Sort
  | DeclareSort Symbol Numeral
  | DefineFun FunctionDef
  | DefineFunRec FunctionDef
  | -- | same number
    DefineFunsRec (NonEmpty FunctionDec) (NonEmpty Term)
  | DefineSort Symbol [Symbol] Sort
  | Echo StringLiteral
  | Exit
  | GetAssertions
  | GetAssignment
  | GetInfo InfoFlag
  | GetModel
  | GetOption Keyword
  | GetProof
  | GetUnsatAssumptions
  | GetUnsatCore
  | GetValue (NonEmpty Term)
  | Pop Numeral
  | Push Numeral
  | Reset
  | ResetAssertions
  | SetInfo Attribute
  | SetLogic Symbol
  | SetOption ScriptOption
  deriving (Command -> Command -> Bool
(Command -> Command -> Bool)
-> (Command -> Command -> Bool) -> Eq Command
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Command -> Command -> Bool
$c/= :: Command -> Command -> Bool
== :: Command -> Command -> Bool
$c== :: Command -> Command -> Bool
Eq, Int -> Command -> ShowS
[Command] -> ShowS
Command -> String
(Int -> Command -> ShowS)
-> (Command -> String) -> ([Command] -> ShowS) -> Show Command
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Command] -> ShowS
$cshowList :: [Command] -> ShowS
show :: Command -> String
$cshow :: Command -> String
showsPrec :: Int -> Command -> ShowS
$cshowsPrec :: Int -> Command -> ShowS
Show)

type Script = [Command]

data BValue = BTrue | BFalse
  deriving (BValue -> BValue -> Bool
(BValue -> BValue -> Bool)
-> (BValue -> BValue -> Bool) -> Eq BValue
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: BValue -> BValue -> Bool
$c/= :: BValue -> BValue -> Bool
== :: BValue -> BValue -> Bool
$c== :: BValue -> BValue -> Bool
Eq, Int -> BValue -> ShowS
[BValue] -> ShowS
BValue -> String
(Int -> BValue -> ShowS)
-> (BValue -> String) -> ([BValue] -> ShowS) -> Show BValue
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [BValue] -> ShowS
$cshowList :: [BValue] -> ShowS
show :: BValue -> String
$cshow :: BValue -> String
showsPrec :: Int -> BValue -> ShowS
$cshowsPrec :: Int -> BValue -> ShowS
Show)

data ScriptOption
  = DiagnosticOutputChannel StringLiteral
  | GlobalDeclarations BValue
  | InteractiveMode BValue
  | PrintSuccess BValue
  | ProduceAssertions BValue
  | ProduceAssignments BValue
  | ProduceModels BValue
  | ProduceProofs BValue
  | ProduceUnsatAssumptions BValue
  | ProduceUnsatCores BValue
  | RandomSeed Numeral
  | RegularOutputChannel StringLiteral
  | ReproducibleResourceLimit Numeral
  | Verbosity Numeral
  | OptionAttr Attribute
  deriving (ScriptOption -> ScriptOption -> Bool
(ScriptOption -> ScriptOption -> Bool)
-> (ScriptOption -> ScriptOption -> Bool) -> Eq ScriptOption
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ScriptOption -> ScriptOption -> Bool
$c/= :: ScriptOption -> ScriptOption -> Bool
== :: ScriptOption -> ScriptOption -> Bool
$c== :: ScriptOption -> ScriptOption -> Bool
Eq, Int -> ScriptOption -> ShowS
[ScriptOption] -> ShowS
ScriptOption -> String
(Int -> ScriptOption -> ShowS)
-> (ScriptOption -> String)
-> ([ScriptOption] -> ShowS)
-> Show ScriptOption
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ScriptOption] -> ShowS
$cshowList :: [ScriptOption] -> ShowS
show :: ScriptOption -> String
$cshow :: ScriptOption -> String
showsPrec :: Int -> ScriptOption -> ShowS
$cshowsPrec :: Int -> ScriptOption -> ShowS
Show)

data InfoFlag
  = AllStatistics
  | AssertionStackLevels
  | Authors
  | ErrorBehavior
  | Name
  | ReasonUnknown
  | Version
  | IFKeyword Keyword
  deriving (InfoFlag -> InfoFlag -> Bool
(InfoFlag -> InfoFlag -> Bool)
-> (InfoFlag -> InfoFlag -> Bool) -> Eq InfoFlag
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: InfoFlag -> InfoFlag -> Bool
$c/= :: InfoFlag -> InfoFlag -> Bool
== :: InfoFlag -> InfoFlag -> Bool
$c== :: InfoFlag -> InfoFlag -> Bool
Eq, Int -> InfoFlag -> ShowS
[InfoFlag] -> ShowS
InfoFlag -> String
(Int -> InfoFlag -> ShowS)
-> (InfoFlag -> String) -> ([InfoFlag] -> ShowS) -> Show InfoFlag
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [InfoFlag] -> ShowS
$cshowList :: [InfoFlag] -> ShowS
show :: InfoFlag -> String
$cshow :: InfoFlag -> String
showsPrec :: Int -> InfoFlag -> ShowS
$cshowsPrec :: Int -> InfoFlag -> ShowS
Show)

-- ** Responses (Sec 3.9.1)

data ResErrorBehavior = ImmediateExit | ContinuedExecution
  deriving (ResErrorBehavior -> ResErrorBehavior -> Bool
(ResErrorBehavior -> ResErrorBehavior -> Bool)
-> (ResErrorBehavior -> ResErrorBehavior -> Bool)
-> Eq ResErrorBehavior
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ResErrorBehavior -> ResErrorBehavior -> Bool
$c/= :: ResErrorBehavior -> ResErrorBehavior -> Bool
== :: ResErrorBehavior -> ResErrorBehavior -> Bool
$c== :: ResErrorBehavior -> ResErrorBehavior -> Bool
Eq, Int -> ResErrorBehavior -> ShowS
[ResErrorBehavior] -> ShowS
ResErrorBehavior -> String
(Int -> ResErrorBehavior -> ShowS)
-> (ResErrorBehavior -> String)
-> ([ResErrorBehavior] -> ShowS)
-> Show ResErrorBehavior
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ResErrorBehavior] -> ShowS
$cshowList :: [ResErrorBehavior] -> ShowS
show :: ResErrorBehavior -> String
$cshow :: ResErrorBehavior -> String
showsPrec :: Int -> ResErrorBehavior -> ShowS
$cshowsPrec :: Int -> ResErrorBehavior -> ShowS
Show)

data ResReasonUnknown = Memout | Incomplete | ResReasonSExpr SExpr
  deriving (ResReasonUnknown -> ResReasonUnknown -> Bool
(ResReasonUnknown -> ResReasonUnknown -> Bool)
-> (ResReasonUnknown -> ResReasonUnknown -> Bool)
-> Eq ResReasonUnknown
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ResReasonUnknown -> ResReasonUnknown -> Bool
$c/= :: ResReasonUnknown -> ResReasonUnknown -> Bool
== :: ResReasonUnknown -> ResReasonUnknown -> Bool
$c== :: ResReasonUnknown -> ResReasonUnknown -> Bool
Eq, Int -> ResReasonUnknown -> ShowS
[ResReasonUnknown] -> ShowS
ResReasonUnknown -> String
(Int -> ResReasonUnknown -> ShowS)
-> (ResReasonUnknown -> String)
-> ([ResReasonUnknown] -> ShowS)
-> Show ResReasonUnknown
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ResReasonUnknown] -> ShowS
$cshowList :: [ResReasonUnknown] -> ShowS
show :: ResReasonUnknown -> String
$cshow :: ResReasonUnknown -> String
showsPrec :: Int -> ResReasonUnknown -> ShowS
$cshowsPrec :: Int -> ResReasonUnknown -> ShowS
Show)

data ResModel
  = RMDefineFun FunctionDef
  | RMDefineFunRec FunctionDef
  | -- | same number
    RMDefineFunsRec (NonEmpty FunctionDec) (NonEmpty Term)

data ResInfo
  = IRErrorBehaviour ResErrorBehavior
  | IRName StringLiteral
  | IRAuthours StringLiteral
  | IRVersion StringLiteral
  | IRReasonUnknown ResReasonUnknown
  | IRAttr Attribute
  deriving (ResInfo -> ResInfo -> Bool
(ResInfo -> ResInfo -> Bool)
-> (ResInfo -> ResInfo -> Bool) -> Eq ResInfo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ResInfo -> ResInfo -> Bool
$c/= :: ResInfo -> ResInfo -> Bool
== :: ResInfo -> ResInfo -> Bool
$c== :: ResInfo -> ResInfo -> Bool
Eq, Int -> ResInfo -> ShowS
[ResInfo] -> ShowS
ResInfo -> String
(Int -> ResInfo -> ShowS)
-> (ResInfo -> String) -> ([ResInfo] -> ShowS) -> Show ResInfo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ResInfo] -> ShowS
$cshowList :: [ResInfo] -> ShowS
show :: ResInfo -> String
$cshow :: ResInfo -> String
showsPrec :: Int -> ResInfo -> ShowS
$cshowsPrec :: Int -> ResInfo -> ShowS
Show)

type ValuationPair = (Term, Term)

type TValuationPair = (Symbol, BValue)

data ResCheckSat = Sat | Unsat | Unknown
  deriving (ResCheckSat -> ResCheckSat -> Bool
(ResCheckSat -> ResCheckSat -> Bool)
-> (ResCheckSat -> ResCheckSat -> Bool) -> Eq ResCheckSat
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ResCheckSat -> ResCheckSat -> Bool
$c/= :: ResCheckSat -> ResCheckSat -> Bool
== :: ResCheckSat -> ResCheckSat -> Bool
$c== :: ResCheckSat -> ResCheckSat -> Bool
Eq, Int -> ResCheckSat -> ShowS
[ResCheckSat] -> ShowS
ResCheckSat -> String
(Int -> ResCheckSat -> ShowS)
-> (ResCheckSat -> String)
-> ([ResCheckSat] -> ShowS)
-> Show ResCheckSat
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ResCheckSat] -> ShowS
$cshowList :: [ResCheckSat] -> ShowS
show :: ResCheckSat -> String
$cshow :: ResCheckSat -> String
showsPrec :: Int -> ResCheckSat -> ShowS
$cshowsPrec :: Int -> ResCheckSat -> ShowS
Show)

-- *** instances

type CheckSatRes = GeneralRes ResCheckSat

type EchoRes = GeneralRes StringLiteral

type GetAssertionsRes = GeneralRes [Term]

type GetAssignmentRes = GeneralRes [TValuationPair]

type GetInfoRes = GeneralRes (NonEmpty ResInfo)

type GetModelRes = GeneralRes ResModel

type GetOptionRes = GeneralRes AttributeValue

type GetProofRes = GeneralRes SExpr

type GetUnsatAssumpRes = GeneralRes [Symbol]

type GetUnsatCoreRes = GeneralRes [Symbol]

type GetValueRes = GeneralRes (NonEmpty ValuationPair)

data GeneralRes res
  = ResSuccess
  | ResSpecific res
  | ResUnsupported
  | ResError StringLiteral
  deriving (GeneralRes res -> GeneralRes res -> Bool
(GeneralRes res -> GeneralRes res -> Bool)
-> (GeneralRes res -> GeneralRes res -> Bool)
-> Eq (GeneralRes res)
forall res. Eq res => GeneralRes res -> GeneralRes res -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: GeneralRes res -> GeneralRes res -> Bool
$c/= :: forall res. Eq res => GeneralRes res -> GeneralRes res -> Bool
== :: GeneralRes res -> GeneralRes res -> Bool
$c== :: forall res. Eq res => GeneralRes res -> GeneralRes res -> Bool
Eq, Int -> GeneralRes res -> ShowS
[GeneralRes res] -> ShowS
GeneralRes res -> String
(Int -> GeneralRes res -> ShowS)
-> (GeneralRes res -> String)
-> ([GeneralRes res] -> ShowS)
-> Show (GeneralRes res)
forall res. Show res => Int -> GeneralRes res -> ShowS
forall res. Show res => [GeneralRes res] -> ShowS
forall res. Show res => GeneralRes res -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [GeneralRes res] -> ShowS
$cshowList :: forall res. Show res => [GeneralRes res] -> ShowS
show :: GeneralRes res -> String
$cshow :: forall res. Show res => GeneralRes res -> String
showsPrec :: Int -> GeneralRes res -> ShowS
$cshowsPrec :: forall res. Show res => Int -> GeneralRes res -> ShowS
Show)

class SpecificSuccessRes s where
  specificSuccessRes :: GenParser st s