Copyright	(c) Uni Bremen 2002-2008
License	GPLv2 or higher, see LICENSE.txt
Maintainer	r.pascanu@gmail.com
Stability	provisional
Portability	non-portable (imports Logic)
Safe Haskell	None

Interfaces.DataTypes

Description

Different data structures that are (or should be) shared by all interfaces of Hets

Synopsis

data IntState = IntState {
- i_hist :: IntHistory
- i_state :: Maybe IntIState
- filename :: String
}
getMaybeLib :: IntState -> Maybe (LibName, LibEnv)
data IntHistory = IntHistory {
- undoList :: [CmdHistory]
- redoList :: [CmdHistory]
}
data CmdHistory = CmdHistory {
- command :: Command
- cmdHistory :: [UndoRedoElem]
}
data IntIState = IntIState {
- i_libEnv :: LibEnv
- i_ln :: LibName
- elements :: [Int_NodeInfo]
- cComorphism :: Maybe AnyComorphism
- prover :: Maybe G_prover
- consChecker :: Maybe G_cons_checker
- save2file :: Bool
- useTheorems :: Bool
- showOutput :: Bool
- script :: ATPTacticScript
- loadScript :: Bool
}
data Int_NodeInfo = Element ProofState Int
data UndoRedoElem
- = UseThmChange Bool
- | Save2FileChange Bool
- | ProverChange (Maybe G_prover)
- | ConsCheckerChange (Maybe G_cons_checker)
- | ScriptChange ATPTacticScript
- | LoadScriptChange Bool
- | CComorphismChange (Maybe AnyComorphism)
- | ListChange [ListChange]
- | IStateChange (Maybe IntIState)
- | DgCommandChange LibName
- | ChShowOutput Bool
data ListChange
- = AxiomsChange [String] Int
- | GoalsChange [String] Int
- | NodesChange [Int_NodeInfo]

Documentation

data IntState Source #

Internal state of the interface, it contains the development graph and a full history. While this in most cases describes the state of development graph at a given time for GUI it is not the same for the PGIP ( it does not describe selected nodes). If one switches from one interface to the other passing this informations should be sufficient with minimal loss of information ( like selected nodes, unfinished script .. and so on)

Constructors

IntState
Fields i_hist :: IntHistory global history management i_state :: Maybe IntIState internal state filename :: String

Instances

Instances details

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

getMaybeLib :: IntState -> Maybe (LibName, LibEnv) Source #

data IntHistory Source #

Contains the detailed global history as two list, a list of actions for undo, and a list of action for redo commands

Constructors

IntHistory
Fields undoList :: [CmdHistory] redoList :: [CmdHistory]

Instances

Instances details

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

data CmdHistory Source #

Contains command description needed for undo/redo actions and for displaying commands in the history

Constructors

CmdHistory
Fields command :: Command cmdHistory :: [UndoRedoElem]

Instances

Instances details

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

data IntIState Source #

full description of the internal state required by all interfaces

Constructors

IntIState
Fields i_libEnv :: LibEnv i_ln :: LibName elements :: [Int_NodeInfo] cComorphism :: Maybe AnyComorphism prover :: Maybe G_prover consChecker :: Maybe G_cons_checker save2file :: Bool useTheorems :: Bool showOutput :: Bool script :: ATPTacticScript loadScript :: Bool

Instances

Instances details

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

data Int_NodeInfo Source #

Constructors

Element ProofState Int

Instances

Instances details

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

data UndoRedoElem Source #

History elements for the proof state, only LibName would be used by GUI because it keeps track only to changes to the development graph, the other are for PGIP but in order to integrate both they should use same structure

Constructors

UseThmChange Bool
Save2FileChange Bool
ProverChange (Maybe G_prover)
ConsCheckerChange (Maybe G_cons_checker)
ScriptChange ATPTacticScript
LoadScriptChange Bool
CComorphismChange (Maybe AnyComorphism)
ListChange [ListChange]
IStateChange (Maybe IntIState)
DgCommandChange LibName
ChShowOutput Bool

Instances

Instances details

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

data ListChange Source #

Constructors

AxiomsChange [String] Int
GoalsChange [String] Int
NodesChange [Int_NodeInfo]

Instances

Instances details

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