GraphLogic.hs revision 1842453990fed8a1bd7a5ac792d7982c1d2bfcd5
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder{- |
25cc5fbba63f84b47e389af749f55abbbde71c8cChristian MaederModule : $Header$
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederDescription : Logic for manipulating the graph in the Central GUI
25cc5fbba63f84b47e389af749f55abbbde71c8cChristian MaederCopyright : (c) Jorina Freya Gerken, Till Mossakowski, Uni Bremen 2002-2006
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederMaintainer : till@tzi.de
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederStability : provisional
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederPortability : non-portable (imports Logic)
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder-}
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder
d8c71aacc9f1c8cd40a8ad8dcdad9be8854b849fChristian Maedermodule GUI.GraphLogic
f2f9df2e17e70674f0bf426ed1763c973ee4cde0Christian Maeder ( undo
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder , redo
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder , reload
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder , performProofAction
96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian Maeder , openProofStatus
c90087f49069855bf684b699f9ca1e2d65eac20bChristian Maeder , saveProofStatus
96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian Maeder , nodeErr
01e383014b555bbcf639c0ca60c5810b3eff83c0Christian Maeder , proofMenu
83394c6b6e6de128e71b67c9251ed7a84485d082Christian Maeder , openTranslateGraph
83394c6b6e6de128e71b67c9251ed7a84485d082Christian Maeder , showReferencedLibrary
abf2487c3aece95c371ea89ac64319370dcb6483Klaus Luettich , showSpec
ce8b15da31cd181b7e90593cbbca98f47eda29d6Till Mossakowski , getSignatureOfNode
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder , getTheoryOfNode
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder , getLocalAxOfNode
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder , translateTheoryOfNode
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder , displaySubsortGraph
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder , displayConceptGraph
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder , lookupTheoryOfNode
2e2094a642e3775b0d76b890556407941d3a53b6Christian Maeder , getSublogicOfNode
2e2094a642e3775b0d76b890556407941d3a53b6Christian Maeder , showOriginOfNode
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder , showProofStatusOfNode
2e2094a642e3775b0d76b890556407941d3a53b6Christian Maeder , proveAtNode
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder , showJustSubtree
8410667510a76409aca9bb24ff0eda0420088274Christian Maeder , showIDOfEdge
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder , getNumberOfNode
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder , showMorphismOfEdge
8410667510a76409aca9bb24ff0eda0420088274Christian Maeder , showOriginOfEdge
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich , checkconservativityOfEdge
eee4b2ee739f163e09d6af6e45c025681e6c01a0Christian Maeder , showProofStatusOfThm
4d56f2fa72e4aec20eb827c11ed49c8cbb7014bdChristian Maeder , convertNodes
eee4b2ee739f163e09d6af6e45c025681e6c01a0Christian Maeder , convertEdges
eee4b2ee739f163e09d6af6e45c025681e6c01a0Christian Maeder , hideNodes
eee4b2ee739f163e09d6af6e45c025681e6c01a0Christian Maeder , getLibDeps
eee4b2ee739f163e09d6af6e45c025681e6c01a0Christian Maeder , hideShowNames
57a2436f9d44e37042498a3b3dfacd301d91bb6dChristian Maeder , showNodes
eee4b2ee739f163e09d6af6e45c025681e6c01a0Christian Maeder , translateGraph
eee4b2ee739f163e09d6af6e45c025681e6c01a0Christian Maeder , showLibGraph
d4892fa7401ceef014ea59d2d900773eaf88fcbdChristian Maeder )
eee4b2ee739f163e09d6af6e45c025681e6c01a0Christian Maeder where
eee4b2ee739f163e09d6af6e45c025681e6c01a0Christian Maeder
eee4b2ee739f163e09d6af6e45c025681e6c01a0Christian Maederimport Logic.Logic(conservativityCheck)
eee4b2ee739f163e09d6af6e45c025681e6c01a0Christian Maederimport Logic.Coerce(coerceSign, coerceMorphism)
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettichimport Logic.Grothendieck
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederimport Logic.Comorphism
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederimport Logic.Prover
55adfe57a4de1f36adc3e3bfc16f342e44a7d444Christian Maeder
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maederimport Comorphisms.LogicGraph(logicGraph)
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederimport Syntax.AS_Library(LIB_NAME, getModTime, getLIB_ID)
e593b89bfd4952698dc37feced21cefe869d87a2Christian Maeder
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederimport Static.GTheory
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maederimport Static.DevGraph
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederimport Static.DGToSpec(dgToSpec, computeTheory)
2e2094a642e3775b0d76b890556407941d3a53b6Christian Maederimport Static.AnalysisLibrary(anaLibExt, anaLib)
f13d1e86e58da53680e78043e8df182eed867efbChristian Maederimport Static.DGTranslation(libEnv_translation)
96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian Maeder
96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian Maederimport Proofs.EdgeUtils
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maederimport Proofs.InferBasic(basicInferenceNode)
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maederimport Proofs.StatusUtils(lookupHistory, removeContraryChanges)
c6fcd42c6d6d9dae8c7835c24fcb7ce8531a9050Christian Maeder
31c49f2fa23d4ac089f35145d80a224deb6ea7e4Till Mossakowskiimport GUI.Utils(listBox, createTextSaveDisplay)
c55a0f77be7e88d3620b419ec8961f4379a586e3Klaus Luettichimport GUI.Taxonomy (displayConceptGraph,displaySubsortGraph)
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maederimport GUI.DGTranslation(getDGLogic)
9e748851c150e1022fb952bab3315e869aaf0214Christian Maederimport GUI.GraphTypes
abf2487c3aece95c371ea89ac64319370dcb6483Klaus Luettichimport GUI.AbstractGraphView as AGV
8cacad2a09782249243b80985f28e9387019fe40Christian Maederimport qualified GUI.HTkUtils (displayTheory,
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder displayTheoryWithWarning,
431d34c7007a787331c4e5ec997badb0f8190fc7Christian Maeder createInfoDisplayWithTwoButtons)
431d34c7007a787331c4e5ec997badb0f8190fc7Christian Maeder
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederimport GraphDisp(deleteArc, deleteNode)
d3ae0072823e2ef0d41d4431fcc768e66489c20eChristian Maederimport TextDisplay(createTextDisplay)
9e748851c150e1022fb952bab3315e869aaf0214Christian Maederimport InfoBus(encapsulateWaitTermAct)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederimport DialogWin (useHTk)
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederimport Messages(errorMess)
9e748851c150e1022fb952bab3315e869aaf0214Christian Maederimport qualified HTk
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maederimport Common.Id(nullRange)
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maederimport Common.DocUtils(showDoc, pretty)
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maederimport Common.Doc(vcat)
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maederimport Common.ResultT(liftR, runResultT)
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maederimport Common.AS_Annotation(isAxiom)
431d34c7007a787331c4e5ec997badb0f8190fc7Christian Maederimport Common.Result as Res
9e748851c150e1022fb952bab3315e869aaf0214Christian Maederimport qualified Common.OrderedMap as OMap
9e748851c150e1022fb952bab3315e869aaf0214Christian Maederimport qualified Common.InjMap as InjMap
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maederimport qualified Common.Lib.Rel as Rel
c9acb8681bcc512245b4f0d1a9f2b189c60e10d4Christian Maederimport qualified Common.Lib.Graph as Tree
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederimport Driver.Options
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maederimport Driver.WriteFn(writeShATermFile)
c0c2380bced8159ff0297ece14eba948bd236471Christian Maederimport Driver.ReadFn(libNameToFile, readVerbose)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederimport System.Directory(getModificationTime)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederimport Data.IORef
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederimport Data.Maybe(fromJust)
9e748851c150e1022fb952bab3315e869aaf0214Christian Maederimport Data.List(nub,deleteBy,find)
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maederimport Data.Graph.Inductive.Graph as Graph(Node, LEdge, LNode, lab', labNode')
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maederimport qualified Data.IntMap as IntMap
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maederimport qualified Data.Map as Map
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder--import Control.Monad()
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maederimport Control.Monad.Trans(lift)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederimport Control.Concurrent.MVar(tryPutMVar, readMVar, tryTakeMVar)
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder
4017ebc0f692820736d796af3110c3b3018c108aChristian Maeder-- | Undo one step of the History
4017ebc0f692820736d796af3110c3b3018c108aChristian Maederundo :: GInfo -> LibEnv -> IO ()
4017ebc0f692820736d796af3110c3b3018c108aChristian Maederundo (GInfo {libEnvIORef = ioRefProofStatus,
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder conversionMapsIORef = convRef,
6ff7a91875597d6e4dfaa68c79187d01473e8341Christian Maeder graphId = gid,
6ff7a91875597d6e4dfaa68c79187d01473e8341Christian Maeder gi_LIB_NAME = ln,
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder gi_GraphInfo = actGraphInfo
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder }) initEnv = do
4017ebc0f692820736d796af3110c3b3018c108aChristian Maeder oldEnv <- readIORef ioRefProofStatus
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder let
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder dg = lookupDGraph ln oldEnv
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder initdg = lookupDGraph ln initEnv
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder phist = proofHistory dg
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder rhist = redoHistory dg
88318aafc287e92931dceffbb943d58a9310001dChristian Maeder if phist == [emptyHistory] then return ()
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder else do
a3c6d8e0670bf2aa71bc8e2a3b1f45d56dd65e4cChristian Maeder let
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder lastchange = head phist
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder phist' = tail phist
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder rhist' = lastchange:rhist
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder dg' = (applyProofHistory phist' initdg ) {redoHistory = rhist'}
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder newEnv = Map.insert ln dg' initEnv
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder writeIORef ioRefProofStatus newEnv
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder remakeGraph convRef gid actGraphInfo dg' ln
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder
4017ebc0f692820736d796af3110c3b3018c108aChristian Maeder-- | redo one step of the redoHistory
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maederredo :: GInfo -> LibEnv -> IO ()
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maederredo (GInfo {libEnvIORef = ioRefProofStatus,
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder conversionMapsIORef = convRef,
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder graphId = gid,
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder gi_LIB_NAME = ln,
f2f9df2e17e70674f0bf426ed1763c973ee4cde0Christian Maeder gi_GraphInfo = actGraphInfo
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder }) initEnv = do
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder oldEnv <- readIORef ioRefProofStatus
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder let
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder dg = lookupDGraph ln oldEnv
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder initdg = lookupDGraph ln initEnv
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder phist = proofHistory dg
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder rhist = redoHistory dg
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder if rhist == [emptyHistory] then return ()
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder else do
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder let
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder nextchange = head rhist
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder rhist' = tail rhist
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder phist' = nextchange:phist
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder dg' = (applyProofHistory phist' initdg) {redoHistory = rhist'}
431d34c7007a787331c4e5ec997badb0f8190fc7Christian Maeder newEnv = Map.insert ln dg' initEnv
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder writeIORef ioRefProofStatus newEnv
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder remakeGraph convRef gid actGraphInfo dg' ln
f4505a64a089693012a3f5c3b1f12a82cd7a2a5aKlaus Luettich
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder-- | reloads the Library of the DevGraph
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederreload :: GInfo -> IO()
f4505a64a089693012a3f5c3b1f12a82cd7a2a5aKlaus Luettichreload (GInfo {libEnvIORef = ioRefProofStatus,
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder conversionMapsIORef = convRef,
6b6773cf587b74259178641d811746a235faf056Christian Maeder graphId = gid,
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder gi_LIB_NAME = ln,
2c619a4dfdc1df27573eba98e81ed1ace906941dChristian Maeder gi_GraphInfo = actGraphInfo,
2c619a4dfdc1df27573eba98e81ed1ace906941dChristian Maeder gi_hetcatsOpts = opts
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder }) = do
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder oldle <- readIORef ioRefProofStatus
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder let
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder libdeps = Rel.toList $ Rel.intransKernel $ Rel.transClosure $ Rel.fromList
d272062059eea4d7479e1c6e8517469f02f61287Christian Maeder $ getLibDeps oldle
0cfef6179a1bfec4f07f460686dd629a27b4b778Christian Maeder ioruplibs <- newIORef ([] :: [LIB_NAME])
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder writeIORef ioruplibs []
83394c6b6e6de128e71b67c9251ed7a84485d082Christian Maeder reloadLibs ioRefProofStatus opts libdeps ioruplibs ln
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder le <- readIORef ioRefProofStatus
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder let
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder dgraph = lookupDGraph ln le
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder writeIORef ioRefProofStatus le
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder remakeGraph convRef gid actGraphInfo dgraph ln
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- | Creates a list of all LIB_NAME pairs, which have a dependency
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaedergetLibDeps :: LibEnv -> [(LIB_NAME, LIB_NAME)]
9df11f85fd7f8c4745d64464876e84ec4e263692Christian MaedergetLibDeps le =
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers concat $ map (\ ln -> getDep ln le) $ Map.keys le
010c56c4cf12dd7977ca36efe85219b91e265ee3Christian Maeder
fb328c4f646dd3dd78a9391c5cb58450a3dd0aa9Klaus Luettich-- | Creates a list of LIB_NAME pairs for the fist argument
5b818f10e11fc79def1fdd5c8a080d64a6438d87Christian MaedergetDep :: LIB_NAME -> LibEnv -> [(LIB_NAME, LIB_NAME)]
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix ReckersgetDep ln le =
0799b5dc3f06d2640e66e9ab54b8b217348fd719Christian Maeder map (\ x -> (ln, x)) $ map (\ (_,x,_) -> dgn_libname x) $ IntMap.elems $
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder IntMap.filter (\ (_,x,_) -> isDGRef x) $ Tree.convertToMap $
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder dgBody $ lookupDGraph ln le
010c56c4cf12dd7977ca36efe85219b91e265ee3Christian Maeder
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers-- | Reloads a library
9e748851c150e1022fb952bab3315e869aaf0214Christian MaederreloadLib :: IORef LibEnv -> HetcatsOpts -> IORef [LIB_NAME] -> LIB_NAME
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder -> IO ()
61fa0ac06ede811c7aad54ec4c4202346727368eChristian MaederreloadLib iorle opts ioruplibs ln = do
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder mfile <- existsAnSource opts {intype = GuessIn}
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder $ rmSuffix $ libNameToFile opts ln
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder case mfile of
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder Nothing -> do
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder return ()
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder Just file -> do
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder le <- readIORef iorle
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder let
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder le' = Map.delete ln le
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder mres <- anaLibExt opts file le'
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder case mres of
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder Just (_, newle) -> do
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder uplibs <- readIORef ioruplibs
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder writeIORef ioruplibs $ ln:uplibs
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder writeIORef iorle newle
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder return ()
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder Nothing -> do
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder fail $ "Could not read original development graph from '"++ file
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder ++ "'"
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder return ()
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder
31db599cbcd9285c3734d16279bc7d88cbc20dc6Christian Maeder-- | Reloads libraries if nessesary
6fe9628743562678acf97d6730ebcfee5e9e50c2Christian MaederreloadLibs :: IORef LibEnv -> HetcatsOpts -> [(LIB_NAME, LIB_NAME)]
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder -> IORef [LIB_NAME] -> LIB_NAME -> IO Bool
61fa0ac06ede811c7aad54ec4c4202346727368eChristian MaederreloadLibs iorle opts deps ioruplibs ln = do
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder uplibs <- readIORef ioruplibs
b565cd55a13dbccc4e66c344316da525c961e4caTill Mossakowski case elem ln uplibs of
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder True -> return True
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder False -> do
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder let
fb328c4f646dd3dd78a9391c5cb58450a3dd0aa9Klaus Luettich deps' = map (snd) $ filter (\ (ln',_) -> ln == ln') deps
fb328c4f646dd3dd78a9391c5cb58450a3dd0aa9Klaus Luettich res <- mapM (reloadLibs iorle opts deps ioruplibs) deps'
e96a0bf4040fd789339958c01f145c5057d26db6René Wagner let
e96a0bf4040fd789339958c01f145c5057d26db6René Wagner libupdate = foldl (\ u r -> if r then True else u) False res
abf2487c3aece95c371ea89ac64319370dcb6483Klaus Luettich case libupdate of
abf2487c3aece95c371ea89ac64319370dcb6483Klaus Luettich True -> do
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder reloadLib iorle opts ioruplibs ln
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder return True
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder False -> do
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers le <- readIORef iorle
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder let
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder newln:_ = filter (ln ==) $ Map.keys le
b565cd55a13dbccc4e66c344316da525c961e4caTill Mossakowski mfile <- existsAnSource opts $ rmSuffix $ libNameToFile opts ln
18a4d5cb6828f080db9c5f9551785c5151027271Christian Maeder case mfile of
18a4d5cb6828f080db9c5f9551785c5151027271Christian Maeder Nothing -> do
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder return False
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Just file -> do
fdb2d618144159395f7bf8ce3327b3c112a17dd3Till Mossakowski newmt <- getModificationTime file
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder let
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder libupdate' = (getModTime $ getLIB_ID newln) < newmt
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder case libupdate' of
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder False -> return False
c9acb8681bcc512245b4f0d1a9f2b189c60e10d4Christian Maeder True -> do
38352346eb1a67ba0f4eab8ad6f718528cf0cde0Christian Maeder reloadLib iorle opts ioruplibs ln
e8896c7bb416c4ced255a4d500808c2ea5a6869aChristian Maeder return True
63e50b4c36074d5fb9de872c4007b688b4bce534Christian Maeder
63e50b4c36074d5fb9de872c4007b688b4bce534Christian Maeder-- | Deletes the old edges and nodes of the Graph and makes new ones
f77f29e84b3f6e791c82e61b13fbf76582bedd2fChristian MaederremakeGraph :: IORef ConversionMaps -> Descr -> GraphInfo -> DGraph -> LIB_NAME
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder -> IO ()
e7757995211bd395dc79d26fe017d99375f7d2a6Christian MaederremakeGraph convRef gid actginfo dgraph ln = do
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder (gs,ev_cnt) <- readIORef actginfo
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder let
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder Just (_, g) = find (\ (gid', _) -> gid' == gid) gs
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder gs' = deleteBy (\ (gid1,_) (gid2,_) -> gid1 == gid2) (gid,g) gs
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder og = theGraph g
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder -- reads and delets the old nodes and edges
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder mapM_ (deleteArc og) $ map (\ (_,_,_,x) -> x) $ map snd $ AGV.edges g
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder mapM_ (deleteNode og) $ map snd $ map snd $ AGV.nodes g
6bf24e5eb644064ad650eb3fd9774483fccbf601Christian Maeder -- stores the graph without nodes and edges in the GraphInfo
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder let
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder g' = g {theGraph = og, AGV.nodes = [], AGV.edges = []}
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder writeIORef actginfo ((gid,g'):gs',ev_cnt)
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder -- creates new nodes and edges
1f8a7f8343f7df719768d2b1d7e3077ee291a1caChristian Maeder convMaps <- readIORef convRef
1f8a7f8343f7df719768d2b1d7e3077ee291a1caChristian Maeder newConvMaps <- convertNodes convMaps gid actginfo dgraph ln
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder finalConvMaps <- convertEdges newConvMaps gid actginfo dgraph ln
6bf24e5eb644064ad650eb3fd9774483fccbf601Christian Maeder -- writes the ConversionMap and redisplays the graph
dbe752ee940baae7f9f231f29c62284bb0f90a25Christian Maeder writeIORef convRef finalConvMaps
53818ced114da21321063fff307aa41c1ab31dd3Achim Mahnke redisplay gid actginfo
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder return ()
53818ced114da21321063fff307aa41c1ab31dd3Achim Mahnke
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederhideShowNames :: GInfo -> Bool -> IO ()
53818ced114da21321063fff307aa41c1ab31dd3Achim MahnkehideShowNames (GInfo {graphId = gid,
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder gi_GraphInfo = actGraphInfo,
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder internalNamesIORef = showInternalNames
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder }) toggle = do
1f63599faaa311cd024d6413f82bff8caae8de24Christian Maeder deactivateGraphWindow gid actGraphInfo
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder (intrn::InternalNames) <- readIORef showInternalNames
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder let showThem = if toggle then not $ showNames intrn else showNames intrn
1f63599faaa311cd024d6413f82bff8caae8de24Christian Maeder showItrn s = if showThem then s else ""
857992065be4ed40a72c6296b6c0aec62ab4c5b9Christian Maeder mapM_ (\(s,upd) -> upd (\_ -> showItrn s)) $ updater intrn
fdb2d618144159395f7bf8ce3327b3c112a17dd3Till Mossakowski writeIORef showInternalNames $ intrn {showNames = showThem}
7c99e334446bb97120e30e967baeeddfdd1278deKlaus Luettich redisplay gid actGraphInfo
4017ebc0f692820736d796af3110c3b3018c108aChristian Maeder activateGraphWindow gid actGraphInfo
4017ebc0f692820736d796af3110c3b3018c108aChristian Maeder return ()
d8c71aacc9f1c8cd40a8ad8dcdad9be8854b849fChristian Maeder
0c355dd0b739631ee472f9a656e266be27fa4e64Christian MaedershowNodes :: GInfo -> IO ()
b49276c9f50038e0bd499ad49f7bd6444566a834Christian MaedershowNodes gInfo@(GInfo {descrIORef = event,
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder graphId = gid,
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder gi_GraphInfo = actGraphInfo
33d042fe6a9eb27a4c48f840b80838f3e7d98e34Christian Maeder }) = do
83394c6b6e6de128e71b67c9251ed7a84485d082Christian Maeder deactivateGraphWindow gid actGraphInfo
fa21fba9ceb1ddf7b3efd54731a12ed8750191d8Christian Maeder descr <- readIORef event
fa21fba9ceb1ddf7b3efd54731a12ed8750191d8Christian Maeder AGV.Result _ errorMsg <- checkHasHiddenNodes gid descr actGraphInfo
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder case errorMsg of
0c355dd0b739631ee472f9a656e266be27fa4e64Christian Maeder Nothing -> do
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder showTemporaryMessage gid actGraphInfo "Revealing hidden nodes ..."
fa21fba9ceb1ddf7b3efd54731a12ed8750191d8Christian Maeder showIt gid descr actGraphInfo
b49276c9f50038e0bd499ad49f7bd6444566a834Christian Maeder hideShowNames gInfo False
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder return ()
b49276c9f50038e0bd499ad49f7bd6444566a834Christian Maeder Just _ -> return ()
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder activateGraphWindow gid actGraphInfo
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder return ()
c7ec85d1103173e089aa5048fd7afb2f9b505124Klaus Luettich
c7ec85d1103173e089aa5048fd7afb2f9b505124Klaus LuettichtranslateGraph :: GInfo -> ConvFunc -> LibFunc -> IO ()
c7ec85d1103173e089aa5048fd7afb2f9b505124Klaus LuettichtranslateGraph (GInfo {libEnvIORef = ioRefProofStatus,
c7ec85d1103173e089aa5048fd7afb2f9b505124Klaus Luettich gi_LIB_NAME = ln,
c7ec85d1103173e089aa5048fd7afb2f9b505124Klaus Luettich gi_hetcatsOpts = opts
b905126bab9454b89041f92b3c50bb9efc85e427Klaus Luettich }) convGraph showLib = do
5ea9168eddbfbfe2282ed46dfe107a8962d6727bChristian Maeder le <- readIORef ioRefProofStatus
c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus Luettich openTranslateGraph le ln opts (getDGLogic le) convGraph showLib
5c69cef4668bbd959d721668313a779126014d1eKlaus Luettich
b905126bab9454b89041f92b3c50bb9efc85e427Klaus LuettichshowLibGraph :: GInfo -> LibFunc -> IO ()
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaedershowLibGraph gInfo showLib = do
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder showLib gInfo
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder return ()
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederperformProofAction :: GInfo -> IO () -> IO ()
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederperformProofAction gInfo@(GInfo {descrIORef = event,
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder graphId = gid,
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder gi_GraphInfo = actGraphInfo
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder }) proofAction = do
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder deactivateGraphWindow gid actGraphInfo
c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus Luettich let actionWithMessage = do
c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus Luettich showTemporaryMessage gid actGraphInfo
c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus Luettich "Applying development graph calculus proof rule..."
c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus Luettich proofAction
c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus Luettich descr <- readIORef event
c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus Luettich AGV.Result _ errorMsg <- checkHasHiddenNodes gid descr actGraphInfo
c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus Luettich case errorMsg of
c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus Luettich Nothing -> do
c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus Luettich showNodes gInfo
c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus Luettich actionWithMessage
c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus Luettich hideNodes gInfo
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder Just _ -> actionWithMessage
b905126bab9454b89041f92b3c50bb9efc85e427Klaus Luettich showTemporaryMessage gid actGraphInfo
b905126bab9454b89041f92b3c50bb9efc85e427Klaus Luettich "Development graph calculus proof rule finished."
b905126bab9454b89041f92b3c50bb9efc85e427Klaus Luettich activateGraphWindow gid actGraphInfo
b905126bab9454b89041f92b3c50bb9efc85e427Klaus Luettich return ()
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder
33d042fe6a9eb27a4c48f840b80838f3e7d98e34Christian MaedersaveProofStatus :: GInfo -> FilePath -> IO ()
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaedersaveProofStatus (GInfo {libEnvIORef = ioRefProofStatus,
dbe752ee940baae7f9f231f29c62284bb0f90a25Christian Maeder gi_LIB_NAME = ln,
1f8a7f8343f7df719768d2b1d7e3077ee291a1caChristian Maeder gi_hetcatsOpts = opts
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder }) file = encapsulateWaitTermAct $ do
1f8a7f8343f7df719768d2b1d7e3077ee291a1caChristian Maeder proofStatus <- readIORef ioRefProofStatus
1f8a7f8343f7df719768d2b1d7e3077ee291a1caChristian Maeder writeShATermFile file (ln, lookupHistory ln proofStatus)
68aab98a58d1460c77a1573a86c32a891756a420Christian Maeder putIfVerbose opts 2 $ "Wrote " ++ file
1f8a7f8343f7df719768d2b1d7e3077ee291a1caChristian Maeder
1f8a7f8343f7df719768d2b1d7e3077ee291a1caChristian Maeder-- | implementation of open menu, read in a proof status
96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian MaederopenProofStatus :: GInfo -> FilePath -> ConvFunc -> LibFunc
96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian Maeder -> IO (Descr, GraphInfo, ConversionMaps)
1f8a7f8343f7df719768d2b1d7e3077ee291a1caChristian MaederopenProofStatus (GInfo {libEnvIORef = ioRefProofStatus,
3a7788e09dd23b364a46c9488cbd1522369113dbChristian Maeder conversionMapsIORef = convRef,
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder gi_LIB_NAME = ln,
ef67402074be14deb95e4ff564737d5593144130Klaus Luettich gi_hetcatsOpts = opts
dbe752ee940baae7f9f231f29c62284bb0f90a25Christian Maeder }) file convGraph showLib = do
ef67402074be14deb95e4ff564737d5593144130Klaus Luettich mh <- readVerbose opts ln file
462d9dc583444aab82732e14a75610684d2dc7e9Christian Maeder case mh of
c9e197862d9d8ef2585270dd08f5194b3aed4a9dKlaus Luettich Nothing -> fail
e7e1ab2ac3f1fded8611bb92ae00e8f3b8c693fbKlaus Luettich $ "Could not read proof status from file '"
ef67402074be14deb95e4ff564737d5593144130Klaus Luettich ++ file ++ "'"
1323eba62fc519b068f5aaec4f9d2be05ffabea9Klaus Luettich Just h -> do
a80c28bb8b7a23ccdf7e08d0fe216fc19cc97273Klaus Luettich let libfile = libNameToFile opts ln
d784803f9c752667b4fcf7393d698002bedf3f89Klaus Luettich m <- anaLib opts { outtypes = [] } libfile
1323eba62fc519b068f5aaec4f9d2be05ffabea9Klaus Luettich case m of
1323eba62fc519b068f5aaec4f9d2be05ffabea9Klaus Luettich Nothing -> fail
1f8a7f8343f7df719768d2b1d7e3077ee291a1caChristian Maeder $ "Could not read original development graph from '"
1f8a7f8343f7df719768d2b1d7e3077ee291a1caChristian Maeder ++ libfile ++ "'"
462d9dc583444aab82732e14a75610684d2dc7e9Christian Maeder Just (_, libEnv) -> case Map.lookup ln libEnv of
5d39c60274aaa76506292d2d9e885fccd27e1eabChristian Maeder Nothing -> fail
5d39c60274aaa76506292d2d9e885fccd27e1eabChristian Maeder $ "Could not get original development graph for '"
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder ++ showDoc ln "'"
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder Just dg -> do
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder oldEnv <- readIORef ioRefProofStatus
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder let proofStatus = Map.insert ln
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder (applyProofHistory h dg) oldEnv
1f8a7f8343f7df719768d2b1d7e3077ee291a1caChristian Maeder writeIORef ioRefProofStatus proofStatus
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder gInfo <- emptyGInfo
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich gInfo' <- setGInfo gInfo ln proofStatus opts
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich (gid, actGraphInfo, convMaps) <-
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder convGraph gInfo' "Proof Status " showLib
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder writeIORef convRef convMaps
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich redisplay gid actGraphInfo
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder return (gid, actGraphInfo, convMaps)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- | apply a rule of the development graph calculus
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian MaederproofMenu :: GInfo
2e2094a642e3775b0d76b890556407941d3a53b6Christian Maeder -> (LibEnv -> IO (Res.Result LibEnv))
340706b6c0c6e3dbacdd7003e20e9cab7f9aa765Christian Maeder -> IO ()
43bb71dfe7ec405f563864d57c1cacdaa8ce9a80Christian MaederproofMenu gInfo@(GInfo {libEnvIORef = ioRefProofStatus,
2e2094a642e3775b0d76b890556407941d3a53b6Christian Maeder descrIORef = event,
340706b6c0c6e3dbacdd7003e20e9cab7f9aa765Christian Maeder conversionMapsIORef = convRef,
fdb2d618144159395f7bf8ce3327b3c112a17dd3Till Mossakowski graphId = gid,
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder gi_LIB_NAME = ln,
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder gi_GraphInfo = actGraphInfo,
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder gi_hetcatsOpts = hOpts,
9c3edf2b283c09d33b2820696886d1ed32fcadc8Christian Maeder proofGUIMVar = guiMVar,
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder visibleNodesIORef = ioRefVisibleNodes
c22d75ec3ea1306219d1c09a5b3e8ff04f753ad6Christian Maeder }) proofFun = do
9c3edf2b283c09d33b2820696886d1ed32fcadc8Christian Maeder filled <- tryPutMVar guiMVar Nothing
c22d75ec3ea1306219d1c09a5b3e8ff04f753ad6Christian Maeder if not filled
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder then readMVar guiMVar >>=
68b77966b2cf7bf2e340bf0fb6b9efc3e6a00467Christian Maeder (maybe (putIfVerbose hOpts 4 "proofMenu: ignored Nothing")
83394c6b6e6de128e71b67c9251ed7a84485d082Christian Maeder (\ w -> do
5bb7eeaca10ea76595229375f907a5a388b7c882Christian Maeder putIfVerbose hOpts 4 $
5bb7eeaca10ea76595229375f907a5a388b7c882Christian Maeder "proofMenu: Ignored Proof command; " ++
5bb7eeaca10ea76595229375f907a5a388b7c882Christian Maeder "maybe a proof window is still open?"
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder HTk.putWinOnTop w))
5bb7eeaca10ea76595229375f907a5a388b7c882Christian Maeder else do
94d3aa05411444596b44ede4531f05dd7ac20fdfChristian Maeder proofStatus <- readIORef ioRefProofStatus
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder putIfVerbose hOpts 4 "Proof started via \"Proofs\" menu"
8410667510a76409aca9bb24ff0eda0420088274Christian Maeder Res.Result ds res <- proofFun proofStatus
ddc9315cc0b1f5dd3d8f99a77f1c75064db33b48Christian Maeder putIfVerbose hOpts 4 "Analyzing result of proof"
ddc9315cc0b1f5dd3d8f99a77f1c75064db33b48Christian Maeder case res of
5d522dff4d0fabf57dd476d4c3de15d354a89f62Christian Maeder Nothing -> mapM_ (putStrLn . show) ds
5d522dff4d0fabf57dd476d4c3de15d354a89f62Christian Maeder Just newProofStatus -> do
5d522dff4d0fabf57dd476d4c3de15d354a89f62Christian Maeder let newGr = lookupDGraph ln newProofStatus
8410667510a76409aca9bb24ff0eda0420088274Christian Maeder history = proofHistory newGr
8410667510a76409aca9bb24ff0eda0420088274Christian Maeder writeIORef ioRefProofStatus newProofStatus
8410667510a76409aca9bb24ff0eda0420088274Christian Maeder descr <- readIORef event
ac43fa22d2d3f91a17674ac164cba3cf39a17795Klaus Luettich convMaps <- readIORef convRef
ac43fa22d2d3f91a17674ac164cba3cf39a17795Klaus Luettich (newDescr,convMapsAux)
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers <- applyChanges gid ln actGraphInfo descr ioRefVisibleNodes
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder convMaps history
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers writeIORef ioRefProofStatus $
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder Map.insert ln newGr newProofStatus
18c1d987ce5818ecf0bfc8af3f43aed2ce86e1eaChristian Maeder writeIORef event newDescr
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder writeIORef convRef convMapsAux
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder hideShowNames gInfo False
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder mGUIMVar <- tryTakeMVar guiMVar
6fe9628743562678acf97d6730ebcfee5e9e50c2Christian Maeder maybe (fail $ "should be filled with Nothing after "++
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder "proof attempt")
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder (const $ return ())
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder mGUIMVar
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian MaedernodeErr :: Descr -> IO ()
fb328c4f646dd3dd78a9391c5cb58450a3dd0aa9Klaus LuettichnodeErr descr = error $ "node with descriptor " ++ show descr
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder ++ " has no corresponding node in the development graph"
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder
61fa0ac06ede811c7aad54ec4c4202346727368eChristian MaedershowSpec :: Descr -> DGraphAndAGraphNode -> DGraph -> IO ()
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian MaedershowSpec descr dgAndabstrNodeMap dgraph =
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder case InjMap.lookupWithB descr dgAndabstrNodeMap of
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder Nothing -> return ()
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder Just (_, node) -> do
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder let sp = dgToSpec dgraph node
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers putStrLn $ case sp of
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder Res.Result ds Nothing -> show $ vcat $ map pretty ds
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder Res.Result _ m -> showDoc m ""
e96a0bf4040fd789339958c01f145c5057d26db6René Wagner
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian MaederhideNodes :: GInfo -> IO ()
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian MaederhideNodes (GInfo {descrIORef = event,
abf2487c3aece95c371ea89ac64319370dcb6483Klaus Luettich graphId = gid,
abf2487c3aece95c371ea89ac64319370dcb6483Klaus Luettich gi_GraphInfo = actGraphInfo
abf2487c3aece95c371ea89ac64319370dcb6483Klaus Luettich }) = do
abf2487c3aece95c371ea89ac64319370dcb6483Klaus Luettich deactivateGraphWindow gid actGraphInfo
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers descr' <- readIORef event
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder AGV.Result _ errorMsg <- checkHasHiddenNodes gid descr' actGraphInfo
83394c6b6e6de128e71b67c9251ed7a84485d082Christian Maeder case errorMsg of
8555737bcc9bf1d0afb6624e4d8668f070bcaba1Christian Maeder Nothing -> return ()
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers Just _ -> do
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder showTemporaryMessage gid actGraphInfo "Hiding unnamed nodes..."
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder AGV.Result descr msg <- hideSetOfNodeTypes gid
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder [--red nodes are not hidden
a80c28bb8b7a23ccdf7e08d0fe216fc19cc97273Klaus Luettich --"open_cons__internal",
a80c28bb8b7a23ccdf7e08d0fe216fc19cc97273Klaus Luettich --"locallyEmpty__open_cons__internal",
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder --"proven_cons__internal",
a80c28bb8b7a23ccdf7e08d0fe216fc19cc97273Klaus Luettich "locallyEmpty__proven_cons__internal"]
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder True actGraphInfo
83394c6b6e6de128e71b67c9251ed7a84485d082Christian Maeder writeIORef event descr
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder case msg of
b9625461755578f3eed04676d42a63fd2caebd0cChristian Maeder Nothing -> do redisplay gid actGraphInfo
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder return ()
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder Just err -> putStrLn err
d0652648f9879c67a194f8b03baafe2700c68eb4Christian Maeder activateGraphWindow gid actGraphInfo
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers return ()
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder{- | auxiliary method for debugging. shows the number of the given node
8b4c68db8b465107cabef8b9cd5b6bc216e1b156Till Mossakowski in the abstraction graph -}
e7757995211bd395dc79d26fe017d99375f7d2a6Christian MaedergetNumberOfNode :: Descr -> IO()
e7757995211bd395dc79d26fe017d99375f7d2a6Christian MaedergetNumberOfNode descr =
23ab8855c58adfbd03a0730584b917b24c603901Christian Maeder let title = "Number of node"
d0652648f9879c67a194f8b03baafe2700c68eb4Christian Maeder-- make the node number consistent
26f228bf3a3fea810223396e5794c217a79a8d5bChristian Maeder in createTextDisplay title (showDoc (descr-1) "") [HTk.size(10,10)]
26f228bf3a3fea810223396e5794c217a79a8d5bChristian Maeder
26f228bf3a3fea810223396e5794c217a79a8d5bChristian Maeder{- | outputs the signature of a node in a window;
ba904a15082557e939db689fcfba0c68c9a4f740Christian Maederused by the node menu defined in initializeGraph -}
ba904a15082557e939db689fcfba0c68c9a4f740Christian MaedergetSignatureOfNode :: Descr -> DGraphAndAGraphNode -> DGraph -> IO()
ba904a15082557e939db689fcfba0c68c9a4f740Christian MaedergetSignatureOfNode descr dgAndabstrNodeMap dgraph =
6ae5607d2def114f998fd49bac4eef12a2620fafChristian Maeder case InjMap.lookupWithB descr dgAndabstrNodeMap of
6ae5607d2def114f998fd49bac4eef12a2620fafChristian Maeder Just (_, node) ->
6ae5607d2def114f998fd49bac4eef12a2620fafChristian Maeder let dgnode = lab' (contextDG dgraph node)
08e5741dd8b6bf9b7419e89298e384e18bc57f64Christian Maeder title = "Signature of "++showName (dgn_name dgnode)
1f63599faaa311cd024d6413f82bff8caae8de24Christian Maeder in createTextDisplay title (showDoc (dgn_sign dgnode) "")
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder [HTk.size(80,50)]
83394c6b6e6de128e71b67c9251ed7a84485d082Christian Maeder Nothing -> nodeErr descr
96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian Maeder
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder{- |
83394c6b6e6de128e71b67c9251ed7a84485d082Christian Maeder fetches the theory from a node inside the IO Monad
96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian Maeder (added by KL based on code in getTheoryOfNode) -}
e7757995211bd395dc79d26fe017d99375f7d2a6Christian MaederlookupTheoryOfNode :: IORef LibEnv -> Descr -> DGraphAndAGraphNode ->
340706b6c0c6e3dbacdd7003e20e9cab7f9aa765Christian Maeder DGraph -> IO (Res.Result (Node,G_theory))
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederlookupTheoryOfNode proofStatusRef descr dgAndabstrNodeMap _ = do
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder libEnv <- readIORef proofStatusRef
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder case (do
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder (ln, node) <-
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder maybeToResult nullRange ("Node "++show descr++" not found")
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder $ InjMap.lookupWithB descr dgAndabstrNodeMap
470ca7a2797069ae4b27c34c1b71419f67be1f84Christian Maeder gth <- computeTheory libEnv ln node
470ca7a2797069ae4b27c34c1b71419f67be1f84Christian Maeder return (node, gth)
470ca7a2797069ae4b27c34c1b71419f67be1f84Christian Maeder ) of
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder r -> do
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder return r
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder
2c619a4dfdc1df27573eba98e81ed1ace906941dChristian Maeder{- | outputs the local axioms of a node in a window;
2c619a4dfdc1df27573eba98e81ed1ace906941dChristian Maederused by the node menu defined in initializeGraph-}
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaedergetLocalAxOfNode :: GInfo -> Descr -> DGraphAndAGraphNode -> DGraph -> IO ()
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaedergetLocalAxOfNode _ descr dgAndabstrNodeMap dgraph = do
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder case InjMap.lookupWithB descr dgAndabstrNodeMap of
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder Just (_, node) ->
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder do let dgnode = lab' (contextDG dgraph node)
481d4fe351800ab00fd323db8974559431227305Christian Maeder case dgnode of
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder DGNode _ gth _ _ _ _ _ ->
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder displayTheory "Local Axioms" node dgraph gth
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder DGRef name _ _ _ _ _ ->
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder createTextDisplay ("Local Axioms of "++ showName name)
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder "no local axioms (reference node to other library)"
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder [HTk.size(30,10)]
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder Nothing -> nodeErr descr
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder{- | outputs the theory of a node in a window;
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maederused by the node menu defined in initializeGraph-}
e7757995211bd395dc79d26fe017d99375f7d2a6Christian MaedergetTheoryOfNode :: GInfo -> Descr -> DGraphAndAGraphNode -> DGraph -> IO ()
e7757995211bd395dc79d26fe017d99375f7d2a6Christian MaedergetTheoryOfNode gInfo descr dgAndabstrNodeMap dgraph = do
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder r <- lookupTheoryOfNode (libEnvIORef gInfo) descr dgAndabstrNodeMap dgraph
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder case r of
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder Res.Result ds res -> do
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder showDiags (gi_hetcatsOpts gInfo) ds
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder case res of
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder (Just (n, gth)) ->
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder GUI.HTkUtils.displayTheoryWithWarning
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder "Theory"
8b4c68db8b465107cabef8b9cd5b6bc216e1b156Till Mossakowski (showName $ dgn_name $ lab' (contextDG dgraph n))
8b4c68db8b465107cabef8b9cd5b6bc216e1b156Till Mossakowski (addHasInHidingWarning dgraph n)
8b4c68db8b465107cabef8b9cd5b6bc216e1b156Till Mossakowski gth
c72c1e75a969ff4c336e77481c2a8e42603f13eeChristian Maeder _ -> return ()
23ab8855c58adfbd03a0730584b917b24c603901Christian Maeder
23ab8855c58adfbd03a0730584b917b24c603901Christian MaederdisplayTheory :: String -> Node -> DGraph -> G_theory -> IO ()
bcaf979d9babe6346aa343687aa7d596e2894cccPaolo TorrinidisplayTheory ext node dgraph gth =
bcaf979d9babe6346aa343687aa7d596e2894cccPaolo Torrini GUI.HTkUtils.displayTheory ext
bcaf979d9babe6346aa343687aa7d596e2894cccPaolo Torrini (showName $ dgn_name $ lab' (contextDG dgraph node))
1f63599faaa311cd024d6413f82bff8caae8de24Christian Maeder gth
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder
bcaf979d9babe6346aa343687aa7d596e2894cccPaolo Torrini{- | translate the theory of a node in a window;
bcaf979d9babe6346aa343687aa7d596e2894cccPaolo Torriniused by the node menu defined in initializeGraph-}
23ab8855c58adfbd03a0730584b917b24c603901Christian MaedertranslateTheoryOfNode :: GInfo -> Descr -> DGraphAndAGraphNode -> DGraph
23ab8855c58adfbd03a0730584b917b24c603901Christian Maeder -> IO ()
23ab8855c58adfbd03a0730584b917b24c603901Christian MaedertranslateTheoryOfNode gInfo@(GInfo {gi_hetcatsOpts = opts})
23ab8855c58adfbd03a0730584b917b24c603901Christian Maeder descr dgAndabstrNodeMap dgraph = do
8b4c68db8b465107cabef8b9cd5b6bc216e1b156Till Mossakowski libEnv <- readIORef $ libEnvIORef gInfo
8b4c68db8b465107cabef8b9cd5b6bc216e1b156Till Mossakowski case (do
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder (ln, node) <-
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder maybeToResult nullRange ("Node "++show descr++" not found")
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder $ InjMap.lookupWithB descr dgAndabstrNodeMap
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder th <- computeTheory libEnv ln node
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder return (node,th) ) of
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder Res.Result [] (Just (node,th)) -> do
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder Res.Result ds _ <- runResultT(
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder do G_theory lid sign _ sens _ <- return th
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers -- find all comorphism paths starting from lid
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder let paths = findComorphismPaths logicGraph (sublogicOfTh th)
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers -- let the user choose one
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers sel <- lift $ listBox "Choose a logic translation"
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder (map show paths)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder i <- case sel of
c55a0f77be7e88d3620b419ec8961f4379a586e3Klaus Luettich Just j -> return j
c55a0f77be7e88d3620b419ec8961f4379a586e3Klaus Luettich _ -> liftR $ fail "no logic translation chosen"
5d4038657f6a63e131f5804af2f7957b69e15a43Klaus Luettich Comorphism cid <- return (paths!!i)
6da66254a8cff186a1e550b4ace23fb7bcac0d90Christian Maeder -- adjust lid's
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder let lidS = sourceLogic cid
1f63599faaa311cd024d6413f82bff8caae8de24Christian Maeder lidT = targetLogic cid
d6c6ad132dcecc84fe71dbeeab6dba0e21483393Klaus Luettich sign' <- coerceSign lid lidS "" sign
d6c6ad132dcecc84fe71dbeeab6dba0e21483393Klaus Luettich sens' <- coerceThSens lid lidS "" sens
d6c6ad132dcecc84fe71dbeeab6dba0e21483393Klaus Luettich -- translate theory along chosen comorphism
1f63599faaa311cd024d6413f82bff8caae8de24Christian Maeder (sign'',sens1) <-
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers liftR $ wrapMapTheory cid (sign', toNamedList sens')
fb328c4f646dd3dd78a9391c5cb58450a3dd0aa9Klaus Luettich lift $ GUI.HTkUtils.displayTheoryWithWarning
fb328c4f646dd3dd78a9391c5cb58450a3dd0aa9Klaus Luettich "Translated Theory"
fb328c4f646dd3dd78a9391c5cb58450a3dd0aa9Klaus Luettich (showName $ dgn_name $ lab' (contextDG dgraph node))
1f63599faaa311cd024d6413f82bff8caae8de24Christian Maeder (addHasInHidingWarning dgraph node)
fb328c4f646dd3dd78a9391c5cb58450a3dd0aa9Klaus Luettich (G_theory lidT sign'' 0 (toThSens sens1) 0)
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder )
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder showDiags opts ds
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder return ()
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder Res.Result ds _ -> showDiags opts ds
1f63599faaa311cd024d6413f82bff8caae8de24Christian Maeder
1f63599faaa311cd024d6413f82bff8caae8de24Christian Maeder{- | outputs the sublogic of a node in a window;
1f63599faaa311cd024d6413f82bff8caae8de24Christian Maederused by the node menu defined in initializeGraph -}
1f63599faaa311cd024d6413f82bff8caae8de24Christian MaedergetSublogicOfNode :: IORef LibEnv -> Descr -> DGraphAndAGraphNode
d0652648f9879c67a194f8b03baafe2700c68eb4Christian Maeder -> DGraph -> IO()
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaedergetSublogicOfNode proofStatusRef descr dgAndabstrNodeMap dgraph = do
431d34c7007a787331c4e5ec997badb0f8190fc7Christian Maeder libEnv <- readIORef proofStatusRef
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder case InjMap.lookupWithB descr dgAndabstrNodeMap of
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder Just (ln, node) ->
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder let dgnode = lab' (contextDG dgraph node)
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder name = case dgnode of
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder (DGNode nname _ _ _ _ _ _) -> nname
88318aafc287e92931dceffbb943d58a9310001dChristian Maeder _ -> emptyNodeName
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder in case computeTheory libEnv ln node of
88318aafc287e92931dceffbb943d58a9310001dChristian Maeder Res.Result _ (Just th) ->
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder let logstr = show $ sublogicOfTh th
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder title = "Sublogic of "++showName name
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder in createTextDisplay title logstr [HTk.size(30,10)]
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder Res.Result ds _ ->
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder error $ "Could not compute theory for sublogic computation: "
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder ++ concatMap show ds
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder Nothing -> nodeErr descr
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder
c72c1e75a969ff4c336e77481c2a8e42603f13eeChristian Maeder-- | prints the origin of the node
c72c1e75a969ff4c336e77481c2a8e42603f13eeChristian MaedershowOriginOfNode :: Descr -> DGraphAndAGraphNode -> DGraph -> IO()
c72c1e75a969ff4c336e77481c2a8e42603f13eeChristian MaedershowOriginOfNode descr dgAndabstrNodeMap dgraph =
fdef3358918491badb0e29e42b5d3b5a01950716Christian Maeder case InjMap.lookupWithB descr dgAndabstrNodeMap of
6ff7a91875597d6e4dfaa68c79187d01473e8341Christian Maeder Just (_, node) ->
6ff7a91875597d6e4dfaa68c79187d01473e8341Christian Maeder do let dgnode = lab' (contextDG dgraph node)
6ff7a91875597d6e4dfaa68c79187d01473e8341Christian Maeder case dgnode of
88318aafc287e92931dceffbb943d58a9310001dChristian Maeder DGNode name _ _ _ orig _ _ ->
fdef3358918491badb0e29e42b5d3b5a01950716Christian Maeder let title = "Origin of node "++showName name
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder in createTextDisplay title
88318aafc287e92931dceffbb943d58a9310001dChristian Maeder (showDoc orig "") [HTk.size(30,10)]
7767474aba4fa2dc51a6c68017d3bcef3b773001Christian Maeder DGRef _ _ _ _ _ _ -> error "showOriginOfNode: no DGNode"
88318aafc287e92931dceffbb943d58a9310001dChristian Maeder Nothing -> nodeErr descr
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder
fdb2d618144159395f7bf8ce3327b3c112a17dd3Till Mossakowski-- | Show proof status of a node
340706b6c0c6e3dbacdd7003e20e9cab7f9aa765Christian MaedershowProofStatusOfNode :: GInfo -> Descr -> DGraphAndAGraphNode -> DGraph
88318aafc287e92931dceffbb943d58a9310001dChristian Maeder -> IO ()
bf76f4fcf07abaebea587df8135de8356c26a363Till MossakowskishowProofStatusOfNode _ descr dgAndabstrNodeMap dgraph =
88318aafc287e92931dceffbb943d58a9310001dChristian Maeder case InjMap.lookupWithB descr dgAndabstrNodeMap of
fdb2d618144159395f7bf8ce3327b3c112a17dd3Till Mossakowski Just (_, node) ->
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder do let dgnode = lab' (contextDG dgraph node)
6e049108aa87dc46bcff96fae50a4625df1d9648Klaus Luettich let stat = showStatusAux dgnode
f4505a64a089693012a3f5c3b1f12a82cd7a2a5aKlaus Luettich let title = "Proof status of node "++showName (dgn_name dgnode)
6e049108aa87dc46bcff96fae50a4625df1d9648Klaus Luettich createTextDisplay title stat [HTk.size(105,55)]
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder Nothing -> nodeErr descr
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder
f4505a64a089693012a3f5c3b1f12a82cd7a2a5aKlaus LuettichshowStatusAux :: DGNodeLab -> String
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaedershowStatusAux dgnode =
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder case dgn_theory dgnode of
f4505a64a089693012a3f5c3b1f12a82cd7a2a5aKlaus Luettich G_theory _ _ _ sens _ ->
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder let goals = OMap.filter (not . isAxiom) sens
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder (proven,open) = OMap.partition isProvenSenStatus goals
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder in "Proven proof goals:\n"
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder ++ showDoc proven ""
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder ++ if not $ hasOpenConsStatus True dgnode
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder then showDoc (dgn_cons_status dgnode)
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder "is the conservativity status of this node"
1a6464613c59e35072b90ca296ae402cbe956144Christian Maeder else ""
438f9bd974c8e668203e636b0f2bc80c589af043Klaus Luettich ++ "\nOpen proof goals:\n"
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder ++ showDoc open ""
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder ++ if hasOpenConsStatus False dgnode
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder then showDoc (dgn_cons_status dgnode)
88318aafc287e92931dceffbb943d58a9310001dChristian Maeder "should be the conservativity status of this node"
438f9bd974c8e668203e636b0f2bc80c589af043Klaus Luettich else ""
88318aafc287e92931dceffbb943d58a9310001dChristian Maeder
c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus Luettich-- | start local theorem proving or consistency checking at a node
proveAtNode :: Bool -> GInfo -> Descr -> DGraphAndAGraphNode -> DGraph -> IO ()
proveAtNode checkCons
gInfo@(GInfo {gi_LIB_NAME = ln, proofGUIMVar = guiMVar})
descr
dgAndabstrNodeMap
dgraph =
case InjMap.lookupWithB descr dgAndabstrNodeMap of
Just libNode -> if (checkCons
|| not (hasIncomingHidingEdge dgraph $ snd libNode))
then
proofMenu gInfo (basicInferenceNode checkCons
logicGraph libNode ln guiMVar)
else
GUI.HTkUtils.createInfoDisplayWithTwoButtons
"Warning"
"This node has incoming hiding links!!!"
"Prove anyway"
(proofMenu gInfo (basicInferenceNode checkCons
logicGraph libNode ln guiMVar))
Nothing -> nodeErr descr
-- | print the id of the edge
showIDOfEdge :: Descr -> Maybe (LEdge DGLinkLab) -> IO ()
showIDOfEdge _ (Just (_, _, linklab)) =
createTextDisplay "ID of Edge" (show $ dgl_id linklab) [HTk.size(30,10)]
showIDOfEdge descr Nothing =
createTextDisplay "Error"
("edge " ++ show descr ++ " has no corresponding edge"
++ "in the development graph") [HTk.size(30,10)]
-- | print the morphism of the edge
showMorphismOfEdge :: Descr -> Maybe (LEdge DGLinkLab) -> IO ()
showMorphismOfEdge _ (Just (_,_,linklab)) =
createTextDisplay "Signature morphism"
(showDoc (dgl_morphism linklab) "" ++ hidingMorph)
[HTk.size(100,40)]
where
hidingMorph = case dgl_type linklab of
HidingThm morph _ -> "\n ++++++ \n"
++ showDoc morph ""
_ -> ""
showMorphismOfEdge descr Nothing =
createTextDisplay "Error"
("edge " ++ show descr ++ " has no corresponding edge"
++ "in the development graph") [HTk.size(30,10)]
-- | print the origin of the edge
showOriginOfEdge :: Descr -> Maybe (LEdge DGLinkLab) -> IO ()
showOriginOfEdge _ (Just (_,_,linklab)) =
createTextDisplay "Origin of link"
(showDoc (dgl_origin linklab) "") [HTk.size(30,10)]
showOriginOfEdge descr Nothing =
createTextDisplay "Error"
("edge " ++ show descr ++ " has no corresponding edge"
++ "in the development graph") [HTk.size(30,10)]
-- | print the proof base of the edge
showProofStatusOfThm :: Descr -> Maybe (LEdge DGLinkLab) -> IO ()
showProofStatusOfThm _ (Just ledge) =
createTextSaveDisplay "Proof Status" "proofstatus.txt"
(showDoc (getProofStatusOfThm ledge) "\n")
showProofStatusOfThm descr Nothing =
-- why putStrLn here and no createTextDisplay elsewhere with this message
putStrLn ("edge " ++ show descr ++ " has no corresponding edge"
++ "in the development graph")
-- | check conservativity of the edge
checkconservativityOfEdge :: Descr -> GInfo -> Maybe (LEdge DGLinkLab) -> IO()
checkconservativityOfEdge _ gInfo
(Just (source,target,linklab)) = do
libEnv <- readIORef $ libEnvIORef gInfo
let dgraph = lookupDGraph (gi_LIB_NAME gInfo) libEnv
dgtar = lab' (contextDG dgraph target)
case dgtar of
DGNode _ (G_theory lid _ _ sens _) _ _ _ _ _ ->
case dgl_morphism linklab of
GMorphism cid _ _ morphism2 _ -> do
morphism2' <- coerceMorphism (targetLogic cid) lid
"checkconservativityOfEdge" morphism2
let th = case computeTheory libEnv (gi_LIB_NAME gInfo) source of
Res.Result _ (Just th1) -> th1
_ -> error "checkconservativityOfEdge: computeTheory"
G_theory lid1 sign1 _ sens1 _ <- return th
sign2 <- coerceSign lid1 lid "checkconservativityOfEdge.coerceSign" sign1
sens2 <- coerceThSens lid1 lid "" sens1
let Res.Result ds res =
conservativityCheck lid (sign2, toNamedList sens2)
morphism2' $ toNamedList sens
showRes = case res of
Just(Just True) -> "The link is conservative"
Just(Just False) -> "The link is not conservative"
_ -> "Could not determine whether link is conservative"
myDiags = unlines (map show ds)
createTextDisplay "Result of conservativity check"
(showRes ++ "\n" ++ myDiags) [HTk.size(50,50)]
DGRef _ _ _ _ _ _ -> error "checkconservativityOfEdge: no DGNode"
checkconservativityOfEdge descr _ Nothing =
createTextDisplay "Error"
("edge " ++ show descr ++ " has no corresponding edge "
++ "in the development graph") [HTk.size(30,10)]
getProofStatusOfThm :: (LEdge DGLinkLab) -> ThmLinkStatus
getProofStatusOfThm (_,_,label) =
case (dgl_type label) of
(LocalThm proofStatus _ _) -> proofStatus
(GlobalThm proofStatus _ _) -> proofStatus
(HidingThm _ proofStatus) -> proofStatus -- richtig?
_ -> error "the given edge is not a theorem"
{- | converts the nodes of the development graph, if it has any,
and returns the resulting conversion maps
if the graph is empty the conversion maps are returned unchanged-}
convertNodes :: ConversionMaps -> Descr -> GraphInfo -> DGraph
-> LIB_NAME -> IO ConversionMaps
convertNodes convMaps descr grInfo dgraph libname
| isEmptyDG dgraph = return convMaps
| otherwise = convertNodesAux convMaps
descr
grInfo
(labNodesDG dgraph)
libname
{- | auxiliary function for convertNodes if the given list of nodes is
emtpy, it returns the conversion maps unchanged otherwise it adds the
converted first node to the abstract graph and to the affected
conversion maps and afterwards calls itself with the remaining node
list -}
convertNodesAux :: ConversionMaps -> Descr -> GraphInfo ->
[LNode DGNodeLab] -> LIB_NAME -> IO ConversionMaps
convertNodesAux convMaps _ _ [] _ = return convMaps
convertNodesAux convMaps descr grInfo ((node,dgnode) : lNodes) libname =
do let nodetype = getDGNodeType dgnode
AGV.Result newDescr _ <- addnode descr
nodetype
(getDGNodeName dgnode)
grInfo
convertNodesAux convMaps
{ dgAndabstrNode = InjMap.insert (libname, node) newDescr
(dgAndabstrNode convMaps)
} descr grInfo lNodes libname
{- | converts the edges of the development graph
works the same way as convertNods does-}
convertEdges :: ConversionMaps -> Descr -> GraphInfo -> DGraph
-> LIB_NAME -> IO ConversionMaps
convertEdges convMaps descr grInfo dgraph libname
| isEmptyDG dgraph = return convMaps
| otherwise = convertEdgesAux convMaps
descr
grInfo
(labEdgesDG dgraph)
libname
-- | auxiliary function for convertEges
convertEdgesAux :: ConversionMaps -> Descr -> GraphInfo ->
[LEdge DGLinkLab] -> LIB_NAME -> IO ConversionMaps
convertEdgesAux convMaps _ _ [] _ = return convMaps
convertEdgesAux convMaps descr grInfo (ledge@(src,tar,edgelab) : lEdges)
libname =
do let srcnode = InjMap.lookupWithA (libname,src) (dgAndabstrNode convMaps)
tarnode = InjMap.lookupWithA (libname,tar) (dgAndabstrNode convMaps)
case (srcnode, tarnode) of
(Just s, Just t) -> do
AGV.Result newDescr msg <- addlink descr (getDGLinkType edgelab)
"" (Just ledge) s t grInfo
case msg of
Nothing -> return ()
Just err -> fail err
newConvMaps <- convertEdgesAux convMaps
{ dgAndabstrEdge = InjMap.insert (libname,
(src, tar, showDoc edgelab ""))
newDescr (dgAndabstrEdge convMaps)
} descr grInfo lEdges libname
return newConvMaps
_ -> error "Cannot find nodes"
-- | show library referened by a DGRef node (=node drawn as a box)
showReferencedLibrary :: Descr -> GInfo -> ConvFunc -> LibFunc
-> IO (Descr, GraphInfo, ConversionMaps)
showReferencedLibrary
descr gInfo@(GInfo {libEnvIORef = ioRefProofStatus,
conversionMapsIORef = convRef,
gi_GraphInfo = actGraphInfo,
gi_hetcatsOpts = opts}) convGraph
showLib = do
convMaps <- readIORef convRef
libname2dgMap <- readIORef ioRefProofStatus
case InjMap.lookupWithB descr (dgAndabstrNode convMaps) of
Just (libname,node) ->
case Map.lookup libname libname2dgMap of
Just dgraph ->
do let (_,(DGRef _ refLibname _ _ _ _)) =
labNode' (contextDG dgraph node)
case Map.lookup refLibname libname2dgMap of
Just _ -> do
(_,next) <- readIORef actGraphInfo
let gInfo' = gInfo {graphId = next}
gInfo'' <- setGInfo gInfo' refLibname libname2dgMap opts
convGraph gInfo'' "development graph" showLib
Nothing -> error $ "The referenced library ("
++ show refLibname
++ ") is unknown"
Nothing -> error $ "Selected node belongs to unknown library: "
++ show libname
Nothing ->
error $ "there is no node with the descriptor " ++ show descr
-- | prune displayed graph to subtree of selected node
showJustSubtree :: Descr -> Descr -> GInfo
-> IO (Descr, [[Node]], Maybe String)
showJustSubtree descr abstractGraph
(GInfo {libEnvIORef = ioRefProofStatus,
conversionMapsIORef = convRef,
visibleNodesIORef = visibleNodesRef,
gi_GraphInfo = actGraphInfo}) = do
convMaps <- readIORef convRef
libname2dgMap <- readIORef ioRefProofStatus
visibleNodes <- readIORef visibleNodesRef
case InjMap.lookupWithB descr (dgAndabstrNode convMaps) of
Just (libname,parentNode) ->
case Map.lookup libname libname2dgMap of
Just dgraph ->
do let allNodes = getNodeDescriptors (head visibleNodes)
libname convMaps
dgNodesOfSubtree = nub (parentNode : getNodesOfSubtree dgraph
(head visibleNodes) parentNode)
-- the selected node (parentNode) shall not be hidden either,
-- and we already know its descriptor (descr)
nodesOfSubtree = getNodeDescriptors dgNodesOfSubtree
libname convMaps
nodesToHide = filter (`notElem` nodesOfSubtree) allNodes
AGV.Result eventDescr errorMsg <- hidenodes abstractGraph
nodesToHide actGraphInfo
return (eventDescr, (dgNodesOfSubtree:visibleNodes), errorMsg)
Nothing -> error $
"showJustSubtree: Selected node belongs to unknown library: "
++ show libname
Nothing -> error $ "showJustSubtree: there is no node with the descriptor "
++ show descr
getNodeDescriptors :: [Node] -> LIB_NAME -> ConversionMaps -> [Descr]
getNodeDescriptors [] _ _ = []
getNodeDescriptors (node:nodelist) libname convMaps =
case InjMap.lookupWithA (libname, node) (dgAndabstrNode convMaps) of
Just descr -> descr:(getNodeDescriptors nodelist libname convMaps)
Nothing -> error $ "getNodeDescriptors: There is no descriptor for dgnode "
++ show node
getNodesOfSubtree :: DGraph -> [Node] -> Node -> [Node]
getNodesOfSubtree dgraph visibleNodes node =
concat (map (getNodesOfSubtree dgraph remainingVisibleNodes) predOfNode)
++ predOfNode
where predOfNode = [ n | n <- (preDG dgraph node), elem n visibleNodes]
remainingVisibleNodes =
[ n | n <- visibleNodes, notElem n predOfNode]
-- | apply the changes of first history item (computed by proof rules,
-- see folder Proofs) to the displayed development graph
applyChanges :: Descr -> LIB_NAME -> GraphInfo -> Descr -> IORef [[Node]]
-> ConversionMaps -> [([DGRule],[DGChange])]
-> IO (Descr, ConversionMaps)
applyChanges _ _ _ eventDescr _ convMaps [] = return (eventDescr,convMaps)
applyChanges gid libname grInfo eventDescr ioRefVisibleNodes convMaps
((_, historyElem) : _) =
applyChangesAux gid libname grInfo ioRefVisibleNodes (eventDescr, convMaps)
$ removeContraryChanges historyElem
-- | auxiliary function for applyChanges
applyChangesAux :: Descr -> LIB_NAME -> GraphInfo -> IORef [[Node]]
-> (Descr, ConversionMaps) -> [DGChange]
-> IO (Descr, ConversionMaps)
applyChangesAux gid libname grInfo ioRefVisibleNodes
(eventDescr, convMaps) changeList =
case changeList of
[] -> return (eventDescr, convMaps)
changes@(_:_) -> do
visibleNodes <- readIORef ioRefVisibleNodes
(newVisibleNodes, newEventDescr, newConvMaps) <-
applyChangesAux2 gid libname grInfo visibleNodes
eventDescr convMaps changes
writeIORef ioRefVisibleNodes newVisibleNodes
return (newEventDescr, newConvMaps)
-- | auxiliary function for applyChanges
applyChangesAux2 :: Descr -> LIB_NAME -> GraphInfo -> [[Node]] -> Descr
-> ConversionMaps -> [DGChange]
-> IO ([[Node]], Descr, ConversionMaps)
applyChangesAux2 _ _ _ visibleNodes eventDescr convMaps [] =
return (visibleNodes, eventDescr+1, convMaps)
applyChangesAux2 gid libname grInfo visibleNodes _ convMaps (change:changes) =
case change of
SetNodeLab _ (node, newLab) -> do
let nodetype = getDGNodeType newLab
nodename = getDGNodeName newLab
dgNode = (libname, node)
case InjMap.lookupWithA dgNode (dgAndabstrNode convMaps) of
Just abstrNode -> do
AGV.Result descr err <-
changeNodeType gid abstrNode nodetype grInfo
case err of
Nothing -> do
let newConvMaps = convMaps
{ dgAndabstrNode = InjMap.updateBWithA dgNode
descr (dgAndabstrNode convMaps) }
applyChangesAux2 gid libname grInfo visibleNodes
(descr+1) newConvMaps changes
Just msg ->
error $ "applyChangesAux2: could not set node "
++ show node ++" with name "
++ show nodename ++ "\n" ++ msg
Nothing -> error $ "applyChangesAux2: could not set node "
++ show node ++ " with name "
++ show nodename ++ ": " ++
"node does not exist in abstraction graph"
InsertNode (node, nodelab) -> do
let nodetype = getDGNodeType nodelab
nodename = getDGNodeName nodelab
AGV.Result descr err <-
addnode gid nodetype nodename grInfo
case err of
Nothing ->
do let dgNode = (libname,node)
newVisibleNodes = map (node :) visibleNodes
newConvMaps = convMaps
{ dgAndabstrNode = InjMap.insert dgNode descr
(dgAndabstrNode convMaps) }
applyChangesAux2 gid libname grInfo newVisibleNodes (descr+1)
newConvMaps changes
Just msg ->
error $ "applyChangesAux2: could not add node " ++ show node
++" with name " ++ show nodename ++ "\n" ++ msg
DeleteNode (node, nodelab) -> do
let nodename = getDGNodeName nodelab
dgnode = (libname,node)
case InjMap.lookupWithA dgnode (dgAndabstrNode convMaps) of
Just abstrNode -> do
AGV.Result descr err <- delnode gid abstrNode grInfo
case err of
Nothing -> do
let newVisibleNodes = map (filter (/= node)) visibleNodes
newConvMaps = convMaps
{ dgAndabstrNode = InjMap.delete dgnode abstrNode
(dgAndabstrNode convMaps) }
applyChangesAux2 gid libname grInfo newVisibleNodes (descr+1)
newConvMaps changes
Just msg -> error $ "applyChangesAux2: could not delete node "
++ show node ++ " with name "
++ show nodename ++ "\n" ++ msg
Nothing -> error $ "applyChangesAux2: could not delete node "
++ show node ++ " with name "
++ show nodename ++": " ++
"node does not exist in abstraction graph"
InsertEdge ledge@(src,tgt,edgelab) ->
do let dgAndabstrNodeMap = dgAndabstrNode convMaps
case (InjMap.lookupWithA (libname, src) dgAndabstrNodeMap,
InjMap.lookupWithA (libname, tgt) dgAndabstrNodeMap) of
(Just abstrSrc, Just abstrTgt) ->
do let dgEdge = (libname, (src,tgt,showDoc edgelab ""))
AGV.Result descr err <-
addlink gid (getDGLinkType edgelab)
"" (Just ledge) abstrSrc abstrTgt grInfo
case err of
Nothing ->
do let newConvMaps = convMaps
{ dgAndabstrEdge = InjMap.insert dgEdge descr
(dgAndabstrEdge convMaps) }
applyChangesAux2 gid libname grInfo visibleNodes
(descr + 1) newConvMaps changes
Just msg ->
error $ "applyChangesAux2: could not add link from "
++ show src ++ " to " ++ show tgt ++ ":\n"
++ show msg
_ -> error $ "applyChangesAux2: could not add link " ++ show src
++ " to " ++ show tgt ++ ": illegal end nodes"
DeleteEdge (src,tgt,edgelab) ->
do let dgEdge = (libname, (src,tgt,showDoc edgelab ""))
dgAndabstrEdgeMap = dgAndabstrEdge convMaps
case (InjMap.lookupWithA dgEdge dgAndabstrEdgeMap) of
Just abstrEdge ->
do AGV.Result descr err <- dellink gid abstrEdge grInfo
case err of
Nothing ->
do let newConvMaps = convMaps
{ dgAndabstrEdge = InjMap.delete dgEdge
abstrEdge (dgAndabstrEdge convMaps) }
applyChangesAux2 gid libname grInfo visibleNodes
(descr + 1) newConvMaps changes
Just msg -> error $
"applyChangesAux2: could not delete edge "
++ shows abstrEdge ":\n" ++ msg
Nothing -> error $ "applyChangesAux2: deleted edge from "
++ shows src " to " ++ shows tgt
" of type " ++ showDoc (dgl_type edgelab)
" and origin " ++ shows (dgl_origin edgelab)
" of development "
++ "graph does not exist in abstraction graph"
-- | display a window of translated graph with maximal sublogic.
openTranslateGraph :: LibEnv -> LIB_NAME -> HetcatsOpts
-> Res.Result G_sublogics -> ConvFunc -> LibFunc -> IO ()
openTranslateGraph libEnv ln opts (Res.Result diagsSl mSublogic) convGraph
showLib =
-- if an error existed by the search of maximal sublogicn
-- (see GUI.DGTranslation.getDGLogic), the process need not to go on.
if hasErrors diagsSl then
errorMess $ unlines $ map show
$ filter (relevantDiagKind . diagKind) diagsSl
else
do case mSublogic of
Just sublogic -> do
let paths = findComorphismPaths logicGraph sublogic
if null paths then
errorMess "This graph has no comorphism to translation."
else do
Res.Result diagsR i <- runResultT ( do
-- the user choose one
sel <- lift $ listBox "Choose a logic translation"
(map show paths)
case sel of
Just j -> return j
_ -> liftR $ fail "no logic translation chosen")
let aComor = paths !! fromJust i
-- graph translation.
case libEnv_translation libEnv aComor of
Res.Result diagsTrans (Just newLibEnv) -> do
showDiags opts (diagsSl ++ diagsR ++ diagsTrans)
if hasErrors (diagsR ++ diagsTrans) then
errorMess $ unlines $ map show
$ filter (relevantDiagKind . diagKind)
$ diagsR ++ diagsTrans
else dg_showGraphAux
(\gI -> do
gInfo <- setGInfo gI ln newLibEnv opts
convGraph gInfo "translation Graph"
showLib)
Res.Result diagsTrans Nothing ->
errorMess $ unlines $ map show
$ filter (relevantDiagKind . diagKind)
$ diagsSl ++ diagsR ++ diagsTrans
Nothing -> errorMess "the maximal sublogic is not found."
where relevantDiagKind Error = True
relevantDiagKind Warning = verbose opts >= 2
relevantDiagKind Hint = verbose opts >= 4
relevantDiagKind Debug = verbose opts >= 5
relevantDiagKind MessageW = False
dg_showGraphAux :: (GInfo -> IO (Descr, GraphInfo, ConversionMaps)) -> IO ()
dg_showGraphAux convFct = do
useHTk -- All messages are displayed in TK dialog windows
-- from this point on
gInfo <- emptyGInfo
(gid, gv, _cmaps) <- convFct gInfo
redisplay gid gv
return ()