{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverloadedStrings #-}

-- |
-- - Module      : Language.SMT2.Parser
-- - Description : SMT language parser
-- - Maintainer  : ubikium@gmail.com
-- - Stability   : experimental
module Language.SMT2.Parser
  ( -- * Utils
    -- $utils
    parseString,
    parseStringEof,
    parseFileMsg,
    parseCommentFreeFileMsg,
    stripSpaces,
    removeComment,

    -- * Lexicons (Sec. 3.1)
    -- $lexicon
    numeral,
    decimal,
    hexadecimal,
    binary,
    stringLiteral,
    reservedWord,
    symbol,
    keyword,

    -- * S-expressions (Sec. 3.2)
    slist,
    specConstant,
    sexpr,

    -- * Identifiers (Sec 3.3)
    index,
    identifier,

    -- * Attributes (Sec. 3.4)
    attributeValue,
    attribute,

    -- * Sorts (Sec 3.5)
    sort,

    -- * Terms and Formulas (Sec 3.6)
    qualIdentifier,
    varBinding,
    sortedVar,
    matchPattern,
    matchCase,
    term,

    -- * Theory declarations (Sec 3.7)
    sortSymbolDecl,
    metaSpecConstant,
    funSymbolDecl,
    parFunSymbolDecl,
    theoryAttribute,
    theoryDecl,

    -- * Logic Declarations (Sec 3.8)
    logicAttribute,
    logic,

    -- * Scripts (Sec 3.9)
    sortDec,
    selectorDec,
    constructorDec,
    datatypeDec,
    functionDec,
    functionDef,
    propLiteral,
    command,
    script,
    bValue,
    scriptOption,
    infoFlag,

    -- ** Responses (Sec 3.9.1)

    -- *** values
    resErrorBehaviour,
    resReasonUnknown,
    resModel,
    resInfo,
    valuationPair,
    tValuationPair,
    resCheckSat,

    -- *** instances
    checkSatRes,
    echoRes,
    getAssertionsRes,
    getAssignmentRes,
    getInfoRes,
    getModelRes,
    getOptionRes,
    getProofRes,
    getUnsatAssumpRes,
    getUnsatCoreRes,
    getValueRes,
  )
where

import Data.Bifunctor (first)
import Data.Char (toLower)
import Data.Functor (($>))
import Data.List.NonEmpty (NonEmpty, fromList)
import qualified Data.Text as T
import Language.SMT2.Syntax
import Text.Parsec (ParseError, parse, try)
import Text.Parsec.Char
import Text.Parsec.Combinator
import Text.Parsec.Prim (many, unexpected, (<?>), (<|>))
import Text.Parsec.Text (GenParser, Parser)

parseString :: Parser a -> T.Text -> Either ParseError a
parseString :: Parser a -> Text -> Either ParseError a
parseString p :: Parser a
p = Parser a -> SourceName -> Text -> Either ParseError a
forall s t a.
Stream s Identity t =>
Parsec s () a -> SourceName -> s -> Either ParseError a
parse Parser a
p ""

parseStringEof :: Parser a -> T.Text -> Either ParseError a
parseStringEof :: Parser a -> Text -> Either ParseError a
parseStringEof p :: Parser a
p = Parser a -> SourceName -> Text -> Either ParseError a
forall s t a.
Stream s Identity t =>
Parsec s () a -> SourceName -> s -> Either ParseError a
parse (Parser a
p Parser a -> ParsecT Text () Identity () -> Parser a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text () Identity ()
forall s (m :: * -> *) t u.
(Stream s m t, Show t) =>
ParsecT s u m ()
eof) ""

-- | parse from a file string, may have leading & trailing spaces and comments
parseFileMsg :: Parser a -> T.Text -> Either T.Text a
parseFileMsg :: Parser a -> Text -> Either Text a
parseFileMsg p :: Parser a
p = Parser a -> Text -> Either Text a
forall a. Parser a -> Text -> Either Text a
parseCommentFreeFileMsg Parser a
p (Text -> Either Text a) -> (Text -> Text) -> Text -> Either Text a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Text
removeComment

-- | parse from a comment-free file string
parseCommentFreeFileMsg :: Parser a -> T.Text -> Either T.Text a
parseCommentFreeFileMsg :: Parser a -> Text -> Either Text a
parseCommentFreeFileMsg p :: Parser a
p = (ParseError -> Text) -> Either ParseError a -> Either Text a
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (SourceName -> Text
T.pack (SourceName -> Text)
-> (ParseError -> SourceName) -> ParseError -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ParseError -> SourceName
forall a. Show a => a -> SourceName
show) (Either ParseError a -> Either Text a)
-> (Text -> Either ParseError a) -> Text -> Either Text a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Parser a -> Text -> Either ParseError a
forall a. Parser a -> Text -> Either ParseError a
parseStringEof (Parser a -> Parser a
forall st a. GenParser st a -> GenParser st a
stripSpaces Parser a
p)

-- * Utils

-- $utils
-- commonly used combinators

-- | overlay @String@ to @Data.Text@
text :: String -> GenParser st T.Text
text :: SourceName -> GenParser st Text
text = (SourceName -> Text
T.pack (SourceName -> Text)
-> ParsecT Text st Identity SourceName -> GenParser st Text
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) (ParsecT Text st Identity SourceName -> GenParser st Text)
-> (SourceName -> ParsecT Text st Identity SourceName)
-> SourceName
-> GenParser st Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourceName -> ParsecT Text st Identity SourceName
forall s (m :: * -> *) u.
Stream s m Char =>
SourceName -> ParsecT s u m SourceName
string

-- | skip one or more @spaces@
spaces1 :: GenParser st ()
spaces1 :: GenParser st ()
spaces1 = ParsecT Text st Identity Char -> GenParser st ()
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m ()
skipMany1 ParsecT Text st Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
space

-- | between round brackets
betweenBrackets :: GenParser st a -> GenParser st a
betweenBrackets :: GenParser st a -> GenParser st a
betweenBrackets = GenParser st a -> GenParser st a
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try (GenParser st a -> GenParser st a)
-> (GenParser st a -> GenParser st a)
-> GenParser st a
-> GenParser st a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ParsecT Text st Identity Char
-> ParsecT Text st Identity Char
-> GenParser st a
-> GenParser st a
forall s (m :: * -> *) t u open close a.
Stream s m t =>
ParsecT s u m open
-> ParsecT s u m close -> ParsecT s u m a -> ParsecT s u m a
between (Char -> ParsecT Text st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '(' ParsecT Text st Identity Char
-> ParsecT Text st Identity () -> ParsecT Text st Identity Char
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces) (ParsecT Text st Identity ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces ParsecT Text st Identity ()
-> ParsecT Text st Identity Char -> ParsecT Text st Identity Char
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Char -> ParsecT Text st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char ')')

-- | @many p@, separated by @spaces1@, possibly has a trailing @spaces1@
sepSpace :: GenParser st a -> GenParser st [a]
sepSpace :: GenParser st a -> GenParser st [a]
sepSpace p :: GenParser st a
p = GenParser st a -> ParsecT Text st Identity () -> GenParser st [a]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepEndBy GenParser st a
p ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1

-- | @many1 p@, separated by @spaces1@, possibly has a trailing @spaces1@
sepSpace1 :: GenParser st a -> GenParser st (NonEmpty a)
sepSpace1 :: GenParser st a -> GenParser st (NonEmpty a)
sepSpace1 p :: GenParser st a
p = [a] -> NonEmpty a
forall a. [a] -> NonEmpty a
fromList ([a] -> NonEmpty a)
-> ParsecT Text st Identity [a] -> GenParser st (NonEmpty a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenParser st a
-> ParsecT Text st Identity () -> ParsecT Text st Identity [a]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepEndBy1 GenParser st a
p ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1

-- | @many p@, separated by @spaces@, possibly has a trailing @spaces@
sepOptSpace :: GenParser st a -> GenParser st [a]
sepOptSpace :: GenParser st a -> GenParser st [a]
sepOptSpace p :: GenParser st a
p = GenParser st a -> ParsecT Text st Identity () -> GenParser st [a]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepEndBy GenParser st a
p ParsecT Text st Identity ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces

-- | @many1 p@, separated by @spaces@, possibly has a trailing @spaces@
sepOptSpace1 :: GenParser st a -> GenParser st (NonEmpty a)
sepOptSpace1 :: GenParser st a -> GenParser st (NonEmpty a)
sepOptSpace1 p :: GenParser st a
p = [a] -> NonEmpty a
forall a. [a] -> NonEmpty a
fromList ([a] -> NonEmpty a)
-> ParsecT Text st Identity [a] -> GenParser st (NonEmpty a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenParser st a
-> ParsecT Text st Identity () -> ParsecT Text st Identity [a]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepEndBy1 GenParser st a
p ParsecT Text st Identity ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces

-- | match an string, ignore @spaces@ after,
-- input is not consumed if failed
tryStr :: String -> GenParser st ()
tryStr :: SourceName -> GenParser st ()
tryStr s :: SourceName
s = GenParser st () -> GenParser st ()
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try (GenParser st () -> GenParser st ())
-> GenParser st () -> GenParser st ()
forall a b. (a -> b) -> a -> b
$ SourceName -> ParsecT Text st Identity SourceName
forall s (m :: * -> *) u.
Stream s m Char =>
SourceName -> ParsecT s u m SourceName
string SourceName
s ParsecT Text st Identity SourceName
-> GenParser st () -> GenParser st ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> GenParser st ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces GenParser st () -> () -> GenParser st ()
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> ()

-- | match an string, must have @spaces1@ after, ignore them,
-- input is not consumed if failed
tryStr1 :: String -> GenParser st ()
tryStr1 :: SourceName -> GenParser st ()
tryStr1 s :: SourceName
s = GenParser st () -> GenParser st ()
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try (GenParser st () -> GenParser st ())
-> GenParser st () -> GenParser st ()
forall a b. (a -> b) -> a -> b
$ SourceName -> ParsecT Text st Identity SourceName
forall s (m :: * -> *) u.
Stream s m Char =>
SourceName -> ParsecT s u m SourceName
string SourceName
s ParsecT Text st Identity SourceName
-> GenParser st () -> GenParser st ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> GenParser st ()
forall st. GenParser st ()
spaces1 GenParser st () -> () -> GenParser st ()
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> ()

tryStrBraket :: String -> GenParser st ()
tryStrBraket :: SourceName -> GenParser st ()
tryStrBraket s :: SourceName
s = GenParser st () -> GenParser st ()
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try (GenParser st () -> GenParser st ())
-> GenParser st () -> GenParser st ()
forall a b. (a -> b) -> a -> b
$ SourceName -> ParsecT Text st Identity SourceName
forall s (m :: * -> *) u.
Stream s m Char =>
SourceName -> ParsecT s u m SourceName
string SourceName
s ParsecT Text st Identity SourceName
-> GenParser st () -> GenParser st ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (GenParser st ()
forall st. GenParser st ()
spaces1 GenParser st () -> GenParser st () -> GenParser st ()
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> GenParser st ()
forall st. GenParser st ()
lookLeftBraket) GenParser st () -> () -> GenParser st ()
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> ()
  where
    lookLeftBraket :: ParsecT Text u Identity ()
lookLeftBraket = ParsecT Text u Identity () -> ParsecT Text u Identity ()
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try (ParsecT Text u Identity () -> ParsecT Text u Identity ())
-> ParsecT Text u Identity () -> ParsecT Text u Identity ()
forall a b. (a -> b) -> a -> b
$ ParsecT Text u Identity Char -> ParsecT Text u Identity Char
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m a
lookAhead (Char -> ParsecT Text u Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '(') ParsecT Text u Identity Char -> () -> ParsecT Text u Identity ()
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> ()

-- | like @tryStr@, but prefix with a @':'@
tryAttr :: String -> GenParser st ()
tryAttr :: SourceName -> GenParser st ()
tryAttr s :: SourceName
s = SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryStr (':' Char -> SourceName -> SourceName
forall a. a -> [a] -> [a]
: SourceName
s)

-- | like @tryStr1@, but prefix with a @':'@
tryAttr1 :: String -> GenParser st ()
tryAttr1 :: SourceName -> GenParser st ()
tryAttr1 s :: SourceName
s = SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryStr1 (':' Char -> SourceName -> SourceName
forall a. a -> [a] -> [a]
: SourceName
s)

-- | strip away the leading and trailing @spaces@
stripSpaces :: GenParser st a -> GenParser st a
stripSpaces :: GenParser st a -> GenParser st a
stripSpaces p :: GenParser st a
p = ParsecT Text st Identity ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces ParsecT Text st Identity () -> GenParser st a -> GenParser st a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> GenParser st a
p GenParser st a -> ParsecT Text st Identity () -> GenParser st a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces

-- | remove comments
removeComment :: T.Text -> T.Text
removeComment :: Text -> Text
removeComment = Text -> Text -> Text
rc Text
T.empty
  where
    rc :: T.Text -> T.Text -> T.Text
    rc :: Text -> Text -> Text
rc acc :: Text
acc rest :: Text
rest =
      if Text -> Bool
T.null Text
rest
        then Text
acc
        else
          let (c :: Char
c, cs :: Text
cs) = (Text -> Char
T.head Text
rest, Text -> Text
T.tail Text
rest)
              f :: Text -> Text -> Text
f = case Char
c of
                '"' -> SourceName -> (Text -> Text) -> Text -> Text -> Text
capture "\"" (Char -> Text -> Text
T.cons '"')
                '|' -> SourceName -> (Text -> Text) -> Text -> Text -> Text
capture "|" (Char -> Text -> Text
T.cons '|')
                ';' -> SourceName -> (Text -> Text) -> Text -> Text -> Text
capture "\n\r" (Text -> Text -> Text
forall a b. a -> b -> a
const (Text -> Text -> Text) -> Text -> Text -> Text
forall a b. (a -> b) -> a -> b
$ Char -> Text
T.singleton ' ')
                x :: Char
x -> Char -> Text -> Text -> Text
nextPos Char
x
           in Text -> Text -> Text
f Text
acc Text
cs
    capture :: String -> (T.Text -> T.Text) -> T.Text -> T.Text -> T.Text
    capture :: SourceName -> (Text -> Text) -> Text -> Text -> Text
capture stops :: SourceName
stops after :: Text -> Text
after acc :: Text
acc cs :: Text
cs =
      let (captured :: Text
captured, rest :: Text
rest) = (Char -> Bool) -> Text -> (Text, Text)
T.break (Char -> SourceName -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` SourceName
stops) Text
cs
       in if Text -> Bool
T.null Text
rest
            then Text
acc Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text -> Text
after Text
captured
            else
              let (s :: Char
s, ss :: Text
ss) = (Text -> Char
T.head Text
rest, Text -> Text
T.tail Text
rest)
               in Text -> Text -> Text
rc (Text
acc Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text -> Text
after Text
captured Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Char -> Text
T.singleton Char
s) Text
ss
    -- 1. if the string is ill-formed, ignore;
    --    let the parser catch, for a better format
    -- 2. the double " escaping in a string literal is the same as capturing twice
    -- 3. for comments ended with \n\r or \r\n, the second is left
    nextPos :: Char -> Text -> Text -> Text
nextPos x :: Char
x acc :: Text
acc = Text -> Text -> Text
rc (Text
acc Text -> Char -> Text
`T.snoc` Char
x)

-- * Lexicons (Sec. 3.1)

-- $lexicon
-- Parsers for lexicons.
--
-- For a numeral, a decimal, or a string literal, the parsed result is the same.
-- For a hexadecimal or a binary, the result is stripped with marks (@#x@ and @#b@).

numeral :: GenParser st Numeral
numeral :: GenParser st Text
numeral =
  SourceName -> GenParser st Text
forall st. SourceName -> GenParser st Text
text "0"
    GenParser st Text -> GenParser st Text -> GenParser st Text
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
      Char
c <- SourceName -> ParsecT Text st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
SourceName -> ParsecT s u m Char
oneOf "123456789"
      SourceName
cs <- ParsecT Text st Identity Char
-> ParsecT Text st Identity SourceName
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many ParsecT Text st Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
digit
      Text -> GenParser st Text
forall (m :: * -> *) a. Monad m => a -> m a
return (Text -> GenParser st Text) -> Text -> GenParser st Text
forall a b. (a -> b) -> a -> b
$ SourceName -> Text
T.pack (Char
c Char -> SourceName -> SourceName
forall a. a -> [a] -> [a]
: SourceName
cs)

decimal :: GenParser st Decimal
decimal :: GenParser st Text
decimal = do
  Text
whole <- GenParser st Text
forall st. GenParser st Text
numeral
  Char -> ParsecT Text st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '.'
  SourceName
zeros <- ParsecT Text st Identity Char
-> ParsecT Text st Identity SourceName
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many (Char -> ParsecT Text st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '0')
  Text
restFractional <- Text -> GenParser st Text -> GenParser st Text
forall s (m :: * -> *) t a u.
Stream s m t =>
a -> ParsecT s u m a -> ParsecT s u m a
option "" GenParser st Text
forall st. GenParser st Text
numeral
  Text -> GenParser st Text
forall (m :: * -> *) a. Monad m => a -> m a
return (Text -> GenParser st Text) -> Text -> GenParser st Text
forall a b. (a -> b) -> a -> b
$ Text
whole Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Char -> Text
T.singleton '.' Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> SourceName -> Text
T.pack SourceName
zeros Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
restFractional

hexadecimal :: GenParser st Hexadecimal
hexadecimal :: GenParser st Text
hexadecimal = SourceName -> GenParser st Text
forall st. SourceName -> GenParser st Text
text "#x" GenParser st Text -> GenParser st Text -> GenParser st Text
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SourceName -> Text
T.pack (SourceName -> Text)
-> (SourceName -> SourceName) -> SourceName -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Char) -> SourceName -> SourceName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Char -> Char
toLower (SourceName -> Text)
-> ParsecT Text st Identity SourceName -> GenParser st Text
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Char
-> ParsecT Text st Identity SourceName
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 ParsecT Text st Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
hexDigit

binary :: GenParser st Binary
binary :: GenParser st Text
binary = SourceName -> GenParser st Text
forall st. SourceName -> GenParser st Text
text "#b" GenParser st Text -> GenParser st Text -> GenParser st Text
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SourceName -> Text
T.pack (SourceName -> Text)
-> ParsecT Text st Identity SourceName -> GenParser st Text
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Char
-> ParsecT Text st Identity SourceName
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 (Char -> ParsecT Text st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '0' ParsecT Text st Identity Char
-> ParsecT Text st Identity Char -> ParsecT Text st Identity Char
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Char -> ParsecT Text st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '1')

stringLiteral :: GenParser st StringLiteral
stringLiteral :: GenParser st Text
stringLiteral = do
  Char -> ParsecT Text st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '"'
  SourceName
str <- ParsecT Text st Identity Char
-> ParsecT Text st Identity SourceName
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many (ParsecT Text st Identity Char
forall u. ParsecT Text u Identity Char
nonEscaped ParsecT Text st Identity Char
-> ParsecT Text st Identity Char -> ParsecT Text st Identity Char
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT Text st Identity Char
forall u. ParsecT Text u Identity Char
escaped)
  Char -> ParsecT Text st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '"'
  Text -> GenParser st Text
forall (m :: * -> *) a. Monad m => a -> m a
return (Text -> GenParser st Text) -> Text -> GenParser st Text
forall a b. (a -> b) -> a -> b
$ SourceName -> Text
T.pack SourceName
str
  where
    nonEscaped :: ParsecT Text u Identity Char
nonEscaped = SourceName -> ParsecT Text u Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
SourceName -> ParsecT s u m Char
noneOf "\""
    escaped :: ParsecT Text u Identity Char
escaped = ParsecT Text u Identity SourceName
-> ParsecT Text u Identity SourceName
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try (SourceName -> ParsecT Text u Identity SourceName
forall s (m :: * -> *) u.
Stream s m Char =>
SourceName -> ParsecT s u m SourceName
string "\"\"") ParsecT Text u Identity SourceName
-> Char -> ParsecT Text u Identity Char
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> '"'

reservedWords :: [String]
reservedWords :: [SourceName]
reservedWords =
  [ -- General
    "!",
    "_",
    "as",
    "DECIMAL",
    "exists",
    "forall",
    "let",
    "NUMERAL",
    "par",
    "STRING",
    -- Command names
    "assert",
    "check-sat",
    "declare-sort",
    "declare-fun",
    "define-sort",
    "define-fun",
    "exit",
    "get-assertions",
    "get-assignment",
    "get-info",
    "get-option",
    "get-proof",
    "get-unsat-core",
    "get-value",
    "pop",
    "push",
    "set-logic",
    "set-info",
    "set-option"
  ]

-- | accept all reserved words,
-- the exact content should be checked later in the parsing procedure
reservedWord :: GenParser st ReservedWord
reservedWord :: GenParser st Text
reservedWord = [GenParser st Text] -> GenParser st Text
forall s (m :: * -> *) t u a.
Stream s m t =>
[ParsecT s u m a] -> ParsecT s u m a
choice (SourceName -> GenParser st Text
forall st. SourceName -> GenParser st Text
parseWord (SourceName -> GenParser st Text)
-> [SourceName] -> [GenParser st Text]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SourceName]
reservedWords)
  where
    parseWord :: String -> GenParser st ReservedWord
    parseWord :: SourceName -> GenParser st Text
parseWord w :: SourceName
w = GenParser st Text -> GenParser st Text
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try (SourceName -> GenParser st Text
forall st. SourceName -> GenParser st Text
text SourceName
w) GenParser st Text
-> ParsecT Text st Identity () -> GenParser st Text
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity Char -> ParsecT Text st Identity ()
forall s (m :: * -> *) t a u.
(Stream s m t, Show a) =>
ParsecT s u m a -> ParsecT s u m ()
notFollowedBy ParsecT Text st Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
anyChar

-- | characters allowed in a name
nameChar :: GenParser st Char
nameChar :: GenParser st Char
nameChar = SourceName -> GenParser st Char
forall s (m :: * -> *) u.
Stream s m Char =>
SourceName -> ParsecT s u m Char
oneOf "~!@$%^&*_-+=<>.?/"

-- |  enclosing a simple symbol in vertical bars does not produce a
-- new symbol, e.g. @abc@ and @|abc|@ are the /same/ symbol
-- this is guaranteed by removing the bars
symbol :: GenParser st Symbol
symbol :: GenParser st Text
symbol = GenParser st Text -> ParsecT Text st Identity ()
forall s (m :: * -> *) t a u.
(Stream s m t, Show a) =>
ParsecT s u m a -> ParsecT s u m ()
notFollowedBy (GenParser st Text -> GenParser st Text
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try GenParser st Text
forall st. GenParser st Text
reservedWord) ParsecT Text st Identity ()
-> GenParser st Text -> GenParser st Text
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (GenParser st Text
forall st. GenParser st Text
quotedSymbol GenParser st Text -> GenParser st Text -> GenParser st Text
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> GenParser st Text
forall st. GenParser st Text
simpleSymbol GenParser st Text -> SourceName -> GenParser st Text
forall s u (m :: * -> *) a.
ParsecT s u m a -> SourceName -> ParsecT s u m a
<?> "symbol")
  where
    simpleSymbol :: ParsecT Text u Identity Text
simpleSymbol = do
      Char
c <- GenParser u Char
forall u. ParsecT Text u Identity Char
nameChar GenParser u Char -> GenParser u Char -> GenParser u Char
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> GenParser u Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
letter
      SourceName
cs <- GenParser u Char -> ParsecT Text u Identity SourceName
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many (GenParser u Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
alphaNum GenParser u Char -> GenParser u Char -> GenParser u Char
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> GenParser u Char
forall u. ParsecT Text u Identity Char
nameChar)
      Text -> ParsecT Text u Identity Text
forall (m :: * -> *) a. Monad m => a -> m a
return (Text -> ParsecT Text u Identity Text)
-> Text -> ParsecT Text u Identity Text
forall a b. (a -> b) -> a -> b
$ SourceName -> Text
T.pack (Char
c Char -> SourceName -> SourceName
forall a. a -> [a] -> [a]
: SourceName
cs)
    quotedSymbol :: ParsecT Text u Identity Text
quotedSymbol = ParsecT Text u Identity Char
-> ParsecT Text u Identity Char
-> ParsecT Text u Identity Text
-> ParsecT Text u Identity Text
forall s (m :: * -> *) t u open close a.
Stream s m t =>
ParsecT s u m open
-> ParsecT s u m close -> ParsecT s u m a -> ParsecT s u m a
between (Char -> ParsecT Text u Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '|') (Char -> ParsecT Text u Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '|') (ParsecT Text u Identity Text -> ParsecT Text u Identity Text)
-> ParsecT Text u Identity Text -> ParsecT Text u Identity Text
forall a b. (a -> b) -> a -> b
$ SourceName -> Text
T.pack (SourceName -> Text)
-> ParsecT Text u Identity SourceName
-> ParsecT Text u Identity Text
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text u Identity Char -> ParsecT Text u Identity SourceName
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many (SourceName -> ParsecT Text u Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
SourceName -> ParsecT s u m Char
noneOf "\\|")

keyword :: GenParser st Keyword
keyword :: GenParser st Text
keyword = do
  Char -> ParsecT Text st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char ':'
  SourceName -> Text
T.pack (SourceName -> Text)
-> ParsecT Text st Identity SourceName -> GenParser st Text
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Char
-> ParsecT Text st Identity SourceName
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 (ParsecT Text st Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
alphaNum ParsecT Text st Identity Char
-> ParsecT Text st Identity Char -> ParsecT Text st Identity Char
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT Text st Identity Char
forall u. ParsecT Text u Identity Char
nameChar)

-- * S-expressions (Sec. 3.2)

slist :: GenParser st SList
slist :: GenParser st SList
slist = GenParser st SList -> GenParser st SList
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st SList -> GenParser st SList)
-> (GenParser st SExpr -> GenParser st SList)
-> GenParser st SExpr
-> GenParser st SList
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GenParser st SExpr -> GenParser st SList
forall st a. GenParser st a -> GenParser st [a]
sepSpace (GenParser st SExpr -> GenParser st SList)
-> GenParser st SExpr -> GenParser st SList
forall a b. (a -> b) -> a -> b
$ GenParser st SExpr
forall st. GenParser st SExpr
sexpr

-- | a constant must be followed by a space to delimit the end
specConstant :: GenParser st SpecConstant
specConstant :: GenParser st SpecConstant
specConstant =
  Text -> SpecConstant
SCDecimal (Text -> SpecConstant)
-> ParsecT Text st Identity Text -> GenParser st SpecConstant
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text -> ParsecT Text st Identity Text
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try ParsecT Text st Identity Text
forall st. GenParser st Text
decimal -- numeral can be a prefix
    GenParser st SpecConstant
-> GenParser st SpecConstant -> GenParser st SpecConstant
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Text -> SpecConstant
SCNumeral (Text -> SpecConstant)
-> ParsecT Text st Identity Text -> GenParser st SpecConstant
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text -> ParsecT Text st Identity Text
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try ParsecT Text st Identity Text
forall st. GenParser st Text
numeral
    GenParser st SpecConstant
-> GenParser st SpecConstant -> GenParser st SpecConstant
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Text -> SpecConstant
SCHexadecimal (Text -> SpecConstant)
-> ParsecT Text st Identity Text -> GenParser st SpecConstant
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text -> ParsecT Text st Identity Text
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try ParsecT Text st Identity Text
forall st. GenParser st Text
hexadecimal
    GenParser st SpecConstant
-> GenParser st SpecConstant -> GenParser st SpecConstant
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Text -> SpecConstant
SCBinary (Text -> SpecConstant)
-> ParsecT Text st Identity Text -> GenParser st SpecConstant
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text -> ParsecT Text st Identity Text
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try ParsecT Text st Identity Text
forall st. GenParser st Text
binary
    GenParser st SpecConstant
-> GenParser st SpecConstant -> GenParser st SpecConstant
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Text -> SpecConstant
SCString (Text -> SpecConstant)
-> ParsecT Text st Identity Text -> GenParser st SpecConstant
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text -> ParsecT Text st Identity Text
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try ParsecT Text st Identity Text
forall st. GenParser st Text
stringLiteral
    GenParser st SpecConstant
-> SourceName -> GenParser st SpecConstant
forall s u (m :: * -> *) a.
ParsecT s u m a -> SourceName -> ParsecT s u m a
<?> "spec constants"

sexpr :: GenParser st SExpr
sexpr :: GenParser st SExpr
sexpr =
  SList -> SExpr
SEList (SList -> SExpr)
-> ParsecT Text st Identity SList -> GenParser st SExpr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity SList -> ParsecT Text st Identity SList
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try ParsecT Text st Identity SList
forall st. GenParser st SList
slist
    GenParser st SExpr -> GenParser st SExpr -> GenParser st SExpr
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SpecConstant -> SExpr
SEConstant (SpecConstant -> SExpr)
-> ParsecT Text st Identity SpecConstant -> GenParser st SExpr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity SpecConstant
-> ParsecT Text st Identity SpecConstant
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try ParsecT Text st Identity SpecConstant
forall st. GenParser st SpecConstant
specConstant
    GenParser st SExpr -> GenParser st SExpr -> GenParser st SExpr
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Text -> SExpr
SEReservedWord (Text -> SExpr)
-> ParsecT Text st Identity Text -> GenParser st SExpr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text -> ParsecT Text st Identity Text
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try ParsecT Text st Identity Text
forall st. GenParser st Text
reservedWord
    GenParser st SExpr -> GenParser st SExpr -> GenParser st SExpr
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Text -> SExpr
SEKeyword (Text -> SExpr)
-> ParsecT Text st Identity Text -> GenParser st SExpr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text -> ParsecT Text st Identity Text
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try ParsecT Text st Identity Text
forall st. GenParser st Text
keyword
    GenParser st SExpr -> GenParser st SExpr -> GenParser st SExpr
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Text -> SExpr
SESymbol (Text -> SExpr)
-> ParsecT Text st Identity Text -> GenParser st SExpr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text -> ParsecT Text st Identity Text
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try ParsecT Text st Identity Text
forall st. GenParser st Text
symbol
    GenParser st SExpr -> SourceName -> GenParser st SExpr
forall s u (m :: * -> *) a.
ParsecT s u m a -> SourceName -> ParsecT s u m a
<?> "s-expressions"

-- * Identifiers (Sec 3.3)

index :: GenParser st Index
index :: GenParser st Index
index =
  Text -> Index
IxNumeral (Text -> Index)
-> ParsecT Text st Identity Text -> GenParser st Index
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text
forall st. GenParser st Text
numeral
    GenParser st Index -> GenParser st Index -> GenParser st Index
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Text -> Index
IxSymbol (Text -> Index)
-> ParsecT Text st Identity Text -> GenParser st Index
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text
forall st. GenParser st Text
symbol

identifier :: GenParser st Identifier
identifier :: GenParser st Identifier
identifier =
  Text -> Identifier
IdSymbol (Text -> Identifier)
-> ParsecT Text st Identity Text -> GenParser st Identifier
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text
forall st. GenParser st Text
symbol -- symbol cannot start with (, so no ambiguity
    GenParser st Identifier
-> GenParser st Identifier -> GenParser st Identifier
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> GenParser st Identifier
forall st. GenParser st Identifier
idIndexed
    GenParser st Identifier -> SourceName -> GenParser st Identifier
forall s u (m :: * -> *) a.
ParsecT s u m a -> SourceName -> ParsecT s u m a
<?> "identifier"
  where
    idIndexed :: GenParser st Identifier
idIndexed = GenParser st Identifier -> GenParser st Identifier
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st Identifier -> GenParser st Identifier)
-> GenParser st Identifier -> GenParser st Identifier
forall a b. (a -> b) -> a -> b
$ do
      Char -> ParsecT Text st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '_' ParsecT Text st Identity Char
-> ParsecT Text st Identity () -> ParsecT Text st Identity Char
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1
      Text
s <- GenParser st Text
forall st. GenParser st Text
symbol GenParser st Text
-> ParsecT Text st Identity () -> GenParser st Text
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1
      Text -> NonEmpty Index -> Identifier
IdIndexed Text
s (NonEmpty Index -> Identifier)
-> ParsecT Text st Identity (NonEmpty Index)
-> GenParser st Identifier
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenParser st Index -> ParsecT Text st Identity (NonEmpty Index)
forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepSpace1 GenParser st Index
forall st. GenParser st Index
index

-- * Attributes (Sec. 3.4)

attributeValue :: GenParser st AttributeValue
attributeValue :: GenParser st AttributeValue
attributeValue =
  SpecConstant -> AttributeValue
AttrValSpecConstant (SpecConstant -> AttributeValue)
-> ParsecT Text st Identity SpecConstant
-> GenParser st AttributeValue
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity SpecConstant
forall st. GenParser st SpecConstant
specConstant
    GenParser st AttributeValue
-> GenParser st AttributeValue -> GenParser st AttributeValue
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Text -> AttributeValue
AttrValSymbol (Text -> AttributeValue)
-> ParsecT Text st Identity Text -> GenParser st AttributeValue
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text
forall st. GenParser st Text
symbol
    GenParser st AttributeValue
-> GenParser st AttributeValue -> GenParser st AttributeValue
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SList -> AttributeValue
AttrValSList (SList -> AttributeValue)
-> ParsecT Text st Identity SList -> GenParser st AttributeValue
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity SList
forall st. GenParser st SList
slist
    GenParser st AttributeValue
-> SourceName -> GenParser st AttributeValue
forall s u (m :: * -> *) a.
ParsecT s u m a -> SourceName -> ParsecT s u m a
<?> "attribute value"

attribute :: GenParser st Attribute
attribute :: GenParser st Attribute
attribute =
  Text -> AttributeValue -> Attribute
AttrKeyValue (Text -> AttributeValue -> Attribute)
-> ParsecT Text st Identity Text
-> ParsecT Text st Identity (AttributeValue -> Attribute)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text -> ParsecT Text st Identity Text
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try (ParsecT Text st Identity Text
forall st. GenParser st Text
keyword ParsecT Text st Identity Text
-> ParsecT Text st Identity () -> ParsecT Text st Identity Text
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1) ParsecT Text st Identity (AttributeValue -> Attribute)
-> ParsecT Text st Identity AttributeValue
-> GenParser st Attribute
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT Text st Identity AttributeValue
forall st. GenParser st AttributeValue
attributeValue
    GenParser st Attribute
-> GenParser st Attribute -> GenParser st Attribute
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Text -> Attribute
AttrKey (Text -> Attribute)
-> ParsecT Text st Identity Text -> GenParser st Attribute
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text
forall st. GenParser st Text
keyword
    GenParser st Attribute -> SourceName -> GenParser st Attribute
forall s u (m :: * -> *) a.
ParsecT s u m a -> SourceName -> ParsecT s u m a
<?> "attribute"

-- * Sorts (Sec 3.5)

sortParameter :: GenParser st Sort
sortParameter :: GenParser st Sort
sortParameter = GenParser st Sort -> GenParser st Sort
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st Sort -> GenParser st Sort)
-> GenParser st Sort -> GenParser st Sort
forall a b. (a -> b) -> a -> b
$ do
  Identifier
i <- GenParser st Identifier
forall st. GenParser st Identifier
identifier GenParser st Identifier
-> ParsecT Text st Identity () -> GenParser st Identifier
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1
  Identifier -> NonEmpty Sort -> Sort
SortParameter Identifier
i (NonEmpty Sort -> Sort)
-> ParsecT Text st Identity (NonEmpty Sort) -> GenParser st Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenParser st Sort -> ParsecT Text st Identity (NonEmpty Sort)
forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepSpace1 GenParser st Sort
forall st. GenParser st Sort
sort

sort :: GenParser st Sort
sort :: GenParser st Sort
sort =
  Identifier -> Sort
SortSymbol (Identifier -> Sort)
-> ParsecT Text st Identity Identifier -> GenParser st Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Identifier
-> ParsecT Text st Identity Identifier
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try ParsecT Text st Identity Identifier
forall st. GenParser st Identifier
identifier
    GenParser st Sort -> GenParser st Sort -> GenParser st Sort
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> GenParser st Sort
forall st. GenParser st Sort
sortParameter
    GenParser st Sort -> SourceName -> GenParser st Sort
forall s u (m :: * -> *) a.
ParsecT s u m a -> SourceName -> ParsecT s u m a
<?> "sort"

-- * Terms and Formulas (Sec 3.6)

qualIdentifier :: GenParser st QualIdentifier
qualIdentifier :: GenParser st QualIdentifier
qualIdentifier =
  Identifier -> QualIdentifier
Unqualified (Identifier -> QualIdentifier)
-> ParsecT Text st Identity Identifier
-> GenParser st QualIdentifier
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Identifier
-> ParsecT Text st Identity Identifier
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try ParsecT Text st Identity Identifier
forall st. GenParser st Identifier
identifier
    GenParser st QualIdentifier
-> GenParser st QualIdentifier -> GenParser st QualIdentifier
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> GenParser st QualIdentifier -> GenParser st QualIdentifier
forall st a. GenParser st a -> GenParser st a
betweenBrackets GenParser st QualIdentifier
forall st. GenParser st QualIdentifier
annotation
    GenParser st QualIdentifier
-> SourceName -> GenParser st QualIdentifier
forall s u (m :: * -> *) a.
ParsecT s u m a -> SourceName -> ParsecT s u m a
<?> "qual identifier"
  where
    annotation :: GenParser st QualIdentifier
    annotation :: GenParser st QualIdentifier
annotation = do
      SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryStrBraket "as"
      Identifier
id <- GenParser st Identifier
forall st. GenParser st Identifier
identifier GenParser st Identifier
-> GenParser st () -> GenParser st Identifier
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* GenParser st ()
forall st. GenParser st ()
spaces1
      Identifier -> Sort -> QualIdentifier
Qualified Identifier
id (Sort -> QualIdentifier)
-> ParsecT Text st Identity Sort -> GenParser st QualIdentifier
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Sort
forall st. GenParser st Sort
sort

varBinding :: GenParser st VarBinding
varBinding :: GenParser st VarBinding
varBinding = GenParser st VarBinding -> GenParser st VarBinding
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st VarBinding -> GenParser st VarBinding)
-> GenParser st VarBinding -> GenParser st VarBinding
forall a b. (a -> b) -> a -> b
$ Text -> Term -> VarBinding
VarBinding (Text -> Term -> VarBinding)
-> ParsecT Text st Identity Text
-> ParsecT Text st Identity (Term -> VarBinding)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text
forall st. GenParser st Text
symbol ParsecT Text st Identity (Term -> VarBinding)
-> ParsecT Text st Identity ()
-> ParsecT Text st Identity (Term -> VarBinding)
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1 ParsecT Text st Identity (Term -> VarBinding)
-> ParsecT Text st Identity Term -> GenParser st VarBinding
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT Text st Identity Term
forall st. GenParser st Term
term

sortedVar :: GenParser st SortedVar
sortedVar :: GenParser st SortedVar
sortedVar = GenParser st SortedVar -> GenParser st SortedVar
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st SortedVar -> GenParser st SortedVar)
-> GenParser st SortedVar -> GenParser st SortedVar
forall a b. (a -> b) -> a -> b
$ Text -> Sort -> SortedVar
SortedVar (Text -> Sort -> SortedVar)
-> ParsecT Text st Identity Text
-> ParsecT Text st Identity (Sort -> SortedVar)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text
forall st. GenParser st Text
symbol ParsecT Text st Identity (Sort -> SortedVar)
-> ParsecT Text st Identity ()
-> ParsecT Text st Identity (Sort -> SortedVar)
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1 ParsecT Text st Identity (Sort -> SortedVar)
-> ParsecT Text st Identity Sort -> GenParser st SortedVar
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT Text st Identity Sort
forall st. GenParser st Sort
sort

matchPattern :: GenParser st MatchPattern
matchPattern :: GenParser st MatchPattern
matchPattern =
  Text -> MatchPattern
MPVariable (Text -> MatchPattern)
-> ParsecT Text st Identity Text -> GenParser st MatchPattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text
forall st. GenParser st Text
symbol
    GenParser st MatchPattern
-> GenParser st MatchPattern -> GenParser st MatchPattern
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> GenParser st MatchPattern
forall st. GenParser st MatchPattern
mPConstructor
    GenParser st MatchPattern
-> SourceName -> GenParser st MatchPattern
forall s u (m :: * -> *) a.
ParsecT s u m a -> SourceName -> ParsecT s u m a
<?> "pattern"
  where
    mPConstructor :: GenParser st MatchPattern
mPConstructor = GenParser st MatchPattern -> GenParser st MatchPattern
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st MatchPattern -> GenParser st MatchPattern)
-> GenParser st MatchPattern -> GenParser st MatchPattern
forall a b. (a -> b) -> a -> b
$ do
      Text
c <- GenParser st Text
forall st. GenParser st Text
symbol GenParser st Text
-> ParsecT Text st Identity () -> GenParser st Text
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1
      Text -> NonEmpty Text -> MatchPattern
MPConstructor Text
c (NonEmpty Text -> MatchPattern)
-> ParsecT Text st Identity (NonEmpty Text)
-> GenParser st MatchPattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenParser st Text -> ParsecT Text st Identity (NonEmpty Text)
forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepSpace1 GenParser st Text
forall st. GenParser st Text
symbol

matchCase :: GenParser st MatchCase
matchCase :: GenParser st MatchCase
matchCase = GenParser st MatchCase -> GenParser st MatchCase
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st MatchCase -> GenParser st MatchCase)
-> GenParser st MatchCase -> GenParser st MatchCase
forall a b. (a -> b) -> a -> b
$ do
  MatchPattern
p <- GenParser st MatchPattern
forall st. GenParser st MatchPattern
matchPattern GenParser st MatchPattern
-> ParsecT Text st Identity () -> GenParser st MatchPattern
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1
  MatchPattern -> Term -> MatchCase
MatchCase MatchPattern
p (Term -> MatchCase)
-> ParsecT Text st Identity Term -> GenParser st MatchCase
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Term
forall st. GenParser st Term
term

term :: GenParser st Term
term :: GenParser st Term
term =
  SpecConstant -> Term
TermSpecConstant (SpecConstant -> Term)
-> ParsecT Text st Identity SpecConstant -> GenParser st Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity SpecConstant
-> ParsecT Text st Identity SpecConstant
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try ParsecT Text st Identity SpecConstant
forall st. GenParser st SpecConstant
specConstant
    GenParser st Term -> GenParser st Term -> GenParser st Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> QualIdentifier -> Term
TermQualIdentifier (QualIdentifier -> Term)
-> ParsecT Text st Identity QualIdentifier -> GenParser st Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity QualIdentifier
-> ParsecT Text st Identity QualIdentifier
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try ParsecT Text st Identity QualIdentifier
forall st. GenParser st QualIdentifier
qualIdentifier
    GenParser st Term -> GenParser st Term -> GenParser st Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> GenParser st Term -> GenParser st Term
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try GenParser st Term
forall st. GenParser st Term
application
    GenParser st Term -> GenParser st Term -> GenParser st Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> GenParser st Term -> GenParser st Term
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try GenParser st Term
forall st. GenParser st Term
binding
    GenParser st Term -> GenParser st Term -> GenParser st Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> GenParser st Term -> GenParser st Term
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try GenParser st Term
forall st. GenParser st Term
quantifyForall
    GenParser st Term -> GenParser st Term -> GenParser st Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> GenParser st Term -> GenParser st Term
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try GenParser st Term
forall st. GenParser st Term
quantifyExists
    GenParser st Term -> GenParser st Term -> GenParser st Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> GenParser st Term -> GenParser st Term
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try GenParser st Term
forall st. GenParser st Term
match
    GenParser st Term -> GenParser st Term -> GenParser st Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> GenParser st Term -> GenParser st Term
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try GenParser st Term
forall st. GenParser st Term
annotation
    GenParser st Term -> SourceName -> GenParser st Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> SourceName -> ParsecT s u m a
<?> "term"
  where
    application :: GenParser st Term
application = GenParser st Term -> GenParser st Term
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st Term -> GenParser st Term)
-> GenParser st Term -> GenParser st Term
forall a b. (a -> b) -> a -> b
$ do
      QualIdentifier
id <- GenParser st QualIdentifier
forall st. GenParser st QualIdentifier
qualIdentifier GenParser st QualIdentifier
-> ParsecT Text st Identity () -> GenParser st QualIdentifier
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces
      QualIdentifier -> NonEmpty Term -> Term
TermApplication QualIdentifier
id (NonEmpty Term -> Term)
-> ParsecT Text st Identity (NonEmpty Term) -> GenParser st Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenParser st Term -> ParsecT Text st Identity (NonEmpty Term)
forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepOptSpace1 GenParser st Term
forall st. GenParser st Term
term
    binding :: GenParser st Term
binding = GenParser st Term -> GenParser st Term
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st Term -> GenParser st Term)
-> GenParser st Term -> GenParser st Term
forall a b. (a -> b) -> a -> b
$ do
      SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryStr "let"
      NonEmpty VarBinding
vbs <- GenParser st (NonEmpty VarBinding)
-> GenParser st (NonEmpty VarBinding)
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st (NonEmpty VarBinding)
 -> GenParser st (NonEmpty VarBinding))
-> GenParser st (NonEmpty VarBinding)
-> GenParser st (NonEmpty VarBinding)
forall a b. (a -> b) -> a -> b
$ GenParser st VarBinding -> GenParser st (NonEmpty VarBinding)
forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepOptSpace1 GenParser st VarBinding
forall st. GenParser st VarBinding
varBinding
      GenParser st ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces
      NonEmpty VarBinding -> Term -> Term
TermLet NonEmpty VarBinding
vbs (Term -> Term) -> GenParser st Term -> GenParser st Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenParser st Term
forall st. GenParser st Term
term
    quantifyForall :: GenParser st Term
quantifyForall = GenParser st Term -> GenParser st Term
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st Term -> GenParser st Term)
-> GenParser st Term -> GenParser st Term
forall a b. (a -> b) -> a -> b
$ do
      SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryStr "forall"
      NonEmpty SortedVar
svs <- GenParser st (NonEmpty SortedVar)
-> GenParser st (NonEmpty SortedVar)
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st (NonEmpty SortedVar)
 -> GenParser st (NonEmpty SortedVar))
-> GenParser st (NonEmpty SortedVar)
-> GenParser st (NonEmpty SortedVar)
forall a b. (a -> b) -> a -> b
$ GenParser st SortedVar -> GenParser st (NonEmpty SortedVar)
forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepOptSpace1 GenParser st SortedVar
forall st. GenParser st SortedVar
sortedVar
      GenParser st ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces
      NonEmpty SortedVar -> Term -> Term
TermForall NonEmpty SortedVar
svs (Term -> Term) -> GenParser st Term -> GenParser st Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenParser st Term
forall st. GenParser st Term
term
    quantifyExists :: GenParser st Term
quantifyExists = GenParser st Term -> GenParser st Term
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st Term -> GenParser st Term)
-> GenParser st Term -> GenParser st Term
forall a b. (a -> b) -> a -> b
$ do
      SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryStr "exists"
      NonEmpty SortedVar
svs <- GenParser st (NonEmpty SortedVar)
-> GenParser st (NonEmpty SortedVar)
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st (NonEmpty SortedVar)
 -> GenParser st (NonEmpty SortedVar))
-> GenParser st (NonEmpty SortedVar)
-> GenParser st (NonEmpty SortedVar)
forall a b. (a -> b) -> a -> b
$ GenParser st SortedVar -> GenParser st (NonEmpty SortedVar)
forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepOptSpace1 GenParser st SortedVar
forall st. GenParser st SortedVar
sortedVar
      GenParser st ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces
      NonEmpty SortedVar -> Term -> Term
TermExists NonEmpty SortedVar
svs (Term -> Term) -> GenParser st Term -> GenParser st Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenParser st Term
forall st. GenParser st Term
term
    match :: GenParser st Term
match = GenParser st Term -> GenParser st Term
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st Term -> GenParser st Term)
-> GenParser st Term -> GenParser st Term
forall a b. (a -> b) -> a -> b
$ do
      SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryStr "match"
      Term
t <- GenParser st Term
forall st. GenParser st Term
term GenParser st Term -> GenParser st () -> GenParser st Term
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* GenParser st ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces
      Term -> NonEmpty MatchCase -> Term
TermMatch Term
t (NonEmpty MatchCase -> Term)
-> ParsecT Text st Identity (NonEmpty MatchCase)
-> GenParser st Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity (NonEmpty MatchCase)
-> ParsecT Text st Identity (NonEmpty MatchCase)
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st MatchCase
-> ParsecT Text st Identity (NonEmpty MatchCase)
forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepOptSpace1 GenParser st MatchCase
forall st. GenParser st MatchCase
matchCase)
    annotation :: GenParser st Term
annotation = GenParser st Term -> GenParser st Term
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st Term -> GenParser st Term)
-> GenParser st Term -> GenParser st Term
forall a b. (a -> b) -> a -> b
$ do
      Char -> ParsecT Text st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '!' ParsecT Text st Identity Char
-> ParsecT Text st Identity () -> ParsecT Text st Identity Char
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1
      Term
t <- GenParser st Term
forall st. GenParser st Term
term GenParser st Term
-> ParsecT Text st Identity () -> GenParser st Term
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1
      Term -> NonEmpty Attribute -> Term
TermAnnotation Term
t (NonEmpty Attribute -> Term)
-> ParsecT Text st Identity (NonEmpty Attribute)
-> GenParser st Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenParser st Attribute
-> ParsecT Text st Identity (NonEmpty Attribute)
forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepSpace1 GenParser st Attribute
forall st. GenParser st Attribute
attribute

-- * Theory declarations (Sec 3.7)

sortSymbolDecl :: GenParser st SortSymbolDecl
sortSymbolDecl :: GenParser st SortSymbolDecl
sortSymbolDecl = GenParser st SortSymbolDecl -> GenParser st SortSymbolDecl
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st SortSymbolDecl -> GenParser st SortSymbolDecl)
-> GenParser st SortSymbolDecl -> GenParser st SortSymbolDecl
forall a b. (a -> b) -> a -> b
$ do
  Identifier
i <- GenParser st Identifier
forall st. GenParser st Identifier
identifier GenParser st Identifier
-> ParsecT Text st Identity () -> GenParser st Identifier
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1
  Text
n <- GenParser st Text
forall st. GenParser st Text
numeral GenParser st Text
-> ParsecT Text st Identity () -> GenParser st Text
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces -- if no attribute, don't need space
  Identifier -> Text -> [Attribute] -> SortSymbolDecl
SortSymbolDecl Identifier
i Text
n ([Attribute] -> SortSymbolDecl)
-> ParsecT Text st Identity [Attribute]
-> GenParser st SortSymbolDecl
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenParser st Attribute -> ParsecT Text st Identity [Attribute]
forall st a. GenParser st a -> GenParser st [a]
sepSpace GenParser st Attribute
forall st. GenParser st Attribute
attribute

metaSpecConstant :: GenParser st MetaSpecConstant
metaSpecConstant :: GenParser st MetaSpecConstant
metaSpecConstant =
  SourceName -> ParsecT Text st Identity SourceName
forall s (m :: * -> *) u.
Stream s m Char =>
SourceName -> ParsecT s u m SourceName
string "NUMERAL" ParsecT Text st Identity SourceName
-> MetaSpecConstant -> GenParser st MetaSpecConstant
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> MetaSpecConstant
MSC_NUMERAL
    GenParser st MetaSpecConstant
-> GenParser st MetaSpecConstant -> GenParser st MetaSpecConstant
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> ParsecT Text st Identity SourceName
forall s (m :: * -> *) u.
Stream s m Char =>
SourceName -> ParsecT s u m SourceName
string "DECIMAL" ParsecT Text st Identity SourceName
-> MetaSpecConstant -> GenParser st MetaSpecConstant
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> MetaSpecConstant
MSC_DECIMAL
    GenParser st MetaSpecConstant
-> GenParser st MetaSpecConstant -> GenParser st MetaSpecConstant
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> ParsecT Text st Identity SourceName
forall s (m :: * -> *) u.
Stream s m Char =>
SourceName -> ParsecT s u m SourceName
string "STRING" ParsecT Text st Identity SourceName
-> MetaSpecConstant -> GenParser st MetaSpecConstant
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> MetaSpecConstant
MSC_STRING
    GenParser st MetaSpecConstant
-> SourceName -> GenParser st MetaSpecConstant
forall s u (m :: * -> *) a.
ParsecT s u m a -> SourceName -> ParsecT s u m a
<?> "meta spec constant"

funSymbolDecl :: GenParser st FunSymbolDecl
funSymbolDecl :: GenParser st FunSymbolDecl
funSymbolDecl =
  GenParser st FunSymbolDecl -> GenParser st FunSymbolDecl
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try (GenParser st FunSymbolDecl -> GenParser st FunSymbolDecl
forall st a. GenParser st a -> GenParser st a
betweenBrackets GenParser st FunSymbolDecl
forall st. ParsecT Text st Identity FunSymbolDecl
funConstant)
    GenParser st FunSymbolDecl
-> GenParser st FunSymbolDecl -> GenParser st FunSymbolDecl
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> GenParser st FunSymbolDecl -> GenParser st FunSymbolDecl
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try (GenParser st FunSymbolDecl -> GenParser st FunSymbolDecl
forall st a. GenParser st a -> GenParser st a
betweenBrackets GenParser st FunSymbolDecl
forall st. ParsecT Text st Identity FunSymbolDecl
funMeta)
    GenParser st FunSymbolDecl
-> GenParser st FunSymbolDecl -> GenParser st FunSymbolDecl
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> GenParser st FunSymbolDecl -> GenParser st FunSymbolDecl
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try (GenParser st FunSymbolDecl -> GenParser st FunSymbolDecl
forall st a. GenParser st a -> GenParser st a
betweenBrackets GenParser st FunSymbolDecl
forall st. ParsecT Text st Identity FunSymbolDecl
funIdentifier)
    GenParser st FunSymbolDecl
-> SourceName -> GenParser st FunSymbolDecl
forall s u (m :: * -> *) a.
ParsecT s u m a -> SourceName -> ParsecT s u m a
<?> "non-parametric function symbol declaration"
  where
    funConstant :: ParsecT Text st Identity FunSymbolDecl
funConstant = do
      SpecConstant
sc <- GenParser st SpecConstant
forall st. GenParser st SpecConstant
specConstant GenParser st SpecConstant
-> ParsecT Text st Identity () -> GenParser st SpecConstant
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1
      Sort
s <- GenParser st Sort
forall st. GenParser st Sort
sort GenParser st Sort
-> ParsecT Text st Identity () -> GenParser st Sort
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1
      SpecConstant -> Sort -> [Attribute] -> FunSymbolDecl
FunConstant SpecConstant
sc Sort
s ([Attribute] -> FunSymbolDecl)
-> ParsecT Text st Identity [Attribute]
-> ParsecT Text st Identity FunSymbolDecl
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenParser st Attribute -> ParsecT Text st Identity [Attribute]
forall st a. GenParser st a -> GenParser st [a]
sepSpace GenParser st Attribute
forall st. GenParser st Attribute
attribute
    funMeta :: ParsecT Text st Identity FunSymbolDecl
funMeta = do
      MetaSpecConstant
m <- GenParser st MetaSpecConstant
forall st. GenParser st MetaSpecConstant
metaSpecConstant GenParser st MetaSpecConstant
-> ParsecT Text st Identity () -> GenParser st MetaSpecConstant
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1
      Sort
s <- GenParser st Sort
forall st. GenParser st Sort
sort GenParser st Sort
-> ParsecT Text st Identity () -> GenParser st Sort
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1
      MetaSpecConstant -> Sort -> [Attribute] -> FunSymbolDecl
FunMeta MetaSpecConstant
m Sort
s ([Attribute] -> FunSymbolDecl)
-> ParsecT Text st Identity [Attribute]
-> ParsecT Text st Identity FunSymbolDecl
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenParser st Attribute -> ParsecT Text st Identity [Attribute]
forall st a. GenParser st a -> GenParser st [a]
sepSpace GenParser st Attribute
forall st. GenParser st Attribute
attribute
    funIdentifier :: ParsecT Text st Identity FunSymbolDecl
funIdentifier = do
      Identifier
i <- GenParser st Identifier
forall st. GenParser st Identifier
identifier GenParser st Identifier
-> ParsecT Text st Identity () -> GenParser st Identifier
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1
      NonEmpty Sort
ss <- GenParser st Sort -> GenParser st (NonEmpty Sort)
forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepSpace1 GenParser st Sort
forall st. GenParser st Sort
sort
      [Attribute]
as <- GenParser st Attribute -> GenParser st [Attribute]
forall st a. GenParser st a -> GenParser st [a]
sepSpace GenParser st Attribute
forall st. GenParser st Attribute
attribute
      FunSymbolDecl -> ParsecT Text st Identity FunSymbolDecl
forall (m :: * -> *) a. Monad m => a -> m a
return (FunSymbolDecl -> ParsecT Text st Identity FunSymbolDecl)
-> FunSymbolDecl -> ParsecT Text st Identity FunSymbolDecl
forall a b. (a -> b) -> a -> b
$ Identifier -> NonEmpty Sort -> [Attribute] -> FunSymbolDecl
FunIdentifier Identifier
i NonEmpty Sort
ss [Attribute]
as

parFunSymbolDecl :: GenParser st ParFunSymbolDecl
parFunSymbolDecl :: GenParser st ParFunSymbolDecl
parFunSymbolDecl =
  FunSymbolDecl -> ParFunSymbolDecl
NonPar (FunSymbolDecl -> ParFunSymbolDecl)
-> ParsecT Text st Identity FunSymbolDecl
-> GenParser st ParFunSymbolDecl
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity FunSymbolDecl
forall st. ParsecT Text st Identity FunSymbolDecl
funSymbolDecl
    GenParser st ParFunSymbolDecl
-> GenParser st ParFunSymbolDecl -> GenParser st ParFunSymbolDecl
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> GenParser st ParFunSymbolDecl -> GenParser st ParFunSymbolDecl
forall st a. GenParser st a -> GenParser st a
betweenBrackets GenParser st ParFunSymbolDecl
forall st. ParsecT Text st Identity ParFunSymbolDecl
par
    GenParser st ParFunSymbolDecl
-> SourceName -> GenParser st ParFunSymbolDecl
forall s u (m :: * -> *) a.
ParsecT s u m a -> SourceName -> ParsecT s u m a
<?> "potentially parametric function symbol declaration"
  where
    par :: ParsecT Text st Identity ParFunSymbolDecl
par = do
      SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryStr "par"
      NonEmpty Text
syms <- GenParser st (NonEmpty Text) -> GenParser st (NonEmpty Text)
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st (NonEmpty Text) -> GenParser st (NonEmpty Text))
-> (GenParser st Text -> GenParser st (NonEmpty Text))
-> GenParser st Text
-> GenParser st (NonEmpty Text)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GenParser st Text -> GenParser st (NonEmpty Text)
forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepSpace1 (GenParser st Text -> GenParser st (NonEmpty Text))
-> GenParser st Text -> GenParser st (NonEmpty Text)
forall a b. (a -> b) -> a -> b
$ GenParser st Text
forall st. GenParser st Text
symbol
      GenParser st ()
forall st. GenParser st ()
spaces1
      ParsecT Text st Identity ParFunSymbolDecl
-> ParsecT Text st Identity ParFunSymbolDecl
forall st a. GenParser st a -> GenParser st a
betweenBrackets (ParsecT Text st Identity ParFunSymbolDecl
 -> ParsecT Text st Identity ParFunSymbolDecl)
-> ParsecT Text st Identity ParFunSymbolDecl
-> ParsecT Text st Identity ParFunSymbolDecl
forall a b. (a -> b) -> a -> b
$ do
        Identifier
idt <- GenParser st Identifier
forall st. GenParser st Identifier
identifier GenParser st Identifier
-> GenParser st () -> GenParser st Identifier
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* GenParser st ()
forall st. GenParser st ()
spaces1
        NonEmpty Sort
ss <- GenParser st Sort -> GenParser st (NonEmpty Sort)
forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepSpace1 GenParser st Sort
forall st. GenParser st Sort
sort
        NonEmpty Text
-> Identifier -> NonEmpty Sort -> [Attribute] -> ParFunSymbolDecl
Par NonEmpty Text
syms Identifier
idt NonEmpty Sort
ss ([Attribute] -> ParFunSymbolDecl)
-> ParsecT Text st Identity [Attribute]
-> ParsecT Text st Identity ParFunSymbolDecl
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenParser st Attribute -> ParsecT Text st Identity [Attribute]
forall st a. GenParser st a -> GenParser st [a]
sepSpace GenParser st Attribute
forall st. GenParser st Attribute
attribute

theoryAttribute :: GenParser st TheoryAttribute
theoryAttribute :: GenParser st TheoryAttribute
theoryAttribute =
  SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryAttr "sorts" GenParser st ()
-> GenParser st TheoryAttribute -> GenParser st TheoryAttribute
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> GenParser st TheoryAttribute -> GenParser st TheoryAttribute
forall st a. GenParser st a -> GenParser st a
betweenBrackets (NonEmpty SortSymbolDecl -> TheoryAttribute
TASorts (NonEmpty SortSymbolDecl -> TheoryAttribute)
-> ParsecT Text st Identity (NonEmpty SortSymbolDecl)
-> GenParser st TheoryAttribute
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenParser st SortSymbolDecl
-> ParsecT Text st Identity (NonEmpty SortSymbolDecl)
forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepSpace1 GenParser st SortSymbolDecl
forall st. GenParser st SortSymbolDecl
sortSymbolDecl)
    GenParser st TheoryAttribute
-> GenParser st TheoryAttribute -> GenParser st TheoryAttribute
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryAttr "funs" GenParser st ()
-> GenParser st TheoryAttribute -> GenParser st TheoryAttribute
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> GenParser st TheoryAttribute -> GenParser st TheoryAttribute
forall st a. GenParser st a -> GenParser st a
betweenBrackets (NonEmpty ParFunSymbolDecl -> TheoryAttribute
TAFuns (NonEmpty ParFunSymbolDecl -> TheoryAttribute)
-> ParsecT Text st Identity (NonEmpty ParFunSymbolDecl)
-> GenParser st TheoryAttribute
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenParser st ParFunSymbolDecl
-> ParsecT Text st Identity (NonEmpty ParFunSymbolDecl)
forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepSpace1 GenParser st ParFunSymbolDecl
forall st. ParsecT Text st Identity ParFunSymbolDecl
parFunSymbolDecl)
    GenParser st TheoryAttribute
-> GenParser st TheoryAttribute -> GenParser st TheoryAttribute
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryAttr "sorts-description" GenParser st ()
-> GenParser st TheoryAttribute -> GenParser st TheoryAttribute
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (Text -> TheoryAttribute
TASortsDescription (Text -> TheoryAttribute)
-> ParsecT Text st Identity Text -> GenParser st TheoryAttribute
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text
forall st. GenParser st Text
stringLiteral)
    GenParser st TheoryAttribute
-> GenParser st TheoryAttribute -> GenParser st TheoryAttribute
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryAttr "funs-description" GenParser st ()
-> GenParser st TheoryAttribute -> GenParser st TheoryAttribute
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (Text -> TheoryAttribute
TAFunsDescription (Text -> TheoryAttribute)
-> ParsecT Text st Identity Text -> GenParser st TheoryAttribute
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text
forall st. GenParser st Text
stringLiteral)
    GenParser st TheoryAttribute
-> GenParser st TheoryAttribute -> GenParser st TheoryAttribute
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryAttr "definition" GenParser st ()
-> GenParser st TheoryAttribute -> GenParser st TheoryAttribute
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (Text -> TheoryAttribute
TADefinition (Text -> TheoryAttribute)
-> ParsecT Text st Identity Text -> GenParser st TheoryAttribute
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text
forall st. GenParser st Text
stringLiteral)
    GenParser st TheoryAttribute
-> GenParser st TheoryAttribute -> GenParser st TheoryAttribute
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryAttr "values" GenParser st ()
-> GenParser st TheoryAttribute -> GenParser st TheoryAttribute
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (Text -> TheoryAttribute
TAValues (Text -> TheoryAttribute)
-> ParsecT Text st Identity Text -> GenParser st TheoryAttribute
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text
forall st. GenParser st Text
stringLiteral)
    GenParser st TheoryAttribute
-> GenParser st TheoryAttribute -> GenParser st TheoryAttribute
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryAttr "notes" GenParser st ()
-> GenParser st TheoryAttribute -> GenParser st TheoryAttribute
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (Text -> TheoryAttribute
TANotes (Text -> TheoryAttribute)
-> ParsecT Text st Identity Text -> GenParser st TheoryAttribute
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text
forall st. GenParser st Text
stringLiteral)
    GenParser st TheoryAttribute
-> GenParser st TheoryAttribute -> GenParser st TheoryAttribute
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Attribute -> TheoryAttribute
TAAttr (Attribute -> TheoryAttribute)
-> ParsecT Text st Identity Attribute
-> GenParser st TheoryAttribute
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Attribute
forall st. GenParser st Attribute
attribute
    GenParser st TheoryAttribute
-> SourceName -> GenParser st TheoryAttribute
forall s u (m :: * -> *) a.
ParsecT s u m a -> SourceName -> ParsecT s u m a
<?> "theory attributes"

theoryDecl :: GenParser st TheoryDecl
theoryDecl :: GenParser st TheoryDecl
theoryDecl = GenParser st TheoryDecl -> GenParser st TheoryDecl
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st TheoryDecl -> GenParser st TheoryDecl)
-> GenParser st TheoryDecl -> GenParser st TheoryDecl
forall a b. (a -> b) -> a -> b
$ do
  SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryStr "theory"
  Text
s <- GenParser st Text
forall st. GenParser st Text
symbol GenParser st Text -> GenParser st () -> GenParser st Text
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* GenParser st ()
forall st. GenParser st ()
spaces1
  Text -> NonEmpty TheoryAttribute -> TheoryDecl
TheoryDecl Text
s (NonEmpty TheoryAttribute -> TheoryDecl)
-> ParsecT Text st Identity (NonEmpty TheoryAttribute)
-> GenParser st TheoryDecl
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenParser st TheoryAttribute
-> ParsecT Text st Identity (NonEmpty TheoryAttribute)
forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepSpace1 GenParser st TheoryAttribute
forall st. GenParser st TheoryAttribute
theoryAttribute

-- * Logic Declarations (Sec 3.8)

logicAttribute :: GenParser st LogicAttribute
logicAttribute :: GenParser st LogicAttribute
logicAttribute =
  SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryAttr "theories" GenParser st ()
-> GenParser st LogicAttribute -> GenParser st LogicAttribute
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> GenParser st LogicAttribute -> GenParser st LogicAttribute
forall st a. GenParser st a -> GenParser st a
betweenBrackets (NonEmpty Text -> LogicAttribute
LATheories (NonEmpty Text -> LogicAttribute)
-> ParsecT Text st Identity (NonEmpty Text)
-> GenParser st LogicAttribute
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenParser st Text -> ParsecT Text st Identity (NonEmpty Text)
forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepSpace1 GenParser st Text
forall st. GenParser st Text
symbol)
    GenParser st LogicAttribute
-> GenParser st LogicAttribute -> GenParser st LogicAttribute
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryAttr "language" GenParser st ()
-> GenParser st LogicAttribute -> GenParser st LogicAttribute
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (Text -> LogicAttribute
LALanguage (Text -> LogicAttribute)
-> GenParser st Text -> GenParser st LogicAttribute
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenParser st Text
forall st. GenParser st Text
stringLiteral)
    GenParser st LogicAttribute
-> GenParser st LogicAttribute -> GenParser st LogicAttribute
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryAttr "extensions" GenParser st ()
-> GenParser st LogicAttribute -> GenParser st LogicAttribute
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (Text -> LogicAttribute
LAExtensions (Text -> LogicAttribute)
-> GenParser st Text -> GenParser st LogicAttribute
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenParser st Text
forall st. GenParser st Text
stringLiteral)
    GenParser st LogicAttribute
-> GenParser st LogicAttribute -> GenParser st LogicAttribute
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryAttr "values" GenParser st ()
-> GenParser st LogicAttribute -> GenParser st LogicAttribute
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (Text -> LogicAttribute
LAValues (Text -> LogicAttribute)
-> GenParser st Text -> GenParser st LogicAttribute
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenParser st Text
forall st. GenParser st Text
stringLiteral)
    GenParser st LogicAttribute
-> GenParser st LogicAttribute -> GenParser st LogicAttribute
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryAttr "notes" GenParser st ()
-> GenParser st LogicAttribute -> GenParser st LogicAttribute
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (Text -> LogicAttribute
LANotes (Text -> LogicAttribute)
-> GenParser st Text -> GenParser st LogicAttribute
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenParser st Text
forall st. GenParser st Text
stringLiteral)
    GenParser st LogicAttribute
-> GenParser st LogicAttribute -> GenParser st LogicAttribute
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Attribute -> LogicAttribute
LAAttr (Attribute -> LogicAttribute)
-> ParsecT Text st Identity Attribute
-> GenParser st LogicAttribute
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Attribute
forall st. GenParser st Attribute
attribute

logic :: GenParser st Logic
logic :: GenParser st Logic
logic = GenParser st Logic -> GenParser st Logic
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st Logic -> GenParser st Logic)
-> GenParser st Logic -> GenParser st Logic
forall a b. (a -> b) -> a -> b
$ do
  SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryStr "logic"
  Text
s <- GenParser st Text
forall st. GenParser st Text
symbol GenParser st Text -> GenParser st () -> GenParser st Text
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* GenParser st ()
forall st. GenParser st ()
spaces1
  Text -> NonEmpty LogicAttribute -> Logic
Logic Text
s (NonEmpty LogicAttribute -> Logic)
-> ParsecT Text st Identity (NonEmpty LogicAttribute)
-> GenParser st Logic
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenParser st LogicAttribute
-> ParsecT Text st Identity (NonEmpty LogicAttribute)
forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepSpace1 GenParser st LogicAttribute
forall st. GenParser st LogicAttribute
logicAttribute

-- * Scripts (Sec 3.9)

sortDec :: GenParser st SortDec
sortDec :: GenParser st SortDec
sortDec = GenParser st SortDec -> GenParser st SortDec
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st SortDec -> GenParser st SortDec)
-> GenParser st SortDec -> GenParser st SortDec
forall a b. (a -> b) -> a -> b
$ do
  Text
s <- GenParser st Text
forall st. GenParser st Text
symbol GenParser st Text
-> ParsecT Text st Identity () -> GenParser st Text
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1
  Text -> Text -> SortDec
SortDec Text
s (Text -> SortDec) -> GenParser st Text -> GenParser st SortDec
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenParser st Text
forall st. GenParser st Text
numeral

selectorDec :: GenParser st SelectorDec
selectorDec :: GenParser st SelectorDec
selectorDec = GenParser st SelectorDec -> GenParser st SelectorDec
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st SelectorDec -> GenParser st SelectorDec)
-> GenParser st SelectorDec -> GenParser st SelectorDec
forall a b. (a -> b) -> a -> b
$ do
  Text
s <- GenParser st Text
forall st. GenParser st Text
symbol GenParser st Text
-> ParsecT Text st Identity () -> GenParser st Text
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1
  Text -> Sort -> SelectorDec
SelectorDec Text
s (Sort -> SelectorDec)
-> ParsecT Text st Identity Sort -> GenParser st SelectorDec
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Sort
forall st. GenParser st Sort
sort

constructorDec :: GenParser st ConstructorDec
constructorDec :: GenParser st ConstructorDec
constructorDec = GenParser st ConstructorDec -> GenParser st ConstructorDec
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st ConstructorDec -> GenParser st ConstructorDec)
-> GenParser st ConstructorDec -> GenParser st ConstructorDec
forall a b. (a -> b) -> a -> b
$ do
  Text
s <- GenParser st Text
forall st. GenParser st Text
symbol GenParser st Text
-> ParsecT Text st Identity () -> GenParser st Text
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1
  Text -> [SelectorDec] -> ConstructorDec
ConstructorDec Text
s ([SelectorDec] -> ConstructorDec)
-> ParsecT Text st Identity [SelectorDec]
-> GenParser st ConstructorDec
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenParser st SelectorDec -> ParsecT Text st Identity [SelectorDec]
forall st a. GenParser st a -> GenParser st [a]
sepSpace GenParser st SelectorDec
forall st. GenParser st SelectorDec
selectorDec

datatypeDec :: GenParser st DatatypeDec
datatypeDec :: GenParser st DatatypeDec
datatypeDec =
  NonEmpty ConstructorDec -> DatatypeDec
DDNonparametric (NonEmpty ConstructorDec -> DatatypeDec)
-> ParsecT Text st Identity (NonEmpty ConstructorDec)
-> GenParser st DatatypeDec
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity (NonEmpty ConstructorDec)
-> ParsecT Text st Identity (NonEmpty ConstructorDec)
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st ConstructorDec
-> ParsecT Text st Identity (NonEmpty ConstructorDec)
forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepSpace1 GenParser st ConstructorDec
forall st. GenParser st ConstructorDec
constructorDec)
    GenParser st DatatypeDec
-> GenParser st DatatypeDec -> GenParser st DatatypeDec
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> GenParser st DatatypeDec
forall st. GenParser st DatatypeDec
parametric
    GenParser st DatatypeDec -> SourceName -> GenParser st DatatypeDec
forall s u (m :: * -> *) a.
ParsecT s u m a -> SourceName -> ParsecT s u m a
<?> "datatype declaration"
  where
    parametric :: GenParser st DatatypeDec
parametric = GenParser st DatatypeDec -> GenParser st DatatypeDec
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st DatatypeDec -> GenParser st DatatypeDec)
-> GenParser st DatatypeDec -> GenParser st DatatypeDec
forall a b. (a -> b) -> a -> b
$ do
      SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryStr1 "par"
      NonEmpty Text
ss <- GenParser st (NonEmpty Text) -> GenParser st (NonEmpty Text)
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st (NonEmpty Text) -> GenParser st (NonEmpty Text))
-> GenParser st (NonEmpty Text) -> GenParser st (NonEmpty Text)
forall a b. (a -> b) -> a -> b
$ GenParser st Text -> GenParser st (NonEmpty Text)
forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepSpace1 GenParser st Text
forall st. GenParser st Text
symbol
      GenParser st ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces
      NonEmpty Text -> NonEmpty ConstructorDec -> DatatypeDec
DDParametric NonEmpty Text
ss (NonEmpty ConstructorDec -> DatatypeDec)
-> ParsecT Text st Identity (NonEmpty ConstructorDec)
-> GenParser st DatatypeDec
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity (NonEmpty ConstructorDec)
-> ParsecT Text st Identity (NonEmpty ConstructorDec)
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st ConstructorDec
-> ParsecT Text st Identity (NonEmpty ConstructorDec)
forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepSpace1 GenParser st ConstructorDec
forall st. GenParser st ConstructorDec
constructorDec)

functionDec :: GenParser st FunctionDec
functionDec :: GenParser st FunctionDec
functionDec = GenParser st FunctionDec -> GenParser st FunctionDec
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st FunctionDec -> GenParser st FunctionDec)
-> GenParser st FunctionDec -> GenParser st FunctionDec
forall a b. (a -> b) -> a -> b
$ do
  Text
s <- GenParser st Text
forall st. GenParser st Text
symbol GenParser st Text
-> ParsecT Text st Identity () -> GenParser st Text
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces
  [SortedVar]
svs <- GenParser st [SortedVar] -> GenParser st [SortedVar]
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st [SortedVar] -> GenParser st [SortedVar])
-> GenParser st [SortedVar] -> GenParser st [SortedVar]
forall a b. (a -> b) -> a -> b
$ GenParser st SortedVar -> GenParser st [SortedVar]
forall st a. GenParser st a -> GenParser st [a]
sepSpace GenParser st SortedVar
forall st. GenParser st SortedVar
sortedVar
  ParsecT Text st Identity ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces
  Text -> [SortedVar] -> Sort -> FunctionDec
FunctionDec Text
s [SortedVar]
svs (Sort -> FunctionDec)
-> ParsecT Text st Identity Sort -> GenParser st FunctionDec
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Sort
forall st. GenParser st Sort
sort

functionDef :: GenParser st FunctionDef
functionDef :: GenParser st FunctionDef
functionDef = GenParser st FunctionDef -> GenParser st FunctionDef
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st FunctionDef -> GenParser st FunctionDef)
-> GenParser st FunctionDef -> GenParser st FunctionDef
forall a b. (a -> b) -> a -> b
$ do
  Text
s <- GenParser st Text
forall st. GenParser st Text
symbol GenParser st Text
-> ParsecT Text st Identity () -> GenParser st Text
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces
  [SortedVar]
svs <- GenParser st [SortedVar] -> GenParser st [SortedVar]
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st [SortedVar] -> GenParser st [SortedVar])
-> GenParser st [SortedVar] -> GenParser st [SortedVar]
forall a b. (a -> b) -> a -> b
$ GenParser st SortedVar -> GenParser st [SortedVar]
forall st a. GenParser st a -> GenParser st [a]
sepSpace GenParser st SortedVar
forall st. GenParser st SortedVar
sortedVar
  Sort
t <- ParsecT Text st Identity ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces ParsecT Text st Identity ()
-> ParsecT Text st Identity Sort -> ParsecT Text st Identity Sort
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT Text st Identity Sort
forall st. GenParser st Sort
sort ParsecT Text st Identity Sort
-> ParsecT Text st Identity () -> ParsecT Text st Identity Sort
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1
  Text -> [SortedVar] -> Sort -> Term -> FunctionDef
FunctionDef Text
s [SortedVar]
svs Sort
t (Term -> FunctionDef)
-> ParsecT Text st Identity Term -> GenParser st FunctionDef
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Term
forall st. GenParser st Term
term

propLiteral :: GenParser st PropLiteral
propLiteral :: GenParser st PropLiteral
propLiteral =
  Text -> PropLiteral
PLPositive (Text -> PropLiteral)
-> ParsecT Text st Identity Text -> GenParser st PropLiteral
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text
forall st. GenParser st Text
symbol
    GenParser st PropLiteral
-> GenParser st PropLiteral -> GenParser st PropLiteral
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Text -> PropLiteral
PLNegative (Text -> PropLiteral)
-> ParsecT Text st Identity Text -> GenParser st PropLiteral
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text -> ParsecT Text st Identity Text
forall st a. GenParser st a -> GenParser st a
betweenBrackets (SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryStr1 "not" GenParser st ()
-> ParsecT Text st Identity Text -> ParsecT Text st Identity Text
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT Text st Identity Text
forall st. GenParser st Text
symbol)

command :: GenParser st Command
command :: GenParser st Command
command =
  SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "assert" (Term -> Command
Assert (Term -> Command)
-> ParsecT Text st Identity Term -> GenParser st Command
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Term
forall st. GenParser st Term
term)
    GenParser st Command
-> GenParser st Command -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "check-sat" (Command -> GenParser st Command
forall (f :: * -> *) a. Applicative f => a -> f a
pure Command
CheckSat)
    GenParser st Command
-> GenParser st Command -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "check-sat-assuming" (GenParser st Command -> GenParser st Command
forall st a. GenParser st a -> GenParser st a
betweenBrackets ([PropLiteral] -> Command
CheckSatAssuming ([PropLiteral] -> Command)
-> ParsecT Text st Identity [PropLiteral] -> GenParser st Command
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenParser st PropLiteral -> ParsecT Text st Identity [PropLiteral]
forall st a. GenParser st a -> GenParser st [a]
sepSpace GenParser st PropLiteral
forall st. GenParser st PropLiteral
propLiteral))
    GenParser st Command
-> GenParser st Command -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "declare-const" (Text -> Sort -> Command
DeclareConst (Text -> Sort -> Command)
-> ParsecT Text st Identity Text
-> ParsecT Text st Identity (Sort -> Command)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ParsecT Text st Identity Text
forall st. GenParser st Text
symbol ParsecT Text st Identity Text
-> ParsecT Text st Identity () -> ParsecT Text st Identity Text
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1) ParsecT Text st Identity (Sort -> Command)
-> ParsecT Text st Identity Sort -> GenParser st Command
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT Text st Identity Sort
forall st. GenParser st Sort
sort)
    GenParser st Command
-> GenParser st Command -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "declare-datatype" (Text -> DatatypeDec -> Command
DeclareDatatype (Text -> DatatypeDec -> Command)
-> ParsecT Text st Identity Text
-> ParsecT Text st Identity (DatatypeDec -> Command)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ParsecT Text st Identity Text
forall st. GenParser st Text
symbol ParsecT Text st Identity Text
-> ParsecT Text st Identity () -> ParsecT Text st Identity Text
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1) ParsecT Text st Identity (DatatypeDec -> Command)
-> ParsecT Text st Identity DatatypeDec -> GenParser st Command
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT Text st Identity DatatypeDec
forall st. GenParser st DatatypeDec
datatypeDec)
    GenParser st Command
-> GenParser st Command -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "declare-datatypes" GenParser st Command
forall st. ParsecT Text st Identity Command
declareDatatypes
    GenParser st Command
-> GenParser st Command -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "declare-fun" GenParser st Command
forall st. ParsecT Text st Identity Command
declareFun
    GenParser st Command
-> GenParser st Command -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "declare-sort" GenParser st Command
forall st. ParsecT Text st Identity Command
declareSort
    GenParser st Command
-> GenParser st Command -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "define-fun" (FunctionDef -> Command
DefineFun (FunctionDef -> Command)
-> ParsecT Text st Identity FunctionDef -> GenParser st Command
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity FunctionDef
forall st. GenParser st FunctionDef
functionDef)
    GenParser st Command
-> GenParser st Command -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "define-fun-rec" (FunctionDef -> Command
DefineFunRec (FunctionDef -> Command)
-> ParsecT Text st Identity FunctionDef -> GenParser st Command
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity FunctionDef
forall st. GenParser st FunctionDef
functionDef)
    GenParser st Command
-> GenParser st Command -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "define-funs-rec" GenParser st Command
forall st. ParsecT Text st Identity Command
defineFunsRec
    GenParser st Command
-> GenParser st Command -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "define-sort" GenParser st Command
forall st. ParsecT Text st Identity Command
defineSort
    GenParser st Command
-> GenParser st Command -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "echo" (Text -> Command
Echo (Text -> Command)
-> ParsecT Text st Identity Text -> GenParser st Command
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text
forall st. GenParser st Text
stringLiteral)
    GenParser st Command
-> GenParser st Command -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "exit" (Command -> GenParser st Command
forall (f :: * -> *) a. Applicative f => a -> f a
pure Command
Exit)
    GenParser st Command
-> GenParser st Command -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "get-assertions" (Command -> GenParser st Command
forall (f :: * -> *) a. Applicative f => a -> f a
pure Command
GetAssertions)
    GenParser st Command
-> GenParser st Command -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "get-assignment" (Command -> GenParser st Command
forall (f :: * -> *) a. Applicative f => a -> f a
pure Command
GetAssignment)
    GenParser st Command
-> GenParser st Command -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "get-info" (InfoFlag -> Command
GetInfo (InfoFlag -> Command)
-> ParsecT Text st Identity InfoFlag -> GenParser st Command
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity InfoFlag
forall st. GenParser st InfoFlag
infoFlag)
    GenParser st Command
-> GenParser st Command -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "get-model" (Command -> GenParser st Command
forall (f :: * -> *) a. Applicative f => a -> f a
pure Command
GetModel)
    GenParser st Command
-> GenParser st Command -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "get-option" (Text -> Command
GetOption (Text -> Command)
-> ParsecT Text st Identity Text -> GenParser st Command
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text
forall st. GenParser st Text
keyword)
    GenParser st Command
-> GenParser st Command -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "get-proof" (Command -> GenParser st Command
forall (f :: * -> *) a. Applicative f => a -> f a
pure Command
GetProof)
    GenParser st Command
-> GenParser st Command -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "get-unsat-assumptions" (Command -> GenParser st Command
forall (f :: * -> *) a. Applicative f => a -> f a
pure Command
GetUnsatAssumptions)
    GenParser st Command
-> GenParser st Command -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "get-unsat-core" (Command -> GenParser st Command
forall (f :: * -> *) a. Applicative f => a -> f a
pure Command
GetUnsatCore)
    GenParser st Command
-> GenParser st Command -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "get-value" (NonEmpty Term -> Command
GetValue (NonEmpty Term -> Command)
-> ParsecT Text st Identity (NonEmpty Term) -> GenParser st Command
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity (NonEmpty Term)
forall st. GenParser st (NonEmpty Term)
getValue)
    GenParser st Command
-> GenParser st Command -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "pop" (Text -> Command
Pop (Text -> Command)
-> ParsecT Text st Identity Text -> GenParser st Command
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text
forall st. GenParser st Text
numeral)
    GenParser st Command
-> GenParser st Command -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "push" (Text -> Command
Push (Text -> Command)
-> ParsecT Text st Identity Text -> GenParser st Command
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text
forall st. GenParser st Text
numeral)
    GenParser st Command
-> GenParser st Command -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "reset" (Command -> GenParser st Command
forall (f :: * -> *) a. Applicative f => a -> f a
pure Command
Reset)
    GenParser st Command
-> GenParser st Command -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "reset-assertions" (Command -> GenParser st Command
forall (f :: * -> *) a. Applicative f => a -> f a
pure Command
ResetAssertions)
    GenParser st Command
-> GenParser st Command -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "set-info" (Attribute -> Command
SetInfo (Attribute -> Command)
-> ParsecT Text st Identity Attribute -> GenParser st Command
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Attribute
forall st. GenParser st Attribute
attribute)
    GenParser st Command
-> GenParser st Command -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "set-logic" (Text -> Command
SetLogic (Text -> Command)
-> ParsecT Text st Identity Text -> GenParser st Command
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text
forall st. GenParser st Text
symbol)
    GenParser st Command
-> GenParser st Command -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "set-option" (ScriptOption -> Command
SetOption (ScriptOption -> Command)
-> ParsecT Text st Identity ScriptOption -> GenParser st Command
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity ScriptOption
forall st. GenParser st ScriptOption
scriptOption)
    GenParser st Command -> SourceName -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> SourceName -> ParsecT s u m a
<?> "command"
  where
    cmd :: SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd s :: SourceName
s p :: ParsecT Text u Identity a
p = ParsecT Text u Identity a -> ParsecT Text u Identity a
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try (ParsecT Text u Identity a -> ParsecT Text u Identity a)
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
forall a b. (a -> b) -> a -> b
$ ParsecT Text u Identity a -> ParsecT Text u Identity a
forall st a. GenParser st a -> GenParser st a
betweenBrackets (SourceName -> GenParser u ()
forall st. SourceName -> GenParser st ()
tryStr SourceName
s GenParser u ()
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT Text u Identity a
p)
    declareDatatypes :: ParsecT Text st Identity Command
declareDatatypes = do
      NonEmpty SortDec
sds <- GenParser st (NonEmpty SortDec) -> GenParser st (NonEmpty SortDec)
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st (NonEmpty SortDec)
 -> GenParser st (NonEmpty SortDec))
-> GenParser st (NonEmpty SortDec)
-> GenParser st (NonEmpty SortDec)
forall a b. (a -> b) -> a -> b
$ GenParser st SortDec -> GenParser st (NonEmpty SortDec)
forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepSpace1 GenParser st SortDec
forall st. GenParser st SortDec
sortDec
      ParsecT Text st Identity ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces
      NonEmpty DatatypeDec
dds <- GenParser st (NonEmpty DatatypeDec)
-> GenParser st (NonEmpty DatatypeDec)
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st (NonEmpty DatatypeDec)
 -> GenParser st (NonEmpty DatatypeDec))
-> GenParser st (NonEmpty DatatypeDec)
-> GenParser st (NonEmpty DatatypeDec)
forall a b. (a -> b) -> a -> b
$ GenParser st DatatypeDec -> GenParser st (NonEmpty DatatypeDec)
forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepSpace1 GenParser st DatatypeDec
forall st. GenParser st DatatypeDec
datatypeDec
      if NonEmpty SortDec -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length NonEmpty SortDec
sds Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== NonEmpty DatatypeDec -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length NonEmpty DatatypeDec
dds
        then Command -> ParsecT Text st Identity Command
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Command -> ParsecT Text st Identity Command)
-> Command -> ParsecT Text st Identity Command
forall a b. (a -> b) -> a -> b
$ NonEmpty SortDec -> NonEmpty DatatypeDec -> Command
DeclareDatatypes NonEmpty SortDec
sds NonEmpty DatatypeDec
dds
        else SourceName -> ParsecT Text st Identity Command
forall s (m :: * -> *) t u a.
Stream s m t =>
SourceName -> ParsecT s u m a
unexpected "declare-datatypes: sorts and datatypes should have same length"
    declareFun :: ParsecT Text st Identity Command
declareFun = do
      Text
s <- GenParser st Text
forall st. GenParser st Text
symbol GenParser st Text
-> ParsecT Text st Identity () -> GenParser st Text
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1
      [Sort]
ss <- GenParser st [Sort] -> GenParser st [Sort]
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st [Sort] -> GenParser st [Sort])
-> GenParser st [Sort] -> GenParser st [Sort]
forall a b. (a -> b) -> a -> b
$ GenParser st Sort -> GenParser st [Sort]
forall st a. GenParser st a -> GenParser st [a]
sepSpace GenParser st Sort
forall st. GenParser st Sort
sort
      ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1
      Text -> [Sort] -> Sort -> Command
DeclareFun Text
s [Sort]
ss (Sort -> Command)
-> GenParser st Sort -> ParsecT Text st Identity Command
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenParser st Sort
forall st. GenParser st Sort
sort
    declareSort :: ParsecT Text st Identity Command
declareSort = do
      Text
s <- GenParser st Text
forall st. GenParser st Text
symbol GenParser st Text
-> ParsecT Text st Identity () -> GenParser st Text
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1
      Text -> Text -> Command
DeclareSort Text
s (Text -> Command)
-> GenParser st Text -> ParsecT Text st Identity Command
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenParser st Text
forall st. GenParser st Text
numeral
    defineFunsRec :: ParsecT Text st Identity Command
defineFunsRec = do
      NonEmpty FunctionDec
fds <- GenParser st (NonEmpty FunctionDec)
-> GenParser st (NonEmpty FunctionDec)
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st (NonEmpty FunctionDec)
 -> GenParser st (NonEmpty FunctionDec))
-> GenParser st (NonEmpty FunctionDec)
-> GenParser st (NonEmpty FunctionDec)
forall a b. (a -> b) -> a -> b
$ GenParser st FunctionDec -> GenParser st (NonEmpty FunctionDec)
forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepSpace1 GenParser st FunctionDec
forall st. GenParser st FunctionDec
functionDec
      ParsecT Text st Identity ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces
      NonEmpty Term
ts <- GenParser st (NonEmpty Term) -> GenParser st (NonEmpty Term)
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st (NonEmpty Term) -> GenParser st (NonEmpty Term))
-> GenParser st (NonEmpty Term) -> GenParser st (NonEmpty Term)
forall a b. (a -> b) -> a -> b
$ GenParser st Term -> GenParser st (NonEmpty Term)
forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepSpace1 GenParser st Term
forall st. GenParser st Term
term
      if NonEmpty FunctionDec -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length NonEmpty FunctionDec
fds Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== NonEmpty Term -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length NonEmpty Term
ts
        then Command -> ParsecT Text st Identity Command
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Command -> ParsecT Text st Identity Command)
-> Command -> ParsecT Text st Identity Command
forall a b. (a -> b) -> a -> b
$ NonEmpty FunctionDec -> NonEmpty Term -> Command
DefineFunsRec NonEmpty FunctionDec
fds NonEmpty Term
ts
        else SourceName -> ParsecT Text st Identity Command
forall s (m :: * -> *) t u a.
Stream s m t =>
SourceName -> ParsecT s u m a
unexpected "define-funs-rec: declarations and terms should have same length"
    defineSort :: ParsecT Text st Identity Command
defineSort = do
      Text
s <- GenParser st Text
forall st. GenParser st Text
symbol GenParser st Text
-> ParsecT Text st Identity () -> GenParser st Text
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1
      [Text]
ss <- GenParser st [Text] -> GenParser st [Text]
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st [Text] -> GenParser st [Text])
-> GenParser st [Text] -> GenParser st [Text]
forall a b. (a -> b) -> a -> b
$ GenParser st Text -> GenParser st [Text]
forall st a. GenParser st a -> GenParser st [a]
sepSpace GenParser st Text
forall st. GenParser st Text
symbol
      ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1
      Text -> [Text] -> Sort -> Command
DefineSort Text
s [Text]
ss (Sort -> Command)
-> ParsecT Text st Identity Sort
-> ParsecT Text st Identity Command
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Sort
forall st. GenParser st Sort
sort
    getValue :: GenParser st (NonEmpty Term)
getValue = GenParser st (NonEmpty Term) -> GenParser st (NonEmpty Term)
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st (NonEmpty Term) -> GenParser st (NonEmpty Term))
-> GenParser st (NonEmpty Term) -> GenParser st (NonEmpty Term)
forall a b. (a -> b) -> a -> b
$ GenParser st Term -> GenParser st (NonEmpty Term)
forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepSpace1 GenParser st Term
forall st. GenParser st Term
term

script :: GenParser st Script
script :: GenParser st Script
script = ParsecT Text st Identity ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces ParsecT Text st Identity ()
-> GenParser st Script -> GenParser st Script
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> GenParser st Command -> GenParser st Script
forall st a. GenParser st a -> GenParser st [a]
sepOptSpace GenParser st Command
forall st. ParsecT Text st Identity Command
command GenParser st Script
-> ParsecT Text st Identity () -> GenParser st Script
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces

bValue :: GenParser st BValue
bValue :: GenParser st BValue
bValue =
  SourceName -> ParsecT Text st Identity SourceName
forall s (m :: * -> *) u.
Stream s m Char =>
SourceName -> ParsecT s u m SourceName
string "true" ParsecT Text st Identity SourceName
-> BValue -> GenParser st BValue
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> BValue
BTrue
    GenParser st BValue -> GenParser st BValue -> GenParser st BValue
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> ParsecT Text st Identity SourceName
forall s (m :: * -> *) u.
Stream s m Char =>
SourceName -> ParsecT s u m SourceName
string "false" ParsecT Text st Identity SourceName
-> BValue -> GenParser st BValue
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> BValue
BFalse
    GenParser st BValue -> SourceName -> GenParser st BValue
forall s u (m :: * -> *) a.
ParsecT s u m a -> SourceName -> ParsecT s u m a
<?> "bool value"

scriptOption :: GenParser st ScriptOption
scriptOption :: GenParser st ScriptOption
scriptOption =
  Text -> ScriptOption
DiagnosticOutputChannel (Text -> ScriptOption)
-> ParsecT Text st Identity Text -> GenParser st ScriptOption
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SourceName
-> ParsecT Text st Identity Text -> ParsecT Text st Identity Text
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
opt "diagnostic-output-channel" ParsecT Text st Identity Text
forall st. GenParser st Text
stringLiteral
    GenParser st ScriptOption
-> GenParser st ScriptOption -> GenParser st ScriptOption
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> BValue -> ScriptOption
GlobalDeclarations (BValue -> ScriptOption)
-> ParsecT Text st Identity BValue -> GenParser st ScriptOption
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SourceName -> ParsecT Text st Identity BValue
forall st. SourceName -> ParsecT Text st Identity BValue
optB "global-declarations"
    GenParser st ScriptOption
-> GenParser st ScriptOption -> GenParser st ScriptOption
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> BValue -> ScriptOption
InteractiveMode (BValue -> ScriptOption)
-> ParsecT Text st Identity BValue -> GenParser st ScriptOption
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SourceName -> ParsecT Text st Identity BValue
forall st. SourceName -> ParsecT Text st Identity BValue
optB "interactive-mode"
    GenParser st ScriptOption
-> GenParser st ScriptOption -> GenParser st ScriptOption
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> BValue -> ScriptOption
PrintSuccess (BValue -> ScriptOption)
-> ParsecT Text st Identity BValue -> GenParser st ScriptOption
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SourceName -> ParsecT Text st Identity BValue
forall st. SourceName -> ParsecT Text st Identity BValue
optB "print-success"
    GenParser st ScriptOption
-> GenParser st ScriptOption -> GenParser st ScriptOption
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> BValue -> ScriptOption
ProduceAssertions (BValue -> ScriptOption)
-> ParsecT Text st Identity BValue -> GenParser st ScriptOption
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SourceName -> ParsecT Text st Identity BValue
forall st. SourceName -> ParsecT Text st Identity BValue
optB "produce-assertions"
    GenParser st ScriptOption
-> GenParser st ScriptOption -> GenParser st ScriptOption
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> BValue -> ScriptOption
ProduceAssignments (BValue -> ScriptOption)
-> ParsecT Text st Identity BValue -> GenParser st ScriptOption
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SourceName -> ParsecT Text st Identity BValue
forall st. SourceName -> ParsecT Text st Identity BValue
optB "produce-assignments"
    GenParser st ScriptOption
-> GenParser st ScriptOption -> GenParser st ScriptOption
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> BValue -> ScriptOption
ProduceModels (BValue -> ScriptOption)
-> ParsecT Text st Identity BValue -> GenParser st ScriptOption
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SourceName -> ParsecT Text st Identity BValue
forall st. SourceName -> ParsecT Text st Identity BValue
optB "produce-models"
    GenParser st ScriptOption
-> GenParser st ScriptOption -> GenParser st ScriptOption
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> BValue -> ScriptOption
ProduceProofs (BValue -> ScriptOption)
-> ParsecT Text st Identity BValue -> GenParser st ScriptOption
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SourceName -> ParsecT Text st Identity BValue
forall st. SourceName -> ParsecT Text st Identity BValue
optB "produce-proofs"
    GenParser st ScriptOption
-> GenParser st ScriptOption -> GenParser st ScriptOption
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> BValue -> ScriptOption
ProduceUnsatAssumptions (BValue -> ScriptOption)
-> ParsecT Text st Identity BValue -> GenParser st ScriptOption
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SourceName -> ParsecT Text st Identity BValue
forall st. SourceName -> ParsecT Text st Identity BValue
optB "produce-unsat-assumptions"
    GenParser st ScriptOption
-> GenParser st ScriptOption -> GenParser st ScriptOption
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> BValue -> ScriptOption
ProduceUnsatCores (BValue -> ScriptOption)
-> ParsecT Text st Identity BValue -> GenParser st ScriptOption
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SourceName -> ParsecT Text st Identity BValue
forall st. SourceName -> ParsecT Text st Identity BValue
optB "produce-unsat-cores"
    GenParser st ScriptOption
-> GenParser st ScriptOption -> GenParser st ScriptOption
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Text -> ScriptOption
RandomSeed (Text -> ScriptOption)
-> ParsecT Text st Identity Text -> GenParser st ScriptOption
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SourceName
-> ParsecT Text st Identity Text -> ParsecT Text st Identity Text
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
opt "random-seed" ParsecT Text st Identity Text
forall st. GenParser st Text
numeral
    GenParser st ScriptOption
-> GenParser st ScriptOption -> GenParser st ScriptOption
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Text -> ScriptOption
RegularOutputChannel (Text -> ScriptOption)
-> ParsecT Text st Identity Text -> GenParser st ScriptOption
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SourceName
-> ParsecT Text st Identity Text -> ParsecT Text st Identity Text
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
opt "regular-output-channel" ParsecT Text st Identity Text
forall st. GenParser st Text
stringLiteral
    GenParser st ScriptOption
-> GenParser st ScriptOption -> GenParser st ScriptOption
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Text -> ScriptOption
ReproducibleResourceLimit (Text -> ScriptOption)
-> ParsecT Text st Identity Text -> GenParser st ScriptOption
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SourceName
-> ParsecT Text st Identity Text -> ParsecT Text st Identity Text
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
opt "reproducible-resource-limit" ParsecT Text st Identity Text
forall st. GenParser st Text
numeral
    GenParser st ScriptOption
-> GenParser st ScriptOption -> GenParser st ScriptOption
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Text -> ScriptOption
Verbosity (Text -> ScriptOption)
-> ParsecT Text st Identity Text -> GenParser st ScriptOption
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SourceName
-> ParsecT Text st Identity Text -> ParsecT Text st Identity Text
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
opt "verbosity" ParsecT Text st Identity Text
forall st. GenParser st Text
numeral
    GenParser st ScriptOption
-> GenParser st ScriptOption -> GenParser st ScriptOption
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Attribute -> ScriptOption
OptionAttr (Attribute -> ScriptOption)
-> ParsecT Text st Identity Attribute -> GenParser st ScriptOption
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Attribute
forall st. GenParser st Attribute
attribute
    GenParser st ScriptOption
-> SourceName -> GenParser st ScriptOption
forall s u (m :: * -> *) a.
ParsecT s u m a -> SourceName -> ParsecT s u m a
<?> "script option"
  where
    opt :: SourceName
-> ParsecT Text st Identity b -> ParsecT Text st Identity b
opt s :: SourceName
s p :: ParsecT Text st Identity b
p = SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryAttr SourceName
s GenParser st () -> GenParser st () -> GenParser st ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> GenParser st ()
forall st. GenParser st ()
spaces1 GenParser st ()
-> ParsecT Text st Identity b -> ParsecT Text st Identity b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT Text st Identity b
p
    optB :: SourceName -> ParsecT Text st Identity BValue
optB s :: SourceName
s = SourceName
-> ParsecT Text st Identity BValue
-> ParsecT Text st Identity BValue
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
opt SourceName
s ParsecT Text st Identity BValue
forall st. GenParser st BValue
bValue

infoFlag :: GenParser st InfoFlag
infoFlag :: GenParser st InfoFlag
infoFlag =
  SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryAttr "all-statistics" GenParser st () -> InfoFlag -> GenParser st InfoFlag
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> InfoFlag
AllStatistics
    GenParser st InfoFlag
-> GenParser st InfoFlag -> GenParser st InfoFlag
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryAttr "assertion-stack-levels" GenParser st () -> InfoFlag -> GenParser st InfoFlag
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> InfoFlag
AssertionStackLevels
    GenParser st InfoFlag
-> GenParser st InfoFlag -> GenParser st InfoFlag
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryAttr "authors" GenParser st () -> InfoFlag -> GenParser st InfoFlag
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> InfoFlag
Authors
    GenParser st InfoFlag
-> GenParser st InfoFlag -> GenParser st InfoFlag
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryAttr "error-behavior" GenParser st () -> InfoFlag -> GenParser st InfoFlag
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> InfoFlag
ErrorBehavior
    GenParser st InfoFlag
-> GenParser st InfoFlag -> GenParser st InfoFlag
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryAttr "name" GenParser st () -> InfoFlag -> GenParser st InfoFlag
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> InfoFlag
Name
    GenParser st InfoFlag
-> GenParser st InfoFlag -> GenParser st InfoFlag
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryAttr "reason-unknown" GenParser st () -> InfoFlag -> GenParser st InfoFlag
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> InfoFlag
ReasonUnknown
    GenParser st InfoFlag
-> GenParser st InfoFlag -> GenParser st InfoFlag
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryAttr "version" GenParser st () -> InfoFlag -> GenParser st InfoFlag
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> InfoFlag
Version
    GenParser st InfoFlag
-> GenParser st InfoFlag -> GenParser st InfoFlag
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Text -> InfoFlag
IFKeyword (Text -> InfoFlag)
-> ParsecT Text st Identity Text -> GenParser st InfoFlag
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text
forall st. GenParser st Text
keyword
    GenParser st InfoFlag -> SourceName -> GenParser st InfoFlag
forall s u (m :: * -> *) a.
ParsecT s u m a -> SourceName -> ParsecT s u m a
<?> "info flag"

-- ** Responses (Sec 3.9.1)

genRes :: SpecificSuccessRes res => GenParser st (GeneralRes res)
genRes :: GenParser st (GeneralRes res)
genRes =
  SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryStr "success" GenParser st () -> GeneralRes res -> GenParser st (GeneralRes res)
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> GeneralRes res
forall res. GeneralRes res
ResSuccess
    GenParser st (GeneralRes res)
-> GenParser st (GeneralRes res) -> GenParser st (GeneralRes res)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> res -> GeneralRes res
forall res. res -> GeneralRes res
ResSpecific (res -> GeneralRes res)
-> ParsecT Text st Identity res -> GenParser st (GeneralRes res)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity res
forall s st. SpecificSuccessRes s => GenParser st s
specificSuccessRes
    GenParser st (GeneralRes res)
-> GenParser st (GeneralRes res) -> GenParser st (GeneralRes res)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryStr "unsupported" GenParser st () -> GeneralRes res -> GenParser st (GeneralRes res)
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> GeneralRes res
forall res. GeneralRes res
ResUnsupported
    GenParser st (GeneralRes res)
-> GenParser st (GeneralRes res) -> GenParser st (GeneralRes res)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Text -> GeneralRes res
forall res. Text -> GeneralRes res
ResError (Text -> GeneralRes res)
-> ParsecT Text st Identity Text -> GenParser st (GeneralRes res)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text -> ParsecT Text st Identity Text
forall st a. GenParser st a -> GenParser st a
betweenBrackets (SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryStr "error" GenParser st () -> GenParser st () -> GenParser st ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> GenParser st ()
forall st. GenParser st ()
spaces1 GenParser st ()
-> ParsecT Text st Identity Text -> ParsecT Text st Identity Text
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT Text st Identity Text
forall st. GenParser st Text
stringLiteral)

resErrorBehaviour :: GenParser st ResErrorBehavior
resErrorBehaviour :: GenParser st ResErrorBehavior
resErrorBehaviour =
  SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryStr "immediate-exit" GenParser st ()
-> ResErrorBehavior -> GenParser st ResErrorBehavior
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> ResErrorBehavior
ImmediateExit
    GenParser st ResErrorBehavior
-> GenParser st ResErrorBehavior -> GenParser st ResErrorBehavior
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryStr "continued-execution" GenParser st ()
-> ResErrorBehavior -> GenParser st ResErrorBehavior
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> ResErrorBehavior
ContinuedExecution
    GenParser st ResErrorBehavior
-> SourceName -> GenParser st ResErrorBehavior
forall s u (m :: * -> *) a.
ParsecT s u m a -> SourceName -> ParsecT s u m a
<?> "response error behavior"

resReasonUnknown :: GenParser st ResReasonUnknown
resReasonUnknown :: GenParser st ResReasonUnknown
resReasonUnknown =
  SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryStr "memout" GenParser st ()
-> ResReasonUnknown -> GenParser st ResReasonUnknown
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> ResReasonUnknown
Memout
    GenParser st ResReasonUnknown
-> GenParser st ResReasonUnknown -> GenParser st ResReasonUnknown
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryStr "incomplete" GenParser st ()
-> ResReasonUnknown -> GenParser st ResReasonUnknown
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> ResReasonUnknown
Incomplete
    GenParser st ResReasonUnknown
-> SourceName -> GenParser st ResReasonUnknown
forall s u (m :: * -> *) a.
ParsecT s u m a -> SourceName -> ParsecT s u m a
<?> "response reason unknown"

resModel :: GenParser st ResModel
resModel :: GenParser st ResModel
resModel =
  SourceName -> GenParser st ResModel -> GenParser st ResModel
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
def "define-fun" (FunctionDef -> ResModel
RMDefineFun (FunctionDef -> ResModel)
-> ParsecT Text st Identity FunctionDef -> GenParser st ResModel
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity FunctionDef
forall st. GenParser st FunctionDef
functionDef)
    GenParser st ResModel
-> GenParser st ResModel -> GenParser st ResModel
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st ResModel -> GenParser st ResModel
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
def "define-fun-rec" (FunctionDef -> ResModel
RMDefineFunRec (FunctionDef -> ResModel)
-> ParsecT Text st Identity FunctionDef -> GenParser st ResModel
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity FunctionDef
forall st. GenParser st FunctionDef
functionDef)
    GenParser st ResModel
-> GenParser st ResModel -> GenParser st ResModel
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st ResModel -> GenParser st ResModel
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
def "define-funs-rec" GenParser st ResModel
forall st. ParsecT Text st Identity ResModel
rMDefineFunsRec
  where
    def :: SourceName
-> ParsecT Text st Identity a -> ParsecT Text st Identity a
def s :: SourceName
s p :: ParsecT Text st Identity a
p = ParsecT Text st Identity a -> ParsecT Text st Identity a
forall st a. GenParser st a -> GenParser st a
betweenBrackets (ParsecT Text st Identity a -> ParsecT Text st Identity a)
-> ParsecT Text st Identity a -> ParsecT Text st Identity a
forall a b. (a -> b) -> a -> b
$ SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryStr SourceName
s GenParser st ()
-> ParsecT Text st Identity a -> ParsecT Text st Identity a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT Text st Identity a
p
    rMDefineFunsRec :: ParsecT Text st Identity ResModel
rMDefineFunsRec = do
      NonEmpty FunctionDec
fdcs <- GenParser st (NonEmpty FunctionDec)
-> GenParser st (NonEmpty FunctionDec)
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st (NonEmpty FunctionDec)
 -> GenParser st (NonEmpty FunctionDec))
-> GenParser st (NonEmpty FunctionDec)
-> GenParser st (NonEmpty FunctionDec)
forall a b. (a -> b) -> a -> b
$ GenParser st FunctionDec -> GenParser st (NonEmpty FunctionDec)
forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepSpace1 GenParser st FunctionDec
forall st. GenParser st FunctionDec
functionDec
      ParsecT Text st Identity ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces
      NonEmpty Term
ts <- GenParser st (NonEmpty Term) -> GenParser st (NonEmpty Term)
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st (NonEmpty Term) -> GenParser st (NonEmpty Term))
-> GenParser st (NonEmpty Term) -> GenParser st (NonEmpty Term)
forall a b. (a -> b) -> a -> b
$ GenParser st Term -> GenParser st (NonEmpty Term)
forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepSpace1 GenParser st Term
forall st. GenParser st Term
term
      if NonEmpty FunctionDec -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length NonEmpty FunctionDec
fdcs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== NonEmpty Term -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length NonEmpty Term
ts
        then ResModel -> ParsecT Text st Identity ResModel
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ResModel -> ParsecT Text st Identity ResModel)
-> ResModel -> ParsecT Text st Identity ResModel
forall a b. (a -> b) -> a -> b
$ NonEmpty FunctionDec -> NonEmpty Term -> ResModel
RMDefineFunsRec NonEmpty FunctionDec
fdcs NonEmpty Term
ts
        else SourceName -> ParsecT Text st Identity ResModel
forall s (m :: * -> *) t u a.
Stream s m t =>
SourceName -> ParsecT s u m a
unexpected "get-model response, declarations and terms should have same length"

instance SpecificSuccessRes ResModel where
  specificSuccessRes :: GenParser st ResModel
specificSuccessRes = GenParser st ResModel
forall st. ParsecT Text st Identity ResModel
resModel

tValuationPair :: GenParser st TValuationPair
tValuationPair :: GenParser st TValuationPair
tValuationPair = GenParser st TValuationPair -> GenParser st TValuationPair
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st TValuationPair -> GenParser st TValuationPair)
-> GenParser st TValuationPair -> GenParser st TValuationPair
forall a b. (a -> b) -> a -> b
$ do
  Text
s <- GenParser st Text
forall st. GenParser st Text
symbol GenParser st Text
-> ParsecT Text st Identity () -> GenParser st Text
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1
  BValue
b <- GenParser st BValue
forall st. GenParser st BValue
bValue
  TValuationPair -> GenParser st TValuationPair
forall (m :: * -> *) a. Monad m => a -> m a
return (Text
s, BValue
b)

resCheckSat :: GenParser st ResCheckSat
resCheckSat :: GenParser st ResCheckSat
resCheckSat =
  SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryStr "sat" GenParser st () -> ResCheckSat -> GenParser st ResCheckSat
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> ResCheckSat
Sat
    GenParser st ResCheckSat
-> GenParser st ResCheckSat -> GenParser st ResCheckSat
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryStr "unsat" GenParser st () -> ResCheckSat -> GenParser st ResCheckSat
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> ResCheckSat
Unsat
    GenParser st ResCheckSat
-> GenParser st ResCheckSat -> GenParser st ResCheckSat
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryStr "unknown" GenParser st () -> ResCheckSat -> GenParser st ResCheckSat
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> ResCheckSat
Unknown

instance SpecificSuccessRes ResCheckSat where
  specificSuccessRes :: GenParser st ResCheckSat
specificSuccessRes = GenParser st ResCheckSat
forall st. GenParser st ResCheckSat
resCheckSat

resInfo :: GenParser st ResInfo
resInfo :: GenParser st ResInfo
resInfo =
  ResErrorBehavior -> ResInfo
IRErrorBehaviour (ResErrorBehavior -> ResInfo)
-> ParsecT Text st Identity ResErrorBehavior
-> GenParser st ResInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryAttr "error-behavior" GenParser st ()
-> ParsecT Text st Identity ResErrorBehavior
-> ParsecT Text st Identity ResErrorBehavior
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT Text st Identity ResErrorBehavior
forall st. GenParser st ResErrorBehavior
resErrorBehaviour)
    GenParser st ResInfo
-> GenParser st ResInfo -> GenParser st ResInfo
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Text -> ResInfo
IRName (Text -> ResInfo)
-> ParsecT Text st Identity Text -> GenParser st ResInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryAttr "name" GenParser st ()
-> ParsecT Text st Identity Text -> ParsecT Text st Identity Text
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT Text st Identity Text
forall st. GenParser st Text
stringLiteral)
    GenParser st ResInfo
-> GenParser st ResInfo -> GenParser st ResInfo
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Text -> ResInfo
IRAuthours (Text -> ResInfo)
-> ParsecT Text st Identity Text -> GenParser st ResInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryAttr "authors" GenParser st ()
-> ParsecT Text st Identity Text -> ParsecT Text st Identity Text
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT Text st Identity Text
forall st. GenParser st Text
stringLiteral)
    GenParser st ResInfo
-> GenParser st ResInfo -> GenParser st ResInfo
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Text -> ResInfo
IRVersion (Text -> ResInfo)
-> ParsecT Text st Identity Text -> GenParser st ResInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryAttr "version" GenParser st ()
-> ParsecT Text st Identity Text -> ParsecT Text st Identity Text
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT Text st Identity Text
forall st. GenParser st Text
stringLiteral)
    GenParser st ResInfo
-> GenParser st ResInfo -> GenParser st ResInfo
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ResReasonUnknown -> ResInfo
IRReasonUnknown (ResReasonUnknown -> ResInfo)
-> ParsecT Text st Identity ResReasonUnknown
-> GenParser st ResInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryAttr "reason-unknown" GenParser st ()
-> ParsecT Text st Identity ResReasonUnknown
-> ParsecT Text st Identity ResReasonUnknown
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT Text st Identity ResReasonUnknown
forall st. GenParser st ResReasonUnknown
resReasonUnknown)
    GenParser st ResInfo
-> GenParser st ResInfo -> GenParser st ResInfo
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Attribute -> ResInfo
IRAttr (Attribute -> ResInfo)
-> ParsecT Text st Identity Attribute -> GenParser st ResInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Attribute
forall st. GenParser st Attribute
attribute

instance SpecificSuccessRes (NonEmpty ResInfo) where
  specificSuccessRes :: GenParser st (NonEmpty ResInfo)
specificSuccessRes = GenParser st (NonEmpty ResInfo) -> GenParser st (NonEmpty ResInfo)
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st (NonEmpty ResInfo)
 -> GenParser st (NonEmpty ResInfo))
-> GenParser st (NonEmpty ResInfo)
-> GenParser st (NonEmpty ResInfo)
forall a b. (a -> b) -> a -> b
$ GenParser st ResInfo -> GenParser st (NonEmpty ResInfo)
forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepSpace1 GenParser st ResInfo
forall st. GenParser st ResInfo
resInfo

-- *** instances

checkSatRes :: GenParser st CheckSatRes
checkSatRes :: GenParser st CheckSatRes
checkSatRes = GenParser st CheckSatRes
forall res st.
SpecificSuccessRes res =>
GenParser st (GeneralRes res)
genRes

instance SpecificSuccessRes StringLiteral where
  specificSuccessRes :: GenParser st Text
specificSuccessRes = GenParser st Text
forall st. GenParser st Text
stringLiteral

echoRes :: GenParser st EchoRes
echoRes :: GenParser st EchoRes
echoRes = GenParser st EchoRes
forall res st.
SpecificSuccessRes res =>
GenParser st (GeneralRes res)
genRes

instance SpecificSuccessRes [Term] where
  specificSuccessRes :: GenParser st [Term]
specificSuccessRes = GenParser st [Term] -> GenParser st [Term]
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st [Term] -> GenParser st [Term])
-> GenParser st [Term] -> GenParser st [Term]
forall a b. (a -> b) -> a -> b
$ GenParser st Term -> GenParser st [Term]
forall st a. GenParser st a -> GenParser st [a]
sepSpace GenParser st Term
forall st. GenParser st Term
term

getAssertionsRes :: GenParser st GetAssertionsRes
getAssertionsRes :: GenParser st GetAssertionsRes
getAssertionsRes = GenParser st GetAssertionsRes
forall res st.
SpecificSuccessRes res =>
GenParser st (GeneralRes res)
genRes

instance SpecificSuccessRes [TValuationPair] where
  specificSuccessRes :: GenParser st [TValuationPair]
specificSuccessRes = GenParser st [TValuationPair] -> GenParser st [TValuationPair]
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st [TValuationPair] -> GenParser st [TValuationPair])
-> GenParser st [TValuationPair] -> GenParser st [TValuationPair]
forall a b. (a -> b) -> a -> b
$ GenParser st TValuationPair -> GenParser st [TValuationPair]
forall st a. GenParser st a -> GenParser st [a]
sepSpace GenParser st TValuationPair
forall st. GenParser st TValuationPair
tValuationPair

getAssignmentRes :: GenParser st GetAssignmentRes
getAssignmentRes :: GenParser st GetAssignmentRes
getAssignmentRes = GenParser st GetAssignmentRes
forall res st.
SpecificSuccessRes res =>
GenParser st (GeneralRes res)
genRes

getInfoRes :: GenParser st GetInfoRes
getInfoRes :: GenParser st GetInfoRes
getInfoRes = GenParser st GetInfoRes
forall res st.
SpecificSuccessRes res =>
GenParser st (GeneralRes res)
genRes

getModelRes :: GenParser st GetModelRes
getModelRes :: GenParser st GetModelRes
getModelRes = GenParser st GetModelRes
forall res st.
SpecificSuccessRes res =>
GenParser st (GeneralRes res)
genRes

instance SpecificSuccessRes AttributeValue where
  specificSuccessRes :: GenParser st AttributeValue
specificSuccessRes = GenParser st AttributeValue
forall st. GenParser st AttributeValue
attributeValue

getOptionRes :: GenParser st GetOptionRes
getOptionRes :: GenParser st GetOptionRes
getOptionRes = GenParser st GetOptionRes
forall res st.
SpecificSuccessRes res =>
GenParser st (GeneralRes res)
genRes

instance SpecificSuccessRes SExpr where
  specificSuccessRes :: GenParser st SExpr
specificSuccessRes = GenParser st SExpr
forall st. GenParser st SExpr
sexpr

getProofRes :: GenParser st GetProofRes
getProofRes :: GenParser st GetProofRes
getProofRes = GenParser st GetProofRes
forall res st.
SpecificSuccessRes res =>
GenParser st (GeneralRes res)
genRes

instance SpecificSuccessRes [Symbol] where
  specificSuccessRes :: GenParser st [Text]
specificSuccessRes = GenParser st [Text] -> GenParser st [Text]
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st [Text] -> GenParser st [Text])
-> GenParser st [Text] -> GenParser st [Text]
forall a b. (a -> b) -> a -> b
$ GenParser st Text -> GenParser st [Text]
forall st a. GenParser st a -> GenParser st [a]
sepSpace GenParser st Text
forall st. GenParser st Text
symbol

getUnsatAssumpRes :: GenParser st GetUnsatAssumpRes
getUnsatAssumpRes :: GenParser st GetUnsatAssumpRes
getUnsatAssumpRes = GenParser st GetUnsatAssumpRes
forall res st.
SpecificSuccessRes res =>
GenParser st (GeneralRes res)
genRes

getUnsatCoreRes :: GenParser st GetUnsatCoreRes
getUnsatCoreRes :: GenParser st GetUnsatAssumpRes
getUnsatCoreRes = GenParser st GetUnsatAssumpRes
forall res st.
SpecificSuccessRes res =>
GenParser st (GeneralRes res)
genRes

valuationPair :: GenParser st ValuationPair
valuationPair :: GenParser st ValuationPair
valuationPair = GenParser st ValuationPair -> GenParser st ValuationPair
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st ValuationPair -> GenParser st ValuationPair)
-> GenParser st ValuationPair -> GenParser st ValuationPair
forall a b. (a -> b) -> a -> b
$ do
  Term
t1 <- GenParser st Term
forall st. GenParser st Term
term GenParser st Term
-> ParsecT Text st Identity () -> GenParser st Term
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1
  Term
t2 <- GenParser st Term
forall st. GenParser st Term
term
  ValuationPair -> GenParser st ValuationPair
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
t1, Term
t2)

instance SpecificSuccessRes (NonEmpty ValuationPair) where
  specificSuccessRes :: GenParser st (NonEmpty ValuationPair)
specificSuccessRes = GenParser st (NonEmpty ValuationPair)
-> GenParser st (NonEmpty ValuationPair)
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st (NonEmpty ValuationPair)
 -> GenParser st (NonEmpty ValuationPair))
-> GenParser st (NonEmpty ValuationPair)
-> GenParser st (NonEmpty ValuationPair)
forall a b. (a -> b) -> a -> b
$ GenParser st ValuationPair -> GenParser st (NonEmpty ValuationPair)
forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepSpace1 GenParser st ValuationPair
forall st. GenParser st ValuationPair
valuationPair

getValueRes :: GenParser st GetValueRes
getValueRes :: GenParser st GetValueRes
getValueRes = GenParser st GetValueRes
forall res st.
SpecificSuccessRes res =>
GenParser st (GeneralRes res)
genRes