ea9ad77838dce923ced1df2ac09a7f0226363593Christian Maeder

ea9ad77838dce923ced1df2ac09a7f0226363593Christian Maeder{- |

e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiModule : $Header$

e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian MaederDescription : Logic for manipulating the graph in the Central GUI

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuCopyright : (c) Jorina Freya Gerken, Till Mossakowski, Uni Bremen 2002-2006

ea9ad77838dce923ced1df2ac09a7f0226363593Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

3f69b6948966979163bdfe8331c38833d5d90ecdChristian Maeder

ea9ad77838dce923ced1df2ac09a7f0226363593Christian MaederMaintainer : till@informatik.uni-bremen.de

ea9ad77838dce923ced1df2ac09a7f0226363593Christian MaederStability : provisional

f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederPortability : non-portable (imports Logic)

e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowski-}

93fa7e4374de6e37328e752991a698bf03032c75Christian Maeder

93fa7e4374de6e37328e752991a698bf03032c75Christian Maedermodule GUI.GraphLogic

e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maeder ( undo

5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder , redo

5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder , reload

3b31ee94edcb328d2aa02ddcfa8a2e227d4c98edChristian Maeder , remakeGraph

3b5d1e9f95905d6595b3bb01b54499a37a3d82acChristian Maeder , performProofAction

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder , openProofStatus

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder , saveProofStatus

75eb4b8bca5dc18a680471287ebe996d908ae5ccChristian Maeder , nodeErr

75eb4b8bca5dc18a680471287ebe996d908ae5ccChristian Maeder , proofMenu

81ae4270c8508e5e630e50923a2e790e7b1e5997Christian Maeder , openTranslateGraph

75eb4b8bca5dc18a680471287ebe996d908ae5ccChristian Maeder , showReferencedLibrary

5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder , showSpec

64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder , getSignatureOfNode

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder , getTheoryOfNode

ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder , getLocalAxOfNode

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder , translateTheoryOfNode

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder , displaySubsortGraph

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder , displayConceptGraph

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder , lookupTheoryOfNode

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder , getSublogicOfNode

2eb84fc82d3ffa9116bc471fda3742bd9e5a24bbChristian Maeder , showOriginOfNode

2eb84fc82d3ffa9116bc471fda3742bd9e5a24bbChristian Maeder , showProofStatusOfNode

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder , proveAtNode

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder , showJustSubtree

ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder , showIDOfEdge

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder , getNumberOfNode

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder , showMorphismOfEdge

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder , showOriginOfEdge

9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder , checkconservativityOfEdge

e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maeder , showProofStatusOfThm

782d5365e084a40e4f717dafbe00fc41476a7cfeChristian Maeder , convertNodes

782d5365e084a40e4f717dafbe00fc41476a7cfeChristian Maeder , convertEdges

782d5365e084a40e4f717dafbe00fc41476a7cfeChristian Maeder , hideNodes

9c07aad044613547d61ab235665c08adcef03a1cChristian Maeder , getLibDeps

782d5365e084a40e4f717dafbe00fc41476a7cfeChristian Maeder , hideShowNames

782d5365e084a40e4f717dafbe00fc41476a7cfeChristian Maeder , showNodes

5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder , translateGraph

5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder , showLibGraph

e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maeder )

5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder where

e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maeder

782d5365e084a40e4f717dafbe00fc41476a7cfeChristian Maederimport Logic.Logic(conservativityCheck)

782d5365e084a40e4f717dafbe00fc41476a7cfeChristian Maederimport Logic.Coerce(coerceSign, coerceMorphism)

782d5365e084a40e4f717dafbe00fc41476a7cfeChristian Maederimport Logic.Grothendieck

9c07aad044613547d61ab235665c08adcef03a1cChristian Maederimport Logic.Comorphism

782d5365e084a40e4f717dafbe00fc41476a7cfeChristian Maederimport Logic.Prover

782d5365e084a40e4f717dafbe00fc41476a7cfeChristian Maeder

a008ea3d3b5667969f058f75e9919f9b9c26260fChristian Maederimport Comorphisms.LogicGraph(logicGraph)

5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maederimport Syntax.AS_Library(LIB_NAME, getModTime, getLIB_ID)

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maederimport Static.GTheory

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maederimport Static.DevGraph

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maederimport Static.DGToSpec(dgToSpec, computeTheory)

e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maederimport Static.AnalysisLibrary(anaLibExt, anaLib)

5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maederimport Static.DGTranslation(libEnv_translation)

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maederimport Proofs.EdgeUtils

5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maederimport Proofs.InferBasic(basicInferenceNode)

e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maederimport Proofs.StatusUtils(lookupHistory, removeContraryChanges)

5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maederimport GUI.Utils(listBox, createTextSaveDisplay)

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maederimport GUI.Taxonomy (displayConceptGraph,displaySubsortGraph)

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maederimport GUI.DGTranslation(getDGLogic)

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maederimport GUI.GraphTypes

5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maederimport GUI.AbstractGraphView as AGV

e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maederimport qualified GUI.HTkUtils (displayTheory,

5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder displayTheoryWithWarning,

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder createInfoDisplayWithTwoButtons)

5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder

e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maederimport GraphDisp(deleteArc, deleteNode)

5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maederimport TextDisplay(createTextDisplay)

e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maederimport InfoBus(encapsulateWaitTermAct)

e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maederimport DialogWin (useHTk)

5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maederimport Messages(errorMess)

e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maederimport qualified HTk

5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maederimport Configuration(size)

e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maeder

5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maederimport Common.Id(nullRange)

c7f5076658d72ea340d7fd8a648908f961af682dChristian Maederimport Common.DocUtils(showDoc, pretty)

5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maederimport Common.Doc(vcat)

e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maederimport Common.ResultT(liftR, runResultT)

5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maederimport Common.AS_Annotation(isAxiom)

5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maederimport Common.Result as Res

5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maederimport qualified Common.OrderedMap as OMap

e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maederimport qualified Common.InjMap as InjMap

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maederimport qualified Common.Lib.Rel as Rel

5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maederimport qualified Common.Lib.Graph as Tree

e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maeder

5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maederimport Driver.Options

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maederimport Driver.WriteFn(writeShATermFile)

4d4ec273e5cb1f17985c6edcf90a295a8b612cefChristian Maederimport Driver.ReadFn(libNameToFile, readVerbose)

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maederimport System.Directory(getModificationTime)

c7f5076658d72ea340d7fd8a648908f961af682dChristian Maeder

5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maederimport Data.IORef

5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maederimport Data.Maybe(fromJust)

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

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maederimport Data.Graph.Inductive.Graph as Graph(Node, LEdge, LNode, lab', labNode')

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maederimport qualified Data.IntMap as IntMap

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maederimport qualified Data.Map as Map

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maederimport Control.Monad.Trans(lift)

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maederimport Control.Concurrent.MVar

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder-- | Undo one step of the History

5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maederundo :: GInfo -> IO ()

e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maederundo (GInfo { libEnvIORef = ioRefProofStatus

5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder , initLibEnv = initEnv

e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maeder , globalHist = gHist

812ee1f62e0e0e7235f3c05b41a0b173497b54ffChristian Maeder , graphId = gid

812ee1f62e0e0e7235f3c05b41a0b173497b54ffChristian Maeder , gi_GraphInfo = actGraph

5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder }) = do

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder oldEnv <- readIORef ioRefProofStatus

e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maeder (guHist, grHist) <- takeMVar gHist

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder case guHist of

5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder [] -> do

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder showTemporaryMessage gid actGraph "History is empty ..."

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder putMVar gHist (guHist, grHist)

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder (ln:guHist') -> do

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder showTemporaryMessage gid actGraph $ "Undo last change to " ++ show ln

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder ++ " ..."

5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder let

5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder dg = lookupDGraph ln oldEnv

5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder initdg = lookupDGraph ln initEnv

812ee1f62e0e0e7235f3c05b41a0b173497b54ffChristian Maeder phist = proofHistory dg

5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder rhist = redoHistory dg

5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder if phist == [emptyHistory] then putMVar gHist (guHist, grHist)

eed6203a39f88e398d86431a66d367036a3d17baChristian Maeder else do

feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder let

eed6203a39f88e398d86431a66d367036a3d17baChristian Maeder lastchange = head phist

9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder phist' = tail phist

71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian Maeder rhist' = lastchange:rhist

62198789c7cb57cac13399055515921c0fe3483fChristian Maeder dg' = (applyProofHistory (init phist') initdg )

feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder {redoHistory = rhist'}

71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian Maeder newEnv = Map.insert ln dg' oldEnv

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder lock = openlock dg'

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder writeIORef ioRefProofStatus newEnv

9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder mRemakeF <- tryTakeMVar lock

46199904d5e648bc1a25108f60a94078ffb99b30Christian Maeder case mRemakeF of

b1c32a0faa63e0c13687f36a2faae5969ec0a9d5Christian Maeder Just remakeF -> do

1012fdd997ea1f35eee2ccdd4015199f09f18fe9Christian Maeder putMVar lock remakeF

46199904d5e648bc1a25108f60a94078ffb99b30Christian Maeder putMVar gHist (guHist', ln:grHist)

b1c32a0faa63e0c13687f36a2faae5969ec0a9d5Christian Maeder remakeF

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder Nothing -> putMVar gHist (guHist', ln:grHist)

81ae4270c8508e5e630e50923a2e790e7b1e5997Christian Maeder

81ae4270c8508e5e630e50923a2e790e7b1e5997Christian Maeder-- | redo one step of the redoHistory

81ae4270c8508e5e630e50923a2e790e7b1e5997Christian Maederredo :: GInfo -> IO ()

81ae4270c8508e5e630e50923a2e790e7b1e5997Christian Maederredo (GInfo { libEnvIORef = ioRefProofStatus

81ae4270c8508e5e630e50923a2e790e7b1e5997Christian Maeder , initLibEnv = initEnv

81ae4270c8508e5e630e50923a2e790e7b1e5997Christian Maeder , globalHist = gHist

81ae4270c8508e5e630e50923a2e790e7b1e5997Christian Maeder , graphId = gid

81ae4270c8508e5e630e50923a2e790e7b1e5997Christian Maeder , gi_GraphInfo = actGraph

81ae4270c8508e5e630e50923a2e790e7b1e5997Christian Maeder }) = do

81ae4270c8508e5e630e50923a2e790e7b1e5997Christian Maeder oldEnv <- readIORef ioRefProofStatus

46199904d5e648bc1a25108f60a94078ffb99b30Christian Maeder (guHist, grHist) <- takeMVar gHist

9c07aad044613547d61ab235665c08adcef03a1cChristian Maeder case grHist of

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder [] -> do

35c791e6c59ef269ec639360dc94943e264d3ad1Christian Maeder showTemporaryMessage gid actGraph "History is empty ..."

35c791e6c59ef269ec639360dc94943e264d3ad1Christian Maeder putMVar gHist (guHist, grHist)

35c791e6c59ef269ec639360dc94943e264d3ad1Christian Maeder (ln:grHist') -> do

35c791e6c59ef269ec639360dc94943e264d3ad1Christian Maeder showTemporaryMessage gid actGraph $ "Redo last change to " ++ show ln

35c791e6c59ef269ec639360dc94943e264d3ad1Christian Maeder ++ " ..."

35c791e6c59ef269ec639360dc94943e264d3ad1Christian Maeder let

35c791e6c59ef269ec639360dc94943e264d3ad1Christian Maeder dg = lookupDGraph ln oldEnv

35c791e6c59ef269ec639360dc94943e264d3ad1Christian Maeder initdg = lookupDGraph ln initEnv

35c791e6c59ef269ec639360dc94943e264d3ad1Christian Maeder phist = proofHistory dg

35c791e6c59ef269ec639360dc94943e264d3ad1Christian Maeder rhist = redoHistory dg

35c791e6c59ef269ec639360dc94943e264d3ad1Christian Maeder if rhist == [emptyHistory] then putMVar gHist (guHist, grHist)

35c791e6c59ef269ec639360dc94943e264d3ad1Christian Maeder else do

35c791e6c59ef269ec639360dc94943e264d3ad1Christian Maeder let

35c791e6c59ef269ec639360dc94943e264d3ad1Christian Maeder nextchange = head rhist

35c791e6c59ef269ec639360dc94943e264d3ad1Christian Maeder rhist' = tail rhist

35c791e6c59ef269ec639360dc94943e264d3ad1Christian Maeder phist' = nextchange:phist

35c791e6c59ef269ec639360dc94943e264d3ad1Christian Maeder dg' = (applyProofHistory (init phist') initdg)

a3000204685374be86c84d76323d95d86e4735acChristian Maeder {redoHistory = rhist'}

35c791e6c59ef269ec639360dc94943e264d3ad1Christian Maeder newEnv = Map.insert ln dg' oldEnv

35c791e6c59ef269ec639360dc94943e264d3ad1Christian Maeder lock = openlock dg'

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder writeIORef ioRefProofStatus newEnv

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder mRemakeF <- tryTakeMVar lock

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder case mRemakeF of

46199904d5e648bc1a25108f60a94078ffb99b30Christian Maeder Just remakeF -> do

e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maeder putMVar lock remakeF

46199904d5e648bc1a25108f60a94078ffb99b30Christian Maeder putMVar gHist (ln:guHist, grHist')

e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maeder remakeF

e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maeder Nothing -> putMVar gHist (ln:guHist, grHist')

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder

a3000204685374be86c84d76323d95d86e4735acChristian Maeder-- | reloads the Library of the DevGraph

a3000204685374be86c84d76323d95d86e4735acChristian Maederreload :: GInfo -> IO()

a3000204685374be86c84d76323d95d86e4735acChristian Maederreload gInfo@(GInfo { libEnvIORef = ioRefProofStatus

9c07aad044613547d61ab235665c08adcef03a1cChristian Maeder , gi_LIB_NAME = ln

9c07aad044613547d61ab235665c08adcef03a1cChristian Maeder , gi_hetcatsOpts = opts

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder }) = do

9c07aad044613547d61ab235665c08adcef03a1cChristian Maeder oldle <- readIORef ioRefProofStatus

9c07aad044613547d61ab235665c08adcef03a1cChristian Maeder let

9c07aad044613547d61ab235665c08adcef03a1cChristian Maeder libdeps = Rel.toList $ Rel.intransKernel $ Rel.transClosure $ Rel.fromList

a3000204685374be86c84d76323d95d86e4735acChristian Maeder $ getLibDeps oldle

9c07aad044613547d61ab235665c08adcef03a1cChristian Maeder ioruplibs <- newIORef ([] :: [LIB_NAME])

46199904d5e648bc1a25108f60a94078ffb99b30Christian Maeder writeIORef ioruplibs []

46199904d5e648bc1a25108f60a94078ffb99b30Christian Maeder reloadLibs ioRefProofStatus opts libdeps ioruplibs ln

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder remakeGraph gInfo

46199904d5e648bc1a25108f60a94078ffb99b30Christian Maeder

9c07aad044613547d61ab235665c08adcef03a1cChristian Maeder-- | Creates a list of all LIB_NAME pairs, which have a dependency

9c07aad044613547d61ab235665c08adcef03a1cChristian MaedergetLibDeps :: LibEnv -> [(LIB_NAME, LIB_NAME)]

9c07aad044613547d61ab235665c08adcef03a1cChristian MaedergetLibDeps le =

46199904d5e648bc1a25108f60a94078ffb99b30Christian Maeder concat $ map (\ ln -> getDep ln le) $ Map.keys le

e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maeder

9c07aad044613547d61ab235665c08adcef03a1cChristian Maeder-- | Creates a list of LIB_NAME pairs for the fist argument

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian MaedergetDep :: LIB_NAME -> LibEnv -> [(LIB_NAME, LIB_NAME)]

46199904d5e648bc1a25108f60a94078ffb99b30Christian MaedergetDep ln le =

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

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

46199904d5e648bc1a25108f60a94078ffb99b30Christian Maeder dgBody $ lookupDGraph ln le

46199904d5e648bc1a25108f60a94078ffb99b30Christian Maeder

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder-- | Reloads a library

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian MaederreloadLib :: IORef LibEnv -> HetcatsOpts -> IORef [LIB_NAME] -> LIB_NAME

9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder -> IO ()

9963c741a47c42d2dedc6e4589c1b197129a6239Christian MaederreloadLib iorle opts ioruplibs ln = do

42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski mfile <- existsAnSource opts {intype = GuessIn}

4693c24801d551cade06e8ff7b4b9f3a8abe12b4Christian Maeder $ rmSuffix $ libNameToFile opts ln

42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski case mfile of

b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder Nothing -> do

9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder return ()

ca0d4947f7b0fdcbf7eac627659e6cff6d3863baChristian Maeder Just file -> do

74085f08cdbbfd79fe5f9c6a455ed0b0cadcf145Christian Maeder le <- readIORef iorle

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder let

74085f08cdbbfd79fe5f9c6a455ed0b0cadcf145Christian Maeder le' = Map.delete ln le

74085f08cdbbfd79fe5f9c6a455ed0b0cadcf145Christian Maeder mres <- anaLibExt opts file le'

74085f08cdbbfd79fe5f9c6a455ed0b0cadcf145Christian Maeder case mres of

4693c24801d551cade06e8ff7b4b9f3a8abe12b4Christian Maeder Just (_, newle) -> do

e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maeder uplibs <- readIORef ioruplibs

4693c24801d551cade06e8ff7b4b9f3a8abe12b4Christian Maeder writeIORef ioruplibs $ ln:uplibs

a255351561838b3743d03c1629d335cfb8b83804Christian Maeder writeIORef iorle newle

74085f08cdbbfd79fe5f9c6a455ed0b0cadcf145Christian Maeder return ()

74085f08cdbbfd79fe5f9c6a455ed0b0cadcf145Christian Maeder Nothing -> do

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

1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder ++ "'"

64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder return ()

9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder

9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder-- | Reloads libraries if nessesary

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

9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder -> IORef [LIB_NAME] -> LIB_NAME -> IO Bool

9963c741a47c42d2dedc6e4589c1b197129a6239Christian MaederreloadLibs iorle opts deps ioruplibs ln = do

e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maeder uplibs <- readIORef ioruplibs

9c07aad044613547d61ab235665c08adcef03a1cChristian Maeder case elem ln uplibs of

a255351561838b3743d03c1629d335cfb8b83804Christian Maeder True -> return True

ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder False -> do

5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder let

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

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

5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder let

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

5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder case libupdate of

87ce48cde10c6835b292e39b43331a5ed94e9b6eChristian Maeder True -> do

87ce48cde10c6835b292e39b43331a5ed94e9b6eChristian Maeder reloadLib iorle opts ioruplibs ln

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder return True

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder False -> do

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder le <- readIORef iorle

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder let

64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder newln:_ = filter (ln ==) $ Map.keys le

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder mfile <- existsAnSource opts $ rmSuffix $ libNameToFile opts ln

64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder case mfile of

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder Nothing -> do

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder return False

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder Just file -> do

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder newmt <- getModificationTime file

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder let

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

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder case libupdate' of

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder False -> return False

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder True -> do

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder reloadLib iorle opts ioruplibs ln

87ce48cde10c6835b292e39b43331a5ed94e9b6eChristian Maeder return True

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder-- | Deletes the old edges and nodes of the Graph and makes new ones

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian MaederremakeGraph :: GInfo -> IO ()

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian MaederremakeGraph (GInfo { libEnvIORef = ioRefProofStatus

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder , conversionMapsIORef = convRef

d645eac2b9bf2e1a458b25982051276232670f09Christian Maeder , graphId = gid

d645eac2b9bf2e1a458b25982051276232670f09Christian Maeder , gi_LIB_NAME = ln

d645eac2b9bf2e1a458b25982051276232670f09Christian Maeder , gi_GraphInfo = actGraphInfo

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder }) = do

d645eac2b9bf2e1a458b25982051276232670f09Christian Maeder le <- readIORef ioRefProofStatus

d645eac2b9bf2e1a458b25982051276232670f09Christian Maeder (gs,ev_cnt) <- readIORef actGraphInfo

d645eac2b9bf2e1a458b25982051276232670f09Christian Maeder let

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder dgraph = lookupDGraph ln le

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder Just (_, g) = find (\ (gid', _) -> gid' == gid) gs

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

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder og = theGraph g

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder -- reads and delets the old nodes and edges

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

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

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder -- stores the graph without nodes and edges in the GraphInfo

abc9c5b7cae1371cf917b6c881adea0dbba470a2Christian Maeder let

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

64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder writeIORef actGraphInfo ((gid,g'):gs',ev_cnt)

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder -- creates new nodes and edges

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder newConvMaps <- convertNodes emptyConversionMaps gid actGraphInfo dgraph ln

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder finalConvMaps <- convertEdges newConvMaps gid actGraphInfo dgraph ln

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder -- writes the ConversionMap and redisplays the graph

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder writeIORef convRef finalConvMaps

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder redisplay gid actGraphInfo

87ce48cde10c6835b292e39b43331a5ed94e9b6eChristian Maeder return ()

87ce48cde10c6835b292e39b43331a5ed94e9b6eChristian Maeder

87ce48cde10c6835b292e39b43331a5ed94e9b6eChristian MaederhideShowNames :: GInfo -> Bool -> IO ()

87ce48cde10c6835b292e39b43331a5ed94e9b6eChristian MaederhideShowNames (GInfo {graphId = gid,

87ce48cde10c6835b292e39b43331a5ed94e9b6eChristian Maeder gi_GraphInfo = actGraphInfo,

a255351561838b3743d03c1629d335cfb8b83804Christian Maeder internalNamesIORef = showInternalNames

3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder }) toggle = do

e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maeder deactivateGraphWindow gid actGraphInfo

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder (intrn::InternalNames) <- readIORef showInternalNames

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder let showThem = if toggle then not $ showNames intrn else showNames intrn

690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder showItrn s = if showThem then s else ""

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

ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder writeIORef showInternalNames $ intrn {showNames = showThem}

5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder redisplay gid actGraphInfo

5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder activateGraphWindow gid actGraphInfo

5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder return ()

a255351561838b3743d03c1629d335cfb8b83804Christian Maeder

690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian MaedershowNodes :: GInfo -> IO ()

e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian MaedershowNodes gInfo@(GInfo {descrIORef = event,

ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder graphId = gid,

0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder gi_GraphInfo = actGraphInfo

5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder }) = do

74085f08cdbbfd79fe5f9c6a455ed0b0cadcf145Christian Maeder deactivateGraphWindow gid actGraphInfo

dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder descr <- readIORef event

9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder AGV.Result _ errorMsg <- checkHasHiddenNodes gid descr actGraphInfo

ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder case errorMsg of

c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder Nothing -> do

0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder showTemporaryMessage gid actGraphInfo "Revealing hidden nodes ..."

e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maeder showIt gid descr actGraphInfo

ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder hideShowNames gInfo False

5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder return ()

5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder Just _ -> do

5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder showTemporaryMessage gid actGraphInfo "No hidden nodes found ..."

a255351561838b3743d03c1629d335cfb8b83804Christian Maeder return ()

690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder activateGraphWindow gid actGraphInfo

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder return ()

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian MaederhideNodes :: GInfo -> IO ()

9c07aad044613547d61ab235665c08adcef03a1cChristian MaederhideNodes (GInfo {descrIORef = event,

9c07aad044613547d61ab235665c08adcef03a1cChristian Maeder graphId = gid,

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder gi_GraphInfo = actGraphInfo

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder }) = do

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder deactivateGraphWindow gid actGraphInfo

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder descr' <- readIORef event

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

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder case errorMsg of

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder Nothing -> do

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder showTemporaryMessage gid actGraphInfo "Nodes already hidden ..."

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder return ()

e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maeder Just _ -> do

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

0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder AGV.Result descr msg <- hideSetOfNodeTypes gid

b1c32a0faa63e0c13687f36a2faae5969ec0a9d5Christian Maeder [--red nodes are not hidden

64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder --"open_cons__internal",

0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder --"locallyEmpty__open_cons__internal",

64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder --"proven_cons__internal",

64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder "locallyEmpty__proven_cons__internal"]

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder True actGraphInfo

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder writeIORef event descr

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder case msg of

a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Nothing -> do redisplay gid actGraphInfo

64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder return ()

64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder Just err -> putStrLn err

a255351561838b3743d03c1629d335cfb8b83804Christian Maeder activateGraphWindow gid actGraphInfo

64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder return ()

64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder

a255351561838b3743d03c1629d335cfb8b83804Christian MaedertranslateGraph :: GInfo -> ConvFunc -> LibFunc -> IO ()

64c3ee43f3cbacbeffb633103ffe6269f2177485Christian MaedertranslateGraph (GInfo {libEnvIORef = ioRefProofStatus,

64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder gi_LIB_NAME = ln,

a255351561838b3743d03c1629d335cfb8b83804Christian Maeder gi_hetcatsOpts = opts

a255351561838b3743d03c1629d335cfb8b83804Christian Maeder }) convGraph showLib = do

64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder le <- readIORef ioRefProofStatus

64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder openTranslateGraph le ln opts (getDGLogic le) convGraph showLib

a255351561838b3743d03c1629d335cfb8b83804Christian Maeder

a255351561838b3743d03c1629d335cfb8b83804Christian MaedershowLibGraph :: GInfo -> LibFunc -> IO ()

64c3ee43f3cbacbeffb633103ffe6269f2177485Christian MaedershowLibGraph gInfo showLib = do

64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder showLib gInfo

a255351561838b3743d03c1629d335cfb8b83804Christian Maeder return ()

64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder

64c3ee43f3cbacbeffb633103ffe6269f2177485Christian MaederperformProofAction :: GInfo -> IO () -> IO ()

a255351561838b3743d03c1629d335cfb8b83804Christian MaederperformProofAction gInfo@(GInfo {descrIORef = event,

64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder graphId = gid,

64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder gi_GraphInfo = actGraphInfo

a255351561838b3743d03c1629d335cfb8b83804Christian Maeder }) proofAction = do

64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder deactivateGraphWindow gid actGraphInfo

64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder let actionWithMessage = do

a255351561838b3743d03c1629d335cfb8b83804Christian Maeder showTemporaryMessage gid actGraphInfo

a255351561838b3743d03c1629d335cfb8b83804Christian Maeder "Applying development graph calculus proof rule..."

64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder proofAction

64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder descr <- readIORef event

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

a255351561838b3743d03c1629d335cfb8b83804Christian Maeder case errorMsg of

64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder Nothing -> do

64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder showNodes gInfo

a255351561838b3743d03c1629d335cfb8b83804Christian Maeder actionWithMessage

64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder hideNodes gInfo

a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Just _ -> actionWithMessage

7d13f393d82fc9e02d741927fad70d6be96081e2Christian Maeder showTemporaryMessage gid actGraphInfo

64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder "Development graph calculus proof rule finished."

64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder activateGraphWindow gid actGraphInfo

a255351561838b3743d03c1629d335cfb8b83804Christian Maeder return ()

64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder

64c3ee43f3cbacbeffb633103ffe6269f2177485Christian MaedersaveProofStatus :: GInfo -> FilePath -> IO ()

a255351561838b3743d03c1629d335cfb8b83804Christian MaedersaveProofStatus (GInfo {libEnvIORef = ioRefProofStatus,

64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder gi_LIB_NAME = ln,

c8ecc5578d32b222f35b625d4dfe7a3fd8bb4173Christian Maeder gi_hetcatsOpts = opts

64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder }) file = encapsulateWaitTermAct $ do

a255351561838b3743d03c1629d335cfb8b83804Christian Maeder proofStatus <- readIORef ioRefProofStatus

a255351561838b3743d03c1629d335cfb8b83804Christian Maeder writeShATermFile file (ln, lookupHistory ln proofStatus)

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder putIfVerbose opts 2 $ "Wrote " ++ file

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

openProofStatus :: GInfo -> FilePath -> ConvFunc -> LibFunc

-> IO (Descr, GraphInfo, ConversionMaps)

openProofStatus gInfo@(GInfo {libEnvIORef = ioRefProofStatus,

conversionMapsIORef = convRef,

gi_LIB_NAME = ln,

gi_hetcatsOpts = opts

}) file convGraph showLib = do

mh <- readVerbose opts ln file

case mh of

Nothing -> fail

$ "Could not read proof status from file '"

++ file ++ "'"

Just h -> do

let libfile = libNameToFile opts ln

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

case m of

Nothing -> fail

$ "Could not read original development graph from '"

++ libfile ++ "'"

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

Nothing -> fail

$ "Could not get original development graph for '"

++ showDoc ln "'"

Just dg -> do

oldEnv <- readIORef ioRefProofStatus

let proofStatus = Map.insert ln

(applyProofHistory h dg) oldEnv

writeIORef ioRefProofStatus proofStatus

gInfo' <- copyGInfo gInfo

(gid, actGraphInfo, convMaps) <-

convGraph (gInfo' {gi_LIB_NAME = ln})

"Proof Status " showLib

writeIORef convRef convMaps

redisplay gid actGraphInfo

return (gid, actGraphInfo, convMaps)

-- | apply a rule of the development graph calculus

proofMenu :: GInfo

-> (LibEnv -> IO (Res.Result LibEnv))

-> IO ()

proofMenu gInfo@(GInfo { libEnvIORef = ioRefProofStatus

, descrIORef = event

, conversionMapsIORef = convRef

, graphId = gid

, gi_LIB_NAME = ln

, gi_GraphInfo = actGraphInfo

, gi_hetcatsOpts = hOpts

, proofGUIMVar = guiMVar

, visibleNodesIORef = ioRefVisibleNodes

, globalHist = gHist

}) proofFun = do

filled <- tryPutMVar guiMVar Nothing

if not filled

then readMVar guiMVar >>=

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

(\ w -> do

putIfVerbose hOpts 4 $

"proofMenu: Ignored Proof command; " ++

"maybe a proof window is still open?"

HTk.putWinOnTop w))

else do

proofStatus <- readIORef ioRefProofStatus

putIfVerbose hOpts 4 "Proof started via \"Proofs\" menu"

Res.Result ds res <- proofFun proofStatus

putIfVerbose hOpts 4 "Analyzing result of proof"

case res of

Nothing -> mapM_ (putStrLn . show) ds

Just newProofStatus -> do

let oldGr = lookupDGraph ln proofStatus

oldHist = proofHistory oldGr

newGr = lookupDGraph ln newProofStatus

history = proofHistory newGr

(guHist, grHist) <- takeMVar gHist

putMVar gHist (replicate (length history - length oldHist) ln

++guHist, grHist)

writeIORef ioRefProofStatus newProofStatus

descr <- readIORef event

convMaps <- readIORef convRef

(newDescr,convMapsAux)

<- applyChanges gid ln actGraphInfo descr ioRefVisibleNodes

convMaps history

writeIORef ioRefProofStatus $

Map.insert ln newGr newProofStatus

writeIORef event newDescr

writeIORef convRef convMapsAux

hideShowNames gInfo False

mGUIMVar <- tryTakeMVar guiMVar

maybe (fail $ "should be filled with Nothing after "++

"proof attempt")

(const $ return ())

mGUIMVar

nodeErr :: Descr -> IO ()

nodeErr descr = error $ "node with descriptor " ++ show descr

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

showSpec :: Descr -> DGraphAndAGraphNode -> DGraph -> IO ()

showSpec descr dgAndabstrNodeMap dgraph =

case InjMap.lookupWithB descr dgAndabstrNodeMap of

Nothing -> return ()

Just (_, node) -> do

let sp = dgToSpec dgraph node

sp' = case sp of

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

Res.Result _ m -> showDoc m ""

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

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

in the abstraction graph -}

getNumberOfNode :: Descr -> IO()

getNumberOfNode descr =

let title = "Number of node"

-- make the node number consistent

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

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

used by the node menu defined in initializeGraph -}

getSignatureOfNode :: Descr -> DGraphAndAGraphNode -> DGraph -> IO()

getSignatureOfNode descr dgAndabstrNodeMap dgraph =

case InjMap.lookupWithB descr dgAndabstrNodeMap of

Just (_, node) ->

let dgnode = lab' (contextDG dgraph node)

title = "Signature of "++showName (dgn_name dgnode)

in createTextDisplay title (showDoc (dgn_sign dgnode) "")

[HTk.size(80,50)]

Nothing -> nodeErr descr

{- |

fetches the theory from a node inside the IO Monad

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

lookupTheoryOfNode :: IORef LibEnv -> Descr -> DGraphAndAGraphNode ->

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

lookupTheoryOfNode proofStatusRef descr dgAndabstrNodeMap _ = do

libEnv <- readIORef proofStatusRef

case (do

(ln, node) <-

maybeToResult nullRange ("Node "++show descr++" not found")

$ InjMap.lookupWithB descr dgAndabstrNodeMap

gth <- computeTheory libEnv ln node

return (node, gth)

) of

r -> do

return r

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

used by the node menu defined in initializeGraph-}

getLocalAxOfNode :: GInfo -> Descr -> DGraphAndAGraphNode -> DGraph -> IO ()

getLocalAxOfNode _ descr dgAndabstrNodeMap dgraph = do

case InjMap.lookupWithB descr dgAndabstrNodeMap of

Just (_, node) ->

do let dgnode = lab' (contextDG dgraph node)

case dgnode of

DGNode _ gth _ _ _ _ _ _ ->

displayTheory "Local Axioms" node dgraph gth

DGRef name _ _ _ _ _ _ ->

createTextDisplay ("Local Axioms of "++ showName name)

"no local axioms (reference node to other library)"

[HTk.size(30,10)]

Nothing -> nodeErr descr

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

used by the node menu defined in initializeGraph-}

getTheoryOfNode :: GInfo -> Descr -> DGraphAndAGraphNode -> DGraph -> IO ()

getTheoryOfNode gInfo descr dgAndabstrNodeMap dgraph = do

r <- lookupTheoryOfNode (libEnvIORef gInfo) descr dgAndabstrNodeMap dgraph

case r of

Res.Result ds res -> do

showDiags (gi_hetcatsOpts gInfo) ds

case res of

(Just (n, gth)) ->

GUI.HTkUtils.displayTheoryWithWarning

"Theory"

(showName $ dgn_name $ lab' (contextDG dgraph n))

(addHasInHidingWarning dgraph n)

gth

_ -> return ()

displayTheory :: String -> Node -> DGraph -> G_theory -> IO ()

displayTheory ext node dgraph gth =

GUI.HTkUtils.displayTheory ext

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

gth

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

used by the node menu defined in initializeGraph-}

translateTheoryOfNode :: GInfo -> Descr -> DGraphAndAGraphNode -> DGraph

-> IO ()

translateTheoryOfNode gInfo@(GInfo {gi_hetcatsOpts = opts})

descr dgAndabstrNodeMap dgraph = do

libEnv <- readIORef $ libEnvIORef gInfo

case (do

(ln, node) <-

maybeToResult nullRange ("Node "++show descr++" not found")

$ InjMap.lookupWithB descr dgAndabstrNodeMap

th <- computeTheory libEnv ln node

return (node,th) ) of

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

Res.Result ds _ <- runResultT(

do G_theory lid sign _ sens _ <- return th

-- find all comorphism paths starting from lid

let paths = findComorphismPaths logicGraph (sublogicOfTh th)

-- let the user choose one

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

(map show paths)

i <- case sel of

Just j -> return j

_ -> liftR $ fail "no logic translation chosen"

Comorphism cid <- return (paths!!i)

-- adjust lid's

let lidS = sourceLogic cid

lidT = targetLogic cid

sign' <- coerceSign lid lidS "" sign

sens' <- coerceThSens lid lidS "" sens

-- translate theory along chosen comorphism

(sign'',sens1) <-

liftR $ wrapMapTheory cid (sign', toNamedList sens')

lift $ GUI.HTkUtils.displayTheoryWithWarning

"Translated Theory"

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

(addHasInHidingWarning dgraph node)

(G_theory lidT sign'' 0 (toThSens sens1) 0)

)

showDiags opts ds

return ()

Res.Result ds _ -> showDiags opts ds

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

used by the node menu defined in initializeGraph -}

getSublogicOfNode :: IORef LibEnv -> Descr -> DGraphAndAGraphNode

-> DGraph -> IO()

getSublogicOfNode proofStatusRef descr dgAndabstrNodeMap dgraph = do

libEnv <- readIORef proofStatusRef

case InjMap.lookupWithB descr dgAndabstrNodeMap of

Just (ln, node) ->

let dgnode = lab' (contextDG dgraph node)

name = case dgnode of

(DGNode nname _ _ _ _ _ _ _) -> nname

_ -> emptyNodeName

in case computeTheory libEnv ln node of

Res.Result _ (Just th) ->

let logstr = show $ sublogicOfTh th

title = "Sublogic of "++showName name

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

Res.Result ds _ ->

error $ "Could not compute theory for sublogic computation: "

++ concatMap show ds

Nothing -> nodeErr descr

-- | prints the origin of the node

showOriginOfNode :: Descr -> DGraphAndAGraphNode -> DGraph -> IO()

showOriginOfNode descr dgAndabstrNodeMap dgraph =

case InjMap.lookupWithB descr dgAndabstrNodeMap of

Just (_, node) ->

do let dgnode = lab' (contextDG dgraph node)

case dgnode of

DGNode name _ _ _ orig _ _ _ ->

let title = "Origin of node "++showName name

in createTextDisplay title

(showDoc orig "") [HTk.size(30,10)]

DGRef _ _ _ _ _ _ _ -> error "showOriginOfNode: no DGNode"

Nothing -> nodeErr descr

-- | Show proof status of a node

showProofStatusOfNode :: GInfo -> Descr -> DGraphAndAGraphNode -> DGraph

-> IO ()

showProofStatusOfNode _ descr dgAndabstrNodeMap dgraph =

case InjMap.lookupWithB descr dgAndabstrNodeMap of

Just (_, node) ->

do let dgnode = lab' (contextDG dgraph node)

let stat = showStatusAux dgnode

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

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

Nothing -> nodeErr descr

showStatusAux :: 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

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}) 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

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)

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