GraphLogic.hs revision 5bed2c62278d4f062c980a72c631578a9ee4a608
beff4152e9f0fe90885458d1a1733b183a2a8816Christian MaederModule : $Header$
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerDescription : 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".
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder , remakeGraph
d1c667fd9445963d9d31e2cf5d0ead15e77082a4cmaeder , performProofAction
93603bd881e43d4ff5a57d7ca4e2b9fa619f25b4cmaeder , openProofStatus
d1c667fd9445963d9d31e2cf5d0ead15e77082a4cmaeder , saveProofStatus
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , openTranslateGraph
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartist , showReferencedLibrary
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , getSignatureOfNode
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , getTheoryOfNode
ea5ccb1c6e89486a54e1f4bd95840147e96093edChristian Maeder , getLocalAxOfNode
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , translateTheoryOfNode
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , displaySubsortGraph
85e1d54a475bfc30b3eac5ae6c5e42a2d7e93f10Christian Maeder , displayConceptGraph
85e1d54a475bfc30b3eac5ae6c5e42a2d7e93f10Christian Maeder , lookupTheoryOfNode
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , getSublogicOfNode
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa , showOriginOfNode
91e24fc45834b35f2a3830d72565640251149bf3Christian Maeder , showProofStatusOfNode
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , proveAtNode
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , showJustSubtree
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , showIDOfEdge
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , getNumberOfNode
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , showMorphismOfEdge
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , showOriginOfEdge
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , checkconservativityOfEdge
0130083f314580170af1195037be3325f125fbceChristian Maeder , showProofStatusOfThm
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , convertNodes
0130083f314580170af1195037be3325f125fbceChristian Maeder , convertEdges
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , hideShowNames
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , translateGraph
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , showLibGraph
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , saveUDGraph
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maederimport Logic.Logic(conservativityCheck)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport Logic.Coerce(coerceSign, coerceMorphism)
7f7460e7095628f3437b116ee78d3043d11f8febChristian Maederimport Syntax.AS_Library(LIB_NAME, getModTime, getLIB_ID)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport Static.DGToSpec(dgToSpec, computeTheory)
9d6562465b41f17c7967d4e5678f34811d958cb2Christian Maederimport Static.AnalysisLibrary(anaLibExt, anaLib)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport Static.DGTranslation(libEnv_translation)
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maederimport Proofs.InferBasic(basicInferenceNode)
7f7460e7095628f3437b116ee78d3043d11f8febChristian Maederimport Proofs.StatusUtils(lookupHistory, removeContraryChanges)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport GUI.Utils(listBox, createTextSaveDisplay)
96ae1a1d2197d0e0d5b80da2474b64c456feb1b0Christian Maederimport GUI.Taxonomy (displayConceptGraph,displaySubsortGraph)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport GUI.DGTranslation(getDGLogic)
4eb859461f8fd904f40f57261cf23e5c73cf8ecaChristian Maederimport qualified GUI.HTkUtils (displayTheory,
4eb859461f8fd904f40f57261cf23e5c73cf8ecaChristian Maeder displayTheoryWithWarning,
4eb859461f8fd904f40f57261cf23e5c73cf8ecaChristian Maeder createInfoDisplayWithTwoButtons)
4eb859461f8fd904f40f57261cf23e5c73cf8ecaChristian Maederimport DaVinciGraph
4eb859461f8fd904f40f57261cf23e5c73cf8ecaChristian Maederimport GraphDisp(deleteArc, deleteNode, getNodeValue)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport GraphConfigure
2353f65833a3da763392f771223250cd50b8d873Christian Maederimport TextDisplay(createTextDisplay)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport InfoBus(encapsulateWaitTermAct)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport DialogWin (useHTk)
dff1de7ad15d1582e25d636c3724dd202874897fChristian Maederimport Messages(errorMess)
dff1de7ad15d1582e25d636c3724dd202874897fChristian Maederimport qualified HTk
96ae1a1d2197d0e0d5b80da2474b64c456feb1b0Christian Maederimport Configuration(size)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport Common.Id(nullRange)
d81905a5b924415c524d702df26204683c82c12eChristian Maederimport Common.DocUtils(showDoc, pretty)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport Common.ResultT(liftR, runResultT)
dff1de7ad15d1582e25d636c3724dd202874897fChristian Maederimport qualified Common.OrderedMap as OMap
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport qualified Common.InjMap as InjMap
cb2044812811d66efe038d914966e04290be93faChristian Maederimport qualified Common.Lib.Rel as Rel
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport qualified Common.Lib.Graph as Tree
0ae7a79e865d4a6022d705d160530682b3c1f825Christian Maederimport Driver.WriteFn(writeShATermFile)
083bc1972a66d73749760eab3a90bf4eb9ca7951Christian Maederimport Driver.ReadFn(libNameToFile, readVerbose)
fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan Pascanuimport System.Directory(getModificationTime)
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksaimport Data.Char(toLower, isSpace)
bc263f610d20a9cd3014ddfca903026127fa0d48Christian Maederimport Data.Maybe(fromJust)
966519955f5f7111abac20118563132b9dd41165Christian Maederimport Data.List(nub,deleteBy,find)
8c8545dd3bf34fbcbc16904b65d249658f8f9efcChristian Maederimport Data.Graph.Inductive.Graph as Graph( Node, LEdge, LNode, lab'
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder , labNode', (&))
0b13f102310e03a20b38c870b5acb88712f316a4Christian Maederimport qualified Data.IntMap as IntMap
0b13f102310e03a20b38c870b5acb88712f316a4Christian Maederimport qualified Data.Map as Map
d4ebd9e5adc974cfa2bdf4bdd155e07be0e26f75Christian MaederrunAndLock :: GInfo -> IO () -> IO ()
d4ebd9e5adc974cfa2bdf4bdd155e07be0e26f75Christian MaederrunAndLock (GInfo { functionLock = lock
0d79ea4ed8512a802ecb6645edac141e0fbcee3fChristian Maeder , graphId = gid
0d79ea4ed8512a802ecb6645edac141e0fbcee3fChristian Maeder , gi_GraphInfo = actGraph
0d79ea4ed8512a802ecb6645edac141e0fbcee3fChristian Maeder }) function = do
a31430de8b0632d29f42634d6395e982bf31b14dChristian Maeder locked <- tryPutMVar lock ()
a31430de8b0632d29f42634d6395e982bf31b14dChristian Maeder case locked of
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder _ <- takeMVar lock
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder showTemporaryMessage gid actGraph $ "an other function is still working"
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder ++ "... please wait ..."
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian MaedernegateChanges :: ([DGRule],[DGChange]) -> ([DGRule],[DGChange])
9ee80c455784287a8b5e1b6bac1f8efa6a2f4bb3cmaedernegateChanges (_, dgChanges) = ([], reverse $ map negateChange dgChanges)
9ee80c455784287a8b5e1b6bac1f8efa6a2f4bb3cmaeder negateChange :: DGChange -> DGChange
8865728716566f42fa73e7e0bc080ba3225df764Christian Maeder negateChange change = case change of
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder InsertNode x -> DeleteNode x
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder DeleteNode x -> InsertNode x
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder InsertEdge x -> DeleteEdge x
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder DeleteEdge x -> InsertEdge x
1f2c732265a1292f0d7c51a4a7ca6be5dd370df6cmaeder SetNodeLab old (node, new) -> SetNodeLab new (node, old)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | Undo one step of the History
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederundo :: GInfo -> Bool -> IO ()
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maederundo gInfo@(GInfo { libEnvIORef = ioRefProofStatus
fdac680252d7347858bd67b4c2a2aaa52e623815Christian Maeder , globalHist = gHist
fdac680252d7347858bd67b4c2a2aaa52e623815Christian Maeder , graphId = gid
a9e804dbec424ec36e34bab955cbe90edac5baa6Christian Maeder , gi_GraphInfo = actGraph
f8cc2399c16fcda7e3bf9d901a0de0cc8a455f86Ewaryst Schulz }) isUndo = do
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder (guHist, grHist) <- takeMVar gHist
b76d27eba526ecac2a20400fa505ec5c642ae7d2Dominik Luecke case if isUndo then guHist else grHist of
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus Luettich showTemporaryMessage gid actGraph "History is empty..."
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus Luettich putMVar gHist (guHist, grHist)
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus Luettich (lns:gHist') -> do
2353f65833a3da763392f771223250cd50b8d873Christian Maeder le <- readIORef ioRefProofStatus
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder undoDGraphs gInfo isUndo lns
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder updateDGraphs le $ filter (\ln -> elem ln lns) $ Map.keys le
2353f65833a3da763392f771223250cd50b8d873Christian Maeder putMVar gHist $ if isUndo then (gHist', (reverse lns):grHist)
2353f65833a3da763392f771223250cd50b8d873Christian Maeder else ((reverse lns):guHist, gHist')
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederundoDGraphs :: GInfo -> Bool -> [LIB_NAME] -> IO ()
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederundoDGraphs _ _ [] = return ()
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederundoDGraphs g u (ln:r) = do
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder undoDGraph g u ln
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder undoDGraphs g u r
0b13f102310e03a20b38c870b5acb88712f316a4Christian MaederundoDGraph :: GInfo -> Bool -> LIB_NAME -> IO ()
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaederundoDGraph gInfo@(GInfo { libEnvIORef = ioRefProofStatus
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder , graphId = gid
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder , gi_GraphInfo = actGraph
00df6fd583c19393fa141d5a0e21ac74c7bf5b19Christian Maeder }) isUndo ln = do
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder showTemporaryMessage gid actGraph $ "Undo last change to " ++ show ln ++ "..."
cb2044812811d66efe038d914966e04290be93faChristian Maeder lockGlobal gInfo
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder le <- readIORef ioRefProofStatus
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder dg = lookupDGraph ln le
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder (phist,rhist) = if isUndo then (proofHistory dg, redoHistory dg)
8d780c893d6df5dab3dcc7d8444b7517f6547f11Christian Maeder else (redoHistory dg, proofHistory dg)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder change = negateChanges $ head phist
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder dg'' = (applyProofHistory [change] dg)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder dg' = case isUndo of
dff1de7ad15d1582e25d636c3724dd202874897fChristian Maeder True -> dg'' { redoHistory = change:rhist
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder , proofHistory = tail phist}
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder False -> dg'' { redoHistory = tail phist
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder , proofHistory = change:rhist}
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder writeIORef ioRefProofStatus $ Map.insert ln dg' le
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder unlockGlobal gInfo
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaederupdateDGraphs :: LibEnv -> [LIB_NAME] -> IO ()
bc263f610d20a9cd3014ddfca903026127fa0d48Christian MaederupdateDGraphs _ [] = return ()
966519955f5f7111abac20118563132b9dd41165Christian MaederupdateDGraphs le (ln:r) = do
bbba6dd86153aacb0f662b182b128df0eb09fd54Christian Maeder updateDGraph $ lookupDGraph ln le
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder updateDGraphs le r
d96bfd1d7a4595bfff87771b91797330fa939455Christian MaederupdateDGraph :: DGraph -> IO ()
8c8545dd3bf34fbcbc16904b65d249658f8f9efcChristian MaederupdateDGraph dg = case openlock dg of
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder Just lock -> do
34d14197eb3dd643a8e6ef3ed8cba5629528e97fAivaras Jakubauskas mRemakeF <- tryTakeMVar lock
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa case mRemakeF of
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder Just remakeF -> do
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder putMVar lock remakeF
0d79ea4ed8512a802ecb6645edac141e0fbcee3fChristian Maeder Nothing -> return ()
a31430de8b0632d29f42634d6395e982bf31b14dChristian Maeder Nothing -> return ()
9ee80c455784287a8b5e1b6bac1f8efa6a2f4bb3cmaeder-- | reloads the Library of the DevGraph
d4ebd9e5adc974cfa2bdf4bdd155e07be0e26f75Christian Maederreload :: GInfo -> IO()
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maederreload gInfo@(GInfo { libEnvIORef = ioRefProofStatus
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder , gi_LIB_NAME = ln
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder , gi_hetcatsOpts = opts
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder lockGlobal gInfo
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder oldle <- readIORef ioRefProofStatus
0b13f102310e03a20b38c870b5acb88712f316a4Christian Maeder libdeps = Rel.toList $ Rel.intransKernel $ Rel.transClosure $ Rel.fromList
2360728d4185c0c04279c999941c64d36626af79Christian Maeder $ getLibDeps oldle
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder ioruplibs <- newIORef ([] :: [LIB_NAME])
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder writeIORef ioruplibs []
00df6fd583c19393fa141d5a0e21ac74c7bf5b19Christian Maeder reloadLibs ioRefProofStatus opts libdeps ioruplibs ln
2360728d4185c0c04279c999941c64d36626af79Christian Maeder unlockGlobal gInfo
2360728d4185c0c04279c999941c64d36626af79Christian Maeder remakeGraph gInfo
96ae1a1d2197d0e0d5b80da2474b64c456feb1b0Christian Maeder-- | Creates a list of all LIB_NAME pairs, which have a dependency
2360728d4185c0c04279c999941c64d36626af79Christian MaedergetLibDeps :: LibEnv -> [(LIB_NAME, LIB_NAME)]
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaedergetLibDeps le =
8d780c893d6df5dab3dcc7d8444b7517f6547f11Christian Maeder concat $ map (\ ln -> getDep ln le) $ Map.keys le
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- | Creates a list of LIB_NAME pairs for the fist argument
dff1de7ad15d1582e25d636c3724dd202874897fChristian MaedergetDep :: LIB_NAME -> LibEnv -> [(LIB_NAME, LIB_NAME)]
2360728d4185c0c04279c999941c64d36626af79Christian MaedergetDep ln le =
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder map (\ x -> (ln, x)) $ map (\ (_,x,_) -> dgn_libname x) $ IntMap.elems $
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder IntMap.filter (\ (_,x,_) -> isDGRef x) $ Tree.convertToMap $
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder dgBody $ lookupDGraph ln le
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- | Reloads a library
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaederreloadLib :: IORef LibEnv -> HetcatsOpts -> IORef [LIB_NAME] -> LIB_NAME
bc263f610d20a9cd3014ddfca903026127fa0d48Christian MaederreloadLib iorle opts ioruplibs ln = do
966519955f5f7111abac20118563132b9dd41165Christian Maeder mfile <- existsAnSource opts {intype = GuessIn}
bbba6dd86153aacb0f662b182b128df0eb09fd54Christian Maeder $ rmSuffix $ libNameToFile opts ln
5a448e9be8c4482a978b174b744237757335140fChristian Maeder case mfile of
d96bfd1d7a4595bfff87771b91797330fa939455Christian Maeder Nothing -> do
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder Just file -> do
34d14197eb3dd643a8e6ef3ed8cba5629528e97fAivaras Jakubauskas le <- readIORef iorle
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder mres <- anaLibExt opts file le'
0d79ea4ed8512a802ecb6645edac141e0fbcee3fChristian Maeder Just (_, newle) -> do
a31430de8b0632d29f42634d6395e982bf31b14dChristian Maeder uplibs <- readIORef ioruplibs
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder writeIORef ioruplibs $ ln:uplibs
9ee80c455784287a8b5e1b6bac1f8efa6a2f4bb3cmaeder writeIORef iorle newle
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder Nothing -> do
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder fail $ "Could not read original development graph from '"++ file
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder-- | Reloads libraries if nessesary
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian MaederreloadLibs :: IORef LibEnv -> HetcatsOpts -> [(LIB_NAME, LIB_NAME)]
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder -> IORef [LIB_NAME] -> LIB_NAME -> IO Bool
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaederreloadLibs iorle opts deps ioruplibs ln = do
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder uplibs <- readIORef ioruplibs
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder case elem ln uplibs of
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder True -> return True
dff1de7ad15d1582e25d636c3724dd202874897fChristian Maeder deps' = map (snd) $ filter (\ (ln',_) -> ln == ln') deps
0b13f102310e03a20b38c870b5acb88712f316a4Christian Maeder res <- mapM (reloadLibs iorle opts deps ioruplibs) deps'
dff1de7ad15d1582e25d636c3724dd202874897fChristian Maeder libupdate = foldl (\ u r -> if r then True else u) False res
0b13f102310e03a20b38c870b5acb88712f316a4Christian Maeder case libupdate of
9ee80c455784287a8b5e1b6bac1f8efa6a2f4bb3cmaeder reloadLib iorle opts ioruplibs ln
9ee80c455784287a8b5e1b6bac1f8efa6a2f4bb3cmaeder return True
0b13f102310e03a20b38c870b5acb88712f316a4Christian Maeder le <- readIORef iorle
0b13f102310e03a20b38c870b5acb88712f316a4Christian Maeder newln:_ = filter (ln ==) $ Map.keys le
0b13f102310e03a20b38c870b5acb88712f316a4Christian Maeder mfile <- existsAnSource opts $ rmSuffix $ libNameToFile opts ln
96ae1a1d2197d0e0d5b80da2474b64c456feb1b0Christian Maeder case mfile of
96ae1a1d2197d0e0d5b80da2474b64c456feb1b0Christian Maeder Nothing -> do
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder Just file -> do
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder newmt <- getModificationTime file
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa libupdate' = (getModTime $ getLIB_ID newln) < newmt
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder case libupdate' of
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder False -> return False
96ae1a1d2197d0e0d5b80da2474b64c456feb1b0Christian Maeder reloadLib iorle opts ioruplibs ln
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder-- | Deletes the old edges and nodes of the Graph and makes new ones
ce8a93047aaf0dc36fa221642292d47852a9862aChristian MaederremakeGraph :: GInfo -> IO ()
0b13f102310e03a20b38c870b5acb88712f316a4Christian MaederremakeGraph (GInfo { libEnvIORef = ioRefProofStatus
0b13f102310e03a20b38c870b5acb88712f316a4Christian Maeder , conversionMapsIORef = convRef
0b13f102310e03a20b38c870b5acb88712f316a4Christian Maeder , graphId = gid
0b13f102310e03a20b38c870b5acb88712f316a4Christian Maeder , gi_LIB_NAME = ln
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder , gi_GraphInfo = actGraphInfo
8bb80c9684e905de8dcfcfb1291542677e7d77b6Christian Maeder le <- readIORef ioRefProofStatus
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder (gs,ev_cnt) <- readIORef actGraphInfo
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder dgraph = lookupDGraph ln le
dff1de7ad15d1582e25d636c3724dd202874897fChristian Maeder Just (_, g) = find (\ (gid', _) -> gid' == gid) gs
8bb80c9684e905de8dcfcfb1291542677e7d77b6Christian Maeder gs' = deleteBy (\ (gid1,_) (gid2,_) -> gid1 == gid2) (gid,g) gs
00df6fd583c19393fa141d5a0e21ac74c7bf5b19Christian Maeder og = theGraph g
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder -- reads and delets the old nodes and edges
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder mapM_ (deleteArc og) $ map (\ (_,_,_,x) -> x) $ Map.elems $ AGV.edges g
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder mapM_ (deleteNode og) $ map snd $ Map.elems $ AGV.nodes g
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder -- stores the graph without nodes and edges in the GraphInfo
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder g' = g {theGraph = og, AGV.nodes = Map.empty, AGV.edges = Map.empty}
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder writeIORef actGraphInfo ((gid,g'):gs',ev_cnt)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder -- creates new nodes and edges
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder newConvMaps <- convertNodes emptyConversionMaps gid actGraphInfo dgraph ln
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder finalConvMaps <- convertEdges newConvMaps gid actGraphInfo dgraph ln
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder -- writes the ConversionMap and redisplays the graph
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder writeIORef convRef finalConvMaps
60e6795dd310e10194e12bb660575aadf941328bEugen Kuksa redisplay gid actGraphInfo
966519955f5f7111abac20118563132b9dd41165Christian MaederhideShowNames :: GInfo -> Bool -> IO ()
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaederhideShowNames (GInfo {graphId = gid,
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder gi_GraphInfo = actGraphInfo,
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder internalNamesIORef = showInternalNames
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder }) toggle = do
dff1de7ad15d1582e25d636c3724dd202874897fChristian Maeder deactivateGraphWindow gid actGraphInfo
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder (intrn::InternalNames) <- readIORef showInternalNames
cb2044812811d66efe038d914966e04290be93faChristian Maeder let showThem = if toggle then not $ showNames intrn else showNames intrn
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder showItrn s = if showThem then s else ""
8d780c893d6df5dab3dcc7d8444b7517f6547f11Christian Maeder mapM_ (\(s,upd) -> upd (\_ -> showItrn s)) $ updater intrn
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder writeIORef showInternalNames $ intrn {showNames = showThem}
96ae1a1d2197d0e0d5b80da2474b64c456feb1b0Christian Maeder redisplay gid actGraphInfo
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder activateGraphWindow gid actGraphInfo
00df6fd583c19393fa141d5a0e21ac74c7bf5b19Christian MaedershowNodes :: GInfo -> IO ()
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaedershowNodes gInfo@(GInfo {descrIORef = event,
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder graphId = gid,
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder gi_GraphInfo = actGraphInfo
bbba6dd86153aacb0f662b182b128df0eb09fd54Christian Maeder deactivateGraphWindow gid actGraphInfo
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder descr <- readIORef event
8c8545dd3bf34fbcbc16904b65d249658f8f9efcChristian Maeder AGV.Result _ errorMsg <- checkHasHiddenNodes gid descr actGraphInfo
33fcc19ef2b59493b4e91eebf701df95fd230765Christian Maeder case errorMsg of
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder Nothing -> do
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder showTemporaryMessage gid actGraphInfo "Revealing hidden nodes ..."
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa showIt gid descr actGraphInfo
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder hideShowNames gInfo False
0d79ea4ed8512a802ecb6645edac141e0fbcee3fChristian Maeder showTemporaryMessage gid actGraphInfo "No hidden nodes found ..."
a31430de8b0632d29f42634d6395e982bf31b14dChristian Maeder activateGraphWindow gid actGraphInfo
9b3e946be44391d35acb2168f4e67d629e560f79Till MossakowskihideNodes :: GInfo -> IO ()
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederhideNodes (GInfo {descrIORef = event,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder graphId = gid,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder gi_GraphInfo = actGraphInfo
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder deactivateGraphWindow gid actGraphInfo
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder descr' <- readIORef event
12aef5992d3af07dee81a4e02cf4be65a83f28bcChristian Maeder AGV.Result _ errorMsg <- checkHasHiddenNodes gid descr' actGraphInfo
2360728d4185c0c04279c999941c64d36626af79Christian Maeder case errorMsg of
2360728d4185c0c04279c999941c64d36626af79Christian Maeder Nothing -> do
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa showTemporaryMessage gid actGraphInfo "Nodes already hidden ..."
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder showTemporaryMessage gid actGraphInfo "Hiding unnamed nodes..."
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian Maeder AGV.Result descr msg <- hideSetOfNodeTypes gid
2360728d4185c0c04279c999941c64d36626af79Christian Maeder [--red nodes are not hidden
2360728d4185c0c04279c999941c64d36626af79Christian Maeder --"open_cons__internal",
0130083f314580170af1195037be3325f125fbceChristian Maeder --"locallyEmpty__open_cons__internal",
d81905a5b924415c524d702df26204683c82c12eChristian Maeder --"proven_cons__internal",
96ae1a1d2197d0e0d5b80da2474b64c456feb1b0Christian Maeder "locallyEmpty__proven_cons__internal"]
2360728d4185c0c04279c999941c64d36626af79Christian Maeder True actGraphInfo
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian Maeder writeIORef event descr
2360728d4185c0c04279c999941c64d36626af79Christian Maeder Nothing -> do redisplay gid actGraphInfo
966519955f5f7111abac20118563132b9dd41165Christian Maeder Just err -> putStrLn err
2360728d4185c0c04279c999941c64d36626af79Christian Maeder activateGraphWindow gid actGraphInfo
2360728d4185c0c04279c999941c64d36626af79Christian MaedertranslateGraph :: GInfo -> ConvFunc -> LibFunc -> IO ()
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian MaedertranslateGraph (GInfo {libEnvIORef = ioRefProofStatus,
dff1de7ad15d1582e25d636c3724dd202874897fChristian Maeder gi_LIB_NAME = ln,
2360728d4185c0c04279c999941c64d36626af79Christian Maeder gi_hetcatsOpts = opts
2360728d4185c0c04279c999941c64d36626af79Christian Maeder }) convGraph showLib = do
2360728d4185c0c04279c999941c64d36626af79Christian Maeder le <- readIORef ioRefProofStatus
2360728d4185c0c04279c999941c64d36626af79Christian Maeder openTranslateGraph le ln opts (getDGLogic le) convGraph showLib
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaedershowLibGraph :: GInfo -> LibFunc -> IO ()
8994ef587ce7c7c39ddd20f0f7e4575838a6694aChristian MaedershowLibGraph gInfo showLib = do
33fcc19ef2b59493b4e91eebf701df95fd230765Christian Maeder showLib gInfo
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder{- | it tries to perform the given action to the given graph.
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder If part of the given graph is not hidden, then the action can
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder be performed directly; otherwise the graph will be shown completely
0b13f102310e03a20b38c870b5acb88712f316a4Christian Maeder firstly, and then the action will be performed, and after that the graph
9ee80c455784287a8b5e1b6bac1f8efa6a2f4bb3cmaeder will be hidden again.
2360728d4185c0c04279c999941c64d36626af79Christian MaederperformProofAction :: GInfo -> IO () -> IO ()
60e6795dd310e10194e12bb660575aadf941328bEugen KuksaperformProofAction gInfo@(GInfo {descrIORef = event,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder graphId = gid,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder gi_GraphInfo = actGraphInfo
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder }) proofAction = do
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder let actionWithMessage = do
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder showTemporaryMessage gid actGraphInfo
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder "Applying development graph calculus proof rule..."
dff1de7ad15d1582e25d636c3724dd202874897fChristian Maeder descr <- readIORef event
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder AGV.Result _ errorMsg <- checkHasHiddenNodes gid descr actGraphInfo
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder case errorMsg of
91e24fc45834b35f2a3830d72565640251149bf3Christian Maeder Nothing -> do
91e24fc45834b35f2a3830d72565640251149bf3Christian Maeder showNodes gInfo
91e24fc45834b35f2a3830d72565640251149bf3Christian Maeder actionWithMessage
91e24fc45834b35f2a3830d72565640251149bf3Christian Maeder hideNodes gInfo
91e24fc45834b35f2a3830d72565640251149bf3Christian Maeder Just _ -> actionWithMessage
91e24fc45834b35f2a3830d72565640251149bf3Christian Maeder showTemporaryMessage gid actGraphInfo
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder "Development graph calculus proof rule finished."
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedersaveProofStatus :: GInfo -> FilePath -> IO ()
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedersaveProofStatus (GInfo {libEnvIORef = ioRefProofStatus,
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder gi_LIB_NAME = ln,
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder gi_hetcatsOpts = opts
2360728d4185c0c04279c999941c64d36626af79Christian Maeder }) file = encapsulateWaitTermAct $ do
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder proofStatus <- readIORef ioRefProofStatus
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder writeShATermFile file (ln, lookupHistory ln proofStatus)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder putIfVerbose opts 2 $ "Wrote " ++ file
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- | implementation of open menu, read in a proof status
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaederopenProofStatus :: GInfo -> FilePath -> ConvFunc -> LibFunc
8762d0e3d492aba4d1621fb0de685f0be1372864notanartist -> IO (Descr, GraphInfo, ConversionMaps)
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartistopenProofStatus gInfo@(GInfo {libEnvIORef = ioRefProofStatus,
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder conversionMapsIORef = convRef,
76d027be764e2ff61bef959efb3ac8f56499e646Christian Maeder gi_LIB_NAME = ln,
9f85afecbd79b3df5a0bb17bd28cd0b288dc3213Kristina Sojakova gi_hetcatsOpts = opts
a166da43d4e8f9dfa7a2651d033c6bea02627ca6Mihai Codescu }) file convGraph showLib = do
22b772f8753f0cdb4508ba460356c238de2ee375Jonathan von Schroeder mh <- readVerbose opts ln file
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder Nothing -> fail
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder $ "Could not read proof status from file '"
63da71bfb4226f504944b293fb77177ebcaea7d4Ewaryst Schulz ++ file ++ "'"
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder let libfile = libNameToFile opts ln
8762d0e3d492aba4d1621fb0de685f0be1372864notanartist m <- anaLib opts { outtypes = [] } libfile
b47b1ea8a412f6e4c731779f6a572384e7cf06d8Christian Maeder Nothing -> fail
26b1c101b72100b69045effdfaab3889de6c8c93Christian Maeder $ "Could not read original development graph from '"
a68ff26ddb1d300f7e16097edef615f130fcd5ceChristian Maeder ++ libfile ++ "'"
9f226cec9f978edaba67aee4c4e04e3d3b994b87Daniel Calegari Just (_, libEnv) -> case Map.lookup ln libEnv of
f730570f7c284b252ad2e24cf23cc594021f9e25Jonathan von Schroeder Nothing -> fail
6f70475dddc12732bdbef3e3dd116373e34cd6b9Christian Maeder $ "Could not get original development graph for '"
897a04683fb30873e84dc3360dea770a4435971cChristian Maeder ++ showDoc ln "'"
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder Just dg -> do
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder lockGlobal gInfo
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder oldEnv <- readIORef ioRefProofStatus
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder let proofStatus = Map.insert ln
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder (applyProofHistory h dg) oldEnv
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder writeIORef ioRefProofStatus proofStatus
8762d0e3d492aba4d1621fb0de685f0be1372864notanartist unlockGlobal gInfo
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartist gInfo' <- copyGInfo gInfo
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder (gid, actGraphInfo, convMaps) <-
63da71bfb4226f504944b293fb77177ebcaea7d4Ewaryst Schulz convGraph (gInfo' {gi_LIB_NAME = ln})
76d027be764e2ff61bef959efb3ac8f56499e646Christian Maeder "Proof Status " showLib
9f85afecbd79b3df5a0bb17bd28cd0b288dc3213Kristina Sojakova writeIORef convRef convMaps
a166da43d4e8f9dfa7a2651d033c6bea02627ca6Mihai Codescu redisplay gid actGraphInfo
22b772f8753f0cdb4508ba460356c238de2ee375Jonathan von Schroeder return (gid, actGraphInfo, convMaps)
f730570f7c284b252ad2e24cf23cc594021f9e25Jonathan von Schroeder-- | apply a rule of the development graph calculus
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaederproofMenu :: GInfo
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder -> (LibEnv -> IO (Res.Result LibEnv))
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaederproofMenu gInfo@(GInfo { libEnvIORef = ioRefProofStatus
8762d0e3d492aba4d1621fb0de685f0be1372864notanartist , descrIORef = event
af6e92e4a9ca308f928f9909acee115f801c5db5Ewaryst Schulz , conversionMapsIORef = convRef
b47b1ea8a412f6e4c731779f6a572384e7cf06d8Christian Maeder , graphId = gid
26b1c101b72100b69045effdfaab3889de6c8c93Christian Maeder , gi_LIB_NAME = ln
a68ff26ddb1d300f7e16097edef615f130fcd5ceChristian Maeder , gi_GraphInfo = actGraphInfo
9f226cec9f978edaba67aee4c4e04e3d3b994b87Daniel Calegari , gi_hetcatsOpts = hOpts
6f70475dddc12732bdbef3e3dd116373e34cd6b9Christian Maeder , proofGUIMVar = guiMVar
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder , visibleNodesIORef = ioRefVisibleNodes
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder , globalHist = gHist
2353f65833a3da763392f771223250cd50b8d873Christian Maeder }) proofFun = do
1ebf8299efa3cdb39c73d40d15e1d1a8a2246e68notanartist filled <- tryPutMVar guiMVar Nothing
1ebf8299efa3cdb39c73d40d15e1d1a8a2246e68notanartist if not filled
1ebf8299efa3cdb39c73d40d15e1d1a8a2246e68notanartist then readMVar guiMVar >>=
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder (maybe (putIfVerbose hOpts 0 "proofMenu: ignored Nothing")
897a04683fb30873e84dc3360dea770a4435971cChristian Maeder putIfVerbose hOpts 4 $
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder "proofMenu: Ignored Proof command; " ++
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder "maybe a proof window is still open?"
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder lockGlobal gInfo
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder proofStatus <- readIORef ioRefProofStatus
8762d0e3d492aba4d1621fb0de685f0be1372864notanartist putIfVerbose hOpts 4 "Proof started via \"Proofs\" menu"
1ebf8299efa3cdb39c73d40d15e1d1a8a2246e68notanartist Res.Result ds res <- proofFun proofStatus
1ebf8299efa3cdb39c73d40d15e1d1a8a2246e68notanartist putIfVerbose hOpts 4 "Analyzing result of proof"
1ebf8299efa3cdb39c73d40d15e1d1a8a2246e68notanartist Nothing -> do
1ebf8299efa3cdb39c73d40d15e1d1a8a2246e68notanartist unlockGlobal gInfo
1ebf8299efa3cdb39c73d40d15e1d1a8a2246e68notanartist mapM_ (putStrLn . show) ds
1ebf8299efa3cdb39c73d40d15e1d1a8a2246e68notanartist Just newProofStatus -> do
1ebf8299efa3cdb39c73d40d15e1d1a8a2246e68notanartist let newGr = lookupDGraph ln newProofStatus
1ebf8299efa3cdb39c73d40d15e1d1a8a2246e68notanartist history = proofHistory newGr
1ebf8299efa3cdb39c73d40d15e1d1a8a2246e68notanartist (guHist, grHist) <- takeMVar gHist
1ebf8299efa3cdb39c73d40d15e1d1a8a2246e68notanartist putMVar gHist
1ebf8299efa3cdb39c73d40d15e1d1a8a2246e68notanartist (calcGlobalHistory proofStatus newProofStatus : guHist, grHist)
1ebf8299efa3cdb39c73d40d15e1d1a8a2246e68notanartist descr <- readIORef event
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartist convMaps <- readIORef convRef
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartist (newDescr,convMapsAux) <- applyChanges gid ln actGraphInfo descr
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartist ioRefVisibleNodes convMaps history
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartist writeIORef ioRefProofStatus newProofStatus
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartist unlockGlobal gInfo
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartist writeIORef event newDescr
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartist writeIORef convRef convMapsAux
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartist hideShowNames gInfo False
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartist mGUIMVar <- tryTakeMVar guiMVar
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartist maybe (fail $ "should be filled with Nothing after "++"proof attempt")
8762d0e3d492aba4d1621fb0de685f0be1372864notanartist (const $ return ())
df87ff823273ae2969e9d29e833845b4c0a9ee77notanartistcalcGlobalHistory :: LibEnv -> LibEnv -> [LIB_NAME]
df87ff823273ae2969e9d29e833845b4c0a9ee77notanartistcalcGlobalHistory old new = let
df87ff823273ae2969e9d29e833845b4c0a9ee77notanartist pHist = (\ ln le -> proofHistory $ lookupDGraph ln le)
df87ff823273ae2969e9d29e833845b4c0a9ee77notanartist length' = (\ ln le -> length $ pHist ln le)
df87ff823273ae2969e9d29e833845b4c0a9ee77notanartist changes = filter (\ ln -> pHist ln old /= pHist ln new) $ Map.keys old
df87ff823273ae2969e9d29e833845b4c0a9ee77notanartist in concatMap (\ ln -> replicate (length' ln new - length' ln old) ln) changes
c3b00d3435293c71ab4e750be084a2d8dcf6209fnotanartistnodeErr :: Descr -> IO ()
e38219f3dd2f5711440478cbffa76ce3db530543cmaedernodeErr descr = error $ "node with descriptor " ++ show descr
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus Luettich ++ " has no corresponding node in the development graph"
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaedershowSpec :: Descr -> DGraphAndAGraphNode -> DGraph -> IO ()
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaedershowSpec descr dgAndabstrNodeMap dgraph =
2360728d4185c0c04279c999941c64d36626af79Christian Maeder case InjMap.lookupWithB descr dgAndabstrNodeMap of
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus Luettich Nothing -> return ()
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus Luettich Just (_, node) -> do
7ebcceae3d34771cae3bbb8c8060bef0b894376eChristian Maeder let sp = dgToSpec dgraph node
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus Luettich sp' = case sp of
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder Res.Result ds Nothing -> show $ vcat $ map pretty ds
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder Res.Result _ m -> showDoc m ""
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder createTextDisplay "Show spec" sp' [size(80,25)]
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder{- | auxiliary method for debugging. shows the number of the given node
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder in the abstraction graph
3ec3a22fe2b9c38a3575c98a82b4e3f988af64a6Eugen KuksagetNumberOfNode :: Descr -> IO()
4c872eeb600fe8479dbda395405cf13c3d573c24Soeren D. SchulzegetNumberOfNode descr =
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder let title = "Number of node"
bc263f610d20a9cd3014ddfca903026127fa0d48Christian Maeder-- make the node number consistent, the descritor should be reduced by one
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder in createTextDisplay title (showDoc (descr-1) "") [HTk.size(10,10)]
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder{- | outputs the signature of a node in a window;
53a3042e1da2253fd3f103bfef4deb47fc0bf6a6Ewaryst Schulzused by the node menu defined in initializeGraph -}
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaedergetSignatureOfNode :: Descr -> DGraphAndAGraphNode -> DGraph -> IO()
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaedergetSignatureOfNode descr dgAndabstrNodeMap dgraph =
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder case InjMap.lookupWithB descr dgAndabstrNodeMap of
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder Just (_, node) ->
726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowski let dgnode = lab' (contextDG dgraph node)
8762d0e3d492aba4d1621fb0de685f0be1372864notanartist title = "Signature of "++showName (dgn_name dgnode)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder in createTextDisplay title (showDoc (dgn_sign dgnode) "")
c30231257d9116b514dce02703a515fe21cd427dTill Mossakowski Nothing -> nodeErr descr
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder fetches the theory from a node inside the IO Monad
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder (added by KL based on code in getTheoryOfNode) -}
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaederlookupTheoryOfNode :: IORef LibEnv -> Descr -> DGraphAndAGraphNode ->
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder DGraph -> IO (Res.Result (Node,G_theory))
1f2c732265a1292f0d7c51a4a7ca6be5dd370df6cmaederlookupTheoryOfNode proofStatusRef descr dgAndabstrNodeMap _ = do
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder libEnv <- readIORef proofStatusRef
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartist (ln, node) <-
3ec3a22fe2b9c38a3575c98a82b4e3f988af64a6Eugen Kuksa maybeToResult nullRange ("Node "++show descr++" not found")
4c872eeb600fe8479dbda395405cf13c3d573c24Soeren D. Schulze $ InjMap.lookupWithB descr dgAndabstrNodeMap
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder gth <- computeTheory libEnv ln node
bc263f610d20a9cd3014ddfca903026127fa0d48Christian Maeder return (node, gth)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder{- | outputs the local axioms of a node in a window;
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maederused by the node menu defined in initializeGraph-}
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaedergetLocalAxOfNode :: GInfo -> Descr -> DGraphAndAGraphNode -> DGraph -> IO ()
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaedergetLocalAxOfNode _ descr dgAndabstrNodeMap dgraph = do
726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowski case InjMap.lookupWithB descr dgAndabstrNodeMap of
987bd66ac5bc367e2bbe50ce2b6355993fb335d9cmaeder Just (_, node) ->
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder let dgnode = lab' (contextDG dgraph node) in
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder if isDGRef dgnode then createTextDisplay
c30231257d9116b514dce02703a515fe21cd427dTill Mossakowski ("Local Axioms of "++ showName (dgn_name dgnode))
427ff3172ae2dfebe3c8fc972735158999997e8aChristian Maeder "no local axioms (reference node to other library)"
3490b73f69b58ab742417b0867d0e2d4a7778cc0Christian Maeder else displayTheory "Local Axioms" node dgraph $ dgn_theory dgnode
59aa5703ac7f3b99e97cd5926e77088b256c5f40Christian Maeder Nothing -> nodeErr descr
987bd66ac5bc367e2bbe50ce2b6355993fb335d9cmaeder{- | outputs the theory of a node in a window;
726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowskiused by the node menu defined in initializeGraph-}
beff4152e9f0fe90885458d1a1733b183a2a8816Christian MaedergetTheoryOfNode :: GInfo -> Descr -> DGraphAndAGraphNode -> DGraph -> IO ()
beff4152e9f0fe90885458d1a1733b183a2a8816Christian MaedergetTheoryOfNode gInfo descr dgAndabstrNodeMap dgraph = do
7968d3a131e5a684ec1ff0c6d88aae638549153dChristian Maeder r <- lookupTheoryOfNode (libEnvIORef gInfo) descr dgAndabstrNodeMap dgraph
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder showDiags (gi_hetcatsOpts gInfo) ds
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus Luettich (Just (n, gth)) ->
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder (showName $ dgn_name $ lab' (contextDG dgraph n))
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder (addHasInHidingWarning dgraph n)
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder _ -> return ()
beff4152e9f0fe90885458d1a1733b183a2a8816Christian MaederdisplayTheory :: String -> Node -> DGraph -> G_theory -> IO ()
beff4152e9f0fe90885458d1a1733b183a2a8816Christian MaederdisplayTheory ext node dgraph gth =
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder (showName $ dgn_name $ lab' (contextDG dgraph node))
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder{- | translate the theory of a node in a window;
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maederused by the node menu defined in initializeGraph-}
78c294da55788b25e175180168371c9536a6d440Christian MaedertranslateTheoryOfNode :: GInfo -> Descr -> DGraphAndAGraphNode -> DGraph
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedertranslateTheoryOfNode gInfo@(GInfo {gi_hetcatsOpts = opts})
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder descr dgAndabstrNodeMap dgraph = do
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder libEnv <- readIORef $ libEnvIORef gInfo
78c294da55788b25e175180168371c9536a6d440Christian Maeder (ln, node) <-
bc263f610d20a9cd3014ddfca903026127fa0d48Christian Maeder maybeToResult nullRange ("Node "++show descr++" not found")
511284753313165e629cedf508752d6818ccc4d2Christian Maeder $ InjMap.lookupWithB descr dgAndabstrNodeMap
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder th <- computeTheory libEnv ln node
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder return (node,th) ) of
78c294da55788b25e175180168371c9536a6d440Christian Maeder Res.Result [] (Just (node,th)) -> do
78c294da55788b25e175180168371c9536a6d440Christian Maeder Res.Result ds _ <- runResultT(
78c294da55788b25e175180168371c9536a6d440Christian Maeder do G_theory lid sign _ sens _ <- return th
78c294da55788b25e175180168371c9536a6d440Christian Maeder -- find all comorphism paths starting from lid
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder let paths = findComorphismPaths logicGraph (sublogicOfTh th)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder -- let the user choose one
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder sel <- lift $ listBox "Choose a logic translation"
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder (map show paths)
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder i <- case sel of
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder Just j -> return j
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder _ -> liftR $ fail "no logic translation chosen"
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder Comorphism cid <- return (paths!!i)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder -- adjust lid's
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder let lidS = sourceLogic cid
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder lidT = targetLogic cid
8865728716566f42fa73e7e0bc080ba3225df764Christian Maeder sign' <- coerceSign lid lidS "" sign
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder sens' <- coerceThSens lid lidS "" sens
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder -- translate theory along chosen comorphism
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder (sign'',sens1) <-
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder liftR $ wrapMapTheory cid (plainSign sign', toNamedList sens')
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder lift $ GUI.HTkUtils.displayTheoryWithWarning
dff1de7ad15d1582e25d636c3724dd202874897fChristian Maeder "Translated Theory"
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder (showName $ dgn_name $ lab' (contextDG dgraph node))
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder (addHasInHidingWarning dgraph node)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder (G_theory lidT (mkExtSign sign'') 0 (toThSens sens1) 0)
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder showDiags opts ds
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder Res.Result ds _ -> showDiags opts ds
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder{- | outputs the sublogic of a node in a window;
60e6795dd310e10194e12bb660575aadf941328bEugen Kuksaused by the node menu defined in initializeGraph -}
60e6795dd310e10194e12bb660575aadf941328bEugen KuksagetSublogicOfNode :: IORef LibEnv -> Descr -> DGraphAndAGraphNode
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder -> DGraph -> IO()
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian MaedergetSublogicOfNode proofStatusRef descr dgAndabstrNodeMap dgraph = do
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder libEnv <- readIORef proofStatusRef
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder case InjMap.lookupWithB descr dgAndabstrNodeMap of
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder Just (ln, node) ->
91ba5d95b2472cb075646b6120a559dc6581a867Christian Maeder let dgnode = lab' (contextDG dgraph node)
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder name = if isDGRef dgnode then emptyNodeName
91ba5d95b2472cb075646b6120a559dc6581a867Christian Maeder else dgn_name dgnode
d1c667fd9445963d9d31e2cf5d0ead15e77082a4cmaeder in case computeTheory libEnv ln node of
d1c667fd9445963d9d31e2cf5d0ead15e77082a4cmaeder Res.Result _ (Just th) ->
d1c667fd9445963d9d31e2cf5d0ead15e77082a4cmaeder let logstr = show $ sublogicOfTh th
d1c667fd9445963d9d31e2cf5d0ead15e77082a4cmaeder title = "Sublogic of "++showName name
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa in createTextDisplay title logstr [HTk.size(30,10)]
d1c667fd9445963d9d31e2cf5d0ead15e77082a4cmaeder error $ "Could not compute theory for sublogic computation: "
d1c667fd9445963d9d31e2cf5d0ead15e77082a4cmaeder ++ concatMap show ds
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder Nothing -> nodeErr descr
a31430de8b0632d29f42634d6395e982bf31b14dChristian Maeder-- | prints the origin of the node
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian MaedershowOriginOfNode :: Descr -> DGraphAndAGraphNode -> DGraph -> IO()
f03420e44d8204b2945edaab5c70a84e7c381892Christian MaedershowOriginOfNode descr dgAndabstrNodeMap dgraph =
d1c667fd9445963d9d31e2cf5d0ead15e77082a4cmaeder case InjMap.lookupWithB descr dgAndabstrNodeMap of
d1c667fd9445963d9d31e2cf5d0ead15e77082a4cmaeder Just (_, node) ->
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder let dgnode = lab' (contextDG dgraph node) in
91ba5d95b2472cb075646b6120a559dc6581a867Christian Maeder if isDGRef dgnode then error "showOriginOfNode: no DGNode" else
dff1de7ad15d1582e25d636c3724dd202874897fChristian Maeder let title = "Origin of node "++ showName (dgn_name dgnode)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder in createTextDisplay title
dff1de7ad15d1582e25d636c3724dd202874897fChristian Maeder (showDoc (dgn_origin dgnode) "") [HTk.size(30,10)]
91ba5d95b2472cb075646b6120a559dc6581a867Christian Maeder Nothing -> nodeErr descr
dff1de7ad15d1582e25d636c3724dd202874897fChristian Maeder-- | Show proof status of a node
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian MaedershowProofStatusOfNode :: GInfo -> Descr -> DGraphAndAGraphNode -> DGraph
46c318705d1532d90572abf9ee869016583d985bTill MossakowskishowProofStatusOfNode _ descr dgAndabstrNodeMap dgraph =
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder case InjMap.lookupWithB descr dgAndabstrNodeMap of
d81905a5b924415c524d702df26204683c82c12eChristian Maeder Just (_, node) ->
96ae1a1d2197d0e0d5b80da2474b64c456feb1b0Christian Maeder do let dgnode = lab' (contextDG dgraph node)
96ae1a1d2197d0e0d5b80da2474b64c456feb1b0Christian Maeder let stat = showStatusAux dgnode
f03420e44d8204b2945edaab5c70a84e7c381892Christian Maeder let title = "Proof status of node "++showName (dgn_name dgnode)
f03420e44d8204b2945edaab5c70a84e7c381892Christian Maeder createTextDisplay title stat [HTk.size(105,55)]
f03420e44d8204b2945edaab5c70a84e7c381892Christian Maeder Nothing -> nodeErr descr
d1c667fd9445963d9d31e2cf5d0ead15e77082a4cmaedershowStatusAux :: DGNodeLab -> String
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian MaedershowStatusAux dgnode =
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder case dgn_theory dgnode of
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder G_theory _ _ _ sens _ ->
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder let goals = OMap.filter (not . isAxiom) sens
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder (proven,open) = OMap.partition isProvenSenStatus goals
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder in "Proven proof goals:\n"
0b13f102310e03a20b38c870b5acb88712f316a4Christian Maeder ++ showDoc proven ""
0b13f102310e03a20b38c870b5acb88712f316a4Christian Maeder ++ if not $ hasOpenConsStatus True dgnode
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder then showDoc (dgn_cons_status dgnode)
f03420e44d8204b2945edaab5c70a84e7c381892Christian Maeder "is the conservativity status of this node"
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder ++ "\nOpen proof goals:\n"
818b228955ef40dd5a253bd942dd6ab8779ed713Christian Maeder ++ showDoc open ""
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder ++ if hasOpenConsStatus False dgnode
bbba6dd86153aacb0f662b182b128df0eb09fd54Christian Maeder then showDoc (dgn_cons_status dgnode)
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder "should be the conservativity status of this node"
33fcc19ef2b59493b4e91eebf701df95fd230765Christian Maeder-- | start local theorem proving or consistency checking at a node
d4ebd9e5adc974cfa2bdf4bdd155e07be0e26f75Christian MaederproveAtNode :: Bool -> GInfo -> Descr -> DGraphAndAGraphNode -> DGraph -> IO ()
0d79ea4ed8512a802ecb6645edac141e0fbcee3fChristian MaederproveAtNode checkCons
9ee80c455784287a8b5e1b6bac1f8efa6a2f4bb3cmaeder gInfo@(GInfo { libEnvIORef = ioRefProofStatus
9ee80c455784287a8b5e1b6bac1f8efa6a2f4bb3cmaeder , gi_LIB_NAME = ln
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder dgAndabstrNodeMap
dff1de7ad15d1582e25d636c3724dd202874897fChristian Maeder case InjMap.lookupWithB descr dgAndabstrNodeMap of
3490b73f69b58ab742417b0867d0e2d4a7778cc0Christian Maeder Just libNode -> do
7968d3a131e5a684ec1ff0c6d88aae638549153dChristian Maeder let (node, dgn) = labNode' (contextDG dgraph $ snd libNode)
7968d3a131e5a684ec1ff0c6d88aae638549153dChristian Maeder (dgraph',dgn') <- case hasLock dgn of
3490b73f69b58ab742417b0867d0e2d4a7778cc0Christian Maeder True -> return (dgraph, dgn)
78c294da55788b25e175180168371c9536a6d440Christian Maeder lockGlobal gInfo
1f2c732265a1292f0d7c51a4a7ca6be5dd370df6cmaeder le <- readIORef ioRefProofStatus
ab2f38d9cd1249f6bc9cc5b838dc2fcd76189c0fChristian Maeder (dgraph',dgn') <- initLocking (lookupDGraph ln le) (node, dgn)
974b0baababf2878820de073b8fad8db68bef08aDominik Luecke writeIORef ioRefProofStatus $ Map.insert ln dgraph' le
8d780c893d6df5dab3dcc7d8444b7517f6547f11Christian Maeder unlockGlobal gInfo
8d780c893d6df5dab3dcc7d8444b7517f6547f11Christian Maeder return (dgraph',dgn')
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder locked <- tryLockLocal dgn'
083bc1972a66d73749760eab3a90bf4eb9ca7951Christian Maeder case locked of
bc263f610d20a9cd3014ddfca903026127fa0d48Christian Maeder False -> createTextDisplay "Error" "Proofwindow already open"
966519955f5f7111abac20118563132b9dd41165Christian Maeder let action = (do
dff1de7ad15d1582e25d636c3724dd202874897fChristian Maeder le <- readIORef ioRefProofStatus
dff1de7ad15d1582e25d636c3724dd202874897fChristian Maeder guiMVar <- newMVar Nothing
00df6fd583c19393fa141d5a0e21ac74c7bf5b19Christian Maeder res <- basicInferenceNode checkCons logicGraph libNode
dff1de7ad15d1582e25d636c3724dd202874897fChristian Maeder ln guiMVar le
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder runProveAtNode gInfo (node, dgn') res)
0ae7a79e865d4a6022d705d160530682b3c1f825Christian Maeder case checkCons || not (hasIncomingHidingEdge dgraph' $ snd libNode) of
f03420e44d8204b2945edaab5c70a84e7c381892Christian Maeder True -> action
0ae7a79e865d4a6022d705d160530682b3c1f825Christian Maeder False -> GUI.HTkUtils.createInfoDisplayWithTwoButtons "Warning"
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder "This node has incoming hiding links!!!" "Prove anyway"
34d14197eb3dd643a8e6ef3ed8cba5629528e97fAivaras Jakubauskas unlockLocal dgn'
34d14197eb3dd643a8e6ef3ed8cba5629528e97fAivaras Jakubauskas Nothing -> nodeErr descr
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederrunProveAtNode :: GInfo -> LNode DGNodeLab -> Res.Result LibEnv -> IO ()
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaederrunProveAtNode gInfo@(GInfo {gi_LIB_NAME = ln}) (v,_)
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder (Res.Result {maybeResult = mle}) = case mle of
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder Just le -> case matchDG v $ lookupDGraph ln le of
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder (Just(_,_,dgn,_), _) -> proofMenu gInfo (mergeDGNodeLab gInfo (v,dgn))
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder _ -> error $ "mergeDGNodeLab no such node: " ++ show v
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder Nothing -> return ()
d1c667fd9445963d9d31e2cf5d0ead15e77082a4cmaedermergeDGNodeLab :: GInfo -> LNode DGNodeLab -> LibEnv -> IO (Res.Result LibEnv)
01a143ff12e858a18437e18aab76b32f5bbb18c4cmaedermergeDGNodeLab (GInfo{gi_LIB_NAME = ln}) (v, new_dgn) le = do
d1c667fd9445963d9d31e2cf5d0ead15e77082a4cmaeder let dg = lookupDGraph ln le
d1c667fd9445963d9d31e2cf5d0ead15e77082a4cmaeder le' <- case matchDG v dg of
d1c667fd9445963d9d31e2cf5d0ead15e77082a4cmaeder (Just(p, _, old_dgn, s), g) -> do
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder theory <- joinG_sentences (dgn_theory old_dgn) $ dgn_theory new_dgn
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder new_dgn' = old_dgn{dgn_theory = theory}
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder dg' = addToProofHistoryDG ([],[SetNodeLab old_dgn (v, new_dgn')]) $
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder g{dgBody = (p, v, new_dgn', s) & (dgBody g)}
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder return $ Map.insert ln dg' le
96ae1a1d2197d0e0d5b80da2474b64c456feb1b0Christian Maeder _ -> error $ "mergeDGNodeLab no such node: " ++ show v
96ae1a1d2197d0e0d5b80da2474b64c456feb1b0Christian Maeder return Res.Result { diags = [], maybeResult = Just le'}
96ae1a1d2197d0e0d5b80da2474b64c456feb1b0Christian Maeder-- | print the id of the edge
96ae1a1d2197d0e0d5b80da2474b64c456feb1b0Christian MaedershowIDOfEdge :: Descr -> Maybe (LEdge DGLinkLab) -> IO ()
96ae1a1d2197d0e0d5b80da2474b64c456feb1b0Christian MaedershowIDOfEdge _ (Just (_, _, linklab)) =
96ae1a1d2197d0e0d5b80da2474b64c456feb1b0Christian Maeder createTextDisplay "ID of Edge" (show $ dgl_id linklab) [HTk.size(30,10)]
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedershowIDOfEdge descr Nothing =
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder createTextDisplay "Error"
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder ("edge " ++ show descr ++ " has no corresponding edge"
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder ++ "in the development graph") [HTk.size(30,10)]
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder-- | print the morphism of the edge
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian MaedershowMorphismOfEdge :: Descr -> Maybe (LEdge DGLinkLab) -> IO ()
fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan PascanushowMorphismOfEdge _ (Just (_,_,linklab)) =
fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan Pascanu createTextDisplay "Signature morphism"
fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan Pascanu (showDoc (dgl_morphism linklab) "" ++ hidingMorph)
fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan Pascanu hidingMorph = case dgl_type linklab of
9308cb2aebeae23f49713896e6d7028b0ac0f83enotanartist HidingThm morph _ -> "\n ++++++ \n"
2360728d4185c0c04279c999941c64d36626af79Christian Maeder ++ showDoc morph ""
fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan PascanushowMorphismOfEdge descr Nothing =
fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan Pascanu createTextDisplay "Error"
66a774f13272fde036481edd2298081ab3d04678Razvan Pascanu ("edge " ++ show descr ++ " has no corresponding edge"
9308cb2aebeae23f49713896e6d7028b0ac0f83enotanartist ++ "in the development graph") [HTk.size(30,10)]
66a774f13272fde036481edd2298081ab3d04678Razvan Pascanu-- | print the origin of the edge
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian MaedershowOriginOfEdge :: Descr -> Maybe (LEdge DGLinkLab) -> IO ()
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian MaedershowOriginOfEdge _ (Just (_,_,linklab)) =
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder createTextDisplay "Origin of link"
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder (showDoc (dgl_origin linklab) "") [HTk.size(30,10)]
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian MaedershowOriginOfEdge descr Nothing =
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder createTextDisplay "Error"
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder ("edge " ++ show descr ++ " has no corresponding edge"
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder ++ "in the development graph") [HTk.size(30,10)]
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- | print the proof base of the edge
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaedershowProofStatusOfThm :: Descr -> Maybe (LEdge DGLinkLab) -> IO ()
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaedershowProofStatusOfThm _ (Just ledge) =
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder createTextSaveDisplay "Proof Status" "proofstatus.txt"
0ea2cddb8715a770e646895e16b7b8085f49167cChristian Maeder (showDoc (getProofStatusOfThm ledge) "\n")
0ea2cddb8715a770e646895e16b7b8085f49167cChristian MaedershowProofStatusOfThm descr Nothing =
7245138e91992b96b153b8ac527e263d9dc8ff5bChristian Maeder -- why putStrLn here and no createTextDisplay elsewhere with this message
7245138e91992b96b153b8ac527e263d9dc8ff5bChristian Maeder putStrLn ("edge " ++ show descr ++ " has no corresponding edge"
7245138e91992b96b153b8ac527e263d9dc8ff5bChristian Maeder ++ "in the development graph")
7245138e91992b96b153b8ac527e263d9dc8ff5bChristian Maeder-- | check conservativity of the edge
0ea2cddb8715a770e646895e16b7b8085f49167cChristian MaedercheckconservativityOfEdge :: Descr -> GInfo -> Maybe (LEdge DGLinkLab) -> IO()
7968d3a131e5a684ec1ff0c6d88aae638549153dChristian MaedercheckconservativityOfEdge _ gInfo
7968d3a131e5a684ec1ff0c6d88aae638549153dChristian Maeder (Just (source,target,linklab)) = do
7968d3a131e5a684ec1ff0c6d88aae638549153dChristian Maeder libEnv <- readIORef $ libEnvIORef gInfo
7968d3a131e5a684ec1ff0c6d88aae638549153dChristian Maeder let dgraph = lookupDGraph (gi_LIB_NAME gInfo) libEnv
a461314c811f4187dff85c8be079a41b2f13f176Christian Maeder dgtar = lab' (contextDG dgraph target)
a461314c811f4187dff85c8be079a41b2f13f176Christian Maeder if isDGRef dgtar then error "checkconservativityOfEdge: no DGNode" else do
a461314c811f4187dff85c8be079a41b2f13f176Christian Maeder G_theory lid _ _ sens _ <- return $ dgn_theory dgtar
a461314c811f4187dff85c8be079a41b2f13f176Christian Maeder GMorphism cid _ _ morphism2 _ <- return $ dgl_morphism linklab
a461314c811f4187dff85c8be079a41b2f13f176Christian Maeder morphism2' <- coerceMorphism (targetLogic cid) lid
a461314c811f4187dff85c8be079a41b2f13f176Christian Maeder "checkconservativityOfEdge" morphism2
0130083f314580170af1195037be3325f125fbceChristian Maeder let th = case computeTheory libEnv (gi_LIB_NAME gInfo) source of
0130083f314580170af1195037be3325f125fbceChristian Maeder Res.Result _ (Just th1) -> th1
c770b05f3d85f8eeb25ba15f7192044f9dd534ddSoeren D. Schulze _ -> error "checkconservativityOfEdge: computeTheory"
c770b05f3d85f8eeb25ba15f7192044f9dd534ddSoeren D. Schulze G_theory lid1 sign1 _ sens1 _ <- return th
c770b05f3d85f8eeb25ba15f7192044f9dd534ddSoeren D. Schulze sign2 <- coerceSign lid1 lid "checkconservativityOfEdge.coerceSign" sign1
c770b05f3d85f8eeb25ba15f7192044f9dd534ddSoeren D. Schulze sens2 <- coerceThSens lid1 lid "" sens1
c770b05f3d85f8eeb25ba15f7192044f9dd534ddSoeren D. Schulze conservativityCheck lid
0130083f314580170af1195037be3325f125fbceChristian Maeder (plainSign sign2, toNamedList sens2)
0130083f314580170af1195037be3325f125fbceChristian Maeder morphism2' $ toNamedList sens
0130083f314580170af1195037be3325f125fbceChristian Maeder showRes = case res of
0130083f314580170af1195037be3325f125fbceChristian Maeder Just(Just True) -> "The link is conservative"
0130083f314580170af1195037be3325f125fbceChristian Maeder Just(Just False) -> "The link is not conservative"
0130083f314580170af1195037be3325f125fbceChristian Maeder _ -> "Could not determine whether link is conservative"
0130083f314580170af1195037be3325f125fbceChristian Maeder myDiags = unlines (map show ds)
057b3bffc58757a98e8e7c1aeaf5cbbc986b3117Christian Maeder createTextDisplay "Result of conservativity check"
3bcd9d942601d59dd55a6069d8b2d1c33d7ced0eChristian Maeder (showRes ++ "\n" ++ myDiags) [HTk.size(50,50)]
057b3bffc58757a98e8e7c1aeaf5cbbc986b3117Christian MaedercheckconservativityOfEdge descr _ Nothing =
c770b05f3d85f8eeb25ba15f7192044f9dd534ddSoeren D. Schulze createTextDisplay "Error"
c770b05f3d85f8eeb25ba15f7192044f9dd534ddSoeren D. Schulze ("edge " ++ show descr ++ " has no corresponding edge "
c770b05f3d85f8eeb25ba15f7192044f9dd534ddSoeren D. Schulze ++ "in the development graph") [HTk.size(30,10)]
9d6562465b41f17c7967d4e5678f34811d958cb2Christian MaedergetProofStatusOfThm :: (LEdge DGLinkLab) -> ThmLinkStatus
9d6562465b41f17c7967d4e5678f34811d958cb2Christian MaedergetProofStatusOfThm (_,_,label) =
daec53c285f692c56db0cefe16061b46ba602cf0Christian Maeder case (dgl_type label) of
daec53c285f692c56db0cefe16061b46ba602cf0Christian Maeder (LocalThm proofStatus _ _) -> proofStatus
daec53c285f692c56db0cefe16061b46ba602cf0Christian Maeder (GlobalThm proofStatus _ _) -> proofStatus
daec53c285f692c56db0cefe16061b46ba602cf0Christian Maeder (HidingThm _ proofStatus) -> proofStatus -- richtig?
daec53c285f692c56db0cefe16061b46ba602cf0Christian Maeder _ -> error "the given edge is not a theorem"
daec53c285f692c56db0cefe16061b46ba602cf0Christian Maeder{- | converts the nodes of the development graph, if it has any,
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maederand returns the resulting conversion maps
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maederif the graph is empty the conversion maps are returned unchanged-}
daec53c285f692c56db0cefe16061b46ba602cf0Christian MaederconvertNodes :: ConversionMaps -> Descr -> GraphInfo -> DGraph
daec53c285f692c56db0cefe16061b46ba602cf0Christian Maeder -> LIB_NAME -> IO ConversionMaps
daec53c285f692c56db0cefe16061b46ba602cf0Christian MaederconvertNodes convMaps descr grInfo dgraph libname
daec53c285f692c56db0cefe16061b46ba602cf0Christian Maeder | isEmptyDG dgraph = return convMaps
daec53c285f692c56db0cefe16061b46ba602cf0Christian Maeder | otherwise = convertNodesAux convMaps
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder (labNodesDG dgraph)
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder{- | auxiliary function for convertNodes if the given list of nodes is
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maederemtpy, it returns the conversion maps unchanged otherwise it adds the
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maederconverted first node to the abstract graph and to the affected
3bcd9d942601d59dd55a6069d8b2d1c33d7ced0eChristian Maederconversion maps and afterwards calls itself with the remaining node
0a64bfd28dff15bc93e1f7a86e0a8052e879636dChristian MaederconvertNodesAux :: ConversionMaps -> Descr -> GraphInfo ->
0a64bfd28dff15bc93e1f7a86e0a8052e879636dChristian Maeder [LNode DGNodeLab] -> LIB_NAME -> IO ConversionMaps
0a64bfd28dff15bc93e1f7a86e0a8052e879636dChristian MaederconvertNodesAux convMaps _ _ [] _ = return convMaps
0a64bfd28dff15bc93e1f7a86e0a8052e879636dChristian MaederconvertNodesAux convMaps descr grInfo ((node,dgnode) : lNodes) libname =
0a64bfd28dff15bc93e1f7a86e0a8052e879636dChristian Maeder do let nodetype = getDGNodeType dgnode
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder AGV.Result newDescr _ <- addnode descr
0b13f102310e03a20b38c870b5acb88712f316a4Christian Maeder (getDGNodeName dgnode)
0b13f102310e03a20b38c870b5acb88712f316a4Christian Maeder convertNodesAux convMaps
0b13f102310e03a20b38c870b5acb88712f316a4Christian Maeder { dgAndabstrNode = InjMap.insert (libname, node) newDescr
0b13f102310e03a20b38c870b5acb88712f316a4Christian Maeder (dgAndabstrNode convMaps)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder } descr grInfo lNodes libname
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder{- | converts the edges of the development graph
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederworks the same way as convertNods does-}
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederconvertEdges :: ConversionMaps -> Descr -> GraphInfo -> DGraph
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder -> LIB_NAME -> IO ConversionMaps
2353f65833a3da763392f771223250cd50b8d873Christian MaederconvertEdges convMaps descr grInfo dgraph libname
2353f65833a3da763392f771223250cd50b8d873Christian Maeder | isEmptyDG dgraph = return convMaps
9308cb2aebeae23f49713896e6d7028b0ac0f83enotanartist | otherwise = convertEdgesAux convMaps
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder (labEdgesDG dgraph)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | auxiliary function for convertEges
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederconvertEdgesAux :: ConversionMaps -> Descr -> GraphInfo ->
9308cb2aebeae23f49713896e6d7028b0ac0f83enotanartist [LEdge DGLinkLab] -> LIB_NAME -> IO ConversionMaps
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederconvertEdgesAux convMaps _ _ [] _ = return convMaps
2353f65833a3da763392f771223250cd50b8d873Christian MaederconvertEdgesAux convMaps descr grInfo (ledge@(src,tar,edgelab) : lEdges)
00df6fd583c19393fa141d5a0e21ac74c7bf5b19Christian Maeder do let srcnode = InjMap.lookupWithA (libname,src) (dgAndabstrNode convMaps)
00df6fd583c19393fa141d5a0e21ac74c7bf5b19Christian Maeder tarnode = InjMap.lookupWithA (libname,tar) (dgAndabstrNode convMaps)
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian Maeder case (srcnode, tarnode) of
528539f3d544c24afe14e979fe51f03e50aa6e9cChristian Maeder (Just s, Just t) -> do
0ae7a79e865d4a6022d705d160530682b3c1f825Christian Maeder AGV.Result newDescr msg <- addlink descr (getDGLinkType edgelab)
863d4b011d04907325f3eed8e89975e38603cb05Christian Maeder "" (Just ledge) s t grInfo
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder Nothing -> return ()
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder Just err -> fail err
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder newConvMaps <- convertEdgesAux convMaps
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder { dgAndabstrEdge = InjMap.insert (libname,
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder (src, tar, showDoc edgelab ""))
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder newDescr (dgAndabstrEdge convMaps)
59a10395caff224b2ec541f94dac5082a506c00fChristian Maeder } descr grInfo lEdges libname
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder return newConvMaps
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder _ -> error "Cannot find nodes"
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder-- | show library referened by a DGRef node (=node drawn as a box)
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedershowReferencedLibrary :: Descr -> GInfo -> ConvFunc -> LibFunc
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder -> IO (Descr, GraphInfo, ConversionMaps)
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedershowReferencedLibrary
2353f65833a3da763392f771223250cd50b8d873Christian Maeder descr gInfo@(GInfo { libEnvIORef = ioRefProofStatus
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder , conversionMapsIORef = convRef}) convGraph showLib = do
9308cb2aebeae23f49713896e6d7028b0ac0f83enotanartist convMaps <- readIORef convRef
2353f65833a3da763392f771223250cd50b8d873Christian Maeder libname2dgMap <- readIORef ioRefProofStatus
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder case InjMap.lookupWithB descr (dgAndabstrNode convMaps) of
12aef5992d3af07dee81a4e02cf4be65a83f28bcChristian Maeder Just (libname,node) ->
12aef5992d3af07dee81a4e02cf4be65a83f28bcChristian Maeder case Map.lookup libname libname2dgMap of
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder Just dgraph ->
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder do let (_, refNode) = labNode' (contextDG dgraph node)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder refLibname = if isDGRef refNode then dgn_libname refNode
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder else error "showReferencedLibrary"
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder case Map.lookup refLibname libname2dgMap of
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder gInfo' <- copyGInfo gInfo
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder (gid,gv,cm) <- convGraph (gInfo'{gi_LIB_NAME = refLibname})
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder "development graph" showLib
057b3bffc58757a98e8e7c1aeaf5cbbc986b3117Christian Maeder deactivateGraphWindow gid gv
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder redisplay gid gv
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder hideNodes gInfo'
057b3bffc58757a98e8e7c1aeaf5cbbc986b3117Christian Maeder layoutImproveAll gid gv
502483734c83d0bf1eadcc94113d0362f8713784Christian Maeder showTemporaryMessage gid gv "Development Graph initialized."
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder activateGraphWindow gid gv
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa return (gid,gv,cm)
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa Nothing -> error $ "The referenced library ("
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa ++ show refLibname
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa ++ ") is unknown"
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa Nothing -> error $ "Selected node belongs to unknown library: "
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa ++ show libname
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder error $ "there is no node with the descriptor " ++ show descr
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder-- | prune displayed graph to subtree of selected node
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedershowJustSubtree :: Descr -> Descr -> GInfo
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder -> IO (Descr, [[Node]], Maybe String)
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian MaedershowJustSubtree descr abstractGraph
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder (GInfo {libEnvIORef = ioRefProofStatus,
96ae1a1d2197d0e0d5b80da2474b64c456feb1b0Christian Maeder conversionMapsIORef = convRef,
96ae1a1d2197d0e0d5b80da2474b64c456feb1b0Christian Maeder visibleNodesIORef = visibleNodesRef,
60e6795dd310e10194e12bb660575aadf941328bEugen Kuksa gi_GraphInfo = actGraphInfo}) = do
afb32b54f3e87b51c5a6242040022f497f7f20abChristian Maeder convMaps <- readIORef convRef
60e6795dd310e10194e12bb660575aadf941328bEugen Kuksa libname2dgMap <- readIORef ioRefProofStatus
60e6795dd310e10194e12bb660575aadf941328bEugen Kuksa visibleNodes <- readIORef visibleNodesRef
60e6795dd310e10194e12bb660575aadf941328bEugen Kuksa case InjMap.lookupWithB descr (dgAndabstrNode convMaps) of
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder Just (libname,parentNode) ->
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder case Map.lookup libname libname2dgMap of
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder Just dgraph ->
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder do let allNodes = getNodeDescriptors (head visibleNodes)
2353f65833a3da763392f771223250cd50b8d873Christian Maeder libname convMaps
4b1833c7d3af466e6bcba24f16304e0a78e8da87Christian Maeder dgNodesOfSubtree = nub (parentNode : getNodesOfSubtree dgraph
fba4eac6b080849889892e1e273ac4c74ddde840Christian Maeder (head visibleNodes) parentNode)
4347b243063d414f97a68b64e30a4f27a612af0aChristian Maeder -- the selected node (parentNode) shall not be hidden either,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder -- and we already know its descriptor (descr)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder nodesOfSubtree = getNodeDescriptors dgNodesOfSubtree
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder libname convMaps
2353f65833a3da763392f771223250cd50b8d873Christian Maeder nodesToHide = filter (`notElem` nodesOfSubtree) allNodes
2353f65833a3da763392f771223250cd50b8d873Christian Maeder AGV.Result eventDescr errorMsg <- hidenodes abstractGraph
9d6562465b41f17c7967d4e5678f34811d958cb2Christian Maeder nodesToHide actGraphInfo
9d6562465b41f17c7967d4e5678f34811d958cb2Christian Maeder return (eventDescr, (dgNodesOfSubtree:visibleNodes), errorMsg)
502483734c83d0bf1eadcc94113d0362f8713784Christian Maeder Nothing -> error $
9d6562465b41f17c7967d4e5678f34811d958cb2Christian Maeder "showJustSubtree: Selected node belongs to unknown library: "
9d6562465b41f17c7967d4e5678f34811d958cb2Christian Maeder ++ show libname
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder Nothing -> error $ "showJustSubtree: there is no node with the descriptor "
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder ++ show descr
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian MaedergetNodeDescriptors :: [Node] -> LIB_NAME -> ConversionMaps -> [Descr]
9d6562465b41f17c7967d4e5678f34811d958cb2Christian MaedergetNodeDescriptors [] _ _ = []
2353f65833a3da763392f771223250cd50b8d873Christian MaedergetNodeDescriptors (node:nodelist) libname convMaps =
dbc98cd8a9a829e020cfa0a9f3aff89de75caaa9Christian Maeder case InjMap.lookupWithA (libname, node) (dgAndabstrNode convMaps) of
2353f65833a3da763392f771223250cd50b8d873Christian Maeder Just descr -> descr:(getNodeDescriptors nodelist libname convMaps)
cb2044812811d66efe038d914966e04290be93faChristian Maeder Nothing -> error $ "getNodeDescriptors: There is no descriptor for dgnode "
0130083f314580170af1195037be3325f125fbceChristian MaedergetNodesOfSubtree :: DGraph -> [Node] -> Node -> [Node]
0130083f314580170af1195037be3325f125fbceChristian MaedergetNodesOfSubtree dgraph visibleNodes node =
502483734c83d0bf1eadcc94113d0362f8713784Christian Maeder concat (map (getNodesOfSubtree dgraph remainingVisibleNodes) predOfNode)
cb2044812811d66efe038d914966e04290be93faChristian Maeder ++ predOfNode
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder where predOfNode = [ n | n <- (preDG dgraph node), elem n visibleNodes]
0130083f314580170af1195037be3325f125fbceChristian Maeder remainingVisibleNodes =
0130083f314580170af1195037be3325f125fbceChristian Maeder [ n | n <- visibleNodes, notElem n predOfNode]
0130083f314580170af1195037be3325f125fbceChristian Maeder-- | apply the changes of first history item (computed by proof rules,
0130083f314580170af1195037be3325f125fbceChristian Maeder-- see folder Proofs) to the displayed development graph
0130083f314580170af1195037be3325f125fbceChristian MaederapplyChanges :: Descr -> LIB_NAME -> GraphInfo -> Descr -> IORef [[Node]]
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder -> ConversionMaps -> [([DGRule],[DGChange])]
cb2044812811d66efe038d914966e04290be93faChristian Maeder -> IO (Descr, ConversionMaps)
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian MaederapplyChanges _ _ _ eventDescr _ convMaps [] = return (eventDescr,convMaps)
0130083f314580170af1195037be3325f125fbceChristian MaederapplyChanges gid libname grInfo eventDescr ioRefVisibleNodes convMaps
502483734c83d0bf1eadcc94113d0362f8713784Christian Maeder ((_, historyElem) : _) =
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder applyChangesAux gid libname grInfo ioRefVisibleNodes (eventDescr, convMaps)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder $ removeContraryChanges historyElem
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder-- | auxiliary function for applyChanges
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian MaederapplyChangesAux :: Descr -> LIB_NAME -> GraphInfo -> IORef [[Node]]
502483734c83d0bf1eadcc94113d0362f8713784Christian Maeder -> (Descr, ConversionMaps) -> [DGChange]
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder -> IO (Descr, ConversionMaps)
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian MaederapplyChangesAux gid libname grInfo ioRefVisibleNodes
2353f65833a3da763392f771223250cd50b8d873Christian Maeder (eventDescr, convMaps) changeList =
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder case changeList of
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder [] -> return (eventDescr, convMaps)
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder changes@(_:_) -> do
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder visibleNodes <- readIORef ioRefVisibleNodes
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder (newVisibleNodes, newEventDescr, newConvMaps) <-
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder applyChangesAux2 gid libname grInfo visibleNodes
2360728d4185c0c04279c999941c64d36626af79Christian Maeder eventDescr convMaps changes
cb2044812811d66efe038d914966e04290be93faChristian Maeder writeIORef ioRefVisibleNodes newVisibleNodes
2360728d4185c0c04279c999941c64d36626af79Christian Maeder return (newEventDescr, newConvMaps)
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder-- | auxiliary function for applyChanges
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian MaederapplyChangesAux2 :: Descr -> LIB_NAME -> GraphInfo -> [[Node]] -> Descr
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder -> ConversionMaps -> [DGChange]
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder -> IO ([[Node]], Descr, ConversionMaps)
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederapplyChangesAux2 _ _ _ visibleNodes eventDescr convMaps [] =
8c8545dd3bf34fbcbc16904b65d249658f8f9efcChristian Maeder return (visibleNodes, eventDescr+1, convMaps)
8c8545dd3bf34fbcbc16904b65d249658f8f9efcChristian MaederapplyChangesAux2 gid libname grInfo visibleNodes _ convMaps (change:changes) =
8c8545dd3bf34fbcbc16904b65d249658f8f9efcChristian Maeder case change of
8c8545dd3bf34fbcbc16904b65d249658f8f9efcChristian Maeder SetNodeLab _ (node, newLab) -> do
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder let nodetype = getDGNodeType newLab
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder nodename = getDGNodeName newLab
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder dgNode = (libname, node)
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder -- ensures that the to be set node is in the graph.
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder case InjMap.lookupWithA dgNode (dgAndabstrNode convMaps) of
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder Just abstrNode -> do
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder changeNodeType gid abstrNode nodetype grInfo
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder -- if everything's all right, sets the map with the new node.
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder -- otherwise the error is shown.
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder Nothing -> do
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder let newConvMaps = convMaps
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder { dgAndabstrNode = InjMap.updateBWithA dgNode
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder descr (dgAndabstrNode convMaps) }
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder applyChangesAux2 gid libname grInfo visibleNodes
0ede68718d0fd43b5d67c233ccfb7a2b673fc9cbChristian Maeder (descr+1) newConvMaps changes
0ede68718d0fd43b5d67c233ccfb7a2b673fc9cbChristian Maeder error $ "applyChangesAux2: could not set node "
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder ++ show node ++" with name "
0ede68718d0fd43b5d67c233ccfb7a2b673fc9cbChristian Maeder ++ show nodename ++ "\n" ++ msg
502483734c83d0bf1eadcc94113d0362f8713784Christian Maeder Nothing -> error $ "applyChangesAux2: could not set node "
502483734c83d0bf1eadcc94113d0362f8713784Christian Maeder ++ show node ++ " with name "
502483734c83d0bf1eadcc94113d0362f8713784Christian Maeder ++ show nodename ++ ": " ++
502483734c83d0bf1eadcc94113d0362f8713784Christian Maeder "node does not exist in abstraction graph"
502483734c83d0bf1eadcc94113d0362f8713784Christian Maeder InsertNode (node, nodelab) -> do
502483734c83d0bf1eadcc94113d0362f8713784Christian Maeder let nodetype = getDGNodeType nodelab
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder nodename = getDGNodeName nodelab
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder addnode gid nodetype nodename grInfo
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder do let dgNode = (libname,node)
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder newVisibleNodes = map (node :) visibleNodes
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder newConvMaps = convMaps
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder { dgAndabstrNode = InjMap.insert dgNode descr
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder (dgAndabstrNode convMaps) }
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder applyChangesAux2 gid libname grInfo newVisibleNodes (descr+1)
bbba6dd86153aacb0f662b182b128df0eb09fd54Christian Maeder newConvMaps changes
7968d3a131e5a684ec1ff0c6d88aae638549153dChristian Maeder error $ "applyChangesAux2: could not add node " ++ show node
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder ++" with name " ++ show nodename ++ "\n" ++ msg
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder DeleteNode (node, nodelab) -> do
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder let nodename = getDGNodeName nodelab
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder dgnode = (libname,node)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder case InjMap.lookupWithA dgnode (dgAndabstrNode convMaps) of
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder Just abstrNode -> do
7f7460e7095628f3437b116ee78d3043d11f8febChristian Maeder AGV.Result descr err <- delnode gid abstrNode grInfo
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder Nothing -> do
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder let newVisibleNodes = map (filter (/= node)) visibleNodes
5941ba0b9a99ac98f78a89a9f3303102657e36ccChristian Maeder newConvMaps = convMaps
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder { dgAndabstrNode = InjMap.delete dgnode abstrNode
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder (dgAndabstrNode convMaps) }
5941ba0b9a99ac98f78a89a9f3303102657e36ccChristian Maeder applyChangesAux2 gid libname grInfo newVisibleNodes (descr+1)
5941ba0b9a99ac98f78a89a9f3303102657e36ccChristian Maeder newConvMaps changes
case (InjMap.lookupWithA (libname, src) dgAndabstrNodeMap,
InjMap.lookupWithA (libname, tgt) dgAndabstrNodeMap) of
AGV.Result descr err <-
{ dgAndabstrEdge = InjMap.insert dgEdge descr
case (InjMap.lookupWithA dgEdge dgAndabstrEdgeMap) of
do AGV.Result descr err <- dellink gid abstrEdge grInfo
{ dgAndabstrEdge = InjMap.delete dgEdge
-> Res.Result G_sublogics -> ConvFunc -> LibFunc -> IO ()
openTranslateGraph libEnv ln opts (Res.Result diagsSl mSublogic) convGraph
-- (see GUI.DGTranslation.getDGLogic), the process need not to go on.
Res.Result diagsR i <- runResultT ( do
Res.Result diagsTrans (Just newLibEnv) -> do
Res.Result diagsTrans Nothing ->
saveUDGraph :: GInfo -> Map.Map String (Shape value, String)
-> Map.Map String (EdgePattern EdgeValue, String) -> IO ()
-> Map.Map String (Shape value, String)
-> Map.Map String (EdgePattern EdgeValue, String) -> IO String
$ Map.toList $ nodes graph
-> Map.Map String (Shape value, String)
-> Map.Map String (EdgePattern EdgeValue, String)
(shape, color) <- case Map.lookup ntype nodemap of
-> Map.Map String (EdgePattern EdgeValue, String)
let links = Map.foldWithKey (\k a@(nid, _, _, _) b -> if nid == nodeid
link2String :: Map.Map String (EdgePattern EdgeValue, String)
(line, color) <- case Map.lookup ltype linkmap of