GraphLogic.hs revision e2a334fa04447bab0555008d5f785670d50e2406
97a9a944b5887e91042b019776c41d5dd74557aferikabele{-# OPTIONS -cpp #-}
97a9a944b5887e91042b019776c41d5dd74557aferikabeleModule : $Header$
a945f35eff8b6a88009ce73de6d4c862ce58de3csliveDescription : 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)
2e545ce2450a9953665f701bb05350f0d3f26275ndThis module provides functions for all the menus in the Hets GUI.
d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowenThese are then assembled to the GUI in "GUI.GraphMenu".
af33a4994ae2ff15bc67d19ff1a7feb906745bf8rbowen , performProofAction
3f08db06526d6901aa08c110b5bc7dde6bc39905nd , openProofStatus
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , saveProofStatus
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , proofMenu
3f08db06526d6901aa08c110b5bc7dde6bc39905nd , showReferencedLibrary
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , getTheoryOfNode
a63f0ab647ad2ab72efc9bea7a66e24e9ebc5cc2nd , translateTheoryOfNode
3b3b7fc78d1f5bfc2769903375050048ff41ff26nd , displaySubsortGraph
ad74a0524a06bfe11b7de9e3b4ce7233ab3bd3f7nd , displayConceptGraph
4aa805f8500255bc52a4c03259fe46df10a1d07cyoshiki , lookupTheoryOfNode
d972e4a0688f66b1402473dd9dacfecefa2132a8rbowen , showProofStatusOfNode
dfb59c684345700bf9186b8d44936f8b1ba082ffgryzor , proveAtNode
ecc5150d35c0dc5ee5119c2717e6660fa331abbftakashi , showNodeInfo
f086b4b402fa9a2fefc7dda85de2a3cc1cd0a654rjung , showEdgeInfo
3b3b7fc78d1f5bfc2769903375050048ff41ff26nd , checkconservativityOfEdge
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , hideNodes
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , hideNewProvedEdges
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , hideShowNames
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , showNodes
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , translateGraph
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna , showLibGraph
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , runAndLock
117c1f888a14e73cdd821dc6c23eb0411144a41cnd , saveUDGraph
117c1f888a14e73cdd821dc6c23eb0411144a41cnd , focusNode
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd , applyChanges
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport Logic.Logic(conservativityCheck,map_sen, comp)
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport Logic.Coerce(coerceSign, coerceMorphism)
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport Comorphisms.LogicGraph(logicGraph)
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport Static.DGTranslation(libEnv_translation, getDGLogic)
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport Proofs.InferBasic(basicInferenceNode)
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport Proofs.StatusUtils(lookupHistory, removeContraryChanges)
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport GUI.Taxonomy (displayConceptGraph,displaySubsortGraph)
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport qualified GUI.GraphAbstraction as GA
117c1f888a14e73cdd821dc6c23eb0411144a41cnd#ifdef UNIVERSION2
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport Reactor.InfoBus(encapsulateWaitTermAct)
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport HTk.Toolkit.DialogWin (useHTk)
0193f13df922db31ff281e3e5ce9632fe42bac87sfimport GraphConfigure
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport InfoBus(encapsulateWaitTermAct)
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport DialogWin (useHTk)
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport qualified GUI.HTkUtils as HTk
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport Common.DocUtils (showDoc)
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport Common.AS_Annotation (isAxiom)
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport Common.Result as Res
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport qualified Common.OrderedMap as OMap
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport qualified Common.Lib.SizedList as SizedList
2b6565aedca9e9c10691b12fd2f3689bf4c85bc7jimimport Driver.WriteLibDefn(writeShATermFile)
2b6565aedca9e9c10691b12fd2f3689bf4c85bc7jimimport Driver.ReadFn(libNameToFile, readVerbose)
6beba165aeced2ca77a6f1593ee08c47a32099efcovenerimport Driver.AnaLib(anaLib)
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport Data.Char(toLower)
9f19223e8fb7b99f5f1cc02c8c3c2c6567793262rbowenimport Data.List(partition, delete)
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport Data.Graph.Inductive.Graph (Node, LEdge, LNode)
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport qualified Data.Map as Map
117c1f888a14e73cdd821dc6c23eb0411144a41cnd-- | Locks the global lock and runs function
117c1f888a14e73cdd821dc6c23eb0411144a41cndrunAndLock :: GInfo -> IO () -> IO ()
117c1f888a14e73cdd821dc6c23eb0411144a41cndrunAndLock (GInfo { functionLock = lock
117c1f888a14e73cdd821dc6c23eb0411144a41cnd , gi_GraphInfo = actGraphInfo
117c1f888a14e73cdd821dc6c23eb0411144a41cnd }) function = do
117c1f888a14e73cdd821dc6c23eb0411144a41cnd locked <- tryPutMVar lock ()
b00fe3c3354db01001b8eddfd9b88441380f837dwrowe case locked of
117c1f888a14e73cdd821dc6c23eb0411144a41cnd takeMVar lock
e83cd73f10044371dd9dfa5f46b6d7d5c585fe54sf GA.redisplay actGraphInfo
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna "an other function is still working ... please wait ..."
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna-- | Undo one step of the History
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquernaundo :: GInfo -> Bool -> IO ()
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquernaundo gInfo@(GInfo { gi_GraphInfo = actGraphInfo }) isUndo = do
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna hhn <- GA.hasHiddenNodes actGraphInfo
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna intSt <- readIORef $ intState gInfo
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna nwSt <- if isUndo then undoOneStep intSt else redoOneStep intSt
d972e4a0688f66b1402473dd9dacfecefa2132a8rbowen writeIORef (intState gInfo) nwSt
173e5f4d5ec46b5febb74ce860d753bb1faaba0fsf if hhn then hideNodes gInfo else return ()
031bbbc0d1189b07330e38d0c126820a9ab7795egryzor-- | reloads the Library of the DevGraph
5ae609a8a09239d20f48a4a95c4f21b713995babwrowereload :: GInfo -> IO()
5ae609a8a09239d20f48a4a95c4f21b713995babwrowereload gInfo@(GInfo { gi_hetcatsOpts = opts
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe , gi_GraphInfo = actGraphInfo
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe lockGlobal gInfo
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe oldst <- readIORef $ intState gInfo
20f499565e77defe9dab24dd85c02f38a1175855nd case i_state oldst of
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen Nothing -> do
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna unlockGlobal gInfo
6fad623c3cc52b4a84d4d36538f6eed886f49f98covener Just ist -> do
6fad623c3cc52b4a84d4d36538f6eed886f49f98covener let oldle = i_libEnv ist
6fad623c3cc52b4a84d4d36538f6eed886f49f98covener ln = i_ln ist
6fad623c3cc52b4a84d4d36538f6eed886f49f98covener libdeps = dependentLibs ln oldle
6fad623c3cc52b4a84d4d36538f6eed886f49f98covener reloaded <- reloadLibs gInfo opts libdeps False
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna unlockGlobal gInfo
4aa603e6448b99f9371397d439795c91a93637eand if reloaded then "Reload complete!"
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen else "Reload not needed!"
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna-- | Reloads a library
031bbbc0d1189b07330e38d0c126820a9ab7795egryzorreloadLib :: IORef IntState -> HetcatsOpts -> LIB_NAME -> FilePath -> IO ()
031bbbc0d1189b07330e38d0c126820a9ab7795egryzorreloadLib iorst opts ln file = do
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna ost <- readIORef iorst
031bbbc0d1189b07330e38d0c126820a9ab7795egryzor case i_state ost of
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna Nothing -> return ()
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna Just ist -> do
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna let le = i_libEnv ist
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna mFunc <- case openlock $ lookupDGraph ln le of
4aa603e6448b99f9371397d439795c91a93637eand Just lock -> tryTakeMVar lock
4aa603e6448b99f9371397d439795c91a93637eand Nothing -> return Nothing
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna mres <- anaLibExt opts file le'
031bbbc0d1189b07330e38d0c126820a9ab7795egryzor case mres of
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna Just (_, newle) -> do
031bbbc0d1189b07330e38d0c126820a9ab7795egryzor nle <- case mFunc of
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna Just func -> do
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna lock <- case openlock $ lookupDGraph ln newle of
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna Just lock -> return lock
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe Nothing -> newEmptyMVar
4aa603e6448b99f9371397d439795c91a93637eand putMVar lock func
4aa603e6448b99f9371397d439795c91a93637eand return $ Map.insert ln (lookupDGraph ln newle)
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen {openlock = Just lock} newle
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe Nothing -> return newle
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe let nwst = ost { i_state = Just ist { i_libEnv = nle } }
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe writeIORef iorst nwst
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe errorDialog "Error" $ "Error when reloading file " ++ show file
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe-- | Reloads libraries if nessesary
5ae609a8a09239d20f48a4a95c4f21b713995babwrowereloadLibs :: GInfo -> HetcatsOpts -> [LIB_NAME] -> Bool -> IO Bool
5ae609a8a09239d20f48a4a95c4f21b713995babwrowereloadLibs _ _ [] reloaded = return reloaded
5ae609a8a09239d20f48a4a95c4f21b713995babwrowereloadLibs gInfo opts (ln:lns) reloaded = do
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe mfile <- existsAnSource opts {intype = GuessIn}
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe $ rmSuffix $ libNameToFile opts ln
d972e4a0688f66b1402473dd9dacfecefa2132a8rbowen case mfile of
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe Nothing -> do
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe errorDialog "Error" $ "File not found: " ++ libNameToFile opts ln
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe return False
031bbbc0d1189b07330e38d0c126820a9ab7795egryzor Just file -> do
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna oldTime <- do
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna ost <- readIORef $ intState gInfo
9f19223e8fb7b99f5f1cc02c8c3c2c6567793262rbowen case i_state ost of
9f19223e8fb7b99f5f1cc02c8c3c2c6567793262rbowen Nothing -> return $ TOD 0 0
c3c006c28c5b03892ccaef6e4d2cbb15a13a2072rbowen Just ist -> do
9f19223e8fb7b99f5f1cc02c8c3c2c6567793262rbowen let newln:_ = filter (ln ==) $ Map.keys $ i_libEnv ist
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna return $ getModTime $ getLIB_ID newln
fe64b2ba25510d8c9dba5560a2d537763566cf40nd newTime <- getModificationTime file
fe64b2ba25510d8c9dba5560a2d537763566cf40nd case reloaded || oldTime < newTime of
fe64b2ba25510d8c9dba5560a2d537763566cf40nd False -> reloadLibs gInfo opts lns False
fe64b2ba25510d8c9dba5560a2d537763566cf40nd True -> do
fe64b2ba25510d8c9dba5560a2d537763566cf40nd reloadLib (intState gInfo) opts ln file
fe64b2ba25510d8c9dba5560a2d537763566cf40nd oGraphs <- readIORef $ openGraphs gInfo
fe64b2ba25510d8c9dba5560a2d537763566cf40nd case Map.lookup ln oGraphs of
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Just gInfo' -> remakeGraph gInfo'
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Nothing -> return ()
fe64b2ba25510d8c9dba5560a2d537763566cf40nd reloadLibs gInfo opts lns True
06ba4a61654b3763ad65f52283832ebf058fdf1cslive-- | Deletes the old edges and nodes of the Graph and makes new ones
06ba4a61654b3763ad65f52283832ebf058fdf1csliveremakeGraph :: GInfo -> IO ()
06ba4a61654b3763ad65f52283832ebf058fdf1csliveremakeGraph gInfo@(GInfo { gi_GraphInfo = actGraphInfo
06ba4a61654b3763ad65f52283832ebf058fdf1cslive ost <- readIORef $ intState gInfo
fb77c505254b6e9c925e23e734463e87574f8f40kess case i_state ost of
fb77c505254b6e9c925e23e734463e87574f8f40kess Nothing -> return ()
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Just ist -> do
06ba4a61654b3763ad65f52283832ebf058fdf1cslive let le = i_libEnv ist
06ba4a61654b3763ad65f52283832ebf058fdf1cslive ln = i_ln ist
06ba4a61654b3763ad65f52283832ebf058fdf1cslive dgraph = lookupDGraph ln le
06ba4a61654b3763ad65f52283832ebf058fdf1cslive showNodes gInfo
06ba4a61654b3763ad65f52283832ebf058fdf1cslive GA.clear actGraphInfo
fb77c505254b6e9c925e23e734463e87574f8f40kess convert actGraphInfo dgraph
06ba4a61654b3763ad65f52283832ebf058fdf1cslive hideNodes gInfo
06ba4a61654b3763ad65f52283832ebf058fdf1cslive-- | Toggles to display internal node names
fb77c505254b6e9c925e23e734463e87574f8f40kesshideShowNames :: GInfo -> Bool -> IO ()
06ba4a61654b3763ad65f52283832ebf058fdf1cslivehideShowNames (GInfo { internalNamesIORef = showInternalNames
06ba4a61654b3763ad65f52283832ebf058fdf1cslive }) toggle = do
06ba4a61654b3763ad65f52283832ebf058fdf1cslive (intrn::InternalNames) <- readIORef showInternalNames
06ba4a61654b3763ad65f52283832ebf058fdf1cslive let showThem = if toggle then not $ showNames intrn else showNames intrn
06ba4a61654b3763ad65f52283832ebf058fdf1cslive showItrn s = if showThem then s else ""
fb77c505254b6e9c925e23e734463e87574f8f40kess mapM_ (\(s,upd) -> upd (\_ -> showItrn s)) $ updater intrn
06ba4a61654b3763ad65f52283832ebf058fdf1cslive writeIORef showInternalNames $ intrn {showNames = showThem}
06ba4a61654b3763ad65f52283832ebf058fdf1cslive-- | shows all hidden nodes and edges
fb77c505254b6e9c925e23e734463e87574f8f40kessshowNodes :: GInfo -> IO ()
fb77c505254b6e9c925e23e734463e87574f8f40kessshowNodes gInfo@(GInfo { gi_GraphInfo = actGraphInfo
fb77c505254b6e9c925e23e734463e87574f8f40kess hhn <- GA.hasHiddenNodes actGraphInfo
bc4b55ec8f31569d606d5680d50189a355bcd7a6rbowen case hhn of
fb77c505254b6e9c925e23e734463e87574f8f40kess True -> do
06ba4a61654b3763ad65f52283832ebf058fdf1cslive GA.showTemporaryMessage actGraphInfo "Revealing hidden nodes ..."
06ba4a61654b3763ad65f52283832ebf058fdf1cslive GA.showAll actGraphInfo
06ba4a61654b3763ad65f52283832ebf058fdf1cslive hideShowNames gInfo False
fb77c505254b6e9c925e23e734463e87574f8f40kess GA.showTemporaryMessage actGraphInfo "No hidden nodes found ..."
06ba4a61654b3763ad65f52283832ebf058fdf1cslive-- | hides all unnamed internal nodes that are proven
fb77c505254b6e9c925e23e734463e87574f8f40kesshideNodes :: GInfo -> IO ()
fb77c505254b6e9c925e23e734463e87574f8f40kesshideNodes gInfo@(GInfo { gi_GraphInfo = actGraphInfo }) = do
06ba4a61654b3763ad65f52283832ebf058fdf1cslive hhn <- GA.hasHiddenNodes actGraphInfo
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd ost <- readIORef $ intState gInfo
4aa603e6448b99f9371397d439795c91a93637eand case i_state ost of
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen Nothing -> return ()
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen Just ist -> if hhn then
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen GA.showTemporaryMessage actGraphInfo "Nodes already hidden ..."
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen GA.showTemporaryMessage actGraphInfo "Hiding unnamed nodes..."
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd let le = i_libEnv ist
fe64b2ba25510d8c9dba5560a2d537763566cf40nd ln = i_ln ist
fe64b2ba25510d8c9dba5560a2d537763566cf40nd dg = lookupDGraph ln le
fe64b2ba25510d8c9dba5560a2d537763566cf40nd nodes = selectNodesByType dg [DGNodeType
fe64b2ba25510d8c9dba5560a2d537763566cf40nd {nonRefType = NonRefType
fe64b2ba25510d8c9dba5560a2d537763566cf40nd {isProvenCons = True
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , isInternalSpec = True}
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , isLocallyEmpty = True}]
fe64b2ba25510d8c9dba5560a2d537763566cf40nd edges = getCompressedEdges dg nodes
fe64b2ba25510d8c9dba5560a2d537763566cf40nd GA.hideNodes actGraphInfo nodes edges
fe64b2ba25510d8c9dba5560a2d537763566cf40nd-- | hides all proven edges created not initialy
fe64b2ba25510d8c9dba5560a2d537763566cf40ndhideNewProvedEdges :: GInfo -> IO ()
313bb560bc5c323cfd40c9cad7335b4b8e060aedkesshideNewProvedEdges gInfo@(GInfo { gi_GraphInfo = actGraphInfo }) = do
ff797e743eb73c1d45b08158aa6b288c2d0c46eeslive ost <- readIORef $ intState gInfo
ff797e743eb73c1d45b08158aa6b288c2d0c46eeslive case i_state ost of
6b64034fa2a644ba291c484c0c01c7df5b8d982ckess Nothing -> return ()
6b64034fa2a644ba291c484c0c01c7df5b8d982ckess Just ist -> do
06ba4a61654b3763ad65f52283832ebf058fdf1cslive let ph = SizedList.toList $ proofHistory
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen $ lookupDGraph (i_ln ist) $ i_libEnv ist
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen edges = foldl (\ e c -> case c of
06ba4a61654b3763ad65f52283832ebf058fdf1cslive InsertEdge (_, _, lbl) -> (dgl_id lbl):e
06ba4a61654b3763ad65f52283832ebf058fdf1cslive DeleteEdge (_, _, lbl) -> delete (dgl_id lbl) e
06ba4a61654b3763ad65f52283832ebf058fdf1cslive ) [] $ flattenHistory ph []
06ba4a61654b3763ad65f52283832ebf058fdf1cslive mapM_ (GA.hideEdge actGraphInfo) edges
4aa603e6448b99f9371397d439795c91a93637eand-- | generates from list of HistElem one list of DGChanges
51b60896224b408a35684bd6ec0fafe5e4abe322rbowenflattenHistory :: [HistElem] -> [DGChange] -> [DGChange]
4aa603e6448b99f9371397d439795c91a93637eandflattenHistory [] cs = cs
51b60896224b408a35684bd6ec0fafe5e4abe322rbowenflattenHistory ((HistElem c):r) cs = flattenHistory r $ c:cs
fe64b2ba25510d8c9dba5560a2d537763566cf40ndflattenHistory ((HistGroup _ ph):r) cs =
fe64b2ba25510d8c9dba5560a2d537763566cf40nd flattenHistory r $ flattenHistory (SizedList.toList ph) cs
fe64b2ba25510d8c9dba5560a2d537763566cf40nd-- | selects all nodes of a type with outgoing edges
fe64b2ba25510d8c9dba5560a2d537763566cf40ndselectNodesByType :: DGraph -> [DGNodeType] -> [Node]
fe64b2ba25510d8c9dba5560a2d537763566cf40ndselectNodesByType dg types =
fe64b2ba25510d8c9dba5560a2d537763566cf40nd filter (\ n -> outDG dg n /= []) $ map fst
fe64b2ba25510d8c9dba5560a2d537763566cf40nd $ filter (\ (_, n) -> elem (getRealDGNodeType n) types) $ labNodesDG dg
fe64b2ba25510d8c9dba5560a2d537763566cf40nd-- | compresses a list of types to the highest one
fe64b2ba25510d8c9dba5560a2d537763566cf40ndcompressTypes :: Bool -> [DGEdgeType] -> (DGEdgeType, Bool)
5224ff8eae5156a05f676f1dad8add2e2f2efe1dndcompressTypes _ [] = error "compressTypes: wrong usage"
627c978514c54179736d152923478be7c8707f9bndcompressTypes b (t:[]) = (t,b)
fe64b2ba25510d8c9dba5560a2d537763566cf40ndcompressTypes b (t1:t2:r) = if t1 == t2 then compressTypes b (t1:r) else
fe64b2ba25510d8c9dba5560a2d537763566cf40nd if t1 > t2 then compressTypes False (t1:r) else compressTypes False (t2:r)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd-- | returns a list of compressed edges
fe64b2ba25510d8c9dba5560a2d537763566cf40ndgetCompressedEdges :: DGraph -> [Node] -> [(Node,Node,(DGEdgeType, Bool))]
fe64b2ba25510d8c9dba5560a2d537763566cf40ndgetCompressedEdges dg hidden = filterDuplicates $ getShortPaths
fe64b2ba25510d8c9dba5560a2d537763566cf40nd $ concatMap (\ e@(_,t,_) -> map (e:) $ getPaths dg t hidden []) inEdges
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd inEdges = filter (\ (_,t,_) -> elem t hidden)
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd $ concatMap (outDG dg)
888b616027180cc8aaa4d2bee5ecc6acec175bc5nd $ foldr (\ n i -> if elem n hidden
b95ae799514ad86a15610ad75808d7065e9847c9kess || elem n i then i else n:i) []
888b616027180cc8aaa4d2bee5ecc6acec175bc5nd $ map (\ (s,_,_) -> s) $ concatMap (innDG dg) hidden
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd-- | filter duplicate paths
5224ff8eae5156a05f676f1dad8add2e2f2efe1dndfilterDuplicates :: [(Node,Node,(DGEdgeType, Bool))]
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd -> [(Node,Node,(DGEdgeType, Bool))]
5224ff8eae5156a05f676f1dad8add2e2f2efe1dndfilterDuplicates [] = []
604c89126c27104f659d7a51b0113e3bd435faf8fieldingfilterDuplicates ((s, t, (et,b)) : r) = edge : filterDuplicates others
06ba4a61654b3763ad65f52283832ebf058fdf1cslive (same,others) = partition (\ (s',t',_) -> s == s' && t == t') r
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen b' = and $ b : map (\ (_,_,(_,b'')) -> b'') same
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen edge = (s,t,compressTypes b' $ et : map (\ (_,_,(et',_)) -> et') same)
888b616027180cc8aaa4d2bee5ecc6acec175bc5nd-- | returns the pahts of a given node through hidden nodes
5224ff8eae5156a05f676f1dad8add2e2f2efe1dndgetPaths :: DGraph -> Node -> [Node] -> [Node] -> [[LEdge DGLinkLab]]
5224ff8eae5156a05f676f1dad8add2e2f2efe1dndgetPaths dg node hidden seen' = case elem node hidden of
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd True -> case edges /= [] of
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd True -> concatMap (\ e@(_,t,_) -> map (e:) $ getPaths dg t hidden seen)
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd False -> []
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd False -> [[]]
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd seen = node:seen'
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd edges = filter (\ (_,t,_) -> notElem t seen) $ outDG dg node
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd-- | returns source and target node of a path with the compressed type
5224ff8eae5156a05f676f1dad8add2e2f2efe1dndgetShortPaths :: [[LEdge DGLinkLab]]
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd -> [(Node,Node,(DGEdgeType,Bool))]
fe64b2ba25510d8c9dba5560a2d537763566cf40ndgetShortPaths [] = []
fe64b2ba25510d8c9dba5560a2d537763566cf40ndgetShortPaths (p : r) =
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd (s, t, compressTypes True $ map (\ (_,_,e) -> getRealDGLinkType e) p)
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd : getShortPaths r
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd (s,_,_) = head p
2509f1cd3be884abbe4852e15b8da00bebaad5b1poirier (_,t,_) = last p
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd-- | Let the user select a Node to focus
4335f1cbf345c91bb996eec540c11ba8ce5d4268ndfocusNode :: GInfo -> IO ()
4335f1cbf345c91bb996eec540c11ba8ce5d4268ndfocusNode gInfo@(GInfo { gi_GraphInfo = grInfo }) = do
b09fcdfc59ada4712150e7bcc7b502bb9e4601d8rjung ost <- readIORef $ intState gInfo
2509f1cd3be884abbe4852e15b8da00bebaad5b1poirier case i_state ost of
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd Nothing -> return ()
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd Just ist -> do
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd let le = i_libEnv ist
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd ln = i_ln ist
2509f1cd3be884abbe4852e15b8da00bebaad5b1poirier idsnodes <- filterM (fmap not . GA.isHiddenNode grInfo . fst)
2509f1cd3be884abbe4852e15b8da00bebaad5b1poirier $ labNodesDG $ lookupDGraph ln le
2509f1cd3be884abbe4852e15b8da00bebaad5b1poirier selection <- listBox "Select a node to focus"
2509f1cd3be884abbe4852e15b8da00bebaad5b1poirier $ map (\ (n, l) -> shows n " " ++ getDGNodeName l) idsnodes
2509f1cd3be884abbe4852e15b8da00bebaad5b1poirier case selection of
2509f1cd3be884abbe4852e15b8da00bebaad5b1poirier Just idx -> GA.focusNode grInfo $ fst $ idsnodes !! idx
2509f1cd3be884abbe4852e15b8da00bebaad5b1poirier Nothing -> return ()
2509f1cd3be884abbe4852e15b8da00bebaad5b1poiriertranslateGraph :: GInfo -> ConvFunc -> LibFunc -> IO ()
2509f1cd3be884abbe4852e15b8da00bebaad5b1poiriertranslateGraph gInfo@(GInfo { gi_hetcatsOpts = opts
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd }) convGraph showLib = do
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd ost <- readIORef $ intState gInfo
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd case i_state ost of
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd Nothing -> return ()
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd Just ist -> do
2509f1cd3be884abbe4852e15b8da00bebaad5b1poirier let le = i_libEnv ist
2509f1cd3be884abbe4852e15b8da00bebaad5b1poirier ln = i_ln ist
2509f1cd3be884abbe4852e15b8da00bebaad5b1poirier openTranslateGraph le ln opts (getDGLogic le) convGraph showLib
4335f1cbf345c91bb996eec540c11ba8ce5d4268ndshowLibGraph :: GInfo -> LibFunc -> IO ()
4335f1cbf345c91bb996eec540c11ba8ce5d4268ndshowLibGraph gInfo showLib = do
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd showLib gInfo
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd{- | it tries to perform the given action to the given graph.
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd If part of the given graph is not hidden, then the action can
fe64b2ba25510d8c9dba5560a2d537763566cf40nd be performed directly; otherwise the graph will be shown completely
fe64b2ba25510d8c9dba5560a2d537763566cf40nd firstly, and then the action will be performed, and after that the graph
fe64b2ba25510d8c9dba5560a2d537763566cf40nd will be hidden again.
fb77c505254b6e9c925e23e734463e87574f8f40kessperformProofAction :: GInfo -> IO () -> IO ()
fe64b2ba25510d8c9dba5560a2d537763566cf40ndperformProofAction gInfo@(GInfo { gi_GraphInfo = actGraphInfo
6f7c18e70781deff3d1129774221de81b43c828end }) proofAction = do
fe64b2ba25510d8c9dba5560a2d537763566cf40nd let actionWithMessage = do
fe64b2ba25510d8c9dba5560a2d537763566cf40nd "Applying development graph calculus proof rule..."
fe64b2ba25510d8c9dba5560a2d537763566cf40nd proofAction
fb77c505254b6e9c925e23e734463e87574f8f40kess hhn <- GA.hasHiddenNodes actGraphInfo
fb77c505254b6e9c925e23e734463e87574f8f40kess case hhn of
fb77c505254b6e9c925e23e734463e87574f8f40kess True -> do
6b64034fa2a644ba291c484c0c01c7df5b8d982ckess showNodes gInfo
06ba4a61654b3763ad65f52283832ebf058fdf1cslive actionWithMessage
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess hideNodes gInfo
10673857794a4b3d9568ca2d983722a87ed352f1rbowen False -> actionWithMessage
ed0dae472b518c553c923a86fb4322d4c50d86a6nd "Development graph calculus proof rule finished."
10673857794a4b3d9568ca2d983722a87ed352f1rbowensaveProofStatus :: GInfo -> FilePath -> IO ()
10673857794a4b3d9568ca2d983722a87ed352f1rbowensaveProofStatus gInfo@(GInfo { gi_hetcatsOpts = opts
bed3c2e56e8f3328e780200466b9d009093db468sf }) file = encapsulateWaitTermAct $ do
bed3c2e56e8f3328e780200466b9d009093db468sf ost <- readIORef $ intState gInfo
bed3c2e56e8f3328e780200466b9d009093db468sf case i_state ost of
bed3c2e56e8f3328e780200466b9d009093db468sf Nothing -> return ()
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Just ist -> do
06ba4a61654b3763ad65f52283832ebf058fdf1cslive let proofStatus = i_libEnv ist
06ba4a61654b3763ad65f52283832ebf058fdf1cslive ln = i_ln ist
fb77c505254b6e9c925e23e734463e87574f8f40kess 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
06ba4a61654b3763ad65f52283832ebf058fdf1csliveopenProofStatus gInfo@(GInfo { gi_hetcatsOpts = opts
06ba4a61654b3763ad65f52283832ebf058fdf1cslive }) file convGraph showLib = do
06ba4a61654b3763ad65f52283832ebf058fdf1cslive ost <- readIORef $ intState gInfo
06ba4a61654b3763ad65f52283832ebf058fdf1cslive case i_state ost of
262bea1fd79e346411f28f66dbbb3aebc72ae42arbowen Nothing -> return ()
1f53e295ebd19aed1767d12da7abfab9936c148cjerenkrantz Just ist -> do
cb3a1082aec4b3b4f4ed238c93c3cc54933a7f0end let ln = i_ln ist
9335f6d807d76d60e54af4ededdebebddb3e3d13noodl mh <- readVerbose opts ln file
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Nothing -> errorDialog "Error" $ "Could not read proof status from file '"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive ++ file ++ "'"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Just h -> do
06ba4a61654b3763ad65f52283832ebf058fdf1cslive let libfile = libNameToFile opts ln
604c89126c27104f659d7a51b0113e3bd435faf8fielding m <- anaLib opts { outtypes = [] } libfile
604c89126c27104f659d7a51b0113e3bd435faf8fielding Nothing -> errorDialog "Error"
604c89126c27104f659d7a51b0113e3bd435faf8fielding $ "Could not read original development graph from '"
604c89126c27104f659d7a51b0113e3bd435faf8fielding ++ libfile ++ "'"
604c89126c27104f659d7a51b0113e3bd435faf8fielding Just (_, libEnv) -> case Map.lookup ln libEnv of
604c89126c27104f659d7a51b0113e3bd435faf8fielding Nothing -> errorDialog "Error" $ "Could not get original"
604c89126c27104f659d7a51b0113e3bd435faf8fielding ++ "development graph for '" ++ showDoc ln "'"
604c89126c27104f659d7a51b0113e3bd435faf8fielding Just dg -> do
e6342815b6b2be821ab51f5e867e210b47203429humbedooh lockGlobal gInfo
e6342815b6b2be821ab51f5e867e210b47203429humbedooh let oldEnv = i_libEnv ist
909ce17e2bd0faef7b1c294f2307f009793fd493nd proofStatus = Map.insert ln
909ce17e2bd0faef7b1c294f2307f009793fd493nd (applyProofHistory h dg) oldEnv
909ce17e2bd0faef7b1c294f2307f009793fd493nd nwst = ost { i_state = Just ist {
06ba4a61654b3763ad65f52283832ebf058fdf1cslive i_libEnv = proofStatus } }
06ba4a61654b3763ad65f52283832ebf058fdf1cslive writeIORef (intState gInfo) nwst
06ba4a61654b3763ad65f52283832ebf058fdf1cslive unlockGlobal gInfo
06ba4a61654b3763ad65f52283832ebf058fdf1cslive gInfo' <- copyGInfo gInfo ln
06ba4a61654b3763ad65f52283832ebf058fdf1cslive convGraph gInfo' "Proof Status " showLib
97a9a944b5887e91042b019776c41d5dd74557aferikabele let actGraphInfo = gi_GraphInfo gInfo
06ba4a61654b3763ad65f52283832ebf058fdf1cslive-- | apply a rule of the development graph calculus
06ba4a61654b3763ad65f52283832ebf058fdf1csliveproofMenu :: GInfo
897b9432efe6e6effa0939f700b1ccc50b29698crbowen -> (LibEnv -> IO (Res.Result LibEnv))
173e5f4d5ec46b5febb74ce860d753bb1faaba0fsfproofMenu gInfo@(GInfo { gi_GraphInfo = actGraphInfo
173e5f4d5ec46b5febb74ce860d753bb1faaba0fsf , gi_hetcatsOpts = hOpts
173e5f4d5ec46b5febb74ce860d753bb1faaba0fsf , proofGUIMVar = guiMVar
d1636bdc2e674b84ee46f534b51be18ecac6bef5rbowen }) str proofFun = do
a84592bb632899fd65753b227741b5ebe6b3b471jim ost <- readIORef $ intState gInfo
a84592bb632899fd65753b227741b5ebe6b3b471jim case i_state ost of
d1636bdc2e674b84ee46f534b51be18ecac6bef5rbowen Nothing -> return ()
d1636bdc2e674b84ee46f534b51be18ecac6bef5rbowen Just ist -> do
d1636bdc2e674b84ee46f534b51be18ecac6bef5rbowen let ln = i_ln ist
d1636bdc2e674b84ee46f534b51be18ecac6bef5rbowen filled <- tryPutMVar guiMVar Nothing
d1636bdc2e674b84ee46f534b51be18ecac6bef5rbowen if not filled
d1636bdc2e674b84ee46f534b51be18ecac6bef5rbowen then readMVar guiMVar >>=
d1636bdc2e674b84ee46f534b51be18ecac6bef5rbowen maybe (putIfVerbose hOpts 0 "proofMenu: ignored Nothing")
d1636bdc2e674b84ee46f534b51be18ecac6bef5rbowen putIfVerbose hOpts 4 $
d1636bdc2e674b84ee46f534b51be18ecac6bef5rbowen "proofMenu: Ignored Proof command; " ++
d1636bdc2e674b84ee46f534b51be18ecac6bef5rbowen "maybe a proof window is still open?"
d1636bdc2e674b84ee46f534b51be18ecac6bef5rbowen lockGlobal gInfo
2e1ba74a0ed02fe61c93492e3958934e750f0b0end let proofStatus = i_libEnv ist
d1636bdc2e674b84ee46f534b51be18ecac6bef5rbowen putIfVerbose hOpts 4 "Proof started via \"Proofs\" menu"
d1636bdc2e674b84ee46f534b51be18ecac6bef5rbowen Res.Result ds res <- proofFun proofStatus
d1636bdc2e674b84ee46f534b51be18ecac6bef5rbowen putIfVerbose hOpts 4 "Analyzing result of proof"
d1636bdc2e674b84ee46f534b51be18ecac6bef5rbowen case res of
d1636bdc2e674b84ee46f534b51be18ecac6bef5rbowen Nothing -> do
a84592bb632899fd65753b227741b5ebe6b3b471jim unlockGlobal gInfo
8e31885fc494b603e0650113dde9e29d1b1d2602maczniak printDiags 2 ds
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Just newProofStatus -> do
06ba4a61654b3763ad65f52283832ebf058fdf1cslive let newGr = lookupDGraph ln newProofStatus
06ba4a61654b3763ad65f52283832ebf058fdf1cslive history = snd $ splitHistory (lookupDGraph ln proofStatus) newGr
97a9a944b5887e91042b019776c41d5dd74557aferikabele doDump hOpts "PrintHistory" $ do
8e31885fc494b603e0650113dde9e29d1b1d2602maczniak putStrLn "History"
8e31885fc494b603e0650113dde9e29d1b1d2602maczniak print $ prettyHistory history
a011221d1a3bfb6ec07a3596c6dc962c58041ee6covener let lln = map (\x-> DgCommandChange x) $ calcGlobalHistory
a011221d1a3bfb6ec07a3596c6dc962c58041ee6covener proofStatus newProofStatus
a011221d1a3bfb6ec07a3596c6dc962c58041ee6covener nmStr = strToCmd str
2b6565aedca9e9c10691b12fd2f3689bf4c85bc7jim nst = add2history nmStr ost lln
a011221d1a3bfb6ec07a3596c6dc962c58041ee6covener -- nst = foldl (add2history nmStr) ost lln
a011221d1a3bfb6ec07a3596c6dc962c58041ee6covener -- (calcGlobalHistory proofStatus newProofStatus : guHist, grHist)
a011221d1a3bfb6ec07a3596c6dc962c58041ee6covener applyChanges actGraphInfo $ reverse
a011221d1a3bfb6ec07a3596c6dc962c58041ee6covener $ flatHistory history
a011221d1a3bfb6ec07a3596c6dc962c58041ee6covener let nwst = nst { i_state = Just ist { i_libEnv=newProofStatus}}
173e5f4d5ec46b5febb74ce860d753bb1faaba0fsf writeIORef (intState gInfo) nwst
173e5f4d5ec46b5febb74ce860d753bb1faaba0fsf unlockGlobal gInfo
173e5f4d5ec46b5febb74ce860d753bb1faaba0fsf hideShowNames gInfo False
173e5f4d5ec46b5febb74ce860d753bb1faaba0fsf mGUIMVar <- tryTakeMVar guiMVar
a011221d1a3bfb6ec07a3596c6dc962c58041ee6covener maybe (fail "should be filled with Nothing after proof attempt")
06ba4a61654b3763ad65f52283832ebf058fdf1cslive (const $ return ())
06ba4a61654b3763ad65f52283832ebf058fdf1cslivecalcGlobalHistory :: LibEnv -> LibEnv -> [LIB_NAME]
51b60896224b408a35684bd6ec0fafe5e4abe322rbowencalcGlobalHistory old new = let
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen length' ln = SizedList.size . proofHistory . lookupDGraph ln
fe64b2ba25510d8c9dba5560a2d537763566cf40nd changes = filter (\ ln -> length' ln old < length' ln new) $ Map.keys old
ed0dae472b518c553c923a86fb4322d4c50d86a6nd in concatMap (\ ln -> replicate (length' ln new - length' ln old) ln) changes
ed0dae472b518c553c923a86fb4322d4c50d86a6ndnodeErr :: Int -> IO ()
ed0dae472b518c553c923a86fb4322d4c50d86a6ndnodeErr descr = error $ "node with descriptor " ++ show descr
da637bcae7b6e150470e701af29da5604a34a17erbowen ++ " has no corresponding node in the development graph"
da637bcae7b6e150470e701af29da5604a34a17erbowenshowNodeInfo :: Int -> DGraph -> IO ()
da637bcae7b6e150470e701af29da5604a34a17erbowenshowNodeInfo descr dgraph = do
da637bcae7b6e150470e701af29da5604a34a17erbowen let dgnode = labDG dgraph descr
da637bcae7b6e150470e701af29da5604a34a17erbowen title = (if isDGRef dgnode then ("reference " ++) else
da637bcae7b6e150470e701af29da5604a34a17erbowen if isInternalNode dgnode then ("internal " ++) else id)
da637bcae7b6e150470e701af29da5604a34a17erbowen "node " ++ getDGNodeName dgnode ++ " " ++ show descr
7802d43d20007fa575e43b6ae77d5177ceffdb71sf createTextDisplay title (title ++ "\n" ++ showDoc dgnode "")
7802d43d20007fa575e43b6ae77d5177ceffdb71sf fetches the theory from a node inside the IO Monad
7802d43d20007fa575e43b6ae77d5177ceffdb71sf (added by KL based on code in getTheoryOfNode) -}
7802d43d20007fa575e43b6ae77d5177ceffdb71sflookupTheoryOfNode :: LibEnv -> LIB_NAME -> Int
7802d43d20007fa575e43b6ae77d5177ceffdb71sf -> IO (Res.Result (LibEnv, Node, G_theory))
bed3c2e56e8f3328e780200466b9d009093db468sflookupTheoryOfNode libEnv ln descr =
bed3c2e56e8f3328e780200466b9d009093db468sf return $ do
bed3c2e56e8f3328e780200466b9d009093db468sf (libEnv', gth) <- computeTheory True libEnv ln descr
bed3c2e56e8f3328e780200466b9d009093db468sf return (libEnv', descr, gth)
bed3c2e56e8f3328e780200466b9d009093db468sfshowDiagMessAux :: Int -> [Diagnosis] -> IO ()
bed3c2e56e8f3328e780200466b9d009093db468sfshowDiagMessAux v ds = let es = Res.filterDiags v ds in
bed3c2e56e8f3328e780200466b9d009093db468sf if null es then return () else
bed3c2e56e8f3328e780200466b9d009093db468sf (if hasErrors es then errorDialog "Error" else infoDialog "Info") $ unlines
bed3c2e56e8f3328e780200466b9d009093db468sf $ map show es
bed3c2e56e8f3328e780200466b9d009093db468sfshowDiagMess :: HetcatsOpts -> [Diagnosis] -> IO ()
bed3c2e56e8f3328e780200466b9d009093db468sfshowDiagMess = showDiagMessAux . verbose
bed3c2e56e8f3328e780200466b9d009093db468sf{- | outputs the theory of a node in a window;
bed3c2e56e8f3328e780200466b9d009093db468sfused by the node menu defined in initializeGraph-}
bed3c2e56e8f3328e780200466b9d009093db468sfgetTheoryOfNode :: GInfo -> Int -> DGraph -> IO ()
bed3c2e56e8f3328e780200466b9d009093db468sfgetTheoryOfNode gInfo@(GInfo { gi_GraphInfo = actGraphInfo
bed3c2e56e8f3328e780200466b9d009093db468sf }) descr dgraph = do
bed3c2e56e8f3328e780200466b9d009093db468sf ost <- readIORef $ intState gInfo
bed3c2e56e8f3328e780200466b9d009093db468sf case i_state ost of
bed3c2e56e8f3328e780200466b9d009093db468sf Nothing -> return ()
bed3c2e56e8f3328e780200466b9d009093db468sf Just ist -> do
bed3c2e56e8f3328e780200466b9d009093db468sf let le = i_libEnv ist
bed3c2e56e8f3328e780200466b9d009093db468sf ln = i_ln ist
bed3c2e56e8f3328e780200466b9d009093db468sf r <- lookupTheoryOfNode le ln descr
bed3c2e56e8f3328e780200466b9d009093db468sf Res.Result ds res -> do
bed3c2e56e8f3328e780200466b9d009093db468sf showDiagMess (gi_hetcatsOpts gInfo) ds
bed3c2e56e8f3328e780200466b9d009093db468sf case res of
bed3c2e56e8f3328e780200466b9d009093db468sf (Just (le', n, gth)) -> do
bed3c2e56e8f3328e780200466b9d009093db468sf lockGlobal gInfo
4aa603e6448b99f9371397d439795c91a93637eand displayTheoryWithWarning "Theory" (getNameOfNode n dgraph)
4aa603e6448b99f9371397d439795c91a93637eand (addHasInHidingWarning dgraph n) gth
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen let newGr = lookupDGraph ln le'
bed3c2e56e8f3328e780200466b9d009093db468sf history = snd $ splitHistory (lookupDGraph ln le) newGr
bed3c2e56e8f3328e780200466b9d009093db468sf applyChanges actGraphInfo $ reverse $ flatHistory history
bed3c2e56e8f3328e780200466b9d009093db468sf let nwst = ost { i_state = Just $ist { i_libEnv = le'} }
bed3c2e56e8f3328e780200466b9d009093db468sf writeIORef (intState gInfo) nwst
bed3c2e56e8f3328e780200466b9d009093db468sf unlockGlobal gInfo
bed3c2e56e8f3328e780200466b9d009093db468sf _ -> return ()
4aa603e6448b99f9371397d439795c91a93637eand{- | translate the theory of a node in a window;
4aa603e6448b99f9371397d439795c91a93637eandused by the node menu defined in initializeGraph-}
51b60896224b408a35684bd6ec0fafe5e4abe322rbowentranslateTheoryOfNode :: GInfo -> Int -> DGraph -> IO ()
bed3c2e56e8f3328e780200466b9d009093db468sftranslateTheoryOfNode
b244bbf442a0aea3dc397b4d0d751f4716c5891dnd gInfo@(GInfo {gi_hetcatsOpts = opts}) node dgraph = do
bed3c2e56e8f3328e780200466b9d009093db468sf ost <- readIORef $ intState gInfo
bed3c2e56e8f3328e780200466b9d009093db468sf case i_state ost of
173e5f4d5ec46b5febb74ce860d753bb1faaba0fsf Nothing -> return ()
bed3c2e56e8f3328e780200466b9d009093db468sf Just ist -> do
bed3c2e56e8f3328e780200466b9d009093db468sf let libEnv = i_libEnv ist
fe64b2ba25510d8c9dba5560a2d537763566cf40nd ln = i_ln ist
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Res.Result ds mEnv = computeTheory False libEnv ln node
fe64b2ba25510d8c9dba5560a2d537763566cf40nd case mEnv of
bed3c2e56e8f3328e780200466b9d009093db468sf Just (_, th@(G_theory lid sign _ sens _)) -> do
fe64b2ba25510d8c9dba5560a2d537763566cf40nd -- find all comorphism paths starting from lid
fe64b2ba25510d8c9dba5560a2d537763566cf40nd let paths = findComorphismPaths logicGraph (sublogicOfTh th)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd -- let the user choose one
fe64b2ba25510d8c9dba5560a2d537763566cf40nd sel <- listBox "Choose a node logic translation" $ map show paths
fe64b2ba25510d8c9dba5560a2d537763566cf40nd case sel of
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Nothing -> errorDialog "Error" "no node logic translation chosen"
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Just i -> do
fb77c505254b6e9c925e23e734463e87574f8f40kess Comorphism cid <- return (paths!!i)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd -- adjust lid's
fb77c505254b6e9c925e23e734463e87574f8f40kess let lidS = sourceLogic cid
fe64b2ba25510d8c9dba5560a2d537763566cf40nd lidT = targetLogic cid
fe64b2ba25510d8c9dba5560a2d537763566cf40nd sign' <- coerceSign lid lidS "" sign
fe64b2ba25510d8c9dba5560a2d537763566cf40nd sens' <- coerceThSens lid lidS "" sens
fe64b2ba25510d8c9dba5560a2d537763566cf40nd -- translate theory along chosen comorphism
c985aca104389df30d6ec0a637ce0ccaac904362nd let Result es mTh = wrapMapTheory cid
fe64b2ba25510d8c9dba5560a2d537763566cf40nd (plainSign sign', toNamedList sens')
88d86cfadffe2275a3dfb67a4d7bdc018630b661rbowen case mTh of
fb77c505254b6e9c925e23e734463e87574f8f40kess Nothing -> showDiagMess opts es
fb77c505254b6e9c925e23e734463e87574f8f40kess Just (sign'', sens1) -> displayTheoryWithWarning
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess "Translated Theory" (getNameOfNode node dgraph)
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess (addHasInHidingWarning dgraph node)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd (G_theory lidT (mkExtSign sign'') startSigId
fe64b2ba25510d8c9dba5560a2d537763566cf40nd (toThSens sens1) startThId)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Nothing -> showDiagMess opts ds
fe64b2ba25510d8c9dba5560a2d537763566cf40nd-- | Show proof status of a node
627c978514c54179736d152923478be7c8707f9bndshowProofStatusOfNode :: GInfo -> Int -> DGraph -> IO ()
fe64b2ba25510d8c9dba5560a2d537763566cf40ndshowProofStatusOfNode _ descr dgraph = do
fb77c505254b6e9c925e23e734463e87574f8f40kess let dgnode = labDG dgraph descr
fb77c505254b6e9c925e23e734463e87574f8f40kess stat = showStatusAux dgnode
fe64b2ba25510d8c9dba5560a2d537763566cf40nd title = "Proof status of node "++showName (dgn_name dgnode)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd createTextDisplay title stat
fe64b2ba25510d8c9dba5560a2d537763566cf40ndshowStatusAux :: DGNodeLab -> String
fe64b2ba25510d8c9dba5560a2d537763566cf40ndshowStatusAux dgnode =
06ba4a61654b3763ad65f52283832ebf058fdf1cslive case dgn_theory dgnode of
06ba4a61654b3763ad65f52283832ebf058fdf1cslive G_theory _ _ _ sens _ ->
5bb5fba250bf526bc51d13b25378d54acb93c1cbnoodl 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
06ba4a61654b3763ad65f52283832ebf058fdf1cslive then consGoal
06ba4a61654b3763ad65f52283832ebf058fdf1cslive ++ "\nOpen proof goals:\n"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive ++ showDoc open ""
06ba4a61654b3763ad65f52283832ebf058fdf1cslive ++ if hasOpenConsStatus False dgnode
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd then consGoal
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd-- | start local theorem proving or consistency checking at a node
06ba4a61654b3763ad65f52283832ebf058fdf1csliveproveAtNode :: Maybe Bool -> GInfo -> Int -> DGraph -> IO ()
06ba4a61654b3763ad65f52283832ebf058fdf1csliveproveAtNode checkCons gInfo descr dgraph = do
06ba4a61654b3763ad65f52283832ebf058fdf1cslive ost <- readIORef $ intState gInfo
06ba4a61654b3763ad65f52283832ebf058fdf1cslive case i_state ost of
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Nothing -> return ()
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Just ist -> do
fb77c505254b6e9c925e23e734463e87574f8f40kess let ln = i_ln ist
fb77c505254b6e9c925e23e734463e87574f8f40kess le = i_libEnv ist
fb77c505254b6e9c925e23e734463e87574f8f40kess dgn = labDG dgraph descr
fe64b2ba25510d8c9dba5560a2d537763566cf40nd libNode = (ln, descr)
9464a57d17bd3db87268f8eed322ceb65cfec818jim dgn' <- case hasLock dgn of
9464a57d17bd3db87268f8eed322ceb65cfec818jim True -> return dgn
9464a57d17bd3db87268f8eed322ceb65cfec818jim False -> do
9464a57d17bd3db87268f8eed322ceb65cfec818jim lockGlobal gInfo
9464a57d17bd3db87268f8eed322ceb65cfec818jim (dgraph', dgn') <- initLocking (lookupDGraph ln le) (descr, dgn)
9464a57d17bd3db87268f8eed322ceb65cfec818jim let nwle = Map.insert ln dgraph' le
9464a57d17bd3db87268f8eed322ceb65cfec818jim nwst = ost { i_state = Just $ ist { i_libEnv = nwle} }
9464a57d17bd3db87268f8eed322ceb65cfec818jim writeIORef (intState gInfo) nwst
9464a57d17bd3db87268f8eed322ceb65cfec818jim unlockGlobal gInfo
9464a57d17bd3db87268f8eed322ceb65cfec818jim return dgn'
0237f43ab925775250e266e479d0a337ff374a4btakashi locked <- tryLockLocal dgn'
9464a57d17bd3db87268f8eed322ceb65cfec818jim case locked of
9464a57d17bd3db87268f8eed322ceb65cfec818jim False -> errorDialog "Error" "Proofwindow already open"
9464a57d17bd3db87268f8eed322ceb65cfec818jim True -> do
9464a57d17bd3db87268f8eed322ceb65cfec818jim let checkCons2 = fromMaybe False checkCons
9a2ff606f1e9b86fdb5ab5d9738a8deb648cbd0btrawick action = do
9464a57d17bd3db87268f8eed322ceb65cfec818jim guiMVar <- newMVar Nothing
c8b79d4b8796531f19dd54bd59d88c3b68338ceahumbedooh res <- basicInferenceNode checkCons logicGraph libNode ln
4aa603e6448b99f9371397d439795c91a93637eand guiMVar le (intState gInfo)
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen runProveAtNode checkCons2 gInfo (descr, dgn') res
9464a57d17bd3db87268f8eed322ceb65cfec818jim unlockLocal dgn'
9464a57d17bd3db87268f8eed322ceb65cfec818jim case checkCons2 ||
9464a57d17bd3db87268f8eed322ceb65cfec818jim not (labelHasHiding dgn') of
9464a57d17bd3db87268f8eed322ceb65cfec818jim True -> do
9464a57d17bd3db87268f8eed322ceb65cfec818jim forkIO action
9464a57d17bd3db87268f8eed322ceb65cfec818jim False -> do
9464a57d17bd3db87268f8eed322ceb65cfec818jim b <- warningDialog "Warning"
9464a57d17bd3db87268f8eed322ceb65cfec818jim ("This node has incoming hiding links!\n" ++
9464a57d17bd3db87268f8eed322ceb65cfec818jim "You should compute the normal form first, " ++
9464a57d17bd3db87268f8eed322ceb65cfec818jim "preferably by applying Proofs -> TheoremHideShift," ++
9464a57d17bd3db87268f8eed322ceb65cfec818jim " otherwise the flattened theory may be too weak. " ++
9464a57d17bd3db87268f8eed322ceb65cfec818jim "In particular, disproving and consistency checks " ++
9464a57d17bd3db87268f8eed322ceb65cfec818jim "might produce wrong results. " ++
9464a57d17bd3db87268f8eed322ceb65cfec818jim " Prove anyway?")
9464a57d17bd3db87268f8eed322ceb65cfec818jim $ Just action
fe64b2ba25510d8c9dba5560a2d537763566cf40nd unless b $ unlockLocal dgn'
fe64b2ba25510d8c9dba5560a2d537763566cf40ndrunProveAtNode :: Bool -> GInfo -> LNode DGNodeLab
604c89126c27104f659d7a51b0113e3bd435faf8fielding -> Res.Result (LibEnv, Res.Result G_theory) -> IO ()
604c89126c27104f659d7a51b0113e3bd435faf8fieldingrunProveAtNode checkCons gInfo (v, dgnode) res = case maybeResult res of
604c89126c27104f659d7a51b0113e3bd435faf8fielding Just (le, tres) -> do
604c89126c27104f659d7a51b0113e3bd435faf8fielding ost <- readIORef $ intState gInfo
604c89126c27104f659d7a51b0113e3bd435faf8fielding case i_state ost of
604c89126c27104f659d7a51b0113e3bd435faf8fielding Nothing -> return ()
604c89126c27104f659d7a51b0113e3bd435faf8fielding Just ist -> do
fe64b2ba25510d8c9dba5560a2d537763566cf40nd let ln = i_ln ist
fe64b2ba25510d8c9dba5560a2d537763566cf40nd nodetext = getDGNodeName dgnode ++ " node: " ++ show v
fe64b2ba25510d8c9dba5560a2d537763566cf40nd when checkCons $ case maybeResult tres of
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Just gth -> createTextSaveDisplay
b09fcdfc59ada4712150e7bcc7b502bb9e4601d8rjung ("Model for " ++ nodetext)
b09fcdfc59ada4712150e7bcc7b502bb9e4601d8rjung "model.log" $ showDoc gth ""
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Nothing -> case diags tres of
604c89126c27104f659d7a51b0113e3bd435faf8fielding ds -> infoDialog nodetext
604c89126c27104f659d7a51b0113e3bd435faf8fielding $ unlines $ "could not (re-)construct a model" : map diagString ds
604c89126c27104f659d7a51b0113e3bd435faf8fielding proofMenu gInfo "mergeDGNodeLab" $ mergeDGNodeLab gInfo
06ba4a61654b3763ad65f52283832ebf058fdf1cslive (v, labDG (lookupDGraph ln le) v)
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen mergeHistoryLast2Entries gInfo
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen Nothing -> showDiagMessAux 2 $ diags res
604c89126c27104f659d7a51b0113e3bd435faf8fieldingmergeDGNodeLab :: GInfo -> LNode DGNodeLab -> LibEnv -> IO (Res.Result LibEnv)
604c89126c27104f659d7a51b0113e3bd435faf8fieldingmergeDGNodeLab gInfo (v, new_dgn) le = do
604c89126c27104f659d7a51b0113e3bd435faf8fielding ost <- readIORef $ intState gInfo
604c89126c27104f659d7a51b0113e3bd435faf8fielding case i_state ost of
604c89126c27104f659d7a51b0113e3bd435faf8fielding Nothing -> return (Result [] (Just le))
604c89126c27104f659d7a51b0113e3bd435faf8fielding Just ist -> do
604c89126c27104f659d7a51b0113e3bd435faf8fielding let ln = i_ln ist
604c89126c27104f659d7a51b0113e3bd435faf8fielding dg = lookupDGraph ln le
604c89126c27104f659d7a51b0113e3bd435faf8fielding old_dgn = labDG dg v
604c89126c27104f659d7a51b0113e3bd435faf8fielding return $ do
fe64b2ba25510d8c9dba5560a2d537763566cf40nd theory <- joinG_sentences (dgn_theory old_dgn) $ dgn_theory new_dgn
9597f440430d8c876dd64f5f78066804650a18ecnoodl let new_dgn' = old_dgn { dgn_theory = theory }
9597f440430d8c876dd64f5f78066804650a18ecnoodl dg'' = changeDGH dg $ SetNodeLab old_dgn (v, new_dgn')
9597f440430d8c876dd64f5f78066804650a18ecnoodl return $ Map.insert ln dg'' le
141fd59714368d3bbe3a3d8f5b8dc8a516c48f9fsf-- | print the id, origin, type, proof-status and morphism of the edge
141fd59714368d3bbe3a3d8f5b8dc8a516c48f9fsfshowEdgeInfo :: Int -> Maybe (LEdge DGLinkLab) -> IO ()
141fd59714368d3bbe3a3d8f5b8dc8a516c48f9fsfshowEdgeInfo descr me = case me of
9597f440430d8c876dd64f5f78066804650a18ecnoodl Just e@(_, _, l) -> let estr = showLEdge e in
9597f440430d8c876dd64f5f78066804650a18ecnoodl createTextDisplay ("Info of " ++ estr)
9597f440430d8c876dd64f5f78066804650a18ecnoodl (estr ++ "\n" ++ showDoc l "")
141fd59714368d3bbe3a3d8f5b8dc8a516c48f9fsf Nothing -> errorDialog "Error"
141fd59714368d3bbe3a3d8f5b8dc8a516c48f9fsf ("edge " ++ show descr ++ " has no corresponding edge"
141fd59714368d3bbe3a3d8f5b8dc8a516c48f9fsf ++ "in the development graph")
141fd59714368d3bbe3a3d8f5b8dc8a516c48f9fsfconservativityRule :: DGRule
141fd59714368d3bbe3a3d8f5b8dc8a516c48f9fsfconservativityRule = DGRule "ConservativityCheck"
141fd59714368d3bbe3a3d8f5b8dc8a516c48f9fsf-- | check conservativity of the edge
141fd59714368d3bbe3a3d8f5b8dc8a516c48f9fsfcheckconservativityOfEdge :: Int -> GInfo -> Maybe (LEdge DGLinkLab) -> IO ()
141fd59714368d3bbe3a3d8f5b8dc8a516c48f9fsfcheckconservativityOfEdge _ gInfo@(GInfo{ gi_GraphInfo = actGraphInfo})
141fd59714368d3bbe3a3d8f5b8dc8a516c48f9fsf (Just (source,target,linklab)) = do
141fd59714368d3bbe3a3d8f5b8dc8a516c48f9fsf ost <- readIORef $ intState gInfo
4aa603e6448b99f9371397d439795c91a93637eand case i_state ost of
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen Nothing -> return ()
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen Just ist -> do
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen let ln = i_ln ist
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen libEnv' = i_libEnv ist
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen lockGlobal gInfo
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen let (_, thTar) =
fb9a29a1e2aead6930d492f7c4bca2f8ae653db7rbowen case computeTheory True libEnv' ln target of
4aa603e6448b99f9371397d439795c91a93637eand Res.Result _ (Just th1) -> th1
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen _ -> error "checkconservativityOfEdge: computeTheory"
9597f440430d8c876dd64f5f78066804650a18ecnoodl G_theory lid _sign _ sensTar _ <- return thTar
cba8c0896ba04d42cf9a9e50df5040fd6bae14a4sf GMorphism cid _ _ morphism2 _ <- return $ dgl_morphism linklab
cba8c0896ba04d42cf9a9e50df5040fd6bae14a4sf morphism2' <- coerceMorphism (targetLogic cid) lid
cba8c0896ba04d42cf9a9e50df5040fd6bae14a4sf "checkconservativityOfEdge2" morphism2
fe64b2ba25510d8c9dba5560a2d537763566cf40nd let compMor = case dgn_sigma $ labDG (lookupDGraph ln libEnv') target of
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Nothing -> morphism2'
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Just (GMorphism cid' _ _ morphism3 _) -> case
fe64b2ba25510d8c9dba5560a2d537763566cf40nd do morphism3' <- coerceMorphism (targetLogic cid') lid
fe64b2ba25510d8c9dba5560a2d537763566cf40nd "checkconservativityOfEdge3" morphism3
cb43ec0a02f97651bf2f46c9f4b9b48d5cb22df7rbowen comp morphism2' morphism3' of
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Res.Result _ (Just phi) -> phi
fe64b2ba25510d8c9dba5560a2d537763566cf40nd _ -> error "checkconservativtiyOfEdge: comp"
fe64b2ba25510d8c9dba5560a2d537763566cf40nd let (_le', thSrc) =
fe64b2ba25510d8c9dba5560a2d537763566cf40nd case computeTheory False libEnv' ln source of
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Res.Result _ (Just th1) -> th1
fe64b2ba25510d8c9dba5560a2d537763566cf40nd _ -> error "checkconservativityOfEdge: computeTheory"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive G_theory lid1 sign1 _ sensSrc1 _ <- return thSrc
06ba4a61654b3763ad65f52283832ebf058fdf1cslive sign2 <- coerceSign lid1 lid "checkconservativityOfEdge.coerceSign" sign1
cb43ec0a02f97651bf2f46c9f4b9b48d5cb22df7rbowen sensSrc2 <- coerceThSens lid1 lid "checkconservativityOfEdge1" sensSrc1
031bbbc0d1189b07330e38d0c126820a9ab7795egryzor let transSensSrc = propagateErrors
cb43ec0a02f97651bf2f46c9f4b9b48d5cb22df7rbowen $ mapThSensValueM (map_sen lid compMor) sensSrc2
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd if length (conservativityCheck lid) < 1
fb77c505254b6e9c925e23e734463e87574f8f40kess errorDialog "Result of conservativity check"
fb77c505254b6e9c925e23e734463e87574f8f40kess "No conservativity checkers available"
fb77c505254b6e9c925e23e734463e87574f8f40kess unlockGlobal gInfo
ff797e743eb73c1d45b08158aa6b288c2d0c46eeslive checkerR <- conservativityChoser $ conservativityCheck lid
4aa603e6448b99f9371397d439795c91a93637eand errorDialog "Result of conservativity check"
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen "No conservativity checker chosen"
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd unlockGlobal gInfo
88d86cfadffe2275a3dfb67a4d7bdc018630b661rbowen let chCons = checkConservativity $
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd fromMaybe (error "checkconservativityOfEdge4")
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd (plainSign sign2, toNamedList sensSrc2)
b06660a3ed3d885e15d99c0209a46c4657df33fbrbowen compMor $ toNamedList
d1348237b33bc1755b9f1165eea52317465a7671nd (sensTar `OMap.difference` transSensSrc)
d1348237b33bc1755b9f1165eea52317465a7671nd showObls [] = ""
06ba4a61654b3763ad65f52283832ebf058fdf1cslive showObls obls= ", provided that the following proof obligations "
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd ++ "can be discharged:\n"
4aa603e6448b99f9371397d439795c91a93637eand ++ concatMap (flip showDoc "\n") obls
8672e74389242ff408471525b8563f85f7d369fdhumbedooh showRes = case res of
4aa603e6448b99f9371397d439795c91a93637eand Just (Just (cst, obls)) -> "The link is "
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen ++ showConsistencyStatus cst ++ showObls obls
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd _ -> "Could not determine whether link is conservative"
fb77c505254b6e9c925e23e734463e87574f8f40kess myDiags = showRelDiags 2 ds
fb77c505254b6e9c925e23e734463e87574f8f40kess createTextDisplay "Result of conservativity check"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive (showRes ++ "\n" ++ myDiags)
6b64034fa2a644ba291c484c0c01c7df5b8d982ckess let consShow = case res of
6b64034fa2a644ba291c484c0c01c7df5b8d982ckess Just (Just (cst, _)) -> cst
06ba4a61654b3763ad65f52283832ebf058fdf1cslive _ -> Unknown "Unknown"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive consNew csv = if show csv == showToComply consShow
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Proven conservativityRule emptyProofBasis
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen (newDglType, change) = case dgl_type linklab of
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen GlobalThm proven conserv _ ->
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen (GlobalThm proven conserv $ consNew conserv, True)
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen LocalThm proven conserv _ ->
4aa603e6448b99f9371397d439795c91a93637eand (LocalThm proven conserv $ consNew conserv, True)
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen t -> (t, False)
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd provenEdge = (source
06ba4a61654b3763ad65f52283832ebf058fdf1cslive dgl_type = newDglType
06ba4a61654b3763ad65f52283832ebf058fdf1cslive changes = if change then [ DeleteEdge (source,target,linklab)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive , InsertEdge provenEdge ] else []
6b64034fa2a644ba291c484c0c01c7df5b8d982ckess dg = lookupDGraph ln libEnv'
06ba4a61654b3763ad65f52283832ebf058fdf1cslive nextGr = changesDGH dg changes
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess newLibEnv = Map.insert ln
6b64034fa2a644ba291c484c0c01c7df5b8d982ckess (groupHistory dg conservativityRule nextGr) libEnv'
6b64034fa2a644ba291c484c0c01c7df5b8d982ckess history = snd $ splitHistory dg nextGr
06ba4a61654b3763ad65f52283832ebf058fdf1cslive applyChanges actGraphInfo $ reverse
06ba4a61654b3763ad65f52283832ebf058fdf1cslive $ flatHistory history
06ba4a61654b3763ad65f52283832ebf058fdf1cslive let nwst = ost { i_state = Just $ ist { i_libEnv = newLibEnv}}
06ba4a61654b3763ad65f52283832ebf058fdf1cslive writeIORef (intState gInfo) nwst
06ba4a61654b3763ad65f52283832ebf058fdf1cslive unlockGlobal gInfo
4aa603e6448b99f9371397d439795c91a93637eandcheckconservativityOfEdge descr _ Nothing =
c8b79d4b8796531f19dd54bd59d88c3b68338ceahumbedooh errorDialog "Error"
4aa603e6448b99f9371397d439795c91a93637eand ("edge " ++ show descr ++ " has no corresponding edge "
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen ++ "in the development graph")
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess-- | Graphical choser for conservativity checkers
6b64034fa2a644ba291c484c0c01c7df5b8d982ckessconservativityChoser :: [ConservativityChecker sign sentence morphism]
6b64034fa2a644ba291c484c0c01c7df5b8d982ckess (Res.Result (ConservativityChecker
6b64034fa2a644ba291c484c0c01c7df5b8d982ckess sign sentence morphism))
6b64034fa2a644ba291c484c0c01c7df5b8d982ckessconservativityChoser checkers = case checkers of
06ba4a61654b3763ad65f52283832ebf058fdf1cslive [] -> return $ fail "No conservativity checkers available"
88d86cfadffe2275a3dfb67a4d7bdc018630b661rbowen [hd] -> return $ return hd
06ba4a61654b3763ad65f52283832ebf058fdf1cslive chosenOne <- listBox "Pick a conservativity checker"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive $ map checker_id checkers
06ba4a61654b3763ad65f52283832ebf058fdf1cslive case chosenOne of
4aa603e6448b99f9371397d439795c91a93637eand Nothing -> return $ fail "No conservativity checker chosen"
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen Just i -> return $ return $ checkers !! i
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen-- | converts a DGraph
06ba4a61654b3763ad65f52283832ebf058fdf1csliveconvert :: GA.GraphInfo -> DGraph -> IO ()
06ba4a61654b3763ad65f52283832ebf058fdf1csliveconvert ginfo dgraph = do
06ba4a61654b3763ad65f52283832ebf058fdf1cslive convertNodes ginfo dgraph
fb77c505254b6e9c925e23e734463e87574f8f40kess convertEdges ginfo dgraph
fb77c505254b6e9c925e23e734463e87574f8f40kess{- | converts the nodes of the development graph, if it has any,
fb77c505254b6e9c925e23e734463e87574f8f40kessand returns the resulting conversion maps
97a9a944b5887e91042b019776c41d5dd74557aferikabeleif the graph is empty the conversion maps are returned unchanged-}
fe64b2ba25510d8c9dba5560a2d537763566cf40ndconvertNodes :: GA.GraphInfo -> DGraph -> IO ()
fe64b2ba25510d8c9dba5560a2d537763566cf40ndconvertNodes ginfo = mapM_ (convertNodesAux ginfo) .labNodesDG
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess{- | auxiliary function for convertNodes if the given list of nodes is
313bb560bc5c323cfd40c9cad7335b4b8e060aedkessemtpy, it returns the conversion maps unchanged otherwise it adds the
06ba4a61654b3763ad65f52283832ebf058fdf1csliveconverted first node to the abstract graph and to the affected
fe64b2ba25510d8c9dba5560a2d537763566cf40ndconversion maps and afterwards calls itself with the remaining node
fe64b2ba25510d8c9dba5560a2d537763566cf40ndconvertNodesAux :: GA.GraphInfo -> LNode DGNodeLab -> IO ()
fe64b2ba25510d8c9dba5560a2d537763566cf40ndconvertNodesAux ginfo (node, dgnode) =
fe64b2ba25510d8c9dba5560a2d537763566cf40nd GA.addNode ginfo node (getRealDGNodeType dgnode) $ getDGNodeName dgnode
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess{- | converts the edges of the development graph
cb43ec0a02f97651bf2f46c9f4b9b48d5cb22df7rbowenworks the same way as convertNods does-}
fe64b2ba25510d8c9dba5560a2d537763566cf40ndconvertEdges :: GA.GraphInfo -> DGraph -> IO ()
fe64b2ba25510d8c9dba5560a2d537763566cf40ndconvertEdges ginfo = mapM_ (convertEdgesAux ginfo) . labEdgesDG
fe64b2ba25510d8c9dba5560a2d537763566cf40nd-- | auxiliary function for convertEges
fe64b2ba25510d8c9dba5560a2d537763566cf40ndconvertEdgesAux :: GA.GraphInfo -> LEdge DGLinkLab -> IO ()
fe64b2ba25510d8c9dba5560a2d537763566cf40ndconvertEdgesAux ginfo e@(src, tar, lbl) =
06ba4a61654b3763ad65f52283832ebf058fdf1cslive GA.addEdge ginfo (dgl_id lbl) (getRealDGLinkType lbl) src tar "" $ Just e
031bbbc0d1189b07330e38d0c126820a9ab7795egryzor-- | show library referened by a DGRef node (=node drawn as a box)
031bbbc0d1189b07330e38d0c126820a9ab7795egryzorshowReferencedLibrary :: Int -> GInfo -> ConvFunc -> LibFunc -> IO ()
031bbbc0d1189b07330e38d0c126820a9ab7795egryzorshowReferencedLibrary descr gInfo
fa1c7ce09927decc1eecd1e9a35cc5331078a052covener convGraph showLib = do
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd ost <- readIORef $ intState gInfo
4aa603e6448b99f9371397d439795c91a93637eand case i_state ost of
8672e74389242ff408471525b8563f85f7d369fdhumbedooh Nothing -> return ()
4aa603e6448b99f9371397d439795c91a93637eand Just ist -> do
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen let ln = i_ln ist
06ba4a61654b3763ad65f52283832ebf058fdf1cslive le = i_libEnv ist
06ba4a61654b3763ad65f52283832ebf058fdf1cslive refNode = labDG (lookupDGraph ln le) descr
06ba4a61654b3763ad65f52283832ebf058fdf1cslive refLibname = if isDGRef refNode then dgn_libname refNode
fe64b2ba25510d8c9dba5560a2d537763566cf40nd else error "showReferencedLibrary"
fa1c7ce09927decc1eecd1e9a35cc5331078a052covener case Map.lookup refLibname le of
fa1c7ce09927decc1eecd1e9a35cc5331078a052covener Just _ -> do
fa1c7ce09927decc1eecd1e9a35cc5331078a052covener gInfo' <- copyGInfo gInfo refLibname
fa1c7ce09927decc1eecd1e9a35cc5331078a052covener convGraph gInfo' "development graph" showLib
fa1c7ce09927decc1eecd1e9a35cc5331078a052covener let gv = gi_GraphInfo gInfo'
fa1c7ce09927decc1eecd1e9a35cc5331078a052covener hideNodes gInfo'
031bbbc0d1189b07330e38d0c126820a9ab7795egryzor GA.showTemporaryMessage gv "Development Graph initialized."
fa1c7ce09927decc1eecd1e9a35cc5331078a052covener Nothing -> error $ "The referenced library (" ++ show refLibname
fa1c7ce09927decc1eecd1e9a35cc5331078a052covener ++ ") is unknown"
b0ffb6279db3bd422faeff9a59a43dc762afe148minfrin-- | apply the changes of first history item (computed by proof rules,
b0ffb6279db3bd422faeff9a59a43dc762afe148minfrin-- see folder Proofs) to the displayed development graph
b6e6d2139d50d64fc4bbd01c4f07d7a4accfec8cndapplyChanges :: GA.GraphInfo -> [DGChange] -> IO ()
d1e976f5d61801abdaf621b7546944168be40ce9minfrinapplyChanges ginfo = mapM_ (applyChangesAux ginfo) . removeContraryChanges
d1e976f5d61801abdaf621b7546944168be40ce9minfrin-- | auxiliary function for applyChanges
4aa603e6448b99f9371397d439795c91a93637eandapplyChangesAux :: GA.GraphInfo -> DGChange -> IO ()
b0ffb6279db3bd422faeff9a59a43dc762afe148minfrinapplyChangesAux ginfo change =
4aa603e6448b99f9371397d439795c91a93637eand case change of
d1e976f5d61801abdaf621b7546944168be40ce9minfrin SetNodeLab _ (node, newLab) ->
d1e976f5d61801abdaf621b7546944168be40ce9minfrin GA.changeNodeType ginfo node $ getRealDGNodeType newLab
fe64b2ba25510d8c9dba5560a2d537763566cf40nd InsertNode (node, nodelab) ->
fe64b2ba25510d8c9dba5560a2d537763566cf40nd GA.addNode ginfo node (getRealDGNodeType nodelab) $ getDGNodeName nodelab
fe64b2ba25510d8c9dba5560a2d537763566cf40nd DeleteNode (node, _) ->
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess InsertEdge e@(src, tgt, lbl) ->
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess GA.addEdge ginfo (dgl_id lbl) (getRealDGLinkType lbl) src tgt "" $ Just e
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess DeleteEdge (_, _, lbl) ->
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess GA.delEdge ginfo $ dgl_id lbl
fe64b2ba25510d8c9dba5560a2d537763566cf40nd-- | display a window of translated graph with maximal sublogic.
fe64b2ba25510d8c9dba5560a2d537763566cf40ndopenTranslateGraph :: LibEnv -> LIB_NAME -> HetcatsOpts
fe64b2ba25510d8c9dba5560a2d537763566cf40nd -> Res.Result G_sublogics -> ConvFunc -> LibFunc -> IO ()
fe64b2ba25510d8c9dba5560a2d537763566cf40ndopenTranslateGraph libEnv ln opts (Res.Result diagsSl mSublogic) convGraph
fe64b2ba25510d8c9dba5560a2d537763566cf40nd -- if an error existed by the search of maximal sublogicn
fe64b2ba25510d8c9dba5560a2d537763566cf40nd -- (see DGTranslation.getDGLogic), the process need not to go on.
fe64b2ba25510d8c9dba5560a2d537763566cf40nd let myErrMess = showDiagMess opts in
fe64b2ba25510d8c9dba5560a2d537763566cf40nd if hasErrors diagsSl then myErrMess diagsSl else case mSublogic of
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Nothing -> errorDialog "Error" "the maximal sublogic is not found."
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Just sublogic -> do
fe64b2ba25510d8c9dba5560a2d537763566cf40nd let paths = findComorphismPaths logicGraph sublogic
9bcfc3697a91b5215893a7d0206865b13fc72148nd if null paths then
fb77c505254b6e9c925e23e734463e87574f8f40kess errorDialog "Error" "This graph has no comorphism to translation."
fb77c505254b6e9c925e23e734463e87574f8f40kess -- the user choose one
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd sel <- listBox "Choose a logic translation"
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen $ map show paths
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen case sel of
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd Nothing -> errorDialog "Error" "no logic translation chosen"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Just j -> do
d565edaec710102f7e7d06252aaf1de67b7ddd25rbowen -- graph translation.
031bbbc0d1189b07330e38d0c126820a9ab7795egryzor let Res.Result diagsTrans mLEnv =
c68acc9d712af079afa2bd1a5a4aeef9a3ea573ckess libEnv_translation libEnv $ paths !! j
06ba4a61654b3763ad65f52283832ebf058fdf1cslive case mLEnv of
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Just newLibEnv -> do
06ba4a61654b3763ad65f52283832ebf058fdf1cslive showDiagMess opts $ diagsSl ++ diagsTrans
fe64b2ba25510d8c9dba5560a2d537763566cf40nd dg_showGraphAux
fe64b2ba25510d8c9dba5560a2d537763566cf40nd (\gI -> do
fe64b2ba25510d8c9dba5560a2d537763566cf40nd ost <- readIORef $ intState gI
1b01d1ee11c612226cb3141eed4581dc179266c1rbowen let nwst = case i_state ost of
1b01d1ee11c612226cb3141eed4581dc179266c1rbowen Nothing -> ost
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Just ist ->
fe64b2ba25510d8c9dba5560a2d537763566cf40nd ost{i_state = Just ist{
fe64b2ba25510d8c9dba5560a2d537763566cf40nd i_libEnv = newLibEnv,
8559a67073808d84d85bb5dd552d4247caafe709sf i_ln = ln }}
8559a67073808d84d85bb5dd552d4247caafe709sf writeIORef (intState gI) nwst
8559a67073808d84d85bb5dd552d4247caafe709sf convGraph (gI{ gi_hetcatsOpts = opts})
8559a67073808d84d85bb5dd552d4247caafe709sf "translation Graph" showLib)
8559a67073808d84d85bb5dd552d4247caafe709sf Nothing -> myErrMess $ diagsSl ++ diagsTrans
8559a67073808d84d85bb5dd552d4247caafe709sfdg_showGraphAux :: (GInfo -> IO ()) -> IO ()
8559a67073808d84d85bb5dd552d4247caafe709sfdg_showGraphAux convFct = do
8559a67073808d84d85bb5dd552d4247caafe709sf useHTk -- All messages are displayed in TK dialog windows
8559a67073808d84d85bb5dd552d4247caafe709sf -- from this point on
8559a67073808d84d85bb5dd552d4247caafe709sf gInfo <- emptyGInfo
8559a67073808d84d85bb5dd552d4247caafe709sf convFct gInfo
8559a67073808d84d85bb5dd552d4247caafe709sf let actGraphInfo = gi_GraphInfo gInfo
8559a67073808d84d85bb5dd552d4247caafe709sf GA.redisplay actGraphInfo
8559a67073808d84d85bb5dd552d4247caafe709sf-- DaVinciGraph to String
4aa603e6448b99f9371397d439795c91a93637eand-- Functions to convert a DaVinciGraph to a String to store as a .udg file
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen-- | saves the uDrawGraph graph to a file
51b60896224b408a35684bd6ec0fafe5e4abe322rbowensaveUDGraph :: GInfo -> Map.Map DGNodeType (Shape value, String)
c8b79d4b8796531f19dd54bd59d88c3b68338ceahumbedooh -> Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String) -> IO ()
4aa603e6448b99f9371397d439795c91a93637eandsaveUDGraph gInfo@(GInfo { gi_GraphInfo = graphInfo
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen , gi_hetcatsOpts = opts
8559a67073808d84d85bb5dd552d4247caafe709sf }) nodemap linkmap = do
8559a67073808d84d85bb5dd552d4247caafe709sf ost <- readIORef $ intState gInfo
8559a67073808d84d85bb5dd552d4247caafe709sf case i_state ost of
8559a67073808d84d85bb5dd552d4247caafe709sf Nothing -> return ()
8559a67073808d84d85bb5dd552d4247caafe709sf Just ist -> do
8559a67073808d84d85bb5dd552d4247caafe709sf let ln = i_ln ist
8559a67073808d84d85bb5dd552d4247caafe709sf maybeFilePath <- fileSaveDialog ((rmSuffix $ libNameToFile opts ln) ++ ".udg")
8559a67073808d84d85bb5dd552d4247caafe709sf [ ("uDrawGraph",["*.udg"])
8559a67073808d84d85bb5dd552d4247caafe709sf , ("All Files", ["*"])] Nothing
8559a67073808d84d85bb5dd552d4247caafe709sf case maybeFilePath of
8559a67073808d84d85bb5dd552d4247caafe709sf Just filepath -> do
8559a67073808d84d85bb5dd552d4247caafe709sf GA.showTemporaryMessage graphInfo "Converting graph..."
8559a67073808d84d85bb5dd552d4247caafe709sf nstring <- nodes2String gInfo nodemap linkmap
8559a67073808d84d85bb5dd552d4247caafe709sf writeFile filepath nstring
8559a67073808d84d85bb5dd552d4247caafe709sf GA.showTemporaryMessage graphInfo $ "Graph stored to " ++ filepath ++ "!"
8559a67073808d84d85bb5dd552d4247caafe709sf Nothing -> GA.showTemporaryMessage graphInfo "Aborted!"
8559a67073808d84d85bb5dd552d4247caafe709sf-- | Converts the nodes of the graph to String representation
8559a67073808d84d85bb5dd552d4247caafe709sfnodes2String :: GInfo -> Map.Map DGNodeType (Shape value, String)
8559a67073808d84d85bb5dd552d4247caafe709sf -> IO String
8559a67073808d84d85bb5dd552d4247caafe709sfnodes2String gInfo@(GInfo { gi_GraphInfo = graphInfo }) nodemap linkmap = do
8559a67073808d84d85bb5dd552d4247caafe709sf ost <- readIORef $ intState gInfo
8559a67073808d84d85bb5dd552d4247caafe709sf case i_state ost of
8559a67073808d84d85bb5dd552d4247caafe709sf Nothing -> return []
8559a67073808d84d85bb5dd552d4247caafe709sf Just ist -> do
8559a67073808d84d85bb5dd552d4247caafe709sf let le = i_libEnv ist
8559a67073808d84d85bb5dd552d4247caafe709sf ln = i_ln ist
8559a67073808d84d85bb5dd552d4247caafe709sf nodes <- filterM (\(n,_) -> do b <- GA.isHiddenNode graphInfo n
8559a67073808d84d85bb5dd552d4247caafe709sf return $ not b)
8559a67073808d84d85bb5dd552d4247caafe709sf $ labNodesDG $ lookupDGraph ln le
8559a67073808d84d85bb5dd552d4247caafe709sf nstring <- foldM (\s node -> do
8559a67073808d84d85bb5dd552d4247caafe709sf s' <- (node2String gInfo nodemap linkmap node)
8559a67073808d84d85bb5dd552d4247caafe709sf return $ s ++ (if s /= "" then ",\n " else "") ++ s')
8559a67073808d84d85bb5dd552d4247caafe709sf return $ "[" ++ nstring ++ "]"
8559a67073808d84d85bb5dd552d4247caafe709sf-- | Converts a node to String representation
8559a67073808d84d85bb5dd552d4247caafe709sfnode2String :: GInfo -> Map.Map DGNodeType (Shape value, String)
7f1788016c02e671dc8e3f12ab33747de4d7ebb2humbedooh -> LNode DGNodeLab -> IO String
51b60896224b408a35684bd6ec0fafe5e4abe322rbowennode2String gInfo nodemap linkmap (nid, dgnode) = do
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen label <- getNodeLabel gInfo dgnode
7f1788016c02e671dc8e3f12ab33747de4d7ebb2humbedooh let ntype = getRealDGNodeType dgnode
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen (shape, color) <- case Map.lookup ntype nodemap of
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen Nothing -> error $ "SaveGraph: can't lookup nodetype: " ++ show ntype
7f1788016c02e671dc8e3f12ab33747de4d7ebb2humbedooh Just (s, c) -> return (s, c)
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen object = "a(\"OBJECT\",\"" ++ label ++ "\"),"
8559a67073808d84d85bb5dd552d4247caafe709sf color' = "a(\"COLOR\",\"" ++ color ++ "\"),"
8559a67073808d84d85bb5dd552d4247caafe709sf shape' = "a(\"_GO\",\"" ++ map toLower (show shape) ++ "\")"
8559a67073808d84d85bb5dd552d4247caafe709sf links <- links2String gInfo linkmap nid
8559a67073808d84d85bb5dd552d4247caafe709sf return $ "l(\"" ++ show nid ++ "\",n(\"" ++ show ntype ++ "\","
8559a67073808d84d85bb5dd552d4247caafe709sf ++ "[" ++ object ++ color' ++ shape' ++ "],"
8559a67073808d84d85bb5dd552d4247caafe709sf ++ "\n [" ++ links ++ "]))"
8559a67073808d84d85bb5dd552d4247caafe709sf-- | Converts all links of a node to String representation
8559a67073808d84d85bb5dd552d4247caafe709sflinks2String :: GInfo -> Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String)
8559a67073808d84d85bb5dd552d4247caafe709sf -> Int -> IO String
8559a67073808d84d85bb5dd552d4247caafe709sflinks2String gInfo@(GInfo { gi_GraphInfo = graphInfo
8559a67073808d84d85bb5dd552d4247caafe709sf }) linkmap nodeid = do
8559a67073808d84d85bb5dd552d4247caafe709sf ost <- readIORef $ intState gInfo
8559a67073808d84d85bb5dd552d4247caafe709sf case i_state ost of
8559a67073808d84d85bb5dd552d4247caafe709sf Nothing -> return []
8559a67073808d84d85bb5dd552d4247caafe709sf Just ist -> do
8559a67073808d84d85bb5dd552d4247caafe709sf let ln = i_ln ist
8559a67073808d84d85bb5dd552d4247caafe709sf le = i_libEnv ist
8559a67073808d84d85bb5dd552d4247caafe709sf edges <- filterM (\ (src, _, edge) -> do
8559a67073808d84d85bb5dd552d4247caafe709sf let eid = dgl_id edge
8559a67073808d84d85bb5dd552d4247caafe709sf b <- GA.isHiddenEdge graphInfo eid
fe64b2ba25510d8c9dba5560a2d537763566cf40nd return $ not b && src == nodeid)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd $ labEdgesDG $ lookupDGraph ln le
fe64b2ba25510d8c9dba5560a2d537763566cf40nd foldM (\ s edge -> do
fb77c505254b6e9c925e23e734463e87574f8f40kess s' <- link2String linkmap edge
fb77c505254b6e9c925e23e734463e87574f8f40kess return $ s ++ (if s /= "" then ",\n " else "") ++ s') "" edges
fe64b2ba25510d8c9dba5560a2d537763566cf40nd-- | Converts a link to String representation
fe64b2ba25510d8c9dba5560a2d537763566cf40ndlink2String :: Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd -> LEdge DGLinkLab -> IO String
fe64b2ba25510d8c9dba5560a2d537763566cf40ndlink2String linkmap (nodeid1, nodeid2, edge) = do
9bcfc3697a91b5215893a7d0206865b13fc72148nd let (EdgeId linkid) = dgl_id edge
ff797e743eb73c1d45b08158aa6b288c2d0c46eeslive ltype = getRealDGLinkType edge
ff797e743eb73c1d45b08158aa6b288c2d0c46eeslive (line, color) <- case Map.lookup ltype linkmap of
fb77c505254b6e9c925e23e734463e87574f8f40kess Nothing -> error $ "SaveGraph: can't lookup linktype: " ++ show ltype
88d86cfadffe2275a3dfb67a4d7bdc018630b661rbowen Just (l, c) -> return (l, c)
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd nm = "\"" ++ show linkid ++ ":" ++ show nodeid1 ++ "->"
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd ++ show nodeid2 ++ "\""
06ba4a61654b3763ad65f52283832ebf058fdf1cslive color' = "a(\"EDGECOLOR\",\"" ++ color ++ "\"),"
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd line' = "a(\"EDGEPATTERN\",\"" ++ map toLower (show line) ++ "\")"
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd return $ "l(" ++ nm ++ ",e(\"" ++ show ltype ++ "\","
06ba4a61654b3763ad65f52283832ebf058fdf1cslive ++ "[" ++ color' ++ line' ++"],"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive ++ "r(\"" ++ show nodeid2 ++ "\")))"
e4286c93598ad346ac365e59ac9c6f9e6e9fd324poirier-- | Returns the name of the Node
e4286c93598ad346ac365e59ac9c6f9e6e9fd324poiriergetNodeLabel :: GInfo -> DGNodeLab -> IO String
e4286c93598ad346ac365e59ac9c6f9e6e9fd324poiriergetNodeLabel (GInfo {internalNamesIORef = ioRefInternal}) dgnode = do
e4286c93598ad346ac365e59ac9c6f9e6e9fd324poirier internal <- readIORef ioRefInternal
06ba4a61654b3763ad65f52283832ebf058fdf1cslive let ntype = getDGNodeType dgnode
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd return $ if (not $ showNames internal) &&
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd elem ntype ["open_cons__internal"
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd , "proven_cons__internal"
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd , "locallyEmpty__open_cons__internal"
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen , "locallyEmpty__proven_cons__internal"]
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen then "" else getDGNodeName dgnode