    {-# LANGUAGE RankNTypes #-}
    {-# LANGUAGE Safe       #-}

    -- | Parse output of Kind2.
    module Copilot.Theorem.Kind2.Output (parseOutput) where

    import Data.List.Extra (isInfixOf, splitOn, stripInfix, trim)
    import Data.Maybe      (mapMaybe)

    import Copilot.Theorem.Prove as P

    import qualified Copilot.Core as C

    import qualified Copilot.Theorem.Misc.Error as Err

    -- | Parse output of Kind2.
    --
    -- The output is expected to be in XML format, as produced by Kind2's @-xml@
    -- flag and documented at
    -- <https://kind.cs.uiowa.edu/kind2_user_doc/3_output/2_machine_readable.html>.
    -- Note that this function does not parse the output as XML: when given a
    -- system in the native transition system format, Kind2 produces output that
    -- is not always well-formed XML (e.g., counterexamples to invariant
    -- properties cannot be printed for systems in that format -- the
    -- counterexample printing functions in Kind2's @src/inputSystem.ml@ fail with
    -- an internal error for native input -- and Kind2 reports the error in the
    -- middle of the XML output). Instead, this function looks for the
    -- @\<Property\>@ tag for the given property and extracts the answers in the
    -- @\<Answer\>@ tags it contains.
    parseOutput :: String    -- ^ Property whose validity is being checked.
                -> C.Prop    -- ^ The property's quantifier.
                -> String    -- ^ XML output of Kind2
                -> P.Output
    parseOutput :: String -> Prop -> String -> Output
    parseOutput String
    propId Prop
    propQuantifier String
    xml
        | String
    "valid"       String -> [String] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [String]
    answers = Output -> Output -> Output
    forall {p}. p -> p -> p
    quantified (Status -> [String] -> Output
    Output Status
    Valid   [])
                                                    (Status -> [String] -> Output
    Output Status
    Invalid [])
        | String
    "falsifiable" String -> [String] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [String]
    answers = Output -> Output -> Output
    forall {p}. p -> p -> p
    quantified (Status -> [String] -> Output
    Output Status
    Invalid [])
                                                    (Status -> [String] -> Output
    Output Status
    Valid   [])
        | String
    "unknown"     String -> [String] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [String]
    answers = Status -> [String] -> Output
    Output Status
    Unknown []
        | [String] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [String]
    answers = String -> Output
    forall a. String -> a
    err (String -> Output) -> String -> Output
    forall a b. (a -> b) -> a -> b
    $ String
    "Answer for property " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    propId String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " not found"
        | Bool
    otherwise    = String -> Output
    forall a. String -> a
    err (String -> Output) -> String -> Output
    forall a b. (a -> b) -> a -> b
    $ String
    "Unrecognized status : " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords [String]
    answers

      where

        -- Pick an output based on the quantifier of the property. The first
        -- argument is returned when the property Kind2 was asked about is valid,
        -- and the second one when it is invalid.
        --
        -- We encode a universally quantified property P as ∀x.P(x) in Kind2, so
        -- the original property is valid iff the Kind2 property is valid.
        --
        -- We encode an existentially quantified property P as ¬(∀x.¬(P(x))) in
        -- Kind2, so the original property is valid iff the Kind2 property is
        -- invalid.
        quantified :: p -> p -> p
    quantified p
    ifValid p
    ifInvalid = case Prop
    propQuantifier of
          C.Forall {} -> p
    ifValid
          C.Exists {} -> p
    ifInvalid

        -- All the answers reported for the property, in the order in which they
        -- appear in the output. A conclusive answer (valid or falsifiable), if
        -- any, takes precedence over inconclusive (unknown) ones, which Kind2 may
        -- also report when the analysis terminates without an answer for all
        -- properties.
        answers :: [String]
    answers = (String -> Maybe String) -> [String] -> [String]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe String -> Maybe String
    answerText
                ([String] -> [String]) -> [String] -> [String]
    forall a b. (a -> b) -> a -> b
    $ (String -> Bool) -> [String] -> [String]
    forall a. (a -> Bool) -> [a] -> [a]
    filter String -> Bool
    isRightProperty
                ([String] -> [String]) -> [String] -> [String]
    forall a b. (a -> b) -> a -> b
    $ String -> [String]
    propertyElems String
    xml

        -- Substrings of the output following a @\<Property @ opening tag, each
        -- extending to the next such tag (or to the end of the output).
        propertyElems :: String -> [String]
    propertyElems = Int -> [String] -> [String]
    forall a. Int -> [a] -> [a]
    drop Int
    1 ([String] -> [String])
    -> (String -> [String]) -> String -> [String]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> String -> [String]
    forall a. (Partial, Eq a) => [a] -> [a] -> [[a]]
    splitOn String
    "<Property "

        -- True if the given property element has the name of the property this
        -- function looks for.
        isRightProperty :: String -> Bool
    isRightProperty String
    elem' =
          (String
    "name=\"" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> String
    escapeAttr String
    propId String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "\"") String -> String -> Bool
    forall a. Eq a => [a] -> [a] -> Bool
    `isInfixOf` String
    openingTag
          where
            openingTag :: String
    openingTag = (Char -> Bool) -> String -> String
    forall a. (a -> Bool) -> [a] -> [a]
    takeWhile (Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Char
    '>') String
    elem'

        -- The contents of the first @\<Answer\>@ tag in the given element, if
        -- any.
        answerText :: String -> Maybe String
    answerText String
    elem' = do
          (_, rest)  <- String -> String -> Maybe (String, String)
    forall a. Eq a => [a] -> [a] -> Maybe ([a], [a])
    stripInfix String
    "<Answer" String
    elem'
          (_, rest') <- stripInfix ">" rest
          let answer = String -> String
    trim (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ (Char -> Bool) -> String -> String
    forall a. (a -> Bool) -> [a] -> [a]
    takeWhile (Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Char
    '<') String
    rest'
          if null answer then Nothing else Just answer

        err :: forall a . String -> a
        err :: forall a. String -> a
    err String
    msg = String -> a
    forall a. String -> a
    Err.fatal (String -> a) -> String -> a
    forall a b. (a -> b) -> a -> b
    $
          String
    "Parse error while reading the Kind2 XML output : \n"
          String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    msg String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "\n\n" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    xml

    -- | Escape a string for use as an XML attribute value.
    escapeAttr :: String -> String
    escapeAttr :: String -> String
    escapeAttr = (Char -> String) -> String -> String
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap Char -> String
    escapeChar
      where
        escapeChar :: Char -> String
    escapeChar Char
    '&' = String
    "&amp;"
        escapeChar Char
    '<' = String
    "&lt;"
        escapeChar Char
    '>' = String
    "&gt;"
        escapeChar Char
    '"' = String
    "&quot;"
        escapeChar Char
    c   = [Char
    c]