content: {- |
  Module      :  ./Static/History.hs
  Description :  history treatment for development graphs
  Copyright   :  (c) Christian Maeder, DFKI GmbH 2009
  License     :  GPLv2 or higher, see LICENSE.txt
  Maintainer  :  Christian.Maeder@dfki.de
  Stability   :  provisional
  Portability :  non-portable(Logic)
  
  functions to keep the history entries in sync with the actual graph changes
  -}
  
  module Static.History
    ( groupHistory
    , changeDGH
    , changesDGH
    , updateDGOnly
    , flatHistory
    , negateChange
    , getLastChange
    , reverseHistory
    , splitHistory
    , applyProofHistory
    , undoHistStep
    , redoHistStep
    , undoAllChanges
    , togglePending
    , justTogglePending
    , clearHistory
    ) where
  
  import Static.DevGraph
  import Static.DgUtils
  
  import qualified Common.Lib.SizedList as SizedList
  
  import Data.Graph.Inductive.Graph as Graph
  import Data.List
  
  -- | add a history item to current history.
  addToProofHistoryDG :: HistElem -> DGraph -> DGraph
  addToProofHistoryDG x dg =
    dg { proofHistory = SizedList.cons x $ proofHistory dg }
  
  -- | get the old history and the new offset
  splitHistory :: DGraph -> DGraph -> (ProofHistory, ProofHistory)
  splitHistory oldGraph newGraph = let
    oldHist = proofHistory oldGraph
    newHist = proofHistory newGraph
    diff = SizedList.take (SizedList.size newHist - SizedList.size oldHist)
           newHist
    in (oldHist, diff)
  
  -- | reverse the history list
  reverseHistory :: SizedList.SizedList HistElem -> SizedList.SizedList HistElem
  reverseHistory = SizedList.reverse . SizedList.map
    (\ e -> case e of
       HistElem _ -> e
       HistGroup r l -> HistGroup r $ reverseHistory l)
  
  -- | group pushd changes, leave history of old graph unchanged
  groupHistory :: DGraph -> DGRule -> DGraph -> DGraph
  groupHistory oldGraph rule newGraph = let
    (oldHist, diff) = splitHistory oldGraph newGraph
    in if SizedList.null diff then newGraph else
       newGraph { proofHistory = SizedList.cons (HistGroup rule diff) oldHist }
  
  -- | get most recent step
  getLastHistElem :: DGraph -> HistElem
  getLastHistElem dg = let hist = proofHistory dg in
    if SizedList.null hist then error "Static.DevGraph.getHistElem"
    else SizedList.head hist
  
  -- | get most recent change
  getLastChange :: DGraph -> DGChange
  getLastChange dg = case getLastHistElem dg of
    HistElem c -> c
    HistGroup _ _ -> error "Static.DevGraph.getLastChange"
  
  -- | negate change
  negateChange :: DGChange -> DGChange
  negateChange change = case change of
        InsertNode x -> DeleteNode x
        DeleteNode x -> InsertNode x
        InsertEdge x -> DeleteEdge x
        DeleteEdge x -> InsertEdge x
        SetNodeLab old (node, new) -> SetNodeLab new (node, old)
  
  flatHistory :: SizedList.SizedList HistElem -> [DGChange]
  flatHistory h = if SizedList.null h then [] else
    (case SizedList.head h of
      HistElem c -> [c]
      HistGroup _ l -> flatHistory l) ++ flatHistory (SizedList.tail h)
  
  undoHistStep :: DGraph -> (DGraph, [DGChange])
  undoHistStep dg = let h = proofHistory dg in
    if SizedList.null h then (dg, []) else let
    he = SizedList.head h
    (ndg, cs) = case he of
      HistElem c -> let (dg2, nc) = updateDGOnly dg $ negateChange c in
         (dg2 { proofHistory = SizedList.tail h }, [nc])
      HistGroup _ l -> let
       (dg2, ncs) = mapAccumL (\ g _ -> undoHistStep g)
          dg { proofHistory = SizedList.append l $ SizedList.tail h }
          $ SizedList.toList l
       in (dg2, concat ncs)
    in (ndg { redoHistory = SizedList.cons he $ redoHistory dg }, cs)
  
  undoAllChangesAux :: DGraph -> DGraph
  undoAllChangesAux dg = let h = proofHistory dg in
    if SizedList.null h then dg else undoAllChangesAux $ fst $ undoHistStep dg
  
  undoAllChanges :: DGraph -> DGraph
  undoAllChanges dg = let nDg = undoAllChangesAux dg in
    nDg { getNewEdgeId = incEdgeId $ maximum (startEdgeId
          : map (\ (_, _, l) -> dgl_id l) (labEdgesDG nDg)) }
  
  redoHistStep :: DGraph -> (DGraph, [DGChange])
  redoHistStep dg = let h = redoHistory dg in
    if SizedList.null h then (dg, []) else
        let he = SizedList.head h
            cs = reverse $ flatHistory $ SizedList.singleton he
            (ndg, ncs) = updateDGAndChanges dg cs
        in (ndg { proofHistory = SizedList.cons he $ proofHistory dg
                , redoHistory = SizedList.tail h }, ncs)
  
  -- | apply the reversed changes to the graph and add them to the history
  applyProofHistory :: SizedList.SizedList HistElem -> DGraph -> DGraph
  applyProofHistory l = applyReverseHistory $ reverseHistory l
  
  applyReverseHistory :: SizedList.SizedList HistElem -> DGraph -> DGraph
  applyReverseHistory l dg = if SizedList.null l then dg else
    applyReverseHistory (SizedList.tail l) $ case SizedList.head l of
      HistElem c -> changeDGH dg c
      HistGroup r h -> let dg2 = applyReverseHistory h dg in
        groupHistory dg r dg2
  
  -- | change the given DGraph with a list of changes
  changesDGH :: DGraph -> [DGChange] -> DGraph
  changesDGH = foldl' changeDGH
  
  -- | toggle the pending flag of the input edges
  togglePending :: DGraph -> [LEdge DGLinkLab] -> DGraph
  togglePending dg = changesDGH dg . concatMap
    (\ e@(s, t, l) ->
         [DeleteEdge e, InsertEdge
          (s, t, l { dglPending = not (dglPending l)})])
  
  -- | toggle the pending flag of the input edges (without history change)
  justTogglePending :: DGraph -> [LEdge DGLinkLab] -> DGraph
  justTogglePending = foldl' togglePendFlag
  
  togglePendFlag :: DGraph -> LEdge DGLinkLab -> DGraph
  togglePendFlag dg (v, _, l) = let
    (Just (ins, _, sl, outs), rg) = match v $ dgBody dg
    in dg { dgBody = (ins, v, sl
                     , map (\ (o, t) ->
              if dgl_id o == dgl_id l
              then (o { dglPending = not (dglPending o) }, t)
              else (o, t)) outs) & rg }
  
  -- | forget redo stack
  clearRedo :: DGraph -> DGraph
  clearRedo g = g { redoHistory = SizedList.empty }
  
  -- | forget history
  clearHistory :: DGraph -> DGraph
  clearHistory g = g { proofHistory = SizedList.empty }
  
  -- | change the given DGraph and the history with the given DGChange.
  changeDGH :: DGraph -> DGChange -> DGraph
  changeDGH g c = let (ng, nc) = updateDGOnly g c in
    addToProofHistoryDG (HistElem nc) $ clearRedo ng
  
  -- | change the given DGraph with a list of DGChange
  updateDGAndChanges :: DGraph -> [DGChange] -> (DGraph, [DGChange])
  updateDGAndChanges = mapAccumL updateDGOnly
  
  {- | change the given DGraph with given DGChange and return a new DGraph and
       the processed DGChange as well. -}
  updateDGOnly :: DGraph -> DGChange -> (DGraph, DGChange)
  updateDGOnly g c =
    case c of
      InsertNode n -> (insLNodeDG n g, InsertNode n)
      DeleteNode n@(i, _) -> (delNodeDG i g, DeleteNode n)
      InsertEdge e -> let (newEdge, ng) = insLEdgeDG e g in
        (ng, InsertEdge newEdge)
      DeleteEdge e -> (delLEdgeDG e g, DeleteEdge e)
      SetNodeLab _ n -> let (newG, o) = labelNodeDG n g in
        (newG, SetNodeLab o n)
  