root/trunk/Interfaces/History.hs @ 11229

{- |
Module      :$Header$
Description : history management functions
Copyright   : uni-bremen and DFKI
License     : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.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
         , add2history
         ) where

import Interfaces.DataTypes
import Common.LibName

import Proofs.AbstractState
import Proofs.EdgeUtils

import Static.DevGraph

import qualified Data.Map as Map
import Data.List

-- | Datatype used to differentiate between the two actions (so that code does
-- not get duplicated
data UndoOrRedo =
   DoUndo
 | DoRedo


-- write2Hist :: IORef IntState -> String -> [UndoRedoElem] -> IO()
-- write2Hist iost name descr
--  = do 
--    ost <- readIORef iost 
--    let nwst = add2history name ost descr
--    writeIORef iost nwst

add2history :: String -> IntState -> [UndoRedoElem] -> IntState
add2history name st descr
 = case undoList $ i_hist st of
    [] ->  let nwEl = Int_CmdHistoryDescription {
                             cmdName = name,
                             cmdDescription = descr }
               hist = i_hist st
           in st{i_hist=hist{ undoList = nwEl:(undoList hist) } }
    h:r ->
      case cmdName h of
       [] -> let nwEl = h { cmdName = name,
                            cmdDescription = descr ++ (cmdDescription h) }
                 hist = i_hist st
             in st{i_hist=hist{ undoList = nwEl:r }}
       _ -> let nwEl = Int_CmdHistoryDescription {
                             cmdName = name,
                             cmdDescription = descr }
                hist = i_hist st
             in st{i_hist=hist{ undoList = nwEl :h:r } }




-- | Undo or redo a command that modified the development graph
undoRedoDgCmd :: UndoOrRedo -> IntState -> LIB_NAME -> IntState
undoRedoDgCmd actionType state ln =
  case i_state state of
    -- should I return an error message??
   Nothing ->  state
   Just dgS ->
     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' = fst $( 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
                                            }
                       }
     in 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' ->
                            case nb' == nb of
                             True ->((Element ps{includedAxioms = nwaxms} nb)
                                     ,[AxiomsChange (includedAxioms ps) nb])
                             False -> (y,[]) ) elems
             nwelems = map (\y -> fst y) nwls
             changesLs = concatMap (\y-> snd y) 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' ->
                            case nb' == nb of
                             True ->((Element ps{selectedGoals = nwgls} nb)
                                     ,[GoalsChange (selectedGoals ps) nb])
                             False ->(y,[])) elems
             nwelems = map (\y -> fst y) nwls
             changeLs = concatMap (\y ->snd y) 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 -> IntState
processAny actype state =
  let hist = 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
  in
   case hist of
    [] -> state
    x:l->
       let
         (nwst,ch) = processUndoRedoElems actype (cmdDescription x) state []
         x' = x { cmdDescription = ch }
         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)
                                        }
                              }
       in nwstate


-- | Process a list of undo or redo changes
processUndoRedoElems :: UndoOrRedo -> [UndoRedoElem] -> IntState
                           -> [UndoRedoElem] ->(IntState,[UndoRedoElem])
processUndoRedoElems actype ls state acc
 = case i_state state of
    Nothing -> (state,[])
    Just ist ->
     case ls of
      [] -> (state,acc)
      (UseThmChange sw):l ->
         let nwst = state {
                      i_state = Just $ ist { useTheorems = sw } }
             ch   = UseThmChange $ useTheorems ist
         in processUndoRedoElems actype l nwst (ch:acc)
      (Save2FileChange sw):l ->
         let nwst = state {
                      i_state = Just $ ist { save2file = sw }  }
             ch   = Save2FileChange $ save2file ist
         in processUndoRedoElems actype l nwst (ch:acc)
      (ProverChange nwp):l ->
         let nwst = state {
                      i_state = Just $ ist { prover = nwp } }
             ch   = ProverChange $ prover ist
         in processUndoRedoElems actype l nwst (ch:acc)
      (ConsCheckerChange nwc):l ->
         let nwst = state {
                      i_state = Just $ ist { consChecker = nwc} }
             ch   = ConsCheckerChange $ consChecker ist
         in processUndoRedoElems actype l nwst (ch:acc)
      (ScriptChange nws):l ->
         let nwst = state {
                      i_state = Just $ ist { script = nws } }
             ch   = ScriptChange $ script ist
         in processUndoRedoElems actype l nwst (ch:acc)
      (LoadScriptChange sw):l ->
         let nwst = state {
                      i_state = Just $ ist { loadScript = sw } }
             ch   = LoadScriptChange $ loadScript ist
         in processUndoRedoElems actype l nwst (ch:acc)
      (CComorphismChange nwc):l ->
         let nwst = state {
                      i_state = Just $ ist { cComorphism = nwc} }
             ch   = CComorphismChange $ cComorphism ist
         in processUndoRedoElems actype l nwst (ch:acc)
      (DgCommandChange nln):l ->
         let nwst = undoRedoDgCmd actype state nln
             ch   = DgCommandChange nln
         in processUndoRedoElems actype l nwst (ch:acc)
      (ListChange nls):l ->
         let (nwels,lc) = processList nls (elements ist) []
             nwst = state {
                     i_state = Just $ ist { elements = nwels } }
             ch   = ListChange lc
         in processUndoRedoElems actype l nwst (ch:acc)
      (IStateChange nist):l ->
         let nwst = state { i_state = nist }
             ch   = IStateChange $ Just ist
         in processUndoRedoElems actype l nwst (ch:acc)


undoOneStep :: IntState -> IntState
undoOneStep = processAny DoUndo


redoOneStep :: IntState -> IntState
redoOneStep = processAny DoRedo