Syntax.hs

{-|
 - Module      : Language.SMT2.Syntax
 - Description : SMT language parser
 - Maintainer  : yokis1997@pku.edu.cn
 - 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 (Eq, Show)

data SExpr = SEConstant SpecConstant
           | SEReservedWord ReservedWord
           | SESymbol Symbol
           | SEKeyword Keyword
           | SEList SList
  deriving (Eq, Show)

type SList = [SExpr]


-- * Identifiers (Sec 3.3)

data Index = IxNumeral Numeral
           | IxSymbol Symbol
  deriving (Eq, Show)

data Identifier = IdSymbol Symbol
                | IdIndexed Symbol (NonEmpty Index)
  deriving (Eq, Show)


-- * Attributes (Sec. 3.4)

data AttributeValue = AttrValSpecConstant SpecConstant
                    | AttrValSymbol Symbol
                    | AttrValSList SList
  deriving (Eq, Show)

data Attribute = AttrKey Keyword
               | AttrKeyValue Keyword AttributeValue
  deriving (Eq, Show)


-- * Sorts (Sec 3.5)

data Sort = SortSymbol Identifier
          | SortParameter Identifier (NonEmpty Sort)
  deriving (Eq, Show)


-- * Terms and Formulas (Sec 3.6)

data QualIdentifier = Unqualified Identifier
                    | Qualified Identifier Sort
  deriving (Eq, Show)

data VarBinding = VarBinding Symbol Term
  deriving (Eq, Show)

data SortedVar = SortedVar Symbol Sort
  deriving (Eq, Show)

data MatchPattern = MPVariable Symbol
                  | MPConstructor Symbol (NonEmpty Symbol)
  deriving (Eq, Show)

data MatchCase = MatchCase MatchPattern Term
  deriving (Eq, 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 (Eq, Show)


-- * Theory declarations (Sec 3.7)

data SortSymbolDecl = SortSymbolDecl Identifier Numeral [Attribute]
  deriving (Eq, Show)

data MetaSpecConstant = MSC_NUMERAL | MSC_DECIMAL | MSC_STRING
  deriving (Eq, Show)

data FunSymbolDecl = FunConstant SpecConstant Sort [Attribute]
                   | FunMeta MetaSpecConstant Sort [Attribute]
                   | FunIdentifier Identifier (NonEmpty Sort) [Attribute] -- ^ potentially overloaded
  deriving (Eq, Show)

data ParFunSymbolDecl = NonPar FunSymbolDecl -- ^ non-parametric
                      | Par (NonEmpty Symbol) Identifier (NonEmpty Sort) [Attribute] -- ^ parametric
  deriving (Eq, Show)

data TheoryAttribute = TASorts (NonEmpty SortSymbolDecl)
                     | TAFuns (NonEmpty ParFunSymbolDecl)
                     | TASortsDescription StringLiteral
                     | TAFunsDescription StringLiteral
                     | TADefinition StringLiteral
                     | TAValues StringLiteral
                     | TANotes StringLiteral
                     | TAAttr Attribute
  deriving (Eq, Show)

data TheoryDecl = TheoryDecl Symbol (NonEmpty TheoryAttribute)
  deriving (Eq, Show)


-- * Logic Declarations (Sec 3.8)

data LogicAttribute = LATheories (NonEmpty Symbol)
                    | LALanguage StringLiteral
                    | LAExtensions StringLiteral
                    | LAValues StringLiteral
                    | LANotes StringLiteral
                    | LAAttr Attribute
  deriving (Eq, Show)

data Logic = Logic Symbol (NonEmpty LogicAttribute)
  deriving (Eq, Show)


-- * Scripts (Sec 3.9)

data SortDec = SortDec Symbol Numeral
  deriving (Eq, Show)

data SelectorDec = SelectorDec Symbol Sort
  deriving (Eq, Show)

data ConstructorDec = ConstructorDec Symbol [SelectorDec]
  deriving (Eq, Show)

data DatatypeDec = DDNonparametric (NonEmpty ConstructorDec)
                  | DDParametric (NonEmpty Symbol) (NonEmpty ConstructorDec)
  deriving (Eq, Show)

data FunctionDec = FunctionDec Symbol [SortedVar] Sort
  deriving (Eq, Show)

data FunctionDef = FunctionDef Symbol [SortedVar] Sort Term
  deriving (Eq, Show)

data PropLiteral = PLPositive Symbol
                 | PLNegative Symbol
  deriving (Eq, Show)

data Command = Assert Term
             | CheckSat
             | CheckSatAssuming [PropLiteral]
             | DeclareConst Symbol Sort
             | DeclareDatatype Symbol DatatypeDec
             | DeclareDatatypes (NonEmpty SortDec) (NonEmpty DatatypeDec) -- ^ same number
             | DeclareFun Symbol [Sort] Sort
             | DeclareSort Symbol Numeral
             | DefineFun FunctionDef
             | DefineFunRec FunctionDef
             | DefineFunsRec (NonEmpty FunctionDec) (NonEmpty Term) -- ^ same number
             | 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 (Eq, Show)

type Script = [Command]

data BValue = BTrue | BFalse
  deriving (Eq, 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 (Eq, Show)

data InfoFlag = AllStatistics | AssertionStackLevels | Authors
              | ErrorBehavior | Name | ReasonUnknown
              | Version | IFKeyword Keyword
  deriving (Eq, Show)

-- ** Responses (Sec 3.9.1)

data ResErrorBehavior = ImmediateExit | ContinuedExecution
  deriving (Eq, Show)

data ResReasonUnknown = Memout | Incomplete | ResReasonSExpr SExpr
  deriving (Eq, Show)

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

data ResInfo = IRErrorBehaviour ResErrorBehavior
             | IRName StringLiteral
             | IRAuthours StringLiteral
             | IRVersion StringLiteral
             | IRReasonUnknown ResReasonUnknown
             | IRAttr Attribute
  deriving (Eq, Show)

type ValuationPair = (Term, Term)

type TValuationPair = (Symbol, BValue)

data ResCheckSat = Sat | Unsat | Unknown
  deriving (Eq, 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 (Eq, Show)

class SpecificSuccessRes s where
  specificSuccessRes :: GenParser st s