Copyright	(c) Christian Maeder DFKI GmbH 2009
License	GPLv2 or higher, see LICENSE.txt
Maintainer	Christian.Maeder@dfki.de
Stability	provisional
Portability	portable
Safe Haskell	None

Interfaces.Command

Description

data types for development graph commands to be invoked via the GUI, the command-line-interface (CMDL), and other tools

Synopsis

data GlobCmd
- = Automatic
- | GlobDecomp
- | GlobSubsume
- | LocalDecomp
- | LocalInference
- | CompositionProveEdges
- | CompositionCreateEdges
- | Conservativity
- | ThmHideShift
- | HideThmShift
- | Colimit
- | NormalForm
- | TriangleCons
- | Freeness
- | ThmFreeShift
- | QualifyNames
- | UndoCmd
- | RedoCmd
- | Importing
- | DisjointUnion
- | Renaming
- | Hiding
- | Heterogeneity
- | ProveCurrent
- | DisproveCurrent
- | CheckConsistencyCurrent
- | CheckConservativityAll
- | DropTranslation
globCmdList :: [GlobCmd]
menuTextGlobCmd :: GlobCmd -> String
cmdlGlobCmd :: GlobCmd -> String
isDgRule :: GlobCmd -> Bool
isFlatteningCmd :: GlobCmd -> Bool
isUndoOrRedo :: GlobCmd -> Bool
describeGlobCmd :: GlobCmd -> String
globCmdNameStr :: GlobCmd -> String
data SelectCmd
- = LibFile
- | Lib
- | Node
- | ComorphismTranslation
- | Prover
- | Goal
- | ConsistencyChecker
- | Link
- | ConservativityCheckerOpen
- | ConservativityChecker
selectCmdList :: [SelectCmd]
selectCmdNameStr :: SelectCmd -> String
describeSelectCmd :: SelectCmd -> String
data InspectCmd
- = Libs
- | Nodes
- | Edges
- | UndoHist
- | RedoHist
- | EdgeInfo
- | CurrentComorphism
- | LocalAxioms
- | NodeInfo
- | ComorphismsTo
- | TranslatedTheory
- | Theory
- | AllGoals
- | ProvenGoals
- | UnprovenGoals
- | Axioms
- | Taxonomy
- | Concept
inspectCmdList :: [InspectCmd]
showInspectCmd :: InspectCmd -> String
requiresNode :: InspectCmd -> Bool
data ChangeCmd
- = Expand
- | AddView
describeChangeCmd :: ChangeCmd -> String
changeCmdList :: [ChangeCmd]
changeCmdNameStr :: ChangeCmd -> String
data Command
- = GlobCmd GlobCmd
- | SelectCmd SelectCmd String
- | TimeLimit Int
- | SetAxioms [String]
- | ShowOutput Bool
- | IncludeProvenTheorems Bool
- | InspectCmd InspectCmd (Maybe String)
- | CommentCmd String
- | GroupCmd [Command]
- | ChangeCmd ChangeCmd String
- | HelpCmd
- | ExitCmd
eqCmd :: Command -> Command -> Bool
mkSelectCmd :: SelectCmd -> Command
mkChangeCmd :: ChangeCmd -> Command
cmdInputStr :: Command -> String
setInputStr :: String -> Command -> Command
cmdNameStr :: Command -> String
showCmd :: Command -> String
describeCmd :: Command -> String
commandList :: [Command]

Documentation

data GlobCmd Source #

Instances

Instances details

Bounded GlobCmd Source #
Instance details Defined in Interfaces.Command Methods minBound :: GlobCmd maxBound :: GlobCmd
Enum GlobCmd Source #
Instance details Defined in Interfaces.Command Methods succ :: GlobCmd -> GlobCmd pred :: GlobCmd -> GlobCmd toEnum :: Int -> GlobCmd fromEnum :: GlobCmd -> Int enumFrom :: GlobCmd -> [GlobCmd] enumFromThen :: GlobCmd -> GlobCmd -> [GlobCmd] enumFromTo :: GlobCmd -> GlobCmd -> [GlobCmd] enumFromThenTo :: GlobCmd -> GlobCmd -> GlobCmd -> [GlobCmd]
Eq GlobCmd Source #
Instance details Defined in Interfaces.Command Methods (==) :: GlobCmd -> GlobCmd -> Bool (/=) :: GlobCmd -> GlobCmd -> Bool
Ord GlobCmd Source #
Instance details Defined in Interfaces.Command Methods compare :: GlobCmd -> GlobCmd -> Ordering (<) :: GlobCmd -> GlobCmd -> Bool (<=) :: GlobCmd -> GlobCmd -> Bool (>) :: GlobCmd -> GlobCmd -> Bool (>=) :: GlobCmd -> GlobCmd -> Bool max :: GlobCmd -> GlobCmd -> GlobCmd min :: GlobCmd -> GlobCmd -> GlobCmd
Show GlobCmd Source #
Instance details Defined in Interfaces.Command Methods showsPrec :: Int -> GlobCmd -> ShowS show :: GlobCmd -> String showList :: [GlobCmd] -> ShowS

globCmdList :: [GlobCmd] Source #

menuTextGlobCmd :: GlobCmd -> String Source #

cmdlGlobCmd :: GlobCmd -> String Source #

even some short names for the command line interface

isDgRule :: GlobCmd -> Bool Source #

isFlatteningCmd :: GlobCmd -> Bool Source #

isUndoOrRedo :: GlobCmd -> Bool Source #

describeGlobCmd :: GlobCmd -> String Source #

globCmdNameStr :: GlobCmd -> String Source #

data SelectCmd Source #

select a named entity

Constructors

LibFile
Lib
Node
ComorphismTranslation
Prover
Goal
ConsistencyChecker
Link
ConservativityCheckerOpen
ConservativityChecker

Instances

Instances details

Bounded SelectCmd Source #
Instance details Defined in Interfaces.Command Methods minBound :: SelectCmd maxBound :: SelectCmd
Enum SelectCmd Source #
Instance details Defined in Interfaces.Command Methods succ :: SelectCmd -> SelectCmd pred :: SelectCmd -> SelectCmd toEnum :: Int -> SelectCmd fromEnum :: SelectCmd -> Int enumFrom :: SelectCmd -> [SelectCmd] enumFromThen :: SelectCmd -> SelectCmd -> [SelectCmd] enumFromTo :: SelectCmd -> SelectCmd -> [SelectCmd] enumFromThenTo :: SelectCmd -> SelectCmd -> SelectCmd -> [SelectCmd]
Eq SelectCmd Source #
Instance details Defined in Interfaces.Command Methods (==) :: SelectCmd -> SelectCmd -> Bool (/=) :: SelectCmd -> SelectCmd -> Bool
Ord SelectCmd Source #
Instance details Defined in Interfaces.Command Methods compare :: SelectCmd -> SelectCmd -> Ordering (<) :: SelectCmd -> SelectCmd -> Bool (<=) :: SelectCmd -> SelectCmd -> Bool (>) :: SelectCmd -> SelectCmd -> Bool (>=) :: SelectCmd -> SelectCmd -> Bool max :: SelectCmd -> SelectCmd -> SelectCmd min :: SelectCmd -> SelectCmd -> SelectCmd
Show SelectCmd Source #
Instance details Defined in Interfaces.Command Methods showsPrec :: Int -> SelectCmd -> ShowS show :: SelectCmd -> String showList :: [SelectCmd] -> ShowS

selectCmdList :: [SelectCmd] Source #

selectCmdNameStr :: SelectCmd -> String Source #

describeSelectCmd :: SelectCmd -> String Source #

data InspectCmd Source #

Constructors

Libs
Nodes
Edges
UndoHist
RedoHist
EdgeInfo
CurrentComorphism
LocalAxioms
NodeInfo
ComorphismsTo
TranslatedTheory
Theory
AllGoals
ProvenGoals
UnprovenGoals
Axioms
Taxonomy
Concept

Instances

Instances details

Bounded InspectCmd Source #
Instance details Defined in Interfaces.Command Methods minBound :: InspectCmd maxBound :: InspectCmd
Enum InspectCmd Source #
Instance details Defined in Interfaces.Command Methods succ :: InspectCmd -> InspectCmd pred :: InspectCmd -> InspectCmd toEnum :: Int -> InspectCmd fromEnum :: InspectCmd -> Int enumFrom :: InspectCmd -> [InspectCmd] enumFromThen :: InspectCmd -> InspectCmd -> [InspectCmd] enumFromTo :: InspectCmd -> InspectCmd -> [InspectCmd] enumFromThenTo :: InspectCmd -> InspectCmd -> InspectCmd -> [InspectCmd]
Eq InspectCmd Source #
Instance details Defined in Interfaces.Command Methods (==) :: InspectCmd -> InspectCmd -> Bool (/=) :: InspectCmd -> InspectCmd -> Bool
Ord InspectCmd Source #
Instance details Defined in Interfaces.Command Methods compare :: InspectCmd -> InspectCmd -> Ordering (<) :: InspectCmd -> InspectCmd -> Bool (<=) :: InspectCmd -> InspectCmd -> Bool (>) :: InspectCmd -> InspectCmd -> Bool (>=) :: InspectCmd -> InspectCmd -> Bool max :: InspectCmd -> InspectCmd -> InspectCmd min :: InspectCmd -> InspectCmd -> InspectCmd
Show InspectCmd Source #
Instance details Defined in Interfaces.Command Methods showsPrec :: Int -> InspectCmd -> ShowS show :: InspectCmd -> String showList :: [InspectCmd] -> ShowS

inspectCmdList :: [InspectCmd] Source #

showInspectCmd :: InspectCmd -> String Source #

requiresNode :: InspectCmd -> Bool Source #

data ChangeCmd Source #

Constructors

Expand
AddView

Instances

Instances details

Bounded ChangeCmd Source #
Instance details Defined in Interfaces.Command Methods minBound :: ChangeCmd maxBound :: ChangeCmd
Enum ChangeCmd Source #
Instance details Defined in Interfaces.Command Methods succ :: ChangeCmd -> ChangeCmd pred :: ChangeCmd -> ChangeCmd toEnum :: Int -> ChangeCmd fromEnum :: ChangeCmd -> Int enumFrom :: ChangeCmd -> [ChangeCmd] enumFromThen :: ChangeCmd -> ChangeCmd -> [ChangeCmd] enumFromTo :: ChangeCmd -> ChangeCmd -> [ChangeCmd] enumFromThenTo :: ChangeCmd -> ChangeCmd -> ChangeCmd -> [ChangeCmd]
Eq ChangeCmd Source #
Instance details Defined in Interfaces.Command Methods (==) :: ChangeCmd -> ChangeCmd -> Bool (/=) :: ChangeCmd -> ChangeCmd -> Bool
Ord ChangeCmd Source #
Instance details Defined in Interfaces.Command Methods compare :: ChangeCmd -> ChangeCmd -> Ordering (<) :: ChangeCmd -> ChangeCmd -> Bool (<=) :: ChangeCmd -> ChangeCmd -> Bool (>) :: ChangeCmd -> ChangeCmd -> Bool (>=) :: ChangeCmd -> ChangeCmd -> Bool max :: ChangeCmd -> ChangeCmd -> ChangeCmd min :: ChangeCmd -> ChangeCmd -> ChangeCmd
Show ChangeCmd Source #
Instance details Defined in Interfaces.Command Methods showsPrec :: Int -> ChangeCmd -> ShowS show :: ChangeCmd -> String showList :: [ChangeCmd] -> ShowS

describeChangeCmd :: ChangeCmd -> String Source #

changeCmdList :: [ChangeCmd] Source #

changeCmdNameStr :: ChangeCmd -> String Source #

data Command Source #

Constructors

GlobCmd GlobCmd
SelectCmd SelectCmd String
TimeLimit Int
SetAxioms [String]
ShowOutput Bool
IncludeProvenTheorems Bool
InspectCmd InspectCmd (Maybe String)
CommentCmd String
GroupCmd [Command]
ChangeCmd ChangeCmd String
HelpCmd
ExitCmd

Instances

Instances details

Show Command Source #
Instance details Defined in Interfaces.Command Methods showsPrec :: Int -> Command -> ShowS show :: Command -> String showList :: [Command] -> ShowS

eqCmd :: Command -> Command -> Bool Source #

mkSelectCmd :: SelectCmd -> Command Source #

mkChangeCmd :: ChangeCmd -> Command Source #

cmdInputStr :: Command -> String Source #

setInputStr :: String -> Command -> Command Source #

cmdNameStr :: Command -> String Source #

showCmd :: Command -> String Source #

show command with arguments

describeCmd :: Command -> String Source #

commandList :: [Command] Source #

Automatic
GlobDecomp
GlobSubsume
LocalDecomp
LocalInference
CompositionProveEdges
CompositionCreateEdges
Conservativity
ThmHideShift
HideThmShift
Colimit
NormalForm
TriangleCons
Freeness
ThmFreeShift
QualifyNames
UndoCmd
RedoCmd
Importing
DisjointUnion
Renaming
Hiding
Heterogeneity
ProveCurrent
DisproveCurrent
CheckConsistencyCurrent
CheckConservativityAll
DropTranslation