DataTypes.hs revision d2a433726b930294ebf92b7d432853424b9590a9
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'ReillyModule : $Header$
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerDescription : Internal data types of the CMDL interface
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'ReillyCopyright : uni-bremen and DFKI
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'ReillyLicense : GPLv2 or higher, see LICENSE.txt
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuMaintainer : r.pascanu@jacobs-university.de
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'ReillyStability : provisional
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'ReillyPortability : portable
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'ReillyCMDL.DataTypes describes the internal states(or datatypes) of the CMDL
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ( CmdlState (..)
57221209d11b05aa0373cc3892d5df89ba96ebf9Christian Maeder , emptyCmdlState
66bc8d6e69cde43f1ccbeb76104cf7b8038acd6cChristian Maeder , CmdlCmdDescription (..)
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder , CmdlCmdPriority (..)
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly , CmdlCmdFnClasses (..)
56899f6457976a2ee20f6a23f088cb5655b15715Liam O'Reilly , NodeOrEdgeFilter (..)
66bc8d6e69cde43f1ccbeb76104cf7b8038acd6cChristian Maeder , CmdlCmdRequirements (..)
a00461fcf7432205a79a0f12dbe6c1ebc58bc000Christian Maeder , formatRequirement
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly , CmdlChannel (..)
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly , CmdlChannelType (..)
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reilly , CmdlChannelProperties (..)
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly , CmdlSocket (..)
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reilly , CmdlUseTranslation (..)
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder , CmdlProverConsChecker (..)
f21c7417bdd1c0282025cba0f5cb0ff5bc5c98eeLiam O'Reilly , CmdlPrompterState (..)
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder , CmdlMessage (..)
50c62c8c45643f09bcb2f4a99b07bf1d072ecf40Christian Maeder , emptyCmdlMessage
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly , CmdlListAction (..)
c0833539c8cf577dd3f2497792fbdd818442744cChristian Maeder , CmdlGoalAxiom (..)
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maederimport Network
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reillyimport System.IO (Handle)
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maederdata CmdlGoalAxiom =
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder ChangeGoals
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reilly | ChangeAxioms
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reillydata CmdlProverConsChecker =
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly | Use_consChecker
648fe1220044aac847acbdfbc4155af5556063ebChristian Maederdata CmdlUseTranslation =
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder | Dont_translate
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder-- * CMDL datatypes
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder{- | CMDLState contains all information the CMDL interface
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder might use at any time. -}
648fe1220044aac847acbdfbc4155af5556063ebChristian Maederdata CmdlState = CmdlState
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder { intState :: IntState -- ^ common interface state
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder , prompter :: CmdlPrompterState -- ^ promter of the interface
ebd23ec61635b0bebf7969d14f65b9d1e39f2b26Liam O'Reilly , openComment :: Bool -- ^ open comment
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder , connections :: [CmdlChannel] -- ^ opened connections
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder , output :: CmdlMessage -- ^ output of interface
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly , hetsOpts :: HetcatsOpts -- ^ hets command options
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder-- | Creates an empty CmdlState
648fe1220044aac847acbdfbc4155af5556063ebChristian MaederemptyCmdlState :: HetcatsOpts -> CmdlState
648fe1220044aac847acbdfbc4155af5556063ebChristian MaederemptyCmdlState opts = CmdlState
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder { intState = IntState
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder { i_state = Nothing
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder , i_hist = IntHistory
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder { undoList = []
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly , redoList = [] }
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly , filename = [] }
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly , prompter = CmdlPrompterState
fa373bc327620e08861294716b4454be8d25669fChristian Maeder { fileLoaded = ""
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder , prompterHead = "> " }
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder , output = emptyCmdlMessage
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder , openComment = False
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder , connections = []
fa373bc327620e08861294716b4454be8d25669fChristian Maeder , hetsOpts = opts }
fa373bc327620e08861294716b4454be8d25669fChristian Maederdata CmdlPrompterState = CmdlPrompterState
fa373bc327620e08861294716b4454be8d25669fChristian Maeder { fileLoaded :: String
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder , prompterHead :: String }
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder{- | Description of a command in order to have a uniform access to any of
e8d99f05c231b379be702a1aa8c7dd0b3c666928Liam O'Reilly the commands -}
e8d99f05c231b379be702a1aa8c7dd0b3c666928Liam O'Reillydata CmdlCmdDescription = CmdlCmdDescription
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder { cmdDescription :: Command
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder , cmdPriority :: CmdlCmdPriority
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly , cmdFn :: CmdlCmdFnClasses
e8d99f05c231b379be702a1aa8c7dd0b3c666928Liam O'Reilly , cmdReq :: CmdlCmdRequirements }
e7cd36335f0f7be9ed5005e71d94c2856b588d62Christian MaedercmdInput :: CmdlCmdDescription -> String
e7cd36335f0f7be9ed5005e71d94c2856b588d62Christian MaedercmdInput = cmdInputStr . cmdDescription
e8d99f05c231b379be702a1aa8c7dd0b3c666928Liam O'ReillycmdName :: CmdlCmdDescription -> String
648fe1220044aac847acbdfbc4155af5556063ebChristian MaedercmdName = cmdNameStr . cmdDescription
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder{- | Some commands have different status, for example 'end-script'
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly needs to be processed even though the interface is in reading script
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly state. The same happens with '}%' even though the interface is in
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder multi line comment state. In order not to treat this few commands
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder separately from the other it is easy just to give to all commands
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder different priorities -}
c0833539c8cf577dd3f2497792fbdd818442744cChristian Maederdata CmdlCmdPriority =
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder CmdNoPriority
c0833539c8cf577dd3f2497792fbdd818442744cChristian Maeder | CmdGreaterThanComments
c0833539c8cf577dd3f2497792fbdd818442744cChristian Maeder | CmdGreaterThanScriptAndComments
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder{- | Any command belongs to one of the following classes of functions,
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder a) f :: s -> IO s
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly b) f :: String -> s -> IO s -}
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian Maederdata CmdlCmdFnClasses =
c0833539c8cf577dd3f2497792fbdd818442744cChristian Maeder CmdNoInput (CmdlState -> IO CmdlState)
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly | CmdWithInput (String -> CmdlState -> IO CmdlState)
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian Maederdata NodeOrEdgeFilter = OpenCons | OpenGoals
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly{- | Datatype describing the types of commands according
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian Maeder to what they expect as input -}
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian Maederdata CmdlCmdRequirements =
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder ReqNodesOrEdges (Maybe Bool) (Maybe NodeOrEdgeFilter)
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder -- ^ Nothing: Both, True: Nodes, False: Edges
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder | ReqConsCheck
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder | ReqComorphism
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maeder | ReqAxm Bool -- ^ True: Axioms, False: Goals
ebd23ec61635b0bebf7969d14f65b9d1e39f2b26Liam O'ReillyformatRequirement :: CmdlCmdRequirements -> String
648fe1220044aac847acbdfbc4155af5556063ebChristian MaederformatRequirement r = let s = showRequirement r in
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder if null s then "" else '<' : s ++ ">"
648fe1220044aac847acbdfbc4155af5556063ebChristian MaedershowRequirement :: CmdlCmdRequirements -> String
648fe1220044aac847acbdfbc4155af5556063ebChristian MaedershowRequirement cr = case cr of
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder ReqConsCheck -> "ConsChecker"
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly ReqProvers -> "Prover"
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder ReqComorphism -> "Comorphism"
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder ReqNodesOrEdges n m -> maybe "" (\ f -> case f of
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder OpenCons -> "OpenCons"
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder OpenGoals -> "Goal") m
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder ++ maybe "NodesOrEdges"
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian Maeder (\ b -> if b then "Nodes" else "Edges") n
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder ReqFile -> "File"
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder ReqAxm b -> if b then "Axioms" else "Goals"
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder ReqNumber -> "Number"
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder ReqNothing -> ""
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder ReqUnknown -> ""
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder-- Communication channel datatypes -----------------------------------------
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder{- | CMDLSocket takes care of opened sockets for comunication with other
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder application like the Broker in the case of PGIP -}
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maederdata CmdlChannel = CmdlChannel
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder { chName :: String
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder , chType :: CmdlChannelType
aa4d26536fffe0153cd81d28925985892ac2f300Christian Maeder , chHandler :: Handle
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder , chSocket :: Maybe CmdlSocket
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder , chProperties :: CmdlChannelProperties }
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder-- | Channel type describes different type of channel
648fe1220044aac847acbdfbc4155af5556063ebChristian Maederdata CmdlChannelType =
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reilly-- | Channel properties describes what a channel can do
580f1724640a78be687e79d0ec95dd2665e77e91Liam O'Reillydata CmdlChannelProperties =
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder | ChReadWrite
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder-- | Describes a socket
f19dc06364e8d6ea36f7c170e1f7a0677de63184Liam O'Reillydata CmdlSocket = CmdlSocket
f21c7417bdd1c0282025cba0f5cb0ff5bc5c98eeLiam O'Reilly { socketHandler :: Socket
f21c7417bdd1c0282025cba0f5cb0ff5bc5c98eeLiam O'Reilly , socketHostName :: HostName
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder , socketPortNumber :: PortNumber }
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- | Datatype describing the list of possible action on a list
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder of selected items -}
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederdata CmdlListAction =
ee48a7a67da604356b665e51aa7545536a09b737Christian Maeder | ActionSetAll
d381ab99d6e2e56e09030577d65d9a118f246d35Christian Maeder | ActionDelAll
ee48a7a67da604356b665e51aa7545536a09b737Christian Maeder-- | output message given by the interface
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maederdata CmdlMessage = CmdlMessage
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder { outputMsg :: String
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder , warningMsg :: String
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reilly , errorMsg :: String }
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'ReillyemptyCmdlMessage :: CmdlMessage
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'ReillyemptyCmdlMessage = CmdlMessage
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reilly { errorMsg = []
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reilly , outputMsg = []
580f1724640a78be687e79d0ec95dd2665e77e91Liam O'Reilly , warningMsg = [] }