DevGraph.hs revision 1bc5dccbf0083a620ae1181c717fea75e4af5e5c
c63ebf815c8a874525cf18670ad74847f7fc7b26Christian MaederModule : $Header$
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaederDescription : Central datastructures for development graphs
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederCopyright : (c) Till Mossakowski, Uni Bremen 2002-2006
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederMaintainer : till@informatik.uni-bremen.de
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederStability : provisional
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederPortability : non-portable(Logic)
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederCentral datastructures for development graphs
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maeder Follows Sect. IV:4.2 of the CASL Reference Manual.
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder T. Mossakowski, S. Autexier and D. Hutter:
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Extending Development Graphs With Hiding.
a1ed34933c266ce85066acb0d7b20c90cb8eb213Christian Maeder H. Hussmann (ed.): Fundamental Approaches to Software Engineering 2001,
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder Lecture Notes in Computer Science 2029, p. 269-283,
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich Springer-Verlag 2001.
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder T. Mossakowski, S. Autexier, D. Hutter, P. Hoffman:
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich CASL Proof calculus. In: CASL reference manual, part IV.
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroederimport Data.Graph.Inductive.Graph as Graph
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroederimport qualified Data.Graph.Inductive.Query.DFS as DFS
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroederimport qualified Data.Graph.Inductive.Query.BFS as BFS
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroederimport qualified Common.Lib.Graph as Tree
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroederimport qualified Data.Map as Map
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroederimport qualified Common.OrderedMap as OMap
4b4a0b61b72cf8478a5d4d5002bca9f699401363Christian Maederimport Data.Char (toLower)
308834907a120fd8771e18292ed2ca9cd767c12dChristian Maederimport Data.List(find, intersect, partition)
9f226cec9f978edaba67aee4c4e04e3d3b994b87Daniel Calegari{- | returns one new node id for the given graph
6a2dad705deefd1b7a7e09b84fd2d75f2213be47Christian MaedergetNewNode :: Tree.Gr a b -> Node
a7c27282e71cf4505026645f96d4f5cb8a284e32Christian MaedergetNewNode g = case newNodes 1 g of
6aea82c63ba1d2efc0329bc784a14e521469ec20Christian Maeder{- | returns a list of edge ids with the given number of edge ids
4ba08bfca0cc8d9da65397b8dfd2654fdb4c0e62Christian Maeder and a specified graph.
431d34c7007a787331c4e5ec997badb0f8190fc7Christian MaedergetNewEdgeIDs :: Int -> DGraph -> EdgeID
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian MaedergetNewEdgeIDs count g = take count [(getNewEdgeID g)..]
db675e8302ddb0d6528088ce68f5e98a00e890e3Christian Maeder{- | tries to find the label of a link whose id is given in
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder a specified graph
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian MaedergetDGLinkLabWithIDs :: EdgeID -> DGraph -> Maybe DGLinkLab
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian MaedergetDGLinkLabWithIDs ids dgraph =
23ffcc44ca8612feccbd8fda63fa5be7ab5f9dc3Christian Maeder case getDGLEdgeWithIDs ids dgraph of
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder Just (_, _, label) -> Just label
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder Nothing -> Nothing
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder{- | tries to find a link, which includes the src, tgt node
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder and its label according to a given id in a specified graph.
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaedergetDGLEdgeWithIDs :: EdgeID -> DGraph -> Maybe (LEdge DGLinkLab)
9e748851c150e1022fb952bab3315e869aaf0214Christian MaedergetDGLEdgeWithIDs ids dgraph =
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder find (\ (_, _, label) -> isIdenticalEdgeID ids $ dgl_id label)
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder $ labEdges $ dgBody dgraph
dc679edd4ca027663212afdf00926ae2ce19b555Christian Maeder{- | returns whether two edge ids are identical to each other or not.
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder two edge ids are identical, only if their intersect
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder is not empty.
ca074a78b8dcccbb8c419586787882f98d0c6163Christian MaederisIdenticalEdgeID :: EdgeID -> EdgeID -> Bool
ca074a78b8dcccbb8c419586787882f98d0c6163Christian MaederisIdenticalEdgeID id1 id2 = not $ null $ intersect id1 id2
4017ebc0f692820736d796af3110c3b3018c108aChristian Maeder{- | similar to getDGLEdgeWithIDs, but an error will be thrown if
b568982efd0997d877286faa592d81b03c8c67b8Christian Maeder the specified edge is not found.
0be0db405c49906bd7057255069bf6df53395ac9Klaus LuettichgetDGLEdgeWithIDsForSure :: EdgeID -> DGraph -> (LEdge DGLinkLab)
ca074a78b8dcccbb8c419586787882f98d0c6163Christian MaedergetDGLEdgeWithIDsForSure ids dgraph =
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder case getDGLEdgeWithIDs ids dgraph of
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Nothing -> error ("ID: "++show ids ++
f2f9df2e17e70674f0bf426ed1763c973ee4cde0Christian Maeder "not found. Static.DevGraph.getDGLEdgeWithIDsForSure")
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder-- * Types for structured specification analysis
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder-- ??? Some info about the theorems already proved for a node
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder-- should be added
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- or should it be kept separately?
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder-- what about open theorems of a node???
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- | name of a node in a DG; auxiliary nodes may have extension string
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder-- and non-zero number (for these, names are usually hidden)
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maedertype NODE_NAME = (SIMPLE_ID, String, Int)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederdata DGNodeInfo = DGNode
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder { node_origin :: DGOrigin -- origin in input language
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder , node_cons :: Conservativity
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder , node_cons_status :: ThmLinkStatus }
3e8b136f23ed57d40ee617f49bcac37830b58cabChristian Maeder | DGRef -- reference to node in a different DG
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder { ref_libname :: LIB_NAME -- pointer to DG where ref'd node resides
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder , ref_node :: Node -- pointer to ref'd node
58b96b17bf8e32c0b0d773380a5e62f992eef2bcChristian Maeder } deriving (Show, Eq)
363939beade943a02b31004cea09dec34fa8a6d9Christian Maederdgn_origin :: DGNodeLab -> DGOrigin
58b96b17bf8e32c0b0d773380a5e62f992eef2bcChristian Maederdgn_origin = node_origin . nodeInfo
eb74267cf39e4e95f9eeb5c765f4c8dac33971b4Christian Maederdgn_cons :: DGNodeLab -> Conservativity
eb74267cf39e4e95f9eeb5c765f4c8dac33971b4Christian Maederdgn_cons = node_cons . nodeInfo
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maederdgn_cons_status :: DGNodeLab -> ThmLinkStatus
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maederdgn_cons_status = node_cons_status . nodeInfo
8d178ae08a52d61379e6b8074f61646499bc88bbChristian Maederdgn_libname :: DGNodeLab -> LIB_NAME
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maederdgn_libname = ref_libname . nodeInfo
6cd33d6101fb1b93baa6d86fac158af18a115108Christian Maederdgn_node :: DGNodeLab -> Node
6cd33d6101fb1b93baa6d86fac158af18a115108Christian Maederdgn_node = ref_node . nodeInfo
6cd33d6101fb1b93baa6d86fac158af18a115108Christian Maeder-- | node inscriptions in development graphs
b2ac5a92cf36382e8deea5661c1964566caf72b3Christian Maederdata DGNodeLab =
b2ac5a92cf36382e8deea5661c1964566caf72b3Christian Maeder { dgn_name :: NODE_NAME -- name in the input language
b2ac5a92cf36382e8deea5661c1964566caf72b3Christian Maeder , dgn_theory :: G_theory -- local theory
7d0ee72ee91ec305408688b969c43f07b9667c80Christian Maeder , dgn_nf :: Maybe Node -- normal form, for Theorem-Hide-Shift
7d0ee72ee91ec305408688b969c43f07b9667c80Christian Maeder , dgn_sigma :: Maybe GMorphism -- inclusion of signature into nf signature
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder , nodeInfo :: DGNodeInfo
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder , dgn_lock :: Maybe (MVar ())
0e5b095a19790411e5352fa7cf57cb0388e70472Christian Maeder } deriving (Show, Eq)
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederinstance Show (MVar ()) where
f1a913f880e409e7327b5deae95738b5448379a1Christian Maederdgn_sign :: DGNodeLab -> G_sign
f1a913f880e409e7327b5deae95738b5448379a1Christian Maederdgn_sign dn = case dgn_theory dn of
14c56dc499da4bbeaeebeb558ceb755150ae341cChristian Maeder G_theory lid sig ind _ _-> G_sign lid sig ind
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaederisInternalNode :: DGNodeLab -> Bool
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederisInternalNode l@DGNodeLab {dgn_name = n} =
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder if isDGRef l then null $ show $ getName n else isInternal n
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder-- | test for 'LeftOpen', return input for refs or no conservativity
93f5b72fdb9ee734caa750b43dd79bbb590dcd73Christian MaederhasOpenConsStatus :: Bool -> DGNodeLab -> Bool
93f5b72fdb9ee734caa750b43dd79bbb590dcd73Christian MaederhasOpenConsStatus b dgn = if isDGRef dgn then b else
328a85c807f2a95c3f147d10b05927eaf862ebebChristian Maeder case dgn_cons dgn of
06dd4e7c29f33f6122a910719e3bd9062256e397Andy Gimblett _ -> case dgn_cons_status dgn of
254df6f22d01eacf7c57b85729e0445747b630d9Christian Maeder LeftOpen -> True
5b818f10e11fc79def1fdd5c8a080d64a6438d87Christian Maeder-- | gets the type of a development graph edge as a string
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix ReckersgetDGNodeType :: DGNodeLab -> String
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaedergetDGNodeType dgnodelab =
819e29dba060687cf391e444e0f6ff88c1908cc3Christian Maeder (if hasOpenGoals dgnodelab then id else ("locallyEmpty__" ++))
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder $ if isDGRef dgnodelab then "dg_ref" else
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder (if hasOpenConsStatus False dgnodelab
140287998aa8592c9c403bd9e308e447ba92ae11Christian Maeder then "open_cons__"
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder else "proven_cons__")
0d0278c34a374b29c2d6c58b39b8b56e283d48e8Christian Maeder ++ if isInternalNode dgnodelab
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder then "internal"
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder-- gets the name of a development graph node as a string
9e748851c150e1022fb952bab3315e869aaf0214Christian MaedergetDGNodeName :: DGNodeLab -> String
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaedergetDGNodeName dgn = showName $ dgn_name dgn
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaederemptyNodeName :: NODE_NAME
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian MaederemptyNodeName = (mkSimpleId "", "", 0)
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian MaedershowInt :: Int -> String
3554301a34639efb6c9961a8571775d0061284c9Christian MaedershowInt i = if i == 0 then "" else show i
3554301a34639efb6c9961a8571775d0061284c9Christian MaedershowName :: NODE_NAME -> String
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian MaedershowName (n, s, i) = show n ++ if ext == "" then "" else "_" ++ ext
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder where ext = s ++ showInt i
aded505f9b42cc38975559c2a5d175ae95de436bChristian MaedermakeName :: SIMPLE_ID -> NODE_NAME
aded505f9b42cc38975559c2a5d175ae95de436bChristian MaedermakeName n = (n, "", 0)
aded505f9b42cc38975559c2a5d175ae95de436bChristian MaedergetName :: NODE_NAME -> SIMPLE_ID
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian MaedergetName (n, _, _) = n
a14767aeac3e78ed100f5b75e210ba563ee10dbaChristian MaedermakeMaybeName :: Maybe SIMPLE_ID -> NODE_NAME
a14767aeac3e78ed100f5b75e210ba563ee10dbaChristian MaedermakeMaybeName Nothing = emptyNodeName
a14767aeac3e78ed100f5b75e210ba563ee10dbaChristian MaedermakeMaybeName (Just n) = makeName n
3554301a34639efb6c9961a8571775d0061284c9Christian Maederinc :: NODE_NAME -> NODE_NAME
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maederinc (n, s, i) = (n, s, i+1)
54ea981a0503c396c2923a1c06421c6235baf27fChristian MaederisInternal :: NODE_NAME -> Bool
54ea981a0503c396c2923a1c06421c6235baf27fChristian MaederisInternal (_, s, i) = i /= 0 || s /= ""
db6729e623b4053149084ccf4b35e5308ac7e359Christian MaederextName :: String -> NODE_NAME -> NODE_NAME
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian MaederextName s (n, s1, i) = (n, s1 ++ showInt i ++ s, 0)
aded505f9b42cc38975559c2a5d175ae95de436bChristian MaederisDGRef :: DGNodeLab -> Bool
f9e0b18852b238ddb649d341194e05d7200d1bbeChristian MaederisDGRef l = case nodeInfo l of
819e29dba060687cf391e444e0f6ff88c1908cc3Christian Maeder DGNode {} -> False
819e29dba060687cf391e444e0f6ff88c1908cc3Christian Maeder DGRef {} -> True
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder-- | test if a given node label has local open goals
254df6f22d01eacf7c57b85729e0445747b630d9Christian MaederhasOpenGoals :: DGNodeLab -> Bool
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian MaederhasOpenGoals dgn =
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder case dgn_theory dgn of
254df6f22d01eacf7c57b85729e0445747b630d9Christian Maeder G_theory _lid _sigma _ sens _->
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder (\s -> not (isAxiom s) && not (isProvenSenStatus s) ) sens
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder{- | an edge id is represented as a list of ints.
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder the reason of an edge can have multiple ids is, for example, there exists
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder an proven edge e1 with id 1 and an unproven edge e2 with id 2 between
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder two nodes. Now after applying some rules e2 is proven, but it's actually
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder the same as the proven edge e1, then the proven e2 should not be inserted
ac34194a668399bb8ef238da77c3a09e93fb253bChristian Maeder into the graph again, but e1 will take e2's id 2 because 2 is probably
4fc9de0da898448f1d3597ebbd8c04a066464c21Christian Maeder saved in some other places. As a result, e1 would have 1 and 2 as its id.
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder This type can be extended to a more complicated struture, like a tree
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder suggested by Till.
c208973c890b8f993297720fd0247bc7481d4304Christian Maedertype EdgeID = [Int]
0d0278c34a374b29c2d6c58b39b8b56e283d48e8Christian Maeder-- | link inscriptions in development graphs
0d0278c34a374b29c2d6c58b39b8b56e283d48e8Christian Maederdata DGLinkLab = DGLink
1842453990fed8a1bd7a5ac792d7982c1d2bfcd5Christian Maeder { dgl_morphism :: GMorphism -- signature morphism of link
0d0278c34a374b29c2d6c58b39b8b56e283d48e8Christian Maeder , dgl_type :: DGLinkType -- type: local, global, def, thm?
1842453990fed8a1bd7a5ac792d7982c1d2bfcd5Christian Maeder , dgl_origin :: DGOrigin -- origin in input language
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder , dgl_id :: EdgeID -- id of the edge
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder } deriving Show
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder-- | create a default ID which has to be changed when inserting a certain edge.
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaederdefaultEdgeID :: EdgeID
01e278bdd7dce13b9303ed3d79683d83c89d09f9Liam O'ReillydefaultEdgeID = []
5ad5dffe06818a13e1632b1119fbca7881085fc1Dominik Luecke{- | Eq instance definition of DGLinkLab.
8c812cd83569e973f10cf69a342424ceabc07af9Christian Maeder Notice that the dgl_id is not compared here, because
8c812cd83569e973f10cf69a342424ceabc07af9Christian Maeder by comparing of two label the edge id should not
8c812cd83569e973f10cf69a342424ceabc07af9Christian Maeder play any role.
31d6d9286988dc31639d105841296759aeb743e0Jonathan von Schroederinstance Eq DGLinkLab where
1535e1d8c82db5f7e2402261983c4c2ef39f4f39Mihai Codescu l1 == l2 = dgl_morphism l1 == dgl_morphism l2
7a3fe82695aa32657693e05712f84d7f81672f2eJonathan von Schroeder && dgl_type l1 == dgl_type l2
7a3fe82695aa32657693e05712f84d7f81672f2eJonathan von Schroeder && dgl_origin l1 == dgl_origin l2
7a3fe82695aa32657693e05712f84d7f81672f2eJonathan von Schroederinstance Pretty DGLinkLab where
05a206508bc898f87fe6ab6e069814df3c29d303Dominik Luecke pretty l = fsep [ pretty (dgl_morphism l)
05a206508bc898f87fe6ab6e069814df3c29d303Dominik Luecke , pretty (dgl_type l)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder , pretty (dgl_origin l)]
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder{- | checks if the given edge is contained in the given
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder list of EdgeIDs.
d54cd08a4cfa26256c38d8ed12c343adbfe1a0e3Christian MaederroughElem :: LEdge DGLinkLab -> [EdgeID] -> Bool
d54cd08a4cfa26256c38d8ed12c343adbfe1a0e3Christian MaederroughElem (_, _, label) =
3b06e23643a9f65390cb8c1caabe83fa7e87a708Till Mossakowski any (\ edgeID -> isIdenticalEdgeID edgeID $ dgl_id label)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder{- | the edit operations of the DGraph
0b349288edfa50fdf38fda1a14e1562d03f92574Christian Maederdata DGChange = InsertNode (LNode DGNodeLab)
5afff1a0f62394414c33b06141175b3ab0b117a5Christian Maeder | DeleteNode (LNode DGNodeLab)
5afff1a0f62394414c33b06141175b3ab0b117a5Christian Maeder | InsertEdge (LEdge DGLinkLab)
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder | DeleteEdge (LEdge DGLinkLab)
1b3a2f98d1cd01fc9e0591f69507e20526727559Dominik Luecke -- it contains the old label and new label with node
f04e8f3ff56405901be968fd4c6e9769239f1a9bKlaus Luettich | SetNodeLab DGNodeLab (LNode DGNodeLab)
ea3bff3e547a1ac714d4db39c5efef95e02b2e7dChristian Maederinstance Show DGChange where
dd6f22b9dcff2695181b86372e4df03d5b96e92dKristina Sojakova show (InsertNode (n, _)) = "InsertNode "++show n -- ++show l
005e0f0c6b0cc898003b03801158c208f3071fc5Kristina Sojakova show (DeleteNode (n, _)) = "DeleteNode "++show n -- ++show l
abf2487c3aece95c371ea89ac64319370dcb6483Klaus Luettich show (InsertEdge (n,m, _)) = "InsertEdge "++show n++"->"++show m -- ++show l
23b4e542dca35852f58d1fb3f7d9078c1de5ab06Christian Maeder show (DeleteEdge (n,m, _)) = "DeleteEdge "++show n++"->"++show m -- ++show l
23b4e542dca35852f58d1fb3f7d9078c1de5ab06Christian Maeder show (SetNodeLab _ (n, _)) = "SetNodeLab of " ++ show n
76b9b2974795a6fb31f242fd032de3ff66df6204Christian Maeder-- | Link types of development graphs
74a992bd019d3319df2f21f9d358ff06cafb5f7eMihaela Turcu-- Sect. IV:4.2 of the CASL Reference Manual explains them in depth
8a78868bae2ec6838c87366c35c57e109154c51eChristian Maederdata DGLinkType = LocalDef
c2e192ace9ef7cfb0e59563f1b24477b2b65cff3Dominik Dietrich | FreeDef MaybeNode -- the "parameter" node
6b75c206b317eb30a08d88a8f27e0295ffeb1546Christian Maeder | CofreeDef MaybeNode -- the "parameter" node
9a4b469ca0a7f44a598e551a973c75195207db58Eugen Kuksa | LocalThm ThmLinkStatus Conservativity ThmLinkStatus
48aa0645e25883048369afc02aac3f49b14a50daChristian Maeder -- ??? Some more proof information is needed here
01645eac73dbc789392674930adc5745c935f3a0Christian Maeder -- (proof tree, ...)
01645eac73dbc789392674930adc5745c935f3a0Christian Maeder | GlobalThm ThmLinkStatus Conservativity ThmLinkStatus
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder | HidingThm GMorphism ThmLinkStatus
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder | FreeThm GMorphism ThmLinkStatus
3a9fce5398f4621558ca220c66c87cee59adc258Jonathan von Schroeder -- DGLink S1 S2 m2 (DGLinkType m1 p) n
b5da047a9a875dec3f968b6c0df96af326f90fa9Alexis Tsogias -- corresponds to a span of morphisms
0a03acf9fa28e6ff00f4d7c9c6acbae64cf09c56Ewaryst Schulz -- S1 <--m1-- S --m2--> S2
0a03acf9fa28e6ff00f4d7c9c6acbae64cf09c56Ewaryst Schulz deriving (Eq,Show)
308834907a120fd8771e18292ed2ca9cd767c12dChristian MaederthmLinkStatus :: DGLinkType -> Maybe ThmLinkStatus
308834907a120fd8771e18292ed2ca9cd767c12dChristian MaederthmLinkStatus (LocalThm s _ _) = Just s
7834a982096d93301a4626f444dd9ea5f9fe17eaChristian MaederthmLinkStatus (GlobalThm s _ _) = Just s
1f9274bb2aa44ea236327814dce99946be52e348Felix Gabriel MancethmLinkStatus (HidingThm _ s) = Just s
1f9274bb2aa44ea236327814dce99946be52e348Felix Gabriel MancethmLinkStatus (FreeThm _ s) = Just s
bab2d88d650448628730ed3b65c9f99c52500e8cChristian MaederthmLinkStatus _ = Nothing
4b4a0b61b72cf8478a5d4d5002bca9f699401363Christian Maederinstance Pretty DGLinkType where
9f226cec9f978edaba67aee4c4e04e3d3b994b87Daniel Calegari pretty t = text $ case t of
9f226cec9f978edaba67aee4c4e04e3d3b994b87Daniel Calegari LocalDef -> "LocalDef"
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder GlobalDef -> "GlobalDef"
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder HidingDef -> "HidingDef"
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder FreeDef _ -> "FreeDef"
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder CofreeDef _ -> "CofreeDef"
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder LocalThm s _ _ -> "LocalThm" ++ getThmTypeAux s
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder GlobalThm s _ _ -> "GlobalThm" ++ getThmTypeAux s
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder HidingThm _ s -> "HidingThm" ++ getThmTypeAux s
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder FreeThm _ s -> "FreeThm" ++ getThmTypeAux s
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder-- | describe the link type of the label
7a3fe82695aa32657693e05712f84d7f81672f2eJonathan von SchroedergetDGLinkType :: DGLinkLab -> String
7a3fe82695aa32657693e05712f84d7f81672f2eJonathan von SchroedergetDGLinkType lnk = let
7a3fe82695aa32657693e05712f84d7f81672f2eJonathan von Schroeder isHom = isHomogeneous $ dgl_morphism lnk
1535e1d8c82db5f7e2402261983c4c2ef39f4f39Mihai Codescu het = if isHom then id else ("het" ++)
1535e1d8c82db5f7e2402261983c4c2ef39f4f39Mihai Codescu in case dgl_morphism lnk of
1535e1d8c82db5f7e2402261983c4c2ef39f4f39Mihai Codescu GMorphism _ _ _ _ _ ->
1535e1d8c82db5f7e2402261983c4c2ef39f4f39Mihai Codescu case dgl_type lnk of
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder GlobalDef -> if isHom then "globaldef"
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder else "hetdef"
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder HidingDef -> "hidingdef"
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder LocalThm s _ _ -> het "local" ++ getThmType s ++ "thm"
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder GlobalThm s _ _ -> het $ getThmType s ++ "thm"
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder HidingThm _ s -> getThmType s ++ "hidingthm"
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder FreeThm _ s -> getThmType s ++ "thm"
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder _ -> "def" -- LocalDef, FreeDef, CofreeDef
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder-- | Conservativity annotations. For compactness, only the greatest
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder-- applicable value is used in a DG
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroederdata Conservativity = None | Cons | Mono | Def deriving (Eq,Ord)
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroederinstance Show Conservativity where
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder show Cons = "Cons"
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder show Mono = "Mono"
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder show Def = "Def"
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder-- | Rules in the development graph calculus,
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder-- Sect. IV:4.4 of the CASL Reference Manual explains them in depth
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder TheoremHideShift
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder | HideTheoremShift (LEdge DGLinkLab)
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder | GlobDecomp (LEdge DGLinkLab) -- edge in the conclusion
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder | LocDecomp (LEdge DGLinkLab)
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder | LocInference (LEdge DGLinkLab)
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder | GlobSubsumption (LEdge DGLinkLab)
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder | Composition [LEdge DGLinkLab]
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder | LocalInference
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder | BasicInference AnyComorphism BasicProof -- coding and proof tree. obsolete?
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder | BasicConsInference Edge BasicConsProof
5199920ca3b698b2149c8cb9d2ce2e98a280ff9dChristian Maeder deriving (Show, Eq)
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maederinstance Pretty DGRule where
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder pretty r = case r of
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder TheoremHideShift -> text "Theorem-Hide-Shift"
9f85afecbd79b3df5a0bb17bd28cd0b288dc3213Kristina Sojakova HideTheoremShift l -> text "Hide-Theorem-Shift; resulting link:"
48aa0645e25883048369afc02aac3f49b14a50daChristian Maeder <+> printLEdgeInProof l
9f85afecbd79b3df5a0bb17bd28cd0b288dc3213Kristina Sojakova Borrowing -> text "Borrowing"
79834070d6d3c63a098e570b12fa3405c607dc70Kristina Sojakova ConsShift -> text "Cons-Shift"
79834070d6d3c63a098e570b12fa3405c607dc70Kristina Sojakova DefShift -> text "Def-Shift"
79834070d6d3c63a098e570b12fa3405c607dc70Kristina Sojakova MonoShift -> text "Mono-Shift"
23b4e542dca35852f58d1fb3f7d9078c1de5ab06Christian Maeder DefToMono -> text "DefToMono"
23b4e542dca35852f58d1fb3f7d9078c1de5ab06Christian Maeder MonoToCons -> text "MonoToCons"
23b4e542dca35852f58d1fb3f7d9078c1de5ab06Christian Maeder FreeIsMono -> text "FreeIsMono"
8a78868bae2ec6838c87366c35c57e109154c51eChristian Maeder MonoIsFree -> text "MonoIsFree"
8a78868bae2ec6838c87366c35c57e109154c51eChristian Maeder GlobDecomp l -> text "Global Decomposition; resulting link:"
8a78868bae2ec6838c87366c35c57e109154c51eChristian Maeder <+> printLEdgeInProof l
624e6701e0deb7ac6c03c0cba0190fbc5033cf93Ewaryst Schulz LocDecomp l -> text "Local Decomposition; resulting link:"
624e6701e0deb7ac6c03c0cba0190fbc5033cf93Ewaryst Schulz <+> printLEdgeInProof l
c2e192ace9ef7cfb0e59563f1b24477b2b65cff3Dominik Dietrich LocInference l -> text "Local Inference; resulting link:"
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Luc <+> printLEdgeInProof l
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Luc GlobSubsumption l -> text "Global Subsumption; resulting link:"
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Luc <+> printLEdgeInProof l
01645eac73dbc789392674930adc5745c935f3a0Christian Maeder Composition ls ->
01645eac73dbc789392674930adc5745c935f3a0Christian Maeder text "Composition" <+> vcat (map printLEdgeInProof ls)
01645eac73dbc789392674930adc5745c935f3a0Christian Maeder LocalInference -> text "Local Inference"
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder BasicInference c bp -> text "Basic Inference using:"
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder <+> text ("Comorphism: "++show c ++ "Proof tree: "++show bp)
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder BasicConsInference _ bp -> text "Basic Cons-Inference using:"
b5da047a9a875dec3f968b6c0df96af326f90fa9Alexis Tsogias <+> text (show bp)
b5da047a9a875dec3f968b6c0df96af326f90fa9Alexis TsogiasprintLEdgeInProof :: LEdge DGLinkLab -> Doc
0a03acf9fa28e6ff00f4d7c9c6acbae64cf09c56Ewaryst SchulzprintLEdgeInProof (s,t,l) =
0a03acf9fa28e6ff00f4d7c9c6acbae64cf09c56Ewaryst Schulz pretty s <> text "-->" <> pretty t <> text ":"
0a03acf9fa28e6ff00f4d7c9c6acbae64cf09c56Ewaryst Schulz <+> printLabInProof l
18d370f8341357f5d6a4068f4bb6981173ece70fFelix Gabriel ManceprintLabInProof :: DGLinkLab -> Doc
7834a982096d93301a4626f444dd9ea5f9fe17eaChristian MaederprintLabInProof l =
ed1b8e97e72b2e3e92edaf2eb22a4b5373d705f1Felix Gabriel Mance fsep [ pretty (dgl_type l)
ed1b8e97e72b2e3e92edaf2eb22a4b5373d705f1Felix Gabriel Mance , text "with origin:"
0a03acf9fa28e6ff00f4d7c9c6acbae64cf09c56Ewaryst Schulz , pretty (dgl_origin l) <> comma
4b4a0b61b72cf8478a5d4d5002bca9f699401363Christian Maeder , text "and morphism:"
fc1bf40b1196cf62c6ce5c971633b5ebfc5936efChristian Maeder , pretty (dgl_morphism l)
9f226cec9f978edaba67aee4c4e04e3d3b994b87Daniel Calegaridata BasicConsProof = BasicConsProof -- more detail to be added ...
9f226cec9f978edaba67aee4c4e04e3d3b994b87Daniel Calegari deriving (Show, Eq)
c70ef4c3b3a62764f715510c9fd67dde3acfe454Christian Maederdata ThmLinkStatus = LeftOpen
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder | Proven DGRule [EdgeID]
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder --[LEdge DGLinkLab] -- Proven DGRule Int
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers deriving (Show, Eq)
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maederinstance Pretty ThmLinkStatus where
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder pretty tls = case tls of
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder LeftOpen -> text "Open"
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder Proven r ls -> fsep [ text "Proven with rule"
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder , text "Proof based on links:"
cc07a598b995acc9436651e66fd18009509047efChristian Maeder ] $+$ vcat(map printOneProofBasis ls)
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder --] $+$ vcat(map printLEdgeInProof ls)
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederprintOneProofBasis :: EdgeID -> Doc
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederprintOneProofBasis pb = pretty pb
50c3cc2b79207355522c5b096172b3c6b7bec300Christian Maeder-- | shows short theorem link status
f443a57f2a8e0ca3daa7431b0c89a18ba52c337aChristian MaedergetThmType :: ThmLinkStatus -> String
f5c9b1e739228c2a2edf055ac419583412569683Christian MaedergetThmType = map toLower . getThmTypeAux
37a9d042e9f85a1d6e229eb80b48f93df810f155Christian MaedergetThmTypeAux :: ThmLinkStatus -> String
7c99e334446bb97120e30e967baeeddfdd1278deKlaus LuettichgetThmTypeAux s = case s of
f5c9b1e739228c2a2edf055ac419583412569683Christian Maeder LeftOpen -> "Unproven"
f5c9b1e739228c2a2edf055ac419583412569683Christian Maeder _ -> "Proven"
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder{- | Data type indicating the origin of nodes and edges in the input language
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder This is not used in the DG calculus, only may be used in the future
33d042fe6a9eb27a4c48f840b80838f3e7d98e34Christian Maeder for reconstruction of input and management of change. -}
83394c6b6e6de128e71b67c9251ed7a84485d082Christian Maederdata DGOrigin = DGBasic | DGExtension | DGTranslation | DGUnion | DGHiding
fa21fba9ceb1ddf7b3efd54731a12ed8750191d8Christian Maeder | DGRevealing | DGRevealTranslation | DGFree | DGCofree
fa21fba9ceb1ddf7b3efd54731a12ed8750191d8Christian Maeder | DGLocal | DGClosed | DGClosedLenv | DGLogicQual
0c355dd0b739631ee472f9a656e266be27fa4e64Christian Maeder | DGFormalParams | DGImports | DGSpecInst SIMPLE_ID | DGFitSpec
fa21fba9ceb1ddf7b3efd54731a12ed8750191d8Christian Maeder | DGView SIMPLE_ID | DGFitView SIMPLE_ID | DGFitViewImp SIMPLE_ID
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder | DGFitViewA SIMPLE_ID | DGFitViewAImp SIMPLE_ID | DGProof
c7ec85d1103173e089aa5048fd7afb2f9b505124Klaus Luettich | DGintegratedSCC | DGEmpty
c7ec85d1103173e089aa5048fd7afb2f9b505124Klaus Luettichinstance Show DGOrigin where
c7ec85d1103173e089aa5048fd7afb2f9b505124Klaus Luettich show o = case o of
810746aea00b81c1eec27dae84d73a43599ff056Christian Maeder DGBasic -> "basic specification"
a883cd4d01fe39d23219cf5333425f195be24d8bChristian Maeder DGExtension -> "extension"
b905126bab9454b89041f92b3c50bb9efc85e427Klaus Luettich DGTranslation -> "translation"
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder DGUnion -> "union"
33d042fe6a9eb27a4c48f840b80838f3e7d98e34Christian Maeder DGHiding -> "hiding"
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder DGRevealing -> "revealing"
0a5571c8adeddd27548445546491725beb224dddChristian Maeder DGRevealTranslation -> "translation part of a revealing"
0a5571c8adeddd27548445546491725beb224dddChristian Maeder DGFree -> "free specification"
0a5571c8adeddd27548445546491725beb224dddChristian Maeder DGCofree -> "cofree specification"
0a5571c8adeddd27548445546491725beb224dddChristian Maeder DGLocal -> "local specification"
0a5571c8adeddd27548445546491725beb224dddChristian Maeder DGClosed -> "closed specification"
f38b3687c5558128515e34fb85d8b466d22dc300Christian Maeder DGClosedLenv -> "closed specification (inclusion of local environment)"
e112e83352048f3db8c8f93ae104193e7338c10fChristian Maeder DGLogicQual -> "specification with logic qualifier"
f38b3687c5558128515e34fb85d8b466d22dc300Christian Maeder DGFormalParams -> "formal parameters of a generic specification"
f38b3687c5558128515e34fb85d8b466d22dc300Christian Maeder DGImports -> "imports of a generic specification"
e642ad0e782f9bb9ba310164358220402eec8cd8Christian Maeder DGSpecInst n -> "instantiation of " ++ tokStr n
f38b3687c5558128515e34fb85d8b466d22dc300Christian Maeder DGFitSpec -> "fittig specification"
f38b3687c5558128515e34fb85d8b466d22dc300Christian Maeder DGView n -> "view " ++ tokStr n
db3016fbc6065fc0d57e68c28ae280e6ac95a39aChristian Maeder DGFitView n -> "fitting view " ++ tokStr n
ef67402074be14deb95e4ff564737d5593144130Klaus Luettich DGFitViewImp n -> "fitting view (imports) " ++ tokStr n
e112e83352048f3db8c8f93ae104193e7338c10fChristian Maeder DGFitViewA n -> "fitting view (actual parameters) " ++ tokStr n
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder DGFitViewAImp n ->
aebb0b18fe5e6ba7dd7e4c66a16a905611ef7ba9Christian Maeder "fitting view (imports and actual parameters) " ++ tokStr n
e05fd774e0181e93963d4302303b20698603a505Christian Maeder DGProof -> "constructed within a proof"
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder DGEmpty -> "empty specification"
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder DGData -> "data specification"
825a1e4ca1e768de4b4883c65a6cb1dce6aa0002Christian Maeder DGintegratedSCC ->
825a1e4ca1e768de4b4883c65a6cb1dce6aa0002Christian Maeder "OWL spec with integrated strongly connected components"
825a1e4ca1e768de4b4883c65a6cb1dce6aa0002Christian Maederinstance Pretty DGOrigin where
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder pretty = text . show
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder-- | Node with signature in a DG
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroederdata NodeSig = NodeSig Node G_sign deriving (Show, Eq)
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder{- | NodeSig or possibly the empty sig in a logic
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder (but since we want to avoid lots of vacuous nodes with empty sig,
e05fd774e0181e93963d4302303b20698603a505Christian Maeder we do not assign a real node in the DG here) -}
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maederdata MaybeNode = JustNode NodeSig | EmptyNode AnyLogic deriving (Show, Eq)
1dfba1f850f6a43094962b459998d1ea11472461Christian Maederinstance Pretty NodeSig where
1dfba1f850f6a43094962b459998d1ea11472461Christian Maeder pretty (NodeSig n sig) =
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder text "node" <+> pretty n <> colon <> pretty sig
e7757995211bd395dc79d26fe017d99375f7d2a6Christian MaederemptyG_sign :: AnyLogic -> G_sign
99afa6000472f3d291fdf9193ea19d334a58658dChristian MaederemptyG_sign (Logic lid) = G_sign lid (ext_empty_signature lid) 0
99afa6000472f3d291fdf9193ea19d334a58658dChristian MaedergetSig :: NodeSig -> G_sign
5bb7eeaca10ea76595229375f907a5a388b7c882Christian MaedergetSig (NodeSig _ sigma) = sigma
5bb7eeaca10ea76595229375f907a5a388b7c882Christian MaedergetNode :: NodeSig -> Node
c59d1c38ef94b4fb1c8d9fda9573bc1e1d2801e7Christian MaedergetNode (NodeSig n _) = n
99afa6000472f3d291fdf9193ea19d334a58658dChristian MaedergetMaybeSig :: MaybeNode -> G_sign
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian MaedergetMaybeSig (JustNode ns) = getSig ns
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaedergetMaybeSig (EmptyNode l) = emptyG_sign l
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus LuettichgetLogic :: MaybeNode -> AnyLogic
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus LuettichgetLogic (JustNode ns) = getNodeLogic ns
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus LuettichgetLogic (EmptyNode l) = l
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus LuettichgetNodeLogic :: NodeSig -> AnyLogic
36f63902db2b3463faa9f59912ad106e2d5aaa24Klaus LuettichgetNodeLogic (NodeSig _ (G_sign lid _ _)) = Logic lid
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus LuettichnewNodeInfo :: DGOrigin -> DGNodeInfo
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus LuettichnewNodeInfo orig = DGNode
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich { node_origin = orig
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich , node_cons = None
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder , node_cons_status = LeftOpen }
810746aea00b81c1eec27dae84d73a43599ff056Christian MaedernewRefInfo :: LIB_NAME -> Node -> DGNodeInfo
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian MaedernewRefInfo ln n = DGRef
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers { ref_libname = ln
1365c420ef71be3d52796ebd369dc2defdedc822Christian Maeder , ref_node = n }
82e29b77f0ef4cccd7ed734692c5e1e93dbbc645Christian MaedernewInfoNodeLab :: NODE_NAME -> DGNodeInfo -> G_theory -> DGNodeLab
a80c28bb8b7a23ccdf7e08d0fe216fc19cc97273Klaus LuettichnewInfoNodeLab name info gTh = DGNodeLab
5f0e3e4cb7dd31033c9682cafa712d2a66b2f3bcChristian Maeder { dgn_name = name
5f0e3e4cb7dd31033c9682cafa712d2a66b2f3bcChristian Maeder , dgn_theory = gTh
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder , dgn_nf = Nothing
b9625461755578f3eed04676d42a63fd2caebd0cChristian Maeder , dgn_sigma = Nothing
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder , nodeInfo = info
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder , dgn_lock = Nothing }
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder-- | create a new node label
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaedernewNodeLab :: NODE_NAME -> DGOrigin -> G_theory -> DGNodeLab
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian MaedernewNodeLab name orig = newInfoNodeLab name (newNodeInfo orig)
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich-- import, formal parameters and united signature of formal params
4ba08bfca0cc8d9da65397b8dfd2654fdb4c0e62Christian Maedertype GenericitySig = (MaybeNode, [NodeSig], MaybeNode)
4ba08bfca0cc8d9da65397b8dfd2654fdb4c0e62Christian Maeder-- import, formal parameters, united signature of formal params, body
4ba08bfca0cc8d9da65397b8dfd2654fdb4c0e62Christian Maedertype ExtGenSig = (MaybeNode, [NodeSig], G_sign, NodeSig)
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich-- source, morphism, parameterized target
1365c420ef71be3d52796ebd369dc2defdedc822Christian Maedertype ExtViewSig = (NodeSig,GMorphism,ExtGenSig)
308834907a120fd8771e18292ed2ca9cd767c12dChristian Maeder-- * Types for architectural and unit specification analysis
1365c420ef71be3d52796ebd369dc2defdedc822Christian Maeder-- (as defined for basic static semantics in Chap. III:5.1)
36f63902db2b3463faa9f59912ad106e2d5aaa24Klaus Luettichdata UnitSig = Unit_sig NodeSig
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder | Par_unit_sig [NodeSig] NodeSig
e420b3848a0e15a9e074b08c413996cbeb5ab06dChristian Maeder deriving Show
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maederdata ImpUnitSigOrSig = Imp_unit_sig MaybeNode UnitSig
cc07a598b995acc9436651e66fd18009509047efChristian Maeder | Sig NodeSig
cc07a598b995acc9436651e66fd18009509047efChristian Maeder deriving Show
825a1e4ca1e768de4b4883c65a6cb1dce6aa0002Christian Maedertype StUnitCtx = Map.Map SIMPLE_ID ImpUnitSigOrSig
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus LuettichemptyStUnitCtx :: StUnitCtx
4ba08bfca0cc8d9da65397b8dfd2654fdb4c0e62Christian MaederemptyStUnitCtx = Map.empty
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederdata ArchSig = ArchSig StUnitCtx UnitSig deriving Show
5580ab3e64410186ccd36cde8a94282d8757ac0dChristian Maeder-- * Types for global and library environments
e284004f10a315dbdb624c8b2522f65d485eaa48Martin Kühldata GlobalEntry =
b446bf54c1dc78690aa12e86aadc49cdd8585847Christian Maeder SpecEntry ExtGenSig
e284004f10a315dbdb624c8b2522f65d485eaa48Martin Kühl | ViewEntry ExtViewSig
e284004f10a315dbdb624c8b2522f65d485eaa48Martin Kühl | ArchEntry ArchSig
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder | UnitEntry UnitSig
50515239e7e190f4a34ca581dd685d002148fbddChristian Maeder deriving Show
0b349288edfa50fdf38fda1a14e1562d03f92574Christian Maedertype GlobalEnv = Map.Map SIMPLE_ID GlobalEntry
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederemptyHistory :: ([DGRule], [DGChange])
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederemptyHistory = ([], [])
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maedertype ProofHistory = [([DGRule], [DGChange])]
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder{- | the actual development graph with auxiliary information. A
8b4c68db8b465107cabef8b9cd5b6bc216e1b156Till Mossakowski 'G_sign' should be stored in 'sigMap' under its 'gSignSelfIdx'. The
8b4c68db8b465107cabef8b9cd5b6bc216e1b156Till Mossakowski same applies to 'G_morphism' with 'morMap' and 'gMorphismSelfIdx'
8b4c68db8b465107cabef8b9cd5b6bc216e1b156Till Mossakowski resp. 'G_theory' with 'thMap' and 'gTheorySelfIdx'. -}
bcaf979d9babe6346aa343687aa7d596e2894cccPaolo Torrinidata DGraph = DGraph
df29370ae8d8b41587957f6bcdcb43a3f1927e47Christian Maeder { globalAnnos :: GlobalAnnos -- ^ global annos of library
bcaf979d9babe6346aa343687aa7d596e2894cccPaolo Torrini , globalEnv :: GlobalEnv -- ^ name entities (specs, views) of a library
5ce19352a9cc47d982819cc889a71cd0a61ac171Christian Maeder , dgBody :: Tree.Gr DGNodeLab DGLinkLab -- ^ actual 'DGraph` tree
5ce19352a9cc47d982819cc889a71cd0a61ac171Christian Maeder , getNewEdgeID :: Int -- ^ edge counter
c9a7e6af169a2adfb92f42331cd578065ed83a2bChristian Maeder , refNodes :: Map.Map Node (LIB_NAME, Node) -- ^ unexpanded 'DGRef's
bcaf979d9babe6346aa343687aa7d596e2894cccPaolo Torrini , allRefNodes :: Map.Map (LIB_NAME, Node) Node -- ^ all DGRef's
23ab8855c58adfbd03a0730584b917b24c603901Christian Maeder , sigMap :: Map.Map Int G_sign -- ^ signature map
df29370ae8d8b41587957f6bcdcb43a3f1927e47Christian Maeder , thMap :: Map.Map Int G_theory -- ^ morphism map
23ab8855c58adfbd03a0730584b917b24c603901Christian Maeder , morMap :: Map.Map Int G_morphism -- ^ theory map
e50e41135ece589f7202bd4ef8d6b97531c2a56eKlaus Luettich , proofHistory :: ProofHistory -- ^ applied proof steps
47b0e9f3cb008cb7997f4e3bae26e4d62dcc887aChristian Maeder , redoHistory :: ProofHistory -- ^ undone proofs steps
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder , openlock :: Maybe (MVar (IO ())) -- ^ control of graph display
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder-----------------------
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder-- some set functions
99afa6000472f3d291fdf9193ea19d334a58658dChristian Maeder-----------------------
50c3cc2b79207355522c5b096172b3c6b7bec300Christian MaedersetSigMapDG :: Map.Map Int G_sign -> DGraph -> DGraph
88318aafc287e92931dceffbb943d58a9310001dChristian MaedersetSigMapDG m dg = dg{sigMap = m}
d3251b01d8270950716e2b419b335264fa773153Christian MaedersetThMapDG :: Map.Map Int G_theory -> DGraph -> DGraph
88318aafc287e92931dceffbb943d58a9310001dChristian MaedersetThMapDG m dg = dg{thMap = m}
50c3cc2b79207355522c5b096172b3c6b7bec300Christian MaedersetMorMapDG :: Map.Map Int G_morphism -> DGraph -> DGraph
e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus LuettichsetMorMapDG m dg = dg{morMap = m}
9096f6c6aaded6cd8288656ceccd4c7b3bd0747eChristian Maeder-----------------------
e112e83352048f3db8c8f93ae104193e7338c10fChristian Maeder-- some lookup functions
e112e83352048f3db8c8f93ae104193e7338c10fChristian Maeder-----------------------
e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus LuettichlookupSigMapDG :: Int -> DGraph -> Maybe G_sign
e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus LuettichlookupSigMapDG i = Map.lookup i . sigMap
e112e83352048f3db8c8f93ae104193e7338c10fChristian MaederlookupThMapDG :: Int -> DGraph -> Maybe G_theory
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaederlookupThMapDG i = Map.lookup i . thMap
61fa0ac06ede811c7aad54ec4c4202346727368eChristian MaederlookupMorMapDG :: Int -> DGraph -> Maybe G_morphism
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederlookupMorMapDG i = Map.lookup i . morMap
f5c9b1e739228c2a2edf055ac419583412569683Christian MaederlookupGlobalEnvDG :: SIMPLE_ID -> DGraph -> Maybe GlobalEntry
363939beade943a02b31004cea09dec34fa8a6d9Christian MaederlookupGlobalEnvDG sid = Map.lookup sid . globalEnv
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaederemptyDG :: DGraph
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian MaederemptyDG = DGraph
88318aafc287e92931dceffbb943d58a9310001dChristian Maeder { globalAnnos = emptyGlobalAnnos
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder , getNewEdgeID = 0
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder , allRefNodes = Map.empty
f4505a64a089693012a3f5c3b1f12a82cd7a2a5aKlaus Luettich , proofHistory = [emptyHistory]
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder , redoHistory = [emptyHistory]
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder , openlock = Nothing
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederemptyDGwithMVar :: IO DGraph
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederemptyDGwithMVar = do
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder ol <- newEmptyMVar
1a6464613c59e35072b90ca296ae402cbe956144Christian Maeder return $ emptyDG {openlock = Just ol}
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian MaedergetMapAndMaxIndex :: (b -> Map.Map Int a) -> b -> (Map.Map Int a, Int)
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian MaedergetMapAndMaxIndex f gctx =
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder let m = f gctx in (m, if Map.null m then 0 else fst $ Map.findMax m)
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian MaedersigMapI :: DGraph -> (Map.Map Int G_sign, Int)
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian MaedersigMapI = getMapAndMaxIndex sigMap
f78ce817f35574674d54e30ad1861a9b4ced20caChristian MaedermorMapI :: DGraph -> (Map.Map Int G_morphism, Int)
f78ce817f35574674d54e30ad1861a9b4ced20caChristian MaedermorMapI = getMapAndMaxIndex morMap
f78ce817f35574674d54e30ad1861a9b4ced20caChristian MaederthMapI :: DGraph -> (Map.Map Int G_theory, Int)
fd2c22348e5a69231f92fb44e35a9970b47c4e93Christian MaederthMapI = getMapAndMaxIndex thMap
f78ce817f35574674d54e30ad1861a9b4ced20caChristian Maedertype LibEnv = Map.Map LIB_NAME DGraph
89c9d707aa817684b88036a2dad66c3437840677Heng Jiang-- | an empty environment
f78ce817f35574674d54e30ad1861a9b4ced20caChristian MaederemptyLibEnv :: LibEnv
f041c9a6bda23de33a38490e35b831ae18d96b45Christian Maeder-- | returns the DGraph that belongs to the given library name
f041c9a6bda23de33a38490e35b831ae18d96b45Christian MaederlookupDGraph :: LIB_NAME -> LibEnv -> DGraph
f041c9a6bda23de33a38490e35b831ae18d96b45Christian MaederlookupDGraph ln =
bea81dabd203833818cb4a5f3758977c695728cdHeng Jiang Map.findWithDefault (error "lookupDGraph") ln
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder-- | Heterogenous sentences
49d647f58ec5bf482da541eec62f531848c49036Christian Maedertype HetSenStatus a = SenStatus a (AnyComorphism,BasicProof)
7834a982096d93301a4626f444dd9ea5f9fe17eaChristian MaederisProvenSenStatus :: HetSenStatus a -> Bool
5c0b769e33f643e5f0b06328ba0eb03e5bd6e18eChristian MaederisProvenSenStatus = any isProvenSenStatusAux . thmStatus
f9442174f64331ccf0bf08178632af7302ccfc96Christian Maeder where isProvenSenStatusAux (_, BasicProof _ pst) = isProvedStat pst
f9442174f64331ccf0bf08178632af7302ccfc96Christian Maeder isProvenSenStatusAux _ = False
53bbc1c9a4e986d1ee9c081d6f0ac7b9546f212bDominik Luecke-- * Grothendieck theory with prover
bf7b17b0e19362e9228672782218678cab275d1eDominik Luecke-- | a pair of prover and theory which are in the same logic
bf7b17b0e19362e9228672782218678cab275d1eDominik Lueckedata G_theory_with_prover =
bf7b17b0e19362e9228672782218678cab275d1eDominik Luecke forall lid sublogics
bf7b17b0e19362e9228672782218678cab275d1eDominik Luecke basic_spec sentence symb_items symb_map_items
bf7b17b0e19362e9228672782218678cab275d1eDominik Luecke sign morphism symbol raw_symbol proof_tree .
bf7b17b0e19362e9228672782218678cab275d1eDominik Luecke Logic lid sublogics
75b0c0c2cbfb7edd3f4c0555227aabbe6c1aa195Christian Maeder basic_spec sentence symb_items symb_map_items
bf7b17b0e19362e9228672782218678cab275d1eDominik Luecke sign morphism symbol raw_symbol proof_tree =>
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu G_theory_with_prover lid
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu (Theory sign sentence proof_tree)
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu (Prover sign sentence sublogics proof_tree)
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu-- | Grothendieck diagrams
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiutype GDiagram = Tree.Gr G_theory GMorphism
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu-- | weakly amalgamable cocones
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae BungiugWeaklyAmalgamableCocone
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu :: GDiagram -> Result (G_theory, Map.Map Graph.Node GMorphism)
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae BungiugWeaklyAmalgamableCocone _ = return
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu ( error "Static.DevGraph.gWeaklyAmalgamableCocone not yet implemented"
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu , Map.empty) -- dummy implementation
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu-- | get the available node id
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae BungiugetNewNodeDG :: DGraph -> Node
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae BungiugetNewNodeDG = getNewNode . dgBody
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu-- | delete the node out of the given DG
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae BungiudelNodeDG :: Node -> DGraph -> DGraph
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae BungiudelNodeDG n dg =
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu dg{dgBody = delNode n $ dgBody dg}
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu-- | delete the LNode out of the given DG
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae BungiudelLNodeDG :: LNode DGNodeLab -> DGraph -> DGraph
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae BungiudelLNodeDG n@(v, l) g = case matchDG v g of
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu (Just(p, _, l', s), g') ->
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu if l' == l then
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu if null p && null s then g'
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu else error $ "delLNodeDG remaining edges: " ++ show (p ++ s)
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu else error $ "delLNodeDG wrong label: " ++ show n
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu _ -> error $ "delLNodeDG no such node: " ++ show n
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu-- | delete a list of nodes out of the given DG
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae BungiudelNodesDG :: [Node] -> DGraph -> DGraph
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae BungiudelNodesDG ns dg =
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu dg{dgBody = delNodes ns $ dgBody dg}
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu-- | insert a new node into given DGraph
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae BungiuinsNodeDG :: LNode DGNodeLab -> DGraph -> DGraph
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae BungiuinsNodeDG n dg =
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu dg{dgBody = insNode n $ dgBody dg}
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu-- | add a new referenced node into the refNodes map of the given DG
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae BungiuaddToRefNodesDG :: (Node, LIB_NAME, Node) -> DGraph -> DGraph
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae BungiuaddToRefNodesDG (n, libn, refn) dg =
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu dg{refNodes = Map.insert n (libn, refn) $ refNodes dg,
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu allRefNodes = Map.insert (libn, refn) n $ allRefNodes dg}
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu-- | delete the given referenced node out of the refnodes map
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae BungiudeleteFromRefNodesDG :: Node -> DGraph -> DGraph
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae BungiudeleteFromRefNodesDG n dg = dg{refNodes = Map.delete n $ refNodes dg}
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu-- | lookup a referenced node with a node id
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae BungiulookupInRefNodesDG :: Node -> DGraph -> Maybe (LIB_NAME, Node)
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae BungiulookupInRefNodesDG n dg =
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu-- | look up a refernced node with its parent infor.
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae BungiulookupInAllRefNodesDG :: (LIB_NAME, Node) -> DGraph -> Maybe Node
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae BungiulookupInAllRefNodesDG refK dg =
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu Map.lookup refK $ allRefNodes dg
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu-- | inserts a lnode into a given DG
b446bf54c1dc78690aa12e86aadc49cdd8585847Christian MaederinsLNodeDG :: LNode DGNodeLab -> DGraph -> DGraph
3b5814dc6ac813faf8a12ecddf4b727ca7b666a8Francisc Nicolae BungiuinsLNodeDG n@(v, _) g =
3b5814dc6ac813faf8a12ecddf4b727ca7b666a8Francisc Nicolae Bungiu if gelemDG v g then error $ "insLNodeDG " ++ show v else insNodeDG n g
9f226cec9f978edaba67aee4c4e04e3d3b994b87Daniel Calegari-- | insert a new node with the given node content into a given DGraph
9f226cec9f978edaba67aee4c4e04e3d3b994b87Daniel CalegariinsNodesDG :: [LNode DGNodeLab] -> DGraph -> DGraph
9f226cec9f978edaba67aee4c4e04e3d3b994b87Daniel CalegariinsNodesDG ns dg =
9f226cec9f978edaba67aee4c4e04e3d3b994b87Daniel Calegari dg{dgBody = insNodes ns $ dgBody dg}
9f226cec9f978edaba67aee4c4e04e3d3b994b87Daniel Calegari-- | delete an edge out of a given DG
9f226cec9f978edaba67aee4c4e04e3d3b994b87Daniel CalegaridelEdgeDG :: Edge -> DGraph -> DGraph
sccDG = DFS.scc . dgBody
topsortDG = DFS.topsort . dgBody
bfsDG n = BFS.bfs n . dgBody