DevGraph.hs revision 1bc5dccbf0083a620ae1181c717fea75e4af5e5c
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder{- |
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)
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederCentral datastructures for development graphs
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maeder Follows Sect. IV:4.2 of the CASL Reference Manual.
f2f9df2e17e70674f0bf426ed1763c973ee4cde0Christian Maeder-}
c9a7e6af169a2adfb92f42331cd578065ed83a2bChristian Maeder
c9a7e6af169a2adfb92f42331cd578065ed83a2bChristian Maeder{-
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder References:
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder
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.
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder T. Mossakowski, S. Autexier, D. Hutter, P. Hoffman:
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich CASL Proof calculus. In: CASL reference manual, part IV.
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Available from http://www.cofi.info
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder
3e8b136f23ed57d40ee617f49bcac37830b58cabChristian Maeder-}
ef9e8535c168d3f774d9e74368a2317a9eda5826Christian Maeder
bab2d88d650448628730ed3b65c9f99c52500e8cChristian Maedermodule Static.DevGraph where
3e8b136f23ed57d40ee617f49bcac37830b58cabChristian Maeder
ef9e8535c168d3f774d9e74368a2317a9eda5826Christian Maederimport Logic.Logic
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederimport Logic.ExtSign
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederimport Logic.Grothendieck
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederimport Logic.Prover
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroederimport Static.GTheory
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroederimport Syntax.AS_Library
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder
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 Schroeder
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroederimport qualified Data.Map as Map
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroederimport qualified Common.OrderedMap as OMap
825a1e4ca1e768de4b4883c65a6cb1dce6aa0002Christian Maeder
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroederimport Common.AS_Annotation
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maederimport Common.GlobalAnnotations
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maederimport Common.Id
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maederimport Common.Doc
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maederimport Common.DocUtils
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maederimport Common.Result
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maederimport Control.Concurrent.MVar
4b4a0b61b72cf8478a5d4d5002bca9f699401363Christian Maeder
4b4a0b61b72cf8478a5d4d5002bca9f699401363Christian Maederimport Data.Char (toLower)
308834907a120fd8771e18292ed2ca9cd767c12dChristian Maederimport Data.List(find, intersect, partition)
bab2d88d650448628730ed3b65c9f99c52500e8cChristian Maeder
9f226cec9f978edaba67aee4c4e04e3d3b994b87Daniel Calegari{- | returns one new node id for the given graph
8cacad2a09782249243b80985f28e9387019fe40Christian Maeder-}
6a2dad705deefd1b7a7e09b84fd2d75f2213be47Christian MaedergetNewNode :: Tree.Gr a b -> Node
a7c27282e71cf4505026645f96d4f5cb8a284e32Christian MaedergetNewNode g = case newNodes 1 g of
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder [n] -> n
014dc30f64ec25e4790cca987d4d1e6635430510Christian Maeder _ -> error "Static.DevGraph.getNewNode"
f04e8f3ff56405901be968fd4c6e9769239f1a9bKlaus Luettich
6aea82c63ba1d2efc0329bc784a14e521469ec20Christian Maeder{- | returns a list of edge ids with the given number of edge ids
4ba08bfca0cc8d9da65397b8dfd2654fdb4c0e62Christian Maeder and a specified graph.
feca1d35123d8c31aee238c9ce79947b0bf65494Christian Maeder-}
431d34c7007a787331c4e5ec997badb0f8190fc7Christian MaedergetNewEdgeIDs :: Int -> DGraph -> EdgeID
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian MaedergetNewEdgeIDs count g = take count [(getNewEdgeID g)..]
f5c0884429b01e74c6e658ded921fb2e16dfb478Christian Maeder
db675e8302ddb0d6528088ce68f5e98a00e890e3Christian Maeder{- | tries to find the label of a link whose id is given in
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder a specified graph
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder-}
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
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 Maeder-}
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
a3c6d8e0670bf2aa71bc8e2a3b1f45d56dd65e4cChristian Maeder
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.
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-}
ca074a78b8dcccbb8c419586787882f98d0c6163Christian MaederisIdenticalEdgeID :: EdgeID -> EdgeID -> Bool
ca074a78b8dcccbb8c419586787882f98d0c6163Christian MaederisIdenticalEdgeID id1 id2 = not $ null $ intersect id1 id2
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder
4017ebc0f692820736d796af3110c3b3018c108aChristian Maeder{- | similar to getDGLEdgeWithIDs, but an error will be thrown if
b568982efd0997d877286faa592d81b03c8c67b8Christian Maeder the specified edge is not found.
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder-}
0be0db405c49906bd7057255069bf6df53395ac9Klaus LuettichgetDGLEdgeWithIDsForSure :: EdgeID -> DGraph -> (LEdge DGLinkLab)
ca074a78b8dcccbb8c419586787882f98d0c6163Christian MaedergetDGLEdgeWithIDsForSure ids dgraph =
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder case getDGLEdgeWithIDs ids dgraph of
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Just e -> e
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Nothing -> error ("ID: "++show ids ++
f2f9df2e17e70674f0bf426ed1763c973ee4cde0Christian Maeder "not found. Static.DevGraph.getDGLEdgeWithIDsForSure")
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder-- * Types for structured specification analysis
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder
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
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 Maeder
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)
e6d5dbbc3308f05197868806e0b860f4f53875f1Christian Maeder
363939beade943a02b31004cea09dec34fa8a6d9Christian Maederdgn_origin :: DGNodeLab -> DGOrigin
58b96b17bf8e32c0b0d773380a5e62f992eef2bcChristian Maederdgn_origin = node_origin . nodeInfo
e4f4d096e5e6d60dd91c746d0e833d0ac7a29c50Christian Maeder
eb74267cf39e4e95f9eeb5c765f4c8dac33971b4Christian Maederdgn_cons :: DGNodeLab -> Conservativity
eb74267cf39e4e95f9eeb5c765f4c8dac33971b4Christian Maederdgn_cons = node_cons . nodeInfo
e4f4d096e5e6d60dd91c746d0e833d0ac7a29c50Christian Maeder
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maederdgn_cons_status :: DGNodeLab -> ThmLinkStatus
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maederdgn_cons_status = node_cons_status . nodeInfo
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder
8d178ae08a52d61379e6b8074f61646499bc88bbChristian Maederdgn_libname :: DGNodeLab -> LIB_NAME
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maederdgn_libname = ref_libname . nodeInfo
6cd33d6101fb1b93baa6d86fac158af18a115108Christian Maeder
6cd33d6101fb1b93baa6d86fac158af18a115108Christian Maederdgn_node :: DGNodeLab -> Node
6cd33d6101fb1b93baa6d86fac158af18a115108Christian Maederdgn_node = ref_node . nodeInfo
6cd33d6101fb1b93baa6d86fac158af18a115108Christian Maeder
6cd33d6101fb1b93baa6d86fac158af18a115108Christian Maeder-- | node inscriptions in development graphs
b2ac5a92cf36382e8deea5661c1964566caf72b3Christian Maederdata DGNodeLab =
ea5432ff6f61c64469b11d9352b23fef4ff152e8Christian Maeder 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)
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederinstance Show (MVar ()) where
f1a913f880e409e7327b5deae95738b5448379a1Christian Maeder show _ = ""
f1a913f880e409e7327b5deae95738b5448379a1Christian Maeder
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
c9a7e6af169a2adfb92f42331cd578065ed83a2bChristian Maeder
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaederisInternalNode :: DGNodeLab -> Bool
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederisInternalNode l@DGNodeLab {dgn_name = n} =
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder if isDGRef l then null $ show $ getName n else isInternal n
93f5b72fdb9ee734caa750b43dd79bbb590dcd73Christian Maeder
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
8fb127028cb7dd361e348a3252e33487f73428bcJonathan von Schroeder None -> b
06dd4e7c29f33f6122a910719e3bd9062256e397Andy Gimblett _ -> case dgn_cons_status dgn of
254df6f22d01eacf7c57b85729e0445747b630d9Christian Maeder LeftOpen -> True
4ba08bfca0cc8d9da65397b8dfd2654fdb4c0e62Christian Maeder _ -> False
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder
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"
3554301a34639efb6c9961a8571775d0061284c9Christian Maeder else "spec"
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder-- gets the name of a development graph node as a string
9e748851c150e1022fb952bab3315e869aaf0214Christian MaedergetDGNodeName :: DGNodeLab -> String
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaedergetDGNodeName dgn = showName $ dgn_name dgn
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaederemptyNodeName :: NODE_NAME
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian MaederemptyNodeName = (mkSimpleId "", "", 0)
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian MaedershowInt :: Int -> String
3554301a34639efb6c9961a8571775d0061284c9Christian MaedershowInt i = if i == 0 then "" else show i
3554301a34639efb6c9961a8571775d0061284c9Christian Maeder
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 Maeder
aded505f9b42cc38975559c2a5d175ae95de436bChristian MaedermakeName :: SIMPLE_ID -> NODE_NAME
aded505f9b42cc38975559c2a5d175ae95de436bChristian MaedermakeName n = (n, "", 0)
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder
aded505f9b42cc38975559c2a5d175ae95de436bChristian MaedergetName :: NODE_NAME -> SIMPLE_ID
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian MaedergetName (n, _, _) = n
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder
a14767aeac3e78ed100f5b75e210ba563ee10dbaChristian MaedermakeMaybeName :: Maybe SIMPLE_ID -> NODE_NAME
a14767aeac3e78ed100f5b75e210ba563ee10dbaChristian MaedermakeMaybeName Nothing = emptyNodeName
a14767aeac3e78ed100f5b75e210ba563ee10dbaChristian MaedermakeMaybeName (Just n) = makeName n
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder
3554301a34639efb6c9961a8571775d0061284c9Christian Maederinc :: NODE_NAME -> NODE_NAME
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maederinc (n, s, i) = (n, s, i+1)
54ea981a0503c396c2923a1c06421c6235baf27fChristian Maeder
54ea981a0503c396c2923a1c06421c6235baf27fChristian MaederisInternal :: NODE_NAME -> Bool
54ea981a0503c396c2923a1c06421c6235baf27fChristian MaederisInternal (_, s, i) = i /= 0 || s /= ""
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder
db6729e623b4053149084ccf4b35e5308ac7e359Christian MaederextName :: String -> NODE_NAME -> NODE_NAME
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian MaederextName s (n, s1, i) = (n, s1 ++ showInt i ++ s, 0)
f9e0b18852b238ddb649d341194e05d7200d1bbeChristian Maeder
aded505f9b42cc38975559c2a5d175ae95de436bChristian MaederisDGRef :: DGNodeLab -> Bool
f9e0b18852b238ddb649d341194e05d7200d1bbeChristian MaederisDGRef l = case nodeInfo l of
819e29dba060687cf391e444e0f6ff88c1908cc3Christian Maeder DGNode {} -> False
819e29dba060687cf391e444e0f6ff88c1908cc3Christian Maeder DGRef {} -> True
819e29dba060687cf391e444e0f6ff88c1908cc3Christian Maeder
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 not $ OMap.null $ OMap.filter
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder (\s -> not (isAxiom s) && not (isProvenSenStatus s) ) sens
254df6f22d01eacf7c57b85729e0445747b630d9Christian Maeder
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 Maeder-}
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder
c208973c890b8f993297720fd0247bc7481d4304Christian Maedertype EdgeID = [Int]
0d0278c34a374b29c2d6c58b39b8b56e283d48e8Christian Maeder
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
986d3f255182539098a97ac86da9eeee5b7a72e3Christian Maeder
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder-- | create a default ID which has to be changed when inserting a certain edge.
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaederdefaultEdgeID :: EdgeID
01e278bdd7dce13b9303ed3d79683d83c89d09f9Liam O'ReillydefaultEdgeID = []
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder
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.
1535e1d8c82db5f7e2402261983c4c2ef39f4f39Mihai Codescu-}
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 Schroeder
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
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder{- | checks if the given edge is contained in the given
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder list of EdgeIDs.
d54cd08a4cfa26256c38d8ed12c343adbfe1a0e3Christian Maeder-}
d54cd08a4cfa26256c38d8ed12c343adbfe1a0e3Christian MaederroughElem :: LEdge DGLinkLab -> [EdgeID] -> Bool
d54cd08a4cfa26256c38d8ed12c343adbfe1a0e3Christian MaederroughElem (_, _, label) =
3b06e23643a9f65390cb8c1caabe83fa7e87a708Till Mossakowski any (\ edgeID -> isIdenticalEdgeID edgeID $ dgl_id label)
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder{- | the edit operations of the DGraph
8c812cd83569e973f10cf69a342424ceabc07af9Christian Maeder-}
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)
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder deriving Eq
f8e1a1eca871a26a535a4ee7d51902ba94b1db1eChristian Maeder
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
23b4e542dca35852f58d1fb3f7d9078c1de5ab06Christian Maeder
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
878a5ecd6acf973907e25e5be6e4a792ea19a05eEwaryst Schulz | GlobalDef
878a5ecd6acf973907e25e5be6e4a792ea19a05eEwaryst Schulz | HidingDef
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)
a604cbad8e2202147b5c6bb9f2e06ae61162d654Felix Gabriel Mance
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
8fd6a3f938496a502bc62f1923ff7c15f59acf91Christian Maeder
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
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
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder
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 Schroeder
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroederinstance Show Conservativity where
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder show None = ""
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder show Cons = "Cons"
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder show Mono = "Mono"
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder show Def = "Def"
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder-- | Rules in the development graph calculus,
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder-- Sect. IV:4.4 of the CASL Reference Manual explains them in depth
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maederdata DGRule =
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder TheoremHideShift
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder | HideTheoremShift (LEdge DGLinkLab)
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder | Borrowing
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder | ConsShift
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder | DefShift
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder | MonoShift
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder | DefToMono
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder | MonoToCons
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder | FreeIsMono
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder | MonoIsFree
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 Maeder
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)
fc09e0a6af734edbd944dd8082bb51985c233b43Alexis Tsogias
b5da047a9a875dec3f968b6c0df96af326f90fa9Alexis TsogiasprintLEdgeInProof :: LEdge DGLinkLab -> Doc
0a03acf9fa28e6ff00f4d7c9c6acbae64cf09c56Ewaryst SchulzprintLEdgeInProof (s,t,l) =
0a03acf9fa28e6ff00f4d7c9c6acbae64cf09c56Ewaryst Schulz pretty s <> text "-->" <> pretty t <> text ":"
0a03acf9fa28e6ff00f4d7c9c6acbae64cf09c56Ewaryst Schulz <+> printLabInProof l
bab2d88d650448628730ed3b65c9f99c52500e8cChristian Maeder
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)
4b4a0b61b72cf8478a5d4d5002bca9f699401363Christian Maeder ]
9f226cec9f978edaba67aee4c4e04e3d3b994b87Daniel Calegari
9f226cec9f978edaba67aee4c4e04e3d3b994b87Daniel Calegaridata BasicConsProof = BasicConsProof -- more detail to be added ...
9f226cec9f978edaba67aee4c4e04e3d3b994b87Daniel Calegari deriving (Show, Eq)
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder
c70ef4c3b3a62764f715510c9fd67dde3acfe454Christian Maederdata ThmLinkStatus = LeftOpen
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder | Proven DGRule [EdgeID]
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder --[LEdge DGLinkLab] -- Proven DGRule Int
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers deriving (Show, Eq)
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder
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"
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder , pretty r
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder , text "Proof based on links:"
cc07a598b995acc9436651e66fd18009509047efChristian Maeder ] $+$ vcat(map printOneProofBasis ls)
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder --] $+$ vcat(map printLEdgeInProof ls)
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederprintOneProofBasis :: EdgeID -> Doc
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederprintOneProofBasis pb = pretty pb
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich
50c3cc2b79207355522c5b096172b3c6b7bec300Christian Maeder-- | shows short theorem link status
f443a57f2a8e0ca3daa7431b0c89a18ba52c337aChristian MaedergetThmType :: ThmLinkStatus -> String
f5c9b1e739228c2a2edf055ac419583412569683Christian MaedergetThmType = map toLower . getThmTypeAux
857992065be4ed40a72c6296b6c0aec62ab4c5b9Christian Maeder
37a9d042e9f85a1d6e229eb80b48f93df810f155Christian MaedergetThmTypeAux :: ThmLinkStatus -> String
7c99e334446bb97120e30e967baeeddfdd1278deKlaus LuettichgetThmTypeAux s = case s of
f5c9b1e739228c2a2edf055ac419583412569683Christian Maeder LeftOpen -> "Unproven"
f5c9b1e739228c2a2edf055ac419583412569683Christian Maeder _ -> "Proven"
f5c9b1e739228c2a2edf055ac419583412569683Christian Maeder
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
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder | DGData
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 Luettich deriving Eq
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder
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 Maeder
825a1e4ca1e768de4b4883c65a6cb1dce6aa0002Christian Maederinstance Pretty DGOrigin where
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder pretty = text . show
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder-- | Node with signature in a DG
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroederdata NodeSig = NodeSig Node G_sign deriving (Show, Eq)
aebb0b18fe5e6ba7dd7e4c66a16a905611ef7ba9Christian Maeder
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 Maeder
1dfba1f850f6a43094962b459998d1ea11472461Christian Maederinstance Pretty NodeSig where
1dfba1f850f6a43094962b459998d1ea11472461Christian Maeder pretty (NodeSig n sig) =
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder text "node" <+> pretty n <> colon <> pretty sig
b64e673e77d2e02c8cd1625ddbd4ea5a97fd5ce3Christian Maeder
e7757995211bd395dc79d26fe017d99375f7d2a6Christian MaederemptyG_sign :: AnyLogic -> G_sign
99afa6000472f3d291fdf9193ea19d334a58658dChristian MaederemptyG_sign (Logic lid) = G_sign lid (ext_empty_signature lid) 0
fa0f3519d71f719d88577b716b1579776b4a2535Christian Maeder
99afa6000472f3d291fdf9193ea19d334a58658dChristian MaedergetSig :: NodeSig -> G_sign
5bb7eeaca10ea76595229375f907a5a388b7c882Christian MaedergetSig (NodeSig _ sigma) = sigma
5bb7eeaca10ea76595229375f907a5a388b7c882Christian Maeder
5bb7eeaca10ea76595229375f907a5a388b7c882Christian MaedergetNode :: NodeSig -> Node
c59d1c38ef94b4fb1c8d9fda9573bc1e1d2801e7Christian MaedergetNode (NodeSig n _) = n
cd36bffee51c77cdadcb9f916b34fa512e311946Christian Maeder
99afa6000472f3d291fdf9193ea19d334a58658dChristian MaedergetMaybeSig :: MaybeNode -> G_sign
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian MaedergetMaybeSig (JustNode ns) = getSig ns
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaedergetMaybeSig (EmptyNode l) = emptyG_sign l
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus LuettichgetLogic :: MaybeNode -> AnyLogic
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus LuettichgetLogic (JustNode ns) = getNodeLogic ns
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus LuettichgetLogic (EmptyNode l) = l
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus LuettichgetNodeLogic :: NodeSig -> AnyLogic
36f63902db2b3463faa9f59912ad106e2d5aaa24Klaus LuettichgetNodeLogic (NodeSig _ (G_sign lid _ _)) = Logic lid
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus LuettichnewNodeInfo :: DGOrigin -> DGNodeInfo
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus LuettichnewNodeInfo orig = DGNode
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich { node_origin = orig
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich , node_cons = None
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder , node_cons_status = LeftOpen }
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder
810746aea00b81c1eec27dae84d73a43599ff056Christian MaedernewRefInfo :: LIB_NAME -> Node -> DGNodeInfo
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian MaedernewRefInfo ln n = DGRef
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers { ref_libname = ln
1365c420ef71be3d52796ebd369dc2defdedc822Christian Maeder , ref_node = n }
a80c28bb8b7a23ccdf7e08d0fe216fc19cc97273Klaus Luettich
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 }
d0652648f9879c67a194f8b03baafe2700c68eb4Christian Maeder
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
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich-- import, formal parameters and united signature of formal params
4ba08bfca0cc8d9da65397b8dfd2654fdb4c0e62Christian Maedertype GenericitySig = (MaybeNode, [NodeSig], MaybeNode)
4ba08bfca0cc8d9da65397b8dfd2654fdb4c0e62Christian Maeder
4ba08bfca0cc8d9da65397b8dfd2654fdb4c0e62Christian Maeder-- import, formal parameters, united signature of formal params, body
4ba08bfca0cc8d9da65397b8dfd2654fdb4c0e62Christian Maedertype ExtGenSig = (MaybeNode, [NodeSig], G_sign, NodeSig)
4ba08bfca0cc8d9da65397b8dfd2654fdb4c0e62Christian Maeder
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich-- source, morphism, parameterized target
1365c420ef71be3d52796ebd369dc2defdedc822Christian Maedertype ExtViewSig = (NodeSig,GMorphism,ExtGenSig)
308834907a120fd8771e18292ed2ca9cd767c12dChristian Maeder
308834907a120fd8771e18292ed2ca9cd767c12dChristian Maeder-- * Types for architectural and unit specification analysis
1365c420ef71be3d52796ebd369dc2defdedc822Christian Maeder-- (as defined for basic static semantics in Chap. III:5.1)
83394c6b6e6de128e71b67c9251ed7a84485d082Christian Maeder
36f63902db2b3463faa9f59912ad106e2d5aaa24Klaus Luettichdata UnitSig = Unit_sig NodeSig
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder | Par_unit_sig [NodeSig] NodeSig
e420b3848a0e15a9e074b08c413996cbeb5ab06dChristian Maeder deriving Show
68d10d143f29fcff3c637ba24f90e983995ceae6Christian Maeder
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maederdata ImpUnitSigOrSig = Imp_unit_sig MaybeNode UnitSig
cc07a598b995acc9436651e66fd18009509047efChristian Maeder | Sig NodeSig
cc07a598b995acc9436651e66fd18009509047efChristian Maeder deriving Show
825a1e4ca1e768de4b4883c65a6cb1dce6aa0002Christian Maeder
825a1e4ca1e768de4b4883c65a6cb1dce6aa0002Christian Maedertype StUnitCtx = Map.Map SIMPLE_ID ImpUnitSigOrSig
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus LuettichemptyStUnitCtx :: StUnitCtx
4ba08bfca0cc8d9da65397b8dfd2654fdb4c0e62Christian MaederemptyStUnitCtx = Map.empty
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederdata ArchSig = ArchSig StUnitCtx UnitSig deriving Show
2c619a4dfdc1df27573eba98e81ed1ace906941dChristian Maeder
5580ab3e64410186ccd36cde8a94282d8757ac0dChristian Maeder-- * Types for global and library environments
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder
e284004f10a315dbdb624c8b2522f65d485eaa48Martin Kühldata GlobalEntry =
b446bf54c1dc78690aa12e86aadc49cdd8585847Christian Maeder SpecEntry ExtGenSig
e284004f10a315dbdb624c8b2522f65d485eaa48Martin Kühl | ViewEntry ExtViewSig
e284004f10a315dbdb624c8b2522f65d485eaa48Martin Kühl | ArchEntry ArchSig
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder | UnitEntry UnitSig
50515239e7e190f4a34ca581dd685d002148fbddChristian Maeder | RefEntry
50515239e7e190f4a34ca581dd685d002148fbddChristian Maeder deriving Show
0b349288edfa50fdf38fda1a14e1562d03f92574Christian Maeder
0b349288edfa50fdf38fda1a14e1562d03f92574Christian Maedertype GlobalEnv = Map.Map SIMPLE_ID GlobalEntry
0b349288edfa50fdf38fda1a14e1562d03f92574Christian Maeder
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederemptyHistory :: ([DGRule], [DGChange])
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederemptyHistory = ([], [])
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maedertype ProofHistory = [([DGRule], [DGChange])]
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder
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 }
431d34c7007a787331c4e5ec997badb0f8190fc7Christian Maeder
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}
24ddb6d7cde9dd6ab04b8631b1b0104e0861ec5fChristian Maeder
d3251b01d8270950716e2b419b335264fa773153Christian MaedersetThMapDG :: Map.Map Int G_theory -> DGraph -> DGraph
88318aafc287e92931dceffbb943d58a9310001dChristian MaedersetThMapDG m dg = dg{thMap = m}
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder
50c3cc2b79207355522c5b096172b3c6b7bec300Christian MaedersetMorMapDG :: Map.Map Int G_morphism -> DGraph -> DGraph
e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus LuettichsetMorMapDG m dg = dg{morMap = m}
9096f6c6aaded6cd8288656ceccd4c7b3bd0747eChristian Maeder
9096f6c6aaded6cd8288656ceccd4c7b3bd0747eChristian Maeder-----------------------
e112e83352048f3db8c8f93ae104193e7338c10fChristian Maeder-- some lookup functions
e112e83352048f3db8c8f93ae104193e7338c10fChristian Maeder-----------------------
e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus Luettich
e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus LuettichlookupSigMapDG :: Int -> DGraph -> Maybe G_sign
e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus LuettichlookupSigMapDG i = Map.lookup i . sigMap
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder
e112e83352048f3db8c8f93ae104193e7338c10fChristian MaederlookupThMapDG :: Int -> DGraph -> Maybe G_theory
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaederlookupThMapDG i = Map.lookup i . thMap
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder
61fa0ac06ede811c7aad54ec4c4202346727368eChristian MaederlookupMorMapDG :: Int -> DGraph -> Maybe G_morphism
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederlookupMorMapDG i = Map.lookup i . morMap
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder
f5c9b1e739228c2a2edf055ac419583412569683Christian MaederlookupGlobalEnvDG :: SIMPLE_ID -> DGraph -> Maybe GlobalEntry
363939beade943a02b31004cea09dec34fa8a6d9Christian MaederlookupGlobalEnvDG sid = Map.lookup sid . globalEnv
c72c1e75a969ff4c336e77481c2a8e42603f13eeChristian Maeder
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaederemptyDG :: DGraph
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian MaederemptyDG = DGraph
88318aafc287e92931dceffbb943d58a9310001dChristian Maeder { globalAnnos = emptyGlobalAnnos
7767474aba4fa2dc51a6c68017d3bcef3b773001Christian Maeder , globalEnv = Map.empty
88318aafc287e92931dceffbb943d58a9310001dChristian Maeder , dgBody = Graph.empty
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder , getNewEdgeID = 0
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder , refNodes = Map.empty
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder , allRefNodes = Map.empty
f4505a64a089693012a3f5c3b1f12a82cd7a2a5aKlaus Luettich , sigMap = Map.empty
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder , thMap = Map.empty
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder , morMap = Map.empty
f4505a64a089693012a3f5c3b1f12a82cd7a2a5aKlaus Luettich , proofHistory = [emptyHistory]
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder , redoHistory = [emptyHistory]
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder , openlock = Nothing
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder }
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederemptyDGwithMVar :: IO DGraph
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederemptyDGwithMVar = do
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder ol <- newEmptyMVar
1a6464613c59e35072b90ca296ae402cbe956144Christian Maeder return $ emptyDG {openlock = Just ol}
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder
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 Maeder
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian MaedersigMapI :: DGraph -> (Map.Map Int G_sign, Int)
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian MaedersigMapI = getMapAndMaxIndex sigMap
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder
f78ce817f35574674d54e30ad1861a9b4ced20caChristian MaedermorMapI :: DGraph -> (Map.Map Int G_morphism, Int)
f78ce817f35574674d54e30ad1861a9b4ced20caChristian MaedermorMapI = getMapAndMaxIndex morMap
f78ce817f35574674d54e30ad1861a9b4ced20caChristian Maeder
f78ce817f35574674d54e30ad1861a9b4ced20caChristian MaederthMapI :: DGraph -> (Map.Map Int G_theory, Int)
fd2c22348e5a69231f92fb44e35a9970b47c4e93Christian MaederthMapI = getMapAndMaxIndex thMap
f78ce817f35574674d54e30ad1861a9b4ced20caChristian Maeder
f78ce817f35574674d54e30ad1861a9b4ced20caChristian Maedertype LibEnv = Map.Map LIB_NAME DGraph
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder
89c9d707aa817684b88036a2dad66c3437840677Heng Jiang-- | an empty environment
f78ce817f35574674d54e30ad1861a9b4ced20caChristian MaederemptyLibEnv :: LibEnv
f78ce817f35574674d54e30ad1861a9b4ced20caChristian MaederemptyLibEnv = Map.empty
f78ce817f35574674d54e30ad1861a9b4ced20caChristian Maeder
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
bf7b17b0e19362e9228672782218678cab275d1eDominik Luecke
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder-- | Heterogenous sentences
49d647f58ec5bf482da541eec62f531848c49036Christian Maedertype HetSenStatus a = SenStatus a (AnyComorphism,BasicProof)
7834a982096d93301a4626f444dd9ea5f9fe17eaChristian Maeder
7834a982096d93301a4626f444dd9ea5f9fe17eaChristian MaederisProvenSenStatus :: HetSenStatus a -> Bool
5c0b769e33f643e5f0b06328ba0eb03e5bd6e18eChristian MaederisProvenSenStatus = any isProvenSenStatusAux . thmStatus
f9442174f64331ccf0bf08178632af7302ccfc96Christian Maeder where isProvenSenStatusAux (_, BasicProof _ pst) = isProvedStat pst
f9442174f64331ccf0bf08178632af7302ccfc96Christian Maeder isProvenSenStatusAux _ = False
c802a1041ed9251f8ad79139454267e802900e2aChristian Maeder
53bbc1c9a4e986d1ee9c081d6f0ac7b9546f212bDominik Luecke-- * Grothendieck theory with prover
bf7b17b0e19362e9228672782218678cab275d1eDominik Luecke
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
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu-- | Grothendieck diagrams
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiutype GDiagram = Tree.Gr G_theory GMorphism
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu
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
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu-- | get the available node id
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae BungiugetNewNodeDG :: DGraph -> Node
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae BungiugetNewNodeDG = getNewNode . dgBody
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu
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
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
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
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
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
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
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 Map.lookup n $ refNodes dg
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu
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
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
e7cf29d9f71f4724aed05916d93a0b656d7104e6Francisc Nicolae Bungiu
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
9f226cec9f978edaba67aee4c4e04e3d3b994b87Daniel Calegari-- | delete an edge out of a given DG
9f226cec9f978edaba67aee4c4e04e3d3b994b87Daniel CalegaridelEdgeDG :: Edge -> DGraph -> DGraph
delEdgeDG e dg =
dg {dgBody = delEdge e $ dgBody dg}
-- | delete a list of edges
delEdgesDG :: [Edge] -> DGraph -> DGraph
delEdgesDG es dg =
dg {dgBody = delEdges es $ dgBody dg}
-- | delete a labeled edge out of the given DG
delLEdgeDG :: LEdge DGLinkLab -> DGraph -> DGraph
delLEdgeDG e@(v, w, l) g = case matchDG v g of
(Just(p, v', l', s), g') ->
let (ls, rs) = partition ((l, w) ==) s in
case ls of
[] -> error $ "delLEdgeDG no edge: " ++ show e
[_] -> g'{dgBody = (p, v', l', rs) & (dgBody g')}
_ -> error $ "delLEdgeDG multiple edges: " ++ show e
_ -> error $ "delLEdgeDG no node for edge: " ++ show e
-- | insert a labeled edge into a given DG
insLEdgeDG :: LEdge DGLinkLab -> DGraph -> DGraph
insLEdgeDG e@(v, w, l) g = case matchDG v g of
(Just(p, v', l', s), g') ->
let ls = filter ((l, w) ==) s in
case ls of
[] -> g'{getNewEdgeID = getNewEdgeID g' + 1,
dgBody = (p, v', l', (l, w) : s) & (dgBody g')}
_ -> error $ "insLEdgeDG multiple edge: " ++ show e
_ -> error $ "insLEdgeDG no node for edge: " ++ show e
{- | tries to insert a labeled edge into a given DG, but if this edge
already exists, then does nothing
-}
insLEdgeNubDG :: LEdge DGLinkLab -> DGraph -> DGraph
insLEdgeNubDG (v, w, l) g =
if (l, w) `elem` s then g
else g'{getNewEdgeID = getNewEdgeID g'+1,
dgBody =
(p, v, l', (l{dgl_id=[getNewEdgeID g]}, w) : s) & (dgBody g')}
where (Just (p, _, l', s), g') = matchDG v g
-- | insert an edge into the given DGraph, which updates
-- the graph body and the edge counter as well.
insEdgeDG :: LEdge DGLinkLab -> DGraph -> DGraph
insEdgeDG l oldDG =
oldDG { dgBody = insEdge l $ dgBody oldDG
, getNewEdgeID = getNewEdgeID oldDG + 1 }
-- | insert a list of labeled edge into a given DG
insEdgesDG :: [LEdge DGLinkLab] -> DGraph -> DGraph
insEdgesDG = flip $ foldr insEdgeDG
-- | get all the edges
labEdgesDG :: DGraph -> [LEdge DGLinkLab]
labEdgesDG = labEdges . dgBody
-- | get all the nodes
labNodesDG :: DGraph -> [LNode DGNodeLab]
labNodesDG = labNodes . dgBody
-- | get the context of the given DG
contextDG :: DGraph -> Node -> Context DGNodeLab DGLinkLab
contextDG = context . dgBody
-- | merge a list of lnodes and ledges into a given DG
mkGraphDG :: [LNode DGNodeLab] -> [LEdge DGLinkLab] -> DGraph -> DGraph
mkGraphDG ns ls dg = insEdgesDG ls $ insNodesDG ns dg
-- | tear the given DGraph appart.
matchDG :: Node -> DGraph -> (MContext DGNodeLab DGLinkLab, DGraph)
matchDG n dg =
let
(mc, newBody) = match n $ dgBody dg
in
(mc, dg{dgBody = newBody})
-- | get all nodes of a given DG with scc algorithm
sccDG :: DGraph -> [[Node]]
sccDG = DFS.scc . dgBody
-- | get the list of nodes in top sorted order
topsortDG :: DGraph -> [Node]
topsortDG = DFS.topsort . dgBody
-- | checks if a DG is empty or not.
isEmptyDG :: DGraph -> Bool
isEmptyDG = isEmpty . dgBody
-- | checks if a given node belongs to a given DG
gelemDG :: Node -> DGraph -> Bool
gelemDG n = (gelem n) . dgBody
-- | get the number of nodes of a given DG
noNodesDG :: DGraph -> Int
noNodesDG = noNodes . dgBody
-- | get all nodes which links to the given node in a given DG
preDG :: DGraph -> Node -> [Node]
preDG = pre . dgBody
-- | get all the incoming ledges of the given node in a given DG
innDG :: DGraph -> Node -> [LEdge DGLinkLab]
innDG = inn . dgBody
-- | get all the outgoing ledges of the given node in a given DG
outDG :: DGraph -> Node -> [LEdge DGLinkLab]
outDG = out . dgBody
-- | get all the nodes of the given DG
nodesDG :: DGraph -> [Node]
nodesDG = nodes . dgBody
-- | get all the edges of the given DG
edgesDG :: DGraph -> [Edge]
edgesDG = edges . dgBody
-- | tries to get the label of the given node in a given DG
labDG :: DGraph -> Node -> Maybe DGNodeLab
labDG = lab . dgBody
-- | gets the given number of new node-ids in a given DG.
newNodesDG :: Int -> DGraph -> [Node]
newNodesDG n = newNodes n . dgBody
-- | gets all nodes in a breadth-first sorted order.
bfsDG :: Node -> DGraph -> [Node]
bfsDG n = BFS.bfs n . dgBody
-- | safe context for graphs
safeContext :: (Show a, Show b, Graph gr) => String -> gr a b -> Node
-> Context a b
safeContext err g v =
case match v g of
(Nothing,_) -> error (err++": Match Exception, Node: "++show v++
" not present in graph with nodes:\n"++
show (nodes g)++"\nand edges:\n"++show (edges g))
(Just c,_) -> c
-- | make it not so general ;)
safeContextDG :: String -> DGraph -> Node -> Context DGNodeLab DGLinkLab
safeContextDG s dg n = safeContext s (dgBody dg) n
-- | sets the node with new label and returns the new graph and the old label
labelNodeDG :: LNode DGNodeLab -> DGraph -> (DGraph, DGNodeLab)
labelNodeDG (v, l) g = case matchDG v g of
(Just(p, _, o, s), g') -> (g'{dgBody = (p, v, l, s) & (dgBody g')}, o)
_ -> error $ "labelNodeDG no such node: " ++ show v
-- | add a proof history into current one of the given DG
setProofHistoryDG :: ProofHistory -> DGraph -> DGraph
setProofHistoryDG h c = c{proofHistory = proofHistory c ++ h}
-- | add a history item into current history.
addToProofHistoryDG :: ([DGRule], [DGChange]) -> DGraph -> DGraph
addToProofHistoryDG x dg = dg{proofHistory = x:proofHistory dg}
-- | update the proof history with a function
setProofHistoryWithDG :: (ProofHistory -> ProofHistory)
-> DGraph -> DGraph
setProofHistoryWithDG f dg = dg{proofHistory = f $ proofHistory dg}
{- | Acquire the local lock. If already locked it waits till it is unlocked
again.-}
lockLocal :: DGNodeLab -> IO ()
lockLocal dgn = case dgn_lock dgn of
Just lock -> putMVar lock ()
Nothing -> error "MVar not initialised"
-- | Tries to acquire the local lock. Return False if already acquired.
tryLockLocal :: DGNodeLab -> IO Bool
tryLockLocal dgn = case dgn_lock dgn of
Just lock -> tryPutMVar lock ()
Nothing -> error "MVar not initialised"
-- | Releases the local lock.
unlockLocal :: DGNodeLab -> IO ()
unlockLocal dgn = case dgn_lock dgn of
Just lock -> do
unlocked <- tryTakeMVar lock
case unlocked of
Just () -> return ()
Nothing -> error "Local lock wasn't locked."
Nothing -> error "MVar not initialised"