{- |
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 :: String -> Element
genProofStep str :: String
str = let
    iname :: String
iname = case String -> String
trim String
str of
             "" -> "whitespace"   -- empty line generates a whitespace element
             '#' : _ -> "comment" -- comments start with #
             _ -> "theoryitem"    -- convert line into a theoryitem element

    in String -> Content -> Element
forall t. Node t => String -> t -> Element
unode String
iname (Content -> Element) -> Content -> Element
forall a b. (a -> b) -> a -> b
$ String -> Content
mkText (String -> Content) -> String -> Content
forall a b. (a -> b) -> a -> b
$ String
str String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n"

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

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

-- generates a pgipelem element that contains the input text
genPgipElem :: String -> Element
genPgipElem :: String -> Element
genPgipElem = String -> Content -> Element
forall t. Node t => String -> t -> Element
unode "pgipelem" (Content -> Element) -> (String -> Content) -> String -> Element
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Content
mkText

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

-- same as above, just for an error instead of normal output
genErrorResponse :: Bool -> String -> Element
genErrorResponse :: Bool -> String -> Element
genErrorResponse fatality :: Bool
fatality =
  [Attr] -> Element -> Element
add_attrs [ String -> String -> Attr
mkAttr "fatality" "fatal" | Bool
fatality]
  (Element -> Element) -> (String -> Element) -> String -> Element
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Element -> Element
forall t. Node t => String -> t -> Element
unode "errorresponse"
  (Element -> Element) -> (String -> Element) -> String -> Element
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Content -> Element
forall t. Node t => String -> t -> Element
unode "pgmltext" (Content -> Element) -> (String -> Content) -> String -> Element
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Content
mkText

{- | It inserts a given string into the XML packet as
normal output -}
addPGIPAnswer :: String -> String -> CmdlPgipState -> CmdlPgipState
addPGIPAnswer :: String -> String -> CmdlPgipState -> CmdlPgipState
addPGIPAnswer msgtxt :: String
msgtxt errmsg :: String
errmsg st :: CmdlPgipState
st =
    if CmdlPgipState -> Bool
useXML CmdlPgipState
st
    then let resp :: CmdlPgipState
resp = if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
msgtxt then CmdlPgipState
st else
               CmdlPgipState -> Element -> CmdlPgipState
addPGIPElement CmdlPgipState
st (Element -> CmdlPgipState) -> Element -> CmdlPgipState
forall a b. (a -> b) -> a -> b
$ String -> Content -> Element
forall t. Node t => String -> t -> Element
genNormalResponse "message"
               (Content -> Element) -> Content -> Element
forall a b. (a -> b) -> a -> b
$ String -> Content
mkText String
msgtxt
         in if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
errmsg then CmdlPgipState
resp
         else CmdlPgipState -> Element -> CmdlPgipState
addPGIPElement CmdlPgipState
resp (Element -> CmdlPgipState) -> Element -> CmdlPgipState
forall a b. (a -> b) -> a -> b
$ Bool -> String -> Element
genErrorResponse Bool
False String
errmsg
    else String -> CmdlPgipState -> CmdlPgipState
addToMsg String
errmsg (CmdlPgipState -> CmdlPgipState) -> CmdlPgipState -> CmdlPgipState
forall a b. (a -> b) -> a -> b
$ String -> CmdlPgipState -> CmdlPgipState
addToMsg String
msgtxt CmdlPgipState
st

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

-- extracts the xml package in XML.Light format (namely the Content type)
addPGIPAttributes :: CmdlPgipState -> Element -> Element
addPGIPAttributes :: CmdlPgipState -> Element -> Element
addPGIPAttributes pgipData :: CmdlPgipState
pgipData e :: Element
e = ([Attr] -> Element -> Element
add_attrs
  ((case CmdlPgipState -> Maybe String
refSeqNb CmdlPgipState
pgipData of
      Nothing -> []
      Just v :: String
v -> [String -> String -> Attr
mkAttr "refseq" String
v])
   [Attr] -> [Attr] -> [Attr]
forall a. [a] -> [a] -> [a]
++ [ String -> String -> Attr
mkAttr "tag" (String -> Attr) -> String -> Attr
forall a b. (a -> b) -> a -> b
$ CmdlPgipState -> String
name CmdlPgipState
pgipData
      , String -> String -> Attr
mkAttr "class" "pg"
      , String -> String -> Attr
mkAttr "id" (String -> Attr) -> String -> Attr
forall a b. (a -> b) -> a -> b
$ CmdlPgipState -> String
pgipId CmdlPgipState
pgipData
      , String -> String -> Attr
mkAttr "seq" (String -> Attr) -> String -> Attr
forall a b. (a -> b) -> a -> b
$ Int -> String
forall a. Show a => a -> String
show (Int -> String) -> Int -> String
forall a b. (a -> b) -> a -> b
$ CmdlPgipState -> Int
seqNb CmdlPgipState
pgipData ])
  (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ String -> () -> Element
forall t. Node t => String -> t -> Element
unode "pgip" ()) { elContent :: [Content]
elContent = [Element -> Content
Elem Element
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 :: CmdlPgipState -> Element -> CmdlPgipState
addPGIPElement pgData :: CmdlPgipState
pgData el :: Element
el =
  CmdlPgipState
pgData { xmlElements :: [Element]
xmlElements = CmdlPgipState -> Element -> Element
addPGIPAttributes CmdlPgipState
pgData Element
el Element -> [Element] -> [Element]
forall a. a -> [a] -> [a]
: CmdlPgipState -> [Element]
xmlElements CmdlPgipState
pgData
         , seqNb :: Int
seqNb = CmdlPgipState -> Int
seqNb CmdlPgipState
pgData Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 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 :: CmdlPgipState -> CmdlPgipState
addPGIPReady pgData :: CmdlPgipState
pgData = CmdlPgipState -> Element -> CmdlPgipState
addPGIPElement CmdlPgipState
pgData (Element -> CmdlPgipState) -> Element -> CmdlPgipState
forall a b. (a -> b) -> a -> b
$ String -> () -> Element
forall t. Node t => String -> t -> Element
unode "ready" ()

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

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

-- | Generates the id of the session between Hets and the Broker
genPgipID :: IO String
genPgipID :: IO String
genPgipID =
  do
   String
t1 <- String -> String -> IO String
getEnvDef "HOSTNAME" ""
   String
t2 <- String -> String -> IO String
getEnvDef "USER" ""
   POSIXTime
t3 <- IO POSIXTime
getPOSIXTime
   String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> IO String) -> String -> IO String
forall a b. (a -> b) -> a -> b
$ String
t1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ "/" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
t2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ "/" String -> String -> String
forall a. [a] -> [a] -> [a]
++ POSIXTime -> String
forall a. Show a => a -> String
show POSIXTime
t3

-- | Concatenates the input string to the message stored in the state
addToMsg :: String -> CmdlPgipState -> CmdlPgipState
addToMsg :: String -> CmdlPgipState -> CmdlPgipState
addToMsg str :: String
str pgD :: CmdlPgipState
pgD = if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
str then CmdlPgipState
pgD else CmdlPgipState
pgD { msgs :: [String]
msgs = String
str String -> [String] -> [String]
forall a. a -> [a] -> [a]
: CmdlPgipState -> [String]
msgs CmdlPgipState
pgD }

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

{- the PGIP protocol defines the pgip element as containing a single
subelement. -}
convertPGIPDataToString :: CmdlPgipState -> String
convertPGIPDataToString :: CmdlPgipState -> String
convertPGIPDataToString =
  String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate "\n" ([String] -> String)
-> (CmdlPgipState -> [String]) -> CmdlPgipState -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> [String]
forall a. [a] -> [a]
reverse ([String] -> [String])
-> (CmdlPgipState -> [String]) -> CmdlPgipState -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Element -> String) -> [Element] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Element -> String
showElement ([Element] -> [String])
-> (CmdlPgipState -> [Element]) -> CmdlPgipState -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CmdlPgipState -> [Element]
xmlElements

isRemote :: HetcatsOpts -> Bool
isRemote :: HetcatsOpts -> Bool
isRemote opts :: HetcatsOpts
opts = HetcatsOpts -> Int
connectP HetcatsOpts
opts Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= -1 Bool -> Bool -> Bool
|| HetcatsOpts -> Int
listen HetcatsOpts
opts Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= -1

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

sendMSGData :: HetcatsOpts -> CmdlPgipState -> IO CmdlPgipState
sendMSGData :: HetcatsOpts -> CmdlPgipState -> IO CmdlPgipState
sendMSGData opts :: HetcatsOpts
opts pgData :: CmdlPgipState
pgData = do
  let msg :: String
msg = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate "\n" ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [String] -> [String]
forall a. [a] -> [a]
reverse ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ CmdlPgipState -> [String]
msgs CmdlPgipState
pgData
  if HetcatsOpts -> Bool
isRemote HetcatsOpts
opts
    then Handle -> String -> IO ()
hPutStrLn (CmdlPgipState -> Handle
hout CmdlPgipState
pgData) String
msg
    else HetcatsOpts -> Int -> String -> IO ()
putIfVerbose HetcatsOpts
opts 1 String
msg
  Handle -> IO ()
hFlush (Handle -> IO ()) -> Handle -> IO ()
forall a b. (a -> b) -> a -> b
$ CmdlPgipState -> Handle
hout CmdlPgipState
pgData
  CmdlPgipState -> IO CmdlPgipState
forall (m :: * -> *) a. Monad m => a -> m a
return CmdlPgipState
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 (CmdlXMLcommands -> CmdlXMLcommands -> Bool
(CmdlXMLcommands -> CmdlXMLcommands -> Bool)
-> (CmdlXMLcommands -> CmdlXMLcommands -> Bool)
-> Eq CmdlXMLcommands
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CmdlXMLcommands -> CmdlXMLcommands -> Bool
$c/= :: CmdlXMLcommands -> CmdlXMLcommands -> Bool
== :: CmdlXMLcommands -> CmdlXMLcommands -> Bool
$c== :: CmdlXMLcommands -> CmdlXMLcommands -> Bool
Eq, Int -> CmdlXMLcommands -> String -> String
[CmdlXMLcommands] -> String -> String
CmdlXMLcommands -> String
(Int -> CmdlXMLcommands -> String -> String)
-> (CmdlXMLcommands -> String)
-> ([CmdlXMLcommands] -> String -> String)
-> Show CmdlXMLcommands
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [CmdlXMLcommands] -> String -> String
$cshowList :: [CmdlXMLcommands] -> String -> String
show :: CmdlXMLcommands -> String
$cshow :: CmdlXMLcommands -> String
showsPrec :: Int -> CmdlXMLcommands -> String -> String
$cshowsPrec :: Int -> CmdlXMLcommands -> String -> String
Show)

-- extracts the seq attribute value to be used as reference number elsewhere
getRefseqNb :: String -> Maybe String
getRefseqNb :: String -> Maybe String
getRefseqNb input :: String
input =
  let xmlTree :: [Content]
xmlTree = String -> [Content]
forall s. XmlSource s => s -> [Content]
parseXML String
input
      elRef :: Maybe Content
elRef = (Content -> Bool) -> [Content] -> Maybe Content
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\ x :: Content
x -> case Content
x of
                              Elem dt :: Element
dt -> QName -> String
qName (Element -> QName
elName Element
dt) String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "pgip"
                              _ -> Bool
False) [Content]
xmlTree
   in case Maybe Content
elRef of
        Nothing -> Maybe String
forall a. Maybe a
Nothing
        Just el :: Content
el -> case Content
el of
                     Elem dt :: Element
dt -> case (Attr -> Bool) -> [Attr] -> Maybe Attr
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\ x :: Attr
x -> QName -> String
qName (Attr -> QName
attrKey Attr
x) String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "seq") ([Attr] -> Maybe Attr) -> [Attr] -> Maybe Attr
forall a b. (a -> b) -> a -> b
$
                                     Element -> [Attr]
elAttribs Element
dt of
                                  Nothing -> Maybe String
forall a. Maybe a
Nothing
                                  Just elatr :: Attr
elatr -> String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ Attr -> String
attrVal Attr
elatr
                     _ -> Maybe String
forall a. Maybe a
Nothing

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

parseXMLElement :: Element -> Maybe CmdlXMLcommands
parseXMLElement :: Element -> Maybe CmdlXMLcommands
parseXMLElement info :: Element
info = let cnt :: String
cnt = Element -> String
strContent Element
info in
  case QName -> String
qName (QName -> String) -> QName -> String
forall a b. (a -> b) -> a -> b
$ Element -> QName
elName Element
info of
    "proverinit" -> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a. a -> Maybe a
Just CmdlXMLcommands
XmlProverInit
    "proverexit" -> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a. a -> Maybe a
Just CmdlXMLcommands
XmlExit
    "startquiet" -> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a. a -> Maybe a
Just CmdlXMLcommands
XmlStartQuiet
    "stopquiet" -> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a. a -> Maybe a
Just CmdlXMLcommands
XmlStopQuiet
    "opengoal" -> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a. a -> Maybe a
Just (CmdlXMLcommands -> Maybe CmdlXMLcommands)
-> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a b. (a -> b) -> a -> b
$ String -> CmdlXMLcommands
XmlOpenGoal String
cnt
    "proofstep" -> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a. a -> Maybe a
Just (CmdlXMLcommands -> Maybe CmdlXMLcommands)
-> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a b. (a -> b) -> a -> b
$ String -> CmdlXMLcommands
XmlExecute String
cnt
    "closegoal" -> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a. a -> Maybe a
Just (CmdlXMLcommands -> Maybe CmdlXMLcommands)
-> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a b. (a -> b) -> a -> b
$ String -> CmdlXMLcommands
XmlCloseGoal String
cnt
    "giveupgoal" -> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a. a -> Maybe a
Just (CmdlXMLcommands -> Maybe CmdlXMLcommands)
-> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a b. (a -> b) -> a -> b
$ String -> CmdlXMLcommands
XmlGiveUpGoal String
cnt
    "spurioscmd" -> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a. a -> Maybe a
Just (CmdlXMLcommands -> Maybe CmdlXMLcommands)
-> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a b. (a -> b) -> a -> b
$ String -> CmdlXMLcommands
XmlExecute String
cnt
    "dostep" -> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a. a -> Maybe a
Just (CmdlXMLcommands -> Maybe CmdlXMLcommands)
-> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a b. (a -> b) -> a -> b
$ String -> CmdlXMLcommands
XmlExecute String
cnt
    "editobj" -> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a. a -> Maybe a
Just (CmdlXMLcommands -> Maybe CmdlXMLcommands)
-> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a b. (a -> b) -> a -> b
$ String -> CmdlXMLcommands
XmlExecute String
cnt
    "undostep" -> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a. a -> Maybe a
Just CmdlXMLcommands
XmlUndo
    "redostep" -> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a. a -> Maybe a
Just CmdlXMLcommands
XmlRedo
    "forget" -> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a. a -> Maybe a
Just (CmdlXMLcommands -> Maybe CmdlXMLcommands)
-> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a b. (a -> b) -> a -> b
$ String -> CmdlXMLcommands
XmlForget String
cnt
    "opentheory" -> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a. a -> Maybe a
Just (CmdlXMLcommands -> Maybe CmdlXMLcommands)
-> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a b. (a -> b) -> a -> b
$ String -> CmdlXMLcommands
XmlOpenTheory String
cnt
    "theoryitem" -> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a. a -> Maybe a
Just (CmdlXMLcommands -> Maybe CmdlXMLcommands)
-> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a b. (a -> b) -> a -> b
$ String -> CmdlXMLcommands
XmlExecute String
cnt
    "closetheory" -> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a. a -> Maybe a
Just (CmdlXMLcommands -> Maybe CmdlXMLcommands)
-> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a b. (a -> b) -> a -> b
$ String -> CmdlXMLcommands
XmlCloseTheory String
cnt
    "closefile" -> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a. a -> Maybe a
Just (CmdlXMLcommands -> Maybe CmdlXMLcommands)
-> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a b. (a -> b) -> a -> b
$ String -> CmdlXMLcommands
XmlCloseFile String
cnt
    "loadfile" -> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a. a -> Maybe a
Just (CmdlXMLcommands -> Maybe CmdlXMLcommands)
-> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a b. (a -> b) -> a -> b
$ String -> CmdlXMLcommands
XmlLoadFile String
cnt
    "askpgip" -> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a. a -> Maybe a
Just CmdlXMLcommands
XmlAskpgip
    "parsescript" -> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a. a -> Maybe a
Just (CmdlXMLcommands -> Maybe CmdlXMLcommands)
-> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a b. (a -> b) -> a -> b
$ String -> CmdlXMLcommands
XmlParseScript String
cnt
    "pgip" -> Maybe CmdlXMLcommands
forall a. Maybe a
Nothing
    s :: String
s -> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a. a -> Maybe a
Just (CmdlXMLcommands -> Maybe CmdlXMLcommands)
-> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a b. (a -> b) -> a -> b
$ String -> CmdlXMLcommands
XmlUnknown String
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 :: CmdlPgipState -> String -> [CmdlXMLcommands]
parseMsg st :: CmdlPgipState
st input :: String
input = if CmdlPgipState -> Bool
useXML CmdlPgipState
st
   then [Content] -> [CmdlXMLcommands] -> [CmdlXMLcommands]
parseXMLTree (String -> [Content]
forall s. XmlSource s => s -> [Content]
parseXML String
input) []
   else (String -> [CmdlXMLcommands]) -> [String] -> [CmdlXMLcommands]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ x :: String
x -> [ String -> CmdlXMLcommands
XmlExecute String
x | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (String -> Bool) -> String -> Bool
forall a b. (a -> b) -> a -> b
$ String -> String
trim String
x ]) ([String] -> [CmdlXMLcommands]) -> [String] -> [CmdlXMLcommands]
forall a b. (a -> b) -> a -> b
$ String -> [String]
lines String
input