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@informatik.uni-bremen.de

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederStability : provisional

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederPortability : non-portable (imports Logic)

43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder-}

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder

d8c71aacc9f1c8cd40a8ad8dcdad9be8854b849fChristian Maedermodule GUI.GraphLogic

f2f9df2e17e70674f0bf426ed1763c973ee4cde0Christian Maeder ( undo

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder , reload

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder , remakeGraph

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder , performProofAction

a53841f6d6e86ac751c12a33dc8aadf53f59d977Klaus Luettich , openProofStatus

a737caf82de97c1907027c03e4b4509eb492b4b8Christian Maeder , saveProofStatus

a737caf82de97c1907027c03e4b4509eb492b4b8Christian Maeder , nodeErr

a737caf82de97c1907027c03e4b4509eb492b4b8Christian Maeder , proofMenu

a737caf82de97c1907027c03e4b4509eb492b4b8Christian Maeder , openTranslateGraph

a737caf82de97c1907027c03e4b4509eb492b4b8Christian Maeder , showReferencedLibrary

a737caf82de97c1907027c03e4b4509eb492b4b8Christian Maeder , showSpec

a53841f6d6e86ac751c12a33dc8aadf53f59d977Klaus Luettich , getSignatureOfNode

a53841f6d6e86ac751c12a33dc8aadf53f59d977Klaus Luettich , getTheoryOfNode

a53841f6d6e86ac751c12a33dc8aadf53f59d977Klaus Luettich , getLocalAxOfNode

a53841f6d6e86ac751c12a33dc8aadf53f59d977Klaus Luettich , translateTheoryOfNode

a737caf82de97c1907027c03e4b4509eb492b4b8Christian Maeder , displaySubsortGraph

3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich , displayConceptGraph

96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian Maeder , lookupTheoryOfNode

01e383014b555bbcf639c0ca60c5810b3eff83c0Christian Maeder , getSublogicOfNode

3b06e23643a9f65390cb8c1caabe83fa7e87a708Till Mossakowski , showOriginOfNode

df29370ae8d8b41587957f6bcdcb43a3f1927e47Christian Maeder , showProofStatusOfNode

bd54a9917cd87169b8e40bcc5616c537fed85815Christian Maeder , proveAtNode

a53841f6d6e86ac751c12a33dc8aadf53f59d977Klaus Luettich , showJustSubtree

a53841f6d6e86ac751c12a33dc8aadf53f59d977Klaus Luettich , showIDOfEdge

8c7a54ad8bf776a530ecf907a373d42415cf4faeChristian Maeder , getNumberOfNode

ce8b15da31cd181b7e90593cbbca98f47eda29d6Till Mossakowski , showMorphismOfEdge

e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder , showOriginOfEdge

e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder , checkconservativityOfEdge

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder , showProofStatusOfThm

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder , convertNodes

ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder , convertEdges

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder , hideNodes

2e2094a642e3775b0d76b890556407941d3a53b6Christian Maeder , getLibDeps

2e2094a642e3775b0d76b890556407941d3a53b6Christian Maeder , hideShowNames

6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder , showNodes

e8db9a65830cf71504e33c6f441a67b4d184a3caChristian Maeder , translateGraph

c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder , showLibGraph

8410667510a76409aca9bb24ff0eda0420088274Christian Maeder )

6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder where

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder

8410667510a76409aca9bb24ff0eda0420088274Christian Maederimport Logic.Logic(conservativityCheck)

404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettichimport Logic.ExtSign

b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maederimport Logic.Coerce(coerceSign, coerceMorphism)

3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettichimport Logic.Grothendieck

3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettichimport Logic.Comorphism

4d56f2fa72e4aec20eb827c11ed49c8cbb7014bdChristian Maederimport Logic.Prover

4cb215739e9ab13447fa21162482ebe485b47455Christian Maeder

8ef75f1cc0437656bf622cec5ac9e8ea221da8f2Christian Maederimport Comorphisms.LogicGraph(logicGraph)

404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederimport Syntax.AS_Library(LIB_NAME, getModTime, getLIB_ID)

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder

55adfe57a4de1f36adc3e3bfc16f342e44a7d444Christian Maederimport Static.GTheory

d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maederimport Static.DevGraph

8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maederimport Static.DGToSpec(dgToSpec, computeTheory)

8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maederimport Static.AnalysisLibrary(anaLibExt, anaLib)

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederimport Static.DGTranslation(libEnv_translation)

e593b89bfd4952698dc37feced21cefe869d87a2Christian Maeder

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederimport Proofs.EdgeUtils

e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maederimport Proofs.InferBasic(basicInferenceNode)

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederimport Proofs.StatusUtils(lookupHistory, removeContraryChanges)

0206ab93ef846e4e0885996d052b9b73b9dc66b0Christian Maeder

f13d1e86e58da53680e78043e8df182eed867efbChristian Maederimport GUI.Utils(listBox, createTextSaveDisplay)

cdd280437686b1e2e25e3761d4adf3d4a0a2d11cKlaus Luettichimport GUI.Taxonomy (displayConceptGraph,displaySubsortGraph)

96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian Maederimport GUI.DGTranslation(getDGLogic)

e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maederimport GUI.GraphTypes

e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maederimport GUI.AbstractGraphView as AGV

c6fcd42c6d6d9dae8c7835c24fcb7ce8531a9050Christian Maederimport qualified GUI.HTkUtils (displayTheory,

31c49f2fa23d4ac089f35145d80a224deb6ea7e4Till Mossakowski displayTheoryWithWarning,

c55a0f77be7e88d3620b419ec8961f4379a586e3Klaus Luettich createInfoDisplayWithTwoButtons)

36f63902db2b3463faa9f59912ad106e2d5aaa24Klaus Luettich

36f63902db2b3463faa9f59912ad106e2d5aaa24Klaus Luettichimport GraphDisp(deleteArc, deleteNode)

363939beade943a02b31004cea09dec34fa8a6d9Christian Maederimport TextDisplay(createTextDisplay)

363939beade943a02b31004cea09dec34fa8a6d9Christian Maederimport InfoBus(encapsulateWaitTermAct)

8cacad2a09782249243b80985f28e9387019fe40Christian Maederimport DialogWin (useHTk)

363939beade943a02b31004cea09dec34fa8a6d9Christian Maederimport Messages(errorMess)

a7c27282e71cf4505026645f96d4f5cb8a284e32Christian Maederimport qualified HTk

363939beade943a02b31004cea09dec34fa8a6d9Christian Maederimport Configuration(size)

8a28707e9155465c6f2236a06eac6580a65c7025Christian Maeder

47b0e9f3cb008cb7997f4e3bae26e4d62dcc887aChristian Maederimport Common.Id(nullRange)

431d34c7007a787331c4e5ec997badb0f8190fc7Christian Maederimport Common.DocUtils(showDoc, pretty)

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederimport Common.Doc(vcat)

d3ae0072823e2ef0d41d4431fcc768e66489c20eChristian Maederimport Common.ResultT(liftR, runResultT)

9e748851c150e1022fb952bab3315e869aaf0214Christian Maederimport Common.AS_Annotation(isAxiom)

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederimport Common.Result as Res

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederimport qualified Common.OrderedMap as OMap

9e748851c150e1022fb952bab3315e869aaf0214Christian Maederimport qualified Common.InjMap as InjMap

9e748851c150e1022fb952bab3315e869aaf0214Christian Maederimport qualified Common.Lib.Rel as Rel

6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maederimport qualified Common.Lib.Graph as Tree

6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder

6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maederimport Driver.Options

6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maederimport Driver.WriteFn(writeShATermFile)

6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maederimport Driver.ReadFn(libNameToFile, readVerbose)

a7c27282e71cf4505026645f96d4f5cb8a284e32Christian Maeder

9e748851c150e1022fb952bab3315e869aaf0214Christian Maederimport System.Directory(getModificationTime)

9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder

f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maederimport Data.IORef

776a1a086df734581431e6edb4343ed4c8d34d55Christian Maederimport Data.Maybe(fromJust)

f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maederimport Data.List(nub,deleteBy,find)

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederimport Data.Graph.Inductive.Graph as Graph(Node, LEdge, LNode, lab', labNode')

61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maederimport qualified Data.IntMap as IntMap

c0c2380bced8159ff0297ece14eba948bd236471Christian Maederimport qualified Data.Map as Map

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederimport Control.Monad.Trans(lift)

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederimport Control.Concurrent.MVar

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaedernegateChanges :: ([DGRule],[DGChange]) -> ([DGRule],[DGChange])

9e748851c150e1022fb952bab3315e869aaf0214Christian MaedernegateChanges (_, dgChanges) = ([], reverse $ map negateChange dgChanges)

6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder where

6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder negateChange :: DGChange -> DGChange

6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder negateChange change = case change of

c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder InsertNode x -> DeleteNode x

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder DeleteNode x -> InsertNode x

ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder InsertEdge x -> DeleteEdge x

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder DeleteEdge x -> InsertEdge x

6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder SetNodeLab old (node, new) -> SetNodeLab new (node, old)

4017ebc0f692820736d796af3110c3b3018c108aChristian Maeder

ad4889ebb40efae8595b0969dd6ba1162d52bac3Christian Maeder-- | Undo one step of the History

4017ebc0f692820736d796af3110c3b3018c108aChristian Maederundo :: GInfo -> Bool -> IO ()

6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maederundo gInfo@(GInfo { libEnvIORef = ioRefProofStatus

6ff7a91875597d6e4dfaa68c79187d01473e8341Christian Maeder , globalHist = gHist

6ff7a91875597d6e4dfaa68c79187d01473e8341Christian Maeder , graphId = gid

6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder , gi_GraphInfo = actGraph

6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder }) isUndo = do

4017ebc0f692820736d796af3110c3b3018c108aChristian Maeder (guHist, grHist) <- takeMVar gHist

6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder putStrLn $ show guHist

6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder putStrLn $ show grHist

6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder case if isUndo then guHist else grHist of

6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder [] -> do

6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder showTemporaryMessage gid actGraph "History is empty..."

88318aafc287e92931dceffbb943d58a9310001dChristian Maeder putMVar gHist (guHist, grHist)

6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder (lns:gHist') -> do

a3c6d8e0670bf2aa71bc8e2a3b1f45d56dd65e4cChristian Maeder le <- readIORef ioRefProofStatus

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder undoDGraphs gInfo isUndo lns

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder putStrLn $ show $ filter (\ln -> elem ln lns) $ Map.keys le

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder updateDGraphs le $ filter (\ln -> elem ln lns) $ Map.keys le

363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder putMVar gHist $ if isUndo then (gHist', (reverse lns):grHist)

363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder else ((reverse lns):guHist, gHist')

363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder

ca074a78b8dcccbb8c419586787882f98d0c6163Christian MaederundoDGraphs :: GInfo -> Bool -> [LIB_NAME] -> IO ()

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederundoDGraphs _ _ [] = return ()

ca074a78b8dcccbb8c419586787882f98d0c6163Christian MaederundoDGraphs g u (ln:r) = do

ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder undoDGraph g u ln

ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder undoDGraphs g u r

4017ebc0f692820736d796af3110c3b3018c108aChristian Maeder

ca074a78b8dcccbb8c419586787882f98d0c6163Christian MaederundoDGraph :: GInfo -> Bool -> LIB_NAME -> IO ()

0be0db405c49906bd7057255069bf6df53395ac9Klaus LuettichundoDGraph (GInfo { libEnvIORef = ioRefProofStatus

ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder , graphId = gid

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder , gi_GraphInfo = actGraph

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder }) isUndo ln = do

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder showTemporaryMessage gid actGraph $ "Undo last change to " ++ show ln ++ "..."

f2f9df2e17e70674f0bf426ed1763c973ee4cde0Christian Maeder le <- readIORef ioRefProofStatus

d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder let

d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder dg = lookupDGraph ln le

d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder (phist,rhist) = if isUndo then (proofHistory dg, redoHistory dg)

d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder else (redoHistory dg, proofHistory dg)

d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder change = negateChanges $ head phist

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder dg'' = (applyProofHistory [change] dg)

d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder dg' = case isUndo of

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder True -> dg'' { redoHistory = change:rhist

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder , proofHistory = tail phist}

ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder False -> dg'' { redoHistory = tail phist

ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder , proofHistory = change:rhist}

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder writeIORef ioRefProofStatus $ Map.insert ln dg' le

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder

ca074a78b8dcccbb8c419586787882f98d0c6163Christian MaederupdateDGraphs :: LibEnv -> [LIB_NAME] -> IO ()

ca074a78b8dcccbb8c419586787882f98d0c6163Christian MaederupdateDGraphs _ [] = return ()

d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian MaederupdateDGraphs le (ln:r) = do

d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder updateDGraph $ lookupDGraph ln le

f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder updateDGraphs le r

d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder

d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian MaederupdateDGraph :: DGraph -> IO ()

89f7631cbfbd1bb99fc152b434bd362a7799d295Christian MaederupdateDGraph dg = case openlock dg of

363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder Just lock -> do

61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder mRemakeF <- tryTakeMVar lock

f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder case mRemakeF of

363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder Just remakeF -> do

363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder putMVar lock remakeF

f4505a64a089693012a3f5c3b1f12a82cd7a2a5aKlaus Luettich remakeF

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder Nothing -> return ()

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder Nothing -> return ()

f4505a64a089693012a3f5c3b1f12a82cd7a2a5aKlaus Luettich

e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder-- | reloads the Library of the DevGraph

6b6773cf587b74259178641d811746a235faf056Christian Maederreload :: GInfo -> IO()

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederreload gInfo@(GInfo { libEnvIORef = ioRefProofStatus

2c619a4dfdc1df27573eba98e81ed1ace906941dChristian Maeder , gi_LIB_NAME = ln

36f63902db2b3463faa9f59912ad106e2d5aaa24Klaus Luettich , 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

7c5c311d67e187280877c45bd89dcba9038bc0a3Christian Maeder ioruplibs <- newIORef ([] :: [LIB_NAME])

7c5c311d67e187280877c45bd89dcba9038bc0a3Christian Maeder writeIORef ioruplibs []

7c5c311d67e187280877c45bd89dcba9038bc0a3Christian Maeder reloadLibs ioRefProofStatus opts libdeps ioruplibs ln

7c5c311d67e187280877c45bd89dcba9038bc0a3Christian Maeder remakeGraph gInfo

7c5c311d67e187280877c45bd89dcba9038bc0a3Christian Maeder

7c5c311d67e187280877c45bd89dcba9038bc0a3Christian Maeder-- | Creates a list of all LIB_NAME pairs, which have a dependency

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaedergetLibDeps :: LibEnv -> [(LIB_NAME, LIB_NAME)]

83394c6b6e6de128e71b67c9251ed7a84485d082Christian MaedergetLibDeps le =

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder concat $ map (\ ln -> getDep ln le) $ Map.keys le

6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- | Creates a list of LIB_NAME pairs for the fist argument

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaedergetDep :: LIB_NAME -> LibEnv -> [(LIB_NAME, LIB_NAME)]

6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian MaedergetDep ln le =

6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder map (\ x -> (ln, x)) $ map (\ (_,x,_) -> dgn_libname x) $ IntMap.elems $

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder IntMap.filter (\ (_,x,_) -> isDGRef x) $ Tree.convertToMap $

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder dgBody $ lookupDGraph ln le

9df11f85fd7f8c4745d64464876e84ec4e263692Christian Maeder

8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers-- | Reloads a library

010c56c4cf12dd7977ca36efe85219b91e265ee3Christian MaederreloadLib :: IORef LibEnv -> HetcatsOpts -> IORef [LIB_NAME] -> LIB_NAME

fb328c4f646dd3dd78a9391c5cb58450a3dd0aa9Klaus Luettich -> IO ()

3b06e23643a9f65390cb8c1caabe83fa7e87a708Till MossakowskireloadLib iorle opts ioruplibs ln = do

5b818f10e11fc79def1fdd5c8a080d64a6438d87Christian Maeder mfile <- existsAnSource opts {intype = GuessIn}

8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers $ rmSuffix $ libNameToFile opts ln

819e29dba060687cf391e444e0f6ff88c1908cc3Christian Maeder case mfile of

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Nothing -> do

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder return ()

383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder Just file -> do

8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers le <- readIORef iorle

9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder let

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder le' = Map.delete ln le

61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder mres <- anaLibExt opts file le'

383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder case mres of

383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder Just (_, newle) -> do

383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder uplibs <- readIORef ioruplibs

383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder writeIORef ioruplibs $ ln:uplibs

383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder writeIORef iorle newle

383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder return ()

d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder Nothing -> do

d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder fail $ "Could not read original development graph from '"++ file

d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder ++ "'"

819e29dba060687cf391e444e0f6ff88c1908cc3Christian Maeder return ()

819e29dba060687cf391e444e0f6ff88c1908cc3Christian Maeder

819e29dba060687cf391e444e0f6ff88c1908cc3Christian Maeder-- | Reloads libraries if nessesary

d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian MaederreloadLibs :: IORef LibEnv -> HetcatsOpts -> [(LIB_NAME, LIB_NAME)]

d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder -> IORef [LIB_NAME] -> LIB_NAME -> IO Bool

d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian MaederreloadLibs iorle opts deps ioruplibs ln = do

d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder uplibs <- readIORef ioruplibs

d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder case elem ln uplibs of

d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder True -> return True

d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder False -> do

d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder let

d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder deps' = map (snd) $ filter (\ (ln',_) -> ln == ln') deps

d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder res <- mapM (reloadLibs iorle opts deps ioruplibs) deps'

d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder let

d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder libupdate = foldl (\ u r -> if r then True else u) False res

d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder case libupdate of

d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder True -> do

d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder reloadLib iorle opts ioruplibs ln

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder return True

e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder False -> do

61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder le <- readIORef iorle

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder let

6fe9628743562678acf97d6730ebcfee5e9e50c2Christian Maeder newln:_ = filter (ln ==) $ Map.keys le

e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder mfile <- existsAnSource opts $ rmSuffix $ libNameToFile opts ln

61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder case mfile of

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Nothing -> do

3b06e23643a9f65390cb8c1caabe83fa7e87a708Till Mossakowski return False

b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder Just file -> do

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder newmt <- getModificationTime file

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder let

61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder libupdate' = (getModTime $ getLIB_ID newln) < newmt

fb328c4f646dd3dd78a9391c5cb58450a3dd0aa9Klaus Luettich case libupdate' of

fb328c4f646dd3dd78a9391c5cb58450a3dd0aa9Klaus Luettich False -> return False

e96a0bf4040fd789339958c01f145c5057d26db6René Wagner True -> do

e96a0bf4040fd789339958c01f145c5057d26db6René Wagner reloadLib iorle opts ioruplibs ln

abf2487c3aece95c371ea89ac64319370dcb6483Klaus Luettich return True

abf2487c3aece95c371ea89ac64319370dcb6483Klaus Luettich

61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder-- | Deletes the old edges and nodes of the Graph and makes new ones

61fa0ac06ede811c7aad54ec4c4202346727368eChristian MaederremakeGraph :: GInfo -> IO ()

61fa0ac06ede811c7aad54ec4c4202346727368eChristian MaederremakeGraph (GInfo { libEnvIORef = ioRefProofStatus

8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers , conversionMapsIORef = convRef

61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder , graphId = gid

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder , gi_LIB_NAME = ln

b9b960bc75e34658e70c4a0231dbc6a6e7373f2dChristian Maeder , gi_GraphInfo = actGraphInfo

18a4d5cb6828f080db9c5f9551785c5151027271Christian Maeder }) = do

0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich le <- readIORef ioRefProofStatus

9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder (gs,ev_cnt) <- readIORef actGraphInfo

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder let

fdb2d618144159395f7bf8ce3327b3c112a17dd3Till Mossakowski dgraph = lookupDGraph ln le

43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder Just (_, g) = find (\ (gid', _) -> gid' == gid) gs

383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder gs' = deleteBy (\ (gid1,_) (gid2,_) -> gid1 == gid2) (gid,g) gs

3b06e23643a9f65390cb8c1caabe83fa7e87a708Till Mossakowski og = theGraph g

61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder -- reads and delets the old nodes and edges

61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder mapM_ (deleteArc og) $ map (\ (_,_,_,x) -> x) $ Map.elems $ AGV.edges g

c9acb8681bcc512245b4f0d1a9f2b189c60e10d4Christian Maeder mapM_ (deleteNode og) $ map snd $ Map.elems $ AGV.nodes g

38352346eb1a67ba0f4eab8ad6f718528cf0cde0Christian Maeder -- stores the graph without nodes and edges in the GraphInfo

8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder let

63e50b4c36074d5fb9de872c4007b688b4bce534Christian Maeder g' = g {theGraph = og, AGV.nodes = Map.empty, AGV.edges = Map.empty}

63e50b4c36074d5fb9de872c4007b688b4bce534Christian Maeder writeIORef actGraphInfo ((gid,g'):gs',ev_cnt)

bd54a9917cd87169b8e40bcc5616c537fed85815Christian Maeder -- creates new nodes and edges

11b55e6fbbc397b9fa41a7d61be53c6f4f027824Christian Maeder newConvMaps <- convertNodes emptyConversionMaps gid actGraphInfo dgraph ln

11b55e6fbbc397b9fa41a7d61be53c6f4f027824Christian Maeder finalConvMaps <- convertEdges newConvMaps gid actGraphInfo dgraph ln

6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder -- writes the ConversionMap and redisplays the graph

e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder writeIORef convRef finalConvMaps

e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder redisplay gid actGraphInfo

d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder return ()

6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederhideShowNames :: GInfo -> Bool -> IO ()

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederhideShowNames (GInfo {graphId = gid,

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder gi_GraphInfo = actGraphInfo,

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder internalNamesIORef = showInternalNames

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder }) toggle = do

6bf24e5eb644064ad650eb3fd9774483fccbf601Christian Maeder deactivateGraphWindow gid actGraphInfo

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder (intrn::InternalNames) <- readIORef showInternalNames

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder let showThem = if toggle then not $ showNames intrn else showNames intrn

ffd3a0c7339cc3637f022c38e66a7aa9f0cf10d3Rainer Grabbe showItrn s = if showThem then s else ""

e8db9a65830cf71504e33c6f441a67b4d184a3caChristian Maeder mapM_ (\(s,upd) -> upd (\_ -> showItrn s)) $ updater intrn

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder writeIORef showInternalNames $ intrn {showNames = showThem}

1f8a7f8343f7df719768d2b1d7e3077ee291a1caChristian Maeder redisplay gid actGraphInfo

1f8a7f8343f7df719768d2b1d7e3077ee291a1caChristian Maeder activateGraphWindow gid actGraphInfo

61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder return ()

6bf24e5eb644064ad650eb3fd9774483fccbf601Christian Maeder

dbe752ee940baae7f9f231f29c62284bb0f90a25Christian MaedershowNodes :: GInfo -> IO ()

53818ced114da21321063fff307aa41c1ab31dd3Achim MahnkeshowNodes gInfo@(GInfo {descrIORef = event,

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder graphId = gid,

53818ced114da21321063fff307aa41c1ab31dd3Achim Mahnke gi_GraphInfo = actGraphInfo

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder }) = do

53818ced114da21321063fff307aa41c1ab31dd3Achim Mahnke deactivateGraphWindow gid actGraphInfo

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder descr <- readIORef event

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder AGV.Result _ errorMsg <- checkHasHiddenNodes gid descr actGraphInfo

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder case errorMsg of

3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich Nothing -> do

3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich showTemporaryMessage gid actGraphInfo "Revealing hidden nodes ..."

363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder showIt gid descr actGraphInfo

363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder hideShowNames gInfo False

1f63599faaa311cd024d6413f82bff8caae8de24Christian Maeder return ()

857992065be4ed40a72c6296b6c0aec62ab4c5b9Christian Maeder Just _ -> do

fdb2d618144159395f7bf8ce3327b3c112a17dd3Till Mossakowski showTemporaryMessage gid actGraphInfo "No hidden nodes found ..."

7c99e334446bb97120e30e967baeeddfdd1278deKlaus Luettich return ()

4017ebc0f692820736d796af3110c3b3018c108aChristian Maeder activateGraphWindow gid actGraphInfo

4017ebc0f692820736d796af3110c3b3018c108aChristian Maeder return ()

e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder

ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian MaederhideNodes :: GInfo -> IO ()

33d042fe6a9eb27a4c48f840b80838f3e7d98e34Christian MaederhideNodes (GInfo {descrIORef = event,

83394c6b6e6de128e71b67c9251ed7a84485d082Christian Maeder graphId = gid,

fa21fba9ceb1ddf7b3efd54731a12ed8750191d8Christian Maeder gi_GraphInfo = actGraphInfo

fa21fba9ceb1ddf7b3efd54731a12ed8750191d8Christian Maeder }) = do

e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder deactivateGraphWindow gid actGraphInfo

0c355dd0b739631ee472f9a656e266be27fa4e64Christian Maeder descr' <- readIORef event

e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder AGV.Result _ errorMsg <- checkHasHiddenNodes gid descr' actGraphInfo

fa21fba9ceb1ddf7b3efd54731a12ed8750191d8Christian Maeder case errorMsg of

b49276c9f50038e0bd499ad49f7bd6444566a834Christian Maeder Nothing -> do

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder showTemporaryMessage gid actGraphInfo "Nodes already hidden ..."

b49276c9f50038e0bd499ad49f7bd6444566a834Christian Maeder return ()

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder Just _ -> do

e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder showTemporaryMessage gid actGraphInfo "Hiding unnamed nodes..."

c7ec85d1103173e089aa5048fd7afb2f9b505124Klaus Luettich AGV.Result descr msg <- hideSetOfNodeTypes gid

c7ec85d1103173e089aa5048fd7afb2f9b505124Klaus Luettich [--red nodes are not hidden

c7ec85d1103173e089aa5048fd7afb2f9b505124Klaus Luettich --"open_cons__internal",

c7ec85d1103173e089aa5048fd7afb2f9b505124Klaus Luettich --"locallyEmpty__open_cons__internal",

c7ec85d1103173e089aa5048fd7afb2f9b505124Klaus Luettich --"proven_cons__internal",

b905126bab9454b89041f92b3c50bb9efc85e427Klaus Luettich "locallyEmpty__proven_cons__internal"]

5ea9168eddbfbfe2282ed46dfe107a8962d6727bChristian Maeder True actGraphInfo

c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus Luettich writeIORef event descr

5c69cef4668bbd959d721668313a779126014d1eKlaus Luettich case msg of

b905126bab9454b89041f92b3c50bb9efc85e427Klaus Luettich Nothing -> do redisplay gid actGraphInfo

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder return ()

e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder Just err -> putStrLn err

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder activateGraphWindow gid actGraphInfo

43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder return ()

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaedertranslateGraph :: GInfo -> ConvFunc -> LibFunc -> IO ()

e7757995211bd395dc79d26fe017d99375f7d2a6Christian MaedertranslateGraph (GInfo {libEnvIORef = ioRefProofStatus,

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder gi_LIB_NAME = ln,

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder gi_hetcatsOpts = opts

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder }) convGraph showLib = do

c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus Luettich le <- readIORef ioRefProofStatus

c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus Luettich openTranslateGraph le ln opts (getDGLogic le) convGraph showLib

c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus Luettich

c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus LuettichshowLibGraph :: GInfo -> LibFunc -> IO ()

c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus LuettichshowLibGraph gInfo showLib = do

c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus Luettich showLib gInfo

c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus Luettich return ()

c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus Luettich

c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus Luettich{- | it tries to perform the given action to the given graph.

c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus Luettich If part of the given graph is not hidden, then the action can

c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus Luettich be performed directly; otherwise the graph will be shown completely

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder firstly, and then the action will be performed, and after that the graph

b905126bab9454b89041f92b3c50bb9efc85e427Klaus Luettich will be hidden again.

b905126bab9454b89041f92b3c50bb9efc85e427Klaus Luettich-}

b905126bab9454b89041f92b3c50bb9efc85e427Klaus LuettichperformProofAction :: GInfo -> IO () -> IO ()

b905126bab9454b89041f92b3c50bb9efc85e427Klaus LuettichperformProofAction gInfo@(GInfo {descrIORef = event,

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder graphId = gid,

33d042fe6a9eb27a4c48f840b80838f3e7d98e34Christian Maeder gi_GraphInfo = actGraphInfo

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder }) proofAction = do

dbe752ee940baae7f9f231f29c62284bb0f90a25Christian Maeder deactivateGraphWindow gid actGraphInfo

1f8a7f8343f7df719768d2b1d7e3077ee291a1caChristian Maeder let actionWithMessage = do

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder showTemporaryMessage gid actGraphInfo

1f8a7f8343f7df719768d2b1d7e3077ee291a1caChristian Maeder "Applying development graph calculus proof rule..."

1f8a7f8343f7df719768d2b1d7e3077ee291a1caChristian Maeder proofAction

68aab98a58d1460c77a1573a86c32a891756a420Christian Maeder descr <- readIORef event

1f8a7f8343f7df719768d2b1d7e3077ee291a1caChristian Maeder AGV.Result _ errorMsg <- checkHasHiddenNodes gid descr actGraphInfo

1f8a7f8343f7df719768d2b1d7e3077ee291a1caChristian Maeder case errorMsg of

96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian Maeder Nothing -> do

96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian Maeder showNodes gInfo

1f8a7f8343f7df719768d2b1d7e3077ee291a1caChristian Maeder actionWithMessage

3a7788e09dd23b364a46c9488cbd1522369113dbChristian Maeder hideNodes gInfo

e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder Just _ -> actionWithMessage

ef67402074be14deb95e4ff564737d5593144130Klaus Luettich showTemporaryMessage gid actGraphInfo

dbe752ee940baae7f9f231f29c62284bb0f90a25Christian Maeder "Development graph calculus proof rule finished."

ef67402074be14deb95e4ff564737d5593144130Klaus Luettich activateGraphWindow gid actGraphInfo

462d9dc583444aab82732e14a75610684d2dc7e9Christian Maeder return ()

c9e197862d9d8ef2585270dd08f5194b3aed4a9dKlaus Luettich

e7e1ab2ac3f1fded8611bb92ae00e8f3b8c693fbKlaus LuettichsaveProofStatus :: GInfo -> FilePath -> IO ()

ef67402074be14deb95e4ff564737d5593144130Klaus LuettichsaveProofStatus (GInfo {libEnvIORef = ioRefProofStatus,

1323eba62fc519b068f5aaec4f9d2be05ffabea9Klaus Luettich gi_LIB_NAME = ln,

a80c28bb8b7a23ccdf7e08d0fe216fc19cc97273Klaus Luettich gi_hetcatsOpts = opts

d784803f9c752667b4fcf7393d698002bedf3f89Klaus Luettich }) file = encapsulateWaitTermAct $ do

1323eba62fc519b068f5aaec4f9d2be05ffabea9Klaus Luettich proofStatus <- readIORef ioRefProofStatus

1323eba62fc519b068f5aaec4f9d2be05ffabea9Klaus Luettich writeShATermFile file (ln, lookupHistory ln proofStatus)

1f8a7f8343f7df719768d2b1d7e3077ee291a1caChristian Maeder putIfVerbose opts 2 $ "Wrote " ++ file

1f8a7f8343f7df719768d2b1d7e3077ee291a1caChristian Maeder

462d9dc583444aab82732e14a75610684d2dc7e9Christian Maeder-- | implementation of open menu, read in a proof status

5d39c60274aaa76506292d2d9e885fccd27e1eabChristian MaederopenProofStatus :: GInfo -> FilePath -> ConvFunc -> LibFunc

5d39c60274aaa76506292d2d9e885fccd27e1eabChristian Maeder -> IO (Descr, GraphInfo, ConversionMaps)

e7757995211bd395dc79d26fe017d99375f7d2a6Christian MaederopenProofStatus gInfo@(GInfo {libEnvIORef = ioRefProofStatus,

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder conversionMapsIORef = convRef,

ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder gi_LIB_NAME = ln,

ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder gi_hetcatsOpts = opts

ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder }) file convGraph showLib = do

1f8a7f8343f7df719768d2b1d7e3077ee291a1caChristian Maeder mh <- readVerbose opts ln file

ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder case mh of

404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich Nothing -> fail

404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich $ "Could not read proof status from file '"

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder ++ file ++ "'"

ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder Just h -> do

404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich let libfile = libNameToFile opts ln

ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder m <- anaLib opts { outtypes = [] } libfile

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder case m of

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Nothing -> fail

ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder $ "Could not read original development graph from '"

2e2094a642e3775b0d76b890556407941d3a53b6Christian Maeder ++ libfile ++ "'"

340706b6c0c6e3dbacdd7003e20e9cab7f9aa765Christian Maeder Just (_, libEnv) -> case Map.lookup ln libEnv of

43bb71dfe7ec405f563864d57c1cacdaa8ce9a80Christian Maeder Nothing -> fail

2e2094a642e3775b0d76b890556407941d3a53b6Christian Maeder $ "Could not get original development graph for '"

340706b6c0c6e3dbacdd7003e20e9cab7f9aa765Christian Maeder ++ showDoc ln "'"

fdb2d618144159395f7bf8ce3327b3c112a17dd3Till Mossakowski Just dg -> do

aa6c527682224a4e1434f80eae8bc2ef67fb6ca6Christian Maeder oldEnv <- readIORef ioRefProofStatus

aa6c527682224a4e1434f80eae8bc2ef67fb6ca6Christian Maeder let proofStatus = Map.insert ln

37951dbd8e5f2418a07f072d9bf551d0c3a1eafcChristian Maeder (applyProofHistory h dg) oldEnv

e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder writeIORef ioRefProofStatus proofStatus

ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder gInfo' <- copyGInfo gInfo

9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder (gid, actGraphInfo, convMaps) <-

aa6c527682224a4e1434f80eae8bc2ef67fb6ca6Christian Maeder convGraph (gInfo' {gi_LIB_NAME = ln})

ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder "Proof Status " showLib

c22d75ec3ea1306219d1c09a5b3e8ff04f753ad6Christian Maeder writeIORef convRef convMaps

9c3edf2b283c09d33b2820696886d1ed32fcadc8Christian Maeder redisplay gid actGraphInfo

c22d75ec3ea1306219d1c09a5b3e8ff04f753ad6Christian Maeder return (gid, actGraphInfo, convMaps)

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder

68b77966b2cf7bf2e340bf0fb6b9efc3e6a00467Christian Maeder-- | apply a rule of the development graph calculus

83394c6b6e6de128e71b67c9251ed7a84485d082Christian MaederproofMenu :: GInfo

5bb7eeaca10ea76595229375f907a5a388b7c882Christian Maeder -> (LibEnv -> IO (Res.Result LibEnv))

5bb7eeaca10ea76595229375f907a5a388b7c882Christian Maeder -> IO ()

5bb7eeaca10ea76595229375f907a5a388b7c882Christian MaederproofMenu gInfo@(GInfo { libEnvIORef = ioRefProofStatus

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder , descrIORef = event

5bb7eeaca10ea76595229375f907a5a388b7c882Christian Maeder , conversionMapsIORef = convRef

94d3aa05411444596b44ede4531f05dd7ac20fdfChristian Maeder , graphId = gid

ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder , gi_LIB_NAME = ln

8410667510a76409aca9bb24ff0eda0420088274Christian Maeder , gi_GraphInfo = actGraphInfo

ddc9315cc0b1f5dd3d8f99a77f1c75064db33b48Christian Maeder , gi_hetcatsOpts = hOpts

ddc9315cc0b1f5dd3d8f99a77f1c75064db33b48Christian Maeder , proofGUIMVar = guiMVar

5d522dff4d0fabf57dd476d4c3de15d354a89f62Christian Maeder , visibleNodesIORef = ioRefVisibleNodes

5d522dff4d0fabf57dd476d4c3de15d354a89f62Christian Maeder , globalHist = gHist

5d522dff4d0fabf57dd476d4c3de15d354a89f62Christian Maeder }) proofFun = do

8410667510a76409aca9bb24ff0eda0420088274Christian Maeder filled <- tryPutMVar guiMVar Nothing

8410667510a76409aca9bb24ff0eda0420088274Christian Maeder if not filled

8410667510a76409aca9bb24ff0eda0420088274Christian Maeder then readMVar guiMVar >>=

b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder (maybe (putIfVerbose hOpts 0 "proofMenu: ignored Nothing")

e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus Luettich (\ w -> do

e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus Luettich putIfVerbose hOpts 4 $

e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus Luettich "proofMenu: Ignored Proof command; " ++

e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus Luettich "maybe a proof window is still open?"

3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich HTk.putWinOnTop w))

3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich else do

3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich proofStatus <- readIORef ioRefProofStatus

3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich putIfVerbose hOpts 4 "Proof started via \"Proofs\" menu"

3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich Res.Result ds res <- proofFun proofStatus

3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich putIfVerbose hOpts 4 "Analyzing result of proof"

3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich case res of

3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich Nothing -> mapM_ (putStrLn . show) ds

3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich Just newProofStatus -> do

3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich let newGr = lookupDGraph ln newProofStatus

36f63902db2b3463faa9f59912ad106e2d5aaa24Klaus Luettich history = proofHistory newGr

3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich (guHist, grHist) <- takeMVar gHist

3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich putMVar gHist $ ((calcGlobalHistory proofStatus newProofStatus):guHist

3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich , grHist)

3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich writeIORef ioRefProofStatus newProofStatus

3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich descr <- readIORef event

ac43fa22d2d3f91a17674ac164cba3cf39a17795Klaus Luettich convMaps <- readIORef convRef

ac43fa22d2d3f91a17674ac164cba3cf39a17795Klaus Luettich (newDescr,convMapsAux) <- applyChanges gid ln actGraphInfo descr

8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers ioRefVisibleNodes convMaps history

61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder writeIORef ioRefProofStatus $ Map.insert ln newGr newProofStatus

8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers writeIORef event newDescr

d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder writeIORef convRef convMapsAux

18c1d987ce5818ecf0bfc8af3f43aed2ce86e1eaChristian Maeder hideShowNames gInfo False

61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder mGUIMVar <- tryTakeMVar guiMVar

d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder maybe (fail $ "should be filled with Nothing after "++"proof attempt")

1c9a63e4f7c6879f51fe0f32154a9116f2c126dbChristian Maeder (const $ return ())

6fe9628743562678acf97d6730ebcfee5e9e50c2Christian Maeder mGUIMVar

d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder

d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian MaedercalcGlobalHistory :: LibEnv -> LibEnv -> [LIB_NAME]

61fa0ac06ede811c7aad54ec4c4202346727368eChristian MaedercalcGlobalHistory old new = let

d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder pHist = (\ ln le -> proofHistory $ lookupDGraph ln le)

d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder length' = (\ ln le -> length $ pHist ln le)

fb328c4f646dd3dd78a9391c5cb58450a3dd0aa9Klaus Luettich changes = filter (\ ln -> pHist ln old /= pHist ln new) $ Map.keys old

3b06e23643a9f65390cb8c1caabe83fa7e87a708Till Mossakowski in concatMap (\ ln -> replicate (length' ln new - length' ln old) ln) changes

3b06e23643a9f65390cb8c1caabe83fa7e87a708Till Mossakowski

3b06e23643a9f65390cb8c1caabe83fa7e87a708Till MossakowskinodeErr :: Descr -> IO ()

d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian MaedernodeErr descr = error $ "node with descriptor " ++ show descr

d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder ++ " has no corresponding node in the development graph"

61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder

d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian MaedershowSpec :: Descr -> DGraphAndAGraphNode -> DGraph -> IO ()

d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian MaedershowSpec descr dgAndabstrNodeMap dgraph =

61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder case InjMap.lookupWithB descr dgAndabstrNodeMap of

d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder Nothing -> return ()

d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder Just (_, node) -> do

8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers let sp = dgToSpec dgraph node

d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder sp' = case sp of

d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder Res.Result ds Nothing -> show $ vcat $ map pretty ds

e96a0bf4040fd789339958c01f145c5057d26db6René Wagner Res.Result _ m -> showDoc m ""

d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder createTextDisplay "Show spec" sp' [size(80,25)]

d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder

abf2487c3aece95c371ea89ac64319370dcb6483Klaus Luettich{- | auxiliary method for debugging. shows the number of the given node

abf2487c3aece95c371ea89ac64319370dcb6483Klaus Luettich in the abstraction graph

abf2487c3aece95c371ea89ac64319370dcb6483Klaus Luettich-}

abf2487c3aece95c371ea89ac64319370dcb6483Klaus LuettichgetNumberOfNode :: Descr -> IO()

8b0f493ae42bad8b94918cc0957f1af57096cda4Felix ReckersgetNumberOfNode descr =

e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder let title = "Number of node"

83394c6b6e6de128e71b67c9251ed7a84485d082Christian Maeder-- make the node number consistent, the descritor should be reduced by one

8555737bcc9bf1d0afb6624e4d8668f070bcaba1Christian Maeder in createTextDisplay title (showDoc (descr-1) "") [HTk.size(10,10)]

8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder{- | outputs the signature of a node in a window;

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederused by the node menu defined in initializeGraph -}

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaedergetSignatureOfNode :: Descr -> DGraphAndAGraphNode -> DGraph -> IO()

3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus LuettichgetSignatureOfNode descr dgAndabstrNodeMap dgraph =

a80c28bb8b7a23ccdf7e08d0fe216fc19cc97273Klaus Luettich case InjMap.lookupWithB descr dgAndabstrNodeMap of

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder Just (_, node) ->

a80c28bb8b7a23ccdf7e08d0fe216fc19cc97273Klaus Luettich let dgnode = lab' (contextDG dgraph node)

6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder title = "Signature of "++showName (dgn_name dgnode)

83394c6b6e6de128e71b67c9251ed7a84485d082Christian Maeder in createTextDisplay title (showDoc (dgn_sign dgnode) "")

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder [HTk.size(80,50)]

b9625461755578f3eed04676d42a63fd2caebd0cChristian Maeder Nothing -> nodeErr descr

e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder{- |

d0652648f9879c67a194f8b03baafe2700c68eb4Christian Maeder fetches the theory from a node inside the IO Monad

363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder (added by KL based on code in getTheoryOfNode) -}

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederlookupTheoryOfNode :: IORef LibEnv -> Descr -> DGraphAndAGraphNode ->

b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder DGraph -> IO (Res.Result (Node,G_theory))

3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus LuettichlookupTheoryOfNode proofStatusRef descr dgAndabstrNodeMap _ = do

3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich libEnv <- readIORef proofStatusRef

3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich case (do

83394c6b6e6de128e71b67c9251ed7a84485d082Christian Maeder (ln, node) <-

36f63902db2b3463faa9f59912ad106e2d5aaa24Klaus Luettich maybeToResult nullRange ("Node "++show descr++" not found")

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder $ InjMap.lookupWithB descr dgAndabstrNodeMap

83394c6b6e6de128e71b67c9251ed7a84485d082Christian Maeder gth <- computeTheory libEnv ln node

36f63902db2b3463faa9f59912ad106e2d5aaa24Klaus Luettich return (node, gth)

e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder ) of

c5e3fc166373b0d90f6e36e8aa234396a1dcd879Christian Maeder r -> do

340706b6c0c6e3dbacdd7003e20e9cab7f9aa765Christian Maeder return r

3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder{- | outputs the local axioms of a node in a window;

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian 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) ->

2c619a4dfdc1df27573eba98e81ed1ace906941dChristian Maeder let dgnode = lab' (contextDG dgraph node) in

2c619a4dfdc1df27573eba98e81ed1ace906941dChristian Maeder if isDGRef dgnode then createTextDisplay

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder ("Local Axioms of "++ showName (dgn_name dgnode))

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder "no local axioms (reference node to other library)"

50515239e7e190f4a34ca581dd685d002148fbddChristian Maeder [HTk.size(30,10)]

50515239e7e190f4a34ca581dd685d002148fbddChristian Maeder else displayTheory "Local Axioms" node dgraph $ dgn_theory dgnode

50515239e7e190f4a34ca581dd685d002148fbddChristian Maeder Nothing -> nodeErr descr

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder{- | outputs the theory of a node in a window;

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederused by the node menu defined in initializeGraph-}

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaedergetTheoryOfNode :: GInfo -> Descr -> DGraphAndAGraphNode -> DGraph -> IO ()

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaedergetTheoryOfNode gInfo descr dgAndabstrNodeMap dgraph = do

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder r <- lookupTheoryOfNode (libEnvIORef gInfo) descr dgAndabstrNodeMap dgraph

8b4c68db8b465107cabef8b9cd5b6bc216e1b156Till Mossakowski case r of

8b4c68db8b465107cabef8b9cd5b6bc216e1b156Till Mossakowski Res.Result ds res -> do

8b4c68db8b465107cabef8b9cd5b6bc216e1b156Till Mossakowski showDiags (gi_hetcatsOpts gInfo) ds

bcaf979d9babe6346aa343687aa7d596e2894cccPaolo Torrini case res of

df29370ae8d8b41587957f6bcdcb43a3f1927e47Christian Maeder (Just (n, gth)) ->

bcaf979d9babe6346aa343687aa7d596e2894cccPaolo Torrini GUI.HTkUtils.displayTheoryWithWarning

5ce19352a9cc47d982819cc889a71cd0a61ac171Christian Maeder "Theory"

5ce19352a9cc47d982819cc889a71cd0a61ac171Christian Maeder (showName $ dgn_name $ lab' (contextDG dgraph n))

5ce19352a9cc47d982819cc889a71cd0a61ac171Christian Maeder (addHasInHidingWarning dgraph n)

bcaf979d9babe6346aa343687aa7d596e2894cccPaolo Torrini gth

23ab8855c58adfbd03a0730584b917b24c603901Christian Maeder _ -> return ()

df29370ae8d8b41587957f6bcdcb43a3f1927e47Christian Maeder

23ab8855c58adfbd03a0730584b917b24c603901Christian MaederdisplayTheory :: String -> Node -> DGraph -> G_theory -> IO ()

e50e41135ece589f7202bd4ef8d6b97531c2a56eKlaus LuettichdisplayTheory ext node dgraph gth =

47b0e9f3cb008cb7997f4e3bae26e4d62dcc887aChristian Maeder GUI.HTkUtils.displayTheory ext

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder (showName $ dgn_name $ lab' (contextDG dgraph node))

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder gth

431d34c7007a787331c4e5ec997badb0f8190fc7Christian Maeder

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder{- | translate the theory of a node in a window;

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederused by the node menu defined in initializeGraph-}

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaedertranslateTheoryOfNode :: GInfo -> Descr -> DGraphAndAGraphNode -> DGraph

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder -> IO ()

43b4c41fbb07705c9df321221ab9cb9832460407Christian MaedertranslateTheoryOfNode gInfo@(GInfo {gi_hetcatsOpts = opts})

88318aafc287e92931dceffbb943d58a9310001dChristian Maeder descr dgAndabstrNodeMap dgraph = do

43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder libEnv <- readIORef $ libEnvIORef gInfo

88318aafc287e92931dceffbb943d58a9310001dChristian Maeder case (do

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder (ln, node) <-

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder maybeToResult nullRange ("Node "++show descr++" not found")

43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder $ InjMap.lookupWithB descr dgAndabstrNodeMap

43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder th <- computeTheory libEnv ln node

e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus Luettich return (node,th) ) of

9096f6c6aaded6cd8288656ceccd4c7b3bd0747eChristian Maeder Res.Result [] (Just (node,th)) -> do

9096f6c6aaded6cd8288656ceccd4c7b3bd0747eChristian Maeder Res.Result ds _ <- runResultT(

e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus Luettich do G_theory lid sign _ sens _ <- return th

e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus Luettich -- find all comorphism paths starting from lid

e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus Luettich let paths = findComorphismPaths logicGraph (sublogicOfTh th)

e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus Luettich -- let the user choose one

e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus Luettich sel <- lift $ listBox "Choose a logic translation"

e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus Luettich (map show paths)

e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus Luettich i <- case sel of

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder Just j -> return j

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder _ -> liftR $ fail "no logic translation chosen"

61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder Comorphism cid <- return (paths!!i)

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder -- adjust lid's

e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus Luettich let lidS = sourceLogic cid

363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder lidT = targetLogic cid

c72c1e75a969ff4c336e77481c2a8e42603f13eeChristian Maeder sign' <- coerceSign lid lidS "" sign

fdef3358918491badb0e29e42b5d3b5a01950716Christian Maeder sens' <- coerceThSens lid lidS "" sens

6ff7a91875597d6e4dfaa68c79187d01473e8341Christian Maeder -- translate theory along chosen comorphism

6ff7a91875597d6e4dfaa68c79187d01473e8341Christian Maeder (sign'',sens1) <-

6ff7a91875597d6e4dfaa68c79187d01473e8341Christian Maeder liftR $ wrapMapTheory cid (plainSign sign', toNamedList sens')

88318aafc287e92931dceffbb943d58a9310001dChristian Maeder lift $ GUI.HTkUtils.displayTheoryWithWarning

fdef3358918491badb0e29e42b5d3b5a01950716Christian Maeder "Translated Theory"

d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder (showName $ dgn_name $ lab' (contextDG dgraph node))

88318aafc287e92931dceffbb943d58a9310001dChristian Maeder (addHasInHidingWarning dgraph node)

7767474aba4fa2dc51a6c68017d3bcef3b773001Christian Maeder (G_theory lidT (mkExtSign sign'') 0 (toThSens sens1) 0)

88318aafc287e92931dceffbb943d58a9310001dChristian Maeder )

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder showDiags opts ds

fdb2d618144159395f7bf8ce3327b3c112a17dd3Till Mossakowski return ()

340706b6c0c6e3dbacdd7003e20e9cab7f9aa765Christian Maeder Res.Result ds _ -> showDiags opts ds

88318aafc287e92931dceffbb943d58a9310001dChristian Maeder

bf76f4fcf07abaebea587df8135de8356c26a363Till Mossakowski{- | outputs the sublogic of a node in a window;

88318aafc287e92931dceffbb943d58a9310001dChristian Maederused by the node menu defined in initializeGraph -}

fdb2d618144159395f7bf8ce3327b3c112a17dd3Till MossakowskigetSublogicOfNode :: IORef LibEnv -> Descr -> DGraphAndAGraphNode

e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder -> DGraph -> IO()

6e049108aa87dc46bcff96fae50a4625df1d9648Klaus LuettichgetSublogicOfNode proofStatusRef descr dgAndabstrNodeMap dgraph = do

363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder libEnv <- readIORef proofStatusRef

6e049108aa87dc46bcff96fae50a4625df1d9648Klaus Luettich case InjMap.lookupWithB descr dgAndabstrNodeMap of

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder Just (ln, node) ->

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder let dgnode = lab' (contextDG dgraph node)

f4505a64a089693012a3f5c3b1f12a82cd7a2a5aKlaus Luettich name = if isDGRef dgnode then emptyNodeName

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder else dgn_name dgnode

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder in case computeTheory libEnv ln node of

f4505a64a089693012a3f5c3b1f12a82cd7a2a5aKlaus Luettich Res.Result _ (Just th) ->

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder let logstr = show $ sublogicOfTh th

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder title = "Sublogic of "++showName name

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder in createTextDisplay title logstr [HTk.size(30,10)]

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder Res.Result ds _ ->

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder error $ "Could not compute theory for sublogic computation: "

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder ++ concatMap show ds

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder Nothing -> nodeErr descr

1a6464613c59e35072b90ca296ae402cbe956144Christian Maeder

0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich-- | prints the origin of the node

0be0db405c49906bd7057255069bf6df53395ac9Klaus LuettichshowOriginOfNode :: Descr -> DGraphAndAGraphNode -> DGraph -> IO()

0be0db405c49906bd7057255069bf6df53395ac9Klaus LuettichshowOriginOfNode descr dgAndabstrNodeMap dgraph =

0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich case InjMap.lookupWithB descr dgAndabstrNodeMap of

0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich Just (_, node) ->

0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich let dgnode = lab' (contextDG dgraph node) in

0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich if isDGRef dgnode then error "showOriginOfNode: no DGNode" else

0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich let title = "Origin of node "++ showName (dgn_name dgnode)

0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich in createTextDisplay title

0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich (showDoc (dgn_origin dgnode) "") [HTk.size(30,10)]

0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich Nothing -> nodeErr descr

0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich

2e62113845a35e07cb46db05714627c95450f267Klaus Luettich-- | Show proof status of a node

0be0db405c49906bd7057255069bf6df53395ac9Klaus LuettichshowProofStatusOfNode :: GInfo -> Descr -> DGraphAndAGraphNode -> DGraph

0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich -> IO ()

0be0db405c49906bd7057255069bf6df53395ac9Klaus LuettichshowProofStatusOfNode _ descr dgAndabstrNodeMap dgraph =

0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich case InjMap.lookupWithB descr dgAndabstrNodeMap of

438f9bd974c8e668203e636b0f2bc80c589af043Klaus Luettich Just (_, node) ->

d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder do let dgnode = lab' (contextDG dgraph node)

9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder let stat = showStatusAux dgnode

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder let title = "Proof status of node "++showName (dgn_name dgnode)

88318aafc287e92931dceffbb943d58a9310001dChristian Maeder createTextDisplay title stat [HTk.size(105,55)]

438f9bd974c8e668203e636b0f2bc80c589af043Klaus Luettich Nothing -> nodeErr descr

88318aafc287e92931dceffbb943d58a9310001dChristian Maeder

e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus LuettichshowStatusAux :: DGNodeLab -> String

showStatusAux dgnode =

case dgn_theory dgnode of

G_theory _ _ _ sens _ ->

let goals = OMap.filter (not . isAxiom) sens

(proven,open) = OMap.partition isProvenSenStatus goals

in "Proven proof goals:\n"

++ showDoc proven ""

++ if not $ hasOpenConsStatus True dgnode

then showDoc (dgn_cons_status dgnode)

"is the conservativity status of this node"

else ""

++ "\nOpen proof goals:\n"

++ showDoc open ""

++ if hasOpenConsStatus False dgnode

then showDoc (dgn_cons_status dgnode)

"should be the conservativity status of this node"

else ""

-- | 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 id

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)

if isDGRef dgtar then error "checkconservativityOfEdge: no DGNode" else do

G_theory lid _ _ sens _ <- return $ dgn_theory dgtar

GMorphism cid _ _ morphism2 _ <- return $ dgl_morphism linklab

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

(plainSign 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)]

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}) 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 (_, refNode) = labNode' (contextDG dgraph node)

refLibname = if isDGRef refNode then dgn_libname refNode

else error "showReferencedLibrary"

case Map.lookup refLibname libname2dgMap of

Just _ -> do

gInfo' <- copyGInfo gInfo

(gid,gv,cm) <- convGraph (gInfo'{gi_LIB_NAME = refLibname})

"development graph" showLib

deactivateGraphWindow gid gv

redisplay gid gv

hideNodes gInfo'

layoutImproveAll gid gv

showTemporaryMessage gid gv "Development Graph initialized."

activateGraphWindow gid gv

return (gid,gv,cm)

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)

-- ensures that the to be set node is in the graph.

case InjMap.lookupWithA dgNode (dgAndabstrNode convMaps) of

Just abstrNode -> do

AGV.Result descr err <-

changeNodeType gid abstrNode nodetype grInfo

-- if everything's all right, sets the map with the new node.

-- otherwise the error is shown.

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@(GInfo{libEnvIORef = iorLE}) -> do

writeIORef iorLE newLibEnv

convGraph (gI{ gi_LIB_NAME = ln

, gi_hetcatsOpts = opts})

"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 ()