{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TemplateHaskell #-}
module What4.Protocol.SMTLib2.Parse
(
CheckSatResponse(..)
, readCheckSatResponse
, GetModelResponse
, readGetModelResponse
, ModelResponse(..)
, DefineFun(..)
, Symbol
, Sort(..)
, pattern Bool
, pattern Int
, pattern Real
, pattern RoundingMode
, pattern Array
, 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
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
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 ()
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 ()
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]
")"
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 :: Parser a -> Parser [a]
parseUntilCloseParen :: forall a. Parser a -> Parser [a]
parseUntilCloseParen = forall a. [a] -> Parser a -> Parser [a]
parseUntilCloseParen' []
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 :: (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
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
class CanParse a where
parse :: Parser a
readFromHandle :: Handle -> IO a
readFromHandle Handle
h = forall a. Handle -> Parser a -> IO a
runParser Handle
h forall a. CanParse a => Parser a
parse
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)
]
readCheckSatResponse :: Handle -> IO CheckSatResponse
readCheckSatResponse :: Handle -> IO CheckSatResponse
readCheckSatResponse = forall a. CanParse a => Handle -> IO a
readFromHandle
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."
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
')'
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
data Sort
= Sort Symbol [Sort]
| BitVec !Integer
| FloatingPoint !Integer !Integer
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
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 []
data Term
= SymbolTerm !Symbol
| AsConst !Sort !Term
| BVTerm !Integer !Integer
| IntTerm !Integer
| RatTerm !Rational
| StoreTerm !Term !Term !Term
| IfEqTerm !Symbol !Term !Term !Term
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
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
}
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
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
type GetModelResponse = [ModelResponse]
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