GraphLogic.hs revision 8618f6dc90d5392c661114468b47c71e4ae4e9be
93fa7e4374de6e37328e752991a698bf03032c75Christian Maeder{-# OPTIONS -cpp #-}
93fa7e4374de6e37328e752991a698bf03032c75Christian Maeder{- |
93fa7e4374de6e37328e752991a698bf03032c75Christian MaederModule : $Header$
93fa7e4374de6e37328e752991a698bf03032c75Christian MaederDescription : Logic for manipulating the graph in the Central GUI
93fa7e4374de6e37328e752991a698bf03032c75Christian MaederCopyright : (c) Jorina Freya Gerken, Till Mossakowski, Uni Bremen 2002-2006
93fa7e4374de6e37328e752991a698bf03032c75Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
93fa7e4374de6e37328e752991a698bf03032c75Christian Maeder
bc67ede91ef5309852f1ba3a5a0d6b429f405e9dChristian MaederMaintainer : till@informatik.uni-bremen.de
bc67ede91ef5309852f1ba3a5a0d6b429f405e9dChristian MaederStability : provisional
bc67ede91ef5309852f1ba3a5a0d6b429f405e9dChristian MaederPortability : non-portable (imports Logic)
bc67ede91ef5309852f1ba3a5a0d6b429f405e9dChristian Maeder
bc67ede91ef5309852f1ba3a5a0d6b429f405e9dChristian MaederThis module provides functions for all the menus in the Hets GUI.
bc67ede91ef5309852f1ba3a5a0d6b429f405e9dChristian MaederThese are then assembled to the GUI in "GUI.GraphMenu".
bc67ede91ef5309852f1ba3a5a0d6b429f405e9dChristian Maeder-}
bc67ede91ef5309852f1ba3a5a0d6b429f405e9dChristian Maeder
93fa7e4374de6e37328e752991a698bf03032c75Christian Maedermodule GUI.GraphLogic
93fa7e4374de6e37328e752991a698bf03032c75Christian Maeder ( undo
3ec187613707411408c677058155bc618f16dabbChristian Maeder , performProofAction
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder , openProofStatus
2eb84fc82d3ffa9116bc471fda3742bd9e5a24bbChristian Maeder , saveProofStatus
dd38bafd384f5a5bc9634aad395505a0fd74395aChristian Maeder , proofMenu
2eb84fc82d3ffa9116bc471fda3742bd9e5a24bbChristian Maeder , showReferencedLibrary
2eb84fc82d3ffa9116bc471fda3742bd9e5a24bbChristian Maeder , getTheoryOfNode
2eb84fc82d3ffa9116bc471fda3742bd9e5a24bbChristian Maeder , translateTheoryOfNode
6e6ba3ab90205840b9c0ea408befaed7d1d7b80bChristian Maeder , displaySubsortGraph
6e6ba3ab90205840b9c0ea408befaed7d1d7b80bChristian Maeder , displayConceptGraph
6e6ba3ab90205840b9c0ea408befaed7d1d7b80bChristian Maeder , showProofStatusOfNode
409578f7f6dbee1e10dd1c969328bb92dabd087dChristian Maeder , proveAtNode
409578f7f6dbee1e10dd1c969328bb92dabd087dChristian Maeder , showNodeInfo
d697755cce49a436e1170e8e158c19f79b0389b8Christian Maeder , showDiagMess
409578f7f6dbee1e10dd1c969328bb92dabd087dChristian Maeder , showEdgeInfo
2eb84fc82d3ffa9116bc471fda3742bd9e5a24bbChristian Maeder , checkconservativityOfEdge
2eb84fc82d3ffa9116bc471fda3742bd9e5a24bbChristian Maeder , convert
4f6bf9805777b4c9b263f647a3fa97c8daeb54b2Christian Maeder , hideNodes
93fa7e4374de6e37328e752991a698bf03032c75Christian Maeder , hideNewProvedEdges
36b1d2b1423e96d38a7f5e9b7a18c4c323eedd0aChristian Maeder , hideShowNames
0ca0057165c510ada537b23f6797c770a51990e3Christian Maeder , showNodes
36b1d2b1423e96d38a7f5e9b7a18c4c323eedd0aChristian Maeder , translateGraph
e4eed2389ec1b1bfa03c662c71e8165e93df43c4Christian Maeder , showLibGraph
e4eed2389ec1b1bfa03c662c71e8165e93df43c4Christian Maeder , runAndLock
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder , saveUDGraph
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder , focusNode
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder , applyChanges
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder ) where
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maederimport Logic.Coerce(coerceSign)
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maederimport Logic.Grothendieck
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maederimport Logic.Comorphism
e4eed2389ec1b1bfa03c662c71e8165e93df43c4Christian Maederimport Logic.Prover
9987d35a267440c71e1e8b21c2ee6081a6390643Christian Maederimport Comorphisms.LogicGraph(logicGraph)
97061dace53e199664c3ec5da6434b8cd46b58dfChristian Maeder
3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maederimport Static.GTheory
9987d35a267440c71e1e8b21c2ee6081a6390643Christian Maederimport Static.DevGraph
97061dace53e199664c3ec5da6434b8cd46b58dfChristian Maederimport Static.PrintDevGraph
3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maederimport Static.DGTranslation(libEnv_translation, getDGLogic)
f161da699d7e8eddbb9294618dbc7a54966d7f7fChristian Maeder
f161da699d7e8eddbb9294618dbc7a54966d7f7fChristian Maederimport Proofs.EdgeUtils
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maederimport Proofs.InferBasic(basicInferenceNode)
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maederimport Proofs.StatusUtils(lookupHistory, removeContraryChanges)
f161da699d7e8eddbb9294618dbc7a54966d7f7fChristian Maederimport Proofs.TheoremHideShift
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder
5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maederimport GUI.Taxonomy (displayConceptGraph,displaySubsortGraph)
9256f871e7dd915ccfb5969e2117f054306cd366Christian Maederimport GUI.GraphTypes
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maederimport qualified GUI.GraphAbstraction as GA
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maederimport GUI.Utils
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder#ifdef UNIVERSION2
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maederimport Graphs.GraphConfigure
5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maederimport Reactor.InfoBus(encapsulateWaitTermAct)
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder#else
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maederimport GraphConfigure
6fb319833285f714693d58e9620d67ab21ddebe4Christian Maederimport InfoBus(encapsulateWaitTermAct)
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder#endif
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maederimport qualified GUI.HTkUtils as HTk
f161da699d7e8eddbb9294618dbc7a54966d7f7fChristian Maeder
5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maederimport Common.DocUtils (showDoc)
950766f1e2b0a1f7e502982c7dacfbf96ec3cb3aChristian Maederimport Common.AS_Annotation (isAxiom)
950766f1e2b0a1f7e502982c7dacfbf96ec3cb3aChristian Maederimport Common.ExtSign
950766f1e2b0a1f7e502982c7dacfbf96ec3cb3aChristian Maederimport Common.LibName
950766f1e2b0a1f7e502982c7dacfbf96ec3cb3aChristian Maederimport Common.Result
5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maederimport qualified Common.OrderedMap as OMap
950766f1e2b0a1f7e502982c7dacfbf96ec3cb3aChristian Maederimport qualified Common.Lib.SizedList as SizedList
950766f1e2b0a1f7e502982c7dacfbf96ec3cb3aChristian Maeder
950766f1e2b0a1f7e502982c7dacfbf96ec3cb3aChristian Maederimport Driver.Options(HetcatsOpts,putIfVerbose,outtypes,doDump,verbose,rmSuffix)
0cc809b79c4276013d0325bedbc33c4244d32705Christian Maederimport Driver.WriteLibDefn(writeShATermFile)
6eed7cde6b75d63ec6b8f7e31caac6919558a676Christian Maederimport Driver.ReadFn(libNameToFile, readVerbose)
03b2c932671a04fdba42cf5b9052b087402072e5Christian Maederimport Driver.AnaLib(anaLib)
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder
950766f1e2b0a1f7e502982c7dacfbf96ec3cb3aChristian Maederimport Data.IORef
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maederimport Data.Char(toLower)
950766f1e2b0a1f7e502982c7dacfbf96ec3cb3aChristian Maederimport Data.List(partition, delete, isPrefixOf)
950766f1e2b0a1f7e502982c7dacfbf96ec3cb3aChristian Maederimport Data.Maybe
950766f1e2b0a1f7e502982c7dacfbf96ec3cb3aChristian Maederimport Data.Graph.Inductive.Graph (Node, LEdge, LNode)
950766f1e2b0a1f7e502982c7dacfbf96ec3cb3aChristian Maederimport qualified Data.Map as Map
950766f1e2b0a1f7e502982c7dacfbf96ec3cb3aChristian Maeder
950766f1e2b0a1f7e502982c7dacfbf96ec3cb3aChristian Maederimport Control.Monad
950766f1e2b0a1f7e502982c7dacfbf96ec3cb3aChristian Maederimport Control.Concurrent (forkIO)
950766f1e2b0a1f7e502982c7dacfbf96ec3cb3aChristian Maederimport Control.Concurrent.MVar
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maederimport Interfaces.History
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maederimport Interfaces.DataTypes
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maederimport Interfaces.Utils
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder-- | Locks the global lock and runs function
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian MaederrunAndLock :: GInfo -> IO () -> IO ()
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian MaederrunAndLock (GInfo { functionLock = lock
03b2c932671a04fdba42cf5b9052b087402072e5Christian Maeder , graphInfo = gi
03b2c932671a04fdba42cf5b9052b087402072e5Christian Maeder }) function = do
03b2c932671a04fdba42cf5b9052b087402072e5Christian Maeder locked <- tryPutMVar lock ()
03b2c932671a04fdba42cf5b9052b087402072e5Christian Maeder case locked of
03b2c932671a04fdba42cf5b9052b087402072e5Christian Maeder True -> do
03b2c932671a04fdba42cf5b9052b087402072e5Christian Maeder GA.deactivateGraphWindow gi
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder function
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder takeMVar lock
03b2c932671a04fdba42cf5b9052b087402072e5Christian Maeder GA.redisplay gi
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder GA.layoutImproveAll gi
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder GA.activateGraphWindow gi
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder False ->
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder GA.showTemporaryMessage gi
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder "an other function is still working ... please wait ..."
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder
03b2c932671a04fdba42cf5b9052b087402072e5Christian Maeder-- | Undo one step of the History
d21f1db14625cb0a536fc06b46fcc115d48a25bbChristian Maederundo :: GInfo -> Bool -> IO ()
03b2c932671a04fdba42cf5b9052b087402072e5Christian Maederundo gInfo@(GInfo { graphInfo = gi }) isUndo = do
d21f1db14625cb0a536fc06b46fcc115d48a25bbChristian Maeder hhn <- GA.hasHiddenNodes gi
d21f1db14625cb0a536fc06b46fcc115d48a25bbChristian Maeder intSt <- readIORef $ intState gInfo
3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder nwSt <- if isUndo then undoOneStep intSt else redoOneStep intSt
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder writeIORef (intState gInfo) nwSt
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder if hhn then hideNodes gInfo else return ()
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder GA.redisplay gi
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder-- | Toggles to display internal node names
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian MaederhideShowNames :: GInfo -> Bool -> IO ()
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian MaederhideShowNames (GInfo { internalNamesIORef = showInternalNames
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder }) toggle = do
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder (intrn::InternalNames) <- readIORef showInternalNames
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder let showThem = if toggle then not $ showNames intrn else showNames intrn
9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder showItrn s = if showThem then s else ""
9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder mapM_ (\(s,upd) -> upd (\_ -> showItrn s)) $ updater intrn
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder writeIORef showInternalNames $ intrn {showNames = showThem}
6e6ba3ab90205840b9c0ea408befaed7d1d7b80bChristian Maeder
6fb319833285f714693d58e9620d67ab21ddebe4Christian Maeder-- | shows all hidden nodes and edges
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian MaedershowNodes :: GInfo -> IO ()
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian MaedershowNodes gInfo@(GInfo { graphInfo = gi
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder }) = do
1919917c90a1bf84a25ca866ac632605ad0548e6Christian Maeder hhn <- GA.hasHiddenNodes gi
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder case hhn of
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder True -> do
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder GA.showTemporaryMessage gi "Revealing hidden nodes ..."
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder GA.showAll gi
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder hideShowNames gInfo False
9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder False ->
9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder GA.showTemporaryMessage gi "No hidden nodes found ..."
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder-- | hides all unnamed internal nodes that are proven
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian MaederhideNodes :: GInfo -> IO ()
d21f1db14625cb0a536fc06b46fcc115d48a25bbChristian MaederhideNodes gInfo@(GInfo { graphInfo = gi
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder , libName = ln }) = do
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder hhn <- GA.hasHiddenNodes gi
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder ost <- readIORef $ intState gInfo
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder case i_state ost of
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder Nothing -> return ()
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder Just ist -> if hhn then
3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder GA.showTemporaryMessage gi "Nodes already hidden ..."
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder else do
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder GA.showTemporaryMessage gi "Hiding unnamed nodes..."
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder let le = i_libEnv ist
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder dg = lookupDGraph ln le
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder nodes = selectNodesByType dg [DGNodeType
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder { nonRefType = NonRefType
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder { isProvenCons = True
dd38bafd384f5a5bc9634aad395505a0fd74395aChristian Maeder , isInternalSpec = True}
dd38bafd384f5a5bc9634aad395505a0fd74395aChristian Maeder , isLocallyEmpty = True}]
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder edges = getCompressedEdges dg nodes
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder GA.hideNodes gi nodes edges
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder-- | hides all proven edges created not initialy
dd38bafd384f5a5bc9634aad395505a0fd74395aChristian MaederhideNewProvedEdges :: GInfo -> IO ()
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian MaederhideNewProvedEdges gInfo@(GInfo { graphInfo = gi
3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder , libName = ln }) = do
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder ost <- readIORef $ intState gInfo
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder case i_state ost of
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder Nothing -> return ()
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder Just ist -> do
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder let ph = SizedList.toList $ proofHistory
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder $ lookupDGraph ln $ i_libEnv ist
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder edges = foldl (\ e c -> case c of
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder InsertEdge (_, _, lbl) -> (dgl_id lbl):e
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder DeleteEdge (_, _, lbl) -> delete (dgl_id lbl) e
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder _ -> e
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder ) [] $ flattenHistory ph []
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder mapM_ (GA.hideEdge gi) edges
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder GA.redisplay gi
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder-- | generates from list of HistElem one list of DGChanges
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian MaederflattenHistory :: [HistElem] -> [DGChange] -> [DGChange]
6fb319833285f714693d58e9620d67ab21ddebe4Christian MaederflattenHistory [] cs = cs
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian MaederflattenHistory ((HistElem c):r) cs = flattenHistory r $ c:cs
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian MaederflattenHistory ((HistGroup _ ph):r) cs =
6fb319833285f714693d58e9620d67ab21ddebe4Christian Maeder flattenHistory r $ flattenHistory (SizedList.toList ph) cs
6fb319833285f714693d58e9620d67ab21ddebe4Christian Maeder
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder-- | selects all nodes of a type with outgoing edges
6fb319833285f714693d58e9620d67ab21ddebe4Christian MaederselectNodesByType :: DGraph -> [DGNodeType] -> [Node]
6fb319833285f714693d58e9620d67ab21ddebe4Christian MaederselectNodesByType dg types =
6fb319833285f714693d58e9620d67ab21ddebe4Christian Maeder filter (\ n -> outDG dg n /= []) $ map fst
c8bf82bdb27dfa58f7f05045c639c14276be3333Christian Maeder $ filter (\ (_, n) -> elem (getRealDGNodeType n) types) $ labNodesDG dg
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder-- | compresses a list of types to the highest one
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian MaedercompressTypes :: Bool -> [DGEdgeType] -> (DGEdgeType, Bool)
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian MaedercompressTypes _ [] = error "compressTypes: wrong usage"
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian MaedercompressTypes b (t:[]) = (t,b)
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian MaedercompressTypes b (t1:t2:r) = if t1 == t2 then compressTypes b (t1:r) else
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder if t1 > t2 then compressTypes False (t1:r) else compressTypes False (t2:r)
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder-- | returns a list of compressed edges
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian MaedergetCompressedEdges :: DGraph -> [Node] -> [(Node,Node,(DGEdgeType, Bool))]
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian MaedergetCompressedEdges dg hidden = filterDuplicates $ getShortPaths
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder $ concatMap (\ e@(_,t,_) -> map (e:) $ getPaths dg t hidden []) inEdges
1919917c90a1bf84a25ca866ac632605ad0548e6Christian Maeder where
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder inEdges = filter (\ (_,t,_) -> elem t hidden)
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder $ concatMap (outDG dg)
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder $ foldr (\ n i -> if elem n hidden
1919917c90a1bf84a25ca866ac632605ad0548e6Christian Maeder || elem n i then i else n:i) []
1919917c90a1bf84a25ca866ac632605ad0548e6Christian Maeder $ map (\ (s,_,_) -> s) $ concatMap (innDG dg) hidden
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder-- | filter duplicate paths
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian MaederfilterDuplicates :: [(Node,Node,(DGEdgeType, Bool))]
f161da699d7e8eddbb9294618dbc7a54966d7f7fChristian Maeder -> [(Node,Node,(DGEdgeType, Bool))]
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian MaederfilterDuplicates [] = []
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian MaederfilterDuplicates ((s, t, (et,b)) : r) = edge : filterDuplicates others
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder where
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder (same,others) = partition (\ (s',t',_) -> s == s' && t == t') r
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder b' = and $ b : map (\ (_,_,(_,b'')) -> b'') same
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder edge = (s,t,compressTypes b' $ et : map (\ (_,_,(et',_)) -> et') same)
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder-- | returns the pahts of a given node through hidden nodes
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian MaedergetPaths :: DGraph -> Node -> [Node] -> [Node] -> [[LEdge DGLinkLab]]
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian MaedergetPaths dg node hidden seen' = case elem node hidden of
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder True -> case edges /= [] of
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder True -> concatMap (\ e@(_,t,_) -> map (e:) $ getPaths dg t hidden seen)
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder edges
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder False -> []
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder False -> [[]]
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder where
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder seen = node:seen'
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder edges = filter (\ (_,t,_) -> notElem t seen) $ outDG dg node
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder-- | returns source and target node of a path with the compressed type
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian MaedergetShortPaths :: [[LEdge DGLinkLab]]
3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder -> [(Node,Node,(DGEdgeType,Bool))]
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian MaedergetShortPaths [] = []
f161da699d7e8eddbb9294618dbc7a54966d7f7fChristian MaedergetShortPaths (p : r) =
9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder (s, t, compressTypes True $ map (\ (_,_,e) -> getRealDGLinkType e) p)
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder : getShortPaths r
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder where
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder (s,_,_) = head p
9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder (_,t,_) = last p
9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder-- | Let the user select a Node to focus
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian MaederfocusNode :: GInfo -> IO ()
accab0bf9b8aa690d70174f41fe94370323959b9Christian MaederfocusNode gInfo@(GInfo { graphInfo = gi
accab0bf9b8aa690d70174f41fe94370323959b9Christian Maeder , libName = ln }) = do
accab0bf9b8aa690d70174f41fe94370323959b9Christian Maeder ost <- readIORef $ intState gInfo
accab0bf9b8aa690d70174f41fe94370323959b9Christian Maeder case i_state ost of
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder Nothing -> return ()
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Just ist -> do
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder let le = i_libEnv ist
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder idsnodes <- filterM (fmap not . GA.isHiddenNode gi . fst)
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder $ labNodesDG $ lookupDGraph ln le
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder selection <- listBox "Select a node to focus"
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder $ map (\ (n, l) -> shows n " " ++ getDGNodeName l) idsnodes
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder case selection of
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder Just idx -> GA.focusNode gi $ fst $ idsnodes !! idx
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder Nothing -> return ()
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder
215b5e40dadbe65b1b225b1b80e2c529ef00bebcChristian MaedershowLibGraph :: GInfo -> LibFunc -> IO ()
215b5e40dadbe65b1b225b1b80e2c529ef00bebcChristian MaedershowLibGraph gInfo showLib = do
215b5e40dadbe65b1b225b1b80e2c529ef00bebcChristian Maeder showLib gInfo
215b5e40dadbe65b1b225b1b80e2c529ef00bebcChristian Maeder return ()
215b5e40dadbe65b1b225b1b80e2c529ef00bebcChristian Maeder
9987d35a267440c71e1e8b21c2ee6081a6390643Christian Maeder{- | it tries to perform the given action to the given graph.
9987d35a267440c71e1e8b21c2ee6081a6390643Christian Maeder If part of the given graph is not hidden, then the action can
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder be performed directly; otherwise the graph will be shown completely
950766f1e2b0a1f7e502982c7dacfbf96ec3cb3aChristian Maeder firstly, and then the action will be performed, and after that the graph
950766f1e2b0a1f7e502982c7dacfbf96ec3cb3aChristian Maeder will be hidden again.
950766f1e2b0a1f7e502982c7dacfbf96ec3cb3aChristian Maeder-}
950766f1e2b0a1f7e502982c7dacfbf96ec3cb3aChristian MaederperformProofAction :: GInfo -> IO () -> IO ()
950766f1e2b0a1f7e502982c7dacfbf96ec3cb3aChristian MaederperformProofAction gInfo@(GInfo { graphInfo = gi
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder }) proofAction = do
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder let actionWithMessage = do
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder GA.showTemporaryMessage gi
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder "Applying development graph calculus proof rule..."
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder proofAction
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder hhn <- GA.hasHiddenNodes gi
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder case hhn of
950766f1e2b0a1f7e502982c7dacfbf96ec3cb3aChristian Maeder True -> do
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder showNodes gInfo
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder actionWithMessage
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder hideNodes gInfo
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder False -> actionWithMessage
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder GA.showTemporaryMessage gi
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder "Development graph calculus proof rule finished."
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian MaedersaveProofStatus :: GInfo -> FilePath -> IO ()
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian MaedersaveProofStatus gInfo@(GInfo { hetcatsOpts = opts
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder , libName = ln
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder }) file = encapsulateWaitTermAct $ do
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder ost <- readIORef $ intState gInfo
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder case i_state ost of
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder Nothing -> return ()
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder Just ist -> do
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder let proofStatus = i_libEnv ist
03b2c932671a04fdba42cf5b9052b087402072e5Christian Maeder writeShATermFile file (ln, lookupHistory ln proofStatus)
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder putIfVerbose opts 2 $ "Wrote " ++ file
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder-- | implementation of open menu, read in a proof status
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian MaederopenProofStatus :: GInfo -> FilePath -> ConvFunc -> LibFunc
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder -> IO ()
3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian MaederopenProofStatus gInfo@(GInfo { hetcatsOpts = opts
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder , libName = ln }) file convGraph showLib = do
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder ost <- readIORef $ intState gInfo
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder case i_state ost of
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder Nothing -> return ()
3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder Just ist -> do
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder mh <- readVerbose opts ln file
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder case mh of
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder Nothing -> errorDialog "Error" $ "Could not read proof status from file '"
3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder ++ file ++ "'"
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder Just h -> do
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder let libfile = libNameToFile opts ln
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder m <- anaLib opts { outtypes = [] } libfile
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder case m of
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder Nothing -> errorDialog "Error"
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder $ "Could not read original development graph from '"
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder ++ libfile ++ "'"
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder Just (_, libEnv) -> case Map.lookup ln libEnv of
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder Nothing -> errorDialog "Error" $ "Could not get original"
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder ++ "development graph for '" ++ showDoc ln "'"
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder Just dg -> do
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder lockGlobal gInfo
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder let oldEnv = i_libEnv ist
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder proofStatus = Map.insert ln
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder (applyProofHistory h dg) oldEnv
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder nwst = ost { i_state = Just ist {
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder i_libEnv = proofStatus } }
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder writeIORef (intState gInfo) nwst
03b2c932671a04fdba42cf5b9052b087402072e5Christian Maeder unlockGlobal gInfo
959680c14d514a07eebf7a0c9f786f86a4fcf1ebChristian Maeder gInfo' <- copyGInfo gInfo ln
36b1d2b1423e96d38a7f5e9b7a18c4c323eedd0aChristian Maeder convGraph gInfo' "Proof Status " showLib
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder let gi = graphInfo gInfo
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder GA.deactivateGraphWindow gi
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder GA.redisplay gi
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder GA.layoutImproveAll gi
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder GA.activateGraphWindow gi
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder-- | apply a rule of the development graph calculus
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian MaederproofMenu :: GInfo
f56e4fe56fdf66d711e5fafaa71c2587dd9a066fChristian Maeder -> String
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder -> (LibEnv -> IO (Result LibEnv))
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder -> IO ()
f56e4fe56fdf66d711e5fafaa71c2587dd9a066fChristian MaederproofMenu gInfo@(GInfo { graphInfo = gi
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder , hetcatsOpts = hOpts
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder , proofGUIMVar = guiMVar
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder , libName = ln
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder }) str proofFun = do
469af98c69977faf5666e689eae863c1606ce269Christian Maeder ost <- readIORef $ intState gInfo
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder case i_state ost of
469af98c69977faf5666e689eae863c1606ce269Christian Maeder Nothing -> return ()
5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maeder Just ist -> do
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder filled <- tryPutMVar guiMVar Nothing
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder if not filled
accab0bf9b8aa690d70174f41fe94370323959b9Christian Maeder then readMVar guiMVar >>=
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder maybe (putIfVerbose hOpts 0 "proofMenu: ignored Nothing")
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder (\ w -> do
f56e4fe56fdf66d711e5fafaa71c2587dd9a066fChristian Maeder putIfVerbose hOpts 4 $
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder "proofMenu: Ignored Proof command; " ++
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder "maybe a proof window is still open?"
f56e4fe56fdf66d711e5fafaa71c2587dd9a066fChristian Maeder HTk.putWinOnTop w)
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder else do
f56e4fe56fdf66d711e5fafaa71c2587dd9a066fChristian Maeder lockGlobal gInfo
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder let proofStatus = i_libEnv ist
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder putIfVerbose hOpts 4 "Proof started via menu"
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Result ds res <- proofFun proofStatus
f56e4fe56fdf66d711e5fafaa71c2587dd9a066fChristian Maeder putIfVerbose hOpts 4 "Analyzing result of proof"
1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder case res of
1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder Nothing -> do
1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder unlockGlobal gInfo
f56e4fe56fdf66d711e5fafaa71c2587dd9a066fChristian Maeder printDiags 2 ds
f56e4fe56fdf66d711e5fafaa71c2587dd9a066fChristian Maeder Just newProofStatus -> do
f56e4fe56fdf66d711e5fafaa71c2587dd9a066fChristian Maeder let newGr = lookupDGraph ln newProofStatus
5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maeder history = snd $ splitHistory (lookupDGraph ln proofStatus) newGr
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder lln = map DgCommandChange $ calcGlobalHistory
5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maeder proofStatus newProofStatus
5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maeder nmStr = strToCmd str
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder nst = add2history nmStr ost lln
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder nwst = nst { i_state = Just ist { i_libEnv=newProofStatus}}
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder doDump hOpts "PrintHistory" $ do
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder putStrLn "History"
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder print $ prettyHistory history
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder applyChanges gi $ reverse $ flatHistory history
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder writeIORef (intState gInfo) nwst
05b5fdc3a64b84276a9792c1df60b2c48c1738bdChristian Maeder unlockGlobal gInfo
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder hideShowNames gInfo False
05b5fdc3a64b84276a9792c1df60b2c48c1738bdChristian Maeder mGUIMVar <- tryTakeMVar guiMVar
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder maybe (fail "should be filled with Nothing after proof attempt")
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder (const $ return ())
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder mGUIMVar
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian MaedercalcGlobalHistory :: LibEnv -> LibEnv -> [LIB_NAME]
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian MaedercalcGlobalHistory old new = let
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder length' ln = SizedList.size . proofHistory . lookupDGraph ln
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder changes = filter (\ ln -> length' ln old < length' ln new) $ Map.keys old
03b2c932671a04fdba42cf5b9052b087402072e5Christian Maeder in concatMap (\ ln -> replicate (length' ln new - length' ln old) ln) changes
3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian MaedershowNodeInfo :: Int -> DGraph -> IO ()
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian MaedershowNodeInfo descr dgraph = do
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder let dgnode = labDG dgraph descr
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder title = (if isDGRef dgnode then ("reference " ++) else
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder if isInternalNode dgnode then ("internal " ++) else id)
bc67ede91ef5309852f1ba3a5a0d6b429f405e9dChristian Maeder "node " ++ getDGNodeName dgnode ++ " " ++ show descr
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder createTextDisplay title (title ++ "\n" ++ showDoc dgnode "")
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian MaedershowDiagMessAux :: Int -> [Diagnosis] -> IO ()
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian MaedershowDiagMessAux v ds = let es = filterDiags v ds in
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder if null es then return () else
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder (if hasErrors es then errorDialog "Error" else infoDialog "Info") $ unlines
6e6ba3ab90205840b9c0ea408befaed7d1d7b80bChristian Maeder $ map show es
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian MaedershowDiagMess :: HetcatsOpts -> [Diagnosis] -> IO ()
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian MaedershowDiagMess = showDiagMessAux . verbose
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder
9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder{- | outputs the theory of a node in a window;
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder used by the node menu -}
959680c14d514a07eebf7a0c9f786f86a4fcf1ebChristian MaedergetTheoryOfNode :: GInfo -> Int -> DGraph -> IO ()
36b1d2b1423e96d38a7f5e9b7a18c4c323eedd0aChristian MaedergetTheoryOfNode gInfo descr dgraph = do
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder ost <- readIORef $ intState gInfo
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder case i_state ost of
1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder Nothing -> return ()
959680c14d514a07eebf7a0c9f786f86a4fcf1ebChristian Maeder Just ist -> do
9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder let Result ds res = computeTheory (i_libEnv ist) (libName gInfo) descr
9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder showDiagMess (hetcatsOpts gInfo) ds
36b1d2b1423e96d38a7f5e9b7a18c4c323eedd0aChristian Maeder maybe (return ())
1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder (displayTheoryWithWarning "Theory" (getNameOfNode descr dgraph)
9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder $ addHasInHidingWarning dgraph descr) res
bc67ede91ef5309852f1ba3a5a0d6b429f405e9dChristian Maeder
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder{- | translate the theory of a node in a window;
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder used by the node menu -}
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian MaedertranslateTheoryOfNode :: GInfo -> Int -> DGraph -> IO ()
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian MaedertranslateTheoryOfNode gInfo@(GInfo { hetcatsOpts = opts
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder , libName = ln }) node dgraph = do
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder ost <- readIORef $ intState gInfo
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder case i_state ost of
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Nothing -> return ()
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder Just ist -> do
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder let libEnv = i_libEnv ist
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder Result ds moTh = computeTheory libEnv ln node
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder case moTh of
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder Just th@(G_theory lid sign _ sens _) -> do
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder -- find all comorphism paths starting from lid
bc67ede91ef5309852f1ba3a5a0d6b429f405e9dChristian Maeder let paths = findComorphismPaths logicGraph (sublogicOfTh th)
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder -- let the user choose one
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder sel <- listBox "Choose a node logic translation" $ map show paths
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder case sel of
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Nothing -> errorDialog "Error" "no node logic translation chosen"
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Just i -> do
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Comorphism cid <- return (paths!!i)
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder -- adjust lid's
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder let lidS = sourceLogic cid
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder lidT = targetLogic cid
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder sign' <- coerceSign lid lidS "" sign
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder sens' <- coerceThSens lid lidS "" sens
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder -- translate theory along chosen comorphism
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder let Result es mTh = wrapMapTheory cid
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder (plainSign sign', toNamedList sens')
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder case mTh of
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Nothing -> showDiagMess opts es
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Just (sign'', sens1) -> displayTheoryWithWarning
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder "Translated Theory" (getNameOfNode node dgraph)
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder (addHasInHidingWarning dgraph node)
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder (G_theory lidT (mkExtSign sign'') startSigId
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder (toThSens sens1) startThId)
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Nothing -> showDiagMess opts ds
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder-- | Show proof status of a node
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian MaedershowProofStatusOfNode :: GInfo -> Int -> DGraph -> IO ()
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian MaedershowProofStatusOfNode _ descr dgraph = do
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder let dgnode = labDG dgraph descr
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder stat = showStatusAux dgnode
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder title = "Proof status of node "++showName (dgn_name dgnode)
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder createTextDisplay title stat
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian MaedershowStatusAux :: DGNodeLab -> String
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian MaedershowStatusAux dgnode =
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder case dgn_theory dgnode of
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder G_theory _ _ _ sens _ ->
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder let goals = OMap.filter (not . isAxiom) sens
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder (proven,open) = OMap.partition isProvenSenStatus goals
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder consGoal = "\nconservativity of this node"
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder in "Proven proof goals:\n"
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder ++ showDoc proven ""
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder ++ if not $ hasOpenConsStatus True dgnode
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder then consGoal
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder else ""
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder ++ "\nOpen proof goals:\n"
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder ++ showDoc open ""
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder ++ if hasOpenConsStatus False dgnode
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder then consGoal
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder else ""
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder-- | start local theorem proving or consistency checking at a node
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian MaederproveAtNode :: Bool -> GInfo -> Int -> DGraph -> IO ()
1eb602487b8b0dff5fad820439fc27264eb8889cChristian MaederproveAtNode checkCons gInfo descr dgraph = do
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder let ln = libName gInfo
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder iSt = intState gInfo
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder ost <- readIORef iSt
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder case i_state ost of
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Nothing -> return ()
1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder Just ist -> do
959680c14d514a07eebf7a0c9f786f86a4fcf1ebChristian Maeder let le = i_libEnv ist
36b1d2b1423e96d38a7f5e9b7a18c4c323eedd0aChristian Maeder dgn = labDG dgraph descr
1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder (dgraph', dgn', le') <- if hasLock dgn then return (dgraph, dgn, le) else do
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder lockGlobal gInfo
9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder (dgraph', dgn') <- initLocking (lookupDGraph ln le) (descr, dgn)
70ca840c8a6cf3591d5f9aa9a3de6fae42d696e8Christian Maeder let nwle = Map.insert ln dgraph' le
93fa7e4374de6e37328e752991a698bf03032c75Christian Maeder nwst = ost { i_state = Just $ ist { i_libEnv = nwle} }
93fa7e4374de6e37328e752991a698bf03032c75Christian Maeder writeIORef iSt nwst
93fa7e4374de6e37328e752991a698bf03032c75Christian Maeder unlockGlobal gInfo
d697755cce49a436e1170e8e158c19f79b0389b8Christian Maeder return (dgraph', dgn', nwle)
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder acquired <- tryLockLocal dgn'
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder if acquired then do
2f98027959ced502c0332e557618b42e41a2504aChristian Maeder let action = do
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder guiMVar <- newMVar Nothing
2f98027959ced502c0332e557618b42e41a2504aChristian Maeder res <- basicInferenceNode checkCons logicGraph ln dgraph'
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder (descr, dgn') guiMVar le' iSt
2f98027959ced502c0332e557618b42e41a2504aChristian Maeder runProveAtNode checkCons gInfo (descr, dgn') res
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder unlockLocal dgn'
6e6ba3ab90205840b9c0ea408befaed7d1d7b80bChristian Maeder if checkCons && labelHasHiding dgn' then do
a5023d78ecc3452c0de580912e7bd018640ddeaaChristian Maeder b <- warningDialog "Warning"
2f98027959ced502c0332e557618b42e41a2504aChristian Maeder (unwords $ hidingWarning ++ ["Try anyway?"]) $ Just action
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder unless b $ unlockLocal dgn'
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder return ()
2f98027959ced502c0332e557618b42e41a2504aChristian Maeder else forkIO action >> return ()
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder else errorDialog "Error" "Proofwindow already open"
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian MaederrunProveAtNode :: Bool -> GInfo -> LNode DGNodeLab
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder -> Result G_theory -> IO ()
2f98027959ced502c0332e557618b42e41a2504aChristian MaederrunProveAtNode checkCons gInfo (v, dgnode) (Result ds mres) =
2f98027959ced502c0332e557618b42e41a2504aChristian Maeder if checkCons then do
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder let nodetext = getDGNodeName dgnode ++ " node: " ++ show v
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder case mres of
2f98027959ced502c0332e557618b42e41a2504aChristian Maeder Just gth -> createTextSaveDisplay ("Model for " ++ nodetext)
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder "model.log" $ showDoc gth ""
2f98027959ced502c0332e557618b42e41a2504aChristian Maeder Nothing -> infoDialog nodetext $ unlines
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder $ "could not (re-)construct a" : "model" : map diagString ds
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder else let oldTh = dgn_theory dgnode in case mres of
2f98027959ced502c0332e557618b42e41a2504aChristian Maeder Just newTh | newTh /= oldTh -> do
2f98027959ced502c0332e557618b42e41a2504aChristian Maeder let Result es tres = joinG_sentences oldTh newTh
2f98027959ced502c0332e557618b42e41a2504aChristian Maeder ln = libName gInfo
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder iSt = intState gInfo
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder showDiagMessAux 2 $ ds ++ es
2f98027959ced502c0332e557618b42e41a2504aChristian Maeder case tres of
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder Just theory -> do
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder lockGlobal gInfo
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder ost <- readIORef iSt
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder case i_state ost of
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder Nothing -> unlockGlobal gInfo
2f98027959ced502c0332e557618b42e41a2504aChristian Maeder Just iist -> do
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder let le = i_libEnv iist
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder dgraph = lookupDGraph ln le
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder new_dgn = dgnode { dgn_theory = theory }
2f98027959ced502c0332e557618b42e41a2504aChristian Maeder newDg = changeDGH dgraph $ SetNodeLab dgnode (v, new_dgn)
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder history = snd $ splitHistory dgraph newDg
2f98027959ced502c0332e557618b42e41a2504aChristian Maeder nst = add2history "" ost [DgCommandChange ln]
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder nwst = nst
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder { i_state = Just iist
2f98027959ced502c0332e557618b42e41a2504aChristian Maeder { i_libEnv = Map.insert ln newDg le } }
2f98027959ced502c0332e557618b42e41a2504aChristian Maeder applyChanges (graphInfo gInfo) $ reverse $ flatHistory history
2f98027959ced502c0332e557618b42e41a2504aChristian Maeder writeIORef iSt nwst
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder unlockGlobal gInfo
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder hideShowNames gInfo False
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder Nothing -> return ()
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder _ -> return ()
fd40e201b7277427113c89724d8a2389c18e9cbdChristian Maeder
fd40e201b7277427113c89724d8a2389c18e9cbdChristian MaederedgeErr :: Int -> IO ()
1eb602487b8b0dff5fad820439fc27264eb8889cChristian MaederedgeErr descr = errorDialog "Error" $ "edge with descriptor " ++ show descr
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder ++ " not found in the development graph"
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder-- | print the id, origin, type, proof-status and morphism of the edge
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian MaedershowEdgeInfo :: Int -> Maybe (LEdge DGLinkLab) -> IO ()
1eb602487b8b0dff5fad820439fc27264eb8889cChristian MaedershowEdgeInfo descr me = case me of
1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder Just e@(_, _, l) -> let estr = showLEdge e in
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder createTextDisplay ("Info of " ++ estr)
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder (estr ++ "\n" ++ showDoc l "")
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder Nothing -> edgeErr descr
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder-- | check conservativity of the edge
1eb602487b8b0dff5fad820439fc27264eb8889cChristian MaedercheckconservativityOfEdge :: Int -> GInfo -> Maybe (LEdge DGLinkLab) -> IO ()
1eb602487b8b0dff5fad820439fc27264eb8889cChristian MaedercheckconservativityOfEdge descr gInfo me = case me of
1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder Nothing -> edgeErr descr
9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder Just lnk -> do
959680c14d514a07eebf7a0c9f786f86a4fcf1ebChristian Maeder let iSt = intState gInfo
959680c14d514a07eebf7a0c9f786f86a4fcf1ebChristian Maeder gi = graphInfo gInfo
ln = libName gInfo
ost <- readIORef iSt
case i_state ost of
Nothing -> return ()
Just iist -> do
lockGlobal gInfo
(str, nwle, ph) <- checkConservativityEdge True lnk (i_libEnv iist) ln
if isPrefixOf "No conservativity" str
then do
errorDialog "Result of conservativity check" str
unlockGlobal gInfo
else do
createTextDisplay "Result of conservativity check" str
applyChanges gi $ reverse $ flatHistory ph
GA.redisplay gi
let nst = add2history "" ost [DgCommandChange ln]
nwst = nst { i_state = Just $ iist { i_libEnv = nwle}}
writeIORef iSt nwst
unlockGlobal gInfo
convert :: GA.GraphInfo -> DGraph -> IO ()
convert ginfo dgraph = do
convertNodes ginfo dgraph
convertEdges ginfo dgraph
{- | converts the nodes of the development graph, if it has any,
and returns the resulting conversion maps
if the graph is empty the conversion maps are returned unchanged-}
convertNodes :: GA.GraphInfo -> DGraph -> IO ()
convertNodes ginfo = mapM_ (convertNodesAux ginfo) .labNodesDG
{- | auxiliary function for convertNodes if the given list of nodes is
emtpy, it returns the conversion maps unchanged otherwise it adds the
converted first node to the abstract graph and to the affected
conversion maps and afterwards calls itself with the remaining node
list -}
convertNodesAux :: GA.GraphInfo -> LNode DGNodeLab -> IO ()
convertNodesAux ginfo (node, dgnode) =
GA.addNode ginfo node (getRealDGNodeType dgnode) $ getDGNodeName dgnode
{- | converts the edges of the development graph
works the same way as convertNods does-}
convertEdges :: GA.GraphInfo -> DGraph -> IO ()
convertEdges ginfo = mapM_ (convertEdgesAux ginfo) . labEdgesDG
-- | auxiliary function for convertEges
convertEdgesAux :: GA.GraphInfo -> LEdge DGLinkLab -> IO ()
convertEdgesAux ginfo e@(src, tar, lbl) =
GA.addEdge ginfo (dgl_id lbl) (getRealDGLinkType lbl) src tar "" $ Just e
-- | show library referened by a DGRef node (=node drawn as a box)
showReferencedLibrary :: Int -> GInfo -> ConvFunc -> LibFunc -> IO ()
showReferencedLibrary descr gInfo@(GInfo{ libName = ln })
convGraph showLib = do
ost <- readIORef $ intState gInfo
case i_state ost of
Nothing -> return ()
Just ist -> do
let le = i_libEnv ist
refNode = labDG (lookupDGraph ln le) descr
refLibname = if isDGRef refNode then dgn_libname refNode
else error "showReferencedLibrary"
case Map.lookup refLibname le of
Just _ -> do
gInfo' <- copyGInfo gInfo refLibname
convGraph gInfo' "development graph" showLib
let gi = graphInfo gInfo'
GA.deactivateGraphWindow gi
hideNodes gInfo'
GA.redisplay gi
GA.layoutImproveAll gi
GA.showTemporaryMessage gi "Development Graph initialized."
GA.activateGraphWindow gi
return ()
Nothing -> error $ "The referenced library (" ++ show refLibname
++ ") is unknown"
-- | apply the changes of first history item (computed by proof rules,
-- see folder Proofs) to the displayed development graph
applyChanges :: GA.GraphInfo -> [DGChange] -> IO ()
applyChanges ginfo = mapM_ (applyChangesAux ginfo) . removeContraryChanges
-- | auxiliary function for applyChanges
applyChangesAux :: GA.GraphInfo -> DGChange -> IO ()
applyChangesAux ginfo change =
case change of
SetNodeLab _ (node, newLab) ->
GA.changeNodeType ginfo node $ getRealDGNodeType newLab
InsertNode (node, nodelab) ->
GA.addNode ginfo node (getRealDGNodeType nodelab) $ getDGNodeName nodelab
DeleteNode (node, _) ->
GA.delNode ginfo node
InsertEdge e@(src, tgt, lbl) ->
GA.addEdge ginfo (dgl_id lbl) (getRealDGLinkType lbl) src tgt "" $ Just e
DeleteEdge (_, _, lbl) ->
GA.delEdge ginfo $ dgl_id lbl
-- | display a window of translated graph with maximal sublogic.
translateGraph :: GInfo -> IO (Maybe LibEnv)
translateGraph gInfo@(GInfo { hetcatsOpts = opts }) = do
ost <- readIORef $ intState gInfo
case i_state ost of
Nothing -> return Nothing
Just ist -> do
let
le = i_libEnv ist
Result diagsSl mSublogic = getDGLogic le
myErrMess = showDiagMess opts
error' = errorDialog "Error"
if hasErrors diagsSl then do
myErrMess diagsSl
return Nothing
else case mSublogic of
Nothing -> do
error' "No maximal sublogic found."
return Nothing
Just sublogic -> do
let paths = findComorphismPaths logicGraph sublogic
if null paths then do
error' "This graph has no comorphism to translation."
return Nothing
else do
sel <- listBox "Choose a logic translation" $ map show paths
case sel of
Nothing -> do
error' "no logic translation chosen"
return Nothing
Just j -> do
let Result diag mle = libEnv_translation le $ paths !! j
case mle of
Just newLibEnv -> do
showDiagMess opts $ diagsSl ++ diag
return $ Just newLibEnv
Nothing -> do
myErrMess $ diagsSl ++ diag
return Nothing
-- DaVinciGraph to String
-- Functions to convert a DaVinciGraph to a String to store as a .udg file
-- | saves the uDrawGraph graph to a file
saveUDGraph :: GInfo -> Map.Map DGNodeType (Shape value, String)
-> Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String) -> IO ()
saveUDGraph gInfo@(GInfo { graphInfo = gi
, hetcatsOpts = opts
, libName = ln }) nodemap linkmap = do
ost <- readIORef $ intState gInfo
case i_state ost of
Nothing -> return ()
Just _ -> do
maybeFilePath <- fileSaveDialog ((rmSuffix $ libNameToFile opts ln)
++ ".udg")
[ ("uDrawGraph",["*.udg"])
, ("All Files", ["*"])] Nothing
case maybeFilePath of
Just filepath -> do
GA.showTemporaryMessage gi "Converting graph..."
nstring <- nodes2String gInfo nodemap linkmap
writeFile filepath nstring
GA.showTemporaryMessage gi $ "Graph stored to " ++ filepath ++ "!"
Nothing -> GA.showTemporaryMessage gi "Aborted!"
-- | Converts the nodes of the graph to String representation
nodes2String :: GInfo -> Map.Map DGNodeType (Shape value, String)
-> Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String)
-> IO String
nodes2String gInfo@(GInfo { graphInfo = gi
, libName = ln }) nodemap linkmap = do
ost <- readIORef $ intState gInfo
case i_state ost of
Nothing -> return []
Just ist -> do
let le = i_libEnv ist
nodes <- filterM (\(n,_) -> do b <- GA.isHiddenNode gi n
return $ not b)
$ labNodesDG $ lookupDGraph ln le
nstring <- foldM (\s node -> do
s' <- (node2String gInfo nodemap linkmap node)
return $ s ++ (if s /= "" then ",\n " else "") ++ s')
"" nodes
return $ "[" ++ nstring ++ "]"
-- | Converts a node to String representation
node2String :: GInfo -> Map.Map DGNodeType (Shape value, String)
-> Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String)
-> LNode DGNodeLab -> IO String
node2String gInfo nodemap linkmap (nid, dgnode) = do
label <- getNodeLabel gInfo dgnode
let ntype = getRealDGNodeType dgnode
(shape, color) <- case Map.lookup ntype nodemap of
Nothing -> error $ "SaveGraph: can't lookup nodetype: " ++ show ntype
Just (s, c) -> return (s, c)
let
object = "a(\"OBJECT\",\"" ++ label ++ "\"),"
color' = "a(\"COLOR\",\"" ++ color ++ "\"),"
shape' = "a(\"_GO\",\"" ++ map toLower (show shape) ++ "\")"
links <- links2String gInfo linkmap nid
return $ "l(\"" ++ show nid ++ "\",n(\"" ++ show ntype ++ "\","
++ "[" ++ object ++ color' ++ shape' ++ "],"
++ "\n [" ++ links ++ "]))"
-- | Converts all links of a node to String representation
links2String :: GInfo -> Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String)
-> Int -> IO String
links2String gInfo@(GInfo { graphInfo = gi
, libName = ln }) linkmap nodeid = do
ost <- readIORef $ intState gInfo
case i_state ost of
Nothing -> return []
Just ist -> do
let le = i_libEnv ist
edges <- filterM (\ (src, _, edge) -> do
let eid = dgl_id edge
b <- GA.isHiddenEdge gi eid
return $ not b && src == nodeid)
$ labEdgesDG $ lookupDGraph ln le
foldM (\ s edge -> do
s' <- link2String linkmap edge
return $ s ++ (if s /= "" then ",\n " else "") ++ s') "" edges
-- | Converts a link to String representation
link2String :: Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String)
-> LEdge DGLinkLab -> IO String
link2String linkmap (nodeid1, nodeid2, edge) = do
let (EdgeId linkid) = dgl_id edge
ltype = getRealDGLinkType edge
(line, color) <- case Map.lookup ltype linkmap of
Nothing -> error $ "SaveGraph: can't lookup linktype: " ++ show ltype
Just (l, c) -> return (l, c)
let
nm = "\"" ++ show linkid ++ ":" ++ show nodeid1 ++ "->"
++ show nodeid2 ++ "\""
color' = "a(\"EDGECOLOR\",\"" ++ color ++ "\"),"
line' = "a(\"EDGEPATTERN\",\"" ++ map toLower (show line) ++ "\")"
return $ "l(" ++ nm ++ ",e(\"" ++ show ltype ++ "\","
++ "[" ++ color' ++ line' ++"],"
++ "r(\"" ++ show nodeid2 ++ "\")))"
-- | Returns the name of the Node
getNodeLabel :: GInfo -> DGNodeLab -> IO String
getNodeLabel (GInfo {internalNamesIORef = ioRefInternal}) dgnode = do
internal <- readIORef ioRefInternal
let ntype = getDGNodeType dgnode
return $ if (not $ showNames internal) &&
elem ntype ["open_cons__internal"
, "proven_cons__internal"
, "locallyEmpty__open_cons__internal"
, "locallyEmpty__proven_cons__internal"]
then "" else getDGNodeName dgnode