content: {-# LANGUAGE ExistentialQuantification #-}
  {- |
  Module      :  ./Interfaces/DataTypes.hs
  Description :  Common Data types to be used between interfaces
  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)
  
  Different data structures that are (or should be) shared by all interfaces
  of Hets
  -}
  
  module Interfaces.DataTypes
    ( IntState (..)
    , getMaybeLib
    , IntHistory (..)
    , CmdHistory (..)
    , IntIState (..)
    , Int_NodeInfo (..)
    , UndoRedoElem (..)
    , ListChange (..)
    ) where
  
  import Static.DevGraph
  import Common.LibName
  import Proofs.AbstractState
  import Logic.Comorphism
  import Interfaces.Command
  import Interfaces.GenericATPState
  
  {- | 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) -}
  data IntState = IntState
    { i_hist :: IntHistory -- ^ global history management
    , i_state :: Maybe IntIState -- ^ internal state
    , filename :: String } deriving (Show)
  
  getMaybeLib :: IntState -> Maybe (LibName, LibEnv)
  getMaybeLib = fmap (\ s -> (i_ln s, i_libEnv s)) . i_state
  
  {- | Contains the detailed global history as two list, a list of actions
     for undo, and a list of action for redo commands -}
  data IntHistory = IntHistory
    { undoList :: [CmdHistory]
    , redoList :: [CmdHistory] } deriving (Show)
  
  {- | Contains command description needed for undo\/redo actions and
     for displaying commands in the history -}
  data CmdHistory = CmdHistory
    { command :: Command
    , cmdHistory :: [UndoRedoElem] } deriving (Show)
  
  {- | 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 -}
  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
    deriving (Show)
  
  data ListChange =
      AxiomsChange [String] Int
    | GoalsChange [String] Int
    | NodesChange [Int_NodeInfo]
    deriving (Show)
  
  -- | full description of the internal state required by all interfaces
  data IntIState = IntIState
    { i_libEnv :: LibEnv
    , i_ln :: LibName
    {- these are PGIP specific, but they need to be treated by the common
       history mechanism , therefore they need to be here -}
    , 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 } deriving (Show)
  
  data Int_NodeInfo = Element ProofState Int deriving Show
  