GraphLogic.hs revision 9da6e0cb2ea6e43f5b09dcd2a9af5468a5d0fcf4
842ae4bd224140319ae7feec1872b93dfd491143fieldingModule : $Header$
842ae4bd224140319ae7feec1872b93dfd491143fieldingDescription : Logic for manipulating the graph in the Central GUI
842ae4bd224140319ae7feec1872b93dfd491143fieldingCopyright : (c) Jorina Freya Gerken, Till Mossakowski, Uni Bremen 2002-2006
842ae4bd224140319ae7feec1872b93dfd491143fieldingLicense : GPLv2 or higher, see LICENSE.txt
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesMaintainer : till@informatik.uni-bremen.de
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesStability : provisional
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesPortability : non-portable (imports Logic)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesThis module provides functions for all the menus in the Hets GUI.
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesThese are then assembled to the GUI in "GUI.GraphMenu".
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes , updateGraph
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes , openProofStatus
e8f95a682820a599fe41b22977010636be5c2717jim , saveProofStatus
e8f95a682820a599fe41b22977010636be5c2717jim , showDGraph
1747d30b98aa1bdbc43994c02cd46ab4cb9319e4fielding , showReferencedLibrary
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes , getTheoryOfNode
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes , translateTheoryOfNode
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes , displaySubsortGraph
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes , displayConceptGraph
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes , showProofStatusOfNode
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes , proveAtNode
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes , showNodeInfo
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes , showDiagMess
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes , showEdgeInfo
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes , checkconservativityOfNode
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes , checkconservativityOfEdge
5c0419d51818eb02045cf923a9fe456127a44c60wrowe , toggleHideNames
5c0419d51818eb02045cf923a9fe456127a44c60wrowe , toggleHideNodes
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes , toggleHideEdges
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes , translateGraph
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes , showLibGraph
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes , runAndLock
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes , saveUDGraph
d266c3777146d36a4c23c17aad6f153aebea1bf4jortonimport Logic.Coerce (coerceSign)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesimport Logic.Prover hiding (openProofStatus)
22f8da8087791fcb95b836c8a81937c5a9bba202bnicholesimport Comorphisms.LogicGraph (logicGraph)
22f8da8087791fcb95b836c8a81937c5a9bba202bnicholesimport Static.DGTranslation (libEnv_translation, getDGLogic)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesimport Proofs.InferBasic (basicInferenceNode)
0568280364eb026393be492ebc732795c4934643jortonimport Proofs.StatusUtils (lookupHistory, removeContraryChanges)
0568280364eb026393be492ebc732795c4934643jortonimport GUI.Taxonomy (displayConceptGraph, displaySubsortGraph)
0568280364eb026393be492ebc732795c4934643jortonimport qualified GUI.GraphAbstraction as GA
0568280364eb026393be492ebc732795c4934643jortonimport Reactor.InfoBus (encapsulateWaitTermAct)
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovenerimport Common.DocUtils (showDoc)
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovenerimport Common.AS_Annotation (isAxiom)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesimport qualified Common.OrderedMap as OMap
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesimport qualified Common.Lib.SizedList as SizedList
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesimport Driver.Options ( HetcatsOpts, putIfVerbose, outtypes, doDump, verbose
796e4a7141265d8ed7036e4628161c6eafb2a789jortonimport Driver.WriteLibDefn (writeShATermFile)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesimport Driver.ReadFn (libNameToFile, readVerbose)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesimport Driver.AnaLib (anaLib)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesimport Data.Char (toLower)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesimport Data.List (partition, delete, isPrefixOf)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesimport Data.Graph.Inductive.Graph (Node, LEdge, LNode)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesimport qualified Data.Map as Map
482f676c6c19b1c5bb5cca04dad11509c1da3a4cwrowe-- | Locks the global lock and runs function
e8f95a682820a599fe41b22977010636be5c2717jimrunAndLock :: GInfo -> IO () -> IO ()
482f676c6c19b1c5bb5cca04dad11509c1da3a4cwrowerunAndLock (GInfo { functionLock = lock
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes , graphInfo = gi
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes }) function = do
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes locked <- tryPutMVar lock ()
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes if locked then do
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes takeMVar lock
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes "an other function is still working ... please wait ..."
a1790fb35c4b352dab721370985c623a9f8f5062rpluem-- | Undo one step of the History
713a2b68bac4aeb1e9c48785006c0732451039depquernaundo :: GInfo -> Bool -> IO ()
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesundo gInfo isUndo = do
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes intSt <- readIORef $ intState gInfo
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes nwSt <- if isUndo then undoOneStepWithUpdate intSt $ updateGraphAux gInfo
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes else redoOneStepWithUpdate intSt $ updateGraphAux gInfo
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes writeIORef (intState gInfo) nwSt
482f676c6c19b1c5bb5cca04dad11509c1da3a4cwroweupdateGraph :: GInfo -> [DGChange] -> IO ()
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesupdateGraph gInfo@(GInfo { libName = ln }) changes = do
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes ost <- readIORef $ intState gInfo
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes case i_state ost of
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes Nothing -> return ()
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes Just ist -> updateGraphAux gInfo ln changes $ lookupDGraph ln $ i_libEnv ist
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesupdateGraphAux :: GInfo -> LibName -> [DGChange] -> DGraph -> IO ()
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesupdateGraphAux gInfo' ln changes dg = do
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovener og <- readIORef $ openGraphs gInfo'
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes case Map.lookup ln og of
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes Nothing -> return ()
f43b67c5a9d29b572eac916f8335cedc80c908bebnicholes Just gInfo@(GInfo { graphInfo = gi
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes , options = opts }) -> do
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes flags <- readIORef opts
8113dac419143273351446c3ad653f3fe5ba5cfdwrowe let edges = if flagHideEdges flags then hideEdgesAux dg else []
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes (nodes, comp) = if flagHideNodes flags then hideNodesAux dg edges
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes else ([], [])
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes "Applying development graph calculus proof rule..."
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes GA.applyChanges gi (removeContraryChanges changes) nodes edges comp
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes "Updating graph..."
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes hideNames gInfo
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovener "Development graph calculus proof rule finished."
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovener-- | Toggles to display internal node names
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovenerhideNames :: GInfo -> IO ()
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovenerhideNames (GInfo { options = opts
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes , internalNames = updaterIORef }) = do
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovener flags <- readIORef opts
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes updater <- readIORef updaterIORef
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovener mapM_ (\ (s, upd) -> upd (const $ if flagHideNames flags then "" else s))
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | Toggles to display internal node names
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholestoggleHideNames :: GInfo -> IO ()
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholestoggleHideNames gInfo@(GInfo { graphInfo = gi
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes , options = opts }) = do
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovener flags <- readIORef opts
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes let hide = not $ flagHideNames flags
8113dac419143273351446c3ad653f3fe5ba5cfdwrowe writeIORef opts $ flags { flagHideNames = hide }
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes GA.showTemporaryMessage gi $ if hide then "Hiding internal names..."
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes else "Revealing internal names..."
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes updateGraph gInfo []
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | hides all unnamed internal nodes that are proven
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholeshideNodesAux :: DGraph -> [EdgeId]
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes -> ([GA.NodeId], [(GA.NodeId, GA.NodeId, DGEdgeType, Bool)])
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholeshideNodesAux dg ignoreEdges =
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes let nodes = selectNodesByType dg
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes (\ n -> isInternalSpec n && isProvenNode n && isProvenCons n)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes edges = getCompressedEdges dg nodes ignoreEdges
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes in (nodes, edges)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholestoggleHideNodes :: GInfo -> IO ()
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholestoggleHideNodes gInfo@(GInfo { graphInfo = gi
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes , options = opts }) = do
1f299703465bd9975d94e9f229f76af807442de2covener flags <- readIORef opts
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovener let hide = not $ flagHideNodes flags
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovener writeIORef opts $ flags { flagHideNodes = hide }
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovener GA.showTemporaryMessage gi $ if hide then "Hiding unnamed nodes..."
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes else "Revealing hidden nodes..."
8113dac419143273351446c3ad653f3fe5ba5cfdwrowe updateGraph gInfo []
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholeshideEdgesAux :: DGraph -> [EdgeId]
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholeshideEdgesAux dg = map dgl_id
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes $ filter (\ (DGLink { dgl_type = linktype }) ->
9ad7b260be233be7d7b5576979825cac72e15498rederpj case linktype of
9ad7b260be233be7d7b5576979825cac72e15498rederpj ScopedLink _ (ThmLink s) c ->
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes isProvenThmLinkStatus s && isProvenConsStatusLink c
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes HidingFreeOrCofreeThm _ _ s -> isProvenThmLinkStatus s
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes $ foldl (\ e c -> case c of
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes InsertEdge (_, _, lbl) -> lbl : e
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes DeleteEdge (_, _, lbl) -> delete lbl e
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes ) [] $ flattenHistory (SizedList.toList $ proofHistory dg) []
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholestoggleHideEdges :: GInfo -> IO ()
3e6d7277b90d3011db832139afc20efb5f17e203rederpjtoggleHideEdges gInfo@(GInfo { graphInfo = gi
3e6d7277b90d3011db832139afc20efb5f17e203rederpj , options = opts }) = do
3e6d7277b90d3011db832139afc20efb5f17e203rederpj flags <- readIORef opts
3e6d7277b90d3011db832139afc20efb5f17e203rederpj let hide = not $ flagHideEdges flags
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes writeIORef opts $ flags { flagHideEdges = hide }
f43b67c5a9d29b572eac916f8335cedc80c908bebnicholes GA.showTemporaryMessage gi $ if hide then "Hiding new proven edges..."
e8f95a682820a599fe41b22977010636be5c2717jim else "Revealing hidden proven edges..."
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovener updateGraph gInfo []
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovener-- | generates from list of HistElem one list of DGChanges
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovenerflattenHistory :: [HistElem] -> [DGChange] -> [DGChange]
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovenerflattenHistory [] cs = cs
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovenerflattenHistory (HistElem c : r) cs = flattenHistory r $ c : cs
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovenerflattenHistory (HistGroup _ ph : r) cs =
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovener flattenHistory r $ flattenHistory (SizedList.toList ph) cs
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovener-- | selects all nodes of a type with outgoing edges
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovenerselectNodesByType :: DGraph -> (DGNodeType -> Bool) -> [Node]
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovenerselectNodesByType dg types =
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovener filter (\ n -> not (null $ outDG dg n) && hasUnprovenEdges dg n) $ map fst
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovener $ filter (types . getRealDGNodeType . snd) $ labNodesDG dg
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovenerhasUnprovenEdges :: DGraph -> Node -> Bool
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovenerhasUnprovenEdges dg =
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovener foldl (\ b (_, _, l) -> case edgeTypeModInc $ getRealDGLinkType l of
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovener ThmType { isProvenEdge = False } -> False
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovener _ -> b) True . (\ n -> innDG dg n ++ outDG dg n)
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovener-- | compresses a list of types to the highest one
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovenercompressTypes :: Bool -> [DGEdgeType] -> (DGEdgeType, Bool)
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovenercompressTypes _ [] = error "compressTypes: wrong usage"
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovenercompressTypes b (t : []) = (t, b)
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovenercompressTypes b (t1 : t2 : r)
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovener | t1 == t2 = compressTypes b (t1 : r)
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovener | t1 > t2 = compressTypes False (t1 : r)
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovener | otherwise = compressTypes False (t2 : r)
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovener-- | innDG with filter of not shown edges
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovenerfInnDG :: [EdgeId] -> DGraph -> Node -> [LEdge DGLinkLab]
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovenerfInnDG ignore dg = filter (\ (_, _, l) -> notElem (dgl_id l) ignore) . innDG dg
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovener-- | outDG with filter of not shown edges
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovenerfOutDG :: [EdgeId] -> DGraph -> Node -> [LEdge DGLinkLab]
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesfOutDG ignore dg = filter (\ (_, _, l) -> notElem (dgl_id l) ignore) . outDG dg
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovener-- | returns a list of compressed edges
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovenergetCompressedEdges :: DGraph -> [Node] -> [EdgeId]
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovener -> [(Node, Node, DGEdgeType, Bool)]
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovenergetCompressedEdges dg hidden ign = filterDuplicates $ getShortPaths
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovener $ concatMap (\ e@(_, t, _) -> map (e :) $ getPaths dg t hidden [] ign) inEdges
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovener inEdges = filter (\ (_, t, _) -> elem t hidden)
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovener $ concatMap (fOutDG ign dg)
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovener $ foldr (\ (n, _, _) i -> if elem n hidden
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovener || elem n i then i else n : i) []
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovener $ concatMap (fInnDG ign dg) hidden
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovener-- | filter duplicate paths
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovenerfilterDuplicates :: [(Node, Node, DGEdgeType, Bool)]
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovener -> [(Node, Node, DGEdgeType, Bool)]
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovenerfilterDuplicates [] = []
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovenerfilterDuplicates r@((s, t, _, _) : _) = edges ++ filterDuplicates others
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovener (same, others) = partition (\ (s', t', _, _) -> s == s' && t == t') r
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes (mtypes, stypes) = partition (\ (_, _, _, b) -> not b) same
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes stypes' = foldr (\ e es -> if elem e es then es else e : es) [] stypes
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes (et', _) = compressTypes False $ map (\ (_, _, et, _) -> et) mtypes
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes edges = if null mtypes then stypes' else (s, t, et', False) : stypes'
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | returns the pahts of a given node through hidden nodes
b08925593f214f621161742925dcf074a8047e0acovenergetPaths :: DGraph -> Node -> [Node] -> [Node] -> [EdgeId]
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes -> [[LEdge DGLinkLab]]
54d22ed1c429b903b029bbd62621f11a9e286137minfringetPaths dg node hidden seen' ign = if elem node hidden then
465bb68501690d7a47bfd2a6129580047d76d8f1rederpj if null edges then []
3dfeb02cfb853d8717ca0cc259b59fea610173f5bnicholes else concatMap (\ e@(_, t, _) -> map (e :) $ getPaths dg t hidden seen ign)
3dfeb02cfb853d8717ca0cc259b59fea610173f5bnicholes seen = node : seen'
54d22ed1c429b903b029bbd62621f11a9e286137minfrin edges = filter (\ (_, t, _) -> notElem t seen) $ fOutDG ign dg node
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes-- | returns source and target node of a path with the compressed type
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholesgetShortPaths :: [[LEdge DGLinkLab]]
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes -> [(Node, Node, DGEdgeType, Bool)]
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholesgetShortPaths [] = []
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholesgetShortPaths (p : r) =
ebe5305f8b22507374358f32b74d12fb50c05a25covener (s, t, et, b)
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes : getShortPaths r
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes (s, _, _) = head p
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes (_, t, _) = last p
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes (et, b) = compressTypes True $ map (\ (_, _, e) -> getRealDGLinkType e) p
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes-- | Let the user select a Node to focus
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesfocusNode :: GInfo -> IO ()
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesfocusNode gInfo@(GInfo { graphInfo = gi
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes , libName = ln }) = do
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes ost <- readIORef $ intState gInfo
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes case i_state ost of
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes Nothing -> return ()
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes Just ist -> do
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes let le = i_libEnv ist
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes idsnodes <- filterM (fmap not . GA.isHiddenNode gi . fst)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes $ labNodesDG $ lookupDGraph ln le
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes selection <- listBox "Select a node to focus"
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes $ map (\ (n, l) -> shows n " " ++ getDGNodeName l) idsnodes
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes case selection of
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes Just idx -> GA.focusNode gi $ fst $ idsnodes !! idx
9ad7b260be233be7d7b5576979825cac72e15498rederpj Nothing -> return ()
9ad7b260be233be7d7b5576979825cac72e15498rederpjshowLibGraph :: GInfo -> LibFunc -> IO ()
9ad7b260be233be7d7b5576979825cac72e15498rederpjshowLibGraph gInfo showLib = do
9ad7b260be233be7d7b5576979825cac72e15498rederpj showLib gInfo
9ad7b260be233be7d7b5576979825cac72e15498rederpjsaveProofStatus :: GInfo -> FilePath -> IO ()
9ad7b260be233be7d7b5576979825cac72e15498rederpjsaveProofStatus gInfo@(GInfo { hetcatsOpts = opts
9ad7b260be233be7d7b5576979825cac72e15498rederpj , libName = ln
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes }) file = encapsulateWaitTermAct $ do
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes ost <- readIORef $ intState gInfo
54d22ed1c429b903b029bbd62621f11a9e286137minfrin case i_state ost of
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes Nothing -> return ()
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes Just ist -> do
ebe5305f8b22507374358f32b74d12fb50c05a25covener let proofStatus = i_libEnv ist
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes writeShATermFile file (ln, lookupHistory ln proofStatus)
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes putIfVerbose opts 2 $ "Wrote " ++ file
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes-- | implementation of open menu, read in a proof status
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholesopenProofStatus :: GInfo -> FilePath -> ConvFunc -> LibFunc
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholesopenProofStatus gInfo@(GInfo { hetcatsOpts = opts
54d22ed1c429b903b029bbd62621f11a9e286137minfrin , libName = ln }) file convGraph showLib = do
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes ost <- readIORef $ intState gInfo
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes case i_state ost of
ebe5305f8b22507374358f32b74d12fb50c05a25covener Nothing -> return ()
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes Just ist -> do
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes mh <- readVerbose logicGraph opts ln file
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes Nothing -> errorDialog "Error" $
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes "Could not read proof status from file '" ++ file ++ "'"
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes Just h -> do
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes let libfile = libNameToFile ln
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes m <- anaLib opts { outtypes = [] } libfile
b08925593f214f621161742925dcf074a8047e0acovener Nothing -> errorDialog "Error"
b08925593f214f621161742925dcf074a8047e0acovener $ "Could not read original development graph from '"
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes ++ libfile ++ "'"
9ad7b260be233be7d7b5576979825cac72e15498rederpj Just (_, libEnv) -> case Map.lookup ln libEnv of
9ad7b260be233be7d7b5576979825cac72e15498rederpj Nothing -> errorDialog "Error" $ "Could not get original"
9ad7b260be233be7d7b5576979825cac72e15498rederpj ++ "development graph for '" ++ showDoc ln "'"
128a5d93141a86e3afa151e921035a07297c9833rederpj Just dg -> do
9ad7b260be233be7d7b5576979825cac72e15498rederpj lockGlobal gInfo
9ad7b260be233be7d7b5576979825cac72e15498rederpj let oldEnv = i_libEnv ist
128a5d93141a86e3afa151e921035a07297c9833rederpj proofStatus = Map.insert ln (applyProofHistory h dg) oldEnv
128a5d93141a86e3afa151e921035a07297c9833rederpj nwst = ost { i_state = Just ist { i_libEnv = proofStatus } }
9ad7b260be233be7d7b5576979825cac72e15498rederpj writeIORef (intState gInfo) nwst
9ad7b260be233be7d7b5576979825cac72e15498rederpj unlockGlobal gInfo
9ad7b260be233be7d7b5576979825cac72e15498rederpj gInfo' <- copyGInfo gInfo ln
9ad7b260be233be7d7b5576979825cac72e15498rederpj convGraph gInfo' "Proof Status " showLib
128a5d93141a86e3afa151e921035a07297c9833rederpj let gi = graphInfo gInfo'
9ad7b260be233be7d7b5576979825cac72e15498rederpj-- | apply a rule of the development graph calculus
128a5d93141a86e3afa151e921035a07297c9833rederpjproofMenu :: GInfo
9ad7b260be233be7d7b5576979825cac72e15498rederpj -> (LibEnv -> IO (Result LibEnv))
9ad7b260be233be7d7b5576979825cac72e15498rederpjproofMenu gInfo@(GInfo { hetcatsOpts = hOpts
9ad7b260be233be7d7b5576979825cac72e15498rederpj , libName = ln
9ad7b260be233be7d7b5576979825cac72e15498rederpj }) cmd proofFun = do
9ad7b260be233be7d7b5576979825cac72e15498rederpj ost <- readIORef $ intState gInfo
9ad7b260be233be7d7b5576979825cac72e15498rederpj case i_state ost of
9ad7b260be233be7d7b5576979825cac72e15498rederpj Nothing -> return ()
9ad7b260be233be7d7b5576979825cac72e15498rederpj Just ist -> do
9ad7b260be233be7d7b5576979825cac72e15498rederpj lockGlobal gInfo
9ad7b260be233be7d7b5576979825cac72e15498rederpj let proofStatus = i_libEnv ist
9ad7b260be233be7d7b5576979825cac72e15498rederpj putIfVerbose hOpts 4 "Proof started via menu"
9ad7b260be233be7d7b5576979825cac72e15498rederpj Result ds res <- proofFun proofStatus
9ad7b260be233be7d7b5576979825cac72e15498rederpj putIfVerbose hOpts 4 "Analyzing result of proof"
9ad7b260be233be7d7b5576979825cac72e15498rederpj case res of
9ad7b260be233be7d7b5576979825cac72e15498rederpj Nothing -> do
9ad7b260be233be7d7b5576979825cac72e15498rederpj unlockGlobal gInfo
9ad7b260be233be7d7b5576979825cac72e15498rederpj printDiags 2 ds
7add8f7fb048534390571801b7794f71cd9e127abnicholes Just newProofStatus -> do
7add8f7fb048534390571801b7794f71cd9e127abnicholes let newGr = lookupDGraph ln newProofStatus
8445dae5cc606ba8ba04efc341cc1e081d95920drpluem history = snd $ splitHistory (lookupDGraph ln proofStatus) newGr
8445dae5cc606ba8ba04efc341cc1e081d95920drpluem lln = map DgCommandChange $ calcGlobalHistory
7add8f7fb048534390571801b7794f71cd9e127abnicholes proofStatus newProofStatus
7add8f7fb048534390571801b7794f71cd9e127abnicholes nst = add2history cmd ost lln
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes nwst = nst { i_state = Just ist { i_libEnv = newProofStatus}}
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes doDump hOpts "PrintHistory" $ do
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes putStrLn "History"
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes print $ prettyHistory history
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes writeIORef (intState gInfo) nwst
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes updateGraph gInfo (reverse $ flatHistory history)
7add8f7fb048534390571801b7794f71cd9e127abnicholes unlockGlobal gInfo
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholescalcGlobalHistory :: LibEnv -> LibEnv -> [LibName]
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholescalcGlobalHistory old new = let
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes length' ln = SizedList.size . proofHistory . lookupDGraph ln
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes changes = filter (\ ln -> length' ln old < length' ln new) $ Map.keys old
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes in concatMap (\ ln -> replicate (length' ln new - length' ln old) ln) changes
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholesshowNodeInfo :: Int -> DGraph -> IO ()
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholesshowNodeInfo descr dgraph = do
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes let dgnode = labDG dgraph descr
7add8f7fb048534390571801b7794f71cd9e127abnicholes title = (if isDGRef dgnode then ("reference " ++) else
7add8f7fb048534390571801b7794f71cd9e127abnicholes if isInternalNode dgnode then ("internal " ++) else id)
141e1368614dc7564e1627671361b01b4869b491bnicholes "node " ++ getDGNodeName dgnode ++ " " ++ show descr
3dfeb02cfb853d8717ca0cc259b59fea610173f5bnicholes createTextDisplay title (title ++ "\n" ++ showDoc dgnode "")
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholesshowDiagMessAux :: Int -> [Diagnosis] -> IO ()
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholesshowDiagMessAux v ds = let es = filterDiags v ds in
e8f95a682820a599fe41b22977010636be5c2717jim unless (null es) $ (if hasErrors es then errorDialog "Error"
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes else infoDialog "Info") $ unlines $ map show es
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholesshowDiagMess :: HetcatsOpts -> [Diagnosis] -> IO ()
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholesshowDiagMess = showDiagMessAux . verbose
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes{- | outputs the theory of a node in a window;
3dfeb02cfb853d8717ca0cc259b59fea610173f5bnicholes used by the node menu -}
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholesgetTheoryOfNode :: GInfo -> Int -> DGraph -> IO ()
3dfeb02cfb853d8717ca0cc259b59fea610173f5bnicholesgetTheoryOfNode gInfo descr dgraph = do
3dfeb02cfb853d8717ca0cc259b59fea610173f5bnicholes ost <- readIORef $ intState gInfo
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes case i_state ost of
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes Nothing -> return ()
e8f95a682820a599fe41b22977010636be5c2717jim Just ist -> case computeTheory (i_libEnv ist) (libName gInfo) descr of
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes errorDialog "Error" $ "no global theory for node " ++ show descr
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes Just th -> displayTheoryWithWarning "Theory" (getNameOfNode descr dgraph)
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes (addHasInHidingWarning dgraph descr) th
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes{- | translate the theory of a node in a window;
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes used by the node menu -}
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholestranslateTheoryOfNode :: GInfo -> Int -> DGraph -> IO ()
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholestranslateTheoryOfNode gInfo@(GInfo { hetcatsOpts = opts
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes , libName = ln }) node dgraph = do
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes ost <- readIORef $ intState gInfo
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes case i_state ost of
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes Nothing -> return ()
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes Just ist -> do
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes let libEnv = i_libEnv ist
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes case computeTheory libEnv ln node of
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes Just th@(G_theory lid sign _ sens _) -> do
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes -- find all comorphism paths starting from lid
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes let paths = findComorphismPaths logicGraph (sublogicOfTh th)
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes -- let the user choose one
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes sel <- listBox "Choose a node logic translation" $ map show paths
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes Nothing -> errorDialog "Error" "no node logic translation chosen"
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes Just i -> do
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes Comorphism cid <- return (paths !! i)
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes -- adjust lid's
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes let lidS = sourceLogic cid
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes lidT = targetLogic cid
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes sign' <- coerceSign lid lidS "" sign
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes sens' <- coerceThSens lid lidS "" sens
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes -- translate theory along chosen comorphism
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes let Result es mTh = wrapMapTheory cid
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes (plainSign sign', toNamedList sens')
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes Nothing -> showDiagMess opts es
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes Just (sign'', sens1) -> displayTheoryWithWarning
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes "Translated Theory" (getNameOfNode node dgraph)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes (addHasInHidingWarning dgraph node)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes $ G_theory lidT (mkExtSign sign'') startSigId (toThSens sens1)
e8f95a682820a599fe41b22977010636be5c2717jim Nothing ->
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes errorDialog "Error" $ "no global theory for node " ++ show node
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | Show proof status of a node
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesshowProofStatusOfNode :: GInfo -> Int -> DGraph -> IO ()
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesshowProofStatusOfNode _ descr dgraph =
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes let dgnode = labDG dgraph descr
54d22ed1c429b903b029bbd62621f11a9e286137minfrin stat = showStatusAux dgnode
54d22ed1c429b903b029bbd62621f11a9e286137minfrin title = "Proof status of node " ++ showName (dgn_name dgnode)
54d22ed1c429b903b029bbd62621f11a9e286137minfrin in createTextDisplay title stat
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesshowStatusAux :: DGNodeLab -> String
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholesshowStatusAux dgnode = case dgn_theory dgnode of
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes G_theory _ _ _ sens _ ->
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes let goals = OMap.filter (not . isAxiom) sens
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes (proven, open) = OMap.partition isProvenSenStatus goals
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes consGoal = "\nconservativity of this node"
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes in "Proven proof goals:\n"
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes ++ showDoc proven ""
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes ++ if not $ hasOpenNodeConsStatus True dgnode
d330a801b1e5d63a4b8b4fd431542ad0903fd71bbnicholes then consGoal
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes ++ "\nOpen proof goals:\n"
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes ++ showDoc open ""
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes ++ if hasOpenNodeConsStatus False dgnode
54d22ed1c429b903b029bbd62621f11a9e286137minfrin then consGoal
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholeshidingWarnDiag :: DGNodeLab -> IO Bool
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholeshidingWarnDiag dgn = if labelHasHiding dgn then
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes warningDialog "Warning" $ unwords $ hidingWarning ++ ["Try anyway?"]
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes else return True
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | start local theorem proving or consistency checking at a node
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesproveAtNode :: GInfo -> Int -> DGraph -> IO ()
54d22ed1c429b903b029bbd62621f11a9e286137minfrinproveAtNode gInfo descr dgraph = do
54d22ed1c429b903b029bbd62621f11a9e286137minfrin let ln = libName gInfo
54d22ed1c429b903b029bbd62621f11a9e286137minfrin iSt = intState gInfo
54d22ed1c429b903b029bbd62621f11a9e286137minfrin ost <- readIORef iSt
54d22ed1c429b903b029bbd62621f11a9e286137minfrin case i_state ost of
54d22ed1c429b903b029bbd62621f11a9e286137minfrin Nothing -> return ()
54d22ed1c429b903b029bbd62621f11a9e286137minfrin Just ist -> do
54d22ed1c429b903b029bbd62621f11a9e286137minfrin let le = i_libEnv ist
54d22ed1c429b903b029bbd62621f11a9e286137minfrin dgn = labDG dgraph descr
e8f95a682820a599fe41b22977010636be5c2717jim (dgraph', dgn', le') <- if hasLock dgn then return (dgraph, dgn, le)
8a03cd420b800a2428f49f4617293de9b2387b20jorton lockGlobal gInfo
54d22ed1c429b903b029bbd62621f11a9e286137minfrin (dgraph', dgn') <- initLocking (lookupDGraph ln le) (descr, dgn)
54d22ed1c429b903b029bbd62621f11a9e286137minfrin let nwle = Map.insert ln dgraph' le
54d22ed1c429b903b029bbd62621f11a9e286137minfrin nwst = ost { i_state = Just $ ist { i_libEnv = nwle} }
54d22ed1c429b903b029bbd62621f11a9e286137minfrin writeIORef iSt nwst
54d22ed1c429b903b029bbd62621f11a9e286137minfrin unlockGlobal gInfo
54d22ed1c429b903b029bbd62621f11a9e286137minfrin return (dgraph', dgn', nwle)
54d22ed1c429b903b029bbd62621f11a9e286137minfrin acquired <- tryLockLocal dgn'
54d22ed1c429b903b029bbd62621f11a9e286137minfrin if acquired then do
54d22ed1c429b903b029bbd62621f11a9e286137minfrin let action = do
54d22ed1c429b903b029bbd62621f11a9e286137minfrin res@(Result d _) <- basicInferenceNode logicGraph ln dgraph'
54d22ed1c429b903b029bbd62621f11a9e286137minfrin (descr, dgn') le' iSt
54d22ed1c429b903b029bbd62621f11a9e286137minfrin when (null d || diagString (head d) /= "Proofs.Proofs: selection")
54d22ed1c429b903b029bbd62621f11a9e286137minfrin $ runProveAtNode gInfo (descr, dgn') res
54d22ed1c429b903b029bbd62621f11a9e286137minfrin b <- hidingWarnDiag dgn'
54d22ed1c429b903b029bbd62621f11a9e286137minfrin when b action
54d22ed1c429b903b029bbd62621f11a9e286137minfrin unlockLocal dgn'
54d22ed1c429b903b029bbd62621f11a9e286137minfrin else errorDialog "Error" "Proofwindow already open"
edc346c3223efd41e6a2057c37cea69744b73dccwrowerunProveAtNode :: GInfo -> LNode DGNodeLab
54d22ed1c429b903b029bbd62621f11a9e286137minfrin -> Result G_theory -> IO ()
54d22ed1c429b903b029bbd62621f11a9e286137minfrinrunProveAtNode gInfo (v, dgnode) (Result ds mres) = case mres of
54d22ed1c429b903b029bbd62621f11a9e286137minfrin Just newTh ->
54d22ed1c429b903b029bbd62621f11a9e286137minfrin let oldTh = dgn_theory dgnode
54d22ed1c429b903b029bbd62621f11a9e286137minfrin rTh = propagateProofs oldTh newTh in
54d22ed1c429b903b029bbd62621f11a9e286137minfrin unless (rTh == oldTh) $ do
54d22ed1c429b903b029bbd62621f11a9e286137minfrin showDiagMessAux 2 ds
54d22ed1c429b903b029bbd62621f11a9e286137minfrin lockGlobal gInfo
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes let ln = libName gInfo
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes iSt = intState gInfo
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes ost <- readIORef iSt
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes let (ost', hist) = updateNodeProof ln ost (v, dgnode) rTh
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes case i_state ost' of
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes Nothing -> return ()
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes Just _ -> do
e8f95a682820a599fe41b22977010636be5c2717jim writeIORef iSt ost'
e8f95a682820a599fe41b22977010636be5c2717jim runAndLock gInfo $ updateGraph gInfo hist
482f676c6c19b1c5bb5cca04dad11509c1da3a4cwrowe unlockGlobal gInfo
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes _ -> return ()
8113dac419143273351446c3ad653f3fe5ba5cfdwrowecheckconservativityOfNode :: GInfo -> Int -> DGraph -> IO ()
8113dac419143273351446c3ad653f3fe5ba5cfdwrowecheckconservativityOfNode gInfo descr dgraph = do
8113dac419143273351446c3ad653f3fe5ba5cfdwrowe let iSt = intState gInfo
f0f6f1b90ab582896f8a7d56d85bd62a55e57d90covener ln = libName gInfo
8113dac419143273351446c3ad653f3fe5ba5cfdwrowe nlbl = labDG dgraph descr
54d22ed1c429b903b029bbd62621f11a9e286137minfrin ost <- readIORef iSt
560fd0658902ab57754616c172d8953e69fc4722bnicholes case i_state ost of
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes Nothing -> return ()
e8f95a682820a599fe41b22977010636be5c2717jim Just iist -> do
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes b <- hidingWarnDiag nlbl
9ad7b260be233be7d7b5576979825cac72e15498rederpj lockGlobal gInfo
9ad7b260be233be7d7b5576979825cac72e15498rederpj (str, libEnv', ph) <- checkConservativityNode True (descr, nlbl)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes (i_libEnv iist) ln
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes if isPrefixOf "No conservativity" str then
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes errorDialog "Result of conservativity check" str
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes createTextDisplay "Result of conservativity check" str
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes let nst = add2history (SelectCmd Node $ showDoc descr "")
560fd0658902ab57754616c172d8953e69fc4722bnicholes ost [DgCommandChange ln]
560fd0658902ab57754616c172d8953e69fc4722bnicholes nwst = nst { i_state = Just $ iist { i_libEnv = libEnv' }}
560fd0658902ab57754616c172d8953e69fc4722bnicholes writeIORef iSt nwst
560fd0658902ab57754616c172d8953e69fc4722bnicholes runAndLock gInfo $ updateGraph gInfo (reverse $ flatHistory ph)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes unlockGlobal gInfo
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesedgeErr :: Int -> IO ()
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesedgeErr descr = errorDialog "Error" $ "edge with descriptor " ++ show descr
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes ++ " not found in the development graph"
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | print the id, origin, type, proof-status and morphism of the edge
e8f95a682820a599fe41b22977010636be5c2717jimshowEdgeInfo :: Int -> Maybe (LEdge DGLinkLab) -> IO ()
e8f95a682820a599fe41b22977010636be5c2717jimshowEdgeInfo descr me = case me of
e8f95a682820a599fe41b22977010636be5c2717jim Just e@(_, _, l) -> let estr = showLEdge e in
e8f95a682820a599fe41b22977010636be5c2717jim createTextDisplay ("Info of " ++ estr)
e8f95a682820a599fe41b22977010636be5c2717jim (estr ++ "\n" ++ showDoc l "")
e8f95a682820a599fe41b22977010636be5c2717jim Nothing -> edgeErr descr
482f676c6c19b1c5bb5cca04dad11509c1da3a4cwrowe-- | check conservativity of the edge
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholescheckconservativityOfEdge :: Int -> GInfo -> Maybe (LEdge DGLinkLab) -> IO ()
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholescheckconservativityOfEdge descr gInfo me = case me of
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes Nothing -> edgeErr descr
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes Just lnk@(_, _, lbl) -> do
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes let iSt = intState gInfo
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes ln = libName gInfo
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes ost <- readIORef iSt
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes case i_state ost of
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes Nothing -> return ()
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes Just iist -> do
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes lockGlobal gInfo
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes (str, nwle, _, ph) <- checkConservativityEdge True lnk
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes (i_libEnv iist) ln
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes if isPrefixOf "No conservativity" str
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes errorDialog "Result of conservativity check" str
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes createTextDisplay "Result of conservativity check" str
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes let nst = add2history (SelectCmd Link $ showDoc (dgl_id lbl) "")
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes ost [DgCommandChange ln]
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes nwst = nst { i_state = Just $ iist { i_libEnv = nwle}}
e8f95a682820a599fe41b22977010636be5c2717jim writeIORef iSt nwst
560fd0658902ab57754616c172d8953e69fc4722bnicholes runAndLock gInfo $ updateGraph gInfo $ reverse $ flatHistory ph
e8f95a682820a599fe41b22977010636be5c2717jim unlockGlobal gInfo
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | show development graph for library
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesshowDGraph :: GInfo -> LibName -> ConvFunc -> LibFunc -> IO ()
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesshowDGraph gi ln convGraph showLib = do
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes putIfVerbose (hetcatsOpts gi) 3 $ "Converting graph for " ++ show ln
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes og <- readIORef $ openGraphs gi
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes case Map.lookup ln og of
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes Nothing -> do
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes updateWindowCount gi succ
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes gi' <- copyGInfo gi ln
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes convGraph gi' "Development Graph" showLib
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes GA.showTemporaryMessage (graphInfo gi') "Development Graph initialized."
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes GA.showTemporaryMessage (graphInfo gi') "Development Graph requested."
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | show library referened by a DGRef node (=node drawn as a box)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesshowReferencedLibrary :: Int -> GInfo -> ConvFunc -> LibFunc -> IO ()
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesshowReferencedLibrary descr gInfo convGraph showLib = do
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes ost <- readIORef $ intState gInfo
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes case i_state ost of
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes Nothing -> return ()
0e05808dc59a321566303084c84b9826a4353cefrederpj Just ist -> do
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes let le = i_libEnv ist
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes ln = libName gInfo
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes refNode = labDG (lookupDGraph ln le) descr
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovener refLibname = if isDGRef refNode then dgn_libname refNode
0e05808dc59a321566303084c84b9826a4353cefrederpj else error "showReferencedLibrary"
ebe5305f8b22507374358f32b74d12fb50c05a25covener case Map.lookup refLibname le of
ebe5305f8b22507374358f32b74d12fb50c05a25covener Just _ -> showDGraph gInfo refLibname convGraph showLib
ebe5305f8b22507374358f32b74d12fb50c05a25covener Nothing -> error $ "The referenced library (" ++ show refLibname
ebe5305f8b22507374358f32b74d12fb50c05a25covener ++ ") is unknown"
ebe5305f8b22507374358f32b74d12fb50c05a25covener-- | display a window of translated graph with maximal sublogic.
ebe5305f8b22507374358f32b74d12fb50c05a25covenertranslateGraph :: GInfo -> IO (Maybe LibEnv)
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovenertranslateGraph gInfo@(GInfo { hetcatsOpts = opts }) = do
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovener ost <- readIORef $ intState gInfo
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovener case i_state ost of
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovener Nothing -> return Nothing
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovener Just ist -> do
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovener le = i_libEnv ist
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovener Result diagsSl mSublogic = getDGLogic le
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovener myErrMess = showDiagMess opts
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovener error' = errorDialog "Error"
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovener if hasErrors diagsSl then do
0e05808dc59a321566303084c84b9826a4353cefrederpj myErrMess diagsSl
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes return Nothing
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovener else case mSublogic of
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes Nothing -> do
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes error' "No maximal sublogic found."
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes return Nothing
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovener Just sublogic -> do
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes let paths = findComorphismPaths logicGraph sublogic
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes if null paths then do
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes error' "This graph has no comorphism to translation."
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes return Nothing
9ad7b260be233be7d7b5576979825cac72e15498rederpj sel <- listBox "Choose a logic translation" $ map show paths
54d22ed1c429b903b029bbd62621f11a9e286137minfrin case sel of
54d22ed1c429b903b029bbd62621f11a9e286137minfrin Nothing -> do
54d22ed1c429b903b029bbd62621f11a9e286137minfrin error' "no logic translation chosen"
54d22ed1c429b903b029bbd62621f11a9e286137minfrin return Nothing
54d22ed1c429b903b029bbd62621f11a9e286137minfrin Just j -> do
54d22ed1c429b903b029bbd62621f11a9e286137minfrin let Result diag mle = libEnv_translation le $ paths !! j
54d22ed1c429b903b029bbd62621f11a9e286137minfrin Just newLibEnv -> do
54d22ed1c429b903b029bbd62621f11a9e286137minfrin showDiagMess opts $ diagsSl ++ diag
54d22ed1c429b903b029bbd62621f11a9e286137minfrin return $ Just newLibEnv
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes Nothing -> do
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovener myErrMess $ diagsSl ++ diag
4e9c24785b525d2956e6e381015c0f2bd0a72f4bcovener return Nothing
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | saves the uDrawGraph graph to a file
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholessaveUDGraph :: GInfo -> Map.Map DGNodeType (Shape value, String)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes -> Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String) -> IO ()
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholessaveUDGraph gInfo@(GInfo { graphInfo = gi
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes , libName = ln }) nodemap linkmap = do
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes ost <- readIORef $ intState gInfo
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes case i_state ost of
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes Nothing -> return ()
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes Just _ -> do
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes maybeFilePath <- fileSaveDialog (rmSuffix (libNameToFile ln) ++ ".udg")
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes [ ("uDrawGraph", ["*.udg"])
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes , ("All Files", ["*"])] Nothing
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes case maybeFilePath of
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes Just filepath -> do
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes GA.showTemporaryMessage gi "Converting graph..."
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes nstring <- nodes2String gInfo nodemap linkmap
482f676c6c19b1c5bb5cca04dad11509c1da3a4cwrowe writeFile filepath nstring
482f676c6c19b1c5bb5cca04dad11509c1da3a4cwrowe GA.showTemporaryMessage gi $ "Graph stored to " ++ filepath ++ "!"
e8f95a682820a599fe41b22977010636be5c2717jim Nothing -> GA.showTemporaryMessage gi "Aborted!"
482f676c6c19b1c5bb5cca04dad11509c1da3a4cwrowe-- | Converts the nodes of the graph to String representation
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesnodes2String :: GInfo -> Map.Map DGNodeType (Shape value, String)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes -> Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes -> IO String
e8f95a682820a599fe41b22977010636be5c2717jimnodes2String gInfo@(GInfo { graphInfo = gi
e8f95a682820a599fe41b22977010636be5c2717jim , libName = ln }) nodemap linkmap = do
8113dac419143273351446c3ad653f3fe5ba5cfdwrowe ost <- readIORef $ intState gInfo
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes case i_state ost of
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes Nothing -> return []
e8f95a682820a599fe41b22977010636be5c2717jim Just ist -> do
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes let le = i_libEnv ist
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes nodes <- filterM (fmap not . GA.isHiddenNode gi . fst)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes $ labNodesDG $ lookupDGraph ln le
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes nstring <- foldM (\ s ->
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes fmap ((if null s then s else s ++ ",\n") ++)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes . node2String gInfo nodemap linkmap)
482f676c6c19b1c5bb5cca04dad11509c1da3a4cwrowe return $ "[" ++ nstring ++ "]"
482f676c6c19b1c5bb5cca04dad11509c1da3a4cwrowe-- | Converts a node to String representation
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesnode2String :: GInfo -> Map.Map DGNodeType (Shape value, String)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes -> Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes -> LNode DGNodeLab -> IO String
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesnode2String gInfo nodemap linkmap (nid, dgnode) = do
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes label <- getNodeLabel gInfo dgnode
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes let ntype = getRealDGNodeType dgnode
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes (shape, color) <- case Map.lookup ntype nodemap of
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes Nothing -> error $ "SaveGraph: can't lookup nodetype: " ++ show ntype
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes Just (s, c) -> return (s, c)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes object = "a(\"OBJECT\",\"" ++ label ++ "\"),"
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes color' = "a(\"COLOR\",\"" ++ color ++ "\"),"
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes shape' = "a(\"_GO\",\"" ++ map toLower (show shape) ++ "\")"
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes links <- links2String gInfo linkmap nid
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes return $ "l(\"" ++ show nid ++ "\",n(\"" ++ show ntype ++ "\","
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes ++ "[" ++ object ++ color' ++ shape' ++ "],"
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes ++ "\n [" ++ links ++ "]))"
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | Converts all links of a node to String representation
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholeslinks2String :: GInfo -> Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes -> Int -> IO String
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholeslinks2String gInfo@(GInfo { graphInfo = gi
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes , libName = ln }) linkmap nodeid = do
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes ost <- readIORef $ intState gInfo
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes case i_state ost of
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes Nothing -> return []
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes Just ist -> do
e8f95a682820a599fe41b22977010636be5c2717jim let le = i_libEnv ist
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes edges <- filterM (\ (src, _, edge) -> do
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes let eid = dgl_id edge
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes return $ not b && src == nodeid)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes $ labEdgesDG $ lookupDGraph ln le
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes foldM (\ s edge -> do
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes s' <- link2String linkmap edge
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes return $ (if null s then "" else s ++ ",\n") ++ s') "" edges
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | Converts a link to String representation
e8f95a682820a599fe41b22977010636be5c2717jimlink2String :: Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes -> LEdge DGLinkLab -> IO String
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholeslink2String linkmap (nodeid1, nodeid2, edge) = do
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes let (EdgeId linkid) = dgl_id edge
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes ltype = getRealDGLinkType edge
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes (line, color) <- case Map.lookup ltype linkmap of
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes Nothing -> error $ "SaveGraph: can't lookup linktype: " ++ show ltype
43c3e6a4b559b76b750c245ee95e2782c15b4296jim Just (l, c) -> return (l, c)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes nm = "\"" ++ show linkid ++ ":" ++ show nodeid1 ++ "->"
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes ++ show nodeid2 ++ "\""
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes color' = "a(\"EDGECOLOR\",\"" ++ color ++ "\"),"
f43b67c5a9d29b572eac916f8335cedc80c908bebnicholes line' = "a(\"EDGEPATTERN\",\"" ++ map toLower (show line) ++ "\")"
43c3e6a4b559b76b750c245ee95e2782c15b4296jim return $ "l(" ++ nm ++ ",e(\"" ++ show ltype ++ "\","
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes ++ "[" ++ color' ++ line' ++ "],"
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes ++ "r(\"" ++ show nodeid2 ++ "\")))"
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | Returns the name of the Node
37af4b0cf648275b68ff41c866c665b4ccf4667dcovenergetNodeLabel :: GInfo -> DGNodeLab -> IO String
37af4b0cf648275b68ff41c866c665b4ccf4667dcovenergetNodeLabel (GInfo { options = opts }) dgnode = do
37af4b0cf648275b68ff41c866c665b4ccf4667dcovener flags <- readIORef opts
37af4b0cf648275b68ff41c866c665b4ccf4667dcovener return $ if flagHideNames flags && isInternalNode dgnode
482f676c6c19b1c5bb5cca04dad11509c1da3a4cwrowe then "" else getDGNodeName dgnode