-- |
-- - 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
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
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
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
SList -> ShowS
SExpr -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: SList -> ShowS
$cshowList :: SList -> 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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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