GraphLogic.hs revision c34e6d82f6b05bb950e168609ae8c0406c854d87
97a9a944b5887e91042b019776c41d5dd74557aferikabeleModule : $Header$
97a9a944b5887e91042b019776c41d5dd74557aferikabeleDescription : Logic for manipulating the graph in the Central GUI
a945f35eff8b6a88009ce73de6d4c862ce58de3csliveCopyright : (c) Jorina Freya Gerken, Till Mossakowski, Uni Bremen 2002-2006
a945f35eff8b6a88009ce73de6d4c862ce58de3csliveLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
fe64b2ba25510d8c9dba5560a2d537763566cf40ndMaintainer : till@informatik.uni-bremen.de
fe64b2ba25510d8c9dba5560a2d537763566cf40ndStability : provisional
fe64b2ba25510d8c9dba5560a2d537763566cf40ndPortability : non-portable (imports Logic)
fe64b2ba25510d8c9dba5560a2d537763566cf40ndThis module provides functions for all the menus in the Hets GUI.
fe64b2ba25510d8c9dba5560a2d537763566cf40ndThese are then assembled to the GUI in "GUI.GraphMenu".
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , performProofAction
4b5981e276e93df97c34e4da05ca5cf8bbd937dand , openProofStatus
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , saveProofStatus
3b3b7fc78d1f5bfc2769903375050048ff41ff26nd , proofMenu
ad74a0524a06bfe11b7de9e3b4ce7233ab3bd3f7nd , openTranslateGraph
4aa805f8500255bc52a4c03259fe46df10a1d07cyoshiki , showReferencedLibrary
3b3b7fc78d1f5bfc2769903375050048ff41ff26nd , getTheoryOfNode
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , translateTheoryOfNode
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , displaySubsortGraph
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , displayConceptGraph
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , lookupTheoryOfNode
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , getSublogicOfNode
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , showProofStatusOfNode
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna , proveAtNode
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , showNodeInfo
117c1f888a14e73cdd821dc6c23eb0411144a41cnd , showEdgeInfo
117c1f888a14e73cdd821dc6c23eb0411144a41cnd , checkconservativityOfEdge
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd , hideNodes
117c1f888a14e73cdd821dc6c23eb0411144a41cnd , getLibDeps
117c1f888a14e73cdd821dc6c23eb0411144a41cnd , hideShowNames
117c1f888a14e73cdd821dc6c23eb0411144a41cnd , showNodes
117c1f888a14e73cdd821dc6c23eb0411144a41cnd , translateGraph
117c1f888a14e73cdd821dc6c23eb0411144a41cnd , showLibGraph
117c1f888a14e73cdd821dc6c23eb0411144a41cnd , runAndLock
117c1f888a14e73cdd821dc6c23eb0411144a41cnd , saveUDGraph
117c1f888a14e73cdd821dc6c23eb0411144a41cnd , focusNode
5f86589186bcc15ee13e288a9d73acbeab2409fbdpejesh , applyChanges
117c1f888a14e73cdd821dc6c23eb0411144a41cnd , applyTypeChanges
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport Logic.Logic(conservativityCheck)
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport Logic.Coerce(coerceSign, coerceMorphism)
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport Comorphisms.LogicGraph(logicGraph)
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport Syntax.AS_Library(LIB_NAME, getModTime, getLIB_ID)
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport Static.DGToSpec(dgToSpec, computeTheory)
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport Static.AnalysisLibrary(anaLibExt, anaLib)
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport Static.DGTranslation(libEnv_translation)
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport Proofs.InferBasic(basicInferenceNode)
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport Proofs.StatusUtils(lookupHistory, removeContraryChanges)
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport GUI.Utils (listBox)
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport GUI.Taxonomy (displayConceptGraph,displaySubsortGraph)
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport GUI.DGTranslation(getDGLogic)
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport qualified GUI.GraphAbstraction as GA
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport qualified GUI.HTkUtils (displayTheoryWithWarning,
117c1f888a14e73cdd821dc6c23eb0411144a41cnd createInfoDisplayWithTwoButtons)
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport GraphConfigure
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport TextDisplay(createTextDisplay)
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport InfoBus(encapsulateWaitTermAct)
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport DialogWin (useHTk)
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport Messages(errorMess)
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport qualified HTk
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport Configuration(size)
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport FileDialog(newFileDialogStr)
b00fe3c3354db01001b8eddfd9b88441380f837dwroweimport Common.DocUtils(showDoc, pretty)
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport Common.Doc(vcat)
a38b5f73e7f0f3b8726fb47d27b145f37036ead0jimimport Common.ResultT(liftR, runResultT)
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport Common.AS_Annotation(isAxiom)
fe64b2ba25510d8c9dba5560a2d537763566cf40ndimport Common.Result as Res
fe64b2ba25510d8c9dba5560a2d537763566cf40ndimport qualified Common.OrderedMap as OMap
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquernaimport qualified Common.Lib.Rel as Rel
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquernaimport Driver.WriteFn(writeShATermFile)
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquernaimport Driver.ReadFn(libNameToFile, readVerbose)
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquernaimport System.Directory(getModificationTime)
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquernaimport Data.Char(toLower)
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquernaimport Data.Maybe(fromJust)
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquernaimport Data.List(find, delete, partition)
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquernaimport Data.Graph.Inductive.Graph (Node, LEdge, LNode, lab', labNodes, (&))
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquernaimport qualified Data.Map as Map
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquernaimport Control.Monad(foldM, filterM)
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna-- | Locks the global lock and runs function
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquernarunAndLock :: GInfo -> IO () -> IO ()
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquernarunAndLock (GInfo { functionLock = lock
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna , gi_GraphInfo = actGraph
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna }) function = do
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna locked <- tryPutMVar lock ()
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna case locked of
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna _ <- takeMVar lock
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna False -> do
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna GA.showTemporaryMessage actGraph $ "an other function is still working"
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna ++ "... please wait ..."
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna-- | negate change
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquernanegateChange :: DGChange -> DGChange
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquernanegateChange change = case change of
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna InsertNode x -> DeleteNode x
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna DeleteNode x -> InsertNode x
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna InsertEdge x -> DeleteEdge x
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna DeleteEdge x -> InsertEdge x
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna SetNodeLab old (node, new) -> SetNodeLab new (node, old)
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna-- | Undo one step of the History
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquernaundo :: GInfo -> Bool -> IO ()
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquernaundo gInfo@(GInfo { globalHist = gHist
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna , gi_GraphInfo = actGraph
ea52f92bf226f48638d3e0e0b0e03568c8e7c5a9noirin }) isUndo = do
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna (guHist, grHist) <- takeMVar gHist
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna case if isUndo then guHist else grHist of
fe64b2ba25510d8c9dba5560a2d537763566cf40nd GA.showTemporaryMessage actGraph "History is empty..."
fe64b2ba25510d8c9dba5560a2d537763566cf40nd putMVar gHist (guHist, grHist)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd (lns:gHist') -> do
fe64b2ba25510d8c9dba5560a2d537763566cf40nd undoDGraphs gInfo isUndo lns
fe64b2ba25510d8c9dba5560a2d537763566cf40nd putMVar gHist $ if isUndo then (gHist', reverse lns : grHist)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd else (reverse lns : guHist, gHist')
fe64b2ba25510d8c9dba5560a2d537763566cf40ndundoDGraphs :: GInfo -> Bool -> [LIB_NAME] -> IO ()
fe64b2ba25510d8c9dba5560a2d537763566cf40ndundoDGraphs _ _ [] = return ()
fe64b2ba25510d8c9dba5560a2d537763566cf40ndundoDGraphs g u (ln:r) = do
c985aca104389df30d6ec0a637ce0ccaac904362nd undoDGraph g u ln
fe64b2ba25510d8c9dba5560a2d537763566cf40nd undoDGraphs g u r
06ba4a61654b3763ad65f52283832ebf058fdf1csliveundoDGraph :: GInfo -> Bool -> LIB_NAME -> IO ()
06ba4a61654b3763ad65f52283832ebf058fdf1csliveundoDGraph gInfo@(GInfo { libEnvIORef = ioRefProofStatus
06ba4a61654b3763ad65f52283832ebf058fdf1cslive , gi_GraphInfo = actGraph
06ba4a61654b3763ad65f52283832ebf058fdf1cslive }) isUndo ln = do
fb77c505254b6e9c925e23e734463e87574f8f40kess GA.showTemporaryMessage actGraph $ "Undo last change to " ++ show ln ++ "..."
fb77c505254b6e9c925e23e734463e87574f8f40kess lockGlobal gInfo
06ba4a61654b3763ad65f52283832ebf058fdf1cslive le <- readIORef ioRefProofStatus
06ba4a61654b3763ad65f52283832ebf058fdf1cslive dg = lookupDGraph ln le
06ba4a61654b3763ad65f52283832ebf058fdf1cslive hist = (proofHistory dg, redoHistory dg)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive swap (a, b) = (b, a)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive (phist, rhist) = (if isUndo then id else swap) hist
fb77c505254b6e9c925e23e734463e87574f8f40kess (cl@(rs, cs), newHist) = case phist of
06ba4a61654b3763ad65f52283832ebf058fdf1cslive hd : tl -> (hd, (tl, hd : rhist))
06ba4a61654b3763ad65f52283832ebf058fdf1cslive _ -> error "undoDGraph"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive (newPHist, newRHist) = (if isUndo then id else swap) newHist
06ba4a61654b3763ad65f52283832ebf058fdf1cslive change = if isUndo then (reverse rs, reverse $ map negateChange cs)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive dg' = (changesDG dg $ snd change)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive { proofHistory = newPHist
06ba4a61654b3763ad65f52283832ebf058fdf1cslive , redoHistory = newRHist }
06ba4a61654b3763ad65f52283832ebf058fdf1cslive writeIORef ioRefProofStatus $ Map.insert ln dg' le
06ba4a61654b3763ad65f52283832ebf058fdf1cslive case openlock dg' of
fb77c505254b6e9c925e23e734463e87574f8f40kess Nothing -> return ()
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Just lock -> do
06ba4a61654b3763ad65f52283832ebf058fdf1cslive mvar <- tryTakeMVar lock
06ba4a61654b3763ad65f52283832ebf058fdf1cslive case mvar of
fb77c505254b6e9c925e23e734463e87574f8f40kess Nothing -> return ()
fb77c505254b6e9c925e23e734463e87574f8f40kess Just applyHist -> do
06ba4a61654b3763ad65f52283832ebf058fdf1cslive applyHist [change]
fb77c505254b6e9c925e23e734463e87574f8f40kess putMVar lock applyHist
bc4b55ec8f31569d606d5680d50189a355bcd7a6rbowen unlockGlobal gInfo
06ba4a61654b3763ad65f52283832ebf058fdf1cslive-- | reloads the Library of the DevGraph
06ba4a61654b3763ad65f52283832ebf058fdf1cslivereload :: GInfo -> IO()
06ba4a61654b3763ad65f52283832ebf058fdf1cslivereload gInfo@(GInfo { libEnvIORef = ioRefProofStatus
06ba4a61654b3763ad65f52283832ebf058fdf1cslive , gi_LIB_NAME = ln
fb77c505254b6e9c925e23e734463e87574f8f40kess , gi_hetcatsOpts = opts
06ba4a61654b3763ad65f52283832ebf058fdf1cslive lockGlobal gInfo
fb77c505254b6e9c925e23e734463e87574f8f40kess oldle <- readIORef ioRefProofStatus
06ba4a61654b3763ad65f52283832ebf058fdf1cslive libdeps = Rel.toList $ Rel.intransKernel $ Rel.transClosure $ Rel.fromList
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd $ getLibDeps oldle
130d299c4b2b15be45532a176604c71fdc7bea5bnd ioruplibs <- newIORef ([] :: [LIB_NAME])
130d299c4b2b15be45532a176604c71fdc7bea5bnd writeIORef ioruplibs []
130d299c4b2b15be45532a176604c71fdc7bea5bnd reloadLibs ioRefProofStatus opts libdeps ioruplibs ln
130d299c4b2b15be45532a176604c71fdc7bea5bnd unlockGlobal gInfo
130d299c4b2b15be45532a176604c71fdc7bea5bnd remakeGraph gInfo
130d299c4b2b15be45532a176604c71fdc7bea5bnd-- | Creates a list of all LIB_NAME pairs, which have a dependency
130d299c4b2b15be45532a176604c71fdc7bea5bndgetLibDeps :: LibEnv -> [(LIB_NAME, LIB_NAME)]
130d299c4b2b15be45532a176604c71fdc7bea5bndgetLibDeps le =
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd concat $ map (\ ln -> getDep ln le) $ Map.keys le
fe64b2ba25510d8c9dba5560a2d537763566cf40nd-- | Creates a list of LIB_NAME pairs for the fist argument
fe64b2ba25510d8c9dba5560a2d537763566cf40ndgetDep :: LIB_NAME -> LibEnv -> [(LIB_NAME, LIB_NAME)]
fe64b2ba25510d8c9dba5560a2d537763566cf40ndgetDep ln le = map (\ (_, x) -> (ln, dgn_libname x)) $
fe64b2ba25510d8c9dba5560a2d537763566cf40nd filter (isDGRef . snd) $ labNodes $ dgBody $ lookupDGraph ln le
fe64b2ba25510d8c9dba5560a2d537763566cf40nd-- | Reloads a library
fe64b2ba25510d8c9dba5560a2d537763566cf40ndreloadLib :: IORef LibEnv -> HetcatsOpts -> IORef [LIB_NAME] -> LIB_NAME
fe64b2ba25510d8c9dba5560a2d537763566cf40ndreloadLib iorle opts ioruplibs ln = do
fe64b2ba25510d8c9dba5560a2d537763566cf40nd mfile <- existsAnSource opts {intype = GuessIn}
fe64b2ba25510d8c9dba5560a2d537763566cf40nd $ rmSuffix $ libNameToFile opts ln
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess case mfile of
ff797e743eb73c1d45b08158aa6b288c2d0c46eeslive Nothing -> do
6b64034fa2a644ba291c484c0c01c7df5b8d982ckess Just file -> do
6b64034fa2a644ba291c484c0c01c7df5b8d982ckess le <- readIORef iorle
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd le' = Map.delete ln le
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd mres <- anaLibExt opts file le'
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd case mres of
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Just (_, newle) -> do
06ba4a61654b3763ad65f52283832ebf058fdf1cslive uplibs <- readIORef ioruplibs
06ba4a61654b3763ad65f52283832ebf058fdf1cslive writeIORef ioruplibs $ ln:uplibs
06ba4a61654b3763ad65f52283832ebf058fdf1cslive writeIORef iorle newle
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Nothing -> do
06ba4a61654b3763ad65f52283832ebf058fdf1cslive errorMess $ "Could not read original development graph from '"++ file
130d299c4b2b15be45532a176604c71fdc7bea5bnd-- | Reloads libraries if nessesary
130d299c4b2b15be45532a176604c71fdc7bea5bndreloadLibs :: IORef LibEnv -> HetcatsOpts -> [(LIB_NAME, LIB_NAME)]
130d299c4b2b15be45532a176604c71fdc7bea5bnd -> IORef [LIB_NAME] -> LIB_NAME -> IO Bool
130d299c4b2b15be45532a176604c71fdc7bea5bndreloadLibs iorle opts deps ioruplibs ln = do
fe64b2ba25510d8c9dba5560a2d537763566cf40nd uplibs <- readIORef ioruplibs
fe64b2ba25510d8c9dba5560a2d537763566cf40nd case elem ln uplibs of
fe64b2ba25510d8c9dba5560a2d537763566cf40nd True -> return True
fe64b2ba25510d8c9dba5560a2d537763566cf40nd False -> do
fe64b2ba25510d8c9dba5560a2d537763566cf40nd deps' = map (snd) $ filter (\ (ln',_) -> ln == ln') deps
fe64b2ba25510d8c9dba5560a2d537763566cf40nd res <- mapM (reloadLibs iorle opts deps ioruplibs) deps'
fe64b2ba25510d8c9dba5560a2d537763566cf40nd libupdate = foldl (\ u r -> if r then True else u) False res
fe64b2ba25510d8c9dba5560a2d537763566cf40nd case libupdate of
fe64b2ba25510d8c9dba5560a2d537763566cf40nd True -> do
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd reloadLib iorle opts ioruplibs ln
627c978514c54179736d152923478be7c8707f9bnd return True
fe64b2ba25510d8c9dba5560a2d537763566cf40nd False -> do
fe64b2ba25510d8c9dba5560a2d537763566cf40nd le <- readIORef iorle
fe64b2ba25510d8c9dba5560a2d537763566cf40nd newln:_ = filter (ln ==) $ Map.keys le
fe64b2ba25510d8c9dba5560a2d537763566cf40nd mfile <- existsAnSource opts $ rmSuffix $ libNameToFile opts ln
fe64b2ba25510d8c9dba5560a2d537763566cf40nd case mfile of
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Nothing -> do
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd return False
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd Just file -> do
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd newmt <- getModificationTime file
b95ae799514ad86a15610ad75808d7065e9847c9kess libupdate' = (getModTime $ getLIB_ID newln) < newmt
888b616027180cc8aaa4d2bee5ecc6acec175bc5nd case libupdate' of
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd False -> return False
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd True -> do
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd reloadLib iorle opts ioruplibs ln
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd return True
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd-- | Deletes the old edges and nodes of the Graph and makes new ones
5224ff8eae5156a05f676f1dad8add2e2f2efe1dndremakeGraph :: GInfo -> IO ()
06ba4a61654b3763ad65f52283832ebf058fdf1csliveremakeGraph (GInfo { libEnvIORef = ioRefProofStatus
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd , gi_LIB_NAME = ln
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd , gi_GraphInfo = actGraphInfo
fe64b2ba25510d8c9dba5560a2d537763566cf40nd le <- readIORef ioRefProofStatus
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd dgraph = lookupDGraph ln le
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd GA.clear actGraphInfo
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd convert actGraphInfo dgraph
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd GA.redisplay actGraphInfo
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd-- | Toggles to display internal node names
5224ff8eae5156a05f676f1dad8add2e2f2efe1dndhideShowNames :: GInfo -> Bool -> IO ()
5224ff8eae5156a05f676f1dad8add2e2f2efe1dndhideShowNames (GInfo { gi_GraphInfo = actGraphInfo
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd , internalNamesIORef = showInternalNames
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd }) toggle = do
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd (intrn::InternalNames) <- readIORef showInternalNames
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd let showThem = if toggle then not $ showNames intrn else showNames intrn
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd showItrn s = if showThem then s else ""
fe64b2ba25510d8c9dba5560a2d537763566cf40nd mapM_ (\(s,upd) -> upd (\_ -> showItrn s)) $ updater intrn
fe64b2ba25510d8c9dba5560a2d537763566cf40nd writeIORef showInternalNames $ intrn {showNames = showThem}
fe64b2ba25510d8c9dba5560a2d537763566cf40nd GA.redisplay actGraphInfo
fb77c505254b6e9c925e23e734463e87574f8f40kess-- | shows all hidden nodes and edges
fb77c505254b6e9c925e23e734463e87574f8f40kessshowNodes :: GInfo -> IO ()
fe64b2ba25510d8c9dba5560a2d537763566cf40ndshowNodes gInfo@(GInfo { gi_GraphInfo = actGraphInfo
fe64b2ba25510d8c9dba5560a2d537763566cf40nd hhn <- GA.hasHiddenNodes actGraphInfo
6fe26506780e73be2a412d758af77fafdf03291and case hhn of
fe64b2ba25510d8c9dba5560a2d537763566cf40nd True -> do
58699879a562774640b95e9eedfd891f336e38c2nd GA.showTemporaryMessage actGraphInfo "Revealing hidden nodes ..."
6fe26506780e73be2a412d758af77fafdf03291and GA.showAll actGraphInfo
6fe26506780e73be2a412d758af77fafdf03291and hideShowNames gInfo False
6fe26506780e73be2a412d758af77fafdf03291and False -> do
58699879a562774640b95e9eedfd891f336e38c2nd GA.showTemporaryMessage actGraphInfo "No hidden nodes found ..."
fb77c505254b6e9c925e23e734463e87574f8f40kess GA.redisplay actGraphInfo
fb77c505254b6e9c925e23e734463e87574f8f40kess-- | hides all unnamed internal nodes that are proven
fb77c505254b6e9c925e23e734463e87574f8f40kesshideNodes :: GInfo -> IO ()
58699879a562774640b95e9eedfd891f336e38c2ndhideNodes (GInfo { libEnvIORef = ioRefProofStatus
58699879a562774640b95e9eedfd891f336e38c2nd , gi_LIB_NAME = ln
58699879a562774640b95e9eedfd891f336e38c2nd , gi_GraphInfo = actGraphInfo
6b64034fa2a644ba291c484c0c01c7df5b8d982ckess hhn <- GA.hasHiddenNodes actGraphInfo
6b64034fa2a644ba291c484c0c01c7df5b8d982ckess case hhn of
58699879a562774640b95e9eedfd891f336e38c2nd True -> do
6b64034fa2a644ba291c484c0c01c7df5b8d982ckess GA.showTemporaryMessage actGraphInfo "Nodes already hidden ..."
58699879a562774640b95e9eedfd891f336e38c2nd False -> do
fb77c505254b6e9c925e23e734463e87574f8f40kess GA.showTemporaryMessage actGraphInfo "Hiding unnamed nodes..."
fb77c505254b6e9c925e23e734463e87574f8f40kess le <- readIORef ioRefProofStatus
fb77c505254b6e9c925e23e734463e87574f8f40kess let dg = lookupDGraph ln le
58699879a562774640b95e9eedfd891f336e38c2nd nodes = selectNodesByType dg [LocallyEmptyProvenConsInternal]
58699879a562774640b95e9eedfd891f336e38c2nd edges = getCompressedEdges dg nodes
58699879a562774640b95e9eedfd891f336e38c2nd GA.hideNodes actGraphInfo nodes edges
58699879a562774640b95e9eedfd891f336e38c2nd GA.redisplay actGraphInfo
58699879a562774640b95e9eedfd891f336e38c2nd-- | selects all nodes of a type with outgoing edges
58699879a562774640b95e9eedfd891f336e38c2ndselectNodesByType :: DGraph -> [DGNodeType] -> [Node]
58699879a562774640b95e9eedfd891f336e38c2ndselectNodesByType dg types =
58699879a562774640b95e9eedfd891f336e38c2nd filter (\ n -> outDG dg n /= []) $ map fst
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess $ filter (\ (_, n) -> elem (getRealDGNodeType n) types) $ labNodesDG dg
9b5e2c5e769dc678a1aca06df75c32022b2f1492trawick-- | compresses a list of types to the highest one
20189240503ef2c8f5dc6e2248b57faab4b23b5andcompressTypes :: [DGEdgeType] -> DGEdgeType
6b64034fa2a644ba291c484c0c01c7df5b8d982ckesscompressTypes [] = error "compressTypes: wrong usage"
6b64034fa2a644ba291c484c0c01c7df5b8d982ckesscompressTypes (t:[]) = t
6b64034fa2a644ba291c484c0c01c7df5b8d982ckesscompressTypes (t1:t2:r) = case t1 > t2 of
4a7affccb2f1f5b94cab395e1bf3825aed715ebcnd True -> compressTypes (t1:r)
4a7affccb2f1f5b94cab395e1bf3825aed715ebcnd False -> compressTypes (t2:r)
4a7affccb2f1f5b94cab395e1bf3825aed715ebcnd-- | returns a list of compressed edges
4a7affccb2f1f5b94cab395e1bf3825aed715ebcndgetCompressedEdges :: DGraph -> [Node] -> [(Node,Node,DGEdgeType)]
4a7affccb2f1f5b94cab395e1bf3825aed715ebcndgetCompressedEdges dg hidden =
4a7affccb2f1f5b94cab395e1bf3825aed715ebcnd filterDuplicates $ getShortPaths $ concat
ec9b02c6869b75575ada34c800672162833a2c06nd $ map (\ e@(_,t,_) -> map (e:) $ getPaths dg t hidden [])
fe64b2ba25510d8c9dba5560a2d537763566cf40nd inEdges = filter (\ (_,t,_) -> elem t hidden)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd $ concat $ map (outDG dg)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd $ foldr (\ n i -> if elem n hidden
fe64b2ba25510d8c9dba5560a2d537763566cf40nd || elem n i then i else n:i) []
fe64b2ba25510d8c9dba5560a2d537763566cf40nd $ map (\ (s,_,_) -> s) $ concat $ map (innDG dg) hidden
fe64b2ba25510d8c9dba5560a2d537763566cf40nd-- | filter duplicate paths
fe64b2ba25510d8c9dba5560a2d537763566cf40ndfilterDuplicates :: [(Node,Node,DGEdgeType)]
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd -> [(Node,Node,DGEdgeType)]
4335f1cbf345c91bb996eec540c11ba8ce5d4268ndfilterDuplicates [] = []
9583adab6bc4b3758e41963c905d9dad9f067131ndfilterDuplicates ((s,t,et):r) = edge:filterDuplicates others
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd (same,others) = partition (\ (s',t',_) -> s == s' && t == t') r
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd edge = (s,t,compressTypes $ et:map (\ (_,_,et') -> et') same)
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd-- | returns the pahts of a given node through hidden nodes
4335f1cbf345c91bb996eec540c11ba8ce5d4268ndgetPaths :: DGraph -> Node -> [Node] -> [Node] -> [[LEdge DGLinkLab]]
4335f1cbf345c91bb996eec540c11ba8ce5d4268ndgetPaths dg node hidden seen' = case elem node hidden of
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd True -> case edges /= [] of
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd True -> concat $ map (\ e@(_,t,_) -> map (e:) $ getPaths dg t hidden seen)
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd False -> []
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd False -> [[]]
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd seen = node:seen'
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd edges = filter (\ (_,t,_) -> notElem t seen) $ outDG dg node
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd-- | returns source and target node of a path with the compressed type
4335f1cbf345c91bb996eec540c11ba8ce5d4268ndgetShortPaths :: [[LEdge DGLinkLab]]
9b5e2c5e769dc678a1aca06df75c32022b2f1492trawick -> [(Node,Node,DGEdgeType)]
4335f1cbf345c91bb996eec540c11ba8ce5d4268ndgetShortPaths [] = []
4335f1cbf345c91bb996eec540c11ba8ce5d4268ndgetShortPaths (p:r) =
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd ((s,t,compressTypes $ map (\ (_,_,e) -> getRealDGLinkType e) p))
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd : getShortPaths r
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd (s,_,_) = head p
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd (_,t,_) = last p
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd-- | Let the user select a Node to focus
4335f1cbf345c91bb996eec540c11ba8ce5d4268ndfocusNode :: GInfo -> IO ()
fe64b2ba25510d8c9dba5560a2d537763566cf40ndfocusNode (GInfo { libEnvIORef = ioRefProofStatus
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , gi_LIB_NAME = ln
fe64b2ba25510d8c9dba5560a2d537763566cf40nd ,gi_GraphInfo = grInfo
fb77c505254b6e9c925e23e734463e87574f8f40kess le <- readIORef ioRefProofStatus
fe64b2ba25510d8c9dba5560a2d537763566cf40nd idsnodes <- filterM (\(n,_) -> do b <- GA.isHiddenNode grInfo n
fe64b2ba25510d8c9dba5560a2d537763566cf40nd return $ not b)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd $ labNodesDG $ lookupDGraph ln le
fe64b2ba25510d8c9dba5560a2d537763566cf40nd let (ids,nodes) = unzip idsnodes
fe64b2ba25510d8c9dba5560a2d537763566cf40nd let nodes' = map (getDGNodeName) nodes
fe64b2ba25510d8c9dba5560a2d537763566cf40nd selection <- listBox "Select a node to focus" nodes'
fb77c505254b6e9c925e23e734463e87574f8f40kess case selection of
fb77c505254b6e9c925e23e734463e87574f8f40kess Just idx -> GA.focusNode grInfo $ ids !! idx
fb77c505254b6e9c925e23e734463e87574f8f40kess Nothing -> return ()
06ba4a61654b3763ad65f52283832ebf058fdf1cslivetranslateGraph :: GInfo -> ConvFunc -> LibFunc -> IO ()
313bb560bc5c323cfd40c9cad7335b4b8e060aedkesstranslateGraph (GInfo {libEnvIORef = ioRefProofStatus,
10673857794a4b3d9568ca2d983722a87ed352f1rbowen gi_LIB_NAME = ln,
fb77c505254b6e9c925e23e734463e87574f8f40kess gi_hetcatsOpts = opts
ed0dae472b518c553c923a86fb4322d4c50d86a6nd }) convGraph showLib = do
ed0dae472b518c553c923a86fb4322d4c50d86a6nd le <- readIORef ioRefProofStatus
10673857794a4b3d9568ca2d983722a87ed352f1rbowen openTranslateGraph le ln opts (getDGLogic le) convGraph showLib
06ba4a61654b3763ad65f52283832ebf058fdf1csliveshowLibGraph :: GInfo -> LibFunc -> IO ()
fb77c505254b6e9c925e23e734463e87574f8f40kessshowLibGraph gInfo showLib = do
fb77c505254b6e9c925e23e734463e87574f8f40kess showLib gInfo
06ba4a61654b3763ad65f52283832ebf058fdf1cslive{- | it tries to perform the given action to the given graph.
06ba4a61654b3763ad65f52283832ebf058fdf1cslive If part of the given graph is not hidden, then the action can
fb77c505254b6e9c925e23e734463e87574f8f40kess be performed directly; otherwise the graph will be shown completely
06ba4a61654b3763ad65f52283832ebf058fdf1cslive firstly, and then the action will be performed, and after that the graph
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd will be hidden again.
06ba4a61654b3763ad65f52283832ebf058fdf1csliveperformProofAction :: GInfo -> IO () -> IO ()
06ba4a61654b3763ad65f52283832ebf058fdf1csliveperformProofAction gInfo@(GInfo { gi_GraphInfo = actGraphInfo
06ba4a61654b3763ad65f52283832ebf058fdf1cslive }) proofAction = do
06ba4a61654b3763ad65f52283832ebf058fdf1cslive let actionWithMessage = do
06ba4a61654b3763ad65f52283832ebf058fdf1cslive "Applying development graph calculus proof rule..."
1f53e295ebd19aed1767d12da7abfab9936c148cjerenkrantz hhn <- GA.hasHiddenNodes actGraphInfo
cb3a1082aec4b3b4f4ed238c93c3cc54933a7f0end case hhn of
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess True -> do
1f53e295ebd19aed1767d12da7abfab9936c148cjerenkrantz showNodes gInfo
06ba4a61654b3763ad65f52283832ebf058fdf1cslive actionWithMessage
06ba4a61654b3763ad65f52283832ebf058fdf1cslive hideNodes gInfo
06ba4a61654b3763ad65f52283832ebf058fdf1cslive False -> actionWithMessage
97a9a944b5887e91042b019776c41d5dd74557aferikabele "Development graph calculus proof rule finished."
97a9a944b5887e91042b019776c41d5dd74557aferikabelesaveProofStatus :: GInfo -> FilePath -> IO ()
909ce17e2bd0faef7b1c294f2307f009793fd493ndsaveProofStatus (GInfo { libEnvIORef = ioRefProofStatus
909ce17e2bd0faef7b1c294f2307f009793fd493nd , gi_LIB_NAME = ln
909ce17e2bd0faef7b1c294f2307f009793fd493nd , gi_hetcatsOpts = opts
909ce17e2bd0faef7b1c294f2307f009793fd493nd }) file = encapsulateWaitTermAct $ do
909ce17e2bd0faef7b1c294f2307f009793fd493nd proofStatus <- readIORef ioRefProofStatus
06ba4a61654b3763ad65f52283832ebf058fdf1cslive writeShATermFile file (ln, lookupHistory ln proofStatus)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive putIfVerbose opts 2 $ "Wrote " ++ file
06ba4a61654b3763ad65f52283832ebf058fdf1cslive-- | implementation of open menu, read in a proof status
06ba4a61654b3763ad65f52283832ebf058fdf1csliveopenProofStatus :: GInfo -> FilePath -> ConvFunc -> LibFunc
97a9a944b5887e91042b019776c41d5dd74557aferikabeleopenProofStatus gInfo@(GInfo { libEnvIORef = ioRefProofStatus
97a9a944b5887e91042b019776c41d5dd74557aferikabele , gi_LIB_NAME = ln
97a9a944b5887e91042b019776c41d5dd74557aferikabele , gi_hetcatsOpts = opts
06ba4a61654b3763ad65f52283832ebf058fdf1cslive }) file convGraph showLib = do
06ba4a61654b3763ad65f52283832ebf058fdf1cslive mh <- readVerbose opts ln file
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Nothing -> errorMess $ "Could not read proof status from file '"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive ++ file ++ "'"
cb3a1082aec4b3b4f4ed238c93c3cc54933a7f0end Just h -> do
06ba4a61654b3763ad65f52283832ebf058fdf1cslive let libfile = libNameToFile opts ln
8e31885fc494b603e0650113dde9e29d1b1d2602maczniak m <- anaLib opts { outtypes = [] } libfile
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Nothing -> errorMess $ "Could not read original development graph"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive ++ " from '" ++ libfile ++ "'"
97a9a944b5887e91042b019776c41d5dd74557aferikabele Just (_, libEnv) -> case Map.lookup ln libEnv of
8e31885fc494b603e0650113dde9e29d1b1d2602maczniak Nothing -> errorMess $ "Could not get original development"
8e31885fc494b603e0650113dde9e29d1b1d2602maczniak ++ " graph for '" ++ showDoc ln "'"
f23fb63b05f89f47d7a3099491f2c68dcce432e9kess Just dg -> do
06ba4a61654b3763ad65f52283832ebf058fdf1cslive lockGlobal gInfo
06ba4a61654b3763ad65f52283832ebf058fdf1cslive oldEnv <- readIORef ioRefProofStatus
06ba4a61654b3763ad65f52283832ebf058fdf1cslive let proofStatus = Map.insert ln
06ba4a61654b3763ad65f52283832ebf058fdf1cslive (applyProofHistory h dg) oldEnv
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd writeIORef ioRefProofStatus proofStatus
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd unlockGlobal gInfo
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd gInfo' <- copyGInfo gInfo ln
fe64b2ba25510d8c9dba5560a2d537763566cf40nd convGraph gInfo' "Proof Status " showLib
ed0dae472b518c553c923a86fb4322d4c50d86a6nd GA.redisplay $ gi_GraphInfo gInfo'
ed0dae472b518c553c923a86fb4322d4c50d86a6nd-- | apply a rule of the development graph calculus
ed0dae472b518c553c923a86fb4322d4c50d86a6ndproofMenu :: GInfo
fe64b2ba25510d8c9dba5560a2d537763566cf40nd -> (LibEnv -> IO (Res.Result LibEnv))
fe64b2ba25510d8c9dba5560a2d537763566cf40ndproofMenu gInfo@(GInfo { libEnvIORef = ioRefProofStatus
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , gi_LIB_NAME = ln
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , gi_GraphInfo = actGraphInfo
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , gi_hetcatsOpts = hOpts
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , proofGUIMVar = guiMVar
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , globalHist = gHist
fe64b2ba25510d8c9dba5560a2d537763566cf40nd }) proofFun = do
fe64b2ba25510d8c9dba5560a2d537763566cf40nd filled <- tryPutMVar guiMVar Nothing
fb77c505254b6e9c925e23e734463e87574f8f40kess if not filled
fe64b2ba25510d8c9dba5560a2d537763566cf40nd then readMVar guiMVar >>=
fb77c505254b6e9c925e23e734463e87574f8f40kess (maybe (putIfVerbose hOpts 0 "proofMenu: ignored Nothing")
fe64b2ba25510d8c9dba5560a2d537763566cf40nd (\ w -> do
fe64b2ba25510d8c9dba5560a2d537763566cf40nd putIfVerbose hOpts 4 $
fe64b2ba25510d8c9dba5560a2d537763566cf40nd "proofMenu: Ignored Proof command; " ++
fe64b2ba25510d8c9dba5560a2d537763566cf40nd "maybe a proof window is still open?"
70ada6b79498c38ab85985a3d30ee11248ce897byoshiki lockGlobal gInfo
fb77c505254b6e9c925e23e734463e87574f8f40kess proofStatus <- readIORef ioRefProofStatus
fb77c505254b6e9c925e23e734463e87574f8f40kess putIfVerbose hOpts 4 "Proof started via \"Proofs\" menu"
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess Res.Result ds res <- proofFun proofStatus
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess putIfVerbose hOpts 4 "Analyzing result of proof"
fe64b2ba25510d8c9dba5560a2d537763566cf40nd case res of
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Nothing -> do
fe64b2ba25510d8c9dba5560a2d537763566cf40nd unlockGlobal gInfo
fe64b2ba25510d8c9dba5560a2d537763566cf40nd mapM_ (putStrLn . show) ds
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Just newProofStatus -> do
627c978514c54179736d152923478be7c8707f9bnd let newGr = lookupDGraph ln newProofStatus
fe64b2ba25510d8c9dba5560a2d537763566cf40nd history = proofHistory newGr
fb77c505254b6e9c925e23e734463e87574f8f40kess (guHist, grHist) <- takeMVar gHist
fb77c505254b6e9c925e23e734463e87574f8f40kess doDump hOpts "PrintHistory" $ do
fe64b2ba25510d8c9dba5560a2d537763566cf40nd putStrLn "History"
fe64b2ba25510d8c9dba5560a2d537763566cf40nd print $ prettyHistory history
fe64b2ba25510d8c9dba5560a2d537763566cf40nd putMVar gHist
fe64b2ba25510d8c9dba5560a2d537763566cf40nd (calcGlobalHistory proofStatus newProofStatus : guHist, grHist)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd applyChanges actGraphInfo history
06ba4a61654b3763ad65f52283832ebf058fdf1cslive applyTypeChanges actGraphInfo newGr
06ba4a61654b3763ad65f52283832ebf058fdf1cslive writeIORef ioRefProofStatus newProofStatus
06ba4a61654b3763ad65f52283832ebf058fdf1cslive unlockGlobal gInfo
06ba4a61654b3763ad65f52283832ebf058fdf1cslive hideShowNames gInfo False
06ba4a61654b3763ad65f52283832ebf058fdf1cslive mGUIMVar <- tryTakeMVar guiMVar
06ba4a61654b3763ad65f52283832ebf058fdf1cslive maybe (fail $ "should be filled with Nothing after proof attempt")
06ba4a61654b3763ad65f52283832ebf058fdf1cslive (const $ return ())
06ba4a61654b3763ad65f52283832ebf058fdf1cslivecalcGlobalHistory :: LibEnv -> LibEnv -> [LIB_NAME]
06ba4a61654b3763ad65f52283832ebf058fdf1cslivecalcGlobalHistory old new = let
06ba4a61654b3763ad65f52283832ebf058fdf1cslive pHist = (\ ln le -> proofHistory $ lookupDGraph ln le)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive length' = (\ ln le -> length $ pHist ln le)
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd changes = filter (\ ln -> pHist ln old /= pHist ln new) $ Map.keys old
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd in concatMap (\ ln -> replicate (length' ln new - length' ln old) ln) changes
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cndnodeErr :: Int -> IO ()
06ba4a61654b3763ad65f52283832ebf058fdf1cslivenodeErr descr = error $ "node with descriptor " ++ show descr
06ba4a61654b3763ad65f52283832ebf058fdf1cslive ++ " has no corresponding node in the development graph"
06ba4a61654b3763ad65f52283832ebf058fdf1csliveshowSpec :: Int -> DGraph -> IO ()
06ba4a61654b3763ad65f52283832ebf058fdf1csliveshowSpec descr dgraph = do
06ba4a61654b3763ad65f52283832ebf058fdf1cslive let sp = dgToSpec dgraph descr
fb77c505254b6e9c925e23e734463e87574f8f40kess sp' = case sp of
fb77c505254b6e9c925e23e734463e87574f8f40kess Res.Result ds Nothing -> show $ vcat $ map pretty ds
fb77c505254b6e9c925e23e734463e87574f8f40kess Res.Result _ m -> showDoc m ""
fe64b2ba25510d8c9dba5560a2d537763566cf40nd createTextDisplay "Show spec" sp' [size(80,25)]
fe64b2ba25510d8c9dba5560a2d537763566cf40ndshowNodeInfo :: Int -> DGraph -> IO ()
fe64b2ba25510d8c9dba5560a2d537763566cf40ndshowNodeInfo descr dgraph = do
fe64b2ba25510d8c9dba5560a2d537763566cf40nd let dgnode = labDG dgraph descr
fe64b2ba25510d8c9dba5560a2d537763566cf40nd title = (if isDGRef dgnode then ("reference " ++) else
fe64b2ba25510d8c9dba5560a2d537763566cf40nd if isInternalNode dgnode then ("internal " ++) else id)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd "node " ++ getDGNodeName dgnode ++ " " ++ show descr
fe64b2ba25510d8c9dba5560a2d537763566cf40nd createTextDisplay title (title ++ "\n" ++ showDoc dgnode "")
fe64b2ba25510d8c9dba5560a2d537763566cf40nd fetches the theory from a node inside the IO Monad
fe64b2ba25510d8c9dba5560a2d537763566cf40nd (added by KL based on code in getTheoryOfNode) -}
06ba4a61654b3763ad65f52283832ebf058fdf1cslivelookupTheoryOfNode :: IORef LibEnv -> LIB_NAME -> Int
20189240503ef2c8f5dc6e2248b57faab4b23b5and -> IO (Res.Result (Node,G_theory))
06ba4a61654b3763ad65f52283832ebf058fdf1cslivelookupTheoryOfNode proofStatusRef ln descr = do
06ba4a61654b3763ad65f52283832ebf058fdf1cslive libEnv <- readIORef proofStatusRef
06ba4a61654b3763ad65f52283832ebf058fdf1cslive case (do gth <- computeTheory libEnv ln descr
06ba4a61654b3763ad65f52283832ebf058fdf1cslive return (descr, gth)) of
06ba4a61654b3763ad65f52283832ebf058fdf1cslive r -> return r
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd{- | outputs the theory of a node in a window;
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cndused by the node menu defined in initializeGraph-}
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cndgetTheoryOfNode :: GInfo -> Int -> DGraph -> IO ()
6b64034fa2a644ba291c484c0c01c7df5b8d982ckessgetTheoryOfNode gInfo@(GInfo { gi_LIB_NAME = ln
fb77c505254b6e9c925e23e734463e87574f8f40kess , libEnvIORef = le }) descr dgraph = do
06ba4a61654b3763ad65f52283832ebf058fdf1cslive r <- lookupTheoryOfNode le ln descr
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Res.Result ds res -> do
06ba4a61654b3763ad65f52283832ebf058fdf1cslive showDiags (gi_hetcatsOpts gInfo) ds
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess case res of
fe64b2ba25510d8c9dba5560a2d537763566cf40nd (Just (n, gth)) ->
fe64b2ba25510d8c9dba5560a2d537763566cf40nd (showName $ dgn_name $ lab' (contextDG dgraph n))
fe64b2ba25510d8c9dba5560a2d537763566cf40nd (addHasInHidingWarning dgraph n)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd _ -> return ()
fe64b2ba25510d8c9dba5560a2d537763566cf40nd{- | translate the theory of a node in a window;
fe64b2ba25510d8c9dba5560a2d537763566cf40ndused by the node menu defined in initializeGraph-}
fe64b2ba25510d8c9dba5560a2d537763566cf40ndtranslateTheoryOfNode :: GInfo -> Int -> DGraph -> IO ()
fe64b2ba25510d8c9dba5560a2d537763566cf40ndtranslateTheoryOfNode gInfo@(GInfo {gi_hetcatsOpts = opts})
fe64b2ba25510d8c9dba5560a2d537763566cf40nd descr dgraph = do
06ba4a61654b3763ad65f52283832ebf058fdf1cslive libEnv <- readIORef $ libEnvIORef gInfo
ff797e743eb73c1d45b08158aa6b288c2d0c46eeslive th <- computeTheory libEnv (gi_LIB_NAME gInfo) descr
ff797e743eb73c1d45b08158aa6b288c2d0c46eeslive return (descr,th) ) of
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd Res.Result [] (Just (node,th)) -> do
ff797e743eb73c1d45b08158aa6b288c2d0c46eeslive Res.Result ds _ <- runResultT(
fb77c505254b6e9c925e23e734463e87574f8f40kess do G_theory lid sign _ sens _ <- return th
fb77c505254b6e9c925e23e734463e87574f8f40kess -- find all comorphism paths starting from lid
fb77c505254b6e9c925e23e734463e87574f8f40kess let paths = findComorphismPaths logicGraph (sublogicOfTh th)
fb77c505254b6e9c925e23e734463e87574f8f40kess -- let the user choose one
ff797e743eb73c1d45b08158aa6b288c2d0c46eeslive sel <- lift $ listBox "Choose a logic translation"
ff797e743eb73c1d45b08158aa6b288c2d0c46eeslive (map show paths)
ff797e743eb73c1d45b08158aa6b288c2d0c46eeslive i <- case sel of
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd Just j -> return j
130d299c4b2b15be45532a176604c71fdc7bea5bnd _ -> liftR $ fail "no logic translation chosen"
130d299c4b2b15be45532a176604c71fdc7bea5bnd Comorphism cid <- return (paths!!i)
130d299c4b2b15be45532a176604c71fdc7bea5bnd -- adjust lid's
130d299c4b2b15be45532a176604c71fdc7bea5bnd let lidS = sourceLogic cid
130d299c4b2b15be45532a176604c71fdc7bea5bnd lidT = targetLogic cid
130d299c4b2b15be45532a176604c71fdc7bea5bnd sign' <- coerceSign lid lidS "" sign
130d299c4b2b15be45532a176604c71fdc7bea5bnd sens' <- coerceThSens lid lidS "" sens
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd -- translate theory along chosen comorphism
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd (sign'',sens1) <-
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd liftR $ wrapMapTheory cid (plainSign sign', toNamedList sens')
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd "Translated Theory"
fb77c505254b6e9c925e23e734463e87574f8f40kess (showName $ dgn_name $ lab' (contextDG dgraph node))
fb77c505254b6e9c925e23e734463e87574f8f40kess (addHasInHidingWarning dgraph node)
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd (G_theory lidT (mkExtSign sign'') startSigId
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd (toThSens sens1) startThId)
d1348237b33bc1755b9f1165eea52317465a7671nd showDiags opts ds
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Res.Result ds _ -> showDiags opts ds
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd{- | outputs the sublogic of a node in a window;
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cndused by the node menu defined in initializeGraph -}
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cndgetSublogicOfNode :: IORef LibEnv -> LIB_NAME -> Int -> DGraph -> IO()
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cndgetSublogicOfNode proofStatusRef ln descr dgraph = do
fb77c505254b6e9c925e23e734463e87574f8f40kess libEnv <- readIORef proofStatusRef
fb77c505254b6e9c925e23e734463e87574f8f40kess let dgnode = labDG dgraph descr
06ba4a61654b3763ad65f52283832ebf058fdf1cslive name = if isDGRef dgnode then emptyNodeName
6b64034fa2a644ba291c484c0c01c7df5b8d982ckess else dgn_name dgnode
6b64034fa2a644ba291c484c0c01c7df5b8d982ckess case computeTheory libEnv ln descr of
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Res.Result _ (Just th) -> do
06ba4a61654b3763ad65f52283832ebf058fdf1cslive let logstr = show $ sublogicOfTh th
06ba4a61654b3763ad65f52283832ebf058fdf1cslive title = "Sublogic of "++showName name
06ba4a61654b3763ad65f52283832ebf058fdf1cslive createTextDisplay title logstr [HTk.size(30,10)]
130d299c4b2b15be45532a176604c71fdc7bea5bnd error $ "Could not compute theory for sublogic computation: "
130d299c4b2b15be45532a176604c71fdc7bea5bnd ++ concatMap show ds
130d299c4b2b15be45532a176604c71fdc7bea5bnd-- | Show proof status of a node
130d299c4b2b15be45532a176604c71fdc7bea5bndshowProofStatusOfNode :: GInfo -> Int -> DGraph -> IO ()
130d299c4b2b15be45532a176604c71fdc7bea5bndshowProofStatusOfNode _ descr dgraph = do
130d299c4b2b15be45532a176604c71fdc7bea5bnd let dgnode = labDG dgraph descr
130d299c4b2b15be45532a176604c71fdc7bea5bnd stat = showStatusAux dgnode
130d299c4b2b15be45532a176604c71fdc7bea5bnd title = "Proof status of node "++showName (dgn_name dgnode)
130d299c4b2b15be45532a176604c71fdc7bea5bnd createTextDisplay title stat [HTk.size(105,55)]
130d299c4b2b15be45532a176604c71fdc7bea5bndshowStatusAux :: DGNodeLab -> String
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cndshowStatusAux dgnode =
06ba4a61654b3763ad65f52283832ebf058fdf1cslive case dgn_theory dgnode of
06ba4a61654b3763ad65f52283832ebf058fdf1cslive G_theory _ _ _ sens _ ->
06ba4a61654b3763ad65f52283832ebf058fdf1cslive let goals = OMap.filter (not . isAxiom) sens
06ba4a61654b3763ad65f52283832ebf058fdf1cslive (proven,open) = OMap.partition isProvenSenStatus goals
06ba4a61654b3763ad65f52283832ebf058fdf1cslive consGoal = "\nconservativity of this node"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive in "Proven proof goals:\n"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive ++ showDoc proven ""
06ba4a61654b3763ad65f52283832ebf058fdf1cslive ++ if not $ hasOpenConsStatus True dgnode
6b64034fa2a644ba291c484c0c01c7df5b8d982ckess then consGoal
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess ++ "\nOpen proof goals:\n"
6b64034fa2a644ba291c484c0c01c7df5b8d982ckess ++ showDoc open ""
6b64034fa2a644ba291c484c0c01c7df5b8d982ckess ++ if hasOpenConsStatus False dgnode
06ba4a61654b3763ad65f52283832ebf058fdf1cslive then consGoal
06ba4a61654b3763ad65f52283832ebf058fdf1cslive-- | start local theorem proving or consistency checking at a node
06ba4a61654b3763ad65f52283832ebf058fdf1csliveproveAtNode :: Bool -> GInfo -> Int -> DGraph -> IO ()
06ba4a61654b3763ad65f52283832ebf058fdf1csliveproveAtNode checkCons gInfo@(GInfo { libEnvIORef = ioRefProofStatus
06ba4a61654b3763ad65f52283832ebf058fdf1cslive , gi_LIB_NAME = ln }) descr dgraph = do
130d299c4b2b15be45532a176604c71fdc7bea5bnd let dgn = labDG dgraph descr
130d299c4b2b15be45532a176604c71fdc7bea5bnd libNode = (ln,descr)
130d299c4b2b15be45532a176604c71fdc7bea5bnd (dgraph',dgn') <- case hasLock dgn of
130d299c4b2b15be45532a176604c71fdc7bea5bnd True -> return (dgraph, dgn)
130d299c4b2b15be45532a176604c71fdc7bea5bnd False -> do
130d299c4b2b15be45532a176604c71fdc7bea5bnd lockGlobal gInfo
130d299c4b2b15be45532a176604c71fdc7bea5bnd le <- readIORef ioRefProofStatus
06ba4a61654b3763ad65f52283832ebf058fdf1cslive (dgraph',dgn') <- initLocking (lookupDGraph ln le) (descr, dgn)
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess writeIORef ioRefProofStatus $ Map.insert ln dgraph' le
6b64034fa2a644ba291c484c0c01c7df5b8d982ckess unlockGlobal gInfo
6b64034fa2a644ba291c484c0c01c7df5b8d982ckess return (dgraph',dgn')
6b64034fa2a644ba291c484c0c01c7df5b8d982ckess locked <- tryLockLocal dgn'
6b64034fa2a644ba291c484c0c01c7df5b8d982ckess case locked of
6b64034fa2a644ba291c484c0c01c7df5b8d982ckess False -> do
06ba4a61654b3763ad65f52283832ebf058fdf1cslive createTextDisplay "Error" "Proofwindow already open" [HTk.size(30,10)]
fb77c505254b6e9c925e23e734463e87574f8f40kess let action = (do le <- readIORef ioRefProofStatus
fb77c505254b6e9c925e23e734463e87574f8f40kess guiMVar <- newMVar Nothing
06ba4a61654b3763ad65f52283832ebf058fdf1cslive res <- basicInferenceNode checkCons logicGraph libNode ln
06ba4a61654b3763ad65f52283832ebf058fdf1cslive runProveAtNode gInfo (descr, dgn') res)
130d299c4b2b15be45532a176604c71fdc7bea5bnd case checkCons || not (hasIncomingHidingEdge dgraph' $ snd libNode) of
130d299c4b2b15be45532a176604c71fdc7bea5bnd True -> action
130d299c4b2b15be45532a176604c71fdc7bea5bnd False -> GUI.HTkUtils.createInfoDisplayWithTwoButtons "Warning"
130d299c4b2b15be45532a176604c71fdc7bea5bnd "This node has incoming hiding links!!!" "Prove anyway"
130d299c4b2b15be45532a176604c71fdc7bea5bnd unlockLocal dgn'
130d299c4b2b15be45532a176604c71fdc7bea5bndrunProveAtNode :: GInfo -> LNode DGNodeLab -> Res.Result LibEnv -> IO ()
06ba4a61654b3763ad65f52283832ebf058fdf1csliverunProveAtNode gInfo@(GInfo {gi_LIB_NAME = ln}) (v,_)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive (Res.Result {maybeResult = mle}) = case mle of
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Just le -> case matchDG v $ lookupDGraph ln le of
fb77c505254b6e9c925e23e734463e87574f8f40kess (Just(_,_,dgn,_), _) -> proofMenu gInfo (mergeDGNodeLab gInfo (v,dgn))
06ba4a61654b3763ad65f52283832ebf058fdf1cslive _ -> error $ "mergeDGNodeLab no such node: " ++ show v
fb77c505254b6e9c925e23e734463e87574f8f40kess Nothing -> return ()
97a9a944b5887e91042b019776c41d5dd74557aferikabelemergeDGNodeLab :: GInfo -> LNode DGNodeLab -> LibEnv -> IO (Res.Result LibEnv)
fe64b2ba25510d8c9dba5560a2d537763566cf40ndmergeDGNodeLab (GInfo{gi_LIB_NAME = ln}) (v, new_dgn) le = do
fe64b2ba25510d8c9dba5560a2d537763566cf40nd let dg = lookupDGraph ln le
fe64b2ba25510d8c9dba5560a2d537763566cf40nd le' <- case matchDG v dg of
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess (Just(p, _, old_dgn, s), g) -> do
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess theory <- joinG_sentences (dgn_theory old_dgn) $ dgn_theory new_dgn
fe64b2ba25510d8c9dba5560a2d537763566cf40nd new_dgn' = old_dgn{dgn_theory = theory}
fe64b2ba25510d8c9dba5560a2d537763566cf40nd dg' = addToProofHistoryDG ([],[SetNodeLab old_dgn (v, new_dgn')]) $
fe64b2ba25510d8c9dba5560a2d537763566cf40nd g{dgBody = (p, v, new_dgn', s) & (dgBody g)}
fe64b2ba25510d8c9dba5560a2d537763566cf40nd return $ Map.insert ln dg' le
fe64b2ba25510d8c9dba5560a2d537763566cf40nd _ -> error $ "mergeDGNodeLab no such node: " ++ show v
fe64b2ba25510d8c9dba5560a2d537763566cf40nd return Res.Result { diags = [], maybeResult = Just le'}
15ba1801088da1aad6d20609cf3f7b0b1eefce8aslive-- | print the id, origin, type, proof-status and morphism of the edge
fe64b2ba25510d8c9dba5560a2d537763566cf40ndshowEdgeInfo :: Int -> Maybe (LEdge DGLinkLab) -> IO ()
fe64b2ba25510d8c9dba5560a2d537763566cf40ndshowEdgeInfo descr me = case me of
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Just e@(_, _, l) -> let estr = showLEdge e in
fe64b2ba25510d8c9dba5560a2d537763566cf40nd createTextDisplay ("Info of " ++ estr)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd (estr ++ "\n" ++ showDoc l "") [HTk.size(70,30)]
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Nothing -> createTextDisplay "Error"
fe64b2ba25510d8c9dba5560a2d537763566cf40nd ("edge " ++ show descr ++ " has no corresponding edge"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive ++ "in the development graph") [HTk.size(50,10)]
06ba4a61654b3763ad65f52283832ebf058fdf1cslive-- | check conservativity of the edge
97a9a944b5887e91042b019776c41d5dd74557aferikabelecheckconservativityOfEdge :: Int -> GInfo -> Maybe (LEdge DGLinkLab) -> IO ()
d1348237b33bc1755b9f1165eea52317465a7671ndcheckconservativityOfEdge _ gInfo
d1348237b33bc1755b9f1165eea52317465a7671nd (Just (source,target,linklab)) = do
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd libEnv <- readIORef $ libEnvIORef gInfo
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd let dgraph = lookupDGraph (gi_LIB_NAME gInfo) libEnv
6954edc623ca2c179eb5b33e97e4304d06fd649frbowen dgtar = lab' (contextDG dgraph target)
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd if isDGRef dgtar then error "checkconservativityOfEdge: no DGNode" else do
06ba4a61654b3763ad65f52283832ebf058fdf1cslive G_theory lid _ _ sens _ <- return $ dgn_theory dgtar
06ba4a61654b3763ad65f52283832ebf058fdf1cslive GMorphism cid _ _ morphism2 _ <- return $ dgl_morphism linklab
06ba4a61654b3763ad65f52283832ebf058fdf1cslive morphism2' <- coerceMorphism (targetLogic cid) lid
fe64b2ba25510d8c9dba5560a2d537763566cf40nd "checkconservativityOfEdge" morphism2
fe64b2ba25510d8c9dba5560a2d537763566cf40nd let th = case computeTheory libEnv (gi_LIB_NAME gInfo) source of
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Res.Result _ (Just th1) -> th1
fe64b2ba25510d8c9dba5560a2d537763566cf40nd _ -> error "checkconservativityOfEdge: computeTheory"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive G_theory lid1 sign1 _ sens1 _ <- return th
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess sign2 <- coerceSign lid1 lid "checkconservativityOfEdge.coerceSign" sign1
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess sens2 <- coerceThSens lid1 lid "" sens1
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess let Res.Result ds res =
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess conservativityCheck lid
fe64b2ba25510d8c9dba5560a2d537763566cf40nd (plainSign sign2, toNamedList sens2)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd morphism2' $ toNamedList sens
fe64b2ba25510d8c9dba5560a2d537763566cf40nd showRes = case res of
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Just(Just True) -> "The link is conservative"
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Just(Just False) -> "The link is not conservative"
fe64b2ba25510d8c9dba5560a2d537763566cf40nd _ -> "Could not determine whether link is conservative"
fe64b2ba25510d8c9dba5560a2d537763566cf40nd myDiags = unlines (map show ds)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd createTextDisplay "Result of conservativity check"
fe64b2ba25510d8c9dba5560a2d537763566cf40nd (showRes ++ "\n" ++ myDiags) [HTk.size(50,50)]
fe64b2ba25510d8c9dba5560a2d537763566cf40ndcheckconservativityOfEdge descr _ Nothing =
fe64b2ba25510d8c9dba5560a2d537763566cf40nd createTextDisplay "Error"
fe64b2ba25510d8c9dba5560a2d537763566cf40nd ("edge " ++ show descr ++ " has no corresponding edge "
9bcfc3697a91b5215893a7d0206865b13fc72148nd ++ "in the development graph") [HTk.size(30,10)]
fb77c505254b6e9c925e23e734463e87574f8f40kess-- | converts a DGraph
fb77c505254b6e9c925e23e734463e87574f8f40kessconvert :: GA.GraphInfo -> DGraph -> IO ()
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cndconvert ginfo dgraph = do
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd convertNodes ginfo dgraph
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd convertEdges ginfo dgraph
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd{- | converts the nodes of the development graph, if it has any,
06ba4a61654b3763ad65f52283832ebf058fdf1csliveand returns the resulting conversion maps
06ba4a61654b3763ad65f52283832ebf058fdf1csliveif the graph is empty the conversion maps are returned unchanged-}
c68acc9d712af079afa2bd1a5a4aeef9a3ea573ckessconvertNodes :: GA.GraphInfo -> DGraph -> IO ()
c68acc9d712af079afa2bd1a5a4aeef9a3ea573ckessconvertNodes ginfo = mapM_ (convertNodesAux ginfo) .labNodesDG
06ba4a61654b3763ad65f52283832ebf058fdf1cslive{- | auxiliary function for convertNodes if the given list of nodes is
06ba4a61654b3763ad65f52283832ebf058fdf1csliveemtpy, it returns the conversion maps unchanged otherwise it adds the
fe64b2ba25510d8c9dba5560a2d537763566cf40ndconverted first node to the abstract graph and to the affected
fe64b2ba25510d8c9dba5560a2d537763566cf40ndconversion maps and afterwards calls itself with the remaining node
1b01d1ee11c612226cb3141eed4581dc179266c1rbowenconvertNodesAux :: GA.GraphInfo -> LNode DGNodeLab -> IO ()
1b01d1ee11c612226cb3141eed4581dc179266c1rbowenconvertNodesAux ginfo (node, dgnode) =
fe64b2ba25510d8c9dba5560a2d537763566cf40nd GA.addNode ginfo node (getRealDGNodeType dgnode) $ getDGNodeName dgnode
fe64b2ba25510d8c9dba5560a2d537763566cf40nd{- | converts the edges of the development graph
fe64b2ba25510d8c9dba5560a2d537763566cf40ndworks the same way as convertNods does-}
fe64b2ba25510d8c9dba5560a2d537763566cf40ndconvertEdges :: GA.GraphInfo -> DGraph -> IO ()
fe64b2ba25510d8c9dba5560a2d537763566cf40ndconvertEdges ginfo = mapM_ (convertEdgesAux ginfo) . labEdgesDG
fb77c505254b6e9c925e23e734463e87574f8f40kess-- | auxiliary function for convertEges
fe64b2ba25510d8c9dba5560a2d537763566cf40ndconvertEdgesAux :: GA.GraphInfo -> LEdge DGLinkLab -> IO ()
fe64b2ba25510d8c9dba5560a2d537763566cf40ndconvertEdgesAux ginfo e@(src, tar, lbl) =
fe64b2ba25510d8c9dba5560a2d537763566cf40nd GA.addEdge ginfo (dgl_id lbl) (getRealDGLinkType lbl) src tar "" $ Just e
fe64b2ba25510d8c9dba5560a2d537763566cf40nd-- | show library referened by a DGRef node (=node drawn as a box)
9bcfc3697a91b5215893a7d0206865b13fc72148ndshowReferencedLibrary :: Int -> GInfo -> ConvFunc -> LibFunc -> IO ()
ff797e743eb73c1d45b08158aa6b288c2d0c46eesliveshowReferencedLibrary descr gInfo@(GInfo { libEnvIORef = ioRefProofStatus
ff797e743eb73c1d45b08158aa6b288c2d0c46eeslive , gi_LIB_NAME = ln })
fb77c505254b6e9c925e23e734463e87574f8f40kess convGraph showLib = do
fb77c505254b6e9c925e23e734463e87574f8f40kess le <- readIORef ioRefProofStatus
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd let refNode = labDG (lookupDGraph ln le) descr
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd refLibname = if isDGRef refNode then dgn_libname refNode
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd else error "showReferencedLibrary"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive case Map.lookup refLibname le of
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd Just _ -> do
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd gInfo' <- copyGInfo gInfo refLibname
06ba4a61654b3763ad65f52283832ebf058fdf1cslive convGraph gInfo' "development graph" showLib
06ba4a61654b3763ad65f52283832ebf058fdf1cslive let gv = gi_GraphInfo gInfo'
9bcfc3697a91b5215893a7d0206865b13fc72148nd hideNodes gInfo'
fb77c505254b6e9c925e23e734463e87574f8f40kess GA.showTemporaryMessage gv "Development Graph initialized."
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd Nothing -> error $ "The referenced library (" ++ show refLibname
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd ++ ") is unknown"
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd-- | apply type changes of edges
fb77c505254b6e9c925e23e734463e87574f8f40kessapplyTypeChanges :: GA.GraphInfo -> DGraph -> IO ()
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cndapplyTypeChanges gi dgraph = do
5f86589186bcc15ee13e288a9d73acbeab2409fbdpejesh mapM_ (\ (node, dgnode) ->
5f86589186bcc15ee13e288a9d73acbeab2409fbdpejesh GA.changeNodeType gi node $ getRealDGNodeType dgnode
5f86589186bcc15ee13e288a9d73acbeab2409fbdpejesh ) $ labNodesDG dgraph
5f86589186bcc15ee13e288a9d73acbeab2409fbdpejesh mapM_ (\ (_, _, lbl) ->
5f86589186bcc15ee13e288a9d73acbeab2409fbdpejesh GA.changeEdgeType gi (dgl_id lbl) $ getRealDGLinkType lbl
5f86589186bcc15ee13e288a9d73acbeab2409fbdpejesh ) $ labEdgesDG dgraph
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess-- | apply the changes of first history item (computed by proof rules,
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess-- see folder Proofs) to the displayed development graph
5f86589186bcc15ee13e288a9d73acbeab2409fbdpejeshapplyChanges :: GA.GraphInfo -> ProofHistory -> IO ()
5f86589186bcc15ee13e288a9d73acbeab2409fbdpejeshapplyChanges _ [] = return ()
fe64b2ba25510d8c9dba5560a2d537763566cf40ndapplyChanges ginfo ((_, hElem) : _) = mapM_ (applyChangesAux ginfo)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd $ removeNullifyingChanges $ removeContraryChanges hElem
fe64b2ba25510d8c9dba5560a2d537763566cf40nd-- | auxiliary function for applyChanges
fe64b2ba25510d8c9dba5560a2d537763566cf40ndapplyChangesAux :: GA.GraphInfo -> DGChange -> IO ()
fe64b2ba25510d8c9dba5560a2d537763566cf40ndapplyChangesAux ginfo change =
fb77c505254b6e9c925e23e734463e87574f8f40kess case change of
fb77c505254b6e9c925e23e734463e87574f8f40kess SetNodeLab _ (node, newLab) ->
fe64b2ba25510d8c9dba5560a2d537763566cf40nd GA.changeNodeType ginfo node $ getRealDGNodeType newLab
fe64b2ba25510d8c9dba5560a2d537763566cf40nd InsertNode (node, nodelab) ->
fe64b2ba25510d8c9dba5560a2d537763566cf40nd GA.addNode ginfo node (getRealDGNodeType nodelab) $ getDGNodeName nodelab
fe64b2ba25510d8c9dba5560a2d537763566cf40nd DeleteNode (node, _) ->
fe64b2ba25510d8c9dba5560a2d537763566cf40nd InsertEdge e@(src, tgt, lbl) ->
9bcfc3697a91b5215893a7d0206865b13fc72148nd GA.addEdge ginfo (dgl_id lbl) (getRealDGLinkType lbl) src tgt "" $ Just e
9bcfc3697a91b5215893a7d0206865b13fc72148nd DeleteEdge (_, _, lbl) ->
5f86589186bcc15ee13e288a9d73acbeab2409fbdpejesh GA.delEdge ginfo $ dgl_id lbl
5f86589186bcc15ee13e288a9d73acbeab2409fbdpejesh-- | removes changed that are eliminating each other like 'add a' and 'del a'
5f86589186bcc15ee13e288a9d73acbeab2409fbdpejeshremoveNullifyingChanges :: [DGChange] -> [DGChange]
5f86589186bcc15ee13e288a9d73acbeab2409fbdpejeshremoveNullifyingChanges [] = []
9b5e2c5e769dc678a1aca06df75c32022b2f1492trawickremoveNullifyingChanges (change:changes) = case change of
6b64034fa2a644ba291c484c0c01c7df5b8d982ckess InsertNode (node, _) -> case find
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess (\ c -> case c of
5f86589186bcc15ee13e288a9d73acbeab2409fbdpejesh DeleteNode (node', _) -> node == node'
5f86589186bcc15ee13e288a9d73acbeab2409fbdpejesh _ -> False) changes of
5f86589186bcc15ee13e288a9d73acbeab2409fbdpejesh Just c' -> removeNullifyingChanges $ delete c' changes
5f86589186bcc15ee13e288a9d73acbeab2409fbdpejesh Nothing -> change:removeNullifyingChanges changes
5f86589186bcc15ee13e288a9d73acbeab2409fbdpejesh InsertEdge (_,_,el) -> let (EdgeId eid) = dgl_id el in case find
9fb925624300c864fe3969a264e52aa83f3c2dd0slive (\ c -> case c of
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess DeleteEdge (_,_,el') -> let (EdgeId eid') = dgl_id el' in eid == eid'
78f4d313fd5edf76dc5cfb8725e082a08cd29740jwoolley _ -> False) changes of
78f4d313fd5edf76dc5cfb8725e082a08cd29740jwoolley Just c' -> removeNullifyingChanges $ delete c' changes
3b9c7ec844aa240622a33735d1b9cbac4232e268rbowen Nothing -> change : removeNullifyingChanges changes
3b9c7ec844aa240622a33735d1b9cbac4232e268rbowen _ -> change : removeNullifyingChanges changes
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess-- | display a window of translated graph with maximal sublogic.
9fb925624300c864fe3969a264e52aa83f3c2dd0sliveopenTranslateGraph :: LibEnv -> LIB_NAME -> HetcatsOpts
5f86589186bcc15ee13e288a9d73acbeab2409fbdpejesh -> Res.Result G_sublogics -> ConvFunc -> LibFunc -> IO ()
5f86589186bcc15ee13e288a9d73acbeab2409fbdpejeshopenTranslateGraph libEnv ln opts (Res.Result diagsSl mSublogic) convGraph
05201775eaa6b363b8a119c8aea5db246b967591yoshiki -- if an error existed by the search of maximal sublogicn
5f86589186bcc15ee13e288a9d73acbeab2409fbdpejesh -- (see GUI.DGTranslation.getDGLogic), the process need not to go on.
5f86589186bcc15ee13e288a9d73acbeab2409fbdpejesh if hasErrors diagsSl then
fb77c505254b6e9c925e23e734463e87574f8f40kess errorMess $ unlines $ map show
5f86589186bcc15ee13e288a9d73acbeab2409fbdpejesh $ filter (relevantDiagKind . diagKind) diagsSl
fb77c505254b6e9c925e23e734463e87574f8f40kess do case mSublogic of
9fb925624300c864fe3969a264e52aa83f3c2dd0slive Just sublogic -> do
5f86589186bcc15ee13e288a9d73acbeab2409fbdpejesh let paths = findComorphismPaths logicGraph sublogic
5f86589186bcc15ee13e288a9d73acbeab2409fbdpejesh if null paths then
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess errorMess "This graph has no comorphism to translation."
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess Res.Result diagsR i <- runResultT ( do
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess -- the user choose one
5f86589186bcc15ee13e288a9d73acbeab2409fbdpejesh sel <- lift $ listBox "Choose a logic translation"
5f86589186bcc15ee13e288a9d73acbeab2409fbdpejesh (map show paths)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd case sel of
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Just j -> return j
fe64b2ba25510d8c9dba5560a2d537763566cf40nd _ -> liftR $ fail "no logic translation chosen")
fe64b2ba25510d8c9dba5560a2d537763566cf40nd let aComor = paths !! fromJust i
fe64b2ba25510d8c9dba5560a2d537763566cf40nd -- graph translation.
fe64b2ba25510d8c9dba5560a2d537763566cf40nd case libEnv_translation libEnv aComor of
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Res.Result diagsTrans (Just newLibEnv) -> do
fe64b2ba25510d8c9dba5560a2d537763566cf40nd showDiags opts (diagsSl ++ diagsR ++ diagsTrans)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd if hasErrors (diagsR ++ diagsTrans) then
fe64b2ba25510d8c9dba5560a2d537763566cf40nd errorMess $ unlines $ map show
fe64b2ba25510d8c9dba5560a2d537763566cf40nd $ filter (relevantDiagKind . diagKind)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd $ diagsR ++ diagsTrans
c985aca104389df30d6ec0a637ce0ccaac904362nd else dg_showGraphAux
c985aca104389df30d6ec0a637ce0ccaac904362nd (\gI@(GInfo{libEnvIORef = iorLE}) -> do
fe64b2ba25510d8c9dba5560a2d537763566cf40nd writeIORef iorLE newLibEnv
06ba4a61654b3763ad65f52283832ebf058fdf1cslive convGraph (gI{ gi_LIB_NAME = ln
06ba4a61654b3763ad65f52283832ebf058fdf1cslive , gi_hetcatsOpts = opts})
06ba4a61654b3763ad65f52283832ebf058fdf1cslive "translation Graph" showLib)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Res.Result diagsTrans Nothing ->
06ba4a61654b3763ad65f52283832ebf058fdf1cslive errorMess $ unlines $ map show
06ba4a61654b3763ad65f52283832ebf058fdf1cslive $ filter (relevantDiagKind . diagKind)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive $ diagsSl ++ diagsR ++ diagsTrans
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Nothing -> errorMess "the maximal sublogic is not found."
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd where relevantDiagKind Error = True
06ba4a61654b3763ad65f52283832ebf058fdf1cslive relevantDiagKind Warning = verbose opts >= 2
06ba4a61654b3763ad65f52283832ebf058fdf1cslive relevantDiagKind Hint = verbose opts >= 4
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd relevantDiagKind Debug = verbose opts >= 5
06ba4a61654b3763ad65f52283832ebf058fdf1cslive relevantDiagKind MessageW = False
06ba4a61654b3763ad65f52283832ebf058fdf1cslivedg_showGraphAux :: (GInfo -> IO ()) -> IO ()
06ba4a61654b3763ad65f52283832ebf058fdf1cslivedg_showGraphAux convFct = do
06ba4a61654b3763ad65f52283832ebf058fdf1cslive useHTk -- All messages are displayed in TK dialog windows
06ba4a61654b3763ad65f52283832ebf058fdf1cslive -- from this point on
06ba4a61654b3763ad65f52283832ebf058fdf1cslive gInfo <- emptyGInfo
06ba4a61654b3763ad65f52283832ebf058fdf1cslive convFct gInfo
06ba4a61654b3763ad65f52283832ebf058fdf1cslive GA.redisplay $ gi_GraphInfo gInfo
59cd19c3d75e35ae820e23f6b0161910784fce4eslive-- DaVinciGraph to String
59cd19c3d75e35ae820e23f6b0161910784fce4eslive-- Functions to convert a DaVinciGraph to a String to store as a .udg file
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd-- | saves the uDrawGraph graph to a file
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cndsaveUDGraph :: GInfo -> Map.Map DGNodeType (Shape value, String)
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd -> Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String) -> IO ()
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cndsaveUDGraph gInfo@(GInfo { gi_GraphInfo = graphInfo
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd , gi_LIB_NAME = ln
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd , gi_hetcatsOpts = opts
06ba4a61654b3763ad65f52283832ebf058fdf1cslive }) nodemap linkmap = do
7a497a1b89d0b52f5284854eb12662b4bd80ba5cnd evnt <- newFileDialogStr "Save as..."
7a497a1b89d0b52f5284854eb12662b4bd80ba5cnd $ (rmSuffix $ libNameToFile opts ln) ++ ".udg"
7a497a1b89d0b52f5284854eb12662b4bd80ba5cnd maybeFilePath <- HTk.sync evnt
7a497a1b89d0b52f5284854eb12662b4bd80ba5cnd case maybeFilePath of
7a497a1b89d0b52f5284854eb12662b4bd80ba5cnd Just filepath -> do
7a497a1b89d0b52f5284854eb12662b4bd80ba5cnd GA.showTemporaryMessage graphInfo "Converting graph..."
7a497a1b89d0b52f5284854eb12662b4bd80ba5cnd nstring <- nodes2String gInfo nodemap linkmap
7a497a1b89d0b52f5284854eb12662b4bd80ba5cnd writeFile filepath nstring
7a497a1b89d0b52f5284854eb12662b4bd80ba5cnd GA.showTemporaryMessage graphInfo $ "Graph stored to " ++ filepath ++ "!"
7a497a1b89d0b52f5284854eb12662b4bd80ba5cnd Nothing -> GA.showTemporaryMessage graphInfo $ "Aborted!"
7a497a1b89d0b52f5284854eb12662b4bd80ba5cnd-- | Converts the nodes of the graph to String representation
7a497a1b89d0b52f5284854eb12662b4bd80ba5cndnodes2String :: GInfo -> Map.Map DGNodeType (Shape value, String)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive -> IO String
06ba4a61654b3763ad65f52283832ebf058fdf1cslivenodes2String gInfo@(GInfo { gi_GraphInfo = graphInfo
fb77c505254b6e9c925e23e734463e87574f8f40kess , gi_LIB_NAME = ln
06ba4a61654b3763ad65f52283832ebf058fdf1cslive , libEnvIORef = ioRefProofStatus
06ba4a61654b3763ad65f52283832ebf058fdf1cslive }) nodemap linkmap = do
06ba4a61654b3763ad65f52283832ebf058fdf1cslive le <- readIORef ioRefProofStatus
06ba4a61654b3763ad65f52283832ebf058fdf1cslive nodes <- filterM (\(n,_) -> do b <- GA.isHiddenNode graphInfo n
06ba4a61654b3763ad65f52283832ebf058fdf1cslive return $ not b)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive $ labNodesDG $ lookupDGraph ln le
06ba4a61654b3763ad65f52283832ebf058fdf1cslive nstring <- foldM (\s node -> do
06ba4a61654b3763ad65f52283832ebf058fdf1cslive s' <- (node2String gInfo nodemap linkmap node)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive return $ s ++ (if s /= "" then ",\n " else "") ++ s')
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess return $ "[" ++ nstring ++ "]"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive-- | Converts a node to String representation
fb77c505254b6e9c925e23e734463e87574f8f40kessnode2String :: GInfo -> Map.Map DGNodeType (Shape value, String)
fb77c505254b6e9c925e23e734463e87574f8f40kess -> Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String)
fb77c505254b6e9c925e23e734463e87574f8f40kess -> LNode DGNodeLab -> IO String
4f854c24127e28f7ad72ce9a39d4448aaf910fc1slivenode2String gInfo nodemap linkmap (nid, dgnode) = do
4f854c24127e28f7ad72ce9a39d4448aaf910fc1slive label <- getNodeLabel gInfo dgnode
4f854c24127e28f7ad72ce9a39d4448aaf910fc1slive let ntype = getRealDGNodeType dgnode
9b5e2c5e769dc678a1aca06df75c32022b2f1492trawick (shape, color) <- case Map.lookup ntype nodemap of
4f854c24127e28f7ad72ce9a39d4448aaf910fc1slive Nothing -> error $ "SaveGraph: can't lookup nodetype: " ++ show ntype
59cd19c3d75e35ae820e23f6b0161910784fce4eslive Just (s, c) -> return (s, c)
59cd19c3d75e35ae820e23f6b0161910784fce4eslive object = "a(\"OBJECT\",\"" ++ label ++ "\"),"
59cd19c3d75e35ae820e23f6b0161910784fce4eslive color' = "a(\"COLOR\",\"" ++ color ++ "\"),"
59cd19c3d75e35ae820e23f6b0161910784fce4eslive shape' = "a(\"_GO\",\"" ++ (map toLower $ show shape) ++ "\")"
59cd19c3d75e35ae820e23f6b0161910784fce4eslive links <- links2String gInfo linkmap nid
59cd19c3d75e35ae820e23f6b0161910784fce4eslive return $ "l(\"" ++ (show nid) ++ "\",n(\"" ++ show ntype ++ "\","
59cd19c3d75e35ae820e23f6b0161910784fce4eslive ++ "[" ++ object ++ color' ++ shape' ++ "],"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive ++ "\n [" ++ links ++ "]))"
fe64b2ba25510d8c9dba5560a2d537763566cf40nd-- | Converts all links of a node to String representation
fe64b2ba25510d8c9dba5560a2d537763566cf40ndlinks2String :: GInfo -> Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd -> Int -> IO String
fe64b2ba25510d8c9dba5560a2d537763566cf40ndlinks2String (GInfo { gi_GraphInfo = graphInfo
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , gi_LIB_NAME = ln
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , libEnvIORef = ioRefProofStatus
fe64b2ba25510d8c9dba5560a2d537763566cf40nd }) linkmap nodeid = do
fe64b2ba25510d8c9dba5560a2d537763566cf40nd le <- readIORef ioRefProofStatus
fe64b2ba25510d8c9dba5560a2d537763566cf40nd edges <- filterM (\(src,_,edge) -> do
fe64b2ba25510d8c9dba5560a2d537763566cf40nd let eid = dgl_id edge
fe64b2ba25510d8c9dba5560a2d537763566cf40nd b <- GA.isHiddenEdge graphInfo eid
fe64b2ba25510d8c9dba5560a2d537763566cf40nd return $ (not b) && src == nodeid)
9fc1345bb54ea7f68c2e59ff3a618c1237a30918yoshiki $ labEdgesDG $ lookupDGraph ln le
fe64b2ba25510d8c9dba5560a2d537763566cf40nd foldM (\s edge -> do
fe64b2ba25510d8c9dba5560a2d537763566cf40nd s' <- link2String linkmap edge
fe64b2ba25510d8c9dba5560a2d537763566cf40nd return $ s ++ (if s /= "" then ",\n " else "") ++ s') "" edges
06ba4a61654b3763ad65f52283832ebf058fdf1cslive-- | Converts a link to String representation
06ba4a61654b3763ad65f52283832ebf058fdf1cslivelink2String :: Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String)
c68acc9d712af079afa2bd1a5a4aeef9a3ea573ckess -> LEdge DGLinkLab -> IO String
c68acc9d712af079afa2bd1a5a4aeef9a3ea573ckesslink2String linkmap (nodeid1, nodeid2, edge) = do
fb109b84906e3ee61680aa289953c2f9e859354erbowen let (EdgeId linkid) = dgl_id edge
fb109b84906e3ee61680aa289953c2f9e859354erbowen ltype = getRealDGLinkType edge
fb109b84906e3ee61680aa289953c2f9e859354erbowen (line, color) <- case Map.lookup ltype linkmap of
fb109b84906e3ee61680aa289953c2f9e859354erbowen Nothing -> error $ "SaveGraph: can't lookup linktype: " ++ show ltype
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess Just (l, c) -> return (l, c)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive name = "\"" ++ (show linkid) ++ ":" ++ (show nodeid1) ++ "->"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive ++ (show nodeid2) ++ "\""
06ba4a61654b3763ad65f52283832ebf058fdf1cslive color' = "a(\"EDGECOLOR\",\"" ++ color ++ "\"),"
fb109b84906e3ee61680aa289953c2f9e859354erbowen line' = "a(\"EDGEPATTERN\",\"" ++ (map toLower $ show line) ++ "\")"
fb109b84906e3ee61680aa289953c2f9e859354erbowen return $ "l(" ++ name ++ ",e(\"" ++ show ltype ++ "\","
fb109b84906e3ee61680aa289953c2f9e859354erbowen ++ "[" ++ color' ++ line' ++"],"
fb109b84906e3ee61680aa289953c2f9e859354erbowen ++ "r(\"" ++ (show nodeid2) ++ "\")))"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive-- | Returns the name of the Node
06ba4a61654b3763ad65f52283832ebf058fdf1cslivegetNodeLabel :: GInfo -> DGNodeLab -> IO String
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cndgetNodeLabel (GInfo {internalNamesIORef = ioRefInternal}) dgnode = do
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd internal <- readIORef ioRefInternal
06ba4a61654b3763ad65f52283832ebf058fdf1cslive let ntype = getDGNodeType dgnode
06ba4a61654b3763ad65f52283832ebf058fdf1cslive case (not $ showNames internal) &&
fb109b84906e3ee61680aa289953c2f9e859354erbowen elem ntype ["open_cons__internal"
fb109b84906e3ee61680aa289953c2f9e859354erbowen , "proven_cons__internal"
fb109b84906e3ee61680aa289953c2f9e859354erbowen , "locallyEmpty__open_cons__internal"
fb109b84906e3ee61680aa289953c2f9e859354erbowen , "locallyEmpty__proven_cons__internal"] of
06ba4a61654b3763ad65f52283832ebf058fdf1cslive True -> return ""
06ba4a61654b3763ad65f52283832ebf058fdf1cslive False -> return $ getDGNodeName dgnode