GraphLogic.hs revision efd5c582300190b8d463545c703902b43d7357f0
93fa7e4374de6e37328e752991a698bf03032c75Christian Maeder
ea9ad77838dce923ced1df2ac09a7f0226363593Christian Maeder{- |
ea9ad77838dce923ced1df2ac09a7f0226363593Christian MaederModule : $Header$
ea9ad77838dce923ced1df2ac09a7f0226363593Christian MaederDescription : Logic for manipulating the graph in the Central GUI
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederCopyright : (c) Jorina Freya Gerken, Till Mossakowski, Uni Bremen 2002-2006
ea9ad77838dce923ced1df2ac09a7f0226363593Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
b4fbc96e05117839ca409f5f20f97b3ac872d1edTill Mossakowski
ea9ad77838dce923ced1df2ac09a7f0226363593Christian MaederMaintainer : till@informatik.uni-bremen.de
ea9ad77838dce923ced1df2ac09a7f0226363593Christian MaederStability : provisional
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederPortability : non-portable (imports Logic)
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder-}
bc67ede91ef5309852f1ba3a5a0d6b429f405e9dChristian Maeder
bc67ede91ef5309852f1ba3a5a0d6b429f405e9dChristian Maedermodule GUI.GraphLogic
ea9ad77838dce923ced1df2ac09a7f0226363593Christian Maeder ( undo
bc67ede91ef5309852f1ba3a5a0d6b429f405e9dChristian Maeder , redo
93fa7e4374de6e37328e752991a698bf03032c75Christian Maeder , reload
93fa7e4374de6e37328e752991a698bf03032c75Christian Maeder , remakeGraph
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder , performProofAction
25a0b76bc87e80c0f697951d9817862755a71d33Christian Maeder , openProofStatus
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder , saveProofStatus
2eb84fc82d3ffa9116bc471fda3742bd9e5a24bbChristian Maeder , nodeErr
2eb84fc82d3ffa9116bc471fda3742bd9e5a24bbChristian Maeder , proofMenu
2eb84fc82d3ffa9116bc471fda3742bd9e5a24bbChristian Maeder , openTranslateGraph
2eb84fc82d3ffa9116bc471fda3742bd9e5a24bbChristian Maeder , showReferencedLibrary
dd836737068504898d4f7843ebd8a3df05f3067dChristian Maeder , showSpec
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder , getSignatureOfNode
95936ba3a6577d40aae065aafac4147f5a308782Christian Maeder , getTheoryOfNode
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder , getLocalAxOfNode
dd836737068504898d4f7843ebd8a3df05f3067dChristian Maeder , translateTheoryOfNode
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder , displaySubsortGraph
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder , displayConceptGraph
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder , lookupTheoryOfNode
eed6203a39f88e398d86431a66d367036a3d17baChristian Maeder , getSublogicOfNode
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder , showOriginOfNode
eed6203a39f88e398d86431a66d367036a3d17baChristian Maeder , showProofStatusOfNode
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder , proveAtNode
71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian Maeder , showJustSubtree
62198789c7cb57cac13399055515921c0fe3483fChristian Maeder , showIDOfEdge
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder , getNumberOfNode
71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian Maeder , showMorphismOfEdge
62198789c7cb57cac13399055515921c0fe3483fChristian Maeder , showOriginOfEdge
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder , checkconservativityOfEdge
71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian Maeder , showProofStatusOfThm
62198789c7cb57cac13399055515921c0fe3483fChristian Maeder , convertNodes
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder , convertEdges
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder , hideNodes
1012fdd997ea1f35eee2ccdd4015199f09f18fe9Christian Maeder , getLibDeps
aeb1d2a7487f480dbab690ec77f51b5a57cb04dfChristian Maeder , hideShowNames
aeb1d2a7487f480dbab690ec77f51b5a57cb04dfChristian Maeder , showNodes
1012fdd997ea1f35eee2ccdd4015199f09f18fe9Christian Maeder , translateGraph
aeb1d2a7487f480dbab690ec77f51b5a57cb04dfChristian Maeder , showLibGraph
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder )
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder where
b502963581a463467939d578b211cb7a173c5428Christian Maeder
906f0b21e2dc78ee4f37f879518be018a0204cd9Christian Maederimport Logic.Logic(conservativityCheck)
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maederimport Logic.Coerce(coerceSign, coerceMorphism)
a255351561838b3743d03c1629d335cfb8b83804Christian Maederimport Logic.Grothendieck
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maederimport Logic.Comorphism
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maederimport Logic.Prover
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maederimport Comorphisms.LogicGraph(logicGraph)
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maederimport Syntax.AS_Library(LIB_NAME, getModTime, getLIB_ID)
eed6203a39f88e398d86431a66d367036a3d17baChristian Maeder
eed6203a39f88e398d86431a66d367036a3d17baChristian Maederimport Static.GTheory
eed6203a39f88e398d86431a66d367036a3d17baChristian Maederimport Static.DevGraph
eed6203a39f88e398d86431a66d367036a3d17baChristian Maederimport Static.DGToSpec(dgToSpec, computeTheory)
eed6203a39f88e398d86431a66d367036a3d17baChristian Maederimport Static.AnalysisLibrary(anaLibExt, anaLib)
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maederimport Static.DGTranslation(libEnv_translation)
eed6203a39f88e398d86431a66d367036a3d17baChristian Maeder
eed6203a39f88e398d86431a66d367036a3d17baChristian Maederimport Proofs.EdgeUtils
eed6203a39f88e398d86431a66d367036a3d17baChristian Maederimport Proofs.InferBasic(basicInferenceNode)
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maederimport Proofs.StatusUtils(lookupHistory, removeContraryChanges)
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowskiimport GUI.Utils(listBox, createTextSaveDisplay)
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maederimport GUI.Taxonomy (displayConceptGraph,displaySubsortGraph)
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maederimport GUI.DGTranslation(getDGLogic)
a255351561838b3743d03c1629d335cfb8b83804Christian Maederimport GUI.GraphTypes
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowskiimport GUI.AbstractGraphView as AGV
a255351561838b3743d03c1629d335cfb8b83804Christian Maederimport qualified GUI.HTkUtils (displayTheory,
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder displayTheoryWithWarning,
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder createInfoDisplayWithTwoButtons)
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowskiimport GraphDisp(deleteArc, deleteNode)
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maederimport TextDisplay(createTextDisplay)
a255351561838b3743d03c1629d335cfb8b83804Christian Maederimport InfoBus(encapsulateWaitTermAct)
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maederimport DialogWin (useHTk)
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowskiimport Messages(errorMess)
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maederimport qualified HTk
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maederimport Configuration(size)
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maederimport Common.Id(nullRange)
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowskiimport Common.DocUtils(showDoc, pretty)
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maederimport Common.Doc(vcat)
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maederimport Common.ResultT(liftR, runResultT)
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maederimport Common.AS_Annotation(isAxiom)
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowskiimport Common.Result as Res
71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian Maederimport qualified Common.OrderedMap as OMap
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maederimport qualified Common.InjMap as InjMap
a255351561838b3743d03c1629d335cfb8b83804Christian Maederimport qualified Common.Lib.Rel as Rel
a255351561838b3743d03c1629d335cfb8b83804Christian Maederimport qualified Common.Lib.Graph as Tree
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowskiimport Driver.Options
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowskiimport Driver.WriteFn(writeShATermFile)
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowskiimport Driver.ReadFn(libNameToFile, readVerbose)
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maederimport System.Directory(getModificationTime)
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski
a255351561838b3743d03c1629d335cfb8b83804Christian Maederimport Data.IORef
a255351561838b3743d03c1629d335cfb8b83804Christian Maederimport Data.Maybe(fromJust)
a255351561838b3743d03c1629d335cfb8b83804Christian Maederimport Data.List(nub,deleteBy,find)
a255351561838b3743d03c1629d335cfb8b83804Christian Maederimport Data.Graph.Inductive.Graph as Graph(Node, LEdge, LNode, lab', labNode')
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maederimport qualified Data.IntMap as IntMap
906f0b21e2dc78ee4f37f879518be018a0204cd9Christian Maederimport qualified Data.Map as Map
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maederimport Control.Monad.Trans(lift)
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maederimport Control.Concurrent.MVar
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder
9963c741a47c42d2dedc6e4589c1b197129a6239Christian MaedernegateChanges :: ([DGRule],[DGChange]) -> ([DGRule],[DGChange])
9963c741a47c42d2dedc6e4589c1b197129a6239Christian MaedernegateChanges (_, dgChanges) = ([], reverse $ map negateChange dgChanges)
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder where
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder negateChange :: DGChange -> DGChange
71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian Maeder negateChange change = case change of
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder InsertNode x -> DeleteNode x
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder DeleteNode x -> InsertNode x
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder InsertEdge x -> DeleteEdge x
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder DeleteEdge x -> InsertEdge x
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder SetNodeLab old (node, new) -> SetNodeLab new (node, old)
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder-- | Undo one step of the History
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maederundo :: GInfo -> IO ()
a255351561838b3743d03c1629d335cfb8b83804Christian Maederundo (GInfo { libEnvIORef = ioRefProofStatus
eed6203a39f88e398d86431a66d367036a3d17baChristian Maeder , globalHist = gHist
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder , graphId = gid
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder , gi_GraphInfo = actGraph
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder }) = do
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder le <- readIORef ioRefProofStatus
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder (guHist, grHist) <- takeMVar gHist
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder case guHist of
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder [] -> do
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder showTemporaryMessage gid actGraph "History is empty ..."
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder putMVar gHist (guHist, grHist)
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder (ln:guHist') -> do
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder showTemporaryMessage gid actGraph $ "Undo last change to " ++ show ln
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder ++ " ..."
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder let
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder dg = lookupDGraph ln le
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder phist = proofHistory dg
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder if phist == [emptyHistory] then putMVar gHist (guHist, grHist)
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder else do
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder let
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder change = negateChanges $ head phist
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder dg' = (applyProofHistory [change] dg)
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder { redoHistory = change:redoHistory dg
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder , proofHistory = tail phist}
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder le' = Map.insert ln dg' le
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder case openlock dg' of
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Just lock -> do
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder writeIORef ioRefProofStatus le'
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder mRemakeF <- tryTakeMVar lock
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder case mRemakeF of
95936ba3a6577d40aae065aafac4147f5a308782Christian Maeder Just remakeF -> do
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder putMVar lock remakeF
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder putMVar gHist (guHist', ln:grHist)
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder remakeF
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Nothing -> putMVar gHist (guHist', ln:grHist)
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder Nothing -> do
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder lock <- newEmptyMVar
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder writeIORef ioRefProofStatus
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder $ Map.insert ln dg'{openlock = Just lock} le'
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder putMVar gHist (guHist', ln:grHist)
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder-- | redo one step of the redoHistory
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maederredo :: GInfo -> IO ()
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maederredo (GInfo { libEnvIORef = ioRefProofStatus
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder , globalHist = gHist
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder , graphId = gid
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder , gi_GraphInfo = actGraph
26d3a8da6b4244d65614b5585927df4948e542a0Christian Maeder }) = do
26d3a8da6b4244d65614b5585927df4948e542a0Christian Maeder le <- readIORef ioRefProofStatus
26d3a8da6b4244d65614b5585927df4948e542a0Christian Maeder (guHist, grHist) <- takeMVar gHist
26d3a8da6b4244d65614b5585927df4948e542a0Christian Maeder case grHist of
26d3a8da6b4244d65614b5585927df4948e542a0Christian Maeder [] -> do
26d3a8da6b4244d65614b5585927df4948e542a0Christian Maeder showTemporaryMessage gid actGraph "History is empty ..."
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder putMVar gHist (guHist, grHist)
3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder (ln:grHist') -> do
dd836737068504898d4f7843ebd8a3df05f3067dChristian Maeder showTemporaryMessage gid actGraph $ "Redo last change to " ++ show ln
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder ++ " ..."
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder let
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder dg = lookupDGraph ln le
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder rhist = redoHistory dg
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder if rhist == [emptyHistory] then putMVar gHist (guHist, grHist)
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder else do
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder let
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder change = negateChanges $ head rhist
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder dg' = (applyProofHistory [change] dg)
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder { redoHistory = tail rhist
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder , proofHistory = change:proofHistory dg}
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder le' = Map.insert ln dg' le
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder case openlock dg' of
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder Just lock -> do
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder writeIORef ioRefProofStatus le'
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder mRemakeF <- tryTakeMVar lock
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder case mRemakeF of
9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder Just remakeF -> do
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder putMVar lock remakeF
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder putMVar gHist (ln:guHist, grHist')
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder remakeF
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder Nothing -> putMVar gHist (ln:guHist, grHist')
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder Nothing -> do
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder lock <- newEmptyMVar
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder writeIORef ioRefProofStatus
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder $ Map.insert ln dg'{openlock = Just lock} le'
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder putMVar gHist (ln:guHist, grHist')
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder-- | reloads the Library of the DevGraph
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maederreload :: GInfo -> IO()
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maederreload gInfo@(GInfo { libEnvIORef = ioRefProofStatus
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder , gi_LIB_NAME = ln
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder , gi_hetcatsOpts = opts
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder }) = do
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder oldle <- readIORef ioRefProofStatus
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder let
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder libdeps = Rel.toList $ Rel.intransKernel $ Rel.transClosure $ Rel.fromList
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder $ getLibDeps oldle
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder ioruplibs <- newIORef ([] :: [LIB_NAME])
bc67ede91ef5309852f1ba3a5a0d6b429f405e9dChristian Maeder writeIORef ioruplibs []
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder reloadLibs ioRefProofStatus opts libdeps ioruplibs ln
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder remakeGraph gInfo
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder-- | Creates a list of all LIB_NAME pairs, which have a dependency
a255351561838b3743d03c1629d335cfb8b83804Christian MaedergetLibDeps :: LibEnv -> [(LIB_NAME, LIB_NAME)]
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian MaedergetLibDeps le =
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder concat $ map (\ ln -> getDep ln le) $ Map.keys le
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder-- | Creates a list of LIB_NAME pairs for the fist argument
a255351561838b3743d03c1629d335cfb8b83804Christian MaedergetDep :: LIB_NAME -> LibEnv -> [(LIB_NAME, LIB_NAME)]
a255351561838b3743d03c1629d335cfb8b83804Christian MaedergetDep ln le =
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder map (\ x -> (ln, x)) $ map (\ (_,x,_) -> dgn_libname x) $ IntMap.elems $
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder IntMap.filter (\ (_,x,_) -> isDGRef x) $ Tree.convertToMap $
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder dgBody $ lookupDGraph ln le
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder-- | Reloads a library
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian MaederreloadLib :: IORef LibEnv -> HetcatsOpts -> IORef [LIB_NAME] -> LIB_NAME
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder -> IO ()
a255351561838b3743d03c1629d335cfb8b83804Christian MaederreloadLib iorle opts ioruplibs ln = do
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder mfile <- existsAnSource opts {intype = GuessIn}
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder $ rmSuffix $ libNameToFile opts ln
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder case mfile of
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Nothing -> do
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder return ()
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Just file -> do
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder le <- readIORef iorle
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder let
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder le' = Map.delete ln le
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder mres <- anaLibExt opts file le'
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder case mres of
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Just (_, newle) -> do
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder uplibs <- readIORef ioruplibs
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder writeIORef ioruplibs $ ln:uplibs
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder writeIORef iorle newle
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder return ()
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Nothing -> do
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder fail $ "Could not read original development graph from '"++ file
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder ++ "'"
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder return ()
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder-- | Reloads libraries if nessesary
a255351561838b3743d03c1629d335cfb8b83804Christian MaederreloadLibs :: IORef LibEnv -> HetcatsOpts -> [(LIB_NAME, LIB_NAME)]
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder -> IORef [LIB_NAME] -> LIB_NAME -> IO Bool
a255351561838b3743d03c1629d335cfb8b83804Christian MaederreloadLibs iorle opts deps ioruplibs ln = do
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski uplibs <- readIORef ioruplibs
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder case elem ln uplibs of
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder True -> return True
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder False -> do
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder let
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder deps' = map (snd) $ filter (\ (ln',_) -> ln == ln') deps
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder res <- mapM (reloadLibs iorle opts deps ioruplibs) deps'
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder let
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder libupdate = foldl (\ u r -> if r then True else u) False res
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder case libupdate of
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder True -> do
reloadLib iorle opts ioruplibs ln
return True
False -> do
le <- readIORef iorle
let
newln:_ = filter (ln ==) $ Map.keys le
mfile <- existsAnSource opts $ rmSuffix $ libNameToFile opts ln
case mfile of
Nothing -> do
return False
Just file -> do
newmt <- getModificationTime file
let
libupdate' = (getModTime $ getLIB_ID newln) < newmt
case libupdate' of
False -> return False
True -> do
reloadLib iorle opts ioruplibs ln
return True
-- | Deletes the old edges and nodes of the Graph and makes new ones
remakeGraph :: GInfo -> IO ()
remakeGraph (GInfo { libEnvIORef = ioRefProofStatus
, conversionMapsIORef = convRef
, graphId = gid
, gi_LIB_NAME = ln
, gi_GraphInfo = actGraphInfo
}) = do
le <- readIORef ioRefProofStatus
(gs,ev_cnt) <- readIORef actGraphInfo
let
dgraph = lookupDGraph ln le
Just (_, g) = find (\ (gid', _) -> gid' == gid) gs
gs' = deleteBy (\ (gid1,_) (gid2,_) -> gid1 == gid2) (gid,g) gs
og = theGraph g
-- reads and delets the old nodes and edges
mapM_ (deleteArc og) $ map (\ (_,_,_,x) -> x) $ Map.elems $ AGV.edges g
mapM_ (deleteNode og) $ map snd $ Map.elems $ AGV.nodes g
-- stores the graph without nodes and edges in the GraphInfo
let
g' = g {theGraph = og, AGV.nodes = Map.empty, AGV.edges = Map.empty}
writeIORef actGraphInfo ((gid,g'):gs',ev_cnt)
-- creates new nodes and edges
newConvMaps <- convertNodes emptyConversionMaps gid actGraphInfo dgraph ln
finalConvMaps <- convertEdges newConvMaps gid actGraphInfo dgraph ln
-- writes the ConversionMap and redisplays the graph
writeIORef convRef finalConvMaps
redisplay gid actGraphInfo
return ()
hideShowNames :: GInfo -> Bool -> IO ()
hideShowNames (GInfo {graphId = gid,
gi_GraphInfo = actGraphInfo,
internalNamesIORef = showInternalNames
}) toggle = do
deactivateGraphWindow gid actGraphInfo
(intrn::InternalNames) <- readIORef showInternalNames
let showThem = if toggle then not $ showNames intrn else showNames intrn
showItrn s = if showThem then s else ""
mapM_ (\(s,upd) -> upd (\_ -> showItrn s)) $ updater intrn
writeIORef showInternalNames $ intrn {showNames = showThem}
redisplay gid actGraphInfo
activateGraphWindow gid actGraphInfo
return ()
showNodes :: GInfo -> IO ()
showNodes gInfo@(GInfo {descrIORef = event,
graphId = gid,
gi_GraphInfo = actGraphInfo
}) = do
deactivateGraphWindow gid actGraphInfo
descr <- readIORef event
AGV.Result _ errorMsg <- checkHasHiddenNodes gid descr actGraphInfo
case errorMsg of
Nothing -> do
showTemporaryMessage gid actGraphInfo "Revealing hidden nodes ..."
showIt gid descr actGraphInfo
hideShowNames gInfo False
return ()
Just _ -> do
showTemporaryMessage gid actGraphInfo "No hidden nodes found ..."
return ()
activateGraphWindow gid actGraphInfo
return ()
hideNodes :: GInfo -> IO ()
hideNodes (GInfo {descrIORef = event,
graphId = gid,
gi_GraphInfo = actGraphInfo
}) = do
deactivateGraphWindow gid actGraphInfo
descr' <- readIORef event
AGV.Result _ errorMsg <- checkHasHiddenNodes gid descr' actGraphInfo
case errorMsg of
Nothing -> do
showTemporaryMessage gid actGraphInfo "Nodes already hidden ..."
return ()
Just _ -> do
showTemporaryMessage gid actGraphInfo "Hiding unnamed nodes..."
AGV.Result descr msg <- hideSetOfNodeTypes gid
[--red nodes are not hidden
--"open_cons__internal",
--"locallyEmpty__open_cons__internal",
--"proven_cons__internal",
"locallyEmpty__proven_cons__internal"]
True actGraphInfo
writeIORef event descr
case msg of
Nothing -> do redisplay gid actGraphInfo
return ()
Just err -> putStrLn err
activateGraphWindow gid actGraphInfo
return ()
translateGraph :: GInfo -> ConvFunc -> LibFunc -> IO ()
translateGraph (GInfo {libEnvIORef = ioRefProofStatus,
gi_LIB_NAME = ln,
gi_hetcatsOpts = opts
}) convGraph showLib = do
le <- readIORef ioRefProofStatus
openTranslateGraph le ln opts (getDGLogic le) convGraph showLib
showLibGraph :: GInfo -> LibFunc -> IO ()
showLibGraph gInfo showLib = do
showLib gInfo
return ()
{- | it tries to perform the given action to the given graph.
If part of the given graph is not hidden, then the action can
be performed directly; otherwise the graph will be shown completely
firstly, and then the action will be performed, and after that the graph
will be hidden again.
-}
performProofAction :: GInfo -> IO () -> IO ()
performProofAction gInfo@(GInfo {descrIORef = event,
graphId = gid,
gi_GraphInfo = actGraphInfo
}) proofAction = do
deactivateGraphWindow gid actGraphInfo
let actionWithMessage = do
showTemporaryMessage gid actGraphInfo
"Applying development graph calculus proof rule..."
proofAction
descr <- readIORef event
AGV.Result _ errorMsg <- checkHasHiddenNodes gid descr actGraphInfo
case errorMsg of
Nothing -> do
showNodes gInfo
actionWithMessage
hideNodes gInfo
Just _ -> actionWithMessage
showTemporaryMessage gid actGraphInfo
"Development graph calculus proof rule finished."
activateGraphWindow gid actGraphInfo
return ()
saveProofStatus :: GInfo -> FilePath -> IO ()
saveProofStatus (GInfo {libEnvIORef = ioRefProofStatus,
gi_LIB_NAME = ln,
gi_hetcatsOpts = opts
}) file = encapsulateWaitTermAct $ do
proofStatus <- readIORef ioRefProofStatus
writeShATermFile file (ln, lookupHistory ln proofStatus)
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, the descritor should be reduced by one
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) ->
let dgnode = lab' (contextDG dgraph node) in
if isDGRef dgnode then createTextDisplay
("Local Axioms of "++ showName (dgn_name dgnode))
"no local axioms (reference node to other library)"
[HTk.size(30,10)]
else displayTheory "Local Axioms" node dgraph $ dgn_theory dgnode
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 = if isDGRef dgnode then emptyNodeName
else dgn_name dgnode
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) ->
let dgnode = lab' (contextDG dgraph node) in
if isDGRef dgnode then error "showOriginOfNode: no DGNode" else
let title = "Origin of node "++ showName (dgn_name dgnode)
in createTextDisplay title
(showDoc (dgn_origin dgnode) "") [HTk.size(30,10)]
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 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 (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 ()