hets/PGIP/XMLstate.hs

{- |
Module      : ./PGIP/XMLstate.hs
Description : after parsing XML message a list of XMLcommands is produced,
              containing commands that need to be executed
Copyright   : uni-bremen and DFKI
License     : GPLv2 or higher, see LICENSE.txt
Maintainer  : r.pascanu@jacobs-university.de
Stability   : provisional
Portability : portable

PGIP.XMLstate contains the description of the XMLstate and a function
that produces such a state
-}

module PGIP.XMLstate where

import Common.Utils (getEnvDef, trim)
import Common.ToXml
import Driver.Options

import Text.XML.Light

import Data.List (find, intercalate)
import Data.Time.Clock.POSIX (getPOSIXTime)

import System.IO (Handle, hPutStrLn, hFlush)

{- Converts any line text that does not stand for a
comment into a theoryitem element -}
genProofStep :: String -> Element
genProofStep str = let
    iname = case trim str of
             "" -> "whitespace"   -- empty line generates a whitespace element
             '#' : _ -> "comment" -- comments start with #
             _ -> "theoryitem"    -- convert line into a theoryitem element

    in unode iname $ mkText $ str ++ "\n"

-- | adds xml structure to unstructured code
addPGIPMarkup :: String -> Element
addPGIPMarkup str = case lines str of
  [] -> error "addPgipMarkUp.empty"
  hd : tl ->
    unode "parseresult"
      $ add_attr (mkAttr "thyname" "whatever") (unode "opentheory" $ mkText hd)
      : map genProofStep tl
      ++ [unode "closetheory" ()]

{-
 - other types of mark ups :
 -   opengoal / closegoal
 -   openblock / closeblock
 -
 -}

-- generates a pgipelem element that contains the input text
genPgipElem :: String -> Element
genPgipElem = unode "pgipelem" . mkText

{- generates a normalresponse element that has a pgml element
containing the output text -}
genNormalResponse :: Node t => String -> t -> Element
genNormalResponse areaValue = unode "normalresponse"
    . add_attr (mkAttr "area" areaValue)
    . unode "pgml"

-- same as above, just for an error instead of normal output
genErrorResponse :: Bool -> String -> Element
genErrorResponse fatality =
  add_attrs [ mkAttr "fatality" "fatal" | fatality]
  . unode "errorresponse"
  . unode "pgmltext" . mkText

{- | It inserts a given string into the XML packet as
normal output -}
addPGIPAnswer :: String -> String -> CmdlPgipState -> CmdlPgipState
addPGIPAnswer msgtxt errmsg st =
    if useXML st
    then let resp = if null msgtxt then st else
               addPGIPElement st $ genNormalResponse "message"
               $ mkText msgtxt
         in if null errmsg then resp
         else addPGIPElement resp $ genErrorResponse False errmsg
    else addToMsg errmsg $ addToMsg msgtxt st

{- | It inserts a given string into the XML packet as
error output -}
addPGIPError :: String -> CmdlPgipState -> CmdlPgipState
addPGIPError str st = case str of
  "" -> st
  _ | useXML st -> addPGIPElement st $ genErrorResponse True str
  _ -> addToMsg str st

-- extracts the xml package in XML.Light format (namely the Content type)
addPGIPAttributes :: CmdlPgipState -> Element -> Element
addPGIPAttributes pgipData e = (add_attrs
  ((case refSeqNb pgipData of
      Nothing -> []
      Just v -> [mkAttr "refseq" v])
   ++ [ mkAttr "tag" $ name pgipData
      , mkAttr "class" "pg"
      , mkAttr "id" $ pgipId pgipData
      , mkAttr "seq" $ show $ seqNb pgipData ])
  $ unode "pgip" ()) { elContent = [Elem e]}

{- adds one element to the end of the content of the xml packet that represents
the current output of the interface to the broker -}
addPGIPElement :: CmdlPgipState -> Element -> CmdlPgipState
addPGIPElement pgData el =
  pgData { xmlElements = addPGIPAttributes pgData el : xmlElements pgData
         , seqNb = seqNb pgData + 1 }

{- adds a ready element at the end of the xml packet that represents the
current output of the interface to the broker -}
addPGIPReady :: CmdlPgipState -> CmdlPgipState
addPGIPReady pgData = addPGIPElement pgData $ unode "ready" ()

-- | State that keeps track of the comunication between Hets and the Broker
data CmdlPgipState = CmdlPgipState
  { pgipId :: String
  , name :: String
  , seqNb :: Int
  , refSeqNb :: Maybe String
  , msgs :: [String]
  , xmlElements :: [Element]
  , hout :: Handle
  , hin :: Handle
  , stop :: Bool
  , resendMsgIfTimeout :: Bool
  , useXML :: Bool
  , maxWaitTime :: Int }

-- | Generates an empty CmdlPgipState
genCMDLPgipState :: Bool -> Handle -> Handle -> Int -> IO CmdlPgipState
genCMDLPgipState swXML h_in h_out timeOut = do
   pgId <- genPgipID
   return CmdlPgipState
     { pgipId = pgId
     , name = "Hets"
     , seqNb = 1
     , refSeqNb = Nothing
     , msgs = []
     , xmlElements = []
     , hin = h_in
     , hout = h_out
     , stop = False
     , resendMsgIfTimeout = True
     , useXML = swXML
     , maxWaitTime = timeOut }

-- | Generates the id of the session between Hets and the Broker
genPgipID :: IO String
genPgipID =
  do
   t1 <- getEnvDef "HOSTNAME" ""
   t2 <- getEnvDef "USER" ""
   t3 <- getPOSIXTime
   return $ t1 ++ "/" ++ t2 ++ "/" ++ show t3

-- | Concatenates the input string to the message stored in the state
addToMsg :: String -> CmdlPgipState -> CmdlPgipState
addToMsg str pgD = if null str then pgD else pgD { msgs = str : msgs pgD }

-- | Resets the content of the message stored in the state
resetPGIPData :: CmdlPgipState -> CmdlPgipState
resetPGIPData pgD = pgD
  { msgs = []
  , xmlElements = [] }

{- the PGIP protocol defines the pgip element as containing a single
subelement. -}
convertPGIPDataToString :: CmdlPgipState -> String
convertPGIPDataToString =
  intercalate "\n" . reverse . map showElement . xmlElements

isRemote :: HetcatsOpts -> Bool
isRemote opts = connectP opts /= -1 || listen opts /= -1

sendPGIPData :: HetcatsOpts -> CmdlPgipState -> IO CmdlPgipState
sendPGIPData opts pgData =
  do
    let xmlMsg = convertPGIPDataToString pgData
        pgData' = addToMsg xmlMsg pgData
    sendMSGData opts pgData'

sendMSGData :: HetcatsOpts -> CmdlPgipState -> IO CmdlPgipState
sendMSGData opts pgData = do
  let msg = intercalate "\n" $ reverse $ msgs pgData
  if isRemote opts
    then hPutStrLn (hout pgData) msg
    else putIfVerbose opts 1 msg
  hFlush $ hout pgData
  return pgData

-- | List of all possible commands inside an XML packet
data CmdlXMLcommands =
   XmlExecute String
 | XmlExit
 | XmlProverInit
 | XmlAskpgip
 | XmlStartQuiet
 | XmlStopQuiet
 | XmlOpenGoal String
 | XmlCloseGoal String
 | XmlGiveUpGoal String
 | XmlUnknown String
 | XmlParseScript String
 | XmlUndo
 | XmlRedo
 | XmlForget String
 | XmlOpenTheory String
 | XmlCloseTheory String
 | XmlCloseFile String
 | XmlLoadFile String deriving (Eq, Show)

-- extracts the seq attribute value to be used as reference number elsewhere
getRefseqNb :: String -> Maybe String
getRefseqNb input =
  let xmlTree = parseXML input
      elRef = find (\ x -> case x of
                              Elem dt -> qName (elName dt) == "pgip"
                              _ -> False) xmlTree
   in case elRef of
        Nothing -> Nothing
        Just el -> case el of
                     Elem dt -> case find (\ x -> qName (attrKey x) == "seq") $
                                     elAttribs dt of
                                  Nothing -> Nothing
                                  Just elatr -> Just $ attrVal elatr
                     _ -> Nothing

{- | parses the xml message creating a list of commands that it needs to
execute -}
parseXMLTree :: [Content] -> [CmdlXMLcommands] -> [CmdlXMLcommands]
parseXMLTree xmltree acc = case xmltree of
    Elem info : ls -> case parseXMLElement info of
                        Just c -> parseXMLTree ls (c : acc)
                        Nothing -> parseXMLTree (elContent info ++ ls) acc
    _ : ls -> parseXMLTree ls acc
    [] -> acc

parseXMLElement :: Element -> Maybe CmdlXMLcommands
parseXMLElement info = let cnt = strContent info in
  case qName $ elName info of
    "proverinit" -> Just XmlProverInit
    "proverexit" -> Just XmlExit
    "startquiet" -> Just XmlStartQuiet
    "stopquiet" -> Just XmlStopQuiet
    "opengoal" -> Just $ XmlOpenGoal cnt
    "proofstep" -> Just $ XmlExecute cnt
    "closegoal" -> Just $ XmlCloseGoal cnt
    "giveupgoal" -> Just $ XmlGiveUpGoal cnt
    "spurioscmd" -> Just $ XmlExecute cnt
    "dostep" -> Just $ XmlExecute cnt
    "editobj" -> Just $ XmlExecute cnt
    "undostep" -> Just XmlUndo
    "redostep" -> Just XmlRedo
    "forget" -> Just $ XmlForget cnt
    "opentheory" -> Just $ XmlOpenTheory cnt
    "theoryitem" -> Just $ XmlExecute cnt
    "closetheory" -> Just $ XmlCloseTheory cnt
    "closefile" -> Just $ XmlCloseFile cnt
    "loadfile" -> Just $ XmlLoadFile cnt
    "askpgip" -> Just XmlAskpgip
    "parsescript" -> Just $ XmlParseScript cnt
    "pgip" -> Nothing
    s -> Just $ XmlUnknown s

{- | Given a packet (a normal string or a xml formated string), the function
converts it into a list of commands -}
parseMsg :: CmdlPgipState -> String -> [CmdlXMLcommands]
parseMsg st input = if useXML st
   then parseXMLTree (parseXML input) []
   else concatMap (\ x -> [ XmlExecute x | not $ null $ trim x ]) $ lines input