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

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

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.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

parseOutput :: String -> String -> P.Output
parseOutput :: String -> String -> Output
parseOutput String
prop 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
  Element
root <- String -> Maybe Element
forall s. XmlSource s => s -> Maybe Element
parseXMLDoc String
xml
  case Element -> String
findAnswer (Element -> String) -> (Element -> Element) -> Element -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Element -> Element
findPropTag (Element -> String) -> Element -> String
forall a b. (a -> b) -> a -> b
$ Element
root of
    String
"valid"   -> Output -> Maybe Output
forall (m :: * -> *) a. Monad m => a -> m a
return (Status -> [String] -> Output
Output Status
Valid   [])
    String
"invalid" -> Output -> Maybe Output
forall (m :: * -> *) a. Monad m => a -> m a
return (Status -> [String] -> Output
Output Status
Invalid [])
    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
prop
      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
prop 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 :: 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

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