{- |

Module : $Header$

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 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 Data.List (nubBy)

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 = Map.adjust (shift . freeIsMono . monoIsFree . 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 dg = groupHistory dg (DGRule "conservativityShift") $

changesDGH dg changes

where

edgs = filter (liftE isGlobalEdge) $ labEdgesDG dg

globThmEdges = filter (liftE isGlobalThm) edgs

consEdgs = [ e | e <- globThmEdges, getConservativity e > None ]

pairs1 = nubBy nubPair

[ (e1, e2)

| e1@(s1, t1, _) <- consEdgs

, e2@(s2, t2, _) <- globThmEdges

, s1 == s2, t1 /= s1, t2 /= s2, not (eqDGLEdge e1 e2) ]

pairs2 = nubBy nubPair

[ (e3, e4)

| e3@(_, t3, _) <- edgs

, e4@(_, t4, _) <- edgs

, t3 == t4, not (eqDGLEdge e3 e4) ]

quads = filter (isAmalgamable dg) $

filter (isolated edgs . snd) $ map posQuad

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

| (e1@(_, t1, _), e2@(_, t2, _)) <- pairs1

, (e3@(s3, _, _), e4@(s4, _, _)) <- pairs2

, t1 == s3 && t2 == s4 || t1 == s4 && t2 == s3 ]

changes = concatMap process 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 ((e1, _), (_, e4)) =

let cons = getConservativity e1

in genEdgeChange

(\ (ConsStatus co pc tl) -> ConsStatus (max cons co) pc tl) e4

-- Checks if a quad is amalgamable.

isAmalgamable :: DGraph -> Quad -> Bool

isAmalgamable dg ((e1@(s1, _, _), e2), (e3@(s3, _, l3), e4@(s4, t4, l4))) =

case resultToMaybe amal of

Just Amalgamates -> True

_ -> False

where

sink = [(s3, dgl_morphism l3), (s4, dgl_morphism l4)]

diag = makeDiagram dg [s1, s3, s4, t4] [e1, e2, e3, e4]

amal = gEnsuresAmalgamability [ColimitThinness, Cell] diag sink

-- Checks wether a pair is duplicate.

nubPair :: Pair -> Pair -> Bool

nubPair (e1, e2) (e3, e4) = eqDGLEdge e1 e3 && eqDGLEdge e2 e4

|| eqDGLEdge e1 e4 && eqDGLEdge e2 e3

eqDGLEdge :: LEdge DGLinkLab -> LEdge DGLinkLab -> Bool

eqDGLEdge (s1, t1, l1) (s2, t2, l2) = (s1, t1) == (s2, t2)

&& eqDGLinkLabById l1 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 q@((e1@(_, t1, _), e2@(_, t2, _)), (e3@(s3, _, _), e4))

| s3 == t1 = q

| s3 == t2 = ((e1, e2), (e4, e3))

| otherwise = 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 edgs (e1@(_, t1, _), e2) =

not $ any (\ x@(_, t, _) -> t == t1 && not (eqDGLEdge x e1)

&& not (eqDGLEdge x e2)) $ filter (liftE isGlobalDef) 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 dg = groupHistory dg (DGRule "freeIsMono") $ changesDGH dg changes

where

edgs = labEdgesDG dg

free = filter (liftE isFreeEdge) edgs

cons = [ e | e <- edgs, liftE isGlobalThm e, getConservativity e == Cons ]

mono = nubBy eqDGLEdge

[ c | c@(_, ct, _) <- cons, (_, ft, _) <- free, ct == ft ]

changes = concatMap (genEdgeChange

(\ (ConsStatus _ pc tl) -> ConsStatus Mono pc tl)) mono

-- Generates a list of changes for the development graph.

genEdgeChange :: (ConsStatus -> ConsStatus) -> LEdge DGLinkLab -> [DGChange]

genEdgeChange f e = [ DeleteEdge e, InsertEdge $ modifyEdgeCons e f ]

-- Modifies the ConsStatus of an edge.

modifyEdgeCons :: LEdge DGLinkLab

-> (ConsStatus -> ConsStatus) -> LEdge DGLinkLab

modifyEdgeCons (s, t, l) f =

(s, t, l {

dgl_type = case dgl_type l of

ScopedLink sc dl cs -> ScopedLink sc dl $ f cs

tp -> tp

, dgl_origin = DGLinkProof

, dgl_id = defaultEdgeId

})

monoIsFree :: DGraph -> DGraph

monoIsFree dg = groupHistory dg (DGRule "monoIsFree") $ changesDGH dg changes

where

mono = filter (\ n -> getNodeConservativity n == Mono) $ labNodesDG dg

thmEdges = filter (\ e -> getConservativity e == None) $

filter (liftE isGlobalThm) $ labEdgesDG dg

freeEdges = [ e | (n, _) <- mono, e@(s, _, _) <- thmEdges, n == s ]

changes = concatMap process freeEdges

process :: LEdge DGLinkLab -> [DGChange]

process e@(s, t, l) = [ DeleteEdge e, InsertEdge (s, t, l {

dgl_type = case dgl_type l of

ScopedLink _ _ (ConsStatus _ _ ls) -> HidingFreeOrCofreeThm

(Just Free) s

(dgl_morphism l) ls

tp -> tp

})]

-- If Node n is cons and the path to Node m is also cons then m is cons too.

compCons :: DGraph -> DGraph

compCons dg = groupHistory dg (DGRule "compCons") $ changesDGH dg changes

where

consNodes = filter (\ n -> getNodeConservativity n /= None) $ labNodesDG dg

changes = concatMap (compConsAux dg) 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 dg n@(i, _) = changes

where

nodeCons = getNodeConservativity n

nodePaths = getAllPathsOfTypeFrom dg i

consPaths = filter (\ p -> snd p == nodeCons) $ zip nodePaths

(map getConservativityOfPath nodePaths)

changes = concatMap process consPaths

process :: ([LEdge DGLinkLab], Conservativity) -> [DGChange]

process (path, sourceCons) =

[ SetNodeLab lab (node, lab') | targetNodeCons < sourceCons ]

where

(_, node, _) = last path

lab = labDG dg node

targetNodeCons = getNodeCons lab

nInfo = nodeInfo lab

lab' = lab {

nodeInfo = nInfo { node_cons_status = mkConsStatus sourceCons }

}