content: {-|
  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.Maybe ( isJust )
  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 = CFG.configOption BT.BaseBoolRepr "solver.strict_parsing"
  
  strictSMTParseOpt :: CFG.ConfigDesc
  strictSMTParseOpt =
    CFG.mkOpt strictSMTParsing CFG.boolOptSty
    (Just $ PPU.reflow $
     Text.concat ["Strictly parse SMT responses and fail on"
                 , "unrecognized data (the default)."
                 , "This might need to be disabled when running"
                 , "the SMT solver in verbose mode."
                 ])
    Nothing
  
  smtParseOptions :: [CFG.ConfigDesc]
  smtParseOptions = [ strictSMTParseOpt ]
  
  
  data SMTResponse = AckSuccess
                   | AckUnsupported
                   | AckError Text
                   | AckSat
                   | AckUnsat
                   | AckUnknown
                   | AckInfeasible -- SyGuS response
                   | AckFail -- SyGuS response
                   | RspName Text
                   | RspVersion Text
                   | RspErrBehavior Text
                   | RspOutOfMemory
                   | RspRsnIncomplete
                   | RspUnkReason SExp
                   | AckSuccessSExp SExp
                   | AckSkipped Text SMTResponse
                   deriving (Eq, Show)
  
  -- | Called to get a response from the SMT connection.
  
  getSolverResponse :: SMTWriter.WriterConn t h
                    -> IO (Either SomeException SMTResponse)
  getSolverResponse conn = do
    mb <- tryJust filterAsync
          (AStreams.parseFromStream
            -- n.b. the parseFromStream with an attoparsec parser used
            -- here will throw
            -- System.IO.Streams.Attoparsec.ParseException on a parser
            -- failure; the rspParser throws some other parse errors
            (rspParser (SMTWriter.strictParsing conn))
            (SMTWriter.connInputHandle conn))
    return 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 intent handleResponse conn cmd =
    let validateResp rsp =
          case rsp of
            AckUnsupported -> throw (SMTLib2Unsupported cmd)
            (AckError msg) -> throw (SMTLib2Error cmd msg)
            (AckSkipped _line rest) -> validateResp rest
            _ -> case handleResponse rsp of
                   Just x -> return x
                   Nothing -> throw $ SMTLib2InvalidResponse cmd intent rsp
    in getSolverResponse conn >>= \case
      Right rsp -> validateResp rsp
      Left se@(SomeException e)
        | isJust $ filterAsync se -> throw e
        | Just (AStreams.ParseException _) <- fromException se
          -> do -- Parser failed and left the unparseable input in the
                -- stream; extract it to show the user
                curInp <- Streams.read (SMTWriter.connInputHandle conn)
                throw $ SMTLib2ParseError intent [cmd] $ Text.pack $
                  unlines [ "Solver response parsing failure."
                          , "*** Exception: " ++ displayException e
                          , "Attempting to parse input for " <> intent <> ":"
                          , show curInp
                          ]
        | otherwise -> throw e
  
  
  
  rspParser :: SMTWriter.ResponseStrictness -> AT.Parser SMTResponse
  rspParser strictness =
    let lexeme p = skipSpaceOrNewline *> p
        parens p = AT.char '(' *> p <* AT.char ')'
        errParser = parens $ lexeme (AT.string "error")
                    *> (AckError <$> lexeme parseSMTLib2String)
        specific_success_response = check_sat_response <|> check_synth_response <|> get_info_response
        check_sat_response = (AckSat <$ AT.string "sat")
                             <|> (AckUnsat <$ AT.string "unsat")
                             <|> (AckUnknown <$ AT.string "unknown")
        check_synth_response = (AckInfeasible <$ AT.string "infeasible")
                               <|> (AckFail <$ AT.string "fail")
        get_info_response = parens info_response
        info_response = errBhvParser
                        <|> nameParser
                        <|> unkReasonParser
                        <|> versionParser
        nameParser = lexeme (AT.string ":name")
                     *> lexeme (RspName <$> parseSMTLib2String)
        versionParser = lexeme (AT.string ":version")
                        *> lexeme (RspVersion <$> parseSMTLib2String)
        errBhvParser = lexeme (AT.string ":error-behavior")
                       *> lexeme (RspErrBehavior <$>
                                  (AT.string "continued-execution"
                                   <|> AT.string "immediate-exit")
                                   -- Explicit error instead of generic
                                   -- fallback since :error-behavior was
                                   -- matched but behavior type was not.
                                   <|> throw (SMTLib2ResponseUnrecognized
                                              SMT2.getErrorBehavior
                                              "bad :error-behavior value")
                                 )
        unkReasonParser =
          lexeme (AT.string ":reason-unknown")
          *> lexeme (RspOutOfMemory <$ AT.string "memout"
                      <|> RspRsnIncomplete <$ AT.string "incomplete"
                      <|> (AT.char '(' *> (RspUnkReason <$> parseSExpBody parseSMTLib2String))
                      -- already matched :reason-unknown, so any other
                      -- arguments to that are errors.
                      <|> throw (SMTLib2ResponseUnrecognized
                                 (SMT2.Cmd "reason?")
                                 "bad :reason-unknown value")
                    )
    in skipSpaceOrNewline *>
       ((AckSuccess <$ AT.string "success")
        <|> (AckUnsupported <$ AT.string "unsupported")
        <|> specific_success_response
        <|> errParser
        <|> (AT.char '(' *> (AckSuccessSExp <$> parseSExpBody parseSMTLib2String))
        -- sometimes verbose output mode will generate interim text
        -- before the actual ack; the following skips lines of input
        -- that aren't recognized.
         <|> (case strictness of
                SMTWriter.Strict -> empty
                SMTWriter.Lenient -> AckSkipped
                                     <$> AT.takeWhile1 (not . AT.isEndOfLine)
                                     <*> (rspParser strictness))
       )
  
  parseSMTLib2String :: AT.Parser Text
  parseSMTLib2String = AT.char '\"' >> go
   where
   go :: AT.Parser Text
   go = do xs <- AT.takeWhile (not . (=='\"'))
           _ <- AT.char '\"'
           (do _ <- AT.char '\"'
               ys <- go
               return (xs <> "\"" <> ys)
            ) <|> return 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 =
      let showCmd (SMT2.Cmd c) = Lazy.unpack $ Builder.toLazyText c
      in unlines . \case
        (SMTLib2Unsupported cmd) ->
          [ "unsupported command:"
          , "  " <> showCmd cmd
          ]
        (SMTLib2Error cmd msg) ->
          [ "Solver reported an error:"
          , "  " ++ Text.unpack msg
          , "in response to command:"
          , "  " <> showCmd cmd
          ]
        (SMTLib2ParseError intent cmds msg) ->
          [ "Could not parse solver response:"
          , "  " ++ Text.unpack msg
          , "in response to commands for " <> intent <> ":"
          ] ++ map showCmd cmds
        (SMTLib2ResponseUnrecognized cmd rsp) ->
          [ "Unrecognized response from solver:"
          , "  " <> Text.unpack rsp
          , "in response to command:"
          , "  " <> showCmd cmd
          ]
        (SMTLib2InvalidResponse cmd intent rsp) ->
          [ "Received parsed and understood but unexpected response from solver:"
          , "  " <> show rsp
          , "in response to command for " <> intent <> ":"
          , "  " <> showCmd cmd
          ]
  
  instance Exception SMTLib2Exception
  