content: {- |
  Module      :./Interfaces/History.hs
  Description : history management functions
  Copyright   : uni-bremen and DFKI
  License     : GPLv2 or higher, see LICENSE.txt
  Maintainer  : r.pascanu@jacobs-university.de
  Stability   : provisional
  Portability : portable
  
  Interfaces.History contains different functions that deal
  with history
  
  -}
  
  module Interfaces.History
           ( undoOneStep
           , redoOneStep
           , undoOneStepWithUpdate
           , redoOneStepWithUpdate
           , add2history
           ) where
  
  import Interfaces.DataTypes
  import Interfaces.Command
  import Common.LibName
  
  import Proofs.AbstractState
  
  import Static.DevGraph
  import Static.History
  
  import qualified Data.Map as Map
  
  {- | Datatype used to differentiate between the two actions (so that code does
  not get duplicated -}
  data UndoOrRedo =
     DoUndo
   | DoRedo
  
  add2history :: Command -> IntState -> [UndoRedoElem] -> IntState
  add2history nm st descr = let
    hst = i_hist st
    ul = undoList hst
    nwEl = CmdHistory
      { command = nm
      , cmdHistory = descr }
    in st { i_hist = hst { undoList = nwEl : ul } }
  
  -- | Undo or redo a command that modified the development graph
  undoRedoDgCmd :: UndoOrRedo -> IntState -> LibName
                -> ([DGChange] -> DGraph -> IO ()) -> IO IntState
  undoRedoDgCmd actionType state ln update =
    case i_state state of
      -- should I return an error message??
     Nothing -> return state
     Just dgS -> do
       let
           {- take ln from the history storage ??
           in contrast to GUI here you operate with only one ln at a time -}
           dg = lookupDGraph ln (i_libEnv dgS)
           (dg', changes) = ( case actionType of
                         DoUndo -> undoHistStep
                         DoRedo -> redoHistStep) dg
           newEnv = Map.insert ln dg' (i_libEnv dgS)
           newst = state { i_state = Just $ dgS { i_libEnv = newEnv } }
       update changes dg'
       return newst
  
  {- | Analyze changes to the selected nodes, return new nodes plus a list
  of changes that would undo last changes -}
  processList :: [ListChange] -> [Int_NodeInfo]
              -> [ListChange] -> ([Int_NodeInfo], [ListChange])
  processList ls elems acc
   = case ls of
      -- if nothing to process return elements and changes
      [] -> (elems, acc)
      x : l ->
        -- else check what type of change we are dealing with
        case x of
         -- if it is a change in axioms
         AxiomsChange nwaxms nb ->
           -- apply change and store the undo action
           let nwls = map (\ y ->
                            case y of
                             Element ps nb' ->
                              if nb' == nb
                              then (Element ps {includedAxioms = nwaxms} nb
                                  , [AxiomsChange (includedAxioms ps) nb])
                              else (y, []) ) elems
               nwelems = map fst nwls
               changesLs = concatMap snd nwls
           in processList l nwelems (changesLs ++ acc)
         -- if it is a change in goals
         GoalsChange nwgls nb ->
           -- apply change and store the undo action
           let nwls = map (\ y ->
                            case y of
                             Element ps nb' ->
                              if nb' == nb
                              then (Element ps {selectedGoals = nwgls} nb
                                  , [GoalsChange (selectedGoals ps) nb])
                              else (y, [])) elems
               nwelems = map fst nwls
               changeLs = concatMap snd nwls
           in processList l nwelems (changeLs ++ acc)
         -- if selected nodes change
         NodesChange nwelems ->
           processList l nwelems (NodesChange elems : acc)
  
  -- | Process one step of undo or redo
  processAny :: UndoOrRedo -> IntState
             -> (LibName -> [DGChange] -> DGraph -> IO ()) -> IO IntState
  processAny actype state update = do
    let hst = case actype of
                {- find out the list of actions according to the action
                (undo/redo) -}
                DoUndo -> undoList $ i_hist state
                DoRedo -> redoList $ i_hist state
    case hst of
      [] -> return state
      x : l -> do
         (nwst, ch) <- processUndoRedoElems actype (cmdHistory x) state [] update
         let
           x' = x { cmdHistory = ch }
           i_hist_state = i_hist state
           nwstate = case actype of
                      DoUndo -> nwst {
                                i_hist = IntHistory {
                                          undoList = l,
                                          redoList = x' : redoList i_hist_state
                                          }
                                }
                      DoRedo -> nwst {
                                i_hist = IntHistory {
                                          redoList = l,
                                          undoList = x' : undoList i_hist_state
                                          }
                                }
         return nwstate
  
  -- | Process a list of undo or redo changes
  processUndoRedoElems :: UndoOrRedo -> [UndoRedoElem] -> IntState
                       -> [UndoRedoElem]
                       -> (LibName -> [DGChange] -> DGraph -> IO ())
                       -> IO (IntState, [UndoRedoElem])
  processUndoRedoElems actype ls state acc update
   = case i_state state of
      Nothing -> return (state, [])
      Just ist ->
       case ls of
        [] -> return (state, acc)
        ChShowOutput s : l -> do
           let nwst = state {i_state = Just $ ist { showOutput = s}}
               ch = ChShowOutput $ showOutput ist
           processUndoRedoElems actype l nwst (ch : acc) update
        UseThmChange sw : l -> do
           let nwst = state { i_state = Just $ ist { useTheorems = sw } }
               ch = UseThmChange $ useTheorems ist
           processUndoRedoElems actype l nwst (ch : acc) update
        Save2FileChange sw : l -> do
           let nwst = state { i_state = Just $ ist { save2file = sw } }
               ch = Save2FileChange $ save2file ist
           processUndoRedoElems actype l nwst (ch : acc) update
        ProverChange nwp : l -> do
           let nwst = state { i_state = Just $ ist { prover = nwp } }
               ch = ProverChange $ prover ist
           processUndoRedoElems actype l nwst (ch : acc) update
        ConsCheckerChange nwc : l -> do
           let nwst = state { i_state = Just $ ist { consChecker = nwc} }
               ch = ConsCheckerChange $ consChecker ist
           processUndoRedoElems actype l nwst (ch : acc) update
        ScriptChange nws : l -> do
           let nwst = state { i_state = Just $ ist { script = nws } }
               ch = ScriptChange $ script ist
           processUndoRedoElems actype l nwst (ch : acc) update
        LoadScriptChange sw : l -> do
           let nwst = state { i_state = Just $ ist { loadScript = sw } }
               ch = LoadScriptChange $ loadScript ist
           processUndoRedoElems actype l nwst (ch : acc) update
        CComorphismChange nwc : l -> do
           let nwst = state { i_state = Just $ ist { cComorphism = nwc} }
               ch = CComorphismChange $ cComorphism ist
           processUndoRedoElems actype l nwst (ch : acc) update
        DgCommandChange nln : l -> do
           nwst <- undoRedoDgCmd actype state nln $ update nln
           let ch = DgCommandChange nln
           processUndoRedoElems actype l nwst (ch : acc) update
        ListChange nls : l -> do
           let (nwels, lc) = processList nls (elements ist) []
               nwst = state { i_state = Just $ ist { elements = nwels } }
               ch = ListChange lc
           processUndoRedoElems actype l nwst (ch : acc) update
        IStateChange nist : l -> do
           let nwst = state { i_state = nist }
               ch = IStateChange $ Just ist
           processUndoRedoElems actype l nwst (ch : acc) update
  
  undoOneStep :: IntState -> IO IntState
  undoOneStep ist = processAny DoUndo ist (\ _ _ _ -> return ())
  
  redoOneStep :: IntState -> IO IntState
  redoOneStep ist = processAny DoRedo ist (\ _ _ _ -> return ())
  
  undoOneStepWithUpdate :: IntState -> (LibName -> [DGChange] -> DGraph -> IO ())
                        -> IO IntState
  undoOneStepWithUpdate = processAny DoUndo
  
  redoOneStepWithUpdate :: IntState -> (LibName -> [DGChange] -> DGraph -> IO ())
                        -> IO IntState
  redoOneStepWithUpdate = processAny DoRedo
  