GraphLogic.hs revision f7b9d64160c23654b7288a3b0ee3e2b95af3e752
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 , 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
9a9860760c6f30558e5e60049692b6fc63904590Markus Gross , checkconservativityOfNode
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer , checkconservativityOfEdge
ea76e25262c3325f293fbdd6560f180ca18f9be4Thiemo Wiedemeyer , toggleHideNames
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer , toggleHideNodes
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer , toggleHideEdges
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo Wiedemeyer , translateGraph
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo Wiedemeyer , showLibGraph
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)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyerimport GUI.Taxonomy (displayConceptGraph,displaySubsortGraph)
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyerimport qualified GUI.GraphAbstraction as GA
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyerimport Reactor.InfoBus (encapsulateWaitTermAct)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyerimport qualified Common.OrderedMap as OMap
4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian Maederimport qualified Common.Lib.SizedList as SizedList
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyerimport Driver.Options ( HetcatsOpts, putIfVerbose, outtypes, doDump, verbose
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyerimport Driver.WriteLibDefn (writeShATermFile)
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyerimport Driver.ReadFn (libNameToFile, readVerbose)
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyerimport Data.Char (toLower)
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyerimport Data.List (partition, delete, 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
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
ea76e25262c3325f293fbdd6560f180ca18f9be4Thiemo Wiedemeyer mapM_ (\(s,upd) -> upd (\_ -> if flagHideNames flags then "" else s)) updater
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
fa1bf658051ac503f27ff1b59edb093398eed6edThiemo Wiedemeyer HidingFreeOrCofreeThm _ _ s -> isProvenThmLinkStatus s
92e96be605537638d75e9d3023ab698bd89cf889Thiemo Wiedemeyer $ foldl (\ e c -> case c of
92e96be605537638d75e9d3023ab698bd89cf889Thiemo Wiedemeyer InsertEdge (_, _, lbl) -> lbl:e
92e96be605537638d75e9d3023ab698bd89cf889Thiemo Wiedemeyer DeleteEdge (_, _, lbl) -> delete 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
d9f20cf968e246ec283f0c09f60af4b47b174398Thiemo WiedemeyerflattenHistory ((HistElem c):r) cs = flattenHistory r $ c:cs
d9f20cf968e246ec283f0c09f60af4b47b174398Thiemo WiedemeyerflattenHistory ((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 =
4014fb09362f3e38a91d7bb11b1484a4790e9297Thiemo Wiedemeyer 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"
3e3efd4ce838940032e875e6d08712a177c9c1d0Thiemo WiedemeyercompressTypes b (t:[]) = (t,b)
32d98ca5e560cf6c1062a0463be4c350af32bed5Thiemo WiedemeyercompressTypes b (t1:t2:r)
32d98ca5e560cf6c1062a0463be4c350af32bed5Thiemo Wiedemeyer | t1 == t2 = compressTypes b (t1:r)
32d98ca5e560cf6c1062a0463be4c350af32bed5Thiemo Wiedemeyer | t1 > t2 = compressTypes False (t1:r)
32d98ca5e560cf6c1062a0463be4c350af32bed5Thiemo Wiedemeyer | otherwise = compressTypes False (t2:r)
788bd3c33ec5aaeb90a1932c341ff837116410cfThiemo Wiedemeyer-- | innDG with filter of not shown edges
788bd3c33ec5aaeb90a1932c341ff837116410cfThiemo WiedemeyerfInnDG :: [EdgeId] -> DGraph -> Node -> [LEdge DGLinkLab]
39a2520d13a7d43f0c0fa71b94255c3f7c500005Christian 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]
39a2520d13a7d43f0c0fa71b94255c3f7c500005Christian 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]
788bd3c33ec5aaeb90a1932c341ff837116410cfThiemo Wiedemeyer -> [(Node,Node,DGEdgeType, Bool)]
788bd3c33ec5aaeb90a1932c341ff837116410cfThiemo WiedemeyergetCompressedEdges dg hidden ign = filterDuplicates $ getShortPaths
788bd3c33ec5aaeb90a1932c341ff837116410cfThiemo Wiedemeyer $ concatMap (\ e@(_,t,_) -> map (e:) $ getPaths dg t hidden [] ign) inEdges
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer inEdges = filter (\ (_,t,_) -> elem t hidden)
788bd3c33ec5aaeb90a1932c341ff837116410cfThiemo Wiedemeyer $ concatMap (fOutDG ign dg)
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer $ foldr (\ n i -> if elem n hidden
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer || elem n i then i else n:i) []
788bd3c33ec5aaeb90a1932c341ff837116410cfThiemo Wiedemeyer $ map (\ (s,_,_) -> s) $ concatMap (fInnDG ign dg) hidden
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer-- | filter duplicate paths
370e81d7af7821f0ac6ee0643613e87a727841e7Thiemo WiedemeyerfilterDuplicates :: [(Node,Node,DGEdgeType, Bool)]
370e81d7af7821f0ac6ee0643613e87a727841e7Thiemo Wiedemeyer -> [(Node,Node,DGEdgeType, Bool)]
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo WiedemeyerfilterDuplicates [] = []
80df5ce65c2bad7a0643106e524fe33cdcfab5b6Thiemo WiedemeyerfilterDuplicates r@((s, t, _, _) : _) = edges ++ filterDuplicates others
370e81d7af7821f0ac6ee0643613e87a727841e7Thiemo Wiedemeyer (same,others) = partition (\ (s',t', _, _) -> s == s' && t == t') r
80df5ce65c2bad7a0643106e524fe33cdcfab5b6Thiemo Wiedemeyer (mtypes,stypes) = partition (\ (_,_,_,b) -> not b) same
80df5ce65c2bad7a0643106e524fe33cdcfab5b6Thiemo Wiedemeyer stypes' = foldr (\e es -> if elem e es then es else e:es) [] stypes
80df5ce65c2bad7a0643106e524fe33cdcfab5b6Thiemo Wiedemeyer (et',_) = compressTypes False $ map (\ (_,_,et,_) -> et) mtypes
32d98ca5e560cf6c1062a0463be4c350af32bed5Thiemo Wiedemeyer 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 []
788bd3c33ec5aaeb90a1932c341ff837116410cfThiemo Wiedemeyer else concatMap (\ e@(_,t,_) -> map (e:) $ getPaths dg t hidden seen ign)
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer seen = node:seen'
788bd3c33ec5aaeb90a1932c341ff837116410cfThiemo Wiedemeyer 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]]
370e81d7af7821f0ac6ee0643613e87a727841e7Thiemo Wiedemeyer -> [(Node,Node,DGEdgeType,Bool)]
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo WiedemeyergetShortPaths [] = []
1ac36418f204bbe56f4cd951a979180721758999Christian MaedergetShortPaths (p : r) =
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo Wiedemeyer : getShortPaths r
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer (s,_,_) = head p
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer (_,t,_) = last p
370e81d7af7821f0ac6ee0643613e87a727841e7Thiemo Wiedemeyer (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
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer mh <- readVerbose logicGraph opts 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 '"
d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer ++ 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
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer 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
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer ost <- readIORef $ intState gInfo
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer case i_state ost of
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer Nothing -> return ()
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer Just ist -> do
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
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
28ca54b0d63d1d26a991711c8c7e85c474994715Christian Maeder nst = add2history cmd ost lln
83263d411f611d9902ef4d98c93be6ad9361c833Christian 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
521045d36343cd17dd217a81d4b9422ad6ab6a07Christian Maeder createTextDisplay title (title ++ "\n" ++ showDoc 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 ()
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer Just ist -> do
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer let Result ds res = computeTheory (i_libEnv ist) (libName gInfo) descr
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer showDiagMess (hetcatsOpts gInfo) ds
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer maybe (return ())
83263d411f611d9902ef4d98c93be6ad9361c833Christian Maeder (displayTheoryWithWarning "Theory" (getNameOfNode descr dgraph)
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer $ addHasInHidingWarning dgraph descr) res
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
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer Result ds moTh = computeTheory libEnv ln node
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer 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"
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer 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)
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer $ G_theory lidT (mkExtSign sign'') startSigId (toThSens sens1)
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer Nothing -> showDiagMess opts ds
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
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer title = "Proof status of node "++showName (dgn_name dgnode)
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer in createTextDisplay title stat
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyershowStatusAux :: DGNodeLab -> String
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo WiedemeyershowStatusAux dgnode = case dgn_theory dgnode of
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer G_theory _ _ _ sens _ ->
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer let goals = OMap.filter (not . isAxiom) sens
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer (proven,open) = OMap.partition isProvenSenStatus goals
c41a1c38edbd787d8fd12b9b5f11b73a37dafe0fChristian Maeder consGoal = "\nconservativity of this node"
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer in "Proven proof goals:\n"
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer ++ showDoc proven ""
260bfc3b7dc8ed037b7d98ee044302415db6fcd7Christian Maeder ++ if not $ hasOpenNodeConsStatus True dgnode
c41a1c38edbd787d8fd12b9b5f11b73a37dafe0fChristian Maeder then consGoal
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer ++ "\nOpen proof goals:\n"
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer ++ showDoc 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
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer-- | start local theorem proving or consistency checking at a node
1e3aca4178372af672efb237d16087c603fe5564Christian MaederproveAtNode :: Bool -> GInfo -> Int -> DGraph -> IO ()
95cb954c00f873306bf1a60b62d3209d3cff4102Christian MaederproveAtNode checkCons gInfo descr dgraph = do
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer let ln = libName gInfo
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer iSt = intState gInfo
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer ost <- readIORef iSt
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer case i_state ost of
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer Nothing -> return ()
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer Just ist -> do
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer let le = i_libEnv ist
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer dgn = labDG dgraph descr
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer (dgraph', dgn', le') <- if hasLock dgn then return (dgraph, dgn, le)
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer lockGlobal gInfo
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
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer unlockGlobal gInfo
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer return (dgraph', dgn', nwle)
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer acquired <- tryLockLocal dgn'
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer if acquired then do
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer let action = do
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer res@(Result d _) <- basicInferenceNode checkCons logicGraph ln
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer dgraph' (descr, dgn') le' iSt
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer when (null d || diagString (head d) /= "Proofs.Proofs: selection")
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer $ runProveAtNode checkCons gInfo (descr, dgn') res
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer b <- hidingWarnDiag dgn'
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer unlockLocal dgn'
f7b9d64160c23654b7288a3b0ee3e2b95af3e752Thiemo Wiedemeyer else errorDialog "Error" "Proofwindow already open"
8244e8866cad2be73b7e2b76a6659535f0f728ccChristian MaederrunProveAtNode :: Bool -> GInfo -> LNode DGNodeLab
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder -> Result G_theory -> IO ()
95cb954c00f873306bf1a60b62d3209d3cff4102Christian MaederrunProveAtNode checkCons gInfo (v, dgnode) (Result ds mres) =
28ca54b0d63d1d26a991711c8c7e85c474994715Christian Maeder let nn = getDGNodeName dgnode in
28ca54b0d63d1d26a991711c8c7e85c474994715Christian Maeder if checkCons then do
28ca54b0d63d1d26a991711c8c7e85c474994715Christian Maeder let nodetext = nn ++ " node: " ++ show v
85a6f36073352ad1732560fbfc958c3c80dfeb80Christian Maeder Just gth -> do
85a6f36073352ad1732560fbfc958c3c80dfeb80Christian Maeder createTextSaveDisplay ("Model for " ++ nodetext)
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer "model.log" $ showDoc gth ""
85a6f36073352ad1732560fbfc958c3c80dfeb80Christian Maeder updateNodeProof checkCons gInfo (v, dgnode) mres
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 showDiagMessAux 2 $ ds ++ es
85a6f36073352ad1732560fbfc958c3c80dfeb80Christian Maeder updateNodeProof checkCons gInfo (v, dgnode) tres
85a6f36073352ad1732560fbfc958c3c80dfeb80Christian Maeder _ -> return ()
85a6f36073352ad1732560fbfc958c3c80dfeb80Christian MaederupdateNodeProof :: Bool -> GInfo -> LNode DGNodeLab -> Maybe G_theory -> IO ()
85a6f36073352ad1732560fbfc958c3c80dfeb80Christian MaederupdateNodeProof checkCons gInfo (v, dgnode) tres = case tres of
85a6f36073352ad1732560fbfc958c3c80dfeb80Christian Maeder Just theory -> do
85a6f36073352ad1732560fbfc958c3c80dfeb80Christian Maeder let ln = libName gInfo
85a6f36073352ad1732560fbfc958c3c80dfeb80Christian Maeder iSt = intState gInfo
85a6f36073352ad1732560fbfc958c3c80dfeb80Christian Maeder nn = getDGNodeName dgnode
85a6f36073352ad1732560fbfc958c3c80dfeb80Christian Maeder lockGlobal gInfo
85a6f36073352ad1732560fbfc958c3c80dfeb80Christian Maeder ost <- readIORef iSt
85a6f36073352ad1732560fbfc958c3c80dfeb80Christian Maeder case i_state ost of
eb600800c6f539148144444c14bf6354b6eaf0ceChristian Maeder Nothing -> return ()
85a6f36073352ad1732560fbfc958c3c80dfeb80Christian Maeder Just iist -> do
85a6f36073352ad1732560fbfc958c3c80dfeb80Christian Maeder let le = i_libEnv iist
85a6f36073352ad1732560fbfc958c3c80dfeb80Christian Maeder dgraph = lookupDGraph ln le
e0eb2520b6b977e1ab84afa8774fdcf26efd2796Christian Maeder new = if checkCons then dgnode
85a6f36073352ad1732560fbfc958c3c80dfeb80Christian Maeder { nodeInfo = case nodeInfo dgnode of
85a6f36073352ad1732560fbfc958c3c80dfeb80Christian Maeder ninfo@DGNode { node_cons_status = ConsStatus c _ _ } ->
85a6f36073352ad1732560fbfc958c3c80dfeb80Christian Maeder ninfo { node_cons_status = ConsStatus c Cons
85a6f36073352ad1732560fbfc958c3c80dfeb80Christian Maeder $ Proven (DGRule "ConsistencyChecker")
85a6f36073352ad1732560fbfc958c3c80dfeb80Christian Maeder emptyProofBasis }
85a6f36073352ad1732560fbfc958c3c80dfeb80Christian Maeder ninfo -> ninfo }
85a6f36073352ad1732560fbfc958c3c80dfeb80Christian Maeder else dgnode { dgn_theory = theory }
e0eb2520b6b977e1ab84afa8774fdcf26efd2796Christian Maeder newLbl = if checkCons then new else new { globalTheory
e0eb2520b6b977e1ab84afa8774fdcf26efd2796Christian Maeder = computeLabelTheory le dgraph (v, new) }
e0eb2520b6b977e1ab84afa8774fdcf26efd2796Christian Maeder newDg = changeDGH dgraph $ SetNodeLab dgnode (v, newLbl)
85a6f36073352ad1732560fbfc958c3c80dfeb80Christian Maeder history = snd $ splitHistory dgraph newDg
85a6f36073352ad1732560fbfc958c3c80dfeb80Christian Maeder nst = add2history
28ca54b0d63d1d26a991711c8c7e85c474994715Christian Maeder (CommentCmd $ "basic inference done on " ++ nn ++ "\n")
28ca54b0d63d1d26a991711c8c7e85c474994715Christian Maeder ost [DgCommandChange ln]
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder { i_state = Just iist
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder { i_libEnv = Map.insert ln newDg le } }
85a6f36073352ad1732560fbfc958c3c80dfeb80Christian Maeder writeIORef iSt nwst
d7aa4e1cbe00f7f3add4da911673b3b176b140c3Thiemo Wiedemeyer runAndLock gInfo $ updateGraph gInfo $ reverse $ flatHistory history
eb600800c6f539148144444c14bf6354b6eaf0ceChristian Maeder unlockGlobal gInfo
85a6f36073352ad1732560fbfc958c3c80dfeb80Christian Maeder Nothing -> return ()
9a9860760c6f30558e5e60049692b6fc63904590Markus GrosscheckconservativityOfNode :: Int -> GInfo -> DGraph -> IO ()
9a9860760c6f30558e5e60049692b6fc63904590Markus GrosscheckconservativityOfNode descr gInfo 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
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian Maeder (str, nwle, ph) <- checkConservativityEdge True lnk (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
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer-- | show library referened by a DGRef node (=node drawn as a box)
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo WiedemeyershowReferencedLibrary :: Int -> GInfo -> ConvFunc -> LibFunc -> IO ()
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo WiedemeyershowReferencedLibrary descr gInfo@(GInfo{ libName = ln })
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer 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
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu 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
0dba5bbaaef2f620f3b83a16ab6b229c3dd50c98Christian Maeder gInfo' <- copyGInfo gInfo refLibname
0dba5bbaaef2f620f3b83a16ab6b229c3dd50c98Christian Maeder convGraph gInfo' "development graph" showLib
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer let gi = graphInfo gInfo'
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer GA.showTemporaryMessage gi "Development Graph initialized."
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer Nothing -> error $ "The referenced library (" ++ show refLibname
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer ++ ") 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-- DaVinciGraph to String
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer-- Functions to convert a DaVinciGraph to a String to store as a .udg file
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 ()
f39c70229e74147a02d15bd45c05a0b1b325532dChristian Maeder maybeFilePath <- fileSaveDialog (rmSuffix (libNameToFile ln) ++ ".udg")
32d98ca5e560cf6c1062a0463be4c350af32bed5Thiemo Wiedemeyer [ ("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
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer , 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
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer nodes <- filterM (\(n,_) -> do b <- GA.isHiddenNode gi n
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu return $ not b)
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer $ labNodesDG $ lookupDGraph ln le
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu nstring <- foldM (\s node -> do
32d98ca5e560cf6c1062a0463be4c350af32bed5Thiemo Wiedemeyer s' <- (node2String gInfo nodemap linkmap node)
32d98ca5e560cf6c1062a0463be4c350af32bed5Thiemo Wiedemeyer return $ (if null s then "" else s ++ ",\n") ++ s')
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) ++ "\")"
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer 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
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer , 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)
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder nm = "\"" ++ show linkid ++ ":" ++ show nodeid1 ++ "->"
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder ++ show nodeid2 ++ "\""
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer color' = "a(\"EDGECOLOR\",\"" ++ color ++ "\"),"
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder line' = "a(\"EDGEPATTERN\",\"" ++ map toLower (show line) ++ "\")"
8f5219469b89a15dc6d4c2c30463775975f5841cRazvan Pascanu return $ "l(" ++ nm ++ ",e(\"" ++ show ltype ++ "\","
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer ++ "[" ++ 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