content: {- |
  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
  