Global.hs revision d11391a2447a2005329a95b5d770f24e62bf5b63
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederModule : $Header$
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederDescription : global proof rules for development graphs
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederCopyright : (c) Jorina F. Gerken, Till Mossakowski, Uni Bremen 2002-2006
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederMaintainer : ken@informatik.uni-bremen.de
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederStability : provisional
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederPortability : non-portable(DevGraph)
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maederglobal proof rules for development graphs.
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder Follows Sect. IV:4.4 of the CASL Reference Manual.
25da71ee832b729e33def344a68f59fe21ce9c07Eugen Kuksa ( globSubsume
25da71ee832b729e33def344a68f59fe21ce9c07Eugen Kuksa , globDecomp
950875ac099734b9eaccf4233773e6df00477f22Eugen Kuksa , globDecompAux -- for Test.hs
7d0db235b17b2109cd45fa50e6d1bbc77823f81dEugen Kuksa , globDecompFromList
25da71ee832b729e33def344a68f59fe21ce9c07Eugen Kuksa , globSubsumeFromList
ef1c24c8229ade3ac872febebd18c181e32fb9c4Christian Maederimport qualified Data.Map as Map
8723ec450f2e7a024230467c0c28a3f154905483cmaederglobDecompRule :: LEdge DGLinkLab -> DGRule
eae0d62755147d991cc3e903f74f98ac31a7cd42Christian MaederglobDecompRule = DGRuleWithEdge "Global-Decomposition"
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder{- apply rule GlobDecomp to all global theorem links in the current DG
e84c877ad38ce9312eab222a79f44da2015572d2Christian Maeder current DG = DGm
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder add to proof status the pair ([GlobDecomp e1,...,GlobDecomp en],DGm+1)
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder where e1...en are the global theorem links in DGm
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder DGm+1 results from DGm by application of GlobDecomp e1,...,GlobDecomp en -}
ef1c24c8229ade3ac872febebd18c181e32fb9c4Christian Maeder{- | applies global decomposition to the list of edges given (global
945e82ed7877917f3ab1657f555e71991372546aChristian Maeder theorem edges) if possible, if empty list is given then to all
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder unproven global theorems.
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder Notice: (for ticket 5, which solves the problem across library border)
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder 1. before the actual global decomposition is applied, the whole DGraph is
ef1c24c8229ade3ac872febebd18c181e32fb9c4Christian Maeder updated firstly by calling the function updateDGraph.
ef1c24c8229ade3ac872febebd18c181e32fb9c4Christian Maeder 2. The changes of the update action should be added as the head of the
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaederglobDecompFromList :: LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv
d97700a22b2585ece83b05f3fff945fdfd0c44b4Christian MaederglobDecompFromList ln globalThmEdges proofStatus =
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder let dgraph = lookupDGraph ln proofStatus
1d65a799298f6b1253d774c22f61029e6eb99cadcmaeder finalGlobalThmEdges = filter (liftE isUnprovenGlobalThm) globalThmEdges
1d65a799298f6b1253d774c22f61029e6eb99cadcmaeder auxGraph = foldl (updateDGraph proofStatus) dgraph
ea5ccb1c6e89486a54e1f4bd95840147e96093edChristian Maeder $ nubOrd $ map (\ (src, _, _) -> src) finalGlobalThmEdges
de8eee2014437ec4020be15cd363257f87e79943Christian Maeder newDGraph = foldl globDecompAux auxGraph finalGlobalThmEdges
ea5ccb1c6e89486a54e1f4bd95840147e96093edChristian Maeder in Map.insert ln newDGraph proofStatus
fd94a6f66ccb5cef99aa42069b61e4b8734dbd3fChristian Maeder{- | update the given DGraph with source nodes of all global unproven
fd94a6f66ccb5cef99aa42069b61e4b8734dbd3fChristian Maeder The idea is, to expand the given DGraph by adding all the referenced
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder nodes related to the given source nodes in other libraries and the
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder corresponding links as well.
e42249ec61f50a83525db6e5fc9f5c4dd1b4cf5fcmaeder If a certain node is a referenced node and not expanded yet, then its
473f5af6e4803fbeecc814065952396f2501039bChristian Maeder parents will be found by calling getRefParents.
473f5af6e4803fbeecc814065952396f2501039bChristian Maeder These parents will be added into current DGraph using updateDGraphAux
473f5af6e4803fbeecc814065952396f2501039bChristian MaederupdateDGraph :: LibEnv -> DGraph
e42249ec61f50a83525db6e5fc9f5c4dd1b4cf5fcmaeder -> Node -- source nodes of all global unproven links
473f5af6e4803fbeecc814065952396f2501039bChristian MaederupdateDGraph le dg x =
20bbcc2b693b3040d7b8cc92ba966580637027d9cmaeder {- checks if it is an unexpanded referenced node
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa the function lookupInRefNodesDG only checks the
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder nodes which are not expanded. -}
e42249ec61f50a83525db6e5fc9f5c4dd1b4cf5fcmaeder case lookupInRefNodesDG x dg of
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder Just (refl, refn) ->
ea5ccb1c6e89486a54e1f4bd95840147e96093edChristian Maeder parents = getRefParents le refl refn
c8afa08a8bda589ef6670068dff0108464be4da7Christian Maeder {- important for those, who's doing redo/undo function:
c99b0eb6632087d502dd4269599c5aa68a148eebSimon Ulbricht notice that if the node is expanded, then it should be
b99c9606f2faafeabb3fa8c596992143a561c787Simon Ulbricht deleted out of the unexpanded map using
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa deleteFromRefNodesDG -}
df67ddf64192bfcae6ece65255ad796a17cbe532Christian Maeder auxDG = foldl (updateDGraphAux le x refl)
473f5af6e4803fbeecc814065952396f2501039bChristian Maeder{- | get all the parents, namely the related referenced nodes and the links
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder between them and the present to be expanded node.
526e7f36639cb58e3c99a54bea082499a6b04a25Christian MaedergetRefParents :: LibEnv -> LibName
7b21830970250ca6369b0ae60f34c990f9a5c5bfTill Mossakowski -> Node -- the present to be expanded node
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder -> [(LNode DGNodeLab, [DGLinkLab])]
18548c6cc2dff13bf9f5f08b3f6cde6ca914df1dChristian MaedergetRefParents le refl refn =
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder {- get the previous objects to the current one -}
64f5f0a8c38d5b2ba33b09e02e92b0e3f812d6d0Eugen Kuksa dg = lookupDGraph refl le
18548c6cc2dff13bf9f5f08b3f6cde6ca914df1dChristian Maeder pres = innDG dg refn
6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder in modifyPs dg pres
7710f7c3425e45af11af124ff37bec27229d24f7Christian Maeder{- | modify the parents to a better form.
2e2559f894aaa661b199e4fa00609f522bc5482aSimon Ulbricht e.g. if the list is like:
df67ddf64192bfcae6ece65255ad796a17cbe532Christian Maeder [(a, 1), (b, 1), (c, 2), (d, 2), (e, 2)]
be1ce1c2b2819ef32743136c13101f1927375311Christian Maeder which means that node 1 is related via links a and b, and node 2 is
6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder related via links c, d and e.
f674d7a58db3f991300a708f3799d80c369781f8Eugen Kuksa then to advoid too many checking by inserting, we can modify the list
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder above to a form like this:
5896f38ba2934056542cb7cb3e6359e88a622547Christian Maeder [(1, [a, b]), (2, [c, d, e])]
526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder which simplifies the inserting afterwards ;)
526e7f36639cb58e3c99a54bea082499a6b04a25Christian MaedermodifyPs :: DGraph -> [LEdge DGLinkLab] -> [(LNode DGNodeLab, [DGLinkLab])]
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian MaedermodifyPs dg ls =
6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder (\ (n, x) -> ((n, labDG dg n), x))
6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder $ modifyPsAux ls
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder modifyPsAux :: Ord a => [(a, t, b)] -> [(a, [b])]
e98c3d3efab62d97ebdeed52f4109d961f6432aaChristian Maeder modifyPsAux l =
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder Map.toList $ Map.fromListWith (++) [(k, [v]) | (k, _, v) <- l ]
8f9ac967da20be8d7782d2fc0a085dd42f79c0cbEugen Kuksa{- | the actual update function to insert a list of related parents to the
8f9ac967da20be8d7782d2fc0a085dd42f79c0cbEugen Kuksa present to be expanded node.
6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder It inserts the related referenced node firstly by calling addParentNode.
703004db20b23870f080c4d9640729b19b7c2288Eugen Kuksa Then it inserts the related links by calling addParentLinks
703004db20b23870f080c4d9640729b19b7c2288Eugen Kuksa Notice that nodes have to be added firstly, so that the links can be
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder connected to the inserted nodes ;), especially by adding to the change
5896f38ba2934056542cb7cb3e6359e88a622547Christian MaederupdateDGraphAux :: LibEnv -> Node -- the present to be expanded node
5896f38ba2934056542cb7cb3e6359e88a622547Christian Maeder -> LibName -> DGraph -> (LNode DGNodeLab, [DGLinkLab])
5fb6343a5a2b4bbc67bc83479c84a92d23d30edfChristian MaederupdateDGraphAux libenv n refl dg (pnl, pls) =
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder (auxDG, newN) = addParentNode libenv dg refl pnl
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder in addParentLinks auxDG newN n pls
18548c6cc2dff13bf9f5f08b3f6cde6ca914df1dChristian Maeder{- | add the given parent node into the current dgraph
18548c6cc2dff13bf9f5f08b3f6cde6ca914df1dChristian MaederaddParentNode :: LibEnv -> DGraph -> LibName
5fb6343a5a2b4bbc67bc83479c84a92d23d30edfChristian Maeder -> LNode DGNodeLab -- the referenced parent node
6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder -> (DGraph, Node)
12882fa70d12d9b56cbd850ccb4b724feb3c62d5Christian MaederaddParentNode libenv dg refl (refn, oldNodelab) =
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder To advoid the chain which is desribed in ticket 5, the parent node should
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder be a non referenced node firstly, so that the actual parent node can be
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder (nodelab, newRefl, newRefn) = if isDGRef oldNodelab then
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder tempRefl = dgn_libname oldNodelab
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder tempRefn = dgn_node oldNodelab
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder originDG = lookupDGraph tempRefl libenv
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder (labDG originDG tempRefn, tempRefl, tempRefn)
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder else (oldNodelab, refl, refn)
b87fb5d6d5aba8fc6d3c528f7da0af228ca76b02Eugen Kuksa Set the sgMap and tMap too.
dfa31ad230c88a66a9722c2a5ab23fe82c33f014Eugen Kuksa Notice for those who are doing undo/redo, because the DGraph is actually
b87fb5d6d5aba8fc6d3c528f7da0af228ca76b02Eugen Kuksa changed if the maps are changed ;)
b87fb5d6d5aba8fc6d3c528f7da0af228ca76b02Eugen Kuksa -- creates an empty GTh, please check the definition of this function
b87fb5d6d5aba8fc6d3c528f7da0af228ca76b02Eugen Kuksa -- because there can be some problem or errors at this place.
8723ec450f2e7a024230467c0c28a3f154905483cmaeder newGTh = case dgn_theory nodelab of
8723ec450f2e7a024230467c0c28a3f154905483cmaeder G_theory lid sig ind _ _ -> noSensGTheory lid sig ind
7b21830970250ca6369b0ae60f34c990f9a5c5bfTill Mossakowski refInfo = newRefInfo newRefl newRefn
e99cb5db53054d96bb97c9b8b130bd249802450eTill Mossakowski newRefNode = (newInfoNodeLab (dgn_name nodelab) refInfo newGTh)
83ce5f14d356cd62e98f4f674da7f11ea1869eb0Till Mossakowski { globalTheory = globalTheory nodelab }
e99cb5db53054d96bb97c9b8b130bd249802450eTill Mossakowski -- checks if this node exists in the current dg, if so, nothing needs to be
dfa31ad230c88a66a9722c2a5ab23fe82c33f014Eugen Kuksa case lookupInAllRefNodesDG refInfo dg of
8723ec450f2e7a024230467c0c28a3f154905483cmaeder Nothing -> let newN = getNewNodeDG dg in
8723ec450f2e7a024230467c0c28a3f154905483cmaeder ( changeDGH (addToRefNodesDG newN refInfo dg)
d3d8d20d41aaaa107cf2dfa4dd0434e6a08b22d5Till Mossakowski $ InsertNode (newN, newRefNode)
31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder Just extN -> (dg, extN)
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder{- | add a list of links between the given two node ids.
5d3978bb76c33d08d6297f69f10bbc04721ee3a5cmaederaddParentLinks :: DGraph -> Node -> Node -> [DGLinkLab] -> DGraph
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaederaddParentLinks dg src tgt ls =
1f0483f71bad0707f10293d0b4db4649aa93fb35Christian Maeder let oldLinks = map (\ (_, _, l) -> l)
1f0483f71bad0707f10293d0b4db4649aa93fb35Christian Maeder $ filter (\ (s, _, _) -> s == src) $ innDG dg tgt
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder newLinks = map (\ l -> l
c5b8b64377e24bcbf5cc108ca433cfbbd6235ba1Christian Maeder { dgl_id = defaultEdgeId
c5b8b64377e24bcbf5cc108ca433cfbbd6235ba1Christian Maeder , dgl_type = invalidateProof $ dgl_type l }) ls
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder in if null oldLinks then
6f9d360a425bdae3bd15289388e64c14a85eca43cmaeder changesDGH dg $ map (\ l -> InsertEdge (src, tgt, l)) newLinks
6f9d360a425bdae3bd15289388e64c14a85eca43cmaeder else dg -- assume ingoing links are already properly set
6f9d360a425bdae3bd15289388e64c14a85eca43cmaeder{- applies global decomposition to all unproven global theorem edges
c5b8b64377e24bcbf5cc108ca433cfbbd6235ba1Christian Maeder if possible -}
26acf851cacd7a31bdc9b25a42af9949942fa7c6Christian MaederglobDecomp :: LibName -> LibEnv -> LibEnv
293abe6af19382a456dbe612aef45054ef76832fcmaederglobDecomp ln proofStatus =
6f9d360a425bdae3bd15289388e64c14a85eca43cmaeder let dgraph = lookupDGraph ln proofStatus
8723ec450f2e7a024230467c0c28a3f154905483cmaeder globalThmEdges = labEdgesDG dgraph
e99cb5db53054d96bb97c9b8b130bd249802450eTill Mossakowski globDecompFromList ln globalThmEdges proofStatus
e5f71ad96ddbaafd3bf8ae0820df93e0db4b0527cmaeder{- auxiliary function for globDecomp (above)
8723ec450f2e7a024230467c0c28a3f154905483cmaeder actual implementation -}
1f0483f71bad0707f10293d0b4db4649aa93fb35Christian MaederglobDecompAux :: DGraph -> LEdge DGLinkLab -> DGraph
8723ec450f2e7a024230467c0c28a3f154905483cmaederglobDecompAux dgraph edge =
8723ec450f2e7a024230467c0c28a3f154905483cmaeder let newDGraph = globDecompForOneEdge dgraph edge
5d93620c37abd9c665d3fe532d4852d62dff4233Christian Maeder in groupHistory dgraph (globDecompRule edge) newDGraph
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder-- applies global decomposition to a single edge
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian MaederglobDecompForOneEdge :: DGraph -> LEdge DGLinkLab -> DGraph
5d93620c37abd9c665d3fe532d4852d62dff4233Christian MaederglobDecompForOneEdge dgraph edge@(source, target, edgeLab) = let
5d93620c37abd9c665d3fe532d4852d62dff4233Christian Maeder defEdgesToSource = filter (liftE isDefEdge) $ innDG dgraph source
232c13ff6847a6f2bac7163392f80ab692cd7774Christian Maeder paths = [edge] : map (: [edge]) defEdgesToSource
12882fa70d12d9b56cbd850ccb4b724feb3c62d5Christian Maeder (newGr, proof_basis) = foldl
4bd27a2cb9efd5d8ff00b5cf823487403add724ecmaeder (globDecompForOneEdgeAux target) (dgraph, emptyProofBasis) paths
5d93620c37abd9c665d3fe532d4852d62dff4233Christian Maeder provenEdge = (source, target, edgeLab
99b26e2ab8ba89bc9a050c1524137eb6269e2753Christian Maeder { dgl_type = setProof (Proven (globDecompRule edge) proof_basis)
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder $ dgl_type edgeLab
26acf851cacd7a31bdc9b25a42af9949942fa7c6Christian Maeder , dgl_origin = DGLinkProof })
6f9d360a425bdae3bd15289388e64c14a85eca43cmaeder in changesDGH newGr [DeleteEdge edge, InsertEdge provenEdge]
6f9d360a425bdae3bd15289388e64c14a85eca43cmaeder{- auxiliary function for globDecompForOneEdge (above)
99b26e2ab8ba89bc9a050c1524137eb6269e2753Christian Maeder actual implementation -}
6f9d360a425bdae3bd15289388e64c14a85eca43cmaederglobDecompForOneEdgeAux :: Node -> (DGraph, ProofBasis)
6f9d360a425bdae3bd15289388e64c14a85eca43cmaeder -> [LEdge DGLinkLab]
6f9d360a425bdae3bd15289388e64c14a85eca43cmaeder -> (DGraph, ProofBasis)
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder-- for each path an unproven localThm edge is inserted
4937a0e373f619dc520799923acec42db5da5eb3Eugen KuksaglobDecompForOneEdgeAux target (dgraph, proof_basis) path =
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder case path of
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder [] -> error "globDecompForOneEdgeAux"
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder (node, _, lbl) : rpath -> let
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder lbltype = dgl_type lbl
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder isHiding = isHidingDef lbltype
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder morphismPath = if isHiding then rpath else path
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder morphism = case calculateMorphismOfPath morphismPath of
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder Just morph -> morph
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder Nothing -> error "globDecomp: could not determine morphism of new edge"
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder defEdgesToTarget = filter
df24d7f0c79862ffd8189698645e201bf07a4d9cEugen Kuksa (\ (s, _, l) -> s == node && isGlobalDef (dgl_type l)
df24d7f0c79862ffd8189698645e201bf07a4d9cEugen Kuksa && dgl_morphism l == morphism)
feb9227bb5c49d5bea1a112500c3b3eba31abdfbcmaeder $ innDG dgraph target
df24d7f0c79862ffd8189698645e201bf07a4d9cEugen Kuksa newEdgeLbl = defDGLink morphism
df24d7f0c79862ffd8189698645e201bf07a4d9cEugen Kuksa (if isHiding then hidingThm $ dgl_morphism lbl
df24d7f0c79862ffd8189698645e201bf07a4d9cEugen Kuksa else if isGlobalDef lbltype then globalThm else localThm)
feb9227bb5c49d5bea1a112500c3b3eba31abdfbcmaeder newEdge = (node, target, newEdgeLbl)
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder in case defEdgesToTarget of
6f9d360a425bdae3bd15289388e64c14a85eca43cmaeder (_, _, dl) : _ | not isHiding
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder -> (dgraph, addEdgeId proof_basis $ dgl_id dl)
dfa31ad230c88a66a9722c2a5ab23fe82c33f014Eugen Kuksa _ | node == target && isInc (getRealDGLinkType newEdgeLbl)
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa && isGlobalDef lbltype
64f5f0a8c38d5b2ba33b09e02e92b0e3f812d6d0Eugen Kuksa -> (dgraph, addEdgeId proof_basis $ dgl_id lbl)
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa _ -> case tryToGetEdge newEdge dgraph of
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa Nothing -> let
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa newGraph = changeDGH dgraph $ InsertEdge newEdge
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa finalEdge = case getLastChange newGraph of
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa InsertEdge final_e -> final_e
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa _ -> error "Proofs.Global.globDecompForOneEdgeAux"
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa in (newGraph, addEdgeId proof_basis $ getEdgeId finalEdge)
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa Just e -> (dgraph, addEdgeId proof_basis $ getEdgeId e)
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen KuksaglobSubsumeFromList :: LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen KuksaglobSubsumeFromList ln globalThmEdges libEnv =
ab38e2fac740c4336afafbe0584053dc2e67002bEugen Kuksa let dgraph = lookupDGraph ln libEnv
dfa31ad230c88a66a9722c2a5ab23fe82c33f014Eugen Kuksa finalGlobalThmEdges = filter (liftE isUnprovenGlobalThm) globalThmEdges
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa nextDGraph = foldl
ab38e2fac740c4336afafbe0584053dc2e67002bEugen Kuksa (globSubsumeAux libEnv) dgraph finalGlobalThmEdges
ab38e2fac740c4336afafbe0584053dc2e67002bEugen Kuksa in Map.insert ln nextDGraph libEnv
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa-- | tries to apply global subsumption to all unproven global theorem edges
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen KuksaglobSubsume :: LibName -> LibEnv -> LibEnv
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen KuksaglobSubsume ln libEnv =
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa let dgraph = lookupDGraph ln libEnv
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa globalThmEdges = labEdgesDG dgraph
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa in globSubsumeFromList ln globalThmEdges libEnv
ab38e2fac740c4336afafbe0584053dc2e67002bEugen Kuksa{- auxiliary function for globSubsume (above) the actual implementation -}
dfa31ad230c88a66a9722c2a5ab23fe82c33f014Eugen KuksaglobSubsumeAux :: LibEnv -> DGraph -> LEdge DGLinkLab -> DGraph
e99cb5db53054d96bb97c9b8b130bd249802450eTill MossakowskiglobSubsumeAux libEnv dgraph ledge@(src, tgt, edgeLab) =
ab38e2fac740c4336afafbe0584053dc2e67002bEugen Kuksa let morphism = dgl_morphism edgeLab
dfa31ad230c88a66a9722c2a5ab23fe82c33f014Eugen Kuksa filteredPaths = filterPathsByMorphism morphism $ filter (noPath ledge)
ab38e2fac740c4336afafbe0584053dc2e67002bEugen Kuksa $ getAllGlobPathsBetween dgraph src tgt
ab38e2fac740c4336afafbe0584053dc2e67002bEugen Kuksa proofbasis = selectProofBasis dgraph ledge filteredPaths
ab38e2fac740c4336afafbe0584053dc2e67002bEugen Kuksa in if not (nullProofBasis proofbasis) || isIdentityEdge ledge libEnv dgraph
d16243f2fd4825f598eee589b68e324e23eb469dEugen Kuksa let globSubsumeRule = DGRuleWithEdge "Global-Subsumption" ledge
d16243f2fd4825f598eee589b68e324e23eb469dEugen Kuksa newEdge = (src, tgt, edgeLab
d16243f2fd4825f598eee589b68e324e23eb469dEugen Kuksa { dgl_type = setProof (Proven globSubsumeRule proofbasis)
ab38e2fac740c4336afafbe0584053dc2e67002bEugen Kuksa $ dgl_type edgeLab
ab38e2fac740c4336afafbe0584053dc2e67002bEugen Kuksa , dgl_origin = DGLinkProof })
ab38e2fac740c4336afafbe0584053dc2e67002bEugen Kuksa newDGraph = changesDGH dgraph [DeleteEdge ledge, InsertEdge newEdge]
64f5f0a8c38d5b2ba33b09e02e92b0e3f812d6d0Eugen Kuksa in groupHistory dgraph globSubsumeRule newDGraph