GraphLogic.hs revision aa21e7aa42fef563dea0cc77edbde76f66cdbe88
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyerModule : $Header$
6b26240dca29e026900a83d51c75ca230a072a16Thiemo WiedemeyerDescription : Logic for manipulating the graph in the Central GUI
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyerCopyright : (c) Jorina Freya Gerken, Till Mossakowski, Uni Bremen 2002-2006
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyerLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
2eeec5240b424984e3ee26296da1eeab6c6d739eChristian MaederMaintainer : till@informatik.uni-bremen.de
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyerStability : provisional
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyerPortability : non-portable (imports Logic)
7520452bb30b5abbd471f82352fc4c1c937e02c5Till MossakowskiThis module provides functions for all the menus in the Hets GUI.
7520452bb30b5abbd471f82352fc4c1c937e02c5Till MossakowskiThese are then assembled to the GUI in "GUI.GraphMenu".
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer , performProofAction
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer , openProofStatus
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer , saveProofStatus
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer , showReferencedLibrary
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer , getTheoryOfNode
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer , translateTheoryOfNode
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer , displaySubsortGraph
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer , displayConceptGraph
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer , showProofStatusOfNode
38122cbf09ad3dcc31a826cc4093f630515a5cfcChristian Maeder , showNodeInfo
83263d411f611d9902ef4d98c93be6ad9361c833Christian Maeder , showDiagMess
521045d36343cd17dd217a81d4b9422ad6ab6a07Christian Maeder , showEdgeInfo
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer , checkconservativityOfEdge
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo Wiedemeyer , toggleHideNodes
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo Wiedemeyer , toggleHideEdges
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo Wiedemeyer , hideShowNames
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo Wiedemeyer , translateGraph
331603b37dec12e37e2e1df9634ef0f2c5c73ddfThiemo Wiedemeyer , showLibGraph
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyerimport Logic.Coerce(coerceSign)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyerimport Static.DGTranslation(libEnv_translation, getDGLogic)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyerimport Proofs.InferBasic(basicInferenceNode)
36f69d35e01d2d6b6bdc165b49661f2a80af8687Mihai Codescuimport Proofs.StatusUtils(lookupHistory, removeContraryChanges)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyerimport GUI.Taxonomy (displayConceptGraph,displaySubsortGraph)
d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyerimport qualified GUI.GraphAbstraction as GA
4e9e95ba35a68f3c767bc0b23ebf9e904e442517Christian Maederimport Reactor.InfoBus(encapsulateWaitTermAct)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyerimport qualified GUI.HTkUtils as HTk
4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian Maederimport qualified Common.OrderedMap as OMap
f456529a89bfb620d39e5fd5b0a53b24643db96dDominik Lueckeimport qualified Common.Lib.SizedList as SizedList
4c8d3c5a9e938633f6147b5a595b9b93bfca99e6Christian Maederimport Driver.Options(HetcatsOpts,putIfVerbose,outtypes,doDump,verbose,rmSuffix)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyerimport Driver.WriteLibDefn(writeShATermFile)
c745add71930134bc085a544783213179bd3e734Thiemo Wiedemeyerimport Driver.ReadFn(libNameToFile, readVerbose)
02a84229da51532505a93fc2abfca1ccf81b4446Razvan Pascanuimport Data.Char(toLower)
1ac36418f204bbe56f4cd951a979180721758999Christian Maederimport Data.List(partition, delete, isPrefixOf)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyerimport Data.Graph.Inductive.Graph (Node, LEdge, LNode)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyerimport qualified Data.Map as Map
331603b37dec12e37e2e1df9634ef0f2c5c73ddfThiemo Wiedemeyer-- | Locks the global lock and runs function
331603b37dec12e37e2e1df9634ef0f2c5c73ddfThiemo WiedemeyerrunAndLock :: GInfo -> IO () -> IO ()
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo WiedemeyerrunAndLock (GInfo { functionLock = lock
331603b37dec12e37e2e1df9634ef0f2c5c73ddfThiemo Wiedemeyer , graphInfo = gi
331603b37dec12e37e2e1df9634ef0f2c5c73ddfThiemo Wiedemeyer }) function = do
331603b37dec12e37e2e1df9634ef0f2c5c73ddfThiemo Wiedemeyer locked <- tryPutMVar lock ()
331603b37dec12e37e2e1df9634ef0f2c5c73ddfThiemo Wiedemeyer case locked of
331603b37dec12e37e2e1df9634ef0f2c5c73ddfThiemo Wiedemeyer "an other function is still working ... please wait ..."
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer-- | Undo one step of the History
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyerundo :: GInfo -> Bool -> IO ()
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanuundo gInfo isUndo = do
0b8b26a22f136a9b2a8e99d655f6fe6b0b96008cThiemo Wiedemeyer intSt <- readIORef $ intState gInfo
0b8b26a22f136a9b2a8e99d655f6fe6b0b96008cThiemo Wiedemeyer nwSt <- if isUndo then undoOneStepWithUpdate intSt $ updateGraph gInfo
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu else redoOneStepWithUpdate intSt $ updateGraph gInfo
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer writeIORef (intState gInfo) nwSt
0b8b26a22f136a9b2a8e99d655f6fe6b0b96008cThiemo WiedemeyerupdateGraph :: GInfo -> LIB_NAME -> [DGChange] -> DGraph -> IO ()
0b8b26a22f136a9b2a8e99d655f6fe6b0b96008cThiemo WiedemeyerupdateGraph gInfo' ln changes dg = do
0b8b26a22f136a9b2a8e99d655f6fe6b0b96008cThiemo Wiedemeyer og <- readIORef $ openGraphs gInfo'
0b8b26a22f136a9b2a8e99d655f6fe6b0b96008cThiemo Wiedemeyer Nothing -> return ()
0b8b26a22f136a9b2a8e99d655f6fe6b0b96008cThiemo Wiedemeyer Just (GInfo { graphInfo = gi
370e81d7af7821f0ac6ee0643613e87a727841e7Thiemo Wiedemeyer , options = opts }) -> do
370e81d7af7821f0ac6ee0643613e87a727841e7Thiemo Wiedemeyer flags <- readIORef opts
370e81d7af7821f0ac6ee0643613e87a727841e7Thiemo Wiedemeyer let (nodes, comp) = if flagHideNodes flags then hideNodesAux dg
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer edges = if flagHideEdges flags then hideEdgesAux dg else []
aa07f9c4585a94514dcff2979d853d6e04c12fb9Thiemo Wiedemeyer GA.applyChanges gi (removeContraryChanges changes) nodes edges comp
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo Wiedemeyer-- | Toggles to display internal node names
aa07f9c4585a94514dcff2979d853d6e04c12fb9Thiemo WiedemeyerhideShowNames :: GInfo -> Bool -> IO ()
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo WiedemeyerhideShowNames (GInfo { internalNamesIORef = showInternalNames
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo Wiedemeyer }) toggle = do
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo Wiedemeyer (intrn::InternalNames) <- readIORef showInternalNames
86b2d79be961f0247a2eed10ed4f86d8d6a7639dChristian Maeder let showThem = if toggle then not $ showNames intrn else showNames intrn
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer showItrn s = if showThem then s else ""
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo Wiedemeyer mapM_ (\(s,upd) -> upd (\_ -> showItrn s)) $ updater intrn
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer writeIORef showInternalNames $ intrn {showNames = showThem}
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer-- | hides all unnamed internal nodes that are proven
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo WiedemeyerhideNodes :: GInfo
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer -> IO ([GA.NodeId], [(GA.NodeId, GA.NodeId, DGEdgeType, Bool)])
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo WiedemeyerhideNodes gInfo@(GInfo { libName = ln
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer , options = opts }) = do
76ecd8e01387d1edc9197f3464073264fa2c789aThiemo Wiedemeyer flags <- readIORef opts
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder if not $ flagHideNodes flags then return ([],[]) else do
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer ost <- readIORef $ intState gInfo
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo Wiedemeyer case i_state ost of
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer Nothing -> return ([],[])
545d0cd78159cade346b579d06052638b19b0f72Thiemo Wiedemeyer Just ist -> return $ hideNodesAux $ lookupDGraph ln $ i_libEnv ist
370e81d7af7821f0ac6ee0643613e87a727841e7Thiemo Wiedemeyer-- | hides all unnamed internal nodes that are proven
370e81d7af7821f0ac6ee0643613e87a727841e7Thiemo WiedemeyerhideNodesAux :: DGraph
370e81d7af7821f0ac6ee0643613e87a727841e7Thiemo Wiedemeyer -> ([GA.NodeId], [(GA.NodeId, GA.NodeId, DGEdgeType, Bool)])
370e81d7af7821f0ac6ee0643613e87a727841e7Thiemo WiedemeyerhideNodesAux dg =
370e81d7af7821f0ac6ee0643613e87a727841e7Thiemo Wiedemeyer let nodes = selectNodesByType dg [DGNodeType { nonRefType = NonRefType
370e81d7af7821f0ac6ee0643613e87a727841e7Thiemo Wiedemeyer { isProvenCons = True
370e81d7af7821f0ac6ee0643613e87a727841e7Thiemo Wiedemeyer , isInternalSpec = True}
370e81d7af7821f0ac6ee0643613e87a727841e7Thiemo Wiedemeyer , isLocallyEmpty = True}]
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu edges = getCompressedEdges dg nodes
a4e6fb26100f53e3b1e9f5b97c2e0a0c129294e5Christian Maeder in (nodes, edges)
370e81d7af7821f0ac6ee0643613e87a727841e7Thiemo WiedemeyertoggleHideNodes :: GInfo -> IO ()
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan PascanutoggleHideNodes gInfo@(GInfo { graphInfo = gi
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu , options = opts }) = do
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu flags <- readIORef opts
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer let hide = not $ flagHideNodes flags
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer writeIORef opts $ flags { flagHideNodes = hide }
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer GA.showTemporaryMessage gi $ if hide then "Hiding unnamed nodes..."
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer else "Revealing hidden nodes ..."
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu (nodes, comp) <- hideNodes gInfo
370e81d7af7821f0ac6ee0643613e87a727841e7Thiemo Wiedemeyer edges <- hideEdges gInfo
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer GA.applyChanges gi [] nodes edges comp
d9f20cf968e246ec283f0c09f60af4b47b174398Thiemo Wiedemeyer-- | hides all proven edges created not initialy
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo WiedemeyerhideEdges :: GInfo -> IO [EdgeId]
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo WiedemeyerhideEdges gInfo@(GInfo { libName = ln
d9f20cf968e246ec283f0c09f60af4b47b174398Thiemo Wiedemeyer , options = opts }) = do
d9f20cf968e246ec283f0c09f60af4b47b174398Thiemo Wiedemeyer flags <- readIORef opts
d9f20cf968e246ec283f0c09f60af4b47b174398Thiemo Wiedemeyer if not $ flagHideEdges flags then return [] else do
d9f20cf968e246ec283f0c09f60af4b47b174398Thiemo Wiedemeyer ost <- readIORef $ intState gInfo
d9f20cf968e246ec283f0c09f60af4b47b174398Thiemo Wiedemeyer case i_state ost of
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer Nothing -> return []
d9f20cf968e246ec283f0c09f60af4b47b174398Thiemo Wiedemeyer Just ist -> return $ hideEdgesAux $ lookupDGraph ln $ i_libEnv ist
d9f20cf968e246ec283f0c09f60af4b47b174398Thiemo WiedemeyerhideEdgesAux :: DGraph -> [EdgeId]
d9f20cf968e246ec283f0c09f60af4b47b174398Thiemo WiedemeyerhideEdgesAux dg =
d9f20cf968e246ec283f0c09f60af4b47b174398Thiemo Wiedemeyer foldl (\ e c -> case c of
370e81d7af7821f0ac6ee0643613e87a727841e7Thiemo Wiedemeyer InsertEdge (_, _, lbl) -> (dgl_id lbl):e
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer DeleteEdge (_, _, lbl) -> delete (dgl_id lbl) e
d9f20cf968e246ec283f0c09f60af4b47b174398Thiemo Wiedemeyer ) [] $ flattenHistory (SizedList.toList $ proofHistory dg) []
d9f20cf968e246ec283f0c09f60af4b47b174398Thiemo WiedemeyertoggleHideEdges :: GInfo -> IO ()
d9f20cf968e246ec283f0c09f60af4b47b174398Thiemo WiedemeyertoggleHideEdges gInfo@(GInfo { graphInfo = gi
d9f20cf968e246ec283f0c09f60af4b47b174398Thiemo Wiedemeyer , options = opts }) = do
d9f20cf968e246ec283f0c09f60af4b47b174398Thiemo Wiedemeyer flags <- readIORef opts
d9f20cf968e246ec283f0c09f60af4b47b174398Thiemo Wiedemeyer let hide = not $ flagHideEdges flags
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer writeIORef opts $ flags { flagHideEdges = hide }
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo Wiedemeyer GA.showTemporaryMessage gi $ if hide then "Hiding new proven edges..."
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer else "Revealing hidden proven edges ..."
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer (nodes, comp) <- hideNodes gInfo
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo Wiedemeyer edges <- hideEdges gInfo
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer GA.applyChanges gi [] nodes edges comp
3e3efd4ce838940032e875e6d08712a177c9c1d0Thiemo Wiedemeyer-- | generates from list of HistElem one list of DGChanges
3e3efd4ce838940032e875e6d08712a177c9c1d0Thiemo WiedemeyerflattenHistory :: [HistElem] -> [DGChange] -> [DGChange]
3e3efd4ce838940032e875e6d08712a177c9c1d0Thiemo WiedemeyerflattenHistory [] cs = cs
3e3efd4ce838940032e875e6d08712a177c9c1d0Thiemo WiedemeyerflattenHistory ((HistElem c):r) cs = flattenHistory r $ c:cs
3e3efd4ce838940032e875e6d08712a177c9c1d0Thiemo WiedemeyerflattenHistory ((HistGroup _ ph):r) cs =
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer flattenHistory r $ flattenHistory (SizedList.toList ph) cs
370e81d7af7821f0ac6ee0643613e87a727841e7Thiemo Wiedemeyer-- | selects all nodes of a type with outgoing edges
1ac36418f204bbe56f4cd951a979180721758999Christian MaederselectNodesByType :: DGraph -> [DGNodeType] -> [Node]
1ac36418f204bbe56f4cd951a979180721758999Christian MaederselectNodesByType dg types = filter (\ n -> outDG dg n /= []) $ map fst
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer $ filter (\ (_, n) -> elem (getRealDGNodeType n) types) $ labNodesDG dg
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder-- | compresses a list of types to the highest one
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo WiedemeyercompressTypes :: Bool -> [DGEdgeType] -> (DGEdgeType, Bool)
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo WiedemeyercompressTypes _ [] = error "compressTypes: wrong usage"
1ac36418f204bbe56f4cd951a979180721758999Christian MaedercompressTypes b (t:[]) = (t,b)
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo WiedemeyercompressTypes b (t1:t2:r) = if t1 == t2 then compressTypes b (t1:r) else
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer if t1 > t2 then compressTypes False (t1:r) else compressTypes False (t2:r)
370e81d7af7821f0ac6ee0643613e87a727841e7Thiemo Wiedemeyer-- | returns a list of compressed edges
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo WiedemeyergetCompressedEdges :: DGraph -> [Node] -> [(Node,Node,DGEdgeType, Bool)]
370e81d7af7821f0ac6ee0643613e87a727841e7Thiemo WiedemeyergetCompressedEdges dg hidden = filterDuplicates $ getShortPaths
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer $ concatMap (\ e@(_,t,_) -> map (e:) $ getPaths dg t hidden []) inEdges
370e81d7af7821f0ac6ee0643613e87a727841e7Thiemo Wiedemeyer inEdges = filter (\ (_,t,_) -> elem t hidden)
370e81d7af7821f0ac6ee0643613e87a727841e7Thiemo Wiedemeyer $ concatMap (outDG dg)
370e81d7af7821f0ac6ee0643613e87a727841e7Thiemo Wiedemeyer $ foldr (\ n i -> if elem n hidden
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer || elem n i then i else n:i) []
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer $ map (\ (s,_,_) -> s) $ concatMap (innDG dg) hidden
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer-- | filter duplicate paths
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo WiedemeyerfilterDuplicates :: [(Node,Node,DGEdgeType, Bool)]
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder -> [(Node,Node,DGEdgeType, Bool)]
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo WiedemeyerfilterDuplicates [] = []
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo WiedemeyerfilterDuplicates ((s, t, et, b) : r) = edge : filterDuplicates others
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer (same,others) = partition (\ (s',t', _, _) -> s == s' && t == t') r
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer b' = and $ b : map (\ (_,_,_,b'') -> b'') same
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer (et'', b''') = compressTypes b' $ et : map (\ (_,_,et',_) -> et') same
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer edge = (s,t,et'',b''')
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo Wiedemeyer-- | returns the pahts of a given node through hidden nodes
370e81d7af7821f0ac6ee0643613e87a727841e7Thiemo WiedemeyergetPaths :: DGraph -> Node -> [Node] -> [Node] -> [[LEdge DGLinkLab]]
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo WiedemeyergetPaths dg node hidden seen' = case elem node hidden of
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder True -> case edges /= [] of
370e81d7af7821f0ac6ee0643613e87a727841e7Thiemo Wiedemeyer True -> concatMap (\ e@(_,t,_) -> map (e:) $ getPaths dg t hidden seen)
370e81d7af7821f0ac6ee0643613e87a727841e7Thiemo Wiedemeyer seen = node:seen'
545d0cd78159cade346b579d06052638b19b0f72Thiemo Wiedemeyer edges = filter (\ (_,t,_) -> notElem t seen) $ outDG dg node
1a389234e68da7c3d087b038307ed8c66fc6dc32Thiemo Wiedemeyer-- | returns source and target node of a path with the compressed type
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo WiedemeyergetShortPaths :: [[LEdge DGLinkLab]]
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer -> [(Node,Node,DGEdgeType,Bool)]
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan PascanugetShortPaths [] = []
a4e6fb26100f53e3b1e9f5b97c2e0a0c129294e5Christian MaedergetShortPaths (p : r) =
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu (s, t, et, b)
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu : getShortPaths r
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer (s,_,_) = head p
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer (_,t,_) = last p
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu (et, b) = compressTypes True $ map (\ (_,_,e) -> getRealDGLinkType e) p
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu-- | Let the user select a Node to focus
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo WiedemeyerfocusNode :: GInfo -> IO ()
1a389234e68da7c3d087b038307ed8c66fc6dc32Thiemo WiedemeyerfocusNode gInfo@(GInfo { graphInfo = gi
1a389234e68da7c3d087b038307ed8c66fc6dc32Thiemo Wiedemeyer , libName = ln }) = do
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo Wiedemeyer ost <- readIORef $ intState gInfo
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo Wiedemeyer case i_state ost of
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo Wiedemeyer Nothing -> return ()
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo Wiedemeyer Just ist -> do
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo Wiedemeyer let le = i_libEnv ist
37e30366abd83c00a5d5447b45694627fd783de8Cui Jian idsnodes <- filterM (fmap not . GA.isHiddenNode gi . fst)
da955132262baab309a50fdffe228c9efe68251dCui Jian $ labNodesDG $ lookupDGraph ln le
37e30366abd83c00a5d5447b45694627fd783de8Cui Jian selection <- listBox "Select a node to focus"
37e30366abd83c00a5d5447b45694627fd783de8Cui Jian $ map (\ (n, l) -> shows n " " ++ getDGNodeName l) idsnodes
37e30366abd83c00a5d5447b45694627fd783de8Cui Jian case selection of
37e30366abd83c00a5d5447b45694627fd783de8Cui Jian Just idx -> GA.focusNode gi $ fst $ idsnodes !! idx
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo Wiedemeyer Nothing -> return ()
370e81d7af7821f0ac6ee0643613e87a727841e7Thiemo WiedemeyershowLibGraph :: GInfo -> LibFunc -> IO ()
370e81d7af7821f0ac6ee0643613e87a727841e7Thiemo WiedemeyershowLibGraph gInfo showLib = do
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer{- | it tries to perform the given action to the given graph.
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer If part of the given graph is not hidden, then the action can
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer be performed directly; otherwise the graph will be shown completely
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu firstly, and then the action will be performed, and after that the graph
a4e6fb26100f53e3b1e9f5b97c2e0a0c129294e5Christian Maeder will be hidden again.
a4e6fb26100f53e3b1e9f5b97c2e0a0c129294e5Christian MaederperformProofAction :: GInfo -> IO () -> IO ()
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan PascanuperformProofAction (GInfo { graphInfo = gi }) proofAction = do
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer GA.showTemporaryMessage gi "Applying development graph calculus proof rule..."
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer GA.showTemporaryMessage gi "Development graph calculus proof rule finished."
109b67ffce2bad83667e2f4a319d2d7f380f91afThiemo WiedemeyersaveProofStatus :: GInfo -> FilePath -> IO ()
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo WiedemeyersaveProofStatus gInfo@(GInfo { hetcatsOpts = opts
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer , libName = ln
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer }) file = encapsulateWaitTermAct $ do
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu ost <- readIORef $ intState gInfo
a4e6fb26100f53e3b1e9f5b97c2e0a0c129294e5Christian Maeder case i_state ost of
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu Nothing -> return ()
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu Just ist -> do
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer let proofStatus = i_libEnv ist
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer writeShATermFile file (ln, lookupHistory ln proofStatus)
d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer putIfVerbose opts 2 $ "Wrote " ++ file
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer-- | implementation of open menu, read in a proof status
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyeropenProofStatus :: GInfo -> FilePath -> ConvFunc -> LibFunc
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyeropenProofStatus gInfo@(GInfo { hetcatsOpts = opts
d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer , libName = ln }) file convGraph showLib = do
d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer ost <- readIORef $ intState gInfo
d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer case i_state ost of
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer Nothing -> return ()
d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer Just ist -> do
d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer mh <- readVerbose opts ln file
966a6c024c828387023fccb0cd0049f78687e5dcThiemo Wiedemeyer Nothing -> errorDialog "Error" $ "Could not read proof status from file '"
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu ++ file ++ "'"
5107ba7da675778f2fded68493512b60eff8a455Christian Maeder let libfile = libNameToFile opts ln
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu m <- anaLib opts { outtypes = [] } libfile
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu Nothing -> errorDialog "Error"
966a6c024c828387023fccb0cd0049f78687e5dcThiemo Wiedemeyer $ "Could not read original development graph from '"
0dba5bbaaef2f620f3b83a16ab6b229c3dd50c98Christian Maeder ++ libfile ++ "'"
0dba5bbaaef2f620f3b83a16ab6b229c3dd50c98Christian Maeder Just (_, libEnv) -> case Map.lookup ln libEnv of
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer Nothing -> errorDialog "Error" $ "Could not get original"
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer ++ "development graph for '" ++ showDoc ln "'"
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer lockGlobal gInfo
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer let oldEnv = i_libEnv ist
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer proofStatus = Map.insert ln
a4e6fb26100f53e3b1e9f5b97c2e0a0c129294e5Christian Maeder (applyProofHistory h dg) oldEnv
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer nwst = ost { i_state = Just ist {
28ca54b0d63d1d26a991711c8c7e85c474994715Christian Maeder i_libEnv = proofStatus } }
1e3aca4178372af672efb237d16087c603fe5564Christian Maeder writeIORef (intState gInfo) nwst
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer unlockGlobal gInfo
370e81d7af7821f0ac6ee0643613e87a727841e7Thiemo Wiedemeyer gInfo' <- copyGInfo gInfo ln
ddc662fdf0207eae2034d7b68ae5e2225c575207Thiemo Wiedemeyer convGraph gInfo' "Proof Status " showLib
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer let gi = graphInfo gInfo
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu-- | apply a rule of the development graph calculus
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan PascanuproofMenu :: GInfo
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder -> (LibEnv -> IO (Result LibEnv))
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyerproofMenu gInfo@(GInfo { hetcatsOpts = hOpts
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer , proofGUIMVar = guiMVar
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer , libName = ln
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder }) cmd proofFun = do
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer ost <- readIORef $ intState gInfo
966a6c024c828387023fccb0cd0049f78687e5dcThiemo Wiedemeyer case i_state ost of
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu Nothing -> return ()
83263d411f611d9902ef4d98c93be6ad9361c833Christian Maeder Just ist -> do
1e3aca4178372af672efb237d16087c603fe5564Christian Maeder filled <- tryPutMVar guiMVar Nothing
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer then readMVar guiMVar >>=
966a6c024c828387023fccb0cd0049f78687e5dcThiemo Wiedemeyer maybe (putIfVerbose hOpts 0 "proofMenu: ignored Nothing")
79d103748927615310322af6f7806c7cef11a802Christian Maeder putIfVerbose hOpts 4 $
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer "proofMenu: Ignored Proof command; " ++
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer "maybe a proof window is still open?"
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu lockGlobal gInfo
28ca54b0d63d1d26a991711c8c7e85c474994715Christian Maeder let proofStatus = i_libEnv ist
83263d411f611d9902ef4d98c93be6ad9361c833Christian Maeder putIfVerbose hOpts 4 "Proof started via menu"
83263d411f611d9902ef4d98c93be6ad9361c833Christian Maeder Result ds res <- proofFun proofStatus
83263d411f611d9902ef4d98c93be6ad9361c833Christian Maeder putIfVerbose hOpts 4 "Analyzing result of proof"
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu Nothing -> do
370e81d7af7821f0ac6ee0643613e87a727841e7Thiemo Wiedemeyer unlockGlobal gInfo
966a6c024c828387023fccb0cd0049f78687e5dcThiemo Wiedemeyer printDiags 2 ds
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer Just newProofStatus -> do
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer let newGr = lookupDGraph ln newProofStatus
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder history = snd $ splitHistory (lookupDGraph ln proofStatus) newGr
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer lln = map DgCommandChange $ calcGlobalHistory
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer proofStatus newProofStatus
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer nst = add2history cmd ost lln
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer nwst = nst { i_state = Just ist { i_libEnv=newProofStatus}}
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer doDump hOpts "PrintHistory" $ do
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder putStrLn "History"
4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian Maeder print $ prettyHistory history
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer writeIORef (intState gInfo) nwst
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer updateGraph gInfo ln (reverse $ flatHistory history) newGr
38122cbf09ad3dcc31a826cc4093f630515a5cfcChristian Maeder unlockGlobal gInfo
38122cbf09ad3dcc31a826cc4093f630515a5cfcChristian Maeder mGUIMVar <- tryTakeMVar guiMVar
38122cbf09ad3dcc31a826cc4093f630515a5cfcChristian Maeder maybe (fail "should be filled with Nothing after proof attempt")
38122cbf09ad3dcc31a826cc4093f630515a5cfcChristian Maeder (const $ return ())
521045d36343cd17dd217a81d4b9422ad6ab6a07Christian MaedercalcGlobalHistory :: LibEnv -> LibEnv -> [LIB_NAME]
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyercalcGlobalHistory old new = let
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder length' ln = SizedList.size . proofHistory . lookupDGraph ln
1e3aca4178372af672efb237d16087c603fe5564Christian Maeder changes = filter (\ ln -> length' ln old < length' ln new) $ Map.keys old
836aa06d367f900bee9aa762250471bcd00b5a9dChristian Maeder in concatMap (\ ln -> replicate (length' ln new - length' ln old) ln) changes
d1066b8fb69179973dcab47154858d77e72760a7Thiemo WiedemeyershowNodeInfo :: Int -> DGraph -> IO ()
66b035879accdc5f8337726173f800286a87fd78Christian MaedershowNodeInfo descr dgraph = do
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder let dgnode = labDG dgraph descr
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder title = (if isDGRef dgnode then ("reference " ++) else
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder if isInternalNode dgnode then ("internal " ++) else id)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer "node " ++ getDGNodeName dgnode ++ " " ++ show descr
83263d411f611d9902ef4d98c93be6ad9361c833Christian Maeder createTextDisplay title (title ++ "\n" ++ showDoc dgnode "")
83263d411f611d9902ef4d98c93be6ad9361c833Christian MaedershowDiagMessAux :: Int -> [Diagnosis] -> IO ()
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan PascanushowDiagMessAux v ds = let es = filterDiags v ds in
a4e6fb26100f53e3b1e9f5b97c2e0a0c129294e5Christian Maeder if null es then return () else
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu (if hasErrors es then errorDialog "Error" else infoDialog "Info") $ unlines
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu $ map show es
83263d411f611d9902ef4d98c93be6ad9361c833Christian MaedershowDiagMess :: HetcatsOpts -> [Diagnosis] -> IO ()
83263d411f611d9902ef4d98c93be6ad9361c833Christian MaedershowDiagMess = showDiagMessAux . verbose
83263d411f611d9902ef4d98c93be6ad9361c833Christian Maeder{- | outputs the theory of a node in a window;
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer used by the node menu -}
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyergetTheoryOfNode :: GInfo -> Int -> DGraph -> IO ()
83263d411f611d9902ef4d98c93be6ad9361c833Christian MaedergetTheoryOfNode gInfo descr dgraph = do
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer ost <- readIORef $ intState gInfo
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer case i_state ost of
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer Nothing -> return ()
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu Just ist -> do
a4e6fb26100f53e3b1e9f5b97c2e0a0c129294e5Christian Maeder let Result ds res = computeTheory (i_libEnv ist) (libName gInfo) descr
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu showDiagMess (hetcatsOpts gInfo) ds
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu maybe (return ())
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu (displayTheoryWithWarning "Theory" (getNameOfNode descr dgraph)
1e3aca4178372af672efb237d16087c603fe5564Christian Maeder $ addHasInHidingWarning dgraph descr) res
6c08e47c4275556c18f4f89521bf21fe94c28dd5Christian Maeder{- | translate the theory of a node in a window;
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer used by the node menu -}
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyertranslateTheoryOfNode :: GInfo -> Int -> DGraph -> IO ()
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyertranslateTheoryOfNode gInfo@(GInfo { hetcatsOpts = opts
66b035879accdc5f8337726173f800286a87fd78Christian Maeder , libName = ln }) node dgraph = do
66b035879accdc5f8337726173f800286a87fd78Christian Maeder ost <- readIORef $ intState gInfo
d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer case i_state ost of
66b035879accdc5f8337726173f800286a87fd78Christian Maeder Nothing -> return ()
66b035879accdc5f8337726173f800286a87fd78Christian Maeder Just ist -> do
66b035879accdc5f8337726173f800286a87fd78Christian Maeder let libEnv = i_libEnv ist
66b035879accdc5f8337726173f800286a87fd78Christian Maeder Result ds moTh = computeTheory libEnv ln node
66b035879accdc5f8337726173f800286a87fd78Christian Maeder Just th@(G_theory lid sign _ sens _) -> do
66b035879accdc5f8337726173f800286a87fd78Christian Maeder -- find all comorphism paths starting from lid
66b035879accdc5f8337726173f800286a87fd78Christian Maeder let paths = findComorphismPaths logicGraph (sublogicOfTh th)
66b035879accdc5f8337726173f800286a87fd78Christian Maeder -- let the user choose one
66b035879accdc5f8337726173f800286a87fd78Christian Maeder sel <- listBox "Choose a node logic translation" $ map show paths
66b035879accdc5f8337726173f800286a87fd78Christian Maeder Nothing -> errorDialog "Error" "no node logic translation chosen"
03bbcb1fefdbd8bc4e8329ca2688809d84aff0a9Christian Maeder Comorphism cid <- return (paths!!i)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer -- adjust lid's
12368e292c1abf7eaf975f20ee30ef7820ac5dd5Christian Maeder let lidS = sourceLogic cid
12368e292c1abf7eaf975f20ee30ef7820ac5dd5Christian Maeder lidT = targetLogic cid
66b035879accdc5f8337726173f800286a87fd78Christian Maeder sign' <- coerceSign lid lidS "" sign
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer sens' <- coerceThSens lid lidS "" sens
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer -- translate theory along chosen comorphism
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer let Result es mTh = wrapMapTheory cid
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer (plainSign sign', toNamedList sens')
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer Nothing -> showDiagMess opts es
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer Just (sign'', sens1) -> displayTheoryWithWarning
d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer "Translated Theory" (getNameOfNode node dgraph)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer (addHasInHidingWarning dgraph node)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer (G_theory lidT (mkExtSign sign'') startSigId
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer (toThSens sens1) startThId)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer Nothing -> showDiagMess opts ds
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer-- | Show proof status of a node
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyershowProofStatusOfNode :: GInfo -> Int -> DGraph -> IO ()
c41a1c38edbd787d8fd12b9b5f11b73a37dafe0fChristian MaedershowProofStatusOfNode _ descr dgraph = do
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer let dgnode = labDG dgraph descr
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer stat = showStatusAux dgnode
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer title = "Proof status of node "++showName (dgn_name dgnode)
c41a1c38edbd787d8fd12b9b5f11b73a37dafe0fChristian Maeder createTextDisplay title stat
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyershowStatusAux :: DGNodeLab -> String
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyershowStatusAux dgnode =
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer case dgn_theory dgnode of
c41a1c38edbd787d8fd12b9b5f11b73a37dafe0fChristian Maeder G_theory _ _ _ sens _ ->
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer let goals = OMap.filter (not . isAxiom) sens
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer (proven,open) = OMap.partition isProvenSenStatus goals
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer consGoal = "\nconservativity of this node"
1e3aca4178372af672efb237d16087c603fe5564Christian Maeder in "Proven proof goals:\n"
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder ++ showDoc proven ""
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder ++ if not $ hasOpenConsStatus True dgnode
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder then consGoal
a4e6fb26100f53e3b1e9f5b97c2e0a0c129294e5Christian Maeder ++ "\nOpen proof goals:\n"
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu ++ showDoc open ""
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu ++ if hasOpenConsStatus False dgnode
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer-- | start local theorem proving or consistency checking at a node
dda4e358a429dc24dd09d42b409d709a19eff159Christian MaederproveAtNode :: Bool -> GInfo -> Int -> DGraph -> IO ()
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan PascanuproveAtNode checkCons gInfo descr dgraph = do
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu let ln = libName gInfo
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder iSt = intState gInfo
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer ost <- readIORef iSt
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder case i_state ost of
e1c24b1dbf5cb1c9bb22b14a40167a4ba7806501Christian Maeder Nothing -> return ()
e1c24b1dbf5cb1c9bb22b14a40167a4ba7806501Christian Maeder Just ist -> do
1e3aca4178372af672efb237d16087c603fe5564Christian Maeder let le = i_libEnv ist
63324a97283728a30932828a612c7b0b0f687624Christian Maeder dgn = labDG dgraph descr
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder (dgraph', dgn', le') <- if hasLock dgn then return (dgraph, dgn, le) else do
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder lockGlobal gInfo
1e3aca4178372af672efb237d16087c603fe5564Christian Maeder (dgraph', dgn') <- initLocking (lookupDGraph ln le) (descr, dgn)
40b73e7d13a858afeac95321fcdb9ac216bfbf01Thiemo Wiedemeyer let nwle = Map.insert ln dgraph' le
1e3aca4178372af672efb237d16087c603fe5564Christian Maeder nwst = ost { i_state = Just $ ist { i_libEnv = nwle} }
16e45483b5ce48f0b92d01c817242a8c9b8bae02Christian Maeder writeIORef iSt nwst
e1c24b1dbf5cb1c9bb22b14a40167a4ba7806501Christian Maeder unlockGlobal gInfo
16e45483b5ce48f0b92d01c817242a8c9b8bae02Christian Maeder return (dgraph', dgn', nwle)
9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyer acquired <- tryLockLocal dgn'
e1c24b1dbf5cb1c9bb22b14a40167a4ba7806501Christian Maeder if acquired then do
e1c24b1dbf5cb1c9bb22b14a40167a4ba7806501Christian Maeder let action = do
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer guiMVar <- newMVar Nothing
8244e8866cad2be73b7e2b76a6659535f0f728ccChristian Maeder res <- basicInferenceNode checkCons logicGraph ln dgraph'
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder (descr, dgn') guiMVar le' iSt
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder runProveAtNode checkCons gInfo (descr, dgn') res
28ca54b0d63d1d26a991711c8c7e85c474994715Christian Maeder unlockLocal dgn'
28ca54b0d63d1d26a991711c8c7e85c474994715Christian Maeder if checkCons && labelHasHiding dgn' then do
28ca54b0d63d1d26a991711c8c7e85c474994715Christian Maeder b <- warningDialog "Warning"
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder (unwords $ hidingWarning ++ ["Try anyway?"]) $ Just action
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer unless b $ unlockLocal dgn'
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder else forkIO action >> return ()
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder else errorDialog "Error" "Proofwindow already open"
95cb954c00f873306bf1a60b62d3209d3cff4102Christian MaederrunProveAtNode :: Bool -> GInfo -> LNode DGNodeLab
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder -> Result G_theory -> IO ()
95cb954c00f873306bf1a60b62d3209d3cff4102Christian MaederrunProveAtNode checkCons gInfo (v, dgnode) (Result ds mres) =
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder let nn = getDGNodeName dgnode in
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder if checkCons then do
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder let nodetext = nn ++ " node: " ++ show v
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder Just gth -> createTextSaveDisplay ("Model for " ++ nodetext)
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder "model.log" $ showDoc gth ""
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder Nothing -> infoDialog nodetext $ unlines
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder $ "could not (re-)construct a" : "model" : map diagString ds
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder else let oldTh = dgn_theory dgnode in case mres of
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder Just newTh | newTh /= oldTh -> do
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder let Result es tres = joinG_sentences oldTh newTh
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder ln = libName gInfo
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder iSt = intState gInfo
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder showDiagMessAux 2 $ ds ++ es
28ca54b0d63d1d26a991711c8c7e85c474994715Christian Maeder Just theory -> do
28ca54b0d63d1d26a991711c8c7e85c474994715Christian Maeder lockGlobal gInfo
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder ost <- readIORef iSt
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder case i_state ost of
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder Nothing -> unlockGlobal gInfo
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder Just iist -> do
370e81d7af7821f0ac6ee0643613e87a727841e7Thiemo Wiedemeyer let le = i_libEnv iist
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder dgraph = lookupDGraph ln le
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder new_dgn = dgnode { dgn_theory = theory }
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder newDg = changeDGH dgraph $ SetNodeLab dgnode (v, new_dgn)
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder history = snd $ splitHistory dgraph newDg
966a6c024c828387023fccb0cd0049f78687e5dcThiemo Wiedemeyer nst = add2history
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian Maeder (CommentCmd $ "basic inference done on " ++ nn ++ "\n")
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian Maeder ost [DgCommandChange ln]
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian Maeder { i_state = Just iist
521045d36343cd17dd217a81d4b9422ad6ab6a07Christian Maeder { i_libEnv = Map.insert ln newDg le } }
521045d36343cd17dd217a81d4b9422ad6ab6a07Christian Maeder writeIORef iSt nwst
521045d36343cd17dd217a81d4b9422ad6ab6a07Christian Maeder updateGraph gInfo ln (reverse $ flatHistory history) newDg
521045d36343cd17dd217a81d4b9422ad6ab6a07Christian Maeder unlockGlobal gInfo
888fefaddbeb8d75a861b1d689b191b44d1853e1Thiemo Wiedemeyer Nothing -> return ()
9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyer _ -> return ()
4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian MaederedgeErr :: Int -> IO ()
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyeredgeErr descr = errorDialog "Error" $ "edge with descriptor " ++ show descr
521045d36343cd17dd217a81d4b9422ad6ab6a07Christian Maeder ++ " not found in the development graph"
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian Maeder-- | print the id, origin, type, proof-status and morphism of the edge
28ca54b0d63d1d26a991711c8c7e85c474994715Christian MaedershowEdgeInfo :: Int -> Maybe (LEdge DGLinkLab) -> IO ()
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian MaedershowEdgeInfo descr me = case me of
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian Maeder Just e@(_, _, l) -> let estr = showLEdge e in
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian Maeder createTextDisplay ("Info of " ++ estr)
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian Maeder (estr ++ "\n" ++ showDoc l "")
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian Maeder Nothing -> edgeErr descr
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian Maeder-- | check conservativity of the edge
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian MaedercheckconservativityOfEdge :: Int -> GInfo -> Maybe (LEdge DGLinkLab) -> IO ()
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian MaedercheckconservativityOfEdge descr gInfo me = case me of
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian Maeder Nothing -> edgeErr descr
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian Maeder Just lnk@(_, _, lbl) -> do
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian Maeder let iSt = intState gInfo
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian Maeder ln = libName gInfo
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian Maeder ost <- readIORef iSt
28ca54b0d63d1d26a991711c8c7e85c474994715Christian Maeder case i_state ost of
28ca54b0d63d1d26a991711c8c7e85c474994715Christian Maeder Nothing -> return ()
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian Maeder Just iist -> do
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian Maeder lockGlobal gInfo
370e81d7af7821f0ac6ee0643613e87a727841e7Thiemo Wiedemeyer (str, nwle, ph) <- checkConservativityEdge True lnk (i_libEnv iist) ln
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian Maeder if isPrefixOf "No conservativity" str
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer errorDialog "Result of conservativity check" str
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer unlockGlobal gInfo
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer createTextDisplay "Result of conservativity check" str
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu let nst = add2history (SelectCmd Link $ showDoc (dgl_id lbl) "")
a4e6fb26100f53e3b1e9f5b97c2e0a0c129294e5Christian Maeder ost [DgCommandChange ln]
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu nwst = nst { i_state = Just $ iist { i_libEnv = nwle}}
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu writeIORef iSt nwst
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer updateGraph gInfo ln (reverse $ flatHistory ph)
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu $ lookupDGraph ln nwle
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu unlockGlobal gInfo
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu-- | show library referened by a DGRef node (=node drawn as a box)
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo WiedemeyershowReferencedLibrary :: Int -> GInfo -> ConvFunc -> LibFunc -> IO ()
0dba5bbaaef2f620f3b83a16ab6b229c3dd50c98Christian MaedershowReferencedLibrary descr gInfo@(GInfo{ libName = ln })
0dba5bbaaef2f620f3b83a16ab6b229c3dd50c98Christian Maeder convGraph showLib = do
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer ost <- readIORef $ intState gInfo
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer case i_state ost of
0dba5bbaaef2f620f3b83a16ab6b229c3dd50c98Christian Maeder Nothing -> return ()
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer Just ist -> do
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer let le = i_libEnv ist
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer refNode = labDG (lookupDGraph ln le) descr
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer refLibname = if isDGRef refNode then dgn_libname refNode
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer else error "showReferencedLibrary"
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer case Map.lookup refLibname le of
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer gInfo' <- copyGInfo gInfo refLibname
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer convGraph gInfo' "development graph" showLib
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer let gi = graphInfo gInfo'
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer hideNodes gInfo'
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer GA.showTemporaryMessage gi "Development Graph initialized."
1e3aca4178372af672efb237d16087c603fe5564Christian Maeder Nothing -> error $ "The referenced library (" ++ show refLibname
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer ++ ") is unknown"
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer-- | display a window of translated graph with maximal sublogic.
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo WiedemeyertranslateGraph :: GInfo -> IO (Maybe LibEnv)
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo WiedemeyertranslateGraph gInfo@(GInfo { hetcatsOpts = opts }) = do
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer ost <- readIORef $ intState gInfo
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer case i_state ost of
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer Nothing -> return Nothing
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer Just ist -> do
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer le = i_libEnv ist
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer Result diagsSl mSublogic = getDGLogic le
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer myErrMess = showDiagMess opts
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer error' = errorDialog "Error"
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer if hasErrors diagsSl then do
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer myErrMess diagsSl
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer return Nothing
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer else case mSublogic of
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer error' "No maximal sublogic found."
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer return Nothing
1e3aca4178372af672efb237d16087c603fe5564Christian Maeder Just sublogic -> do
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer let paths = findComorphismPaths logicGraph sublogic
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer if null paths then do
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer error' "This graph has no comorphism to translation."
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer return Nothing
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer sel <- listBox "Choose a logic translation" $ map show paths
c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu Nothing -> do
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer error' "no logic translation chosen"
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer return Nothing
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer let Result diag mle = libEnv_translation le $ paths !! j
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo Wiedemeyer Just newLibEnv -> do
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer showDiagMess opts $ diagsSl ++ diag
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer return $ Just newLibEnv
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu myErrMess $ diagsSl ++ diag
a4e6fb26100f53e3b1e9f5b97c2e0a0c129294e5Christian Maeder return Nothing
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer-- DaVinciGraph to String
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer-- Functions to convert a DaVinciGraph to a String to store as a .udg file
d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer-- | saves the uDrawGraph graph to a file
d1066b8fb69179973dcab47154858d77e72760a7Thiemo WiedemeyersaveUDGraph :: GInfo -> Map.Map DGNodeType (Shape value, String)
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu -> Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String) -> IO ()
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan PascanusaveUDGraph gInfo@(GInfo { graphInfo = gi
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer , hetcatsOpts = opts
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer , libName = ln }) nodemap linkmap = do
93eeaffa1087fc6eae3f19b8ca5affb7802799fdThiemo Wiedemeyer ost <- readIORef $ intState gInfo
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer case i_state ost of
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer Nothing -> return ()
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer maybeFilePath <- fileSaveDialog ((rmSuffix $ libNameToFile opts ln)
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo Wiedemeyer [ ("uDrawGraph",["*.udg"])
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer , ("All Files", ["*"])] Nothing
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer case maybeFilePath of
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer Just filepath -> do
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu GA.showTemporaryMessage gi "Converting graph..."
a4e6fb26100f53e3b1e9f5b97c2e0a0c129294e5Christian Maeder nstring <- nodes2String gInfo nodemap linkmap
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu writeFile filepath nstring
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu GA.showTemporaryMessage gi $ "Graph stored to " ++ filepath ++ "!"
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu Nothing -> GA.showTemporaryMessage gi "Aborted!"
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu-- | Converts the nodes of the graph to String representation
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyernodes2String :: GInfo -> Map.Map DGNodeType (Shape value, String)
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu -> Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String)
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyernodes2String gInfo@(GInfo { graphInfo = gi
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer , libName = ln }) nodemap linkmap = do
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu ost <- readIORef $ intState gInfo
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer case i_state ost of
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer Nothing -> return []
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo Wiedemeyer Just ist -> do
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo Wiedemeyer let le = i_libEnv ist
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer nodes <- filterM (\(n,_) -> do b <- GA.isHiddenNode gi n
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer return $ not b)
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer $ labNodesDG $ lookupDGraph ln le
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo Wiedemeyer nstring <- foldM (\s node -> do
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer s' <- (node2String gInfo nodemap linkmap node)
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo Wiedemeyer return $ s ++ (if s /= "" then ",\n " else "") ++ s')
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer return $ "[" ++ nstring ++ "]"
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer-- | Converts a node to String representation
1ac36418f204bbe56f4cd951a979180721758999Christian Maedernode2String :: GInfo -> Map.Map DGNodeType (Shape value, String)
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer -> Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String)
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder -> LNode DGNodeLab -> IO String
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyernode2String gInfo nodemap linkmap (nid, dgnode) = do
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer label <- getNodeLabel gInfo dgnode
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer let ntype = getRealDGNodeType dgnode
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer (shape, color) <- case Map.lookup ntype nodemap of
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo Wiedemeyer Nothing -> error $ "SaveGraph: can't lookup nodetype: " ++ show ntype
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer Just (s, c) -> return (s, c)
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer object = "a(\"OBJECT\",\"" ++ label ++ "\"),"
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu color' = "a(\"COLOR\",\"" ++ color ++ "\"),"
a4e6fb26100f53e3b1e9f5b97c2e0a0c129294e5Christian Maeder shape' = "a(\"_GO\",\"" ++ map toLower (show shape) ++ "\")"
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu links <- links2String gInfo linkmap nid
a4e6fb26100f53e3b1e9f5b97c2e0a0c129294e5Christian Maeder return $ "l(\"" ++ show nid ++ "\",n(\"" ++ show ntype ++ "\","
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer ++ "[" ++ object ++ color' ++ shape' ++ "],"
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder ++ "\n [" ++ links ++ "]))"
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer-- | Converts all links of a node to String representation
1ac36418f204bbe56f4cd951a979180721758999Christian Maederlinks2String :: GInfo -> Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String)
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder -> Int -> IO String
1ac36418f204bbe56f4cd951a979180721758999Christian Maederlinks2String gInfo@(GInfo { graphInfo = gi
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer , libName = ln }) linkmap nodeid = do
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer ost <- readIORef $ intState gInfo
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer case i_state ost of
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer Nothing -> return []
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo Wiedemeyer Just ist -> do
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer let le = i_libEnv ist
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer edges <- filterM (\ (src, _, edge) -> do
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer let eid = dgl_id edge
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo Wiedemeyer return $ not b && src == nodeid)
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo Wiedemeyer $ labEdgesDG $ lookupDGraph ln le
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer foldM (\ s edge -> do
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer s' <- link2String linkmap edge
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder return $ s ++ (if s /= "" then ",\n " else "") ++ s') "" edges
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer-- | Converts a link to String representation
1ac36418f204bbe56f4cd951a979180721758999Christian Maederlink2String :: Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String)
8f5219469b89a15dc6d4c2c30463775975f5841cRazvan Pascanu -> LEdge DGLinkLab -> IO String
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyerlink2String linkmap (nodeid1, nodeid2, edge) = do
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder let (EdgeId linkid) = dgl_id edge
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer ltype = getRealDGLinkType edge
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer (line, color) <- case Map.lookup ltype linkmap of
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer Nothing -> error $ "SaveGraph: can't lookup linktype: " ++ show ltype
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer Just (l, c) -> return (l, c)
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer nm = "\"" ++ show linkid ++ ":" ++ show nodeid1 ++ "->"
79d103748927615310322af6f7806c7cef11a802Christian Maeder ++ show nodeid2 ++ "\""
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer color' = "a(\"EDGECOLOR\",\"" ++ color ++ "\"),"
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer line' = "a(\"EDGEPATTERN\",\"" ++ map toLower (show line) ++ "\")"
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer return $ "l(" ++ nm ++ ",e(\"" ++ show ltype ++ "\","
79d103748927615310322af6f7806c7cef11a802Christian Maeder ++ "[" ++ color' ++ line' ++"],"
79d103748927615310322af6f7806c7cef11a802Christian Maeder ++ "r(\"" ++ show nodeid2 ++ "\")))"