{- |
Module      :  ./Proofs/TriangleCons.hs
Description :  apply triangle-cons rule for all edges in development graphs
Copyright   :  (c) Christian Maeder, DFKI GmbH 2010
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  non-portable(Logic)

-}


module Proofs.TriangleCons where

import Static.DevGraph
import Static.DgUtils
import Static.History

import Common.Consistency
import Common.Result
import Common.LibName

import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.Graph.Inductive.Graph

import Control.Monad

triangleConsRule :: DGRule
triangleConsRule :: DGRule
triangleConsRule = String -> DGRule
DGRule "TriangleCons"

triangleCons :: LibName -> LibEnv -> Result LibEnv
triangleCons :: LibName -> LibEnv -> Result LibEnv
triangleCons ln :: LibName
ln le :: LibEnv
le = do
 let dg :: DGraph
dg = LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln LibEnv
le
 DGraph
newDg <- (DGraph -> LEdge DGLinkLab -> Result DGraph)
-> DGraph -> [LEdge DGLinkLab] -> Result DGraph
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM DGraph -> LEdge DGLinkLab -> Result DGraph
triangleConsDG DGraph
dg ([LEdge DGLinkLab] -> Result DGraph)
-> [LEdge DGLinkLab] -> Result DGraph
forall a b. (a -> b) -> a -> b
$
             (LEdge DGLinkLab -> Bool) -> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (_, _, l :: DGLinkLab
l) -> let e :: DGEdgeType
e = DGLinkLab -> DGEdgeType
getRealDGLinkType DGLinkLab
l in
               DGEdgeType -> DGEdgeTypeModInc
edgeTypeModInc DGEdgeType
e DGEdgeTypeModInc -> DGEdgeTypeModInc -> Bool
forall a. Eq a => a -> a -> Bool
== DGEdgeTypeModInc
GlobalDef
               Bool -> Bool -> Bool
&& DGLinkType -> Conservativity
getCons (DGLinkLab -> DGLinkType
dgl_type DGLinkLab
l) Conservativity -> Conservativity -> Bool
forall a. Eq a => a -> a -> Bool
== Conservativity
Cons
             )
          ([LEdge DGLinkLab] -> [LEdge DGLinkLab])
-> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a b. (a -> b) -> a -> b
$ DGraph -> [LEdge DGLinkLab]
labEdgesDG DGraph
dg
 LibEnv -> Result LibEnv
forall (m :: * -> *) a. Monad m => a -> m a
return (LibEnv -> Result LibEnv) -> LibEnv -> Result LibEnv
forall a b. (a -> b) -> a -> b
$ LibName -> DGraph -> LibEnv -> LibEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert LibName
ln
    (DGraph -> DGRule -> DGraph -> DGraph
groupHistory DGraph
dg DGRule
triangleConsRule DGraph
newDg) LibEnv
le

triangleConsDG :: DGraph -> LEdge DGLinkLab -> Result DGraph
triangleConsDG :: DGraph -> LEdge DGLinkLab -> Result DGraph
triangleConsDG dg :: DGraph
dg (s :: Node
s, t :: Node
t, l :: DGLinkLab
l) = do
 let g :: Gr DGNodeLab DGLinkLab
g = DGraph -> Gr DGNodeLab DGLinkLab
dgBody DGraph
dg
     markCons :: DGLinkLab -> DGLinkLab -> [DGChange]
markCons l1 :: DGLinkLab
l1 l2 :: DGLinkLab
l2 = let
        l' :: DGLinkLab
l' = DGLinkLab
l {dgl_type :: DGLinkType
dgl_type = case DGLinkLab -> DGLinkType
dgl_type DGLinkLab
l of
                           ScopedLink a :: Scope
a b :: LinkKind
b _ ->
                              Scope -> LinkKind -> ConsStatus -> DGLinkType
ScopedLink Scope
a LinkKind
b (ConsStatus -> DGLinkType) -> ConsStatus -> DGLinkType
forall a b. (a -> b) -> a -> b
$
                               Conservativity -> Conservativity -> ThmLinkStatus -> ConsStatus
ConsStatus
                                 Conservativity
Cons
                                 Conservativity
Cons
                                 (ThmLinkStatus -> ConsStatus) -> ThmLinkStatus -> ConsStatus
forall a b. (a -> b) -> a -> b
$ DGRule -> ProofBasis -> ThmLinkStatus
Proven DGRule
triangleConsRule (ProofBasis -> ThmLinkStatus) -> ProofBasis -> ThmLinkStatus
forall a b. (a -> b) -> a -> b
$
                                    Set EdgeId -> ProofBasis
ProofBasis (Set EdgeId -> ProofBasis) -> Set EdgeId -> ProofBasis
forall a b. (a -> b) -> a -> b
$ [EdgeId] -> Set EdgeId
forall a. Ord a => [a] -> Set a
Set.fromList ([EdgeId] -> Set EdgeId) -> [EdgeId] -> Set EdgeId
forall a b. (a -> b) -> a -> b
$
                                     (DGLinkLab -> EdgeId) -> [DGLinkLab] -> [EdgeId]
forall a b. (a -> b) -> [a] -> [b]
map DGLinkLab -> EdgeId
dgl_id [DGLinkLab
l1, DGLinkLab
l2]
                           dt :: DGLinkType
dt -> DGLinkType
dt}
       in [LEdge DGLinkLab -> DGChange
DeleteEdge (Node
s, Node
t, DGLinkLab
l), LEdge DGLinkLab -> DGChange
InsertEdge (Node
s, Node
t, DGLinkLab
l')]
     checkThm :: DGEdgeTypeModInc -> Bool
checkThm eType :: DGEdgeTypeModInc
eType =
       case DGEdgeTypeModInc
eType of
         ThmType (GlobalOrLocalThm _ _) _ _ _ -> Bool
True
         _ -> Bool
False
     oThm :: [LEdge DGLinkLab]
oThm = (LEdge DGLinkLab -> Bool) -> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (_, _, ll :: DGLinkLab
ll) -> let e :: DGEdgeType
e = DGLinkLab -> DGEdgeType
getRealDGLinkType DGLinkLab
ll in
               DGEdgeTypeModInc -> Bool
checkThm (DGEdgeType -> DGEdgeTypeModInc
edgeTypeModInc DGEdgeType
e)
             ) ([LEdge DGLinkLab] -> [LEdge DGLinkLab])
-> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a b. (a -> b) -> a -> b
$ Gr DGNodeLab DGLinkLab -> Node -> [LEdge DGLinkLab]
forall (gr :: * -> * -> *) a b.
Graph gr =>
gr a b -> Node -> [LEdge b]
out Gr DGNodeLab DGLinkLab
g Node
t
 case [LEdge DGLinkLab]
oThm of
   [] -> DGraph -> Result DGraph
forall (m :: * -> *) a. Monad m => a -> m a
return DGraph
dg -- no outgoing thm link found
   _ -> do
    let bases :: [(LEdge DGLinkLab, LEdge DGLinkLab)]
bases = ((LEdge DGLinkLab, LEdge DGLinkLab) -> Bool)
-> [(LEdge DGLinkLab, LEdge DGLinkLab)]
-> [(LEdge DGLinkLab, LEdge DGLinkLab)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ ((s' :: Node
s', _, _), _) -> Node
s Node -> Node -> Bool
forall a. Eq a => a -> a -> Bool
== Node
s')
                ([(LEdge DGLinkLab, LEdge DGLinkLab)]
 -> [(LEdge DGLinkLab, LEdge DGLinkLab)])
-> [(LEdge DGLinkLab, LEdge DGLinkLab)]
-> [(LEdge DGLinkLab, LEdge DGLinkLab)]
forall a b. (a -> b) -> a -> b
$ (LEdge DGLinkLab -> [(LEdge DGLinkLab, LEdge DGLinkLab)])
-> [LEdge DGLinkLab] -> [(LEdge DGLinkLab, LEdge DGLinkLab)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ dge :: LEdge DGLinkLab
dge@(_, tt :: Node
tt, _) ->
                        (LEdge DGLinkLab -> (LEdge DGLinkLab, LEdge DGLinkLab))
-> [LEdge DGLinkLab] -> [(LEdge DGLinkLab, LEdge DGLinkLab)]
forall a b. (a -> b) -> [a] -> [b]
map (\ x :: LEdge DGLinkLab
x -> (LEdge DGLinkLab
x, LEdge DGLinkLab
dge))
                         ([LEdge DGLinkLab] -> [(LEdge DGLinkLab, LEdge DGLinkLab)])
-> [LEdge DGLinkLab] -> [(LEdge DGLinkLab, LEdge DGLinkLab)]
forall a b. (a -> b) -> a -> b
$ (LEdge DGLinkLab -> Bool) -> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (_, _, lx :: DGLinkLab
lx) ->
                             DGLinkType -> Conservativity
getCons (DGLinkLab -> DGLinkType
dgl_type DGLinkLab
lx) Conservativity -> Conservativity -> Bool
forall a. Eq a => a -> a -> Bool
== Conservativity
Cons
                           ) ([LEdge DGLinkLab] -> [LEdge DGLinkLab])
-> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a b. (a -> b) -> a -> b
$ Gr DGNodeLab DGLinkLab -> Node -> [LEdge DGLinkLab]
forall (gr :: * -> * -> *) a b.
Graph gr =>
gr a b -> Node -> [LEdge b]
inn Gr DGNodeLab DGLinkLab
g Node
tt)
                  [LEdge DGLinkLab]
oThm
    case [(LEdge DGLinkLab, LEdge DGLinkLab)]
bases of
      [] -> DGraph -> Result DGraph
forall (m :: * -> *) a. Monad m => a -> m a
return DGraph
dg -- no cons link found
      ((_, _, cl :: DGLinkLab
cl), (_, _, tl :: DGLinkLab
tl)) : _ -> do
        let changes :: [DGChange]
changes = DGLinkLab -> DGLinkLab -> [DGChange]
markCons DGLinkLab
cl DGLinkLab
tl
        DGraph -> Result DGraph
forall (m :: * -> *) a. Monad m => a -> m a
return (DGraph -> Result DGraph) -> DGraph -> Result DGraph
forall a b. (a -> b) -> a -> b
$ DGraph -> [DGChange] -> DGraph
changesDGH DGraph
dg [DGChange]
changes