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

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

    import Text.XML.Light       hiding (findChild)
    import Copilot.Theorem.Prove  as P
    import Data.Maybe           (fromJust)

    import qualified Copilot.Core as C

    import qualified Copilot.Theorem.Misc.Error as Err

    simpleName :: String -> QName
    simpleName String
    s = String -> Maybe String -> Maybe String -> QName
    QName String
    s Maybe String
    forall a. Maybe a
    Nothing Maybe String
    forall a. Maybe a
    Nothing

    -- | Parse output of Kind2.
    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 = Maybe Output -> Output
    forall a. HasCallStack => Maybe a -> a
    fromJust (Maybe Output -> Output) -> Maybe Output -> Output
    forall a b. (a -> b) -> a -> b
    $ do
      root <- String -> Maybe Element
    forall s. XmlSource s => s -> Maybe Element
    parseXMLDoc String
    xml
      case findAnswer . findPropTag $ root of
        String
    "valid"       -> case Prop
    propQuantifier of
                           -- 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.
                           C.Forall {} -> Output -> Maybe Output
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Status -> [String] -> Output
    Output Status
    Valid   [])
                           -- We encode an existentially quantified property P as
                           -- ¬(∀x.¬(P(x))) in Kind2, so the original property is
                           -- invalid iff the Kind2 property is valid.
                           C.Exists {} -> Output -> Maybe Output
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Status -> [String] -> Output
    Output Status
    Invalid [])
        String
    "falsifiable" -> case Prop
    propQuantifier of
                           -- We encode a universally quantified property P as
                           -- ∀x.P(x) in Kind2, so the original property is invalid
                           -- iff the Kind2 property is invalid.
                           C.Forall {} -> Output -> Maybe Output
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Status -> [String] -> Output
    Output Status
    Invalid [])
                           -- 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.
                           C.Exists {} -> Output -> Maybe Output
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Status -> [String] -> Output
    Output Status
    Valid   [])
        String
    s             -> String -> Maybe Output
    forall a. String -> a
    err (String -> Maybe Output) -> String -> Maybe Output
    forall a b. (a -> b) -> a -> b
    $ String
    "Unrecognized status : " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    s

      where

        searchForRuntimeError :: a
    searchForRuntimeError = a
    forall a. HasCallStack => a
    undefined

        findPropTag :: Element -> Element
    findPropTag Element
    root =
          let rightElement :: Element -> Bool
    rightElement Element
    elt =
                QName -> String
    qName (Element -> QName
    elName Element
    elt) String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    == String
    "Property"
                Bool -> Bool -> Bool
    && QName -> [Attr] -> Maybe String
    lookupAttr (String -> QName
    simpleName String
    "name") (Element -> [Attr]
    elAttribs Element
    elt)
                    Maybe String -> Maybe String -> Bool
    forall a. Eq a => a -> a -> Bool
    == String -> Maybe String
    forall a. a -> Maybe a
    Just String
    propId
          in case (Element -> Bool) -> Element -> [Element]
    filterChildren Element -> Bool
    rightElement Element
    root of
               Element
    tag : [Element]
    _ -> Element
    tag
               [Element]
    _ -> String -> Element
    forall a. String -> a
    err (String -> Element) -> String -> Element
    forall a b. (a -> b) -> a -> b
    $ String
    "Tag for property " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    propId String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " not found"

        findAnswer :: Element -> String
    findAnswer Element
    tag =
          case QName -> Element -> [Element]
    findChildren (String -> QName
    simpleName String
    "Answer") Element
    tag of
            Element
    answTag : [Element]
    _ ->
              case [Content] -> [CData]
    onlyText (Element -> [Content]
    elContent Element
    answTag) of
                CData
    answ : [CData]
    _ -> CData -> String
    cdData CData
    answ
                [CData]
    _ -> String -> String
    forall a. String -> a
    err String
    "Invalid 'Answer' attribute"
            [Element]
    _ -> String -> String
    forall a. String -> a
    err String
    "Attribute 'Answer' not found"

        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