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