GraphLogic.hs revision f456529a89bfb620d39e5fd5b0a53b24643db96d
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach{- |
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederModule : $Header$
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettDescription : Logic for manipulating the graph in the Central GUI
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederCopyright : (c) Jorina Freya Gerken, Till Mossakowski, Uni Bremen 2002-2006
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescu
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachMaintainer : till@informatik.uni-bremen.de
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederStability : provisional
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachPortability : non-portable (imports Logic)
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachThis module provides functions for all the menus in the Hets GUI.
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettThese are then assembled to the GUI in "GUI.GraphMenu".
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett
78718c37b1a50086a27e0f031db4cf82bea934aeChristian Maeder-}
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachmodule GUI.GraphLogic
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach ( undo
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach , reload
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach , performProofAction
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder , openProofStatus
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder , saveProofStatus
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder , nodeErr
dfc58f5ec6492d1a9b9babd9cdcdbb15baa6e657Christian Maeder , proofMenu
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach , showReferencedLibrary
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder , getTheoryOfNode
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder , translateTheoryOfNode
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder , displaySubsortGraph
1538a6e8d77301d6de757616ffc69ee61f1482e4Andy Gimblett , displayConceptGraph
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach , lookupTheoryOfNode
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach , showProofStatusOfNode
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder , proveAtNode
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach , showNodeInfo
792df0347edab377785d98c63e2be8e2ce0a8bdeChristian Maeder , showEdgeInfo
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder , checkconservativityOfEdge
0ea916d1e6aea10fd7b84f802fb5148a79d8c20aAndy Gimblett , convert
04ceed96d1528b939f2e592d0656290d81d1c045Andy Gimblett , hideNodes
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett , getLibDeps
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly , hideShowNames
9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder , showNodes
1538a6e8d77301d6de757616ffc69ee61f1482e4Andy Gimblett , translateGraph
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder , showLibGraph
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly , runAndLock
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly , saveUDGraph
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder , focusNode
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder , applyChanges
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder ) where
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder
c4b2418421546a337f83332fe0db04742dcd735dAndy Gimblettimport Logic.Logic(conservativityCheck,map_sen, comp)
bcd914850de931848b86d7728192a149f9c0108bChristian Maederimport Logic.Coerce(coerceSign, coerceMorphism)
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maederimport Logic.Grothendieck
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederimport Logic.Comorphism
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederimport Logic.Prover
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederimport Comorphisms.LogicGraph(logicGraph)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederimport Static.GTheory
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblettimport Static.DevGraph
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederimport Static.PrintDevGraph
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maederimport Static.DGTranslation(libEnv_translation)
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder
a78bb62cd6f0beb2dab862db865357fc9d3c25feChristian Maederimport Proofs.EdgeUtils
a78bb62cd6f0beb2dab862db865357fc9d3c25feChristian Maederimport Proofs.InferBasic(basicInferenceNode)
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maederimport Proofs.StatusUtils(lookupHistory, removeContraryChanges)
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maederimport Proofs.TheoremHideShift
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder
7e7d791d2f643ffd82843b78e424b6f9f68c24eeChristian Maederimport GUI.Utils (listBox, createTextSaveDisplay)
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maederimport GUI.Taxonomy (displayConceptGraph,displaySubsortGraph)
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maederimport GUI.DGTranslation(getDGLogic)
bcd914850de931848b86d7728192a149f9c0108bChristian Maederimport GUI.GraphTypes
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maederimport qualified GUI.GraphAbstraction as GA
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maederimport qualified GUI.HTkUtils (displayTheoryWithWarning,
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder createInfoDisplayWithTwoButtons,
bcd914850de931848b86d7728192a149f9c0108bChristian Maeder createInfoWindow)
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maederimport GraphConfigure
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maederimport TextDisplay(createTextDisplay)
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maederimport InfoBus(encapsulateWaitTermAct)
8db2221917c1bc569614f3481bcdb3b988facaedChristian Maederimport DialogWin (useHTk)
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maederimport Messages(warningMess, errorMess)
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maederimport qualified HTk
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblettimport Configuration(size)
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblettimport FileDialog(newFileDialogStr)
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblettimport Common.DocUtils (showDoc)
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reillyimport Common.AS_Annotation (isAxiom)
fbc0c2baf563fe5b664f0152674a8d3acecca58cAndy Gimblettimport Common.Consistency
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblettimport Common.ExtSign
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblettimport Common.LibName
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblettimport Common.Result as Res
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblettimport qualified Common.OrderedMap as OMap
842ae753ab848a8508c4832ab64296b929167a97Christian Maederimport qualified Common.Lib.Rel as Rel
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian Maeder
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian Maederimport Data.Maybe
90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblett
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblettimport Driver.Options
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederimport Driver.WriteLibDefn(writeShATermFile)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederimport Driver.ReadFn(libNameToFile, readVerbose)
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblettimport Driver.AnaLib(anaLibExt, anaLib)
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maederimport System.Directory(getModificationTime)
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder
842ae753ab848a8508c4832ab64296b929167a97Christian Maederimport Data.IORef
842ae753ab848a8508c4832ab64296b929167a97Christian Maederimport Data.Char(toLower)
842ae753ab848a8508c4832ab64296b929167a97Christian Maederimport Data.List(partition)
842ae753ab848a8508c4832ab64296b929167a97Christian Maederimport Data.Graph.Inductive.Graph (Node, LEdge, LNode)
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maederimport qualified Data.Map as Map
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maederimport Control.Monad(foldM, filterM)
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblettimport Control.Concurrent.MVar
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach-- | Locks the global lock and runs function
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettrunAndLock :: GInfo -> IO () -> IO ()
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian MaederrunAndLock (GInfo { functionLock = lock
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder , gi_GraphInfo = actGraphInfo
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder }) function = do
dfc58f5ec6492d1a9b9babd9cdcdbb15baa6e657Christian Maeder locked <- tryPutMVar lock ()
dfc58f5ec6492d1a9b9babd9cdcdbb15baa6e657Christian Maeder case locked of
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly True -> do
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly GA.deactivateGraphWindow actGraphInfo
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly function
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly takeMVar lock
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly GA.redisplay actGraphInfo
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly GA.layoutImproveAll actGraphInfo
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder GA.activateGraphWindow actGraphInfo
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder False ->
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder GA.showTemporaryMessage actGraphInfo
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett $ "an other function is still working ... please wait ..."
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett-- | negate change
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettnegateChange :: DGChange -> DGChange
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian MaedernegateChange change = case change of
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett InsertNode x -> DeleteNode x
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly DeleteNode x -> InsertNode x
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett InsertEdge x -> DeleteEdge x
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett DeleteEdge x -> InsertEdge x
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett SetNodeLab old (node, new) -> SetNodeLab new (node, old)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly-- | Undo one step of the History
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyundo :: GInfo -> Bool -> IO ()
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederundo gInfo@(GInfo { globalHist = gHist
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly , gi_GraphInfo = actGraph
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder }) isUndo = do
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly (guHist, grHist) <- takeMVar gHist
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly case if isUndo then guHist else grHist of
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly [] -> do
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly GA.showTemporaryMessage actGraph "History is empty..."
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly putMVar gHist (guHist, grHist)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder (lns:gHist') -> do
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder undoDGraphs gInfo isUndo lns
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly putMVar gHist $ if isUndo then (gHist', reverse lns : grHist)
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian Maeder else (reverse lns : guHist, gHist')
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian Maeder
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettundoDGraphs :: GInfo -> Bool -> [LIB_NAME] -> IO ()
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettundoDGraphs _ _ [] = return ()
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettundoDGraphs g u (ln:r) = do
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder undoDGraph g u ln
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder undoDGraphs g u r
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder
0b8146e4f675518993a34eb2255ad7ddd7bf82a4Christian MaederundoDGraph :: GInfo -> Bool -> LIB_NAME -> IO ()
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederundoDGraph gInfo@(GInfo { libEnvIORef = ioRefProofStatus
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly , gi_GraphInfo = actGraph
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly }) isUndo ln = do
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly GA.showTemporaryMessage actGraph $
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly (if isUndo then "Un" else "Re") ++ "do last change to "
4620f04678d4221ed3547f5bcab117d41ffd86f4Christian Maeder ++ show ln ++ "..."
4620f04678d4221ed3547f5bcab117d41ffd86f4Christian Maeder lockGlobal gInfo
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder le <- readIORef ioRefProofStatus
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly let
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly dg = lookupDGraph ln le
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly hist = (proofHistory dg, redoHistory dg)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly swap (a, b) = (b, a)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly (phist, rhist) = (if isUndo then id else swap) hist
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly (cl@(rs, cs), newHist) = case phist of
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly hd : tl -> (hd, (tl, hd : rhist))
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly _ -> error "undoDGraph"
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly (newPHist, newRHist) = (if isUndo then id else swap) newHist
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly change = if isUndo then (reverse rs, reverse $ map negateChange cs)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly else cl
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly dg' = (changesDG dg $ snd change)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly { proofHistory = newPHist
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly , redoHistory = newRHist }
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder writeIORef ioRefProofStatus $ Map.insert ln dg' le
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder case openlock dg' of
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder Nothing -> return ()
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder Just lock -> do
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder mvar <- tryTakeMVar lock
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly case mvar of
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Nothing -> return ()
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Just applyHist -> do
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly applyHist [change]
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly putMVar lock applyHist
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly unlockGlobal gInfo
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly-- | reloads the Library of the DevGraph
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyreload :: GInfo -> IO()
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reillyreload gInfo@(GInfo { libEnvIORef = ioRefProofStatus
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly , gi_LIB_NAME = ln
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett , gi_hetcatsOpts = opts
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder , gi_GraphInfo = actGraphInfo
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder }) = do
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder lockGlobal gInfo
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder oldle <- readIORef ioRefProofStatus
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder let
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder libdeps = Rel.toList $ Rel.intransKernel $ Rel.transClosure $ Rel.fromList
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly $ getLibDeps oldle
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ioruplibs <- newIORef ([] :: [LIB_NAME])
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly writeIORef ioruplibs []
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly reloadLibs ioRefProofStatus opts libdeps ioruplibs ln
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly unlockGlobal gInfo
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly libs <- readIORef ioruplibs
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly case libs of
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly [] -> GA.showTemporaryMessage actGraphInfo "Reload not needed!"
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly _ -> remakeGraph gInfo
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly-- | Creates a list of all LIB_NAME pairs, which have a dependency
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'ReillygetLibDeps :: LibEnv -> [(LIB_NAME, LIB_NAME)]
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaedergetLibDeps le =
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder concat $ map (\ ln -> getDep ln le) $ Map.keys le
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder-- | Creates a list of LIB_NAME pairs for the fist argument
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaedergetDep :: LIB_NAME -> LibEnv -> [(LIB_NAME, LIB_NAME)]
0b8146e4f675518993a34eb2255ad7ddd7bf82a4Christian MaedergetDep ln le = map (\ (_, x) -> (ln, dgn_libname x)) $
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly filter (isDGRef . snd) $ labNodesDG $ lookupDGraph ln le
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly-- | Reloads a library
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederreloadLib :: IORef LibEnv -> HetcatsOpts -> IORef [LIB_NAME] -> LIB_NAME
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder -> IO ()
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederreloadLib iorle opts ioruplibs ln = do
7e7d791d2f643ffd82843b78e424b6f9f68c24eeChristian Maeder mfile <- existsAnSource opts {intype = GuessIn}
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder $ rmSuffix $ libNameToFile opts ln
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder case mfile of
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder Nothing -> return ()
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder Just file -> do
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder le <- readIORef iorle
bcd914850de931848b86d7728192a149f9c0108bChristian Maeder mFunc <- case openlock $ lookupDGraph ln le of
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly Just lock -> tryTakeMVar lock
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett Nothing -> return Nothing
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder let
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly le' = Map.delete ln le
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly mres <- anaLibExt opts file le'
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly case mres of
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder Just (_, newle) -> do
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder uplibs <- readIORef ioruplibs
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder writeIORef ioruplibs $ ln:uplibs
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder case mFunc of
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder Just func -> case openlock $ lookupDGraph ln newle of
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder Just lock -> putMVar lock func
e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett Nothing -> errorMess "Reload: Can't set openlock in DevGraph"
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett Nothing -> return ()
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly writeIORef iorle $ newle
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder Nothing ->
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder errorMess $ "Error when reloading file "
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder ++ show file
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder-- | Reloads libraries if nessesary
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederreloadLibs :: IORef LibEnv -> HetcatsOpts -> [(LIB_NAME, LIB_NAME)]
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett -> IORef [LIB_NAME] -> LIB_NAME -> IO Bool
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettreloadLibs iorle opts deps ioruplibs ln = do
fbc0c2baf563fe5b664f0152674a8d3acecca58cAndy Gimblett uplibs <- readIORef ioruplibs
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder case elem ln uplibs of
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder True -> return True
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder False -> do
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder let
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder deps' = map (snd) $ filter (\ (ln',_) -> ln == ln') deps
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder res <- mapM (reloadLibs iorle opts deps ioruplibs) deps'
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder let
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly libupdate = foldl (\ u r -> if r then True else u) False res
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett case libupdate of
06a77f038c0e1740672274377901d37d0113226dLiam O'Reilly True -> do
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder reloadLib iorle opts ioruplibs ln
06a77f038c0e1740672274377901d37d0113226dLiam O'Reilly return True
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly False -> do
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly le <- readIORef iorle
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett let
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder newln:_ = filter (ln ==) $ Map.keys le
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder mfile <- existsAnSource opts $ rmSuffix $ libNameToFile opts ln
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly case mfile of
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett Nothing -> return False
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Just file -> do
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder newmt <- getModificationTime file
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly let
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett libupdate' = (getModTime $ getLIB_ID newln) < newmt
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder case libupdate' of
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder False -> return False
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly True -> do
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett reloadLib iorle opts ioruplibs ln
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly return True
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly-- | Deletes the old edges and nodes of the Graph and makes new ones
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillyremakeGraph :: GInfo -> IO ()
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy GimblettremakeGraph gInfo@(GInfo { libEnvIORef = ioRefProofStatus
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly , gi_LIB_NAME = ln
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly , gi_GraphInfo = actGraphInfo
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly }) = do
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly le <- readIORef ioRefProofStatus
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett let
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder dgraph = lookupDGraph ln le
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder showNodes gInfo
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder GA.clear actGraphInfo
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder convert actGraphInfo dgraph
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder hideNodes gInfo
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly-- | Toggles to display internal node names
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillyhideShowNames :: GInfo -> Bool -> IO ()
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy GimbletthideShowNames (GInfo { internalNamesIORef = showInternalNames
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder }) toggle = do
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder (intrn::InternalNames) <- readIORef showInternalNames
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder let showThem = if toggle then not $ showNames intrn else showNames intrn
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder showItrn s = if showThem then s else ""
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly mapM_ (\(s,upd) -> upd (\_ -> showItrn s)) $ updater intrn
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly writeIORef showInternalNames $ intrn {showNames = showThem}
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder-- | shows all hidden nodes and edges
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian MaedershowNodes :: GInfo -> IO ()
842ae753ab848a8508c4832ab64296b929167a97Christian MaedershowNodes gInfo@(GInfo { gi_GraphInfo = actGraphInfo
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder }) = do
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly hhn <- GA.hasHiddenNodes actGraphInfo
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly case hhn of
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett True -> do
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder GA.showTemporaryMessage actGraphInfo "Revealing hidden nodes ..."
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder GA.showAll actGraphInfo
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder hideShowNames gInfo False
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder False -> do
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly GA.showTemporaryMessage actGraphInfo "No hidden nodes found ..."
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett-- | hides all unnamed internal nodes that are proven
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian MaederhideNodes :: GInfo -> IO ()
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian MaederhideNodes (GInfo { libEnvIORef = ioRefProofStatus
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder , gi_LIB_NAME = ln
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder , gi_GraphInfo = actGraphInfo
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly }) = do
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly hhn <- GA.hasHiddenNodes actGraphInfo
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett case hhn of
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder True ->
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder GA.showTemporaryMessage actGraphInfo "Nodes already hidden ..."
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder False -> do
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder GA.showTemporaryMessage actGraphInfo "Hiding unnamed nodes..."
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly le <- readIORef ioRefProofStatus
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly let dg = lookupDGraph ln le
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly nodes = selectNodesByType dg [DGNodeType
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett {nonRefType = NonRefType
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder {isProvenCons = True
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly , isInternalSpec = True}
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder , isLocallyEmpty = True}]
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder edges = getCompressedEdges dg nodes
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder GA.hideNodes actGraphInfo nodes edges
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly-- | selects all nodes of a type with outgoing edges
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillyselectNodesByType :: DGraph -> [DGNodeType] -> [Node]
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy GimblettselectNodesByType dg types =
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder filter (\ n -> outDG dg n /= []) $ map fst
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly $ filter (\ (_, n) -> elem (getRealDGNodeType n) types) $ labNodesDG dg
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly-- | compresses a list of types to the highest one
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian MaedercompressTypes :: [DGEdgeType] -> DGEdgeType
5858e6262048894b0e933b547852f04aed009b58Andy GimblettcompressTypes [] = error "compressTypes: wrong usage"
5858e6262048894b0e933b547852f04aed009b58Andy GimblettcompressTypes (t:[]) = t
842ae753ab848a8508c4832ab64296b929167a97Christian MaedercompressTypes (t1:t2:r) = case t1 > t2 of
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder True -> compressTypes (t1:r)
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly False -> compressTypes (t2:r)
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly-- | returns a list of compressed edges
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy GimblettgetCompressedEdges :: DGraph -> [Node] -> [(Node,Node,DGEdgeType)]
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian MaedergetCompressedEdges dg hidden =
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly filterDuplicates $ getShortPaths $ concat
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder $ map (\ e@(_,t,_) -> map (e:) $ getPaths dg t hidden [])
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder inEdges
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder where
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly inEdges = filter (\ (_,t,_) -> elem t hidden)
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett $ concat $ map (outDG dg)
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder $ foldr (\ n i -> if elem n hidden
5a859092c242b0e37183a44c3c79479125b2920aChristian Maeder || elem n i then i else n:i) []
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder $ map (\ (s,_,_) -> s) $ concat $ map (innDG dg) hidden
5a859092c242b0e37183a44c3c79479125b2920aChristian Maeder
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder-- | filter duplicate paths
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'ReillyfilterDuplicates :: [(Node,Node,DGEdgeType)]
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly -> [(Node,Node,DGEdgeType)]
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy GimblettfilterDuplicates [] = []
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian MaederfilterDuplicates ((s,t,et):r) = edge:filterDuplicates others
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder where
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly (same,others) = partition (\ (s',t',_) -> s == s' && t == t') r
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder edge = (s,t,compressTypes $ et:map (\ (_,_,et') -> et') same)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder-- | returns the pahts of a given node through hidden nodes
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaedergetPaths :: DGraph -> Node -> [Node] -> [Node] -> [[LEdge DGLinkLab]]
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaedergetPaths dg node hidden seen' = case elem node hidden of
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly True -> case edges /= [] of
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly True -> concat $ map (\ e@(_,t,_) -> map (e:) $ getPaths dg t hidden seen)
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly edges
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly False -> []
a09bfcbcb0fba5663fca1968aa82daebf2e092c4Andy Gimblett False -> [[]]
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder where
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder seen = node:seen'
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder edges = filter (\ (_,t,_) -> notElem t seen) $ outDG dg node
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder-- | returns source and target node of a path with the compressed type
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian MaedergetShortPaths :: [[LEdge DGLinkLab]]
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder -> [(Node,Node,DGEdgeType)]
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillygetShortPaths [] = []
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillygetShortPaths (p:r) =
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ((s,t,compressTypes $ map (\ (_,_,e) -> getRealDGLinkType e) p))
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder : getShortPaths r
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder where
06a77f038c0e1740672274377901d37d0113226dLiam O'Reilly (s,_,_) = head p
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly (_,t,_) = last p
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly-- | Let the user select a Node to focus
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyfocusNode :: GInfo -> IO ()
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'ReillyfocusNode GInfo { libEnvIORef = ioRefProofStatus
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly , gi_LIB_NAME = ln
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder , gi_GraphInfo = grInfo } = do
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder le <- readIORef ioRefProofStatus
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly idsnodes <- filterM (fmap not . GA.isHiddenNode grInfo . fst)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder $ labNodesDG $ lookupDGraph ln le
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder selection <- listBox "Select a node to focus"
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly $ map (\ (n, l) -> shows n " " ++ getDGNodeName l) idsnodes
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder case selection of
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder Just idx -> GA.focusNode grInfo $ fst $ idsnodes !! idx
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder Nothing -> return ()
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaedertranslateGraph :: GInfo -> ConvFunc -> LibFunc -> IO ()
06a77f038c0e1740672274377901d37d0113226dLiam O'ReillytranslateGraph (GInfo {libEnvIORef = ioRefProofStatus,
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder gi_LIB_NAME = ln,
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder gi_hetcatsOpts = opts
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder }) convGraph showLib = do
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder le <- readIORef ioRefProofStatus
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder openTranslateGraph le ln opts (getDGLogic le) convGraph showLib
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian MaedershowLibGraph :: GInfo -> LibFunc -> IO ()
842ae753ab848a8508c4832ab64296b929167a97Christian MaedershowLibGraph gInfo showLib = do
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett showLib gInfo
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder return ()
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder{- | it tries to perform the given action to the given graph.
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder If part of the given graph is not hidden, then the action can
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder be performed directly; otherwise the graph will be shown completely
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder firstly, and then the action will be performed, and after that the graph
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder will be hidden again.
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder-}
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederperformProofAction :: GInfo -> IO () -> IO ()
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederperformProofAction gInfo@(GInfo { gi_GraphInfo = actGraphInfo
c56c0630e0299eca5dd603cdac49aab4463c0671Liam O'Reilly }) proofAction = do
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder let actionWithMessage = do
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder GA.showTemporaryMessage actGraphInfo
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder "Applying development graph calculus proof rule..."
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder proofAction
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett hhn <- GA.hasHiddenNodes actGraphInfo
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett case hhn of
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett True -> do
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder showNodes gInfo
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder actionWithMessage
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly hideNodes gInfo
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly False -> actionWithMessage
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly GA.showTemporaryMessage actGraphInfo
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly "Development graph calculus proof rule finished."
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'ReillysaveProofStatus :: GInfo -> FilePath -> IO ()
0b8146e4f675518993a34eb2255ad7ddd7bf82a4Christian MaedersaveProofStatus (GInfo { libEnvIORef = ioRefProofStatus
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder , gi_LIB_NAME = ln
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly , gi_hetcatsOpts = opts
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly }) file = encapsulateWaitTermAct $ do
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly proofStatus <- readIORef ioRefProofStatus
dd7da1b5fedc05b92ba023ebd803e6f4a662503bChristian Maeder writeShATermFile file (ln, lookupHistory ln proofStatus)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly putIfVerbose opts 2 $ "Wrote " ++ file
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder-- | implementation of open menu, read in a proof status
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederopenProofStatus :: GInfo -> FilePath -> ConvFunc -> LibFunc
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly -> IO ()
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyopenProofStatus gInfo@(GInfo { libEnvIORef = ioRefProofStatus
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder , gi_LIB_NAME = ln
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly , gi_hetcatsOpts = opts
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder }) file convGraph showLib = do
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder mh <- readVerbose opts ln file
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder case mh of
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Nothing -> errorMess $ "Could not read proof status from file '"
096d1f4ecffdbaa9e8543b712f24a636ba5accffLiam O'Reilly ++ file ++ "'"
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Just h -> do
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly let libfile = libNameToFile opts ln
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder m <- anaLib opts { outtypes = [] } libfile
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder case m of
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder Nothing -> errorMess $ "Could not read original development graph"
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder ++ " from '" ++ libfile ++ "'"
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder Just (_, libEnv) -> case Map.lookup ln libEnv of
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder Nothing -> errorMess $ "Could not get original development"
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder ++ " graph for '" ++ showDoc ln "'"
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder Just dg -> do
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder lockGlobal gInfo
0b8146e4f675518993a34eb2255ad7ddd7bf82a4Christian Maeder oldEnv <- readIORef ioRefProofStatus
0b8146e4f675518993a34eb2255ad7ddd7bf82a4Christian Maeder let proofStatus = Map.insert ln
0b8146e4f675518993a34eb2255ad7ddd7bf82a4Christian Maeder (applyProofHistory h dg) oldEnv
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder writeIORef ioRefProofStatus proofStatus
0b8146e4f675518993a34eb2255ad7ddd7bf82a4Christian Maeder unlockGlobal gInfo
0b8146e4f675518993a34eb2255ad7ddd7bf82a4Christian Maeder gInfo' <- copyGInfo gInfo ln
0b8146e4f675518993a34eb2255ad7ddd7bf82a4Christian Maeder convGraph gInfo' "Proof Status " showLib
0b8146e4f675518993a34eb2255ad7ddd7bf82a4Christian Maeder let actGraphInfo = gi_GraphInfo gInfo
0b8146e4f675518993a34eb2255ad7ddd7bf82a4Christian Maeder GA.deactivateGraphWindow actGraphInfo
0b8146e4f675518993a34eb2255ad7ddd7bf82a4Christian Maeder GA.redisplay actGraphInfo
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder GA.layoutImproveAll actGraphInfo
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder GA.activateGraphWindow actGraphInfo
0b8146e4f675518993a34eb2255ad7ddd7bf82a4Christian Maeder
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder-- | apply a rule of the development graph calculus
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian MaederproofMenu :: GInfo
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder -> (LibEnv -> IO (Res.Result LibEnv))
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder -> IO ()
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian MaederproofMenu gInfo@(GInfo { libEnvIORef = ioRefProofStatus
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder , gi_LIB_NAME = ln
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder , gi_GraphInfo = actGraphInfo
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder , gi_hetcatsOpts = hOpts
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder , proofGUIMVar = guiMVar
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder , globalHist = gHist
0b8146e4f675518993a34eb2255ad7ddd7bf82a4Christian Maeder }) proofFun = do
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder filled <- tryPutMVar guiMVar Nothing
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder if not filled
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder then readMVar guiMVar >>=
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder (maybe (putIfVerbose hOpts 0 "proofMenu: ignored Nothing")
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder (\ w -> do
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett putIfVerbose hOpts 4 $
fbc0c2baf563fe5b664f0152674a8d3acecca58cAndy Gimblett "proofMenu: Ignored Proof command; " ++
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder "maybe a proof window is still open?"
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder HTk.putWinOnTop w))
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder else do
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder lockGlobal gInfo
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder proofStatus <- readIORef ioRefProofStatus
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder putIfVerbose hOpts 4 "Proof started via \"Proofs\" menu"
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly Res.Result ds res <- proofFun proofStatus
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly putIfVerbose hOpts 4 "Analyzing result of proof"
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly case res of
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder Nothing -> do
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly unlockGlobal gInfo
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly printDiags 2 ds
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly Just newProofStatus -> do
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly let newGr = lookupDGraph ln newProofStatus
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly history = proofHistory newGr
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly (guHist, grHist) <- takeMVar gHist
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly doDump hOpts "PrintHistory" $ do
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly putStrLn "History"
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly print $ prettyHistory history
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly putMVar gHist
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly (calcGlobalHistory proofStatus newProofStatus : guHist, grHist)
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly applyChanges actGraphInfo history
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly writeIORef ioRefProofStatus newProofStatus
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly unlockGlobal gInfo
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder hideShowNames gInfo False
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder mGUIMVar <- tryTakeMVar guiMVar
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder maybe (fail $ "should be filled with Nothing after proof attempt")
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder (const $ return ())
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder mGUIMVar
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'ReillycalcGlobalHistory :: LibEnv -> LibEnv -> [LIB_NAME]
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'ReillycalcGlobalHistory old new = let
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly pHist = (\ ln le -> proofHistory $ lookupDGraph ln le)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder length' = (\ ln le -> length $ pHist ln le)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder changes = filter (\ ln -> pHist ln old /= pHist ln new) $ Map.keys old
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly in concatMap (\ ln -> replicate (length' ln new - length' ln old) ln) changes
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'ReillynodeErr :: Int -> IO ()
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'ReillynodeErr descr = error $ "node with descriptor " ++ show descr
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly ++ " has no corresponding node in the development graph"
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaedershowNodeInfo :: Int -> DGraph -> IO ()
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'ReillyshowNodeInfo descr dgraph = do
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly let dgnode = labDG dgraph descr
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly title = (if isDGRef dgnode then ("reference " ++) else
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly if isInternalNode dgnode then ("internal " ++) else id)
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly "node " ++ getDGNodeName dgnode ++ " " ++ show descr
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly createTextDisplay title (title ++ "\n" ++ showDoc dgnode "")
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder [HTk.size(70, 30)]
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder{- |
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder fetches the theory from a node inside the IO Monad
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder (added by KL based on code in getTheoryOfNode) -}
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederlookupTheoryOfNode :: IORef LibEnv -> LIB_NAME -> Int
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder -> IO (Res.Result (LibEnv, Node, G_theory))
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian MaederlookupTheoryOfNode proofStatusRef ln descr = do
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly libEnv <- readIORef proofStatusRef
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly return $ do
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder (libEnv', gth) <- computeTheory True libEnv ln descr
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly return (libEnv', descr, gth)
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly
842ae753ab848a8508c4832ab64296b929167a97Christian MaedershowDiagMess :: HetcatsOpts -> [Diagnosis] -> IO ()
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'ReillyshowDiagMess opts ds = let es = Res.filterDiags (verbose opts) ds in
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly if null es then return () else
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder (if hasErrors es then errorMess else warningMess) $ unlines $ map show es
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder{- | outputs the theory of a node in a window;
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederused by the node menu defined in initializeGraph-}
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'ReillygetTheoryOfNode :: GInfo -> Int -> DGraph -> IO ()
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'ReillygetTheoryOfNode gInfo@(GInfo { gi_LIB_NAME = ln
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly , gi_GraphInfo = actGraphInfo
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly , libEnvIORef = le
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder }) descr dgraph = do
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly r <- lookupTheoryOfNode le ln descr
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly case r of
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly Res.Result ds res -> do
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly showDiagMess (gi_hetcatsOpts gInfo) ds
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder case res of
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder (Just (le', n, gth)) -> do
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder lockGlobal gInfo
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder GUI.HTkUtils.displayTheoryWithWarning
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder "Theory" (getNameOfNode n dgraph)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder (addHasInHidingWarning dgraph n)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder gth
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder let newGr = lookupDGraph ln le'
a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett newHistory = proofHistory newGr
a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett libEnv <- readIORef le
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder let oldHistory = proofHistory $ lookupDGraph ln libEnv
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder history = take (length newHistory - length oldHistory) newHistory
a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett applyChanges actGraphInfo history
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder writeIORef le le'
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder unlockGlobal gInfo
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder _ -> return ()
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder{- | translate the theory of a node in a window;
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblettused by the node menu defined in initializeGraph-}
842ae753ab848a8508c4832ab64296b929167a97Christian MaedertranslateTheoryOfNode :: GInfo -> Int -> DGraph -> IO ()
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaedertranslateTheoryOfNode
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder gInfo@(GInfo {gi_hetcatsOpts = opts, libEnvIORef = le}) node dgraph = do
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder libEnv <- readIORef le
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder let Res.Result ds mEnv = computeTheory False libEnv (gi_LIB_NAME gInfo) node
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder case mEnv of
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Just (_, th@(G_theory lid sign _ sens _)) -> do
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder -- find all comorphism paths starting from lid
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder let paths = findComorphismPaths logicGraph (sublogicOfTh th)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder -- let the user choose one
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder sel <- listBox "Choose a node logic translation" $ map show paths
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder case sel of
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder Nothing -> warningMess "no node logic translation chosen"
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Just i -> do
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Comorphism cid <- return (paths!!i)
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder -- adjust lid's
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder let lidS = sourceLogic cid
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder lidT = targetLogic cid
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder sign' <- coerceSign lid lidS "" sign
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder sens' <- coerceThSens lid lidS "" sens
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder -- translate theory along chosen comorphism
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder let Result es mTh = wrapMapTheory cid
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder (plainSign sign', toNamedList sens')
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder case mTh of
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Nothing -> showDiagMess opts es
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Just (sign'', sens1) -> GUI.HTkUtils.displayTheoryWithWarning
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder "Translated Theory" (getNameOfNode node dgraph)
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder (addHasInHidingWarning dgraph node)
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder (G_theory lidT (mkExtSign sign'') startSigId
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder (toThSens sens1) startThId)
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Nothing -> showDiagMess opts ds
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder-- | Show proof status of a node
842ae753ab848a8508c4832ab64296b929167a97Christian MaedershowProofStatusOfNode :: GInfo -> Int -> DGraph -> IO ()
842ae753ab848a8508c4832ab64296b929167a97Christian MaedershowProofStatusOfNode _ descr dgraph = do
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder let dgnode = labDG dgraph descr
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder stat = showStatusAux dgnode
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder title = "Proof status of node "++showName (dgn_name dgnode)
a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett createTextDisplay title stat [HTk.size(105,55)]
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaedershowStatusAux :: DGNodeLab -> String
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaedershowStatusAux dgnode =
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder case dgn_theory dgnode of
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder G_theory _ _ _ sens _ ->
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder let goals = OMap.filter (not . isAxiom) sens
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder (proven,open) = OMap.partition isProvenSenStatus goals
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder consGoal = "\nconservativity of this node"
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder in "Proven proof goals:\n"
9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett ++ showDoc proven ""
9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett ++ if not $ hasOpenConsStatus True dgnode
a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett then consGoal
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder else ""
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder ++ "\nOpen proof goals:\n"
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder ++ showDoc open ""
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder ++ if hasOpenConsStatus False dgnode
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder then consGoal
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder else ""
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder-- | start local theorem proving or consistency checking at a node
842ae753ab848a8508c4832ab64296b929167a97Christian MaederproveAtNode :: Bool -> GInfo -> Int -> DGraph -> IO ()
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederproveAtNode checkCons gInfo@(GInfo { libEnvIORef = ioRefProofStatus
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder , gi_LIB_NAME = ln
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder , commandHist = ch }) descr dgraph = do
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder let dgn = labDG dgraph descr
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder libNode = (ln,descr)
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder (dgraph',dgn') <- case hasLock dgn of
f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett True -> return (dgraph, dgn)
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett False -> do
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett lockGlobal gInfo
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder le <- readIORef ioRefProofStatus
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder (dgraph',dgn') <- initLocking (lookupDGraph ln le) (descr, dgn)
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly writeIORef ioRefProofStatus $ Map.insert ln dgraph' le
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly unlockGlobal gInfo
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly return (dgraph',dgn')
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder locked <- tryLockLocal dgn'
bba1e274cf727c39b4f1dd8970539a2bb967f20fLiam O'Reilly case locked of
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly False -> do
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly createTextDisplay "Error" "Proofwindow already open" [HTk.size(30,10)]
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly True -> do
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder let action = do
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder le <- readIORef ioRefProofStatus
bba1e274cf727c39b4f1dd8970539a2bb967f20fLiam O'Reilly guiMVar <- newMVar Nothing
bba1e274cf727c39b4f1dd8970539a2bb967f20fLiam O'Reilly res <- basicInferenceNode checkCons logicGraph libNode ln
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly guiMVar le ch
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly runProveAtNode gInfo (descr, dgn') res
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly case checkCons || not (hasIncomingHidingEdge dgraph' $ snd libNode) of
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder True -> action
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder False -> GUI.HTkUtils.createInfoDisplayWithTwoButtons "Warning"
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly "This node has incoming hiding links!!!" "Prove anyway"
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly action
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder unlockLocal dgn'
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'ReillyrunProveAtNode :: GInfo -> LNode DGNodeLab
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly -> Res.Result (LibEnv, Res.Result G_theory) -> IO ()
842ae753ab848a8508c4832ab64296b929167a97Christian MaederrunProveAtNode gInfo (v, dgnode) res = case maybeResult res of
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Just (le, tres) -> do
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly case maybeResult tres of
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly Just gth -> createTextSaveDisplay
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly ("Model for " ++ getDGNodeName dgnode ++ " node: " ++ show v)
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly "model.log" $ showDoc gth ""
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder Nothing -> case diags tres of
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder [] -> return ()
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder ds ->
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly createTextDisplay "Error" (showRelDiags 2 ds) [HTk.size(50,10)]
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett proofMenu gInfo $ mergeDGNodeLab gInfo
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder (v, labDG (lookupDGraph (gi_LIB_NAME gInfo) le) v)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder Nothing -> return ()
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaedermergeDGNodeLab :: GInfo -> LNode DGNodeLab -> LibEnv -> IO (Res.Result LibEnv)
842ae753ab848a8508c4832ab64296b929167a97Christian MaedermergeDGNodeLab (GInfo{gi_LIB_NAME = ln}) (v, new_dgn) le = do
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett let dg = lookupDGraph ln le
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett old_dgn = labDG dg v
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder return $ do
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder theory <- joinG_sentences (dgn_theory old_dgn) $ dgn_theory new_dgn
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett let new_dgn' = old_dgn { dgn_theory = theory }
5a859092c242b0e37183a44c3c79479125b2920aChristian Maeder (dg', _) = labelNodeDG (v, new_dgn') dg
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder dg'' = addToProofHistoryDG ([], [SetNodeLab old_dgn (v, new_dgn')]) dg'
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett return $ Map.insert ln dg'' le
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder-- | print the id, origin, type, proof-status and morphism of the edge
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaedershowEdgeInfo :: Int -> Maybe (LEdge DGLinkLab) -> IO ()
842ae753ab848a8508c4832ab64296b929167a97Christian MaedershowEdgeInfo descr me = case me of
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett Just e@(_, _, l) -> let estr = showLEdge e in
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett createTextDisplay ("Info of " ++ estr)
e7ddd5495421698701a2bbc57a5b3390a11d12caChristian Maeder (estr ++ "\n" ++ showDoc l "") [HTk.size(70,30)]
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Nothing -> createTextDisplay "Error"
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett ("edge " ++ show descr ++ " has no corresponding edge"
e7ddd5495421698701a2bbc57a5b3390a11d12caChristian Maeder ++ "in the development graph") [HTk.size(50,10)]
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett-- | check conservativity of the edge
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaedercheckconservativityOfEdge :: Int -> GInfo -> Maybe (LEdge DGLinkLab) -> IO ()
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaedercheckconservativityOfEdge _ gInfo@(GInfo{gi_LIB_NAME = ln,
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder gi_GraphInfo = actGraphInfo,
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder libEnvIORef = le})
f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett (Just (source,target,linklab)) = do
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder lockGlobal gInfo
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder libEnv <- readIORef $ libEnvIORef gInfo
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder let libEnv' = case convertToNf ln libEnv target of
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder Result _ (Just lE) -> lE
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder _ -> error "checkconservativityOfEdge: convertToNf"
dd7da1b5fedc05b92ba023ebd803e6f4a662503bChristian Maeder let (_, thTar) =
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder case computeTheory True libEnv' ln target of
f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett Res.Result _ (Just th1) -> th1
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett _ -> error "checkconservativityOfEdge: computeTheory"
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett G_theory lid _sign _ sensTar _ <- return thTar
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder GMorphism cid _ _ morphism2 _ <- return $ dgl_morphism linklab
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder Just (GMorphism cid' _ _ morphism3 _) <- return $
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder dgn_sigma $ labDG (lookupDGraph ln libEnv') target
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder morphism2' <- coerceMorphism (targetLogic cid) lid
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder "checkconservativityOfEdge2" morphism2
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder morphism3' <- coerceMorphism (targetLogic cid') lid
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett "checkconservativityOfEdge3" morphism3
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett let compMor = case comp morphism2' morphism3' of
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett Res.Result _ (Just phi) -> phi
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder _ -> error "checkconservativtiyOfEdge: comp"
c909c215242232fe78ce335e677e6f22264a0ee9Christian Maeder let (_le', thSrc) =
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett case computeTheory False libEnv' (gi_LIB_NAME gInfo) source of
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett Res.Result _ (Just th1) -> th1
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder _ -> error "checkconservativityOfEdge: computeTheory"
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder G_theory lid1 sign1 _ sensSrc1 _ <- return thSrc
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder sign2 <- coerceSign lid1 lid "checkconservativityOfEdge.coerceSign" sign1
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder sensSrc2 <- coerceThSens lid1 lid "checkconservativityOfEdge1" sensSrc1
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder let transSensSrc = propagateErrors
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder $ mapThSensValueM (map_sen lid compMor) sensSrc2
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder if (length $ conservativityCheck lid) < 1
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder then
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder do
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett GUI.HTkUtils.createInfoWindow "Result of conservativity check"
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett "No conservativity checkers available"
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder let newGr = lookupDGraph ln libEnv'
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder newHistory = proofHistory newGr
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder oldHistory = proofHistory $ lookupDGraph ln libEnv
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder history = take (length newHistory - length oldHistory) newHistory
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder applyChanges actGraphInfo history
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder writeIORef le libEnv'
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder unlockGlobal gInfo
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder else
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder do
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder checkerR <- conservativityChoser $ conservativityCheck lid
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder if Res.hasErrors $ Res.diags checkerR
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder then
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder do
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett GUI.HTkUtils.createInfoWindow "Result of conservativity check"
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder "No conservativity checker chosen"
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder let newGr = lookupDGraph ln libEnv'
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett newHistory = proofHistory newGr
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder oldHistory = proofHistory $ lookupDGraph ln libEnv
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder history = take (length newHistory - length oldHistory) newHistory
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder applyChanges actGraphInfo history
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder writeIORef le libEnv'
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder unlockGlobal gInfo
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder else
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly do
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett let chCons = checkConservativity $
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett fromJust $ Res.maybeResult $ checkerR
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett let Res.Result ds res =
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder chCons
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett (plainSign sign2, toNamedList sensSrc2)
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett compMor $ toNamedList
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett (sensTar `OMap.difference` transSensSrc)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder showObls [] = ""
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder showObls obls = ", provided that the following proof obligations "
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder ++ "can be discharged:\n"
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder ++ concatMap (flip showDoc "\n") obls
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder showRes = case res of
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder Just (Just (cst, obls)) -> "The link is "
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett ++ showConsistencyStatus cst ++ showObls obls
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder _ -> "Could not determine whether link is conservative"
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder myDiags = showRelDiags 2 ds
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder createTextDisplay "Result of conservativity check"
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder (showRes ++ "\n" ++ myDiags) [HTk.size(50,50)]
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder let newGr = lookupDGraph ln libEnv'
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder newHistory = proofHistory newGr
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder oldHistory = proofHistory $ lookupDGraph ln libEnv
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder history = take (length newHistory - length oldHistory) newHistory
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder applyChanges actGraphInfo history
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder writeIORef le libEnv'
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder unlockGlobal gInfo
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaedercheckconservativityOfEdge descr _ Nothing =
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder createTextDisplay "Error"
("edge " ++ show descr ++ " has no corresponding edge "
++ "in the development graph") [HTk.size(30,10)]
-- | Graphical choser for conservativity checkers
conservativityChoser :: [ConservativityChecker sign sentence morphism]
-> IO
(Res.Result (ConservativityChecker
sign sentence morphism))
conservativityChoser checkers =
case length $ checkers of
0 -> return $ fail "No conservativity checkers available"
_ ->
do
chosenOne <- listBox "Pick a conservativity checker"
$ map checker_id checkers
case chosenOne of
Nothing -> return $ fail "No conservativity checker chosen"
Just 1 -> return $ return $ head $ checkers
Just i -> return $ return $ (checkers !! i)
-- | converts a DGraph
convert :: GA.GraphInfo -> DGraph -> IO ()
convert ginfo dgraph = do
convertNodes ginfo dgraph
convertEdges ginfo dgraph
{- | 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 :: GA.GraphInfo -> DGraph -> IO ()
convertNodes ginfo = mapM_ (convertNodesAux ginfo) .labNodesDG
{- | 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 :: GA.GraphInfo -> LNode DGNodeLab -> IO ()
convertNodesAux ginfo (node, dgnode) =
GA.addNode ginfo node (getRealDGNodeType dgnode) $ getDGNodeName dgnode
{- | converts the edges of the development graph
works the same way as convertNods does-}
convertEdges :: GA.GraphInfo -> DGraph -> IO ()
convertEdges ginfo = mapM_ (convertEdgesAux ginfo) . labEdgesDG
-- | auxiliary function for convertEges
convertEdgesAux :: GA.GraphInfo -> LEdge DGLinkLab -> IO ()
convertEdgesAux ginfo e@(src, tar, lbl) =
GA.addEdge ginfo (dgl_id lbl) (getRealDGLinkType lbl) src tar "" $ Just e
-- | show library referened by a DGRef node (=node drawn as a box)
showReferencedLibrary :: Int -> GInfo -> ConvFunc -> LibFunc -> IO ()
showReferencedLibrary descr gInfo@(GInfo { libEnvIORef = ioRefProofStatus
, gi_LIB_NAME = ln })
convGraph showLib = do
le <- readIORef ioRefProofStatus
let refNode = labDG (lookupDGraph ln le) descr
refLibname = if isDGRef refNode then dgn_libname refNode
else error "showReferencedLibrary"
case Map.lookup refLibname le of
Just _ -> do
gInfo' <- copyGInfo gInfo refLibname
convGraph gInfo' "development graph" showLib
let gv = gi_GraphInfo gInfo'
GA.deactivateGraphWindow gv
hideNodes gInfo'
GA.redisplay gv
GA.layoutImproveAll gv
GA.showTemporaryMessage gv "Development Graph initialized."
GA.activateGraphWindow gv
return ()
Nothing -> error $ "The referenced library (" ++ show refLibname
++ ") is unknown"
-- | apply the changes of first history item (computed by proof rules,
-- see folder Proofs) to the displayed development graph
applyChanges :: GA.GraphInfo -> ProofHistory -> IO ()
applyChanges _ [] = return ()
applyChanges ginfo ((_, hElem) : _) = mapM_ (applyChangesAux ginfo)
$ removeContraryChanges hElem
-- | auxiliary function for applyChanges
applyChangesAux :: GA.GraphInfo -> DGChange -> IO ()
applyChangesAux ginfo change =
case change of
SetNodeLab _ (node, newLab) ->
GA.changeNodeType ginfo node $ getRealDGNodeType newLab
InsertNode (node, nodelab) ->
GA.addNode ginfo node (getRealDGNodeType nodelab) $ getDGNodeName nodelab
DeleteNode (node, _) ->
GA.delNode ginfo node
InsertEdge e@(src, tgt, lbl) ->
GA.addEdge ginfo (dgl_id lbl) (getRealDGLinkType lbl) src tgt "" $ Just e
DeleteEdge (_, _, lbl) ->
GA.delEdge ginfo $ dgl_id lbl
-- | 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.
let myErrMess = showDiagMess opts in
if hasErrors diagsSl then myErrMess diagsSl else case mSublogic of
Nothing -> errorMess "the maximal sublogic is not found."
Just sublogic -> do
let paths = findComorphismPaths logicGraph sublogic
if null paths then
errorMess "This graph has no comorphism to translation."
else do
-- the user choose one
sel <- listBox "Choose a logic translation"
$ map show paths
case sel of
Nothing -> warningMess "no logic translation chosen"
Just j -> do
-- graph translation.
let Res.Result diagsTrans mLEnv =
libEnv_translation libEnv $ paths !! j
case mLEnv of
Just newLibEnv -> do
showDiagMess opts $ diagsSl ++ diagsTrans
dg_showGraphAux
(\gI@(GInfo{libEnvIORef = iorLE}) -> do
writeIORef iorLE newLibEnv
convGraph (gI{ gi_LIB_NAME = ln
, gi_hetcatsOpts = opts})
"translation Graph" showLib)
Nothing -> myErrMess $ diagsSl ++ diagsTrans
dg_showGraphAux :: (GInfo -> IO ()) -> IO ()
dg_showGraphAux convFct = do
useHTk -- All messages are displayed in TK dialog windows
-- from this point on
gInfo <- emptyGInfo
convFct gInfo
let actGraphInfo = gi_GraphInfo gInfo
GA.deactivateGraphWindow actGraphInfo
GA.redisplay actGraphInfo
GA.layoutImproveAll actGraphInfo
GA.activateGraphWindow actGraphInfo
-- DaVinciGraph to String
-- Functions to convert a DaVinciGraph to a String to store as a .udg file
-- | saves the uDrawGraph graph to a file
saveUDGraph :: GInfo -> Map.Map DGNodeType (Shape value, String)
-> Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String) -> IO ()
saveUDGraph gInfo@(GInfo { gi_GraphInfo = graphInfo
, gi_LIB_NAME = ln
, gi_hetcatsOpts = opts
}) nodemap linkmap = do
evnt <- newFileDialogStr "Save as..."
$ (rmSuffix $ libNameToFile opts ln) ++ ".udg"
maybeFilePath <- HTk.sync evnt
case maybeFilePath of
Just filepath -> do
GA.showTemporaryMessage graphInfo "Converting graph..."
nstring <- nodes2String gInfo nodemap linkmap
writeFile filepath nstring
GA.showTemporaryMessage graphInfo $ "Graph stored to " ++ filepath ++ "!"
Nothing -> GA.showTemporaryMessage graphInfo $ "Aborted!"
-- | Converts the nodes of the graph to String representation
nodes2String :: GInfo -> Map.Map DGNodeType (Shape value, String)
-> Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String)
-> IO String
nodes2String gInfo@(GInfo { gi_GraphInfo = graphInfo
, gi_LIB_NAME = ln
, libEnvIORef = ioRefProofStatus
}) nodemap linkmap = do
le <- readIORef ioRefProofStatus
nodes <- filterM (\(n,_) -> do b <- GA.isHiddenNode graphInfo n
return $ not b)
$ labNodesDG $ lookupDGraph ln le
nstring <- foldM (\s node -> do
s' <- (node2String gInfo nodemap linkmap node)
return $ s ++ (if s /= "" then ",\n " else "") ++ s')
"" nodes
return $ "[" ++ nstring ++ "]"
-- | Converts a node to String representation
node2String :: GInfo -> Map.Map DGNodeType (Shape value, String)
-> Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String)
-> LNode DGNodeLab -> IO String
node2String gInfo nodemap linkmap (nid, dgnode) = do
label <- getNodeLabel gInfo dgnode
let ntype = getRealDGNodeType dgnode
(shape, color) <- case Map.lookup ntype nodemap of
Nothing -> error $ "SaveGraph: can't lookup nodetype: " ++ show ntype
Just (s, c) -> return (s, c)
let
object = "a(\"OBJECT\",\"" ++ label ++ "\"),"
color' = "a(\"COLOR\",\"" ++ color ++ "\"),"
shape' = "a(\"_GO\",\"" ++ (map toLower $ show shape) ++ "\")"
links <- links2String gInfo linkmap nid
return $ "l(\"" ++ (show nid) ++ "\",n(\"" ++ show ntype ++ "\","
++ "[" ++ object ++ color' ++ shape' ++ "],"
++ "\n [" ++ links ++ "]))"
-- | Converts all links of a node to String representation
links2String :: GInfo -> Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String)
-> Int -> IO String
links2String (GInfo { gi_GraphInfo = graphInfo
, gi_LIB_NAME = ln
, libEnvIORef = ioRefProofStatus
}) linkmap nodeid = do
le <- readIORef ioRefProofStatus
edges <- filterM (\(src,_,edge) -> do
let eid = dgl_id edge
b <- GA.isHiddenEdge graphInfo eid
return $ (not b) && src == nodeid)
$ labEdgesDG $ lookupDGraph ln le
foldM (\s edge -> do
s' <- link2String linkmap edge
return $ s ++ (if s /= "" then ",\n " else "") ++ s') "" edges
-- | Converts a link to String representation
link2String :: Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String)
-> LEdge DGLinkLab -> IO String
link2String linkmap (nodeid1, nodeid2, edge) = do
let (EdgeId linkid) = dgl_id edge
ltype = getRealDGLinkType edge
(line, color) <- case Map.lookup ltype linkmap of
Nothing -> error $ "SaveGraph: can't lookup linktype: " ++ show ltype
Just (l, c) -> return (l, c)
let
name = "\"" ++ (show linkid) ++ ":" ++ (show nodeid1) ++ "->"
++ (show nodeid2) ++ "\""
color' = "a(\"EDGECOLOR\",\"" ++ color ++ "\"),"
line' = "a(\"EDGEPATTERN\",\"" ++ (map toLower $ show line) ++ "\")"
return $ "l(" ++ name ++ ",e(\"" ++ show ltype ++ "\","
++ "[" ++ color' ++ line' ++"],"
++ "r(\"" ++ (show nodeid2) ++ "\")))"
-- | Returns the name of the Node
getNodeLabel :: GInfo -> DGNodeLab -> IO String
getNodeLabel (GInfo {internalNamesIORef = ioRefInternal}) dgnode = do
internal <- readIORef ioRefInternal
let ntype = getDGNodeType dgnode
return $ if (not $ showNames internal) &&
elem ntype ["open_cons__internal"
, "proven_cons__internal"
, "locallyEmpty__open_cons__internal"
, "locallyEmpty__proven_cons__internal"]
then "" else getDGNodeName dgnode