4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder{- |

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederModule : $Header$

5ba323da9f037264b4a356085e844889aedeac23Christian MaederDescription : Central datastructures for development graphs

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian MaederCopyright : (c) Till Mossakowski, Uni Bremen 2002-2006

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

23f2c59644866aa82e90de353e77f9f1d1b51b9aChristian MaederMaintainer : till@informatik.uni-bremen.de

3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederStability : provisional

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederPortability : non-portable(Logic)

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederCentral datastructures for development graphs

f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder Follows Sect. IV:4.2 of the CASL Reference Manual.

23f2c59644866aa82e90de353e77f9f1d1b51b9aChristian Maeder-}

23f2c59644866aa82e90de353e77f9f1d1b51b9aChristian Maeder

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder{-

23f2c59644866aa82e90de353e77f9f1d1b51b9aChristian Maeder References:

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder T. Mossakowski, S. Autexier and D. Hutter:

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder Extending Development Graphs With Hiding.

fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder H. Hussmann (ed.): Fundamental Approaches to Software Engineering 2001,

792df0347edab377785d98c63e2be8e2ce0a8bdeChristian Maeder Lecture Notes in Computer Science 2029, p. 269-283,

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder Springer-Verlag 2001.

23f8d286586ff38a9e73052b2c7c04c62c5c638fChristian Maeder

ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder T. Mossakowski, S. Autexier, D. Hutter, P. Hoffman:

ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder CASL Proof calculus. In: CASL reference manual, part IV.

fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder Available from http://www.cofi.info

f8f78a2c8796a387a4348cc672ae08e8d9f69315Christian Maeder

950e053ba55ac9c7d9c26a1ab48bd00202b29511Christian Maeder-}

f8f78a2c8796a387a4348cc672ae08e8d9f69315Christian Maeder

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maedermodule Static.DevGraph where

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder

f8f78a2c8796a387a4348cc672ae08e8d9f69315Christian Maederimport Logic.Logic

af621d0066770895fd79562728e93099c8c52060Christian Maederimport Logic.Comorphism(mkIdComorphism)

7c554e9d4a39b8eb3b0881f20807c95dd8e793aeChristian Maederimport Common.ExtSign

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport Logic.ExtSign

79d11c2e3ad242ebb241f5d4a5e98a674c0b986fChristian Maederimport Logic.Grothendieck

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maederimport Logic.Prover

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maederimport Static.GTheory

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maederimport Syntax.AS_Library

f8f78a2c8796a387a4348cc672ae08e8d9f69315Christian Maeder

024621f43239cfe9629e35d35a8669fad7acbba2Christian Maederimport Data.Graph.Inductive.Graph as Graph

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maederimport qualified Data.Graph.Inductive.Query.DFS as DFS

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maederimport qualified Data.Graph.Inductive.Query.BFS as BFS

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maederimport qualified Common.Lib.Graph as Tree

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maederimport qualified Data.Map as Map

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maederimport qualified Common.OrderedMap as OMap

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maederimport Common.AS_Annotation

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maederimport Common.GlobalAnnotations

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maederimport Common.Id

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maederimport Common.Doc

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maederimport Common.DocUtils

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maederimport Common.Result

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maederimport Control.Concurrent.MVar

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maederimport Data.Char (toLower)

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maederimport Data.List(find, intersect, partition)

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maederimport Static.WACocone

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maederimport Common.SFKT

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder{- | returns one new node id for the given graph

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder-}

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaedergetNewNode :: Tree.Gr a b -> Node

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaedergetNewNode g = case newNodes 1 g of

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder [n] -> n

9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder _ -> error "Static.DevGraph.getNewNode"

9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder

9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder{- | returns a list of edge ids with the given number of edge ids

9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder and a specified graph.

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder-}

9e0472be46104307b974fe5079bf5cc9e94a1a96Christian MaedergetNewEdgeIDs :: Int -> DGraph -> EdgeID

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaedergetNewEdgeIDs count g = take count [(getNewEdgeID g)..]

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder

9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder{- | tries to find the label of a link whose id is given in

9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder a specified graph

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder-}

afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaedergetDGLinkLabWithIDs :: EdgeID -> DGraph -> Maybe DGLinkLab

afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaedergetDGLinkLabWithIDs ids dgraph =

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder case getDGLEdgeWithIDs ids dgraph of

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder Just (_, _, label) -> Just label

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder Nothing -> Nothing

792df0347edab377785d98c63e2be8e2ce0a8bdeChristian Maeder

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder{- | tries to find a link, which includes the src, tgt node

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder and its label according to a given id in a specified graph.

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder-}

d976ba42e9d48c289f9c73147669c7e57b7aa98eChristian MaedergetDGLEdgeWithIDs :: EdgeID -> DGraph -> Maybe (LEdge DGLinkLab)

d976ba42e9d48c289f9c73147669c7e57b7aa98eChristian MaedergetDGLEdgeWithIDs ids dgraph =

986e0e9cf8c2358f455460b3fc75ce7c5dcf0973Christian Maeder find (\ (_, _, label) -> isIdenticalEdgeID ids $ dgl_id label)

6a7e00a968cb0f3f9ccae19ab47ef3636c7e79bfChristian Maeder $ labEdges $ dgBody dgraph

6a7e00a968cb0f3f9ccae19ab47ef3636c7e79bfChristian Maeder

88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder{- | returns whether two edge ids are identical to each other or not.

88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder two edge ids are identical, only if their intersect

88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder is not empty.

6a7e00a968cb0f3f9ccae19ab47ef3636c7e79bfChristian Maeder-}

6a7e00a968cb0f3f9ccae19ab47ef3636c7e79bfChristian MaederisIdenticalEdgeID :: EdgeID -> EdgeID -> Bool

6a7e00a968cb0f3f9ccae19ab47ef3636c7e79bfChristian MaederisIdenticalEdgeID id1 id2 = not $ null $ intersect id1 id2

5ba323da9f037264b4a356085e844889aedeac23Christian Maeder

6a7e00a968cb0f3f9ccae19ab47ef3636c7e79bfChristian Maeder{- | similar to getDGLEdgeWithIDs, but an error will be thrown if

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder the specified edge is not found.

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder-}

59c301c268f79cfde0a4c30a2c572a368db98da5Christian MaedergetDGLEdgeWithIDsForSure :: EdgeID -> DGraph -> (LEdge DGLinkLab)

59c301c268f79cfde0a4c30a2c572a368db98da5Christian MaedergetDGLEdgeWithIDsForSure ids dgraph =

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder case getDGLEdgeWithIDs ids dgraph of

0a320bc4cdbf38f480b75ac15a54db1c4885b497Christian Maeder Just e -> e

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder Nothing -> error ("ID: "++show ids ++

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder "not found. Static.DevGraph.getDGLEdgeWithIDsForSure")

0a320bc4cdbf38f480b75ac15a54db1c4885b497Christian Maeder

5334aa8fe0b0d1eb8a1cad40b741aa07172773c9Christian Maeder-- * Types for structured specification analysis

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder

31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder-- ??? Some info about the theorems already proved for a node

31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder-- should be added

31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder-- or should it be kept separately?

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder-- what about open theorems of a node???

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder-- | name of a node in a DG; auxiliary nodes may have extension string

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder-- and non-zero number (for these, names are usually hidden)

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maedertype NODE_NAME = (SIMPLE_ID, String, Int)

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder

5334aa8fe0b0d1eb8a1cad40b741aa07172773c9Christian Maederdata DGNodeInfo = DGNode

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder { node_origin :: DGOrigin -- origin in input language

5334aa8fe0b0d1eb8a1cad40b741aa07172773c9Christian Maeder , node_cons :: Conservativity

5334aa8fe0b0d1eb8a1cad40b741aa07172773c9Christian Maeder , node_cons_status :: ThmLinkStatus }

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder | DGRef -- reference to node in a different DG

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder { ref_libname :: LIB_NAME -- pointer to DG where ref'd node resides

5334aa8fe0b0d1eb8a1cad40b741aa07172773c9Christian Maeder , ref_node :: Node -- pointer to ref'd node

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder } deriving (Show, Eq)

5334aa8fe0b0d1eb8a1cad40b741aa07172773c9Christian Maeder

ad187062b0009820118c1b773a232e29b879a2faChristian Maederdgn_origin :: DGNodeLab -> DGOrigin

5334aa8fe0b0d1eb8a1cad40b741aa07172773c9Christian Maederdgn_origin = node_origin . nodeInfo

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder

ad187062b0009820118c1b773a232e29b879a2faChristian Maederdgn_cons :: DGNodeLab -> Conservativity

ad187062b0009820118c1b773a232e29b879a2faChristian Maederdgn_cons = node_cons . nodeInfo

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maederdgn_cons_status :: DGNodeLab -> ThmLinkStatus

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maederdgn_cons_status = node_cons_status . nodeInfo

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maederdgn_libname :: DGNodeLab -> LIB_NAME

e76e6a43f51438215737d6fc176c89da05bb86daChristian Maederdgn_libname = ref_libname . nodeInfo

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maederdgn_node :: DGNodeLab -> Node

31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maederdgn_node = ref_node . nodeInfo

997c56f3bc74a703043010978e5013fdb074d659Christian Maeder

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder-- | node inscriptions in development graphs

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maederdata DGNodeLab =

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder DGNodeLab

8485da94b57d8b5135ee685b55c982b037ed4140Christian Maeder { dgn_name :: NODE_NAME -- name in the input language

8485da94b57d8b5135ee685b55c982b037ed4140Christian Maeder , dgn_theory :: G_theory -- local theory

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder , dgn_nf :: Maybe Node -- normal form, for Theorem-Hide-Shift

e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder , dgn_sigma :: Maybe GMorphism -- inclusion of signature into nf signature

e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder , nodeInfo :: DGNodeInfo

e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder , dgn_lock :: Maybe (MVar ())

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder } deriving (Show, Eq)

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder

e76e6a43f51438215737d6fc176c89da05bb86daChristian Maederinstance Show (MVar ()) where

e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder show _ = ""

e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maederdgn_sign :: DGNodeLab -> G_sign

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maederdgn_sign dn = case dgn_theory dn of

dc6b48bb46df8e56da3491c98476e6da0d1d5d1dChristian Maeder G_theory lid sig ind _ _-> G_sign lid sig ind

53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederisInternalNode :: DGNodeLab -> Bool

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian MaederisInternalNode l@DGNodeLab {dgn_name = n} =

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder if isDGRef l then null $ show $ getName n else isInternal n

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder-- | test for 'LeftOpen', return input for refs or no conservativity

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaederhasOpenConsStatus :: Bool -> DGNodeLab -> Bool

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaederhasOpenConsStatus b dgn = if isDGRef dgn then b else

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder case dgn_cons dgn of

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder None -> b

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder _ -> case dgn_cons_status dgn of

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder LeftOpen -> True

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder _ -> False

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder-- | gets the type of a development graph edge as a string

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaedergetDGNodeType :: DGNodeLab -> String

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaedergetDGNodeType dgnodelab =

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder (if hasOpenGoals dgnodelab then id else ("locallyEmpty__" ++))

f6f2955769bfe80dbb4cca3b3ee33c5a8a0f5355Christian Maeder $ if isDGRef dgnodelab then "dg_ref" else

c1031ac42b3f3d7d0fe7d9d6b54423a092d473a0Christian Maeder (if hasOpenConsStatus False dgnodelab

fce77b2785912d1abbcc3680088b235f534bdeffChristian Maeder then "open_cons__"

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder else "proven_cons__")

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder ++ if isInternalNode dgnodelab

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder then "internal"

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder else "spec"

ac19566dc64536c38b5d1d3ae510fb8a07784c2fChristian Maeder

039b7a8265baaeab2ded2a3e3826c04f13364d87Christian Maeder-- gets the name of a development graph node as a string

fe5dbb45b6a8abf34375b4bc5f2a81cda664c0e4Christian MaedergetDGNodeName :: DGNodeLab -> String

3cafc73a998493f9ed3d5e934c0ab80bcfb465c2Christian MaedergetDGNodeName dgn = showName $ dgn_name dgn

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder

039b7a8265baaeab2ded2a3e3826c04f13364d87Christian MaederemptyNodeName :: NODE_NAME

ac19566dc64536c38b5d1d3ae510fb8a07784c2fChristian MaederemptyNodeName = (mkSimpleId "", "", 0)

3cafc73a998493f9ed3d5e934c0ab80bcfb465c2Christian Maeder

7bf6d421b0ea31ae63f1fe04919942b931abda47Christian MaedershowInt :: Int -> String

021d7137df04ec1834911d99d90243a092841cedChristian MaedershowInt i = if i == 0 then "" else show i

021d7137df04ec1834911d99d90243a092841cedChristian Maeder

7c554e9d4a39b8eb3b0881f20807c95dd8e793aeChristian MaedershowName :: NODE_NAME -> String

5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian MaedershowName (n, s, i) = show n ++ if ext == "" then "" else "_" ++ ext

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder where ext = s ++ showInt i

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder

c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian MaedermakeName :: SIMPLE_ID -> NODE_NAME

7c554e9d4a39b8eb3b0881f20807c95dd8e793aeChristian MaedermakeName n = (n, "", 0)

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian MaedergetName :: NODE_NAME -> SIMPLE_ID

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian MaedergetName (n, _, _) = n

adfdcfa67b7f12df6df7292e238c3f9a4b637980Christian Maeder

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian MaedermakeMaybeName :: Maybe SIMPLE_ID -> NODE_NAME

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian MaedermakeMaybeName Nothing = emptyNodeName

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian MaedermakeMaybeName (Just n) = makeName n

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maederinc :: NODE_NAME -> NODE_NAME

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maederinc (n, s, i) = (n, s, i+1)

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian MaederisInternal :: NODE_NAME -> Bool

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian MaederisInternal (_, s, i) = i /= 0 || s /= ""

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian MaederextName :: String -> NODE_NAME -> NODE_NAME

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian MaederextName s (n, s1, i) = (n, s1 ++ showInt i ++ s, 0)

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian MaederisDGRef :: DGNodeLab -> Bool

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian MaederisDGRef l = case nodeInfo l of

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder DGNode {} -> False

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder DGRef {} -> True

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder-- | test if a given node label has local open goals

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian MaederhasOpenGoals :: DGNodeLab -> Bool

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaederhasOpenGoals dgn =

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder case dgn_theory dgn of

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder G_theory _lid _sigma _ sens _->

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder not $ OMap.null $ OMap.filter

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder (\s -> not (isAxiom s) && not (isProvenSenStatus s) ) sens

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder{- | an edge id is represented as a list of ints.

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder the reason of an edge can have multiple ids is, for example, there exists

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder an proven edge e1 with id 1 and an unproven edge e2 with id 2 between

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder two nodes. Now after applying some rules e2 is proven, but it's actually

7bf6d421b0ea31ae63f1fe04919942b931abda47Christian Maeder the same as the proven edge e1, then the proven e2 should not be inserted

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder into the graph again, but e1 will take e2's id 2 because 2 is probably

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder saved in some other places. As a result, e1 would have 1 and 2 as its id.

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder This type can be extended to a more complicated struture, like a tree

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder suggested by Till.

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder-}

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maedertype EdgeID = [Int]

908a6351595b57641353608c4449d5faa0d1adf8Christian Maeder

908a6351595b57641353608c4449d5faa0d1adf8Christian Maeder-- | link inscriptions in development graphs

908a6351595b57641353608c4449d5faa0d1adf8Christian Maederdata DGLinkLab = DGLink

908a6351595b57641353608c4449d5faa0d1adf8Christian Maeder { dgl_morphism :: GMorphism -- signature morphism of link

908a6351595b57641353608c4449d5faa0d1adf8Christian Maeder , dgl_type :: DGLinkType -- type: local, global, def, thm?

bb3bdd4a260606a6184b5f5a5774ca6632ca597aChristian Maeder , dgl_origin :: DGOrigin -- origin in input language

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder , dgl_id :: EdgeID -- id of the edge

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder } deriving Show

e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder-- | create a default ID which has to be changed when inserting a certain edge.

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaederdefaultEdgeID :: EdgeID

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian MaederdefaultEdgeID = []

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder

{- | Eq instance definition of DGLinkLab.

Notice that the dgl_id is not compared here, because

by comparing of two label the edge id should not

play any role.

-}

instance Eq DGLinkLab where

l1 == l2 = dgl_morphism l1 == dgl_morphism l2

&& dgl_type l1 == dgl_type l2

&& dgl_origin l1 == dgl_origin l2

instance Pretty DGLinkLab where

pretty l = fsep [ pretty (dgl_morphism l)

, pretty (dgl_type l)

, pretty (dgl_origin l)]

{- | checks if the given edge is contained in the given

list of EdgeIDs.

-}

roughElem :: LEdge DGLinkLab -> [EdgeID] -> Bool

roughElem (_, _, label) =

any (\ edgeID -> isIdenticalEdgeID edgeID $ dgl_id label)

{- | the edit operations of the DGraph

-}

data DGChange = InsertNode (LNode DGNodeLab)

| DeleteNode (LNode DGNodeLab)

| InsertEdge (LEdge DGLinkLab)

| DeleteEdge (LEdge DGLinkLab)

-- it contains the old label and new label with node

| SetNodeLab DGNodeLab (LNode DGNodeLab)

deriving Eq

instance Show DGChange where

show (InsertNode (n, _)) = "InsertNode "++show n -- ++show l

show (DeleteNode (n, _)) = "DeleteNode "++show n -- ++show l

show (InsertEdge (n,m, _)) = "InsertEdge "++show n++"->"++show m -- ++show l

show (DeleteEdge (n,m, _)) = "DeleteEdge "++show n++"->"++show m -- ++show l

show (SetNodeLab _ (n, _)) = "SetNodeLab of " ++ show n

-- | Link types of development graphs

-- Sect. IV:4.2 of the CASL Reference Manual explains them in depth

data DGLinkType = LocalDef

| GlobalDef

| HidingDef

| FreeDef MaybeNode -- the "parameter" node

| CofreeDef MaybeNode -- the "parameter" node

| LocalThm ThmLinkStatus Conservativity ThmLinkStatus

-- ??? Some more proof information is needed here

-- (proof tree, ...)

| GlobalThm ThmLinkStatus Conservativity ThmLinkStatus

| HidingThm GMorphism ThmLinkStatus

| FreeThm GMorphism ThmLinkStatus

-- DGLink S1 S2 m2 (DGLinkType m1 p) n

-- corresponds to a span of morphisms

-- S1 <--m1-- S --m2--> S2

deriving (Eq,Show)

thmLinkStatus :: DGLinkType -> Maybe ThmLinkStatus

thmLinkStatus (LocalThm s _ _) = Just s

thmLinkStatus (GlobalThm s _ _) = Just s

thmLinkStatus (HidingThm _ s) = Just s

thmLinkStatus (FreeThm _ s) = Just s

thmLinkStatus _ = Nothing

instance Pretty DGLinkType where

pretty t = text $ case t of

LocalDef -> "LocalDef"

GlobalDef -> "GlobalDef"

HidingDef -> "HidingDef"

FreeDef _ -> "FreeDef"

CofreeDef _ -> "CofreeDef"

LocalThm s _ _ -> "LocalThm" ++ getThmTypeAux s

GlobalThm s _ _ -> "GlobalThm" ++ getThmTypeAux s

HidingThm _ s -> "HidingThm" ++ getThmTypeAux s

FreeThm _ s -> "FreeThm" ++ getThmTypeAux s

-- | describe the link type of the label

getDGLinkType :: DGLinkLab -> String

getDGLinkType lnk = let

isHom = isHomogeneous $ dgl_morphism lnk

het = if isHom then id else ("het" ++)

in case dgl_morphism lnk of

GMorphism _ _ _ _ _ ->

case dgl_type lnk of

GlobalDef -> if isHom then "globaldef"

else "hetdef"

HidingDef -> "hidingdef"

LocalThm s _ _ -> het "local" ++ getThmType s ++ "thm"

GlobalThm s _ _ -> het $ getThmType s ++ "thm"

HidingThm _ s -> getThmType s ++ "hidingthm"

FreeThm _ s -> getThmType s ++ "thm"

_ -> "def" -- LocalDef, FreeDef, CofreeDef

-- | Conservativity annotations. For compactness, only the greatest

-- applicable value is used in a DG

data Conservativity = None | Cons | Mono | Def deriving (Eq,Ord)

instance Show Conservativity where

show None = ""

show Cons = "Cons"

show Mono = "Mono"

show Def = "Def"

-- | Rules in the development graph calculus,

-- Sect. IV:4.4 of the CASL Reference Manual explains them in depth

data DGRule =

TheoremHideShift

| HideTheoremShift (LEdge DGLinkLab)

| ComputeColimit

| Borrowing

| ConsShift

| DefShift

| MonoShift

| DefToMono

| MonoToCons

| FreeIsMono

| MonoIsFree

| GlobDecomp (LEdge DGLinkLab) -- edge in the conclusion

| LocDecomp (LEdge DGLinkLab)

| LocInference (LEdge DGLinkLab)

| GlobSubsumption (LEdge DGLinkLab)

| Composition [LEdge DGLinkLab]

| LocalInference

| BasicInference AnyComorphism BasicProof -- coding and proof tree. obsolete?

| BasicConsInference Edge BasicConsProof

deriving (Show, Eq)

instance Pretty DGRule where

pretty r = case r of

TheoremHideShift -> text "Theorem-Hide-Shift"

HideTheoremShift l -> text "Hide-Theorem-Shift; resulting link:"

<+> printLEdgeInProof l

Borrowing -> text "Borrowing"

ComputeColimit -> text"ComputeColimit"

ConsShift -> text "Cons-Shift"

DefShift -> text "Def-Shift"

MonoShift -> text "Mono-Shift"

DefToMono -> text "DefToMono"

MonoToCons -> text "MonoToCons"

FreeIsMono -> text "FreeIsMono"

MonoIsFree -> text "MonoIsFree"

GlobDecomp l -> text "Global Decomposition; resulting link:"

<+> printLEdgeInProof l

LocDecomp l -> text "Local Decomposition; resulting link:"

<+> printLEdgeInProof l

LocInference l -> text "Local Inference; resulting link:"

<+> printLEdgeInProof l

GlobSubsumption l -> text "Global Subsumption; resulting link:"

<+> printLEdgeInProof l

Composition ls ->

text "Composition" <+> vcat (map printLEdgeInProof ls)

LocalInference -> text "Local Inference"

BasicInference c bp -> text "Basic Inference using:"

<+> text ("Comorphism: "++show c ++ "Proof tree: "++show bp)

BasicConsInference _ bp -> text "Basic Cons-Inference using:"

<+> text (show bp)

printLEdgeInProof :: LEdge DGLinkLab -> Doc

printLEdgeInProof (s,t,l) =

pretty s <> text "-->" <> pretty t <> text ":"

<+> printLabInProof l

printLabInProof :: DGLinkLab -> Doc

printLabInProof l =

fsep [ pretty (dgl_type l)

, text "with origin:"

, pretty (dgl_origin l) <> comma

, text "and morphism:"

, pretty (dgl_morphism l)

]

data BasicConsProof = BasicConsProof -- more detail to be added ...

deriving (Show, Eq)

data ThmLinkStatus = LeftOpen

| Proven DGRule [EdgeID]

--[LEdge DGLinkLab] -- Proven DGRule Int

deriving (Show, Eq)

instance Pretty ThmLinkStatus where

pretty tls = case tls of

LeftOpen -> text "Open"

Proven r ls -> fsep [ text "Proven with rule"

, pretty r

, text "Proof based on links:"

] $+$ vcat(map printOneProofBasis ls)

--] $+$ vcat(map printLEdgeInProof ls)

printOneProofBasis :: EdgeID -> Doc

printOneProofBasis pb = pretty pb

-- | shows short theorem link status

getThmType :: ThmLinkStatus -> String

getThmType = map toLower . getThmTypeAux

getThmTypeAux :: ThmLinkStatus -> String

getThmTypeAux s = case s of

LeftOpen -> "Unproven"

_ -> "Proven"

{- | Data type indicating the origin of nodes and edges in the input language

This is not used in the DG calculus, only may be used in the future

for reconstruction of input and management of change. -}

data DGOrigin = DGBasic | DGExtension | DGTranslation | DGUnion | DGHiding

| DGRevealing | DGRevealTranslation | DGFree | DGCofree

| DGLocal | DGClosed | DGClosedLenv | DGLogicQual

| DGData

| DGFormalParams | DGImports | DGSpecInst SIMPLE_ID | DGFitSpec

| DGView SIMPLE_ID | DGFitView SIMPLE_ID | DGFitViewImp SIMPLE_ID

| DGFitViewA SIMPLE_ID | DGFitViewAImp SIMPLE_ID | DGProof

| DGintegratedSCC | DGEmpty

deriving Eq

instance Show DGOrigin where

show o = case o of

DGBasic -> "basic specification"

DGExtension -> "extension"

DGTranslation -> "translation"

DGUnion -> "union"

DGHiding -> "hiding"

DGRevealing -> "revealing"

DGRevealTranslation -> "translation part of a revealing"

DGFree -> "free specification"

DGCofree -> "cofree specification"

DGLocal -> "local specification"

DGClosed -> "closed specification"

DGClosedLenv -> "closed specification (inclusion of local environment)"

DGLogicQual -> "specification with logic qualifier"

DGFormalParams -> "formal parameters of a generic specification"

DGImports -> "imports of a generic specification"

DGSpecInst n -> "instantiation of " ++ tokStr n

DGFitSpec -> "fittig specification"

DGView n -> "view " ++ tokStr n

DGFitView n -> "fitting view " ++ tokStr n

DGFitViewImp n -> "fitting view (imports) " ++ tokStr n

DGFitViewA n -> "fitting view (actual parameters) " ++ tokStr n

DGFitViewAImp n ->

"fitting view (imports and actual parameters) " ++ tokStr n

DGProof -> "constructed within a proof"

DGEmpty -> "empty specification"

DGData -> "data specification"

DGintegratedSCC ->

"OWL spec with integrated strongly connected components"

instance Pretty DGOrigin where

pretty = text . show

-- | Node with signature in a DG

data NodeSig = NodeSig Node G_sign deriving (Show, Eq)

{- | NodeSig or possibly the empty sig in a logic

(but since we want to avoid lots of vacuous nodes with empty sig,

we do not assign a real node in the DG here) -}

data MaybeNode = JustNode NodeSig | EmptyNode AnyLogic deriving (Show, Eq)

instance Pretty NodeSig where

pretty (NodeSig n sig) =

text "node" <+> pretty n <> colon <> pretty sig

emptyG_sign :: AnyLogic -> G_sign

emptyG_sign (Logic lid) = G_sign lid (ext_empty_signature lid) 0

getSig :: NodeSig -> G_sign

getSig (NodeSig _ sigma) = sigma

getNode :: NodeSig -> Node

getNode (NodeSig n _) = n

getMaybeSig :: MaybeNode -> G_sign

getMaybeSig (JustNode ns) = getSig ns

getMaybeSig (EmptyNode l) = emptyG_sign l

getLogic :: MaybeNode -> AnyLogic

getLogic (JustNode ns) = getNodeLogic ns

getLogic (EmptyNode l) = l

getNodeLogic :: NodeSig -> AnyLogic

getNodeLogic (NodeSig _ (G_sign lid _ _)) = Logic lid

newNodeInfo :: DGOrigin -> DGNodeInfo

newNodeInfo orig = DGNode

{ node_origin = orig

, node_cons = None

, node_cons_status = LeftOpen }

newRefInfo :: LIB_NAME -> Node -> DGNodeInfo

newRefInfo ln n = DGRef

{ ref_libname = ln

, ref_node = n }

newInfoNodeLab :: NODE_NAME -> DGNodeInfo -> G_theory -> DGNodeLab

newInfoNodeLab name info gTh = DGNodeLab

{ dgn_name = name

, dgn_theory = gTh

, dgn_nf = Nothing

, dgn_sigma = Nothing

, nodeInfo = info

, dgn_lock = Nothing }

-- | create a new node label

newNodeLab :: NODE_NAME -> DGOrigin -> G_theory -> DGNodeLab

newNodeLab name orig = newInfoNodeLab name (newNodeInfo orig)

-- import, formal parameters and united signature of formal params

type GenericitySig = (MaybeNode, [NodeSig], MaybeNode)

-- import, formal parameters, united signature of formal params, body

type ExtGenSig = (MaybeNode, [NodeSig], G_sign, NodeSig)

-- source, morphism, parameterized target

type ExtViewSig = (NodeSig,GMorphism,ExtGenSig)

-- * Types for architectural and unit specification analysis

-- (as defined for basic static semantics in Chap. III:5.1)

data UnitSig = Unit_sig NodeSig

| Par_unit_sig [NodeSig] NodeSig

deriving Show

data ImpUnitSigOrSig = Imp_unit_sig MaybeNode UnitSig

| Sig NodeSig

deriving Show

type StUnitCtx = Map.Map SIMPLE_ID ImpUnitSigOrSig

emptyStUnitCtx :: StUnitCtx

emptyStUnitCtx = Map.empty

data ArchSig = ArchSig StUnitCtx UnitSig deriving Show

-- * Types for global and library environments

data GlobalEntry =

SpecEntry ExtGenSig

| ViewEntry ExtViewSig

| ArchEntry ArchSig

| UnitEntry UnitSig

| RefEntry

deriving Show

type GlobalEnv = Map.Map SIMPLE_ID GlobalEntry

emptyHistory :: ([DGRule], [DGChange])

emptyHistory = ([], [])

type ProofHistory = [([DGRule], [DGChange])]

{- | the actual development graph with auxiliary information. A

'G_sign' should be stored in 'sigMap' under its 'gSignSelfIdx'. The

same applies to 'G_morphism' with 'morMap' and 'gMorphismSelfIdx'

resp. 'G_theory' with 'thMap' and 'gTheorySelfIdx'. -}

data DGraph = DGraph

{ globalAnnos :: GlobalAnnos -- ^ global annos of library

, globalEnv :: GlobalEnv -- ^ name entities (specs, views) of a library

, dgBody :: Tree.Gr DGNodeLab DGLinkLab -- ^ actual 'DGraph` tree

, getNewEdgeID :: Int -- ^ edge counter

, refNodes :: Map.Map Node (LIB_NAME, Node) -- ^ unexpanded 'DGRef's

, allRefNodes :: Map.Map (LIB_NAME, Node) Node -- ^ all DGRef's

, sigMap :: Map.Map Int G_sign -- ^ signature map

, thMap :: Map.Map Int G_theory -- ^ morphism map

, morMap :: Map.Map Int G_morphism -- ^ theory map

, proofHistory :: ProofHistory -- ^ applied proof steps

, redoHistory :: ProofHistory -- ^ undone proofs steps

, openlock :: Maybe (MVar (IO ())) -- ^ control of graph display

}

emptyDG :: DGraph

emptyDG = DGraph

{ globalAnnos = emptyGlobalAnnos

, globalEnv = Map.empty

, dgBody = Graph.empty

, getNewEdgeID = 0

, refNodes = Map.empty

, allRefNodes = Map.empty

, sigMap = Map.empty

, thMap = Map.empty

, morMap = Map.empty

, proofHistory = [emptyHistory]

, redoHistory = [emptyHistory]

, openlock = Nothing

}

emptyDGwithMVar :: IO DGraph

emptyDGwithMVar = do

ol <- newEmptyMVar

return $ emptyDG {openlock = Just ol}

-----------------------

-- some set functions

-----------------------

setSigMapDG :: Map.Map Int G_sign -> DGraph -> DGraph

setSigMapDG m dg = dg{sigMap = m}

setThMapDG :: Map.Map Int G_theory -> DGraph -> DGraph

setThMapDG m dg = dg{thMap = m}

setMorMapDG :: Map.Map Int G_morphism -> DGraph -> DGraph

setMorMapDG m dg = dg{morMap = m}

-----------------------

-- some lookup functions

-----------------------

lookupSigMapDG :: Int -> DGraph -> Maybe G_sign

lookupSigMapDG i = Map.lookup i . sigMap

lookupThMapDG :: Int -> DGraph -> Maybe G_theory

lookupThMapDG i = Map.lookup i . thMap

lookupMorMapDG :: Int -> DGraph -> Maybe G_morphism

lookupMorMapDG i = Map.lookup i . morMap

lookupGlobalEnvDG :: SIMPLE_ID -> DGraph -> Maybe GlobalEntry

lookupGlobalEnvDG sid = Map.lookup sid . globalEnv

getMapAndMaxIndex :: (b -> Map.Map Int a) -> b -> (Map.Map Int a, Int)

getMapAndMaxIndex f gctx =

let m = f gctx in (m, if Map.null m then 0 else fst $ Map.findMax m)

sigMapI :: DGraph -> (Map.Map Int G_sign, Int)

sigMapI = getMapAndMaxIndex sigMap

morMapI :: DGraph -> (Map.Map Int G_morphism, Int)

morMapI = getMapAndMaxIndex morMap

thMapI :: DGraph -> (Map.Map Int G_theory, Int)

thMapI = getMapAndMaxIndex thMap

type LibEnv = Map.Map LIB_NAME DGraph

-- | an empty environment

emptyLibEnv :: LibEnv

emptyLibEnv = Map.empty

-- | returns the DGraph that belongs to the given library name

lookupDGraph :: LIB_NAME -> LibEnv -> DGraph

lookupDGraph ln =

Map.findWithDefault (error "lookupDGraph") ln

-- | Heterogenous sentences

type HetSenStatus a = SenStatus a (AnyComorphism,BasicProof)

isProvenSenStatus :: HetSenStatus a -> Bool

isProvenSenStatus = any isProvenSenStatusAux . thmStatus

where isProvenSenStatusAux (_, BasicProof _ pst) = isProvedStat pst

isProvenSenStatusAux _ = False

-- * Grothendieck theory with prover

-- | a pair of prover and theory which are in the same logic

data G_theory_with_prover =

forall lid sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree .

Logic lid sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree =>

G_theory_with_prover lid

(Theory sign sentence proof_tree)

(Prover sign sentence sublogics proof_tree)

-- | weakly amalgamable cocones

gWeaklyAmalgamableCocone :: GDiagram -> Result (G_theory, Map.Map Int GMorphism)

gWeaklyAmalgamableCocone diag =

if isHomogeneousGDiagram diag then do

case head $ labNodes diag of

(_, G_theory lid _ _ _ _) -> do

graph <- homogeniseGDiagram lid diag

(sig, mor) <- signature_colimit lid graph

-- until the amalgamability check is fixed

let gth = G_theory lid (mkExtSign sig) 0 noSens 0

cid = mkIdComorphism lid (top_sublogic lid)

morFun = Map.fromList $

map (\(n, s)->(n, GMorphism cid (mkExtSign s) 0 (mor Map.! n) 0)) $

labNodes graph

return (gth, morFun)

else if not $ isConnected diag then fail "Graph is not connected"

else if not $ isAcyclic $ removeIdentities diag then

-- TO DO: instead of acyclic, test whether the diagram is thin

fail "Graph is not acyclic" else do

let funDesc = initDescList diag

graph <- observe $ hetWeakAmalgCocone diag funDesc

-- TO DO: modify this function so it would return

-- all possible answers and offer them as choices to the user

buildStrMorphisms diag graph

-- | get the available node id

getNewNodeDG :: DGraph -> Node

getNewNodeDG = getNewNode . dgBody

-- | delete the node out of the given DG

delNodeDG :: Node -> DGraph -> DGraph

delNodeDG n dg =

dg{dgBody = delNode n $ dgBody dg}

-- | delete the LNode out of the given DG

delLNodeDG :: LNode DGNodeLab -> DGraph -> DGraph

delLNodeDG n@(v, l) g = case matchDG v g of

(Just(p, _, l', s), g') ->

if l' == l then

if null p && null s then g'

else error $ "delLNodeDG remaining edges: " ++ show (p ++ s)

else error $ "delLNodeDG wrong label: " ++ show n

_ -> error $ "delLNodeDG no such node: " ++ show n

-- | delete a list of nodes out of the given DG

delNodesDG :: [Node] -> DGraph -> DGraph

delNodesDG ns dg =

dg{dgBody = delNodes ns $ dgBody dg}

-- | insert a new node into given DGraph

insNodeDG :: LNode DGNodeLab -> DGraph -> DGraph

insNodeDG n dg =

dg{dgBody = insNode n $ dgBody dg}

-- | add a new referenced node into the refNodes map of the given DG

addToRefNodesDG :: (Node, LIB_NAME, Node) -> DGraph -> DGraph

addToRefNodesDG (n, libn, refn) dg =

dg{refNodes = Map.insert n (libn, refn) $ refNodes dg,

allRefNodes = Map.insert (libn, refn) n $ allRefNodes dg}

-- | delete the given referenced node out of the refnodes map

deleteFromRefNodesDG :: Node -> DGraph -> DGraph

deleteFromRefNodesDG n dg = dg{refNodes = Map.delete n $ refNodes dg}

-- | lookup a referenced node with a node id

lookupInRefNodesDG :: Node -> DGraph -> Maybe (LIB_NAME, Node)

lookupInRefNodesDG n dg =

Map.lookup n $ refNodes dg

-- | look up a refernced node with its parent infor.

lookupInAllRefNodesDG :: (LIB_NAME, Node) -> DGraph -> Maybe Node

lookupInAllRefNodesDG refK dg =

Map.lookup refK $ allRefNodes dg

-- | inserts a lnode into a given DG

insLNodeDG :: LNode DGNodeLab -> DGraph -> DGraph

insLNodeDG n@(v, _) g =

if gelemDG v g then error $ "insLNodeDG " ++ show v else insNodeDG n g

-- | insert a new node with the given node content into a given DGraph

insNodesDG :: [LNode DGNodeLab] -> DGraph -> DGraph

insNodesDG ns dg =

dg{dgBody = insNodes ns $ dgBody dg}

-- | delete an edge out of a given DG

delEdgeDG :: 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"