{- |

Module : $Header$

Description : conservativity proof rule for development graphs

Copyright : (c) Markus Gross, DFKI 2009

License : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.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(changesDGH, isFreeEdge, isGlobalEdge, isGlobalThm,

getAllPathsOfTypeFrom)

import Proofs.ComputeColimit(makeDiagram)

import Static.DevGraph

import Static.GTheory(gEnsuresAmalgamability)

import Data.Graph.Inductive.Graph(LEdge, LNode)

import Data.List(nubBy, nub)

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,

e1 /= e2, s1 == s2, t1 /= s1, t2 /= s2 ]

pairs2 = nubBy nubPair [ (e3, e4) | e3@(_,t3,_)<-edgs, e4@(_,t4,_)<-edgs,

e3 /= e4 && t3 == t4 ]

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) = (e1 == e3 && e2 == e4) || (e1 == e4) && (e2 == e3)

-- 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,_) -> x /= e1 && x /= e2 && t == t1 ) $

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 = nub [ 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)

(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 }

}