{- |
Module      : ./PGIP/XMLparsing.hs
Description : XML processing for the CMDL interface
Copyright   : uni-bremen and DFKI
License     : GPLv2 or higher, see LICENSE.txt
Maintainer  : r.pascanu@jacobs-university.de
Stability   : provisional
Portability : portable

PGIP.XMLparsing contains commands for parsing or creating XML messages
-}

module PGIP.XMLparsing where

import PGIP.XMLstate

import CMDL.DataTypes
import CMDL.DataTypesUtils
import CMDL.DgCommands (cUse)
import CMDL.ProcessScript
import CMDL.Interface (cmdlRunShell)

import Interfaces.DataTypes
import Interfaces.Command
import Interfaces.Utils (emptyIntIState)

import Driver.Options
import Driver.ReadFn

import qualified Static.ToXml as ToXml
import Static.DevGraph

import Common.LibName
import Common.ToXml

import Text.XML.Light as XML

import Network.Socket

import System.IO

import Data.List (isInfixOf)

{- | Generates the XML packet that contains information about what
commands can the interface respond to -}
addPGIPHandshake :: CmdlPgipState -> CmdlPgipState
addPGIPHandshake :: CmdlPgipState -> CmdlPgipState
addPGIPHandshake pgipData :: CmdlPgipState
pgipData = if CmdlPgipState -> Bool
useXML CmdlPgipState
pgipData
       then CmdlPgipState -> Element -> CmdlPgipState
addPGIPElement CmdlPgipState
pgipData

            (Element -> CmdlPgipState) -> Element -> CmdlPgipState
forall a b. (a -> b) -> a -> b
$ Attr -> Element -> Element
add_attr (String -> String -> Attr
mkAttr "version" "2.0")
            (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ String -> [Element] -> Element
forall t. Node t => String -> t -> Element
unode "acceptedpgipelems" ([Element] -> Element) -> [Element] -> Element
forall a b. (a -> b) -> a -> b
$ (String -> Element) -> [String] -> [Element]
forall a b. (a -> b) -> [a] -> [b]
map String -> Element
genPgipElem
             [ "askpgip"
             , "askpgml"
             , "askprefs"
             , "getprefs"
             , "setprefs"
             , "proverinit"
             , "proverexit"
             , "startquiet"
             , "stopquiet"
             , "pgmlsymbolon"
             , "pgmlsymboloff"
             , "dostep"
             , "undostep"
             , "redostep"
             , "abortgoal"
             , "forget"
             , "restoregoal"
             , "askids"
             , "showid"
             , "askguise"
             , "parsescript"
             , "showproofstate"
             , "showctxt"
             , "searchtheorems"
             , "setlinewidth"
             , "viewdoc"
             , "doitem"
             , "undoitem"
             , "redoitem"
             , "aborttheory"
             , "retracttheory"
             , "loadfile"
             , "openfile"
             , "closefile"
             , "abortfile"
             , "changecwd"
             , "systemcmd"]
       else CmdlPgipState
pgipData

{- | The function executes a communication step, i.e. waits for input,
processes the message and outputs the answer -}
communicationStep :: CmdlPgipState -> CmdlState -> IO (CmdlPgipState, CmdlState)
communicationStep :: CmdlPgipState -> CmdlState -> IO (CmdlPgipState, CmdlState)
communicationStep pgD :: CmdlPgipState
pgD st :: CmdlState
st = do
   -- tries to read a packet from the input
  Bool
b <- Handle -> IO Bool
hIsEOF (CmdlPgipState -> Handle
hin CmdlPgipState
pgD)
  if Bool
b then (CmdlPgipState, CmdlState) -> IO (CmdlPgipState, CmdlState)
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlPgipState
pgD { stop :: Bool
stop = Bool
True }, CmdlState
st) else do
   Maybe String
tmp <- Int -> CmdlPgipState -> IO (Maybe String)
timeoutReadPacket (CmdlPgipState -> Int
maxWaitTime CmdlPgipState
pgD) CmdlPgipState
pgD
   case Maybe String
tmp of
    Nothing -> if CmdlPgipState -> Bool
resendMsgIfTimeout CmdlPgipState
pgD
      {- if the interface receives nothing in the given timeframe
      described by maxWaitTime and the flag resendMsgIfTimeout is
      set, that the interface resends last packet assuming that last
      send was a fail -}
                then do
                       CmdlPgipState
nwpgD <- HetcatsOpts -> CmdlPgipState -> IO CmdlPgipState
sendPGIPData (CmdlState -> HetcatsOpts
hetsOpts CmdlState
st) CmdlPgipState
pgD
                       CmdlPgipState -> CmdlState -> IO (CmdlPgipState, CmdlState)
communicationStep CmdlPgipState
nwpgD CmdlState
st
       {- if the flag is not set, that the network waits some more for the
       broker to respond or give a new command -}
                else CmdlPgipState -> CmdlState -> IO (CmdlPgipState, CmdlState)
communicationStep CmdlPgipState
pgD CmdlState
st
    {- if something is received, that the commands are parsed and executed
    and a response is generated -}
    Just smtxt :: String
smtxt ->
      do
        let cmds :: [CmdlXMLcommands]
cmds = CmdlPgipState -> String -> [CmdlXMLcommands]
parseMsg CmdlPgipState
pgD String
smtxt
            refseqNb :: Maybe String
refseqNb = String -> Maybe String
getRefseqNb String
smtxt
        (nwSt :: CmdlState
nwSt, nwPgD :: CmdlPgipState
nwPgD) <- [CmdlXMLcommands]
-> CmdlState -> CmdlPgipState -> IO (CmdlState, CmdlPgipState)
processCmds [CmdlXMLcommands]
cmds CmdlState
st (CmdlPgipState -> IO (CmdlState, CmdlPgipState))
-> CmdlPgipState -> IO (CmdlState, CmdlPgipState)
forall a b. (a -> b) -> a -> b
$ CmdlPgipState -> CmdlPgipState
resetPGIPData (CmdlPgipState -> CmdlPgipState) -> CmdlPgipState -> CmdlPgipState
forall a b. (a -> b) -> a -> b
$
                           CmdlPgipState
pgD { refSeqNb :: Maybe String
refSeqNb = Maybe String
refseqNb }
        if CmdlPgipState -> Bool
useXML CmdlPgipState
pgD then do
                 CmdlPgipState
nwPgipSt <- HetcatsOpts -> CmdlPgipState -> IO CmdlPgipState
sendPGIPData (CmdlState -> HetcatsOpts
hetsOpts CmdlState
nwSt) CmdlPgipState
nwPgD
                 (CmdlPgipState, CmdlState) -> IO (CmdlPgipState, CmdlState)
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlPgipState
nwPgipSt, CmdlState
nwSt)
          else do
                 CmdlPgipState
nwPgD' <- HetcatsOpts -> CmdlPgipState -> IO CmdlPgipState
sendMSGData (CmdlState -> HetcatsOpts
hetsOpts CmdlState
nwSt) CmdlPgipState
nwPgD
                 (CmdlPgipState, CmdlState) -> IO (CmdlPgipState, CmdlState)
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlPgipState
nwPgD', CmdlState
nwSt)

-- | Comunicate over a port
cmdlListenOrConnect2Port :: HetcatsOpts -> CmdlState -> IO CmdlState
cmdlListenOrConnect2Port :: HetcatsOpts -> CmdlState -> IO CmdlState
cmdlListenOrConnect2Port opts :: HetcatsOpts
opts state :: CmdlState
state = do
    let portNb :: Int
portNb = HetcatsOpts -> Int
Driver.Options.listen HetcatsOpts
opts
        conPN :: Int
conPN = HetcatsOpts -> Int
connectP HetcatsOpts
opts
        hostName :: String
hostName = HetcatsOpts -> String
connectH HetcatsOpts
opts
        swXML :: Bool
swXML = HetcatsOpts -> Bool
xmlFlag HetcatsOpts
opts
        hints :: AddrInfo
hints = AddrInfo
defaultHints { addrSocketType :: SocketType
addrSocketType = SocketType
Stream }

    Handle
servH <- if Int
portNb Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= -1 then do
        HetcatsOpts -> Int -> String -> IO ()
putIfVerbose HetcatsOpts
opts 1 (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "Starting hets. Listen to port " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
portNb
        AddrInfo
addrInfo <- [AddrInfo] -> AddrInfo
forall a. [a] -> a
head ([AddrInfo] -> AddrInfo) -> IO [AddrInfo] -> IO AddrInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe AddrInfo -> Maybe String -> Maybe String -> IO [AddrInfo]
getAddrInfo (AddrInfo -> Maybe AddrInfo
forall a. a -> Maybe a
Just AddrInfo
hints) Maybe String
forall a. Maybe a
Nothing (String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ Int -> String
forall a. Show a => a -> String
show Int
portNb)
        Socket
servSock <- Family -> SocketType -> ProtocolNumber -> IO Socket
socket (AddrInfo -> Family
addrFamily AddrInfo
addrInfo) (AddrInfo -> SocketType
addrSocketType AddrInfo
addrInfo) (AddrInfo -> ProtocolNumber
addrProtocol AddrInfo
addrInfo)
        Socket -> SockAddr -> IO ()
bind Socket
servSock (SockAddr -> IO ()) -> SockAddr -> IO ()
forall a b. (a -> b) -> a -> b
$ AddrInfo -> SockAddr
addrAddress AddrInfo
addrInfo
        Socket -> Int -> IO ()
Network.Socket.listen Socket
servSock 1024
        (acceptedServSock :: Socket
acceptedServSock, _) <- Socket -> IO (Socket, SockAddr)
accept Socket
servSock
        Socket -> IOMode -> IO Handle
socketToHandle Socket
acceptedServSock IOMode
ReadWriteMode
      else if Int
conPN Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= -1 then do
        HetcatsOpts -> Int -> String -> IO ()
putIfVerbose HetcatsOpts
opts 1 (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "Starting hets. Connecting to port "
          String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
conPN String -> String -> String
forall a. [a] -> [a] -> [a]
++ " on host " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
hostName
        AddrInfo
addrInfo <- [AddrInfo] -> AddrInfo
forall a. [a] -> a
head ([AddrInfo] -> AddrInfo) -> IO [AddrInfo] -> IO AddrInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe AddrInfo -> Maybe String -> Maybe String -> IO [AddrInfo]
getAddrInfo (AddrInfo -> Maybe AddrInfo
forall a. a -> Maybe a
Just AddrInfo
hints) (String -> Maybe String
forall a. a -> Maybe a
Just String
hostName) (String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ Int -> String
forall a. Show a => a -> String
show Int
conPN)
        Socket
sock <- Family -> SocketType -> ProtocolNumber -> IO Socket
socket (AddrInfo -> Family
addrFamily AddrInfo
addrInfo) (AddrInfo -> SocketType
addrSocketType AddrInfo
addrInfo) (AddrInfo -> ProtocolNumber
addrProtocol AddrInfo
addrInfo)
        Socket -> SockAddr -> IO ()
connect Socket
sock (SockAddr -> IO ()) -> SockAddr -> IO ()
forall a b. (a -> b) -> a -> b
$ AddrInfo -> SockAddr
addrAddress AddrInfo
addrInfo
        Socket -> IOMode -> IO Handle
socketToHandle Socket
sock IOMode
ReadWriteMode
      else String -> IO Handle
forall a. HasCallStack => String -> a
error "cmlListenOrConnect2Port: missing port number"
    Bool -> Handle -> Handle -> Int -> CmdlState -> IO CmdlState
cmdlStartLoop Bool
swXML Handle
servH Handle
servH 1000 CmdlState
state

{- | Reads from a handle, it waits only for a certain amount of time,
if no input comes it will return Nothing -}
timeoutReadPacket :: Int -> CmdlPgipState -> IO (Maybe String)
timeoutReadPacket :: Int -> CmdlPgipState -> IO (Maybe String)
timeoutReadPacket untilTimeout :: Int
untilTimeout st :: CmdlPgipState
st = do
    let h :: Handle
h = CmdlPgipState -> Handle
hin CmdlPgipState
st
    Bool
smtmp <- Handle -> Int -> IO Bool
hWaitForInput Handle
h Int
untilTimeout
    if Bool
smtmp then do
            String
ms <- if CmdlPgipState -> Bool
useXML CmdlPgipState
st
                    then String -> Handle -> IO String
readPacket [] Handle
h
                    else Handle -> IO String
hGetLine Handle
h
            Maybe String -> IO (Maybe String)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe String -> IO (Maybe String))
-> Maybe String -> IO (Maybe String)
forall a b. (a -> b) -> a -> b
$ String -> Maybe String
forall a. a -> Maybe a
Just String
ms
      else Maybe String -> IO (Maybe String)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe String
forall a. Maybe a
Nothing

-- | Waits until it reads an entire XML packet
readPacket :: String -> Handle -> IO String
readPacket :: String -> Handle -> IO String
readPacket acc :: String
acc hf :: Handle
hf = do
    String
tmp <- Handle -> IO String
hGetLine Handle
hf
    let str :: String
str = String
acc String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
tmp String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n"
    if String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isInfixOf "</pgip>" String
tmp
      then String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return String
str
      else String -> Handle -> IO String
readPacket String
str Handle
hf

cmdlStartLoop :: Bool -> Handle -> Handle -> Int -> CmdlState
              -> IO CmdlState
cmdlStartLoop :: Bool -> Handle -> Handle -> Int -> CmdlState -> IO CmdlState
cmdlStartLoop swXML :: Bool
swXML h_in :: Handle
h_in h_out :: Handle
h_out timeOut :: Int
timeOut state :: CmdlState
state = do
    CmdlPgipState
pgData <- Bool -> Handle -> Handle -> Int -> IO CmdlPgipState
genCMDLPgipState Bool
swXML Handle
h_in Handle
h_out Int
timeOut
    let pgD :: CmdlPgipState
pgD = CmdlPgipState -> CmdlPgipState
addPGIPReady (CmdlPgipState -> CmdlPgipState) -> CmdlPgipState -> CmdlPgipState
forall a b. (a -> b) -> a -> b
$ CmdlPgipState -> CmdlPgipState
addPGIPHandshake (CmdlPgipState -> CmdlPgipState) -> CmdlPgipState -> CmdlPgipState
forall a b. (a -> b) -> a -> b
$ CmdlPgipState -> CmdlPgipState
resetPGIPData CmdlPgipState
pgData
    CmdlPgipState
pgD' <- HetcatsOpts -> CmdlPgipState -> IO CmdlPgipState
sendPGIPData (CmdlState -> HetcatsOpts
hetsOpts CmdlState
state) CmdlPgipState
pgD
    CmdlPgipState -> CmdlState -> IO CmdlState
waitLoop CmdlPgipState
pgD' CmdlState
state

waitLoop :: CmdlPgipState -> CmdlState -> IO CmdlState
waitLoop :: CmdlPgipState -> CmdlState -> IO CmdlState
waitLoop pgData :: CmdlPgipState
pgData state :: CmdlState
state = do
  (pgData' :: CmdlPgipState
pgData', state' :: CmdlState
state') <- CmdlPgipState -> CmdlState -> IO (CmdlPgipState, CmdlState)
communicationStep CmdlPgipState
pgData CmdlState
state
  if CmdlPgipState -> Bool
stop CmdlPgipState
pgData'
    then CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return CmdlState
state'
    else CmdlPgipState -> CmdlState -> IO CmdlState
waitLoop CmdlPgipState
pgData' CmdlState
state'

{- | Runs a shell in which the communication is expected to be
through XML packets -}
cmdlRunXMLShell :: CmdlState -> IO CmdlState
cmdlRunXMLShell :: CmdlState -> IO CmdlState
cmdlRunXMLShell = Bool -> Handle -> Handle -> Int -> CmdlState -> IO CmdlState
cmdlStartLoop Bool
True Handle
stdin Handle
stdout (-1)

-- | Processes a list of input files
processInput :: HetcatsOpts -> [FilePath] -> CmdlState -> IO CmdlState
processInput :: HetcatsOpts -> [String] -> CmdlState -> IO CmdlState
processInput opts :: HetcatsOpts
opts ls :: [String]
ls state :: CmdlState
state = case [String]
ls of
    [] -> CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return CmdlState
state
    l :: String
l : ll :: [String]
ll -> (case String -> InType -> InType
guess String
l InType
GuessIn of
               ProofCommand -> Bool -> String -> CmdlState -> IO CmdlState
cmdlProcessScriptFile Bool
True
               _ -> String -> CmdlState -> IO CmdlState
cUse) String
l CmdlState
state IO CmdlState -> (CmdlState -> IO CmdlState) -> IO CmdlState
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= HetcatsOpts -> [String] -> CmdlState -> IO CmdlState
processInput HetcatsOpts
opts [String]
ll

cmdlRun :: HetcatsOpts -> IO CmdlState
cmdlRun :: HetcatsOpts -> IO CmdlState
cmdlRun opts :: HetcatsOpts
opts =
  HetcatsOpts -> [String] -> CmdlState -> IO CmdlState
processInput HetcatsOpts
opts (HetcatsOpts -> [String]
infiles HetcatsOpts
opts) (HetcatsOpts -> CmdlState
emptyCmdlState HetcatsOpts
opts) IO CmdlState -> (CmdlState -> IO CmdlState) -> IO CmdlState
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
  if HetcatsOpts -> Bool
isRemote HetcatsOpts
opts
    then HetcatsOpts -> CmdlState -> IO CmdlState
cmdlListenOrConnect2Port HetcatsOpts
opts
    else if HetcatsOpts -> Bool
interactive HetcatsOpts
opts
           then if HetcatsOpts -> Bool
xmlFlag HetcatsOpts
opts
                  then CmdlState -> IO CmdlState
cmdlRunXMLShell
                  else CmdlState -> IO CmdlState
cmdlRunShell
           else CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return

processString :: [CmdlXMLcommands] -> String -> CmdlState -> CmdlPgipState
  -> IO (CmdlState, CmdlPgipState)
processString :: [CmdlXMLcommands]
-> String
-> CmdlState
-> CmdlPgipState
-> IO (CmdlState, CmdlPgipState)
processString pl :: [CmdlXMLcommands]
pl str :: String
str st :: CmdlState
st pgSt :: CmdlPgipState
pgSt = do
  (nwSt :: CmdlState
nwSt, mCmd :: Maybe Command
mCmd) <- String
-> Int -> String -> CmdlState -> IO (CmdlState, Maybe Command)
cmdlProcessString "" 0 String
str CmdlState
st
  [CmdlXMLcommands]
-> CmdlState
-> CmdlPgipState
-> Maybe Command
-> IO (CmdlState, CmdlPgipState)
postProcessCmd [CmdlXMLcommands]
pl CmdlState
nwSt CmdlPgipState
pgSt Maybe Command
mCmd

-- copy messages to pgip state
processMsgs :: CmdlState -> CmdlPgipState -> (CmdlPgipState, String)
processMsgs :: CmdlState -> CmdlPgipState -> (CmdlPgipState, String)
processMsgs nwSt :: CmdlState
nwSt pgSt :: CmdlPgipState
pgSt =
  let o :: CmdlMessage
o = CmdlState -> CmdlMessage
output CmdlState
nwSt
      ms :: String
ms = CmdlMessage -> String
outputMsg CmdlMessage
o
      ws :: String
ws = CmdlMessage -> String
warningMsg CmdlMessage
o
      es :: String
es = CmdlMessage -> String
errorMsg CmdlMessage
o
      -- there should be at most one
  in (if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
es then String -> String -> CmdlPgipState -> CmdlPgipState
addPGIPAnswer String
ms String
ws CmdlPgipState
pgSt else String -> CmdlPgipState -> CmdlPgipState
addPGIPError String
es CmdlPgipState
pgSt, String
es)

processCommand :: [CmdlXMLcommands] -> Command -> CmdlState -> CmdlPgipState
  -> IO (CmdlState, CmdlPgipState)
processCommand :: [CmdlXMLcommands]
-> Command
-> CmdlState
-> CmdlPgipState
-> IO (CmdlState, CmdlPgipState)
processCommand pl :: [CmdlXMLcommands]
pl cmd :: Command
cmd st :: CmdlState
st pgSt :: CmdlPgipState
pgSt = do
  CmdlState
nwSt <- Command -> CmdlState -> IO CmdlState
cmdlProcessCmd Command
cmd CmdlState
st
  [CmdlXMLcommands]
-> CmdlState
-> CmdlPgipState
-> Maybe Command
-> IO (CmdlState, CmdlPgipState)
postProcessCmd [CmdlXMLcommands]
pl CmdlState
nwSt CmdlPgipState
pgSt (Command -> Maybe Command
forall a. a -> Maybe a
Just Command
cmd)

-- postprocess a previously run command and recurse
postProcessCmd :: [CmdlXMLcommands] -> CmdlState -> CmdlPgipState
  -> Maybe Command -> IO (CmdlState, CmdlPgipState)
postProcessCmd :: [CmdlXMLcommands]
-> CmdlState
-> CmdlPgipState
-> Maybe Command
-> IO (CmdlState, CmdlPgipState)
postProcessCmd pl :: [CmdlXMLcommands]
pl nwSt0 :: CmdlState
nwSt0 pgSt :: CmdlPgipState
pgSt mCmd :: Maybe Command
mCmd = let
  (pgSt1 :: CmdlPgipState
pgSt1, es :: String
es) = CmdlState -> CmdlPgipState -> (CmdlPgipState, String)
processMsgs CmdlState
nwSt0 CmdlPgipState
pgSt
  nwSt :: CmdlState
nwSt = CmdlState
nwSt0 { output :: CmdlMessage
output = CmdlMessage
emptyCmdlMessage } -- remove messages form cmdl state
  in if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
es then [CmdlXMLcommands]
-> CmdlState -> CmdlPgipState -> IO (CmdlState, CmdlPgipState)
processCmds [CmdlXMLcommands]
pl CmdlState
nwSt (CmdlPgipState -> IO (CmdlState, CmdlPgipState))
-> CmdlPgipState -> IO (CmdlState, CmdlPgipState)
forall a b. (a -> b) -> a -> b
$ CmdlState -> Maybe Command -> CmdlPgipState -> CmdlPgipState
informCmd CmdlState
nwSt Maybe Command
mCmd CmdlPgipState
pgSt1 else
  (CmdlState, CmdlPgipState) -> IO (CmdlState, CmdlPgipState)
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlState
nwSt, CmdlPgipState -> CmdlPgipState
addPGIPReady CmdlPgipState
pgSt1)

informCmd :: CmdlState -> Maybe Command -> CmdlPgipState -> CmdlPgipState
informCmd :: CmdlState -> Maybe Command -> CmdlPgipState -> CmdlPgipState
informCmd nwSt :: CmdlState
nwSt mCmd :: Maybe Command
mCmd pgSt1 :: CmdlPgipState
pgSt1 = let opts :: HetcatsOpts
opts = CmdlState -> HetcatsOpts
hetsOpts CmdlState
nwSt in
  case (IntState -> Maybe (LibName, LibEnv)
getMaybeLib (IntState -> Maybe (LibName, LibEnv))
-> IntState -> Maybe (LibName, LibEnv)
forall a b. (a -> b) -> a -> b
$ CmdlState -> IntState
intState CmdlState
nwSt, Maybe Command
mCmd) of
          (Just (lN :: LibName
lN, lEnv :: LibEnv
lEnv), Just cmd :: Command
cmd) -> case Command
cmd of
            SelectCmd LibFile _ ->
              HetcatsOpts -> LibName -> LibEnv -> CmdlPgipState -> CmdlPgipState
informDGraph HetcatsOpts
opts LibName
lN LibEnv
lEnv (CmdlPgipState -> CmdlPgipState) -> CmdlPgipState -> CmdlPgipState
forall a b. (a -> b) -> a -> b
$ CmdlPgipState -> Element -> CmdlPgipState
addPGIPElement CmdlPgipState
pgSt1
                (Element -> CmdlPgipState) -> Element -> CmdlPgipState
forall a b. (a -> b) -> a -> b
$ Attr -> Element -> Element
add_attr (String -> String -> Attr
mkAttr "url" (String -> Attr) -> String -> Attr
forall a b. (a -> b) -> a -> b
$ LibName -> String
libNameToFile LibName
lN)
                (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ String -> () -> Element
forall t. Node t => String -> t -> Element
unode "informfileloaded" ()
            GlobCmd g :: GlobCmd
g | GlobCmd
g GlobCmd -> GlobCmd -> Bool
forall a. Ord a => a -> a -> Bool
< GlobCmd
ProveCurrent ->
              HetcatsOpts -> LibName -> LibEnv -> CmdlPgipState -> CmdlPgipState
informDGraph HetcatsOpts
opts LibName
lN LibEnv
lEnv CmdlPgipState
pgSt1
            _ -> CmdlPgipState
pgSt1
          _ -> CmdlPgipState
pgSt1

informDGraph :: HetcatsOpts -> LibName -> LibEnv -> CmdlPgipState
  -> CmdlPgipState
informDGraph :: HetcatsOpts -> LibName -> LibEnv -> CmdlPgipState -> CmdlPgipState
informDGraph opts :: HetcatsOpts
opts lN :: LibName
lN lEnv :: LibEnv
lEnv pgSt :: CmdlPgipState
pgSt =
  CmdlPgipState -> Element -> CmdlPgipState
addPGIPElement CmdlPgipState
pgSt (Element -> CmdlPgipState) -> Element -> CmdlPgipState
forall a b. (a -> b) -> a -> b
$ String -> Element -> Element
forall t. Node t => String -> t -> Element
unode "informdevelopmentgraph"
    (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ HetcatsOpts -> LibEnv -> LibName -> DGraph -> Element
ToXml.dGraph HetcatsOpts
opts LibEnv
lEnv LibName
lN
    (DGraph -> Element) -> DGraph -> Element
forall a b. (a -> b) -> a -> b
$ LibName -> LibEnv -> DGraph
lookupDGraph LibName
lN LibEnv
lEnv

-- | Executes given commands and returns output message and the new state
processCmds :: [CmdlXMLcommands] -> CmdlState -> CmdlPgipState
  -> IO (CmdlState, CmdlPgipState)
processCmds :: [CmdlXMLcommands]
-> CmdlState -> CmdlPgipState -> IO (CmdlState, CmdlPgipState)
processCmds cmds :: [CmdlXMLcommands]
cmds state :: CmdlState
state pgipSt :: CmdlPgipState
pgipSt = do
    let opts :: HetcatsOpts
opts = CmdlState -> HetcatsOpts
hetsOpts CmdlState
state
    case [CmdlXMLcommands]
cmds of
     [] -> (CmdlState, CmdlPgipState) -> IO (CmdlState, CmdlPgipState)
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlState
state, CmdlPgipState -> CmdlPgipState
addPGIPReady CmdlPgipState
pgipSt)
            {- ensures that the response is ended with a ready element
            such that the broker does wait for more input -}
     XmlExecute str :: String
str : l :: [CmdlXMLcommands]
l -> [CmdlXMLcommands]
-> String
-> CmdlState
-> CmdlPgipState
-> IO (CmdlState, CmdlPgipState)
processString [CmdlXMLcommands]
l String
str CmdlState
state (CmdlPgipState -> CmdlPgipState
resetPGIPData CmdlPgipState
pgipSt)
     XmlExit : l :: [CmdlXMLcommands]
l -> [CmdlXMLcommands]
-> CmdlState -> CmdlPgipState -> IO (CmdlState, CmdlPgipState)
processCmds [CmdlXMLcommands]
l CmdlState
state (CmdlPgipState -> IO (CmdlState, CmdlPgipState))
-> CmdlPgipState -> IO (CmdlState, CmdlPgipState)
forall a b. (a -> b) -> a -> b
$
         String -> String -> CmdlPgipState -> CmdlPgipState
addPGIPAnswer "Exiting prover" [] CmdlPgipState
pgipSt { stop :: Bool
stop = Bool
True }
     XmlAskpgip : l :: [CmdlXMLcommands]
l -> [CmdlXMLcommands]
-> CmdlState -> CmdlPgipState -> IO (CmdlState, CmdlPgipState)
processCmds [CmdlXMLcommands]
l CmdlState
state (CmdlPgipState -> IO (CmdlState, CmdlPgipState))
-> CmdlPgipState -> IO (CmdlState, CmdlPgipState)
forall a b. (a -> b) -> a -> b
$ CmdlPgipState -> CmdlPgipState
addPGIPHandshake CmdlPgipState
pgipSt
     XmlProverInit : l :: [CmdlXMLcommands]
l -> [CmdlXMLcommands]
-> CmdlState -> CmdlPgipState -> IO (CmdlState, CmdlPgipState)
processCmds [CmdlXMLcommands]
l (HetcatsOpts -> CmdlState
emptyCmdlState HetcatsOpts
opts) (CmdlPgipState -> IO (CmdlState, CmdlPgipState))
-> CmdlPgipState -> IO (CmdlState, CmdlPgipState)
forall a b. (a -> b) -> a -> b
$
         String -> String -> CmdlPgipState -> CmdlPgipState
addPGIPAnswer "Prover state was reset" [] CmdlPgipState
pgipSt
     XmlStartQuiet : l :: [CmdlXMLcommands]
l -> do
         {- To inform that quiet mode is enabled we need to send this with the
         old options. -}
         let pgD :: CmdlPgipState
pgD = CmdlPgipState -> CmdlPgipState
addPGIPReady (CmdlPgipState -> CmdlPgipState) -> CmdlPgipState -> CmdlPgipState
forall a b. (a -> b) -> a -> b
$ String -> String -> CmdlPgipState -> CmdlPgipState
addPGIPAnswer "Quiet mode enabled" [] CmdlPgipState
pgipSt
         CmdlPgipState
pgipSt' <- if CmdlPgipState -> Bool
useXML CmdlPgipState
pgD
                      then HetcatsOpts -> CmdlPgipState -> IO CmdlPgipState
sendPGIPData HetcatsOpts
opts CmdlPgipState
pgD
                      else HetcatsOpts -> CmdlPgipState -> IO CmdlPgipState
sendMSGData HetcatsOpts
opts CmdlPgipState
pgD
         [CmdlXMLcommands]
-> CmdlState -> CmdlPgipState -> IO (CmdlState, CmdlPgipState)
processCmds [CmdlXMLcommands]
l (CmdlState
state { hetsOpts :: HetcatsOpts
hetsOpts = HetcatsOpts
opts { verbose :: Int
verbose = 0 } }) CmdlPgipState
pgipSt'
     XmlStopQuiet : l :: [CmdlXMLcommands]
l ->
                  [CmdlXMLcommands]
-> CmdlState -> CmdlPgipState -> IO (CmdlState, CmdlPgipState)
processCmds [CmdlXMLcommands]
l (CmdlState
state { hetsOpts :: HetcatsOpts
hetsOpts = HetcatsOpts
opts { verbose :: Int
verbose = 1 } }) (CmdlPgipState -> IO (CmdlState, CmdlPgipState))
-> CmdlPgipState -> IO (CmdlState, CmdlPgipState)
forall a b. (a -> b) -> a -> b
$
                    String -> String -> CmdlPgipState -> CmdlPgipState
addPGIPAnswer "Quiet mode disabled" [] CmdlPgipState
pgipSt
     XmlOpenGoal str :: String
str : l :: [CmdlXMLcommands]
l -> [CmdlXMLcommands]
-> Command
-> CmdlState
-> CmdlPgipState
-> IO (CmdlState, CmdlPgipState)
processCommand [CmdlXMLcommands]
l (SelectCmd -> String -> Command
SelectCmd SelectCmd
Goal String
str) CmdlState
state CmdlPgipState
pgipSt
     XmlCloseGoal str :: String
str : l :: [CmdlXMLcommands]
l -> [CmdlXMLcommands]
-> Command
-> CmdlState
-> CmdlPgipState
-> IO (CmdlState, CmdlPgipState)
processCommand (String -> CmdlXMLcommands
XmlGiveUpGoal String
str CmdlXMLcommands -> [CmdlXMLcommands] -> [CmdlXMLcommands]
forall a. a -> [a] -> [a]
: [CmdlXMLcommands]
l)
         (GlobCmd -> Command
GlobCmd GlobCmd
ProveCurrent) CmdlState
state CmdlPgipState
pgipSt
     XmlGiveUpGoal str :: String
str : l :: [CmdlXMLcommands]
l -> [CmdlXMLcommands]
-> String
-> CmdlState
-> CmdlPgipState
-> IO (CmdlState, CmdlPgipState)
processString [CmdlXMLcommands]
l ("del goals " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
str) CmdlState
state CmdlPgipState
pgipSt
     XmlUnknown str :: String
str : l :: [CmdlXMLcommands]
l -> [CmdlXMLcommands]
-> CmdlState -> CmdlPgipState -> IO (CmdlState, CmdlPgipState)
processCmds [CmdlXMLcommands]
l CmdlState
state (CmdlPgipState -> IO (CmdlState, CmdlPgipState))
-> CmdlPgipState -> IO (CmdlState, CmdlPgipState)
forall a b. (a -> b) -> a -> b
$
           String -> String -> CmdlPgipState -> CmdlPgipState
addPGIPAnswer [] ("Unknown command: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
str) CmdlPgipState
pgipSt
     XmlUndo : l :: [CmdlXMLcommands]
l -> [CmdlXMLcommands]
-> Command
-> CmdlState
-> CmdlPgipState
-> IO (CmdlState, CmdlPgipState)
processCommand [CmdlXMLcommands]
l (GlobCmd -> Command
GlobCmd GlobCmd
UndoCmd) CmdlState
state CmdlPgipState
pgipSt
     XmlRedo : l :: [CmdlXMLcommands]
l -> [CmdlXMLcommands]
-> Command
-> CmdlState
-> CmdlPgipState
-> IO (CmdlState, CmdlPgipState)
processCommand [CmdlXMLcommands]
l (GlobCmd -> Command
GlobCmd GlobCmd
RedoCmd) CmdlState
state CmdlPgipState
pgipSt
     XmlForget str :: String
str : l :: [CmdlXMLcommands]
l -> [CmdlXMLcommands]
-> String
-> CmdlState
-> CmdlPgipState
-> IO (CmdlState, CmdlPgipState)
processString [CmdlXMLcommands]
l ("del axioms " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
str) CmdlState
state CmdlPgipState
pgipSt
     XmlOpenTheory str :: String
str : l :: [CmdlXMLcommands]
l -> [CmdlXMLcommands]
-> String
-> CmdlState
-> CmdlPgipState
-> IO (CmdlState, CmdlPgipState)
processString [CmdlXMLcommands]
l String
str CmdlState
state CmdlPgipState
pgipSt
     XmlCloseTheory _ : l :: [CmdlXMLcommands]
l -> let
         nwSt :: CmdlState
nwSt = case IntState -> Maybe IntIState
i_state (IntState -> Maybe IntIState) -> IntState -> Maybe IntIState
forall a b. (a -> b) -> a -> b
$ CmdlState -> IntState
intState CmdlState
state of
           Nothing -> CmdlState
state
           Just ist :: IntIState
ist -> [UndoRedoElem] -> CmdlState -> CmdlState
add2hist [Maybe IntIState -> UndoRedoElem
IStateChange (Maybe IntIState -> UndoRedoElem)
-> Maybe IntIState -> UndoRedoElem
forall a b. (a -> b) -> a -> b
$ IntIState -> Maybe IntIState
forall a. a -> Maybe a
Just IntIState
ist] (CmdlState -> CmdlState) -> CmdlState -> CmdlState
forall a b. (a -> b) -> a -> b
$ CmdlState
state
             { intState :: IntState
intState = (CmdlState -> IntState
intState CmdlState
state)
                 { i_state :: Maybe IntIState
i_state = IntIState -> Maybe IntIState
forall a. a -> Maybe a
Just (IntIState -> Maybe IntIState) -> IntIState -> Maybe IntIState
forall a b. (a -> b) -> a -> b
$ LibEnv -> LibName -> IntIState
emptyIntIState (IntIState -> LibEnv
i_libEnv IntIState
ist)
                     (LibName -> IntIState) -> LibName -> IntIState
forall a b. (a -> b) -> a -> b
$ IntIState -> LibName
i_ln IntIState
ist }}
         in [CmdlXMLcommands]
-> CmdlState -> CmdlPgipState -> IO (CmdlState, CmdlPgipState)
processCmds [CmdlXMLcommands]
l CmdlState
nwSt (CmdlPgipState -> IO (CmdlState, CmdlPgipState))
-> CmdlPgipState -> IO (CmdlState, CmdlPgipState)
forall a b. (a -> b) -> a -> b
$ String -> String -> CmdlPgipState -> CmdlPgipState
addPGIPAnswer "Theory closed" [] CmdlPgipState
pgipSt
     XmlCloseFile _ : l :: [CmdlXMLcommands]
l -> [CmdlXMLcommands]
-> CmdlState -> CmdlPgipState -> IO (CmdlState, CmdlPgipState)
processCmds [CmdlXMLcommands]
l (HetcatsOpts -> CmdlState
emptyCmdlState HetcatsOpts
opts)
                   (String -> String -> CmdlPgipState -> CmdlPgipState
addPGIPAnswer "File closed" [] CmdlPgipState
pgipSt)
     XmlParseScript str :: String
str : _ ->
         [CmdlXMLcommands]
-> CmdlState -> CmdlPgipState -> IO (CmdlState, CmdlPgipState)
processCmds [] CmdlState
state (CmdlPgipState -> IO (CmdlState, CmdlPgipState))
-> (Element -> CmdlPgipState)
-> Element
-> IO (CmdlState, CmdlPgipState)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CmdlPgipState -> Element -> CmdlPgipState
addPGIPElement CmdlPgipState
pgipSt (Element -> IO (CmdlState, CmdlPgipState))
-> Element -> IO (CmdlState, CmdlPgipState)
forall a b. (a -> b) -> a -> b
$ String -> Element
addPGIPMarkup String
str
     XmlLoadFile str :: String
str : l :: [CmdlXMLcommands]
l ->
         [CmdlXMLcommands]
-> Command
-> CmdlState
-> CmdlPgipState
-> IO (CmdlState, CmdlPgipState)
processCommand [CmdlXMLcommands]
l (SelectCmd -> String -> Command
SelectCmd SelectCmd
LibFile String
str) CmdlState
state CmdlPgipState
pgipSt

{- deleting axioms or goals should be implemented via a select command after
inspecting the current axioms or goals. The current strings do not work. -}