{-|
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
    -- * GetModelResponse
  , 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 (when)
import           Control.Monad.Reader (ReaderT(..))
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 { forall a. Parser a -> ReaderT Handle IO a
unParser :: ReaderT Handle IO a }
  deriving ((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
$cfmap :: forall a b. (a -> b) -> Parser a -> Parser b
fmap :: forall a b. (a -> b) -> Parser a -> Parser b
$c<$ :: forall a b. a -> Parser b -> Parser a
<$ :: forall a b. a -> Parser b -> Parser a
Functor, Functor Parser
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
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
$cpure :: forall a. a -> Parser a
pure :: forall a. a -> Parser a
$c<*> :: forall a b. Parser (a -> b) -> Parser a -> Parser b
<*> :: forall a b. Parser (a -> b) -> Parser a -> Parser b
$cliftA2 :: forall a b c. (a -> b -> c) -> Parser a -> Parser b -> Parser c
liftA2 :: forall a b c. (a -> b -> c) -> Parser a -> Parser b -> Parser c
$c*> :: forall a b. Parser a -> Parser b -> Parser b
*> :: forall a b. Parser a -> Parser b -> Parser b
$c<* :: forall a b. Parser a -> Parser b -> Parser a
<* :: forall a b. Parser a -> Parser b -> Parser a
Applicative)

instance Monad Parser where
  Parser ReaderT Handle IO a
m >>= :: forall a b. 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 a b.
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 :: forall a. [Char] -> Parser a
fail = [Char] -> Parser a
forall a. HasCallStack => [Char] -> a
error

runParser :: Handle -> Parser a -> IO a
runParser :: forall a. 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 a b. IO a -> IO b -> IO b
forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> () -> IO ()
forall a. a -> IO a
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
  c <- Parser Char
peekChar
  if isSpace c then do
    dropChar >> dropWhitespace
   else
    pure ()

-- | Drop whitespace, and if next character matches expected return,
-- otherwise fail.
matchChar :: Char -> Parser ()
matchChar :: Char -> Parser ()
matchChar Char
expected = do
  c <- Parser Char
parseChar
  if c == expected then
    pure ()
   else if isSpace c then
    matchChar expected
   else
    fail $ "Unexpected input char " ++ show c ++ "(expected " ++ show expected ++ ")"

-- | Drop whitespace until we reach the given string.
matchString :: BS.ByteString -> Parser ()
matchString :: ByteString -> Parser ()
matchString ByteString
expected = do
  Parser ()
dropWhitespace
  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)
  when (found /= expected) $ do
    fail $ "Unexpected string " ++ show found ++ "(expected " ++ show expected ++ ")"

parseUntilCloseParen' :: [a] -> Parser a -> Parser [a]
parseUntilCloseParen' :: forall a. [a] -> Parser a -> Parser [a]
parseUntilCloseParen' [a]
prev Parser a
p = do
  c <- Parser Char
peekChar
  if isSpace c then
    dropChar >> parseUntilCloseParen' prev p
   else if c == ')' then
    dropChar *> pure (reverse prev)
   else do
    p >>= \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 :: forall a. 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
  c <- Parser Char
peekChar
  if p c then do
    _ <- parseChar
    takeChars' p (c2b c:prev)
   else do
    pure $! 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
  l <- (Char -> Bool) -> [Word8] -> Parser [Word8]
takeChars' Char -> Bool
p []
  pure $! BS.pack (reverse l)


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

-- | Parse a quoted string.
parseQuotedString :: Parser String
parseQuotedString :: Parser [Char]
parseQuotedString = do
  Char -> Parser ()
matchChar Char
'"'
  l <- (Char -> Bool) -> Parser ByteString
takeChars (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
'"')
  matchChar '"'
  pure $ UTF8.toString 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
    isParen <- Parser Bool
checkParen
    if isParen then do
      matchString "error"
      dropWhitespace
      msg <- parseQuotedString
      closeParen
      pure (CheckSatError msg)
     else
      matchApp [ ("sat",     pure SatResponse)
               , ("unsat",   pure UnsatResponse)
               , ("unknown", pure UnknownResponse)
               , ("unsupported", pure 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
$c== :: Symbol -> Symbol -> Bool
== :: Symbol -> Symbol -> Bool
$c/= :: Symbol -> Symbol -> Bool
/= :: Symbol -> Symbol -> Bool
Eq)

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

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

symbolCharSet :: HashSet Char
symbolCharSet :: HashSet Char
symbolCharSet = [Char] -> HashSet Char
forall a. (Eq a, Hashable a) => [a] -> HashSet a
HSet.fromList
  ([Char] -> HashSet Char) -> [Char] -> HashSet Char
forall a b. (a -> b) -> a -> b
$  [Char
'A'..Char
'Z']
  [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char
'a'..Char
'z']
  [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char
'0'..Char
'9']
  [Char] -> [Char] -> [Char]
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` ([Char] -> 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 => 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
    c0 <- Parser Char
peekChar
    if c0 == '|' then do
      r <- takeChars' (`notElem` ['|', '/']) [c2b c0]
      ce <- peekChar
      when (ce /= '|') $ do
        fail $ "Unexpected character " ++ show ce ++ " inside symbol."
      pure $! Symbol (BS.pack $ reverse (c2b ce:r))
     else if HSet.member c0 initialSymbolCharSet then do
      r <- BS.pack . reverse <$> takeChars' (`HSet.member` symbolCharSet) [c2b c0]
      when (HSet.member r reservedWords) $ do
        fail $ "Symbol cannot be reserved word " ++ show r
      pure $! Symbol r
     else do
      fail $ "Unexpected character " ++ show c0 ++ " starting symbol."

-- | This skips whitespace than reads in the next alphabetic or dash
-- characters.
matchApp :: [(BS.ByteString, Parser a)] -> Parser a
matchApp :: forall a. [(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
'-'
  w <- (Char -> Bool) -> Parser ByteString
takeChars Char -> Bool
allowedChar
  case filter (\(ByteString
m,Parser a
_p) -> ByteString
m ByteString -> ByteString -> Bool
forall a. Eq a => a -> a -> Bool
== ByteString
w) actions of
    [] -> do
      w' <- (Char -> Bool) -> Parser ByteString
takeChars (\Char
c -> Char
c Char -> [Char] -> Bool
forall (t :: Type -> Type) a.
(Foldable t, Eq a) =>
a -> t a -> Bool
`notElem` [Char
'\r', Char
'\n'])
      fail $ "Unsupported keyword: " ++ UTF8.toString (w <> w')
    [(ByteString
_,Parser a
p)] -> Parser a
p
    (ByteString, Parser a)
_:(ByteString, Parser a)
_:[(ByteString, Parser a)]
_ -> [Char] -> Parser a
forall a. [Char] -> Parser a
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail ([Char] -> Parser a) -> [Char] -> Parser a
forall a b. (a -> b) -> a -> b
$ [Char]
"internal error: Duplicate keywords " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ByteString -> [Char]
forall a. Show a => a -> [Char]
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
  c <- Parser Char
peekChar
  if c == '(' then
    dropChar >> pure True
   else if isSpace c then
    parseChar >> checkParen
   else
    pure 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 $mBool :: forall {r}. Sort -> ((# #) -> r) -> ((# #) -> r) -> r
$bBool :: Sort
Bool = Sort "Bool" []

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

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

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

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

parseDecimal' :: Integer -> Parser Integer
parseDecimal' :: Integer -> Parser Integer
parseDecimal' Integer
cur = do
  c <- Parser Char
peekChar
  if '0' <= c && c <= '9' then do
    dropChar
    parseDecimal' $! 10 * cur + toInteger (fromEnum c - fromEnum '0')
   else
    pure 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 a b. Parser a -> Parser b -> Parser b
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
    isParen <- Parser Bool
checkParen
    if isParen then do
      sym <- parse
      if sym == "_" then do
        r <- matchApp [ (,) "BitVec" (BitVec <$> parse)
                      , (,) "FloatingPoint" (FloatingPoint <$> parse <*> parse)
                      ]
        closeParen
        pure r
       else
        Sort sym <$> parseUntilCloseParen parse
     else do
      sym <- parse
      pure $! Sort 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
  isParen <- Parser Bool
checkParen
  if isParen then do
    matchString "-"
    r <- parse
    closeParen
    pure $! negate r
   else do
    parse

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

parseTermApp :: Parser Term
parseTermApp :: Parser Term
parseTermApp = do
  Parser ()
dropWhitespace
  -- Look for (as const tp) as argument
  isParen <- Parser Bool
checkParen
  if isParen then do
    matchString "as"
    matchString "const"
    r <- AsConst <$> parse <*> parse
    closeParen
    pure $! r
   else do
    op <- parse :: Parser Symbol
    case 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 a b. Parser (a -> b) -> Parser a -> Parser b
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
        num <- Parser Integer
parseIntegerTerm
        den <- parse
        when (den == 0) $ fail $ "Model contains divide-by-zero"
        pure $ RatTerm (num % 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 a b. Parser (a -> b) -> Parser a -> Parser b
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 a b. Parser (a -> b) -> Parser a -> Parser b
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
        (var,val) <- Parser (Symbol, Term)
parseEq
        t <- parse
        f <- parse
        pure $ IfEqTerm var val t f
      Symbol
_ -> do
        [Char] -> Parser Term
forall a. [Char] -> Parser a
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail ([Char] -> Parser Term) -> [Char] -> Parser Term
forall a b. (a -> b) -> a -> b
$ [Char]
"Unsupported operator symbol " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Symbol -> [Char]
forall a. Show a => a -> [Char]
show Symbol
op

instance CanParse Term where
  parse :: Parser Term
parse = do
    Parser ()
dropWhitespace
    c <- Parser Char
peekChar
    if c == '(' then do
      t <- parseTermApp
      closeParen
      pure $! t
     else if isDigit c then
      IntTerm <$> parseDecimal
     else if c == '@' then
      SymbolTerm <$> parse
     else
      fail $ "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 a b. Parser a -> Parser b -> Parser b
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 a b. Parser (a -> b) -> Parser a -> Parser b
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 a b. Parser a -> Parser b -> Parser a
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
  sym <- Parser Symbol
forall a. CanParse a => Parser a
parse
  args <- openParen *> parseUntilCloseParen parseSortedVar
  res <- parse
  def <- parse
  pure $! DefineFun { funSymbol = sym
                    , funArgs = args
                    , funResultSort = res
                    , funDef = def
                    }

instance CanParse ModelResponse where
  parse :: Parser ModelResponse
parse = do
    Parser ()
openParen
    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 a b. Parser (a -> b) -> Parser a -> Parser b
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
$ [Char] -> Parser ModelResponse
forall a. [Char] -> Parser a
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail [Char]
"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
$ [Char] -> Parser ModelResponse
forall a. [Char] -> Parser a
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail [Char]
"Do not yet support define-funs-rec"
                  ]
    closeParen
    pure $! 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 a b. Parser a -> Parser b -> Parser b
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