content: {-# 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 s = QName s Nothing 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 propId propQuantifier xml = fromJust $ do
    root <- parseXMLDoc xml
    case findAnswer . findPropTag $ root of
      "valid"       -> case 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 {} -> return (Output 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 {} -> return (Output Invalid [])
      "falsifiable" -> case 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 {} -> return (Output 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 {} -> return (Output Valid   [])
      s             -> err $ "Unrecognized status : " ++ s
  
    where
  
      searchForRuntimeError = undefined
  
      findPropTag root =
        let rightElement elt =
              qName (elName elt) == "Property"
              && lookupAttr (simpleName "name") (elAttribs elt)
                  == Just propId
        in case filterChildren rightElement root of
             tag : _ -> tag
             _ -> err $ "Tag for property " ++ propId ++ " not found"
  
      findAnswer tag =
        case findChildren (simpleName "Answer") tag of
          answTag : _ ->
            case onlyText (elContent answTag) of
              answ : _ -> cdData answ
              _ -> err "Invalid 'Answer' attribute"
          _ -> err "Attribute 'Answer' not found"
  
      err :: forall a . String -> a
      err msg = Err.fatal $
        "Parse error while reading the Kind2 XML output : \n"
        ++ msg ++ "\n\n" ++ xml
  