GraphLogic.hs revision 16cef01b8c0a4ecd453efadd5a03134cfff62baf
f82568a780e35e8786958c49a1259434e2088b9cniqModule : $Header$
f82568a780e35e8786958c49a1259434e2088b9cniqDescription : Logic for manipulating the graph in the Central GUI
f82568a780e35e8786958c49a1259434e2088b9cniqCopyright : (c) Jorina Freya Gerken, Till Mossakowski, Uni Bremen 2002-2006
11e076839c8d5a82d55e710194d0daac51390dbdsfLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
f82568a780e35e8786958c49a1259434e2088b9cniqMaintainer : till@informatik.uni-bremen.de
f82568a780e35e8786958c49a1259434e2088b9cniqStability : provisional
f82568a780e35e8786958c49a1259434e2088b9cniqPortability : non-portable (imports Logic)
5bfaaf573bacb45c1cf290ce85ecc676587e8a64jimThis module provides functions for all the menus in the Hets GUI.
5bfaaf573bacb45c1cf290ce85ecc676587e8a64jimThese are then assembled to the GUI in "GUI.GraphMenu".
f82568a780e35e8786958c49a1259434e2088b9cniq , performProofAction
f82568a780e35e8786958c49a1259434e2088b9cniq , openProofStatus
f82568a780e35e8786958c49a1259434e2088b9cniq , saveProofStatus
f82568a780e35e8786958c49a1259434e2088b9cniq , proofMenu
f82568a780e35e8786958c49a1259434e2088b9cniq , showReferencedLibrary
f82568a780e35e8786958c49a1259434e2088b9cniq , getTheoryOfNode
f82568a780e35e8786958c49a1259434e2088b9cniq , translateTheoryOfNode
f82568a780e35e8786958c49a1259434e2088b9cniq , displaySubsortGraph
7bccdbc7016c4ea9d196a15c391d5e629d886e34jorton , displayConceptGraph
f82568a780e35e8786958c49a1259434e2088b9cniq , lookupTheoryOfNode
f82568a780e35e8786958c49a1259434e2088b9cniq , showProofStatusOfNode
f82568a780e35e8786958c49a1259434e2088b9cniq , proveAtNode
f82568a780e35e8786958c49a1259434e2088b9cniq , showNodeInfo
f82568a780e35e8786958c49a1259434e2088b9cniq , showEdgeInfo
f82568a780e35e8786958c49a1259434e2088b9cniq , checkconservativityOfEdge
6fde49e04de4cc97908b20ea01f0c3940f3a1e54rpluem , hideNodes
6fde49e04de4cc97908b20ea01f0c3940f3a1e54rpluem , getLibDeps
f82568a780e35e8786958c49a1259434e2088b9cniq , hideShowNames
f82568a780e35e8786958c49a1259434e2088b9cniq , showNodes
f82568a780e35e8786958c49a1259434e2088b9cniq , translateGraph
f82568a780e35e8786958c49a1259434e2088b9cniq , showLibGraph
f82568a780e35e8786958c49a1259434e2088b9cniq , runAndLock
f82568a780e35e8786958c49a1259434e2088b9cniq , saveUDGraph
f82568a780e35e8786958c49a1259434e2088b9cniq , focusNode
f82568a780e35e8786958c49a1259434e2088b9cniq , applyChanges
f82568a780e35e8786958c49a1259434e2088b9cniqimport Logic.Logic(conservativityCheck,map_sen, comp)
f82568a780e35e8786958c49a1259434e2088b9cniqimport Logic.Coerce(coerceSign, coerceMorphism)
f82568a780e35e8786958c49a1259434e2088b9cniqimport Comorphisms.LogicGraph(logicGraph)
f82568a780e35e8786958c49a1259434e2088b9cniqimport Syntax.AS_Library(LIB_NAME, getModTime, getLIB_ID)
7bccdbc7016c4ea9d196a15c391d5e629d886e34jortonimport Static.AnalysisLibrary(anaLibExt, anaLib)
f82568a780e35e8786958c49a1259434e2088b9cniqimport Static.DGTranslation(libEnv_translation)
f82568a780e35e8786958c49a1259434e2088b9cniqimport Proofs.InferBasic(basicInferenceNode)
f82568a780e35e8786958c49a1259434e2088b9cniqimport Proofs.StatusUtils(lookupHistory, removeContraryChanges)
f82568a780e35e8786958c49a1259434e2088b9cniqimport GUI.Utils (listBox, createTextSaveDisplay)
f82568a780e35e8786958c49a1259434e2088b9cniqimport GUI.Taxonomy (displayConceptGraph,displaySubsortGraph)
f82568a780e35e8786958c49a1259434e2088b9cniqimport GUI.DGTranslation(getDGLogic)
f82568a780e35e8786958c49a1259434e2088b9cniqimport qualified GUI.GraphAbstraction as GA
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniqimport qualified GUI.HTkUtils (displayTheoryWithWarning,
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq createInfoDisplayWithTwoButtons)
f82568a780e35e8786958c49a1259434e2088b9cniqimport GraphConfigure
f82568a780e35e8786958c49a1259434e2088b9cniqimport TextDisplay(createTextDisplay)
f82568a780e35e8786958c49a1259434e2088b9cniqimport InfoBus(encapsulateWaitTermAct)
f82568a780e35e8786958c49a1259434e2088b9cniqimport DialogWin (useHTk)
f82568a780e35e8786958c49a1259434e2088b9cniqimport Messages(warningMess, errorMess)
f82568a780e35e8786958c49a1259434e2088b9cniqimport qualified HTk
f82568a780e35e8786958c49a1259434e2088b9cniqimport Configuration(size)
f82568a780e35e8786958c49a1259434e2088b9cniqimport FileDialog(newFileDialogStr)
f82568a780e35e8786958c49a1259434e2088b9cniqimport Common.DocUtils (showDoc)
f82568a780e35e8786958c49a1259434e2088b9cniqimport Common.AS_Annotation(isAxiom)
f82568a780e35e8786958c49a1259434e2088b9cniqimport Common.Result as Res
f82568a780e35e8786958c49a1259434e2088b9cniqimport qualified Common.OrderedMap as OMap
f82568a780e35e8786958c49a1259434e2088b9cniqimport qualified Common.Lib.Rel as Rel
f82568a780e35e8786958c49a1259434e2088b9cniqimport Driver.WriteFn(writeShATermFile)
f82568a780e35e8786958c49a1259434e2088b9cniqimport Driver.ReadFn(libNameToFile, readVerbose)
f82568a780e35e8786958c49a1259434e2088b9cniqimport System.Directory(getModificationTime)
f82568a780e35e8786958c49a1259434e2088b9cniqimport Data.Char(toLower)
f82568a780e35e8786958c49a1259434e2088b9cniqimport Data.List(partition)
ab2b977442827214b1d884decf3e3f1579fd45e1rpluemimport Data.Graph.Inductive.Graph (Node, LEdge, LNode)
ab2b977442827214b1d884decf3e3f1579fd45e1rpluemimport qualified Data.Map as Map
ab2b977442827214b1d884decf3e3f1579fd45e1rpluemimport Control.Monad(foldM, filterM)
f82568a780e35e8786958c49a1259434e2088b9cniq-- | Locks the global lock and runs function
f82568a780e35e8786958c49a1259434e2088b9cniqrunAndLock :: GInfo -> IO () -> IO ()
f82568a780e35e8786958c49a1259434e2088b9cniqrunAndLock (GInfo { functionLock = lock
f82568a780e35e8786958c49a1259434e2088b9cniq , gi_GraphInfo = actGraphInfo
f82568a780e35e8786958c49a1259434e2088b9cniq }) function = do
f82568a780e35e8786958c49a1259434e2088b9cniq locked <- tryPutMVar lock ()
f82568a780e35e8786958c49a1259434e2088b9cniq case locked of
f82568a780e35e8786958c49a1259434e2088b9cniq True -> do
f82568a780e35e8786958c49a1259434e2088b9cniq takeMVar lock
f82568a780e35e8786958c49a1259434e2088b9cniq GA.redisplay actGraphInfo
f82568a780e35e8786958c49a1259434e2088b9cniq $ "an other function is still working ... please wait ..."
f82568a780e35e8786958c49a1259434e2088b9cniq-- | negate change
f82568a780e35e8786958c49a1259434e2088b9cniqnegateChange :: DGChange -> DGChange
f82568a780e35e8786958c49a1259434e2088b9cniqnegateChange change = case change of
f82568a780e35e8786958c49a1259434e2088b9cniq InsertNode x -> DeleteNode x
f82568a780e35e8786958c49a1259434e2088b9cniq DeleteNode x -> InsertNode x
f82568a780e35e8786958c49a1259434e2088b9cniq InsertEdge x -> DeleteEdge x
f82568a780e35e8786958c49a1259434e2088b9cniq DeleteEdge x -> InsertEdge x
f82568a780e35e8786958c49a1259434e2088b9cniq SetNodeLab old (node, new) -> SetNodeLab new (node, old)
f82568a780e35e8786958c49a1259434e2088b9cniq-- | Undo one step of the History
f82568a780e35e8786958c49a1259434e2088b9cniqundo :: GInfo -> Bool -> IO ()
f82568a780e35e8786958c49a1259434e2088b9cniqundo gInfo@(GInfo { globalHist = gHist
f82568a780e35e8786958c49a1259434e2088b9cniq , gi_GraphInfo = actGraph
f82568a780e35e8786958c49a1259434e2088b9cniq }) isUndo = do
f82568a780e35e8786958c49a1259434e2088b9cniq (guHist, grHist) <- takeMVar gHist
f82568a780e35e8786958c49a1259434e2088b9cniq case if isUndo then guHist else grHist of
f82568a780e35e8786958c49a1259434e2088b9cniq GA.showTemporaryMessage actGraph "History is empty..."
f82568a780e35e8786958c49a1259434e2088b9cniq putMVar gHist (guHist, grHist)
f82568a780e35e8786958c49a1259434e2088b9cniq (lns:gHist') -> do
f82568a780e35e8786958c49a1259434e2088b9cniq undoDGraphs gInfo isUndo lns
f82568a780e35e8786958c49a1259434e2088b9cniq putMVar gHist $ if isUndo then (gHist', reverse lns : grHist)
f82568a780e35e8786958c49a1259434e2088b9cniq else (reverse lns : guHist, gHist')
f82568a780e35e8786958c49a1259434e2088b9cniqundoDGraphs :: GInfo -> Bool -> [LIB_NAME] -> IO ()
f82568a780e35e8786958c49a1259434e2088b9cniqundoDGraphs _ _ [] = return ()
f82568a780e35e8786958c49a1259434e2088b9cniqundoDGraphs g u (ln:r) = do
f82568a780e35e8786958c49a1259434e2088b9cniq undoDGraph g u ln
f82568a780e35e8786958c49a1259434e2088b9cniq undoDGraphs g u r
f82568a780e35e8786958c49a1259434e2088b9cniqundoDGraph :: GInfo -> Bool -> LIB_NAME -> IO ()
f82568a780e35e8786958c49a1259434e2088b9cniqundoDGraph gInfo@(GInfo { libEnvIORef = ioRefProofStatus
f82568a780e35e8786958c49a1259434e2088b9cniq , gi_GraphInfo = actGraph
f82568a780e35e8786958c49a1259434e2088b9cniq }) isUndo ln = do
f82568a780e35e8786958c49a1259434e2088b9cniq (if isUndo then "Un" else "Re") ++ "do last change to "
f82568a780e35e8786958c49a1259434e2088b9cniq ++ show ln ++ "..."
f82568a780e35e8786958c49a1259434e2088b9cniq lockGlobal gInfo
f82568a780e35e8786958c49a1259434e2088b9cniq le <- readIORef ioRefProofStatus
f82568a780e35e8786958c49a1259434e2088b9cniq dg = lookupDGraph ln le
f82568a780e35e8786958c49a1259434e2088b9cniq hist = (proofHistory dg, redoHistory dg)
f82568a780e35e8786958c49a1259434e2088b9cniq swap (a, b) = (b, a)
f82568a780e35e8786958c49a1259434e2088b9cniq (phist, rhist) = (if isUndo then id else swap) hist
f82568a780e35e8786958c49a1259434e2088b9cniq (cl@(rs, cs), newHist) = case phist of
f82568a780e35e8786958c49a1259434e2088b9cniq hd : tl -> (hd, (tl, hd : rhist))
f82568a780e35e8786958c49a1259434e2088b9cniq _ -> error "undoDGraph"
f82568a780e35e8786958c49a1259434e2088b9cniq (newPHist, newRHist) = (if isUndo then id else swap) newHist
f82568a780e35e8786958c49a1259434e2088b9cniq change = if isUndo then (reverse rs, reverse $ map negateChange cs)
f82568a780e35e8786958c49a1259434e2088b9cniq dg' = (changesDG dg $ snd change)
f82568a780e35e8786958c49a1259434e2088b9cniq { proofHistory = newPHist
f82568a780e35e8786958c49a1259434e2088b9cniq , redoHistory = newRHist }
f82568a780e35e8786958c49a1259434e2088b9cniq writeIORef ioRefProofStatus $ Map.insert ln dg' le
f82568a780e35e8786958c49a1259434e2088b9cniq case openlock dg' of
f82568a780e35e8786958c49a1259434e2088b9cniq Nothing -> return ()
f82568a780e35e8786958c49a1259434e2088b9cniq Just lock -> do
f82568a780e35e8786958c49a1259434e2088b9cniq mvar <- tryTakeMVar lock
f82568a780e35e8786958c49a1259434e2088b9cniq case mvar of
f82568a780e35e8786958c49a1259434e2088b9cniq Nothing -> return ()
f82568a780e35e8786958c49a1259434e2088b9cniq Just applyHist -> do
f82568a780e35e8786958c49a1259434e2088b9cniq applyHist [change]
f82568a780e35e8786958c49a1259434e2088b9cniq putMVar lock applyHist
f82568a780e35e8786958c49a1259434e2088b9cniq unlockGlobal gInfo
f82568a780e35e8786958c49a1259434e2088b9cniq-- | reloads the Library of the DevGraph
f82568a780e35e8786958c49a1259434e2088b9cniqreload :: GInfo -> IO()
f82568a780e35e8786958c49a1259434e2088b9cniqreload gInfo@(GInfo { libEnvIORef = ioRefProofStatus
f82568a780e35e8786958c49a1259434e2088b9cniq , gi_LIB_NAME = ln
f82568a780e35e8786958c49a1259434e2088b9cniq , gi_hetcatsOpts = opts
f82568a780e35e8786958c49a1259434e2088b9cniq , gi_GraphInfo = actGraphInfo
f82568a780e35e8786958c49a1259434e2088b9cniq lockGlobal gInfo
f82568a780e35e8786958c49a1259434e2088b9cniq oldle <- readIORef ioRefProofStatus
f82568a780e35e8786958c49a1259434e2088b9cniq libdeps = Rel.toList $ Rel.intransKernel $ Rel.transClosure $ Rel.fromList
f82568a780e35e8786958c49a1259434e2088b9cniq $ getLibDeps oldle
f82568a780e35e8786958c49a1259434e2088b9cniq ioruplibs <- newIORef ([] :: [LIB_NAME])
f82568a780e35e8786958c49a1259434e2088b9cniq writeIORef ioruplibs []
f82568a780e35e8786958c49a1259434e2088b9cniq reloadLibs ioRefProofStatus opts libdeps ioruplibs ln
f82568a780e35e8786958c49a1259434e2088b9cniq unlockGlobal gInfo
f82568a780e35e8786958c49a1259434e2088b9cniq libs <- readIORef ioruplibs
f82568a780e35e8786958c49a1259434e2088b9cniq case libs of
f82568a780e35e8786958c49a1259434e2088b9cniq [] -> GA.showTemporaryMessage actGraphInfo "Reload not needed!"
f82568a780e35e8786958c49a1259434e2088b9cniq _ -> remakeGraph gInfo
f82568a780e35e8786958c49a1259434e2088b9cniq-- | Creates a list of all LIB_NAME pairs, which have a dependency
f82568a780e35e8786958c49a1259434e2088b9cniqgetLibDeps :: LibEnv -> [(LIB_NAME, LIB_NAME)]
f82568a780e35e8786958c49a1259434e2088b9cniqgetLibDeps le =
f82568a780e35e8786958c49a1259434e2088b9cniq concat $ map (\ ln -> getDep ln le) $ Map.keys le
f82568a780e35e8786958c49a1259434e2088b9cniq-- | Creates a list of LIB_NAME pairs for the fist argument
f82568a780e35e8786958c49a1259434e2088b9cniqgetDep :: LIB_NAME -> LibEnv -> [(LIB_NAME, LIB_NAME)]
f82568a780e35e8786958c49a1259434e2088b9cniqgetDep ln le = map (\ (_, x) -> (ln, dgn_libname x)) $
f82568a780e35e8786958c49a1259434e2088b9cniq filter (isDGRef . snd) $ labNodesDG $ lookupDGraph ln le
f82568a780e35e8786958c49a1259434e2088b9cniq-- | Reloads a library
f82568a780e35e8786958c49a1259434e2088b9cniqreloadLib :: IORef LibEnv -> HetcatsOpts -> IORef [LIB_NAME] -> LIB_NAME
f82568a780e35e8786958c49a1259434e2088b9cniqreloadLib iorle opts ioruplibs ln = do
f82568a780e35e8786958c49a1259434e2088b9cniq mfile <- existsAnSource opts {intype = GuessIn}
f82568a780e35e8786958c49a1259434e2088b9cniq $ rmSuffix $ libNameToFile opts ln
f82568a780e35e8786958c49a1259434e2088b9cniq case mfile of
f82568a780e35e8786958c49a1259434e2088b9cniq Nothing -> return ()
f82568a780e35e8786958c49a1259434e2088b9cniq Just file -> do
f82568a780e35e8786958c49a1259434e2088b9cniq le <- readIORef iorle
f82568a780e35e8786958c49a1259434e2088b9cniq mFunc <- case openlock $ lookupDGraph ln le of
f82568a780e35e8786958c49a1259434e2088b9cniq Just lock -> tryTakeMVar lock
f82568a780e35e8786958c49a1259434e2088b9cniq Nothing -> return Nothing
f82568a780e35e8786958c49a1259434e2088b9cniq mres <- anaLibExt opts file le'
f82568a780e35e8786958c49a1259434e2088b9cniq case mres of
f82568a780e35e8786958c49a1259434e2088b9cniq Just (_, newle) -> do
f82568a780e35e8786958c49a1259434e2088b9cniq uplibs <- readIORef ioruplibs
f82568a780e35e8786958c49a1259434e2088b9cniq writeIORef ioruplibs $ ln:uplibs
f82568a780e35e8786958c49a1259434e2088b9cniq case mFunc of
f82568a780e35e8786958c49a1259434e2088b9cniq Just func -> case openlock $ lookupDGraph ln newle of
f82568a780e35e8786958c49a1259434e2088b9cniq Just lock -> putMVar lock func
f82568a780e35e8786958c49a1259434e2088b9cniq Nothing -> errorMess "Reload: Can't set openlock in DevGraph"
f82568a780e35e8786958c49a1259434e2088b9cniq Nothing -> return ()
f82568a780e35e8786958c49a1259434e2088b9cniq writeIORef iorle $ newle
f82568a780e35e8786958c49a1259434e2088b9cniq Nothing ->
f82568a780e35e8786958c49a1259434e2088b9cniq errorMess $ "Could not read original development graph from "
f82568a780e35e8786958c49a1259434e2088b9cniq ++ show file
f82568a780e35e8786958c49a1259434e2088b9cniq-- | Reloads libraries if nessesary
f82568a780e35e8786958c49a1259434e2088b9cniqreloadLibs :: IORef LibEnv -> HetcatsOpts -> [(LIB_NAME, LIB_NAME)]
f82568a780e35e8786958c49a1259434e2088b9cniq -> IORef [LIB_NAME] -> LIB_NAME -> IO Bool
f82568a780e35e8786958c49a1259434e2088b9cniqreloadLibs iorle opts deps ioruplibs ln = do
f82568a780e35e8786958c49a1259434e2088b9cniq uplibs <- readIORef ioruplibs
f82568a780e35e8786958c49a1259434e2088b9cniq case elem ln uplibs of
f82568a780e35e8786958c49a1259434e2088b9cniq True -> return True
f82568a780e35e8786958c49a1259434e2088b9cniq False -> do
f82568a780e35e8786958c49a1259434e2088b9cniq deps' = map (snd) $ filter (\ (ln',_) -> ln == ln') deps
f82568a780e35e8786958c49a1259434e2088b9cniq res <- mapM (reloadLibs iorle opts deps ioruplibs) deps'
f82568a780e35e8786958c49a1259434e2088b9cniq libupdate = foldl (\ u r -> if r then True else u) False res
f82568a780e35e8786958c49a1259434e2088b9cniq case libupdate of
f82568a780e35e8786958c49a1259434e2088b9cniq True -> do
f82568a780e35e8786958c49a1259434e2088b9cniq reloadLib iorle opts ioruplibs ln
f82568a780e35e8786958c49a1259434e2088b9cniq return True
f82568a780e35e8786958c49a1259434e2088b9cniq False -> do
f82568a780e35e8786958c49a1259434e2088b9cniq le <- readIORef iorle
f82568a780e35e8786958c49a1259434e2088b9cniq newln:_ = filter (ln ==) $ Map.keys le
f82568a780e35e8786958c49a1259434e2088b9cniq mfile <- existsAnSource opts $ rmSuffix $ libNameToFile opts ln
f82568a780e35e8786958c49a1259434e2088b9cniq case mfile of
f82568a780e35e8786958c49a1259434e2088b9cniq Nothing -> return False
f82568a780e35e8786958c49a1259434e2088b9cniq Just file -> do
f82568a780e35e8786958c49a1259434e2088b9cniq newmt <- getModificationTime file
f82568a780e35e8786958c49a1259434e2088b9cniq libupdate' = (getModTime $ getLIB_ID newln) < newmt
f82568a780e35e8786958c49a1259434e2088b9cniq case libupdate' of
f82568a780e35e8786958c49a1259434e2088b9cniq False -> return False
f82568a780e35e8786958c49a1259434e2088b9cniq True -> do
f82568a780e35e8786958c49a1259434e2088b9cniq reloadLib iorle opts ioruplibs ln
f82568a780e35e8786958c49a1259434e2088b9cniq return True
f82568a780e35e8786958c49a1259434e2088b9cniq-- | Deletes the old edges and nodes of the Graph and makes new ones
f82568a780e35e8786958c49a1259434e2088b9cniqremakeGraph :: GInfo -> IO ()
f82568a780e35e8786958c49a1259434e2088b9cniqremakeGraph gInfo@(GInfo { libEnvIORef = ioRefProofStatus
f82568a780e35e8786958c49a1259434e2088b9cniq , gi_LIB_NAME = ln
f82568a780e35e8786958c49a1259434e2088b9cniq , gi_GraphInfo = actGraphInfo
f82568a780e35e8786958c49a1259434e2088b9cniq le <- readIORef ioRefProofStatus
f82568a780e35e8786958c49a1259434e2088b9cniq dgraph = lookupDGraph ln le
f82568a780e35e8786958c49a1259434e2088b9cniq showNodes gInfo
f82568a780e35e8786958c49a1259434e2088b9cniq GA.clear actGraphInfo
f82568a780e35e8786958c49a1259434e2088b9cniq convert actGraphInfo dgraph
f82568a780e35e8786958c49a1259434e2088b9cniq hideNodes gInfo
f82568a780e35e8786958c49a1259434e2088b9cniq-- | Toggles to display internal node names
f82568a780e35e8786958c49a1259434e2088b9cniqhideShowNames :: GInfo -> Bool -> IO ()
f82568a780e35e8786958c49a1259434e2088b9cniqhideShowNames (GInfo { internalNamesIORef = showInternalNames
f82568a780e35e8786958c49a1259434e2088b9cniq }) toggle = do
f82568a780e35e8786958c49a1259434e2088b9cniq (intrn::InternalNames) <- readIORef showInternalNames
f82568a780e35e8786958c49a1259434e2088b9cniq let showThem = if toggle then not $ showNames intrn else showNames intrn
f82568a780e35e8786958c49a1259434e2088b9cniq showItrn s = if showThem then s else ""
f82568a780e35e8786958c49a1259434e2088b9cniq mapM_ (\(s,upd) -> upd (\_ -> showItrn s)) $ updater intrn
f82568a780e35e8786958c49a1259434e2088b9cniq writeIORef showInternalNames $ intrn {showNames = showThem}
f82568a780e35e8786958c49a1259434e2088b9cniq-- | shows all hidden nodes and edges
f82568a780e35e8786958c49a1259434e2088b9cniqshowNodes :: GInfo -> IO ()
f82568a780e35e8786958c49a1259434e2088b9cniqshowNodes gInfo@(GInfo { gi_GraphInfo = actGraphInfo
f82568a780e35e8786958c49a1259434e2088b9cniq hhn <- GA.hasHiddenNodes actGraphInfo
f82568a780e35e8786958c49a1259434e2088b9cniq case hhn of
f82568a780e35e8786958c49a1259434e2088b9cniq True -> do
f82568a780e35e8786958c49a1259434e2088b9cniq GA.showTemporaryMessage actGraphInfo "Revealing hidden nodes ..."
f82568a780e35e8786958c49a1259434e2088b9cniq GA.showAll actGraphInfo
f82568a780e35e8786958c49a1259434e2088b9cniq hideShowNames gInfo False
f82568a780e35e8786958c49a1259434e2088b9cniq False -> do
f82568a780e35e8786958c49a1259434e2088b9cniq GA.showTemporaryMessage actGraphInfo "No hidden nodes found ..."
f82568a780e35e8786958c49a1259434e2088b9cniq-- | hides all unnamed internal nodes that are proven
f82568a780e35e8786958c49a1259434e2088b9cniqhideNodes :: GInfo -> IO ()
f82568a780e35e8786958c49a1259434e2088b9cniqhideNodes (GInfo { libEnvIORef = ioRefProofStatus
f82568a780e35e8786958c49a1259434e2088b9cniq , gi_LIB_NAME = ln
f82568a780e35e8786958c49a1259434e2088b9cniq , gi_GraphInfo = actGraphInfo
f82568a780e35e8786958c49a1259434e2088b9cniq hhn <- GA.hasHiddenNodes actGraphInfo
f82568a780e35e8786958c49a1259434e2088b9cniq case hhn of
f82568a780e35e8786958c49a1259434e2088b9cniq GA.showTemporaryMessage actGraphInfo "Nodes already hidden ..."
f82568a780e35e8786958c49a1259434e2088b9cniq False -> do
f82568a780e35e8786958c49a1259434e2088b9cniq GA.showTemporaryMessage actGraphInfo "Hiding unnamed nodes..."
f82568a780e35e8786958c49a1259434e2088b9cniq le <- readIORef ioRefProofStatus
f82568a780e35e8786958c49a1259434e2088b9cniq let dg = lookupDGraph ln le
f82568a780e35e8786958c49a1259434e2088b9cniq nodes = selectNodesByType dg [LocallyEmptyProvenConsInternal]
f82568a780e35e8786958c49a1259434e2088b9cniq edges = getCompressedEdges dg nodes
f82568a780e35e8786958c49a1259434e2088b9cniq GA.hideNodes actGraphInfo nodes edges
f82568a780e35e8786958c49a1259434e2088b9cniq-- | selects all nodes of a type with outgoing edges
f82568a780e35e8786958c49a1259434e2088b9cniqselectNodesByType :: DGraph -> [DGNodeType] -> [Node]
f82568a780e35e8786958c49a1259434e2088b9cniqselectNodesByType dg types =
f82568a780e35e8786958c49a1259434e2088b9cniq filter (\ n -> outDG dg n /= []) $ map fst
f82568a780e35e8786958c49a1259434e2088b9cniq $ filter (\ (_, n) -> elem (getRealDGNodeType n) types) $ labNodesDG dg
f82568a780e35e8786958c49a1259434e2088b9cniq-- | compresses a list of types to the highest one
f82568a780e35e8786958c49a1259434e2088b9cniqcompressTypes :: [DGEdgeType] -> DGEdgeType
f82568a780e35e8786958c49a1259434e2088b9cniqcompressTypes [] = error "compressTypes: wrong usage"
f82568a780e35e8786958c49a1259434e2088b9cniqcompressTypes (t:[]) = t
f82568a780e35e8786958c49a1259434e2088b9cniqcompressTypes (t1:t2:r) = case t1 > t2 of
f82568a780e35e8786958c49a1259434e2088b9cniq True -> compressTypes (t1:r)
f82568a780e35e8786958c49a1259434e2088b9cniq False -> compressTypes (t2:r)
f82568a780e35e8786958c49a1259434e2088b9cniq-- | returns a list of compressed edges
f82568a780e35e8786958c49a1259434e2088b9cniqgetCompressedEdges :: DGraph -> [Node] -> [(Node,Node,DGEdgeType)]
f82568a780e35e8786958c49a1259434e2088b9cniqgetCompressedEdges dg hidden =
f82568a780e35e8786958c49a1259434e2088b9cniq filterDuplicates $ getShortPaths $ concat
f82568a780e35e8786958c49a1259434e2088b9cniq $ map (\ e@(_,t,_) -> map (e:) $ getPaths dg t hidden [])
f82568a780e35e8786958c49a1259434e2088b9cniq inEdges = filter (\ (_,t,_) -> elem t hidden)
f82568a780e35e8786958c49a1259434e2088b9cniq $ concat $ map (outDG dg)
f82568a780e35e8786958c49a1259434e2088b9cniq $ foldr (\ n i -> if elem n hidden
f82568a780e35e8786958c49a1259434e2088b9cniq || elem n i then i else n:i) []
f82568a780e35e8786958c49a1259434e2088b9cniq $ map (\ (s,_,_) -> s) $ concat $ map (innDG dg) hidden
f82568a780e35e8786958c49a1259434e2088b9cniq-- | filter duplicate paths
f82568a780e35e8786958c49a1259434e2088b9cniqfilterDuplicates :: [(Node,Node,DGEdgeType)]
f82568a780e35e8786958c49a1259434e2088b9cniq -> [(Node,Node,DGEdgeType)]
f82568a780e35e8786958c49a1259434e2088b9cniqfilterDuplicates [] = []
f82568a780e35e8786958c49a1259434e2088b9cniqfilterDuplicates ((s,t,et):r) = edge:filterDuplicates others
f82568a780e35e8786958c49a1259434e2088b9cniq (same,others) = partition (\ (s',t',_) -> s == s' && t == t') r
f82568a780e35e8786958c49a1259434e2088b9cniq edge = (s,t,compressTypes $ et:map (\ (_,_,et') -> et') same)
f82568a780e35e8786958c49a1259434e2088b9cniq-- | returns the pahts of a given node through hidden nodes
f82568a780e35e8786958c49a1259434e2088b9cniqgetPaths :: DGraph -> Node -> [Node] -> [Node] -> [[LEdge DGLinkLab]]
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniqgetPaths dg node hidden seen' = case elem node hidden of
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq True -> case edges /= [] of
f82568a780e35e8786958c49a1259434e2088b9cniq True -> concat $ map (\ e@(_,t,_) -> map (e:) $ getPaths dg t hidden seen)
f82568a780e35e8786958c49a1259434e2088b9cniq False -> []
f82568a780e35e8786958c49a1259434e2088b9cniq False -> [[]]
f82568a780e35e8786958c49a1259434e2088b9cniq seen = node:seen'
f82568a780e35e8786958c49a1259434e2088b9cniq edges = filter (\ (_,t,_) -> notElem t seen) $ outDG dg node
f82568a780e35e8786958c49a1259434e2088b9cniq-- | returns source and target node of a path with the compressed type
f82568a780e35e8786958c49a1259434e2088b9cniqgetShortPaths :: [[LEdge DGLinkLab]]
f82568a780e35e8786958c49a1259434e2088b9cniq -> [(Node,Node,DGEdgeType)]
f82568a780e35e8786958c49a1259434e2088b9cniqgetShortPaths [] = []
f82568a780e35e8786958c49a1259434e2088b9cniqgetShortPaths (p:r) =
f82568a780e35e8786958c49a1259434e2088b9cniq ((s,t,compressTypes $ map (\ (_,_,e) -> getRealDGLinkType e) p))
f82568a780e35e8786958c49a1259434e2088b9cniq : getShortPaths r
5bfaaf573bacb45c1cf290ce85ecc676587e8a64jim (s,_,_) = head p
f82568a780e35e8786958c49a1259434e2088b9cniq (_,t,_) = last p
f82568a780e35e8786958c49a1259434e2088b9cniq-- | Let the user select a Node to focus
f82568a780e35e8786958c49a1259434e2088b9cniqfocusNode :: GInfo -> IO ()
f82568a780e35e8786958c49a1259434e2088b9cniqfocusNode GInfo { libEnvIORef = ioRefProofStatus
f82568a780e35e8786958c49a1259434e2088b9cniq , gi_LIB_NAME = ln
f82568a780e35e8786958c49a1259434e2088b9cniq , gi_GraphInfo = grInfo } = do
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq le <- readIORef ioRefProofStatus
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq idsnodes <- filterM (fmap not . GA.isHiddenNode grInfo . fst)
f82568a780e35e8786958c49a1259434e2088b9cniq $ labNodesDG $ lookupDGraph ln le
f82568a780e35e8786958c49a1259434e2088b9cniq selection <- listBox "Select a node to focus"
f82568a780e35e8786958c49a1259434e2088b9cniq $ map (\ (n, l) -> shows n " " ++ getDGNodeName l) idsnodes
f82568a780e35e8786958c49a1259434e2088b9cniq case selection of
f82568a780e35e8786958c49a1259434e2088b9cniq Just idx -> GA.focusNode grInfo $ fst $ idsnodes !! idx
f82568a780e35e8786958c49a1259434e2088b9cniq Nothing -> return ()
f82568a780e35e8786958c49a1259434e2088b9cniqtranslateGraph :: GInfo -> ConvFunc -> LibFunc -> IO ()
f82568a780e35e8786958c49a1259434e2088b9cniqtranslateGraph (GInfo {libEnvIORef = ioRefProofStatus,
f82568a780e35e8786958c49a1259434e2088b9cniq gi_LIB_NAME = ln,
f82568a780e35e8786958c49a1259434e2088b9cniq gi_hetcatsOpts = opts
f82568a780e35e8786958c49a1259434e2088b9cniq }) convGraph showLib = do
f82568a780e35e8786958c49a1259434e2088b9cniq le <- readIORef ioRefProofStatus
f82568a780e35e8786958c49a1259434e2088b9cniq openTranslateGraph le ln opts (getDGLogic le) convGraph showLib
f82568a780e35e8786958c49a1259434e2088b9cniqshowLibGraph :: GInfo -> LibFunc -> IO ()
f82568a780e35e8786958c49a1259434e2088b9cniqshowLibGraph gInfo showLib = do
f82568a780e35e8786958c49a1259434e2088b9cniq showLib gInfo
f82568a780e35e8786958c49a1259434e2088b9cniq{- | it tries to perform the given action to the given graph.
f82568a780e35e8786958c49a1259434e2088b9cniq If part of the given graph is not hidden, then the action can
f82568a780e35e8786958c49a1259434e2088b9cniq be performed directly; otherwise the graph will be shown completely
f82568a780e35e8786958c49a1259434e2088b9cniq firstly, and then the action will be performed, and after that the graph
f82568a780e35e8786958c49a1259434e2088b9cniq will be hidden again.
f82568a780e35e8786958c49a1259434e2088b9cniqperformProofAction :: GInfo -> IO () -> IO ()
f82568a780e35e8786958c49a1259434e2088b9cniqperformProofAction gInfo@(GInfo { gi_GraphInfo = actGraphInfo
f82568a780e35e8786958c49a1259434e2088b9cniq }) proofAction = do
f82568a780e35e8786958c49a1259434e2088b9cniq let actionWithMessage = do
f82568a780e35e8786958c49a1259434e2088b9cniq "Applying development graph calculus proof rule..."
f82568a780e35e8786958c49a1259434e2088b9cniq proofAction
f82568a780e35e8786958c49a1259434e2088b9cniq hhn <- GA.hasHiddenNodes actGraphInfo
f82568a780e35e8786958c49a1259434e2088b9cniq case hhn of
f82568a780e35e8786958c49a1259434e2088b9cniq True -> do
f82568a780e35e8786958c49a1259434e2088b9cniq showNodes gInfo
f82568a780e35e8786958c49a1259434e2088b9cniq actionWithMessage
f82568a780e35e8786958c49a1259434e2088b9cniq hideNodes gInfo
f82568a780e35e8786958c49a1259434e2088b9cniq False -> actionWithMessage
f82568a780e35e8786958c49a1259434e2088b9cniq "Development graph calculus proof rule finished."
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniqsaveProofStatus :: GInfo -> FilePath -> IO ()
f82568a780e35e8786958c49a1259434e2088b9cniqsaveProofStatus (GInfo { libEnvIORef = ioRefProofStatus
f82568a780e35e8786958c49a1259434e2088b9cniq , gi_LIB_NAME = ln
f82568a780e35e8786958c49a1259434e2088b9cniq , gi_hetcatsOpts = opts
f82568a780e35e8786958c49a1259434e2088b9cniq }) file = encapsulateWaitTermAct $ do
f82568a780e35e8786958c49a1259434e2088b9cniq proofStatus <- readIORef ioRefProofStatus
f82568a780e35e8786958c49a1259434e2088b9cniq writeShATermFile file (ln, lookupHistory ln proofStatus)
f82568a780e35e8786958c49a1259434e2088b9cniq putIfVerbose opts 2 $ "Wrote " ++ file
f82568a780e35e8786958c49a1259434e2088b9cniq-- | implementation of open menu, read in a proof status
f82568a780e35e8786958c49a1259434e2088b9cniqopenProofStatus :: GInfo -> FilePath -> ConvFunc -> LibFunc
f82568a780e35e8786958c49a1259434e2088b9cniqopenProofStatus gInfo@(GInfo { libEnvIORef = ioRefProofStatus
f82568a780e35e8786958c49a1259434e2088b9cniq , gi_LIB_NAME = ln
f82568a780e35e8786958c49a1259434e2088b9cniq , gi_hetcatsOpts = opts
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq }) file convGraph showLib = do
f82568a780e35e8786958c49a1259434e2088b9cniq mh <- readVerbose opts ln file
f82568a780e35e8786958c49a1259434e2088b9cniq case mh of
f82568a780e35e8786958c49a1259434e2088b9cniq Nothing -> errorMess $ "Could not read proof status from file '"
f82568a780e35e8786958c49a1259434e2088b9cniq ++ file ++ "'"
f82568a780e35e8786958c49a1259434e2088b9cniq Just h -> do
f82568a780e35e8786958c49a1259434e2088b9cniq let libfile = libNameToFile opts ln
f82568a780e35e8786958c49a1259434e2088b9cniq m <- anaLib opts { outtypes = [] } libfile
f82568a780e35e8786958c49a1259434e2088b9cniq Nothing -> errorMess $ "Could not read original development graph"
f82568a780e35e8786958c49a1259434e2088b9cniq ++ " from '" ++ libfile ++ "'"
f82568a780e35e8786958c49a1259434e2088b9cniq Just (_, libEnv) -> case Map.lookup ln libEnv of
f82568a780e35e8786958c49a1259434e2088b9cniq Nothing -> errorMess $ "Could not get original development"
f82568a780e35e8786958c49a1259434e2088b9cniq ++ " graph for '" ++ showDoc ln "'"
f82568a780e35e8786958c49a1259434e2088b9cniq Just dg -> do
f82568a780e35e8786958c49a1259434e2088b9cniq lockGlobal gInfo
f82568a780e35e8786958c49a1259434e2088b9cniq oldEnv <- readIORef ioRefProofStatus
f82568a780e35e8786958c49a1259434e2088b9cniq let proofStatus = Map.insert ln
f82568a780e35e8786958c49a1259434e2088b9cniq (applyProofHistory h dg) oldEnv
f82568a780e35e8786958c49a1259434e2088b9cniq writeIORef ioRefProofStatus proofStatus
f82568a780e35e8786958c49a1259434e2088b9cniq unlockGlobal gInfo
f82568a780e35e8786958c49a1259434e2088b9cniq gInfo' <- copyGInfo gInfo ln
f82568a780e35e8786958c49a1259434e2088b9cniq convGraph gInfo' "Proof Status " showLib
f82568a780e35e8786958c49a1259434e2088b9cniq let actGraphInfo = gi_GraphInfo gInfo
f82568a780e35e8786958c49a1259434e2088b9cniq GA.redisplay actGraphInfo
f82568a780e35e8786958c49a1259434e2088b9cniq-- | apply a rule of the development graph calculus
f82568a780e35e8786958c49a1259434e2088b9cniqproofMenu :: GInfo
f82568a780e35e8786958c49a1259434e2088b9cniq -> (LibEnv -> IO (Res.Result LibEnv))
f82568a780e35e8786958c49a1259434e2088b9cniqproofMenu gInfo@(GInfo { libEnvIORef = ioRefProofStatus
f82568a780e35e8786958c49a1259434e2088b9cniq , gi_LIB_NAME = ln
f82568a780e35e8786958c49a1259434e2088b9cniq , gi_GraphInfo = actGraphInfo
f82568a780e35e8786958c49a1259434e2088b9cniq , gi_hetcatsOpts = hOpts
f82568a780e35e8786958c49a1259434e2088b9cniq , proofGUIMVar = guiMVar
f82568a780e35e8786958c49a1259434e2088b9cniq , globalHist = gHist
f82568a780e35e8786958c49a1259434e2088b9cniq }) proofFun = do
f82568a780e35e8786958c49a1259434e2088b9cniq filled <- tryPutMVar guiMVar Nothing
f82568a780e35e8786958c49a1259434e2088b9cniq if not filled
f82568a780e35e8786958c49a1259434e2088b9cniq then readMVar guiMVar >>=
f82568a780e35e8786958c49a1259434e2088b9cniq (maybe (putIfVerbose hOpts 0 "proofMenu: ignored Nothing")
f82568a780e35e8786958c49a1259434e2088b9cniq (\ w -> do
f82568a780e35e8786958c49a1259434e2088b9cniq putIfVerbose hOpts 4 $
f82568a780e35e8786958c49a1259434e2088b9cniq "proofMenu: Ignored Proof command; " ++
f82568a780e35e8786958c49a1259434e2088b9cniq "maybe a proof window is still open?"
f82568a780e35e8786958c49a1259434e2088b9cniq lockGlobal gInfo
f82568a780e35e8786958c49a1259434e2088b9cniq proofStatus <- readIORef ioRefProofStatus
f82568a780e35e8786958c49a1259434e2088b9cniq putIfVerbose hOpts 4 "Proof started via \"Proofs\" menu"
f82568a780e35e8786958c49a1259434e2088b9cniq Res.Result ds res <- proofFun proofStatus
f82568a780e35e8786958c49a1259434e2088b9cniq putIfVerbose hOpts 4 "Analyzing result of proof"
f82568a780e35e8786958c49a1259434e2088b9cniq case res of
f82568a780e35e8786958c49a1259434e2088b9cniq Nothing -> do
f82568a780e35e8786958c49a1259434e2088b9cniq unlockGlobal gInfo
f82568a780e35e8786958c49a1259434e2088b9cniq printDiags 2 ds
f82568a780e35e8786958c49a1259434e2088b9cniq Just newProofStatus -> do
f82568a780e35e8786958c49a1259434e2088b9cniq let newGr = lookupDGraph ln newProofStatus
f82568a780e35e8786958c49a1259434e2088b9cniq history = proofHistory newGr
f82568a780e35e8786958c49a1259434e2088b9cniq (guHist, grHist) <- takeMVar gHist
f82568a780e35e8786958c49a1259434e2088b9cniq doDump hOpts "PrintHistory" $ do
f82568a780e35e8786958c49a1259434e2088b9cniq putStrLn "History"
f82568a780e35e8786958c49a1259434e2088b9cniq print $ prettyHistory history
f82568a780e35e8786958c49a1259434e2088b9cniq putMVar gHist
f82568a780e35e8786958c49a1259434e2088b9cniq (calcGlobalHistory proofStatus newProofStatus : guHist, grHist)
f82568a780e35e8786958c49a1259434e2088b9cniq applyChanges actGraphInfo history
f82568a780e35e8786958c49a1259434e2088b9cniq writeIORef ioRefProofStatus newProofStatus
f82568a780e35e8786958c49a1259434e2088b9cniq unlockGlobal gInfo
f82568a780e35e8786958c49a1259434e2088b9cniq hideShowNames gInfo False
f82568a780e35e8786958c49a1259434e2088b9cniq mGUIMVar <- tryTakeMVar guiMVar
f82568a780e35e8786958c49a1259434e2088b9cniq maybe (fail $ "should be filled with Nothing after proof attempt")
f82568a780e35e8786958c49a1259434e2088b9cniq (const $ return ())
f82568a780e35e8786958c49a1259434e2088b9cniqcalcGlobalHistory :: LibEnv -> LibEnv -> [LIB_NAME]
f82568a780e35e8786958c49a1259434e2088b9cniqcalcGlobalHistory old new = let
f82568a780e35e8786958c49a1259434e2088b9cniq pHist = (\ ln le -> proofHistory $ lookupDGraph ln le)
f82568a780e35e8786958c49a1259434e2088b9cniq length' = (\ ln le -> length $ pHist ln le)
f82568a780e35e8786958c49a1259434e2088b9cniq changes = filter (\ ln -> pHist ln old /= pHist ln new) $ Map.keys old
f82568a780e35e8786958c49a1259434e2088b9cniq in concatMap (\ ln -> replicate (length' ln new - length' ln old) ln) changes
f82568a780e35e8786958c49a1259434e2088b9cniqnodeErr :: Int -> IO ()
f82568a780e35e8786958c49a1259434e2088b9cniqnodeErr descr = error $ "node with descriptor " ++ show descr
f82568a780e35e8786958c49a1259434e2088b9cniq ++ " has no corresponding node in the development graph"
f82568a780e35e8786958c49a1259434e2088b9cniqshowNodeInfo :: Int -> DGraph -> IO ()
f82568a780e35e8786958c49a1259434e2088b9cniqshowNodeInfo descr dgraph = do
f82568a780e35e8786958c49a1259434e2088b9cniq let dgnode = labDG dgraph descr
f82568a780e35e8786958c49a1259434e2088b9cniq title = (if isDGRef dgnode then ("reference " ++) else
f82568a780e35e8786958c49a1259434e2088b9cniq if isInternalNode dgnode then ("internal " ++) else id)
f82568a780e35e8786958c49a1259434e2088b9cniq "node " ++ getDGNodeName dgnode ++ " " ++ show descr
f82568a780e35e8786958c49a1259434e2088b9cniq createTextDisplay title (title ++ "\n" ++ showDoc dgnode "")
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq fetches the theory from a node inside the IO Monad
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq (added by KL based on code in getTheoryOfNode) -}
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniqlookupTheoryOfNode :: IORef LibEnv -> LIB_NAME -> Int
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq -> IO (Res.Result (LibEnv, Node, G_theory))
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniqlookupTheoryOfNode proofStatusRef ln descr = do
f82568a780e35e8786958c49a1259434e2088b9cniq libEnv <- readIORef proofStatusRef
f82568a780e35e8786958c49a1259434e2088b9cniq return $ do
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq (libEnv', gth) <- computeTheory True libEnv ln descr
f82568a780e35e8786958c49a1259434e2088b9cniq return (libEnv', descr, gth)
f82568a780e35e8786958c49a1259434e2088b9cniqshowDiagMess :: HetcatsOpts -> [Diagnosis] -> IO ()
f82568a780e35e8786958c49a1259434e2088b9cniqshowDiagMess opts ds = let es = Res.filterDiags (verbose opts) ds in
f82568a780e35e8786958c49a1259434e2088b9cniq if null es then return () else
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq (if hasErrors es then errorMess else warningMess) $ unlines $ map show es
f82568a780e35e8786958c49a1259434e2088b9cniq{- | outputs the theory of a node in a window;
f82568a780e35e8786958c49a1259434e2088b9cniqused by the node menu defined in initializeGraph-}
f82568a780e35e8786958c49a1259434e2088b9cniqgetTheoryOfNode :: GInfo -> Int -> DGraph -> IO ()
f82568a780e35e8786958c49a1259434e2088b9cniqgetTheoryOfNode gInfo@(GInfo { gi_LIB_NAME = ln
f82568a780e35e8786958c49a1259434e2088b9cniq , gi_GraphInfo = actGraphInfo
f82568a780e35e8786958c49a1259434e2088b9cniq , libEnvIORef = le
f82568a780e35e8786958c49a1259434e2088b9cniq }) descr dgraph = do
f82568a780e35e8786958c49a1259434e2088b9cniq r <- lookupTheoryOfNode le ln descr
f82568a780e35e8786958c49a1259434e2088b9cniq Res.Result ds res -> do
f82568a780e35e8786958c49a1259434e2088b9cniq showDiagMess (gi_hetcatsOpts gInfo) ds
f82568a780e35e8786958c49a1259434e2088b9cniq case res of
f82568a780e35e8786958c49a1259434e2088b9cniq (Just (le', n, gth)) -> do
f82568a780e35e8786958c49a1259434e2088b9cniq lockGlobal gInfo
f82568a780e35e8786958c49a1259434e2088b9cniq "Theory" (getNameOfNode n dgraph)
f82568a780e35e8786958c49a1259434e2088b9cniq (addHasInHidingWarning dgraph n)
f82568a780e35e8786958c49a1259434e2088b9cniq let newGr = lookupDGraph ln le'
f82568a780e35e8786958c49a1259434e2088b9cniq newHistory = proofHistory newGr
f82568a780e35e8786958c49a1259434e2088b9cniq libEnv <- readIORef le
f82568a780e35e8786958c49a1259434e2088b9cniq let oldHistory = proofHistory $ lookupDGraph ln libEnv
f82568a780e35e8786958c49a1259434e2088b9cniq history = take (length newHistory - length oldHistory) newHistory
f82568a780e35e8786958c49a1259434e2088b9cniq applyChanges actGraphInfo history
f82568a780e35e8786958c49a1259434e2088b9cniq writeIORef le le'
f82568a780e35e8786958c49a1259434e2088b9cniq unlockGlobal gInfo
f82568a780e35e8786958c49a1259434e2088b9cniq _ -> return ()
f82568a780e35e8786958c49a1259434e2088b9cniq{- | translate the theory of a node in a window;
f82568a780e35e8786958c49a1259434e2088b9cniqused by the node menu defined in initializeGraph-}
f82568a780e35e8786958c49a1259434e2088b9cniqtranslateTheoryOfNode :: GInfo -> Int -> DGraph -> IO ()
f82568a780e35e8786958c49a1259434e2088b9cniqtranslateTheoryOfNode
f82568a780e35e8786958c49a1259434e2088b9cniq gInfo@(GInfo {gi_hetcatsOpts = opts, libEnvIORef = le}) node dgraph = do
f82568a780e35e8786958c49a1259434e2088b9cniq libEnv <- readIORef le
f82568a780e35e8786958c49a1259434e2088b9cniq let Res.Result ds mEnv = computeTheory False libEnv (gi_LIB_NAME gInfo) node
f82568a780e35e8786958c49a1259434e2088b9cniq case mEnv of
f82568a780e35e8786958c49a1259434e2088b9cniq Just (_, th@(G_theory lid sign _ sens _)) -> do
f82568a780e35e8786958c49a1259434e2088b9cniq -- find all comorphism paths starting from lid
f82568a780e35e8786958c49a1259434e2088b9cniq let paths = findComorphismPaths logicGraph (sublogicOfTh th)
f82568a780e35e8786958c49a1259434e2088b9cniq -- let the user choose one
f82568a780e35e8786958c49a1259434e2088b9cniq sel <- listBox "Choose a node logic translation" $ map show paths
f82568a780e35e8786958c49a1259434e2088b9cniq case sel of
f82568a780e35e8786958c49a1259434e2088b9cniq Nothing -> warningMess "no node logic translation chosen"
f82568a780e35e8786958c49a1259434e2088b9cniq Just i -> do
f82568a780e35e8786958c49a1259434e2088b9cniq Comorphism cid <- return (paths!!i)
f82568a780e35e8786958c49a1259434e2088b9cniq -- adjust lid's
f82568a780e35e8786958c49a1259434e2088b9cniq let lidS = sourceLogic cid
f82568a780e35e8786958c49a1259434e2088b9cniq lidT = targetLogic cid
f82568a780e35e8786958c49a1259434e2088b9cniq sign' <- coerceSign lid lidS "" sign
f82568a780e35e8786958c49a1259434e2088b9cniq sens' <- coerceThSens lid lidS "" sens
f82568a780e35e8786958c49a1259434e2088b9cniq -- translate theory along chosen comorphism
f82568a780e35e8786958c49a1259434e2088b9cniq let Result es mTh = wrapMapTheory cid
f82568a780e35e8786958c49a1259434e2088b9cniq (plainSign sign', toNamedList sens')
f82568a780e35e8786958c49a1259434e2088b9cniq case mTh of
f82568a780e35e8786958c49a1259434e2088b9cniq Nothing -> showDiagMess opts es
f82568a780e35e8786958c49a1259434e2088b9cniq Just (sign'', sens1) -> GUI.HTkUtils.displayTheoryWithWarning
f82568a780e35e8786958c49a1259434e2088b9cniq "Translated Theory" (getNameOfNode node dgraph)
f82568a780e35e8786958c49a1259434e2088b9cniq (addHasInHidingWarning dgraph node)
f82568a780e35e8786958c49a1259434e2088b9cniq (G_theory lidT (mkExtSign sign'') startSigId
f82568a780e35e8786958c49a1259434e2088b9cniq (toThSens sens1) startThId)
f82568a780e35e8786958c49a1259434e2088b9cniq Nothing -> showDiagMess opts ds
f82568a780e35e8786958c49a1259434e2088b9cniq-- | Show proof status of a node
f82568a780e35e8786958c49a1259434e2088b9cniqshowProofStatusOfNode :: GInfo -> Int -> DGraph -> IO ()
f82568a780e35e8786958c49a1259434e2088b9cniqshowProofStatusOfNode _ descr dgraph = do
f82568a780e35e8786958c49a1259434e2088b9cniq let dgnode = labDG dgraph descr
f82568a780e35e8786958c49a1259434e2088b9cniq stat = showStatusAux dgnode
f82568a780e35e8786958c49a1259434e2088b9cniq title = "Proof status of node "++showName (dgn_name dgnode)
f82568a780e35e8786958c49a1259434e2088b9cniq createTextDisplay title stat [HTk.size(105,55)]
f82568a780e35e8786958c49a1259434e2088b9cniqshowStatusAux :: DGNodeLab -> String
f82568a780e35e8786958c49a1259434e2088b9cniqshowStatusAux dgnode =
f82568a780e35e8786958c49a1259434e2088b9cniq case dgn_theory dgnode of
f82568a780e35e8786958c49a1259434e2088b9cniq G_theory _ _ _ sens _ ->
f82568a780e35e8786958c49a1259434e2088b9cniq let goals = OMap.filter (not . isAxiom) sens
f82568a780e35e8786958c49a1259434e2088b9cniq (proven,open) = OMap.partition isProvenSenStatus goals
f82568a780e35e8786958c49a1259434e2088b9cniq consGoal = "\nconservativity of this node"
f82568a780e35e8786958c49a1259434e2088b9cniq in "Proven proof goals:\n"
f82568a780e35e8786958c49a1259434e2088b9cniq ++ showDoc proven ""
f82568a780e35e8786958c49a1259434e2088b9cniq ++ if not $ hasOpenConsStatus True dgnode
f82568a780e35e8786958c49a1259434e2088b9cniq then consGoal
f82568a780e35e8786958c49a1259434e2088b9cniq ++ "\nOpen proof goals:\n"
f82568a780e35e8786958c49a1259434e2088b9cniq ++ showDoc open ""
f82568a780e35e8786958c49a1259434e2088b9cniq ++ if hasOpenConsStatus False dgnode
f82568a780e35e8786958c49a1259434e2088b9cniq then consGoal
f82568a780e35e8786958c49a1259434e2088b9cniq-- | start local theorem proving or consistency checking at a node
f82568a780e35e8786958c49a1259434e2088b9cniqproveAtNode :: Bool -> GInfo -> Int -> DGraph -> IO ()
f82568a780e35e8786958c49a1259434e2088b9cniqproveAtNode checkCons gInfo@(GInfo { libEnvIORef = ioRefProofStatus
f82568a780e35e8786958c49a1259434e2088b9cniq , gi_LIB_NAME = ln
f82568a780e35e8786958c49a1259434e2088b9cniq , commandHist = ch }) descr dgraph = do
f82568a780e35e8786958c49a1259434e2088b9cniq let dgn = labDG dgraph descr
f82568a780e35e8786958c49a1259434e2088b9cniq libNode = (ln,descr)
f82568a780e35e8786958c49a1259434e2088b9cniq (dgraph',dgn') <- case hasLock dgn of
f82568a780e35e8786958c49a1259434e2088b9cniq True -> return (dgraph, dgn)
f82568a780e35e8786958c49a1259434e2088b9cniq False -> do
f82568a780e35e8786958c49a1259434e2088b9cniq lockGlobal gInfo
f82568a780e35e8786958c49a1259434e2088b9cniq le <- readIORef ioRefProofStatus
f82568a780e35e8786958c49a1259434e2088b9cniq (dgraph',dgn') <- initLocking (lookupDGraph ln le) (descr, dgn)
f82568a780e35e8786958c49a1259434e2088b9cniq writeIORef ioRefProofStatus $ Map.insert ln dgraph' le
f82568a780e35e8786958c49a1259434e2088b9cniq unlockGlobal gInfo
f82568a780e35e8786958c49a1259434e2088b9cniq return (dgraph',dgn')
f82568a780e35e8786958c49a1259434e2088b9cniq locked <- tryLockLocal dgn'
f82568a780e35e8786958c49a1259434e2088b9cniq case locked of
f82568a780e35e8786958c49a1259434e2088b9cniq False -> do
f82568a780e35e8786958c49a1259434e2088b9cniq createTextDisplay "Error" "Proofwindow already open" [HTk.size(30,10)]
f82568a780e35e8786958c49a1259434e2088b9cniq True -> do
f82568a780e35e8786958c49a1259434e2088b9cniq let action = do
f82568a780e35e8786958c49a1259434e2088b9cniq le <- readIORef ioRefProofStatus
f82568a780e35e8786958c49a1259434e2088b9cniq guiMVar <- newMVar Nothing
f82568a780e35e8786958c49a1259434e2088b9cniq res <- basicInferenceNode checkCons logicGraph libNode ln
f82568a780e35e8786958c49a1259434e2088b9cniq guiMVar le ch
f82568a780e35e8786958c49a1259434e2088b9cniq runProveAtNode gInfo (descr, dgn') res
f82568a780e35e8786958c49a1259434e2088b9cniq case checkCons || not (hasIncomingHidingEdge dgraph' $ snd libNode) of
f82568a780e35e8786958c49a1259434e2088b9cniq True -> action
7bccdbc7016c4ea9d196a15c391d5e629d886e34jorton False -> GUI.HTkUtils.createInfoDisplayWithTwoButtons "Warning"
7bccdbc7016c4ea9d196a15c391d5e629d886e34jorton "This node has incoming hiding links!!!" "Prove anyway"
f82568a780e35e8786958c49a1259434e2088b9cniq unlockLocal dgn'
f82568a780e35e8786958c49a1259434e2088b9cniqrunProveAtNode :: GInfo -> LNode DGNodeLab
f82568a780e35e8786958c49a1259434e2088b9cniqrunProveAtNode gInfo (v, dgnode) res = case maybeResult res of
f82568a780e35e8786958c49a1259434e2088b9cniq Just (le, tres) -> do
f82568a780e35e8786958c49a1259434e2088b9cniq case maybeResult tres of
f82568a780e35e8786958c49a1259434e2088b9cniq Just gth -> createTextSaveDisplay
f82568a780e35e8786958c49a1259434e2088b9cniq ("Model for " ++ getDGNodeName dgnode ++ " node: " ++ show v)
f82568a780e35e8786958c49a1259434e2088b9cniq "model.log" $ showDoc gth ""
f82568a780e35e8786958c49a1259434e2088b9cniq Nothing -> case diags tres of
f82568a780e35e8786958c49a1259434e2088b9cniq [] -> return ()
f82568a780e35e8786958c49a1259434e2088b9cniq createTextDisplay "Error" (showRelDiags 2 ds) [HTk.size(50,10)]
f82568a780e35e8786958c49a1259434e2088b9cniq proofMenu gInfo $ mergeDGNodeLab gInfo
f82568a780e35e8786958c49a1259434e2088b9cniq (v, labDG (lookupDGraph (gi_LIB_NAME gInfo) le) v)
f82568a780e35e8786958c49a1259434e2088b9cniq Nothing -> return ()
f82568a780e35e8786958c49a1259434e2088b9cniqmergeDGNodeLab :: GInfo -> LNode DGNodeLab -> LibEnv -> IO (Res.Result LibEnv)
f82568a780e35e8786958c49a1259434e2088b9cniqmergeDGNodeLab (GInfo{gi_LIB_NAME = ln}) (v, new_dgn) le = do
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq let dg = lookupDGraph ln le
f82568a780e35e8786958c49a1259434e2088b9cniq old_dgn = labDG dg v
f82568a780e35e8786958c49a1259434e2088b9cniq return $ do
f82568a780e35e8786958c49a1259434e2088b9cniq theory <- joinG_sentences (dgn_theory old_dgn) $ dgn_theory new_dgn
f82568a780e35e8786958c49a1259434e2088b9cniq let new_dgn' = old_dgn { dgn_theory = theory }
f82568a780e35e8786958c49a1259434e2088b9cniq (dg', _) = labelNodeDG (v, new_dgn') dg
f82568a780e35e8786958c49a1259434e2088b9cniq dg'' = addToProofHistoryDG ([], [SetNodeLab old_dgn (v, new_dgn')]) dg'
f82568a780e35e8786958c49a1259434e2088b9cniq return $ Map.insert ln dg'' le
f82568a780e35e8786958c49a1259434e2088b9cniq-- | print the id, origin, type, proof-status and morphism of the edge
f82568a780e35e8786958c49a1259434e2088b9cniqshowEdgeInfo :: Int -> Maybe (LEdge DGLinkLab) -> IO ()
f82568a780e35e8786958c49a1259434e2088b9cniqshowEdgeInfo descr me = case me of
f82568a780e35e8786958c49a1259434e2088b9cniq Just e@(_, _, l) -> let estr = showLEdge e in
f82568a780e35e8786958c49a1259434e2088b9cniq createTextDisplay ("Info of " ++ estr)
f82568a780e35e8786958c49a1259434e2088b9cniq (estr ++ "\n" ++ showDoc l "") [HTk.size(70,30)]
f82568a780e35e8786958c49a1259434e2088b9cniq Nothing -> createTextDisplay "Error"
f82568a780e35e8786958c49a1259434e2088b9cniq ("edge " ++ show descr ++ " has no corresponding edge"
f82568a780e35e8786958c49a1259434e2088b9cniq ++ "in the development graph") [HTk.size(50,10)]
f82568a780e35e8786958c49a1259434e2088b9cniq-- | check conservativity of the edge
f82568a780e35e8786958c49a1259434e2088b9cniqcheckconservativityOfEdge :: Int -> GInfo -> Maybe (LEdge DGLinkLab) -> IO ()
f82568a780e35e8786958c49a1259434e2088b9cniqcheckconservativityOfEdge _ gInfo@(GInfo{gi_LIB_NAME = ln,
f82568a780e35e8786958c49a1259434e2088b9cniq gi_GraphInfo = actGraphInfo,
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq libEnvIORef = le})
f82568a780e35e8786958c49a1259434e2088b9cniq (Just (source,target,linklab)) = do
f82568a780e35e8786958c49a1259434e2088b9cniq lockGlobal gInfo
f82568a780e35e8786958c49a1259434e2088b9cniq libEnv <- readIORef $ libEnvIORef gInfo
f82568a780e35e8786958c49a1259434e2088b9cniq let libEnv' = case convertToNf ln libEnv target of
f82568a780e35e8786958c49a1259434e2088b9cniq Result _ (Just lE) -> lE
f82568a780e35e8786958c49a1259434e2088b9cniq _ -> error "checkconservativityOfEdge: convertToNf"
f82568a780e35e8786958c49a1259434e2088b9cniq let (_, thTar) =
f82568a780e35e8786958c49a1259434e2088b9cniq case computeTheory True libEnv' ln target of
f82568a780e35e8786958c49a1259434e2088b9cniq Res.Result _ (Just th1) -> th1
f82568a780e35e8786958c49a1259434e2088b9cniq _ -> error "checkconservativityOfEdge: computeTheory"
f82568a780e35e8786958c49a1259434e2088b9cniq G_theory lid _sign _ sensTar _ <- return thTar
f82568a780e35e8786958c49a1259434e2088b9cniq GMorphism cid _ _ morphism2 _ <- return $ dgl_morphism linklab
f82568a780e35e8786958c49a1259434e2088b9cniq Just (GMorphism cid' _ _ morphism3 _) <- return $
f82568a780e35e8786958c49a1259434e2088b9cniq dgn_sigma $ labDG (lookupDGraph ln libEnv') target
f82568a780e35e8786958c49a1259434e2088b9cniq morphism2' <- coerceMorphism (targetLogic cid) lid
f82568a780e35e8786958c49a1259434e2088b9cniq "checkconservativityOfEdge" morphism2
f82568a780e35e8786958c49a1259434e2088b9cniq morphism3' <- coerceMorphism (targetLogic cid') lid
f82568a780e35e8786958c49a1259434e2088b9cniq "checkconservativityOfEdge" morphism3
f82568a780e35e8786958c49a1259434e2088b9cniq let compMor = case comp morphism2' morphism3' of
f82568a780e35e8786958c49a1259434e2088b9cniq Res.Result _ (Just phi) -> phi
f82568a780e35e8786958c49a1259434e2088b9cniq _ -> error "checkconservativtiyOfEdge: comp"
f82568a780e35e8786958c49a1259434e2088b9cniq let (_le', thSrc) =
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq case computeTheory False libEnv' (gi_LIB_NAME gInfo) source of
f82568a780e35e8786958c49a1259434e2088b9cniq Res.Result _ (Just th1) -> th1
f82568a780e35e8786958c49a1259434e2088b9cniq _ -> error "checkconservativityOfEdge: computeTheory"
f82568a780e35e8786958c49a1259434e2088b9cniq G_theory lid1 sign1 _ sensSrc1 _ <- return thSrc
f82568a780e35e8786958c49a1259434e2088b9cniq sign2 <- coerceSign lid1 lid "checkconservativityOfEdge.coerceSign" sign1
f82568a780e35e8786958c49a1259434e2088b9cniq sensSrc2 <- coerceThSens lid1 lid "" sensSrc1
f82568a780e35e8786958c49a1259434e2088b9cniq let transSensSrc =
f82568a780e35e8786958c49a1259434e2088b9cniq mapThSensValue (propagateErrors . map_sen lid compMor) sensSrc2
f82568a780e35e8786958c49a1259434e2088b9cniq let Res.Result ds res =
f82568a780e35e8786958c49a1259434e2088b9cniq conservativityCheck lid
f82568a780e35e8786958c49a1259434e2088b9cniq (plainSign sign2, toNamedList sensSrc2)
f82568a780e35e8786958c49a1259434e2088b9cniq compMor $ toNamedList (sensTar `OMap.difference` transSensSrc)
f82568a780e35e8786958c49a1259434e2088b9cniq showObls [] = ""
f82568a780e35e8786958c49a1259434e2088b9cniq showObls obls = ", provided that the following proof obligations "
f82568a780e35e8786958c49a1259434e2088b9cniq ++"can be discharged:\n"
f82568a780e35e8786958c49a1259434e2088b9cniq ++ concatMap ((++"\n").flip showDoc "") obls
f82568a780e35e8786958c49a1259434e2088b9cniq showRes = case res of
f82568a780e35e8786958c49a1259434e2088b9cniq Just (Just (Inconsistent,obls)) ->
f82568a780e35e8786958c49a1259434e2088b9cniq "The link is not conservative"++showObls obls
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq Just (Just (Conservative,obls)) ->
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq "The link is conservative"++showObls obls
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq Just (Just (Monomorphic,obls)) ->
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq "The link is monomorphic"++showObls obls
f82568a780e35e8786958c49a1259434e2088b9cniq Just (Just (Definitional,obls)) ->
f82568a780e35e8786958c49a1259434e2088b9cniq "The link is definitional"++showObls obls
f82568a780e35e8786958c49a1259434e2088b9cniq _ -> "Could not determine whether link is conservative"
f82568a780e35e8786958c49a1259434e2088b9cniq myDiags = showRelDiags 2 ds
f82568a780e35e8786958c49a1259434e2088b9cniq createTextDisplay "Result of conservativity check"
f82568a780e35e8786958c49a1259434e2088b9cniq (showRes ++ "\n" ++ myDiags) [HTk.size(50,50)]
f82568a780e35e8786958c49a1259434e2088b9cniq let newGr = lookupDGraph ln libEnv'
f82568a780e35e8786958c49a1259434e2088b9cniq newHistory = proofHistory newGr
f82568a780e35e8786958c49a1259434e2088b9cniq oldHistory = proofHistory $ lookupDGraph ln libEnv
f82568a780e35e8786958c49a1259434e2088b9cniq history = take (length newHistory - length oldHistory) newHistory
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq applyChanges actGraphInfo history
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq writeIORef le libEnv'
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq unlockGlobal gInfo
f82568a780e35e8786958c49a1259434e2088b9cniqcheckconservativityOfEdge descr _ Nothing =
f82568a780e35e8786958c49a1259434e2088b9cniq createTextDisplay "Error"
f82568a780e35e8786958c49a1259434e2088b9cniq ("edge " ++ show descr ++ " has no corresponding edge "
f82568a780e35e8786958c49a1259434e2088b9cniq ++ "in the development graph") [HTk.size(30,10)]
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq-- | converts a DGraph
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniqconvert :: GA.GraphInfo -> DGraph -> IO ()
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniqconvert ginfo dgraph = do
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq convertNodes ginfo dgraph
f82568a780e35e8786958c49a1259434e2088b9cniq convertEdges ginfo dgraph
f82568a780e35e8786958c49a1259434e2088b9cniq{- | converts the nodes of the development graph, if it has any,
f82568a780e35e8786958c49a1259434e2088b9cniqand returns the resulting conversion maps
f82568a780e35e8786958c49a1259434e2088b9cniqif the graph is empty the conversion maps are returned unchanged-}
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniqconvertNodes :: GA.GraphInfo -> DGraph -> IO ()
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniqconvertNodes ginfo = mapM_ (convertNodesAux ginfo) .labNodesDG
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq{- | auxiliary function for convertNodes if the given list of nodes is
f82568a780e35e8786958c49a1259434e2088b9cniqemtpy, it returns the conversion maps unchanged otherwise it adds the
f82568a780e35e8786958c49a1259434e2088b9cniqconverted first node to the abstract graph and to the affected
f82568a780e35e8786958c49a1259434e2088b9cniqconversion maps and afterwards calls itself with the remaining node
f82568a780e35e8786958c49a1259434e2088b9cniqconvertNodesAux :: GA.GraphInfo -> LNode DGNodeLab -> IO ()
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniqconvertNodesAux ginfo (node, dgnode) =
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq GA.addNode ginfo node (getRealDGNodeType dgnode) $ getDGNodeName dgnode
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq{- | converts the edges of the development graph
f82568a780e35e8786958c49a1259434e2088b9cniqworks the same way as convertNods does-}
f82568a780e35e8786958c49a1259434e2088b9cniqconvertEdges :: GA.GraphInfo -> DGraph -> IO ()
f82568a780e35e8786958c49a1259434e2088b9cniqconvertEdges ginfo = mapM_ (convertEdgesAux ginfo) . labEdgesDG
f82568a780e35e8786958c49a1259434e2088b9cniq-- | auxiliary function for convertEges
f82568a780e35e8786958c49a1259434e2088b9cniqconvertEdgesAux :: GA.GraphInfo -> LEdge DGLinkLab -> IO ()
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniqconvertEdgesAux ginfo e@(src, tar, lbl) =
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq GA.addEdge ginfo (dgl_id lbl) (getRealDGLinkType lbl) src tar "" $ Just e
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq-- | show library referened by a DGRef node (=node drawn as a box)
f82568a780e35e8786958c49a1259434e2088b9cniqshowReferencedLibrary :: Int -> GInfo -> ConvFunc -> LibFunc -> IO ()
f82568a780e35e8786958c49a1259434e2088b9cniqshowReferencedLibrary descr gInfo@(GInfo { libEnvIORef = ioRefProofStatus
f82568a780e35e8786958c49a1259434e2088b9cniq , gi_LIB_NAME = ln })
f82568a780e35e8786958c49a1259434e2088b9cniq convGraph showLib = do
f82568a780e35e8786958c49a1259434e2088b9cniq le <- readIORef ioRefProofStatus
f82568a780e35e8786958c49a1259434e2088b9cniq let refNode = labDG (lookupDGraph ln le) descr
f82568a780e35e8786958c49a1259434e2088b9cniq refLibname = if isDGRef refNode then dgn_libname refNode
f82568a780e35e8786958c49a1259434e2088b9cniq else error "showReferencedLibrary"
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq case Map.lookup refLibname le of
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq Just _ -> do
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq gInfo' <- copyGInfo gInfo refLibname
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq convGraph gInfo' "development graph" showLib
f82568a780e35e8786958c49a1259434e2088b9cniq let gv = gi_GraphInfo gInfo'
f82568a780e35e8786958c49a1259434e2088b9cniq hideNodes gInfo'
f82568a780e35e8786958c49a1259434e2088b9cniq GA.showTemporaryMessage gv "Development Graph initialized."
f82568a780e35e8786958c49a1259434e2088b9cniq Nothing -> error $ "The referenced library (" ++ show refLibname
f82568a780e35e8786958c49a1259434e2088b9cniq ++ ") is unknown"
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq-- | apply the changes of first history item (computed by proof rules,
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq-- see folder Proofs) to the displayed development graph
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniqapplyChanges :: GA.GraphInfo -> ProofHistory -> IO ()
f82568a780e35e8786958c49a1259434e2088b9cniqapplyChanges _ [] = return ()
f82568a780e35e8786958c49a1259434e2088b9cniqapplyChanges ginfo ((_, hElem) : _) = mapM_ (applyChangesAux ginfo)
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq $ removeContraryChanges hElem
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq-- | auxiliary function for applyChanges
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniqapplyChangesAux :: GA.GraphInfo -> DGChange -> IO ()
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniqapplyChangesAux ginfo change =
f82568a780e35e8786958c49a1259434e2088b9cniq case change of
f82568a780e35e8786958c49a1259434e2088b9cniq SetNodeLab _ (node, newLab) ->
f82568a780e35e8786958c49a1259434e2088b9cniq GA.changeNodeType ginfo node $ getRealDGNodeType newLab
f82568a780e35e8786958c49a1259434e2088b9cniq InsertNode (node, nodelab) ->
f82568a780e35e8786958c49a1259434e2088b9cniq GA.addNode ginfo node (getRealDGNodeType nodelab) $ getDGNodeName nodelab
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq DeleteNode (node, _) ->
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq InsertEdge e@(src, tgt, lbl) ->
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq GA.addEdge ginfo (dgl_id lbl) (getRealDGLinkType lbl) src tgt "" $ Just e
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq DeleteEdge (_, _, lbl) ->
f82568a780e35e8786958c49a1259434e2088b9cniq GA.delEdge ginfo $ dgl_id lbl
f82568a780e35e8786958c49a1259434e2088b9cniq-- | display a window of translated graph with maximal sublogic.
f82568a780e35e8786958c49a1259434e2088b9cniqopenTranslateGraph :: LibEnv -> LIB_NAME -> HetcatsOpts
f82568a780e35e8786958c49a1259434e2088b9cniq -> Res.Result G_sublogics -> ConvFunc -> LibFunc -> IO ()
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniqopenTranslateGraph libEnv ln opts (Res.Result diagsSl mSublogic) convGraph
f82568a780e35e8786958c49a1259434e2088b9cniq -- if an error existed by the search of maximal sublogicn
f82568a780e35e8786958c49a1259434e2088b9cniq -- (see GUI.DGTranslation.getDGLogic), the process need not to go on.
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq let myErrMess = showDiagMess opts in
f82568a780e35e8786958c49a1259434e2088b9cniq if hasErrors diagsSl then myErrMess diagsSl else case mSublogic of
f82568a780e35e8786958c49a1259434e2088b9cniq Nothing -> errorMess "the maximal sublogic is not found."
f82568a780e35e8786958c49a1259434e2088b9cniq Just sublogic -> do
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq let paths = findComorphismPaths logicGraph sublogic
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq if null paths then
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq errorMess "This graph has no comorphism to translation."
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq -- the user choose one
f82568a780e35e8786958c49a1259434e2088b9cniq sel <- listBox "Choose a logic translation"
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq $ map show paths
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq case sel of
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq Nothing -> warningMess "no logic translation chosen"
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq Just j -> do
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq -- graph translation.
f82568a780e35e8786958c49a1259434e2088b9cniq let Res.Result diagsTrans mLEnv =
f82568a780e35e8786958c49a1259434e2088b9cniq libEnv_translation libEnv $ paths !! j
f82568a780e35e8786958c49a1259434e2088b9cniq case mLEnv of
f82568a780e35e8786958c49a1259434e2088b9cniq Just newLibEnv -> do
f82568a780e35e8786958c49a1259434e2088b9cniq showDiagMess opts $ diagsSl ++ diagsTrans
f82568a780e35e8786958c49a1259434e2088b9cniq dg_showGraphAux
f82568a780e35e8786958c49a1259434e2088b9cniq (\gI@(GInfo{libEnvIORef = iorLE}) -> do
f82568a780e35e8786958c49a1259434e2088b9cniq writeIORef iorLE newLibEnv
f82568a780e35e8786958c49a1259434e2088b9cniq convGraph (gI{ gi_LIB_NAME = ln
f82568a780e35e8786958c49a1259434e2088b9cniq , gi_hetcatsOpts = opts})
f82568a780e35e8786958c49a1259434e2088b9cniq "translation Graph" showLib)
f82568a780e35e8786958c49a1259434e2088b9cniq Nothing -> myErrMess $ diagsSl ++ diagsTrans
f82568a780e35e8786958c49a1259434e2088b9cniqdg_showGraphAux :: (GInfo -> IO ()) -> IO ()
f82568a780e35e8786958c49a1259434e2088b9cniqdg_showGraphAux convFct = do
f82568a780e35e8786958c49a1259434e2088b9cniq useHTk -- All messages are displayed in TK dialog windows
f82568a780e35e8786958c49a1259434e2088b9cniq -- from this point on
f82568a780e35e8786958c49a1259434e2088b9cniq gInfo <- emptyGInfo
f82568a780e35e8786958c49a1259434e2088b9cniq convFct gInfo
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq let actGraphInfo = gi_GraphInfo gInfo
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq GA.redisplay actGraphInfo
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq-- DaVinciGraph to String
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq-- Functions to convert a DaVinciGraph to a String to store as a .udg file
f82568a780e35e8786958c49a1259434e2088b9cniq-- | saves the uDrawGraph graph to a file
f82568a780e35e8786958c49a1259434e2088b9cniqsaveUDGraph :: GInfo -> Map.Map DGNodeType (Shape value, String)
f82568a780e35e8786958c49a1259434e2088b9cniq -> Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String) -> IO ()
f82568a780e35e8786958c49a1259434e2088b9cniqsaveUDGraph gInfo@(GInfo { gi_GraphInfo = graphInfo
f82568a780e35e8786958c49a1259434e2088b9cniq , gi_LIB_NAME = ln
f82568a780e35e8786958c49a1259434e2088b9cniq , gi_hetcatsOpts = opts
f82568a780e35e8786958c49a1259434e2088b9cniq }) nodemap linkmap = do
f82568a780e35e8786958c49a1259434e2088b9cniq evnt <- newFileDialogStr "Save as..."
f82568a780e35e8786958c49a1259434e2088b9cniq $ (rmSuffix $ libNameToFile opts ln) ++ ".udg"
f82568a780e35e8786958c49a1259434e2088b9cniq maybeFilePath <- HTk.sync evnt
f82568a780e35e8786958c49a1259434e2088b9cniq case maybeFilePath of
f82568a780e35e8786958c49a1259434e2088b9cniq Just filepath -> do
f82568a780e35e8786958c49a1259434e2088b9cniq GA.showTemporaryMessage graphInfo "Converting graph..."
f82568a780e35e8786958c49a1259434e2088b9cniq nstring <- nodes2String gInfo nodemap linkmap
f82568a780e35e8786958c49a1259434e2088b9cniq writeFile filepath nstring
f82568a780e35e8786958c49a1259434e2088b9cniq GA.showTemporaryMessage graphInfo $ "Graph stored to " ++ filepath ++ "!"
f82568a780e35e8786958c49a1259434e2088b9cniq Nothing -> GA.showTemporaryMessage graphInfo $ "Aborted!"
f82568a780e35e8786958c49a1259434e2088b9cniq-- | Converts the nodes of the graph to String representation
f82568a780e35e8786958c49a1259434e2088b9cniqnodes2String :: GInfo -> Map.Map DGNodeType (Shape value, String)
f82568a780e35e8786958c49a1259434e2088b9cniq -> Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String)
f82568a780e35e8786958c49a1259434e2088b9cniq -> IO String
f82568a780e35e8786958c49a1259434e2088b9cniqnodes2String gInfo@(GInfo { gi_GraphInfo = graphInfo
5bfaaf573bacb45c1cf290ce85ecc676587e8a64jim , gi_LIB_NAME = ln
f82568a780e35e8786958c49a1259434e2088b9cniq , libEnvIORef = ioRefProofStatus
f82568a780e35e8786958c49a1259434e2088b9cniq }) nodemap linkmap = do
f82568a780e35e8786958c49a1259434e2088b9cniq le <- readIORef ioRefProofStatus
f82568a780e35e8786958c49a1259434e2088b9cniq nodes <- filterM (\(n,_) -> do b <- GA.isHiddenNode graphInfo n
f82568a780e35e8786958c49a1259434e2088b9cniq return $ not b)
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq $ labNodesDG $ lookupDGraph ln le
f82568a780e35e8786958c49a1259434e2088b9cniq nstring <- foldM (\s node -> do
f82568a780e35e8786958c49a1259434e2088b9cniq s' <- (node2String gInfo nodemap linkmap node)
f82568a780e35e8786958c49a1259434e2088b9cniq return $ s ++ (if s /= "" then ",\n " else "") ++ s')
f82568a780e35e8786958c49a1259434e2088b9cniq return $ "[" ++ nstring ++ "]"
f82568a780e35e8786958c49a1259434e2088b9cniq-- | Converts a node to String representation
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniqnode2String :: GInfo -> Map.Map DGNodeType (Shape value, String)
f82568a780e35e8786958c49a1259434e2088b9cniq -> Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String)
f82568a780e35e8786958c49a1259434e2088b9cniq -> LNode DGNodeLab -> IO String
f82568a780e35e8786958c49a1259434e2088b9cniqnode2String gInfo nodemap linkmap (nid, dgnode) = do
f82568a780e35e8786958c49a1259434e2088b9cniq label <- getNodeLabel gInfo dgnode
f82568a780e35e8786958c49a1259434e2088b9cniq let ntype = getRealDGNodeType dgnode
f82568a780e35e8786958c49a1259434e2088b9cniq (shape, color) <- case Map.lookup ntype nodemap of
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq Nothing -> error $ "SaveGraph: can't lookup nodetype: " ++ show ntype
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq Just (s, c) -> return (s, c)
f82568a780e35e8786958c49a1259434e2088b9cniq object = "a(\"OBJECT\",\"" ++ label ++ "\"),"
f82568a780e35e8786958c49a1259434e2088b9cniq color' = "a(\"COLOR\",\"" ++ color ++ "\"),"
f82568a780e35e8786958c49a1259434e2088b9cniq shape' = "a(\"_GO\",\"" ++ (map toLower $ show shape) ++ "\")"
f82568a780e35e8786958c49a1259434e2088b9cniq links <- links2String gInfo linkmap nid
f82568a780e35e8786958c49a1259434e2088b9cniq return $ "l(\"" ++ (show nid) ++ "\",n(\"" ++ show ntype ++ "\","
f82568a780e35e8786958c49a1259434e2088b9cniq ++ "[" ++ object ++ color' ++ shape' ++ "],"
f82568a780e35e8786958c49a1259434e2088b9cniq ++ "\n [" ++ links ++ "]))"
f82568a780e35e8786958c49a1259434e2088b9cniq-- | Converts all links of a node to String representation
f82568a780e35e8786958c49a1259434e2088b9cniqlinks2String :: GInfo -> Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String)
f82568a780e35e8786958c49a1259434e2088b9cniq -> Int -> IO String
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniqlinks2String (GInfo { gi_GraphInfo = graphInfo
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq , gi_LIB_NAME = ln
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq , libEnvIORef = ioRefProofStatus
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq }) linkmap nodeid = do
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq le <- readIORef ioRefProofStatus
f82568a780e35e8786958c49a1259434e2088b9cniq edges <- filterM (\(src,_,edge) -> do
f82568a780e35e8786958c49a1259434e2088b9cniq let eid = dgl_id edge
f82568a780e35e8786958c49a1259434e2088b9cniq b <- GA.isHiddenEdge graphInfo eid
f82568a780e35e8786958c49a1259434e2088b9cniq return $ (not b) && src == nodeid)
f82568a780e35e8786958c49a1259434e2088b9cniq $ labEdgesDG $ lookupDGraph ln le
f82568a780e35e8786958c49a1259434e2088b9cniq foldM (\s edge -> do
f82568a780e35e8786958c49a1259434e2088b9cniq s' <- link2String linkmap edge
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq return $ s ++ (if s /= "" then ",\n " else "") ++ s') "" edges
f82568a780e35e8786958c49a1259434e2088b9cniq-- | Converts a link to String representation
f82568a780e35e8786958c49a1259434e2088b9cniqlink2String :: Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String)
f82568a780e35e8786958c49a1259434e2088b9cniq -> LEdge DGLinkLab -> IO String
f82568a780e35e8786958c49a1259434e2088b9cniqlink2String linkmap (nodeid1, nodeid2, edge) = do
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq let (EdgeId linkid) = dgl_id edge
f82568a780e35e8786958c49a1259434e2088b9cniq ltype = getRealDGLinkType edge
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq (line, color) <- case Map.lookup ltype linkmap of
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq Nothing -> error $ "SaveGraph: can't lookup linktype: " ++ show ltype
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq Just (l, c) -> return (l, c)
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq name = "\"" ++ (show linkid) ++ ":" ++ (show nodeid1) ++ "->"
0134ffd85f3bcfd84cf0bea0f4b797a885eb78adniq ++ (show nodeid2) ++ "\""
f82568a780e35e8786958c49a1259434e2088b9cniq color' = "a(\"EDGECOLOR\",\"" ++ color ++ "\"),"
f82568a780e35e8786958c49a1259434e2088b9cniq line' = "a(\"EDGEPATTERN\",\"" ++ (map toLower $ show line) ++ "\")"