```{- |
Module      :  ./Proofs/Conservativity.hs
Description :  conservativity proof rule for development graphs
Copyright   :  (c) Markus Gross, DFKI 2009
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  mgross@informatik.uni-bremen.de
Stability   :  provisional
Portability :  non-portable(Logic)

conservativity proof rule for development graphs
Follows Sect. IV:4.4.2 of the CASL Reference Manual.
-}

module Proofs.Conservativity (conservativity) where

import Common.Amalgamate (Amalgamates (Amalgamates), CASLAmalgOpt (..))
import Common.Consistency
import Common.LibName (LibName)
import Common.Result (resultToMaybe)
import Common.Utils (nubOrdOn)

import Proofs.EdgeUtils (getAllPathsOfTypeFrom)
import Proofs.ComputeColimit (makeDiagram)

import Static.DevGraph
import Static.DgUtils
import Static.GTheory (gEnsuresAmalgamability)
import Static.History

import Data.Graph.Inductive.Graph (LEdge, LNode)
import qualified Data.Map as Map

-- * Conservativity rules

{- A pair is defined as:

(e1, e2)

n ---- e2 ----> n
|
|
e1
|
|
v
n

-}
type Pair = (LEdge DGLinkLab, LEdge DGLinkLab)

{- A quad is defined as:

((e1, e2), (e3, e4))

n ---- e2 ----> n
|               |
|               |
e1              e4
|               |
|               |
v               v
n ---- e3 ----> n

-}
type Quad = (Pair, Pair)

-- Main function, calls all rules.
conservativity :: LibName -> LibEnv -> LibEnv
conservativity :: LibName -> LibEnv -> LibEnv
conservativity = (DGraph -> DGraph) -> LibName -> LibEnv -> LibEnv
forall k a. Ord k => (a -> a) -> k -> Map k a -> Map k a
Map.adjust (DGraph -> DGraph
shift (DGraph -> DGraph) -> (DGraph -> DGraph) -> DGraph -> DGraph
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGraph -> DGraph
freeIsMono (DGraph -> DGraph) -> (DGraph -> DGraph) -> DGraph -> DGraph
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGraph -> DGraph
monoIsFree (DGraph -> DGraph) -> (DGraph -> DGraph) -> DGraph -> DGraph
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGraph -> DGraph
compCons)

{- Shift-Rule.
First a list of edge pairs with the same source node is generated.
Then all pairs are positioned correctly. All pairs which have
one edge with a cons value are kept.
A list of quads (pair, pair) is generated. Each input pair is combined with
another pair, which has the same target and where the edges have the same
source nodes. (See type Quad for a picture.)
The target node of the quads must be isolated and the quad has to be
amalgamable.
Afterwards the quad is positioned correctly and the edges are updated. -}
shift :: DGraph -> DGraph
shift :: DGraph -> DGraph
shift dg :: DGraph
dg = DGraph -> DGRule -> DGraph -> DGraph
groupHistory DGraph
dg (String -> DGRule
DGRule "conservativityShift") (DGraph -> DGraph) -> DGraph -> DGraph
forall a b. (a -> b) -> a -> b
\$
DGraph -> [DGChange] -> DGraph
changesDGH DGraph
dg [DGChange]
changes
where
edgs :: [LEdge DGLinkLab]
edgs = (LEdge DGLinkLab -> Bool) -> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a. (a -> Bool) -> [a] -> [a]
filter ((DGLinkType -> Bool) -> LEdge DGLinkLab -> Bool
forall a. (DGLinkType -> a) -> LEdge DGLinkLab -> a
liftE DGLinkType -> Bool
forall a b. (a -> b) -> a -> b
\$ DGraph -> [LEdge DGLinkLab]
labEdgesDG DGraph
dg
globThmEdges :: [LEdge DGLinkLab]
globThmEdges = (LEdge DGLinkLab -> Bool) -> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a. (a -> Bool) -> [a] -> [a]
filter ((DGLinkType -> Bool) -> LEdge DGLinkLab -> Bool
forall a. (DGLinkType -> a) -> LEdge DGLinkLab -> a
liftE DGLinkType -> Bool
edgs
consEdgs :: [LEdge DGLinkLab]
consEdgs = [ LEdge DGLinkLab
e | LEdge DGLinkLab
e <- [LEdge DGLinkLab]
globThmEdges, LEdge DGLinkLab -> Conservativity
e Conservativity -> Conservativity -> Bool
forall a. Ord a => a -> a -> Bool
> Conservativity
None ]
pairs1 :: [Pair]
pairs1 = (Pair -> ((Int, Int, EdgeId), (Int, Int, EdgeId)))
-> [Pair] -> [Pair]
forall b a. Ord b => (a -> b) -> [a] -> [a]
nubOrdOn Pair -> ((Int, Int, EdgeId), (Int, Int, EdgeId))
pairInd
e2)
| e1 :: LEdge DGLinkLab
e1@(s1 :: Int
s1, t1 :: Int
t1, _) <- [LEdge DGLinkLab]
consEdgs
, e2 :: LEdge DGLinkLab
e2@(s2 :: Int
s2, t2 :: Int
t2, _) <- [LEdge DGLinkLab]
globThmEdges
, Int
s1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
s2, Int
t1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
s1, Int
t2 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
s2, Bool -> Bool
not (LEdge DGLinkLab -> LEdge DGLinkLab -> Bool
e2) ]
pairs2 :: [Pair]
pairs2 = (Pair -> ((Int, Int, EdgeId), (Int, Int, EdgeId)))
-> [Pair] -> [Pair]
forall b a. Ord b => (a -> b) -> [a] -> [a]
nubOrdOn Pair -> ((Int, Int, EdgeId), (Int, Int, EdgeId))
pairInd
e4)
| e3 :: LEdge DGLinkLab
e3@(_, t3 :: Int
t3, _) <- [LEdge DGLinkLab]
edgs
, e4 :: LEdge DGLinkLab
e4@(_, t4 :: Int
t4, _) <- [LEdge DGLinkLab]
edgs
, Int
t3 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
t4, Bool -> Bool
not (LEdge DGLinkLab -> LEdge DGLinkLab -> Bool
e4) ]
forall a. (a -> Bool) -> [a] -> [a]
filter (DGraph -> Quad -> Bool
isAmalgamable DGraph
forall a b. (a -> b) -> a -> b
\$
forall a. (a -> Bool) -> [a] -> [a]
filter ([LEdge DGLinkLab] -> Pair -> Bool
edgs (Pair -> Bool) -> (Quad -> Pair) -> Quad -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Quad -> Pair
forall a b. (a, b) -> b
forall a b. (a -> b) -> a -> b
forall a b. (a -> b) -> [a] -> [b]
e4))
| (e1 :: LEdge DGLinkLab
e1@(_, t1 :: Int
t1, _), e2 :: LEdge DGLinkLab
e2@(_, t2 :: Int
t2, _)) <- [Pair]
pairs1
, (e3 :: LEdge DGLinkLab
e3@(s3 :: Int
s3, _, _), e4 :: LEdge DGLinkLab
e4@(s4 :: Int
s4, _, _)) <- [Pair]
pairs2
, Int
t1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
s3 Bool -> Bool -> Bool
&& Int
t2 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
s4 Bool -> Bool -> Bool
|| Int
t1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
s4 Bool -> Bool -> Bool
&& Int
t2 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
s3 ]
changes :: [DGChange]
changes = (Quad -> [DGChange]) -> [Quad] -> [DGChange]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Quad -> [DGChange]
{- Updates the e4 edge with the cons value from the e1 edge.
The quads have to be positioned correctly before using this function. -}
process :: Quad -> [DGChange]
process :: Quad -> [DGChange]
process ((e1 :: LEdge DGLinkLab
e1, _), (_, e4 :: LEdge DGLinkLab
e4)) =
let cons :: Conservativity
cons = LEdge DGLinkLab -> Conservativity
e1
in (ConsStatus -> ConsStatus) -> LEdge DGLinkLab -> [DGChange]
genEdgeChange
(\ (ConsStatus co :: Conservativity
co pc :: Conservativity
pc tl :: ThmLinkStatus
tl) -> Conservativity -> Conservativity -> ThmLinkStatus -> ConsStatus
ConsStatus (Conservativity -> Conservativity -> Conservativity
forall a. Ord a => a -> a -> a
max Conservativity
cons Conservativity
co) Conservativity
e4

-- Checks if a quad is amalgamable.
isAmalgamable :: DGraph -> Quad -> Bool
isAmalgamable :: DGraph -> Quad -> Bool
isAmalgamable dg :: DGraph
dg ((e1 :: LEdge DGLinkLab
e1@(s1 :: Int
s1, _, _), e2 :: LEdge DGLinkLab
e2), (e3 :: LEdge DGLinkLab
e3@(s3 :: Int
s3, _, l3 :: DGLinkLab
l3), e4 :: LEdge DGLinkLab
e4@(s4 :: Int
s4, t4 :: Int
t4, l4 :: DGLinkLab
l4))) =
case Result Amalgamates -> Maybe Amalgamates
forall a. Result a -> Maybe a
resultToMaybe Result Amalgamates
amal of
Just Amalgamates -> Bool
True
_ -> Bool
False
where
sink :: [(Int, GMorphism)]
sink = [(Int
s3, DGLinkLab -> GMorphism
l3), (Int
s4, DGLinkLab -> GMorphism
l4)]
diag :: GDiagram
diag = DGraph -> [Int] -> [LEdge DGLinkLab] -> GDiagram
makeDiagram DGraph
dg [Int
s1, Int
s3, Int
s4, Int
e4]
amal :: Result Amalgamates
amal = [CASLAmalgOpt]
-> GDiagram -> [(Int, GMorphism)] -> Result Amalgamates
gEnsuresAmalgamability [CASLAmalgOpt
ColimitThinness, CASLAmalgOpt
Cell] GDiagram
diag [(Int, GMorphism)]
sink

-- | Checks whether a pair is duplicate (disregarding pair order).
pairInd :: Pair -> ((Int, Int, EdgeId), (Int, Int, EdgeId))
pairInd :: Pair -> ((Int, Int, EdgeId), (Int, Int, EdgeId))
pairInd ((s1 :: Int
s1, t1 :: Int
t1, l1 :: DGLinkLab
l1), (s2 :: Int
s2, t2 :: Int
t2, l2 :: DGLinkLab
l2)) =
let e1 :: (Int, Int, EdgeId)
e1 = (Int
s1, Int
t1, DGLinkLab -> EdgeId
l1)
e2 :: (Int, Int, EdgeId)
e2 = (Int
s2, Int
t2, DGLinkLab -> EdgeId
l2)
in if (Int, Int, EdgeId)
e1 (Int, Int, EdgeId) -> (Int, Int, EdgeId) -> Bool
forall a. Ord a => a -> a -> Bool
< (Int, Int, EdgeId)
e2 then ((Int, Int, EdgeId)
e1, (Int, Int, EdgeId)
e2) else ((Int, Int, EdgeId)
e2, (Int, Int, EdgeId)
e1)

eqDGLEdge :: LEdge DGLinkLab -> LEdge DGLinkLab -> Bool
eqDGLEdge :: LEdge DGLinkLab -> LEdge DGLinkLab -> Bool
eqDGLEdge (s1 :: Int
s1, t1 :: Int
t1, l1 :: DGLinkLab
l1) (s2 :: Int
s2, t2 :: Int
t2, l2 :: DGLinkLab
l2) = (Int
s1, Int
t1) (Int, Int) -> (Int, Int) -> Bool
forall a. Eq a => a -> a -> Bool
== (Int
s2, Int
t2)
Bool -> Bool -> Bool
l2

{- Positions a quad so that the e4 edge is the one whose source node is the
target node of e2. Also checks if the e4 has no conservativity value. -}
q@((e1 :: LEdge DGLinkLab
e1@(_, t1 :: Int
t1, _), e2 :: LEdge DGLinkLab
e2@(_, t2 :: Int
t2, _)), (e3 :: LEdge DGLinkLab
e3@(s3 :: Int
s3, _, _), e4 :: LEdge DGLinkLab
e4))
| Int
s3 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
q
| Int
s3 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
t2 = ((LEdge DGLinkLab
e3))
| Bool
otherwise = String -> Quad
forall a. HasCallStack => String -> a

{- Checks wether the node of the pair is isolated.
Both edges of the pair have the same target node. -}
isolated :: [LEdge DGLinkLab] -> Pair -> Bool
isolated :: [LEdge DGLinkLab] -> Pair -> Bool
isolated edgs :: [LEdge DGLinkLab]
edgs (e1 :: LEdge DGLinkLab
e1@(_, t1 :: Int
t1, _), e2 :: LEdge DGLinkLab
e2) =
Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
\$ (LEdge DGLinkLab -> Bool) -> [LEdge DGLinkLab] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\ x :: LEdge DGLinkLab
x@(_, t :: Int
t, _) -> Int
t Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
t1 Bool -> Bool -> Bool
&& Bool -> Bool
not (LEdge DGLinkLab -> LEdge DGLinkLab -> Bool
e1)
Bool -> Bool -> Bool
&& Bool -> Bool
not (LEdge DGLinkLab -> LEdge DGLinkLab -> Bool
e2)) ([LEdge DGLinkLab] -> Bool) -> [LEdge DGLinkLab] -> Bool
forall a b. (a -> b) -> a -> b
\$ (LEdge DGLinkLab -> Bool) -> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a. (a -> Bool) -> [a] -> [a]
filter ((DGLinkType -> Bool) -> LEdge DGLinkLab -> Bool
forall a. (DGLinkType -> a) -> LEdge DGLinkLab -> a
liftE DGLinkType -> Bool
edgs

{- First get all free links in the graph. Then all cons links.
When the free and cons link point to the same node, the cons link is upgraded
to mono. -}
freeIsMono :: DGraph -> DGraph
freeIsMono :: DGraph -> DGraph
freeIsMono dg :: DGraph
dg = DGraph -> DGRule -> DGraph -> DGraph
groupHistory DGraph
dg (String -> DGRule
DGRule "freeIsMono") (DGraph -> DGraph) -> DGraph -> DGraph
forall a b. (a -> b) -> a -> b
\$ DGraph -> [DGChange] -> DGraph
changesDGH DGraph
dg [DGChange]
changes
where
edgs :: [LEdge DGLinkLab]
edgs = DGraph -> [LEdge DGLinkLab]
labEdgesDG DGraph
dg
free :: [LEdge DGLinkLab]
free = (LEdge DGLinkLab -> Bool) -> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a. (a -> Bool) -> [a] -> [a]
filter ((DGLinkType -> Bool) -> LEdge DGLinkLab -> Bool
forall a. (DGLinkType -> a) -> LEdge DGLinkLab -> a
liftE DGLinkType -> Bool
edgs
cons :: [LEdge DGLinkLab]
cons = [ LEdge DGLinkLab
e | LEdge DGLinkLab
e <- [LEdge DGLinkLab]
edgs, (DGLinkType -> Bool) -> LEdge DGLinkLab -> Bool
forall a. (DGLinkType -> a) -> LEdge DGLinkLab -> a
liftE DGLinkType -> Bool
e, LEdge DGLinkLab -> Conservativity
e Conservativity -> Conservativity -> Bool
forall a. Eq a => a -> a -> Bool
== Conservativity
Cons ]
mono :: [LEdge DGLinkLab]
mono = (LEdge DGLinkLab -> (Int, Int, EdgeId))
forall b a. Ord b => (a -> b) -> [a] -> [a]
nubOrdOn (\ (s :: Int
s, t :: Int
t, l :: DGLinkLab
l) -> (Int
s, Int
t, DGLinkLab -> EdgeId
l))
c | c :: LEdge DGLinkLab
c@(_, ct :: Int
ct, _) <- [LEdge DGLinkLab]
cons, (_, ft :: Int
ft, _) <- [LEdge DGLinkLab]
free, Int
ct Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ft ]
changes :: [DGChange]
changes = (LEdge DGLinkLab -> [DGChange]) -> [LEdge DGLinkLab] -> [DGChange]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((ConsStatus -> ConsStatus) -> LEdge DGLinkLab -> [DGChange]
genEdgeChange
(\ (ConsStatus _ pc :: Conservativity
pc tl :: ThmLinkStatus
tl) -> Conservativity -> Conservativity -> ThmLinkStatus -> ConsStatus
ConsStatus Conservativity
Mono Conservativity
mono

-- Generates a list of changes for the development graph.
genEdgeChange :: (ConsStatus -> ConsStatus) -> LEdge DGLinkLab -> [DGChange]
genEdgeChange :: (ConsStatus -> ConsStatus) -> LEdge DGLinkLab -> [DGChange]
genEdgeChange f :: ConsStatus -> ConsStatus
f e :: LEdge DGLinkLab
e = [ LEdge DGLinkLab -> DGChange
e, LEdge DGLinkLab -> DGChange
InsertEdge (LEdge DGLinkLab -> DGChange) -> LEdge DGLinkLab -> DGChange
forall a b. (a -> b) -> a -> b
\$ LEdge DGLinkLab -> (ConsStatus -> ConsStatus) -> LEdge DGLinkLab
e ConsStatus -> ConsStatus
f ]

-- Modifies the ConsStatus of an edge.
modifyEdgeCons :: LEdge DGLinkLab
-> (ConsStatus -> ConsStatus) -> LEdge DGLinkLab
modifyEdgeCons :: LEdge DGLinkLab -> (ConsStatus -> ConsStatus) -> LEdge DGLinkLab
modifyEdgeCons (s :: Int
s, t :: Int
t, l :: DGLinkLab
l) f :: ConsStatus -> ConsStatus
f =
(Int
s, Int
l {
l of
ScopedLink sc :: Scope
sc dl :: LinkKind
dl cs :: ConsStatus
cs -> Scope -> LinkKind -> ConsStatus -> DGLinkType
dl (ConsStatus -> DGLinkType) -> ConsStatus -> DGLinkType
forall a b. (a -> b) -> a -> b
\$ ConsStatus -> ConsStatus
f ConsStatus
cs
tp
, dgl_origin :: DGLinkOrigin
, dgl_id :: EdgeId
dgl_id = EdgeId
defaultEdgeId
})

monoIsFree :: DGraph -> DGraph
monoIsFree :: DGraph -> DGraph
monoIsFree dg :: DGraph
dg = DGraph -> DGRule -> DGraph -> DGraph
groupHistory DGraph
dg (String -> DGRule
DGRule "monoIsFree") (DGraph -> DGraph) -> DGraph -> DGraph
forall a b. (a -> b) -> a -> b
\$ DGraph -> [DGChange] -> DGraph
changesDGH DGraph
dg [DGChange]
changes
where
mono :: [LNode DGNodeLab]
mono = (LNode DGNodeLab -> Bool) -> [LNode DGNodeLab] -> [LNode DGNodeLab]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ n :: LNode DGNodeLab
n -> LNode DGNodeLab -> Conservativity
getNodeConservativity LNode DGNodeLab
n Conservativity -> Conservativity -> Bool
forall a. Eq a => a -> a -> Bool
== Conservativity
Mono) ([LNode DGNodeLab] -> [LNode DGNodeLab])
-> [LNode DGNodeLab] -> [LNode DGNodeLab]
forall a b. (a -> b) -> a -> b
\$ DGraph -> [LNode DGNodeLab]
labNodesDG DGraph
dg
thmEdges :: [LEdge DGLinkLab]
thmEdges = (LEdge DGLinkLab -> Bool) -> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ e :: LEdge DGLinkLab
e -> LEdge DGLinkLab -> Conservativity
e Conservativity -> Conservativity -> Bool
forall a. Eq a => a -> a -> Bool
== Conservativity
forall a b. (a -> b) -> a -> b
\$
(LEdge DGLinkLab -> Bool) -> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a. (a -> Bool) -> [a] -> [a]
filter ((DGLinkType -> Bool) -> LEdge DGLinkLab -> Bool
forall a. (DGLinkType -> a) -> LEdge DGLinkLab -> a
liftE DGLinkType -> Bool
forall a b. (a -> b) -> a -> b
\$ DGraph -> [LEdge DGLinkLab]
labEdgesDG DGraph
dg
freeEdges :: [LEdge DGLinkLab]
freeEdges = [ LEdge DGLinkLab
e | (n :: Int
n, _) <- [LNode DGNodeLab]
mono, e :: LEdge DGLinkLab
e@(s :: Int
s, _, _) <- [LEdge DGLinkLab]
thmEdges, Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
s ]
changes :: [DGChange]
changes = (LEdge DGLinkLab -> [DGChange]) -> [LEdge DGLinkLab] -> [DGChange]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap LEdge DGLinkLab -> [DGChange]
freeEdges
process :: LEdge DGLinkLab -> [DGChange]
process :: LEdge DGLinkLab -> [DGChange]
process e :: LEdge DGLinkLab
e@(s :: Int
s, t :: Int
t, l :: DGLinkLab
l) = [ LEdge DGLinkLab -> DGChange
e, LEdge DGLinkLab -> DGChange
InsertEdge (Int
s, Int
l {
l of
ScopedLink _ _ (ConsStatus _ _ ls :: ThmLinkStatus
ls) -> Maybe FreeOrCofree
-> Int -> GMorphism -> ThmLinkStatus -> DGLinkType
HidingFreeOrCofreeThm
(FreeOrCofree -> Maybe FreeOrCofree
forall a. a -> Maybe a
Just FreeOrCofree
Free) Int
s
ls
tp
})]

-- If Node n is cons and the path to Node m is also cons then m is cons too.
compCons :: DGraph -> DGraph
compCons :: DGraph -> DGraph
compCons dg :: DGraph
dg = DGraph -> DGRule -> DGraph -> DGraph
groupHistory DGraph
dg (String -> DGRule
DGRule "compCons") (DGraph -> DGraph) -> DGraph -> DGraph
forall a b. (a -> b) -> a -> b
\$ DGraph -> [DGChange] -> DGraph
changesDGH DGraph
dg [DGChange]
changes
where
consNodes :: [LNode DGNodeLab]
consNodes = (LNode DGNodeLab -> Bool) -> [LNode DGNodeLab] -> [LNode DGNodeLab]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ n :: LNode DGNodeLab
n -> LNode DGNodeLab -> Conservativity
getNodeConservativity LNode DGNodeLab
n Conservativity -> Conservativity -> Bool
forall a. Eq a => a -> a -> Bool
/= Conservativity
None) ([LNode DGNodeLab] -> [LNode DGNodeLab])
-> [LNode DGNodeLab] -> [LNode DGNodeLab]
forall a b. (a -> b) -> a -> b
\$ DGraph -> [LNode DGNodeLab]
labNodesDG DGraph
dg
changes :: [DGChange]
changes = (LNode DGNodeLab -> [DGChange]) -> [LNode DGNodeLab] -> [DGChange]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (DGraph -> LNode DGNodeLab -> [DGChange]
compConsAux DGraph
dg) [LNode DGNodeLab]
consNodes

{- First get all paths. Check if the path cons matches with the node cons.
If the target node cons is weaker than the path cons replace it. -}
compConsAux :: DGraph -> LNode DGNodeLab -> [DGChange]
compConsAux :: DGraph -> LNode DGNodeLab -> [DGChange]
compConsAux dg :: DGraph
dg n :: LNode DGNodeLab
n@(i :: Int
i, _) = [DGChange]
changes
where
nodeCons :: Conservativity
nodeCons = LNode DGNodeLab -> Conservativity
getNodeConservativity LNode DGNodeLab
n
nodePaths :: [[LEdge DGLinkLab]]
nodePaths = DGraph -> Int -> [[LEdge DGLinkLab]]
getAllPathsOfTypeFrom DGraph
dg Int
i
consPaths :: [([LEdge DGLinkLab], Conservativity)]
consPaths = (([LEdge DGLinkLab], Conservativity) -> Bool)
-> [([LEdge DGLinkLab], Conservativity)]
-> [([LEdge DGLinkLab], Conservativity)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ p :: ([LEdge DGLinkLab], Conservativity)
p -> ([LEdge DGLinkLab], Conservativity) -> Conservativity
forall a b. (a, b) -> b
snd ([LEdge DGLinkLab], Conservativity)
p Conservativity -> Conservativity -> Bool
forall a. Eq a => a -> a -> Bool
== Conservativity
nodeCons) ([([LEdge DGLinkLab], Conservativity)]
-> [([LEdge DGLinkLab], Conservativity)])
-> [([LEdge DGLinkLab], Conservativity)]
-> [([LEdge DGLinkLab], Conservativity)]
forall a b. (a -> b) -> a -> b
-> [Conservativity] -> [([LEdge DGLinkLab], Conservativity)]
forall a b. [a] -> [b] -> [(a, b)]
nodePaths
(([LEdge DGLinkLab] -> Conservativity)
-> [[LEdge DGLinkLab]] -> [Conservativity]
forall a b. (a -> b) -> [a] -> [b]
map [LEdge DGLinkLab] -> Conservativity
nodePaths)
changes :: [DGChange]
changes = (([LEdge DGLinkLab], Conservativity) -> [DGChange])
-> [([LEdge DGLinkLab], Conservativity)] -> [DGChange]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([LEdge DGLinkLab], Conservativity) -> [DGChange]
process [([LEdge DGLinkLab], Conservativity)]
consPaths
process :: ([LEdge DGLinkLab], Conservativity) -> [DGChange]
process :: ([LEdge DGLinkLab], Conservativity) -> [DGChange]
process (path :: [LEdge DGLinkLab]
path, sourceCons :: Conservativity
sourceCons) =
[ DGNodeLab -> LNode DGNodeLab -> DGChange
SetNodeLab DGNodeLab
lab (Int
node, DGNodeLab
lab') | Conservativity
targetNodeCons Conservativity -> Conservativity -> Bool
forall a. Ord a => a -> a -> Bool
< Conservativity
sourceCons ]
where
(_, node :: Int
node, _) = [LEdge DGLinkLab] -> LEdge DGLinkLab
forall a. [a] -> a
path
lab :: DGNodeLab
lab = DGraph -> Int -> DGNodeLab
labDG DGraph
dg Int
node
targetNodeCons :: Conservativity
targetNodeCons = DGNodeLab -> Conservativity
getNodeCons DGNodeLab
lab
nInfo :: DGNodeInfo
nInfo = DGNodeLab -> DGNodeInfo
nodeInfo DGNodeLab
lab
lab' :: DGNodeLab
lab' = DGNodeLab
lab {
nodeInfo :: DGNodeInfo
nodeInfo = DGNodeInfo
nInfo { node_cons_status :: ConsStatus
node_cons_status = Conservativity -> ConsStatus
mkConsStatus Conservativity
sourceCons }
}
```