GraphLogic.hs revision 2028dc2c091bb60343e15985948a59b955276cbf
beff4152e9f0fe90885458d1a1733b183a2a8816Christian MaederModule : $Header$
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederDescription : Logic for manipulating the graph in the Central GUI
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiCopyright : (c) Jorina Freya Gerken, Till Mossakowski, Uni Bremen 2002-2006
2725abe920f91de62ae5c0b7230c1627cccf5fabChristian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederMaintainer : till@informatik.uni-bremen.de
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederStability : provisional
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederPortability : non-portable (imports Logic)
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederThis module provides functions for all the menus in the Hets GUI.
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederThese are then assembled to the GUI in "GUI.GraphMenu".
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , performProofAction
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , openProofStatus
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , saveProofStatus
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , openTranslateGraph
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , showReferencedLibrary
85e1d54a475bfc30b3eac5ae6c5e42a2d7e93f10Christian Maeder , getTheoryOfNode
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , translateTheoryOfNode
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , displaySubsortGraph
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , displayConceptGraph
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , lookupTheoryOfNode
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , showProofStatusOfNode
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , proveAtNode
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , showNodeInfo
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , showEdgeInfo
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , checkconservativityOfEdge
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , hideShowNames
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , translateGraph
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , showLibGraph
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , saveUDGraph
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , applyChanges
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder , applyTypeChanges
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport Logic.Logic(conservativityCheck)
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maederimport Logic.Coerce(coerceSign, coerceMorphism)
9d6562465b41f17c7967d4e5678f34811d958cb2Christian Maederimport Syntax.AS_Library(LIB_NAME, getModTime, getLIB_ID)
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maederimport Static.DGToSpec(dgToSpec, computeTheory)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport Static.AnalysisLibrary(anaLibExt, anaLib)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport Static.DGTranslation(libEnv_translation)
38c817b94e0a5b1ae94178b1075c187e07bcc5e1Christian Maederimport Proofs.InferBasic(basicInferenceNode)
38c817b94e0a5b1ae94178b1075c187e07bcc5e1Christian Maederimport Proofs.StatusUtils(lookupHistory, removeContraryChanges)
2353f65833a3da763392f771223250cd50b8d873Christian Maederimport GUI.Utils (listBox)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport GUI.Taxonomy (displayConceptGraph,displaySubsortGraph)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport GUI.DGTranslation(getDGLogic)
cb2044812811d66efe038d914966e04290be93faChristian Maederimport qualified GUI.GraphAbstraction as GA
bc263f610d20a9cd3014ddfca903026127fa0d48Christian Maederimport qualified GUI.HTkUtils (displayTheoryWithWarning,
8c8545dd3bf34fbcbc16904b65d249658f8f9efcChristian Maeder createInfoDisplayWithTwoButtons)
d81905a5b924415c524d702df26204683c82c12eChristian Maederimport GraphConfigure
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport TextDisplay(createTextDisplay)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport InfoBus(encapsulateWaitTermAct)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport DialogWin (useHTk)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport Messages(errorMess)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport qualified HTk
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport Configuration(size)
cb2044812811d66efe038d914966e04290be93faChristian Maederimport FileDialog(newFileDialogStr)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport Common.DocUtils(showDoc, pretty)
0ae7a79e865d4a6022d705d160530682b3c1f825Christian Maederimport Common.ResultT(liftR, runResultT)
fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan Pascanuimport qualified Common.OrderedMap as OMap
b324cda6178c49ddeead3ce62b832ccf644cbcabRazvan Pascanuimport qualified Common.Lib.Rel as Rel
966519955f5f7111abac20118563132b9dd41165Christian Maederimport Driver.WriteFn(writeShATermFile)
8c8545dd3bf34fbcbc16904b65d249658f8f9efcChristian Maederimport Driver.ReadFn(libNameToFile, readVerbose)
33fcc19ef2b59493b4e91eebf701df95fd230765Christian Maederimport System.Directory(getModificationTime)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport Data.Maybe(fromJust)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport Data.List(find, delete, partition)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport Data.Graph.Inductive.Graph (Node, LEdge, LNode)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport qualified Data.Map as Map
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport Control.Monad(foldM, filterM)
fdac680252d7347858bd67b4c2a2aaa52e623815Christian Maeder-- | Locks the global lock and runs function
fdac680252d7347858bd67b4c2a2aaa52e623815Christian MaederrunAndLock :: GInfo -> IO () -> IO ()
a9e804dbec424ec36e34bab955cbe90edac5baa6Christian MaederrunAndLock (GInfo { functionLock = lock
f8cc2399c16fcda7e3bf9d901a0de0cc8a455f86Ewaryst Schulz , gi_GraphInfo = actGraph
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder }) function = do
b76d27eba526ecac2a20400fa505ec5c642ae7d2Dominik Luecke locked <- tryPutMVar lock ()
b76d27eba526ecac2a20400fa505ec5c642ae7d2Dominik Luecke case locked of
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus Luettich takeMVar lock
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder GA.showTemporaryMessage actGraph $ "an other function is still working"
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder ++ "... please wait ..."
2353f65833a3da763392f771223250cd50b8d873Christian Maeder-- | negate change
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedernegateChange :: DGChange -> DGChange
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedernegateChange change = case change of
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder InsertNode x -> DeleteNode x
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder DeleteNode x -> InsertNode x
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder InsertEdge x -> DeleteEdge x
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder DeleteEdge x -> InsertEdge x
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder SetNodeLab old (node, new) -> SetNodeLab new (node, old)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- | Undo one step of the History
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maederundo :: GInfo -> Bool -> IO ()
00df6fd583c19393fa141d5a0e21ac74c7bf5b19Christian Maederundo gInfo@(GInfo { globalHist = gHist
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder , gi_GraphInfo = actGraph
cb2044812811d66efe038d914966e04290be93faChristian Maeder }) isUndo = do
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder (guHist, grHist) <- takeMVar gHist
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder case if isUndo then guHist else grHist of
8d780c893d6df5dab3dcc7d8444b7517f6547f11Christian Maeder GA.showTemporaryMessage actGraph "History is empty..."
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder putMVar gHist (guHist, grHist)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder (lns:gHist') -> do
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder undoDGraphs gInfo isUndo lns
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder putMVar gHist $ if isUndo then (gHist', reverse lns : grHist)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder else (reverse lns : guHist, gHist')
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaederundoDGraphs :: GInfo -> Bool -> [LIB_NAME] -> IO ()
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaederundoDGraphs _ _ [] = return ()
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaederundoDGraphs g u (ln:r) = do
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder undoDGraph g u ln
bc263f610d20a9cd3014ddfca903026127fa0d48Christian Maeder undoDGraphs g u r
bbba6dd86153aacb0f662b182b128df0eb09fd54Christian MaederundoDGraph :: GInfo -> Bool -> LIB_NAME -> IO ()
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian MaederundoDGraph gInfo@(GInfo { libEnvIORef = ioRefProofStatus
d96bfd1d7a4595bfff87771b91797330fa939455Christian Maeder , gi_GraphInfo = actGraph
d96bfd1d7a4595bfff87771b91797330fa939455Christian Maeder }) isUndo ln = do
8c8545dd3bf34fbcbc16904b65d249658f8f9efcChristian Maeder GA.showTemporaryMessage actGraph $ "Undo last change to " ++ show ln ++ "..."
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder lockGlobal gInfo
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder le <- readIORef ioRefProofStatus
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder dg = lookupDGraph ln le
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder hist = (proofHistory dg, redoHistory dg)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder swap (a, b) = (b, a)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder (phist, rhist) = (if isUndo then id else swap) hist
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder (cl@(rs, cs), newHist) = case phist of
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder hd : tl -> (hd, (tl, hd : rhist))
2360728d4185c0c04279c999941c64d36626af79Christian Maeder _ -> error "undoDGraph"
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder (newPHist, newRHist) = (if isUndo then id else swap) newHist
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder change = if isUndo then (reverse rs, reverse $ map negateChange cs)
2360728d4185c0c04279c999941c64d36626af79Christian Maeder dg' = (changesDG dg $ snd change)
2360728d4185c0c04279c999941c64d36626af79Christian Maeder { proofHistory = newPHist
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder , redoHistory = newRHist }
2360728d4185c0c04279c999941c64d36626af79Christian Maeder writeIORef ioRefProofStatus $ Map.insert ln dg' le
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder case openlock dg' of
8d780c893d6df5dab3dcc7d8444b7517f6547f11Christian Maeder Nothing -> return ()
2360728d4185c0c04279c999941c64d36626af79Christian Maeder Just lock -> do
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder mvar <- tryTakeMVar lock
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder Nothing -> return ()
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder Just applyHist -> do
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder applyHist [change]
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder putMVar lock applyHist
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder unlockGlobal gInfo
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- | reloads the Library of the DevGraph
bc263f610d20a9cd3014ddfca903026127fa0d48Christian Maederreload :: GInfo -> IO()
966519955f5f7111abac20118563132b9dd41165Christian Maederreload gInfo@(GInfo { libEnvIORef = ioRefProofStatus
bbba6dd86153aacb0f662b182b128df0eb09fd54Christian Maeder , gi_LIB_NAME = ln
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder , gi_hetcatsOpts = opts
8c8545dd3bf34fbcbc16904b65d249658f8f9efcChristian Maeder lockGlobal gInfo
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder oldle <- readIORef ioRefProofStatus
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder libdeps = Rel.toList $ Rel.intransKernel $ Rel.transClosure $ Rel.fromList
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder $ getLibDeps oldle
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder ioruplibs <- newIORef ([] :: [LIB_NAME])
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder writeIORef ioruplibs []
bbba6dd86153aacb0f662b182b128df0eb09fd54Christian Maeder reloadLibs ioRefProofStatus opts libdeps ioruplibs ln
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder unlockGlobal gInfo
cb2044812811d66efe038d914966e04290be93faChristian Maeder remakeGraph gInfo
bbba6dd86153aacb0f662b182b128df0eb09fd54Christian Maeder-- | Creates a list of all LIB_NAME pairs, which have a dependency
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaedergetLibDeps :: LibEnv -> [(LIB_NAME, LIB_NAME)]
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaedergetLibDeps le =
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder concat $ map (\ ln -> getDep ln le) $ Map.keys le
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder-- | Creates a list of LIB_NAME pairs for the fist argument
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian MaedergetDep :: LIB_NAME -> LibEnv -> [(LIB_NAME, LIB_NAME)]
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian MaedergetDep ln le = map (\ (_, x) -> (ln, dgn_libname x)) $
8c8545dd3bf34fbcbc16904b65d249658f8f9efcChristian Maeder filter (isDGRef . snd) $ labNodesDG $ lookupDGraph ln le
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- | Reloads a library
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaederreloadLib :: IORef LibEnv -> HetcatsOpts -> IORef [LIB_NAME] -> LIB_NAME
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaederreloadLib iorle opts ioruplibs ln = do
bc263f610d20a9cd3014ddfca903026127fa0d48Christian Maeder mfile <- existsAnSource opts {intype = GuessIn}
966519955f5f7111abac20118563132b9dd41165Christian Maeder $ rmSuffix $ libNameToFile opts ln
8bb80c9684e905de8dcfcfb1291542677e7d77b6Christian Maeder case mfile of
8bb80c9684e905de8dcfcfb1291542677e7d77b6Christian Maeder Nothing -> do
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder Just file -> do
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder le <- readIORef iorle
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder mres <- anaLibExt opts file le'
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder Just (_, newle) -> do
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder uplibs <- readIORef ioruplibs
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder writeIORef ioruplibs $ ln:uplibs
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder writeIORef iorle newle
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder Nothing -> do
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder errorMess $ "Could not read original development graph from '"++ file
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- | Reloads libraries if nessesary
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaederreloadLibs :: IORef LibEnv -> HetcatsOpts -> [(LIB_NAME, LIB_NAME)]
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder -> IORef [LIB_NAME] -> LIB_NAME -> IO Bool
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaederreloadLibs iorle opts deps ioruplibs ln = do
cb2044812811d66efe038d914966e04290be93faChristian Maeder uplibs <- readIORef ioruplibs
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder case elem ln uplibs of
8d780c893d6df5dab3dcc7d8444b7517f6547f11Christian Maeder True -> return True
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder deps' = map (snd) $ filter (\ (ln',_) -> ln == ln') deps
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder res <- mapM (reloadLibs iorle opts deps ioruplibs) deps'
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder libupdate = foldl (\ u r -> if r then True else u) False res
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder case libupdate of
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder reloadLib iorle opts ioruplibs ln
8c8545dd3bf34fbcbc16904b65d249658f8f9efcChristian Maeder le <- readIORef iorle
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder newln:_ = filter (ln ==) $ Map.keys le
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder mfile <- existsAnSource opts $ rmSuffix $ libNameToFile opts ln
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder case mfile of
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder Nothing -> do
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian Maeder Just file -> do
12aef5992d3af07dee81a4e02cf4be65a83f28bcChristian Maeder newmt <- getModificationTime file
2360728d4185c0c04279c999941c64d36626af79Christian Maeder libupdate' = (getModTime $ getLIB_ID newln) < newmt
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder case libupdate' of
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian Maeder False -> return False
2360728d4185c0c04279c999941c64d36626af79Christian Maeder reloadLib iorle opts ioruplibs ln
2360728d4185c0c04279c999941c64d36626af79Christian Maeder-- | Deletes the old edges and nodes of the Graph and makes new ones
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian MaederremakeGraph :: GInfo -> IO ()
8d780c893d6df5dab3dcc7d8444b7517f6547f11Christian MaederremakeGraph (GInfo { libEnvIORef = ioRefProofStatus
2360728d4185c0c04279c999941c64d36626af79Christian Maeder , gi_LIB_NAME = ln
bc263f610d20a9cd3014ddfca903026127fa0d48Christian Maeder , gi_GraphInfo = actGraphInfo
2360728d4185c0c04279c999941c64d36626af79Christian Maeder le <- readIORef ioRefProofStatus
00df6fd583c19393fa141d5a0e21ac74c7bf5b19Christian Maeder dgraph = lookupDGraph ln le
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian Maeder convert actGraphInfo dgraph
2360728d4185c0c04279c999941c64d36626af79Christian Maeder-- | Toggles to display internal node names
2360728d4185c0c04279c999941c64d36626af79Christian MaederhideShowNames :: GInfo -> Bool -> IO ()
2360728d4185c0c04279c999941c64d36626af79Christian MaederhideShowNames (GInfo { gi_GraphInfo = actGraphInfo
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder , internalNamesIORef = showInternalNames
8994ef587ce7c7c39ddd20f0f7e4575838a6694aChristian Maeder }) toggle = do
2360728d4185c0c04279c999941c64d36626af79Christian Maeder (intrn::InternalNames) <- readIORef showInternalNames
2360728d4185c0c04279c999941c64d36626af79Christian Maeder let showThem = if toggle then not $ showNames intrn else showNames intrn
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder showItrn s = if showThem then s else ""
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder mapM_ (\(s,upd) -> upd (\_ -> showItrn s)) $ updater intrn
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder writeIORef showInternalNames $ intrn {showNames = showThem}
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- | shows all hidden nodes and edges
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaedershowNodes :: GInfo -> IO ()
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaedershowNodes gInfo@(GInfo { gi_GraphInfo = actGraphInfo
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder hhn <- GA.hasHiddenNodes actGraphInfo
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder GA.showTemporaryMessage actGraphInfo "Revealing hidden nodes ..."
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder hideShowNames gInfo False
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder GA.showTemporaryMessage actGraphInfo "No hidden nodes found ..."
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- | hides all unnamed internal nodes that are proven
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaederhideNodes :: GInfo -> IO ()
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaederhideNodes (GInfo { libEnvIORef = ioRefProofStatus
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder , gi_LIB_NAME = ln
76d027be764e2ff61bef959efb3ac8f56499e646Christian Maeder , gi_GraphInfo = actGraphInfo
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder hhn <- GA.hasHiddenNodes actGraphInfo
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder GA.showTemporaryMessage actGraphInfo "Nodes already hidden ..."
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc GA.showTemporaryMessage actGraphInfo "Hiding unnamed nodes..."
d95f77e19ae3835318a6340d872193fbb3cbab05Karl Luc le <- readIORef ioRefProofStatus
26b1c101b72100b69045effdfaab3889de6c8c93Christian Maeder let dg = lookupDGraph ln le
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder nodes = selectNodesByType dg [LocallyEmptyProvenConsInternal]
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder edges = getCompressedEdges dg nodes
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder GA.hideNodes actGraphInfo nodes edges
2360728d4185c0c04279c999941c64d36626af79Christian Maeder-- | selects all nodes of a type with outgoing edges
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaederselectNodesByType :: DGraph -> [DGNodeType] -> [Node]
63da71bfb4226f504944b293fb77177ebcaea7d4Ewaryst SchulzselectNodesByType dg types =
76d027be764e2ff61bef959efb3ac8f56499e646Christian Maeder filter (\ n -> outDG dg n /= []) $ map fst
9f85afecbd79b3df5a0bb17bd28cd0b288dc3213Kristina Sojakova $ filter (\ (_, n) -> elem (getRealDGNodeType n) types) $ labNodesDG dg
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- | compresses a list of types to the highest one
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaedercompressTypes :: [DGEdgeType] -> DGEdgeType
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaedercompressTypes [] = error "compressTypes: wrong usage"
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaedercompressTypes (t:[]) = t
af6e92e4a9ca308f928f9909acee115f801c5db5Ewaryst SchulzcompressTypes (t1:t2:r) = case t1 > t2 of
4692b8b63985ab174478d389e20a544054e09ce8Karl Luc True -> compressTypes (t1:r)
d95f77e19ae3835318a6340d872193fbb3cbab05Karl Luc False -> compressTypes (t2:r)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | returns a list of compressed edges
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedergetCompressedEdges :: DGraph -> [Node] -> [(Node,Node,DGEdgeType)]
2353f65833a3da763392f771223250cd50b8d873Christian MaedergetCompressedEdges dg hidden =
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder filterDuplicates $ getShortPaths $ concat
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder $ map (\ e@(_,t,_) -> map (e:) $ getPaths dg t hidden [])
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder inEdges = filter (\ (_,t,_) -> elem t hidden)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder $ concat $ map (outDG dg)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder $ foldr (\ n i -> if elem n hidden
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder || elem n i then i else n:i) []
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder $ map (\ (s,_,_) -> s) $ concat $ map (innDG dg) hidden
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- | filter duplicate paths
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaederfilterDuplicates :: [(Node,Node,DGEdgeType)]
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder -> [(Node,Node,DGEdgeType)]
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederfilterDuplicates [] = []
12aef5992d3af07dee81a4e02cf4be65a83f28bcChristian MaederfilterDuplicates ((s,t,et):r) = edge:filterDuplicates others
26b1c101b72100b69045effdfaab3889de6c8c93Christian Maeder (same,others) = partition (\ (s',t',_) -> s == s' && t == t') r
af6e92e4a9ca308f928f9909acee115f801c5db5Ewaryst Schulz edge = (s,t,compressTypes $ et:map (\ (_,_,et') -> et') same)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | returns the pahts of a given node through hidden nodes
818b228955ef40dd5a253bd942dd6ab8779ed713Christian MaedergetPaths :: DGraph -> Node -> [Node] -> [Node] -> [[LEdge DGLinkLab]]
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedergetPaths dg node hidden seen' = case elem node hidden of
7ebcceae3d34771cae3bbb8c8060bef0b894376eChristian Maeder True -> case edges /= [] of
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus Luettich True -> concat $ map (\ e@(_,t,_) -> map (e:) $ getPaths dg t hidden seen)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder False -> [[]]
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus Luettich seen = node:seen'
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus Luettich edges = filter (\ (_,t,_) -> notElem t seen) $ outDG dg node
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus Luettich-- | returns source and target node of a path with the compressed type
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedergetShortPaths :: [[LEdge DGLinkLab]]
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder -> [(Node,Node,DGEdgeType)]
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaedergetShortPaths [] = []
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaedergetShortPaths (p:r) =
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder ((s,t,compressTypes $ map (\ (_,_,e) -> getRealDGLinkType e) p))
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder : getShortPaths r
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder (s,_,_) = head p
bc263f610d20a9cd3014ddfca903026127fa0d48Christian Maeder (_,t,_) = last p
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- | Let the user select a Node to focus
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaederfocusNode :: GInfo -> IO ()
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaederfocusNode (GInfo { libEnvIORef = ioRefProofStatus
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder , gi_LIB_NAME = ln
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder ,gi_GraphInfo = grInfo
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder le <- readIORef ioRefProofStatus
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder idsnodes <- filterM (\(n,_) -> do b <- GA.isHiddenNode grInfo n
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder return $ not b)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder $ labNodesDG $ lookupDGraph ln le
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder let (ids,nodes) = unzip idsnodes
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder let nodes' = map (getDGNodeName) nodes
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder selection <- listBox "Select a node to focus" nodes'
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder case selection of
df86c42574168135e8e2af9cf468fae774874cd0Christian Maeder Just idx -> GA.focusNode grInfo $ ids !! idx
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder Nothing -> return ()
f8cc2399c16fcda7e3bf9d901a0de0cc8a455f86Ewaryst SchulztranslateGraph :: GInfo -> ConvFunc -> LibFunc -> IO ()
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaedertranslateGraph (GInfo {libEnvIORef = ioRefProofStatus,
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder gi_LIB_NAME = ln,
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder gi_hetcatsOpts = opts
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder }) convGraph showLib = do
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder le <- readIORef ioRefProofStatus
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder openTranslateGraph le ln opts (getDGLogic le) convGraph showLib
3490b73f69b58ab742417b0867d0e2d4a7778cc0Christian MaedershowLibGraph :: GInfo -> LibFunc -> IO ()
3490b73f69b58ab742417b0867d0e2d4a7778cc0Christian MaedershowLibGraph gInfo showLib = do
59aa5703ac7f3b99e97cd5926e77088b256c5f40Christian Maeder showLib gInfo
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder{- | it tries to perform the given action to the given graph.
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder If part of the given graph is not hidden, then the action can
7968d3a131e5a684ec1ff0c6d88aae638549153dChristian Maeder be performed directly; otherwise the graph will be shown completely
3490b73f69b58ab742417b0867d0e2d4a7778cc0Christian Maeder firstly, and then the action will be performed, and after that the graph
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder will be hidden again.
beff4152e9f0fe90885458d1a1733b183a2a8816Christian MaederperformProofAction :: GInfo -> IO () -> IO ()
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus LuettichperformProofAction gInfo@(GInfo { gi_GraphInfo = actGraphInfo
b76d27eba526ecac2a20400fa505ec5c642ae7d2Dominik Luecke }) proofAction = do
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder let actionWithMessage = do
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder "Applying development graph calculus proof rule..."
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder hhn <- GA.hasHiddenNodes actGraphInfo
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder showNodes gInfo
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder actionWithMessage
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder hideNodes gInfo
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder False -> actionWithMessage
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder "Development graph calculus proof rule finished."
511284753313165e629cedf508752d6818ccc4d2Christian MaedersaveProofStatus :: GInfo -> FilePath -> IO ()
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedersaveProofStatus (GInfo { libEnvIORef = ioRefProofStatus
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder , gi_LIB_NAME = ln
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder , gi_hetcatsOpts = opts
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder }) file = encapsulateWaitTermAct $ do
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder proofStatus <- readIORef ioRefProofStatus
bc263f610d20a9cd3014ddfca903026127fa0d48Christian Maeder writeShATermFile file (ln, lookupHistory ln proofStatus)
511284753313165e629cedf508752d6818ccc4d2Christian Maeder putIfVerbose opts 2 $ "Wrote " ++ file
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | implementation of open menu, read in a proof status
511284753313165e629cedf508752d6818ccc4d2Christian MaederopenProofStatus :: GInfo -> FilePath -> ConvFunc -> LibFunc
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederopenProofStatus gInfo@(GInfo { libEnvIORef = ioRefProofStatus
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder , gi_LIB_NAME = ln
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder , gi_hetcatsOpts = opts
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder }) file convGraph showLib = do
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder mh <- readVerbose opts ln file
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder Nothing -> errorMess $ "Could not read proof status from file '"
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder ++ file ++ "'"
8865728716566f42fa73e7e0bc080ba3225df764Christian Maeder let libfile = libNameToFile opts ln
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder m <- anaLib opts { outtypes = [] } libfile
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder Nothing -> errorMess $ "Could not read original development graph"
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder ++ " from '" ++ libfile ++ "'"
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder Just (_, libEnv) -> case Map.lookup ln libEnv of
f03420e44d8204b2945edaab5c70a84e7c381892Christian Maeder Nothing -> errorMess $ "Could not get original development"
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder ++ " graph for '" ++ showDoc ln "'"
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder Just dg -> do
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder lockGlobal gInfo
8bb80c9684e905de8dcfcfb1291542677e7d77b6Christian Maeder oldEnv <- readIORef ioRefProofStatus
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder let proofStatus = Map.insert ln
91ba5d95b2472cb075646b6120a559dc6581a867Christian Maeder (applyProofHistory h dg) oldEnv
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder writeIORef ioRefProofStatus proofStatus
91ba5d95b2472cb075646b6120a559dc6581a867Christian Maeder unlockGlobal gInfo
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder gInfo' <- copyGInfo gInfo ln
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder convGraph gInfo' "Proof Status " showLib
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder GA.redisplay $ gi_GraphInfo gInfo'
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder-- | apply a rule of the development graph calculus
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian MaederproofMenu :: GInfo
91ba5d95b2472cb075646b6120a559dc6581a867Christian Maeder -> (LibEnv -> IO (Res.Result LibEnv))
91ba5d95b2472cb075646b6120a559dc6581a867Christian MaederproofMenu gInfo@(GInfo { libEnvIORef = ioRefProofStatus
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder , gi_LIB_NAME = ln
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder , gi_GraphInfo = actGraphInfo
f03420e44d8204b2945edaab5c70a84e7c381892Christian Maeder , gi_hetcatsOpts = hOpts
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder , proofGUIMVar = guiMVar
91ba5d95b2472cb075646b6120a559dc6581a867Christian Maeder , globalHist = gHist
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder }) proofFun = do
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder filled <- tryPutMVar guiMVar Nothing
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder if not filled
91ba5d95b2472cb075646b6120a559dc6581a867Christian Maeder then readMVar guiMVar >>=
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder (maybe (putIfVerbose hOpts 0 "proofMenu: ignored Nothing")
f03420e44d8204b2945edaab5c70a84e7c381892Christian Maeder putIfVerbose hOpts 4 $
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder "proofMenu: Ignored Proof command; " ++
d81905a5b924415c524d702df26204683c82c12eChristian Maeder "maybe a proof window is still open?"
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder lockGlobal gInfo
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder proofStatus <- readIORef ioRefProofStatus
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder putIfVerbose hOpts 4 "Proof started via \"Proofs\" menu"
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder Res.Result ds res <- proofFun proofStatus
f03420e44d8204b2945edaab5c70a84e7c381892Christian Maeder putIfVerbose hOpts 4 "Analyzing result of proof"
f03420e44d8204b2945edaab5c70a84e7c381892Christian Maeder Nothing -> do
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder unlockGlobal gInfo
91ba5d95b2472cb075646b6120a559dc6581a867Christian Maeder mapM_ (putStrLn . show) ds
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder Just newProofStatus -> do
f03420e44d8204b2945edaab5c70a84e7c381892Christian Maeder let newGr = lookupDGraph ln newProofStatus
f03420e44d8204b2945edaab5c70a84e7c381892Christian Maeder history = proofHistory newGr
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder (guHist, grHist) <- takeMVar gHist
818b228955ef40dd5a253bd942dd6ab8779ed713Christian Maeder doDump hOpts "PrintHistory" $ do
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder putStrLn "History"
bbba6dd86153aacb0f662b182b128df0eb09fd54Christian Maeder print $ prettyHistory history
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder putMVar gHist
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder (calcGlobalHistory proofStatus newProofStatus : guHist, grHist)
8c8545dd3bf34fbcbc16904b65d249658f8f9efcChristian Maeder applyChanges actGraphInfo history
33fcc19ef2b59493b4e91eebf701df95fd230765Christian Maeder applyTypeChanges actGraphInfo newGr
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder writeIORef ioRefProofStatus newProofStatus
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder unlockGlobal gInfo
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder hideShowNames gInfo False
4a2f7efdf67dfcda0946f1b6373f41976ddea7a4Christian Maeder mGUIMVar <- tryTakeMVar guiMVar
3490b73f69b58ab742417b0867d0e2d4a7778cc0Christian Maeder maybe (fail $ "should be filled with Nothing after proof attempt")
3490b73f69b58ab742417b0867d0e2d4a7778cc0Christian Maeder (const $ return ())
3490b73f69b58ab742417b0867d0e2d4a7778cc0Christian MaedercalcGlobalHistory :: LibEnv -> LibEnv -> [LIB_NAME]
beff4152e9f0fe90885458d1a1733b183a2a8816Christian MaedercalcGlobalHistory old new = let
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder pHist = (\ ln le -> proofHistory $ lookupDGraph ln le)
ab2f38d9cd1249f6bc9cc5b838dc2fcd76189c0fChristian Maeder length' = (\ ln le -> length $ pHist ln le)
974b0baababf2878820de073b8fad8db68bef08aDominik Luecke changes = filter (\ ln -> pHist ln old /= pHist ln new) $ Map.keys old
8d780c893d6df5dab3dcc7d8444b7517f6547f11Christian Maeder in concatMap (\ ln -> replicate (length' ln new - length' ln old) ln) changes
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian MaedernodeErr :: Int -> IO ()
083bc1972a66d73749760eab3a90bf4eb9ca7951Christian MaedernodeErr descr = error $ "node with descriptor " ++ show descr
bc263f610d20a9cd3014ddfca903026127fa0d48Christian Maeder ++ " has no corresponding node in the development graph"
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian MaedershowSpec :: Int -> DGraph -> IO ()
966519955f5f7111abac20118563132b9dd41165Christian MaedershowSpec descr dgraph = do
00df6fd583c19393fa141d5a0e21ac74c7bf5b19Christian Maeder let sp = dgToSpec dgraph descr
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian Maeder sp' = case sp of
00df6fd583c19393fa141d5a0e21ac74c7bf5b19Christian Maeder Res.Result ds Nothing -> show $ vcat $ map pretty ds
00df6fd583c19393fa141d5a0e21ac74c7bf5b19Christian Maeder Res.Result _ m -> showDoc m ""
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder createTextDisplay "Show spec" sp' [size(80,25)]
f03420e44d8204b2945edaab5c70a84e7c381892Christian MaedershowNodeInfo :: Int -> DGraph -> IO ()
0ae7a79e865d4a6022d705d160530682b3c1f825Christian MaedershowNodeInfo descr dgraph = do
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder let dgnode = labDG dgraph descr
2353f65833a3da763392f771223250cd50b8d873Christian Maeder title = (if isDGRef dgnode then ("reference " ++) else
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder if isInternalNode dgnode then ("internal " ++) else id)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder "node " ++ getDGNodeName dgnode ++ " " ++ show descr
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder createTextDisplay title (title ++ "\n" ++ showDoc dgnode "")
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder fetches the theory from a node inside the IO Monad
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder (added by KL based on code in getTheoryOfNode) -}
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaederlookupTheoryOfNode :: IORef LibEnv -> LIB_NAME -> Int
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder -> IO (Res.Result (Node,G_theory))
2360728d4185c0c04279c999941c64d36626af79Christian MaederlookupTheoryOfNode proofStatusRef ln descr = do
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder libEnv <- readIORef proofStatusRef
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder case (do gth <- computeTheory libEnv ln descr
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder return (descr, gth)) of
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder r -> return r
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder{- | outputs the theory of a node in a window;
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maederused by the node menu defined in initializeGraph-}
fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan PascanugetTheoryOfNode :: GInfo -> Int -> DGraph -> IO ()
fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan PascanugetTheoryOfNode gInfo@(GInfo { gi_LIB_NAME = ln
fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan Pascanu , libEnvIORef = le }) descr dgraph = do
fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan Pascanu r <- lookupTheoryOfNode le ln descr
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder showDiags (gi_hetcatsOpts gInfo) ds
fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan Pascanu (Just (n, gth)) ->
fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan Pascanu "Theory" (getNameOfNode n dgraph)
66a774f13272fde036481edd2298081ab3d04678Razvan Pascanu (addHasInHidingWarning dgraph n)
2360728d4185c0c04279c999941c64d36626af79Christian Maeder _ -> return ()
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder{- | translate the theory of a node in a window;
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maederused by the node menu defined in initializeGraph-}
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian MaedertranslateTheoryOfNode :: GInfo -> Int -> DGraph -> IO ()
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian MaedertranslateTheoryOfNode gInfo@(GInfo {gi_hetcatsOpts = opts})
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder descr dgraph = do
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder libEnv <- readIORef $ libEnvIORef gInfo
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder th <- computeTheory libEnv (gi_LIB_NAME gInfo) descr
9dd71ac51c9a6e72bcb126224f9c64131698b636Christian Maeder return (descr,th) ) of
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder Res.Result [] (Just (node,th)) -> do
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder Res.Result ds _ <- runResultT(
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder do G_theory lid sign _ sens _ <- return th
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder -- find all comorphism paths starting from lid
0ea2cddb8715a770e646895e16b7b8085f49167cChristian Maeder let paths = findComorphismPaths logicGraph (sublogicOfTh th)
0ea2cddb8715a770e646895e16b7b8085f49167cChristian Maeder -- let the user choose one
7245138e91992b96b153b8ac527e263d9dc8ff5bChristian Maeder sel <- lift $ listBox "Choose a logic translation"
7245138e91992b96b153b8ac527e263d9dc8ff5bChristian Maeder (map show paths)
7245138e91992b96b153b8ac527e263d9dc8ff5bChristian Maeder i <- case sel of
7245138e91992b96b153b8ac527e263d9dc8ff5bChristian Maeder Just j -> return j
7245138e91992b96b153b8ac527e263d9dc8ff5bChristian Maeder _ -> liftR $ fail "no logic translation chosen"
0ea2cddb8715a770e646895e16b7b8085f49167cChristian Maeder Comorphism cid <- return (paths!!i)
7968d3a131e5a684ec1ff0c6d88aae638549153dChristian Maeder -- adjust lid's
7968d3a131e5a684ec1ff0c6d88aae638549153dChristian Maeder let lidS = sourceLogic cid
7968d3a131e5a684ec1ff0c6d88aae638549153dChristian Maeder lidT = targetLogic cid
7968d3a131e5a684ec1ff0c6d88aae638549153dChristian Maeder sign' <- coerceSign lid lidS "" sign
a461314c811f4187dff85c8be079a41b2f13f176Christian Maeder sens' <- coerceThSens lid lidS "" sens
a461314c811f4187dff85c8be079a41b2f13f176Christian Maeder -- translate theory along chosen comorphism
a461314c811f4187dff85c8be079a41b2f13f176Christian Maeder (sign'',sens1) <-
a461314c811f4187dff85c8be079a41b2f13f176Christian Maeder liftR $ wrapMapTheory cid (plainSign sign', toNamedList sens')
a461314c811f4187dff85c8be079a41b2f13f176Christian Maeder lift $ GUI.HTkUtils.displayTheoryWithWarning
a461314c811f4187dff85c8be079a41b2f13f176Christian Maeder "Translated Theory" (getNameOfNode node dgraph)
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder (addHasInHidingWarning dgraph node)
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder (G_theory lidT (mkExtSign sign'') startSigId
3bcd9d942601d59dd55a6069d8b2d1c33d7ced0eChristian Maeder (toThSens sens1) startThId)
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder showDiags opts ds
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder Res.Result ds _ -> showDiags opts ds
a461314c811f4187dff85c8be079a41b2f13f176Christian Maeder-- | Show proof status of a node
a461314c811f4187dff85c8be079a41b2f13f176Christian MaedershowProofStatusOfNode :: GInfo -> Int -> DGraph -> IO ()
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian MaedershowProofStatusOfNode _ descr dgraph = do
3bcd9d942601d59dd55a6069d8b2d1c33d7ced0eChristian Maeder let dgnode = labDG dgraph descr
3bcd9d942601d59dd55a6069d8b2d1c33d7ced0eChristian Maeder stat = showStatusAux dgnode
7245138e91992b96b153b8ac527e263d9dc8ff5bChristian Maeder title = "Proof status of node "++showName (dgn_name dgnode)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder createTextDisplay title stat [HTk.size(105,55)]
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian MaedershowStatusAux :: DGNodeLab -> String
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedershowStatusAux dgnode =
9d6562465b41f17c7967d4e5678f34811d958cb2Christian Maeder case dgn_theory dgnode of
9d6562465b41f17c7967d4e5678f34811d958cb2Christian Maeder G_theory _ _ _ sens _ ->
daec53c285f692c56db0cefe16061b46ba602cf0Christian Maeder let goals = OMap.filter (not . isAxiom) sens
daec53c285f692c56db0cefe16061b46ba602cf0Christian Maeder (proven,open) = OMap.partition isProvenSenStatus goals
daec53c285f692c56db0cefe16061b46ba602cf0Christian Maeder consGoal = "\nconservativity of this node"
daec53c285f692c56db0cefe16061b46ba602cf0Christian Maeder in "Proven proof goals:\n"
daec53c285f692c56db0cefe16061b46ba602cf0Christian Maeder ++ showDoc proven ""
daec53c285f692c56db0cefe16061b46ba602cf0Christian Maeder ++ if not $ hasOpenConsStatus True dgnode
daec53c285f692c56db0cefe16061b46ba602cf0Christian Maeder then consGoal
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder ++ "\nOpen proof goals:\n"
daec53c285f692c56db0cefe16061b46ba602cf0Christian Maeder ++ showDoc open ""
daec53c285f692c56db0cefe16061b46ba602cf0Christian Maeder ++ if hasOpenConsStatus False dgnode
daec53c285f692c56db0cefe16061b46ba602cf0Christian Maeder then consGoal
daec53c285f692c56db0cefe16061b46ba602cf0Christian Maeder-- | start local theorem proving or consistency checking at a node
daec53c285f692c56db0cefe16061b46ba602cf0Christian MaederproveAtNode :: Bool -> GInfo -> Int -> DGraph -> IO ()
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaederproveAtNode checkCons gInfo@(GInfo { libEnvIORef = ioRefProofStatus
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder , gi_LIB_NAME = ln }) descr dgraph = do
93bc87ee96c68506945dbad8c704badaa42ecf14Christian Maeder let dgn = labDG dgraph descr
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder libNode = (ln,descr)
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder (dgraph',dgn') <- case hasLock dgn of
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder True -> return (dgraph, dgn)
0a64bfd28dff15bc93e1f7a86e0a8052e879636dChristian Maeder lockGlobal gInfo
0a64bfd28dff15bc93e1f7a86e0a8052e879636dChristian Maeder le <- readIORef ioRefProofStatus
0a64bfd28dff15bc93e1f7a86e0a8052e879636dChristian Maeder (dgraph',dgn') <- initLocking (lookupDGraph ln le) (descr, dgn)
0a64bfd28dff15bc93e1f7a86e0a8052e879636dChristian Maeder writeIORef ioRefProofStatus $ Map.insert ln dgraph' le
0a64bfd28dff15bc93e1f7a86e0a8052e879636dChristian Maeder unlockGlobal gInfo
0a64bfd28dff15bc93e1f7a86e0a8052e879636dChristian Maeder return (dgraph',dgn')
0a64bfd28dff15bc93e1f7a86e0a8052e879636dChristian Maeder locked <- tryLockLocal dgn'
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder case locked of
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder createTextDisplay "Error" "Proofwindow already open" [HTk.size(30,10)]
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder let action = (do le <- readIORef ioRefProofStatus
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder guiMVar <- newMVar Nothing
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder res <- basicInferenceNode checkCons logicGraph libNode ln
2353f65833a3da763392f771223250cd50b8d873Christian Maeder runProveAtNode gInfo (descr, dgn') res)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder case checkCons || not (hasIncomingHidingEdge dgraph' $ snd libNode) of
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder True -> action
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder False -> GUI.HTkUtils.createInfoDisplayWithTwoButtons "Warning"
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder "This node has incoming hiding links!!!" "Prove anyway"
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder unlockLocal dgn'
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederrunProveAtNode :: GInfo -> LNode DGNodeLab -> Res.Result LibEnv -> IO ()
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederrunProveAtNode gInfo@(GInfo {gi_LIB_NAME = ln}) (v,_)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder (Res.Result {maybeResult = mle}) = case mle of
00df6fd583c19393fa141d5a0e21ac74c7bf5b19Christian Maeder proofMenu gInfo $ mergeDGNodeLab gInfo (v, labDG (lookupDGraph ln le) v)
00df6fd583c19393fa141d5a0e21ac74c7bf5b19Christian Maeder Nothing -> return ()
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian MaedermergeDGNodeLab :: GInfo -> LNode DGNodeLab -> LibEnv -> IO (Res.Result LibEnv)
528539f3d544c24afe14e979fe51f03e50aa6e9cChristian MaedermergeDGNodeLab (GInfo{gi_LIB_NAME = ln}) (v, new_dgn) le = do
0ae7a79e865d4a6022d705d160530682b3c1f825Christian Maeder let dg = lookupDGraph ln le
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder old_dgn = labDG dg v
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder theory <- joinG_sentences (dgn_theory old_dgn) $ dgn_theory new_dgn
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder let new_dgn' = old_dgn { dgn_theory = theory }
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder (dg', _) = labelNodeDG (v, new_dgn') dg
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder dg'' = addToProofHistoryDG ([], [SetNodeLab old_dgn (v, new_dgn')]) dg'
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder return $ Map.insert ln dg'' le
59a10395caff224b2ec541f94dac5082a506c00fChristian Maeder-- | print the id, origin, type, proof-status and morphism of the edge
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedershowEdgeInfo :: Int -> Maybe (LEdge DGLinkLab) -> IO ()
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian MaedershowEdgeInfo descr me = case me of
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder Just e@(_, _, l) -> let estr = showLEdge e in
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder createTextDisplay ("Info of " ++ estr)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder (estr ++ "\n" ++ showDoc l "") [HTk.size(70,30)]
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder Nothing -> createTextDisplay "Error"
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder ("edge " ++ show descr ++ " has no corresponding edge"
2353f65833a3da763392f771223250cd50b8d873Christian Maeder ++ "in the development graph") [HTk.size(50,10)]
2353f65833a3da763392f771223250cd50b8d873Christian Maeder-- | check conservativity of the edge
2353f65833a3da763392f771223250cd50b8d873Christian MaedercheckconservativityOfEdge :: Int -> GInfo -> Maybe (LEdge DGLinkLab) -> IO ()
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedercheckconservativityOfEdge _ gInfo
12aef5992d3af07dee81a4e02cf4be65a83f28bcChristian Maeder (Just (source,target,linklab)) = do
12aef5992d3af07dee81a4e02cf4be65a83f28bcChristian Maeder libEnv <- readIORef $ libEnvIORef gInfo
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder let dgraph = lookupDGraph (gi_LIB_NAME gInfo) libEnv
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder dgtar = labDG dgraph target
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder if isDGRef dgtar then error "checkconservativityOfEdge: no DGNode" else do
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder G_theory lid _ _ sens _ <- return $ dgn_theory dgtar
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder GMorphism cid _ _ morphism2 _ <- return $ dgl_morphism linklab
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder morphism2' <- coerceMorphism (targetLogic cid) lid
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder "checkconservativityOfEdge" morphism2
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder let th = case computeTheory libEnv (gi_LIB_NAME gInfo) source of
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder Res.Result _ (Just th1) -> th1
964ee9fff06b8c821e1d00207f6f185301371be8Christian Maeder _ -> error "checkconservativityOfEdge: computeTheory"
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder G_theory lid1 sign1 _ sens1 _ <- return th
12aef5992d3af07dee81a4e02cf4be65a83f28bcChristian Maeder sign2 <- coerceSign lid1 lid "checkconservativityOfEdge.coerceSign" sign1
964ee9fff06b8c821e1d00207f6f185301371be8Christian Maeder sens2 <- coerceThSens lid1 lid "" sens1
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder conservativityCheck lid
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder (plainSign sign2, toNamedList sens2)
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder morphism2' $ toNamedList sens
964ee9fff06b8c821e1d00207f6f185301371be8Christian Maeder showRes = case res of
964ee9fff06b8c821e1d00207f6f185301371be8Christian Maeder Just(Just True) -> "The link is conservative"
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder Just(Just False) -> "The link is not conservative"
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder _ -> "Could not determine whether link is conservative"
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder myDiags = unlines (map show ds)
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder createTextDisplay "Result of conservativity check"
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder (showRes ++ "\n" ++ myDiags) [HTk.size(50,50)]
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedercheckconservativityOfEdge descr _ Nothing =
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder createTextDisplay "Error"
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder ("edge " ++ show descr ++ " has no corresponding edge "
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder ++ "in the development graph") [HTk.size(30,10)]
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder-- | converts a DGraph
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maederconvert :: GA.GraphInfo -> DGraph -> IO ()
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maederconvert ginfo dgraph = do
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder convertNodes ginfo dgraph
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder convertEdges ginfo dgraph
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder{- | converts the nodes of the development graph, if it has any,
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maederand returns the resulting conversion maps
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maederif the graph is empty the conversion maps are returned unchanged-}
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederconvertNodes :: GA.GraphInfo -> DGraph -> IO ()
59a10395caff224b2ec541f94dac5082a506c00fChristian MaederconvertNodes ginfo = mapM_ (convertNodesAux ginfo) .labNodesDG
12aef5992d3af07dee81a4e02cf4be65a83f28bcChristian Maeder{- | auxiliary function for convertNodes if the given list of nodes is
12aef5992d3af07dee81a4e02cf4be65a83f28bcChristian Maederemtpy, it returns the conversion maps unchanged otherwise it adds the
12aef5992d3af07dee81a4e02cf4be65a83f28bcChristian Maederconverted first node to the abstract graph and to the affected
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maederconversion maps and afterwards calls itself with the remaining node
12aef5992d3af07dee81a4e02cf4be65a83f28bcChristian MaederconvertNodesAux :: GA.GraphInfo -> LNode DGNodeLab -> IO ()
12aef5992d3af07dee81a4e02cf4be65a83f28bcChristian MaederconvertNodesAux ginfo (node, dgnode) =
12aef5992d3af07dee81a4e02cf4be65a83f28bcChristian Maeder GA.addNode ginfo node (getRealDGNodeType dgnode) $ getDGNodeName dgnode
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder{- | converts the edges of the development graph
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederworks the same way as convertNods does-}
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederconvertEdges :: GA.GraphInfo -> DGraph -> IO ()
2353f65833a3da763392f771223250cd50b8d873Christian MaederconvertEdges ginfo = mapM_ (convertEdgesAux ginfo) . labEdgesDG
12aef5992d3af07dee81a4e02cf4be65a83f28bcChristian Maeder-- | auxiliary function for convertEges
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian MaederconvertEdgesAux :: GA.GraphInfo -> LEdge DGLinkLab -> IO ()
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian MaederconvertEdgesAux ginfo e@(src, tar, lbl) =
4b1833c7d3af466e6bcba24f16304e0a78e8da87Christian Maeder GA.addEdge ginfo (dgl_id lbl) (getRealDGLinkType lbl) src tar "" $ Just e
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | show library referened by a DGRef node (=node drawn as a box)
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedershowReferencedLibrary :: Int -> GInfo -> ConvFunc -> LibFunc -> IO ()
2353f65833a3da763392f771223250cd50b8d873Christian MaedershowReferencedLibrary descr gInfo@(GInfo { libEnvIORef = ioRefProofStatus
2353f65833a3da763392f771223250cd50b8d873Christian Maeder , gi_LIB_NAME = ln })
9d6562465b41f17c7967d4e5678f34811d958cb2Christian Maeder convGraph showLib = do
9d6562465b41f17c7967d4e5678f34811d958cb2Christian Maeder le <- readIORef ioRefProofStatus
2353f65833a3da763392f771223250cd50b8d873Christian Maeder let refNode = labDG (lookupDGraph ln le) descr
9d6562465b41f17c7967d4e5678f34811d958cb2Christian Maeder refLibname = if isDGRef refNode then dgn_libname refNode
9d6562465b41f17c7967d4e5678f34811d958cb2Christian Maeder else error "showReferencedLibrary"
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder case Map.lookup refLibname le of
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder gInfo' <- copyGInfo gInfo refLibname
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder convGraph gInfo' "development graph" showLib
9d6562465b41f17c7967d4e5678f34811d958cb2Christian Maeder let gv = gi_GraphInfo gInfo'
2353f65833a3da763392f771223250cd50b8d873Christian Maeder hideNodes gInfo'
cb2044812811d66efe038d914966e04290be93faChristian Maeder GA.showTemporaryMessage gv "Development Graph initialized."
2353f65833a3da763392f771223250cd50b8d873Christian Maeder Nothing -> error $ "The referenced library (" ++ show refLibname
cb2044812811d66efe038d914966e04290be93faChristian Maeder ++ ") is unknown"
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder-- | apply type changes of edges
cb2044812811d66efe038d914966e04290be93faChristian MaederapplyTypeChanges :: GA.GraphInfo -> DGraph -> IO ()
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian MaederapplyTypeChanges gi dgraph = do
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder mapM_ (\ (node, dgnode) ->
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder GA.changeNodeType gi node $ getRealDGNodeType dgnode
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder ) $ labNodesDG dgraph
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder mapM_ (\ (_, _, lbl) ->
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder GA.changeEdgeType gi (dgl_id lbl) $ getRealDGLinkType lbl
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder ) $ labEdgesDG dgraph
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder-- | apply the changes of first history item (computed by proof rules,
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder-- see folder Proofs) to the displayed development graph
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian MaederapplyChanges :: GA.GraphInfo -> ProofHistory -> IO ()
2353f65833a3da763392f771223250cd50b8d873Christian MaederapplyChanges _ [] = return ()
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederapplyChanges ginfo ((_, hElem) : _) = mapM_ (applyChangesAux ginfo)
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder $ removeNullifyingChanges $ removeContraryChanges hElem
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder-- | auxiliary function for applyChanges
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian MaederapplyChangesAux :: GA.GraphInfo -> DGChange -> IO ()
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederapplyChangesAux ginfo change =
2360728d4185c0c04279c999941c64d36626af79Christian Maeder case change of
cb2044812811d66efe038d914966e04290be93faChristian Maeder SetNodeLab _ (node, newLab) ->
2360728d4185c0c04279c999941c64d36626af79Christian Maeder GA.changeNodeType ginfo node $ getRealDGNodeType newLab
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder InsertNode (node, nodelab) ->
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder GA.addNode ginfo node (getRealDGNodeType nodelab) $ getDGNodeName nodelab
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder DeleteNode (node, _) ->
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder InsertEdge e@(src, tgt, lbl) ->
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder GA.addEdge ginfo (dgl_id lbl) (getRealDGLinkType lbl) src tgt "" $ Just e
8c8545dd3bf34fbcbc16904b65d249658f8f9efcChristian Maeder DeleteEdge (_, _, lbl) ->
8c8545dd3bf34fbcbc16904b65d249658f8f9efcChristian Maeder GA.delEdge ginfo $ dgl_id lbl
8c8545dd3bf34fbcbc16904b65d249658f8f9efcChristian Maeder-- | removes changed that are eliminating each other like 'add a' and 'del a'
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederremoveNullifyingChanges :: [DGChange] -> [DGChange]
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederremoveNullifyingChanges [] = []
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederremoveNullifyingChanges (change:changes) = case change of
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder InsertNode (node, _) -> case find
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder (\ c -> case c of
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder DeleteNode (node', _) -> node == node'
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder _ -> False) changes of
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder Just c' -> removeNullifyingChanges $ delete c' changes
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder Nothing -> change:removeNullifyingChanges changes
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder InsertEdge (_,_,el) -> let (EdgeId eid) = dgl_id el in case find
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder (\ c -> case c of
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder DeleteEdge (_,_,el') -> let (EdgeId eid') = dgl_id el' in eid == eid'
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder _ -> False) changes of
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder Just c' -> removeNullifyingChanges $ delete c' changes
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder Nothing -> change : removeNullifyingChanges changes
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder _ -> change : removeNullifyingChanges changes
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder-- | display a window of translated graph with maximal sublogic.
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian MaederopenTranslateGraph :: LibEnv -> LIB_NAME -> HetcatsOpts
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder -> Res.Result G_sublogics -> ConvFunc -> LibFunc -> IO ()
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian MaederopenTranslateGraph libEnv ln opts (Res.Result diagsSl mSublogic) convGraph
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder -- if an error existed by the search of maximal sublogicn
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder -- (see GUI.DGTranslation.getDGLogic), the process need not to go on.
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder if hasErrors diagsSl then
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder errorMess $ unlines $ map show
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder $ filter (relevantDiagKind . diagKind) diagsSl
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder do case mSublogic of
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder Just sublogic -> do
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder let paths = findComorphismPaths logicGraph sublogic
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder if null paths then
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder errorMess "This graph has no comorphism to translation."
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder Res.Result diagsR i <- runResultT ( do
7968d3a131e5a684ec1ff0c6d88aae638549153dChristian Maeder -- the user choose one
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder sel <- lift $ listBox "Choose a logic translation"
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder (map show paths)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder Just j -> return j
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder _ -> liftR $ fail "no logic translation chosen")
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder let aComor = paths !! fromJust i
7f7460e7095628f3437b116ee78d3043d11f8febChristian Maeder -- graph translation.
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder case libEnv_translation libEnv aComor of
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder Res.Result diagsTrans (Just newLibEnv) -> do
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder showDiags opts (diagsSl ++ diagsR ++ diagsTrans)
5941ba0b9a99ac98f78a89a9f3303102657e36ccChristian Maeder if hasErrors (diagsR ++ diagsTrans) then
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder errorMess $ unlines $ map show
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder $ filter (relevantDiagKind . diagKind)
5941ba0b9a99ac98f78a89a9f3303102657e36ccChristian Maeder $ diagsR ++ diagsTrans
5941ba0b9a99ac98f78a89a9f3303102657e36ccChristian Maeder else dg_showGraphAux
Res.Result diagsTrans Nothing ->
GA.redisplay $ gi_GraphInfo gInfo
saveUDGraph :: GInfo -> Map.Map DGNodeType (Shape value, String)
maybeFilePath <- HTk.sync evnt
GA.showTemporaryMessage graphInfo "Converting graph..."
GA.showTemporaryMessage graphInfo $ "Graph stored to " ++ filepath ++ "!"
Nothing -> GA.showTemporaryMessage graphInfo $ "Aborted!"
nodes2String :: GInfo -> Map.Map DGNodeType (Shape value, String)
nodes <- filterM (\(n,_) -> do b <- GA.isHiddenNode graphInfo n
node2String :: GInfo -> Map.Map DGNodeType (Shape value, String)
(shape, color) <- case Map.lookup ntype nodemap of
b <- GA.isHiddenEdge graphInfo eid
(line, color) <- case Map.lookup ltype linkmap of