{- |
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 :: LibName -> LibEnv -> ProofHistory
lookupHistory ln :: LibName
ln = ProofHistory -> ProofHistory
clearHist (ProofHistory -> ProofHistory)
-> (LibEnv -> ProofHistory) -> LibEnv -> ProofHistory
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGraph -> ProofHistory
proofHistory (DGraph -> ProofHistory)
-> (LibEnv -> DGraph) -> LibEnv -> ProofHistory
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln

-- | clear label lock
clr :: DGNodeLab -> DGNodeLab
clr :: DGNodeLab -> DGNodeLab
clr l :: DGNodeLab
l = DGNodeLab
l { dgn_lock :: Maybe (MVar ())
dgn_lock = Maybe (MVar ())
forall a. Maybe a
Nothing }

clearLock :: DGChange -> DGChange
clearLock :: DGChange -> DGChange
clearLock c :: DGChange
c = case DGChange
c of
  InsertNode (n :: Node
n, l :: DGNodeLab
l) -> LNode DGNodeLab -> DGChange
InsertNode (Node
n, DGNodeLab -> DGNodeLab
clr DGNodeLab
l)
  DeleteNode (n :: Node
n, l :: DGNodeLab
l) -> LNode DGNodeLab -> DGChange
InsertNode (Node
n, DGNodeLab -> DGNodeLab
clr DGNodeLab
l)
  SetNodeLab o :: DGNodeLab
o (n :: Node
n, l :: DGNodeLab
l) -> DGNodeLab -> LNode DGNodeLab -> DGChange
SetNodeLab (DGNodeLab -> DGNodeLab
clr DGNodeLab
o) (Node
n, DGNodeLab -> DGNodeLab
clr DGNodeLab
l)
  _ -> DGChange
c

clearHist :: ProofHistory -> ProofHistory
clearHist :: ProofHistory -> ProofHistory
clearHist = (HistElem -> HistElem) -> ProofHistory -> ProofHistory
forall a b. (a -> b) -> SizedList a -> SizedList b
SizedList.map HistElem -> HistElem
clearElem

clearElem :: HistElem -> HistElem
clearElem :: HistElem -> HistElem
clearElem e :: HistElem
e = case HistElem
e of
  HistElem c :: DGChange
c -> DGChange -> HistElem
HistElem (DGChange -> HistElem) -> DGChange -> HistElem
forall a b. (a -> b) -> a -> b
$ DGChange -> DGChange
clearLock DGChange
c
  HistGroup r :: DGRule
r h :: ProofHistory
h -> DGRule -> ProofHistory -> HistElem
HistGroup DGRule
r (ProofHistory -> HistElem) -> ProofHistory -> HistElem
forall a b. (a -> b) -> a -> b
$ ProofHistory -> ProofHistory
clearHist ProofHistory
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 :: [DGChange] -> [DGChange]
removeContraryChanges cs :: [DGChange]
cs = case [DGChange]
cs of
  [] -> []
  c1 :: DGChange
c1 : r :: [DGChange]
r -> let recurse :: [DGChange]
recurse = DGChange
c1 DGChange -> [DGChange] -> [DGChange]
forall a. a -> [a] -> [a]
: [DGChange] -> [DGChange]
removeContraryChanges [DGChange]
r in case DGChange
c1 of
    SetNodeLab oldLbl :: DGNodeLab
oldLbl (n :: Node
n, _) -> let
        (r1 :: [DGChange]
r1, r2 :: [DGChange]
r2) = (DGChange -> Bool) -> [DGChange] -> ([DGChange], [DGChange])
forall a. (a -> Bool) -> [a] -> ([a], [a])
break (\ c2 :: DGChange
c2 -> case DGChange
c2 of
            SetNodeLab _ (m :: Node
m, _) -> Node
n Node -> Node -> Bool
forall a. Eq a => a -> a -> Bool
== Node
m
            DeleteNode (m :: Node
m, _) -> Node
n Node -> Node -> Bool
forall a. Eq a => a -> a -> Bool
== Node
m
            _ -> Bool
False) [DGChange]
r
        in case [DGChange]
r2 of
             [] -> [DGChange]
recurse
             c2 :: DGChange
c2 : r3 :: [DGChange]
r3 -> [DGChange] -> [DGChange]
removeContraryChanges ([DGChange] -> [DGChange]) -> [DGChange] -> [DGChange]
forall a b. (a -> b) -> a -> b
$ [DGChange]
r1 [DGChange] -> [DGChange] -> [DGChange]
forall a. [a] -> [a] -> [a]
++ case DGChange
c2 of
                 SetNodeLab _ (_, lbl :: DGNodeLab
lbl) -> DGNodeLab -> LNode DGNodeLab -> DGChange
SetNodeLab DGNodeLab
oldLbl (Node
n, DGNodeLab
lbl) DGChange -> [DGChange] -> [DGChange]
forall a. a -> [a] -> [a]
: [DGChange]
r3
                 DeleteNode _ -> LNode DGNodeLab -> DGChange
DeleteNode (Node
n, DGNodeLab
oldLbl) DGChange -> [DGChange] -> [DGChange]
forall a. a -> [a] -> [a]
: [DGChange]
r3
                 _ -> [DGChange]
r2
    InsertNode (n :: Node
n, _) -> let
        (r1 :: [DGChange]
r1, r2 :: [DGChange]
r2) = (DGChange -> Bool) -> [DGChange] -> ([DGChange], [DGChange])
forall a. (a -> Bool) -> [a] -> ([a], [a])
break (\ c2 :: DGChange
c2 -> case DGChange
c2 of
            DeleteNode (m :: Node
m, _) -> Node
n Node -> Node -> Bool
forall a. Eq a => a -> a -> Bool
== Node
m
            _ -> Bool
False) [DGChange]
r
        (r1a :: [DGChange]
r1a, r1b :: [DGChange]
r1b) = (DGChange -> Bool) -> [DGChange] -> ([DGChange], [DGChange])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (\ c2 :: DGChange
c2 -> case DGChange
c2 of
            SetNodeLab _ (m :: Node
m, _) -> Node
n Node -> Node -> Bool
forall a. Eq a => a -> a -> Bool
== Node
m
            _ -> Bool
False) [DGChange]
r1
        in case [DGChange]
r2 of
             [] -> case [DGChange] -> [DGChange]
forall a. [a] -> [a]
reverse [DGChange]
r1a of
                SetNodeLab _ (_, lbl :: DGNodeLab
lbl) : _ ->
                    LNode DGNodeLab -> DGChange
InsertNode (Node
n, DGNodeLab
lbl) DGChange -> [DGChange] -> [DGChange]
forall a. a -> [a] -> [a]
: [DGChange] -> [DGChange]
removeContraryChanges [DGChange]
r1b
                _ -> [DGChange]
recurse
             _ : r3 :: [DGChange]
r3 -> [DGChange] -> [DGChange]
removeContraryChanges ([DGChange] -> [DGChange]) -> [DGChange] -> [DGChange]
forall a b. (a -> b) -> a -> b
$
                       (DGChange -> Bool) -> [DGChange] -> [DGChange]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ c2 :: DGChange
c2 -> case DGChange
c2 of
                          InsertEdge (s :: Node
s, t :: Node
t, _) -> Node
s Node -> Node -> Bool
forall a. Eq a => a -> a -> Bool
/= Node
n Bool -> Bool -> Bool
&& Node
t Node -> Node -> Bool
forall a. Eq a => a -> a -> Bool
/= Node
n
                          DeleteEdge (s :: Node
s, t :: Node
t, _) -> Node
s Node -> Node -> Bool
forall a. Eq a => a -> a -> Bool
/= Node
n Bool -> Bool -> Bool
&& Node
t Node -> Node -> Bool
forall a. Eq a => a -> a -> Bool
/= Node
n
                          _ -> Bool
True) [DGChange]
r1b [DGChange] -> [DGChange] -> [DGChange]
forall a. [a] -> [a] -> [a]
++ [DGChange]
r3
    DeleteNode (n :: Node
n, oldLbl :: DGNodeLab
oldLbl) -> let
        (r1 :: [DGChange]
r1, r2 :: [DGChange]
r2) = (DGChange -> Bool) -> [DGChange] -> ([DGChange], [DGChange])
forall a. (a -> Bool) -> [a] -> ([a], [a])
break (\ c2 :: DGChange
c2 -> case DGChange
c2 of
            InsertNode (m :: Node
m, _) -> Node
n Node -> Node -> Bool
forall a. Eq a => a -> a -> Bool
== Node
m
            _ -> Bool
False) [DGChange]
r
        in case [DGChange]
r2 of
             InsertNode (_, lbl :: DGNodeLab
lbl) : r3 :: [DGChange]
r3 ->
               [DGChange] -> [DGChange]
removeContraryChanges ([DGChange] -> [DGChange]) -> [DGChange] -> [DGChange]
forall a b. (a -> b) -> a -> b
$ [DGChange]
r1 [DGChange] -> [DGChange] -> [DGChange]
forall a. [a] -> [a] -> [a]
++ DGNodeLab -> LNode DGNodeLab -> DGChange
SetNodeLab DGNodeLab
oldLbl (Node
n, DGNodeLab
lbl) DGChange -> [DGChange] -> [DGChange]
forall a. a -> [a] -> [a]
: [DGChange]
r3
             _ -> [DGChange]
recurse
    InsertEdge e1 :: LEdge DGLinkLab
e1 -> let
        (r1 :: [DGChange]
r1, r2 :: [DGChange]
r2) = (DGChange -> Bool) -> [DGChange] -> ([DGChange], [DGChange])
forall a. (a -> Bool) -> [a] -> ([a], [a])
break (\ c2 :: DGChange
c2 -> case DGChange
c2 of
            DeleteEdge e2 :: LEdge DGLinkLab
e2 -> LEdge DGLinkLab -> LEdge DGLinkLab -> Bool
eqDGLEdge LEdge DGLinkLab
e1 LEdge DGLinkLab
e2
            _ -> Bool
False) [DGChange]
r
        in case [DGChange]
r2 of
             [] -> [DGChange]
recurse
             _ : r3 :: [DGChange]
r3 -> [DGChange] -> [DGChange]
removeContraryChanges ([DGChange] -> [DGChange]) -> [DGChange] -> [DGChange]
forall a b. (a -> b) -> a -> b
$ [DGChange]
r1 [DGChange] -> [DGChange] -> [DGChange]
forall a. [a] -> [a] -> [a]
++ [DGChange]
r3
    DeleteEdge e1 :: LEdge DGLinkLab
e1 -> let
        (r1 :: [DGChange]
r1, r2 :: [DGChange]
r2) = (DGChange -> Bool) -> [DGChange] -> ([DGChange], [DGChange])
forall a. (a -> Bool) -> [a] -> ([a], [a])
break (\ c2 :: DGChange
c2 -> case DGChange
c2 of
            InsertEdge e2 :: LEdge DGLinkLab
e2 -> LEdge DGLinkLab -> LEdge DGLinkLab -> Bool
eqDGLEdge LEdge DGLinkLab
e1 LEdge DGLinkLab
e2
            _ -> Bool
False) [DGChange]
r
        in case [DGChange]
r2 of
             [] -> [DGChange]
recurse
             _ : r3 :: [DGChange]
r3 -> [DGChange] -> [DGChange]
removeContraryChanges ([DGChange] -> [DGChange]) -> [DGChange] -> [DGChange]
forall a b. (a -> b) -> a -> b
$ [DGChange]
r1 [DGChange] -> [DGChange] -> [DGChange]
forall a. [a] -> [a] -> [a]
++ [DGChange]
r3

eqDGLEdge :: LEdge DGLinkLab -> LEdge DGLinkLab -> Bool
eqDGLEdge :: LEdge DGLinkLab -> LEdge DGLinkLab -> Bool
eqDGLEdge (s1 :: Node
s1, t1 :: Node
t1, l1 :: DGLinkLab
l1) (s2 :: Node
s2, t2 :: Node
t2, l2 :: DGLinkLab
l2) = (Node
s1, Node
t1) (Node, Node) -> (Node, Node) -> Bool
forall a. Eq a => a -> a -> Bool
== (Node
s2, Node
t2)
  Bool -> Bool -> Bool
&& DGLinkLab -> DGLinkLab -> Bool
eqDGLinkLabContent DGLinkLab
l1 DGLinkLab
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 :: LEdge DGLinkLab -> LibEnv -> DGraph -> Bool
isIdentityEdge (src :: Node
src, tgt :: Node
tgt, edgeLab :: DGLinkLab
edgeLab) ps :: LibEnv
ps dgraph :: DGraph
dgraph =
  let nodeLab :: DGNodeLab
nodeLab = DGraph -> Node -> DGNodeLab
labDG DGraph
dgraph Node
src
      gsig :: G_sign
gsig = DGNodeLab -> G_sign
dgn_sign DGNodeLab
nodeLab
      res :: Bool
res = Node
src Node -> Node -> Bool
forall a. Eq a => a -> a -> Bool
== Node
tgt Bool -> Bool -> Bool
&&
        DGLinkLab -> GMorphism
dgl_morphism DGLinkLab
edgeLab GMorphism -> GMorphism -> Bool
forall a. Eq a => a -> a -> Bool
== G_sign -> GMorphism
forall object morphism.
Category object morphism =>
object -> morphism
ide G_sign
gsig
  in if DGNodeLab -> Bool
isDGRef DGNodeLab
nodeLab then -- just a consistency check
    let dg :: DGraph
dg = LibName -> LibEnv -> DGraph
lookupDGraph (DGNodeLab -> LibName
dgn_libname DGNodeLab
nodeLab) LibEnv
ps
        gsig2 :: G_sign
gsig2 = DGNodeLab -> G_sign
dgn_sign (DGNodeLab -> G_sign) -> DGNodeLab -> G_sign
forall a b. (a -> b) -> a -> b
$ DGraph -> Node -> DGNodeLab
labDG DGraph
dg (Node -> DGNodeLab) -> Node -> DGNodeLab
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> Node
dgn_node DGNodeLab
nodeLab
    in if G_sign
gsig2 G_sign -> G_sign -> Bool
forall a. Eq a => a -> a -> Bool
== G_sign
gsig then Bool
res else [Char] -> Bool
forall a. HasCallStack => [Char] -> a
error "isIdentityEdge"
  else Bool
res