{- |
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
isGlobalEdge) ([LEdge DGLinkLab] -> [LEdge DGLinkLab])
-> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
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
isGlobalThm) [LEdge DGLinkLab]
edgs
    consEdgs :: [LEdge DGLinkLab]
consEdgs = [ LEdge DGLinkLab
e | LEdge DGLinkLab
e <- [LEdge DGLinkLab]
globThmEdges, LEdge DGLinkLab -> Conservativity
getConservativity LEdge DGLinkLab
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
      [ (LEdge DGLinkLab
e1, LEdge DGLinkLab
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
eqDGLEdge LEdge DGLinkLab
e1 LEdge DGLinkLab
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
      [ (LEdge DGLinkLab
e3, LEdge DGLinkLab
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
eqDGLEdge LEdge DGLinkLab
e3 LEdge DGLinkLab
e4) ]
    quads :: [Quad]
quads = (Quad -> Bool) -> [Quad] -> [Quad]
forall a. (a -> Bool) -> [a] -> [a]
filter (DGraph -> Quad -> Bool
isAmalgamable DGraph
dg) ([Quad] -> [Quad]) -> [Quad] -> [Quad]
forall a b. (a -> b) -> a -> b
$
            (Quad -> Bool) -> [Quad] -> [Quad]
forall a. (a -> Bool) -> [a] -> [a]
filter ([LEdge DGLinkLab] -> Pair -> Bool
isolated [LEdge DGLinkLab]
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
snd) ([Quad] -> [Quad]) -> [Quad] -> [Quad]
forall a b. (a -> b) -> a -> b
$ (Quad -> Quad) -> [Quad] -> [Quad]
forall a b. (a -> b) -> [a] -> [b]
map Quad -> Quad
posQuad
      [ ((LEdge DGLinkLab
e1, LEdge DGLinkLab
e2), (LEdge DGLinkLab
e3, LEdge DGLinkLab
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]
process [Quad]
quads
    {- 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
getConservativity LEdge DGLinkLab
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
pc ThmLinkStatus
tl) LEdge DGLinkLab
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
dgl_morphism DGLinkLab
l3), (Int
s4, DGLinkLab -> GMorphism
dgl_morphism DGLinkLab
l4)]
    diag :: GDiagram
diag = DGraph -> [Int] -> [LEdge DGLinkLab] -> GDiagram
makeDiagram DGraph
dg [Int
s1, Int
s3, Int
s4, Int
t4] [LEdge DGLinkLab
e1, LEdge DGLinkLab
e2, LEdge DGLinkLab
e3, LEdge DGLinkLab
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
dgl_id DGLinkLab
l1)
      e2 :: (Int, Int, EdgeId)
e2 = (Int
s2, Int
t2, DGLinkLab -> EdgeId
dgl_id DGLinkLab
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
&& DGLinkLab -> DGLinkLab -> Bool
eqDGLinkLabById DGLinkLab
l1 DGLinkLab
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. -}
posQuad :: Quad -> Quad
posQuad :: Quad -> Quad
posQuad q :: Quad
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
t1 = Quad
q
  | Int
s3 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
t2 = ((LEdge DGLinkLab
e1, LEdge DGLinkLab
e2), (LEdge DGLinkLab
e4, LEdge DGLinkLab
e3))
  | Bool
otherwise = String -> Quad
forall a. HasCallStack => String -> a
error "Proofs.Conservativity.posQuad"

{- 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
eqDGLEdge LEdge DGLinkLab
x LEdge DGLinkLab
e1)
             Bool -> Bool -> Bool
&& Bool -> Bool
not (LEdge DGLinkLab -> LEdge DGLinkLab -> Bool
eqDGLEdge LEdge DGLinkLab
x LEdge DGLinkLab
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
isGlobalDef) [LEdge DGLinkLab]
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
isFreeEdge) [LEdge DGLinkLab]
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
isGlobalThm LEdge DGLinkLab
e, LEdge DGLinkLab -> Conservativity
getConservativity LEdge DGLinkLab
e Conservativity -> Conservativity -> Bool
forall a. Eq a => a -> a -> Bool
== Conservativity
Cons ]
    mono :: [LEdge DGLinkLab]
mono = (LEdge DGLinkLab -> (Int, Int, EdgeId))
-> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
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
dgl_id DGLinkLab
l))
           [ LEdge DGLinkLab
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
pc ThmLinkStatus
tl)) [LEdge DGLinkLab]
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
DeleteEdge LEdge DGLinkLab
e, LEdge DGLinkLab -> DGChange
InsertEdge (LEdge DGLinkLab -> DGChange) -> LEdge DGLinkLab -> DGChange
forall a b. (a -> b) -> a -> b
$ LEdge DGLinkLab -> (ConsStatus -> ConsStatus) -> LEdge DGLinkLab
modifyEdgeCons 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
t, DGLinkLab
l {
     dgl_type :: DGLinkType
dgl_type = case DGLinkLab -> DGLinkType
dgl_type DGLinkLab
l of
                ScopedLink sc :: Scope
sc dl :: LinkKind
dl cs :: ConsStatus
cs -> Scope -> LinkKind -> ConsStatus -> DGLinkType
ScopedLink Scope
sc LinkKind
dl (ConsStatus -> DGLinkType) -> ConsStatus -> DGLinkType
forall a b. (a -> b) -> a -> b
$ ConsStatus -> ConsStatus
f ConsStatus
cs
                tp :: DGLinkType
tp -> DGLinkType
tp
   , dgl_origin :: DGLinkOrigin
dgl_origin = DGLinkOrigin
DGLinkProof
   , 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
getConservativity LEdge DGLinkLab
e Conservativity -> Conservativity -> Bool
forall a. Eq a => a -> a -> Bool
== Conservativity
None) ([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 ((DGLinkType -> Bool) -> LEdge DGLinkLab -> Bool
forall a. (DGLinkType -> a) -> LEdge DGLinkLab -> a
liftE DGLinkType -> Bool
isGlobalThm) ([LEdge DGLinkLab] -> [LEdge DGLinkLab])
-> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
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]
process [LEdge DGLinkLab]
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
DeleteEdge LEdge DGLinkLab
e, LEdge DGLinkLab -> DGChange
InsertEdge (Int
s, Int
t, DGLinkLab
l {
        dgl_type :: DGLinkType
dgl_type = case DGLinkLab -> DGLinkType
dgl_type DGLinkLab
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
                                                         (DGLinkLab -> GMorphism
dgl_morphism DGLinkLab
l) ThmLinkStatus
ls
                   tp :: DGLinkType
tp -> DGLinkType
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
$ [[LEdge DGLinkLab]]
-> [Conservativity] -> [([LEdge DGLinkLab], Conservativity)]
forall a b. [a] -> [b] -> [(a, b)]
zip [[LEdge DGLinkLab]]
nodePaths
                (([LEdge DGLinkLab] -> Conservativity)
-> [[LEdge DGLinkLab]] -> [Conservativity]
forall a b. (a -> b) -> [a] -> [b]
map [LEdge DGLinkLab] -> Conservativity
getConservativityOfPath [[LEdge DGLinkLab]]
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
last [LEdge DGLinkLab]
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 }
          }