{-# 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
  { IntState -> IntHistory
i_hist :: IntHistory -- ^ global history management
  , IntState -> Maybe IntIState
i_state :: Maybe IntIState -- ^ internal state
  , IntState -> String
filename :: String } deriving (Int -> IntState -> ShowS
[IntState] -> ShowS
IntState -> String
(Int -> IntState -> ShowS)
-> (IntState -> String) -> ([IntState] -> ShowS) -> Show IntState
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [IntState] -> ShowS
$cshowList :: [IntState] -> ShowS
show :: IntState -> String
$cshow :: IntState -> String
showsPrec :: Int -> IntState -> ShowS
$cshowsPrec :: Int -> IntState -> ShowS
Show)

getMaybeLib :: IntState -> Maybe (LibName, LibEnv)
getMaybeLib :: IntState -> Maybe (LibName, LibEnv)
getMaybeLib = (IntIState -> (LibName, LibEnv))
-> Maybe IntIState -> Maybe (LibName, LibEnv)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\ s :: IntIState
s -> (IntIState -> LibName
i_ln IntIState
s, IntIState -> LibEnv
i_libEnv IntIState
s)) (Maybe IntIState -> Maybe (LibName, LibEnv))
-> (IntState -> Maybe IntIState)
-> IntState
-> Maybe (LibName, LibEnv)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntState -> Maybe IntIState
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
  { IntHistory -> [CmdHistory]
undoList :: [CmdHistory]
  , IntHistory -> [CmdHistory]
redoList :: [CmdHistory] } deriving (Int -> IntHistory -> ShowS
[IntHistory] -> ShowS
IntHistory -> String
(Int -> IntHistory -> ShowS)
-> (IntHistory -> String)
-> ([IntHistory] -> ShowS)
-> Show IntHistory
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [IntHistory] -> ShowS
$cshowList :: [IntHistory] -> ShowS
show :: IntHistory -> String
$cshow :: IntHistory -> String
showsPrec :: Int -> IntHistory -> ShowS
$cshowsPrec :: Int -> IntHistory -> ShowS
Show)

{- | Contains command description needed for undo\/redo actions and
   for displaying commands in the history -}
data CmdHistory = CmdHistory
  { CmdHistory -> Command
command :: Command
  , CmdHistory -> [UndoRedoElem]
cmdHistory :: [UndoRedoElem] } deriving (Int -> CmdHistory -> ShowS
[CmdHistory] -> ShowS
CmdHistory -> String
(Int -> CmdHistory -> ShowS)
-> (CmdHistory -> String)
-> ([CmdHistory] -> ShowS)
-> Show CmdHistory
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CmdHistory] -> ShowS
$cshowList :: [CmdHistory] -> ShowS
show :: CmdHistory -> String
$cshow :: CmdHistory -> String
showsPrec :: Int -> CmdHistory -> ShowS
$cshowsPrec :: Int -> CmdHistory -> ShowS
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 (Int -> UndoRedoElem -> ShowS
[UndoRedoElem] -> ShowS
UndoRedoElem -> String
(Int -> UndoRedoElem -> ShowS)
-> (UndoRedoElem -> String)
-> ([UndoRedoElem] -> ShowS)
-> Show UndoRedoElem
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [UndoRedoElem] -> ShowS
$cshowList :: [UndoRedoElem] -> ShowS
show :: UndoRedoElem -> String
$cshow :: UndoRedoElem -> String
showsPrec :: Int -> UndoRedoElem -> ShowS
$cshowsPrec :: Int -> UndoRedoElem -> ShowS
Show)

data ListChange =
    AxiomsChange [String] Int
  | GoalsChange [String] Int
  | NodesChange [Int_NodeInfo]
  deriving (Int -> ListChange -> ShowS
[ListChange] -> ShowS
ListChange -> String
(Int -> ListChange -> ShowS)
-> (ListChange -> String)
-> ([ListChange] -> ShowS)
-> Show ListChange
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ListChange] -> ShowS
$cshowList :: [ListChange] -> ShowS
show :: ListChange -> String
$cshow :: ListChange -> String
showsPrec :: Int -> ListChange -> ShowS
$cshowsPrec :: Int -> ListChange -> ShowS
Show)

-- | full description of the internal state required by all interfaces
data IntIState = IntIState
  { IntIState -> LibEnv
i_libEnv :: LibEnv
  , IntIState -> LibName
i_ln :: LibName
  {- these are PGIP specific, but they need to be treated by the common
     history mechanism , therefore they need to be here -}
  , IntIState -> [Int_NodeInfo]
elements :: [Int_NodeInfo]
  , IntIState -> Maybe AnyComorphism
cComorphism :: Maybe AnyComorphism
  , IntIState -> Maybe G_prover
prover :: Maybe G_prover
  , IntIState -> Maybe G_cons_checker
consChecker :: Maybe G_cons_checker
  , IntIState -> Bool
save2file :: Bool
  , IntIState -> Bool
useTheorems :: Bool
  , IntIState -> Bool
showOutput :: Bool
  , IntIState -> ATPTacticScript
script :: ATPTacticScript
  , IntIState -> Bool
loadScript :: Bool } deriving (Int -> IntIState -> ShowS
[IntIState] -> ShowS
IntIState -> String
(Int -> IntIState -> ShowS)
-> (IntIState -> String)
-> ([IntIState] -> ShowS)
-> Show IntIState
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [IntIState] -> ShowS
$cshowList :: [IntIState] -> ShowS
show :: IntIState -> String
$cshow :: IntIState -> String
showsPrec :: Int -> IntIState -> ShowS
$cshowsPrec :: Int -> IntIState -> ShowS
Show)

data Int_NodeInfo = Element ProofState Int deriving Int -> Int_NodeInfo -> ShowS
[Int_NodeInfo] -> ShowS
Int_NodeInfo -> String
(Int -> Int_NodeInfo -> ShowS)
-> (Int_NodeInfo -> String)
-> ([Int_NodeInfo] -> ShowS)
-> Show Int_NodeInfo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Int_NodeInfo] -> ShowS
$cshowList :: [Int_NodeInfo] -> ShowS
show :: Int_NodeInfo -> String
$cshow :: Int_NodeInfo -> String
showsPrec :: Int -> Int_NodeInfo -> ShowS
$cshowsPrec :: Int -> Int_NodeInfo -> ShowS
Show