{-|
This module defines types and operations for parsing results from SMTLIB2.

It does not depend on the rest of What4 so that it can be used
directly by clients interested in generating SMTLIB without depending
on the What4 formula interface.  All the type constructors are exposed
so that clients can generate new values that are not exposed through
this interface.
-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TemplateHaskell #-}
module What4.Protocol.SMTLib2.Parse
  ( -- * CheckSatResponse
    CheckSatResponse(..)
  , readCheckSatResponse
    -- * GetModelResonse
  , GetModelResponse
  , readGetModelResponse
  , ModelResponse(..)
  , DefineFun(..)
  , Symbol
    -- ** Sorts
  , Sort(..)
  , pattern Bool
  , pattern Int
  , pattern Real
  , pattern RoundingMode
  , pattern Array
    -- ** Terms
  , Term(..)
  ) where

#if !MIN_VERSION_base(4,13,0)
import Control.Monad.Fail( MonadFail )
import qualified Control.Monad.Fail
#endif

import           Control.Monad.Reader
import qualified Data.ByteString as BS
import qualified Data.ByteString.UTF8 as UTF8
import           Data.Char
import           Data.HashSet (HashSet)
import qualified Data.HashSet as HSet
import           Data.Ratio
import           Data.String
import           Data.Word
import           System.IO

c2b :: Char -> Word8
c2b :: Char -> Word8
c2b = Int -> Word8
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Word8) -> (Char -> Int) -> Char -> Word8
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Int
forall a. Enum a => a -> Int
fromEnum

------------------------------------------------------------------------
-- Parser definitions

-- | A parser monad that just reads from a handle.
--
-- We use our own parser rather than Attoparsec or some other library
-- so that we can incrementally request characters.
--
-- We likely could replace this with Attoparsec by assuming that
-- SMTLIB solvers always end their output responses with newlines, or
-- feeding output one character at a time.
newtype Parser a = Parser { Parser a -> ReaderT Handle IO a
unParser :: ReaderT Handle IO a }
  deriving (a -> Parser b -> Parser a
(a -> b) -> Parser a -> Parser b
(forall a b. (a -> b) -> Parser a -> Parser b)
-> (forall a b. a -> Parser b -> Parser a) -> Functor Parser
forall a b. a -> Parser b -> Parser a
forall a b. (a -> b) -> Parser a -> Parser b
forall (f :: Type -> Type).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Parser b -> Parser a
$c<$ :: forall a b. a -> Parser b -> Parser a
fmap :: (a -> b) -> Parser a -> Parser b
$cfmap :: forall a b. (a -> b) -> Parser a -> Parser b
Functor, Functor Parser
a -> Parser a
Functor Parser
-> (forall a. a -> Parser a)
-> (forall a b. Parser (a -> b) -> Parser a -> Parser b)
-> (forall a b c.
    (a -> b -> c) -> Parser a -> Parser b -> Parser c)
-> (forall a b. Parser a -> Parser b -> Parser b)
-> (forall a b. Parser a -> Parser b -> Parser a)
-> Applicative Parser
Parser a -> Parser b -> Parser b
Parser a -> Parser b -> Parser a
Parser (a -> b) -> Parser a -> Parser b
(a -> b -> c) -> Parser a -> Parser b -> Parser c
forall a. a -> Parser a
forall a b. Parser a -> Parser b -> Parser a
forall a b. Parser a -> Parser b -> Parser b
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall a b c. (a -> b -> c) -> Parser a -> Parser b -> Parser c
forall (f :: Type -> Type).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: Parser a -> Parser b -> Parser a
$c<* :: forall a b. Parser a -> Parser b -> Parser a
*> :: Parser a -> Parser b -> Parser b
$c*> :: forall a b. Parser a -> Parser b -> Parser b
liftA2 :: (a -> b -> c) -> Parser a -> Parser b -> Parser c
$cliftA2 :: forall a b c. (a -> b -> c) -> Parser a -> Parser b -> Parser c
<*> :: Parser (a -> b) -> Parser a -> Parser b
$c<*> :: forall a b. Parser (a -> b) -> Parser a -> Parser b
pure :: a -> Parser a
$cpure :: forall a. a -> Parser a
$cp1Applicative :: Functor Parser
Applicative)

instance Monad Parser where
  Parser ReaderT Handle IO a
m >>= :: Parser a -> (a -> Parser b) -> Parser b
>>= a -> Parser b
h = ReaderT Handle IO b -> Parser b
forall a. ReaderT Handle IO a -> Parser a
Parser (ReaderT Handle IO b -> Parser b)
-> ReaderT Handle IO b -> Parser b
forall a b. (a -> b) -> a -> b
$ ReaderT Handle IO a
m ReaderT Handle IO a
-> (a -> ReaderT Handle IO b) -> ReaderT Handle IO b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= Parser b -> ReaderT Handle IO b
forall a. Parser a -> ReaderT Handle IO a
unParser (Parser b -> ReaderT Handle IO b)
-> (a -> Parser b) -> a -> ReaderT Handle IO b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Parser b
h
#if !MIN_VERSION_base(4,13,0)
  fail = Control.Monad.Fail.fail
#endif

instance MonadFail Parser where
  fail :: String -> Parser a
fail = String -> Parser a
forall a. HasCallStack => String -> a
error

runParser :: Handle -> Parser a -> IO a
runParser :: Handle -> Parser a -> IO a
runParser Handle
h (Parser ReaderT Handle IO a
f) = ReaderT Handle IO a -> Handle -> IO a
forall r (m :: Type -> Type) a. ReaderT r m a -> r -> m a
runReaderT ReaderT Handle IO a
f Handle
h

parseChar :: Parser Char
parseChar :: Parser Char
parseChar = ReaderT Handle IO Char -> Parser Char
forall a. ReaderT Handle IO a -> Parser a
Parser (ReaderT Handle IO Char -> Parser Char)
-> ReaderT Handle IO Char -> Parser Char
forall a b. (a -> b) -> a -> b
$ (Handle -> IO Char) -> ReaderT Handle IO Char
forall r (m :: Type -> Type) a. (r -> m a) -> ReaderT r m a
ReaderT ((Handle -> IO Char) -> ReaderT Handle IO Char)
-> (Handle -> IO Char) -> ReaderT Handle IO Char
forall a b. (a -> b) -> a -> b
$ Handle -> IO Char
hGetChar

-- | Peek ahead to get the next character.
peekChar :: Parser Char
peekChar :: Parser Char
peekChar = ReaderT Handle IO Char -> Parser Char
forall a. ReaderT Handle IO a -> Parser a
Parser (ReaderT Handle IO Char -> Parser Char)
-> ReaderT Handle IO Char -> Parser Char
forall a b. (a -> b) -> a -> b
$ (Handle -> IO Char) -> ReaderT Handle IO Char
forall r (m :: Type -> Type) a. (r -> m a) -> ReaderT r m a
ReaderT ((Handle -> IO Char) -> ReaderT Handle IO Char)
-> (Handle -> IO Char) -> ReaderT Handle IO Char
forall a b. (a -> b) -> a -> b
$ Handle -> IO Char
hLookAhead

dropChar :: Parser ()
dropChar :: Parser ()
dropChar = ReaderT Handle IO () -> Parser ()
forall a. ReaderT Handle IO a -> Parser a
Parser (ReaderT Handle IO () -> Parser ())
-> ReaderT Handle IO () -> Parser ()
forall a b. (a -> b) -> a -> b
$ (Handle -> IO ()) -> ReaderT Handle IO ()
forall r (m :: Type -> Type) a. (r -> m a) -> ReaderT r m a
ReaderT ((Handle -> IO ()) -> ReaderT Handle IO ())
-> (Handle -> IO ()) -> ReaderT Handle IO ()
forall a b. (a -> b) -> a -> b
$ \Handle
h -> Handle -> IO Char
hGetChar Handle
h IO Char -> IO () -> IO ()
forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> () -> IO ()
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ()

-- | Drop characters until we get a non-whitespace character.
dropWhitespace :: Parser ()
dropWhitespace :: Parser ()
dropWhitespace = do
  Char
c <- Parser Char
peekChar
  if Char -> Bool
isSpace Char
c then do
    Parser ()
dropChar Parser () -> Parser () -> Parser ()
forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> Parser ()
dropWhitespace
   else
    () -> Parser ()
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ()

-- | Drop whitespace, and if next character matches expected return,
-- otherwise fail.
matchChar :: Char -> Parser ()
matchChar :: Char -> Parser ()
matchChar Char
expected = do
  Char
c <- Parser Char
parseChar
  if Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
expected then
    () -> Parser ()
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ()
   else if Char -> Bool
isSpace Char
c then
    Char -> Parser ()
matchChar Char
expected
   else
    String -> Parser ()
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> Parser ()) -> String -> Parser ()
forall a b. (a -> b) -> a -> b
$ String
"Unexpected input char " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Char -> String
forall a. Show a => a -> String
show Char
c String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"(expected " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Char -> String
forall a. Show a => a -> String
show Char
expected String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

-- | Drop whitespace until we reach the given string.
matchString :: BS.ByteString -> Parser ()
matchString :: ByteString -> Parser ()
matchString ByteString
expected = do
  Parser ()
dropWhitespace
  ByteString
found <- ReaderT Handle IO ByteString -> Parser ByteString
forall a. ReaderT Handle IO a -> Parser a
Parser (ReaderT Handle IO ByteString -> Parser ByteString)
-> ReaderT Handle IO ByteString -> Parser ByteString
forall a b. (a -> b) -> a -> b
$ (Handle -> IO ByteString) -> ReaderT Handle IO ByteString
forall r (m :: Type -> Type) a. (r -> m a) -> ReaderT r m a
ReaderT ((Handle -> IO ByteString) -> ReaderT Handle IO ByteString)
-> (Handle -> IO ByteString) -> ReaderT Handle IO ByteString
forall a b. (a -> b) -> a -> b
$ \Handle
h -> Handle -> Int -> IO ByteString
BS.hGet Handle
h (ByteString -> Int
BS.length ByteString
expected)
  Bool -> Parser () -> Parser ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (ByteString
found ByteString -> ByteString -> Bool
forall a. Eq a => a -> a -> Bool
/= ByteString
expected) (Parser () -> Parser ()) -> Parser () -> Parser ()
forall a b. (a -> b) -> a -> b
$ do
    String -> Parser ()
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> Parser ()) -> String -> Parser ()
forall a b. (a -> b) -> a -> b
$ String
"Unexpected string " String -> String -> String
forall a. [a] -> [a] -> [a]
++ ByteString -> String
forall a. Show a => a -> String
show ByteString
found String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"(expected " String -> String -> String
forall a. [a] -> [a] -> [a]
++ ByteString -> String
forall a. Show a => a -> String
show ByteString
expected String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

parseUntilCloseParen' :: [a] -> Parser a -> Parser [a]
parseUntilCloseParen' :: [a] -> Parser a -> Parser [a]
parseUntilCloseParen' [a]
prev Parser a
p = do
  Char
c <- Parser Char
peekChar
  if Char -> Bool
isSpace Char
c then
    Parser ()
dropChar Parser () -> Parser [a] -> Parser [a]
forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> [a] -> Parser a -> Parser [a]
forall a. [a] -> Parser a -> Parser [a]
parseUntilCloseParen' [a]
prev Parser a
p
   else if Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
')' then
    Parser ()
dropChar Parser () -> Parser [a] -> Parser [a]
forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> [a] -> Parser [a]
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ([a] -> [a]
forall a. [a] -> [a]
reverse [a]
prev)
   else do
    Parser a
p Parser a -> (a -> Parser [a]) -> Parser [a]
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
n -> [a] -> Parser a -> Parser [a]
forall a. [a] -> Parser a -> Parser [a]
parseUntilCloseParen' (a
na -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
prev) Parser a
p

-- | @parseUntilCloseParen p@ will drop whitespace characters, and
-- run @p@
parseUntilCloseParen :: Parser a -> Parser [a]
parseUntilCloseParen :: Parser a -> Parser [a]
parseUntilCloseParen = [a] -> Parser a -> Parser [a]
forall a. [a] -> Parser a -> Parser [a]
parseUntilCloseParen' []

-- | @takeChars' p prev h@ prepends characters read from @h@ to @prev@
-- until @p@ is false, and returns the resulting string.
takeChars' :: (Char -> Bool) -> [Word8] -> Parser [Word8]
takeChars' :: (Char -> Bool) -> [Word8] -> Parser [Word8]
takeChars' Char -> Bool
p [Word8]
prev = do
  Char
c <- Parser Char
peekChar
  if Char -> Bool
p Char
c then do
    Char
_ <- Parser Char
parseChar
    (Char -> Bool) -> [Word8] -> Parser [Word8]
takeChars' Char -> Bool
p (Char -> Word8
c2b Char
cWord8 -> [Word8] -> [Word8]
forall a. a -> [a] -> [a]
:[Word8]
prev)
   else do
    [Word8] -> Parser [Word8]
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ([Word8] -> Parser [Word8]) -> [Word8] -> Parser [Word8]
forall a b. (a -> b) -> a -> b
$! [Word8]
prev

-- | @takeChars p@ returns the bytestring formed by reading
-- characters until @p@ is false.
takeChars :: (Char -> Bool) -> Parser BS.ByteString
takeChars :: (Char -> Bool) -> Parser ByteString
takeChars Char -> Bool
p = do
  [Word8]
l <- (Char -> Bool) -> [Word8] -> Parser [Word8]
takeChars' Char -> Bool
p []
  ByteString -> Parser ByteString
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (ByteString -> Parser ByteString)
-> ByteString -> Parser ByteString
forall a b. (a -> b) -> a -> b
$! [Word8] -> ByteString
BS.pack ([Word8] -> [Word8]
forall a. [a] -> [a]
reverse [Word8]
l)


instance IsString (Parser ()) where
  fromString :: String -> Parser ()
fromString = ByteString -> Parser ()
matchString (ByteString -> Parser ())
-> (String -> ByteString) -> String -> Parser ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ByteString
forall a. IsString a => String -> a
fromString

-- | Parse a quoted string.
parseQuotedString :: Parser String
parseQuotedString :: Parser String
parseQuotedString = do
  Char -> Parser ()
matchChar Char
'"'
  ByteString
l <- (Char -> Bool) -> Parser ByteString
takeChars (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
'"')
  Char -> Parser ()
matchChar Char
'"'
  String -> Parser String
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (String -> Parser String) -> String -> Parser String
forall a b. (a -> b) -> a -> b
$ ByteString -> String
UTF8.toString ByteString
l

-- | Defines common operations for parsing SMTLIB results.
class CanParse a where
  -- | Parser for values of this type.
  parse :: Parser a

  -- | Read from a handle.
  readFromHandle :: Handle -> IO a
  readFromHandle Handle
h = Handle -> Parser a -> IO a
forall a. Handle -> Parser a -> IO a
runParser Handle
h Parser a
forall a. CanParse a => Parser a
parse


------------------------------------------------------------------------
-- Parse check-sat definitions

-- | Result of check-sat and check-sat-assuming
data CheckSatResponse
   = SatResponse
   | UnsatResponse
   | UnknownResponse
   | CheckSatUnsupported
   | CheckSatError !String

instance CanParse CheckSatResponse where
  parse :: Parser CheckSatResponse
parse = do
    Bool
isParen <- Parser Bool
checkParen
    if Bool
isParen then do
      ByteString -> Parser ()
matchString ByteString
"error"
      Parser ()
dropWhitespace
      String
msg <- Parser String
parseQuotedString
      Parser ()
closeParen
      CheckSatResponse -> Parser CheckSatResponse
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (String -> CheckSatResponse
CheckSatError String
msg)
     else
      [(ByteString, Parser CheckSatResponse)] -> Parser CheckSatResponse
forall a. [(ByteString, Parser a)] -> Parser a
matchApp [ (ByteString
"sat",     CheckSatResponse -> Parser CheckSatResponse
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure CheckSatResponse
SatResponse)
               , (ByteString
"unsat",   CheckSatResponse -> Parser CheckSatResponse
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure CheckSatResponse
UnsatResponse)
               , (ByteString
"unknown", CheckSatResponse -> Parser CheckSatResponse
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure CheckSatResponse
UnknownResponse)
               , (ByteString
"unsupported", CheckSatResponse -> Parser CheckSatResponse
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure CheckSatResponse
CheckSatUnsupported)
               ]

-- | Read the results of a @(check-sat)@ request.
readCheckSatResponse :: Handle -> IO CheckSatResponse
readCheckSatResponse :: Handle -> IO CheckSatResponse
readCheckSatResponse = Handle -> IO CheckSatResponse
forall a. CanParse a => Handle -> IO a
readFromHandle

------------------------------------------------------------------------
-- Parse get-model definitions

-- | An SMT symbol
newtype Symbol = Symbol BS.ByteString
  deriving (Symbol -> Symbol -> Bool
(Symbol -> Symbol -> Bool)
-> (Symbol -> Symbol -> Bool) -> Eq Symbol
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Symbol -> Symbol -> Bool
$c/= :: Symbol -> Symbol -> Bool
== :: Symbol -> Symbol -> Bool
$c== :: Symbol -> Symbol -> Bool
Eq)

instance Show Symbol where
  show :: Symbol -> String
show (Symbol ByteString
s) = ByteString -> String
forall a. Show a => a -> String
show ByteString
s

instance IsString Symbol where
  fromString :: String -> Symbol
fromString = ByteString -> Symbol
Symbol (ByteString -> Symbol)
-> (String -> ByteString) -> String -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ByteString
forall a. IsString a => String -> a
fromString

symbolCharSet :: HashSet Char
symbolCharSet :: HashSet Char
symbolCharSet = String -> HashSet Char
forall a. (Eq a, Hashable a) => [a] -> HashSet a
HSet.fromList
  (String -> HashSet Char) -> String -> HashSet Char
forall a b. (a -> b) -> a -> b
$  [Char
'A'..Char
'Z']
  String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Char
'a'..Char
'z']
  String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Char
'0'..Char
'9']
  String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Char
'~', Char
'!', Char
'@', Char
'$', Char
'%', Char
'^', Char
'&', Char
'*', Char
'_', Char
'-', Char
'+', Char
'=', Char
'<', Char
'>', Char
'.', Char
'?', Char
'/']

initialSymbolCharSet :: HashSet Char
initialSymbolCharSet :: HashSet Char
initialSymbolCharSet = HashSet Char
symbolCharSet HashSet Char -> HashSet Char -> HashSet Char
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
`HSet.difference` (String -> HashSet Char
forall a. (Eq a, Hashable a) => [a] -> HashSet a
HSet.fromList [Char
'0'..Char
'9'])

generalReservedWords :: HashSet BS.ByteString
generalReservedWords :: HashSet ByteString
generalReservedWords = [ByteString] -> HashSet ByteString
forall a. (Eq a, Hashable a) => [a] -> HashSet a
HSet.fromList ([ByteString] -> HashSet ByteString)
-> [ByteString] -> HashSet ByteString
forall a b. (a -> b) -> a -> b
$
  [ ByteString
"!"
  , ByteString
"_"
  , ByteString
"as"
  , ByteString
"BINARY"
  , ByteString
"DECIMAL"
  , ByteString
"exists"
  , ByteString
"HEXADECIMAL"
  , ByteString
"forall"
  , ByteString
"let"
  , ByteString
"match"
  , ByteString
"NUMERAL"
  , ByteString
"par"
  , ByteString
"STRING"
  ]

commandNames :: HashSet BS.ByteString
commandNames :: HashSet ByteString
commandNames = [ByteString] -> HashSet ByteString
forall a. (Eq a, Hashable a) => [a] -> HashSet a
HSet.fromList ([ByteString] -> HashSet ByteString)
-> [ByteString] -> HashSet ByteString
forall a b. (a -> b) -> a -> b
$
  [ ByteString
"assert"
  , ByteString
"check-sat"
  , ByteString
"check-sat-assuming"
  , ByteString
"declare-const"
  , ByteString
"declare-datatype"
  , ByteString
"declare-datatypes"
  , ByteString
"declare-fun"
  , ByteString
"declare-sort"
  , ByteString
"define-fun"
  , ByteString
"define-fun-rec"
  , ByteString
"define-sort"
  , ByteString
"echo"
  , ByteString
"exit"
  , ByteString
"get-assertions"
  , ByteString
"get-assignment"
  , ByteString
"get-info"
  , ByteString
"get-model"
  , ByteString
"get-option"
  , ByteString
"get-proof"
  , ByteString
"get-unsat-assumptions"
  , ByteString
"get-unsat-core"
  , ByteString
"get-value"
  , ByteString
"pop"
  , ByteString
"push"
  , ByteString
"reset"
  , ByteString
"reset-assertions"
  , ByteString
"set-info"
  , ByteString
"set-logic"
  , ByteString
"set-option"
  ]

reservedWords :: HashSet BS.ByteString
reservedWords :: HashSet ByteString
reservedWords = HashSet ByteString -> HashSet ByteString -> HashSet ByteString
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
HSet.union HashSet ByteString
generalReservedWords HashSet ByteString
commandNames

instance CanParse Symbol where
  parse :: Parser Symbol
parse = do
    Parser ()
dropWhitespace
    Char
c0 <- Parser Char
peekChar
    if Char
c0 Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'|' then do
      [Word8]
r <- (Char -> Bool) -> [Word8] -> Parser [Word8]
takeChars' (Char -> String -> Bool
forall (t :: Type -> Type) a.
(Foldable t, Eq a) =>
a -> t a -> Bool
`notElem` [Char
'|', Char
'/']) [Char -> Word8
c2b Char
c0]
      Char
ce <- Parser Char
peekChar
      Bool -> Parser () -> Parser ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (Char
ce Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
'|') (Parser () -> Parser ()) -> Parser () -> Parser ()
forall a b. (a -> b) -> a -> b
$ do
        String -> Parser ()
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> Parser ()) -> String -> Parser ()
forall a b. (a -> b) -> a -> b
$ String
"Unexpected character " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Char -> String
forall a. Show a => a -> String
show Char
ce String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" inside symbol."
      Symbol -> Parser Symbol
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Symbol -> Parser Symbol) -> Symbol -> Parser Symbol
forall a b. (a -> b) -> a -> b
$! ByteString -> Symbol
Symbol ([Word8] -> ByteString
BS.pack ([Word8] -> ByteString) -> [Word8] -> ByteString
forall a b. (a -> b) -> a -> b
$ [Word8] -> [Word8]
forall a. [a] -> [a]
reverse (Char -> Word8
c2b Char
ceWord8 -> [Word8] -> [Word8]
forall a. a -> [a] -> [a]
:[Word8]
r))
     else if Char -> HashSet Char -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
HSet.member Char
c0 HashSet Char
initialSymbolCharSet then do
      ByteString
r <- [Word8] -> ByteString
BS.pack ([Word8] -> ByteString)
-> ([Word8] -> [Word8]) -> [Word8] -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Word8] -> [Word8]
forall a. [a] -> [a]
reverse ([Word8] -> ByteString) -> Parser [Word8] -> Parser ByteString
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (Char -> Bool) -> [Word8] -> Parser [Word8]
takeChars' (Char -> HashSet Char -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`HSet.member` HashSet Char
symbolCharSet) [Char -> Word8
c2b Char
c0]
      Bool -> Parser () -> Parser ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (ByteString -> HashSet ByteString -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
HSet.member ByteString
r HashSet ByteString
reservedWords) (Parser () -> Parser ()) -> Parser () -> Parser ()
forall a b. (a -> b) -> a -> b
$ do
        String -> Parser ()
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> Parser ()) -> String -> Parser ()
forall a b. (a -> b) -> a -> b
$ String
"Symbol cannot be reserved word " String -> String -> String
forall a. [a] -> [a] -> [a]
++ ByteString -> String
forall a. Show a => a -> String
show ByteString
r
      Symbol -> Parser Symbol
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Symbol -> Parser Symbol) -> Symbol -> Parser Symbol
forall a b. (a -> b) -> a -> b
$! ByteString -> Symbol
Symbol ByteString
r
     else do
      String -> Parser Symbol
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> Parser Symbol) -> String -> Parser Symbol
forall a b. (a -> b) -> a -> b
$ String
"Unexpected character " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Char -> String
forall a. Show a => a -> String
show Char
c0 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" starting symbol."

-- | This skips whitespace than reads in the next alphabetic or dash
-- characters.
matchApp :: [(BS.ByteString, Parser a)] -> Parser a
matchApp :: [(ByteString, Parser a)] -> Parser a
matchApp [(ByteString, Parser a)]
actions = do
  Parser ()
dropWhitespace
  let allowedChar :: Char -> Bool
allowedChar Char
c = Char
'A' Char -> Char -> Bool
forall a. Ord a => a -> a -> Bool
<= Char
c Bool -> Bool -> Bool
&& Char
c Char -> Char -> Bool
forall a. Ord a => a -> a -> Bool
<= Char
'Z' Bool -> Bool -> Bool
|| Char
'a' Char -> Char -> Bool
forall a. Ord a => a -> a -> Bool
<= Char
c Bool -> Bool -> Bool
&& Char
c Char -> Char -> Bool
forall a. Ord a => a -> a -> Bool
<= Char
'z' Bool -> Bool -> Bool
|| Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'-'
  ByteString
w <- (Char -> Bool) -> Parser ByteString
takeChars Char -> Bool
allowedChar
  case ((ByteString, Parser a) -> Bool)
-> [(ByteString, Parser a)] -> [(ByteString, Parser a)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(ByteString
m,Parser a
_p) -> ByteString
m ByteString -> ByteString -> Bool
forall a. Eq a => a -> a -> Bool
== ByteString
w) [(ByteString, Parser a)]
actions of
    [] -> do
      ByteString
w' <- (Char -> Bool) -> Parser ByteString
takeChars (\Char
c -> Char
c Char -> String -> Bool
forall (t :: Type -> Type) a.
(Foldable t, Eq a) =>
a -> t a -> Bool
`notElem` [Char
'\r', Char
'\n'])
      String -> Parser a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> Parser a) -> String -> Parser a
forall a b. (a -> b) -> a -> b
$ String
"Unsupported keyword: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ ByteString -> String
UTF8.toString (ByteString
w ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> ByteString
w')
    [(ByteString
_,Parser a
p)] -> Parser a
p
    (ByteString, Parser a)
_:(ByteString, Parser a)
_:[(ByteString, Parser a)]
_ -> String -> Parser a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> Parser a) -> String -> Parser a
forall a b. (a -> b) -> a -> b
$ String
"internal error: Duplicate keywords " String -> String -> String
forall a. [a] -> [a] -> [a]
++ ByteString -> String
forall a. Show a => a -> String
show ByteString
w

openParen :: Parser ()
openParen :: Parser ()
openParen = Char -> Parser ()
matchChar Char
'('

closeParen :: Parser ()
closeParen :: Parser ()
closeParen = Char -> Parser ()
matchChar Char
')'

-- | Read in whitespace, and then if next character is a paren
checkParen :: Parser Bool
checkParen :: Parser Bool
checkParen = do
  Char
c <- Parser Char
peekChar
  if Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'(' then
    Parser ()
dropChar Parser () -> Parser Bool -> Parser Bool
forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> Bool -> Parser Bool
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Bool
True
   else if Char -> Bool
isSpace Char
c then
    Parser Char
parseChar Parser Char -> Parser Bool -> Parser Bool
forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> Parser Bool
checkParen
   else
    Bool -> Parser Bool
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Bool
False

-- | An SMT sort.
data Sort
  = Sort Symbol [Sort]
    -- ^ A named sort with the given arguments.
  | BitVec !Integer
    -- ^ A bitvector with the given width.
  | FloatingPoint !Integer !Integer
    -- ^ floating point with exponent bits followed by significand bit.

pattern Bool :: Sort
pattern $bBool :: Sort
$mBool :: forall r. Sort -> (Void# -> r) -> (Void# -> r) -> r
Bool = Sort "Bool" []

pattern Int :: Sort
pattern $bInt :: Sort
$mInt :: forall r. Sort -> (Void# -> r) -> (Void# -> r) -> r
Int = Sort "Int" []

pattern Real :: Sort
pattern $bReal :: Sort
$mReal :: forall r. Sort -> (Void# -> r) -> (Void# -> r) -> r
Real = Sort "Real" []

pattern RoundingMode :: Sort
pattern $bRoundingMode :: Sort
$mRoundingMode :: forall r. Sort -> (Void# -> r) -> (Void# -> r) -> r
RoundingMode = Sort "RoundingMode" []

pattern Array :: Sort -> Sort -> Sort
pattern $bArray :: Sort -> Sort -> Sort
$mArray :: forall r. Sort -> (Sort -> Sort -> r) -> (Void# -> r) -> r
Array x y = Sort "Array" [x,y]

parseDecimal' :: Integer -> Parser Integer
parseDecimal' :: Integer -> Parser Integer
parseDecimal' Integer
cur = do
  Char
c <- Parser Char
peekChar
  if Char
'0' Char -> Char -> Bool
forall a. Ord a => a -> a -> Bool
<= Char
c Bool -> Bool -> Bool
&& Char
c Char -> Char -> Bool
forall a. Ord a => a -> a -> Bool
<= Char
'9' then do
    Parser ()
dropChar
    Integer -> Parser Integer
parseDecimal' (Integer -> Parser Integer) -> Integer -> Parser Integer
forall a b. (a -> b) -> a -> b
$! Integer
10 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
cur Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Char -> Int
forall a. Enum a => a -> Int
fromEnum Char
c Int -> Int -> Int
forall a. Num a => a -> a -> a
- Char -> Int
forall a. Enum a => a -> Int
fromEnum Char
'0')
   else
    Integer -> Parser Integer
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Integer
cur

-- | Parse the next characters as a decimal number.
--
-- Note. No whitespace may proceed the number.
parseDecimal ::Parser Integer
parseDecimal :: Parser Integer
parseDecimal = Integer -> Parser Integer
parseDecimal' Integer
0

instance CanParse Integer where
  parse :: Parser Integer
parse = Parser ()
dropWhitespace Parser () -> Parser Integer -> Parser Integer
forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> Parser Integer
parseDecimal

instance CanParse Sort where
  parse :: Parser Sort
parse = do
    Bool
isParen <- Parser Bool
checkParen
    if Bool
isParen then do
      Symbol
sym <- Parser Symbol
forall a. CanParse a => Parser a
parse
      if Symbol
sym Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
"_" then do
        Sort
r <- [(ByteString, Parser Sort)] -> Parser Sort
forall a. [(ByteString, Parser a)] -> Parser a
matchApp [ (,) ByteString
"BitVec" (Integer -> Sort
BitVec (Integer -> Sort) -> Parser Integer -> Parser Sort
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Integer
forall a. CanParse a => Parser a
parse)
                      , (,) ByteString
"FloatingPoint" (Integer -> Integer -> Sort
FloatingPoint (Integer -> Integer -> Sort)
-> Parser Integer -> Parser (Integer -> Sort)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Integer
forall a. CanParse a => Parser a
parse Parser (Integer -> Sort) -> Parser Integer -> Parser Sort
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Parser Integer
forall a. CanParse a => Parser a
parse)
                      ]
        Parser ()
closeParen
        Sort -> Parser Sort
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Sort
r
       else
        Symbol -> [Sort] -> Sort
Sort Symbol
sym ([Sort] -> Sort) -> Parser [Sort] -> Parser Sort
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Sort -> Parser [Sort]
forall a. Parser a -> Parser [a]
parseUntilCloseParen Parser Sort
forall a. CanParse a => Parser a
parse
     else do
      Symbol
sym <- Parser Symbol
forall a. CanParse a => Parser a
parse
      Sort -> Parser Sort
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Sort -> Parser Sort) -> Sort -> Parser Sort
forall a b. (a -> b) -> a -> b
$! Symbol -> [Sort] -> Sort
Sort Symbol
sym []

-- | This denotes an SMTLIB term over a fixed vocabulary.
data Term
   = SymbolTerm !Symbol
   | AsConst !Sort !Term
   | BVTerm !Integer !Integer
   | IntTerm !Integer
     -- ^ @IntTerm v@ denotes the SMTLIB expression @v@ if @v >= 0@ and @(- `(negate v))
     -- otherwise.
   | RatTerm !Rational
     -- ^ @RatTerm r@ denotes the SMTLIB expression @(/ `(numerator r) `(denomator r))@.
   | StoreTerm !Term !Term !Term
     -- ^ @StoreTerm a i v@ denotes the SMTLIB expression @(store a i v)@.
   | IfEqTerm !Symbol !Term !Term !Term
     -- ^ @IfEqTerm v c t f@ denotes the SMTLIB expression @(ite (= v c) t f)@.

parseIntegerTerm :: Parser Integer
parseIntegerTerm :: Parser Integer
parseIntegerTerm = do
  Bool
isParen <- Parser Bool
checkParen
  if Bool
isParen then do
    ByteString -> Parser ()
matchString ByteString
"-"
    Integer
r <- Parser Integer
forall a. CanParse a => Parser a
parse
    Parser ()
closeParen
    Integer -> Parser Integer
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Integer -> Parser Integer) -> Integer -> Parser Integer
forall a b. (a -> b) -> a -> b
$! Integer -> Integer
forall a. Num a => a -> a
negate Integer
r
   else do
    Parser Integer
forall a. CanParse a => Parser a
parse

parseEq :: Parser (Symbol, Term)
parseEq :: Parser (Symbol, Term)
parseEq = do
  Parser ()
openParen
  ByteString -> Parser ()
matchString ByteString
"="
  Symbol
var <- Parser Symbol
forall a. CanParse a => Parser a
parse
  Term
val <- Parser Term
forall a. CanParse a => Parser a
parse
  Parser ()
closeParen
  (Symbol, Term) -> Parser (Symbol, Term)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Symbol
var,Term
val)

parseTermApp :: Parser Term
parseTermApp :: Parser Term
parseTermApp = do
  Parser ()
dropWhitespace
  -- Look for (as const tp) as argument
  Bool
isParen <- Parser Bool
checkParen
  if Bool
isParen then do
    ByteString -> Parser ()
matchString ByteString
"as"
    ByteString -> Parser ()
matchString ByteString
"const"
    Term
r <- Sort -> Term -> Term
AsConst (Sort -> Term -> Term) -> Parser Sort -> Parser (Term -> Term)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Sort
forall a. CanParse a => Parser a
parse Parser (Term -> Term) -> Parser Term -> Parser Term
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Parser Term
forall a. CanParse a => Parser a
parse
    Parser ()
closeParen
    Term -> Parser Term
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term -> Parser Term) -> Term -> Parser Term
forall a b. (a -> b) -> a -> b
$! Term
r
   else do
    Symbol
op <- Parser Symbol
forall a. CanParse a => Parser a
parse :: Parser Symbol
    case Symbol
op of
      Symbol
"_" -> do
        ByteString -> Parser ()
matchString ByteString
"bv"
        Integer -> Integer -> Term
BVTerm (Integer -> Integer -> Term)
-> Parser Integer -> Parser (Integer -> Term)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Integer
parseDecimal Parser (Integer -> Term) -> Parser Integer -> Parser Term
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Parser Integer
forall a. CanParse a => Parser a
parse
      Symbol
"/" -> do
        Integer
num <- Parser Integer
parseIntegerTerm
        Integer
den <- Parser Integer
forall a. CanParse a => Parser a
parse
        Bool -> Parser () -> Parser ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (Integer
den Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0) (Parser () -> Parser ()) -> Parser () -> Parser ()
forall a b. (a -> b) -> a -> b
$ String -> Parser ()
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> Parser ()) -> String -> Parser ()
forall a b. (a -> b) -> a -> b
$ String
"Model contains divide-by-zero"
        Term -> Parser Term
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term -> Parser Term) -> Term -> Parser Term
forall a b. (a -> b) -> a -> b
$ Rational -> Term
RatTerm (Integer
num Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% Integer
den)
      Symbol
"-" -> do
        Integer -> Term
IntTerm (Integer -> Term) -> (Integer -> Integer) -> Integer -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer
forall a. Num a => a -> a
negate (Integer -> Term) -> Parser Integer -> Parser Term
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Integer
forall a. CanParse a => Parser a
parse
      Symbol
"store" ->
        Term -> Term -> Term -> Term
StoreTerm (Term -> Term -> Term -> Term)
-> Parser Term -> Parser (Term -> Term -> Term)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Term
forall a. CanParse a => Parser a
parse Parser (Term -> Term -> Term)
-> Parser Term -> Parser (Term -> Term)
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Parser Term
forall a. CanParse a => Parser a
parse Parser (Term -> Term) -> Parser Term -> Parser Term
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Parser Term
forall a. CanParse a => Parser a
parse
      Symbol
"ite" -> do
        (Symbol
var,Term
val) <- Parser (Symbol, Term)
parseEq
        Term
t <- Parser Term
forall a. CanParse a => Parser a
parse
        Term
f <- Parser Term
forall a. CanParse a => Parser a
parse
        Term -> Parser Term
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term -> Parser Term) -> Term -> Parser Term
forall a b. (a -> b) -> a -> b
$ Symbol -> Term -> Term -> Term -> Term
IfEqTerm Symbol
var Term
val Term
t Term
f
      Symbol
_ -> do
        String -> Parser Term
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> Parser Term) -> String -> Parser Term
forall a b. (a -> b) -> a -> b
$ String
"Unsupported operator symbol " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Symbol -> String
forall a. Show a => a -> String
show Symbol
op

instance CanParse Term where
  parse :: Parser Term
parse = do
    Parser ()
dropWhitespace
    Char
c <- Parser Char
peekChar
    if Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'(' then do
      Term
t <- Parser Term
parseTermApp
      Parser ()
closeParen
      Term -> Parser Term
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term -> Parser Term) -> Term -> Parser Term
forall a b. (a -> b) -> a -> b
$! Term
t
     else if Char -> Bool
isDigit Char
c then
      Integer -> Term
IntTerm (Integer -> Term) -> Parser Integer -> Parser Term
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Integer
parseDecimal
     else if Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'@' then
      Symbol -> Term
SymbolTerm (Symbol -> Term) -> Parser Symbol -> Parser Term
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Symbol
forall a. CanParse a => Parser a
parse
     else
      String -> Parser Term
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> Parser Term) -> String -> Parser Term
forall a b. (a -> b) -> a -> b
$ String
"Could not parse term"


data DefineFun = DefineFun { DefineFun -> Symbol
funSymbol :: !Symbol
                           , DefineFun -> [(Symbol, Sort)]
funArgs :: ![(Symbol, Sort)]
                           , DefineFun -> Sort
funResultSort :: !Sort
                           , DefineFun -> Term
funDef :: !Term
                           }

-- | A line in the model response
data ModelResponse
   = DeclareSortResponse !Symbol !Integer
   | DefineFunResponse !DefineFun

parseSortedVar :: Parser (Symbol, Sort)
parseSortedVar :: Parser (Symbol, Sort)
parseSortedVar = Parser ()
openParen Parser () -> Parser (Symbol, Sort) -> Parser (Symbol, Sort)
forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> ((,) (Symbol -> Sort -> (Symbol, Sort))
-> Parser Symbol -> Parser (Sort -> (Symbol, Sort))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Symbol
forall a. CanParse a => Parser a
parse Parser (Sort -> (Symbol, Sort))
-> Parser Sort -> Parser (Symbol, Sort)
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Parser Sort
forall a. CanParse a => Parser a
parse) Parser (Symbol, Sort) -> Parser () -> Parser (Symbol, Sort)
forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f a
<* Parser ()
closeParen

-- | Parses ⟨symbol⟩ ( ⟨sorted_var⟩* ) ⟨sort⟩ ⟨term⟩
parseDefineFun :: Parser DefineFun
parseDefineFun :: Parser DefineFun
parseDefineFun = do
  Symbol
sym <- Parser Symbol
forall a. CanParse a => Parser a
parse
  [(Symbol, Sort)]
args <- Parser ()
openParen Parser () -> Parser [(Symbol, Sort)] -> Parser [(Symbol, Sort)]
forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> Parser (Symbol, Sort) -> Parser [(Symbol, Sort)]
forall a. Parser a -> Parser [a]
parseUntilCloseParen Parser (Symbol, Sort)
parseSortedVar
  Sort
res <- Parser Sort
forall a. CanParse a => Parser a
parse
  Term
def <- Parser Term
forall a. CanParse a => Parser a
parse
  DefineFun -> Parser DefineFun
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (DefineFun -> Parser DefineFun) -> DefineFun -> Parser DefineFun
forall a b. (a -> b) -> a -> b
$! DefineFun :: Symbol -> [(Symbol, Sort)] -> Sort -> Term -> DefineFun
DefineFun { funSymbol :: Symbol
funSymbol = Symbol
sym
                    , funArgs :: [(Symbol, Sort)]
funArgs = [(Symbol, Sort)]
args
                    , funResultSort :: Sort
funResultSort = Sort
res
                    , funDef :: Term
funDef = Term
def
                    }

instance CanParse ModelResponse where
  parse :: Parser ModelResponse
parse = do
    Parser ()
openParen
    ModelResponse
r <- [(ByteString, Parser ModelResponse)] -> Parser ModelResponse
forall a. [(ByteString, Parser a)] -> Parser a
matchApp [ (,) ByteString
"declare-sort"    (Parser ModelResponse -> (ByteString, Parser ModelResponse))
-> Parser ModelResponse -> (ByteString, Parser ModelResponse)
forall a b. (a -> b) -> a -> b
$ Symbol -> Integer -> ModelResponse
DeclareSortResponse (Symbol -> Integer -> ModelResponse)
-> Parser Symbol -> Parser (Integer -> ModelResponse)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Symbol
forall a. CanParse a => Parser a
parse Parser (Integer -> ModelResponse)
-> Parser Integer -> Parser ModelResponse
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Parser Integer
forall a. CanParse a => Parser a
parse
                  , (,) ByteString
"define-fun"      (Parser ModelResponse -> (ByteString, Parser ModelResponse))
-> Parser ModelResponse -> (ByteString, Parser ModelResponse)
forall a b. (a -> b) -> a -> b
$ DefineFun -> ModelResponse
DefineFunResponse (DefineFun -> ModelResponse)
-> Parser DefineFun -> Parser ModelResponse
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser DefineFun
parseDefineFun
                  , (,) ByteString
"define-fun-rec"  (Parser ModelResponse -> (ByteString, Parser ModelResponse))
-> Parser ModelResponse -> (ByteString, Parser ModelResponse)
forall a b. (a -> b) -> a -> b
$ String -> Parser ModelResponse
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"Do not yet support define-fun-rec"
                  , (,) ByteString
"define-funs-rec" (Parser ModelResponse -> (ByteString, Parser ModelResponse))
-> Parser ModelResponse -> (ByteString, Parser ModelResponse)
forall a b. (a -> b) -> a -> b
$ String -> Parser ModelResponse
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"Do not yet support define-funs-rec"
                  ]
    Parser ()
closeParen
    ModelResponse -> Parser ModelResponse
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (ModelResponse -> Parser ModelResponse)
-> ModelResponse -> Parser ModelResponse
forall a b. (a -> b) -> a -> b
$! ModelResponse
r

-- | The parsed declarations and definitions returned by "(get-model)"
type GetModelResponse = [ModelResponse]

-- | This reads the model response from a "(get-model)" request.
readGetModelResponse :: Handle -> IO GetModelResponse
readGetModelResponse :: Handle -> IO GetModelResponse
readGetModelResponse Handle
h =
  Handle -> Parser GetModelResponse -> IO GetModelResponse
forall a. Handle -> Parser a -> IO a
runParser Handle
h (Parser GetModelResponse -> IO GetModelResponse)
-> Parser GetModelResponse -> IO GetModelResponse
forall a b. (a -> b) -> a -> b
$
    Parser ()
openParen Parser () -> Parser GetModelResponse -> Parser GetModelResponse
forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> Parser ModelResponse -> Parser GetModelResponse
forall a. Parser a -> Parser [a]
parseUntilCloseParen Parser ModelResponse
forall a. CanParse a => Parser a
parse