6b26240dca29e026900a83d51c75ca230a072a16Thiemo WiedemeyerDescription : Logic for manipulating the graph in the Central GUI
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyerCopyright : (c) Jorina Freya Gerken, Till Mossakowski, Uni Bremen 2002-2006
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.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 , openProofStatus
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer , saveProofStatus
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer , showReferencedLibrary
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer , getTheoryOfNode
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer , translateTheoryOfNode
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer , displaySubsortGraph
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer , displayConceptGraph
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer , showProofStatusOfNode
b0adcc203b4267d5535b430372935a5f36726db1Simon Ulbricht , ensureLockAtNode
38122cbf09ad3dcc31a826cc4093f630515a5cfcChristian Maeder , showNodeInfo
83263d411f611d9902ef4d98c93be6ad9361c833Christian Maeder , showDiagMess
abea93ed557b22ea833e1524ee5ca11afc12208aSimon Ulbricht , showDiagMessAux
521045d36343cd17dd217a81d4b9422ad6ab6a07Christian Maeder , showEdgeInfo
9a9860760c6f30558e5e60049692b6fc63904590Markus Gross , checkconservativityOfNode
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer , checkconservativityOfEdge
ea76e25262c3325f293fbdd6560f180ca18f9be4Thiemo Wiedemeyer , toggleHideNames
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer , toggleHideNodes
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer , toggleHideEdges
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo Wiedemeyer , translateGraph
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo Wiedemeyer , showLibGraph
f059d29e63508be7316ac161428eee7fc804736eChristian Maeder , calcGlobalHistory
1c039dc13801bb9c90ad6a1bac0e56af19fd2fbfMihai Codescu , add2history
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyerimport Logic.Coerce (coerceSign)
3a6decfd748f532d5cb03fbcb7a42fa37b0faab3Christian Maederimport Logic.Prover hiding (openProofStatus)
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyerimport Comorphisms.LogicGraph (logicGraph)
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyerimport Static.DGTranslation (libEnv_translation, getDGLogic)
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyerimport Proofs.InferBasic (basicInferenceNode)
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyerimport Proofs.StatusUtils (lookupHistory, removeContraryChanges)
239991d3955da0cfb760af4d506069446e1676b7Christian Maederimport GUI.Taxonomy (displayConceptGraph, displaySubsortGraph)
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyerimport qualified GUI.GraphAbstraction as GA
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyerimport Reactor.InfoBus (encapsulateWaitTermAct)
3587928ae948e8505f5af052dd4dc7cd97b6638eChristian Maederimport Common.DocUtils (showDoc, showGlobalDoc)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyerimport qualified Common.OrderedMap as OMap
4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian Maederimport qualified Common.Lib.SizedList as SizedList
a79266feb130561fa1a95ae0429d0574f625f6ceChristian Maederimport Driver.Options (HetcatsOpts, putIfVerbose, outtypes, doDump, verbose)
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyerimport Driver.WriteLibDefn (writeShATermFile)
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyerimport Driver.ReadFn (libNameToFile, readVerbose)
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyerimport Data.Char (toLower)
0d0278c34a374b29c2d6c58b39b8b56e283d48e8Christian Maederimport Data.List (partition, deleteBy, isPrefixOf)
2028dc2c091bb60343e15985948a59b955276cbfChristian Maederimport Data.Graph.Inductive.Graph (Node, LEdge, LNode)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyerimport qualified Data.Map as Map
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer-- | Locks the global lock and runs function
331603b37dec12e37e2e1df9634ef0f2c5c73ddfThiemo WiedemeyerrunAndLock :: GInfo -> IO () -> IO ()
d7aa4e1cbe00f7f3add4da911673b3b176b140c3Thiemo WiedemeyerrunAndLock (GInfo { functionLock = lock
d7aa4e1cbe00f7f3add4da911673b3b176b140c3Thiemo Wiedemeyer , graphInfo = gi
d7aa4e1cbe00f7f3add4da911673b3b176b140c3Thiemo Wiedemeyer }) function = do
331603b37dec12e37e2e1df9634ef0f2c5c73ddfThiemo Wiedemeyer locked <- tryPutMVar lock ()
32d98ca5e560cf6c1062a0463be4c350af32bed5Thiemo Wiedemeyer if locked then do
32d98ca5e560cf6c1062a0463be4c350af32bed5Thiemo Wiedemeyer "an other function is still working ... please wait ..."
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer-- | Undo one step of the History
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyerundo :: GInfo -> Bool -> IO ()
d71a37fb09bce02af6c98e7a5ab0aa5639058e4fThiemo Wiedemeyerundo gInfo isUndo = do
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu intSt <- readIORef $ intState gInfo
d7aa4e1cbe00f7f3add4da911673b3b176b140c3Thiemo Wiedemeyer nwSt <- if isUndo then undoOneStepWithUpdate intSt $ updateGraphAux gInfo
d7aa4e1cbe00f7f3add4da911673b3b176b140c3Thiemo Wiedemeyer else redoOneStepWithUpdate intSt $ updateGraphAux gInfo
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu writeIORef (intState gInfo) nwSt
d7aa4e1cbe00f7f3add4da911673b3b176b140c3Thiemo WiedemeyerupdateGraph :: GInfo -> [DGChange] -> IO ()
d7aa4e1cbe00f7f3add4da911673b3b176b140c3Thiemo WiedemeyerupdateGraph gInfo@(GInfo { libName = ln }) changes = do
d7aa4e1cbe00f7f3add4da911673b3b176b140c3Thiemo Wiedemeyer ost <- readIORef $ intState gInfo
d7aa4e1cbe00f7f3add4da911673b3b176b140c3Thiemo Wiedemeyer case i_state ost of
d7aa4e1cbe00f7f3add4da911673b3b176b140c3Thiemo Wiedemeyer Nothing -> return ()
d7aa4e1cbe00f7f3add4da911673b3b176b140c3Thiemo Wiedemeyer Just ist -> updateGraphAux gInfo ln changes $ lookupDGraph ln $ i_libEnv ist
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian MaederupdateGraphAux :: GInfo -> LibName -> [DGChange] -> DGraph -> IO ()
d7aa4e1cbe00f7f3add4da911673b3b176b140c3Thiemo WiedemeyerupdateGraphAux gInfo' ln changes dg = do
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer og <- readIORef $ openGraphs gInfo'
0b8b26a22f136a9b2a8e99d655f6fe6b0b96008cThiemo Wiedemeyer Nothing -> return ()
ea76e25262c3325f293fbdd6560f180ca18f9be4Thiemo Wiedemeyer Just gInfo@(GInfo { graphInfo = gi
ea76e25262c3325f293fbdd6560f180ca18f9be4Thiemo Wiedemeyer , options = opts }) -> do
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer flags <- readIORef opts
788bd3c33ec5aaeb90a1932c341ff837116410cfThiemo Wiedemeyer let edges = if flagHideEdges flags then hideEdgesAux dg else []
788bd3c33ec5aaeb90a1932c341ff837116410cfThiemo Wiedemeyer (nodes, comp) = if flagHideNodes flags then hideNodesAux dg edges
239991d3955da0cfb760af4d506069446e1676b7Christian Maeder else ([], [])
d7aa4e1cbe00f7f3add4da911673b3b176b140c3Thiemo Wiedemeyer "Applying development graph calculus proof rule..."
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer GA.applyChanges gi (removeContraryChanges changes) nodes edges comp
d7aa4e1cbe00f7f3add4da911673b3b176b140c3Thiemo Wiedemeyer "Updating graph..."
d7aa4e1cbe00f7f3add4da911673b3b176b140c3Thiemo Wiedemeyer hideNames gInfo
d7aa4e1cbe00f7f3add4da911673b3b176b140c3Thiemo Wiedemeyer "Development graph calculus proof rule finished."
ea76e25262c3325f293fbdd6560f180ca18f9be4Thiemo Wiedemeyer-- | Toggles to display internal node names
ea76e25262c3325f293fbdd6560f180ca18f9be4Thiemo WiedemeyerhideNames :: GInfo -> IO ()
ea76e25262c3325f293fbdd6560f180ca18f9be4Thiemo WiedemeyerhideNames (GInfo { options = opts
ea76e25262c3325f293fbdd6560f180ca18f9be4Thiemo Wiedemeyer , internalNames = updaterIORef }) = do
ea76e25262c3325f293fbdd6560f180ca18f9be4Thiemo Wiedemeyer flags <- readIORef opts
ea76e25262c3325f293fbdd6560f180ca18f9be4Thiemo Wiedemeyer updater <- readIORef updaterIORef
239991d3955da0cfb760af4d506069446e1676b7Christian Maeder mapM_ (\ (s, upd) -> upd (const $ if flagHideNames flags then "" else s))
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer-- | Toggles to display internal node names
ea76e25262c3325f293fbdd6560f180ca18f9be4Thiemo WiedemeyertoggleHideNames :: GInfo -> IO ()
ea76e25262c3325f293fbdd6560f180ca18f9be4Thiemo WiedemeyertoggleHideNames gInfo@(GInfo { graphInfo = gi
ea76e25262c3325f293fbdd6560f180ca18f9be4Thiemo Wiedemeyer , options = opts }) = do
ea76e25262c3325f293fbdd6560f180ca18f9be4Thiemo Wiedemeyer flags <- readIORef opts
ea76e25262c3325f293fbdd6560f180ca18f9be4Thiemo Wiedemeyer let hide = not $ flagHideNames flags
ea76e25262c3325f293fbdd6560f180ca18f9be4Thiemo Wiedemeyer writeIORef opts $ flags { flagHideNames = hide }
d7aa4e1cbe00f7f3add4da911673b3b176b140c3Thiemo Wiedemeyer GA.showTemporaryMessage gi $ if hide then "Hiding internal names..."
d7aa4e1cbe00f7f3add4da911673b3b176b140c3Thiemo Wiedemeyer else "Revealing internal names..."
d7aa4e1cbe00f7f3add4da911673b3b176b140c3Thiemo Wiedemeyer updateGraph gInfo []
d71a37fb09bce02af6c98e7a5ab0aa5639058e4fThiemo Wiedemeyer-- | hides all unnamed internal nodes that are proven
788bd3c33ec5aaeb90a1932c341ff837116410cfThiemo WiedemeyerhideNodesAux :: DGraph -> [EdgeId]
d71a37fb09bce02af6c98e7a5ab0aa5639058e4fThiemo Wiedemeyer -> ([GA.NodeId], [(GA.NodeId, GA.NodeId, DGEdgeType, Bool)])
788bd3c33ec5aaeb90a1932c341ff837116410cfThiemo WiedemeyerhideNodesAux dg ignoreEdges =
39a2520d13a7d43f0c0fa71b94255c3f7c500005Christian Maeder let nodes = selectNodesByType dg
39a2520d13a7d43f0c0fa71b94255c3f7c500005Christian Maeder (\ n -> isInternalSpec n && isProvenNode n && isProvenCons n)
788bd3c33ec5aaeb90a1932c341ff837116410cfThiemo Wiedemeyer edges = getCompressedEdges dg nodes ignoreEdges
d71a37fb09bce02af6c98e7a5ab0aa5639058e4fThiemo Wiedemeyer in (nodes, edges)
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo WiedemeyertoggleHideNodes :: GInfo -> IO ()
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo WiedemeyertoggleHideNodes gInfo@(GInfo { graphInfo = gi
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer , options = opts }) = do
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer flags <- readIORef opts
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer let hide = not $ flagHideNodes flags
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer writeIORef opts $ flags { flagHideNodes = hide }
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer GA.showTemporaryMessage gi $ if hide then "Hiding unnamed nodes..."
d7aa4e1cbe00f7f3add4da911673b3b176b140c3Thiemo Wiedemeyer else "Revealing hidden nodes..."
d7aa4e1cbe00f7f3add4da911673b3b176b140c3Thiemo Wiedemeyer updateGraph gInfo []
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo WiedemeyerhideEdgesAux :: DGraph -> [EdgeId]
92e96be605537638d75e9d3023ab698bd89cf889Thiemo WiedemeyerhideEdgesAux dg = map dgl_id
92e96be605537638d75e9d3023ab698bd89cf889Thiemo Wiedemeyer $ filter (\ (DGLink { dgl_type = linktype }) ->
fa1bf658051ac503f27ff1b59edb093398eed6edThiemo Wiedemeyer case linktype of
fa1bf658051ac503f27ff1b59edb093398eed6edThiemo Wiedemeyer ScopedLink _ (ThmLink s) c ->
fa1bf658051ac503f27ff1b59edb093398eed6edThiemo Wiedemeyer isProvenThmLinkStatus s && isProvenConsStatusLink c
d24317c8197e565e60c8f41309de246249c1e57eChristian Maeder HidingFreeOrCofreeThm _ _ _ s -> isProvenThmLinkStatus s
92e96be605537638d75e9d3023ab698bd89cf889Thiemo Wiedemeyer $ foldl (\ e c -> case c of
239991d3955da0cfb760af4d506069446e1676b7Christian Maeder InsertEdge (_, _, lbl) -> lbl : e
0d0278c34a374b29c2d6c58b39b8b56e283d48e8Christian Maeder DeleteEdge (_, _, lbl) -> deleteBy eqDGLinkLabById lbl e
92e96be605537638d75e9d3023ab698bd89cf889Thiemo Wiedemeyer ) [] $ flattenHistory (SizedList.toList $ proofHistory dg) []
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo WiedemeyertoggleHideEdges :: GInfo -> IO ()
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo WiedemeyertoggleHideEdges gInfo@(GInfo { graphInfo = gi
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer , options = opts }) = do
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer flags <- readIORef opts
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer let hide = not $ flagHideEdges flags
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer writeIORef opts $ flags { flagHideEdges = hide }
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer GA.showTemporaryMessage gi $ if hide then "Hiding new proven edges..."
d7aa4e1cbe00f7f3add4da911673b3b176b140c3Thiemo Wiedemeyer else "Revealing hidden proven edges..."
d7aa4e1cbe00f7f3add4da911673b3b176b140c3Thiemo Wiedemeyer updateGraph gInfo []
d9f20cf968e246ec283f0c09f60af4b47b174398Thiemo Wiedemeyer-- | generates from list of HistElem one list of DGChanges
d9f20cf968e246ec283f0c09f60af4b47b174398Thiemo WiedemeyerflattenHistory :: [HistElem] -> [DGChange] -> [DGChange]
d9f20cf968e246ec283f0c09f60af4b47b174398Thiemo WiedemeyerflattenHistory [] cs = cs
239991d3955da0cfb760af4d506069446e1676b7Christian MaederflattenHistory (HistElem c : r) cs = flattenHistory r $ c : cs
239991d3955da0cfb760af4d506069446e1676b7Christian MaederflattenHistory (HistGroup _ ph : r) cs =
d9f20cf968e246ec283f0c09f60af4b47b174398Thiemo Wiedemeyer flattenHistory r $ flattenHistory (SizedList.toList ph) cs
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer-- | selects all nodes of a type with outgoing edges
39a2520d13a7d43f0c0fa71b94255c3f7c500005Christian MaederselectNodesByType :: DGraph -> (DGNodeType -> Bool) -> [Node]
4014fb09362f3e38a91d7bb11b1484a4790e9297Thiemo WiedemeyerselectNodesByType dg types =
da1f9fa9339a0115d0559411929835bcff74e5f5Thiemo Wiedemeyer filter (\ n -> not (null $ outDG dg n) && hasUnprovenEdges dg n) $ map fst
39a2520d13a7d43f0c0fa71b94255c3f7c500005Christian Maeder $ filter (types . getRealDGNodeType . snd) $ labNodesDG dg
da1f9fa9339a0115d0559411929835bcff74e5f5Thiemo WiedemeyerhasUnprovenEdges :: DGraph -> Node -> Bool
da1f9fa9339a0115d0559411929835bcff74e5f5Thiemo WiedemeyerhasUnprovenEdges dg =
239991d3955da0cfb760af4d506069446e1676b7Christian Maeder foldl (\ b (_, _, l) -> case edgeTypeModInc $ getRealDGLinkType l of
4014fb09362f3e38a91d7bb11b1484a4790e9297Thiemo Wiedemeyer ThmType { isProvenEdge = False } -> False
da1f9fa9339a0115d0559411929835bcff74e5f5Thiemo Wiedemeyer _ -> b) True . (\ n -> innDG dg n ++ outDG dg n)
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer-- | compresses a list of types to the highest one
3e3efd4ce838940032e875e6d08712a177c9c1d0Thiemo WiedemeyercompressTypes :: Bool -> [DGEdgeType] -> (DGEdgeType, Bool)
3e3efd4ce838940032e875e6d08712a177c9c1d0Thiemo WiedemeyercompressTypes _ [] = error "compressTypes: wrong usage"
239991d3955da0cfb760af4d506069446e1676b7Christian MaedercompressTypes b (t : []) = (t, b)
239991d3955da0cfb760af4d506069446e1676b7Christian MaedercompressTypes b (t1 : t2 : r)
239991d3955da0cfb760af4d506069446e1676b7Christian Maeder | t1 == t2 = compressTypes b (t1 : r)
239991d3955da0cfb760af4d506069446e1676b7Christian Maeder | t1 > t2 = compressTypes False (t1 : r)
239991d3955da0cfb760af4d506069446e1676b7Christian Maeder | otherwise = compressTypes False (t2 : r)
788bd3c33ec5aaeb90a1932c341ff837116410cfThiemo Wiedemeyer-- | innDG with filter of not shown edges
788bd3c33ec5aaeb90a1932c341ff837116410cfThiemo WiedemeyerfInnDG :: [EdgeId] -> DGraph -> Node -> [LEdge DGLinkLab]
239991d3955da0cfb760af4d506069446e1676b7Christian MaederfInnDG ignore dg = filter (\ (_, _, l) -> notElem (dgl_id l) ignore) . innDG dg
788bd3c33ec5aaeb90a1932c341ff837116410cfThiemo Wiedemeyer-- | outDG with filter of not shown edges
788bd3c33ec5aaeb90a1932c341ff837116410cfThiemo WiedemeyerfOutDG :: [EdgeId] -> DGraph -> Node -> [LEdge DGLinkLab]
239991d3955da0cfb760af4d506069446e1676b7Christian MaederfOutDG ignore dg = filter (\ (_, _, l) -> notElem (dgl_id l) ignore) . outDG dg
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer-- | returns a list of compressed edges
788bd3c33ec5aaeb90a1932c341ff837116410cfThiemo WiedemeyergetCompressedEdges :: DGraph -> [Node] -> [EdgeId]
239991d3955da0cfb760af4d506069446e1676b7Christian Maeder -> [(Node, Node, DGEdgeType, Bool)]
788bd3c33ec5aaeb90a1932c341ff837116410cfThiemo WiedemeyergetCompressedEdges dg hidden ign = filterDuplicates $ getShortPaths
239991d3955da0cfb760af4d506069446e1676b7Christian Maeder $ concatMap (\ e@(_, t, _) -> map (e :) $ getPaths dg t hidden [] ign) inEdges
239991d3955da0cfb760af4d506069446e1676b7Christian Maeder inEdges = filter (\ (_, t, _) -> elem t hidden)
788bd3c33ec5aaeb90a1932c341ff837116410cfThiemo Wiedemeyer $ concatMap (fOutDG ign dg)
239991d3955da0cfb760af4d506069446e1676b7Christian Maeder $ foldr (\ (n, _, _) i -> if elem n hidden
239991d3955da0cfb760af4d506069446e1676b7Christian Maeder || elem n i then i else n : i) []
239991d3955da0cfb760af4d506069446e1676b7Christian Maeder $ concatMap (fInnDG ign dg) hidden
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer-- | filter duplicate paths
239991d3955da0cfb760af4d506069446e1676b7Christian MaederfilterDuplicates :: [(Node, Node, DGEdgeType, Bool)]
239991d3955da0cfb760af4d506069446e1676b7Christian Maeder -> [(Node, Node, DGEdgeType, Bool)]
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo WiedemeyerfilterDuplicates [] = []
80df5ce65c2bad7a0643106e524fe33cdcfab5b6Thiemo WiedemeyerfilterDuplicates r@((s, t, _, _) : _) = edges ++ filterDuplicates others
239991d3955da0cfb760af4d506069446e1676b7Christian Maeder (same, others) = partition (\ (s', t', _, _) -> s == s' && t == t') r
239991d3955da0cfb760af4d506069446e1676b7Christian Maeder (mtypes, stypes) = partition (\ (_, _, _, b) -> not b) same
239991d3955da0cfb760af4d506069446e1676b7Christian Maeder stypes' = foldr (\ e es -> if elem e es then es else e : es) [] stypes
239991d3955da0cfb760af4d506069446e1676b7Christian Maeder (et', _) = compressTypes False $ map (\ (_, _, et, _) -> et) mtypes
239991d3955da0cfb760af4d506069446e1676b7Christian Maeder edges = if null mtypes then stypes' else (s, t, et', False) : stypes'
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer-- | returns the pahts of a given node through hidden nodes
788bd3c33ec5aaeb90a1932c341ff837116410cfThiemo WiedemeyergetPaths :: DGraph -> Node -> [Node] -> [Node] -> [EdgeId]
788bd3c33ec5aaeb90a1932c341ff837116410cfThiemo Wiedemeyer -> [[LEdge DGLinkLab]]
788bd3c33ec5aaeb90a1932c341ff837116410cfThiemo WiedemeyergetPaths dg node hidden seen' ign = if elem node hidden then
32d98ca5e560cf6c1062a0463be4c350af32bed5Thiemo Wiedemeyer if null edges then []
239991d3955da0cfb760af4d506069446e1676b7Christian Maeder else concatMap (\ e@(_, t, _) -> map (e :) $ getPaths dg t hidden seen ign)
239991d3955da0cfb760af4d506069446e1676b7Christian Maeder seen = node : seen'
239991d3955da0cfb760af4d506069446e1676b7Christian Maeder edges = filter (\ (_, t, _) -> notElem t seen) $ fOutDG ign dg node
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer-- | returns source and target node of a path with the compressed type
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo WiedemeyergetShortPaths :: [[LEdge DGLinkLab]]
239991d3955da0cfb760af4d506069446e1676b7Christian Maeder -> [(Node, Node, DGEdgeType, Bool)]
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo WiedemeyergetShortPaths [] = []
1ac36418f204bbe56f4cd951a979180721758999Christian MaedergetShortPaths (p : r) =
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo Wiedemeyer : getShortPaths r
239991d3955da0cfb760af4d506069446e1676b7Christian Maeder (s, _, _) = head p
239991d3955da0cfb760af4d506069446e1676b7Christian Maeder (_, t, _) = last p
239991d3955da0cfb760af4d506069446e1676b7Christian Maeder (et, b) = compressTypes True $ map (\ (_, _, e) -> getRealDGLinkType e) p
1a389234e68da7c3d087b038307ed8c66fc6dc32Thiemo Wiedemeyer-- | Let the user select a Node to focus
1a389234e68da7c3d087b038307ed8c66fc6dc32Thiemo WiedemeyerfocusNode :: GInfo -> IO ()
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo WiedemeyerfocusNode gInfo@(GInfo { graphInfo = gi
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer , libName = ln }) = do
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu ost <- readIORef $ intState gInfo
a4e6fb26100f53e3b1e9f5b97c2e0a0c129294e5Christian Maeder case i_state ost of
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu Nothing -> return ()
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu Just ist -> do
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu let le = i_libEnv ist
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer idsnodes <- filterM (fmap not . GA.isHiddenNode gi . fst)
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer $ labNodesDG $ lookupDGraph ln le
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu selection <- listBox "Select a node to focus"
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu $ map (\ (n, l) -> shows n " " ++ getDGNodeName l) idsnodes
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu case selection of
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer Just idx -> GA.focusNode gi $ fst $ idsnodes !! idx
1a389234e68da7c3d087b038307ed8c66fc6dc32Thiemo Wiedemeyer Nothing -> return ()
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo WiedemeyershowLibGraph :: GInfo -> LibFunc -> IO ()
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo WiedemeyershowLibGraph gInfo showLib = do
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyersaveProofStatus :: GInfo -> FilePath -> IO ()
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo 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 ()
a4e6fb26100f53e3b1e9f5b97c2e0a0c129294e5Christian Maeder Just ist -> do
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu let proofStatus = i_libEnv ist
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer writeShATermFile file (ln, lookupHistory ln proofStatus)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer putIfVerbose opts 2 $ "Wrote " ++ file
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer-- | implementation of open menu, read in a proof status
109b67ffce2bad83667e2f4a319d2d7f380f91afThiemo WiedemeyeropenProofStatus :: GInfo -> FilePath -> ConvFunc -> LibFunc
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo WiedemeyeropenProofStatus gInfo@(GInfo { hetcatsOpts = opts
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer , libName = ln }) file convGraph showLib = do
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer ost <- readIORef $ intState gInfo
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer case i_state ost of
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer Nothing -> return ()
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer Just ist -> do
2a9702a373738717c83824512bd9389b5870fc92Christian Maeder mh <- readVerbose logicGraph opts (Just ln) file
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer Nothing -> errorDialog "Error" $
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer "Could not read proof status from file '" ++ file ++ "'"
f39c70229e74147a02d15bd45c05a0b1b325532dChristian Maeder let libfile = libNameToFile ln
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer m <- anaLib opts { outtypes = [] } libfile
d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer Nothing -> errorDialog "Error"
d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer $ "Could not read original development graph from '"
239991d3955da0cfb760af4d506069446e1676b7Christian Maeder ++ libfile ++ "'"
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer Just (_, libEnv) -> case Map.lookup ln libEnv of
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer Nothing -> errorDialog "Error" $ "Could not get original"
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer ++ "development graph for '" ++ showDoc ln "'"
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer lockGlobal gInfo
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer let oldEnv = i_libEnv ist
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer proofStatus = Map.insert ln (applyProofHistory h dg) oldEnv
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer nwst = ost { i_state = Just ist { i_libEnv = proofStatus } }
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer writeIORef (intState gInfo) nwst
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer unlockGlobal gInfo
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer gInfo' <- copyGInfo gInfo ln
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer convGraph gInfo' "Proof Status " showLib
8bdd8707c8e341f1fc57fcbf884520bfe06a5028Christian Maeder let gi = graphInfo gInfo'
a4e6fb26100f53e3b1e9f5b97c2e0a0c129294e5Christian Maeder-- | apply a rule of the development graph calculus
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyerproofMenu :: GInfo
1e3aca4178372af672efb237d16087c603fe5564Christian Maeder -> (LibEnv -> IO (Result LibEnv))
370e81d7af7821f0ac6ee0643613e87a727841e7Thiemo WiedemeyerproofMenu gInfo@(GInfo { hetcatsOpts = hOpts
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer , libName = ln
28ca54b0d63d1d26a991711c8c7e85c474994715Christian Maeder }) cmd proofFun = do
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ost <- readIORef $ intState gInfo
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer case i_state ost of
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer Nothing -> return ()
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer Just ist -> do
c5f9e2f0598f061c50c7f097add808c0ec7d1feaLoredana Mihaela Diaconu let ost2 = add2history cmd ost []
c5f9e2f0598f061c50c7f097add808c0ec7d1feaLoredana Mihaela Diaconu ost3 = add2history (CommentCmd "") ost2 []
c5f9e2f0598f061c50c7f097add808c0ec7d1feaLoredana Mihaela Diaconu writeIORef (intState gInfo) ost3
966a6c024c828387023fccb0cd0049f78687e5dcThiemo Wiedemeyer lockGlobal gInfo
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu let proofStatus = i_libEnv ist
83263d411f611d9902ef4d98c93be6ad9361c833Christian Maeder putIfVerbose hOpts 4 "Proof started via menu"
1e3aca4178372af672efb237d16087c603fe5564Christian Maeder Result ds res <- proofFun proofStatus
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer putIfVerbose hOpts 4 "Analyzing result of proof"
966a6c024c828387023fccb0cd0049f78687e5dcThiemo Wiedemeyer unlockGlobal gInfo
79d103748927615310322af6f7806c7cef11a802Christian Maeder printDiags 2 ds
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer Just newProofStatus -> do
4eefbf3ad21b510729d5423d08de513b310e9cd0Loredana Mihaela Diaconu ostate <- readIORef $ intState gInfo
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer let newGr = lookupDGraph ln newProofStatus
4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian Maeder history = snd $ splitHistory (lookupDGraph ln proofStatus) newGr
83263d411f611d9902ef4d98c93be6ad9361c833Christian Maeder lln = map DgCommandChange $ calcGlobalHistory
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu proofStatus newProofStatus
c5f9e2f0598f061c50c7f097add808c0ec7d1feaLoredana Mihaela Diaconu nst = add2history (CommentCmd "") ostate lln
239991d3955da0cfb760af4d506069446e1676b7Christian Maeder nwst = nst { i_state = Just ist { i_libEnv = newProofStatus}}
83263d411f611d9902ef4d98c93be6ad9361c833Christian Maeder doDump hOpts "PrintHistory" $ do
83263d411f611d9902ef4d98c93be6ad9361c833Christian Maeder putStrLn "History"
83263d411f611d9902ef4d98c93be6ad9361c833Christian Maeder print $ prettyHistory history
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu writeIORef (intState gInfo) nwst
d7aa4e1cbe00f7f3add4da911673b3b176b140c3Thiemo Wiedemeyer updateGraph gInfo (reverse $ flatHistory history)
966a6c024c828387023fccb0cd0049f78687e5dcThiemo Wiedemeyer unlockGlobal gInfo
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian MaedercalcGlobalHistory :: LibEnv -> LibEnv -> [LibName]
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo WiedemeyercalcGlobalHistory old new = let
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder length' ln = SizedList.size . proofHistory . lookupDGraph ln
4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian Maeder changes = filter (\ ln -> length' ln old < length' ln new) $ Map.keys old
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer in concatMap (\ ln -> replicate (length' ln new - length' ln old) ln) changes
38122cbf09ad3dcc31a826cc4093f630515a5cfcChristian MaedershowNodeInfo :: Int -> DGraph -> IO ()
38122cbf09ad3dcc31a826cc4093f630515a5cfcChristian MaedershowNodeInfo descr dgraph = do
38122cbf09ad3dcc31a826cc4093f630515a5cfcChristian Maeder let dgnode = labDG dgraph descr
38122cbf09ad3dcc31a826cc4093f630515a5cfcChristian Maeder title = (if isDGRef dgnode then ("reference " ++) else
38122cbf09ad3dcc31a826cc4093f630515a5cfcChristian Maeder if isInternalNode dgnode then ("internal " ++) else id)
521045d36343cd17dd217a81d4b9422ad6ab6a07Christian Maeder "node " ++ getDGNodeName dgnode ++ " " ++ show descr
3587928ae948e8505f5af052dd4dc7cd97b6638eChristian Maeder createTextDisplay title $ title ++ "\n"
3587928ae948e8505f5af052dd4dc7cd97b6638eChristian Maeder ++ showGlobalDoc (globalAnnos dgraph) dgnode ""
1ac36418f204bbe56f4cd951a979180721758999Christian MaedershowDiagMessAux :: Int -> [Diagnosis] -> IO ()
1e3aca4178372af672efb237d16087c603fe5564Christian MaedershowDiagMessAux v ds = let es = filterDiags v ds in
32d98ca5e560cf6c1062a0463be4c350af32bed5Thiemo Wiedemeyer unless (null es) $ (if hasErrors es then errorDialog "Error"
32d98ca5e560cf6c1062a0463be4c350af32bed5Thiemo Wiedemeyer else infoDialog "Info") $ unlines $ map show es
1ac36418f204bbe56f4cd951a979180721758999Christian MaedershowDiagMess :: HetcatsOpts -> [Diagnosis] -> IO ()
1ac36418f204bbe56f4cd951a979180721758999Christian MaedershowDiagMess = showDiagMessAux . verbose
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer{- | outputs the theory of a node in a window;
83263d411f611d9902ef4d98c93be6ad9361c833Christian Maeder used by the node menu -}
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo WiedemeyergetTheoryOfNode :: GInfo -> Int -> DGraph -> IO ()
83263d411f611d9902ef4d98c93be6ad9361c833Christian MaedergetTheoryOfNode gInfo descr dgraph = do
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer ost <- readIORef $ intState gInfo
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer case i_state ost of
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer Nothing -> return ()
1937dccb04b363364f7a7de17fdaae1d70583af9Christian Maeder Just ist -> case computeTheory (i_libEnv ist) (libName gInfo) descr of
1937dccb04b363364f7a7de17fdaae1d70583af9Christian Maeder errorDialog "Error" $ "no global theory for node " ++ show descr
cc31ad5864570db2fc7b2cb3e04810c8727d145aChristian Maeder Just th -> displayTheoryOfNode (getNameOfNode descr dgraph)
cc31ad5864570db2fc7b2cb3e04810c8727d145aChristian Maeder (addHasInHidingWarning dgraph descr
cc31ad5864570db2fc7b2cb3e04810c8727d145aChristian Maeder ++ showGlobalDoc (globalAnnos dgraph) th "\n")
cc31ad5864570db2fc7b2cb3e04810c8727d145aChristian Maeder-- | displays a theory with warning in a window
cc31ad5864570db2fc7b2cb3e04810c8727d145aChristian MaederdisplayTheoryOfNode :: String -- ^ Name of theory
cc31ad5864570db2fc7b2cb3e04810c8727d145aChristian Maeder -> String -- ^ Body text
cc31ad5864570db2fc7b2cb3e04810c8727d145aChristian MaederdisplayTheoryOfNode n = createTextSaveDisplay ("Theory of " ++ n) (n ++ ".het")
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer{- | translate the theory of a node in a window;
83263d411f611d9902ef4d98c93be6ad9361c833Christian Maeder used by the node menu -}
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo WiedemeyertranslateTheoryOfNode :: GInfo -> Int -> DGraph -> IO ()
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo WiedemeyertranslateTheoryOfNode gInfo@(GInfo { hetcatsOpts = opts
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer , libName = ln }) node dgraph = do
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer ost <- readIORef $ intState gInfo
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer case i_state ost of
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer Nothing -> return ()
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer Just ist -> do
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer let libEnv = i_libEnv ist
1937dccb04b363364f7a7de17fdaae1d70583af9Christian Maeder case computeTheory libEnv ln node of
c1d06b3018b34ede2b3fb6c7fe2ad28cd5ce5b68Christian Maeder Just th@(G_theory lid _ sign _ sens _) -> do
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer -- find all comorphism paths starting from lid
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer let paths = findComorphismPaths logicGraph (sublogicOfTh th)
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer -- let the user choose one
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer sel <- listBox "Choose a node logic translation" $ map show paths
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer Nothing -> errorDialog "Error" "no node logic translation chosen"
239991d3955da0cfb760af4d506069446e1676b7Christian Maeder Comorphism cid <- return (paths !! i)
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer -- adjust lid's
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer let lidS = sourceLogic cid
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer lidT = targetLogic cid
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer sign' <- coerceSign lid lidS "" sign
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer sens' <- coerceThSens lid lidS "" sens
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer -- translate theory along chosen comorphism
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer let Result es mTh = wrapMapTheory cid
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer (plainSign sign', toNamedList sens')
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer Nothing -> showDiagMess opts es
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer Just (sign'', sens1) -> displayTheoryWithWarning
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer "Translated Theory" (getNameOfNode node dgraph)
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer (addHasInHidingWarning dgraph node)
c1d06b3018b34ede2b3fb6c7fe2ad28cd5ce5b68Christian Maeder $ G_theory lidT Nothing (mkExtSign sign'') startSigId
c1d06b3018b34ede2b3fb6c7fe2ad28cd5ce5b68Christian Maeder (toThSens sens1) startThId
1937dccb04b363364f7a7de17fdaae1d70583af9Christian Maeder errorDialog "Error" $ "no global theory for node " ++ show node
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer-- | Show proof status of a node
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo WiedemeyershowProofStatusOfNode :: GInfo -> Int -> DGraph -> IO ()
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo WiedemeyershowProofStatusOfNode _ descr dgraph =
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer let dgnode = labDG dgraph descr
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer stat = showStatusAux dgnode
a2af8492313011f78cbedbfd302dc12150b9f7efChristian Maeder title = "Proof status of node " ++ getDGNodeName dgnode
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer in createTextDisplay title stat
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyershowStatusAux :: DGNodeLab -> String
a7e5c17a679fa2dae5998cd04c7e9e06c05c8164Christian MaedershowStatusAux dgnode = case simplifyTh $ dgn_theory dgnode of
c1d06b3018b34ede2b3fb6c7fe2ad28cd5ce5b68Christian Maeder G_theory _ _ _ _ sens _ ->
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer let goals = OMap.filter (not . isAxiom) sens
239991d3955da0cfb760af4d506069446e1676b7Christian Maeder (proven, open) = OMap.partition isProvenSenStatus goals
c41a1c38edbd787d8fd12b9b5f11b73a37dafe0fChristian Maeder consGoal = "\nconservativity of this node"
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer in "Proven proof goals:\n"
a7e5c17a679fa2dae5998cd04c7e9e06c05c8164Christian Maeder ++ showDoc (OMap.map sentence proven) ""
260bfc3b7dc8ed037b7d98ee044302415db6fcd7Christian Maeder ++ if not $ hasOpenNodeConsStatus True dgnode
c41a1c38edbd787d8fd12b9b5f11b73a37dafe0fChristian Maeder then consGoal
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer ++ "\nOpen proof goals:\n"
a7e5c17a679fa2dae5998cd04c7e9e06c05c8164Christian Maeder ++ showDoc (OMap.map sentence open) ""
260bfc3b7dc8ed037b7d98ee044302415db6fcd7Christian Maeder ++ if hasOpenNodeConsStatus False dgnode
c41a1c38edbd787d8fd12b9b5f11b73a37dafe0fChristian Maeder then consGoal
92d79cd0ad22cf74b345e1381d806ffc364d9ea1Thiemo WiedemeyerhidingWarnDiag :: DGNodeLab -> IO Bool
dbd5da92be2bc4a8afcaa21980a5f59831037171Thiemo WiedemeyerhidingWarnDiag dgn = if labelHasHiding dgn then
dbd5da92be2bc4a8afcaa21980a5f59831037171Thiemo Wiedemeyer warningDialog "Warning" $ unwords $ hidingWarning ++ ["Try anyway?"]
92d79cd0ad22cf74b345e1381d806ffc364d9ea1Thiemo Wiedemeyer else return True
9cfd9e8213e51ea282e68509183fb023aba59491Simon UlbrichtensureLockAtNode :: GInfo -> Int -> DGraph
9cfd9e8213e51ea282e68509183fb023aba59491Simon Ulbricht -> IO (Maybe (DGraph, DGNodeLab, LibEnv))
9cfd9e8213e51ea282e68509183fb023aba59491Simon UlbrichtensureLockAtNode gi descr dg = do
9cfd9e8213e51ea282e68509183fb023aba59491Simon Ulbricht let ln = libName gi
9cfd9e8213e51ea282e68509183fb023aba59491Simon Ulbricht iSt = intState gi
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer ost <- readIORef iSt
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer case i_state ost of
9cfd9e8213e51ea282e68509183fb023aba59491Simon Ulbricht Nothing -> return Nothing
3587928ae948e8505f5af052dd4dc7cd97b6638eChristian Maeder Just ist -> let
9cfd9e8213e51ea282e68509183fb023aba59491Simon Ulbricht le = i_libEnv ist
3587928ae948e8505f5af052dd4dc7cd97b6638eChristian Maeder dgn = labDG dg descr in if hasLock dgn
cc31ad5864570db2fc7b2cb3e04810c8727d145aChristian Maeder then return $ Just (dg, dgn, le)
9cfd9e8213e51ea282e68509183fb023aba59491Simon Ulbricht lockGlobal gi
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer (dgraph', dgn') <- initLocking (lookupDGraph ln le) (descr, dgn)
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer let nwle = Map.insert ln dgraph' le
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer nwst = ost { i_state = Just $ ist { i_libEnv = nwle} }
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer writeIORef iSt nwst
9cfd9e8213e51ea282e68509183fb023aba59491Simon Ulbricht unlockGlobal gi
9cfd9e8213e51ea282e68509183fb023aba59491Simon Ulbricht return $ Just (dgraph', dgn', nwle)
9cfd9e8213e51ea282e68509183fb023aba59491Simon Ulbricht-- | start local theorem proving or consistency checking at a node
9cfd9e8213e51ea282e68509183fb023aba59491Simon UlbrichtproveAtNode :: GInfo -> Int -> DGraph -> IO ()
9cfd9e8213e51ea282e68509183fb023aba59491Simon UlbrichtproveAtNode gInfo descr dgraph = do
9cfd9e8213e51ea282e68509183fb023aba59491Simon Ulbricht let ln = libName gInfo
9cfd9e8213e51ea282e68509183fb023aba59491Simon Ulbricht iSt = intState gInfo
9cfd9e8213e51ea282e68509183fb023aba59491Simon Ulbricht lockedEnv <- ensureLockAtNode gInfo descr dgraph
9cfd9e8213e51ea282e68509183fb023aba59491Simon Ulbricht case lockedEnv of
9cfd9e8213e51ea282e68509183fb023aba59491Simon Ulbricht Nothing -> return ()
9cfd9e8213e51ea282e68509183fb023aba59491Simon Ulbricht Just (dgraph', dgn', le') -> do
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer acquired <- tryLockLocal dgn'
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer if acquired then do
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer let action = do
0cdeccb66730b876f73bddd2705ddc62e180320dThiemo Wiedemeyer res@(Result d _) <- basicInferenceNode logicGraph ln dgraph'
0cdeccb66730b876f73bddd2705ddc62e180320dThiemo Wiedemeyer (descr, dgn') le' iSt
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer when (null d || diagString (head d) /= "Proofs.Proofs: selection")
0cdeccb66730b876f73bddd2705ddc62e180320dThiemo Wiedemeyer $ runProveAtNode gInfo (descr, dgn') res
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer b <- hidingWarnDiag dgn'
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer unlockLocal dgn'
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer else errorDialog "Error" "Proofwindow already open"
0cdeccb66730b876f73bddd2705ddc62e180320dThiemo WiedemeyerrunProveAtNode :: GInfo -> LNode DGNodeLab
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder -> Result G_theory -> IO ()
0cdeccb66730b876f73bddd2705ddc62e180320dThiemo WiedemeyerrunProveAtNode gInfo (v, dgnode) (Result ds mres) = case mres of
0cdeccb66730b876f73bddd2705ddc62e180320dThiemo Wiedemeyer let oldTh = dgn_theory dgnode
0cdeccb66730b876f73bddd2705ddc62e180320dThiemo Wiedemeyer rTh = propagateProofs oldTh newTh in
0cdeccb66730b876f73bddd2705ddc62e180320dThiemo Wiedemeyer unless (rTh == oldTh) $ do
0cdeccb66730b876f73bddd2705ddc62e180320dThiemo Wiedemeyer showDiagMessAux 2 ds
56f49c2883b1da5b18c57ca94457b2c4757a28d3Markus Gross lockGlobal gInfo
56f49c2883b1da5b18c57ca94457b2c4757a28d3Markus Gross let ln = libName gInfo
56f49c2883b1da5b18c57ca94457b2c4757a28d3Markus Gross iSt = intState gInfo
56f49c2883b1da5b18c57ca94457b2c4757a28d3Markus Gross ost <- readIORef iSt
039763ad866bb92d1818e09d1e5a0491af5af3d9Christian Maeder let (ost', hist) = updateNodeProof ln ost (v, dgnode) rTh
039763ad866bb92d1818e09d1e5a0491af5af3d9Christian Maeder case i_state ost' of
039763ad866bb92d1818e09d1e5a0491af5af3d9Christian Maeder Nothing -> return ()
cc8cec541a2ff37538daa477997ec8040ab257acChristian Maeder writeIORef iSt ost'
cc8cec541a2ff37538daa477997ec8040ab257acChristian Maeder runAndLock gInfo $ updateGraph gInfo hist
56f49c2883b1da5b18c57ca94457b2c4757a28d3Markus Gross unlockGlobal gInfo
0cdeccb66730b876f73bddd2705ddc62e180320dThiemo Wiedemeyer _ -> return ()
239991d3955da0cfb760af4d506069446e1676b7Christian MaedercheckconservativityOfNode :: GInfo -> Int -> DGraph -> IO ()
239991d3955da0cfb760af4d506069446e1676b7Christian MaedercheckconservativityOfNode gInfo descr dgraph = do
9a9860760c6f30558e5e60049692b6fc63904590Markus Gross let iSt = intState gInfo
9a9860760c6f30558e5e60049692b6fc63904590Markus Gross ln = libName gInfo
eb600800c6f539148144444c14bf6354b6eaf0ceChristian Maeder nlbl = labDG dgraph descr
9a9860760c6f30558e5e60049692b6fc63904590Markus Gross ost <- readIORef iSt
9a9860760c6f30558e5e60049692b6fc63904590Markus Gross case i_state ost of
9a9860760c6f30558e5e60049692b6fc63904590Markus Gross Nothing -> return ()
92d79cd0ad22cf74b345e1381d806ffc364d9ea1Thiemo Wiedemeyer Just iist -> do
92d79cd0ad22cf74b345e1381d806ffc364d9ea1Thiemo Wiedemeyer b <- hidingWarnDiag nlbl
92d79cd0ad22cf74b345e1381d806ffc364d9ea1Thiemo Wiedemeyer lockGlobal gInfo
92d79cd0ad22cf74b345e1381d806ffc364d9ea1Thiemo Wiedemeyer (str, libEnv', ph) <- checkConservativityNode True (descr, nlbl)
92d79cd0ad22cf74b345e1381d806ffc364d9ea1Thiemo Wiedemeyer (i_libEnv iist) ln
92d79cd0ad22cf74b345e1381d806ffc364d9ea1Thiemo Wiedemeyer if isPrefixOf "No conservativity" str then
9a9860760c6f30558e5e60049692b6fc63904590Markus Gross errorDialog "Result of conservativity check" str
92d79cd0ad22cf74b345e1381d806ffc364d9ea1Thiemo Wiedemeyer createTextDisplay "Result of conservativity check" str
92d79cd0ad22cf74b345e1381d806ffc364d9ea1Thiemo Wiedemeyer let nst = add2history (SelectCmd Node $ showDoc descr "")
92d79cd0ad22cf74b345e1381d806ffc364d9ea1Thiemo Wiedemeyer ost [DgCommandChange ln]
92d79cd0ad22cf74b345e1381d806ffc364d9ea1Thiemo Wiedemeyer nwst = nst { i_state = Just $ iist { i_libEnv = libEnv' }}
92d79cd0ad22cf74b345e1381d806ffc364d9ea1Thiemo Wiedemeyer writeIORef iSt nwst
92d79cd0ad22cf74b345e1381d806ffc364d9ea1Thiemo Wiedemeyer runAndLock gInfo $ updateGraph gInfo (reverse $ flatHistory ph)
eb600800c6f539148144444c14bf6354b6eaf0ceChristian Maeder unlockGlobal gInfo
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian MaederedgeErr :: Int -> IO ()
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian MaederedgeErr descr = errorDialog "Error" $ "edge with descriptor " ++ show descr
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian Maeder ++ " not found in the development graph"
521045d36343cd17dd217a81d4b9422ad6ab6a07Christian Maeder-- | print the id, origin, type, proof-status and morphism of the edge
521045d36343cd17dd217a81d4b9422ad6ab6a07Christian MaedershowEdgeInfo :: Int -> Maybe (LEdge DGLinkLab) -> IO ()
521045d36343cd17dd217a81d4b9422ad6ab6a07Christian MaedershowEdgeInfo descr me = case me of
521045d36343cd17dd217a81d4b9422ad6ab6a07Christian Maeder Just e@(_, _, l) -> let estr = showLEdge e in
888fefaddbeb8d75a861b1d689b191b44d1853e1Thiemo Wiedemeyer createTextDisplay ("Info of " ++ estr)
9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyer (estr ++ "\n" ++ showDoc l "")
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian Maeder Nothing -> edgeErr descr
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer-- | check conservativity of the edge
521045d36343cd17dd217a81d4b9422ad6ab6a07Christian MaedercheckconservativityOfEdge :: Int -> GInfo -> Maybe (LEdge DGLinkLab) -> IO ()
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian MaedercheckconservativityOfEdge descr gInfo me = case me of
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian Maeder Nothing -> edgeErr descr
28ca54b0d63d1d26a991711c8c7e85c474994715Christian Maeder Just lnk@(_, _, lbl) -> do
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian Maeder let iSt = intState gInfo
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian Maeder ln = libName gInfo
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian Maeder ost <- readIORef iSt
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian Maeder case i_state ost of
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian Maeder Nothing -> return ()
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian Maeder Just iist -> do
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian Maeder lockGlobal gInfo
611c5a1783d95809487402fc94cb466aa4c7f300Markus Gross (str, nwle, _, ph) <- checkConservativityEdge True lnk
611c5a1783d95809487402fc94cb466aa4c7f300Markus Gross (i_libEnv iist) ln
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian Maeder if isPrefixOf "No conservativity" str
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian Maeder errorDialog "Result of conservativity check" str
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian Maeder createTextDisplay "Result of conservativity check" str
28ca54b0d63d1d26a991711c8c7e85c474994715Christian Maeder let nst = add2history (SelectCmd Link $ showDoc (dgl_id lbl) "")
28ca54b0d63d1d26a991711c8c7e85c474994715Christian Maeder ost [DgCommandChange ln]
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian Maeder nwst = nst { i_state = Just $ iist { i_libEnv = nwle}}
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian Maeder writeIORef iSt nwst
d7aa4e1cbe00f7f3add4da911673b3b176b140c3Thiemo Wiedemeyer runAndLock gInfo $ updateGraph gInfo $ reverse $ flatHistory ph
eb600800c6f539148144444c14bf6354b6eaf0ceChristian Maeder unlockGlobal gInfo
8bdd8707c8e341f1fc57fcbf884520bfe06a5028Christian Maeder-- | show development graph for library
8bdd8707c8e341f1fc57fcbf884520bfe06a5028Christian MaedershowDGraph :: GInfo -> LibName -> ConvFunc -> LibFunc -> IO ()
8bdd8707c8e341f1fc57fcbf884520bfe06a5028Christian MaedershowDGraph gi ln convGraph showLib = do
8bdd8707c8e341f1fc57fcbf884520bfe06a5028Christian Maeder putIfVerbose (hetcatsOpts gi) 3 $ "Converting graph for " ++ show ln
8bdd8707c8e341f1fc57fcbf884520bfe06a5028Christian Maeder og <- readIORef $ openGraphs gi
8bdd8707c8e341f1fc57fcbf884520bfe06a5028Christian Maeder Nothing -> do
8bdd8707c8e341f1fc57fcbf884520bfe06a5028Christian Maeder updateWindowCount gi succ
8bdd8707c8e341f1fc57fcbf884520bfe06a5028Christian Maeder gi' <- copyGInfo gi ln
44dede2d8d8903c83b2cda83288718953836b5f3Christian Maeder convGraph gi' "Hets Development Graph" showLib
8bdd8707c8e341f1fc57fcbf884520bfe06a5028Christian Maeder GA.showTemporaryMessage (graphInfo gi') "Development Graph initialized."
8bdd8707c8e341f1fc57fcbf884520bfe06a5028Christian Maeder GA.showTemporaryMessage (graphInfo gi') "Development Graph requested."
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer-- | show library referened by a DGRef node (=node drawn as a box)
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo WiedemeyershowReferencedLibrary :: Int -> GInfo -> ConvFunc -> LibFunc -> IO ()
8bdd8707c8e341f1fc57fcbf884520bfe06a5028Christian MaedershowReferencedLibrary descr gInfo convGraph showLib = do
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu ost <- readIORef $ intState gInfo
a4e6fb26100f53e3b1e9f5b97c2e0a0c129294e5Christian Maeder case i_state ost of
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu Nothing -> return ()
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu Just ist -> do
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer let le = i_libEnv ist
8bdd8707c8e341f1fc57fcbf884520bfe06a5028Christian Maeder ln = libName gInfo
239991d3955da0cfb760af4d506069446e1676b7Christian Maeder refNode = labDG (lookupDGraph ln le) descr
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu refLibname = if isDGRef refNode then dgn_libname refNode
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu else error "showReferencedLibrary"
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu case Map.lookup refLibname le of
8bdd8707c8e341f1fc57fcbf884520bfe06a5028Christian Maeder Just _ -> showDGraph gInfo refLibname convGraph showLib
f059d29e63508be7316ac161428eee7fc804736eChristian Maeder Nothing -> errorDialog "Error"
f059d29e63508be7316ac161428eee7fc804736eChristian Maeder $ "The referenced library (" ++ show refLibname ++ ") is unknown"
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo 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
1e3aca4178372af672efb237d16087c603fe5564Christian Maeder 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
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer 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
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer error' "no logic translation chosen"
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer return Nothing
1e3aca4178372af672efb237d16087c603fe5564Christian Maeder let Result diag mle = libEnv_translation le $ paths !! j
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer Just newLibEnv -> do
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer showDiagMess opts $ diagsSl ++ diag
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer return $ Just newLibEnv
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer myErrMess $ diagsSl ++ diag
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer return Nothing
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer-- | saves the uDrawGraph graph to a file
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo WiedemeyersaveUDGraph :: GInfo -> Map.Map DGNodeType (Shape value, String)
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo Wiedemeyer -> Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String) -> IO ()
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo WiedemeyersaveUDGraph gInfo@(GInfo { graphInfo = gi
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer , libName = ln }) nodemap linkmap = do
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu ost <- readIORef $ intState gInfo
a4e6fb26100f53e3b1e9f5b97c2e0a0c129294e5Christian Maeder case i_state ost of
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu Nothing -> return ()
a79266feb130561fa1a95ae0429d0574f625f6ceChristian Maeder maybeFilePath <- fileSaveDialog (libNameToFile ln ++ ".udg")
239991d3955da0cfb760af4d506069446e1676b7Christian Maeder [ ("uDrawGraph", ["*.udg"])
32d98ca5e560cf6c1062a0463be4c350af32bed5Thiemo Wiedemeyer , ("All Files", ["*"])] Nothing
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu case maybeFilePath of
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu Just filepath -> do
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer GA.showTemporaryMessage gi "Converting graph..."
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer nstring <- nodes2String gInfo nodemap linkmap
93eeaffa1087fc6eae3f19b8ca5affb7802799fdThiemo Wiedemeyer writeFile filepath nstring
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer GA.showTemporaryMessage gi $ "Graph stored to " ++ filepath ++ "!"
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer Nothing -> GA.showTemporaryMessage gi "Aborted!"
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer-- | Converts the nodes of the graph to String representation
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo Wiedemeyernodes2String :: GInfo -> Map.Map DGNodeType (Shape value, String)
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo Wiedemeyer -> Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String)
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyernodes2String gInfo@(GInfo { graphInfo = gi
239991d3955da0cfb760af4d506069446e1676b7Christian Maeder , libName = ln }) nodemap linkmap = do
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu ost <- readIORef $ intState gInfo
a4e6fb26100f53e3b1e9f5b97c2e0a0c129294e5Christian Maeder case i_state ost of
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu Nothing -> return []
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu Just ist -> do
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu let le = i_libEnv ist
239991d3955da0cfb760af4d506069446e1676b7Christian Maeder nodes <- filterM (fmap not . GA.isHiddenNode gi . fst)
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer $ labNodesDG $ lookupDGraph ln le
239991d3955da0cfb760af4d506069446e1676b7Christian Maeder nstring <- foldM (\ s ->
239991d3955da0cfb760af4d506069446e1676b7Christian Maeder fmap ((if null s then s else s ++ ",\n") ++)
239991d3955da0cfb760af4d506069446e1676b7Christian Maeder . node2String gInfo nodemap linkmap)
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu return $ "[" ++ nstring ++ "]"
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer-- | Converts a node to String representation
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo Wiedemeyernode2String :: GInfo -> Map.Map DGNodeType (Shape value, String)
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo Wiedemeyer -> Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String)
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer -> LNode DGNodeLab -> IO String
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyernode2String gInfo nodemap linkmap (nid, dgnode) = do
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer label <- getNodeLabel gInfo dgnode
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo 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)
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer object = "a(\"OBJECT\",\"" ++ label ++ "\"),"
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer color' = "a(\"COLOR\",\"" ++ color ++ "\"),"
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder shape' = "a(\"_GO\",\"" ++ map toLower (show shape) ++ "\")"
239991d3955da0cfb760af4d506069446e1676b7Christian Maeder links <- links2String gInfo linkmap nid
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder return $ "l(\"" ++ show nid ++ "\",n(\"" ++ show ntype ++ "\","
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer ++ "[" ++ object ++ color' ++ shape' ++ "],"
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer ++ "\n [" ++ links ++ "]))"
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer-- | Converts all links of a node to String representation
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo Wiedemeyerlinks2String :: GInfo -> Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String)
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer -> Int -> IO String
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyerlinks2String gInfo@(GInfo { graphInfo = gi
239991d3955da0cfb760af4d506069446e1676b7Christian Maeder , libName = ln }) linkmap nodeid = do
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu ost <- readIORef $ intState gInfo
a4e6fb26100f53e3b1e9f5b97c2e0a0c129294e5Christian Maeder case i_state ost of
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu Nothing -> return []
a4e6fb26100f53e3b1e9f5b97c2e0a0c129294e5Christian Maeder Just ist -> do
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer let le = i_libEnv ist
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder edges <- filterM (\ (src, _, edge) -> do
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder let eid = dgl_id edge
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder return $ not b && src == nodeid)
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder $ labEdgesDG $ lookupDGraph ln le
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder foldM (\ s edge -> do
32d98ca5e560cf6c1062a0463be4c350af32bed5Thiemo Wiedemeyer s' <- link2String linkmap edge
32d98ca5e560cf6c1062a0463be4c350af32bed5Thiemo Wiedemeyer return $ (if null s then "" else s ++ ",\n") ++ s') "" edges
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer-- | Converts a link to String representation
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo Wiedemeyerlink2String :: Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String)
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer -> LEdge DGLinkLab -> IO String
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyerlink2String linkmap (nodeid1, nodeid2, edge) = do
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer let (EdgeId linkid) = dgl_id edge
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo Wiedemeyer ltype = getRealDGLinkType edge
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo Wiedemeyer (line, color) <- case Map.lookup ltype linkmap of
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo Wiedemeyer Nothing -> error $ "SaveGraph: can't lookup linktype: " ++ show ltype
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer Just (l, c) -> return (l, c)
239991d3955da0cfb760af4d506069446e1676b7Christian Maeder nm = "\"" ++ show linkid ++ ":" ++ show nodeid1 ++ "->"
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder ++ show nodeid2 ++ "\""
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer color' = "a(\"EDGECOLOR\",\"" ++ color ++ "\"),"
239991d3955da0cfb760af4d506069446e1676b7Christian Maeder line' = "a(\"EDGEPATTERN\",\"" ++ map toLower (show line) ++ "\")"
8f5219469b89a15dc6d4c2c30463775975f5841cRazvan Pascanu return $ "l(" ++ nm ++ ",e(\"" ++ show ltype ++ "\","
239991d3955da0cfb760af4d506069446e1676b7Christian Maeder ++ "[" ++ color' ++ line' ++ "],"
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder ++ "r(\"" ++ show nodeid2 ++ "\")))"
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer-- | Returns the name of the Node
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo WiedemeyergetNodeLabel :: GInfo -> DGNodeLab -> IO String
ea76e25262c3325f293fbdd6560f180ca18f9be4Thiemo WiedemeyergetNodeLabel (GInfo { options = opts }) dgnode = do
ea76e25262c3325f293fbdd6560f180ca18f9be4Thiemo Wiedemeyer flags <- readIORef opts
f5b31c8df89d0c8898cfabe0bd6c671e8285c0f1Christian Maeder return $ if flagHideNames flags && isInternalNode dgnode
79d103748927615310322af6f7806c7cef11a802Christian Maeder then "" else getDGNodeName dgnode