{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverloadedStrings #-}
module Language.SMT2.Parser
(
parseString,
parseStringEof,
parseFileMsg,
parseCommentFreeFileMsg,
stripSpaces,
removeComment,
numeral,
decimal,
hexadecimal,
binary,
stringLiteral,
reservedWord,
symbol,
keyword,
slist,
specConstant,
sexpr,
index,
identifier,
attributeValue,
attribute,
sort,
qualIdentifier,
varBinding,
sortedVar,
matchPattern,
matchCase,
term,
sortSymbolDecl,
metaSpecConstant,
funSymbolDecl,
parFunSymbolDecl,
theoryAttribute,
theoryDecl,
logicAttribute,
logic,
sortDec,
selectorDec,
constructorDec,
datatypeDec,
functionDec,
functionDef,
propLiteral,
command,
script,
bValue,
scriptOption,
infoFlag,
resErrorBehaviour,
resReasonUnknown,
resModel,
resInfo,
valuationPair,
tValuationPair,
resCheckSat,
checkSatRes,
echoRes,
getAssertionsRes,
getAssignmentRes,
getInfoRes,
getModelRes,
getOptionRes,
getProofRes,
getUnsatAssumpRes,
getUnsatCoreRes,
getValueRes,
)
where
import Data.Bifunctor (first)
import Data.Char (toLower)
import Data.Functor (($>))
import Data.List.NonEmpty (NonEmpty, fromList)
import qualified Data.Text as T
import Language.SMT2.Syntax
import Text.Parsec (ParseError, parse, try)
import Text.Parsec.Char
import Text.Parsec.Combinator
import Text.Parsec.Prim (many, unexpected, (<?>), (<|>))
import Text.Parsec.Text (GenParser, Parser)
parseString :: Parser a -> T.Text -> Either ParseError a
parseString :: Parser a -> Text -> Either ParseError a
parseString p :: Parser a
p = Parser a -> SourceName -> Text -> Either ParseError a
forall s t a.
Stream s Identity t =>
Parsec s () a -> SourceName -> s -> Either ParseError a
parse Parser a
p ""
parseStringEof :: Parser a -> T.Text -> Either ParseError a
parseStringEof :: Parser a -> Text -> Either ParseError a
parseStringEof p :: Parser a
p = Parser a -> SourceName -> Text -> Either ParseError a
forall s t a.
Stream s Identity t =>
Parsec s () a -> SourceName -> s -> Either ParseError a
parse (Parser a
p Parser a -> ParsecT Text () Identity () -> Parser a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text () Identity ()
forall s (m :: * -> *) t u.
(Stream s m t, Show t) =>
ParsecT s u m ()
eof) ""
parseFileMsg :: Parser a -> T.Text -> Either T.Text a
parseFileMsg :: Parser a -> Text -> Either Text a
parseFileMsg p :: Parser a
p = Parser a -> Text -> Either Text a
forall a. Parser a -> Text -> Either Text a
parseCommentFreeFileMsg Parser a
p (Text -> Either Text a) -> (Text -> Text) -> Text -> Either Text a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Text
removeComment
parseCommentFreeFileMsg :: Parser a -> T.Text -> Either T.Text a
p :: Parser a
p = (ParseError -> Text) -> Either ParseError a -> Either Text a
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (SourceName -> Text
T.pack (SourceName -> Text)
-> (ParseError -> SourceName) -> ParseError -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ParseError -> SourceName
forall a. Show a => a -> SourceName
show) (Either ParseError a -> Either Text a)
-> (Text -> Either ParseError a) -> Text -> Either Text a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Parser a -> Text -> Either ParseError a
forall a. Parser a -> Text -> Either ParseError a
parseStringEof (Parser a -> Parser a
forall st a. GenParser st a -> GenParser st a
stripSpaces Parser a
p)
text :: String -> GenParser st T.Text
text :: SourceName -> GenParser st Text
text = (SourceName -> Text
T.pack (SourceName -> Text)
-> ParsecT Text st Identity SourceName -> GenParser st Text
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) (ParsecT Text st Identity SourceName -> GenParser st Text)
-> (SourceName -> ParsecT Text st Identity SourceName)
-> SourceName
-> GenParser st Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourceName -> ParsecT Text st Identity SourceName
forall s (m :: * -> *) u.
Stream s m Char =>
SourceName -> ParsecT s u m SourceName
string
spaces1 :: GenParser st ()
spaces1 :: GenParser st ()
spaces1 = ParsecT Text st Identity Char -> GenParser st ()
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m ()
skipMany1 ParsecT Text st Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
space
betweenBrackets :: GenParser st a -> GenParser st a
betweenBrackets :: GenParser st a -> GenParser st a
betweenBrackets = GenParser st a -> GenParser st a
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try (GenParser st a -> GenParser st a)
-> (GenParser st a -> GenParser st a)
-> GenParser st a
-> GenParser st a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ParsecT Text st Identity Char
-> ParsecT Text st Identity Char
-> GenParser st a
-> GenParser st a
forall s (m :: * -> *) t u open close a.
Stream s m t =>
ParsecT s u m open
-> ParsecT s u m close -> ParsecT s u m a -> ParsecT s u m a
between (Char -> ParsecT Text st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '(' ParsecT Text st Identity Char
-> ParsecT Text st Identity () -> ParsecT Text st Identity Char
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces) (ParsecT Text st Identity ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces ParsecT Text st Identity ()
-> ParsecT Text st Identity Char -> ParsecT Text st Identity Char
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Char -> ParsecT Text st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char ')')
sepSpace :: GenParser st a -> GenParser st [a]
sepSpace :: GenParser st a -> GenParser st [a]
sepSpace p :: GenParser st a
p = GenParser st a -> ParsecT Text st Identity () -> GenParser st [a]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepEndBy GenParser st a
p ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1
sepSpace1 :: GenParser st a -> GenParser st (NonEmpty a)
sepSpace1 :: GenParser st a -> GenParser st (NonEmpty a)
sepSpace1 p :: GenParser st a
p = [a] -> NonEmpty a
forall a. [a] -> NonEmpty a
fromList ([a] -> NonEmpty a)
-> ParsecT Text st Identity [a] -> GenParser st (NonEmpty a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenParser st a
-> ParsecT Text st Identity () -> ParsecT Text st Identity [a]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepEndBy1 GenParser st a
p ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1
sepOptSpace :: GenParser st a -> GenParser st [a]
sepOptSpace :: GenParser st a -> GenParser st [a]
sepOptSpace p :: GenParser st a
p = GenParser st a -> ParsecT Text st Identity () -> GenParser st [a]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepEndBy GenParser st a
p ParsecT Text st Identity ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces
sepOptSpace1 :: GenParser st a -> GenParser st (NonEmpty a)
sepOptSpace1 :: GenParser st a -> GenParser st (NonEmpty a)
sepOptSpace1 p :: GenParser st a
p = [a] -> NonEmpty a
forall a. [a] -> NonEmpty a
fromList ([a] -> NonEmpty a)
-> ParsecT Text st Identity [a] -> GenParser st (NonEmpty a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenParser st a
-> ParsecT Text st Identity () -> ParsecT Text st Identity [a]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepEndBy1 GenParser st a
p ParsecT Text st Identity ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces
tryStr :: String -> GenParser st ()
tryStr :: SourceName -> GenParser st ()
tryStr s :: SourceName
s = GenParser st () -> GenParser st ()
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try (GenParser st () -> GenParser st ())
-> GenParser st () -> GenParser st ()
forall a b. (a -> b) -> a -> b
$ SourceName -> ParsecT Text st Identity SourceName
forall s (m :: * -> *) u.
Stream s m Char =>
SourceName -> ParsecT s u m SourceName
string SourceName
s ParsecT Text st Identity SourceName
-> GenParser st () -> GenParser st ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> GenParser st ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces GenParser st () -> () -> GenParser st ()
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> ()
tryStr1 :: String -> GenParser st ()
tryStr1 :: SourceName -> GenParser st ()
tryStr1 s :: SourceName
s = GenParser st () -> GenParser st ()
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try (GenParser st () -> GenParser st ())
-> GenParser st () -> GenParser st ()
forall a b. (a -> b) -> a -> b
$ SourceName -> ParsecT Text st Identity SourceName
forall s (m :: * -> *) u.
Stream s m Char =>
SourceName -> ParsecT s u m SourceName
string SourceName
s ParsecT Text st Identity SourceName
-> GenParser st () -> GenParser st ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> GenParser st ()
forall st. GenParser st ()
spaces1 GenParser st () -> () -> GenParser st ()
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> ()
tryStrBraket :: String -> GenParser st ()
tryStrBraket :: SourceName -> GenParser st ()
tryStrBraket s :: SourceName
s = GenParser st () -> GenParser st ()
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try (GenParser st () -> GenParser st ())
-> GenParser st () -> GenParser st ()
forall a b. (a -> b) -> a -> b
$ SourceName -> ParsecT Text st Identity SourceName
forall s (m :: * -> *) u.
Stream s m Char =>
SourceName -> ParsecT s u m SourceName
string SourceName
s ParsecT Text st Identity SourceName
-> GenParser st () -> GenParser st ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (GenParser st ()
forall st. GenParser st ()
spaces1 GenParser st () -> GenParser st () -> GenParser st ()
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> GenParser st ()
forall st. GenParser st ()
lookLeftBraket) GenParser st () -> () -> GenParser st ()
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> ()
where
lookLeftBraket :: ParsecT Text u Identity ()
lookLeftBraket = ParsecT Text u Identity () -> ParsecT Text u Identity ()
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try (ParsecT Text u Identity () -> ParsecT Text u Identity ())
-> ParsecT Text u Identity () -> ParsecT Text u Identity ()
forall a b. (a -> b) -> a -> b
$ ParsecT Text u Identity Char -> ParsecT Text u Identity Char
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m a
lookAhead (Char -> ParsecT Text u Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '(') ParsecT Text u Identity Char -> () -> ParsecT Text u Identity ()
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> ()
tryAttr :: String -> GenParser st ()
tryAttr :: SourceName -> GenParser st ()
tryAttr s :: SourceName
s = SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryStr (':' Char -> SourceName -> SourceName
forall a. a -> [a] -> [a]
: SourceName
s)
tryAttr1 :: String -> GenParser st ()
tryAttr1 :: SourceName -> GenParser st ()
tryAttr1 s :: SourceName
s = SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryStr1 (':' Char -> SourceName -> SourceName
forall a. a -> [a] -> [a]
: SourceName
s)
stripSpaces :: GenParser st a -> GenParser st a
stripSpaces :: GenParser st a -> GenParser st a
stripSpaces p :: GenParser st a
p = ParsecT Text st Identity ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces ParsecT Text st Identity () -> GenParser st a -> GenParser st a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> GenParser st a
p GenParser st a -> ParsecT Text st Identity () -> GenParser st a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces
removeComment :: T.Text -> T.Text
= Text -> Text -> Text
rc Text
T.empty
where
rc :: T.Text -> T.Text -> T.Text
rc :: Text -> Text -> Text
rc acc :: Text
acc rest :: Text
rest =
if Text -> Bool
T.null Text
rest
then Text
acc
else
let (c :: Char
c, cs :: Text
cs) = (Text -> Char
T.head Text
rest, Text -> Text
T.tail Text
rest)
f :: Text -> Text -> Text
f = case Char
c of
'"' -> SourceName -> (Text -> Text) -> Text -> Text -> Text
capture "\"" (Char -> Text -> Text
T.cons '"')
'|' -> SourceName -> (Text -> Text) -> Text -> Text -> Text
capture "|" (Char -> Text -> Text
T.cons '|')
';' -> SourceName -> (Text -> Text) -> Text -> Text -> Text
capture "\n\r" (Text -> Text -> Text
forall a b. a -> b -> a
const (Text -> Text -> Text) -> Text -> Text -> Text
forall a b. (a -> b) -> a -> b
$ Char -> Text
T.singleton ' ')
x :: Char
x -> Char -> Text -> Text -> Text
nextPos Char
x
in Text -> Text -> Text
f Text
acc Text
cs
capture :: String -> (T.Text -> T.Text) -> T.Text -> T.Text -> T.Text
capture :: SourceName -> (Text -> Text) -> Text -> Text -> Text
capture stops :: SourceName
stops after :: Text -> Text
after acc :: Text
acc cs :: Text
cs =
let (captured :: Text
captured, rest :: Text
rest) = (Char -> Bool) -> Text -> (Text, Text)
T.break (Char -> SourceName -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` SourceName
stops) Text
cs
in if Text -> Bool
T.null Text
rest
then Text
acc Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text -> Text
after Text
captured
else
let (s :: Char
s, ss :: Text
ss) = (Text -> Char
T.head Text
rest, Text -> Text
T.tail Text
rest)
in Text -> Text -> Text
rc (Text
acc Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text -> Text
after Text
captured Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Char -> Text
T.singleton Char
s) Text
ss
nextPos :: Char -> Text -> Text -> Text
nextPos x :: Char
x acc :: Text
acc = Text -> Text -> Text
rc (Text
acc Text -> Char -> Text
`T.snoc` Char
x)
numeral :: GenParser st Numeral
numeral :: GenParser st Text
numeral =
SourceName -> GenParser st Text
forall st. SourceName -> GenParser st Text
text "0"
GenParser st Text -> GenParser st Text -> GenParser st Text
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
Char
c <- SourceName -> ParsecT Text st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
SourceName -> ParsecT s u m Char
oneOf "123456789"
SourceName
cs <- ParsecT Text st Identity Char
-> ParsecT Text st Identity SourceName
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many ParsecT Text st Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
digit
Text -> GenParser st Text
forall (m :: * -> *) a. Monad m => a -> m a
return (Text -> GenParser st Text) -> Text -> GenParser st Text
forall a b. (a -> b) -> a -> b
$ SourceName -> Text
T.pack (Char
c Char -> SourceName -> SourceName
forall a. a -> [a] -> [a]
: SourceName
cs)
decimal :: GenParser st Decimal
decimal :: GenParser st Text
decimal = do
Text
whole <- GenParser st Text
forall st. GenParser st Text
numeral
Char -> ParsecT Text st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '.'
SourceName
zeros <- ParsecT Text st Identity Char
-> ParsecT Text st Identity SourceName
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many (Char -> ParsecT Text st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '0')
Text
restFractional <- Text -> GenParser st Text -> GenParser st Text
forall s (m :: * -> *) t a u.
Stream s m t =>
a -> ParsecT s u m a -> ParsecT s u m a
option "" GenParser st Text
forall st. GenParser st Text
numeral
Text -> GenParser st Text
forall (m :: * -> *) a. Monad m => a -> m a
return (Text -> GenParser st Text) -> Text -> GenParser st Text
forall a b. (a -> b) -> a -> b
$ Text
whole Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Char -> Text
T.singleton '.' Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> SourceName -> Text
T.pack SourceName
zeros Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
restFractional
hexadecimal :: GenParser st Hexadecimal
hexadecimal :: GenParser st Text
hexadecimal = SourceName -> GenParser st Text
forall st. SourceName -> GenParser st Text
text "#x" GenParser st Text -> GenParser st Text -> GenParser st Text
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SourceName -> Text
T.pack (SourceName -> Text)
-> (SourceName -> SourceName) -> SourceName -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Char) -> SourceName -> SourceName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Char -> Char
toLower (SourceName -> Text)
-> ParsecT Text st Identity SourceName -> GenParser st Text
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Char
-> ParsecT Text st Identity SourceName
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 ParsecT Text st Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
hexDigit
binary :: GenParser st Binary
binary :: GenParser st Text
binary = SourceName -> GenParser st Text
forall st. SourceName -> GenParser st Text
text "#b" GenParser st Text -> GenParser st Text -> GenParser st Text
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SourceName -> Text
T.pack (SourceName -> Text)
-> ParsecT Text st Identity SourceName -> GenParser st Text
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Char
-> ParsecT Text st Identity SourceName
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 (Char -> ParsecT Text st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '0' ParsecT Text st Identity Char
-> ParsecT Text st Identity Char -> ParsecT Text st Identity Char
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Char -> ParsecT Text st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '1')
stringLiteral :: GenParser st StringLiteral
stringLiteral :: GenParser st Text
stringLiteral = do
Char -> ParsecT Text st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '"'
SourceName
str <- ParsecT Text st Identity Char
-> ParsecT Text st Identity SourceName
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many (ParsecT Text st Identity Char
forall u. ParsecT Text u Identity Char
nonEscaped ParsecT Text st Identity Char
-> ParsecT Text st Identity Char -> ParsecT Text st Identity Char
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT Text st Identity Char
forall u. ParsecT Text u Identity Char
escaped)
Char -> ParsecT Text st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '"'
Text -> GenParser st Text
forall (m :: * -> *) a. Monad m => a -> m a
return (Text -> GenParser st Text) -> Text -> GenParser st Text
forall a b. (a -> b) -> a -> b
$ SourceName -> Text
T.pack SourceName
str
where
nonEscaped :: ParsecT Text u Identity Char
nonEscaped = SourceName -> ParsecT Text u Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
SourceName -> ParsecT s u m Char
noneOf "\""
escaped :: ParsecT Text u Identity Char
escaped = ParsecT Text u Identity SourceName
-> ParsecT Text u Identity SourceName
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try (SourceName -> ParsecT Text u Identity SourceName
forall s (m :: * -> *) u.
Stream s m Char =>
SourceName -> ParsecT s u m SourceName
string "\"\"") ParsecT Text u Identity SourceName
-> Char -> ParsecT Text u Identity Char
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> '"'
reservedWords :: [String]
reservedWords :: [SourceName]
reservedWords =
[
"!",
"_",
"as",
"DECIMAL",
"exists",
"forall",
"let",
"NUMERAL",
"par",
"STRING",
"assert",
"check-sat",
"declare-sort",
"declare-fun",
"define-sort",
"define-fun",
"exit",
"get-assertions",
"get-assignment",
"get-info",
"get-option",
"get-proof",
"get-unsat-core",
"get-value",
"pop",
"push",
"set-logic",
"set-info",
"set-option"
]
reservedWord :: GenParser st ReservedWord
reservedWord :: GenParser st Text
reservedWord = [GenParser st Text] -> GenParser st Text
forall s (m :: * -> *) t u a.
Stream s m t =>
[ParsecT s u m a] -> ParsecT s u m a
choice (SourceName -> GenParser st Text
forall st. SourceName -> GenParser st Text
parseWord (SourceName -> GenParser st Text)
-> [SourceName] -> [GenParser st Text]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SourceName]
reservedWords)
where
parseWord :: String -> GenParser st ReservedWord
parseWord :: SourceName -> GenParser st Text
parseWord w :: SourceName
w = GenParser st Text -> GenParser st Text
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try (SourceName -> GenParser st Text
forall st. SourceName -> GenParser st Text
text SourceName
w) GenParser st Text
-> ParsecT Text st Identity () -> GenParser st Text
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity Char -> ParsecT Text st Identity ()
forall s (m :: * -> *) t a u.
(Stream s m t, Show a) =>
ParsecT s u m a -> ParsecT s u m ()
notFollowedBy ParsecT Text st Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
anyChar
nameChar :: GenParser st Char
nameChar :: GenParser st Char
nameChar = SourceName -> GenParser st Char
forall s (m :: * -> *) u.
Stream s m Char =>
SourceName -> ParsecT s u m Char
oneOf "~!@$%^&*_-+=<>.?/"
symbol :: GenParser st Symbol
symbol :: GenParser st Text
symbol = GenParser st Text -> ParsecT Text st Identity ()
forall s (m :: * -> *) t a u.
(Stream s m t, Show a) =>
ParsecT s u m a -> ParsecT s u m ()
notFollowedBy (GenParser st Text -> GenParser st Text
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try GenParser st Text
forall st. GenParser st Text
reservedWord) ParsecT Text st Identity ()
-> GenParser st Text -> GenParser st Text
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (GenParser st Text
forall st. GenParser st Text
quotedSymbol GenParser st Text -> GenParser st Text -> GenParser st Text
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> GenParser st Text
forall st. GenParser st Text
simpleSymbol GenParser st Text -> SourceName -> GenParser st Text
forall s u (m :: * -> *) a.
ParsecT s u m a -> SourceName -> ParsecT s u m a
<?> "symbol")
where
simpleSymbol :: ParsecT Text u Identity Text
simpleSymbol = do
Char
c <- GenParser u Char
forall u. ParsecT Text u Identity Char
nameChar GenParser u Char -> GenParser u Char -> GenParser u Char
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> GenParser u Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
letter
SourceName
cs <- GenParser u Char -> ParsecT Text u Identity SourceName
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many (GenParser u Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
alphaNum GenParser u Char -> GenParser u Char -> GenParser u Char
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> GenParser u Char
forall u. ParsecT Text u Identity Char
nameChar)
Text -> ParsecT Text u Identity Text
forall (m :: * -> *) a. Monad m => a -> m a
return (Text -> ParsecT Text u Identity Text)
-> Text -> ParsecT Text u Identity Text
forall a b. (a -> b) -> a -> b
$ SourceName -> Text
T.pack (Char
c Char -> SourceName -> SourceName
forall a. a -> [a] -> [a]
: SourceName
cs)
quotedSymbol :: ParsecT Text u Identity Text
quotedSymbol = ParsecT Text u Identity Char
-> ParsecT Text u Identity Char
-> ParsecT Text u Identity Text
-> ParsecT Text u Identity Text
forall s (m :: * -> *) t u open close a.
Stream s m t =>
ParsecT s u m open
-> ParsecT s u m close -> ParsecT s u m a -> ParsecT s u m a
between (Char -> ParsecT Text u Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '|') (Char -> ParsecT Text u Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '|') (ParsecT Text u Identity Text -> ParsecT Text u Identity Text)
-> ParsecT Text u Identity Text -> ParsecT Text u Identity Text
forall a b. (a -> b) -> a -> b
$ SourceName -> Text
T.pack (SourceName -> Text)
-> ParsecT Text u Identity SourceName
-> ParsecT Text u Identity Text
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text u Identity Char -> ParsecT Text u Identity SourceName
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many (SourceName -> ParsecT Text u Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
SourceName -> ParsecT s u m Char
noneOf "\\|")
keyword :: GenParser st Keyword
keyword :: GenParser st Text
keyword = do
Char -> ParsecT Text st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char ':'
SourceName -> Text
T.pack (SourceName -> Text)
-> ParsecT Text st Identity SourceName -> GenParser st Text
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Char
-> ParsecT Text st Identity SourceName
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 (ParsecT Text st Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
alphaNum ParsecT Text st Identity Char
-> ParsecT Text st Identity Char -> ParsecT Text st Identity Char
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT Text st Identity Char
forall u. ParsecT Text u Identity Char
nameChar)
slist :: GenParser st SList
slist :: GenParser st SList
slist = GenParser st SList -> GenParser st SList
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st SList -> GenParser st SList)
-> (GenParser st SExpr -> GenParser st SList)
-> GenParser st SExpr
-> GenParser st SList
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GenParser st SExpr -> GenParser st SList
forall st a. GenParser st a -> GenParser st [a]
sepSpace (GenParser st SExpr -> GenParser st SList)
-> GenParser st SExpr -> GenParser st SList
forall a b. (a -> b) -> a -> b
$ GenParser st SExpr
forall st. GenParser st SExpr
sexpr
specConstant :: GenParser st SpecConstant
specConstant :: GenParser st SpecConstant
specConstant =
Text -> SpecConstant
SCDecimal (Text -> SpecConstant)
-> ParsecT Text st Identity Text -> GenParser st SpecConstant
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text -> ParsecT Text st Identity Text
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try ParsecT Text st Identity Text
forall st. GenParser st Text
decimal
GenParser st SpecConstant
-> GenParser st SpecConstant -> GenParser st SpecConstant
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Text -> SpecConstant
SCNumeral (Text -> SpecConstant)
-> ParsecT Text st Identity Text -> GenParser st SpecConstant
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text -> ParsecT Text st Identity Text
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try ParsecT Text st Identity Text
forall st. GenParser st Text
numeral
GenParser st SpecConstant
-> GenParser st SpecConstant -> GenParser st SpecConstant
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Text -> SpecConstant
SCHexadecimal (Text -> SpecConstant)
-> ParsecT Text st Identity Text -> GenParser st SpecConstant
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text -> ParsecT Text st Identity Text
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try ParsecT Text st Identity Text
forall st. GenParser st Text
hexadecimal
GenParser st SpecConstant
-> GenParser st SpecConstant -> GenParser st SpecConstant
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Text -> SpecConstant
SCBinary (Text -> SpecConstant)
-> ParsecT Text st Identity Text -> GenParser st SpecConstant
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text -> ParsecT Text st Identity Text
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try ParsecT Text st Identity Text
forall st. GenParser st Text
binary
GenParser st SpecConstant
-> GenParser st SpecConstant -> GenParser st SpecConstant
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Text -> SpecConstant
SCString (Text -> SpecConstant)
-> ParsecT Text st Identity Text -> GenParser st SpecConstant
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text -> ParsecT Text st Identity Text
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try ParsecT Text st Identity Text
forall st. GenParser st Text
stringLiteral
GenParser st SpecConstant
-> SourceName -> GenParser st SpecConstant
forall s u (m :: * -> *) a.
ParsecT s u m a -> SourceName -> ParsecT s u m a
<?> "spec constants"
sexpr :: GenParser st SExpr
sexpr :: GenParser st SExpr
sexpr =
SList -> SExpr
SEList (SList -> SExpr)
-> ParsecT Text st Identity SList -> GenParser st SExpr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity SList -> ParsecT Text st Identity SList
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try ParsecT Text st Identity SList
forall st. GenParser st SList
slist
GenParser st SExpr -> GenParser st SExpr -> GenParser st SExpr
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SpecConstant -> SExpr
SEConstant (SpecConstant -> SExpr)
-> ParsecT Text st Identity SpecConstant -> GenParser st SExpr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity SpecConstant
-> ParsecT Text st Identity SpecConstant
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try ParsecT Text st Identity SpecConstant
forall st. GenParser st SpecConstant
specConstant
GenParser st SExpr -> GenParser st SExpr -> GenParser st SExpr
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Text -> SExpr
SEReservedWord (Text -> SExpr)
-> ParsecT Text st Identity Text -> GenParser st SExpr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text -> ParsecT Text st Identity Text
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try ParsecT Text st Identity Text
forall st. GenParser st Text
reservedWord
GenParser st SExpr -> GenParser st SExpr -> GenParser st SExpr
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Text -> SExpr
SEKeyword (Text -> SExpr)
-> ParsecT Text st Identity Text -> GenParser st SExpr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text -> ParsecT Text st Identity Text
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try ParsecT Text st Identity Text
forall st. GenParser st Text
keyword
GenParser st SExpr -> GenParser st SExpr -> GenParser st SExpr
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Text -> SExpr
SESymbol (Text -> SExpr)
-> ParsecT Text st Identity Text -> GenParser st SExpr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text -> ParsecT Text st Identity Text
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try ParsecT Text st Identity Text
forall st. GenParser st Text
symbol
GenParser st SExpr -> SourceName -> GenParser st SExpr
forall s u (m :: * -> *) a.
ParsecT s u m a -> SourceName -> ParsecT s u m a
<?> "s-expressions"
index :: GenParser st Index
index :: GenParser st Index
index =
Text -> Index
IxNumeral (Text -> Index)
-> ParsecT Text st Identity Text -> GenParser st Index
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text
forall st. GenParser st Text
numeral
GenParser st Index -> GenParser st Index -> GenParser st Index
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Text -> Index
IxSymbol (Text -> Index)
-> ParsecT Text st Identity Text -> GenParser st Index
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text
forall st. GenParser st Text
symbol
identifier :: GenParser st Identifier
identifier :: GenParser st Identifier
identifier =
Text -> Identifier
IdSymbol (Text -> Identifier)
-> ParsecT Text st Identity Text -> GenParser st Identifier
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text
forall st. GenParser st Text
symbol
GenParser st Identifier
-> GenParser st Identifier -> GenParser st Identifier
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> GenParser st Identifier
forall st. GenParser st Identifier
idIndexed
GenParser st Identifier -> SourceName -> GenParser st Identifier
forall s u (m :: * -> *) a.
ParsecT s u m a -> SourceName -> ParsecT s u m a
<?> "identifier"
where
idIndexed :: GenParser st Identifier
idIndexed = GenParser st Identifier -> GenParser st Identifier
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st Identifier -> GenParser st Identifier)
-> GenParser st Identifier -> GenParser st Identifier
forall a b. (a -> b) -> a -> b
$ do
Char -> ParsecT Text st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '_' ParsecT Text st Identity Char
-> ParsecT Text st Identity () -> ParsecT Text st Identity Char
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1
Text
s <- GenParser st Text
forall st. GenParser st Text
symbol GenParser st Text
-> ParsecT Text st Identity () -> GenParser st Text
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1
Text -> NonEmpty Index -> Identifier
IdIndexed Text
s (NonEmpty Index -> Identifier)
-> ParsecT Text st Identity (NonEmpty Index)
-> GenParser st Identifier
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenParser st Index -> ParsecT Text st Identity (NonEmpty Index)
forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepSpace1 GenParser st Index
forall st. GenParser st Index
index
attributeValue :: GenParser st AttributeValue
attributeValue :: GenParser st AttributeValue
attributeValue =
SpecConstant -> AttributeValue
AttrValSpecConstant (SpecConstant -> AttributeValue)
-> ParsecT Text st Identity SpecConstant
-> GenParser st AttributeValue
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity SpecConstant
forall st. GenParser st SpecConstant
specConstant
GenParser st AttributeValue
-> GenParser st AttributeValue -> GenParser st AttributeValue
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Text -> AttributeValue
AttrValSymbol (Text -> AttributeValue)
-> ParsecT Text st Identity Text -> GenParser st AttributeValue
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text
forall st. GenParser st Text
symbol
GenParser st AttributeValue
-> GenParser st AttributeValue -> GenParser st AttributeValue
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SList -> AttributeValue
AttrValSList (SList -> AttributeValue)
-> ParsecT Text st Identity SList -> GenParser st AttributeValue
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity SList
forall st. GenParser st SList
slist
GenParser st AttributeValue
-> SourceName -> GenParser st AttributeValue
forall s u (m :: * -> *) a.
ParsecT s u m a -> SourceName -> ParsecT s u m a
<?> "attribute value"
attribute :: GenParser st Attribute
attribute :: GenParser st Attribute
attribute =
Text -> AttributeValue -> Attribute
AttrKeyValue (Text -> AttributeValue -> Attribute)
-> ParsecT Text st Identity Text
-> ParsecT Text st Identity (AttributeValue -> Attribute)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text -> ParsecT Text st Identity Text
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try (ParsecT Text st Identity Text
forall st. GenParser st Text
keyword ParsecT Text st Identity Text
-> ParsecT Text st Identity () -> ParsecT Text st Identity Text
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1) ParsecT Text st Identity (AttributeValue -> Attribute)
-> ParsecT Text st Identity AttributeValue
-> GenParser st Attribute
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT Text st Identity AttributeValue
forall st. GenParser st AttributeValue
attributeValue
GenParser st Attribute
-> GenParser st Attribute -> GenParser st Attribute
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Text -> Attribute
AttrKey (Text -> Attribute)
-> ParsecT Text st Identity Text -> GenParser st Attribute
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text
forall st. GenParser st Text
keyword
GenParser st Attribute -> SourceName -> GenParser st Attribute
forall s u (m :: * -> *) a.
ParsecT s u m a -> SourceName -> ParsecT s u m a
<?> "attribute"
sortParameter :: GenParser st Sort
sortParameter :: GenParser st Sort
sortParameter = GenParser st Sort -> GenParser st Sort
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st Sort -> GenParser st Sort)
-> GenParser st Sort -> GenParser st Sort
forall a b. (a -> b) -> a -> b
$ do
Identifier
i <- GenParser st Identifier
forall st. GenParser st Identifier
identifier GenParser st Identifier
-> ParsecT Text st Identity () -> GenParser st Identifier
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1
Identifier -> NonEmpty Sort -> Sort
SortParameter Identifier
i (NonEmpty Sort -> Sort)
-> ParsecT Text st Identity (NonEmpty Sort) -> GenParser st Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenParser st Sort -> ParsecT Text st Identity (NonEmpty Sort)
forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepSpace1 GenParser st Sort
forall st. GenParser st Sort
sort
sort :: GenParser st Sort
sort :: GenParser st Sort
sort =
Identifier -> Sort
SortSymbol (Identifier -> Sort)
-> ParsecT Text st Identity Identifier -> GenParser st Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Identifier
-> ParsecT Text st Identity Identifier
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try ParsecT Text st Identity Identifier
forall st. GenParser st Identifier
identifier
GenParser st Sort -> GenParser st Sort -> GenParser st Sort
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> GenParser st Sort
forall st. GenParser st Sort
sortParameter
GenParser st Sort -> SourceName -> GenParser st Sort
forall s u (m :: * -> *) a.
ParsecT s u m a -> SourceName -> ParsecT s u m a
<?> "sort"
qualIdentifier :: GenParser st QualIdentifier
qualIdentifier :: GenParser st QualIdentifier
qualIdentifier =
Identifier -> QualIdentifier
Unqualified (Identifier -> QualIdentifier)
-> ParsecT Text st Identity Identifier
-> GenParser st QualIdentifier
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Identifier
-> ParsecT Text st Identity Identifier
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try ParsecT Text st Identity Identifier
forall st. GenParser st Identifier
identifier
GenParser st QualIdentifier
-> GenParser st QualIdentifier -> GenParser st QualIdentifier
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> GenParser st QualIdentifier -> GenParser st QualIdentifier
forall st a. GenParser st a -> GenParser st a
betweenBrackets GenParser st QualIdentifier
forall st. GenParser st QualIdentifier
annotation
GenParser st QualIdentifier
-> SourceName -> GenParser st QualIdentifier
forall s u (m :: * -> *) a.
ParsecT s u m a -> SourceName -> ParsecT s u m a
<?> "qual identifier"
where
annotation :: GenParser st QualIdentifier
annotation :: GenParser st QualIdentifier
annotation = do
SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryStrBraket "as"
Identifier
id <- GenParser st Identifier
forall st. GenParser st Identifier
identifier GenParser st Identifier
-> GenParser st () -> GenParser st Identifier
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* GenParser st ()
forall st. GenParser st ()
spaces1
Identifier -> Sort -> QualIdentifier
Qualified Identifier
id (Sort -> QualIdentifier)
-> ParsecT Text st Identity Sort -> GenParser st QualIdentifier
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Sort
forall st. GenParser st Sort
sort
varBinding :: GenParser st VarBinding
varBinding :: GenParser st VarBinding
varBinding = GenParser st VarBinding -> GenParser st VarBinding
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st VarBinding -> GenParser st VarBinding)
-> GenParser st VarBinding -> GenParser st VarBinding
forall a b. (a -> b) -> a -> b
$ Text -> Term -> VarBinding
VarBinding (Text -> Term -> VarBinding)
-> ParsecT Text st Identity Text
-> ParsecT Text st Identity (Term -> VarBinding)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text
forall st. GenParser st Text
symbol ParsecT Text st Identity (Term -> VarBinding)
-> ParsecT Text st Identity ()
-> ParsecT Text st Identity (Term -> VarBinding)
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1 ParsecT Text st Identity (Term -> VarBinding)
-> ParsecT Text st Identity Term -> GenParser st VarBinding
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT Text st Identity Term
forall st. GenParser st Term
term
sortedVar :: GenParser st SortedVar
sortedVar :: GenParser st SortedVar
sortedVar = GenParser st SortedVar -> GenParser st SortedVar
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st SortedVar -> GenParser st SortedVar)
-> GenParser st SortedVar -> GenParser st SortedVar
forall a b. (a -> b) -> a -> b
$ Text -> Sort -> SortedVar
SortedVar (Text -> Sort -> SortedVar)
-> ParsecT Text st Identity Text
-> ParsecT Text st Identity (Sort -> SortedVar)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text
forall st. GenParser st Text
symbol ParsecT Text st Identity (Sort -> SortedVar)
-> ParsecT Text st Identity ()
-> ParsecT Text st Identity (Sort -> SortedVar)
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1 ParsecT Text st Identity (Sort -> SortedVar)
-> ParsecT Text st Identity Sort -> GenParser st SortedVar
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT Text st Identity Sort
forall st. GenParser st Sort
sort
matchPattern :: GenParser st MatchPattern
matchPattern :: GenParser st MatchPattern
matchPattern =
Text -> MatchPattern
MPVariable (Text -> MatchPattern)
-> ParsecT Text st Identity Text -> GenParser st MatchPattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text
forall st. GenParser st Text
symbol
GenParser st MatchPattern
-> GenParser st MatchPattern -> GenParser st MatchPattern
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> GenParser st MatchPattern
forall st. GenParser st MatchPattern
mPConstructor
GenParser st MatchPattern
-> SourceName -> GenParser st MatchPattern
forall s u (m :: * -> *) a.
ParsecT s u m a -> SourceName -> ParsecT s u m a
<?> "pattern"
where
mPConstructor :: GenParser st MatchPattern
mPConstructor = GenParser st MatchPattern -> GenParser st MatchPattern
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st MatchPattern -> GenParser st MatchPattern)
-> GenParser st MatchPattern -> GenParser st MatchPattern
forall a b. (a -> b) -> a -> b
$ do
Text
c <- GenParser st Text
forall st. GenParser st Text
symbol GenParser st Text
-> ParsecT Text st Identity () -> GenParser st Text
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1
Text -> NonEmpty Text -> MatchPattern
MPConstructor Text
c (NonEmpty Text -> MatchPattern)
-> ParsecT Text st Identity (NonEmpty Text)
-> GenParser st MatchPattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenParser st Text -> ParsecT Text st Identity (NonEmpty Text)
forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepSpace1 GenParser st Text
forall st. GenParser st Text
symbol
matchCase :: GenParser st MatchCase
matchCase :: GenParser st MatchCase
matchCase = GenParser st MatchCase -> GenParser st MatchCase
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st MatchCase -> GenParser st MatchCase)
-> GenParser st MatchCase -> GenParser st MatchCase
forall a b. (a -> b) -> a -> b
$ do
MatchPattern
p <- GenParser st MatchPattern
forall st. GenParser st MatchPattern
matchPattern GenParser st MatchPattern
-> ParsecT Text st Identity () -> GenParser st MatchPattern
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1
MatchPattern -> Term -> MatchCase
MatchCase MatchPattern
p (Term -> MatchCase)
-> ParsecT Text st Identity Term -> GenParser st MatchCase
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Term
forall st. GenParser st Term
term
term :: GenParser st Term
term :: GenParser st Term
term =
SpecConstant -> Term
TermSpecConstant (SpecConstant -> Term)
-> ParsecT Text st Identity SpecConstant -> GenParser st Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity SpecConstant
-> ParsecT Text st Identity SpecConstant
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try ParsecT Text st Identity SpecConstant
forall st. GenParser st SpecConstant
specConstant
GenParser st Term -> GenParser st Term -> GenParser st Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> QualIdentifier -> Term
TermQualIdentifier (QualIdentifier -> Term)
-> ParsecT Text st Identity QualIdentifier -> GenParser st Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity QualIdentifier
-> ParsecT Text st Identity QualIdentifier
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try ParsecT Text st Identity QualIdentifier
forall st. GenParser st QualIdentifier
qualIdentifier
GenParser st Term -> GenParser st Term -> GenParser st Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> GenParser st Term -> GenParser st Term
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try GenParser st Term
forall st. GenParser st Term
application
GenParser st Term -> GenParser st Term -> GenParser st Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> GenParser st Term -> GenParser st Term
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try GenParser st Term
forall st. GenParser st Term
binding
GenParser st Term -> GenParser st Term -> GenParser st Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> GenParser st Term -> GenParser st Term
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try GenParser st Term
forall st. GenParser st Term
quantifyForall
GenParser st Term -> GenParser st Term -> GenParser st Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> GenParser st Term -> GenParser st Term
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try GenParser st Term
forall st. GenParser st Term
quantifyExists
GenParser st Term -> GenParser st Term -> GenParser st Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> GenParser st Term -> GenParser st Term
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try GenParser st Term
forall st. GenParser st Term
match
GenParser st Term -> GenParser st Term -> GenParser st Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> GenParser st Term -> GenParser st Term
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try GenParser st Term
forall st. GenParser st Term
annotation
GenParser st Term -> SourceName -> GenParser st Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> SourceName -> ParsecT s u m a
<?> "term"
where
application :: GenParser st Term
application = GenParser st Term -> GenParser st Term
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st Term -> GenParser st Term)
-> GenParser st Term -> GenParser st Term
forall a b. (a -> b) -> a -> b
$ do
QualIdentifier
id <- GenParser st QualIdentifier
forall st. GenParser st QualIdentifier
qualIdentifier GenParser st QualIdentifier
-> ParsecT Text st Identity () -> GenParser st QualIdentifier
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces
QualIdentifier -> NonEmpty Term -> Term
TermApplication QualIdentifier
id (NonEmpty Term -> Term)
-> ParsecT Text st Identity (NonEmpty Term) -> GenParser st Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenParser st Term -> ParsecT Text st Identity (NonEmpty Term)
forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepOptSpace1 GenParser st Term
forall st. GenParser st Term
term
binding :: GenParser st Term
binding = GenParser st Term -> GenParser st Term
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st Term -> GenParser st Term)
-> GenParser st Term -> GenParser st Term
forall a b. (a -> b) -> a -> b
$ do
SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryStr "let"
NonEmpty VarBinding
vbs <- GenParser st (NonEmpty VarBinding)
-> GenParser st (NonEmpty VarBinding)
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st (NonEmpty VarBinding)
-> GenParser st (NonEmpty VarBinding))
-> GenParser st (NonEmpty VarBinding)
-> GenParser st (NonEmpty VarBinding)
forall a b. (a -> b) -> a -> b
$ GenParser st VarBinding -> GenParser st (NonEmpty VarBinding)
forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepOptSpace1 GenParser st VarBinding
forall st. GenParser st VarBinding
varBinding
GenParser st ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces
NonEmpty VarBinding -> Term -> Term
TermLet NonEmpty VarBinding
vbs (Term -> Term) -> GenParser st Term -> GenParser st Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenParser st Term
forall st. GenParser st Term
term
quantifyForall :: GenParser st Term
quantifyForall = GenParser st Term -> GenParser st Term
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st Term -> GenParser st Term)
-> GenParser st Term -> GenParser st Term
forall a b. (a -> b) -> a -> b
$ do
SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryStr "forall"
NonEmpty SortedVar
svs <- GenParser st (NonEmpty SortedVar)
-> GenParser st (NonEmpty SortedVar)
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st (NonEmpty SortedVar)
-> GenParser st (NonEmpty SortedVar))
-> GenParser st (NonEmpty SortedVar)
-> GenParser st (NonEmpty SortedVar)
forall a b. (a -> b) -> a -> b
$ GenParser st SortedVar -> GenParser st (NonEmpty SortedVar)
forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepOptSpace1 GenParser st SortedVar
forall st. GenParser st SortedVar
sortedVar
GenParser st ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces
NonEmpty SortedVar -> Term -> Term
TermForall NonEmpty SortedVar
svs (Term -> Term) -> GenParser st Term -> GenParser st Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenParser st Term
forall st. GenParser st Term
term
quantifyExists :: GenParser st Term
quantifyExists = GenParser st Term -> GenParser st Term
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st Term -> GenParser st Term)
-> GenParser st Term -> GenParser st Term
forall a b. (a -> b) -> a -> b
$ do
SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryStr "exists"
NonEmpty SortedVar
svs <- GenParser st (NonEmpty SortedVar)
-> GenParser st (NonEmpty SortedVar)
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st (NonEmpty SortedVar)
-> GenParser st (NonEmpty SortedVar))
-> GenParser st (NonEmpty SortedVar)
-> GenParser st (NonEmpty SortedVar)
forall a b. (a -> b) -> a -> b
$ GenParser st SortedVar -> GenParser st (NonEmpty SortedVar)
forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepOptSpace1 GenParser st SortedVar
forall st. GenParser st SortedVar
sortedVar
GenParser st ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces
NonEmpty SortedVar -> Term -> Term
TermExists NonEmpty SortedVar
svs (Term -> Term) -> GenParser st Term -> GenParser st Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenParser st Term
forall st. GenParser st Term
term
match :: GenParser st Term
match = GenParser st Term -> GenParser st Term
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st Term -> GenParser st Term)
-> GenParser st Term -> GenParser st Term
forall a b. (a -> b) -> a -> b
$ do
SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryStr "match"
Term
t <- GenParser st Term
forall st. GenParser st Term
term GenParser st Term -> GenParser st () -> GenParser st Term
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* GenParser st ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces
Term -> NonEmpty MatchCase -> Term
TermMatch Term
t (NonEmpty MatchCase -> Term)
-> ParsecT Text st Identity (NonEmpty MatchCase)
-> GenParser st Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity (NonEmpty MatchCase)
-> ParsecT Text st Identity (NonEmpty MatchCase)
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st MatchCase
-> ParsecT Text st Identity (NonEmpty MatchCase)
forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepOptSpace1 GenParser st MatchCase
forall st. GenParser st MatchCase
matchCase)
annotation :: GenParser st Term
annotation = GenParser st Term -> GenParser st Term
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st Term -> GenParser st Term)
-> GenParser st Term -> GenParser st Term
forall a b. (a -> b) -> a -> b
$ do
Char -> ParsecT Text st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '!' ParsecT Text st Identity Char
-> ParsecT Text st Identity () -> ParsecT Text st Identity Char
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1
Term
t <- GenParser st Term
forall st. GenParser st Term
term GenParser st Term
-> ParsecT Text st Identity () -> GenParser st Term
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1
Term -> NonEmpty Attribute -> Term
TermAnnotation Term
t (NonEmpty Attribute -> Term)
-> ParsecT Text st Identity (NonEmpty Attribute)
-> GenParser st Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenParser st Attribute
-> ParsecT Text st Identity (NonEmpty Attribute)
forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepSpace1 GenParser st Attribute
forall st. GenParser st Attribute
attribute
sortSymbolDecl :: GenParser st SortSymbolDecl
sortSymbolDecl :: GenParser st SortSymbolDecl
sortSymbolDecl = GenParser st SortSymbolDecl -> GenParser st SortSymbolDecl
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st SortSymbolDecl -> GenParser st SortSymbolDecl)
-> GenParser st SortSymbolDecl -> GenParser st SortSymbolDecl
forall a b. (a -> b) -> a -> b
$ do
Identifier
i <- GenParser st Identifier
forall st. GenParser st Identifier
identifier GenParser st Identifier
-> ParsecT Text st Identity () -> GenParser st Identifier
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1
Text
n <- GenParser st Text
forall st. GenParser st Text
numeral GenParser st Text
-> ParsecT Text st Identity () -> GenParser st Text
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces
Identifier -> Text -> [Attribute] -> SortSymbolDecl
SortSymbolDecl Identifier
i Text
n ([Attribute] -> SortSymbolDecl)
-> ParsecT Text st Identity [Attribute]
-> GenParser st SortSymbolDecl
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenParser st Attribute -> ParsecT Text st Identity [Attribute]
forall st a. GenParser st a -> GenParser st [a]
sepSpace GenParser st Attribute
forall st. GenParser st Attribute
attribute
metaSpecConstant :: GenParser st MetaSpecConstant
metaSpecConstant :: GenParser st MetaSpecConstant
metaSpecConstant =
SourceName -> ParsecT Text st Identity SourceName
forall s (m :: * -> *) u.
Stream s m Char =>
SourceName -> ParsecT s u m SourceName
string "NUMERAL" ParsecT Text st Identity SourceName
-> MetaSpecConstant -> GenParser st MetaSpecConstant
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> MetaSpecConstant
MSC_NUMERAL
GenParser st MetaSpecConstant
-> GenParser st MetaSpecConstant -> GenParser st MetaSpecConstant
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> ParsecT Text st Identity SourceName
forall s (m :: * -> *) u.
Stream s m Char =>
SourceName -> ParsecT s u m SourceName
string "DECIMAL" ParsecT Text st Identity SourceName
-> MetaSpecConstant -> GenParser st MetaSpecConstant
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> MetaSpecConstant
MSC_DECIMAL
GenParser st MetaSpecConstant
-> GenParser st MetaSpecConstant -> GenParser st MetaSpecConstant
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> ParsecT Text st Identity SourceName
forall s (m :: * -> *) u.
Stream s m Char =>
SourceName -> ParsecT s u m SourceName
string "STRING" ParsecT Text st Identity SourceName
-> MetaSpecConstant -> GenParser st MetaSpecConstant
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> MetaSpecConstant
MSC_STRING
GenParser st MetaSpecConstant
-> SourceName -> GenParser st MetaSpecConstant
forall s u (m :: * -> *) a.
ParsecT s u m a -> SourceName -> ParsecT s u m a
<?> "meta spec constant"
funSymbolDecl :: GenParser st FunSymbolDecl
funSymbolDecl :: GenParser st FunSymbolDecl
funSymbolDecl =
GenParser st FunSymbolDecl -> GenParser st FunSymbolDecl
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try (GenParser st FunSymbolDecl -> GenParser st FunSymbolDecl
forall st a. GenParser st a -> GenParser st a
betweenBrackets GenParser st FunSymbolDecl
forall st. ParsecT Text st Identity FunSymbolDecl
funConstant)
GenParser st FunSymbolDecl
-> GenParser st FunSymbolDecl -> GenParser st FunSymbolDecl
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> GenParser st FunSymbolDecl -> GenParser st FunSymbolDecl
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try (GenParser st FunSymbolDecl -> GenParser st FunSymbolDecl
forall st a. GenParser st a -> GenParser st a
betweenBrackets GenParser st FunSymbolDecl
forall st. ParsecT Text st Identity FunSymbolDecl
funMeta)
GenParser st FunSymbolDecl
-> GenParser st FunSymbolDecl -> GenParser st FunSymbolDecl
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> GenParser st FunSymbolDecl -> GenParser st FunSymbolDecl
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try (GenParser st FunSymbolDecl -> GenParser st FunSymbolDecl
forall st a. GenParser st a -> GenParser st a
betweenBrackets GenParser st FunSymbolDecl
forall st. ParsecT Text st Identity FunSymbolDecl
funIdentifier)
GenParser st FunSymbolDecl
-> SourceName -> GenParser st FunSymbolDecl
forall s u (m :: * -> *) a.
ParsecT s u m a -> SourceName -> ParsecT s u m a
<?> "non-parametric function symbol declaration"
where
funConstant :: ParsecT Text st Identity FunSymbolDecl
funConstant = do
SpecConstant
sc <- GenParser st SpecConstant
forall st. GenParser st SpecConstant
specConstant GenParser st SpecConstant
-> ParsecT Text st Identity () -> GenParser st SpecConstant
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1
Sort
s <- GenParser st Sort
forall st. GenParser st Sort
sort GenParser st Sort
-> ParsecT Text st Identity () -> GenParser st Sort
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1
SpecConstant -> Sort -> [Attribute] -> FunSymbolDecl
FunConstant SpecConstant
sc Sort
s ([Attribute] -> FunSymbolDecl)
-> ParsecT Text st Identity [Attribute]
-> ParsecT Text st Identity FunSymbolDecl
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenParser st Attribute -> ParsecT Text st Identity [Attribute]
forall st a. GenParser st a -> GenParser st [a]
sepSpace GenParser st Attribute
forall st. GenParser st Attribute
attribute
funMeta :: ParsecT Text st Identity FunSymbolDecl
funMeta = do
MetaSpecConstant
m <- GenParser st MetaSpecConstant
forall st. GenParser st MetaSpecConstant
metaSpecConstant GenParser st MetaSpecConstant
-> ParsecT Text st Identity () -> GenParser st MetaSpecConstant
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1
Sort
s <- GenParser st Sort
forall st. GenParser st Sort
sort GenParser st Sort
-> ParsecT Text st Identity () -> GenParser st Sort
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1
MetaSpecConstant -> Sort -> [Attribute] -> FunSymbolDecl
FunMeta MetaSpecConstant
m Sort
s ([Attribute] -> FunSymbolDecl)
-> ParsecT Text st Identity [Attribute]
-> ParsecT Text st Identity FunSymbolDecl
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenParser st Attribute -> ParsecT Text st Identity [Attribute]
forall st a. GenParser st a -> GenParser st [a]
sepSpace GenParser st Attribute
forall st. GenParser st Attribute
attribute
funIdentifier :: ParsecT Text st Identity FunSymbolDecl
funIdentifier = do
Identifier
i <- GenParser st Identifier
forall st. GenParser st Identifier
identifier GenParser st Identifier
-> ParsecT Text st Identity () -> GenParser st Identifier
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1
NonEmpty Sort
ss <- GenParser st Sort -> GenParser st (NonEmpty Sort)
forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepSpace1 GenParser st Sort
forall st. GenParser st Sort
sort
[Attribute]
as <- GenParser st Attribute -> GenParser st [Attribute]
forall st a. GenParser st a -> GenParser st [a]
sepSpace GenParser st Attribute
forall st. GenParser st Attribute
attribute
FunSymbolDecl -> ParsecT Text st Identity FunSymbolDecl
forall (m :: * -> *) a. Monad m => a -> m a
return (FunSymbolDecl -> ParsecT Text st Identity FunSymbolDecl)
-> FunSymbolDecl -> ParsecT Text st Identity FunSymbolDecl
forall a b. (a -> b) -> a -> b
$ Identifier -> NonEmpty Sort -> [Attribute] -> FunSymbolDecl
FunIdentifier Identifier
i NonEmpty Sort
ss [Attribute]
as
parFunSymbolDecl :: GenParser st ParFunSymbolDecl
parFunSymbolDecl :: GenParser st ParFunSymbolDecl
parFunSymbolDecl =
FunSymbolDecl -> ParFunSymbolDecl
NonPar (FunSymbolDecl -> ParFunSymbolDecl)
-> ParsecT Text st Identity FunSymbolDecl
-> GenParser st ParFunSymbolDecl
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity FunSymbolDecl
forall st. ParsecT Text st Identity FunSymbolDecl
funSymbolDecl
GenParser st ParFunSymbolDecl
-> GenParser st ParFunSymbolDecl -> GenParser st ParFunSymbolDecl
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> GenParser st ParFunSymbolDecl -> GenParser st ParFunSymbolDecl
forall st a. GenParser st a -> GenParser st a
betweenBrackets GenParser st ParFunSymbolDecl
forall st. ParsecT Text st Identity ParFunSymbolDecl
par
GenParser st ParFunSymbolDecl
-> SourceName -> GenParser st ParFunSymbolDecl
forall s u (m :: * -> *) a.
ParsecT s u m a -> SourceName -> ParsecT s u m a
<?> "potentially parametric function symbol declaration"
where
par :: ParsecT Text st Identity ParFunSymbolDecl
par = do
SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryStr "par"
NonEmpty Text
syms <- GenParser st (NonEmpty Text) -> GenParser st (NonEmpty Text)
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st (NonEmpty Text) -> GenParser st (NonEmpty Text))
-> (GenParser st Text -> GenParser st (NonEmpty Text))
-> GenParser st Text
-> GenParser st (NonEmpty Text)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GenParser st Text -> GenParser st (NonEmpty Text)
forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepSpace1 (GenParser st Text -> GenParser st (NonEmpty Text))
-> GenParser st Text -> GenParser st (NonEmpty Text)
forall a b. (a -> b) -> a -> b
$ GenParser st Text
forall st. GenParser st Text
symbol
GenParser st ()
forall st. GenParser st ()
spaces1
ParsecT Text st Identity ParFunSymbolDecl
-> ParsecT Text st Identity ParFunSymbolDecl
forall st a. GenParser st a -> GenParser st a
betweenBrackets (ParsecT Text st Identity ParFunSymbolDecl
-> ParsecT Text st Identity ParFunSymbolDecl)
-> ParsecT Text st Identity ParFunSymbolDecl
-> ParsecT Text st Identity ParFunSymbolDecl
forall a b. (a -> b) -> a -> b
$ do
Identifier
idt <- GenParser st Identifier
forall st. GenParser st Identifier
identifier GenParser st Identifier
-> GenParser st () -> GenParser st Identifier
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* GenParser st ()
forall st. GenParser st ()
spaces1
NonEmpty Sort
ss <- GenParser st Sort -> GenParser st (NonEmpty Sort)
forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepSpace1 GenParser st Sort
forall st. GenParser st Sort
sort
NonEmpty Text
-> Identifier -> NonEmpty Sort -> [Attribute] -> ParFunSymbolDecl
Par NonEmpty Text
syms Identifier
idt NonEmpty Sort
ss ([Attribute] -> ParFunSymbolDecl)
-> ParsecT Text st Identity [Attribute]
-> ParsecT Text st Identity ParFunSymbolDecl
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenParser st Attribute -> ParsecT Text st Identity [Attribute]
forall st a. GenParser st a -> GenParser st [a]
sepSpace GenParser st Attribute
forall st. GenParser st Attribute
attribute
theoryAttribute :: GenParser st TheoryAttribute
theoryAttribute :: GenParser st TheoryAttribute
theoryAttribute =
SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryAttr "sorts" GenParser st ()
-> GenParser st TheoryAttribute -> GenParser st TheoryAttribute
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> GenParser st TheoryAttribute -> GenParser st TheoryAttribute
forall st a. GenParser st a -> GenParser st a
betweenBrackets (NonEmpty SortSymbolDecl -> TheoryAttribute
TASorts (NonEmpty SortSymbolDecl -> TheoryAttribute)
-> ParsecT Text st Identity (NonEmpty SortSymbolDecl)
-> GenParser st TheoryAttribute
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenParser st SortSymbolDecl
-> ParsecT Text st Identity (NonEmpty SortSymbolDecl)
forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepSpace1 GenParser st SortSymbolDecl
forall st. GenParser st SortSymbolDecl
sortSymbolDecl)
GenParser st TheoryAttribute
-> GenParser st TheoryAttribute -> GenParser st TheoryAttribute
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryAttr "funs" GenParser st ()
-> GenParser st TheoryAttribute -> GenParser st TheoryAttribute
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> GenParser st TheoryAttribute -> GenParser st TheoryAttribute
forall st a. GenParser st a -> GenParser st a
betweenBrackets (NonEmpty ParFunSymbolDecl -> TheoryAttribute
TAFuns (NonEmpty ParFunSymbolDecl -> TheoryAttribute)
-> ParsecT Text st Identity (NonEmpty ParFunSymbolDecl)
-> GenParser st TheoryAttribute
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenParser st ParFunSymbolDecl
-> ParsecT Text st Identity (NonEmpty ParFunSymbolDecl)
forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepSpace1 GenParser st ParFunSymbolDecl
forall st. ParsecT Text st Identity ParFunSymbolDecl
parFunSymbolDecl)
GenParser st TheoryAttribute
-> GenParser st TheoryAttribute -> GenParser st TheoryAttribute
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryAttr "sorts-description" GenParser st ()
-> GenParser st TheoryAttribute -> GenParser st TheoryAttribute
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (Text -> TheoryAttribute
TASortsDescription (Text -> TheoryAttribute)
-> ParsecT Text st Identity Text -> GenParser st TheoryAttribute
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text
forall st. GenParser st Text
stringLiteral)
GenParser st TheoryAttribute
-> GenParser st TheoryAttribute -> GenParser st TheoryAttribute
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryAttr "funs-description" GenParser st ()
-> GenParser st TheoryAttribute -> GenParser st TheoryAttribute
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (Text -> TheoryAttribute
TAFunsDescription (Text -> TheoryAttribute)
-> ParsecT Text st Identity Text -> GenParser st TheoryAttribute
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text
forall st. GenParser st Text
stringLiteral)
GenParser st TheoryAttribute
-> GenParser st TheoryAttribute -> GenParser st TheoryAttribute
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryAttr "definition" GenParser st ()
-> GenParser st TheoryAttribute -> GenParser st TheoryAttribute
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (Text -> TheoryAttribute
TADefinition (Text -> TheoryAttribute)
-> ParsecT Text st Identity Text -> GenParser st TheoryAttribute
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text
forall st. GenParser st Text
stringLiteral)
GenParser st TheoryAttribute
-> GenParser st TheoryAttribute -> GenParser st TheoryAttribute
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryAttr "values" GenParser st ()
-> GenParser st TheoryAttribute -> GenParser st TheoryAttribute
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (Text -> TheoryAttribute
TAValues (Text -> TheoryAttribute)
-> ParsecT Text st Identity Text -> GenParser st TheoryAttribute
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text
forall st. GenParser st Text
stringLiteral)
GenParser st TheoryAttribute
-> GenParser st TheoryAttribute -> GenParser st TheoryAttribute
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryAttr "notes" GenParser st ()
-> GenParser st TheoryAttribute -> GenParser st TheoryAttribute
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (Text -> TheoryAttribute
TANotes (Text -> TheoryAttribute)
-> ParsecT Text st Identity Text -> GenParser st TheoryAttribute
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text
forall st. GenParser st Text
stringLiteral)
GenParser st TheoryAttribute
-> GenParser st TheoryAttribute -> GenParser st TheoryAttribute
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Attribute -> TheoryAttribute
TAAttr (Attribute -> TheoryAttribute)
-> ParsecT Text st Identity Attribute
-> GenParser st TheoryAttribute
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Attribute
forall st. GenParser st Attribute
attribute
GenParser st TheoryAttribute
-> SourceName -> GenParser st TheoryAttribute
forall s u (m :: * -> *) a.
ParsecT s u m a -> SourceName -> ParsecT s u m a
<?> "theory attributes"
theoryDecl :: GenParser st TheoryDecl
theoryDecl :: GenParser st TheoryDecl
theoryDecl = GenParser st TheoryDecl -> GenParser st TheoryDecl
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st TheoryDecl -> GenParser st TheoryDecl)
-> GenParser st TheoryDecl -> GenParser st TheoryDecl
forall a b. (a -> b) -> a -> b
$ do
SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryStr "theory"
Text
s <- GenParser st Text
forall st. GenParser st Text
symbol GenParser st Text -> GenParser st () -> GenParser st Text
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* GenParser st ()
forall st. GenParser st ()
spaces1
Text -> NonEmpty TheoryAttribute -> TheoryDecl
TheoryDecl Text
s (NonEmpty TheoryAttribute -> TheoryDecl)
-> ParsecT Text st Identity (NonEmpty TheoryAttribute)
-> GenParser st TheoryDecl
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenParser st TheoryAttribute
-> ParsecT Text st Identity (NonEmpty TheoryAttribute)
forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepSpace1 GenParser st TheoryAttribute
forall st. GenParser st TheoryAttribute
theoryAttribute
logicAttribute :: GenParser st LogicAttribute
logicAttribute :: GenParser st LogicAttribute
logicAttribute =
SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryAttr "theories" GenParser st ()
-> GenParser st LogicAttribute -> GenParser st LogicAttribute
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> GenParser st LogicAttribute -> GenParser st LogicAttribute
forall st a. GenParser st a -> GenParser st a
betweenBrackets (NonEmpty Text -> LogicAttribute
LATheories (NonEmpty Text -> LogicAttribute)
-> ParsecT Text st Identity (NonEmpty Text)
-> GenParser st LogicAttribute
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenParser st Text -> ParsecT Text st Identity (NonEmpty Text)
forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepSpace1 GenParser st Text
forall st. GenParser st Text
symbol)
GenParser st LogicAttribute
-> GenParser st LogicAttribute -> GenParser st LogicAttribute
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryAttr "language" GenParser st ()
-> GenParser st LogicAttribute -> GenParser st LogicAttribute
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (Text -> LogicAttribute
LALanguage (Text -> LogicAttribute)
-> GenParser st Text -> GenParser st LogicAttribute
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenParser st Text
forall st. GenParser st Text
stringLiteral)
GenParser st LogicAttribute
-> GenParser st LogicAttribute -> GenParser st LogicAttribute
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryAttr "extensions" GenParser st ()
-> GenParser st LogicAttribute -> GenParser st LogicAttribute
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (Text -> LogicAttribute
LAExtensions (Text -> LogicAttribute)
-> GenParser st Text -> GenParser st LogicAttribute
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenParser st Text
forall st. GenParser st Text
stringLiteral)
GenParser st LogicAttribute
-> GenParser st LogicAttribute -> GenParser st LogicAttribute
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryAttr "values" GenParser st ()
-> GenParser st LogicAttribute -> GenParser st LogicAttribute
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (Text -> LogicAttribute
LAValues (Text -> LogicAttribute)
-> GenParser st Text -> GenParser st LogicAttribute
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenParser st Text
forall st. GenParser st Text
stringLiteral)
GenParser st LogicAttribute
-> GenParser st LogicAttribute -> GenParser st LogicAttribute
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryAttr "notes" GenParser st ()
-> GenParser st LogicAttribute -> GenParser st LogicAttribute
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (Text -> LogicAttribute
LANotes (Text -> LogicAttribute)
-> GenParser st Text -> GenParser st LogicAttribute
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenParser st Text
forall st. GenParser st Text
stringLiteral)
GenParser st LogicAttribute
-> GenParser st LogicAttribute -> GenParser st LogicAttribute
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Attribute -> LogicAttribute
LAAttr (Attribute -> LogicAttribute)
-> ParsecT Text st Identity Attribute
-> GenParser st LogicAttribute
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Attribute
forall st. GenParser st Attribute
attribute
logic :: GenParser st Logic
logic :: GenParser st Logic
logic = GenParser st Logic -> GenParser st Logic
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st Logic -> GenParser st Logic)
-> GenParser st Logic -> GenParser st Logic
forall a b. (a -> b) -> a -> b
$ do
SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryStr "logic"
Text
s <- GenParser st Text
forall st. GenParser st Text
symbol GenParser st Text -> GenParser st () -> GenParser st Text
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* GenParser st ()
forall st. GenParser st ()
spaces1
Text -> NonEmpty LogicAttribute -> Logic
Logic Text
s (NonEmpty LogicAttribute -> Logic)
-> ParsecT Text st Identity (NonEmpty LogicAttribute)
-> GenParser st Logic
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenParser st LogicAttribute
-> ParsecT Text st Identity (NonEmpty LogicAttribute)
forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepSpace1 GenParser st LogicAttribute
forall st. GenParser st LogicAttribute
logicAttribute
sortDec :: GenParser st SortDec
sortDec :: GenParser st SortDec
sortDec = GenParser st SortDec -> GenParser st SortDec
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st SortDec -> GenParser st SortDec)
-> GenParser st SortDec -> GenParser st SortDec
forall a b. (a -> b) -> a -> b
$ do
Text
s <- GenParser st Text
forall st. GenParser st Text
symbol GenParser st Text
-> ParsecT Text st Identity () -> GenParser st Text
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1
Text -> Text -> SortDec
SortDec Text
s (Text -> SortDec) -> GenParser st Text -> GenParser st SortDec
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenParser st Text
forall st. GenParser st Text
numeral
selectorDec :: GenParser st SelectorDec
selectorDec :: GenParser st SelectorDec
selectorDec = GenParser st SelectorDec -> GenParser st SelectorDec
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st SelectorDec -> GenParser st SelectorDec)
-> GenParser st SelectorDec -> GenParser st SelectorDec
forall a b. (a -> b) -> a -> b
$ do
Text
s <- GenParser st Text
forall st. GenParser st Text
symbol GenParser st Text
-> ParsecT Text st Identity () -> GenParser st Text
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1
Text -> Sort -> SelectorDec
SelectorDec Text
s (Sort -> SelectorDec)
-> ParsecT Text st Identity Sort -> GenParser st SelectorDec
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Sort
forall st. GenParser st Sort
sort
constructorDec :: GenParser st ConstructorDec
constructorDec :: GenParser st ConstructorDec
constructorDec = GenParser st ConstructorDec -> GenParser st ConstructorDec
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st ConstructorDec -> GenParser st ConstructorDec)
-> GenParser st ConstructorDec -> GenParser st ConstructorDec
forall a b. (a -> b) -> a -> b
$ do
Text
s <- GenParser st Text
forall st. GenParser st Text
symbol GenParser st Text
-> ParsecT Text st Identity () -> GenParser st Text
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1
Text -> [SelectorDec] -> ConstructorDec
ConstructorDec Text
s ([SelectorDec] -> ConstructorDec)
-> ParsecT Text st Identity [SelectorDec]
-> GenParser st ConstructorDec
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenParser st SelectorDec -> ParsecT Text st Identity [SelectorDec]
forall st a. GenParser st a -> GenParser st [a]
sepSpace GenParser st SelectorDec
forall st. GenParser st SelectorDec
selectorDec
datatypeDec :: GenParser st DatatypeDec
datatypeDec :: GenParser st DatatypeDec
datatypeDec =
NonEmpty ConstructorDec -> DatatypeDec
DDNonparametric (NonEmpty ConstructorDec -> DatatypeDec)
-> ParsecT Text st Identity (NonEmpty ConstructorDec)
-> GenParser st DatatypeDec
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity (NonEmpty ConstructorDec)
-> ParsecT Text st Identity (NonEmpty ConstructorDec)
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st ConstructorDec
-> ParsecT Text st Identity (NonEmpty ConstructorDec)
forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepSpace1 GenParser st ConstructorDec
forall st. GenParser st ConstructorDec
constructorDec)
GenParser st DatatypeDec
-> GenParser st DatatypeDec -> GenParser st DatatypeDec
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> GenParser st DatatypeDec
forall st. GenParser st DatatypeDec
parametric
GenParser st DatatypeDec -> SourceName -> GenParser st DatatypeDec
forall s u (m :: * -> *) a.
ParsecT s u m a -> SourceName -> ParsecT s u m a
<?> "datatype declaration"
where
parametric :: GenParser st DatatypeDec
parametric = GenParser st DatatypeDec -> GenParser st DatatypeDec
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st DatatypeDec -> GenParser st DatatypeDec)
-> GenParser st DatatypeDec -> GenParser st DatatypeDec
forall a b. (a -> b) -> a -> b
$ do
SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryStr1 "par"
NonEmpty Text
ss <- GenParser st (NonEmpty Text) -> GenParser st (NonEmpty Text)
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st (NonEmpty Text) -> GenParser st (NonEmpty Text))
-> GenParser st (NonEmpty Text) -> GenParser st (NonEmpty Text)
forall a b. (a -> b) -> a -> b
$ GenParser st Text -> GenParser st (NonEmpty Text)
forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepSpace1 GenParser st Text
forall st. GenParser st Text
symbol
GenParser st ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces
NonEmpty Text -> NonEmpty ConstructorDec -> DatatypeDec
DDParametric NonEmpty Text
ss (NonEmpty ConstructorDec -> DatatypeDec)
-> ParsecT Text st Identity (NonEmpty ConstructorDec)
-> GenParser st DatatypeDec
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity (NonEmpty ConstructorDec)
-> ParsecT Text st Identity (NonEmpty ConstructorDec)
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st ConstructorDec
-> ParsecT Text st Identity (NonEmpty ConstructorDec)
forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepSpace1 GenParser st ConstructorDec
forall st. GenParser st ConstructorDec
constructorDec)
functionDec :: GenParser st FunctionDec
functionDec :: GenParser st FunctionDec
functionDec = GenParser st FunctionDec -> GenParser st FunctionDec
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st FunctionDec -> GenParser st FunctionDec)
-> GenParser st FunctionDec -> GenParser st FunctionDec
forall a b. (a -> b) -> a -> b
$ do
Text
s <- GenParser st Text
forall st. GenParser st Text
symbol GenParser st Text
-> ParsecT Text st Identity () -> GenParser st Text
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces
[SortedVar]
svs <- GenParser st [SortedVar] -> GenParser st [SortedVar]
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st [SortedVar] -> GenParser st [SortedVar])
-> GenParser st [SortedVar] -> GenParser st [SortedVar]
forall a b. (a -> b) -> a -> b
$ GenParser st SortedVar -> GenParser st [SortedVar]
forall st a. GenParser st a -> GenParser st [a]
sepSpace GenParser st SortedVar
forall st. GenParser st SortedVar
sortedVar
ParsecT Text st Identity ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces
Text -> [SortedVar] -> Sort -> FunctionDec
FunctionDec Text
s [SortedVar]
svs (Sort -> FunctionDec)
-> ParsecT Text st Identity Sort -> GenParser st FunctionDec
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Sort
forall st. GenParser st Sort
sort
functionDef :: GenParser st FunctionDef
functionDef :: GenParser st FunctionDef
functionDef = GenParser st FunctionDef -> GenParser st FunctionDef
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st FunctionDef -> GenParser st FunctionDef)
-> GenParser st FunctionDef -> GenParser st FunctionDef
forall a b. (a -> b) -> a -> b
$ do
Text
s <- GenParser st Text
forall st. GenParser st Text
symbol GenParser st Text
-> ParsecT Text st Identity () -> GenParser st Text
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces
[SortedVar]
svs <- GenParser st [SortedVar] -> GenParser st [SortedVar]
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st [SortedVar] -> GenParser st [SortedVar])
-> GenParser st [SortedVar] -> GenParser st [SortedVar]
forall a b. (a -> b) -> a -> b
$ GenParser st SortedVar -> GenParser st [SortedVar]
forall st a. GenParser st a -> GenParser st [a]
sepSpace GenParser st SortedVar
forall st. GenParser st SortedVar
sortedVar
Sort
t <- ParsecT Text st Identity ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces ParsecT Text st Identity ()
-> ParsecT Text st Identity Sort -> ParsecT Text st Identity Sort
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT Text st Identity Sort
forall st. GenParser st Sort
sort ParsecT Text st Identity Sort
-> ParsecT Text st Identity () -> ParsecT Text st Identity Sort
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1
Text -> [SortedVar] -> Sort -> Term -> FunctionDef
FunctionDef Text
s [SortedVar]
svs Sort
t (Term -> FunctionDef)
-> ParsecT Text st Identity Term -> GenParser st FunctionDef
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Term
forall st. GenParser st Term
term
propLiteral :: GenParser st PropLiteral
propLiteral :: GenParser st PropLiteral
propLiteral =
Text -> PropLiteral
PLPositive (Text -> PropLiteral)
-> ParsecT Text st Identity Text -> GenParser st PropLiteral
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text
forall st. GenParser st Text
symbol
GenParser st PropLiteral
-> GenParser st PropLiteral -> GenParser st PropLiteral
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Text -> PropLiteral
PLNegative (Text -> PropLiteral)
-> ParsecT Text st Identity Text -> GenParser st PropLiteral
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text -> ParsecT Text st Identity Text
forall st a. GenParser st a -> GenParser st a
betweenBrackets (SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryStr1 "not" GenParser st ()
-> ParsecT Text st Identity Text -> ParsecT Text st Identity Text
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT Text st Identity Text
forall st. GenParser st Text
symbol)
command :: GenParser st Command
command :: GenParser st Command
command =
SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "assert" (Term -> Command
Assert (Term -> Command)
-> ParsecT Text st Identity Term -> GenParser st Command
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Term
forall st. GenParser st Term
term)
GenParser st Command
-> GenParser st Command -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "check-sat" (Command -> GenParser st Command
forall (f :: * -> *) a. Applicative f => a -> f a
pure Command
CheckSat)
GenParser st Command
-> GenParser st Command -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "check-sat-assuming" (GenParser st Command -> GenParser st Command
forall st a. GenParser st a -> GenParser st a
betweenBrackets ([PropLiteral] -> Command
CheckSatAssuming ([PropLiteral] -> Command)
-> ParsecT Text st Identity [PropLiteral] -> GenParser st Command
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenParser st PropLiteral -> ParsecT Text st Identity [PropLiteral]
forall st a. GenParser st a -> GenParser st [a]
sepSpace GenParser st PropLiteral
forall st. GenParser st PropLiteral
propLiteral))
GenParser st Command
-> GenParser st Command -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "declare-const" (Text -> Sort -> Command
DeclareConst (Text -> Sort -> Command)
-> ParsecT Text st Identity Text
-> ParsecT Text st Identity (Sort -> Command)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ParsecT Text st Identity Text
forall st. GenParser st Text
symbol ParsecT Text st Identity Text
-> ParsecT Text st Identity () -> ParsecT Text st Identity Text
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1) ParsecT Text st Identity (Sort -> Command)
-> ParsecT Text st Identity Sort -> GenParser st Command
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT Text st Identity Sort
forall st. GenParser st Sort
sort)
GenParser st Command
-> GenParser st Command -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "declare-datatype" (Text -> DatatypeDec -> Command
DeclareDatatype (Text -> DatatypeDec -> Command)
-> ParsecT Text st Identity Text
-> ParsecT Text st Identity (DatatypeDec -> Command)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ParsecT Text st Identity Text
forall st. GenParser st Text
symbol ParsecT Text st Identity Text
-> ParsecT Text st Identity () -> ParsecT Text st Identity Text
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1) ParsecT Text st Identity (DatatypeDec -> Command)
-> ParsecT Text st Identity DatatypeDec -> GenParser st Command
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT Text st Identity DatatypeDec
forall st. GenParser st DatatypeDec
datatypeDec)
GenParser st Command
-> GenParser st Command -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "declare-datatypes" GenParser st Command
forall st. ParsecT Text st Identity Command
declareDatatypes
GenParser st Command
-> GenParser st Command -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "declare-fun" GenParser st Command
forall st. ParsecT Text st Identity Command
declareFun
GenParser st Command
-> GenParser st Command -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "declare-sort" GenParser st Command
forall st. ParsecT Text st Identity Command
declareSort
GenParser st Command
-> GenParser st Command -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "define-fun" (FunctionDef -> Command
DefineFun (FunctionDef -> Command)
-> ParsecT Text st Identity FunctionDef -> GenParser st Command
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity FunctionDef
forall st. GenParser st FunctionDef
functionDef)
GenParser st Command
-> GenParser st Command -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "define-fun-rec" (FunctionDef -> Command
DefineFunRec (FunctionDef -> Command)
-> ParsecT Text st Identity FunctionDef -> GenParser st Command
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity FunctionDef
forall st. GenParser st FunctionDef
functionDef)
GenParser st Command
-> GenParser st Command -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "define-funs-rec" GenParser st Command
forall st. ParsecT Text st Identity Command
defineFunsRec
GenParser st Command
-> GenParser st Command -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "define-sort" GenParser st Command
forall st. ParsecT Text st Identity Command
defineSort
GenParser st Command
-> GenParser st Command -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "echo" (Text -> Command
Echo (Text -> Command)
-> ParsecT Text st Identity Text -> GenParser st Command
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text
forall st. GenParser st Text
stringLiteral)
GenParser st Command
-> GenParser st Command -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "exit" (Command -> GenParser st Command
forall (f :: * -> *) a. Applicative f => a -> f a
pure Command
Exit)
GenParser st Command
-> GenParser st Command -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "get-assertions" (Command -> GenParser st Command
forall (f :: * -> *) a. Applicative f => a -> f a
pure Command
GetAssertions)
GenParser st Command
-> GenParser st Command -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "get-assignment" (Command -> GenParser st Command
forall (f :: * -> *) a. Applicative f => a -> f a
pure Command
GetAssignment)
GenParser st Command
-> GenParser st Command -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "get-info" (InfoFlag -> Command
GetInfo (InfoFlag -> Command)
-> ParsecT Text st Identity InfoFlag -> GenParser st Command
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity InfoFlag
forall st. GenParser st InfoFlag
infoFlag)
GenParser st Command
-> GenParser st Command -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "get-model" (Command -> GenParser st Command
forall (f :: * -> *) a. Applicative f => a -> f a
pure Command
GetModel)
GenParser st Command
-> GenParser st Command -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "get-option" (Text -> Command
GetOption (Text -> Command)
-> ParsecT Text st Identity Text -> GenParser st Command
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text
forall st. GenParser st Text
keyword)
GenParser st Command
-> GenParser st Command -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "get-proof" (Command -> GenParser st Command
forall (f :: * -> *) a. Applicative f => a -> f a
pure Command
GetProof)
GenParser st Command
-> GenParser st Command -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "get-unsat-assumptions" (Command -> GenParser st Command
forall (f :: * -> *) a. Applicative f => a -> f a
pure Command
GetUnsatAssumptions)
GenParser st Command
-> GenParser st Command -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "get-unsat-core" (Command -> GenParser st Command
forall (f :: * -> *) a. Applicative f => a -> f a
pure Command
GetUnsatCore)
GenParser st Command
-> GenParser st Command -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "get-value" (NonEmpty Term -> Command
GetValue (NonEmpty Term -> Command)
-> ParsecT Text st Identity (NonEmpty Term) -> GenParser st Command
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity (NonEmpty Term)
forall st. GenParser st (NonEmpty Term)
getValue)
GenParser st Command
-> GenParser st Command -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "pop" (Text -> Command
Pop (Text -> Command)
-> ParsecT Text st Identity Text -> GenParser st Command
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text
forall st. GenParser st Text
numeral)
GenParser st Command
-> GenParser st Command -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "push" (Text -> Command
Push (Text -> Command)
-> ParsecT Text st Identity Text -> GenParser st Command
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text
forall st. GenParser st Text
numeral)
GenParser st Command
-> GenParser st Command -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "reset" (Command -> GenParser st Command
forall (f :: * -> *) a. Applicative f => a -> f a
pure Command
Reset)
GenParser st Command
-> GenParser st Command -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "reset-assertions" (Command -> GenParser st Command
forall (f :: * -> *) a. Applicative f => a -> f a
pure Command
ResetAssertions)
GenParser st Command
-> GenParser st Command -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "set-info" (Attribute -> Command
SetInfo (Attribute -> Command)
-> ParsecT Text st Identity Attribute -> GenParser st Command
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Attribute
forall st. GenParser st Attribute
attribute)
GenParser st Command
-> GenParser st Command -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "set-logic" (Text -> Command
SetLogic (Text -> Command)
-> ParsecT Text st Identity Text -> GenParser st Command
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text
forall st. GenParser st Text
symbol)
GenParser st Command
-> GenParser st Command -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st Command -> GenParser st Command
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd "set-option" (ScriptOption -> Command
SetOption (ScriptOption -> Command)
-> ParsecT Text st Identity ScriptOption -> GenParser st Command
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity ScriptOption
forall st. GenParser st ScriptOption
scriptOption)
GenParser st Command -> SourceName -> GenParser st Command
forall s u (m :: * -> *) a.
ParsecT s u m a -> SourceName -> ParsecT s u m a
<?> "command"
where
cmd :: SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
cmd s :: SourceName
s p :: ParsecT Text u Identity a
p = ParsecT Text u Identity a -> ParsecT Text u Identity a
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try (ParsecT Text u Identity a -> ParsecT Text u Identity a)
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
forall a b. (a -> b) -> a -> b
$ ParsecT Text u Identity a -> ParsecT Text u Identity a
forall st a. GenParser st a -> GenParser st a
betweenBrackets (SourceName -> GenParser u ()
forall st. SourceName -> GenParser st ()
tryStr SourceName
s GenParser u ()
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT Text u Identity a
p)
declareDatatypes :: ParsecT Text st Identity Command
declareDatatypes = do
NonEmpty SortDec
sds <- GenParser st (NonEmpty SortDec) -> GenParser st (NonEmpty SortDec)
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st (NonEmpty SortDec)
-> GenParser st (NonEmpty SortDec))
-> GenParser st (NonEmpty SortDec)
-> GenParser st (NonEmpty SortDec)
forall a b. (a -> b) -> a -> b
$ GenParser st SortDec -> GenParser st (NonEmpty SortDec)
forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepSpace1 GenParser st SortDec
forall st. GenParser st SortDec
sortDec
ParsecT Text st Identity ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces
NonEmpty DatatypeDec
dds <- GenParser st (NonEmpty DatatypeDec)
-> GenParser st (NonEmpty DatatypeDec)
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st (NonEmpty DatatypeDec)
-> GenParser st (NonEmpty DatatypeDec))
-> GenParser st (NonEmpty DatatypeDec)
-> GenParser st (NonEmpty DatatypeDec)
forall a b. (a -> b) -> a -> b
$ GenParser st DatatypeDec -> GenParser st (NonEmpty DatatypeDec)
forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepSpace1 GenParser st DatatypeDec
forall st. GenParser st DatatypeDec
datatypeDec
if NonEmpty SortDec -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length NonEmpty SortDec
sds Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== NonEmpty DatatypeDec -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length NonEmpty DatatypeDec
dds
then Command -> ParsecT Text st Identity Command
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Command -> ParsecT Text st Identity Command)
-> Command -> ParsecT Text st Identity Command
forall a b. (a -> b) -> a -> b
$ NonEmpty SortDec -> NonEmpty DatatypeDec -> Command
DeclareDatatypes NonEmpty SortDec
sds NonEmpty DatatypeDec
dds
else SourceName -> ParsecT Text st Identity Command
forall s (m :: * -> *) t u a.
Stream s m t =>
SourceName -> ParsecT s u m a
unexpected "declare-datatypes: sorts and datatypes should have same length"
declareFun :: ParsecT Text st Identity Command
declareFun = do
Text
s <- GenParser st Text
forall st. GenParser st Text
symbol GenParser st Text
-> ParsecT Text st Identity () -> GenParser st Text
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1
[Sort]
ss <- GenParser st [Sort] -> GenParser st [Sort]
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st [Sort] -> GenParser st [Sort])
-> GenParser st [Sort] -> GenParser st [Sort]
forall a b. (a -> b) -> a -> b
$ GenParser st Sort -> GenParser st [Sort]
forall st a. GenParser st a -> GenParser st [a]
sepSpace GenParser st Sort
forall st. GenParser st Sort
sort
ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1
Text -> [Sort] -> Sort -> Command
DeclareFun Text
s [Sort]
ss (Sort -> Command)
-> GenParser st Sort -> ParsecT Text st Identity Command
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenParser st Sort
forall st. GenParser st Sort
sort
declareSort :: ParsecT Text st Identity Command
declareSort = do
Text
s <- GenParser st Text
forall st. GenParser st Text
symbol GenParser st Text
-> ParsecT Text st Identity () -> GenParser st Text
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1
Text -> Text -> Command
DeclareSort Text
s (Text -> Command)
-> GenParser st Text -> ParsecT Text st Identity Command
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenParser st Text
forall st. GenParser st Text
numeral
defineFunsRec :: ParsecT Text st Identity Command
defineFunsRec = do
NonEmpty FunctionDec
fds <- GenParser st (NonEmpty FunctionDec)
-> GenParser st (NonEmpty FunctionDec)
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st (NonEmpty FunctionDec)
-> GenParser st (NonEmpty FunctionDec))
-> GenParser st (NonEmpty FunctionDec)
-> GenParser st (NonEmpty FunctionDec)
forall a b. (a -> b) -> a -> b
$ GenParser st FunctionDec -> GenParser st (NonEmpty FunctionDec)
forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepSpace1 GenParser st FunctionDec
forall st. GenParser st FunctionDec
functionDec
ParsecT Text st Identity ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces
NonEmpty Term
ts <- GenParser st (NonEmpty Term) -> GenParser st (NonEmpty Term)
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st (NonEmpty Term) -> GenParser st (NonEmpty Term))
-> GenParser st (NonEmpty Term) -> GenParser st (NonEmpty Term)
forall a b. (a -> b) -> a -> b
$ GenParser st Term -> GenParser st (NonEmpty Term)
forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepSpace1 GenParser st Term
forall st. GenParser st Term
term
if NonEmpty FunctionDec -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length NonEmpty FunctionDec
fds Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== NonEmpty Term -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length NonEmpty Term
ts
then Command -> ParsecT Text st Identity Command
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Command -> ParsecT Text st Identity Command)
-> Command -> ParsecT Text st Identity Command
forall a b. (a -> b) -> a -> b
$ NonEmpty FunctionDec -> NonEmpty Term -> Command
DefineFunsRec NonEmpty FunctionDec
fds NonEmpty Term
ts
else SourceName -> ParsecT Text st Identity Command
forall s (m :: * -> *) t u a.
Stream s m t =>
SourceName -> ParsecT s u m a
unexpected "define-funs-rec: declarations and terms should have same length"
defineSort :: ParsecT Text st Identity Command
defineSort = do
Text
s <- GenParser st Text
forall st. GenParser st Text
symbol GenParser st Text
-> ParsecT Text st Identity () -> GenParser st Text
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1
[Text]
ss <- GenParser st [Text] -> GenParser st [Text]
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st [Text] -> GenParser st [Text])
-> GenParser st [Text] -> GenParser st [Text]
forall a b. (a -> b) -> a -> b
$ GenParser st Text -> GenParser st [Text]
forall st a. GenParser st a -> GenParser st [a]
sepSpace GenParser st Text
forall st. GenParser st Text
symbol
ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1
Text -> [Text] -> Sort -> Command
DefineSort Text
s [Text]
ss (Sort -> Command)
-> ParsecT Text st Identity Sort
-> ParsecT Text st Identity Command
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Sort
forall st. GenParser st Sort
sort
getValue :: GenParser st (NonEmpty Term)
getValue = GenParser st (NonEmpty Term) -> GenParser st (NonEmpty Term)
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st (NonEmpty Term) -> GenParser st (NonEmpty Term))
-> GenParser st (NonEmpty Term) -> GenParser st (NonEmpty Term)
forall a b. (a -> b) -> a -> b
$ GenParser st Term -> GenParser st (NonEmpty Term)
forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepSpace1 GenParser st Term
forall st. GenParser st Term
term
script :: GenParser st Script
script :: GenParser st Script
script = ParsecT Text st Identity ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces ParsecT Text st Identity ()
-> GenParser st Script -> GenParser st Script
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> GenParser st Command -> GenParser st Script
forall st a. GenParser st a -> GenParser st [a]
sepOptSpace GenParser st Command
forall st. ParsecT Text st Identity Command
command GenParser st Script
-> ParsecT Text st Identity () -> GenParser st Script
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces
bValue :: GenParser st BValue
bValue :: GenParser st BValue
bValue =
SourceName -> ParsecT Text st Identity SourceName
forall s (m :: * -> *) u.
Stream s m Char =>
SourceName -> ParsecT s u m SourceName
string "true" ParsecT Text st Identity SourceName
-> BValue -> GenParser st BValue
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> BValue
BTrue
GenParser st BValue -> GenParser st BValue -> GenParser st BValue
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> ParsecT Text st Identity SourceName
forall s (m :: * -> *) u.
Stream s m Char =>
SourceName -> ParsecT s u m SourceName
string "false" ParsecT Text st Identity SourceName
-> BValue -> GenParser st BValue
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> BValue
BFalse
GenParser st BValue -> SourceName -> GenParser st BValue
forall s u (m :: * -> *) a.
ParsecT s u m a -> SourceName -> ParsecT s u m a
<?> "bool value"
scriptOption :: GenParser st ScriptOption
scriptOption :: GenParser st ScriptOption
scriptOption =
Text -> ScriptOption
DiagnosticOutputChannel (Text -> ScriptOption)
-> ParsecT Text st Identity Text -> GenParser st ScriptOption
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SourceName
-> ParsecT Text st Identity Text -> ParsecT Text st Identity Text
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
opt "diagnostic-output-channel" ParsecT Text st Identity Text
forall st. GenParser st Text
stringLiteral
GenParser st ScriptOption
-> GenParser st ScriptOption -> GenParser st ScriptOption
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> BValue -> ScriptOption
GlobalDeclarations (BValue -> ScriptOption)
-> ParsecT Text st Identity BValue -> GenParser st ScriptOption
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SourceName -> ParsecT Text st Identity BValue
forall st. SourceName -> ParsecT Text st Identity BValue
optB "global-declarations"
GenParser st ScriptOption
-> GenParser st ScriptOption -> GenParser st ScriptOption
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> BValue -> ScriptOption
InteractiveMode (BValue -> ScriptOption)
-> ParsecT Text st Identity BValue -> GenParser st ScriptOption
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SourceName -> ParsecT Text st Identity BValue
forall st. SourceName -> ParsecT Text st Identity BValue
optB "interactive-mode"
GenParser st ScriptOption
-> GenParser st ScriptOption -> GenParser st ScriptOption
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> BValue -> ScriptOption
PrintSuccess (BValue -> ScriptOption)
-> ParsecT Text st Identity BValue -> GenParser st ScriptOption
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SourceName -> ParsecT Text st Identity BValue
forall st. SourceName -> ParsecT Text st Identity BValue
optB "print-success"
GenParser st ScriptOption
-> GenParser st ScriptOption -> GenParser st ScriptOption
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> BValue -> ScriptOption
ProduceAssertions (BValue -> ScriptOption)
-> ParsecT Text st Identity BValue -> GenParser st ScriptOption
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SourceName -> ParsecT Text st Identity BValue
forall st. SourceName -> ParsecT Text st Identity BValue
optB "produce-assertions"
GenParser st ScriptOption
-> GenParser st ScriptOption -> GenParser st ScriptOption
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> BValue -> ScriptOption
ProduceAssignments (BValue -> ScriptOption)
-> ParsecT Text st Identity BValue -> GenParser st ScriptOption
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SourceName -> ParsecT Text st Identity BValue
forall st. SourceName -> ParsecT Text st Identity BValue
optB "produce-assignments"
GenParser st ScriptOption
-> GenParser st ScriptOption -> GenParser st ScriptOption
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> BValue -> ScriptOption
ProduceModels (BValue -> ScriptOption)
-> ParsecT Text st Identity BValue -> GenParser st ScriptOption
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SourceName -> ParsecT Text st Identity BValue
forall st. SourceName -> ParsecT Text st Identity BValue
optB "produce-models"
GenParser st ScriptOption
-> GenParser st ScriptOption -> GenParser st ScriptOption
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> BValue -> ScriptOption
ProduceProofs (BValue -> ScriptOption)
-> ParsecT Text st Identity BValue -> GenParser st ScriptOption
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SourceName -> ParsecT Text st Identity BValue
forall st. SourceName -> ParsecT Text st Identity BValue
optB "produce-proofs"
GenParser st ScriptOption
-> GenParser st ScriptOption -> GenParser st ScriptOption
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> BValue -> ScriptOption
ProduceUnsatAssumptions (BValue -> ScriptOption)
-> ParsecT Text st Identity BValue -> GenParser st ScriptOption
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SourceName -> ParsecT Text st Identity BValue
forall st. SourceName -> ParsecT Text st Identity BValue
optB "produce-unsat-assumptions"
GenParser st ScriptOption
-> GenParser st ScriptOption -> GenParser st ScriptOption
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> BValue -> ScriptOption
ProduceUnsatCores (BValue -> ScriptOption)
-> ParsecT Text st Identity BValue -> GenParser st ScriptOption
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SourceName -> ParsecT Text st Identity BValue
forall st. SourceName -> ParsecT Text st Identity BValue
optB "produce-unsat-cores"
GenParser st ScriptOption
-> GenParser st ScriptOption -> GenParser st ScriptOption
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Text -> ScriptOption
RandomSeed (Text -> ScriptOption)
-> ParsecT Text st Identity Text -> GenParser st ScriptOption
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SourceName
-> ParsecT Text st Identity Text -> ParsecT Text st Identity Text
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
opt "random-seed" ParsecT Text st Identity Text
forall st. GenParser st Text
numeral
GenParser st ScriptOption
-> GenParser st ScriptOption -> GenParser st ScriptOption
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Text -> ScriptOption
RegularOutputChannel (Text -> ScriptOption)
-> ParsecT Text st Identity Text -> GenParser st ScriptOption
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SourceName
-> ParsecT Text st Identity Text -> ParsecT Text st Identity Text
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
opt "regular-output-channel" ParsecT Text st Identity Text
forall st. GenParser st Text
stringLiteral
GenParser st ScriptOption
-> GenParser st ScriptOption -> GenParser st ScriptOption
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Text -> ScriptOption
ReproducibleResourceLimit (Text -> ScriptOption)
-> ParsecT Text st Identity Text -> GenParser st ScriptOption
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SourceName
-> ParsecT Text st Identity Text -> ParsecT Text st Identity Text
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
opt "reproducible-resource-limit" ParsecT Text st Identity Text
forall st. GenParser st Text
numeral
GenParser st ScriptOption
-> GenParser st ScriptOption -> GenParser st ScriptOption
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Text -> ScriptOption
Verbosity (Text -> ScriptOption)
-> ParsecT Text st Identity Text -> GenParser st ScriptOption
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SourceName
-> ParsecT Text st Identity Text -> ParsecT Text st Identity Text
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
opt "verbosity" ParsecT Text st Identity Text
forall st. GenParser st Text
numeral
GenParser st ScriptOption
-> GenParser st ScriptOption -> GenParser st ScriptOption
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Attribute -> ScriptOption
OptionAttr (Attribute -> ScriptOption)
-> ParsecT Text st Identity Attribute -> GenParser st ScriptOption
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Attribute
forall st. GenParser st Attribute
attribute
GenParser st ScriptOption
-> SourceName -> GenParser st ScriptOption
forall s u (m :: * -> *) a.
ParsecT s u m a -> SourceName -> ParsecT s u m a
<?> "script option"
where
opt :: SourceName
-> ParsecT Text st Identity b -> ParsecT Text st Identity b
opt s :: SourceName
s p :: ParsecT Text st Identity b
p = SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryAttr SourceName
s GenParser st () -> GenParser st () -> GenParser st ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> GenParser st ()
forall st. GenParser st ()
spaces1 GenParser st ()
-> ParsecT Text st Identity b -> ParsecT Text st Identity b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT Text st Identity b
p
optB :: SourceName -> ParsecT Text st Identity BValue
optB s :: SourceName
s = SourceName
-> ParsecT Text st Identity BValue
-> ParsecT Text st Identity BValue
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
opt SourceName
s ParsecT Text st Identity BValue
forall st. GenParser st BValue
bValue
infoFlag :: GenParser st InfoFlag
infoFlag :: GenParser st InfoFlag
infoFlag =
SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryAttr "all-statistics" GenParser st () -> InfoFlag -> GenParser st InfoFlag
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> InfoFlag
AllStatistics
GenParser st InfoFlag
-> GenParser st InfoFlag -> GenParser st InfoFlag
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryAttr "assertion-stack-levels" GenParser st () -> InfoFlag -> GenParser st InfoFlag
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> InfoFlag
AssertionStackLevels
GenParser st InfoFlag
-> GenParser st InfoFlag -> GenParser st InfoFlag
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryAttr "authors" GenParser st () -> InfoFlag -> GenParser st InfoFlag
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> InfoFlag
Authors
GenParser st InfoFlag
-> GenParser st InfoFlag -> GenParser st InfoFlag
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryAttr "error-behavior" GenParser st () -> InfoFlag -> GenParser st InfoFlag
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> InfoFlag
ErrorBehavior
GenParser st InfoFlag
-> GenParser st InfoFlag -> GenParser st InfoFlag
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryAttr "name" GenParser st () -> InfoFlag -> GenParser st InfoFlag
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> InfoFlag
Name
GenParser st InfoFlag
-> GenParser st InfoFlag -> GenParser st InfoFlag
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryAttr "reason-unknown" GenParser st () -> InfoFlag -> GenParser st InfoFlag
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> InfoFlag
ReasonUnknown
GenParser st InfoFlag
-> GenParser st InfoFlag -> GenParser st InfoFlag
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryAttr "version" GenParser st () -> InfoFlag -> GenParser st InfoFlag
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> InfoFlag
Version
GenParser st InfoFlag
-> GenParser st InfoFlag -> GenParser st InfoFlag
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Text -> InfoFlag
IFKeyword (Text -> InfoFlag)
-> ParsecT Text st Identity Text -> GenParser st InfoFlag
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text
forall st. GenParser st Text
keyword
GenParser st InfoFlag -> SourceName -> GenParser st InfoFlag
forall s u (m :: * -> *) a.
ParsecT s u m a -> SourceName -> ParsecT s u m a
<?> "info flag"
genRes :: SpecificSuccessRes res => GenParser st (GeneralRes res)
genRes :: GenParser st (GeneralRes res)
genRes =
SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryStr "success" GenParser st () -> GeneralRes res -> GenParser st (GeneralRes res)
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> GeneralRes res
forall res. GeneralRes res
ResSuccess
GenParser st (GeneralRes res)
-> GenParser st (GeneralRes res) -> GenParser st (GeneralRes res)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> res -> GeneralRes res
forall res. res -> GeneralRes res
ResSpecific (res -> GeneralRes res)
-> ParsecT Text st Identity res -> GenParser st (GeneralRes res)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity res
forall s st. SpecificSuccessRes s => GenParser st s
specificSuccessRes
GenParser st (GeneralRes res)
-> GenParser st (GeneralRes res) -> GenParser st (GeneralRes res)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryStr "unsupported" GenParser st () -> GeneralRes res -> GenParser st (GeneralRes res)
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> GeneralRes res
forall res. GeneralRes res
ResUnsupported
GenParser st (GeneralRes res)
-> GenParser st (GeneralRes res) -> GenParser st (GeneralRes res)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Text -> GeneralRes res
forall res. Text -> GeneralRes res
ResError (Text -> GeneralRes res)
-> ParsecT Text st Identity Text -> GenParser st (GeneralRes res)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Text -> ParsecT Text st Identity Text
forall st a. GenParser st a -> GenParser st a
betweenBrackets (SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryStr "error" GenParser st () -> GenParser st () -> GenParser st ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> GenParser st ()
forall st. GenParser st ()
spaces1 GenParser st ()
-> ParsecT Text st Identity Text -> ParsecT Text st Identity Text
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT Text st Identity Text
forall st. GenParser st Text
stringLiteral)
resErrorBehaviour :: GenParser st ResErrorBehavior
resErrorBehaviour :: GenParser st ResErrorBehavior
resErrorBehaviour =
SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryStr "immediate-exit" GenParser st ()
-> ResErrorBehavior -> GenParser st ResErrorBehavior
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> ResErrorBehavior
ImmediateExit
GenParser st ResErrorBehavior
-> GenParser st ResErrorBehavior -> GenParser st ResErrorBehavior
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryStr "continued-execution" GenParser st ()
-> ResErrorBehavior -> GenParser st ResErrorBehavior
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> ResErrorBehavior
ContinuedExecution
GenParser st ResErrorBehavior
-> SourceName -> GenParser st ResErrorBehavior
forall s u (m :: * -> *) a.
ParsecT s u m a -> SourceName -> ParsecT s u m a
<?> "response error behavior"
resReasonUnknown :: GenParser st ResReasonUnknown
resReasonUnknown :: GenParser st ResReasonUnknown
resReasonUnknown =
SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryStr "memout" GenParser st ()
-> ResReasonUnknown -> GenParser st ResReasonUnknown
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> ResReasonUnknown
Memout
GenParser st ResReasonUnknown
-> GenParser st ResReasonUnknown -> GenParser st ResReasonUnknown
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryStr "incomplete" GenParser st ()
-> ResReasonUnknown -> GenParser st ResReasonUnknown
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> ResReasonUnknown
Incomplete
GenParser st ResReasonUnknown
-> SourceName -> GenParser st ResReasonUnknown
forall s u (m :: * -> *) a.
ParsecT s u m a -> SourceName -> ParsecT s u m a
<?> "response reason unknown"
resModel :: GenParser st ResModel
resModel :: GenParser st ResModel
resModel =
SourceName -> GenParser st ResModel -> GenParser st ResModel
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
def "define-fun" (FunctionDef -> ResModel
RMDefineFun (FunctionDef -> ResModel)
-> ParsecT Text st Identity FunctionDef -> GenParser st ResModel
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity FunctionDef
forall st. GenParser st FunctionDef
functionDef)
GenParser st ResModel
-> GenParser st ResModel -> GenParser st ResModel
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st ResModel -> GenParser st ResModel
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
def "define-fun-rec" (FunctionDef -> ResModel
RMDefineFunRec (FunctionDef -> ResModel)
-> ParsecT Text st Identity FunctionDef -> GenParser st ResModel
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity FunctionDef
forall st. GenParser st FunctionDef
functionDef)
GenParser st ResModel
-> GenParser st ResModel -> GenParser st ResModel
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st ResModel -> GenParser st ResModel
forall u a.
SourceName
-> ParsecT Text u Identity a -> ParsecT Text u Identity a
def "define-funs-rec" GenParser st ResModel
forall st. ParsecT Text st Identity ResModel
rMDefineFunsRec
where
def :: SourceName
-> ParsecT Text st Identity a -> ParsecT Text st Identity a
def s :: SourceName
s p :: ParsecT Text st Identity a
p = ParsecT Text st Identity a -> ParsecT Text st Identity a
forall st a. GenParser st a -> GenParser st a
betweenBrackets (ParsecT Text st Identity a -> ParsecT Text st Identity a)
-> ParsecT Text st Identity a -> ParsecT Text st Identity a
forall a b. (a -> b) -> a -> b
$ SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryStr SourceName
s GenParser st ()
-> ParsecT Text st Identity a -> ParsecT Text st Identity a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT Text st Identity a
p
rMDefineFunsRec :: ParsecT Text st Identity ResModel
rMDefineFunsRec = do
NonEmpty FunctionDec
fdcs <- GenParser st (NonEmpty FunctionDec)
-> GenParser st (NonEmpty FunctionDec)
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st (NonEmpty FunctionDec)
-> GenParser st (NonEmpty FunctionDec))
-> GenParser st (NonEmpty FunctionDec)
-> GenParser st (NonEmpty FunctionDec)
forall a b. (a -> b) -> a -> b
$ GenParser st FunctionDec -> GenParser st (NonEmpty FunctionDec)
forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepSpace1 GenParser st FunctionDec
forall st. GenParser st FunctionDec
functionDec
ParsecT Text st Identity ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces
NonEmpty Term
ts <- GenParser st (NonEmpty Term) -> GenParser st (NonEmpty Term)
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st (NonEmpty Term) -> GenParser st (NonEmpty Term))
-> GenParser st (NonEmpty Term) -> GenParser st (NonEmpty Term)
forall a b. (a -> b) -> a -> b
$ GenParser st Term -> GenParser st (NonEmpty Term)
forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepSpace1 GenParser st Term
forall st. GenParser st Term
term
if NonEmpty FunctionDec -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length NonEmpty FunctionDec
fdcs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== NonEmpty Term -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length NonEmpty Term
ts
then ResModel -> ParsecT Text st Identity ResModel
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ResModel -> ParsecT Text st Identity ResModel)
-> ResModel -> ParsecT Text st Identity ResModel
forall a b. (a -> b) -> a -> b
$ NonEmpty FunctionDec -> NonEmpty Term -> ResModel
RMDefineFunsRec NonEmpty FunctionDec
fdcs NonEmpty Term
ts
else SourceName -> ParsecT Text st Identity ResModel
forall s (m :: * -> *) t u a.
Stream s m t =>
SourceName -> ParsecT s u m a
unexpected "get-model response, declarations and terms should have same length"
instance SpecificSuccessRes ResModel where
specificSuccessRes :: GenParser st ResModel
specificSuccessRes = GenParser st ResModel
forall st. ParsecT Text st Identity ResModel
resModel
tValuationPair :: GenParser st TValuationPair
tValuationPair :: GenParser st TValuationPair
tValuationPair = GenParser st TValuationPair -> GenParser st TValuationPair
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st TValuationPair -> GenParser st TValuationPair)
-> GenParser st TValuationPair -> GenParser st TValuationPair
forall a b. (a -> b) -> a -> b
$ do
Text
s <- GenParser st Text
forall st. GenParser st Text
symbol GenParser st Text
-> ParsecT Text st Identity () -> GenParser st Text
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1
BValue
b <- GenParser st BValue
forall st. GenParser st BValue
bValue
TValuationPair -> GenParser st TValuationPair
forall (m :: * -> *) a. Monad m => a -> m a
return (Text
s, BValue
b)
resCheckSat :: GenParser st ResCheckSat
resCheckSat :: GenParser st ResCheckSat
resCheckSat =
SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryStr "sat" GenParser st () -> ResCheckSat -> GenParser st ResCheckSat
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> ResCheckSat
Sat
GenParser st ResCheckSat
-> GenParser st ResCheckSat -> GenParser st ResCheckSat
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryStr "unsat" GenParser st () -> ResCheckSat -> GenParser st ResCheckSat
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> ResCheckSat
Unsat
GenParser st ResCheckSat
-> GenParser st ResCheckSat -> GenParser st ResCheckSat
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryStr "unknown" GenParser st () -> ResCheckSat -> GenParser st ResCheckSat
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> ResCheckSat
Unknown
instance SpecificSuccessRes ResCheckSat where
specificSuccessRes :: GenParser st ResCheckSat
specificSuccessRes = GenParser st ResCheckSat
forall st. GenParser st ResCheckSat
resCheckSat
resInfo :: GenParser st ResInfo
resInfo :: GenParser st ResInfo
resInfo =
ResErrorBehavior -> ResInfo
IRErrorBehaviour (ResErrorBehavior -> ResInfo)
-> ParsecT Text st Identity ResErrorBehavior
-> GenParser st ResInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryAttr "error-behavior" GenParser st ()
-> ParsecT Text st Identity ResErrorBehavior
-> ParsecT Text st Identity ResErrorBehavior
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT Text st Identity ResErrorBehavior
forall st. GenParser st ResErrorBehavior
resErrorBehaviour)
GenParser st ResInfo
-> GenParser st ResInfo -> GenParser st ResInfo
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Text -> ResInfo
IRName (Text -> ResInfo)
-> ParsecT Text st Identity Text -> GenParser st ResInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryAttr "name" GenParser st ()
-> ParsecT Text st Identity Text -> ParsecT Text st Identity Text
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT Text st Identity Text
forall st. GenParser st Text
stringLiteral)
GenParser st ResInfo
-> GenParser st ResInfo -> GenParser st ResInfo
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Text -> ResInfo
IRAuthours (Text -> ResInfo)
-> ParsecT Text st Identity Text -> GenParser st ResInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryAttr "authors" GenParser st ()
-> ParsecT Text st Identity Text -> ParsecT Text st Identity Text
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT Text st Identity Text
forall st. GenParser st Text
stringLiteral)
GenParser st ResInfo
-> GenParser st ResInfo -> GenParser st ResInfo
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Text -> ResInfo
IRVersion (Text -> ResInfo)
-> ParsecT Text st Identity Text -> GenParser st ResInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryAttr "version" GenParser st ()
-> ParsecT Text st Identity Text -> ParsecT Text st Identity Text
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT Text st Identity Text
forall st. GenParser st Text
stringLiteral)
GenParser st ResInfo
-> GenParser st ResInfo -> GenParser st ResInfo
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ResReasonUnknown -> ResInfo
IRReasonUnknown (ResReasonUnknown -> ResInfo)
-> ParsecT Text st Identity ResReasonUnknown
-> GenParser st ResInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SourceName -> GenParser st ()
forall st. SourceName -> GenParser st ()
tryAttr "reason-unknown" GenParser st ()
-> ParsecT Text st Identity ResReasonUnknown
-> ParsecT Text st Identity ResReasonUnknown
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT Text st Identity ResReasonUnknown
forall st. GenParser st ResReasonUnknown
resReasonUnknown)
GenParser st ResInfo
-> GenParser st ResInfo -> GenParser st ResInfo
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Attribute -> ResInfo
IRAttr (Attribute -> ResInfo)
-> ParsecT Text st Identity Attribute -> GenParser st ResInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Text st Identity Attribute
forall st. GenParser st Attribute
attribute
instance SpecificSuccessRes (NonEmpty ResInfo) where
specificSuccessRes :: GenParser st (NonEmpty ResInfo)
specificSuccessRes = GenParser st (NonEmpty ResInfo) -> GenParser st (NonEmpty ResInfo)
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st (NonEmpty ResInfo)
-> GenParser st (NonEmpty ResInfo))
-> GenParser st (NonEmpty ResInfo)
-> GenParser st (NonEmpty ResInfo)
forall a b. (a -> b) -> a -> b
$ GenParser st ResInfo -> GenParser st (NonEmpty ResInfo)
forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepSpace1 GenParser st ResInfo
forall st. GenParser st ResInfo
resInfo
checkSatRes :: GenParser st CheckSatRes
checkSatRes :: GenParser st CheckSatRes
checkSatRes = GenParser st CheckSatRes
forall res st.
SpecificSuccessRes res =>
GenParser st (GeneralRes res)
genRes
instance SpecificSuccessRes StringLiteral where
specificSuccessRes :: GenParser st Text
specificSuccessRes = GenParser st Text
forall st. GenParser st Text
stringLiteral
echoRes :: GenParser st EchoRes
echoRes :: GenParser st EchoRes
echoRes = GenParser st EchoRes
forall res st.
SpecificSuccessRes res =>
GenParser st (GeneralRes res)
genRes
instance SpecificSuccessRes [Term] where
specificSuccessRes :: GenParser st [Term]
specificSuccessRes = GenParser st [Term] -> GenParser st [Term]
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st [Term] -> GenParser st [Term])
-> GenParser st [Term] -> GenParser st [Term]
forall a b. (a -> b) -> a -> b
$ GenParser st Term -> GenParser st [Term]
forall st a. GenParser st a -> GenParser st [a]
sepSpace GenParser st Term
forall st. GenParser st Term
term
getAssertionsRes :: GenParser st GetAssertionsRes
getAssertionsRes :: GenParser st GetAssertionsRes
getAssertionsRes = GenParser st GetAssertionsRes
forall res st.
SpecificSuccessRes res =>
GenParser st (GeneralRes res)
genRes
instance SpecificSuccessRes [TValuationPair] where
specificSuccessRes :: GenParser st [TValuationPair]
specificSuccessRes = GenParser st [TValuationPair] -> GenParser st [TValuationPair]
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st [TValuationPair] -> GenParser st [TValuationPair])
-> GenParser st [TValuationPair] -> GenParser st [TValuationPair]
forall a b. (a -> b) -> a -> b
$ GenParser st TValuationPair -> GenParser st [TValuationPair]
forall st a. GenParser st a -> GenParser st [a]
sepSpace GenParser st TValuationPair
forall st. GenParser st TValuationPair
tValuationPair
getAssignmentRes :: GenParser st GetAssignmentRes
getAssignmentRes :: GenParser st GetAssignmentRes
getAssignmentRes = GenParser st GetAssignmentRes
forall res st.
SpecificSuccessRes res =>
GenParser st (GeneralRes res)
genRes
getInfoRes :: GenParser st GetInfoRes
getInfoRes :: GenParser st GetInfoRes
getInfoRes = GenParser st GetInfoRes
forall res st.
SpecificSuccessRes res =>
GenParser st (GeneralRes res)
genRes
getModelRes :: GenParser st GetModelRes
getModelRes :: GenParser st GetModelRes
getModelRes = GenParser st GetModelRes
forall res st.
SpecificSuccessRes res =>
GenParser st (GeneralRes res)
genRes
instance SpecificSuccessRes AttributeValue where
specificSuccessRes :: GenParser st AttributeValue
specificSuccessRes = GenParser st AttributeValue
forall st. GenParser st AttributeValue
attributeValue
getOptionRes :: GenParser st GetOptionRes
getOptionRes :: GenParser st GetOptionRes
getOptionRes = GenParser st GetOptionRes
forall res st.
SpecificSuccessRes res =>
GenParser st (GeneralRes res)
genRes
instance SpecificSuccessRes SExpr where
specificSuccessRes :: GenParser st SExpr
specificSuccessRes = GenParser st SExpr
forall st. GenParser st SExpr
sexpr
getProofRes :: GenParser st GetProofRes
getProofRes :: GenParser st GetProofRes
getProofRes = GenParser st GetProofRes
forall res st.
SpecificSuccessRes res =>
GenParser st (GeneralRes res)
genRes
instance SpecificSuccessRes [Symbol] where
specificSuccessRes :: GenParser st [Text]
specificSuccessRes = GenParser st [Text] -> GenParser st [Text]
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st [Text] -> GenParser st [Text])
-> GenParser st [Text] -> GenParser st [Text]
forall a b. (a -> b) -> a -> b
$ GenParser st Text -> GenParser st [Text]
forall st a. GenParser st a -> GenParser st [a]
sepSpace GenParser st Text
forall st. GenParser st Text
symbol
getUnsatAssumpRes :: GenParser st GetUnsatAssumpRes
getUnsatAssumpRes :: GenParser st GetUnsatAssumpRes
getUnsatAssumpRes = GenParser st GetUnsatAssumpRes
forall res st.
SpecificSuccessRes res =>
GenParser st (GeneralRes res)
genRes
getUnsatCoreRes :: GenParser st GetUnsatCoreRes
getUnsatCoreRes :: GenParser st GetUnsatAssumpRes
getUnsatCoreRes = GenParser st GetUnsatAssumpRes
forall res st.
SpecificSuccessRes res =>
GenParser st (GeneralRes res)
genRes
valuationPair :: GenParser st ValuationPair
valuationPair :: GenParser st ValuationPair
valuationPair = GenParser st ValuationPair -> GenParser st ValuationPair
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st ValuationPair -> GenParser st ValuationPair)
-> GenParser st ValuationPair -> GenParser st ValuationPair
forall a b. (a -> b) -> a -> b
$ do
Term
t1 <- GenParser st Term
forall st. GenParser st Term
term GenParser st Term
-> ParsecT Text st Identity () -> GenParser st Term
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Text st Identity ()
forall st. GenParser st ()
spaces1
Term
t2 <- GenParser st Term
forall st. GenParser st Term
term
ValuationPair -> GenParser st ValuationPair
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
t1, Term
t2)
instance SpecificSuccessRes (NonEmpty ValuationPair) where
specificSuccessRes :: GenParser st (NonEmpty ValuationPair)
specificSuccessRes = GenParser st (NonEmpty ValuationPair)
-> GenParser st (NonEmpty ValuationPair)
forall st a. GenParser st a -> GenParser st a
betweenBrackets (GenParser st (NonEmpty ValuationPair)
-> GenParser st (NonEmpty ValuationPair))
-> GenParser st (NonEmpty ValuationPair)
-> GenParser st (NonEmpty ValuationPair)
forall a b. (a -> b) -> a -> b
$ GenParser st ValuationPair -> GenParser st (NonEmpty ValuationPair)
forall st a. GenParser st a -> GenParser st (NonEmpty a)
sepSpace1 GenParser st ValuationPair
forall st. GenParser st ValuationPair
valuationPair
getValueRes :: GenParser st GetValueRes
getValueRes :: GenParser st GetValueRes
getValueRes = GenParser st GetValueRes
forall res st.
SpecificSuccessRes res =>
GenParser st (GeneralRes res)
genRes