GraphLogic.hs revision 2a9702a373738717c83824512bd9389b5870fc92
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechModule : $Header$
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechDescription : Logic for manipulating the graph in the Central GUI
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechCopyright : (c) Jorina Freya Gerken, Till Mossakowski, Uni Bremen 2002-2006
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechLicense : GPLv2 or higher, see LICENSE.txt
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechMaintainer : till@informatik.uni-bremen.de
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechStability : provisional
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechPortability : non-portable (imports Logic)
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechThis module provides functions for all the menus in the Hets GUI.
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechThese are then assembled to the GUI in "GUI.GraphMenu".
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech , updateGraph
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech , openProofStatus
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech , saveProofStatus
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech , showDGraph
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech , showReferencedLibrary
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech , getTheoryOfNode
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech , translateTheoryOfNode
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech , displaySubsortGraph
dd285415d7a8d8376207960cfa3e977524c3b98cJakub Hrozek , displayConceptGraph
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech , showProofStatusOfNode
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech , proveAtNode
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech , ensureLockAtNode
dd285415d7a8d8376207960cfa3e977524c3b98cJakub Hrozek , showNodeInfo
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech , showDiagMess
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech , showDiagMessAux
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech , showEdgeInfo
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech , checkconservativityOfNode
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech , checkconservativityOfEdge
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech , toggleHideNames
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech , toggleHideNodes
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech , toggleHideEdges
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech , translateGraph
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech , showLibGraph
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech , runAndLock
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech , saveUDGraph
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech , calcGlobalHistory
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech , add2history
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cechimport Logic.Coerce (coerceSign)
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cechimport Logic.Prover hiding (openProofStatus)
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cechimport Comorphisms.LogicGraph (logicGraph)
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cechimport Static.DGTranslation (libEnv_translation, getDGLogic)
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cechimport Proofs.InferBasic (basicInferenceNode)
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cechimport Proofs.StatusUtils (lookupHistory, removeContraryChanges)
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cechimport GUI.Taxonomy (displayConceptGraph, displaySubsortGraph)
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cechimport qualified GUI.GraphAbstraction as GA
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cechimport Reactor.InfoBus (encapsulateWaitTermAct)
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cechimport Common.DocUtils (showDoc, showGlobalDoc)
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cechimport qualified Common.OrderedMap as OMap
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cechimport qualified Common.Lib.SizedList as SizedList
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cechimport Driver.Options (HetcatsOpts, putIfVerbose, outtypes, doDump, verbose)
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cechimport Driver.WriteLibDefn (writeShATermFile)
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cechimport Driver.ReadFn (libNameToFile, readVerbose)
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cechimport Driver.AnaLib (anaLib)
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cechimport Data.Char (toLower)
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cechimport Data.List (partition, deleteBy, isPrefixOf)
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cechimport Data.Graph.Inductive.Graph (Node, LEdge, LNode)
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cechimport qualified Data.Map as Map
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech-- | Locks the global lock and runs function
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechrunAndLock :: GInfo -> IO () -> IO ()
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechrunAndLock (GInfo { functionLock = lock
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech , graphInfo = gi
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech }) function = do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech locked <- tryPutMVar lock ()
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech if locked then do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech takeMVar lock
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech "an other function is still working ... please wait ..."
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech-- | Undo one step of the History
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cechundo :: GInfo -> Bool -> IO ()
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cechundo gInfo isUndo = do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech intSt <- readIORef $ intState gInfo
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech nwSt <- if isUndo then undoOneStepWithUpdate intSt $ updateGraphAux gInfo
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech else redoOneStepWithUpdate intSt $ updateGraphAux gInfo
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech writeIORef (intState gInfo) nwSt
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechupdateGraph :: GInfo -> [DGChange] -> IO ()
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechupdateGraph gInfo@(GInfo { libName = ln }) changes = do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech ost <- readIORef $ intState gInfo
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech case i_state ost of
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Nothing -> return ()
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Just ist -> updateGraphAux gInfo ln changes $ lookupDGraph ln $ i_libEnv ist
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechupdateGraphAux :: GInfo -> LibName -> [DGChange] -> DGraph -> IO ()
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechupdateGraphAux gInfo' ln changes dg = do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech og <- readIORef $ openGraphs gInfo'
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech case Map.lookup ln og of
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Nothing -> return ()
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Just gInfo@(GInfo { graphInfo = gi
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech , options = opts }) -> do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech flags <- readIORef opts
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech let edges = if flagHideEdges flags then hideEdgesAux dg else []
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech (nodes, comp) = if flagHideNodes flags then hideNodesAux dg edges
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech else ([], [])
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech "Applying development graph calculus proof rule..."
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech GA.applyChanges gi (removeContraryChanges changes) nodes edges comp
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech "Updating graph..."
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech hideNames gInfo
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech "Development graph calculus proof rule finished."
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech-- | Toggles to display internal node names
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechhideNames :: GInfo -> IO ()
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechhideNames (GInfo { options = opts
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech , internalNames = updaterIORef }) = do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech flags <- readIORef opts
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech updater <- readIORef updaterIORef
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech mapM_ (\ (s, upd) -> upd (const $ if flagHideNames flags then "" else s))
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech-- | Toggles to display internal node names
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechtoggleHideNames :: GInfo -> IO ()
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechtoggleHideNames gInfo@(GInfo { graphInfo = gi
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech , options = opts }) = do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech flags <- readIORef opts
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech let hide = not $ flagHideNames flags
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech writeIORef opts $ flags { flagHideNames = hide }
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech GA.showTemporaryMessage gi $ if hide then "Hiding internal names..."
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech else "Revealing internal names..."
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech updateGraph gInfo []
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech-- | hides all unnamed internal nodes that are proven
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechhideNodesAux :: DGraph -> [EdgeId]
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech -> ([GA.NodeId], [(GA.NodeId, GA.NodeId, DGEdgeType, Bool)])
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechhideNodesAux dg ignoreEdges =
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech let nodes = selectNodesByType dg
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech (\ n -> isInternalSpec n && isProvenNode n && isProvenCons n)
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech edges = getCompressedEdges dg nodes ignoreEdges
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech in (nodes, edges)
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechtoggleHideNodes :: GInfo -> IO ()
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechtoggleHideNodes gInfo@(GInfo { graphInfo = gi
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech , options = opts }) = do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech flags <- readIORef opts
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech let hide = not $ flagHideNodes flags
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech writeIORef opts $ flags { flagHideNodes = hide }
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech GA.showTemporaryMessage gi $ if hide then "Hiding unnamed nodes..."
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech else "Revealing hidden nodes..."
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech updateGraph gInfo []
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechhideEdgesAux :: DGraph -> [EdgeId]
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechhideEdgesAux dg = map dgl_id
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech $ filter (\ (DGLink { dgl_type = linktype }) ->
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech case linktype of
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech ScopedLink _ (ThmLink s) c ->
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech isProvenThmLinkStatus s && isProvenConsStatusLink c
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech HidingFreeOrCofreeThm _ _ _ s -> isProvenThmLinkStatus s
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech $ foldl (\ e c -> case c of
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech InsertEdge (_, _, lbl) -> lbl : e
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech DeleteEdge (_, _, lbl) -> deleteBy eqDGLinkLabById lbl e
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech ) [] $ flattenHistory (SizedList.toList $ proofHistory dg) []
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechtoggleHideEdges :: GInfo -> IO ()
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechtoggleHideEdges gInfo@(GInfo { graphInfo = gi
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech , options = opts }) = do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech flags <- readIORef opts
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech let hide = not $ flagHideEdges flags
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech writeIORef opts $ flags { flagHideEdges = hide }
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech GA.showTemporaryMessage gi $ if hide then "Hiding new proven edges..."
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech else "Revealing hidden proven edges..."
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech updateGraph gInfo []
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech-- | generates from list of HistElem one list of DGChanges
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechflattenHistory :: [HistElem] -> [DGChange] -> [DGChange]
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechflattenHistory [] cs = cs
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechflattenHistory (HistElem c : r) cs = flattenHistory r $ c : cs
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechflattenHistory (HistGroup _ ph : r) cs =
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech flattenHistory r $ flattenHistory (SizedList.toList ph) cs
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech-- | selects all nodes of a type with outgoing edges
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechselectNodesByType :: DGraph -> (DGNodeType -> Bool) -> [Node]
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechselectNodesByType dg types =
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech filter (\ n -> not (null $ outDG dg n) && hasUnprovenEdges dg n) $ map fst
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech $ filter (types . getRealDGNodeType . snd) $ labNodesDG dg
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechhasUnprovenEdges :: DGraph -> Node -> Bool
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechhasUnprovenEdges dg =
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech foldl (\ b (_, _, l) -> case edgeTypeModInc $ getRealDGLinkType l of
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech ThmType { isProvenEdge = False } -> False
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech _ -> b) True . (\ n -> innDG dg n ++ outDG dg n)
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech-- | compresses a list of types to the highest one
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechcompressTypes :: Bool -> [DGEdgeType] -> (DGEdgeType, Bool)
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechcompressTypes _ [] = error "compressTypes: wrong usage"
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechcompressTypes b (t : []) = (t, b)
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechcompressTypes b (t1 : t2 : r)
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech | t1 == t2 = compressTypes b (t1 : r)
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech | t1 > t2 = compressTypes False (t1 : r)
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech | otherwise = compressTypes False (t2 : r)
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech-- | innDG with filter of not shown edges
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechfInnDG :: [EdgeId] -> DGraph -> Node -> [LEdge DGLinkLab]
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechfInnDG ignore dg = filter (\ (_, _, l) -> notElem (dgl_id l) ignore) . innDG dg
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech-- | outDG with filter of not shown edges
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechfOutDG :: [EdgeId] -> DGraph -> Node -> [LEdge DGLinkLab]
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechfOutDG ignore dg = filter (\ (_, _, l) -> notElem (dgl_id l) ignore) . outDG dg
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech-- | returns a list of compressed edges
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechgetCompressedEdges :: DGraph -> [Node] -> [EdgeId]
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech -> [(Node, Node, DGEdgeType, Bool)]
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechgetCompressedEdges dg hidden ign = filterDuplicates $ getShortPaths
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech $ concatMap (\ e@(_, t, _) -> map (e :) $ getPaths dg t hidden [] ign) inEdges
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech inEdges = filter (\ (_, t, _) -> elem t hidden)
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech $ concatMap (fOutDG ign dg)
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech $ foldr (\ (n, _, _) i -> if elem n hidden
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech || elem n i then i else n : i) []
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech $ concatMap (fInnDG ign dg) hidden
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech-- | filter duplicate paths
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechfilterDuplicates :: [(Node, Node, DGEdgeType, Bool)]
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech -> [(Node, Node, DGEdgeType, Bool)]
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechfilterDuplicates [] = []
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechfilterDuplicates r@((s, t, _, _) : _) = edges ++ filterDuplicates others
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech (same, others) = partition (\ (s', t', _, _) -> s == s' && t == t') r
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech (mtypes, stypes) = partition (\ (_, _, _, b) -> not b) same
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech stypes' = foldr (\ e es -> if elem e es then es else e : es) [] stypes
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech (et', _) = compressTypes False $ map (\ (_, _, et, _) -> et) mtypes
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech edges = if null mtypes then stypes' else (s, t, et', False) : stypes'
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech-- | returns the pahts of a given node through hidden nodes
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechgetPaths :: DGraph -> Node -> [Node] -> [Node] -> [EdgeId]
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech -> [[LEdge DGLinkLab]]
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechgetPaths dg node hidden seen' ign = if elem node hidden then
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech if null edges then []
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech else concatMap (\ e@(_, t, _) -> map (e :) $ getPaths dg t hidden seen ign)
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech seen = node : seen'
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech edges = filter (\ (_, t, _) -> notElem t seen) $ fOutDG ign dg node
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech-- | returns source and target node of a path with the compressed type
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechgetShortPaths :: [[LEdge DGLinkLab]]
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech -> [(Node, Node, DGEdgeType, Bool)]
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechgetShortPaths [] = []
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechgetShortPaths (p : r) =
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech (s, t, et, b)
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech : getShortPaths r
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech (s, _, _) = head p
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech (_, t, _) = last p
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech (et, b) = compressTypes True $ map (\ (_, _, e) -> getRealDGLinkType e) p
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech-- | Let the user select a Node to focus
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechfocusNode :: GInfo -> IO ()
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechfocusNode gInfo@(GInfo { graphInfo = gi
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech , libName = ln }) = do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech ost <- readIORef $ intState gInfo
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech case i_state ost of
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Nothing -> return ()
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Just ist -> do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech let le = i_libEnv ist
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech idsnodes <- filterM (fmap not . GA.isHiddenNode gi . fst)
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech $ labNodesDG $ lookupDGraph ln le
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech selection <- listBox "Select a node to focus"
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech $ map (\ (n, l) -> shows n " " ++ getDGNodeName l) idsnodes
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech case selection of
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Just idx -> GA.focusNode gi $ fst $ idsnodes !! idx
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Nothing -> return ()
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechshowLibGraph :: GInfo -> LibFunc -> IO ()
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechshowLibGraph gInfo showLib = do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech showLib gInfo
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechsaveProofStatus :: GInfo -> FilePath -> IO ()
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechsaveProofStatus gInfo@(GInfo { hetcatsOpts = opts
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech , libName = ln
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech }) file = encapsulateWaitTermAct $ do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech ost <- readIORef $ intState gInfo
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech case i_state ost of
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Nothing -> return ()
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Just ist -> do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech let proofStatus = i_libEnv ist
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech writeShATermFile file (ln, lookupHistory ln proofStatus)
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech putIfVerbose opts 2 $ "Wrote " ++ file
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech-- | implementation of open menu, read in a proof status
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechopenProofStatus :: GInfo -> FilePath -> ConvFunc -> LibFunc
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechopenProofStatus gInfo@(GInfo { hetcatsOpts = opts
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech , libName = ln }) file convGraph showLib = do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech ost <- readIORef $ intState gInfo
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech case i_state ost of
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Nothing -> return ()
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Just ist -> do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech mh <- readVerbose logicGraph opts (Just ln) file
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Nothing -> errorDialog "Error" $
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech "Could not read proof status from file '" ++ file ++ "'"
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Just h -> do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech let libfile = libNameToFile ln
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech m <- anaLib opts { outtypes = [] } libfile
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Nothing -> errorDialog "Error"
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech $ "Could not read original development graph from '"
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech ++ libfile ++ "'"
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Just (_, libEnv) -> case Map.lookup ln libEnv of
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Nothing -> errorDialog "Error" $ "Could not get original"
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech ++ "development graph for '" ++ showDoc ln "'"
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Just dg -> do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech lockGlobal gInfo
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech let oldEnv = i_libEnv ist
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech proofStatus = Map.insert ln (applyProofHistory h dg) oldEnv
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech nwst = ost { i_state = Just ist { i_libEnv = proofStatus } }
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech writeIORef (intState gInfo) nwst
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech unlockGlobal gInfo
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech gInfo' <- copyGInfo gInfo ln
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech convGraph gInfo' "Proof Status " showLib
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech let gi = graphInfo gInfo'
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech-- | apply a rule of the development graph calculus
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechproofMenu :: GInfo
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech -> (LibEnv -> IO (Result LibEnv))
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechproofMenu gInfo@(GInfo { hetcatsOpts = hOpts
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech , libName = ln
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech }) cmd proofFun = do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech ost <- readIORef $ intState gInfo
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech case i_state ost of
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Nothing -> return ()
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Just ist -> do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech let ost2 = add2history cmd ost []
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech ost3 = add2history (CommentCmd "") ost2 []
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech writeIORef (intState gInfo) ost3
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech lockGlobal gInfo
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech let proofStatus = i_libEnv ist
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech putIfVerbose hOpts 4 "Proof started via menu"
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Result ds res <- proofFun proofStatus
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech putIfVerbose hOpts 4 "Analyzing result of proof"
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Nothing -> do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech unlockGlobal gInfo
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech printDiags 2 ds
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Just newProofStatus -> do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech ostate <- readIORef $ intState gInfo
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech let newGr = lookupDGraph ln newProofStatus
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech history = snd $ splitHistory (lookupDGraph ln proofStatus) newGr
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech lln = map DgCommandChange $ calcGlobalHistory
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech proofStatus newProofStatus
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech nst = add2history (CommentCmd "") ostate lln
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech nwst = nst { i_state = Just ist { i_libEnv = newProofStatus}}
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech doDump hOpts "PrintHistory" $ do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech putStrLn "History"
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech print $ prettyHistory history
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech writeIORef (intState gInfo) nwst
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech updateGraph gInfo (reverse $ flatHistory history)
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech unlockGlobal gInfo
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechcalcGlobalHistory :: LibEnv -> LibEnv -> [LibName]
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechcalcGlobalHistory old new = let
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech length' ln = SizedList.size . proofHistory . lookupDGraph ln
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech changes = filter (\ ln -> length' ln old < length' ln new) $ Map.keys old
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech in concatMap (\ ln -> replicate (length' ln new - length' ln old) ln) changes
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechshowNodeInfo :: Int -> DGraph -> IO ()
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechshowNodeInfo descr dgraph = do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech let dgnode = labDG dgraph descr
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech title = (if isDGRef dgnode then ("reference " ++) else
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech if isInternalNode dgnode then ("internal " ++) else id)
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech "node " ++ getDGNodeName dgnode ++ " " ++ show descr
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech createTextDisplay title $ title ++ "\n"
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech ++ showGlobalDoc (globalAnnos dgraph) dgnode ""
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechshowDiagMessAux :: Int -> [Diagnosis] -> IO ()
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechshowDiagMessAux v ds = let es = filterDiags v ds in
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech unless (null es) $ (if hasErrors es then errorDialog "Error"
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech else infoDialog "Info") $ unlines $ map show es
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechshowDiagMess :: HetcatsOpts -> [Diagnosis] -> IO ()
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechshowDiagMess = showDiagMessAux . verbose
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech{- | outputs the theory of a node in a window;
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech used by the node menu -}
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechgetTheoryOfNode :: GInfo -> Int -> DGraph -> IO ()
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechgetTheoryOfNode gInfo descr dgraph = do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech ost <- readIORef $ intState gInfo
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech case i_state ost of
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Nothing -> return ()
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Just ist -> case computeTheory (i_libEnv ist) (libName gInfo) descr of
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech errorDialog "Error" $ "no global theory for node " ++ show descr
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Just th -> displayTheoryOfNode (getNameOfNode descr dgraph)
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech (addHasInHidingWarning dgraph descr
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech ++ showGlobalDoc (globalAnnos dgraph) th "\n")
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech-- | displays a theory with warning in a window
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechdisplayTheoryOfNode :: String -- ^ Name of theory
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech -> String -- ^ Body text
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechdisplayTheoryOfNode n = createTextSaveDisplay ("Theory of " ++ n) (n ++ ".het")
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech{- | translate the theory of a node in a window;
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech used by the node menu -}
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechtranslateTheoryOfNode :: GInfo -> Int -> DGraph -> IO ()
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechtranslateTheoryOfNode gInfo@(GInfo { hetcatsOpts = opts
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech , libName = ln }) node dgraph = do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech ost <- readIORef $ intState gInfo
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech case i_state ost of
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Nothing -> return ()
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Just ist -> do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech let libEnv = i_libEnv ist
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech case computeTheory libEnv ln node of
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Just th@(G_theory lid _ sign _ sens _) -> do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech -- find all comorphism paths starting from lid
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech let paths = findComorphismPaths logicGraph (sublogicOfTh th)
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech -- let the user choose one
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech sel <- listBox "Choose a node logic translation" $ map show paths
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Nothing -> errorDialog "Error" "no node logic translation chosen"
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Just i -> do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Comorphism cid <- return (paths !! i)
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech -- adjust lid's
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech let lidS = sourceLogic cid
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech lidT = targetLogic cid
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech sign' <- coerceSign lid lidS "" sign
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech sens' <- coerceThSens lid lidS "" sens
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech -- translate theory along chosen comorphism
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech let Result es mTh = wrapMapTheory cid
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech (plainSign sign', toNamedList sens')
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Nothing -> showDiagMess opts es
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Just (sign'', sens1) -> displayTheoryWithWarning
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech "Translated Theory" (getNameOfNode node dgraph)
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech (addHasInHidingWarning dgraph node)
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech $ G_theory lidT Nothing (mkExtSign sign'') startSigId
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech (toThSens sens1) startThId
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech errorDialog "Error" $ "no global theory for node " ++ show node
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech-- | Show proof status of a node
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechshowProofStatusOfNode :: GInfo -> Int -> DGraph -> IO ()
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechshowProofStatusOfNode _ descr dgraph =
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech let dgnode = labDG dgraph descr
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech stat = showStatusAux dgnode
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech title = "Proof status of node " ++ getDGNodeName dgnode
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech in createTextDisplay title stat
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechshowStatusAux :: DGNodeLab -> String
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechshowStatusAux dgnode = case simplifyTh $ dgn_theory dgnode of
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech G_theory _ _ _ _ sens _ ->
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech let goals = OMap.filter (not . isAxiom) sens
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech (proven, open) = OMap.partition isProvenSenStatus goals
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech consGoal = "\nconservativity of this node"
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech in "Proven proof goals:\n"
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech ++ showDoc (OMap.map sentence proven) ""
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech ++ if not $ hasOpenNodeConsStatus True dgnode
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech then consGoal
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech ++ "\nOpen proof goals:\n"
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech ++ showDoc (OMap.map sentence open) ""
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech ++ if hasOpenNodeConsStatus False dgnode
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech then consGoal
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechhidingWarnDiag :: DGNodeLab -> IO Bool
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechhidingWarnDiag dgn = if labelHasHiding dgn then
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech warningDialog "Warning" $ unwords $ hidingWarning ++ ["Try anyway?"]
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech else return True
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechensureLockAtNode :: GInfo -> Int -> DGraph
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech -> IO (Maybe (DGraph, DGNodeLab, LibEnv))
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechensureLockAtNode gi descr dg = do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech let ln = libName gi
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech iSt = intState gi
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech ost <- readIORef iSt
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech case i_state ost of
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Nothing -> return Nothing
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Just ist -> let
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech le = i_libEnv ist
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech dgn = labDG dg descr in if hasLock dgn
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech then return $ Just (dg, dgn, le)
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech lockGlobal gi
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech (dgraph', dgn') <- initLocking (lookupDGraph ln le) (descr, dgn)
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech let nwle = Map.insert ln dgraph' le
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech nwst = ost { i_state = Just $ ist { i_libEnv = nwle} }
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech writeIORef iSt nwst
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech unlockGlobal gi
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech return $ Just (dgraph', dgn', nwle)
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech-- | start local theorem proving or consistency checking at a node
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechproveAtNode :: GInfo -> Int -> DGraph -> IO ()
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechproveAtNode gInfo descr dgraph = do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech let ln = libName gInfo
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech iSt = intState gInfo
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech lockedEnv <- ensureLockAtNode gInfo descr dgraph
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech case lockedEnv of
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Nothing -> return ()
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Just (dgraph', dgn', le') -> do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech acquired <- tryLockLocal dgn'
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech if acquired then do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech let action = do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech res@(Result d _) <- basicInferenceNode logicGraph ln dgraph'
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech (descr, dgn') le' iSt
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech when (null d || diagString (head d) /= "Proofs.Proofs: selection")
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech $ runProveAtNode gInfo (descr, dgn') res
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech b <- hidingWarnDiag dgn'
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech when b action
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech unlockLocal dgn'
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech else errorDialog "Error" "Proofwindow already open"
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechrunProveAtNode :: GInfo -> LNode DGNodeLab
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech -> Result G_theory -> IO ()
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechrunProveAtNode gInfo (v, dgnode) (Result ds mres) = case mres of
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Just newTh ->
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech let oldTh = dgn_theory dgnode
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech rTh = propagateProofs oldTh newTh in
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech unless (rTh == oldTh) $ do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech showDiagMessAux 2 ds
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech lockGlobal gInfo
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech let ln = libName gInfo
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech iSt = intState gInfo
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech ost <- readIORef iSt
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech let (ost', hist) = updateNodeProof ln ost (v, dgnode) rTh
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech case i_state ost' of
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Nothing -> return ()
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Just _ -> do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech writeIORef iSt ost'
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech runAndLock gInfo $ updateGraph gInfo hist
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech unlockGlobal gInfo
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech _ -> return ()
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechcheckconservativityOfNode :: GInfo -> Int -> DGraph -> IO ()
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechcheckconservativityOfNode gInfo descr dgraph = do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech let iSt = intState gInfo
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech ln = libName gInfo
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech nlbl = labDG dgraph descr
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech ost <- readIORef iSt
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech case i_state ost of
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Nothing -> return ()
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Just iist -> do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech b <- hidingWarnDiag nlbl
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech lockGlobal gInfo
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech (str, libEnv', ph) <- checkConservativityNode True (descr, nlbl)
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech (i_libEnv iist) ln
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech if isPrefixOf "No conservativity" str then
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech errorDialog "Result of conservativity check" str
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech createTextDisplay "Result of conservativity check" str
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech let nst = add2history (SelectCmd Node $ showDoc descr "")
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech ost [DgCommandChange ln]
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech nwst = nst { i_state = Just $ iist { i_libEnv = libEnv' }}
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech writeIORef iSt nwst
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech runAndLock gInfo $ updateGraph gInfo (reverse $ flatHistory ph)
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech unlockGlobal gInfo
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechedgeErr :: Int -> IO ()
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechedgeErr descr = errorDialog "Error" $ "edge with descriptor " ++ show descr
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech ++ " not found in the development graph"
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech-- | print the id, origin, type, proof-status and morphism of the edge
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechshowEdgeInfo :: Int -> Maybe (LEdge DGLinkLab) -> IO ()
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechshowEdgeInfo descr me = case me of
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Just e@(_, _, l) -> let estr = showLEdge e in
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech createTextDisplay ("Info of " ++ estr)
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech (estr ++ "\n" ++ showDoc l "")
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Nothing -> edgeErr descr
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech-- | check conservativity of the edge
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechcheckconservativityOfEdge :: Int -> GInfo -> Maybe (LEdge DGLinkLab) -> IO ()
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechcheckconservativityOfEdge descr gInfo me = case me of
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Nothing -> edgeErr descr
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Just lnk@(_, _, lbl) -> do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech let iSt = intState gInfo
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech ln = libName gInfo
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech ost <- readIORef iSt
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech case i_state ost of
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Nothing -> return ()
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Just iist -> do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech lockGlobal gInfo
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech (str, nwle, _, ph) <- checkConservativityEdge True lnk
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech (i_libEnv iist) ln
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech if isPrefixOf "No conservativity" str
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech errorDialog "Result of conservativity check" str
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech createTextDisplay "Result of conservativity check" str
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech let nst = add2history (SelectCmd Link $ showDoc (dgl_id lbl) "")
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech ost [DgCommandChange ln]
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech nwst = nst { i_state = Just $ iist { i_libEnv = nwle}}
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech writeIORef iSt nwst
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech runAndLock gInfo $ updateGraph gInfo $ reverse $ flatHistory ph
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech unlockGlobal gInfo
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech-- | show development graph for library
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechshowDGraph :: GInfo -> LibName -> ConvFunc -> LibFunc -> IO ()
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechshowDGraph gi ln convGraph showLib = do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech putIfVerbose (hetcatsOpts gi) 3 $ "Converting graph for " ++ show ln
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech og <- readIORef $ openGraphs gi
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech case Map.lookup ln og of
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Nothing -> do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech updateWindowCount gi succ
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech gi' <- copyGInfo gi ln
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech convGraph gi' "Development Graph" showLib
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech GA.showTemporaryMessage (graphInfo gi') "Development Graph initialized."
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech GA.showTemporaryMessage (graphInfo gi') "Development Graph requested."
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech-- | show library referened by a DGRef node (=node drawn as a box)
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechshowReferencedLibrary :: Int -> GInfo -> ConvFunc -> LibFunc -> IO ()
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechshowReferencedLibrary descr gInfo convGraph showLib = do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech ost <- readIORef $ intState gInfo
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech case i_state ost of
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Nothing -> return ()
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Just ist -> do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech let le = i_libEnv ist
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech ln = libName gInfo
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech refNode = labDG (lookupDGraph ln le) descr
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech refLibname = if isDGRef refNode then dgn_libname refNode
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech else error "showReferencedLibrary"
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech case Map.lookup refLibname le of
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Just _ -> showDGraph gInfo refLibname convGraph showLib
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Nothing -> errorDialog "Error"
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech $ "The referenced library (" ++ show refLibname ++ ") is unknown"
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech-- | display a window of translated graph with maximal sublogic.
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechtranslateGraph :: GInfo -> IO (Maybe LibEnv)
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechtranslateGraph gInfo@(GInfo { hetcatsOpts = opts }) = do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech ost <- readIORef $ intState gInfo
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech case i_state ost of
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Nothing -> return Nothing
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Just ist -> do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech le = i_libEnv ist
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Result diagsSl mSublogic = getDGLogic le
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech myErrMess = showDiagMess opts
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech error' = errorDialog "Error"
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech if hasErrors diagsSl then do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech myErrMess diagsSl
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech return Nothing
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech else case mSublogic of
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Nothing -> do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech error' "No maximal sublogic found."
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech return Nothing
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Just sublogic -> do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech let paths = findComorphismPaths logicGraph sublogic
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech if null paths then do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech error' "This graph has no comorphism to translation."
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech return Nothing
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech sel <- listBox "Choose a logic translation" $ map show paths
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Nothing -> do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech error' "no logic translation chosen"
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech return Nothing
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Just j -> do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech let Result diag mle = libEnv_translation le $ paths !! j
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Just newLibEnv -> do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech showDiagMess opts $ diagsSl ++ diag
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech return $ Just newLibEnv
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Nothing -> do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech myErrMess $ diagsSl ++ diag
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech return Nothing
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech-- | saves the uDrawGraph graph to a file
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechsaveUDGraph :: GInfo -> Map.Map DGNodeType (Shape value, String)
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech -> Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String) -> IO ()
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechsaveUDGraph gInfo@(GInfo { graphInfo = gi
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech , libName = ln }) nodemap linkmap = do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech ost <- readIORef $ intState gInfo
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech case i_state ost of
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Nothing -> return ()
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Just _ -> do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech maybeFilePath <- fileSaveDialog (libNameToFile ln ++ ".udg")
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech [ ("uDrawGraph", ["*.udg"])
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech , ("All Files", ["*"])] Nothing
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech case maybeFilePath of
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Just filepath -> do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech GA.showTemporaryMessage gi "Converting graph..."
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech nstring <- nodes2String gInfo nodemap linkmap
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech writeFile filepath nstring
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech GA.showTemporaryMessage gi $ "Graph stored to " ++ filepath ++ "!"
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Nothing -> GA.showTemporaryMessage gi "Aborted!"
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech-- | Converts the nodes of the graph to String representation
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cechnodes2String :: GInfo -> Map.Map DGNodeType (Shape value, String)
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech -> Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String)
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech -> IO String
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cechnodes2String gInfo@(GInfo { graphInfo = gi
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech , libName = ln }) nodemap linkmap = do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech ost <- readIORef $ intState gInfo
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech case i_state ost of
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Nothing -> return []
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Just ist -> do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech let le = i_libEnv ist
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech nodes <- filterM (fmap not . GA.isHiddenNode gi . fst)
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech $ labNodesDG $ lookupDGraph ln le
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech nstring <- foldM (\ s ->
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech fmap ((if null s then s else s ++ ",\n") ++)
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech . node2String gInfo nodemap linkmap)
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech return $ "[" ++ nstring ++ "]"
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech-- | Converts a node to String representation
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cechnode2String :: GInfo -> Map.Map DGNodeType (Shape value, String)
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech -> Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String)
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech -> LNode DGNodeLab -> IO String
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cechnode2String gInfo nodemap linkmap (nid, dgnode) = do
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech label <- getNodeLabel gInfo dgnode
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech let ntype = getRealDGNodeType dgnode
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech (shape, color) <- case Map.lookup ntype nodemap of
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Nothing -> error $ "SaveGraph: can't lookup nodetype: " ++ show ntype
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Just (s, c) -> return (s, c)
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech object = "a(\"OBJECT\",\"" ++ label ++ "\"),"
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech color' = "a(\"COLOR\",\"" ++ color ++ "\"),"
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech shape' = "a(\"_GO\",\"" ++ map toLower (show shape) ++ "\")"
27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech links <- links2String gInfo linkmap nid
b <- GA.isHiddenEdge gi eid
(line, color) <- case Map.lookup ltype linkmap of