    {-|
    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