content: {- |
  Module      :  ./Proofs/StatusUtils.hs
  Description :  the proof status with manipulating functions
  Copyright   :  (c) Jorina F. Gerken, Till Mossakowski, Uni Bremen 2002-2006
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  Christian.Maeder@dfki.de
  Stability   :  provisional
  Portability :  non-portable(Logic)
  
  the proof status with manipulating functions
  -}
  
  module Proofs.StatusUtils
      ( lookupHistory
      , removeContraryChanges
      , isIdentityEdge
      ) where
  
  import Static.DevGraph
  import Data.Graph.Inductive.Graph
  import Common.LibName
  import Logic.Logic
  import qualified Common.Lib.SizedList as SizedList
  
  import Data.List
  
  {-
     proof status = (DG0,[(R1,DG1),...,(Rn,DGn)])
     DG0 is the development graph resulting from the static analysis
     Ri is a list of rules that transforms DGi-1 to DGi
     With the list of intermediate proof states, one can easily implement
      an undo operation
  -}
  
  -- * methods used in several proofs
  
  -- | returns the history that belongs to the given library name
  lookupHistory :: LibName -> LibEnv -> ProofHistory
  lookupHistory ln = clearHist . proofHistory . lookupDGraph ln
  
  -- | clear label lock
  clr :: DGNodeLab -> DGNodeLab
  clr l = l { dgn_lock = Nothing }
  
  clearLock :: DGChange -> DGChange
  clearLock c = case c of
    InsertNode (n, l) -> InsertNode (n, clr l)
    DeleteNode (n, l) -> InsertNode (n, clr l)
    SetNodeLab o (n, l) -> SetNodeLab (clr o) (n, clr l)
    _ -> c
  
  clearHist :: ProofHistory -> ProofHistory
  clearHist = SizedList.map clearElem
  
  clearElem :: HistElem -> HistElem
  clearElem e = case e of
    HistElem c -> HistElem $ clearLock c
    HistGroup r h -> HistGroup r $ clearHist h
  
  -- * methods that keep the change list clean
  
  {- | remove the contray changes out of the list if it's necessary,
  so that the list can stay clean. -}
  removeContraryChanges :: [DGChange] -> [DGChange]
  removeContraryChanges cs = case cs of
    [] -> []
    c1 : r -> let recurse = c1 : removeContraryChanges r in case c1 of
      SetNodeLab oldLbl (n, _) -> let
          (r1, r2) = break (\ c2 -> case c2 of
              SetNodeLab _ (m, _) -> n == m
              DeleteNode (m, _) -> n == m
              _ -> False) r
          in case r2 of
               [] -> recurse
               c2 : r3 -> removeContraryChanges $ r1 ++ case c2 of
                   SetNodeLab _ (_, lbl) -> SetNodeLab oldLbl (n, lbl) : r3
                   DeleteNode _ -> DeleteNode (n, oldLbl) : r3
                   _ -> r2
      InsertNode (n, _) -> let
          (r1, r2) = break (\ c2 -> case c2 of
              DeleteNode (m, _) -> n == m
              _ -> False) r
          (r1a, r1b) = partition (\ c2 -> case c2 of
              SetNodeLab _ (m, _) -> n == m
              _ -> False) r1
          in case r2 of
               [] -> case reverse r1a of
                  SetNodeLab _ (_, lbl) : _ ->
                      InsertNode (n, lbl) : removeContraryChanges r1b
                  _ -> recurse
               _ : r3 -> removeContraryChanges $
                         filter (\ c2 -> case c2 of
                            InsertEdge (s, t, _) -> s /= n && t /= n
                            DeleteEdge (s, t, _) -> s /= n && t /= n
                            _ -> True) r1b ++ r3
      DeleteNode (n, oldLbl) -> let
          (r1, r2) = break (\ c2 -> case c2 of
              InsertNode (m, _) -> n == m
              _ -> False) r
          in case r2 of
               InsertNode (_, lbl) : r3 ->
                 removeContraryChanges $ r1 ++ SetNodeLab oldLbl (n, lbl) : r3
               _ -> recurse
      InsertEdge e1 -> let
          (r1, r2) = break (\ c2 -> case c2 of
              DeleteEdge e2 -> eqDGLEdge e1 e2
              _ -> False) r
          in case r2 of
               [] -> recurse
               _ : r3 -> removeContraryChanges $ r1 ++ r3
      DeleteEdge e1 -> let
          (r1, r2) = break (\ c2 -> case c2 of
              InsertEdge e2 -> eqDGLEdge e1 e2
              _ -> False) r
          in case r2 of
               [] -> recurse
               _ : r3 -> removeContraryChanges $ r1 ++ r3
  
  eqDGLEdge :: LEdge DGLinkLab -> LEdge DGLinkLab -> Bool
  eqDGLEdge (s1, t1, l1) (s2, t2, l2) = (s1, t1) == (s2, t2)
    && eqDGLinkLabContent l1 l2
  
  {- | check if the given edge is an identity edge, namely a loop
       from a node to itself with an identity morphism. -}
  isIdentityEdge :: LEdge DGLinkLab -> LibEnv -> DGraph -> Bool
  isIdentityEdge (src, tgt, edgeLab) ps dgraph =
    let nodeLab = labDG dgraph src
        gsig = dgn_sign nodeLab
        res = src == tgt &&
          dgl_morphism edgeLab == ide gsig
    in if isDGRef nodeLab then -- just a consistency check
      let dg = lookupDGraph (dgn_libname nodeLab) ps
          gsig2 = dgn_sign $ labDG dg $ dgn_node nodeLab
      in if gsig2 == gsig then res else error "isIdentityEdge"
    else res
  