| Copyright | uni-bremen and DFKI |
|---|---|
| License | GPLv2 or higher, see LICENSE.txt |
| Maintainer | r.pascanu@jacobs-university.de |
| Stability | provisional |
| Portability | portable |
| Safe Haskell | None |
CMDL.DataTypes
Description
CMDL.DataTypes describes the internal states(or datatypes) of the CMDL interface.
Synopsis
- data CmdlState = CmdlState {
- intState :: IntState
- prompter :: CmdlPrompterState
- openComment :: Bool
- connections :: [CmdlChannel]
- output :: CmdlMessage
- hetsOpts :: HetcatsOpts
- errorCode :: Int
- consCheckers :: [G_cons_checker]
- emptyCmdlState :: HetcatsOpts -> CmdlState
- data CmdlCmdDescription = CmdlCmdDescription {}
- cmdInput :: CmdlCmdDescription -> String
- cmdName :: CmdlCmdDescription -> String
- data CmdlCmdPriority
- data CmdlCmdFnClasses
- = CmdNoInput (CmdlState -> IO CmdlState)
- | CmdWithInput (String -> CmdlState -> IO CmdlState)
- data NodeOrEdgeFilter
- data CmdlCmdRequirements
- = ReqNodesOrEdges (Maybe Bool) (Maybe NodeOrEdgeFilter)
- | ReqProvers
- | ReqConsCheck
- | ReqComorphism
- | ReqLogic
- | ReqFile
- | ReqAxm Bool
- | ReqNumber
- | ReqNothing
- | ReqUnknown
- formatRequirement :: CmdlCmdRequirements -> String
- data CmdlChannel = CmdlChannel {
- chName :: String
- chType :: CmdlChannelType
- chHandler :: Handle
- chSocket :: Maybe CmdlSocket
- chProperties :: CmdlChannelProperties
- data CmdlChannelType
- data CmdlChannelProperties
- = ChRead
- | ChWrite
- | ChReadWrite
- data CmdlSocket = CmdlSocket {
- socketHandler :: Socket
- socketHostName :: HostName
- socketPortNumber :: PortNumber
- data CmdlUseTranslation
- data CmdlProverConsChecker
- data CmdlPrompterState = CmdlPrompterState {
- fileLoaded :: String
- prompterHead :: String
- data CmdlMessage = CmdlMessage {
- outputMsg :: String
- warningMsg :: String
- errorMsg :: String
- emptyCmdlMessage :: CmdlMessage
- data CmdlListAction
- data CmdlGoalAxiom
- data ProveCmdType
Documentation
CMDLState contains all information the CMDL interface might use at any time.
Constructors
| CmdlState | |
Fields
| |
emptyCmdlState :: HetcatsOpts -> CmdlState Source #
Creates an empty CmdlState
data CmdlCmdDescription Source #
Description of a command in order to have a uniform access to any of the commands
Constructors
| CmdlCmdDescription | |
Fields | |
Instances
| Show CmdlCmdDescription Source # | |
Defined in CMDL.DataTypes Methods showsPrec :: Int -> CmdlCmdDescription -> ShowS show :: CmdlCmdDescription -> String showList :: [CmdlCmdDescription] -> ShowS | |
cmdInput :: CmdlCmdDescription -> String Source #
cmdName :: CmdlCmdDescription -> String Source #
data CmdlCmdPriority Source #
Some commands have different status, for example 'end-script' needs to be processed even though the interface is in reading script state. The same happens with '}%' even though the interface is in multi line comment state. In order not to treat this few commands separately from the other it is easy just to give to all commands different priorities
data CmdlCmdFnClasses Source #
Any command belongs to one of the following classes of functions, a) f :: s -> IO s b) f :: String -> s -> IO s
Constructors
| CmdNoInput (CmdlState -> IO CmdlState) | |
| CmdWithInput (String -> CmdlState -> IO CmdlState) |
data NodeOrEdgeFilter Source #
data CmdlCmdRequirements Source #
Datatype describing the types of commands according to what they expect as input
Constructors
| ReqNodesOrEdges (Maybe Bool) (Maybe NodeOrEdgeFilter) | Nothing: Both, True: Nodes, False: Edges |
| ReqProvers | |
| ReqConsCheck | |
| ReqComorphism | |
| ReqLogic | |
| ReqFile | |
| ReqAxm Bool | True: Axioms, False: Goals |
| ReqNumber | |
| ReqNothing | |
| ReqUnknown |
formatRequirement :: CmdlCmdRequirements -> String Source #
data CmdlChannel Source #
CMDLSocket takes care of opened sockets for comunication with other application like the Broker in the case of PGIP
Constructors
| CmdlChannel | |
Fields
| |
data CmdlChannelType Source #
Channel type describes different type of channel
data CmdlChannelProperties Source #
Channel properties describes what a channel can do
Constructors
| ChRead | |
| ChWrite | |
| ChReadWrite |
data CmdlSocket Source #
Describes a socket
Constructors
| CmdlSocket | |
Fields
| |
data CmdlUseTranslation Source #
Constructors
| Do_translate | |
| Dont_translate |
data CmdlProverConsChecker Source #
Constructors
| Use_prover | |
| Use_consChecker |
data CmdlPrompterState Source #
Constructors
| CmdlPrompterState | |
Fields
| |
data CmdlMessage Source #
output message given by the interface
Constructors
| CmdlMessage | |
Fields
| |
data CmdlListAction Source #
Datatype describing the list of possible action on a list of selected items
Constructors
| ActionSet | |
| ActionSetAll | |
| ActionDel | |
| ActionDelAll | |
| ActionAdd |
data CmdlGoalAxiom Source #
Constructors
| ChangeGoals | |
| ChangeAxioms |