Conservativity.hs revision 98890889ffb2e8f6f722b00e265a211f13b5a861
c3d42e13d2a7c3749229498658aec34e7e4fd0a0Christian MaederModule : $Header$
c3d42e13d2a7c3749229498658aec34e7e4fd0a0Christian MaederDescription : conservativity proof rule for development graphs
cd7372fc7e6e43c389619f63daa6eb872d9d5b16Christian MaederCopyright : (c) Markus Gross, DFKI 2009
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
c3d42e13d2a7c3749229498658aec34e7e4fd0a0Christian MaederMaintainer : mgross@informatik.uni-bremen.de
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederStability : provisional
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederPortability : non-portable(Logic)
99c923311eab71a85f1dcc4785d349609c828da4Christian Maederconservativity proof rule for development graphs
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder Follows Sect. IV:4.4.2 of the CASL Reference Manual.
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maedermodule Proofs.Conservativity (conservativity) where
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederimport Common.Amalgamate(Amalgamates(Amalgamates), CASLAmalgOpt(..))
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maederimport Common.Result(resultToMaybe)
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maederimport Proofs.EdgeUtils(isFreeEdge, isGlobalEdge, isGlobalThm,
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder getAllPathsOfTypeFrom)
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maederimport Proofs.ComputeColimit(makeDiagram)
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maederimport Static.GTheory(gEnsuresAmalgamability)
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maederimport Data.Graph.Inductive.Graph(LEdge, LNode)
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maederimport Data.List(nubBy, nub)
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maederimport qualified Data.Map as Map
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder------------------------------------------------
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder-- Conservativity rules
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder------------------------------------------------
989ba1f28e0846635a9f098bebbfbdfa9b1c5ed0Jonathan von Schroeder{- A pair is defined as:
90d97972167d142dde6ee8b18d9625332040261fJonathan von Schroedern ---- e2 ----> n
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maedertype Pair = (LEdge DGLinkLab, LEdge DGLinkLab)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini{- A quad is defined as:
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini((e1, e2), (e3, e4))
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrinin ---- e2 ----> n
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrinin ---- e3 ----> n
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrinitype Quad = (Pair, Pair)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- Main function, calls all rules.
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torriniconservativity :: LibName -> LibEnv -> LibEnv
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torriniconservativity = Map.adjust (shift . freeIsMono . monoIsFree . compCons)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- Shift-Rule.
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- First a list of edge pairs with the same source node is generated.
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- Then all pairs are positioned correctly. All pairs which have
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- one edge with a cons value are kept.
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- A list of quads (pair, pair) is generated. Each input pair is combined with
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- another pair, which has the same target and where the edges have the same
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- source nodes. (See type Quad for a picture.)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- The target node of the quads must be isolated and the quad has to be
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- amalgamable.
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- Afterwards the quad is positioned correctly and the edges are updated.
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrinishift :: DGraph -> DGraph
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrinishift dg = groupHistory dg (DGRule "conservativityShift") $
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini changesDGH dg changes
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini edgs = filter (liftE isGlobalEdge) $ labEdgesDG dg
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini globThmEdges = filter (liftE isGlobalThm) edgs
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini consEdgs = [ e | e <-globThmEdges, getConservativity e > None ]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini pairs1 = nubBy nubPair [ (e1, e2) | e1@(s1,t1,_)<-consEdgs,
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini e2@(s2,t2,_)<-globThmEdges,
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini e1 /= e2, s1 == s2, t1 /= s1, t2 /= s2 ]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini pairs2 = nubBy nubPair [ (e3, e4) | e3@(_,t3,_)<-edgs, e4@(_,t4,_)<-edgs,
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini e3 /= e4 && t3 == t4 ]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini quads = filter (isAmalgamable dg) $
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini filter (isolated edgs . snd) $ map posQuad
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini [ ((e1, e2), (e3, e4)) | (e1@(_,t1,_), e2@(_,t2,_))<-pairs1,
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian Maeder (e3@(s3,_,_), e4@(s4,_,_))<-pairs2,
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini (t1 == s3 && t2 == s4) ||
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini (t1 == s4 && t2 == s3) ]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini changes = concatMap process quads
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini -- Updates the e4 edge with the cons value from the e1 edge.
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini -- The quads have to be positioned correctly before using this function.
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini process :: Quad -> [DGChange]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini process ((e1, _), (_, e4)) =
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini let cons = getConservativity e1
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini in genEdgeChange
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly (\ (ConsStatus co pc tl) -> ConsStatus (max cons co) pc tl) e4
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly-- Checks if a quad is amalgamable.
d9c1248c7972dfdafbacb1b73b2eb965eac9ef42Liam O'ReillyisAmalgamable :: DGraph -> Quad -> Bool
d9c1248c7972dfdafbacb1b73b2eb965eac9ef42Liam O'ReillyisAmalgamable dg ((e1@(s1,_,_), e2), (e3@(s3,_,l3), e4@(s4,t4,l4))) =
d9c1248c7972dfdafbacb1b73b2eb965eac9ef42Liam O'Reilly case resultToMaybe amal of
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Just Amalgamates -> True
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly sink = [(s3, dgl_morphism l3), (s4, dgl_morphism l4)]
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly diag = makeDiagram dg [s1, s3, s4, t4] [e1, e2, e3, e4]
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly amal = gEnsuresAmalgamability [ColimitThinness,Cell] diag sink
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly-- Checks wether a pair is duplicate.
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'ReillynubPair :: Pair -> Pair -> Bool
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'ReillynubPair (e1, e2) (e3, e4) = (e1 == e3 && e2 == e4) || (e1 == e4) && (e2 == e3)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- Positions a quad so that the e4 edge is the one whose source node is the
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder-- target node of e2. Also checks if the e4 has no conservativity value.
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederposQuad :: Quad -> Quad
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederposQuad q@((e1@(_,t1,_), e2@(_,t2,_)), (e3@(s3,_,_), e4))
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder | s3 == t1 = q
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini | s3 == t2 = ((e1, e2), (e4, e3))
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini | otherwise = error "Proofs.Conservativity.posQuad"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- Checks wether the node of the pair is isolated.
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- Both edges of the pair have the same target node.
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torriniisolated :: [LEdge DGLinkLab] -> Pair -> Bool
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torriniisolated edgs (e1@(_,t1,_), e2) =
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini not $ any (\ x@(_,t,_) -> x /= e1 && x /= e2 && t == t1 ) $
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini filter (liftE isGlobalDef) edgs
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- First get all free links in the graph. Then all cons links.
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- When the free and cons link point to the same node, the cons link is upgraded
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinifreeIsMono :: DGraph -> DGraph
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinifreeIsMono dg = groupHistory dg (DGRule "freeIsMono") $ changesDGH dg changes
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini edgs = labEdgesDG dg
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini free = filter (liftE isFreeEdge) edgs
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini cons = [ e | e<-edgs, liftE isGlobalThm e, getConservativity e == Cons ]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini mono = nub [ c | c@(_, ct, _)<-cons, (_, ft, _)<-free, ct == ft ]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini changes = concatMap (genEdgeChange
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini (\ (ConsStatus _ pc tl) -> ConsStatus Mono pc tl)) mono
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- Generates a list of changes for the development graph.
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinigenEdgeChange :: (ConsStatus -> ConsStatus) -> LEdge DGLinkLab -> [DGChange]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinigenEdgeChange f e = [ DeleteEdge e, InsertEdge $ modifyEdgeCons e f ]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- Modifies the ConsStatus of an edge.
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinimodifyEdgeCons :: LEdge DGLinkLab
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini -> (ConsStatus -> ConsStatus) -> LEdge DGLinkLab
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinimodifyEdgeCons (s, t, l) f =
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini dgl_type = case dgl_type l of
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ScopedLink sc dl cs -> ScopedLink sc dl $ f cs
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini , dgl_origin = DGLinkProof
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini , dgl_id = defaultEdgeId
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian MaedermonoIsFree :: DGraph -> DGraph
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinimonoIsFree dg = groupHistory dg (DGRule "monoIsFree") $ changesDGH dg changes
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder mono = filter (\ n -> getNodeConservativity n == Mono) $ labNodesDG dg
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder thmEdges = filter (\ e -> getConservativity e == None) $
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini filter (liftE isGlobalThm) $ labEdgesDG dg
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini freeEdges = [ e | (n,_)<-mono, e@(s,_,_)<-thmEdges, n == s ]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini changes = concatMap process freeEdges
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini process :: LEdge DGLinkLab -> [DGChange]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini process e@(s, t, l) = [ DeleteEdge e, InsertEdge (s, t, l {
d4e8d3a0ddb1a63754edc3571b6a3a54a7b62d04Paolo Torrini dgl_type = case dgl_type l of
d4e8d3a0ddb1a63754edc3571b6a3a54a7b62d04Paolo Torrini ScopedLink _ _ (ConsStatus _ _ ls) -> HidingFreeOrCofreeThm
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder (dgl_morphism l) ls
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maeder-- If Node n is cons and the path to Node m is also cons then m is cons too.
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinicompCons :: DGraph -> DGraph
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinicompCons dg = groupHistory dg (DGRule "compCons") $ changesDGH dg changes
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder consNodes = filter (\ n -> getNodeConservativity n /= None) $ labNodesDG dg
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder changes = concatMap (compConsAux dg) consNodes
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder-- First get all paths. Check if the path cons matches with the node cons.
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- If the target node cons is weaker than the path cons replace it.
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinicompConsAux :: DGraph -> LNode DGNodeLab -> [DGChange]
8fdd06d4f6530909e3e24547893a62b042117fb4Christian MaedercompConsAux dg n@(i, _) = changes
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder nodeCons = getNodeConservativity n
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini nodePaths = getAllPathsOfTypeFrom dg i
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini consPaths = filter (\ p -> snd p == nodeCons) $ zip nodePaths
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder (map getConservativityOfPath nodePaths)
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder changes = concatMap process consPaths
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder process :: ([LEdge DGLinkLab], Conservativity) -> [DGChange]
c730c28919b53f940ed319ebb42780244c528e29Paolo Torrini process (path, sourceCons) =
c730c28919b53f940ed319ebb42780244c528e29Paolo Torrini [ SetNodeLab lab (node, lab') | targetNodeCons < sourceCons ]
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder (_, node, _) = last path
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder lab = labDG dg node
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini targetNodeCons = getNodeCons lab
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini nInfo = nodeInfo lab
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini nodeInfo = nInfo { node_cons_status = mkConsStatus sourceCons }