{-|
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.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 = forall a b. (Integral a, Num b) => a -> b
fromIntegral forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 -> 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
<$ :: forall a b. a -> Parser b -> Parser a
$c<$ :: forall a b. a -> Parser b -> Parser a
fmap :: forall a b. (a -> b) -> Parser a -> Parser b
$cfmap :: forall a b. (a -> b) -> Parser a -> Parser b
Functor, Functor 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
<* :: forall a b. Parser a -> Parser b -> Parser a
$c<* :: forall a b. Parser a -> Parser b -> Parser a
*> :: forall a b. Parser a -> Parser b -> Parser b
$c*> :: forall a b. Parser a -> Parser b -> Parser b
liftA2 :: forall a b c. (a -> b -> c) -> Parser a -> Parser b -> Parser c
$cliftA2 :: forall a b c. (a -> b -> c) -> Parser a -> Parser b -> Parser c
<*> :: forall a b. Parser (a -> b) -> Parser a -> Parser b
$c<*> :: forall a b. Parser (a -> b) -> Parser a -> Parser b
pure :: forall a. a -> Parser a
$cpure :: forall a. a -> 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 = forall a. ReaderT Handle IO a -> Parser a
Parser forall a b. (a -> b) -> a -> b
$ ReaderT Handle IO a
m forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall a. Parser a -> ReaderT Handle IO a
unParser 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 = 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) = 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 = forall a. ReaderT Handle IO a -> Parser a
Parser forall a b. (a -> b) -> a -> b
$ forall r (m :: Type -> Type) a. (r -> m a) -> ReaderT r m a
ReaderT 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 = forall a. ReaderT Handle IO a -> Parser a
Parser forall a b. (a -> b) -> a -> b
$ forall r (m :: Type -> Type) a. (r -> m a) -> ReaderT r m a
ReaderT forall a b. (a -> b) -> a -> b
$ Handle -> IO Char
hLookAhead

dropChar :: Parser ()
dropChar :: Parser ()
dropChar = forall a. ReaderT Handle IO a -> Parser a
Parser forall a b. (a -> b) -> a -> b
$ forall r (m :: Type -> Type) a. (r -> m a) -> ReaderT r m a
ReaderT forall a b. (a -> b) -> a -> b
$ \Handle
h -> Handle -> IO Char
hGetChar Handle
h forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> 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 forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> Parser ()
dropWhitespace
   else
    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 forall a. Eq a => a -> a -> Bool
== Char
expected then
    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
    forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail forall a b. (a -> b) -> a -> b
$ [Char]
"Unexpected input char " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Char
c forall a. [a] -> [a] -> [a]
++ [Char]
"(expected " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Char
expected forall a. [a] -> [a] -> [a]
++ [Char]
")"

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

parseUntilCloseParen' :: [a] -> Parser a -> Parser [a]
parseUntilCloseParen' :: forall a. [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 forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> forall a. [a] -> Parser a -> Parser [a]
parseUntilCloseParen' [a]
prev Parser a
p
   else if Char
c forall a. Eq a => a -> a -> Bool
== Char
')' then
    Parser ()
dropChar forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (forall a. [a] -> [a]
reverse [a]
prev)
   else do
    Parser a
p forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
n -> forall a. [a] -> Parser a -> Parser [a]
parseUntilCloseParen' (a
nforall 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 = 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
cforall a. a -> [a] -> [a]
:[Word8]
prev)
   else do
    forall (f :: Type -> Type) a. Applicative f => a -> f a
pure 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 []
  forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! [Word8] -> ByteString
BS.pack (forall a. [a] -> [a]
reverse [Word8]
l)


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

-- | Parse a quoted string.
parseQuotedString :: Parser String
parseQuotedString :: Parser [Char]
parseQuotedString = do
  Char -> Parser ()
matchChar Char
'"'
  ByteString
l <- (Char -> Bool) -> Parser ByteString
takeChars (forall a. Eq a => a -> a -> Bool
/= Char
'"')
  Char -> Parser ()
matchChar Char
'"'
  forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ ByteString -> [Char]
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 = forall a. Handle -> Parser a -> IO a
runParser Handle
h 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
      [Char]
msg <- Parser [Char]
parseQuotedString
      Parser ()
closeParen
      forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ([Char] -> CheckSatResponse
CheckSatError [Char]
msg)
     else
      forall a. [(ByteString, Parser a)] -> Parser a
matchApp [ (ByteString
"sat",     forall (f :: Type -> Type) a. Applicative f => a -> f a
pure CheckSatResponse
SatResponse)
               , (ByteString
"unsat",   forall (f :: Type -> Type) a. Applicative f => a -> f a
pure CheckSatResponse
UnsatResponse)
               , (ByteString
"unknown", forall (f :: Type -> Type) a. Applicative f => a -> f a
pure CheckSatResponse
UnknownResponse)
               , (ByteString
"unsupported", 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 = forall a. CanParse a => Handle -> IO a
readFromHandle

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

-- | An SMT symbol
newtype Symbol = Symbol BS.ByteString
  deriving (Symbol -> Symbol -> Bool
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 -> [Char]
show (Symbol ByteString
s) = forall a. Show a => a -> [Char]
show ByteString
s

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

symbolCharSet :: HashSet Char
symbolCharSet :: HashSet Char
symbolCharSet = forall a. (Eq a, Hashable a) => [a] -> HashSet a
HSet.fromList
  forall a b. (a -> b) -> a -> b
$  [Char
'A'..Char
'Z']
  forall a. [a] -> [a] -> [a]
++ [Char
'a'..Char
'z']
  forall a. [a] -> [a] -> [a]
++ [Char
'0'..Char
'9']
  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 forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
`HSet.difference` (forall a. (Eq a, Hashable a) => [a] -> HashSet a
HSet.fromList [Char
'0'..Char
'9'])

generalReservedWords :: HashSet BS.ByteString
generalReservedWords :: HashSet ByteString
generalReservedWords = forall a. (Eq a, Hashable a) => [a] -> HashSet a
HSet.fromList 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 = forall a. (Eq a, Hashable a) => [a] -> HashSet a
HSet.fromList 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 = 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 forall a. Eq a => a -> a -> Bool
== Char
'|' then do
      [Word8]
r <- (Char -> Bool) -> [Word8] -> Parser [Word8]
takeChars' (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
      forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (Char
ce forall a. Eq a => a -> a -> Bool
/= Char
'|') forall a b. (a -> b) -> a -> b
$ do
        forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail forall a b. (a -> b) -> a -> b
$ [Char]
"Unexpected character " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Char
ce forall a. [a] -> [a] -> [a]
++ [Char]
" inside symbol."
      forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! ByteString -> Symbol
Symbol ([Word8] -> ByteString
BS.pack forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
reverse (Char -> Word8
c2b Char
ceforall a. a -> [a] -> [a]
:[Word8]
r))
     else if 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> [a]
reverse forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (Char -> Bool) -> [Word8] -> Parser [Word8]
takeChars' (forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`HSet.member` HashSet Char
symbolCharSet) [Char -> Word8
c2b Char
c0]
      forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
HSet.member ByteString
r HashSet ByteString
reservedWords) forall a b. (a -> b) -> a -> b
$ do
        forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail forall a b. (a -> b) -> a -> b
$ [Char]
"Symbol cannot be reserved word " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show ByteString
r
      forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! ByteString -> Symbol
Symbol ByteString
r
     else do
      forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail forall a b. (a -> b) -> a -> b
$ [Char]
"Unexpected character " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Char
c0 forall a. [a] -> [a] -> [a]
++ [Char]
" 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' forall a. Ord a => a -> a -> Bool
<= Char
c Bool -> Bool -> Bool
&& Char
c forall a. Ord a => a -> a -> Bool
<= Char
'Z' Bool -> Bool -> Bool
|| Char
'a' forall a. Ord a => a -> a -> Bool
<= Char
c Bool -> Bool -> Bool
&& Char
c forall a. Ord a => a -> a -> Bool
<= Char
'z' Bool -> Bool -> Bool
|| Char
c forall a. Eq a => a -> a -> Bool
== Char
'-'
  ByteString
w <- (Char -> Bool) -> Parser ByteString
takeChars Char -> Bool
allowedChar
  case forall a. (a -> Bool) -> [a] -> [a]
filter (\(ByteString
m,Parser a
_p) -> ByteString
m 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 forall (t :: Type -> Type) a.
(Foldable t, Eq a) =>
a -> t a -> Bool
`notElem` [Char
'\r', Char
'\n'])
      forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail forall a b. (a -> b) -> a -> b
$ [Char]
"Unsupported keyword: " forall a. [a] -> [a] -> [a]
++ ByteString -> [Char]
UTF8.toString (ByteString
w 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)]
_ -> forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail forall a b. (a -> b) -> a -> b
$ [Char]
"internal error: Duplicate keywords " forall a. [a] -> [a] -> [a]
++ 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
  Char
c <- Parser Char
peekChar
  if Char
c forall a. Eq a => a -> a -> Bool
== Char
'(' then
    Parser ()
dropChar forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Bool
True
   else if Char -> Bool
isSpace Char
c then
    Parser Char
parseChar forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> Parser Bool
checkParen
   else
    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 -> ((# #) -> r) -> ((# #) -> r) -> r
Bool = Sort "Bool" []

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

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

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

pattern Array :: Sort -> Sort -> Sort
pattern $bArray :: Sort -> Sort -> Sort
$mArray :: forall {r}. Sort -> (Sort -> Sort -> r) -> ((# #) -> 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' forall a. Ord a => a -> a -> Bool
<= Char
c Bool -> Bool -> Bool
&& Char
c forall a. Ord a => a -> a -> Bool
<= Char
'9' then do
    Parser ()
dropChar
    Integer -> Parser Integer
parseDecimal' forall a b. (a -> b) -> a -> b
$! Integer
10 forall a. Num a => a -> a -> a
* Integer
cur forall a. Num a => a -> a -> a
+ forall a. Integral a => a -> Integer
toInteger (forall a. Enum a => a -> Int
fromEnum Char
c forall a. Num a => a -> a -> a
- forall a. Enum a => a -> Int
fromEnum Char
'0')
   else
    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 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 <- forall a. CanParse a => Parser a
parse
      if Symbol
sym forall a. Eq a => a -> a -> Bool
== Symbol
"_" then do
        Sort
r <- forall a. [(ByteString, Parser a)] -> Parser a
matchApp [ (,) ByteString
"BitVec" (Integer -> Sort
BitVec forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. CanParse a => Parser a
parse)
                      , (,) ByteString
"FloatingPoint" (Integer -> Integer -> Sort
FloatingPoint forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. CanParse a => Parser a
parse forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall a. CanParse a => Parser a
parse)
                      ]
        Parser ()
closeParen
        forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Sort
r
       else
        Symbol -> [Sort] -> Sort
Sort Symbol
sym forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Parser a -> Parser [a]
parseUntilCloseParen forall a. CanParse a => Parser a
parse
     else do
      Symbol
sym <- forall a. CanParse a => Parser a
parse
      forall (f :: Type -> Type) a. Applicative f => a -> f a
pure 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 <- forall a. CanParse a => Parser a
parse
    Parser ()
closeParen
    forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! forall a. Num a => a -> a
negate Integer
r
   else do
    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 <- forall a. CanParse a => Parser a
parse
  Term
val <- forall a. CanParse a => Parser a
parse
  Parser ()
closeParen
  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 forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. CanParse a => Parser a
parse forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall a. CanParse a => Parser a
parse
    Parser ()
closeParen
    forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! Term
r
   else do
    Symbol
op <- forall a. CanParse a => Parser a
parse :: Parser Symbol
    case Symbol
op of
      Symbol
"_" -> do
        ByteString -> Parser ()
matchString ByteString
"bv"
        Integer -> Integer -> Term
BVTerm forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Integer
parseDecimal forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall a. CanParse a => Parser a
parse
      Symbol
"/" -> do
        Integer
num <- Parser Integer
parseIntegerTerm
        Integer
den <- forall a. CanParse a => Parser a
parse
        forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (Integer
den forall a. Eq a => a -> a -> Bool
== Integer
0) forall a b. (a -> b) -> a -> b
$ forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail forall a b. (a -> b) -> a -> b
$ [Char]
"Model contains divide-by-zero"
        forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Rational -> Term
RatTerm (Integer
num forall a. Integral a => a -> a -> Ratio a
% Integer
den)
      Symbol
"-" -> do
        Integer -> Term
IntTerm forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Num a => a -> a
negate forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. CanParse a => Parser a
parse
      Symbol
"store" ->
        Term -> Term -> Term -> Term
StoreTerm forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. CanParse a => Parser a
parse forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall a. CanParse a => Parser a
parse forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall a. CanParse a => Parser a
parse
      Symbol
"ite" -> do
        (Symbol
var,Term
val) <- Parser (Symbol, Term)
parseEq
        Term
t <- forall a. CanParse a => Parser a
parse
        Term
f <- forall a. CanParse a => Parser a
parse
        forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Symbol -> Term -> Term -> Term -> Term
IfEqTerm Symbol
var Term
val Term
t Term
f
      Symbol
_ -> do
        forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail forall a b. (a -> b) -> a -> b
$ [Char]
"Unsupported operator symbol " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Symbol
op

instance CanParse Term where
  parse :: Parser Term
parse = do
    Parser ()
dropWhitespace
    Char
c <- Parser Char
peekChar
    if Char
c forall a. Eq a => a -> a -> Bool
== Char
'(' then do
      Term
t <- Parser Term
parseTermApp
      Parser ()
closeParen
      forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! Term
t
     else if Char -> Bool
isDigit Char
c then
      Integer -> Term
IntTerm forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Integer
parseDecimal
     else if Char
c forall a. Eq a => a -> a -> Bool
== Char
'@' then
      Symbol -> Term
SymbolTerm forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. CanParse a => Parser a
parse
     else
      forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail forall a b. (a -> b) -> a -> b
$ [Char]
"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 forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> ((,) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. CanParse a => Parser a
parse forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall a. CanParse a => Parser a
parse) 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 <- forall a. CanParse a => Parser a
parse
  [(Symbol, Sort)]
args <- Parser ()
openParen forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> forall a. Parser a -> Parser [a]
parseUntilCloseParen Parser (Symbol, Sort)
parseSortedVar
  Sort
res <- forall a. CanParse a => Parser a
parse
  Term
def <- forall a. CanParse a => Parser a
parse
  forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! 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 <- forall a. [(ByteString, Parser a)] -> Parser a
matchApp [ (,) ByteString
"declare-sort"    forall a b. (a -> b) -> a -> b
$ Symbol -> Integer -> ModelResponse
DeclareSortResponse forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. CanParse a => Parser a
parse forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall a. CanParse a => Parser a
parse
                  , (,) ByteString
"define-fun"      forall a b. (a -> b) -> a -> b
$ DefineFun -> ModelResponse
DefineFunResponse forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser DefineFun
parseDefineFun
                  , (,) ByteString
"define-fun-rec"  forall a b. (a -> b) -> a -> b
$ forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail [Char]
"Do not yet support define-fun-rec"
                  , (,) ByteString
"define-funs-rec" forall a b. (a -> b) -> a -> b
$ forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail [Char]
"Do not yet support define-funs-rec"
                  ]
    Parser ()
closeParen
    forall (f :: Type -> Type) a. Applicative f => a -> f a
pure 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 =
  forall a. Handle -> Parser a -> IO a
runParser Handle
h forall a b. (a -> b) -> a -> b
$
    Parser ()
openParen forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> forall a. Parser a -> Parser [a]
parseUntilCloseParen forall a. CanParse a => Parser a
parse