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