GraphLogic.hs revision 0d0278c34a374b29c2d6c58b39b8b56e283d48e8
25cc5fbba63f84b47e389af749f55abbbde71c8cChristian MaederModule : $Header$
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederDescription : Logic for manipulating the graph in the Central GUI
25cc5fbba63f84b47e389af749f55abbbde71c8cChristian MaederCopyright : (c) Jorina Freya Gerken, Till Mossakowski, Uni Bremen 2002-2006
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederLicense : GPLv2 or higher, see LICENSE.txt
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederMaintainer : till@informatik.uni-bremen.de
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederStability : provisional
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederPortability : non-portable (imports Logic)
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederThis module provides functions for all the menus in the Hets GUI.
d8c71aacc9f1c8cd40a8ad8dcdad9be8854b849fChristian MaederThese are then assembled to the GUI in "GUI.GraphMenu".
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder , updateGraph
a53841f6d6e86ac751c12a33dc8aadf53f59d977Klaus Luettich , openProofStatus
a53841f6d6e86ac751c12a33dc8aadf53f59d977Klaus Luettich , saveProofStatus
a737caf82de97c1907027c03e4b4509eb492b4b8Christian Maeder , showReferencedLibrary
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich , getTheoryOfNode
96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian Maeder , translateTheoryOfNode
01e383014b555bbcf639c0ca60c5810b3eff83c0Christian Maeder , displaySubsortGraph
3b06e23643a9f65390cb8c1caabe83fa7e87a708Till Mossakowski , displayConceptGraph
df29370ae8d8b41587957f6bcdcb43a3f1927e47Christian Maeder , showProofStatusOfNode
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder , proveAtNode
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder , ensureLockAtNode
ce8b15da31cd181b7e90593cbbca98f47eda29d6Till Mossakowski , showNodeInfo
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder , showDiagMess
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder , showDiagMessAux
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder , showEdgeInfo
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder , checkconservativityOfNode
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder , checkconservativityOfEdge
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder , toggleHideNames
2e2094a642e3775b0d76b890556407941d3a53b6Christian Maeder , toggleHideNodes
2e2094a642e3775b0d76b890556407941d3a53b6Christian Maeder , toggleHideEdges
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder , translateGraph
e8db9a65830cf71504e33c6f441a67b4d184a3caChristian Maeder , showLibGraph
8410667510a76409aca9bb24ff0eda0420088274Christian Maeder , saveUDGraph
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder , calcGlobalHistory
8410667510a76409aca9bb24ff0eda0420088274Christian Maeder , add2history
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettichimport Logic.Coerce (coerceSign)
4cb215739e9ab13447fa21162482ebe485b47455Christian Maederimport Logic.Prover hiding (openProofStatus)
8ef75f1cc0437656bf622cec5ac9e8ea221da8f2Christian Maederimport Comorphisms.LogicGraph (logicGraph)
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maederimport Static.DGTranslation (libEnv_translation, getDGLogic)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederimport Proofs.InferBasic (basicInferenceNode)
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederimport Proofs.StatusUtils (lookupHistory, removeContraryChanges)
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maederimport GUI.Taxonomy (displayConceptGraph, displaySubsortGraph)
7cc09dd93962a2155c34d209d1d4cd7d7b838264Christian Maederimport qualified GUI.GraphAbstraction as GA
c3053d57f642ca507cdf79512e604437c4546cb9Christian Maederimport Reactor.InfoBus (encapsulateWaitTermAct)
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maederimport Common.DocUtils (showDoc, showGlobalDoc)
356fa49fe3e6a8398f92d13e9f920d0f093697ecChristian Maederimport qualified Common.OrderedMap as OMap
356fa49fe3e6a8398f92d13e9f920d0f093697ecChristian Maederimport qualified Common.Lib.SizedList as SizedList
356fa49fe3e6a8398f92d13e9f920d0f093697ecChristian Maederimport Driver.Options ( HetcatsOpts, putIfVerbose, outtypes, doDump, verbose
0206ab93ef846e4e0885996d052b9b73b9dc66b0Christian Maederimport Driver.WriteLibDefn (writeShATermFile)
f13d1e86e58da53680e78043e8df182eed867efbChristian Maederimport Driver.ReadFn (libNameToFile, readVerbose)
757e6c79ec40491d45dc72c82b5eb59a386634b0Jian Chun Wangimport Data.Char (toLower)
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maederimport Data.List (partition, deleteBy, isPrefixOf)
c6fcd42c6d6d9dae8c7835c24fcb7ce8531a9050Christian Maederimport Data.Graph.Inductive.Graph (Node, LEdge, LNode)
31c49f2fa23d4ac089f35145d80a224deb6ea7e4Till Mossakowskiimport qualified Data.Map as Map
8a28707e9155465c6f2236a06eac6580a65c7025Christian Maeder-- | Locks the global lock and runs function
df35538fec1d9135602308d577255c0d466b6365Christian MaederrunAndLock :: GInfo -> IO () -> IO ()
df35538fec1d9135602308d577255c0d466b6365Christian MaederrunAndLock (GInfo { functionLock = lock
431d34c7007a787331c4e5ec997badb0f8190fc7Christian Maeder , graphInfo = gi
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder }) function = do
d3ae0072823e2ef0d41d4431fcc768e66489c20eChristian Maeder locked <- tryPutMVar lock ()
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder if locked then do
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder takeMVar lock
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder "an other function is still working ... please wait ..."
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder-- | Undo one step of the History
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maederundo :: GInfo -> Bool -> IO ()
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maederundo gInfo isUndo = do
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder intSt <- readIORef $ intState gInfo
a7c27282e71cf4505026645f96d4f5cb8a284e32Christian Maeder nwSt <- if isUndo then undoOneStepWithUpdate intSt $ updateGraphAux gInfo
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder else redoOneStepWithUpdate intSt $ updateGraphAux gInfo
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder writeIORef (intState gInfo) nwSt
776a1a086df734581431e6edb4343ed4c8d34d55Christian MaederupdateGraph :: GInfo -> [DGChange] -> IO ()
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian MaederupdateGraph gInfo@(GInfo { libName = ln }) changes = do
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder ost <- readIORef $ intState gInfo
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder case i_state ost of
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder Nothing -> return ()
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Just ist -> updateGraphAux gInfo ln changes $ lookupDGraph ln $ i_libEnv ist
c0c2380bced8159ff0297ece14eba948bd236471Christian MaederupdateGraphAux :: GInfo -> LibName -> [DGChange] -> DGraph -> IO ()
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederupdateGraphAux gInfo' ln changes dg = do
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder og <- readIORef $ openGraphs gInfo'
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Nothing -> return ()
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Just gInfo@(GInfo { graphInfo = gi
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder , options = opts }) -> do
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder flags <- readIORef opts
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder let edges = if flagHideEdges flags then hideEdgesAux dg else []
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder (nodes, comp) = if flagHideNodes flags then hideNodesAux dg edges
0769e2a25732dc2544b2a7425dfa284e24d23b71Christian Maeder else ([], [])
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder "Applying development graph calculus proof rule..."
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder GA.applyChanges gi (removeContraryChanges changes) nodes edges comp
ad4889ebb40efae8595b0969dd6ba1162d52bac3Christian Maeder "Updating graph..."
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder hideNames gInfo
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder "Development graph calculus proof rule finished."
a9b59eb2ce961014974276cdae0e9df4419bd212Christian Maeder-- | Toggles to display internal node names
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian MaederhideNames :: GInfo -> IO ()
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian MaederhideNames (GInfo { options = opts
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder , internalNames = updaterIORef }) = do
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder flags <- readIORef opts
88318aafc287e92931dceffbb943d58a9310001dChristian Maeder updater <- readIORef updaterIORef
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder mapM_ (\ (s, upd) -> upd (const $ if flagHideNames flags then "" else s))
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- | Toggles to display internal node names
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaedertoggleHideNames :: GInfo -> IO ()
363939beade943a02b31004cea09dec34fa8a6d9Christian MaedertoggleHideNames gInfo@(GInfo { graphInfo = gi
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder , options = opts }) = do
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder flags <- readIORef opts
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder let hide = not $ flagHideNames flags
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder writeIORef opts $ flags { flagHideNames = hide }
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder GA.showTemporaryMessage gi $ if hide then "Hiding internal names..."
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder else "Revealing internal names..."
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder updateGraph gInfo []
b568982efd0997d877286faa592d81b03c8c67b8Christian Maeder-- | hides all unnamed internal nodes that are proven
ca074a78b8dcccbb8c419586787882f98d0c6163Christian MaederhideNodesAux :: DGraph -> [EdgeId]
0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich -> ([GA.NodeId], [(GA.NodeId, GA.NodeId, DGEdgeType, Bool)])
ca074a78b8dcccbb8c419586787882f98d0c6163Christian MaederhideNodesAux dg ignoreEdges =
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder let nodes = selectNodesByType dg
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder (\ n -> isInternalSpec n && isProvenNode n && isProvenCons n)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder edges = getCompressedEdges dg nodes ignoreEdges
f2f9df2e17e70674f0bf426ed1763c973ee4cde0Christian Maeder in (nodes, edges)
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian MaedertoggleHideNodes :: GInfo -> IO ()
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian MaedertoggleHideNodes gInfo@(GInfo { graphInfo = gi
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder , options = opts }) = do
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder flags <- readIORef opts
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder let hide = not $ flagHideNodes flags
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder writeIORef opts $ flags { flagHideNodes = hide }
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder GA.showTemporaryMessage gi $ if hide then "Hiding unnamed nodes..."
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder else "Revealing hidden nodes..."
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder updateGraph gInfo []
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederhideEdgesAux :: DGraph -> [EdgeId]
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederhideEdgesAux dg = map dgl_id
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder $ filter (\ (DGLink { dgl_type = linktype }) ->
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder case linktype of
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder ScopedLink _ (ThmLink s) c ->
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder isProvenThmLinkStatus s && isProvenConsStatusLink c
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder HidingFreeOrCofreeThm _ _ _ s -> isProvenThmLinkStatus s
89f7631cbfbd1bb99fc152b434bd362a7799d295Christian Maeder $ foldl (\ e c -> case c of
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder InsertEdge (_, _, lbl) -> lbl : e
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder DeleteEdge (_, _, lbl) -> deleteBy eqDGLinkLabById lbl e
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder ) [] $ flattenHistory (SizedList.toList $ proofHistory dg) []
f4505a64a089693012a3f5c3b1f12a82cd7a2a5aKlaus LuettichtoggleHideEdges :: GInfo -> IO ()
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaedertoggleHideEdges gInfo@(GInfo { graphInfo = gi
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder , options = opts }) = do
f4505a64a089693012a3f5c3b1f12a82cd7a2a5aKlaus Luettich flags <- readIORef opts
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder let hide = not $ flagHideEdges flags
6b6773cf587b74259178641d811746a235faf056Christian Maeder writeIORef opts $ flags { flagHideEdges = hide }
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder GA.showTemporaryMessage gi $ if hide then "Hiding new proven edges..."
2c619a4dfdc1df27573eba98e81ed1ace906941dChristian Maeder else "Revealing hidden proven edges..."
36f63902db2b3463faa9f59912ad106e2d5aaa24Klaus Luettich updateGraph gInfo []
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder-- | generates from list of HistElem one list of DGChanges
e7757995211bd395dc79d26fe017d99375f7d2a6Christian MaederflattenHistory :: [HistElem] -> [DGChange] -> [DGChange]
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederflattenHistory [] cs = cs
01b16c4bdd2a3577214f79a64aed02f54e8a204eChristian MaederflattenHistory (HistElem c : r) cs = flattenHistory r $ c : cs
7c5c311d67e187280877c45bd89dcba9038bc0a3Christian MaederflattenHistory (HistGroup _ ph : r) cs =
7c5c311d67e187280877c45bd89dcba9038bc0a3Christian Maeder flattenHistory r $ flattenHistory (SizedList.toList ph) cs
7c5c311d67e187280877c45bd89dcba9038bc0a3Christian Maeder-- | selects all nodes of a type with outgoing edges
7c5c311d67e187280877c45bd89dcba9038bc0a3Christian MaederselectNodesByType :: DGraph -> (DGNodeType -> Bool) -> [Node]
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederselectNodesByType dg types =
83394c6b6e6de128e71b67c9251ed7a84485d082Christian Maeder filter (\ n -> not (null $ outDG dg n) && hasUnprovenEdges dg n) $ map fst
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder $ filter (types . getRealDGNodeType . snd) $ labNodesDG dg
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederhasUnprovenEdges :: DGraph -> Node -> Bool
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederhasUnprovenEdges dg =
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder foldl (\ b (_, _, l) -> case edgeTypeModInc $ getRealDGLinkType l of
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder ThmType { isProvenEdge = False } -> False
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder _ -> b) True . (\ n -> innDG dg n ++ outDG dg n)
9df11f85fd7f8c4745d64464876e84ec4e263692Christian Maeder-- | compresses a list of types to the highest one
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix ReckerscompressTypes :: Bool -> [DGEdgeType] -> (DGEdgeType, Bool)
010c56c4cf12dd7977ca36efe85219b91e265ee3Christian MaedercompressTypes _ [] = error "compressTypes: wrong usage"
fb328c4f646dd3dd78a9391c5cb58450a3dd0aa9Klaus LuettichcompressTypes b (t : []) = (t, b)
3b06e23643a9f65390cb8c1caabe83fa7e87a708Till MossakowskicompressTypes b (t1 : t2 : r)
5b818f10e11fc79def1fdd5c8a080d64a6438d87Christian Maeder | t1 == t2 = compressTypes b (t1 : r)
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers | t1 > t2 = compressTypes False (t1 : r)
819e29dba060687cf391e444e0f6ff88c1908cc3Christian Maeder | otherwise = compressTypes False (t2 : r)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- | innDG with filter of not shown edges
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian MaederfInnDG :: [EdgeId] -> DGraph -> Node -> [LEdge DGLinkLab]
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix ReckersfInnDG ignore dg = filter (\ (_, _, l) -> notElem (dgl_id l) ignore) . innDG dg
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- | outDG with filter of not shown edges
61fa0ac06ede811c7aad54ec4c4202346727368eChristian MaederfOutDG :: [EdgeId] -> DGraph -> Node -> [LEdge DGLinkLab]
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian MaederfOutDG ignore dg = filter (\ (_, _, l) -> notElem (dgl_id l) ignore) . outDG dg
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder-- | returns a list of compressed edges
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian MaedergetCompressedEdges :: DGraph -> [Node] -> [EdgeId]
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder -> [(Node, Node, DGEdgeType, Bool)]
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian MaedergetCompressedEdges dg hidden ign = filterDuplicates $ getShortPaths
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder $ concatMap (\ e@(_, t, _) -> map (e :) $ getPaths dg t hidden [] ign) inEdges
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder inEdges = filter (\ (_, t, _) -> elem t hidden)
819e29dba060687cf391e444e0f6ff88c1908cc3Christian Maeder $ concatMap (fOutDG ign dg)
819e29dba060687cf391e444e0f6ff88c1908cc3Christian Maeder $ foldr (\ (n, _, _) i -> if elem n hidden
819e29dba060687cf391e444e0f6ff88c1908cc3Christian Maeder || elem n i then i else n : i) []
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder $ concatMap (fInnDG ign dg) hidden
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder-- | filter duplicate paths
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian MaederfilterDuplicates :: [(Node, Node, DGEdgeType, Bool)]
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder -> [(Node, Node, DGEdgeType, Bool)]
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian MaederfilterDuplicates [] = []
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian MaederfilterDuplicates r@((s, t, _, _) : _) = edges ++ filterDuplicates others
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder (same, others) = partition (\ (s', t', _, _) -> s == s' && t == t') r
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder (mtypes, stypes) = partition (\ (_, _, _, b) -> not b) same
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder stypes' = foldr (\ e es -> if elem e es then es else e : es) [] stypes
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder (et', _) = compressTypes False $ map (\ (_, _, et, _) -> et) mtypes
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder edges = if null mtypes then stypes' else (s, t, et', False) : stypes'
ac34194a668399bb8ef238da77c3a09e93fb253bChristian Maeder-- | returns the pahts of a given node through hidden nodes
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian MaedergetPaths :: DGraph -> Node -> [Node] -> [Node] -> [EdgeId]
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder -> [[LEdge DGLinkLab]]
e7757995211bd395dc79d26fe017d99375f7d2a6Christian MaedergetPaths dg node hidden seen' ign = if elem node hidden then
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder if null edges then []
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder else concatMap (\ e@(_, t, _) -> map (e :) $ getPaths dg t hidden seen ign)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder seen = node : seen'
3b06e23643a9f65390cb8c1caabe83fa7e87a708Till Mossakowski edges = filter (\ (_, t, _) -> notElem t seen) $ fOutDG ign dg node
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- | returns source and target node of a path with the compressed type
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaedergetShortPaths :: [[LEdge DGLinkLab]]
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder -> [(Node, Node, DGEdgeType, Bool)]
fb328c4f646dd3dd78a9391c5cb58450a3dd0aa9Klaus LuettichgetShortPaths [] = []
fb328c4f646dd3dd78a9391c5cb58450a3dd0aa9Klaus LuettichgetShortPaths (p : r) =
e96a0bf4040fd789339958c01f145c5057d26db6René Wagner (s, t, et, b)
e96a0bf4040fd789339958c01f145c5057d26db6René Wagner : getShortPaths r
abf2487c3aece95c371ea89ac64319370dcb6483Klaus Luettich (s, _, _) = head p
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder (_, t, _) = last p
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder (et, b) = compressTypes True $ map (\ (_, _, e) -> getRealDGLinkType e) p
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers-- | Let the user select a Node to focus
61fa0ac06ede811c7aad54ec4c4202346727368eChristian MaederfocusNode :: GInfo -> IO ()
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederfocusNode gInfo@(GInfo { graphInfo = gi
b9b960bc75e34658e70c4a0231dbc6a6e7373f2dChristian Maeder , libName = ln }) = do
18a4d5cb6828f080db9c5f9551785c5151027271Christian Maeder ost <- readIORef $ intState gInfo
0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich case i_state ost of
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder Nothing -> return ()
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Just ist -> do
fdb2d618144159395f7bf8ce3327b3c112a17dd3Till Mossakowski let le = i_libEnv ist
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder idsnodes <- filterM (fmap not . GA.isHiddenNode gi . fst)
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder $ labNodesDG $ lookupDGraph ln le
3b06e23643a9f65390cb8c1caabe83fa7e87a708Till Mossakowski selection <- listBox "Select a node to focus"
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder $ map (\ (n, l) -> shows n " " ++ getDGNodeName l) idsnodes
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder case selection of
c9acb8681bcc512245b4f0d1a9f2b189c60e10d4Christian Maeder Just idx -> GA.focusNode gi $ fst $ idsnodes !! idx
38352346eb1a67ba0f4eab8ad6f718528cf0cde0Christian Maeder Nothing -> return ()
63e50b4c36074d5fb9de872c4007b688b4bce534Christian MaedershowLibGraph :: GInfo -> LibFunc -> IO ()
63e50b4c36074d5fb9de872c4007b688b4bce534Christian MaedershowLibGraph gInfo showLib = do
bd54a9917cd87169b8e40bcc5616c537fed85815Christian Maeder showLib gInfo
11b55e6fbbc397b9fa41a7d61be53c6f4f027824Christian MaedersaveProofStatus :: GInfo -> FilePath -> IO ()
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian MaedersaveProofStatus gInfo@(GInfo { hetcatsOpts = opts
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder , libName = ln
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder }) file = encapsulateWaitTermAct $ do
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder ost <- readIORef $ intState gInfo
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder case i_state ost of
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Nothing -> return ()
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Just ist -> do
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder let proofStatus = i_libEnv ist
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder writeShATermFile file (ln, lookupHistory ln proofStatus)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder putIfVerbose opts 2 $ "Wrote " ++ file
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- | implementation of open menu, read in a proof status
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederopenProofStatus :: GInfo -> FilePath -> ConvFunc -> LibFunc
e8db9a65830cf71504e33c6f441a67b4d184a3caChristian MaederopenProofStatus gInfo@(GInfo { hetcatsOpts = opts
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder , libName = ln }) file convGraph showLib = do
1f8a7f8343f7df719768d2b1d7e3077ee291a1caChristian Maeder ost <- readIORef $ intState gInfo
1f8a7f8343f7df719768d2b1d7e3077ee291a1caChristian Maeder case i_state ost of
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder Nothing -> return ()
6bf24e5eb644064ad650eb3fd9774483fccbf601Christian Maeder Just ist -> do
dbe752ee940baae7f9f231f29c62284bb0f90a25Christian Maeder mh <- readVerbose logicGraph opts ln file
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Nothing -> errorDialog "Error" $
53818ced114da21321063fff307aa41c1ab31dd3Achim Mahnke "Could not read proof status from file '" ++ file ++ "'"
53818ced114da21321063fff307aa41c1ab31dd3Achim Mahnke let libfile = libNameToFile ln
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder m <- anaLib opts { outtypes = [] } libfile
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder Nothing -> errorDialog "Error"
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich $ "Could not read original development graph from '"
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder ++ libfile ++ "'"
27785f379d6810811b4e6d23feab18845fde9a98Christian Maeder Just (_, libEnv) -> case Map.lookup ln libEnv of
f443a57f2a8e0ca3daa7431b0c89a18ba52c337aChristian Maeder Nothing -> errorDialog "Error" $ "Could not get original"
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder ++ "development graph for '" ++ showDoc ln "'"
1f63599faaa311cd024d6413f82bff8caae8de24Christian Maeder Just dg -> do
857992065be4ed40a72c6296b6c0aec62ab4c5b9Christian Maeder lockGlobal gInfo
fdb2d618144159395f7bf8ce3327b3c112a17dd3Till Mossakowski let oldEnv = i_libEnv ist
7c99e334446bb97120e30e967baeeddfdd1278deKlaus Luettich proofStatus = Map.insert ln (applyProofHistory h dg) oldEnv
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maeder nwst = ost { i_state = Just ist { i_libEnv = proofStatus } }
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maeder writeIORef (intState gInfo) nwst
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maeder unlockGlobal gInfo
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder gInfo' <- copyGInfo gInfo ln
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder convGraph gInfo' "Proof Status " showLib
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maeder let gi = graphInfo gInfo'
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder-- | apply a rule of the development graph calculus
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian MaederproofMenu :: GInfo
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder -> (LibEnv -> IO (Result LibEnv))
1aee4aaddde105264c1faf394d88e302c05094ffChristian MaederproofMenu gInfo@(GInfo { hetcatsOpts = hOpts
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maeder , libName = ln
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder }) cmd proofFun = do
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder ost <- readIORef $ intState gInfo
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder case i_state ost of
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder Nothing -> return ()
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder Just ist -> do
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder lockGlobal gInfo
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maeder let proofStatus = i_libEnv ist
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder putIfVerbose hOpts 4 "Proof started via menu"
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder Result ds res <- proofFun proofStatus
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder putIfVerbose hOpts 4 "Analyzing result of proof"
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder Nothing -> do
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder unlockGlobal gInfo
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maeder printDiags 2 ds
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder Just newProofStatus -> do
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder let newGr = lookupDGraph ln newProofStatus
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder history = snd $ splitHistory (lookupDGraph ln proofStatus) newGr
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder lln = map DgCommandChange $ calcGlobalHistory
27785f379d6810811b4e6d23feab18845fde9a98Christian Maeder proofStatus newProofStatus
27785f379d6810811b4e6d23feab18845fde9a98Christian Maeder nst = add2history cmd ost lln
27785f379d6810811b4e6d23feab18845fde9a98Christian Maeder nwst = nst { i_state = Just ist { i_libEnv = newProofStatus}}
27785f379d6810811b4e6d23feab18845fde9a98Christian Maeder doDump hOpts "PrintHistory" $ do
27785f379d6810811b4e6d23feab18845fde9a98Christian Maeder putStrLn "History"
4017ebc0f692820736d796af3110c3b3018c108aChristian Maeder print $ prettyHistory history
4017ebc0f692820736d796af3110c3b3018c108aChristian Maeder writeIORef (intState gInfo) nwst
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder updateGraph gInfo (reverse $ flatHistory history)
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder unlockGlobal gInfo
83394c6b6e6de128e71b67c9251ed7a84485d082Christian MaedercalcGlobalHistory :: LibEnv -> LibEnv -> [LibName]
fa21fba9ceb1ddf7b3efd54731a12ed8750191d8Christian MaedercalcGlobalHistory old new = let
fa21fba9ceb1ddf7b3efd54731a12ed8750191d8Christian Maeder length' ln = SizedList.size . proofHistory . lookupDGraph ln
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder changes = filter (\ ln -> length' ln old < length' ln new) $ Map.keys old
0c355dd0b739631ee472f9a656e266be27fa4e64Christian Maeder in concatMap (\ ln -> replicate (length' ln new - length' ln old) ln) changes
fa21fba9ceb1ddf7b3efd54731a12ed8750191d8Christian MaedershowNodeInfo :: Int -> DGraph -> IO ()
b49276c9f50038e0bd499ad49f7bd6444566a834Christian MaedershowNodeInfo descr dgraph = do
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder let dgnode = labDG dgraph descr
b49276c9f50038e0bd499ad49f7bd6444566a834Christian Maeder title = (if isDGRef dgnode then ("reference " ++) else
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder if isInternalNode dgnode then ("internal " ++) else id)
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder "node " ++ getDGNodeName dgnode ++ " " ++ show descr
c7ec85d1103173e089aa5048fd7afb2f9b505124Klaus Luettich createTextDisplay title $ title ++ "\n"
c7ec85d1103173e089aa5048fd7afb2f9b505124Klaus Luettich ++ showGlobalDoc (globalAnnos dgraph) dgnode ""
c7ec85d1103173e089aa5048fd7afb2f9b505124Klaus LuettichshowDiagMessAux :: Int -> [Diagnosis] -> IO ()
c7ec85d1103173e089aa5048fd7afb2f9b505124Klaus LuettichshowDiagMessAux v ds = let es = filterDiags v ds in
b905126bab9454b89041f92b3c50bb9efc85e427Klaus Luettich unless (null es) $ (if hasErrors es then errorDialog "Error"
a883cd4d01fe39d23219cf5333425f195be24d8bChristian Maeder else infoDialog "Info") $ unlines $ map show es
b905126bab9454b89041f92b3c50bb9efc85e427Klaus LuettichshowDiagMess :: HetcatsOpts -> [Diagnosis] -> IO ()
c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus LuettichshowDiagMess = showDiagMessAux . verbose
c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus Luettich{- | outputs the theory of a node in a window;
c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus Luettich used by the node menu -}
c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus LuettichgetTheoryOfNode :: GInfo -> Int -> DGraph -> IO ()
c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus LuettichgetTheoryOfNode gInfo descr dgraph = do
c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus Luettich ost <- readIORef $ intState gInfo
c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus Luettich case i_state ost of
c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus Luettich Nothing -> return ()
c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus Luettich Just ist -> case computeTheory (i_libEnv ist) (libName gInfo) descr of
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder errorDialog "Error" $ "no global theory for node " ++ show descr
b905126bab9454b89041f92b3c50bb9efc85e427Klaus Luettich Just th -> displayTheoryOfNode (getNameOfNode descr dgraph)
b905126bab9454b89041f92b3c50bb9efc85e427Klaus Luettich (addHasInHidingWarning dgraph descr
b905126bab9454b89041f92b3c50bb9efc85e427Klaus Luettich ++ showGlobalDoc (globalAnnos dgraph) th "\n")
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder-- | displays a theory with warning in a window
33d042fe6a9eb27a4c48f840b80838f3e7d98e34Christian MaederdisplayTheoryOfNode :: String -- ^ Name of theory
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder -> String -- ^ Body text
1f8a7f8343f7df719768d2b1d7e3077ee291a1caChristian MaederdisplayTheoryOfNode n = createTextSaveDisplay ("Theory of " ++ n) (n ++ ".het")
1f8a7f8343f7df719768d2b1d7e3077ee291a1caChristian Maeder{- | translate the theory of a node in a window;
1f8a7f8343f7df719768d2b1d7e3077ee291a1caChristian Maeder used by the node menu -}
68aab98a58d1460c77a1573a86c32a891756a420Christian MaedertranslateTheoryOfNode :: GInfo -> Int -> DGraph -> IO ()
1f8a7f8343f7df719768d2b1d7e3077ee291a1caChristian MaedertranslateTheoryOfNode gInfo@(GInfo { hetcatsOpts = opts
1f8a7f8343f7df719768d2b1d7e3077ee291a1caChristian Maeder , libName = ln }) node dgraph = do
96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian Maeder ost <- readIORef $ intState gInfo
96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian Maeder case i_state ost of
1f8a7f8343f7df719768d2b1d7e3077ee291a1caChristian Maeder Nothing -> return ()
3a7788e09dd23b364a46c9488cbd1522369113dbChristian Maeder Just ist -> do
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder let libEnv = i_libEnv ist
ef67402074be14deb95e4ff564737d5593144130Klaus Luettich case computeTheory libEnv ln node of
dbe752ee940baae7f9f231f29c62284bb0f90a25Christian Maeder Just th@(G_theory lid sign _ sens _) -> do
ef67402074be14deb95e4ff564737d5593144130Klaus Luettich -- find all comorphism paths starting from lid
462d9dc583444aab82732e14a75610684d2dc7e9Christian Maeder let paths = findComorphismPaths logicGraph (sublogicOfTh th)
c9e197862d9d8ef2585270dd08f5194b3aed4a9dKlaus Luettich -- let the user choose one
e7e1ab2ac3f1fded8611bb92ae00e8f3b8c693fbKlaus Luettich sel <- listBox "Choose a node logic translation" $ map show paths
1323eba62fc519b068f5aaec4f9d2be05ffabea9Klaus Luettich Nothing -> errorDialog "Error" "no node logic translation chosen"
d784803f9c752667b4fcf7393d698002bedf3f89Klaus Luettich Comorphism cid <- return (paths !! i)
1323eba62fc519b068f5aaec4f9d2be05ffabea9Klaus Luettich -- adjust lid's
1323eba62fc519b068f5aaec4f9d2be05ffabea9Klaus Luettich let lidS = sourceLogic cid
1f8a7f8343f7df719768d2b1d7e3077ee291a1caChristian Maeder lidT = targetLogic cid
1f8a7f8343f7df719768d2b1d7e3077ee291a1caChristian Maeder sign' <- coerceSign lid lidS "" sign
462d9dc583444aab82732e14a75610684d2dc7e9Christian Maeder sens' <- coerceThSens lid lidS "" sens
5d39c60274aaa76506292d2d9e885fccd27e1eabChristian Maeder -- translate theory along chosen comorphism
5d39c60274aaa76506292d2d9e885fccd27e1eabChristian Maeder let Result es mTh = wrapMapTheory cid
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder (plainSign sign', toNamedList sens')
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder Nothing -> showDiagMess opts es
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder Just (sign'', sens1) -> displayTheoryWithWarning
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder "Translated Theory" (getNameOfNode node dgraph)
1f8a7f8343f7df719768d2b1d7e3077ee291a1caChristian Maeder (addHasInHidingWarning dgraph node)
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder $ G_theory lidT (mkExtSign sign'') startSigId (toThSens sens1)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder errorDialog "Error" $ "no global theory for node " ++ show node
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich-- | Show proof status of a node
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian MaedershowProofStatusOfNode :: GInfo -> Int -> DGraph -> IO ()
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaedershowProofStatusOfNode _ descr dgraph =
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder let dgnode = labDG dgraph descr
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder stat = showStatusAux dgnode
f2d9352f2999f82c36b4b65535d14a6a40ae5a82Christian Maeder title = "Proof status of node " ++ showName (dgn_name dgnode)
340706b6c0c6e3dbacdd7003e20e9cab7f9aa765Christian Maeder in createTextDisplay title stat
f2d9352f2999f82c36b4b65535d14a6a40ae5a82Christian MaedershowStatusAux :: DGNodeLab -> String
340706b6c0c6e3dbacdd7003e20e9cab7f9aa765Christian MaedershowStatusAux dgnode = case dgn_theory dgnode of
fdb2d618144159395f7bf8ce3327b3c112a17dd3Till Mossakowski G_theory _ _ _ sens _ ->
aa6c527682224a4e1434f80eae8bc2ef67fb6ca6Christian Maeder let goals = OMap.filter (not . isAxiom) sens
aa6c527682224a4e1434f80eae8bc2ef67fb6ca6Christian Maeder (proven, open) = OMap.partition isProvenSenStatus goals
37951dbd8e5f2418a07f072d9bf551d0c3a1eafcChristian Maeder consGoal = "\nconservativity of this node"
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder in "Proven proof goals:\n"
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder ++ showDoc proven ""
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder ++ if not $ hasOpenNodeConsStatus True dgnode
aa6c527682224a4e1434f80eae8bc2ef67fb6ca6Christian Maeder then consGoal
c22d75ec3ea1306219d1c09a5b3e8ff04f753ad6Christian Maeder ++ "\nOpen proof goals:\n"
9c3edf2b283c09d33b2820696886d1ed32fcadc8Christian Maeder ++ showDoc open ""
c22d75ec3ea1306219d1c09a5b3e8ff04f753ad6Christian Maeder ++ if hasOpenNodeConsStatus False dgnode
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder then consGoal
5bb7eeaca10ea76595229375f907a5a388b7c882Christian MaederhidingWarnDiag :: DGNodeLab -> IO Bool
5bb7eeaca10ea76595229375f907a5a388b7c882Christian MaederhidingWarnDiag dgn = if labelHasHiding dgn then
5bb7eeaca10ea76595229375f907a5a388b7c882Christian Maeder warningDialog "Warning" $ unwords $ hidingWarning ++ ["Try anyway?"]
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder else return True
1aee4aaddde105264c1faf394d88e302c05094ffChristian MaederensureLockAtNode :: GInfo -> Int -> DGraph
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder -> IO (Maybe (DGraph, DGNodeLab, LibEnv))
8410667510a76409aca9bb24ff0eda0420088274Christian MaederensureLockAtNode gi descr dg = do
ddc9315cc0b1f5dd3d8f99a77f1c75064db33b48Christian Maeder let ln = libName gi
ddc9315cc0b1f5dd3d8f99a77f1c75064db33b48Christian Maeder iSt = intState gi
5d522dff4d0fabf57dd476d4c3de15d354a89f62Christian Maeder ost <- readIORef iSt
5d522dff4d0fabf57dd476d4c3de15d354a89f62Christian Maeder case i_state ost of
5d522dff4d0fabf57dd476d4c3de15d354a89f62Christian Maeder Nothing -> return Nothing
8410667510a76409aca9bb24ff0eda0420088274Christian Maeder Just ist -> let
8410667510a76409aca9bb24ff0eda0420088274Christian Maeder le = i_libEnv ist
8410667510a76409aca9bb24ff0eda0420088274Christian Maeder dgn = labDG dg descr in if hasLock dgn
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder then return $ Just (dg, dgn, le)
e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus Luettich lockGlobal gi
e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus Luettich (dgraph', dgn') <- initLocking (lookupDGraph ln le) (descr, dgn)
e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus Luettich let nwle = Map.insert ln dgraph' le
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich nwst = ost { i_state = Just $ ist { i_libEnv = nwle} }
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich writeIORef iSt nwst
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich unlockGlobal gi
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich return $ Just (dgraph', dgn', nwle)
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich-- | start local theorem proving or consistency checking at a node
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus LuettichproveAtNode :: GInfo -> Int -> DGraph -> IO ()
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus LuettichproveAtNode gInfo descr dgraph = do
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich let ln = libName gInfo
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich iSt = intState gInfo
36f63902db2b3463faa9f59912ad106e2d5aaa24Klaus Luettich lockedEnv <- ensureLockAtNode gInfo descr dgraph
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich case lockedEnv of
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich Nothing -> return ()
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich Just (dgraph', dgn', le') -> do
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich acquired <- tryLockLocal dgn'
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich if acquired then do
ac43fa22d2d3f91a17674ac164cba3cf39a17795Klaus Luettich let action = do
ac43fa22d2d3f91a17674ac164cba3cf39a17795Klaus Luettich res@(Result d _) <- basicInferenceNode logicGraph ln dgraph'
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers (descr, dgn') le' iSt
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder when (null d || diagString (head d) /= "Proofs.Proofs: selection")
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers $ runProveAtNode gInfo (descr, dgn') res
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder b <- hidingWarnDiag dgn'
18c1d987ce5818ecf0bfc8af3f43aed2ce86e1eaChristian Maeder when b action
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder unlockLocal dgn'
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder else errorDialog "Error" "Proofwindow already open"
6fe9628743562678acf97d6730ebcfee5e9e50c2Christian MaederrunProveAtNode :: GInfo -> LNode DGNodeLab
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder -> Result G_theory -> IO ()
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian MaederrunProveAtNode gInfo (v, dgnode) (Result ds mres) = case mres of
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder Just newTh ->
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder let oldTh = dgn_theory dgnode
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder rTh = propagateProofs oldTh newTh in
fb328c4f646dd3dd78a9391c5cb58450a3dd0aa9Klaus Luettich unless (rTh == oldTh) $ do
3b06e23643a9f65390cb8c1caabe83fa7e87a708Till Mossakowski showDiagMessAux 2 ds
3b06e23643a9f65390cb8c1caabe83fa7e87a708Till Mossakowski lockGlobal gInfo
3b06e23643a9f65390cb8c1caabe83fa7e87a708Till Mossakowski let ln = libName gInfo
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder iSt = intState gInfo
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder ost <- readIORef iSt
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder let (ost', hist) = updateNodeProof ln ost (v, dgnode) rTh
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder case i_state ost' of
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder Nothing -> return ()
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder writeIORef iSt ost'
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder runAndLock gInfo $ updateGraph gInfo hist
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers unlockGlobal gInfo
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder _ -> return ()
e96a0bf4040fd789339958c01f145c5057d26db6René WagnercheckconservativityOfNode :: GInfo -> Int -> DGraph -> IO ()
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian MaedercheckconservativityOfNode gInfo descr dgraph = do
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder let iSt = intState gInfo
abf2487c3aece95c371ea89ac64319370dcb6483Klaus Luettich ln = libName gInfo
abf2487c3aece95c371ea89ac64319370dcb6483Klaus Luettich nlbl = labDG dgraph descr
abf2487c3aece95c371ea89ac64319370dcb6483Klaus Luettich ost <- readIORef iSt
abf2487c3aece95c371ea89ac64319370dcb6483Klaus Luettich case i_state ost of
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers Nothing -> return ()
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder Just iist -> do
83394c6b6e6de128e71b67c9251ed7a84485d082Christian Maeder b <- hidingWarnDiag nlbl
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers lockGlobal gInfo
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder (str, libEnv', ph) <- checkConservativityNode True (descr, nlbl)
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder (i_libEnv iist) ln
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder if isPrefixOf "No conservativity" str then
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich errorDialog "Result of conservativity check" str
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder createTextDisplay "Result of conservativity check" str
a80c28bb8b7a23ccdf7e08d0fe216fc19cc97273Klaus Luettich let nst = add2history (SelectCmd Node $ showDoc descr "")
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder ost [DgCommandChange ln]
83394c6b6e6de128e71b67c9251ed7a84485d082Christian Maeder nwst = nst { i_state = Just $ iist { i_libEnv = libEnv' }}
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder writeIORef iSt nwst
b9625461755578f3eed04676d42a63fd2caebd0cChristian Maeder runAndLock gInfo $ updateGraph gInfo (reverse $ flatHistory ph)
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder unlockGlobal gInfo
d0652648f9879c67a194f8b03baafe2700c68eb4Christian MaederedgeErr :: Int -> IO ()
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian MaederedgeErr descr = errorDialog "Error" $ "edge with descriptor " ++ show descr
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder ++ " not found in the development graph"
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder-- | print the id, origin, type, proof-status and morphism of the edge
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus LuettichshowEdgeInfo :: Int -> Maybe (LEdge DGLinkLab) -> IO ()
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus LuettichshowEdgeInfo descr me = case me of
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich Just e@(_, _, l) -> let estr = showLEdge e in
83394c6b6e6de128e71b67c9251ed7a84485d082Christian Maeder createTextDisplay ("Info of " ++ estr)
36f63902db2b3463faa9f59912ad106e2d5aaa24Klaus Luettich (estr ++ "\n" ++ showDoc l "")
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder Nothing -> edgeErr descr
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder-- | check conservativity of the edge
27785f379d6810811b4e6d23feab18845fde9a98Christian MaedercheckconservativityOfEdge :: Int -> GInfo -> Maybe (LEdge DGLinkLab) -> IO ()
1aee4aaddde105264c1faf394d88e302c05094ffChristian MaedercheckconservativityOfEdge descr gInfo me = case me of
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder Nothing -> edgeErr descr
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder Just lnk@(_, _, lbl) -> do
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder let iSt = intState gInfo
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder ln = libName gInfo
27785f379d6810811b4e6d23feab18845fde9a98Christian Maeder ost <- readIORef iSt
27785f379d6810811b4e6d23feab18845fde9a98Christian Maeder case i_state ost of
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder Nothing -> return ()
83394c6b6e6de128e71b67c9251ed7a84485d082Christian Maeder Just iist -> do
27785f379d6810811b4e6d23feab18845fde9a98Christian Maeder lockGlobal gInfo
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder (str, nwle, _, ph) <- checkConservativityEdge True lnk
c5e3fc166373b0d90f6e36e8aa234396a1dcd879Christian Maeder (i_libEnv iist) ln
340706b6c0c6e3dbacdd7003e20e9cab7f9aa765Christian Maeder if isPrefixOf "No conservativity" str
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder errorDialog "Result of conservativity check" str
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder createTextDisplay "Result of conservativity check" str
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder let nst = add2history (SelectCmd Link $ showDoc (dgl_id lbl) "")
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder ost [DgCommandChange ln]
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder nwst = nst { i_state = Just $ iist { i_libEnv = nwle}}
2c619a4dfdc1df27573eba98e81ed1ace906941dChristian Maeder writeIORef iSt nwst
2c619a4dfdc1df27573eba98e81ed1ace906941dChristian Maeder runAndLock gInfo $ updateGraph gInfo $ reverse $ flatHistory ph
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder unlockGlobal gInfo
50515239e7e190f4a34ca581dd685d002148fbddChristian Maeder-- | show development graph for library
50515239e7e190f4a34ca581dd685d002148fbddChristian MaedershowDGraph :: GInfo -> LibName -> ConvFunc -> LibFunc -> IO ()
50515239e7e190f4a34ca581dd685d002148fbddChristian MaedershowDGraph gi ln convGraph showLib = do
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder putIfVerbose (hetcatsOpts gi) 3 $ "Converting graph for " ++ show ln
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder og <- readIORef $ openGraphs gi
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder Nothing -> do
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder updateWindowCount gi succ
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder gi' <- copyGInfo gi ln
8b4c68db8b465107cabef8b9cd5b6bc216e1b156Till Mossakowski convGraph gi' "Development Graph" showLib
8b4c68db8b465107cabef8b9cd5b6bc216e1b156Till Mossakowski GA.showTemporaryMessage (graphInfo gi') "Development Graph initialized."
bcaf979d9babe6346aa343687aa7d596e2894cccPaolo Torrini GA.showTemporaryMessage (graphInfo gi') "Development Graph requested."
bcaf979d9babe6346aa343687aa7d596e2894cccPaolo Torrini-- | show library referened by a DGRef node (=node drawn as a box)
5ce19352a9cc47d982819cc889a71cd0a61ac171Christian MaedershowReferencedLibrary :: Int -> GInfo -> ConvFunc -> LibFunc -> IO ()
5ce19352a9cc47d982819cc889a71cd0a61ac171Christian MaedershowReferencedLibrary descr gInfo convGraph showLib = do
5ce19352a9cc47d982819cc889a71cd0a61ac171Christian Maeder ost <- readIORef $ intState gInfo
bcaf979d9babe6346aa343687aa7d596e2894cccPaolo Torrini case i_state ost of
23ab8855c58adfbd03a0730584b917b24c603901Christian Maeder Nothing -> return ()
df29370ae8d8b41587957f6bcdcb43a3f1927e47Christian Maeder Just ist -> do
23ab8855c58adfbd03a0730584b917b24c603901Christian Maeder let le = i_libEnv ist
e50e41135ece589f7202bd4ef8d6b97531c2a56eKlaus Luettich ln = libName gInfo
47b0e9f3cb008cb7997f4e3bae26e4d62dcc887aChristian Maeder refNode = labDG (lookupDGraph ln le) descr
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder refLibname = if isDGRef refNode then dgn_libname refNode
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder else error "showReferencedLibrary"
431d34c7007a787331c4e5ec997badb0f8190fc7Christian Maeder case Map.lookup refLibname le of
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder Just _ -> showDGraph gInfo refLibname convGraph showLib
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder Nothing -> errorDialog "Error"
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder $ "The referenced library (" ++ show refLibname ++ ") is unknown"
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder-- | display a window of translated graph with maximal sublogic.
88318aafc287e92931dceffbb943d58a9310001dChristian MaedertranslateGraph :: GInfo -> IO (Maybe LibEnv)
43b4c41fbb07705c9df321221ab9cb9832460407Christian MaedertranslateGraph gInfo@(GInfo { hetcatsOpts = opts }) = do
88318aafc287e92931dceffbb943d58a9310001dChristian Maeder ost <- readIORef $ intState gInfo
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder case i_state ost of
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder Nothing -> return Nothing
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder Just ist -> do
e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus Luettich le = i_libEnv ist
9096f6c6aaded6cd8288656ceccd4c7b3bd0747eChristian Maeder Result diagsSl mSublogic = getDGLogic le
9096f6c6aaded6cd8288656ceccd4c7b3bd0747eChristian Maeder myErrMess = showDiagMess opts
e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus Luettich error' = errorDialog "Error"
e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus Luettich if hasErrors diagsSl then do
e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus Luettich myErrMess diagsSl
e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus Luettich return Nothing
e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus Luettich else case mSublogic of
e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus Luettich Nothing -> do
e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus Luettich error' "No maximal sublogic found."
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder return Nothing
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder Just sublogic -> do
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder let paths = findComorphismPaths logicGraph sublogic
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder if null paths then do
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder error' "This graph has no comorphism to translation."
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder return Nothing
fdef3358918491badb0e29e42b5d3b5a01950716Christian Maeder sel <- listBox "Choose a logic translation" $ map show paths
6ff7a91875597d6e4dfaa68c79187d01473e8341Christian Maeder Nothing -> do
6ff7a91875597d6e4dfaa68c79187d01473e8341Christian Maeder error' "no logic translation chosen"
88318aafc287e92931dceffbb943d58a9310001dChristian Maeder return Nothing
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder let Result diag mle = libEnv_translation le $ paths !! j
7767474aba4fa2dc51a6c68017d3bcef3b773001Christian Maeder Just newLibEnv -> do
88318aafc287e92931dceffbb943d58a9310001dChristian Maeder showDiagMess opts $ diagsSl ++ diag
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder return $ Just newLibEnv
fdb2d618144159395f7bf8ce3327b3c112a17dd3Till Mossakowski Nothing -> do
340706b6c0c6e3dbacdd7003e20e9cab7f9aa765Christian Maeder myErrMess $ diagsSl ++ diag
88318aafc287e92931dceffbb943d58a9310001dChristian Maeder return Nothing
88318aafc287e92931dceffbb943d58a9310001dChristian Maeder-- | saves the uDrawGraph graph to a file
fdb2d618144159395f7bf8ce3327b3c112a17dd3Till MossakowskisaveUDGraph :: GInfo -> Map.Map DGNodeType (Shape value, String)
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder -> Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String) -> IO ()
6e049108aa87dc46bcff96fae50a4625df1d9648Klaus LuettichsaveUDGraph gInfo@(GInfo { graphInfo = gi
473bc1f3f3443f18e0ee83e4642fab42183470f2Christian Maeder , libName = ln }) nodemap linkmap = do
473bc1f3f3443f18e0ee83e4642fab42183470f2Christian Maeder ost <- readIORef $ intState gInfo
6e049108aa87dc46bcff96fae50a4625df1d9648Klaus Luettich case i_state ost of
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder Nothing -> return ()
f4505a64a089693012a3f5c3b1f12a82cd7a2a5aKlaus Luettich maybeFilePath <- fileSaveDialog (rmSuffix (libNameToFile ln) ++ ".udg")
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder [ ("uDrawGraph", ["*.udg"])
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder , ("All Files", ["*"])] Nothing
f4505a64a089693012a3f5c3b1f12a82cd7a2a5aKlaus Luettich case maybeFilePath of
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder Just filepath -> do
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder GA.showTemporaryMessage gi "Converting graph..."
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder nstring <- nodes2String gInfo nodemap linkmap
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder writeFile filepath nstring
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder GA.showTemporaryMessage gi $ "Graph stored to " ++ filepath ++ "!"
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder Nothing -> GA.showTemporaryMessage gi "Aborted!"
1a6464613c59e35072b90ca296ae402cbe956144Christian Maeder-- | Converts the nodes of the graph to String representation
0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettichnodes2String :: GInfo -> Map.Map DGNodeType (Shape value, String)
0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich -> Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String)
0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettichnodes2String gInfo@(GInfo { graphInfo = gi
0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich , libName = ln }) nodemap linkmap = do
0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich ost <- readIORef $ intState gInfo
0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich case i_state ost of
0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich Nothing -> return []
0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich Just ist -> do
0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich let le = i_libEnv ist
0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich nodes <- filterM (fmap not . GA.isHiddenNode gi . fst)
0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich $ labNodesDG $ lookupDGraph ln le
2e62113845a35e07cb46db05714627c95450f267Klaus Luettich nstring <- foldM (\ s ->
0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich fmap ((if null s then s else s ++ ",\n") ++)
0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich . node2String gInfo nodemap linkmap)
0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich return $ "[" ++ nstring ++ "]"
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder-- | Converts a node to String representation
9e748851c150e1022fb952bab3315e869aaf0214Christian Maedernode2String :: GInfo -> Map.Map DGNodeType (Shape value, String)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder -> Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String)
88318aafc287e92931dceffbb943d58a9310001dChristian Maeder -> LNode DGNodeLab -> IO String
438f9bd974c8e668203e636b0f2bc80c589af043Klaus Luettichnode2String gInfo nodemap linkmap (nid, dgnode) = do
88318aafc287e92931dceffbb943d58a9310001dChristian Maeder label <- getNodeLabel gInfo dgnode
feac53e31a8351e3e3c6621f6a14b5714008bfc7Heng Jiang let ntype = getRealDGNodeType dgnode
89c9d707aa817684b88036a2dad66c3437840677Heng Jiang (shape, color) <- case Map.lookup ntype nodemap of
af12672e86f22a822a9915a21efbbbc04a01e3c1Heng Jiang Nothing -> error $ "SaveGraph: can't lookup nodetype: " ++ show ntype
af12672e86f22a822a9915a21efbbbc04a01e3c1Heng Jiang Just (s, c) -> return (s, c)
af12672e86f22a822a9915a21efbbbc04a01e3c1Heng Jiang object = "a(\"OBJECT\",\"" ++ label ++ "\"),"
af12672e86f22a822a9915a21efbbbc04a01e3c1Heng Jiang color' = "a(\"COLOR\",\"" ++ color ++ "\"),"
af12672e86f22a822a9915a21efbbbc04a01e3c1Heng Jiang shape' = "a(\"_GO\",\"" ++ map toLower (show shape) ++ "\")"
8394ed8354319d3d5c72780813ea9a868b9d379fHeng Jiang links <- links2String gInfo linkmap nid
77aa4b87bdccf1aa41b01546cbe093a58f846bdaHeng Jiang return $ "l(\"" ++ show nid ++ "\",n(\"" ++ show ntype ++ "\","
02b60bce7eac99f86a8f80bf3f651bdaf7316e0eHeng Jiang ++ "[" ++ object ++ color' ++ shape' ++ "],"
8394ed8354319d3d5c72780813ea9a868b9d379fHeng Jiang ++ "\n [" ++ links ++ "]))"
02b60bce7eac99f86a8f80bf3f651bdaf7316e0eHeng Jiang-- | Converts all links of a node to String representation
02b60bce7eac99f86a8f80bf3f651bdaf7316e0eHeng Jianglinks2String :: GInfo -> Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String)
8394ed8354319d3d5c72780813ea9a868b9d379fHeng Jiang -> Int -> IO String
02b60bce7eac99f86a8f80bf3f651bdaf7316e0eHeng Jianglinks2String gInfo@(GInfo { graphInfo = gi
02b60bce7eac99f86a8f80bf3f651bdaf7316e0eHeng Jiang , libName = ln }) linkmap nodeid = do
c8d5f54940ff821a1b55da52f3b55be432507ba3Heng Jiang ost <- readIORef $ intState gInfo
8394ed8354319d3d5c72780813ea9a868b9d379fHeng Jiang case i_state ost of
af12672e86f22a822a9915a21efbbbc04a01e3c1Heng Jiang Nothing -> return []
af12672e86f22a822a9915a21efbbbc04a01e3c1Heng Jiang Just ist -> do
af12672e86f22a822a9915a21efbbbc04a01e3c1Heng Jiang let le = i_libEnv ist
af12672e86f22a822a9915a21efbbbc04a01e3c1Heng Jiang edges <- filterM (\ (src, _, edge) -> do
af12672e86f22a822a9915a21efbbbc04a01e3c1Heng Jiang let eid = dgl_id edge
af12672e86f22a822a9915a21efbbbc04a01e3c1Heng Jiang return $ not b && src == nodeid)
af12672e86f22a822a9915a21efbbbc04a01e3c1Heng Jiang $ labEdgesDG $ lookupDGraph ln le
af12672e86f22a822a9915a21efbbbc04a01e3c1Heng Jiang foldM (\ s edge -> do
af12672e86f22a822a9915a21efbbbc04a01e3c1Heng Jiang s' <- link2String linkmap edge
feac53e31a8351e3e3c6621f6a14b5714008bfc7Heng Jiang return $ (if null s then "" else s ++ ",\n") ++ s') "" edges
(line, color) <- case Map.lookup ltype linkmap of