| 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.
- data CmdlState = CmdlState {}
- 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
- formatRequirement :: CmdlCmdRequirements -> String
- data CmdlChannel = CmdlChannel {}
- data CmdlChannelType
- data CmdlChannelProperties
- = ChRead
- | ChWrite
- | ChReadWrite
- data CmdlSocket = CmdlSocket {}
- data CmdlUseTranslation
- data CmdlProverConsChecker
- data CmdlPrompterState = CmdlPrompterState {}
- data CmdlMessage = CmdlMessage {}
- emptyCmdlMessage :: CmdlMessage
- data CmdlListAction
- data CmdlGoalAxiom
- data ProveCmdType
Documentation
data CmdlState
CMDLState contains all information the CMDL interface might use at any time.
Constructors
| CmdlState | |
Fields
| |
emptyCmdlState :: HetcatsOpts -> CmdlState
Creates an empty CmdlState
data CmdlCmdDescription
Description of a command in order to have a uniform access to any of the commands
Constructors
| CmdlCmdDescription | |
Fields | |
Instances
cmdInput :: CmdlCmdDescription -> String
cmdName :: CmdlCmdDescription -> String
data CmdlCmdPriority
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
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
data CmdlCmdRequirements
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 |
data CmdlChannel
CMDLSocket takes care of opened sockets for comunication with other application like the Broker in the case of PGIP
Constructors
| CmdlChannel | |
Fields | |
data CmdlChannelType
Channel type describes different type of channel
Channel properties describes what a channel can do
Constructors
| ChRead | |
| ChWrite | |
| ChReadWrite |
data CmdlUseTranslation
Constructors
| Do_translate | |
| Dont_translate |
Constructors
| Use_prover | |
| Use_consChecker |
data CmdlPrompterState
Constructors
| CmdlPrompterState | |
Fields
| |
data CmdlListAction
Datatype describing the list of possible action on a list of selected items
Constructors
| ActionSet | |
| ActionSetAll | |
| ActionDel | |
| ActionDelAll | |
| ActionAdd |
data CmdlGoalAxiom
Constructors
| ChangeGoals | |
| ChangeAxioms |
data ProveCmdType