GraphLogic.hs revision 4e9e95ba35a68f3c767bc0b23ebf9e904e442517
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder{-# OPTIONS -cpp #-}
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaederModule : $Header$
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederDescription : Logic for manipulating the graph in the Central GUI
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaederCopyright : (c) Jorina Freya Gerken, Till Mossakowski, Uni Bremen 2002-2006
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederMaintainer : till@informatik.uni-bremen.de
43b4c41fbb07705c9df321221ab9cb9832460407Christian MaederStability : provisional
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederPortability : non-portable (imports Logic)
f2f9df2e17e70674f0bf426ed1763c973ee4cde0Christian MaederThis module provides functions for all the menus in the Hets GUI.
c9a7e6af169a2adfb92f42331cd578065ed83a2bChristian MaederThese are then assembled to the GUI in "GUI.GraphMenu".
a1ed34933c266ce85066acb0d7b20c90cb8eb213Christian Maeder , performProofAction
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder , openProofStatus
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich , saveProofStatus
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich , showReferencedLibrary
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder , getTheoryOfNode
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder , translateTheoryOfNode
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder , displaySubsortGraph
ce5b44277ea06257548ff625e928cb1290c6d297cmaeder , displayConceptGraph
bab2d88d650448628730ed3b65c9f99c52500e8cChristian Maeder , lookupTheoryOfNode
fa8878c6145f652f615a04a5e9c15a1d1327bc92cmaeder , showProofStatusOfNode
ce5b44277ea06257548ff625e928cb1290c6d297cmaeder , proveAtNode
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder , showNodeInfo
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder , showEdgeInfo
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder , checkconservativityOfEdge
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder , hideShowNames
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder , translateGraph
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maederimport Logic.Logic(conservativityCheck,map_sen, comp)
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maederimport Logic.Coerce(coerceSign, coerceMorphism)
bab2d88d650448628730ed3b65c9f99c52500e8cChristian Maederimport Static.DGTranslation(libEnv_translation)
6a2dad705deefd1b7a7e09b84fd2d75f2213be47Christian Maederimport Proofs.InferBasic(basicInferenceNode)
a7c27282e71cf4505026645f96d4f5cb8a284e32Christian Maederimport Proofs.StatusUtils(lookupHistory, removeContraryChanges)
f04e8f3ff56405901be968fd4c6e9769239f1a9bKlaus Luettichimport GUI.Taxonomy (displayConceptGraph,displaySubsortGraph)
6aea82c63ba1d2efc0329bc784a14e521469ec20Christian Maederimport GUI.DGTranslation(getDGLogic)
feca1d35123d8c31aee238c9ce79947b0bf65494Christian Maederimport qualified GUI.GraphAbstraction as GA
f5c0884429b01e74c6e658ded921fb2e16dfb478Christian Maeder#ifdef UNIVERSION2
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maederimport Reactor.InfoBus(encapsulateWaitTermAct)
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maederimport GraphConfigure
23ffcc44ca8612feccbd8fda63fa5be7ab5f9dc3Christian Maederimport InfoBus(encapsulateWaitTermAct)
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maederimport DialogWin (useHTk)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederimport qualified GUI.HTkUtils as HTk
a3c6d8e0670bf2aa71bc8e2a3b1f45d56dd65e4cChristian Maederimport qualified Common.OrderedMap as OMap
dc679edd4ca027663212afdf00926ae2ce19b555Christian Maederimport qualified Common.Lib.Rel as Rel
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederimport qualified Common.Lib.SizedList as SizedList
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maederimport Driver.WriteLibDefn(writeShATermFile)
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maederimport Driver.ReadFn(libNameToFile, readVerbose)
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maederimport Driver.AnaLib(anaLibExt, anaLib)
b568982efd0997d877286faa592d81b03c8c67b8Christian Maederimport System.Directory(getModificationTime)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederimport Data.List(partition)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederimport Data.Graph.Inductive.Graph (Node, LEdge, LNode)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederimport qualified Data.Map as Map
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder-- | Locks the global lock and runs function
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederrunAndLock :: GInfo -> IO () -> IO ()
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian MaederrunAndLock (GInfo { functionLock = lock
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder , gi_GraphInfo = actGraphInfo
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder }) function = do
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder locked <- tryPutMVar lock ()
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder case locked of
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder takeMVar lock
e6d5dbbc3308f05197868806e0b860f4f53875f1Christian Maeder $ "an other function is still working ... please wait ..."
58b96b17bf8e32c0b0d773380a5e62f992eef2bcChristian Maeder-- | Undo one step of the History
e4f4d096e5e6d60dd91c746d0e833d0ac7a29c50Christian Maederundo :: GInfo -> Bool -> IO ()
eb74267cf39e4e95f9eeb5c765f4c8dac33971b4Christian Maederundo gInfo@(GInfo { globalHist = gHist
eb74267cf39e4e95f9eeb5c765f4c8dac33971b4Christian Maeder , gi_GraphInfo = actGraph
e4f4d096e5e6d60dd91c746d0e833d0ac7a29c50Christian Maeder }) isUndo = do
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder (guHist, grHist) <- takeMVar gHist
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder case if isUndo then guHist else grHist of
8d178ae08a52d61379e6b8074f61646499bc88bbChristian Maeder GA.showTemporaryMessage actGraph "History is empty..."
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder putMVar gHist (guHist, grHist)
6cd33d6101fb1b93baa6d86fac158af18a115108Christian Maeder lns : gHist' -> do
6cd33d6101fb1b93baa6d86fac158af18a115108Christian Maeder undoDGraphs gInfo isUndo lns
6cd33d6101fb1b93baa6d86fac158af18a115108Christian Maeder putMVar gHist $ if isUndo then (gHist', reverse lns : grHist)
6cd33d6101fb1b93baa6d86fac158af18a115108Christian Maeder else (reverse lns : guHist, gHist')
b2ac5a92cf36382e8deea5661c1964566caf72b3Christian MaederundoDGraphs :: GInfo -> Bool -> [LIB_NAME] -> IO ()
ea5432ff6f61c64469b11d9352b23fef4ff152e8Christian MaederundoDGraphs g u = mapM_ $ undoDGraph g u
b2ac5a92cf36382e8deea5661c1964566caf72b3Christian MaederundoDGraph :: GInfo -> Bool -> LIB_NAME -> IO ()
7d0ee72ee91ec305408688b969c43f07b9667c80Christian MaederundoDGraph gInfo@(GInfo { libEnvIORef = ioRefProofStatus
7d0ee72ee91ec305408688b969c43f07b9667c80Christian Maeder , gi_GraphInfo = actGraph
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder }) isUndo ln = do
0e5b095a19790411e5352fa7cf57cb0388e70472Christian Maeder (if isUndo then "Un" else "Re") ++ "do last change to "
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder ++ show ln ++ "..."
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder lockGlobal gInfo
f1a913f880e409e7327b5deae95738b5448379a1Christian Maeder le <- readIORef ioRefProofStatus
f1a913f880e409e7327b5deae95738b5448379a1Christian Maeder dg = lookupDGraph ln le
f1a913f880e409e7327b5deae95738b5448379a1Christian Maeder (dg', changes) = (if isUndo then undoHistStep else redoHistStep) dg
14c56dc499da4bbeaeebeb558ceb755150ae341cChristian Maeder writeIORef ioRefProofStatus $ Map.insert ln dg' le
c9a7e6af169a2adfb92f42331cd578065ed83a2bChristian Maeder case openlock dg' of
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder Nothing -> return ()
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder Just lock -> do
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder mvar <- tryTakeMVar lock
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Nothing -> return ()
93f5b72fdb9ee734caa750b43dd79bbb590dcd73Christian Maeder Just applyHist -> do
93f5b72fdb9ee734caa750b43dd79bbb590dcd73Christian Maeder applyHist changes
328a85c807f2a95c3f147d10b05927eaf862ebebChristian Maeder putMVar lock applyHist
8fb127028cb7dd361e348a3252e33487f73428bcJonathan von Schroeder unlockGlobal gInfo
254df6f22d01eacf7c57b85729e0445747b630d9Christian Maeder-- | reloads the Library of the DevGraph
4ba08bfca0cc8d9da65397b8dfd2654fdb4c0e62Christian Maederreload :: GInfo -> IO()
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maederreload gInfo@(GInfo { libEnvIORef = ioRefProofStatus
5b818f10e11fc79def1fdd5c8a080d64a6438d87Christian Maeder , gi_LIB_NAME = ln
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers , gi_hetcatsOpts = opts
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder , gi_GraphInfo = actGraphInfo
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder lockGlobal gInfo
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder oldle <- readIORef ioRefProofStatus
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder libdeps = Rel.toList $ Rel.intransKernel $ Rel.transClosure $ Rel.fromList
0d0278c34a374b29c2d6c58b39b8b56e283d48e8Christian Maeder $ getLibDeps oldle
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder ioruplibs <- newIORef ([] :: [LIB_NAME])
3554301a34639efb6c9961a8571775d0061284c9Christian Maeder writeIORef ioruplibs []
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers reloadLibs ioRefProofStatus opts libdeps ioruplibs ln
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder unlockGlobal gInfo
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder libs <- readIORef ioruplibs
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder [] -> GA.showTemporaryMessage actGraphInfo "Reload not needed!"
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder _ -> remakeGraph gInfo
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder-- | Creates a list of all LIB_NAME pairs, which have a dependency
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian MaedergetLibDeps :: LibEnv -> [(LIB_NAME, LIB_NAME)]
3554301a34639efb6c9961a8571775d0061284c9Christian MaedergetLibDeps le =
3554301a34639efb6c9961a8571775d0061284c9Christian Maeder concat $ map (\ ln -> getDep ln le) $ Map.keys le
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder-- | Creates a list of LIB_NAME pairs for the fist argument
aded505f9b42cc38975559c2a5d175ae95de436bChristian MaedergetDep :: LIB_NAME -> LibEnv -> [(LIB_NAME, LIB_NAME)]
aded505f9b42cc38975559c2a5d175ae95de436bChristian MaedergetDep ln le = map (\ (_, x) -> (ln, dgn_libname x)) $
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder filter (isDGRef . snd) $ labNodesDG $ lookupDGraph ln le
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder-- | Reloads a library
aded505f9b42cc38975559c2a5d175ae95de436bChristian MaederreloadLib :: IORef LibEnv -> HetcatsOpts -> IORef [LIB_NAME] -> LIB_NAME
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian MaederreloadLib iorle opts ioruplibs ln = do
a14767aeac3e78ed100f5b75e210ba563ee10dbaChristian Maeder mfile <- existsAnSource opts {intype = GuessIn}
a14767aeac3e78ed100f5b75e210ba563ee10dbaChristian Maeder $ rmSuffix $ libNameToFile opts ln
a14767aeac3e78ed100f5b75e210ba563ee10dbaChristian Maeder case mfile of
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder Nothing -> return ()
3554301a34639efb6c9961a8571775d0061284c9Christian Maeder Just file -> do
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder le <- readIORef iorle
54ea981a0503c396c2923a1c06421c6235baf27fChristian Maeder mFunc <- case openlock $ lookupDGraph ln le of
54ea981a0503c396c2923a1c06421c6235baf27fChristian Maeder Just lock -> tryTakeMVar lock
54ea981a0503c396c2923a1c06421c6235baf27fChristian Maeder Nothing -> return Nothing
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder mres <- anaLibExt opts file le'
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder Just (_, newle) -> do
f9e0b18852b238ddb649d341194e05d7200d1bbeChristian Maeder uplibs <- readIORef ioruplibs
819e29dba060687cf391e444e0f6ff88c1908cc3Christian Maeder writeIORef ioruplibs $ ln:uplibs
819e29dba060687cf391e444e0f6ff88c1908cc3Christian Maeder case mFunc of
819e29dba060687cf391e444e0f6ff88c1908cc3Christian Maeder Just func -> case openlock $ lookupDGraph ln newle of
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder Just lock -> putMVar lock func
254df6f22d01eacf7c57b85729e0445747b630d9Christian Maeder Nothing -> errorDialog "Error"
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder "Reload: Can't set openlock in DevGraph"
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder Nothing -> return ()
254df6f22d01eacf7c57b85729e0445747b630d9Christian Maeder writeIORef iorle $ newle
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder errorDialog "Error" $ "Error when reloading file " ++ show file
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder-- | Reloads libraries if nessesary
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian MaederreloadLibs :: IORef LibEnv -> HetcatsOpts -> [(LIB_NAME, LIB_NAME)]
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder -> IORef [LIB_NAME] -> LIB_NAME -> IO Bool
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian MaederreloadLibs iorle opts deps ioruplibs ln = do
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder uplibs <- readIORef ioruplibs
ac34194a668399bb8ef238da77c3a09e93fb253bChristian Maeder case elem ln uplibs of
4fc9de0da898448f1d3597ebbd8c04a066464c21Christian Maeder True -> return True
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder deps' = map (snd) $ filter (\ (ln',_) -> ln == ln') deps
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder res <- mapM (reloadLibs iorle opts deps ioruplibs) deps'
0d0278c34a374b29c2d6c58b39b8b56e283d48e8Christian Maeder libupdate = foldl (\ u r -> if r then True else u) False res
0d0278c34a374b29c2d6c58b39b8b56e283d48e8Christian Maeder case libupdate of
1842453990fed8a1bd7a5ac792d7982c1d2bfcd5Christian Maeder reloadLib iorle opts ioruplibs ln
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder le <- readIORef iorle
986d3f255182539098a97ac86da9eeee5b7a72e3Christian Maeder newln:_ = filter (ln ==) $ Map.keys le
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder mfile <- existsAnSource opts $ rmSuffix $ libNameToFile opts ln
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder case mfile of
01e278bdd7dce13b9303ed3d79683d83c89d09f9Liam O'Reilly Nothing -> return False
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder Just file -> do
5ad5dffe06818a13e1632b1119fbca7881085fc1Dominik Luecke newmt <- getModificationTime file
8c812cd83569e973f10cf69a342424ceabc07af9Christian Maeder libupdate' = (getModTime $ getLIB_ID newln) < newmt
8c812cd83569e973f10cf69a342424ceabc07af9Christian Maeder case libupdate' of
1535e1d8c82db5f7e2402261983c4c2ef39f4f39Mihai Codescu False -> return False
1535e1d8c82db5f7e2402261983c4c2ef39f4f39Mihai Codescu reloadLib iorle opts ioruplibs ln
7a3fe82695aa32657693e05712f84d7f81672f2eJonathan von Schroeder-- | Deletes the old edges and nodes of the Graph and makes new ones
7a3fe82695aa32657693e05712f84d7f81672f2eJonathan von SchroederremakeGraph :: GInfo -> IO ()
05a206508bc898f87fe6ab6e069814df3c29d303Dominik LueckeremakeGraph gInfo@(GInfo { libEnvIORef = ioRefProofStatus
05a206508bc898f87fe6ab6e069814df3c29d303Dominik Luecke , gi_LIB_NAME = ln
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder , gi_GraphInfo = actGraphInfo
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder le <- readIORef ioRefProofStatus
d54cd08a4cfa26256c38d8ed12c343adbfe1a0e3Christian Maeder dgraph = lookupDGraph ln le
d54cd08a4cfa26256c38d8ed12c343adbfe1a0e3Christian Maeder showNodes gInfo
3b06e23643a9f65390cb8c1caabe83fa7e87a708Till Mossakowski convert actGraphInfo dgraph
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder hideNodes gInfo
8c812cd83569e973f10cf69a342424ceabc07af9Christian Maeder-- | Toggles to display internal node names
0b349288edfa50fdf38fda1a14e1562d03f92574Christian MaederhideShowNames :: GInfo -> Bool -> IO ()
5afff1a0f62394414c33b06141175b3ab0b117a5Christian MaederhideShowNames (GInfo { internalNamesIORef = showInternalNames
5afff1a0f62394414c33b06141175b3ab0b117a5Christian Maeder }) toggle = do
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder (intrn::InternalNames) <- readIORef showInternalNames
1b3a2f98d1cd01fc9e0591f69507e20526727559Dominik Luecke let showThem = if toggle then not $ showNames intrn else showNames intrn
f04e8f3ff56405901be968fd4c6e9769239f1a9bKlaus Luettich showItrn s = if showThem then s else ""
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder mapM_ (\(s,upd) -> upd (\_ -> showItrn s)) $ updater intrn
f8e1a1eca871a26a535a4ee7d51902ba94b1db1eChristian Maeder writeIORef showInternalNames $ intrn {showNames = showThem}
dd6f22b9dcff2695181b86372e4df03d5b96e92dKristina Sojakova-- | shows all hidden nodes and edges
005e0f0c6b0cc898003b03801158c208f3071fc5Kristina SojakovashowNodes :: GInfo -> IO ()
abf2487c3aece95c371ea89ac64319370dcb6483Klaus LuettichshowNodes gInfo@(GInfo { gi_GraphInfo = actGraphInfo
23b4e542dca35852f58d1fb3f7d9078c1de5ab06Christian Maeder hhn <- GA.hasHiddenNodes actGraphInfo
74a992bd019d3319df2f21f9d358ff06cafb5f7eMihaela Turcu GA.showTemporaryMessage actGraphInfo "Revealing hidden nodes ..."
878a5ecd6acf973907e25e5be6e4a792ea19a05eEwaryst Schulz hideShowNames gInfo False
c2e192ace9ef7cfb0e59563f1b24477b2b65cff3Dominik Dietrich GA.showTemporaryMessage actGraphInfo "No hidden nodes found ..."
9a4b469ca0a7f44a598e551a973c75195207db58Eugen Kuksa-- | hides all unnamed internal nodes that are proven
48aa0645e25883048369afc02aac3f49b14a50daChristian MaederhideNodes :: GInfo -> IO ()
01645eac73dbc789392674930adc5745c935f3a0Christian MaederhideNodes (GInfo { libEnvIORef = ioRefProofStatus
01645eac73dbc789392674930adc5745c935f3a0Christian Maeder , gi_LIB_NAME = ln
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder , gi_GraphInfo = actGraphInfo
3a9fce5398f4621558ca220c66c87cee59adc258Jonathan von Schroeder hhn <- GA.hasHiddenNodes actGraphInfo
0a03acf9fa28e6ff00f4d7c9c6acbae64cf09c56Ewaryst Schulz GA.showTemporaryMessage actGraphInfo "Nodes already hidden ..."
308834907a120fd8771e18292ed2ca9cd767c12dChristian Maeder GA.showTemporaryMessage actGraphInfo "Hiding unnamed nodes..."
308834907a120fd8771e18292ed2ca9cd767c12dChristian Maeder le <- readIORef ioRefProofStatus
7834a982096d93301a4626f444dd9ea5f9fe17eaChristian Maeder let dg = lookupDGraph ln le
1f9274bb2aa44ea236327814dce99946be52e348Felix Gabriel Mance nodes = selectNodesByType dg [DGNodeType
1f9274bb2aa44ea236327814dce99946be52e348Felix Gabriel Mance {nonRefType = NonRefType
bab2d88d650448628730ed3b65c9f99c52500e8cChristian Maeder {isProvenCons = True
8fd6a3f938496a502bc62f1923ff7c15f59acf91Christian Maeder , isInternalSpec = True}
4b4a0b61b72cf8478a5d4d5002bca9f699401363Christian Maeder , isLocallyEmpty = True}]
d62661e54e2662d53b583ae48609f5037701078dcmaeder edges = getCompressedEdges dg nodes
9f226cec9f978edaba67aee4c4e04e3d3b994b87Daniel Calegari GA.hideNodes actGraphInfo nodes edges
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder-- | selects all nodes of a type with outgoing edges
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaederselectNodesByType :: DGraph -> [DGNodeType] -> [Node]
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaederselectNodesByType dg types =
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder filter (\ n -> outDG dg n /= []) $ map fst
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder $ filter (\ (_, n) -> elem (getRealDGNodeType n) types) $ labNodesDG dg
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder-- | compresses a list of types to the highest one
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaedercompressTypes :: [DGEdgeType] -> DGEdgeType
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaedercompressTypes [] = error "compressTypes: wrong usage"
7a3fe82695aa32657693e05712f84d7f81672f2eJonathan von SchroedercompressTypes (t:[]) = t
7a3fe82695aa32657693e05712f84d7f81672f2eJonathan von SchroedercompressTypes (t1:t2:r) = case t1 > t2 of
7a3fe82695aa32657693e05712f84d7f81672f2eJonathan von Schroeder True -> compressTypes (t1:r)
1535e1d8c82db5f7e2402261983c4c2ef39f4f39Mihai Codescu False -> compressTypes (t2:r)
1535e1d8c82db5f7e2402261983c4c2ef39f4f39Mihai Codescu-- | returns a list of compressed edges
1535e1d8c82db5f7e2402261983c4c2ef39f4f39Mihai CodescugetCompressedEdges :: DGraph -> [Node] -> [(Node,Node,DGEdgeType)]
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaedergetCompressedEdges dg hidden =
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder filterDuplicates $ getShortPaths $ concat
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder $ map (\ e@(_,t,_) -> map (e:) $ getPaths dg t hidden [])
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder inEdges = filter (\ (_,t,_) -> elem t hidden)
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder $ concat $ map (outDG dg)
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder $ foldr (\ n i -> if elem n hidden
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder || elem n i then i else n:i) []
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder $ map (\ (s,_,_) -> s) $ concat $ map (innDG dg) hidden
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder-- | filter duplicate paths
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederfilterDuplicates :: [(Node,Node,DGEdgeType)]
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder -> [(Node,Node,DGEdgeType)]
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederfilterDuplicates [] = []
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaederfilterDuplicates ((s,t,et):r) = edge:filterDuplicates others
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder (same,others) = partition (\ (s',t',_) -> s == s' && t == t') r
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder edge = (s,t,compressTypes $ et:map (\ (_,_,et') -> et') same)
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder-- | returns the pahts of a given node through hidden nodes
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaedergetPaths :: DGraph -> Node -> [Node] -> [Node] -> [[LEdge DGLinkLab]]
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaedergetPaths dg node hidden seen' = case elem node hidden of
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder True -> case edges /= [] of
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder True -> concat $ map (\ e@(_,t,_) -> map (e:) $ getPaths dg t hidden seen)
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder False -> [[]]
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder seen = node:seen'
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder edges = filter (\ (_,t,_) -> notElem t seen) $ outDG dg node
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder-- | returns source and target node of a path with the compressed type
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaedergetShortPaths :: [[LEdge DGLinkLab]]
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder -> [(Node,Node,DGEdgeType)]
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaedergetShortPaths [] = []
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaedergetShortPaths (p:r) =
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder ((s,t,compressTypes $ map (\ (_,_,e) -> getRealDGLinkType e) p))
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder : getShortPaths r
5199920ca3b698b2149c8cb9d2ce2e98a280ff9dChristian Maeder (s,_,_) = head p
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder (_,t,_) = last p
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder-- | Let the user select a Node to focus
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaederfocusNode :: GInfo -> IO ()
9f85afecbd79b3df5a0bb17bd28cd0b288dc3213Kristina SojakovafocusNode GInfo { libEnvIORef = ioRefProofStatus
48aa0645e25883048369afc02aac3f49b14a50daChristian Maeder , gi_LIB_NAME = ln
9f85afecbd79b3df5a0bb17bd28cd0b288dc3213Kristina Sojakova , gi_GraphInfo = grInfo } = do
79834070d6d3c63a098e570b12fa3405c607dc70Kristina Sojakova le <- readIORef ioRefProofStatus
79834070d6d3c63a098e570b12fa3405c607dc70Kristina Sojakova idsnodes <- filterM (fmap not . GA.isHiddenNode grInfo . fst)
79834070d6d3c63a098e570b12fa3405c607dc70Kristina Sojakova $ labNodesDG $ lookupDGraph ln le
23b4e542dca35852f58d1fb3f7d9078c1de5ab06Christian Maeder selection <- listBox "Select a node to focus"
23b4e542dca35852f58d1fb3f7d9078c1de5ab06Christian Maeder $ map (\ (n, l) -> shows n " " ++ getDGNodeName l) idsnodes
23b4e542dca35852f58d1fb3f7d9078c1de5ab06Christian Maeder case selection of
8a78868bae2ec6838c87366c35c57e109154c51eChristian Maeder Just idx -> GA.focusNode grInfo $ fst $ idsnodes !! idx
8a78868bae2ec6838c87366c35c57e109154c51eChristian Maeder Nothing -> return ()
624e6701e0deb7ac6c03c0cba0190fbc5033cf93Ewaryst SchulztranslateGraph :: GInfo -> ConvFunc -> LibFunc -> IO ()
624e6701e0deb7ac6c03c0cba0190fbc5033cf93Ewaryst SchulztranslateGraph (GInfo {libEnvIORef = ioRefProofStatus,
c2e192ace9ef7cfb0e59563f1b24477b2b65cff3Dominik Dietrich gi_LIB_NAME = ln,
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Luc gi_hetcatsOpts = opts
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Luc }) convGraph showLib = do
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Luc le <- readIORef ioRefProofStatus
01645eac73dbc789392674930adc5745c935f3a0Christian Maeder openTranslateGraph le ln opts (getDGLogic le) convGraph showLib
01645eac73dbc789392674930adc5745c935f3a0Christian MaedershowLibGraph :: GInfo -> LibFunc -> IO ()
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian MaedershowLibGraph gInfo showLib = do
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder showLib gInfo
fc09e0a6af734edbd944dd8082bb51985c233b43Alexis Tsogias{- | it tries to perform the given action to the given graph.
b5da047a9a875dec3f968b6c0df96af326f90fa9Alexis Tsogias If part of the given graph is not hidden, then the action can
0a03acf9fa28e6ff00f4d7c9c6acbae64cf09c56Ewaryst Schulz be performed directly; otherwise the graph will be shown completely
0a03acf9fa28e6ff00f4d7c9c6acbae64cf09c56Ewaryst Schulz firstly, and then the action will be performed, and after that the graph
0a03acf9fa28e6ff00f4d7c9c6acbae64cf09c56Ewaryst Schulz will be hidden again.
18d370f8341357f5d6a4068f4bb6981173ece70fFelix Gabriel ManceperformProofAction :: GInfo -> IO () -> IO ()
7834a982096d93301a4626f444dd9ea5f9fe17eaChristian MaederperformProofAction gInfo@(GInfo { gi_GraphInfo = actGraphInfo
ed1b8e97e72b2e3e92edaf2eb22a4b5373d705f1Felix Gabriel Mance }) proofAction = do
ed1b8e97e72b2e3e92edaf2eb22a4b5373d705f1Felix Gabriel Mance let actionWithMessage = do
4b4a0b61b72cf8478a5d4d5002bca9f699401363Christian Maeder "Applying development graph calculus proof rule..."
4b4a0b61b72cf8478a5d4d5002bca9f699401363Christian Maeder hhn <- GA.hasHiddenNodes actGraphInfo
d62661e54e2662d53b583ae48609f5037701078dcmaeder case hhn of
d62661e54e2662d53b583ae48609f5037701078dcmaeder showNodes gInfo
9f226cec9f978edaba67aee4c4e04e3d3b994b87Daniel Calegari actionWithMessage
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder hideNodes gInfo
c70ef4c3b3a62764f715510c9fd67dde3acfe454Christian Maeder False -> actionWithMessage
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder "Development graph calculus proof rule finished."
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaedersaveProofStatus :: GInfo -> FilePath -> IO ()
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaedersaveProofStatus (GInfo { libEnvIORef = ioRefProofStatus
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder , gi_LIB_NAME = ln
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder , gi_hetcatsOpts = opts
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder }) file = encapsulateWaitTermAct $ do
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder proofStatus <- readIORef ioRefProofStatus
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder writeShATermFile file (ln, lookupHistory ln proofStatus)
67d711ed8d639b1c6e123896e7133d03911c1128Christian Maeder putIfVerbose opts 2 $ "Wrote " ++ file
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder-- | implementation of open menu, read in a proof status
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederopenProofStatus :: GInfo -> FilePath -> ConvFunc -> LibFunc
360ce9b5c746ac021944db12eb26e3df2697b8c7Christian MaederopenProofStatus gInfo@(GInfo { libEnvIORef = ioRefProofStatus
360ce9b5c746ac021944db12eb26e3df2697b8c7Christian Maeder , gi_LIB_NAME = ln
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich , gi_hetcatsOpts = opts
50c3cc2b79207355522c5b096172b3c6b7bec300Christian Maeder }) file convGraph showLib = do
f443a57f2a8e0ca3daa7431b0c89a18ba52c337aChristian Maeder mh <- readVerbose opts ln file
857992065be4ed40a72c6296b6c0aec62ab4c5b9Christian Maeder Nothing -> errorDialog "Error" $ "Could not read proof status from file '"
37a9d042e9f85a1d6e229eb80b48f93df810f155Christian Maeder let libfile = libNameToFile opts ln
7c99e334446bb97120e30e967baeeddfdd1278deKlaus Luettich m <- anaLib opts { outtypes = [] } libfile
f5c9b1e739228c2a2edf055ac419583412569683Christian Maeder Nothing -> errorDialog "Error"
f5c9b1e739228c2a2edf055ac419583412569683Christian Maeder $ "Could not read original development graph from '"
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder ++ libfile ++ "'"
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder Just (_, libEnv) -> case Map.lookup ln libEnv of
33d042fe6a9eb27a4c48f840b80838f3e7d98e34Christian Maeder Nothing -> errorDialog "Error" $ "Could not get original"
83394c6b6e6de128e71b67c9251ed7a84485d082Christian Maeder ++ "development graph for '" ++ showDoc ln "'"
fa21fba9ceb1ddf7b3efd54731a12ed8750191d8Christian Maeder Just dg -> do
fa21fba9ceb1ddf7b3efd54731a12ed8750191d8Christian Maeder lockGlobal gInfo
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder oldEnv <- readIORef ioRefProofStatus
0c355dd0b739631ee472f9a656e266be27fa4e64Christian Maeder let proofStatus = Map.insert ln
fa21fba9ceb1ddf7b3efd54731a12ed8750191d8Christian Maeder (applyProofHistory h dg) oldEnv
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder writeIORef ioRefProofStatus proofStatus
c7ec85d1103173e089aa5048fd7afb2f9b505124Klaus Luettich unlockGlobal gInfo
c7ec85d1103173e089aa5048fd7afb2f9b505124Klaus Luettich gInfo' <- copyGInfo gInfo ln
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder convGraph gInfo' "Proof Status " showLib
c7ec85d1103173e089aa5048fd7afb2f9b505124Klaus Luettich let actGraphInfo = gi_GraphInfo gInfo
33d042fe6a9eb27a4c48f840b80838f3e7d98e34Christian Maeder-- | apply a rule of the development graph calculus
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederproofMenu :: GInfo
0a5571c8adeddd27548445546491725beb224dddChristian Maeder -> (LibEnv -> IO (Res.Result LibEnv))
0a5571c8adeddd27548445546491725beb224dddChristian MaederproofMenu gInfo@(GInfo { libEnvIORef = ioRefProofStatus
0a5571c8adeddd27548445546491725beb224dddChristian Maeder , gi_LIB_NAME = ln
0a5571c8adeddd27548445546491725beb224dddChristian Maeder , gi_GraphInfo = actGraphInfo
f38b3687c5558128515e34fb85d8b466d22dc300Christian Maeder , gi_hetcatsOpts = hOpts
e112e83352048f3db8c8f93ae104193e7338c10fChristian Maeder , proofGUIMVar = guiMVar
f38b3687c5558128515e34fb85d8b466d22dc300Christian Maeder , globalHist = gHist
f38b3687c5558128515e34fb85d8b466d22dc300Christian Maeder }) proofFun = do
e642ad0e782f9bb9ba310164358220402eec8cd8Christian Maeder filled <- tryPutMVar guiMVar Nothing
f38b3687c5558128515e34fb85d8b466d22dc300Christian Maeder if not filled
f38b3687c5558128515e34fb85d8b466d22dc300Christian Maeder then readMVar guiMVar >>=
db3016fbc6065fc0d57e68c28ae280e6ac95a39aChristian Maeder (maybe (putIfVerbose hOpts 0 "proofMenu: ignored Nothing")
e112e83352048f3db8c8f93ae104193e7338c10fChristian Maeder putIfVerbose hOpts 4 $
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder "proofMenu: Ignored Proof command; " ++
ddbf07996361d7e88cf23858a8f85595fa493514Jonathan von Schroeder "maybe a proof window is still open?"
ddbf07996361d7e88cf23858a8f85595fa493514Jonathan von Schroeder lockGlobal gInfo
ddbf07996361d7e88cf23858a8f85595fa493514Jonathan von Schroeder proofStatus <- readIORef ioRefProofStatus
ddbf07996361d7e88cf23858a8f85595fa493514Jonathan von Schroeder putIfVerbose hOpts 4 "Proof started via \"Proofs\" menu"
ddbf07996361d7e88cf23858a8f85595fa493514Jonathan von Schroeder Res.Result ds res <- proofFun proofStatus
aebb0b18fe5e6ba7dd7e4c66a16a905611ef7ba9Christian Maeder putIfVerbose hOpts 4 "Analyzing result of proof"
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder Nothing -> do
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder unlockGlobal gInfo
825a1e4ca1e768de4b4883c65a6cb1dce6aa0002Christian Maeder printDiags 2 ds
825a1e4ca1e768de4b4883c65a6cb1dce6aa0002Christian Maeder Just newProofStatus -> do
825a1e4ca1e768de4b4883c65a6cb1dce6aa0002Christian Maeder let newGr = lookupDGraph ln newProofStatus
825a1e4ca1e768de4b4883c65a6cb1dce6aa0002Christian Maeder history = snd $ splitHistory (lookupDGraph ln proofStatus) newGr
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder (guHist, grHist) <- takeMVar gHist
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder doDump hOpts "PrintHistory" $ do
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder putStrLn "History"
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder print $ prettyHistory history
aebb0b18fe5e6ba7dd7e4c66a16a905611ef7ba9Christian Maeder putMVar gHist
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder (calcGlobalHistory proofStatus newProofStatus : guHist, grHist)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder applyChanges actGraphInfo $ reverse
e05fd774e0181e93963d4302303b20698603a505Christian Maeder $ flatHistory history
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder writeIORef ioRefProofStatus newProofStatus
1dfba1f850f6a43094962b459998d1ea11472461Christian Maeder unlockGlobal gInfo
1dfba1f850f6a43094962b459998d1ea11472461Christian Maeder hideShowNames gInfo False
1dfba1f850f6a43094962b459998d1ea11472461Christian Maeder mGUIMVar <- tryTakeMVar guiMVar
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder maybe (fail $ "should be filled with Nothing after proof attempt")
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder (const $ return ())
99afa6000472f3d291fdf9193ea19d334a58658dChristian MaedercalcGlobalHistory :: LibEnv -> LibEnv -> [LIB_NAME]
5bb7eeaca10ea76595229375f907a5a388b7c882Christian MaedercalcGlobalHistory old new = let
5bb7eeaca10ea76595229375f907a5a388b7c882Christian Maeder length' = \ ln -> SizedList.size . proofHistory . lookupDGraph ln
5bb7eeaca10ea76595229375f907a5a388b7c882Christian Maeder changes = filter (\ ln -> length' ln old < length' ln new) $ Map.keys old
cd36bffee51c77cdadcb9f916b34fa512e311946Christian Maeder in concatMap (\ ln -> replicate (length' ln new - length' ln old) ln) changes
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian MaedernodeErr :: Int -> IO ()
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaedernodeErr descr = error $ "node with descriptor " ++ show descr
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich ++ " has no corresponding node in the development graph"
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus LuettichshowNodeInfo :: Int -> DGraph -> IO ()
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus LuettichshowNodeInfo descr dgraph = do
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich let dgnode = labDG dgraph descr
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich title = (if isDGRef dgnode then ("reference " ++) else
36f63902db2b3463faa9f59912ad106e2d5aaa24Klaus Luettich if isInternalNode dgnode then ("internal " ++) else id)
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich "node " ++ getDGNodeName dgnode ++ " " ++ show descr
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich createTextDisplay title (title ++ "\n" ++ showDoc dgnode "")
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich fetches the theory from a node inside the IO Monad
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder (added by KL based on code in getTheoryOfNode) -}
e7757995211bd395dc79d26fe017d99375f7d2a6Christian MaederlookupTheoryOfNode :: IORef LibEnv -> LIB_NAME -> Int
810746aea00b81c1eec27dae84d73a43599ff056Christian Maeder -> IO (Res.Result (LibEnv, Node, G_theory))
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian MaederlookupTheoryOfNode proofStatusRef ln descr = do
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers libEnv <- readIORef proofStatusRef
a80c28bb8b7a23ccdf7e08d0fe216fc19cc97273Klaus Luettich (libEnv', gth) <- computeTheory True libEnv ln descr
82e29b77f0ef4cccd7ed734692c5e1e93dbbc645Christian Maeder return (libEnv', descr, gth)
5f0e3e4cb7dd31033c9682cafa712d2a66b2f3bcChristian MaedershowDiagMess :: HetcatsOpts -> [Diagnosis] -> IO ()
120145afbf940aff243cb3e847188383d6d622b6Christian MaedershowDiagMess opts ds = let es = Res.filterDiags (verbose opts) ds in
5f0e3e4cb7dd31033c9682cafa712d2a66b2f3bcChristian Maeder if null es then return () else
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder (if hasErrors es then errorDialog "Error" else infoDialog "Info") $ unlines
b9625461755578f3eed04676d42a63fd2caebd0cChristian Maeder $ map show es
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder{- | outputs the theory of a node in a window;
d0652648f9879c67a194f8b03baafe2700c68eb4Christian Maederused by the node menu defined in initializeGraph-}
363939beade943a02b31004cea09dec34fa8a6d9Christian MaedergetTheoryOfNode :: GInfo -> Int -> DGraph -> IO ()
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaedergetTheoryOfNode gInfo@(GInfo { gi_LIB_NAME = ln
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder , gi_GraphInfo = actGraphInfo
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich , libEnvIORef = le
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich }) descr dgraph = do
4ba08bfca0cc8d9da65397b8dfd2654fdb4c0e62Christian Maeder r <- lookupTheoryOfNode le ln descr
4ba08bfca0cc8d9da65397b8dfd2654fdb4c0e62Christian Maeder showDiagMess (gi_hetcatsOpts gInfo) ds
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich (Just (le', n, gth)) -> do
1365c420ef71be3d52796ebd369dc2defdedc822Christian Maeder lockGlobal gInfo
308834907a120fd8771e18292ed2ca9cd767c12dChristian Maeder displayTheoryWithWarning "Theory" (getNameOfNode n dgraph)
308834907a120fd8771e18292ed2ca9cd767c12dChristian Maeder (addHasInHidingWarning dgraph n) gth
1365c420ef71be3d52796ebd369dc2defdedc822Christian Maeder let newGr = lookupDGraph ln le'
83394c6b6e6de128e71b67c9251ed7a84485d082Christian Maeder libEnv <- readIORef le
36f63902db2b3463faa9f59912ad106e2d5aaa24Klaus Luettich let history = snd $ splitHistory (lookupDGraph ln libEnv) newGr
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder applyChanges actGraphInfo $ reverse $ flatHistory history
e420b3848a0e15a9e074b08c413996cbeb5ab06dChristian Maeder writeIORef le le'
68d10d143f29fcff3c637ba24f90e983995ceae6Christian Maeder unlockGlobal gInfo
42ce525125971c5e8ff32a38de5d7ea174d6508cChristian Maeder _ -> return ()
cc07a598b995acc9436651e66fd18009509047efChristian Maeder{- | translate the theory of a node in a window;
825a1e4ca1e768de4b4883c65a6cb1dce6aa0002Christian Maederused by the node menu defined in initializeGraph-}
825a1e4ca1e768de4b4883c65a6cb1dce6aa0002Christian MaedertranslateTheoryOfNode :: GInfo -> Int -> DGraph -> IO ()
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus LuettichtranslateTheoryOfNode
4ba08bfca0cc8d9da65397b8dfd2654fdb4c0e62Christian Maeder gInfo@(GInfo {gi_hetcatsOpts = opts, libEnvIORef = le}) node dgraph = do
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder libEnv <- readIORef le
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder let Res.Result ds mEnv = computeTheory False libEnv (gi_LIB_NAME gInfo) node
5580ab3e64410186ccd36cde8a94282d8757ac0dChristian Maeder Just (_, th@(G_theory lid sign _ sens _)) -> do
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder -- find all comorphism paths starting from lid
e284004f10a315dbdb624c8b2522f65d485eaa48Martin Kühl let paths = findComorphismPaths logicGraph (sublogicOfTh th)
b446bf54c1dc78690aa12e86aadc49cdd8585847Christian Maeder -- let the user choose one
e284004f10a315dbdb624c8b2522f65d485eaa48Martin Kühl sel <- listBox "Choose a node logic translation" $ map show paths
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder Nothing -> errorDialog "Error" "no node logic translation chosen"
50515239e7e190f4a34ca581dd685d002148fbddChristian Maeder Comorphism cid <- return (paths!!i)
0b349288edfa50fdf38fda1a14e1562d03f92574Christian Maeder -- adjust lid's
0b349288edfa50fdf38fda1a14e1562d03f92574Christian Maeder let lidS = sourceLogic cid
0b349288edfa50fdf38fda1a14e1562d03f92574Christian Maeder lidT = targetLogic cid
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder sign' <- coerceSign lid lidS "" sign
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder sens' <- coerceThSens lid lidS "" sens
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder -- translate theory along chosen comorphism
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder let Result es mTh = wrapMapTheory cid
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder (plainSign sign', toNamedList sens')
8b4c68db8b465107cabef8b9cd5b6bc216e1b156Till Mossakowski Nothing -> showDiagMess opts es
8b4c68db8b465107cabef8b9cd5b6bc216e1b156Till Mossakowski Just (sign'', sens1) -> displayTheoryWithWarning
8b4c68db8b465107cabef8b9cd5b6bc216e1b156Till Mossakowski "Translated Theory" (getNameOfNode node dgraph)
bcaf979d9babe6346aa343687aa7d596e2894cccPaolo Torrini (addHasInHidingWarning dgraph node)
df29370ae8d8b41587957f6bcdcb43a3f1927e47Christian Maeder (G_theory lidT (mkExtSign sign'') startSigId
bcaf979d9babe6346aa343687aa7d596e2894cccPaolo Torrini (toThSens sens1) startThId)
5ce19352a9cc47d982819cc889a71cd0a61ac171Christian Maeder Nothing -> showDiagMess opts ds
c9a7e6af169a2adfb92f42331cd578065ed83a2bChristian Maeder-- | Show proof status of a node
bcaf979d9babe6346aa343687aa7d596e2894cccPaolo TorrinishowProofStatusOfNode :: GInfo -> Int -> DGraph -> IO ()
23ab8855c58adfbd03a0730584b917b24c603901Christian MaedershowProofStatusOfNode _ descr dgraph = do
df29370ae8d8b41587957f6bcdcb43a3f1927e47Christian Maeder let dgnode = labDG dgraph descr
23ab8855c58adfbd03a0730584b917b24c603901Christian Maeder stat = showStatusAux dgnode
e50e41135ece589f7202bd4ef8d6b97531c2a56eKlaus Luettich title = "Proof status of node "++showName (dgn_name dgnode)
47b0e9f3cb008cb7997f4e3bae26e4d62dcc887aChristian Maeder createTextDisplay title stat
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaedershowStatusAux :: DGNodeLab -> String
431d34c7007a787331c4e5ec997badb0f8190fc7Christian MaedershowStatusAux dgnode =
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder case dgn_theory dgnode of
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder G_theory _ _ _ sens _ ->
99afa6000472f3d291fdf9193ea19d334a58658dChristian Maeder let goals = OMap.filter (not . isAxiom) sens
39bc7bbfc84f8b49f8434d299ec3a602c0437581Christian Maeder (proven,open) = OMap.partition isProvenSenStatus goals
88318aafc287e92931dceffbb943d58a9310001dChristian Maeder consGoal = "\nconservativity of this node"
24ddb6d7cde9dd6ab04b8631b1b0104e0861ec5fChristian Maeder in "Proven proof goals:\n"
39bc7bbfc84f8b49f8434d299ec3a602c0437581Christian Maeder ++ showDoc proven ""
88318aafc287e92931dceffbb943d58a9310001dChristian Maeder ++ if not $ hasOpenConsStatus True dgnode
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder then consGoal
39bc7bbfc84f8b49f8434d299ec3a602c0437581Christian Maeder ++ "\nOpen proof goals:\n"
a6091cb14d14a9273e8eacdfe33be1247b26c689Christian Maeder ++ showDoc open ""
39bc7bbfc84f8b49f8434d299ec3a602c0437581Christian Maeder ++ if hasOpenConsStatus False dgnode
50c3cc2b79207355522c5b096172b3c6b7bec300Christian Maeder then consGoal
9096f6c6aaded6cd8288656ceccd4c7b3bd0747eChristian Maeder-- | start local theorem proving or consistency checking at a node
e112e83352048f3db8c8f93ae104193e7338c10fChristian MaederproveAtNode :: Bool -> GInfo -> Int -> DGraph -> IO ()
e112e83352048f3db8c8f93ae104193e7338c10fChristian MaederproveAtNode checkCons gInfo@(GInfo { libEnvIORef = ioRefProofStatus
e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus Luettich , gi_LIB_NAME = ln
e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus Luettich , commandHist = ch }) descr dgraph = do
e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus Luettich let dgn = labDG dgraph descr
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder libNode = (ln,descr)
e112e83352048f3db8c8f93ae104193e7338c10fChristian Maeder (dgraph',dgn') <- case hasLock dgn of
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder True -> return (dgraph, dgn)
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder lockGlobal gInfo
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder le <- readIORef ioRefProofStatus
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder (dgraph',dgn') <- initLocking (lookupDGraph ln le) (descr, dgn)
f5c9b1e739228c2a2edf055ac419583412569683Christian Maeder writeIORef ioRefProofStatus $ Map.insert ln dgraph' le
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder unlockGlobal gInfo
c72c1e75a969ff4c336e77481c2a8e42603f13eeChristian Maeder return (dgraph',dgn')
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder locked <- tryLockLocal dgn'
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder case locked of
7767474aba4fa2dc51a6c68017d3bcef3b773001Christian Maeder errorDialog "Error" "Proofwindow already open"
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder let action = do
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder le <- readIORef ioRefProofStatus
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder guiMVar <- newMVar Nothing
f4505a64a089693012a3f5c3b1f12a82cd7a2a5aKlaus Luettich res <- basicInferenceNode checkCons logicGraph libNode ln
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder guiMVar le ch
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder runProveAtNode checkCons gInfo (descr, dgn') res
f4505a64a089693012a3f5c3b1f12a82cd7a2a5aKlaus Luettich unlockLocal dgn'
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder case checkCons || not (hasIncomingHidingEdge dgraph' $ snd libNode) of
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder forkIO action
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder b <- warningDialog "Warning"
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder "This node has incoming hiding links!\n Prove anyway?"
1a6464613c59e35072b90ca296ae402cbe956144Christian Maeder $ Just action
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder unless b $ unlockLocal dgn'
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian MaederrunProveAtNode :: Bool -> GInfo -> LNode DGNodeLab
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder -> Res.Result (LibEnv, Res.Result G_theory) -> IO ()
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian MaederrunProveAtNode checkCons gInfo (v, dgnode) res = case maybeResult res of
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder Just (le, tres) -> do
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder let nodetext = getDGNodeName dgnode ++ " node: " ++ show v
f78ce817f35574674d54e30ad1861a9b4ced20caChristian Maeder when checkCons $ case maybeResult tres of
f78ce817f35574674d54e30ad1861a9b4ced20caChristian Maeder Just gth -> createTextSaveDisplay
f78ce817f35574674d54e30ad1861a9b4ced20caChristian Maeder ("Model for " ++ nodetext)
f78ce817f35574674d54e30ad1861a9b4ced20caChristian Maeder "model.log" $ showDoc gth ""
fd2c22348e5a69231f92fb44e35a9970b47c4e93Christian Maeder Nothing -> case diags tres of
f78ce817f35574674d54e30ad1861a9b4ced20caChristian Maeder ds -> infoDialog nodetext
f78ce817f35574674d54e30ad1861a9b4ced20caChristian Maeder $ unlines $ "could not (re-)construct a model" : map diagString ds
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder proofMenu gInfo $ mergeDGNodeLab gInfo
89c9d707aa817684b88036a2dad66c3437840677Heng Jiang (v, labDG (lookupDGraph (gi_LIB_NAME gInfo) le) v)
f78ce817f35574674d54e30ad1861a9b4ced20caChristian Maeder Nothing -> return ()
f78ce817f35574674d54e30ad1861a9b4ced20caChristian MaedermergeDGNodeLab :: GInfo -> LNode DGNodeLab -> LibEnv -> IO (Res.Result LibEnv)
f041c9a6bda23de33a38490e35b831ae18d96b45Christian MaedermergeDGNodeLab (GInfo{gi_LIB_NAME = ln}) (v, new_dgn) le = do
f041c9a6bda23de33a38490e35b831ae18d96b45Christian Maeder let dg = lookupDGraph ln le
f041c9a6bda23de33a38490e35b831ae18d96b45Christian Maeder old_dgn = labDG dg v
bf7b17b0e19362e9228672782218678cab275d1eDominik Luecke theory <- joinG_sentences (dgn_theory old_dgn) $ dgn_theory new_dgn
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder let new_dgn' = old_dgn { dgn_theory = theory }
49d647f58ec5bf482da541eec62f531848c49036Christian Maeder dg'' = changeDGH dg $ SetNodeLab old_dgn (v, new_dgn')
7834a982096d93301a4626f444dd9ea5f9fe17eaChristian Maeder return $ Map.insert ln dg'' le
409fdf3eb3a0824ab032c4bc1f00f5838fd54d4cChristian Maeder-- | print the id, origin, type, proof-status and morphism of the edge
409fdf3eb3a0824ab032c4bc1f00f5838fd54d4cChristian MaedershowEdgeInfo :: Int -> Maybe (LEdge DGLinkLab) -> IO ()
5c0b769e33f643e5f0b06328ba0eb03e5bd6e18eChristian MaedershowEdgeInfo descr me = case me of
f9442174f64331ccf0bf08178632af7302ccfc96Christian Maeder Just e@(_, _, l) -> let estr = showLEdge e in
f9442174f64331ccf0bf08178632af7302ccfc96Christian Maeder infoDialog ("Info of " ++ estr)
c802a1041ed9251f8ad79139454267e802900e2aChristian Maeder (estr ++ "\n" ++ showDoc l "")
53bbc1c9a4e986d1ee9c081d6f0ac7b9546f212bDominik Luecke Nothing -> errorDialog "Error"
bf7b17b0e19362e9228672782218678cab275d1eDominik Luecke ("edge " ++ show descr ++ " has no corresponding edge"
bf7b17b0e19362e9228672782218678cab275d1eDominik Luecke ++ "in the development graph")
bf7b17b0e19362e9228672782218678cab275d1eDominik LueckeconservativityRule :: DGRule
bf7b17b0e19362e9228672782218678cab275d1eDominik LueckeconservativityRule = DGRule "ConservativityCheck"
bf7b17b0e19362e9228672782218678cab275d1eDominik Luecke-- | check conservativity of the edge
75b0c0c2cbfb7edd3f4c0555227aabbe6c1aa195Christian MaedercheckconservativityOfEdge :: Int -> GInfo -> Maybe (LEdge DGLinkLab) -> IO ()
bf7b17b0e19362e9228672782218678cab275d1eDominik LueckecheckconservativityOfEdge _ gInfo@(GInfo{gi_LIB_NAME = ln,
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu gi_GraphInfo = _actGraphInfo,
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu libEnvIORef = le})
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu (Just (source,target,linklab)) = do
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu lockGlobal gInfo
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu libEnv <- readIORef $ libEnvIORef gInfo
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu let libEnv' = case convertToNf ln libEnv target of
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu Result _ (Just lE) -> lE
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu _ -> error "checkconservativityOfEdge: convertToNf"
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu let (_, thTar) =
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu case computeTheory True libEnv' ln target of
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu Res.Result _ (Just th1) -> th1
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu _ -> error "checkconservativityOfEdge: computeTheory"
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu G_theory lid _sign _ sensTar _ <- return thTar
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu GMorphism cid _ _ morphism2 _ <- return $ dgl_morphism linklab
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu Just (GMorphism cid' _ _ morphism3 _) <- return $
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu dgn_sigma $ labDG (lookupDGraph ln libEnv') target
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu morphism2' <- coerceMorphism (targetLogic cid) lid
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu "checkconservativityOfEdge2" morphism2
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu morphism3' <- coerceMorphism (targetLogic cid') lid
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu "checkconservativityOfEdge3" morphism3
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu let compMor = case comp morphism2' morphism3' of
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu Res.Result _ (Just phi) -> phi
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu _ -> error "checkconservativtiyOfEdge: comp"
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu let (_le', thSrc) =
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu case computeTheory False libEnv' (gi_LIB_NAME gInfo) source of
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu Res.Result _ (Just th1) -> th1
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu _ -> error "checkconservativityOfEdge: computeTheory"
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu G_theory lid1 sign1 _ sensSrc1 _ <- return thSrc
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu sign2 <- coerceSign lid1 lid "checkconservativityOfEdge.coerceSign" sign1
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu sensSrc2 <- coerceThSens lid1 lid "checkconservativityOfEdge1" sensSrc1
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu let transSensSrc = propagateErrors
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu $ mapThSensValueM (map_sen lid compMor) sensSrc2
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu if length (conservativityCheck lid) < 1
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu infoDialog "Result of conservativity check"
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu "No conservativity checkers available"
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu writeIORef le libEnv'
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu unlockGlobal gInfo
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu checkerR <- conservativityChoser $ conservativityCheck lid
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu if Res.hasErrors $ Res.diags checkerR
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu infoDialog "Result of conservativity check"
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu "No conservativity checker chosen"
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu writeIORef le libEnv'
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu unlockGlobal gInfo
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu let chCons = checkConservativity $
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu maybe (error "checkconservativityOfEdge4") id
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu (plainSign sign2, toNamedList sensSrc2)
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu compMor $ toNamedList
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu (sensTar `OMap.difference` transSensSrc)
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu showObls [] = ""
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu showObls obls = ", provided that the following proof obligations "
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu ++ "can be discharged:\n"
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu ++ concatMap (flip showDoc "\n") obls
ae3e4689adbf4de67f4e1cdda6db2c0e406027d0Francisc Nicolae Bungiu showRes = case res of
b446bf54c1dc78690aa12e86aadc49cdd8585847Christian Maeder Just (Just (cst, obls)) -> "The link is "
3b5814dc6ac813faf8a12ecddf4b727ca7b666a8Francisc Nicolae Bungiu ++ showConsistencyStatus cst ++ showObls obls
3b5814dc6ac813faf8a12ecddf4b727ca7b666a8Francisc Nicolae Bungiu _ -> "Could not determine whether link is conservative"
e7cf29d9f71f4724aed05916d93a0b656d7104e6Francisc Nicolae Bungiu myDiags = showRelDiags 2 ds
9f226cec9f978edaba67aee4c4e04e3d3b994b87Daniel Calegari createTextDisplay "Result of conservativity check"
9f226cec9f978edaba67aee4c4e04e3d3b994b87Daniel Calegari (showRes ++ "\n" ++ myDiags)
9f226cec9f978edaba67aee4c4e04e3d3b994b87Daniel Calegari consShow = case res of
9f226cec9f978edaba67aee4c4e04e3d3b994b87Daniel Calegari Just (Just (cst, _)) -> cst
9f226cec9f978edaba67aee4c4e04e3d3b994b87Daniel Calegari _ -> Unknown "Unknown"
9f226cec9f978edaba67aee4c4e04e3d3b994b87Daniel Calegari GlobalThm proven conserv _ = dgl_type linklab
newLibEnv = Map.insert ln
(Res.Result (ConservativityChecker
convert :: GA.GraphInfo -> DGraph -> IO ()
convertNodes :: GA.GraphInfo -> DGraph -> IO ()
convertNodesAux :: GA.GraphInfo -> LNode DGNodeLab -> IO ()
GA.addNode ginfo node (getRealDGNodeType dgnode) $ getDGNodeName dgnode
convertEdges :: GA.GraphInfo -> DGraph -> IO ()
convertEdgesAux :: GA.GraphInfo -> LEdge DGLinkLab -> IO ()
GA.addEdge ginfo (dgl_id lbl) (getRealDGLinkType lbl) src tar "" $ Just e
case Map.lookup refLibname le of
GA.redisplay gv
GA.showTemporaryMessage gv "Development Graph initialized."
applyChanges :: GA.GraphInfo -> [DGChange] -> IO ()
applyChangesAux :: GA.GraphInfo -> DGChange -> IO ()
GA.changeNodeType ginfo node $ getRealDGNodeType newLab
GA.addNode ginfo node (getRealDGNodeType nodelab) $ getDGNodeName nodelab
GA.delNode ginfo node
GA.addEdge ginfo (dgl_id lbl) (getRealDGLinkType lbl) src tgt "" $ Just e
GA.delEdge ginfo $ dgl_id lbl
-> 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.
let Res.Result diagsTrans mLEnv =
GA.deactivateGraphWindow actGraphInfo
GA.redisplay actGraphInfo
GA.layoutImproveAll actGraphInfo
GA.activateGraphWindow actGraphInfo
saveUDGraph :: GInfo -> Map.Map DGNodeType (Shape value, String)
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