{-# 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 :: forall a. Parser a -> Text -> Either ParseError a
parseString Parser a
p = forall s t a.
Stream s Identity t =>
Parsec s () a -> SourceName -> s -> Either ParseError a
parse Parser a
p SourceName
""

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

-- | parse from a file string, may have leading & trailing spaces and comments
parseFileMsg :: Parser a -> T.Text -> Either T.Text a
parseFileMsg :: forall a. Parser a -> Text -> Either Text a
parseFileMsg Parser a
p = forall a. Parser a -> Text -> Either Text a
parseCommentFreeFileMsg Parser a
p 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 :: forall a. Parser a -> Text -> Either Text a
parseCommentFreeFileMsg Parser a
p = forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (SourceName -> Text
T.pack forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> SourceName
show) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Parser a -> Text -> Either ParseError a
parseStringEof (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 :: forall st. SourceName -> GenParser st Text
text = (SourceName -> Text
T.pack forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s (m :: * -> *) u.
Stream s m Char =>
SourceName -> ParsecT s u m SourceName
string

-- | skip one or more @spaces@
spaces1 :: GenParser st ()
spaces1 :: forall st. GenParser st ()
spaces1 = forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m ()
skipMany1 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 :: forall st a. GenParser st a -> GenParser st a
betweenBrackets = forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 (forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char Char
'(' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces) (forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char Char
')')

-- | @many p@, separated by @spaces1@, possibly has a trailing @spaces1@
sepSpace :: GenParser st a -> GenParser st [a]
sepSpace :: forall st a. GenParser st a -> GenParser st [a]
sepSpace GenParser st a
p = 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 forall st. GenParser st ()
spaces1

-- | @many1 p@, separated by @spaces1@, possibly has a trailing @spaces1@
sepSpace1 :: GenParser st a -> GenParser st (NonEmpty a)
sepSpace1 :: forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepSpace1 GenParser st a
p = forall a. [a] -> NonEmpty a
fromList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 forall st. GenParser st ()
spaces1

-- | @many p@, separated by @spaces@, possibly has a trailing @spaces@
sepOptSpace :: GenParser st a -> GenParser st [a]
sepOptSpace :: forall st a. GenParser st a -> GenParser st [a]
sepOptSpace GenParser st a
p = 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 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 :: forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepOptSpace1 GenParser st a
p = forall a. [a] -> NonEmpty a
fromList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 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 :: forall st. SourceName -> GenParser st ()
tryStr SourceName
s = forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try forall a b. (a -> b) -> a -> b
$ forall s (m :: * -> *) u.
Stream s m Char =>
SourceName -> ParsecT s u m SourceName
string SourceName
s forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces 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 :: forall st. SourceName -> GenParser st ()
tryStr1 SourceName
s = forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try forall a b. (a -> b) -> a -> b
$ forall s (m :: * -> *) u.
Stream s m Char =>
SourceName -> ParsecT s u m SourceName
string SourceName
s forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall st. GenParser st ()
spaces1 forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> ()

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

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

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

-- | strip away the leading and trailing @spaces@
stripSpaces :: GenParser st a -> GenParser st a
stripSpaces :: forall st a. GenParser st a -> GenParser st a
stripSpaces GenParser st a
p = forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> GenParser st a
p forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* 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 Text
acc Text
rest =
      if Text -> Bool
T.null Text
rest
        then Text
acc
        else
          let (Char
c, Text
cs) = (Text -> Char
T.head Text
rest, Text -> Text
T.tail Text
rest)
              f :: Text -> Text -> Text
f = case Char
c of
                Char
'"' -> SourceName -> (Text -> Text) -> Text -> Text -> Text
capture SourceName
"\"" (Char -> Text -> Text
T.cons Char
'"')
                Char
'|' -> SourceName -> (Text -> Text) -> Text -> Text -> Text
capture SourceName
"|" (Char -> Text -> Text
T.cons Char
'|')
                Char
';' -> SourceName -> (Text -> Text) -> Text -> Text -> Text
capture SourceName
"\n\r" (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ Char -> Text
T.singleton Char
' ')
                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 SourceName
stops Text -> Text
after Text
acc Text
cs =
      let (Text
captured, Text
rest) = (Char -> Bool) -> Text -> (Text, Text)
T.break (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 forall a. Semigroup a => a -> a -> a
<> Text -> Text
after Text
captured
            else
              let (Char
s, Text
ss) = (Text -> Char
T.head Text
rest, Text -> Text
T.tail Text
rest)
               in Text -> Text -> Text
rc (Text
acc forall a. Semigroup a => a -> a -> a
<> Text -> Text
after Text
captured 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 Char
x 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 :: forall st. GenParser st Text
numeral =
  forall st. SourceName -> GenParser st Text
text SourceName
"0"
    forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
      Char
c <- forall s (m :: * -> *) u.
Stream s m Char =>
SourceName -> ParsecT s u m Char
oneOf SourceName
"123456789"
      SourceName
cs <- forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
digit
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ SourceName -> Text
T.pack (Char
c forall a. a -> [a] -> [a]
: SourceName
cs)

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

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

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

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

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

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

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

-- |  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 :: forall st. GenParser st Text
symbol = forall s (m :: * -> *) t a u.
(Stream s m t, Show a) =>
ParsecT s u m a -> ParsecT s u m ()
notFollowedBy (forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try forall st. GenParser st Text
reservedWord) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (forall st. GenParser st Text
quotedSymbol forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> forall st. GenParser st Text
simpleSymbol forall s u (m :: * -> *) a.
ParsecT s u m a -> SourceName -> ParsecT s u m a
<?> SourceName
"symbol")
  where
    simpleSymbol :: ParsecT Text u Identity Text
simpleSymbol = do
      Char
c <- forall {u}. ParsecT Text u Identity Char
nameChar forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
letter
      SourceName
cs <- forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many (forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
alphaNum forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> forall {u}. ParsecT Text u Identity Char
nameChar)
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ SourceName -> Text
T.pack (Char
c forall a. a -> [a] -> [a]
: SourceName
cs)
    quotedSymbol :: ParsecT Text u Identity Text
quotedSymbol = 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 (forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char Char
'|') (forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char Char
'|') forall a b. (a -> b) -> a -> b
$ SourceName -> Text
T.pack forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many (forall s (m :: * -> *) u.
Stream s m Char =>
SourceName -> ParsecT s u m Char
noneOf SourceName
"\\|")

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

-- * S-expressions (Sec. 3.2)

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

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

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

-- * Identifiers (Sec 3.3)

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

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

-- * Attributes (Sec. 3.4)

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

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

-- * Sorts (Sec 3.5)

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

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

-- * Terms and Formulas (Sec 3.6)

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

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

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

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

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

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

-- * Theory declarations (Sec 3.7)

sortSymbolDecl :: GenParser st SortSymbolDecl
sortSymbolDecl :: forall st. GenParser st SortSymbolDecl
sortSymbolDecl = forall st a. GenParser st a -> GenParser st a
betweenBrackets forall a b. (a -> b) -> a -> b
$ do
  Identifier
i <- forall st. GenParser st Identifier
identifier forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* forall st. GenParser st ()
spaces1
  Text
n <- forall st. GenParser st Text
numeral forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall st a. GenParser st a -> GenParser st [a]
sepSpace forall st. GenParser st Attribute
attribute

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

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

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

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

-- * Logic Declarations (Sec 3.8)

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

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

-- * Scripts (Sec 3.9)

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

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

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

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

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

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

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

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

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

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

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

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

-- ** Responses (Sec 3.9.1)

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

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

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

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

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

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

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

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

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

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

-- *** instances

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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