{-|
This module defines types and operations for parsing SMTLib2 solver responses.

These are high-level responses, as describe in
@https://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf@,
page 47, Figure 3.9.

This parser is designed to be the top level handling for solver
responses, and to be used in conjuction with
What4.Protocol.SMTLib2.Parse and What4.Protocol.SExp with the latter
handling detailed parsing of specific constructs returned in the body
of the general response.
-}

{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}

module What4.Protocol.SMTLib2.Response
  (
    SMTResponse(..)
  , SMTLib2Exception(..)
  , getSolverResponse
  , getLimitedSolverResponse
  , smtParseOptions
  , strictSMTParsing
  , strictSMTParseOpt
  )
where

import           Control.Applicative
import           Control.Exception
import qualified Data.Attoparsec.Text as AT
import           Data.Text ( Text )
import qualified Data.Text as Text
import qualified Data.Text.Lazy as Lazy
import qualified Data.Text.Lazy.Builder as Builder
import qualified Prettyprinter.Util as PPU
import qualified System.IO.Streams as Streams
import qualified System.IO.Streams.Attoparsec.Text as AStreams

import qualified What4.BaseTypes as BT
import qualified What4.Config as CFG
import           What4.Protocol.SExp
import qualified What4.Protocol.SMTLib2.Syntax as SMT2
import qualified What4.Protocol.SMTWriter as SMTWriter
import           What4.Utils.Process ( filterAsync )


strictSMTParsing :: CFG.ConfigOption BT.BaseBoolType
strictSMTParsing :: ConfigOption BaseBoolType
strictSMTParsing = BaseTypeRepr BaseBoolType -> String -> ConfigOption BaseBoolType
forall (tp :: BaseType).
BaseTypeRepr tp -> String -> ConfigOption tp
CFG.configOption BaseTypeRepr BaseBoolType
BT.BaseBoolRepr String
"solver.strict_parsing"

strictSMTParseOpt :: CFG.ConfigDesc
strictSMTParseOpt :: ConfigDesc
strictSMTParseOpt =
  ConfigOption BaseBoolType
-> OptionStyle BaseBoolType
-> Maybe (Doc Void)
-> Maybe (ConcreteVal BaseBoolType)
-> ConfigDesc
forall (tp :: BaseType).
ConfigOption tp
-> OptionStyle tp
-> Maybe (Doc Void)
-> Maybe (ConcreteVal tp)
-> ConfigDesc
CFG.mkOpt ConfigOption BaseBoolType
strictSMTParsing OptionStyle BaseBoolType
CFG.boolOptSty
  (Doc Void -> Maybe (Doc Void)
forall a. a -> Maybe a
Just (Doc Void -> Maybe (Doc Void)) -> Doc Void -> Maybe (Doc Void)
forall a b. (a -> b) -> a -> b
$ Text -> Doc Void
forall ann. Text -> Doc ann
PPU.reflow (Text -> Doc Void) -> Text -> Doc Void
forall a b. (a -> b) -> a -> b
$
   [Text] -> Text
Text.concat [Text
"Strictly parse SMT responses and fail on"
               , Text
"unrecognized data (the default)."
               , Text
"This might need to be disabled when running"
               , Text
"the SMT solver in verbose mode."
               ])
  Maybe (ConcreteVal BaseBoolType)
forall a. Maybe a
Nothing

smtParseOptions :: [CFG.ConfigDesc]
smtParseOptions :: [ConfigDesc]
smtParseOptions = [ ConfigDesc
strictSMTParseOpt ]


data SMTResponse = AckSuccess
                 | AckUnsupported
                 | AckError Text
                 | AckSat
                 | AckUnsat
                 | AckUnknown
                 | RspName Text
                 | RspVersion Text
                 | RspErrBehavior Text
                 | RspOutOfMemory
                 | RspRsnIncomplete
                 | RspUnkReason SExp
                 | AckSuccessSExp SExp
                 | AckSkipped Text SMTResponse
                 deriving (SMTResponse -> SMTResponse -> Bool
(SMTResponse -> SMTResponse -> Bool)
-> (SMTResponse -> SMTResponse -> Bool) -> Eq SMTResponse
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SMTResponse -> SMTResponse -> Bool
$c/= :: SMTResponse -> SMTResponse -> Bool
== :: SMTResponse -> SMTResponse -> Bool
$c== :: SMTResponse -> SMTResponse -> Bool
Eq, Int -> SMTResponse -> ShowS
[SMTResponse] -> ShowS
SMTResponse -> String
(Int -> SMTResponse -> ShowS)
-> (SMTResponse -> String)
-> ([SMTResponse] -> ShowS)
-> Show SMTResponse
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SMTResponse] -> ShowS
$cshowList :: [SMTResponse] -> ShowS
show :: SMTResponse -> String
$cshow :: SMTResponse -> String
showsPrec :: Int -> SMTResponse -> ShowS
$cshowsPrec :: Int -> SMTResponse -> ShowS
Show)

-- | Called to get a response from the SMT connection.

getSolverResponse :: SMTWriter.WriterConn t h
                  -> IO (Either SomeException SMTResponse)
getSolverResponse :: WriterConn t h -> IO (Either SomeException SMTResponse)
getSolverResponse WriterConn t h
conn = do
  Either SomeException SMTResponse
mb <- (SomeException -> Maybe SomeException)
-> IO SMTResponse -> IO (Either SomeException SMTResponse)
forall e b a.
Exception e =>
(e -> Maybe b) -> IO a -> IO (Either b a)
tryJust SomeException -> Maybe SomeException
filterAsync
        (Parser SMTResponse -> InputStream Text -> IO SMTResponse
forall r. Parser r -> InputStream Text -> IO r
AStreams.parseFromStream
          (ResponseStrictness -> Parser SMTResponse
rspParser (WriterConn t h -> ResponseStrictness
forall t h. WriterConn t h -> ResponseStrictness
SMTWriter.strictParsing WriterConn t h
conn))
          (WriterConn t h -> InputStream Text
forall t h. WriterConn t h -> InputStream Text
SMTWriter.connInputHandle WriterConn t h
conn))
  Either SomeException SMTResponse
-> IO (Either SomeException SMTResponse)
forall (m :: Type -> Type) a. Monad m => a -> m a
return Either SomeException SMTResponse
mb


-- | Gets a limited set of responses, throwing an exception when a
-- response is not matched by the filter.  Also throws exceptions for
-- standard error results.  The passed command and intent arguments
-- are only used for marking error messages.
--
-- Callers which do not want exceptions thrown for standard error
-- conditions should feel free to use 'getSolverResponse' and handle
-- all response cases themselves.

getLimitedSolverResponse :: String
                         -> (SMTResponse -> Maybe a)
                         -> SMTWriter.WriterConn t h
                         -> SMT2.Command
                         -> IO a
getLimitedSolverResponse :: String
-> (SMTResponse -> Maybe a) -> WriterConn t h -> Command -> IO a
getLimitedSolverResponse String
intent SMTResponse -> Maybe a
handleResponse WriterConn t h
conn Command
cmd =
  let validateResp :: SMTResponse -> m a
validateResp SMTResponse
rsp =
        case SMTResponse
rsp of
          SMTResponse
AckUnsupported -> SMTLib2Exception -> m a
forall a e. Exception e => e -> a
throw (Command -> SMTLib2Exception
SMTLib2Unsupported Command
cmd)
          (AckError Text
msg) -> SMTLib2Exception -> m a
forall a e. Exception e => e -> a
throw (Command -> Text -> SMTLib2Exception
SMTLib2Error Command
cmd Text
msg)
          (AckSkipped Text
_line SMTResponse
rest) -> SMTResponse -> m a
validateResp SMTResponse
rest
          SMTResponse
_ -> case SMTResponse -> Maybe a
handleResponse SMTResponse
rsp of
                 Just a
x -> a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return a
x
                 Maybe a
Nothing -> SMTLib2Exception -> m a
forall a e. Exception e => e -> a
throw (SMTLib2Exception -> m a) -> SMTLib2Exception -> m a
forall a b. (a -> b) -> a -> b
$ Command -> String -> SMTResponse -> SMTLib2Exception
SMTLib2InvalidResponse Command
cmd String
intent SMTResponse
rsp
  in WriterConn t h -> IO (Either SomeException SMTResponse)
forall t h. WriterConn t h -> IO (Either SomeException SMTResponse)
getSolverResponse WriterConn t h
conn IO (Either SomeException SMTResponse)
-> (Either SomeException SMTResponse -> IO a) -> IO a
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Right SMTResponse
rsp -> SMTResponse -> IO a
forall (m :: Type -> Type). Monad m => SMTResponse -> m a
validateResp SMTResponse
rsp
    Left (SomeException e
e) -> do
      Maybe Text
curInp <- InputStream Text -> IO (Maybe Text)
forall a. InputStream a -> IO (Maybe a)
Streams.read (WriterConn t h -> InputStream Text
forall t h. WriterConn t h -> InputStream Text
SMTWriter.connInputHandle WriterConn t h
conn)
      SMTLib2Exception -> IO a
forall a e. Exception e => e -> a
throw (SMTLib2Exception -> IO a) -> SMTLib2Exception -> IO a
forall a b. (a -> b) -> a -> b
$ String -> [Command] -> Text -> SMTLib2Exception
SMTLib2ParseError String
intent [Command
cmd] (Text -> SMTLib2Exception) -> Text -> SMTLib2Exception
forall a b. (a -> b) -> a -> b
$ String -> Text
Text.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$
        [String] -> String
unlines [ String
"Solver response parsing failure."
                , String
"*** Exception: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ e -> String
forall e. Exception e => e -> String
displayException e
e
                , String
"Attempting to parse input for " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
intent String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
":"
                , Maybe Text -> String
forall a. Show a => a -> String
show Maybe Text
curInp
                ]


rspParser :: SMTWriter.ResponseStrictness -> AT.Parser SMTResponse
rspParser :: ResponseStrictness -> Parser SMTResponse
rspParser ResponseStrictness
strictness =
  let lexeme :: Parser Text b -> Parser Text b
lexeme Parser Text b
p = Parser ()
skipSpaceOrNewline Parser () -> Parser Text b -> Parser Text b
forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> Parser Text b
p
      parens :: Parser Text a -> Parser Text a
parens Parser Text a
p = Char -> Parser Char
AT.char Char
'(' Parser Char -> Parser Text a -> Parser Text a
forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> Parser Text a
p Parser Text a -> Parser Char -> Parser Text a
forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f a
<* Char -> Parser Char
AT.char Char
')'
      errParser :: Parser SMTResponse
errParser = Parser SMTResponse -> Parser SMTResponse
forall a. Parser Text a -> Parser Text a
parens (Parser SMTResponse -> Parser SMTResponse)
-> Parser SMTResponse -> Parser SMTResponse
forall a b. (a -> b) -> a -> b
$ Parser Text Text -> Parser Text Text
forall a. Parser Text a -> Parser Text a
lexeme (Text -> Parser Text Text
AT.string Text
"error")
                  Parser Text Text -> Parser SMTResponse -> Parser SMTResponse
forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> (Text -> SMTResponse
AckError (Text -> SMTResponse) -> Parser Text Text -> Parser SMTResponse
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Text Text -> Parser Text Text
forall a. Parser Text a -> Parser Text a
lexeme Parser Text Text
parseSMTLib2String)
      specific_success_response :: Parser SMTResponse
specific_success_response = Parser SMTResponse
check_sat_response Parser SMTResponse -> Parser SMTResponse -> Parser SMTResponse
forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> Parser SMTResponse
get_info_response
      check_sat_response :: Parser SMTResponse
check_sat_response = (SMTResponse
AckSat SMTResponse -> Parser Text Text -> Parser SMTResponse
forall (f :: Type -> Type) a b. Functor f => a -> f b -> f a
<$ Text -> Parser Text Text
AT.string Text
"sat")
                           Parser SMTResponse -> Parser SMTResponse -> Parser SMTResponse
forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> (SMTResponse
AckUnsat SMTResponse -> Parser Text Text -> Parser SMTResponse
forall (f :: Type -> Type) a b. Functor f => a -> f b -> f a
<$ Text -> Parser Text Text
AT.string Text
"unsat")
                           Parser SMTResponse -> Parser SMTResponse -> Parser SMTResponse
forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> (SMTResponse
AckUnknown SMTResponse -> Parser Text Text -> Parser SMTResponse
forall (f :: Type -> Type) a b. Functor f => a -> f b -> f a
<$ Text -> Parser Text Text
AT.string Text
"unknown")
      get_info_response :: Parser SMTResponse
get_info_response = Parser SMTResponse -> Parser SMTResponse
forall a. Parser Text a -> Parser Text a
parens Parser SMTResponse
info_response
      info_response :: Parser SMTResponse
info_response = Parser SMTResponse
errBhvParser
                      Parser SMTResponse -> Parser SMTResponse -> Parser SMTResponse
forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> Parser SMTResponse
nameParser
                      Parser SMTResponse -> Parser SMTResponse -> Parser SMTResponse
forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> Parser SMTResponse
unkReasonParser
                      Parser SMTResponse -> Parser SMTResponse -> Parser SMTResponse
forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> Parser SMTResponse
versionParser
      nameParser :: Parser SMTResponse
nameParser = Parser Text Text -> Parser Text Text
forall a. Parser Text a -> Parser Text a
lexeme (Text -> Parser Text Text
AT.string Text
":name")
                   Parser Text Text -> Parser SMTResponse -> Parser SMTResponse
forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> Parser SMTResponse -> Parser SMTResponse
forall a. Parser Text a -> Parser Text a
lexeme (Text -> SMTResponse
RspName (Text -> SMTResponse) -> Parser Text Text -> Parser SMTResponse
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Text Text
parseSMTLib2String)
      versionParser :: Parser SMTResponse
versionParser = Parser Text Text -> Parser Text Text
forall a. Parser Text a -> Parser Text a
lexeme (Text -> Parser Text Text
AT.string Text
":version")
                      Parser Text Text -> Parser SMTResponse -> Parser SMTResponse
forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> Parser SMTResponse -> Parser SMTResponse
forall a. Parser Text a -> Parser Text a
lexeme (Text -> SMTResponse
RspVersion (Text -> SMTResponse) -> Parser Text Text -> Parser SMTResponse
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Text Text
parseSMTLib2String)
      errBhvParser :: Parser SMTResponse
errBhvParser = Parser Text Text -> Parser Text Text
forall a. Parser Text a -> Parser Text a
lexeme (Text -> Parser Text Text
AT.string Text
":error-behavior")
                     Parser Text Text -> Parser SMTResponse -> Parser SMTResponse
forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> Parser SMTResponse -> Parser SMTResponse
forall a. Parser Text a -> Parser Text a
lexeme (Text -> SMTResponse
RspErrBehavior (Text -> SMTResponse) -> Parser Text Text -> Parser SMTResponse
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$>
                                (Text -> Parser Text Text
AT.string Text
"continued-execution"
                                 Parser Text Text -> Parser Text Text -> Parser Text Text
forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> Text -> Parser Text Text
AT.string Text
"immediate-exit")
                                 -- Explicit error instead of generic
                                 -- fallback since :error-behavior was
                                 -- matched but behavior type was not.
                                 Parser SMTResponse -> Parser SMTResponse -> Parser SMTResponse
forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> SMTLib2Exception -> Parser SMTResponse
forall a e. Exception e => e -> a
throw (Command -> Text -> SMTLib2Exception
SMTLib2ResponseUnrecognized
                                            Command
SMT2.getErrorBehavior
                                            Text
"bad :error-behavior value")
                               )
      unkReasonParser :: Parser SMTResponse
unkReasonParser =
        Parser Text Text -> Parser Text Text
forall a. Parser Text a -> Parser Text a
lexeme (Text -> Parser Text Text
AT.string Text
":reason-unknown")
        Parser Text Text -> Parser SMTResponse -> Parser SMTResponse
forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> Parser SMTResponse -> Parser SMTResponse
forall a. Parser Text a -> Parser Text a
lexeme (SMTResponse
RspOutOfMemory SMTResponse -> Parser Text Text -> Parser SMTResponse
forall (f :: Type -> Type) a b. Functor f => a -> f b -> f a
<$ Text -> Parser Text Text
AT.string Text
"memout"
                    Parser SMTResponse -> Parser SMTResponse -> Parser SMTResponse
forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> SMTResponse
RspRsnIncomplete SMTResponse -> Parser Text Text -> Parser SMTResponse
forall (f :: Type -> Type) a b. Functor f => a -> f b -> f a
<$ Text -> Parser Text Text
AT.string Text
"incomplete"
                    Parser SMTResponse -> Parser SMTResponse -> Parser SMTResponse
forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> (Char -> Parser Char
AT.char Char
'(' Parser Char -> Parser SMTResponse -> Parser SMTResponse
forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> (SExp -> SMTResponse
RspUnkReason (SExp -> SMTResponse) -> Parser Text SExp -> Parser SMTResponse
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Text Text -> Parser Text SExp
parseSExpBody Parser Text Text
parseSMTLib2String))
                    -- already matched :reason-unknown, so any other
                    -- arguments to that are errors.
                    Parser SMTResponse -> Parser SMTResponse -> Parser SMTResponse
forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> SMTLib2Exception -> Parser SMTResponse
forall a e. Exception e => e -> a
throw (Command -> Text -> SMTLib2Exception
SMTLib2ResponseUnrecognized
                               (Builder -> Command
SMT2.Cmd Builder
"reason?")
                               Text
"bad :reason-unknown value")
                  )
  in Parser ()
skipSpaceOrNewline Parser () -> Parser SMTResponse -> Parser SMTResponse
forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*>
     ((SMTResponse
AckSuccess SMTResponse -> Parser Text Text -> Parser SMTResponse
forall (f :: Type -> Type) a b. Functor f => a -> f b -> f a
<$ Text -> Parser Text Text
AT.string Text
"success")
      Parser SMTResponse -> Parser SMTResponse -> Parser SMTResponse
forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> (SMTResponse
AckUnsupported SMTResponse -> Parser Text Text -> Parser SMTResponse
forall (f :: Type -> Type) a b. Functor f => a -> f b -> f a
<$ Text -> Parser Text Text
AT.string Text
"unsupported")
      Parser SMTResponse -> Parser SMTResponse -> Parser SMTResponse
forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> Parser SMTResponse
specific_success_response
      Parser SMTResponse -> Parser SMTResponse -> Parser SMTResponse
forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> Parser SMTResponse
errParser
      Parser SMTResponse -> Parser SMTResponse -> Parser SMTResponse
forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> (Char -> Parser Char
AT.char Char
'(' Parser Char -> Parser SMTResponse -> Parser SMTResponse
forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> (SExp -> SMTResponse
AckSuccessSExp (SExp -> SMTResponse) -> Parser Text SExp -> Parser SMTResponse
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Text Text -> Parser Text SExp
parseSExpBody Parser Text Text
parseSMTLib2String))
      -- sometimes verbose output mode will generate interim text
      -- before the actual ack; the following skips lines of input
      -- that aren't recognized.
       Parser SMTResponse -> Parser SMTResponse -> Parser SMTResponse
forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> (case ResponseStrictness
strictness of
              ResponseStrictness
SMTWriter.Strict -> Parser SMTResponse
forall (f :: Type -> Type) a. Alternative f => f a
empty
              ResponseStrictness
SMTWriter.Lenient -> Text -> SMTResponse -> SMTResponse
AckSkipped
                                   (Text -> SMTResponse -> SMTResponse)
-> Parser Text Text -> Parser Text (SMTResponse -> SMTResponse)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (Char -> Bool) -> Parser Text Text
AT.takeWhile1 (Bool -> Bool
not (Bool -> Bool) -> (Char -> Bool) -> Char -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Bool
AT.isEndOfLine)
                                   Parser Text (SMTResponse -> SMTResponse)
-> Parser SMTResponse -> Parser SMTResponse
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (ResponseStrictness -> Parser SMTResponse
rspParser ResponseStrictness
strictness))
     )

parseSMTLib2String :: AT.Parser Text
parseSMTLib2String :: Parser Text Text
parseSMTLib2String = Char -> Parser Char
AT.char Char
'\"' Parser Char -> Parser Text Text -> Parser Text Text
forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> Parser Text Text
go
 where
 go :: AT.Parser Text
 go :: Parser Text Text
go = do Text
xs <- (Char -> Bool) -> Parser Text Text
AT.takeWhile (Bool -> Bool
not (Bool -> Bool) -> (Char -> Bool) -> Char -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
==Char
'\"'))
         Char
_ <- Char -> Parser Char
AT.char Char
'\"'
         (do Char
_ <- Char -> Parser Char
AT.char Char
'\"'
             Text
ys <- Parser Text Text
go
             Text -> Parser Text Text
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Text
xs Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"\"" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
ys)
          ) Parser Text Text -> Parser Text Text -> Parser Text Text
forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> Text -> Parser Text Text
forall (m :: Type -> Type) a. Monad m => a -> m a
return Text
xs

----------------------------------------------------------------------

data SMTLib2Exception
  = SMTLib2Unsupported SMT2.Command
  | SMTLib2Error SMT2.Command Text
  | SMTLib2ParseError SMTLib2Intent [SMT2.Command] Text
  | SMTLib2ResponseUnrecognized SMT2.Command Text
  | SMTLib2InvalidResponse SMT2.Command SMTLib2Intent SMTResponse

type SMTLib2Intent = String

instance Show SMTLib2Exception where
  show :: SMTLib2Exception -> String
show =
    let showCmd :: Command -> String
showCmd (SMT2.Cmd Builder
c) = Text -> String
Lazy.unpack (Text -> String) -> Text -> String
forall a b. (a -> b) -> a -> b
$ Builder -> Text
Builder.toLazyText Builder
c
    in [String] -> String
unlines ([String] -> String)
-> (SMTLib2Exception -> [String]) -> SMTLib2Exception -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
      (SMTLib2Unsupported Command
cmd) ->
        [ String
"unsupported command:"
        , String
"  " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Command -> String
showCmd Command
cmd
        ]
      (SMTLib2Error Command
cmd Text
msg) ->
        [ String
"Solver reported an error:"
        , String
"  " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Text -> String
Text.unpack Text
msg
        , String
"in response to command:"
        , String
"  " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Command -> String
showCmd Command
cmd
        ]
      (SMTLib2ParseError String
intent [Command]
cmds Text
msg) ->
        [ String
"Could not parse solver response:"
        , String
"  " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Text -> String
Text.unpack Text
msg
        , String
"in response to commands for " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
intent String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
":"
        ] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (Command -> String) -> [Command] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Command -> String
showCmd [Command]
cmds
      (SMTLib2ResponseUnrecognized Command
cmd Text
rsp) ->
        [ String
"Unrecognized response from solver:"
        , String
"  " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Text -> String
Text.unpack Text
rsp
        , String
"in response to command:"
        , String
"  " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Command -> String
showCmd Command
cmd
        ]
      (SMTLib2InvalidResponse Command
cmd String
intent SMTResponse
rsp) ->
        [ String
"Received parsed and understood but unexpected response from solver:"
        , String
"  " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> SMTResponse -> String
forall a. Show a => a -> String
show SMTResponse
rsp
        , String
"in response to command for " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
intent String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
":"
        , String
"  " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Command -> String
showCmd Command
cmd
        ]

instance Exception SMTLib2Exception