DataTypes.hs revision f153609d4ff5616d7caa410df605afcdfb9956df
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : $Header$
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiDescription : Common Data types to be used between interfaces
4fd9d02aaec1d0447c2897f977c4c48b0c7e5c20Christian MaederCopyright : (c) Uni Bremen 2002-2008
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : r.pascanu@gmail.com
2a0b5e7b246cc32d46b4ed4e53ab8e909e41c3d0Heng JiangStability : provisional
2a0b5e7b246cc32d46b4ed4e53ab8e909e41c3d0Heng JiangPortability : non-portable (imports Logic)
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiDifferent data structures that are (or should be) shared by all interfaces
dade808234103ea180fa5a2457f2ee8ff76c8e1dChristian Maeder ( IntState(..)
dade808234103ea180fa5a2457f2ee8ff76c8e1dChristian Maeder , IntHistory(..)
dade808234103ea180fa5a2457f2ee8ff76c8e1dChristian Maeder , Int_CmdHistoryDescription(..)
dade808234103ea180fa5a2457f2ee8ff76c8e1dChristian Maeder , IntIState(..)
dade808234103ea180fa5a2457f2ee8ff76c8e1dChristian Maeder , Int_NodeInfo(..)
dade808234103ea180fa5a2457f2ee8ff76c8e1dChristian Maeder , UndoRedoElem(..)
2a0b5e7b246cc32d46b4ed4e53ab8e909e41c3d0Heng Jiang , ListChange(..)
c698ca3d47b105a82ec1f19e8c6bc29ab1d1b63dChristian Maeder-- | Internal state of the interface, it contains the development graph
c698ca3d47b105a82ec1f19e8c6bc29ab1d1b63dChristian Maeder-- and a full history. While this in most cases describes the state of
c698ca3d47b105a82ec1f19e8c6bc29ab1d1b63dChristian Maeder-- development graph at a given time for GUI it is not the same for the
eaf34cf96fbfcdcce7f3bdb322c4ea7ebd1fd220Liam O'Reilly-- PGIP ( it does not describe selected nodes). If one switches from one
c698ca3d47b105a82ec1f19e8c6bc29ab1d1b63dChristian Maeder-- interface to the other passing this informations should be sufficient
c698ca3d47b105a82ec1f19e8c6bc29ab1d1b63dChristian Maeder-- with minimal loss of information ( like selected nodes, unfinished
c698ca3d47b105a82ec1f19e8c6bc29ab1d1b63dChristian Maeder-- script .. and so on)
def40d8182c4db2a91afaec94458809a7568baf3Liam O'Reillydata IntState = IntState {
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder -- global history management
a208edf329751a734895216ad5b0e334a9ac6a44Christian Maeder i_hist :: IntHistory,
e00f5b4d89ac027e883461aab6248e33ad10ae8eChristian Maeder -- internal state
e00f5b4d89ac027e883461aab6248e33ad10ae8eChristian Maeder i_state :: Maybe IntIState
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder-- | Contains the detailed global history as two list, a list of actions
bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian Maeder-- for undo, and a list of action for redo commands
dade808234103ea180fa5a2457f2ee8ff76c8e1dChristian Maederdata IntHistory = IntHistory {
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder -- | history for undo command, a list of command descriptions
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder undoList :: [Int_CmdHistoryDescription],
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder -- | history for redo command, a list of command descriptions
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder redoList :: [Int_CmdHistoryDescription]
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder-- | Contains command description needed for undo/redo actions and
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder-- for displaying commands in the history
e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maederdata Int_CmdHistoryDescription = Int_CmdHistoryDescription {
bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian Maeder -- | command name, used for displaying history elements
dade808234103ea180fa5a2457f2ee8ff76c8e1dChristian Maeder cmdName :: String,
dade808234103ea180fa5a2457f2ee8ff76c8e1dChristian Maeder -- | libname needed to undo actions
dade808234103ea180fa5a2457f2ee8ff76c8e1dChristian Maeder cmdDescription :: [UndoRedoElem]
dade808234103ea180fa5a2457f2ee8ff76c8e1dChristian Maeder-- | History elements for the proof state, only LIB_NAME would be used
2a0b5e7b246cc32d46b4ed4e53ab8e909e41c3d0Heng Jiang-- by GUI/ because it keeps track only to changes to the development graph,
c8ecc5578d32b222f35b625d4dfe7a3fd8bb4173Christian Maeder-- the other are for PGIP but in order to integrate both they should use
c8ecc5578d32b222f35b625d4dfe7a3fd8bb4173Christian Maeder-- same structure
2a0b5e7b246cc32d46b4ed4e53ab8e909e41c3d0Heng Jiangdata UndoRedoElem =
bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian Maeder UseThmChange Bool
e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder | Save2FileChange Bool
e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder | ProverChange (Maybe G_prover)
2a0b5e7b246cc32d46b4ed4e53ab8e909e41c3d0Heng Jiang | ConsCheckerChange (Maybe G_cons_checker)
e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder | ScriptChange ATPTactic_script
4fd9d02aaec1d0447c2897f977c4c48b0c7e5c20Christian Maeder | LoadScriptChange Bool
4fd9d02aaec1d0447c2897f977c4c48b0c7e5c20Christian Maeder | CComorphismChange (Maybe AnyComorphism)
4fd9d02aaec1d0447c2897f977c4c48b0c7e5c20Christian Maeder | ListChange [ListChange]
4fd9d02aaec1d0447c2897f977c4c48b0c7e5c20Christian Maeder | IStateChange (Maybe IntIState)
4fd9d02aaec1d0447c2897f977c4c48b0c7e5c20Christian Maeder | DgCommandChange LIB_NAME
e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maederdata ListChange =
e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder AxiomsChange [String] Int
2a0b5e7b246cc32d46b4ed4e53ab8e909e41c3d0Heng Jiang | GoalsChange [String] Int
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder | NodesChange [Int_NodeInfo]
4fd9d02aaec1d0447c2897f977c4c48b0c7e5c20Christian Maeder-- | full description of the internal state required by all interfaces
4fd9d02aaec1d0447c2897f977c4c48b0c7e5c20Christian Maederdata IntIState = IntIState {
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder i_libEnv :: LibEnv,
4fd9d02aaec1d0447c2897f977c4c48b0c7e5c20Christian Maeder i_ln :: LIB_NAME,
4fd9d02aaec1d0447c2897f977c4c48b0c7e5c20Christian Maeder -- these are PGIP specific, but they need to be treated by the common
2a0b5e7b246cc32d46b4ed4e53ab8e909e41c3d0Heng Jiang -- history mechanism , therefore they need to be here
2a0b5e7b246cc32d46b4ed4e53ab8e909e41c3d0Heng Jiang elements :: [Int_NodeInfo],
4fd9d02aaec1d0447c2897f977c4c48b0c7e5c20Christian Maeder cComorphism :: Maybe AnyComorphism,
2a0b5e7b246cc32d46b4ed4e53ab8e909e41c3d0Heng Jiang prover :: Maybe G_prover,
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder consChecker :: Maybe G_cons_checker,
e00f5b4d89ac027e883461aab6248e33ad10ae8eChristian Maeder save2file :: Bool,
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder useTheorems :: Bool,
4fd9d02aaec1d0447c2897f977c4c48b0c7e5c20Christian Maeder script :: ATPTactic_script,
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder loadScript :: Bool
4fd9d02aaec1d0447c2897f977c4c48b0c7e5c20Christian Maederdata Int_NodeInfo = forall lid1 sublogics1
4fd9d02aaec1d0447c2897f977c4c48b0c7e5c20Christian Maeder basic_spec1 sentence1 symb_items1 symb_map_items1
e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1 .
e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder Logic lid1 sublogics1 basic_spec1 sentence1
e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder symb_items1 symb_map_items1 sign1 morphism1
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder symbol1 raw_symbol1 proof_tree1 =>
4fd9d02aaec1d0447c2897f977c4c48b0c7e5c20Christian Maeder Element (ProofState lid1 sentence1) Int