GraphLogic.hs revision b6a59f004903ac7bc96323ee3ef09c01fd221157
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederModule : $Header$
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederDescription : Logic for manipulating the graph in the Central GUI
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederCopyright : (c) Jorina Freya Gerken, Till Mossakowski, Uni Bremen 2002-2006
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederMaintainer : till@informatik.uni-bremen.de
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederStability : provisional
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederPortability : non-portable (imports Logic)
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederThis module provides functions for all the menus in the Hets GUI.
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederThese are then assembled to the GUI in "GUI.GraphMenu".
7d0db235b17b2109cd45fa50e6d1bbc77823f81dEugen Kuksa , remakeGraph
25da71ee832b729e33def344a68f59fe21ce9c07Eugen Kuksa , performProofAction
92ae4d5885ea837ffe3dae9b2de742f871229b94Christian Maeder , openProofStatus
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder , saveProofStatus
8d2321e17a34951fbd52f68e9f9f148f0890e471Christian Maeder , openTranslateGraph
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder , showReferencedLibrary
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder , getSignatureOfNode
e5f71ad96ddbaafd3bf8ae0820df93e0db4b0527cmaeder , getTheoryOfNode
e5f71ad96ddbaafd3bf8ae0820df93e0db4b0527cmaeder , getLocalAxOfNode
eae0d62755147d991cc3e903f74f98ac31a7cd42Christian Maeder , translateTheoryOfNode
8723ec450f2e7a024230467c0c28a3f154905483cmaeder , displaySubsortGraph
8723ec450f2e7a024230467c0c28a3f154905483cmaeder , displayConceptGraph
ab38e2fac740c4336afafbe0584053dc2e67002bEugen Kuksa , lookupTheoryOfNode
8723ec450f2e7a024230467c0c28a3f154905483cmaeder , getSublogicOfNode
eae0d62755147d991cc3e903f74f98ac31a7cd42Christian Maeder , showOriginOfNode
d4263171d0ce2cbc390a7b44bff98e8b3c0f8ce7Christian Maeder , showProofStatusOfNode
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder , proveAtNode
e84c877ad38ce9312eab222a79f44da2015572d2Christian Maeder , showJustSubtree
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder , showIDOfEdge
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder , getNumberOfNode
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder , showMorphismOfEdge
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder , showOriginOfEdge
ef1c24c8229ade3ac872febebd18c181e32fb9c4Christian Maeder , checkconservativityOfEdge
ef1c24c8229ade3ac872febebd18c181e32fb9c4Christian Maeder , showProofStatusOfThm
945e82ed7877917f3ab1657f555e71991372546aChristian Maeder , convertNodes
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder , convertEdges
ef1c24c8229ade3ac872febebd18c181e32fb9c4Christian Maeder , hideShowNames
7c99a6c982aaf61547de8054296c8055c8d1a13aSimon Ulbricht , translateGraph
ef1c24c8229ade3ac872febebd18c181e32fb9c4Christian Maeder , showLibGraph
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder , runAndLock
d97700a22b2585ece83b05f3fff945fdfd0c44b4Christian Maeder , saveUDGraph
de8eee2014437ec4020be15cd363257f87e79943Christian Maederimport Logic.Logic(conservativityCheck)
ea5ccb1c6e89486a54e1f4bd95840147e96093edChristian Maederimport Logic.Coerce(coerceSign, coerceMorphism)
e42249ec61f50a83525db6e5fc9f5c4dd1b4cf5fcmaederimport Syntax.AS_Library(LIB_NAME, getModTime, getLIB_ID)
e42249ec61f50a83525db6e5fc9f5c4dd1b4cf5fcmaederimport Static.DGToSpec(dgToSpec, computeTheory)
6a88f8edd881afaf4b865b01bfbb4faaf0e7a3c9Simon Ulbrichtimport Static.AnalysisLibrary(anaLibExt, anaLib)
473f5af6e4803fbeecc814065952396f2501039bChristian Maederimport Static.DGTranslation(libEnv_translation)
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maederimport Proofs.InferBasic(basicInferenceNode)
e42249ec61f50a83525db6e5fc9f5c4dd1b4cf5fcmaederimport Proofs.StatusUtils(lookupHistory, removeContraryChanges)
734a5ebd38032798f0ab908e2d52862c71b2c127Simon Ulbrichtimport GUI.Utils(listBox, createTextSaveDisplay)
ea5ccb1c6e89486a54e1f4bd95840147e96093edChristian Maederimport GUI.Taxonomy (displayConceptGraph,displaySubsortGraph)
c8afa08a8bda589ef6670068dff0108464be4da7Christian Maederimport GUI.DGTranslation(getDGLogic)
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksaimport qualified GUI.HTkUtils (displayTheory,
df67ddf64192bfcae6ece65255ad796a17cbe532Christian Maeder displayTheoryWithWarning,
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder createInfoDisplayWithTwoButtons)
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maederimport DaVinciGraph
526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maederimport GraphDisp(deleteArc, deleteNode, getNodeValue, setNodeFocus)
473f5af6e4803fbeecc814065952396f2501039bChristian Maederimport GraphConfigure
f675b8f0a612e37472640da57b48d795bef4427eChristian Maederimport TextDisplay(createTextDisplay)
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maederimport InfoBus(encapsulateWaitTermAct)
526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maederimport DialogWin (useHTk)
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maederimport Messages(errorMess)
18548c6cc2dff13bf9f5f08b3f6cde6ca914df1dChristian Maederimport qualified HTk
dae8246f1f55b6a85e946fc1bfb6d32d556395f1Simon Ulbrichtimport Configuration(size)
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maederimport FileDialog(newFileDialogStr)
18548c6cc2dff13bf9f5f08b3f6cde6ca914df1dChristian Maederimport Common.Id(nullRange)
6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maederimport Common.DocUtils(showDoc, pretty)
7710f7c3425e45af11af124ff37bec27229d24f7Christian Maederimport Common.ResultT(liftR, runResultT)
6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maederimport qualified Common.OrderedMap as OMap
f674d7a58db3f991300a708f3799d80c369781f8Eugen Kuksaimport qualified Common.InjMap as InjMap
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maederimport qualified Common.Lib.Rel as Rel
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maederimport Driver.WriteFn(writeShATermFile)
526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maederimport Driver.ReadFn(libNameToFile, readVerbose)
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maederimport System.Directory(getModificationTime)
eca54dc24f2c59cc51645115347a89ba2b40de36cmaederimport Data.Maybe(fromJust)
e98c3d3efab62d97ebdeed52f4109d961f6432aaChristian Maederimport Data.List(nub,deleteBy,find)
eca54dc24f2c59cc51645115347a89ba2b40de36cmaederimport Data.Graph.Inductive.Graph as Graph( Node, LEdge, LNode, lab'
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder , labNode', labNodes, (&))
eca54dc24f2c59cc51645115347a89ba2b40de36cmaederimport qualified Data.Map as Map
26acf851cacd7a31bdc9b25a42af9949942fa7c6Christian MaederrunAndLock :: GInfo -> IO () -> IO ()
5896f38ba2934056542cb7cb3e6359e88a622547Christian MaederrunAndLock (GInfo { functionLock = lock
5896f38ba2934056542cb7cb3e6359e88a622547Christian Maeder , graphId = gid
5896f38ba2934056542cb7cb3e6359e88a622547Christian Maeder , gi_GraphInfo = actGraph
5fb6343a5a2b4bbc67bc83479c84a92d23d30edfChristian Maeder }) function = do
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder locked <- tryPutMVar lock ()
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder case locked of
18548c6cc2dff13bf9f5f08b3f6cde6ca914df1dChristian Maeder _ <- takeMVar lock
5fb6343a5a2b4bbc67bc83479c84a92d23d30edfChristian Maeder showTemporaryMessage gid actGraph $ "an other function is still working"
6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder ++ "... please wait ..."
12882fa70d12d9b56cbd850ccb4b724feb3c62d5Christian MaedernegateChanges :: ([DGRule],[DGChange]) -> ([DGRule],[DGChange])
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian MaedernegateChanges (_, dgChanges) = ([], map negateChange dgChanges)
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder negateChange :: DGChange -> DGChange
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder negateChange change = case change of
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder InsertNode x -> DeleteNode x
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder DeleteNode x -> InsertNode x
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder InsertEdge x -> DeleteEdge x
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder DeleteEdge x -> InsertEdge x
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder SetNodeLab old (node, new) -> SetNodeLab new (node, old)
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder-- | Undo one step of the History
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maederundo :: GInfo -> Bool -> IO ()
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maederundo gInfo@(GInfo { libEnvIORef = ioRefProofStatus
b87fb5d6d5aba8fc6d3c528f7da0af228ca76b02Eugen Kuksa , globalHist = gHist
dfa31ad230c88a66a9722c2a5ab23fe82c33f014Eugen Kuksa , graphId = gid
b87fb5d6d5aba8fc6d3c528f7da0af228ca76b02Eugen Kuksa , gi_GraphInfo = actGraph
dfa31ad230c88a66a9722c2a5ab23fe82c33f014Eugen Kuksa }) isUndo = do
b87fb5d6d5aba8fc6d3c528f7da0af228ca76b02Eugen Kuksa (guHist, grHist) <- takeMVar gHist
b87fb5d6d5aba8fc6d3c528f7da0af228ca76b02Eugen Kuksa case if isUndo then guHist else grHist of
8723ec450f2e7a024230467c0c28a3f154905483cmaeder showTemporaryMessage gid actGraph "History is empty..."
8723ec450f2e7a024230467c0c28a3f154905483cmaeder putMVar gHist (guHist, grHist)
dfa31ad230c88a66a9722c2a5ab23fe82c33f014Eugen Kuksa (lns:gHist') -> do
8723ec450f2e7a024230467c0c28a3f154905483cmaeder le <- readIORef ioRefProofStatus
8723ec450f2e7a024230467c0c28a3f154905483cmaeder undoDGraphs gInfo isUndo lns
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder updateDGraphs le $ filter (\ln -> elem ln lns) $ Map.keys le
31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder putMVar gHist $ if isUndo then (gHist', (reverse lns):grHist)
31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder else ((reverse lns):guHist, gHist')
6f9d360a425bdae3bd15289388e64c14a85eca43cmaederundoDGraphs :: GInfo -> Bool -> [LIB_NAME] -> IO ()
5d3978bb76c33d08d6297f69f10bbc04721ee3a5cmaederundoDGraphs _ _ [] = return ()
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaederundoDGraphs g u (ln:r) = do
1f0483f71bad0707f10293d0b4db4649aa93fb35Christian Maeder undoDGraph g u ln
1f0483f71bad0707f10293d0b4db4649aa93fb35Christian Maeder undoDGraphs g u r
c5b8b64377e24bcbf5cc108ca433cfbbd6235ba1Christian MaederundoDGraph :: GInfo -> Bool -> LIB_NAME -> IO ()
c5b8b64377e24bcbf5cc108ca433cfbbd6235ba1Christian MaederundoDGraph gInfo@(GInfo { libEnvIORef = ioRefProofStatus
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder , graphId = gid
6f9d360a425bdae3bd15289388e64c14a85eca43cmaeder , gi_GraphInfo = actGraph
6f9d360a425bdae3bd15289388e64c14a85eca43cmaeder }) isUndo ln = do
c5b8b64377e24bcbf5cc108ca433cfbbd6235ba1Christian Maeder showTemporaryMessage gid actGraph $ "Undo last change to " ++ show ln ++ "..."
6f9d360a425bdae3bd15289388e64c14a85eca43cmaeder lockGlobal gInfo
c5b8b64377e24bcbf5cc108ca433cfbbd6235ba1Christian Maeder le <- readIORef ioRefProofStatus
293abe6af19382a456dbe612aef45054ef76832fcmaeder dg = lookupDGraph ln le
6f9d360a425bdae3bd15289388e64c14a85eca43cmaeder (phist,rhist) = if isUndo then (proofHistory dg, redoHistory dg)
8723ec450f2e7a024230467c0c28a3f154905483cmaeder else (redoHistory dg, proofHistory dg)
e5f71ad96ddbaafd3bf8ae0820df93e0db4b0527cmaeder change = negateChanges $ head phist
e5f71ad96ddbaafd3bf8ae0820df93e0db4b0527cmaeder dg'' = changesDG dg $ (if isUndo then id else reverse) $ snd change
8723ec450f2e7a024230467c0c28a3f154905483cmaeder dg' = case isUndo of
1f0483f71bad0707f10293d0b4db4649aa93fb35Christian Maeder True -> dg'' { redoHistory = change:rhist
8723ec450f2e7a024230467c0c28a3f154905483cmaeder , proofHistory = tail phist}
8723ec450f2e7a024230467c0c28a3f154905483cmaeder False -> dg'' { redoHistory = tail phist
5d93620c37abd9c665d3fe532d4852d62dff4233Christian Maeder , proofHistory = change:rhist}
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder writeIORef ioRefProofStatus $ Map.insert ln dg' le
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder unlockGlobal gInfo
5d93620c37abd9c665d3fe532d4852d62dff4233Christian MaederupdateDGraphs :: LibEnv -> [LIB_NAME] -> IO ()
5d93620c37abd9c665d3fe532d4852d62dff4233Christian MaederupdateDGraphs _ [] = return ()
232c13ff6847a6f2bac7163392f80ab692cd7774Christian MaederupdateDGraphs le (ln:r) = do
12882fa70d12d9b56cbd850ccb4b724feb3c62d5Christian Maeder updateDGraph $ lookupDGraph ln le
4bd27a2cb9efd5d8ff00b5cf823487403add724ecmaeder updateDGraphs le r
99b26e2ab8ba89bc9a050c1524137eb6269e2753Christian MaederupdateDGraph :: DGraph -> IO ()
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaederupdateDGraph dg = case openlock dg of
26acf851cacd7a31bdc9b25a42af9949942fa7c6Christian Maeder Just lock -> do
6f9d360a425bdae3bd15289388e64c14a85eca43cmaeder mRemakeF <- tryTakeMVar lock
c5b8b64377e24bcbf5cc108ca433cfbbd6235ba1Christian Maeder case mRemakeF of
6f9d360a425bdae3bd15289388e64c14a85eca43cmaeder Just remakeF -> do
99b26e2ab8ba89bc9a050c1524137eb6269e2753Christian Maeder putMVar lock remakeF
6f9d360a425bdae3bd15289388e64c14a85eca43cmaeder Nothing -> return ()
6f9d360a425bdae3bd15289388e64c14a85eca43cmaeder Nothing -> return ()
4937a0e373f619dc520799923acec42db5da5eb3Eugen Kuksa-- | reloads the Library of the DevGraph
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaederreload :: GInfo -> IO()
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaederreload gInfo@(GInfo { libEnvIORef = ioRefProofStatus
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder , gi_LIB_NAME = ln
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder , gi_hetcatsOpts = opts
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder lockGlobal gInfo
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder oldle <- readIORef ioRefProofStatus
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder libdeps = Rel.toList $ Rel.intransKernel $ Rel.transClosure $ Rel.fromList
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder $ getLibDeps oldle
df24d7f0c79862ffd8189698645e201bf07a4d9cEugen Kuksa ioruplibs <- newIORef ([] :: [LIB_NAME])
df24d7f0c79862ffd8189698645e201bf07a4d9cEugen Kuksa writeIORef ioruplibs []
feb9227bb5c49d5bea1a112500c3b3eba31abdfbcmaeder reloadLibs ioRefProofStatus opts libdeps ioruplibs ln
df24d7f0c79862ffd8189698645e201bf07a4d9cEugen Kuksa unlockGlobal gInfo
df24d7f0c79862ffd8189698645e201bf07a4d9cEugen Kuksa remakeGraph gInfo
df24d7f0c79862ffd8189698645e201bf07a4d9cEugen Kuksa-- | Creates a list of all LIB_NAME pairs, which have a dependency
feb9227bb5c49d5bea1a112500c3b3eba31abdfbcmaedergetLibDeps :: LibEnv -> [(LIB_NAME, LIB_NAME)]
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaedergetLibDeps le =
6f9d360a425bdae3bd15289388e64c14a85eca43cmaeder concat $ map (\ ln -> getDep ln le) $ Map.keys le
dfa31ad230c88a66a9722c2a5ab23fe82c33f014Eugen Kuksa-- | Creates a list of LIB_NAME pairs for the fist argument
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen KuksagetDep :: LIB_NAME -> LibEnv -> [(LIB_NAME, LIB_NAME)]
64f5f0a8c38d5b2ba33b09e02e92b0e3f812d6d0Eugen KuksagetDep ln le =
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa map (\ (_, x) -> (ln, dgn_libname x)) $
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa filter (isDGRef . snd) $ labNodes $ dgBody $ lookupDGraph ln le
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa-- | Reloads a library
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen KuksareloadLib :: IORef LibEnv -> HetcatsOpts -> IORef [LIB_NAME] -> LIB_NAME
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen KuksareloadLib iorle opts ioruplibs ln = do
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa mfile <- existsAnSource opts {intype = GuessIn}
64f5f0a8c38d5b2ba33b09e02e92b0e3f812d6d0Eugen Kuksa $ rmSuffix $ libNameToFile opts ln
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa case mfile of
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa Nothing -> do
dfa31ad230c88a66a9722c2a5ab23fe82c33f014Eugen Kuksa Just file -> do
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa le <- readIORef iorle
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa mres <- anaLibExt opts file le'
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa case mres of
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa Just (_, newle) -> do
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa uplibs <- readIORef ioruplibs
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa writeIORef ioruplibs $ ln:uplibs
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa writeIORef iorle newle
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa Nothing -> do
ab38e2fac740c4336afafbe0584053dc2e67002bEugen Kuksa fail $ "Could not read original development graph from '"++ file
dfa31ad230c88a66a9722c2a5ab23fe82c33f014Eugen Kuksa-- | Reloads libraries if nessesary
ab38e2fac740c4336afafbe0584053dc2e67002bEugen KuksareloadLibs :: IORef LibEnv -> HetcatsOpts -> [(LIB_NAME, LIB_NAME)]
ab38e2fac740c4336afafbe0584053dc2e67002bEugen Kuksa -> IORef [LIB_NAME] -> LIB_NAME -> IO Bool
ab38e2fac740c4336afafbe0584053dc2e67002bEugen KuksareloadLibs iorle opts deps ioruplibs ln = do
ab38e2fac740c4336afafbe0584053dc2e67002bEugen Kuksa uplibs <- readIORef ioruplibs
d16243f2fd4825f598eee589b68e324e23eb469dEugen Kuksa case elem ln uplibs of
d16243f2fd4825f598eee589b68e324e23eb469dEugen Kuksa True -> return True
ab38e2fac740c4336afafbe0584053dc2e67002bEugen Kuksa deps' = map (snd) $ filter (\ (ln',_) -> ln == ln') deps
ab38e2fac740c4336afafbe0584053dc2e67002bEugen Kuksa res <- mapM (reloadLibs iorle opts deps ioruplibs) deps'
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa libupdate = foldl (\ u r -> if r then True else u) False res
64f5f0a8c38d5b2ba33b09e02e92b0e3f812d6d0Eugen Kuksa case libupdate of
64f5f0a8c38d5b2ba33b09e02e92b0e3f812d6d0Eugen Kuksa reloadLib iorle opts ioruplibs ln
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder False -> do
6f9d360a425bdae3bd15289388e64c14a85eca43cmaeder le <- readIORef iorle
6f9d360a425bdae3bd15289388e64c14a85eca43cmaeder newln:_ = filter (ln ==) $ Map.keys le
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder mfile <- existsAnSource opts $ rmSuffix $ libNameToFile opts ln
8723ec450f2e7a024230467c0c28a3f154905483cmaeder case mfile of
8723ec450f2e7a024230467c0c28a3f154905483cmaeder Nothing -> do
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder return False
8723ec450f2e7a024230467c0c28a3f154905483cmaeder Just file -> do
8723ec450f2e7a024230467c0c28a3f154905483cmaeder newmt <- getModificationTime file
12882fa70d12d9b56cbd850ccb4b724feb3c62d5Christian Maeder libupdate' = (getModTime $ getLIB_ID newln) < newmt
0b144823976d79a34bff62f7f9ec032e80b8ce85Simon Ulbricht case libupdate' of
0b144823976d79a34bff62f7f9ec032e80b8ce85Simon Ulbricht False -> return False
8723ec450f2e7a024230467c0c28a3f154905483cmaeder reloadLib iorle opts ioruplibs ln
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa-- | Deletes the old edges and nodes of the Graph and makes new ones
8723ec450f2e7a024230467c0c28a3f154905483cmaederremakeGraph :: GInfo -> IO ()
986888e7f4d8ed681272a79c63f329ce8037063dcmaederremakeGraph (GInfo { libEnvIORef = ioRefProofStatus
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder , conversionMapsIORef = convRef
0b144823976d79a34bff62f7f9ec032e80b8ce85Simon Ulbricht , graphId = gid
8723ec450f2e7a024230467c0c28a3f154905483cmaeder , gi_LIB_NAME = ln
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht , gi_GraphInfo = actGraphInfo
8723ec450f2e7a024230467c0c28a3f154905483cmaeder le <- readIORef ioRefProofStatus
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht (gs,ev_cnt) <- readIORef actGraphInfo
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht dgraph = lookupDGraph ln le
8723ec450f2e7a024230467c0c28a3f154905483cmaeder Just (_, g) = find (\ (gid', _) -> gid' == gid) gs
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht gs' = deleteBy (\ (gid1,_) (gid2,_) -> gid1 == gid2) (gid,g) gs
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht og = theGraph g
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht -- reads and delets the old nodes and edges
8723ec450f2e7a024230467c0c28a3f154905483cmaeder mapM_ (deleteArc og) $ map (\ (_,_,_,x) -> x) $ Map.elems $ AGV.edges g
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder mapM_ (deleteNode og) $ map snd $ Map.elems $ AGV.nodes g
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht -- stores the graph without nodes and edges in the GraphInfo
12882fa70d12d9b56cbd850ccb4b724feb3c62d5Christian Maeder g' = g {theGraph = og, AGV.nodes = Map.empty, AGV.edges = Map.empty}
0b144823976d79a34bff62f7f9ec032e80b8ce85Simon Ulbricht writeIORef actGraphInfo ((gid,g'):gs',ev_cnt)
8723ec450f2e7a024230467c0c28a3f154905483cmaeder -- creates new nodes and edges
8723ec450f2e7a024230467c0c28a3f154905483cmaeder newConvMaps <- convertNodes emptyConversionMaps gid actGraphInfo dgraph ln
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht finalConvMaps <- convertEdges newConvMaps gid actGraphInfo dgraph ln
12882fa70d12d9b56cbd850ccb4b724feb3c62d5Christian Maeder -- writes the ConversionMap and redisplays the graph
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht writeIORef convRef finalConvMaps
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht redisplay gid actGraphInfo
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon UlbrichthideShowNames :: GInfo -> Bool -> IO ()
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon UlbrichthideShowNames (GInfo {graphId = gid,
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht gi_GraphInfo = actGraphInfo,
8723ec450f2e7a024230467c0c28a3f154905483cmaeder internalNamesIORef = showInternalNames
de8983abdf4b35af1ed1fdee2de4dff13c2368bacmaeder }) toggle = do
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht deactivateGraphWindow gid actGraphInfo
0a46a4d711eca869ad75b4df84dabd72783ebdd2Simon Ulbricht (intrn::InternalNames) <- readIORef showInternalNames
12882fa70d12d9b56cbd850ccb4b724feb3c62d5Christian Maeder let showThem = if toggle then not $ showNames intrn else showNames intrn
0b144823976d79a34bff62f7f9ec032e80b8ce85Simon Ulbricht showItrn s = if showThem then s else ""
12882fa70d12d9b56cbd850ccb4b724feb3c62d5Christian Maeder mapM_ (\(s,upd) -> upd (\_ -> showItrn s)) $ updater intrn
0b144823976d79a34bff62f7f9ec032e80b8ce85Simon Ulbricht writeIORef showInternalNames $ intrn {showNames = showThem}
0b144823976d79a34bff62f7f9ec032e80b8ce85Simon Ulbricht redisplay gid actGraphInfo
0b144823976d79a34bff62f7f9ec032e80b8ce85Simon Ulbricht activateGraphWindow gid actGraphInfo
0a46a4d711eca869ad75b4df84dabd72783ebdd2Simon UlbrichtshowNodes :: GInfo -> IO ()
ccd9cf19d129595770d592d3d0d80c6619f7a141Eugen KuksashowNodes gInfo@(GInfo {descrIORef = event,
465c6b72e8e480969b5f08658e394992bcc08bfcSimon Ulbricht graphId = gid,
0b144823976d79a34bff62f7f9ec032e80b8ce85Simon Ulbricht gi_GraphInfo = actGraphInfo
0a46a4d711eca869ad75b4df84dabd72783ebdd2Simon Ulbricht deactivateGraphWindow gid actGraphInfo
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa descr <- readIORef event
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa AGV.Result _ errorMsg <- checkHasHiddenNodes gid descr actGraphInfo
0b144823976d79a34bff62f7f9ec032e80b8ce85Simon Ulbricht case errorMsg of
4937a0e373f619dc520799923acec42db5da5eb3Eugen Kuksa Nothing -> do
4937a0e373f619dc520799923acec42db5da5eb3Eugen Kuksa showTemporaryMessage gid actGraphInfo "Revealing hidden nodes ..."
4937a0e373f619dc520799923acec42db5da5eb3Eugen Kuksa showIt gid descr actGraphInfo
4f820114168836fb05b720c429866baa5665690eChristian Maeder hideShowNames gInfo False
4937a0e373f619dc520799923acec42db5da5eb3Eugen Kuksa Just _ -> do
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht showTemporaryMessage gid actGraphInfo "No hidden nodes found ..."
4937a0e373f619dc520799923acec42db5da5eb3Eugen Kuksa activateGraphWindow gid actGraphInfo
1d65a799298f6b1253d774c22f61029e6eb99cadcmaederhideNodes :: GInfo -> IO ()
6fb590a3747600c145abfd7c3483039fb03af032Christian MaederhideNodes (GInfo {descrIORef = event,
6fb590a3747600c145abfd7c3483039fb03af032Christian Maeder graphId = gid,
6fb590a3747600c145abfd7c3483039fb03af032Christian Maeder gi_GraphInfo = actGraphInfo
6fb590a3747600c145abfd7c3483039fb03af032Christian Maeder deactivateGraphWindow gid actGraphInfo
6fb590a3747600c145abfd7c3483039fb03af032Christian Maeder descr' <- readIORef event
cbd64ad1d663565751cb9442f78a40ff96c6bed6Eugen Kuksa AGV.Result _ errorMsg <- checkHasHiddenNodes gid descr' actGraphInfo
6fb590a3747600c145abfd7c3483039fb03af032Christian Maeder case errorMsg of
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht Nothing -> do
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder showTemporaryMessage gid actGraphInfo "Nodes already hidden ..."
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder Just _ -> do
fcd8dd6d9029180ae5e777e94a973c5e355a55cfcmaeder showTemporaryMessage gid actGraphInfo "Hiding unnamed nodes..."
fcd8dd6d9029180ae5e777e94a973c5e355a55cfcmaeder AGV.Result descr msg <- hideSetOfNodeTypes gid
fcd8dd6d9029180ae5e777e94a973c5e355a55cfcmaeder [--red nodes are not hidden
fcd8dd6d9029180ae5e777e94a973c5e355a55cfcmaeder --"open_cons__internal",
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa --"locallyEmpty__open_cons__internal",
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa --"proven_cons__internal",
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa "locallyEmpty__proven_cons__internal"]
4937a0e373f619dc520799923acec42db5da5eb3Eugen Kuksa True actGraphInfo
4937a0e373f619dc520799923acec42db5da5eb3Eugen Kuksa writeIORef event descr
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa Nothing -> do redisplay gid actGraphInfo
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht Just err -> putStrLn err
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht activateGraphWindow gid actGraphInfo
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa-- | Let the user select a Node to focus
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen KuksafocusNode :: GInfo -> IO ()
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen KuksafocusNode (GInfo { gi_GraphInfo = actGraphInfo }) = do
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa ((_, graph):_, _) <- readIORef actGraphInfo
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa let nodes' = map (snd . snd) $ Map.toList $ nodes graph
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa nodes'' <- mapM (\node -> do
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa (label, _, _) <- getNodeValue (theGraph graph) node
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa return label) nodes'
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa selection <- listBox "Select a node to focus" nodes''
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa case selection of
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa Just idx -> do
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa setNodeFocus (theGraph graph) $ nodes' !! idx
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa Nothing -> return ()
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen KuksatranslateGraph :: GInfo -> ConvFunc -> LibFunc -> IO ()
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen KuksatranslateGraph (GInfo {libEnvIORef = ioRefProofStatus,
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa gi_LIB_NAME = ln,
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa gi_hetcatsOpts = opts
f345dca8aecfdbc7137a28dda45f9a5574d1fd14Eugen Kuksa }) convGraph showLib = do
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa le <- readIORef ioRefProofStatus
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa openTranslateGraph le ln opts (getDGLogic le) convGraph showLib
4ded733c298c9fd95db25858b897da482f4ab3e7Eugen KuksashowLibGraph :: GInfo -> LibFunc -> IO ()
4ded733c298c9fd95db25858b897da482f4ab3e7Eugen KuksashowLibGraph gInfo showLib = do
4ded733c298c9fd95db25858b897da482f4ab3e7Eugen Kuksa showLib gInfo
4ded733c298c9fd95db25858b897da482f4ab3e7Eugen Kuksa{- | it tries to perform the given action to the given graph.
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa If part of the given graph is not hidden, then the action can
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa be performed directly; otherwise the graph will be shown completely
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa firstly, and then the action will be performed, and after that the graph
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa will be hidden again.
4ded733c298c9fd95db25858b897da482f4ab3e7Eugen KuksaperformProofAction :: GInfo -> IO () -> IO ()
f345dca8aecfdbc7137a28dda45f9a5574d1fd14Eugen KuksaperformProofAction gInfo@(GInfo {descrIORef = event,
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa graphId = gid,
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa gi_GraphInfo = actGraphInfo
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa }) proofAction = do
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa let actionWithMessage = do
f345dca8aecfdbc7137a28dda45f9a5574d1fd14Eugen Kuksa showTemporaryMessage gid actGraphInfo
f382d86a384743a770cd5490a641e38ed1069c5cChristian Maeder "Applying development graph calculus proof rule..."
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa descr <- readIORef event
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder AGV.Result _ errorMsg <- checkHasHiddenNodes gid descr actGraphInfo
4937a0e373f619dc520799923acec42db5da5eb3Eugen Kuksa case errorMsg of
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder Nothing -> do
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht showNodes gInfo
f382d86a384743a770cd5490a641e38ed1069c5cChristian Maeder actionWithMessage
4ded733c298c9fd95db25858b897da482f4ab3e7Eugen Kuksa hideNodes gInfo
4ded733c298c9fd95db25858b897da482f4ab3e7Eugen Kuksa Just _ -> actionWithMessage
4ded733c298c9fd95db25858b897da482f4ab3e7Eugen Kuksa showTemporaryMessage gid actGraphInfo
4ded733c298c9fd95db25858b897da482f4ab3e7Eugen Kuksa "Development graph calculus proof rule finished."
f382d86a384743a770cd5490a641e38ed1069c5cChristian MaedersaveProofStatus :: GInfo -> FilePath -> IO ()
562e30787355109feb0133ffea2ad86b6c143c26Simon UlbrichtsaveProofStatus (GInfo {libEnvIORef = ioRefProofStatus,
d1c667fd9445963d9d31e2cf5d0ead15e77082a4cmaeder gi_LIB_NAME = ln,
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa gi_hetcatsOpts = opts
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa }) file = encapsulateWaitTermAct $ do
8723ec450f2e7a024230467c0c28a3f154905483cmaeder proofStatus <- readIORef ioRefProofStatus
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder writeShATermFile file (ln, lookupHistory ln proofStatus)
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder putIfVerbose opts 2 $ "Wrote " ++ file
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht-- | implementation of open menu, read in a proof status
12882fa70d12d9b56cbd850ccb4b724feb3c62d5Christian MaederopenProofStatus :: GInfo -> FilePath -> ConvFunc -> LibFunc
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder -> IO (Descr, GraphInfo, ConversionMaps)
986888e7f4d8ed681272a79c63f329ce8037063dcmaederopenProofStatus gInfo@(GInfo {libEnvIORef = ioRefProofStatus,
4bd27a2cb9efd5d8ff00b5cf823487403add724ecmaeder conversionMapsIORef = convRef,
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder gi_LIB_NAME = ln,
4bd27a2cb9efd5d8ff00b5cf823487403add724ecmaeder gi_hetcatsOpts = opts
2e76bbbed1c936bb0aee1753837e1c50416847a2Simon Ulbricht }) file convGraph showLib = do
8723ec450f2e7a024230467c0c28a3f154905483cmaeder mh <- readVerbose opts ln file
8723ec450f2e7a024230467c0c28a3f154905483cmaeder Nothing -> fail
8723ec450f2e7a024230467c0c28a3f154905483cmaeder $ "Could not read proof status from file '"
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder ++ file ++ "'"
1d65a799298f6b1253d774c22f61029e6eb99cadcmaeder Just h -> do
90d3a604eeb43972cef8bfd283a0118a4ad6e9e7cmaeder let libfile = libNameToFile opts ln
1d65a799298f6b1253d774c22f61029e6eb99cadcmaeder m <- anaLib opts { outtypes = [] } libfile
8723ec450f2e7a024230467c0c28a3f154905483cmaeder Nothing -> fail
7463a1bf64cfa90917e2afb6a5017ec411d2b3dbSimon Ulbricht $ "Could not read original development graph from '"
7f150d7930b47c297e184638ecd811b3656b0dadChristian Maeder ++ libfile ++ "'"
2e76bbbed1c936bb0aee1753837e1c50416847a2Simon Ulbricht Just (_, libEnv) -> case Map.lookup ln libEnv of
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder Nothing -> fail
bf51e183eda8e66f16795b35ce9a62468974b8e3Christian Maeder $ "Could not get original development graph for '"
2e76bbbed1c936bb0aee1753837e1c50416847a2Simon Ulbricht ++ showDoc ln "'"
f6a562e28240e4f9107c199ba7a8e500ccfbfa55Simon Ulbricht Just dg -> do
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder lockGlobal gInfo
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder oldEnv <- readIORef ioRefProofStatus
f382d86a384743a770cd5490a641e38ed1069c5cChristian Maeder let proofStatus = Map.insert ln
f382d86a384743a770cd5490a641e38ed1069c5cChristian Maeder (applyProofHistory h dg) oldEnv
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht writeIORef ioRefProofStatus proofStatus
22bb4a9063684a0f37dd7d0e6b21086adcc1e789Christian Maeder unlockGlobal gInfo
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht gInfo' <- copyGInfo gInfo
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht (gid, actGraphInfo, convMaps) <-
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht convGraph (gInfo' {gi_LIB_NAME = ln})
f6a562e28240e4f9107c199ba7a8e500ccfbfa55Simon Ulbricht "Proof Status " showLib
f6a562e28240e4f9107c199ba7a8e500ccfbfa55Simon Ulbricht writeIORef convRef convMaps
22bb4a9063684a0f37dd7d0e6b21086adcc1e789Christian Maeder redisplay gid actGraphInfo
41a3368af0eaad78c660477e7ded53b2ba85a275Christian Maeder return (gid, actGraphInfo, convMaps)
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht-- | apply a rule of the development graph calculus
2e76bbbed1c936bb0aee1753837e1c50416847a2Simon UlbrichtproofMenu :: GInfo
bf51e183eda8e66f16795b35ce9a62468974b8e3Christian Maeder -> (LibEnv -> IO (Res.Result LibEnv))
7f150d7930b47c297e184638ecd811b3656b0dadChristian MaederproofMenu gInfo@(GInfo { libEnvIORef = ioRefProofStatus
2e76bbbed1c936bb0aee1753837e1c50416847a2Simon Ulbricht , descrIORef = event
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder , conversionMapsIORef = convRef
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder , graphId = gid
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder , gi_LIB_NAME = ln
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder , gi_GraphInfo = actGraphInfo
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder , gi_hetcatsOpts = hOpts
2e76bbbed1c936bb0aee1753837e1c50416847a2Simon Ulbricht , proofGUIMVar = guiMVar
2e76bbbed1c936bb0aee1753837e1c50416847a2Simon Ulbricht , visibleNodesIORef = ioRefVisibleNodes
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder , globalHist = gHist
b532acc045cf5e26beb0691acc136d11188cce87Christian Maeder }) proofFun = do
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder filled <- tryPutMVar guiMVar Nothing
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder if not filled
d1c667fd9445963d9d31e2cf5d0ead15e77082a4cmaeder then readMVar guiMVar >>=
d1c667fd9445963d9d31e2cf5d0ead15e77082a4cmaeder (maybe (putIfVerbose hOpts 0 "proofMenu: ignored Nothing")
d1c667fd9445963d9d31e2cf5d0ead15e77082a4cmaeder putIfVerbose hOpts 4 $
d1c667fd9445963d9d31e2cf5d0ead15e77082a4cmaeder "proofMenu: Ignored Proof command; " ++
d1c667fd9445963d9d31e2cf5d0ead15e77082a4cmaeder "maybe a proof window is still open?"
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder lockGlobal gInfo
d1c667fd9445963d9d31e2cf5d0ead15e77082a4cmaeder proofStatus <- readIORef ioRefProofStatus
cbd64ad1d663565751cb9442f78a40ff96c6bed6Eugen Kuksa putIfVerbose hOpts 4 "Proof started via \"Proofs\" menu"
f382d86a384743a770cd5490a641e38ed1069c5cChristian Maeder Res.Result ds res <- proofFun proofStatus
f382d86a384743a770cd5490a641e38ed1069c5cChristian Maeder putIfVerbose hOpts 4 "Analyzing result of proof"
22bb4a9063684a0f37dd7d0e6b21086adcc1e789Christian Maeder Nothing -> do
22bb4a9063684a0f37dd7d0e6b21086adcc1e789Christian Maeder unlockGlobal gInfo
22bb4a9063684a0f37dd7d0e6b21086adcc1e789Christian Maeder mapM_ (putStrLn . show) ds
22bb4a9063684a0f37dd7d0e6b21086adcc1e789Christian Maeder Just newProofStatus -> do
22bb4a9063684a0f37dd7d0e6b21086adcc1e789Christian Maeder let newGr = lookupDGraph ln newProofStatus
e24da6268aa5791c7efd44571cafc0e36bf568dbChristian Maeder history = proofHistory newGr
e24da6268aa5791c7efd44571cafc0e36bf568dbChristian Maeder (guHist, grHist) <- takeMVar gHist
e24da6268aa5791c7efd44571cafc0e36bf568dbChristian Maeder doDump hOpts "PrintHistory" $ do
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa putStrLn "History"
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa print $ prettyHistory history
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa putMVar gHist
fdae29fce51a3b43f17e1cad0deb0f5381b9d3f6Christian Maeder (calcGlobalHistory proofStatus newProofStatus : guHist, grHist)
fdae29fce51a3b43f17e1cad0deb0f5381b9d3f6Christian Maeder descr <- readIORef event
fdae29fce51a3b43f17e1cad0deb0f5381b9d3f6Christian Maeder convMaps <- readIORef convRef
f382d86a384743a770cd5490a641e38ed1069c5cChristian Maeder (newDescr,convMapsAux) <- applyChanges gid ln actGraphInfo descr
bc76266f6a06f30dc77341fb2898d7f5765ff05cChristian Maeder ioRefVisibleNodes convMaps history
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht writeIORef ioRefProofStatus newProofStatus
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht unlockGlobal gInfo
2e2559f894aaa661b199e4fa00609f522bc5482aSimon Ulbricht writeIORef event newDescr
2e2559f894aaa661b199e4fa00609f522bc5482aSimon Ulbricht writeIORef convRef convMapsAux
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder hideShowNames gInfo False
05c714be15ce094d83f1b989cdf5236be78419bfSimon Ulbricht mGUIMVar <- tryTakeMVar guiMVar
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder maybe (fail $ "should be filled with Nothing after "++"proof attempt")
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder (const $ return ())
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon UlbrichtcalcGlobalHistory :: LibEnv -> LibEnv -> [LIB_NAME]
05c714be15ce094d83f1b989cdf5236be78419bfSimon UlbrichtcalcGlobalHistory old new = let
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder pHist = (\ ln le -> proofHistory $ lookupDGraph ln le)
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder length' = (\ ln le -> length $ pHist ln le)
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder changes = filter (\ ln -> pHist ln old /= pHist ln new) $ Map.keys old
f6a562e28240e4f9107c199ba7a8e500ccfbfa55Simon Ulbricht in concatMap (\ ln -> replicate (length' ln new - length' ln old) ln) changes
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen KuksanodeErr :: Descr -> IO ()
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen KuksanodeErr descr = error $ "node with descriptor " ++ show descr
f382d86a384743a770cd5490a641e38ed1069c5cChristian Maeder ++ " has no corresponding node in the development graph"
30ccae9374798a92124e1b294404f7b55ffbb412Christian MaedershowSpec :: Descr -> DGraphAndAGraphNode -> DGraph -> IO ()
fdae29fce51a3b43f17e1cad0deb0f5381b9d3f6Christian MaedershowSpec descr dgAndabstrNodeMap dgraph =
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder case InjMap.lookupWithB descr dgAndabstrNodeMap of
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder Nothing -> return ()
fdae29fce51a3b43f17e1cad0deb0f5381b9d3f6Christian Maeder Just (_, node) -> do
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder let sp = dgToSpec dgraph node
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder sp' = case sp of
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa Res.Result ds Nothing -> show $ vcat $ map pretty ds
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder Res.Result _ m -> showDoc m ""
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder createTextDisplay "Show spec" sp' [size(80,25)]
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder{- | auxiliary method for debugging. shows the number of the given node
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder in the abstraction graph
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon UlbrichtgetNumberOfNode :: Descr -> IO()
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon UlbrichtgetNumberOfNode descr =
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder let title = "Number of node"
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder-- make the node number consistent, the descritor should be reduced by one
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder in createTextDisplay title (showDoc (descr-1) "") [HTk.size(10,10)]
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder{- | outputs the signature of a node in a window;
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maederused by the node menu defined in initializeGraph -}
30ccae9374798a92124e1b294404f7b55ffbb412Christian MaedergetSignatureOfNode :: Descr -> DGraphAndAGraphNode -> DGraph -> IO()
30ccae9374798a92124e1b294404f7b55ffbb412Christian MaedergetSignatureOfNode descr dgAndabstrNodeMap dgraph =
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder case InjMap.lookupWithB descr dgAndabstrNodeMap of
05c714be15ce094d83f1b989cdf5236be78419bfSimon Ulbricht Just (_, node) ->
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht let dgnode = lab' (contextDG dgraph node)
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht title = "Signature of "++showName (dgn_name dgnode)
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht in createTextDisplay title (showDoc (dgn_sign dgnode) "")
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht Nothing -> nodeErr descr
f07364021546acc2fa5da55501bd6207b040f7bfEugen Kuksa fetches the theory from a node inside the IO Monad
f07364021546acc2fa5da55501bd6207b040f7bfEugen Kuksa (added by KL based on code in getTheoryOfNode) -}
f07364021546acc2fa5da55501bd6207b040f7bfEugen KuksalookupTheoryOfNode :: IORef LibEnv -> Descr -> DGraphAndAGraphNode ->
8723ec450f2e7a024230467c0c28a3f154905483cmaeder DGraph -> IO (Res.Result (Node,G_theory))
8723ec450f2e7a024230467c0c28a3f154905483cmaederlookupTheoryOfNode proofStatusRef descr dgAndabstrNodeMap _ = do
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder libEnv <- readIORef proofStatusRef
0bbc28585c7d42913167ff78a862ef25ea59e85eChristian Maeder (ln, node) <-
0bbc28585c7d42913167ff78a862ef25ea59e85eChristian Maeder maybeToResult nullRange ("Node "++show descr++" not found")
e4a035578fa9d1911eee097e2ed9a998c90c7805Christian Maeder $ InjMap.lookupWithB descr dgAndabstrNodeMap
0bbc28585c7d42913167ff78a862ef25ea59e85eChristian Maeder gth <- computeTheory libEnv ln node
0bbc28585c7d42913167ff78a862ef25ea59e85eChristian Maeder return (node, gth)
00d671cc654fe8d1571fa594bbebc9a2906ea880cmaeder{- | outputs the local axioms of a node in a window;
986888e7f4d8ed681272a79c63f329ce8037063dcmaederused by the node menu defined in initializeGraph-}
8723ec450f2e7a024230467c0c28a3f154905483cmaedergetLocalAxOfNode :: GInfo -> Descr -> DGraphAndAGraphNode -> DGraph -> IO ()
8723ec450f2e7a024230467c0c28a3f154905483cmaedergetLocalAxOfNode _ descr dgAndabstrNodeMap dgraph = do
fb9ec1e4dd1877781ec2b491fb0a6bcd38a7b04dcmaeder case InjMap.lookupWithB descr dgAndabstrNodeMap of
8723ec450f2e7a024230467c0c28a3f154905483cmaeder Just (_, node) ->
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder let dgnode = lab' (contextDG dgraph node) in
2ccdb81b4018e0a76f6dad3a940ba1241e98f6d9cmaeder if isDGRef dgnode then createTextDisplay
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder ("Local Axioms of "++ showName (dgn_name dgnode))
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder "no local axioms (reference node to other library)"
0bbc28585c7d42913167ff78a862ef25ea59e85eChristian Maeder else displayTheory "Local Axioms" node dgraph $ dgn_theory dgnode
0bbc28585c7d42913167ff78a862ef25ea59e85eChristian Maeder Nothing -> nodeErr descr
0bbc28585c7d42913167ff78a862ef25ea59e85eChristian Maeder{- | outputs the theory of a node in a window;
0bbc28585c7d42913167ff78a862ef25ea59e85eChristian Maederused by the node menu defined in initializeGraph-}
0bbc28585c7d42913167ff78a862ef25ea59e85eChristian MaedergetTheoryOfNode :: GInfo -> Descr -> DGraphAndAGraphNode -> DGraph -> IO ()
69ad4a5f0c84ae5d0cdd7518c3698c36342a47d9cmaedergetTheoryOfNode gInfo descr dgAndabstrNodeMap dgraph = do
69ad4a5f0c84ae5d0cdd7518c3698c36342a47d9cmaeder r <- lookupTheoryOfNode (libEnvIORef gInfo) descr dgAndabstrNodeMap dgraph
69ad4a5f0c84ae5d0cdd7518c3698c36342a47d9cmaeder showDiags (gi_hetcatsOpts gInfo) ds
4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder (Just (n, gth)) ->
8d2321e17a34951fbd52f68e9f9f148f0890e471Christian Maeder (showName $ dgn_name $ lab' (contextDG dgraph n))
ad5671edfa2ed767ec4fdc2f3099603d6fe8b97ecmaeder (addHasInHidingWarning dgraph n)
8d2321e17a34951fbd52f68e9f9f148f0890e471Christian Maeder _ -> return ()
8d2321e17a34951fbd52f68e9f9f148f0890e471Christian MaederdisplayTheory :: String -> Node -> DGraph -> G_theory -> IO ()
4ed68712ee368cbebfeaa327968583cb022e3c72Christian MaederdisplayTheory ext node dgraph gth =
69ad4a5f0c84ae5d0cdd7518c3698c36342a47d9cmaeder (showName $ dgn_name $ lab' (contextDG dgraph node))
69ad4a5f0c84ae5d0cdd7518c3698c36342a47d9cmaeder{- | translate the theory of a node in a window;
69ad4a5f0c84ae5d0cdd7518c3698c36342a47d9cmaederused by the node menu defined in initializeGraph-}
4ed68712ee368cbebfeaa327968583cb022e3c72Christian MaedertranslateTheoryOfNode :: GInfo -> Descr -> DGraphAndAGraphNode -> DGraph
f3fb0e085030be5bc309d946a6a9c20736dd3e0fSimon UlbrichttranslateTheoryOfNode gInfo@(GInfo {gi_hetcatsOpts = opts})
69ad4a5f0c84ae5d0cdd7518c3698c36342a47d9cmaeder descr dgAndabstrNodeMap dgraph = do
69ad4a5f0c84ae5d0cdd7518c3698c36342a47d9cmaeder libEnv <- readIORef $ libEnvIORef gInfo
69ad4a5f0c84ae5d0cdd7518c3698c36342a47d9cmaeder (ln, node) <-
116efc752fbf094a464c4f4940d9a450ab41c6c9Simon Ulbricht maybeToResult nullRange ("Node "++show descr++" not found")
8723ec450f2e7a024230467c0c28a3f154905483cmaeder $ InjMap.lookupWithB descr dgAndabstrNodeMap
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder th <- computeTheory libEnv ln node
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder return (node,th) ) of
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder Res.Result [] (Just (node,th)) -> do
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder Res.Result ds _ <- runResultT(
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder do G_theory lid sign _ sens _ <- return th
00d671cc654fe8d1571fa594bbebc9a2906ea880cmaeder -- find all comorphism paths starting from lid
853f27e556cb4e8c53f535df8e7b0ad665cf9bbcnotanartist let paths = findComorphismPaths logicGraph (sublogicOfTh th)
00d671cc654fe8d1571fa594bbebc9a2906ea880cmaeder -- let the user choose one
00d671cc654fe8d1571fa594bbebc9a2906ea880cmaeder sel <- lift $ listBox "Choose a logic translation"
00d671cc654fe8d1571fa594bbebc9a2906ea880cmaeder (map show paths)
00d671cc654fe8d1571fa594bbebc9a2906ea880cmaeder i <- case sel of
e5f71ad96ddbaafd3bf8ae0820df93e0db4b0527cmaeder Just j -> return j
526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder _ -> liftR $ fail "no logic translation chosen"
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder Comorphism cid <- return (paths!!i)
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder -- adjust lid's
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder let lidS = sourceLogic cid
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder lidT = targetLogic cid
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder sign' <- coerceSign lid lidS "" sign
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder sens' <- coerceThSens lid lidS "" sens
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder -- translate theory along chosen comorphism
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder (sign'',sens1) <-
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder liftR $ wrapMapTheory cid (plainSign sign', toNamedList sens')
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder "Translated Theory"
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder (showName $ dgn_name $ lab' (contextDG dgraph node))
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder (addHasInHidingWarning dgraph node)
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder (G_theory lidT (mkExtSign sign'') startSigId
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder (toThSens sens1) startThId)
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder showDiags opts ds
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder Res.Result ds _ -> showDiags opts ds
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder{- | outputs the sublogic of a node in a window;
eca54dc24f2c59cc51645115347a89ba2b40de36cmaederused by the node menu defined in initializeGraph -}
eca54dc24f2c59cc51645115347a89ba2b40de36cmaedergetSublogicOfNode :: IORef LibEnv -> Descr -> DGraphAndAGraphNode
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder -> DGraph -> IO()
eca54dc24f2c59cc51645115347a89ba2b40de36cmaedergetSublogicOfNode proofStatusRef descr dgAndabstrNodeMap dgraph = do
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder libEnv <- readIORef proofStatusRef
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder case InjMap.lookupWithB descr dgAndabstrNodeMap of
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder Just (ln, node) ->
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder let dgnode = lab' (contextDG dgraph node)
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder name = if isDGRef dgnode then emptyNodeName
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder else dgn_name dgnode
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder in case computeTheory libEnv ln node of
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder Res.Result _ (Just th) ->
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder let logstr = show $ sublogicOfTh th
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder title = "Sublogic of "++showName name
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder in createTextDisplay title logstr [HTk.size(30,10)]
5896f38ba2934056542cb7cb3e6359e88a622547Christian Maeder error $ "Could not compute theory for sublogic computation: "
e98c3d3efab62d97ebdeed52f4109d961f6432aaChristian Maeder ++ concatMap show ds
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder Nothing -> nodeErr descr
dbce18afddbe9b055be0e37f51e00d00d519b1cdChristian Maeder-- | prints the origin of the node
dbce18afddbe9b055be0e37f51e00d00d519b1cdChristian MaedershowOriginOfNode :: Descr -> DGraphAndAGraphNode -> DGraph -> IO()
5896f38ba2934056542cb7cb3e6359e88a622547Christian MaedershowOriginOfNode descr dgAndabstrNodeMap dgraph =
26acf851cacd7a31bdc9b25a42af9949942fa7c6Christian Maeder case InjMap.lookupWithB descr dgAndabstrNodeMap of
5896f38ba2934056542cb7cb3e6359e88a622547Christian Maeder Just (_, node) ->
5896f38ba2934056542cb7cb3e6359e88a622547Christian Maeder let dgnode = lab' (contextDG dgraph node) in
26acf851cacd7a31bdc9b25a42af9949942fa7c6Christian Maeder if isDGRef dgnode then error "showOriginOfNode: no DGNode" else
fd94a6f66ccb5cef99aa42069b61e4b8734dbd3fChristian Maeder let title = "Origin of node "++ showName (dgn_name dgnode)
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder in createTextDisplay title
bd90cf050d470eb42f6e0b79327cc53bd0f80dc9Christian Maeder (showDoc (dgn_origin dgnode) "") [HTk.size(30,10)]
bd90cf050d470eb42f6e0b79327cc53bd0f80dc9Christian Maeder Nothing -> nodeErr descr
de8eee2014437ec4020be15cd363257f87e79943Christian Maeder-- | Show proof status of a node
de8eee2014437ec4020be15cd363257f87e79943Christian MaedershowProofStatusOfNode :: GInfo -> Descr -> DGraphAndAGraphNode -> DGraph
bd90cf050d470eb42f6e0b79327cc53bd0f80dc9Christian MaedershowProofStatusOfNode _ descr dgAndabstrNodeMap dgraph =
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder case InjMap.lookupWithB descr dgAndabstrNodeMap of
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder Just (_, node) ->
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder do let dgnode = lab' (contextDG dgraph node)
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder let stat = showStatusAux dgnode
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder let title = "Proof status of node "++showName (dgn_name dgnode)
bd90cf050d470eb42f6e0b79327cc53bd0f80dc9Christian Maeder createTextDisplay title stat [HTk.size(105,55)]
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder Nothing -> nodeErr descr
5a448e9be8c4482a978b174b744237757335140fChristian MaedershowStatusAux :: DGNodeLab -> String
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian MaedershowStatusAux dgnode =
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder case dgn_theory dgnode of
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder G_theory _ _ _ sens _ ->
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder let goals = OMap.filter (not . isAxiom) sens
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder (proven,open) = OMap.partition isProvenSenStatus goals
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder consGoal = "\nconservativity of this node"
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder in "Proven proof goals:\n"
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder ++ showDoc proven ""
142fd5dd7fcfa170f08b2a0ab232859428f6e3c2Christian Maeder ++ if not $ hasOpenConsStatus True dgnode
142fd5dd7fcfa170f08b2a0ab232859428f6e3c2Christian Maeder then consGoal
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder ++ "\nOpen proof goals:\n"
3f08b178a44369b618a5e0b5f1fc2207fe043aabChristian Maeder ++ showDoc open ""
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder ++ if hasOpenConsStatus False dgnode
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder then consGoal
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder-- | start local theorem proving or consistency checking at a node
986888e7f4d8ed681272a79c63f329ce8037063dcmaederproveAtNode :: Bool -> GInfo -> Descr -> DGraphAndAGraphNode -> DGraph -> IO ()
986888e7f4d8ed681272a79c63f329ce8037063dcmaederproveAtNode checkCons
ea5ccb1c6e89486a54e1f4bd95840147e96093edChristian Maeder gInfo@(GInfo { libEnvIORef = ioRefProofStatus
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder , gi_LIB_NAME = ln
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder dgAndabstrNodeMap
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder case InjMap.lookupWithB descr dgAndabstrNodeMap of
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder Just libNode -> do
26acf851cacd7a31bdc9b25a42af9949942fa7c6Christian Maeder let (node, dgn) = labNode' (contextDG dgraph $ snd libNode)
4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder (dgraph',dgn') <- case hasLock dgn of
016b8f06b709deef8c24b3d6c59f085857a166d4Christian Maeder True -> return (dgraph, dgn)
2ccdb81b4018e0a76f6dad3a940ba1241e98f6d9cmaeder False -> do
2ccdb81b4018e0a76f6dad3a940ba1241e98f6d9cmaeder lockGlobal gInfo
2ccdb81b4018e0a76f6dad3a940ba1241e98f6d9cmaeder le <- readIORef ioRefProofStatus
2ccdb81b4018e0a76f6dad3a940ba1241e98f6d9cmaeder (dgraph',dgn') <- initLocking (lookupDGraph ln le) (node, dgn)
016b8f06b709deef8c24b3d6c59f085857a166d4Christian Maeder writeIORef ioRefProofStatus $ Map.insert ln dgraph' le
fb9ec1e4dd1877781ec2b491fb0a6bcd38a7b04dcmaeder unlockGlobal gInfo
2ccdb81b4018e0a76f6dad3a940ba1241e98f6d9cmaeder return (dgraph',dgn')
2ccdb81b4018e0a76f6dad3a940ba1241e98f6d9cmaeder locked <- tryLockLocal dgn'
2ccdb81b4018e0a76f6dad3a940ba1241e98f6d9cmaeder case locked of
2ccdb81b4018e0a76f6dad3a940ba1241e98f6d9cmaeder False -> createTextDisplay "Error" "Proofwindow already open"
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder let action = (do
2ccdb81b4018e0a76f6dad3a940ba1241e98f6d9cmaeder le <- readIORef ioRefProofStatus
2ccdb81b4018e0a76f6dad3a940ba1241e98f6d9cmaeder guiMVar <- newMVar Nothing
2ccdb81b4018e0a76f6dad3a940ba1241e98f6d9cmaeder res <- basicInferenceNode checkCons logicGraph libNode
2ccdb81b4018e0a76f6dad3a940ba1241e98f6d9cmaeder ln guiMVar le
2ccdb81b4018e0a76f6dad3a940ba1241e98f6d9cmaeder runProveAtNode gInfo (node, dgn') res)
2ccdb81b4018e0a76f6dad3a940ba1241e98f6d9cmaeder case checkCons || not (hasIncomingHidingEdge dgraph' $ snd libNode) of
2ccdb81b4018e0a76f6dad3a940ba1241e98f6d9cmaeder True -> action
016b8f06b709deef8c24b3d6c59f085857a166d4Christian Maeder False -> GUI.HTkUtils.createInfoDisplayWithTwoButtons "Warning"
2ccdb81b4018e0a76f6dad3a940ba1241e98f6d9cmaeder "This node has incoming hiding links!!!" "Prove anyway"
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder unlockLocal dgn'
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder Nothing -> nodeErr descr
eca54dc24f2c59cc51645115347a89ba2b40de36cmaederrunProveAtNode :: GInfo -> LNode DGNodeLab -> Res.Result LibEnv -> IO ()
eca54dc24f2c59cc51645115347a89ba2b40de36cmaederrunProveAtNode gInfo@(GInfo {gi_LIB_NAME = ln}) (v,_)
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder (Res.Result {maybeResult = mle}) = case mle of
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder Just le -> case matchDG v $ lookupDGraph ln le of
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder (Just(_,_,dgn,_), _) -> proofMenu gInfo (mergeDGNodeLab gInfo (v,dgn))
2ccdb81b4018e0a76f6dad3a940ba1241e98f6d9cmaeder _ -> error $ "mergeDGNodeLab no such node: " ++ show v
2ccdb81b4018e0a76f6dad3a940ba1241e98f6d9cmaeder Nothing -> return ()
eca54dc24f2c59cc51645115347a89ba2b40de36cmaedermergeDGNodeLab :: GInfo -> LNode DGNodeLab -> LibEnv -> IO (Res.Result LibEnv)
df67ddf64192bfcae6ece65255ad796a17cbe532Christian MaedermergeDGNodeLab (GInfo{gi_LIB_NAME = ln}) (v, new_dgn) le = do
4d54e7814b18ce142359c92a5868e6dcff9219b5Christian Maeder let dg = lookupDGraph ln le
4d54e7814b18ce142359c92a5868e6dcff9219b5Christian Maeder le' <- case matchDG v dg of
142fd5dd7fcfa170f08b2a0ab232859428f6e3c2Christian Maeder (Just(p, _, old_dgn, s), g) -> do
4d54e7814b18ce142359c92a5868e6dcff9219b5Christian Maeder theory <- joinG_sentences (dgn_theory old_dgn) $ dgn_theory new_dgn
7be1485dfcaa5decb3586d194ff4b2443668e349Simon Ulbricht new_dgn' = old_dgn{dgn_theory = theory}
7be1485dfcaa5decb3586d194ff4b2443668e349Simon Ulbricht dg' = addToProofHistoryDG ([],[SetNodeLab old_dgn (v, new_dgn')]) $
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder g{dgBody = (p, v, new_dgn', s) & (dgBody g)}
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder return $ Map.insert ln dg' le
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder _ -> error $ "mergeDGNodeLab no such node: " ++ show v
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder return Res.Result { diags = [], maybeResult = Just le'}
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder-- | print the id of the edge
f675b8f0a612e37472640da57b48d795bef4427eChristian MaedershowIDOfEdge :: Descr -> Maybe (LEdge DGLinkLab) -> IO ()
f675b8f0a612e37472640da57b48d795bef4427eChristian MaedershowIDOfEdge _ (Just (_, _, linklab)) =
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder createTextDisplay "ID of Edge" (show $ dgl_id linklab) [HTk.size(30,10)]
f675b8f0a612e37472640da57b48d795bef4427eChristian MaedershowIDOfEdge descr Nothing =
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder createTextDisplay "Error"
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder ("edge " ++ show descr ++ " has no corresponding edge"
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder ++ "in the development graph") [HTk.size(30,10)]
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder-- | print the morphism of the edge
7a3e20d1b7fe1b0e47c0b9138716b0bbc8ecf1f6Christian MaedershowMorphismOfEdge :: Descr -> Maybe (LEdge DGLinkLab) -> IO ()
7a3e20d1b7fe1b0e47c0b9138716b0bbc8ecf1f6Christian MaedershowMorphismOfEdge _ (Just (_,_,linklab)) =
7a3e20d1b7fe1b0e47c0b9138716b0bbc8ecf1f6Christian Maeder createTextDisplay "Signature morphism"
7a3e20d1b7fe1b0e47c0b9138716b0bbc8ecf1f6Christian Maeder (showDoc (dgl_morphism linklab) "" ++ hidingMorph)
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder hidingMorph = case dgl_type linklab of
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder HidingThm morph _ -> "\n ++++++ \n"
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder ++ showDoc morph ""
f675b8f0a612e37472640da57b48d795bef4427eChristian MaedershowMorphismOfEdge descr Nothing =
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder createTextDisplay "Error"
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder ("edge " ++ show descr ++ " has no corresponding edge"
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder ++ "in the development graph") [HTk.size(30,10)]
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder-- | print the origin of the edge
f675b8f0a612e37472640da57b48d795bef4427eChristian MaedershowOriginOfEdge :: Descr -> Maybe (LEdge DGLinkLab) -> IO ()
f675b8f0a612e37472640da57b48d795bef4427eChristian MaedershowOriginOfEdge _ (Just (_,_,linklab)) =
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder createTextDisplay "Origin of link"
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder (showDoc (dgl_origin linklab) "") [HTk.size(30,10)]
f675b8f0a612e37472640da57b48d795bef4427eChristian MaedershowOriginOfEdge descr Nothing =
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder createTextDisplay "Error"
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder ("edge " ++ show descr ++ " has no corresponding edge"
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder ++ "in the development graph") [HTk.size(30,10)]
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder-- | print the proof base of the edge
f675b8f0a612e37472640da57b48d795bef4427eChristian MaedershowProofStatusOfThm :: Descr -> Maybe (LEdge DGLinkLab) -> IO ()
f675b8f0a612e37472640da57b48d795bef4427eChristian MaedershowProofStatusOfThm _ (Just ledge) =
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder createTextSaveDisplay "Proof Status" "proofstatus.txt"
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder (showDoc (getProofStatusOfThm ledge) "\n")
f675b8f0a612e37472640da57b48d795bef4427eChristian MaedershowProofStatusOfThm descr Nothing =
526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder -- why putStrLn here and no createTextDisplay elsewhere with this message
df67ddf64192bfcae6ece65255ad796a17cbe532Christian Maeder putStrLn ("edge " ++ show descr ++ " has no corresponding edge"
df67ddf64192bfcae6ece65255ad796a17cbe532Christian Maeder ++ "in the development graph")
df67ddf64192bfcae6ece65255ad796a17cbe532Christian Maeder-- | check conservativity of the edge
df67ddf64192bfcae6ece65255ad796a17cbe532Christian MaedercheckconservativityOfEdge :: Descr -> GInfo -> Maybe (LEdge DGLinkLab) -> IO()
233754e153e665aa748bf8b45bd8b1938b6c21a7Christian MaedercheckconservativityOfEdge _ gInfo
8723ec450f2e7a024230467c0c28a3f154905483cmaeder (Just (source,target,linklab)) = do
8723ec450f2e7a024230467c0c28a3f154905483cmaeder libEnv <- readIORef $ libEnvIORef gInfo
8723ec450f2e7a024230467c0c28a3f154905483cmaeder let dgraph = lookupDGraph (gi_LIB_NAME gInfo) libEnv
e4a035578fa9d1911eee097e2ed9a998c90c7805Christian Maeder dgtar = lab' (contextDG dgraph target)
7463a1bf64cfa90917e2afb6a5017ec411d2b3dbSimon Ulbricht if isDGRef dgtar then error "checkconservativityOfEdge: no DGNode" else do
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa G_theory lid _ _ sens _ <- return $ dgn_theory dgtar
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa GMorphism cid _ _ morphism2 _ <- return $ dgl_morphism linklab
8723ec450f2e7a024230467c0c28a3f154905483cmaeder morphism2' <- coerceMorphism (targetLogic cid) lid
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder "checkconservativityOfEdge" morphism2
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder let th = case computeTheory libEnv (gi_LIB_NAME gInfo) source of
5bedf8c26d27eac08962c78379bcb2e5cb529036Christian Maeder Res.Result _ (Just th1) -> th1
233754e153e665aa748bf8b45bd8b1938b6c21a7Christian Maeder _ -> error "checkconservativityOfEdge: computeTheory"
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa G_theory lid1 sign1 _ sens1 _ <- return th
4ded733c298c9fd95db25858b897da482f4ab3e7Eugen Kuksa sign2 <- coerceSign lid1 lid "checkconservativityOfEdge.coerceSign" sign1
703004db20b23870f080c4d9640729b19b7c2288Eugen Kuksa sens2 <- coerceThSens lid1 lid "" sens1
5bedf8c26d27eac08962c78379bcb2e5cb529036Christian Maeder conservativityCheck lid
2e76bbbed1c936bb0aee1753837e1c50416847a2Simon Ulbricht (plainSign sign2, toNamedList sens2)
2e76bbbed1c936bb0aee1753837e1c50416847a2Simon Ulbricht morphism2' $ toNamedList sens
11c3a215d5cf043181e83929f1ce214df65cb587Christian Maeder showRes = case res of
1defc008da0fae281b776ffe464e2fef549804b5cmaeder Just(Just True) -> "The link is conservative"
2e76bbbed1c936bb0aee1753837e1c50416847a2Simon Ulbricht Just(Just False) -> "The link is not conservative"
bec39c85aaeeea5e171f391166f9d46a5492618aEugen Kuksa _ -> "Could not determine whether link is conservative"
103848575cd92efdb3d4dc9809c16254d7415c2ecmaeder myDiags = unlines (map show ds)
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder createTextDisplay "Result of conservativity check"
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder (showRes ++ "\n" ++ myDiags) [HTk.size(50,50)]
986888e7f4d8ed681272a79c63f329ce8037063dcmaedercheckconservativityOfEdge descr _ Nothing =
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder createTextDisplay "Error"
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder ("edge " ++ show descr ++ " has no corresponding edge "
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder ++ "in the development graph") [HTk.size(30,10)]
986888e7f4d8ed681272a79c63f329ce8037063dcmaedergetProofStatusOfThm :: (LEdge DGLinkLab) -> ThmLinkStatus
986888e7f4d8ed681272a79c63f329ce8037063dcmaedergetProofStatusOfThm (_,_,label) =
ea5ccb1c6e89486a54e1f4bd95840147e96093edChristian Maeder case (dgl_type label) of
ea5ccb1c6e89486a54e1f4bd95840147e96093edChristian Maeder (LocalThm proofStatus _ _) -> proofStatus
1defc008da0fae281b776ffe464e2fef549804b5cmaeder (GlobalThm proofStatus _ _) -> proofStatus
5c89bca8b187e75ff87be1afe964c1aeba8a7725Eugen Kuksa (HidingThm _ proofStatus) -> proofStatus -- richtig?
5c89bca8b187e75ff87be1afe964c1aeba8a7725Eugen Kuksa _ -> error "the given edge is not a theorem"
d102a920578426a89411cc8dabe47d7a881eab8fEugen Kuksa{- | converts the nodes of the development graph, if it has any,
d102a920578426a89411cc8dabe47d7a881eab8fEugen Kuksaand returns the resulting conversion maps
5c89bca8b187e75ff87be1afe964c1aeba8a7725Eugen Kuksaif the graph is empty the conversion maps are returned unchanged-}
0552b690f40f3d73d4d4b2241fcb24d2ecc0c21eEugen KuksaconvertNodes :: ConversionMaps -> Descr -> GraphInfo -> DGraph
0552b690f40f3d73d4d4b2241fcb24d2ecc0c21eEugen Kuksa -> LIB_NAME -> IO ConversionMaps
950875ac099734b9eaccf4233773e6df00477f22Eugen KuksaconvertNodes convMaps descr grInfo dgraph libname
950875ac099734b9eaccf4233773e6df00477f22Eugen Kuksa | isEmptyDG dgraph = return convMaps
950875ac099734b9eaccf4233773e6df00477f22Eugen Kuksa | otherwise = convertNodesAux convMaps
465c6b72e8e480969b5f08658e394992bcc08bfcSimon Ulbricht (labNodesDG dgraph)
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa{- | auxiliary function for convertNodes if the given list of nodes is
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksaemtpy, it returns the conversion maps unchanged otherwise it adds the
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksaconverted first node to the abstract graph and to the affected
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksaconversion maps and afterwards calls itself with the remaining node
2ed0ce5565323b3a233d9258b0ff63dfa4a8e8e1Eugen KuksaconvertNodesAux :: ConversionMaps -> Descr -> GraphInfo ->
2ed0ce5565323b3a233d9258b0ff63dfa4a8e8e1Eugen Kuksa [LNode DGNodeLab] -> LIB_NAME -> IO ConversionMaps
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen KuksaconvertNodesAux convMaps _ _ [] _ = return convMaps
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen KuksaconvertNodesAux convMaps descr grInfo ((node,dgnode) : lNodes) libname =
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa do let nodetype = getDGNodeType dgnode
2ed0ce5565323b3a233d9258b0ff63dfa4a8e8e1Eugen Kuksa AGV.Result newDescr _ <- addnode descr
2ed0ce5565323b3a233d9258b0ff63dfa4a8e8e1Eugen Kuksa (getDGNodeName dgnode)
2ed0ce5565323b3a233d9258b0ff63dfa4a8e8e1Eugen Kuksa convertNodesAux convMaps
2ed0ce5565323b3a233d9258b0ff63dfa4a8e8e1Eugen Kuksa { dgAndabstrNode = InjMap.insert (libname, node) newDescr
18548c6cc2dff13bf9f5f08b3f6cde6ca914df1dChristian Maeder (dgAndabstrNode convMaps)
b0bf54186358372d2be6a95e36ed3ef5fd64b7a3Christian Maeder } descr grInfo lNodes libname
7c661ba558707feaa5d8a299365c2191e1afabb2Christian Maeder{- | converts the edges of the development graph
7c661ba558707feaa5d8a299365c2191e1afabb2Christian Maederworks the same way as convertNods does-}
7c661ba558707feaa5d8a299365c2191e1afabb2Christian MaederconvertEdges :: ConversionMaps -> Descr -> GraphInfo -> DGraph
3abf8a8f697c113233027f0c865ed57deb274542Christian Maeder -> LIB_NAME -> IO ConversionMaps
8ca6b0820806f62042d84a1fff11599db55591c4Christian MaederconvertEdges convMaps descr grInfo dgraph libname
dbce18afddbe9b055be0e37f51e00d00d519b1cdChristian Maeder | isEmptyDG dgraph = return convMaps
1defc008da0fae281b776ffe464e2fef549804b5cmaeder | otherwise = convertEdgesAux convMaps
18548c6cc2dff13bf9f5f08b3f6cde6ca914df1dChristian Maeder (labEdgesDG dgraph)
23ee432f8fe96e07f2523ca7c4bda9bcce1ea6f0Simon Ulbricht-- | auxiliary function for convertEges
1defc008da0fae281b776ffe464e2fef549804b5cmaederconvertEdgesAux :: ConversionMaps -> Descr -> GraphInfo ->
1defc008da0fae281b776ffe464e2fef549804b5cmaeder [LEdge DGLinkLab] -> LIB_NAME -> IO ConversionMaps
1defc008da0fae281b776ffe464e2fef549804b5cmaederconvertEdgesAux convMaps _ _ [] _ = return convMaps
5727dbcb926ede2e7b05f43685476ce656ce01e4Christian MaederconvertEdgesAux convMaps descr grInfo (ledge@(src,tar,edgelab) : lEdges)
5727dbcb926ede2e7b05f43685476ce656ce01e4Christian Maeder do let srcnode = InjMap.lookupWithA (libname,src) (dgAndabstrNode convMaps)
5727dbcb926ede2e7b05f43685476ce656ce01e4Christian Maeder tarnode = InjMap.lookupWithA (libname,tar) (dgAndabstrNode convMaps)
5727dbcb926ede2e7b05f43685476ce656ce01e4Christian Maeder case (srcnode, tarnode) of
5727dbcb926ede2e7b05f43685476ce656ce01e4Christian Maeder (Just s, Just t) -> do
5727dbcb926ede2e7b05f43685476ce656ce01e4Christian Maeder AGV.Result newDescr msg <- addlink descr (getDGLinkType edgelab)
5727dbcb926ede2e7b05f43685476ce656ce01e4Christian Maeder "" (Just ledge) s t grInfo
43d8d7472d3a0a78d9a2c85122815a81deb8689aChristian Maeder Nothing -> return ()
c99b0eb6632087d502dd4269599c5aa68a148eebSimon Ulbricht Just err -> fail err
bb9642ff292545658dc11251b83a7b7af3c1fccbChristian Maeder newConvMaps <- convertEdgesAux convMaps
be1ce1c2b2819ef32743136c13101f1927375311Christian Maeder { dgAndabstrEdge = InjMap.insert (libname,
5727dbcb926ede2e7b05f43685476ce656ce01e4Christian Maeder (src, tar, showDoc edgelab ""))
92ae4d5885ea837ffe3dae9b2de742f871229b94Christian Maeder newDescr (dgAndabstrEdge convMaps)
92ae4d5885ea837ffe3dae9b2de742f871229b94Christian Maeder } descr grInfo lEdges libname
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder return newConvMaps
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder _ -> error "Cannot find nodes"
5727dbcb926ede2e7b05f43685476ce656ce01e4Christian Maeder-- | show library referened by a DGRef node (=node drawn as a box)
5727dbcb926ede2e7b05f43685476ce656ce01e4Christian MaedershowReferencedLibrary :: Descr -> GInfo -> ConvFunc -> LibFunc
5727dbcb926ede2e7b05f43685476ce656ce01e4Christian Maeder -> IO (Descr, GraphInfo, ConversionMaps)
5727dbcb926ede2e7b05f43685476ce656ce01e4Christian MaedershowReferencedLibrary
ccd9cf19d129595770d592d3d0d80c6619f7a141Eugen Kuksa descr gInfo@(GInfo { libEnvIORef = ioRefProofStatus
5a89ec196dfd3e342f6d4ef3a318bc9992190bbaChristian Maeder , conversionMapsIORef = convRef}) convGraph showLib = do
5a89ec196dfd3e342f6d4ef3a318bc9992190bbaChristian Maeder convMaps <- readIORef convRef
e2374b99721dab596695fda64b96aecc5ecf23c9Eugen Kuksa libname2dgMap <- readIORef ioRefProofStatus
ccd9cf19d129595770d592d3d0d80c6619f7a141Eugen Kuksa case InjMap.lookupWithB descr (dgAndabstrNode convMaps) of
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa Just (libname,node) ->
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa case Map.lookup libname libname2dgMap of
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder Just dgraph ->
5a89ec196dfd3e342f6d4ef3a318bc9992190bbaChristian Maeder do let (_, refNode) = labNode' (contextDG dgraph node)
2ed0ce5565323b3a233d9258b0ff63dfa4a8e8e1Eugen Kuksa refLibname = if isDGRef refNode then dgn_libname refNode
2ed0ce5565323b3a233d9258b0ff63dfa4a8e8e1Eugen Kuksa else error "showReferencedLibrary"
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa case Map.lookup refLibname libname2dgMap of
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa Just _ -> do
2ed0ce5565323b3a233d9258b0ff63dfa4a8e8e1Eugen Kuksa gInfo' <- copyGInfo gInfo
2ed0ce5565323b3a233d9258b0ff63dfa4a8e8e1Eugen Kuksa (gid,gv,cm) <- convGraph (gInfo'{gi_LIB_NAME = refLibname})
2ed0ce5565323b3a233d9258b0ff63dfa4a8e8e1Eugen Kuksa "development graph" showLib
2ed0ce5565323b3a233d9258b0ff63dfa4a8e8e1Eugen Kuksa deactivateGraphWindow gid gv
5a89ec196dfd3e342f6d4ef3a318bc9992190bbaChristian Maeder redisplay gid gv
d4d3caef3878e583180d50f670957f1406d1effbcmaeder hideNodes gInfo'
d4d3caef3878e583180d50f670957f1406d1effbcmaeder layoutImproveAll gid gv
dbce18afddbe9b055be0e37f51e00d00d519b1cdChristian Maeder showTemporaryMessage gid gv "Development Graph initialized."
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder activateGraphWindow gid gv
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder return (gid,gv,cm)
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder Nothing -> error $ "The referenced library ("
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder ++ show refLibname
7d0db235b17b2109cd45fa50e6d1bbc77823f81dEugen Kuksa ++ ") is unknown"
7d0db235b17b2109cd45fa50e6d1bbc77823f81dEugen Kuksa Nothing -> error $ "Selected node belongs to unknown library: "
7d0db235b17b2109cd45fa50e6d1bbc77823f81dEugen Kuksa ++ show libname
d102a920578426a89411cc8dabe47d7a881eab8fEugen Kuksa error $ "there is no node with the descriptor " ++ show descr
7d0db235b17b2109cd45fa50e6d1bbc77823f81dEugen Kuksa-- | prune displayed graph to subtree of selected node
0552b690f40f3d73d4d4b2241fcb24d2ecc0c21eEugen KuksashowJustSubtree :: Descr -> Descr -> GInfo
0552b690f40f3d73d4d4b2241fcb24d2ecc0c21eEugen Kuksa -> IO (Descr, [[Node]], Maybe String)
950875ac099734b9eaccf4233773e6df00477f22Eugen KuksashowJustSubtree descr abstractGraph
950875ac099734b9eaccf4233773e6df00477f22Eugen Kuksa (GInfo {libEnvIORef = ioRefProofStatus,
950875ac099734b9eaccf4233773e6df00477f22Eugen Kuksa conversionMapsIORef = convRef,
950875ac099734b9eaccf4233773e6df00477f22Eugen Kuksa visibleNodesIORef = visibleNodesRef,
950875ac099734b9eaccf4233773e6df00477f22Eugen Kuksa gi_GraphInfo = actGraphInfo}) = do
5727dbcb926ede2e7b05f43685476ce656ce01e4Christian Maeder convMaps <- readIORef convRef
18548c6cc2dff13bf9f5f08b3f6cde6ca914df1dChristian Maeder libname2dgMap <- readIORef ioRefProofStatus
b532acc045cf5e26beb0691acc136d11188cce87Christian Maeder visibleNodes <- readIORef visibleNodesRef
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder case InjMap.lookupWithB descr (dgAndabstrNode convMaps) of
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder Just (libname,parentNode) ->
b532acc045cf5e26beb0691acc136d11188cce87Christian Maeder case Map.lookup libname libname2dgMap of
b532acc045cf5e26beb0691acc136d11188cce87Christian Maeder Just dgraph ->
df67ddf64192bfcae6ece65255ad796a17cbe532Christian Maeder do let allNodes = getNodeDescriptors (head visibleNodes)
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa libname convMaps
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa dgNodesOfSubtree = nub (parentNode : getNodesOfSubtree dgraph
18d589be75aa0cbaacae9ab2884c0b07943de024Eugen Kuksa (head visibleNodes) parentNode)
f674d7a58db3f991300a708f3799d80c369781f8Eugen Kuksa -- the selected node (parentNode) shall not be hidden either,
f674d7a58db3f991300a708f3799d80c369781f8Eugen Kuksa -- and we already know its descriptor (descr)
f674d7a58db3f991300a708f3799d80c369781f8Eugen Kuksa nodesOfSubtree = getNodeDescriptors dgNodesOfSubtree
f674d7a58db3f991300a708f3799d80c369781f8Eugen Kuksa libname convMaps
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa nodesToHide = filter (`notElem` nodesOfSubtree) allNodes
f674d7a58db3f991300a708f3799d80c369781f8Eugen Kuksa AGV.Result eventDescr errorMsg <- hidenodes abstractGraph
f674d7a58db3f991300a708f3799d80c369781f8Eugen Kuksa nodesToHide actGraphInfo
f674d7a58db3f991300a708f3799d80c369781f8Eugen Kuksa return (eventDescr, (dgNodesOfSubtree:visibleNodes), errorMsg)
f674d7a58db3f991300a708f3799d80c369781f8Eugen Kuksa Nothing -> error $
f674d7a58db3f991300a708f3799d80c369781f8Eugen Kuksa "showJustSubtree: Selected node belongs to unknown library: "
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa ++ show libname
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa Nothing -> error $ "showJustSubtree: there is no node with the descriptor "
f674d7a58db3f991300a708f3799d80c369781f8Eugen Kuksa ++ show descr
f674d7a58db3f991300a708f3799d80c369781f8Eugen KuksagetNodeDescriptors :: [Node] -> LIB_NAME -> ConversionMaps -> [Descr]
55ab20b85d8838544a83c1ef2e01e1f2b2da7496Eugen KuksagetNodeDescriptors [] _ _ = []
f674d7a58db3f991300a708f3799d80c369781f8Eugen KuksagetNodeDescriptors (node:nodelist) libname convMaps =
f674d7a58db3f991300a708f3799d80c369781f8Eugen Kuksa case InjMap.lookupWithA (libname, node) (dgAndabstrNode convMaps) of
55ab20b85d8838544a83c1ef2e01e1f2b2da7496Eugen Kuksa Just descr -> descr:(getNodeDescriptors nodelist libname convMaps)
55ab20b85d8838544a83c1ef2e01e1f2b2da7496Eugen Kuksa Nothing -> error $ "getNodeDescriptors: There is no descriptor for dgnode "
55ab20b85d8838544a83c1ef2e01e1f2b2da7496Eugen Kuksa ++ show node
55ab20b85d8838544a83c1ef2e01e1f2b2da7496Eugen KuksagetNodesOfSubtree :: DGraph -> [Node] -> Node -> [Node]
55ab20b85d8838544a83c1ef2e01e1f2b2da7496Eugen KuksagetNodesOfSubtree dgraph visibleNodes node =
55ab20b85d8838544a83c1ef2e01e1f2b2da7496Eugen Kuksa concat (map (getNodesOfSubtree dgraph remainingVisibleNodes) predOfNode)
f674d7a58db3f991300a708f3799d80c369781f8Eugen Kuksa ++ predOfNode
f674d7a58db3f991300a708f3799d80c369781f8Eugen Kuksa where predOfNode = [ n | n <- (preDG dgraph node), elem n visibleNodes]
f674d7a58db3f991300a708f3799d80c369781f8Eugen Kuksa remainingVisibleNodes =
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa [ n | n <- visibleNodes, notElem n predOfNode]
f674d7a58db3f991300a708f3799d80c369781f8Eugen Kuksa-- | apply the changes of first history item (computed by proof rules,
f674d7a58db3f991300a708f3799d80c369781f8Eugen Kuksa-- see folder Proofs) to the displayed development graph
f674d7a58db3f991300a708f3799d80c369781f8Eugen KuksaapplyChanges :: Descr -> LIB_NAME -> GraphInfo -> Descr -> IORef [[Node]]
f674d7a58db3f991300a708f3799d80c369781f8Eugen Kuksa -> ConversionMaps -> [([DGRule],[DGChange])]
f674d7a58db3f991300a708f3799d80c369781f8Eugen Kuksa -> IO (Descr, ConversionMaps)
f674d7a58db3f991300a708f3799d80c369781f8Eugen KuksaapplyChanges _ _ _ eventDescr _ convMaps [] = return (eventDescr,convMaps)
f674d7a58db3f991300a708f3799d80c369781f8Eugen KuksaapplyChanges gid libname grInfo eventDescr ioRefVisibleNodes convMaps
f674d7a58db3f991300a708f3799d80c369781f8Eugen Kuksa ((_, historyElem) : _) =
f674d7a58db3f991300a708f3799d80c369781f8Eugen Kuksa applyChangesAux gid libname grInfo ioRefVisibleNodes (eventDescr, convMaps)
f674d7a58db3f991300a708f3799d80c369781f8Eugen Kuksa $ removeContraryChanges historyElem
f674d7a58db3f991300a708f3799d80c369781f8Eugen Kuksa-- | auxiliary function for applyChanges
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen KuksaapplyChangesAux :: Descr -> LIB_NAME -> GraphInfo -> IORef [[Node]]
f674d7a58db3f991300a708f3799d80c369781f8Eugen Kuksa -> (Descr, ConversionMaps) -> [DGChange]
29d783ee57c3d959b74fea330bb21ff7e5b8e185Christian Maeder -> IO (Descr, ConversionMaps)
29d783ee57c3d959b74fea330bb21ff7e5b8e185Christian MaederapplyChangesAux gid libname grInfo ioRefVisibleNodes
29d783ee57c3d959b74fea330bb21ff7e5b8e185Christian Maeder (eventDescr, convMaps) changeList =
29d783ee57c3d959b74fea330bb21ff7e5b8e185Christian Maeder case changeList of
29d783ee57c3d959b74fea330bb21ff7e5b8e185Christian Maeder [] -> return (eventDescr, convMaps)
29d783ee57c3d959b74fea330bb21ff7e5b8e185Christian Maeder changes@(_:_) -> do
6a88f8edd881afaf4b865b01bfbb4faaf0e7a3c9Simon Ulbricht visibleNodes <- readIORef ioRefVisibleNodes
6a88f8edd881afaf4b865b01bfbb4faaf0e7a3c9Simon Ulbricht (newVisibleNodes, newEventDescr, newConvMaps) <-
6a88f8edd881afaf4b865b01bfbb4faaf0e7a3c9Simon Ulbricht applyChangesAux2 gid libname grInfo visibleNodes
319f8219a74a41859b9d1991817644549ab43d61Simon Ulbricht eventDescr convMaps changes
319f8219a74a41859b9d1991817644549ab43d61Simon Ulbricht writeIORef ioRefVisibleNodes newVisibleNodes
319f8219a74a41859b9d1991817644549ab43d61Simon Ulbricht return (newEventDescr, newConvMaps)
319f8219a74a41859b9d1991817644549ab43d61Simon Ulbricht-- | auxiliary function for applyChanges
319f8219a74a41859b9d1991817644549ab43d61Simon UlbrichtapplyChangesAux2 :: Descr -> LIB_NAME -> GraphInfo -> [[Node]] -> Descr
319f8219a74a41859b9d1991817644549ab43d61Simon Ulbricht -> ConversionMaps -> [DGChange]
1cc76b3190979d475bc8f2c1ffe627d9abf2410bChristian Maeder -> IO ([[Node]], Descr, ConversionMaps)
1cc76b3190979d475bc8f2c1ffe627d9abf2410bChristian MaederapplyChangesAux2 _ _ _ visibleNodes eventDescr convMaps [] =
1cc76b3190979d475bc8f2c1ffe627d9abf2410bChristian Maeder return (visibleNodes, eventDescr+1, convMaps)
2e76bbbed1c936bb0aee1753837e1c50416847a2Simon UlbrichtapplyChangesAux2 gid libname grInfo visibleNodes _ convMaps (change:changes) =
2e76bbbed1c936bb0aee1753837e1c50416847a2Simon Ulbricht case change of
37c793236d73cd400bb268672e0d0f7f97a89a70Simon Ulbricht SetNodeLab _ (node, newLab) -> do
319f8219a74a41859b9d1991817644549ab43d61Simon Ulbricht let nodetype = getDGNodeType newLab
2e2559f894aaa661b199e4fa00609f522bc5482aSimon Ulbricht nodename = getDGNodeName newLab
7cb31cb2104c666b2762976f7ed86da10575a980Simon Ulbricht dgNode = (libname, node)
7cb31cb2104c666b2762976f7ed86da10575a980Simon Ulbricht -- ensures that the to be set node is in the graph.
7cb31cb2104c666b2762976f7ed86da10575a980Simon Ulbricht case InjMap.lookupWithA dgNode (dgAndabstrNode convMaps) of
7cb31cb2104c666b2762976f7ed86da10575a980Simon Ulbricht Just abstrNode -> do
7cb31cb2104c666b2762976f7ed86da10575a980Simon Ulbricht changeNodeType gid abstrNode nodetype grInfo
7cb31cb2104c666b2762976f7ed86da10575a980Simon Ulbricht -- if everything's all right, sets the map with the new node.
7cb31cb2104c666b2762976f7ed86da10575a980Simon Ulbricht -- otherwise the error is shown.
f8b5384f117f1eb77f87b9bc982513109b3c2d56Christian Maeder Nothing -> do
f59ad2f2dc308e549d70f0de4c0054df3b2bbfcaChristian Maeder let newConvMaps = convMaps
2b1abe6d680bc23b703f7ffbf6d214be15aa9f1fSimon Ulbricht { dgAndabstrNode = InjMap.updateBWithA dgNode
2b1abe6d680bc23b703f7ffbf6d214be15aa9f1fSimon Ulbricht descr (dgAndabstrNode convMaps) }
92b34c379207fb8752258be174cb8ef4162dc865Simon Ulbricht applyChangesAux2 gid libname grInfo visibleNodes
c1d06b3018b34ede2b3fb6c7fe2ad28cd5ce5b68Christian Maeder (descr+1) newConvMaps changes
d5a6311a0badccb57c915d3f7d0657615338e12cSimon Ulbricht error $ "applyChangesAux2: could not set node "
37c793236d73cd400bb268672e0d0f7f97a89a70Simon Ulbricht ++ show node ++" with name "
d5a6311a0badccb57c915d3f7d0657615338e12cSimon Ulbricht ++ show nodename ++ "\n" ++ msg
37c793236d73cd400bb268672e0d0f7f97a89a70Simon Ulbricht Nothing -> error $ "applyChangesAux2: could not set node "
2b1abe6d680bc23b703f7ffbf6d214be15aa9f1fSimon Ulbricht ++ show node ++ " with name "
2b1abe6d680bc23b703f7ffbf6d214be15aa9f1fSimon Ulbricht ++ show nodename ++ ": " ++
2b1abe6d680bc23b703f7ffbf6d214be15aa9f1fSimon Ulbricht "node does not exist in abstraction graph"
2b1abe6d680bc23b703f7ffbf6d214be15aa9f1fSimon Ulbricht InsertNode (node, nodelab) -> do
2b1abe6d680bc23b703f7ffbf6d214be15aa9f1fSimon Ulbricht let nodetype = getDGNodeType nodelab
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder nodename = getDGNodeName nodelab
2b1abe6d680bc23b703f7ffbf6d214be15aa9f1fSimon Ulbricht addnode gid nodetype nodename grInfo
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder case err of
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder do let dgNode = (libname,node)
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder newVisibleNodes = map (node :) visibleNodes
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder newConvMaps = convMaps
f59ad2f2dc308e549d70f0de4c0054df3b2bbfcaChristian Maeder { dgAndabstrNode = InjMap.insert dgNode descr
f8b5384f117f1eb77f87b9bc982513109b3c2d56Christian Maeder (dgAndabstrNode convMaps) }
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder applyChangesAux2 gid libname grInfo newVisibleNodes (descr+1)
0a46a4d711eca869ad75b4df84dabd72783ebdd2Simon Ulbricht newConvMaps changes
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder Just msg ->
2b1abe6d680bc23b703f7ffbf6d214be15aa9f1fSimon Ulbricht error $ "applyChangesAux2: could not add node " ++ show node
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder ++" with name " ++ show nodename ++ "\n" ++ msg
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder DeleteNode (node, nodelab) -> do
0a46a4d711eca869ad75b4df84dabd72783ebdd2Simon Ulbricht let nodename = getDGNodeName nodelab
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder dgnode = (libname,node)
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder case InjMap.lookupWithA dgnode (dgAndabstrNode convMaps) of
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder Just abstrNode -> do
0a46a4d711eca869ad75b4df84dabd72783ebdd2Simon Ulbricht AGV.Result descr err <- delnode gid abstrNode grInfo
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder case err of
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder Nothing -> do
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder let newVisibleNodes = map (filter (/= node)) visibleNodes
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder newConvMaps = convMaps
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder { dgAndabstrNode = InjMap.delete dgnode abstrNode
0a46a4d711eca869ad75b4df84dabd72783ebdd2Simon Ulbricht (dgAndabstrNode convMaps) }
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder applyChangesAux2 gid libname grInfo newVisibleNodes (descr+1)
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder newConvMaps changes
e4a035578fa9d1911eee097e2ed9a998c90c7805Christian Maeder Just msg -> error $ "applyChangesAux2: could not delete node "
e4a035578fa9d1911eee097e2ed9a998c90c7805Christian Maeder ++ show node ++ " with name "
0a46a4d711eca869ad75b4df84dabd72783ebdd2Simon Ulbricht ++ show nodename ++ "\n" ++ msg
0a46a4d711eca869ad75b4df84dabd72783ebdd2Simon Ulbricht Nothing -> error $ "applyChangesAux2: could not delete node "
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder ++ show node ++ " with name "
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder ++ show nodename ++": " ++
465c6b72e8e480969b5f08658e394992bcc08bfcSimon Ulbricht "node does not exist in abstraction graph"
439fdeeb1323b17084fad1b7fe619e49c270999fSimon Ulbricht InsertEdge ledge@(src,tgt,edgelab) ->
6a88f8edd881afaf4b865b01bfbb4faaf0e7a3c9Simon Ulbricht do let dgAndabstrNodeMap = dgAndabstrNode convMaps
f59ad2f2dc308e549d70f0de4c0054df3b2bbfcaChristian Maeder case (InjMap.lookupWithA (libname, src) dgAndabstrNodeMap,
f59ad2f2dc308e549d70f0de4c0054df3b2bbfcaChristian Maeder InjMap.lookupWithA (libname, tgt) dgAndabstrNodeMap) of
6a88f8edd881afaf4b865b01bfbb4faaf0e7a3c9Simon Ulbricht (Just abstrSrc, Just abstrTgt) ->
f8b5384f117f1eb77f87b9bc982513109b3c2d56Christian Maeder do let dgEdge = (libname, (src,tgt,showDoc edgelab ""))
439fdeeb1323b17084fad1b7fe619e49c270999fSimon Ulbricht addlink gid (getDGLinkType edgelab)
7c99a6c982aaf61547de8054296c8055c8d1a13aSimon Ulbricht "" (Just ledge) abstrSrc abstrTgt grInfo
7c99a6c982aaf61547de8054296c8055c8d1a13aSimon Ulbricht do let newConvMaps = convMaps
a2af8492313011f78cbedbfd302dc12150b9f7efChristian Maeder { dgAndabstrEdge = InjMap.insert dgEdge descr
f8b5384f117f1eb77f87b9bc982513109b3c2d56Christian Maeder (dgAndabstrEdge convMaps) }
6a88f8edd881afaf4b865b01bfbb4faaf0e7a3c9Simon Ulbricht applyChangesAux2 gid libname grInfo visibleNodes
439fdeeb1323b17084fad1b7fe619e49c270999fSimon Ulbricht (descr + 1) newConvMaps changes
0a46a4d711eca869ad75b4df84dabd72783ebdd2Simon Ulbricht error $ "applyChangesAux2: could not add link from "
0a46a4d711eca869ad75b4df84dabd72783ebdd2Simon Ulbricht ++ show src ++ " to " ++ show tgt ++ ":\n"
6a88f8edd881afaf4b865b01bfbb4faaf0e7a3c9Simon Ulbricht _ -> error $ "applyChangesAux2: could not add link " ++ show src
f59ad2f2dc308e549d70f0de4c0054df3b2bbfcaChristian Maeder ++ " to " ++ show tgt ++ ": illegal end nodes"
6a88f8edd881afaf4b865b01bfbb4faaf0e7a3c9Simon Ulbricht DeleteEdge (src,tgt,edgelab) ->
0a46a4d711eca869ad75b4df84dabd72783ebdd2Simon Ulbricht do let dgEdge = (libname, (src,tgt,showDoc edgelab ""))
0a46a4d711eca869ad75b4df84dabd72783ebdd2Simon Ulbricht dgAndabstrEdgeMap = dgAndabstrEdge convMaps
0a46a4d711eca869ad75b4df84dabd72783ebdd2Simon Ulbricht case (InjMap.lookupWithA dgEdge dgAndabstrEdgeMap) of
439fdeeb1323b17084fad1b7fe619e49c270999fSimon Ulbricht Just abstrEdge ->
af2bfaed5d36cafe1092fe2bc1dbf5a763dfafcdSimon Ulbricht do AGV.Result descr err <- dellink gid abstrEdge grInfo
af2bfaed5d36cafe1092fe2bc1dbf5a763dfafcdSimon Ulbricht do let newConvMaps = convMaps
af2bfaed5d36cafe1092fe2bc1dbf5a763dfafcdSimon Ulbricht { dgAndabstrEdge = InjMap.delete dgEdge
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder abstrEdge (dgAndabstrEdge convMaps) }
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder applyChangesAux2 gid libname grInfo visibleNodes
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder (descr + 1) newConvMaps changes
af2bfaed5d36cafe1092fe2bc1dbf5a763dfafcdSimon Ulbricht Just msg -> error $
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder "applyChangesAux2: could not delete edge "
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder ++ shows abstrEdge ":\n" ++ msg
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder Nothing -> error $ "applyChangesAux2: deleted edge from "
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder ++ shows src " to " ++ shows tgt
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder " of type " ++ showDoc (dgl_type edgelab)
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder " and origin " ++ shows (dgl_origin edgelab)
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder " of development "
0a46a4d711eca869ad75b4df84dabd72783ebdd2Simon Ulbricht ++ "graph does not exist in abstraction graph"
66e5f6ab072171b6fd02ccc20846386773354391Christian Maeder-- | display a window of translated graph with maximal sublogic.
66e5f6ab072171b6fd02ccc20846386773354391Christian MaederopenTranslateGraph :: LibEnv -> LIB_NAME -> HetcatsOpts
66e5f6ab072171b6fd02ccc20846386773354391Christian Maeder -> Res.Result G_sublogics -> ConvFunc -> LibFunc -> IO ()
2b1abe6d680bc23b703f7ffbf6d214be15aa9f1fSimon UlbrichtopenTranslateGraph libEnv ln opts (Res.Result diagsSl mSublogic) convGraph
2b1abe6d680bc23b703f7ffbf6d214be15aa9f1fSimon Ulbricht -- if an error existed by the search of maximal sublogicn
2b1abe6d680bc23b703f7ffbf6d214be15aa9f1fSimon Ulbricht -- (see GUI.DGTranslation.getDGLogic), the process need not to go on.
2b1abe6d680bc23b703f7ffbf6d214be15aa9f1fSimon Ulbricht if hasErrors diagsSl then
0a46a4d711eca869ad75b4df84dabd72783ebdd2Simon Ulbricht errorMess $ unlines $ map show
0a46a4d711eca869ad75b4df84dabd72783ebdd2Simon Ulbricht $ filter (relevantDiagKind . diagKind) diagsSl
f59ad2f2dc308e549d70f0de4c0054df3b2bbfcaChristian Maeder do case mSublogic of
f59ad2f2dc308e549d70f0de4c0054df3b2bbfcaChristian Maeder Just sublogic -> do
f59ad2f2dc308e549d70f0de4c0054df3b2bbfcaChristian Maeder let paths = findComorphismPaths logicGraph sublogic
f59ad2f2dc308e549d70f0de4c0054df3b2bbfcaChristian Maeder if null paths then
2b1abe6d680bc23b703f7ffbf6d214be15aa9f1fSimon Ulbricht errorMess "This graph has no comorphism to translation."
2b1abe6d680bc23b703f7ffbf6d214be15aa9f1fSimon Ulbricht Res.Result diagsR i <- runResultT ( do
0a46a4d711eca869ad75b4df84dabd72783ebdd2Simon Ulbricht -- the user choose one
2b1abe6d680bc23b703f7ffbf6d214be15aa9f1fSimon Ulbricht sel <- lift $ listBox "Choose a logic translation"
2b1abe6d680bc23b703f7ffbf6d214be15aa9f1fSimon Ulbricht (map show paths)
d5a6311a0badccb57c915d3f7d0657615338e12cSimon Ulbricht Just j -> return j
0a46a4d711eca869ad75b4df84dabd72783ebdd2Simon Ulbricht _ -> liftR $ fail "no logic translation chosen")
b99c9606f2faafeabb3fa8c596992143a561c787Simon Ulbricht let aComor = paths !! fromJust i
b99c9606f2faafeabb3fa8c596992143a561c787Simon Ulbricht -- graph translation.
0a46a4d711eca869ad75b4df84dabd72783ebdd2Simon Ulbricht case libEnv_translation libEnv aComor of
0a46a4d711eca869ad75b4df84dabd72783ebdd2Simon Ulbricht Res.Result diagsTrans (Just newLibEnv) -> do
f8b5384f117f1eb77f87b9bc982513109b3c2d56Christian Maeder showDiags opts (diagsSl ++ diagsR ++ diagsTrans)
b99c9606f2faafeabb3fa8c596992143a561c787Simon Ulbricht if hasErrors (diagsR ++ diagsTrans) then
d5a6311a0badccb57c915d3f7d0657615338e12cSimon Ulbricht errorMess $ unlines $ map show
d5a6311a0badccb57c915d3f7d0657615338e12cSimon Ulbricht $ filter (relevantDiagKind . diagKind)
b99c9606f2faafeabb3fa8c596992143a561c787Simon Ulbricht $ diagsR ++ diagsTrans
b99c9606f2faafeabb3fa8c596992143a561c787Simon Ulbricht else dg_showGraphAux
0a46a4d711eca869ad75b4df84dabd72783ebdd2Simon Ulbricht (\gI@(GInfo{libEnvIORef = iorLE}) -> do
0a46a4d711eca869ad75b4df84dabd72783ebdd2Simon Ulbricht writeIORef iorLE newLibEnv
b99c9606f2faafeabb3fa8c596992143a561c787Simon Ulbricht convGraph (gI{ gi_LIB_NAME = ln
d5a6311a0badccb57c915d3f7d0657615338e12cSimon Ulbricht , gi_hetcatsOpts = opts})
d5a6311a0badccb57c915d3f7d0657615338e12cSimon Ulbricht "translation Graph" showLib)
b99c9606f2faafeabb3fa8c596992143a561c787Simon Ulbricht Res.Result diagsTrans Nothing ->
b99c9606f2faafeabb3fa8c596992143a561c787Simon Ulbricht errorMess $ unlines $ map show
b99c9606f2faafeabb3fa8c596992143a561c787Simon Ulbricht $ filter (relevantDiagKind . diagKind)
6a88f8edd881afaf4b865b01bfbb4faaf0e7a3c9Simon Ulbricht $ diagsSl ++ diagsR ++ diagsTrans
b99c9606f2faafeabb3fa8c596992143a561c787Simon Ulbricht Nothing -> errorMess "the maximal sublogic is not found."
6a88f8edd881afaf4b865b01bfbb4faaf0e7a3c9Simon Ulbricht where relevantDiagKind Error = True
b99c9606f2faafeabb3fa8c596992143a561c787Simon Ulbricht relevantDiagKind Warning = verbose opts >= 2
b99c9606f2faafeabb3fa8c596992143a561c787Simon Ulbricht relevantDiagKind Hint = verbose opts >= 4
b99c9606f2faafeabb3fa8c596992143a561c787Simon Ulbricht relevantDiagKind Debug = verbose opts >= 5
b99c9606f2faafeabb3fa8c596992143a561c787Simon Ulbricht relevantDiagKind MessageW = False
b99c9606f2faafeabb3fa8c596992143a561c787Simon Ulbrichtdg_showGraphAux :: (GInfo -> IO (Descr, GraphInfo, ConversionMaps)) -> IO ()
b99c9606f2faafeabb3fa8c596992143a561c787Simon Ulbrichtdg_showGraphAux convFct = do
86acceed922b3079355e5aced742709ec790aab3Simon Ulbricht useHTk -- All messages are displayed in TK dialog windows
0f3c9fa687758f7282fd74539600c580ac165594Simon Ulbricht -- from this point on
c4afbc0e8d0896b0e7efec66a9f15e3ca16f2233Simon Ulbricht gInfo <- emptyGInfo
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder (gid, gv, _cmaps) <- convFct (gInfo)
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder redisplay gid gv
98fb0b2bb596c5af3ef20eb9dc063871cc03ee03Simon Ulbricht-- DaVinciGraph to String
9d46cd96eb5f63953a7608635e9cc2d22506e5d7Simon Ulbricht-- Functions to convert a DaVinciGraph to a String to store as a .udg file
98fb0b2bb596c5af3ef20eb9dc063871cc03ee03Simon Ulbricht-- | saves the uDrawGraph graph to a file
98530a5430d24712d3d75213f8e21b6b0421770eSimon UlbrichtsaveUDGraph :: GInfo -> Map.Map String (Shape value, String)
98530a5430d24712d3d75213f8e21b6b0421770eSimon Ulbricht -> Map.Map String (EdgePattern EdgeValue, String) -> IO ()
98530a5430d24712d3d75213f8e21b6b0421770eSimon UlbrichtsaveUDGraph gInfo@(GInfo { gi_GraphInfo = graphInfo
98fb0b2bb596c5af3ef20eb9dc063871cc03ee03Simon Ulbricht , graphId = gid
98fb0b2bb596c5af3ef20eb9dc063871cc03ee03Simon Ulbricht , gi_LIB_NAME = ln
98fb0b2bb596c5af3ef20eb9dc063871cc03ee03Simon Ulbricht , gi_hetcatsOpts = opts
679aeef257123e594df0769b43ac12fe98854a54Simon Ulbricht }) nodemap linkmap = do
679aeef257123e594df0769b43ac12fe98854a54Simon Ulbricht evnt <- newFileDialogStr "Save as..."
679aeef257123e594df0769b43ac12fe98854a54Simon Ulbricht $ (rmSuffix $ libNameToFile opts ln) ++ ".udg"
98fb0b2bb596c5af3ef20eb9dc063871cc03ee03Simon Ulbricht maybeFilePath <- HTk.sync evnt
98fb0b2bb596c5af3ef20eb9dc063871cc03ee03Simon Ulbricht case maybeFilePath of
679aeef257123e594df0769b43ac12fe98854a54Simon Ulbricht Just filepath -> do
98fb0b2bb596c5af3ef20eb9dc063871cc03ee03Simon Ulbricht showTemporaryMessage gid graphInfo "Converting graph..."
98530a5430d24712d3d75213f8e21b6b0421770eSimon Ulbricht ((_, graph):_, _) <- readIORef graphInfo
98fb0b2bb596c5af3ef20eb9dc063871cc03ee03Simon Ulbricht nstring <- nodes2String gInfo graph nodemap linkmap
98fb0b2bb596c5af3ef20eb9dc063871cc03ee03Simon Ulbricht writeFile filepath nstring
98fb0b2bb596c5af3ef20eb9dc063871cc03ee03Simon Ulbricht showTemporaryMessage gid graphInfo $ "Graph stored to " ++ filepath ++ "!"
98fb0b2bb596c5af3ef20eb9dc063871cc03ee03Simon Ulbricht Nothing -> do
98fb0b2bb596c5af3ef20eb9dc063871cc03ee03Simon Ulbricht showTemporaryMessage gid graphInfo $ "Aborted!"
98530a5430d24712d3d75213f8e21b6b0421770eSimon Ulbricht-- | Converts the nodes of the graph to String representation
98530a5430d24712d3d75213f8e21b6b0421770eSimon Ulbrichtnodes2String :: GInfo -> AbstractionGraph
98530a5430d24712d3d75213f8e21b6b0421770eSimon Ulbricht -> Map.Map String (Shape value, String)
98530a5430d24712d3d75213f8e21b6b0421770eSimon Ulbricht -> Map.Map String (EdgePattern EdgeValue, String) -> IO String
98530a5430d24712d3d75213f8e21b6b0421770eSimon Ulbrichtnodes2String gInfo graph nodemap linkmap = do
98530a5430d24712d3d75213f8e21b6b0421770eSimon Ulbricht nstring <- foldM (\s (k, a) -> do
98530a5430d24712d3d75213f8e21b6b0421770eSimon Ulbricht s' <- (node2String gInfo graph nodemap linkmap k a)
98530a5430d24712d3d75213f8e21b6b0421770eSimon Ulbricht return $ s ++ (if s /= "" then ",\n " else "") ++ s') ""
98fb0b2bb596c5af3ef20eb9dc063871cc03ee03Simon Ulbricht $ Map.toList $ nodes graph
d4d3caef3878e583180d50f670957f1406d1effbcmaeder return $ "[" ++ nstring ++ "]"
d4d3caef3878e583180d50f670957f1406d1effbcmaeder-- | Converts a node to String representation
cddd87cd39be9d031348ef95051c4d14067e1646cmaedernode2String :: GInfo -> AbstractionGraph
0f3c9fa687758f7282fd74539600c580ac165594Simon Ulbricht -> Map.Map String (Shape value, String)
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder -> Map.Map String (EdgePattern EdgeValue, String)
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder -> Int -> (String, DaVinciNode (String,Int,Int)) -> IO String
cddd87cd39be9d031348ef95051c4d14067e1646cmaedernode2String gInfo graph nodemap linkmap nodeid (ntype, node) = do
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder label <- getNodeLabel gInfo graph ntype node
0f3c9fa687758f7282fd74539600c580ac165594Simon Ulbricht (shape, color) <- case Map.lookup ntype nodemap of
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder Nothing -> error $ "SaveGraph: can't lookup nodetype: " ++ ntype
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder Just (s, c) -> return (s, c)
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder object = "a(\"OBJECT\",\"" ++ label ++ "\"),"
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder color' = "a(\"COLOR\",\"" ++ color ++ "\"),"
844c7d2ec3917393e139e53503757098d568713eSimon Ulbricht shape' = "a(\"_GO\",\"" ++ (map toLower $ show shape) ++ "\")"
734a5ebd38032798f0ab908e2d52862c71b2c127Simon Ulbricht links <- links2String graph linkmap nodeid
41a3368af0eaad78c660477e7ded53b2ba85a275Christian Maeder return $ "l(\"" ++ (show nodeid) ++ "\",n(\"" ++ ntype ++ "\","
04c445e50a1d8b95e667595594e6b551c8b2ff59Simon Ulbricht ++ "[" ++ object ++ color' ++ shape' ++ "],"
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder ++ "\n [" ++ links ++ "]))"
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder-- | Converts all links of a node to String representation
473f5af6e4803fbeecc814065952396f2501039bChristian Maederlinks2String :: AbstractionGraph
8dfcec5538467723b1cf9d1651de7c9c89fe4aabChristian Maeder -> Map.Map String (EdgePattern EdgeValue, String)
8dfcec5538467723b1cf9d1651de7c9c89fe4aabChristian Maeder -> Int -> IO String
8dfcec5538467723b1cf9d1651de7c9c89fe4aabChristian Maederlinks2String graph linkmap nodeid = do
8dfcec5538467723b1cf9d1651de7c9c89fe4aabChristian Maeder let links = Map.foldWithKey (\k a@(nid, _, _, _) b -> if nid == nodeid
26f0691ae6929941ee21ca3d33732a0ce45a8079cmaeder then (k, a):b
8dfcec5538467723b1cf9d1651de7c9c89fe4aabChristian Maeder else b) [] $ edges graph
22bb4a9063684a0f37dd7d0e6b21086adcc1e789Christian Maeder foldM (\s (k, a) -> do
22bb4a9063684a0f37dd7d0e6b21086adcc1e789Christian Maeder s' <- link2String linkmap k a
8dfcec5538467723b1cf9d1651de7c9c89fe4aabChristian Maeder return $ s ++ (if s /= "" then ",\n " else "") ++ s') "" links
8dfcec5538467723b1cf9d1651de7c9c89fe4aabChristian Maeder-- | Converts a link to String representation
8dfcec5538467723b1cf9d1651de7c9c89fe4aabChristian Maederlink2String :: Map.Map String (EdgePattern EdgeValue, String)
d2111c9d2eb254b2a5ab71b27a6a07f1e353aec7Christian Maeder -> Int -> (Int, Int, String, DaVinciArc EdgeValue) -> IO String
cddd87cd39be9d031348ef95051c4d14067e1646cmaederlink2String linkmap linkid (nodeid1, nodeid2, ltype, _) = do
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder (line, color) <- case Map.lookup ltype linkmap of
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder Nothing -> error $ "SaveGraph: can't lookup linktype: " ++ ltype
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder Just (l, c) -> return (l, c)
d2111c9d2eb254b2a5ab71b27a6a07f1e353aec7Christian Maeder name = "\"" ++ (show linkid) ++ ":" ++ (show nodeid1) ++ "->"
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder ++ (show nodeid2) ++ "\""
d2111c9d2eb254b2a5ab71b27a6a07f1e353aec7Christian Maeder color' = "a(\"EDGECOLOR\",\"" ++ color ++ "\"),"
dbce18afddbe9b055be0e37f51e00d00d519b1cdChristian Maeder line' = "a(\"EDGEPATTERN\",\"" ++ (map toLower $ show line) ++ "\")"
d2111c9d2eb254b2a5ab71b27a6a07f1e353aec7Christian Maeder return $ "l(" ++ name ++ ",e(\"" ++ ltype ++ "\","
96074fcf7dc0751450e132610b9bb31207ce0cd2Eugen Kuksa ++ "[" ++ color' ++ line' ++"],"
d102a920578426a89411cc8dabe47d7a881eab8fEugen Kuksa ++ "r(\"" ++ (show nodeid2) ++ "\")))"
96074fcf7dc0751450e132610b9bb31207ce0cd2Eugen Kuksa-- | Returns the name of the Node
96074fcf7dc0751450e132610b9bb31207ce0cd2Eugen KuksagetNodeLabel :: GInfo -> AbstractionGraph -> String
96074fcf7dc0751450e132610b9bb31207ce0cd2Eugen Kuksa -> DaVinciNode (String,Int,Int) -> IO String
5c89bca8b187e75ff87be1afe964c1aeba8a7725Eugen KuksagetNodeLabel (GInfo {internalNamesIORef = ioRefInternal}) graph ntype node = do
d102a920578426a89411cc8dabe47d7a881eab8fEugen Kuksa internal <- readIORef ioRefInternal
5c89bca8b187e75ff87be1afe964c1aeba8a7725Eugen Kuksa (label, _, _) <- getNodeValue (theGraph graph) node
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder case (not $ showNames internal) &&
eb24ac2f4701c8e012acf1bb8f686baa5422bb5aChristian Maeder ( ntype == "open_cons__internal"
eb24ac2f4701c8e012acf1bb8f686baa5422bb5aChristian Maeder || ntype == "proven_cons__internal"
eb24ac2f4701c8e012acf1bb8f686baa5422bb5aChristian Maeder || ntype == "locallyEmpty__open_cons__internal"
41a3368af0eaad78c660477e7ded53b2ba85a275Christian Maeder || ntype == "locallyEmpty__proven_cons__internal") of
dae8246f1f55b6a85e946fc1bfb6d32d556395f1Simon Ulbricht True -> return ""
f56cdf11927c31495bae642a9eb383212c90ba61Christian Maeder False -> return label