e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiDescription : global proof rules for development graphs
333780eae2be9f20fe46dedbf5eb46ffa0cbfd02Christian MaederCopyright : (c) Jorina F. Gerken, Till Mossakowski, Uni Bremen 2002-2006
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
cfbd735270fe52115cef0508d265785efcb99cd7Christian MaederMaintainer : Christian.Maeder@dfki.de
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederStability : provisional
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian MaederPortability : non-portable(DevGraph)
e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowskiglobal proof rules for development graphs.
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder Follows Sect. IV:4.4 of the CASL Reference Manual.
846286f96bb7bd5d2b9db834561a815f832a8d90Christian Maeder ( globSubsume
846286f96bb7bd5d2b9db834561a815f832a8d90Christian Maeder , globDecompAux -- for Test.hs
846286f96bb7bd5d2b9db834561a815f832a8d90Christian Maeder , globDecompFromList
846286f96bb7bd5d2b9db834561a815f832a8d90Christian Maeder , globSubsumeFromList
d6a6c1a2fb6526fdcacd8386c9aa3340169a1049Cui Jianimport qualified Data.Map as Map
0a5165c161ce13d434b5c0488b533a8de98aafaaChristian MaederglobDecompRule :: EdgeId -> DGRule
c4df2219ea6f47a5e510503e475c38362e8464ebChristian MaederglobDecompRule = DGRuleWithEdge "Global-Decomposition"
04d04d19fdd5320953c78ad5b6d2d11f85bc4bcfChristian Maeder{- apply rule GlobDecomp to all global theorem links in the current DG
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder current DG = DGm
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder add to proof status the pair ([GlobDecomp e1,...,GlobDecomp en],DGm+1)
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder where e1...en are the global theorem links in DGm
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder DGm+1 results from DGm by application of GlobDecomp e1,...,GlobDecomp en -}
99e6fb75f064189db8f26fe74eb8f01af353e58eCui Jian{- | applies global decomposition to the list of edges given (global
99e6fb75f064189db8f26fe74eb8f01af353e58eCui Jian theorem edges) if possible, if empty list is given then to all
99e6fb75f064189db8f26fe74eb8f01af353e58eCui Jian unproven global theorems.
99e6fb75f064189db8f26fe74eb8f01af353e58eCui Jian Notice: (for ticket 5, which solves the problem across library border)
99e6fb75f064189db8f26fe74eb8f01af353e58eCui Jian 1. before the actual global decomposition is applied, the whole DGraph is
99e6fb75f064189db8f26fe74eb8f01af353e58eCui Jian updated firstly by calling the function updateDGraph.
99e6fb75f064189db8f26fe74eb8f01af353e58eCui Jian 2. The changes of the update action should be added as the head of the
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian MaederglobDecompFromList :: LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv
6948b7295a0521212803f15cf919395d2073e2c9Christian MaederglobDecompFromList ln globalThmEdges proofStatus =
6948b7295a0521212803f15cf919395d2073e2c9Christian Maeder let dgraph = lookupDGraph ln proofStatus
6948b7295a0521212803f15cf919395d2073e2c9Christian Maeder finalGlobalThmEdges = filter (liftE isUnprovenGlobalThm) globalThmEdges
4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian Maeder auxGraph = foldl (updateDGraph proofStatus) dgraph
7308170a663b06590b9ca5c9470baafbbf411f35Christian Maeder $ nubOrd $ map (\ (src, _, _) -> src) finalGlobalThmEdges
4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian Maeder newDGraph = foldl globDecompAux auxGraph finalGlobalThmEdges
4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian Maeder in Map.insert ln newDGraph proofStatus
99e6fb75f064189db8f26fe74eb8f01af353e58eCui Jian{- | update the given DGraph with source nodes of all global unproven
99e6fb75f064189db8f26fe74eb8f01af353e58eCui Jian The idea is, to expand the given DGraph by adding all the referenced
99e6fb75f064189db8f26fe74eb8f01af353e58eCui Jian nodes related to the given source nodes in other libraries and the
99e6fb75f064189db8f26fe74eb8f01af353e58eCui Jian corresponding links as well.
99e6fb75f064189db8f26fe74eb8f01af353e58eCui Jian If a certain node is a referenced node and not expanded yet, then its
afe76697dd6888856a066934a1112a38809b27faChristian Maeder parents will be found by calling getRefParents.
99e6fb75f064189db8f26fe74eb8f01af353e58eCui Jian These parents will be added into current DGraph using updateDGraphAux
afe76697dd6888856a066934a1112a38809b27faChristian MaederupdateDGraph :: LibEnv -> DGraph
afe76697dd6888856a066934a1112a38809b27faChristian Maeder -> Node -- source nodes of all global unproven links
afe76697dd6888856a066934a1112a38809b27faChristian MaederupdateDGraph le dg x =
290674793b16476e77c99fcf6cadecdb7b2947c9Christian Maeder case lookupRefNodeM le Nothing dg x of
290674793b16476e77c99fcf6cadecdb7b2947c9Christian Maeder (Just refl, refDg, (refn, _)) ->
290674793b16476e77c99fcf6cadecdb7b2947c9Christian Maeder parents = getRefParents refDg refn
99e6fb75f064189db8f26fe74eb8f01af353e58eCui Jian {- important for those, who's doing redo/undo function:
17d4f8c5576d93f36cafe68161cdb960ec49ce7cChristian Maeder notice that if the node is expanded, then it should be
17d4f8c5576d93f36cafe68161cdb960ec49ce7cChristian Maeder deleted out of the unexpanded map using
99e6fb75f064189db8f26fe74eb8f01af353e58eCui Jian deleteFromRefNodesDG -}
290674793b16476e77c99fcf6cadecdb7b2947c9Christian Maeder auxDG = foldl (updateDGraphAux le x refl refDg)
99e6fb75f064189db8f26fe74eb8f01af353e58eCui Jian{- | get all the parents, namely the related referenced nodes and the links
99e6fb75f064189db8f26fe74eb8f01af353e58eCui Jian between them and the present to be expanded node.
290674793b16476e77c99fcf6cadecdb7b2947c9Christian MaedergetRefParents :: DGraph
17d4f8c5576d93f36cafe68161cdb960ec49ce7cChristian Maeder -> Node -- the present to be expanded node
290674793b16476e77c99fcf6cadecdb7b2947c9Christian Maeder -> [(Node, [DGLinkLab])]
290674793b16476e77c99fcf6cadecdb7b2947c9Christian MaedergetRefParents dg refn =
0a5165c161ce13d434b5c0488b533a8de98aafaaChristian Maeder -- get the previous objects to the current one
df38505443a40ea057313d099cec2621fc408f80Christian Maeder pres = innDG dg refn
290674793b16476e77c99fcf6cadecdb7b2947c9Christian Maeder in modifyPs pres
99e6fb75f064189db8f26fe74eb8f01af353e58eCui Jian{- | modify the parents to a better form.
99e6fb75f064189db8f26fe74eb8f01af353e58eCui Jian e.g. if the list is like:
99e6fb75f064189db8f26fe74eb8f01af353e58eCui Jian [(a, 1), (b, 1), (c, 2), (d, 2), (e, 2)]
99e6fb75f064189db8f26fe74eb8f01af353e58eCui Jian which means that node 1 is related via links a and b, and node 2 is
99e6fb75f064189db8f26fe74eb8f01af353e58eCui Jian related via links c, d and e.
99e6fb75f064189db8f26fe74eb8f01af353e58eCui Jian then to advoid too many checking by inserting, we can modify the list
99e6fb75f064189db8f26fe74eb8f01af353e58eCui Jian above to a form like this:
99e6fb75f064189db8f26fe74eb8f01af353e58eCui Jian [(1, [a, b]), (2, [c, d, e])]
99e6fb75f064189db8f26fe74eb8f01af353e58eCui Jian which simplifies the inserting afterwards ;)
290674793b16476e77c99fcf6cadecdb7b2947c9Christian MaedermodifyPs :: [LEdge DGLinkLab] -> [(Node, [DGLinkLab])]
290674793b16476e77c99fcf6cadecdb7b2947c9Christian MaedermodifyPs = Map.toList . Map.fromListWith (++)
290674793b16476e77c99fcf6cadecdb7b2947c9Christian Maeder . map (\ (k, _, v) -> (k, [v]))
99e6fb75f064189db8f26fe74eb8f01af353e58eCui Jian{- | the actual update function to insert a list of related parents to the
99e6fb75f064189db8f26fe74eb8f01af353e58eCui Jian present to be expanded node.
290674793b16476e77c99fcf6cadecdb7b2947c9Christian Maeder It inserts the related referenced node first by calling addParentNode.
290674793b16476e77c99fcf6cadecdb7b2947c9Christian Maeder Then it inserts the related links by calling addParentLinks.
7b95c208b55d0a41e2cdb21c7cf0ffb644798231Christian MaederupdateDGraphAux :: LibEnv -> Node -- the present to be expanded node
290674793b16476e77c99fcf6cadecdb7b2947c9Christian Maeder -> DGraph -- ^ the reference graph for the libname
290674793b16476e77c99fcf6cadecdb7b2947c9Christian Maeder -> DGraph -> (Node, [DGLinkLab])
290674793b16476e77c99fcf6cadecdb7b2947c9Christian MaederupdateDGraphAux libenv n refl refDg dg (pn, pls) =
290674793b16476e77c99fcf6cadecdb7b2947c9Christian Maeder (auxDG, newN) = addParentNode libenv dg refl refDg pn
4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian Maeder in addParentLinks auxDG newN n pls
0a5165c161ce13d434b5c0488b533a8de98aafaaChristian Maeder-- | add the given parent node into the current dgraph
7b95c208b55d0a41e2cdb21c7cf0ffb644798231Christian MaederaddParentNode :: LibEnv -> DGraph -> LibName
290674793b16476e77c99fcf6cadecdb7b2947c9Christian Maeder -> DGraph -- ^ the reference graph for the libname
290674793b16476e77c99fcf6cadecdb7b2947c9Christian Maeder -> Node -- the referenced parent node
4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian Maeder -> (DGraph, Node)
290674793b16476e77c99fcf6cadecdb7b2947c9Christian MaederaddParentNode libenv dg refl refDg refn =
7b95c208b55d0a41e2cdb21c7cf0ffb644798231Christian Maeder To advoid the chain which is desribed in ticket 5, the parent node should
7b95c208b55d0a41e2cdb21c7cf0ffb644798231Christian Maeder be a non referenced node firstly, so that the actual parent node can be
290674793b16476e77c99fcf6cadecdb7b2947c9Christian Maeder (newRefl, _, (newRefn, nodelab)) = lookupRefNode libenv refl
99e6fb75f064189db8f26fe74eb8f01af353e58eCui Jian Set the sgMap and tMap too.
99e6fb75f064189db8f26fe74eb8f01af353e58eCui Jian Notice for those who are doing undo/redo, because the DGraph is actually
99e6fb75f064189db8f26fe74eb8f01af353e58eCui Jian changed if the maps are changed ;)
0a5165c161ce13d434b5c0488b533a8de98aafaaChristian Maeder creates an empty GTh, please check the definition of this function
0a5165c161ce13d434b5c0488b533a8de98aafaaChristian Maeder because there can be some problem or errors at this place. -}
0a4602500f0b48437405cb9f0eef36066093a60cChristian Maeder newGTh = case dgn_theory nodelab of
c1d06b3018b34ede2b3fb6c7fe2ad28cd5ce5b68Christian Maeder G_theory lid _ sig ind _ _ -> noSensGTheory lid sig ind
84a30e66aef85cc54d3dd6f8e408729007fe8809Christian Maeder refInfo = newRefInfo newRefl newRefn
0155c8d32b79581866f07cc593aa8a4c722ceef2Christian Maeder newRefNode = (newInfoNodeLab (dgn_name nodelab) refInfo newGTh)
0155c8d32b79581866f07cc593aa8a4c722ceef2Christian Maeder { globalTheory = globalTheory nodelab }
0a5165c161ce13d434b5c0488b533a8de98aafaaChristian Maeder {- checks if this node exists in the current dg, if so, nothing needs to be
84a30e66aef85cc54d3dd6f8e408729007fe8809Christian Maeder case lookupInAllRefNodesDG refInfo dg of
4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian Maeder Nothing -> let newN = getNewNodeDG dg in
66c6e29ddfa36396c7ebfc02d01d8d7e6c26976cChristian Maeder (changeDGH dg $ InsertNode (newN, newRefNode), newN)
4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian Maeder Just extN -> (dg, extN)
0a5165c161ce13d434b5c0488b533a8de98aafaaChristian Maeder-- | add a list of links between the given two node ids.
4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian MaederaddParentLinks :: DGraph -> Node -> Node -> [DGLinkLab] -> DGraph
7308170a663b06590b9ca5c9470baafbbf411f35Christian MaederaddParentLinks dg src tgt ls =
7308170a663b06590b9ca5c9470baafbbf411f35Christian Maeder let oldLinks = map (\ (_, _, l) -> l)
7308170a663b06590b9ca5c9470baafbbf411f35Christian Maeder $ filter (\ (s, _, _) -> s == src) $ innDG dg tgt
7308170a663b06590b9ca5c9470baafbbf411f35Christian Maeder newLinks = map (\ l -> l
7308170a663b06590b9ca5c9470baafbbf411f35Christian Maeder { dgl_id = defaultEdgeId
df38505443a40ea057313d099cec2621fc408f80Christian Maeder , dgl_type = invalidateProof $ dgl_type l }) ls
7308170a663b06590b9ca5c9470baafbbf411f35Christian Maeder in if null oldLinks then
7308170a663b06590b9ca5c9470baafbbf411f35Christian Maeder changesDGH dg $ map (\ l -> InsertEdge (src, tgt, l)) newLinks
7308170a663b06590b9ca5c9470baafbbf411f35Christian Maeder else dg -- assume ingoing links are already properly set
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder{- applies global decomposition to all unproven global theorem edges
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder if possible -}
0155c8d32b79581866f07cc593aa8a4c722ceef2Christian MaederglobDecomp :: LibName -> LibEnv -> LibEnv
333780eae2be9f20fe46dedbf5eb46ffa0cbfd02Christian MaederglobDecomp ln proofStatus =
6948b7295a0521212803f15cf919395d2073e2c9Christian Maeder let dgraph = lookupDGraph ln proofStatus
8b4b1dc5b5bc6e85f9f910b0d992fe658eb064beChristian Maeder globalThmEdges = labEdgesDG dgraph
846286f96bb7bd5d2b9db834561a815f832a8d90Christian Maeder globDecompFromList ln globalThmEdges proofStatus
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder{- auxiliary function for globDecomp (above)
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder actual implementation -}
4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian MaederglobDecompAux :: DGraph -> LEdge DGLinkLab -> DGraph
afe76697dd6888856a066934a1112a38809b27faChristian MaederglobDecompAux dgraph edge =
4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian Maeder let newDGraph = globDecompForOneEdge dgraph edge
0a5165c161ce13d434b5c0488b533a8de98aafaaChristian Maeder in groupHistory dgraph (globDecompRule $ getEdgeId edge) newDGraph
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder-- applies global decomposition to a single edge
4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian MaederglobDecompForOneEdge :: DGraph -> LEdge DGLinkLab -> DGraph
afe76697dd6888856a066934a1112a38809b27faChristian MaederglobDecompForOneEdge dgraph edge@(source, target, edgeLab) = let
77f7dcf46acba47d5986907cae32ce6c615871c9Christian Maeder defEdgesToSource = filter (liftE isDefEdge) $ innDG dgraph source
77f7dcf46acba47d5986907cae32ce6c615871c9Christian Maeder paths = [edge] : map (: [edge]) defEdgesToSource
77f7dcf46acba47d5986907cae32ce6c615871c9Christian Maeder (newGr, proof_basis) = foldl
afe76697dd6888856a066934a1112a38809b27faChristian Maeder (globDecompForOneEdgeAux target) (dgraph, emptyProofBasis) paths
afe76697dd6888856a066934a1112a38809b27faChristian Maeder provenEdge = (source, target, edgeLab
0a5165c161ce13d434b5c0488b533a8de98aafaaChristian Maeder { dgl_type = setProof (Proven (globDecompRule $ getEdgeId edge)
9192fdd8f0e682ac0f0183dd854d5210fbfa4ec5Christian Maeder $ dgl_type edgeLab
4f07c310c7083eaf5d54fb7d14a4db1cd28e45faChristian Maeder , dglPending = True
bbd9ff47b93f02c2cb2f101b074da02a2f683fe3Christian Maeder , dgl_origin = DGLinkProof })
4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian Maeder in changesDGH newGr [DeleteEdge edge, InsertEdge provenEdge]
9192fdd8f0e682ac0f0183dd854d5210fbfa4ec5Christian Maeder{- auxiliary function for globDecompForOneEdge (above)
afe76697dd6888856a066934a1112a38809b27faChristian Maeder actual implementation -}
afe76697dd6888856a066934a1112a38809b27faChristian MaederglobDecompForOneEdgeAux :: Node -> (DGraph, ProofBasis)
afe76697dd6888856a066934a1112a38809b27faChristian Maeder -> [LEdge DGLinkLab]
4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian Maeder -> (DGraph, ProofBasis)
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder-- for each path an unproven localThm edge is inserted
afe76697dd6888856a066934a1112a38809b27faChristian MaederglobDecompForOneEdgeAux target (dgraph, proof_basis) path =
afe76697dd6888856a066934a1112a38809b27faChristian Maeder [] -> error "globDecompForOneEdgeAux"
d24317c8197e565e60c8f41309de246249c1e57eChristian Maeder (node, tar, lbl) : rpath -> let
afe76697dd6888856a066934a1112a38809b27faChristian Maeder lbltype = dgl_type lbl
afe76697dd6888856a066934a1112a38809b27faChristian Maeder isHiding = isHidingDef lbltype
b85135bea5cb5c8b0841d28fcf9e51f5c0461218Christian Maeder morphismPath = if isHiding then rpath else path
0a5165c161ce13d434b5c0488b533a8de98aafaaChristian Maeder morphism = fromMaybe
0a5165c161ce13d434b5c0488b533a8de98aafaaChristian Maeder (error "globDecomp: could not determine morphism of new edge")
0a5165c161ce13d434b5c0488b533a8de98aafaaChristian Maeder $ calculateMorphismOfPath morphismPath
77f7dcf46acba47d5986907cae32ce6c615871c9Christian Maeder defEdgesToTarget = filter
77f7dcf46acba47d5986907cae32ce6c615871c9Christian Maeder (\ (s, _, l) -> s == node && isGlobalDef (dgl_type l)
77f7dcf46acba47d5986907cae32ce6c615871c9Christian Maeder && dgl_morphism l == morphism)
77f7dcf46acba47d5986907cae32ce6c615871c9Christian Maeder $ innDG dgraph target
d11391a2447a2005329a95b5d770f24e62bf5b63Christian Maeder newEdgeLbl = defDGLink morphism
d24317c8197e565e60c8f41309de246249c1e57eChristian Maeder (if isHiding then hidingThm tar $ dgl_morphism lbl
d11391a2447a2005329a95b5d770f24e62bf5b63Christian Maeder else if isGlobalDef lbltype then globalThm else localThm)
767e78dd0b080bc40892d0fbaff1b1528adfe36bChristian Maeder newEdge = (node, target, newEdgeLbl)
77f7dcf46acba47d5986907cae32ce6c615871c9Christian Maeder in case defEdgesToTarget of
cd45bb1a7c7bcf5667e3db4cd78dcea51b95d9a7Christian Maeder (_, _, dl) : _ | not isHiding
77f7dcf46acba47d5986907cae32ce6c615871c9Christian Maeder -> (dgraph, addEdgeId proof_basis $ dgl_id dl)
77f7dcf46acba47d5986907cae32ce6c615871c9Christian Maeder _ | node == target && isInc (getRealDGLinkType newEdgeLbl)
77f7dcf46acba47d5986907cae32ce6c615871c9Christian Maeder && isGlobalDef lbltype
77f7dcf46acba47d5986907cae32ce6c615871c9Christian Maeder -> (dgraph, addEdgeId proof_basis $ dgl_id lbl)
77f7dcf46acba47d5986907cae32ce6c615871c9Christian Maeder _ -> case tryToGetEdge newEdge dgraph of
afe76697dd6888856a066934a1112a38809b27faChristian Maeder Nothing -> let
4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian Maeder newGraph = changeDGH dgraph $ InsertEdge newEdge
4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian Maeder finalEdge = case getLastChange newGraph of
4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian Maeder InsertEdge final_e -> final_e
afe76697dd6888856a066934a1112a38809b27faChristian Maeder _ -> error "Proofs.Global.globDecompForOneEdgeAux"
4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian Maeder in (newGraph, addEdgeId proof_basis $ getEdgeId finalEdge)
4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian Maeder Just e -> (dgraph, addEdgeId proof_basis $ getEdgeId e)
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian MaederglobSubsumeFromList :: LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv
6948b7295a0521212803f15cf919395d2073e2c9Christian MaederglobSubsumeFromList ln globalThmEdges libEnv =
6948b7295a0521212803f15cf919395d2073e2c9Christian Maeder let dgraph = lookupDGraph ln libEnv
6948b7295a0521212803f15cf919395d2073e2c9Christian Maeder finalGlobalThmEdges = filter (liftE isUnprovenGlobalThm) globalThmEdges
4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian Maeder nextDGraph = foldl
afe76697dd6888856a066934a1112a38809b27faChristian Maeder (globSubsumeAux libEnv) dgraph finalGlobalThmEdges
4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian Maeder in Map.insert ln nextDGraph libEnv
846286f96bb7bd5d2b9db834561a815f832a8d90Christian Maeder-- | tries to apply global subsumption to all unproven global theorem edges
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian MaederglobSubsume :: LibName -> LibEnv -> LibEnv
04d04d19fdd5320953c78ad5b6d2d11f85bc4bcfChristian MaederglobSubsume ln libEnv =
6948b7295a0521212803f15cf919395d2073e2c9Christian Maeder let dgraph = lookupDGraph ln libEnv
e482d85bc68c1ef56fbf0371b7287271b9857165Christian Maeder globalThmEdges = labEdgesDG dgraph
6948b7295a0521212803f15cf919395d2073e2c9Christian Maeder in globSubsumeFromList ln globalThmEdges libEnv
0a5165c161ce13d434b5c0488b533a8de98aafaaChristian Maeder-- auxiliary function for globSubsume (above) the actual implementation
0a5165c161ce13d434b5c0488b533a8de98aafaaChristian MaederglobSubsumeAux :: LibEnv -> DGraph -> LEdge DGLinkLab -> DGraph
afe76697dd6888856a066934a1112a38809b27faChristian MaederglobSubsumeAux libEnv dgraph ledge@(src, tgt, edgeLab) =
bbd9ff47b93f02c2cb2f101b074da02a2f683fe3Christian Maeder let morphism = dgl_morphism edgeLab
bbd9ff47b93f02c2cb2f101b074da02a2f683fe3Christian Maeder filteredPaths = filterPathsByMorphism morphism $ filter (noPath ledge)
1788a1325a425375f05ca01f62903d748718e3efChristian Maeder $ getAllGlobPathsBetween dgraph src tgt
bbd9ff47b93f02c2cb2f101b074da02a2f683fe3Christian Maeder proofbasis = selectProofBasis dgraph ledge filteredPaths
bbd9ff47b93f02c2cb2f101b074da02a2f683fe3Christian Maeder in if not (nullProofBasis proofbasis) || isIdentityEdge ledge libEnv dgraph
0a5165c161ce13d434b5c0488b533a8de98aafaaChristian Maeder let globSubsumeRule = DGRuleWithEdge "Global-Subsumption"
0a5165c161ce13d434b5c0488b533a8de98aafaaChristian Maeder $ getEdgeId ledge
bbd9ff47b93f02c2cb2f101b074da02a2f683fe3Christian Maeder newEdge = (src, tgt, edgeLab
9192fdd8f0e682ac0f0183dd854d5210fbfa4ec5Christian Maeder { dgl_type = setProof (Proven globSubsumeRule proofbasis)
9192fdd8f0e682ac0f0183dd854d5210fbfa4ec5Christian Maeder $ dgl_type edgeLab
bbd9ff47b93f02c2cb2f101b074da02a2f683fe3Christian Maeder , dgl_origin = DGLinkProof })
4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian Maeder newDGraph = changesDGH dgraph [DeleteEdge ledge, InsertEdge newEdge]
c4df2219ea6f47a5e510503e475c38362e8464ebChristian Maeder in groupHistory dgraph globSubsumeRule newDGraph