{- |
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 -> IO () -> IO ()
runAndLock (GInfo { functionLock :: GInfo -> MVar ()
functionLock = MVar ()
lock
                  , graphInfo :: GInfo -> GraphInfo
graphInfo = GraphInfo
gi
                  }) function :: IO ()
function = do
  Bool
locked <- MVar () -> () -> IO Bool
forall a. MVar a -> a -> IO Bool
tryPutMVar MVar ()
lock ()
  if Bool
locked then do
      IO ()
function
      MVar () -> IO ()
forall a. MVar a -> IO a
takeMVar MVar ()
lock
    else GraphInfo -> String -> IO ()
GA.showTemporaryMessage GraphInfo
gi
           "an other function is still working ... please wait ..."

-- | Undo one step of the History
undo :: GInfo -> Bool -> IO ()
undo :: GInfo -> Bool -> IO ()
undo gInfo :: GInfo
gInfo isUndo :: Bool
isUndo = do
  IntState
intSt <- IORef IntState -> IO IntState
forall a. IORef a -> IO a
readIORef (IORef IntState -> IO IntState) -> IORef IntState -> IO IntState
forall a b. (a -> b) -> a -> b
$ GInfo -> IORef IntState
intState GInfo
gInfo
  IntState
nwSt <- if Bool
isUndo then IntState
-> (LibName -> [DGChange] -> DGraph -> IO ()) -> IO IntState
undoOneStepWithUpdate IntState
intSt ((LibName -> [DGChange] -> DGraph -> IO ()) -> IO IntState)
-> (LibName -> [DGChange] -> DGraph -> IO ()) -> IO IntState
forall a b. (a -> b) -> a -> b
$ GInfo -> LibName -> [DGChange] -> DGraph -> IO ()
updateGraphAux GInfo
gInfo
                    else IntState
-> (LibName -> [DGChange] -> DGraph -> IO ()) -> IO IntState
redoOneStepWithUpdate IntState
intSt ((LibName -> [DGChange] -> DGraph -> IO ()) -> IO IntState)
-> (LibName -> [DGChange] -> DGraph -> IO ()) -> IO IntState
forall a b. (a -> b) -> a -> b
$ GInfo -> LibName -> [DGChange] -> DGraph -> IO ()
updateGraphAux GInfo
gInfo
  IORef IntState -> IntState -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (GInfo -> IORef IntState
intState GInfo
gInfo) IntState
nwSt

updateGraph :: GInfo -> [DGChange] -> IO ()
updateGraph :: GInfo -> [DGChange] -> IO ()
updateGraph gInfo :: GInfo
gInfo@(GInfo { libName :: GInfo -> LibName
libName = LibName
ln }) changes :: [DGChange]
changes = do
  IntState
ost <- IORef IntState -> IO IntState
forall a. IORef a -> IO a
readIORef (IORef IntState -> IO IntState) -> IORef IntState -> IO IntState
forall a b. (a -> b) -> a -> b
$ GInfo -> IORef IntState
intState GInfo
gInfo
  case IntState -> Maybe IntIState
i_state IntState
ost of
    Nothing -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Just ist :: IntIState
ist -> GInfo -> LibName -> [DGChange] -> DGraph -> IO ()
updateGraphAux GInfo
gInfo LibName
ln [DGChange]
changes (DGraph -> IO ()) -> DGraph -> IO ()
forall a b. (a -> b) -> a -> b
$ LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln (LibEnv -> DGraph) -> LibEnv -> DGraph
forall a b. (a -> b) -> a -> b
$ IntIState -> LibEnv
i_libEnv IntIState
ist

updateGraphAux :: GInfo -> LibName -> [DGChange] -> DGraph -> IO ()
updateGraphAux :: GInfo -> LibName -> [DGChange] -> DGraph -> IO ()
updateGraphAux gInfo' :: GInfo
gInfo' ln :: LibName
ln changes :: [DGChange]
changes dg :: DGraph
dg = do
  Map LibName GInfo
og <- IORef (Map LibName GInfo) -> IO (Map LibName GInfo)
forall a. IORef a -> IO a
readIORef (IORef (Map LibName GInfo) -> IO (Map LibName GInfo))
-> IORef (Map LibName GInfo) -> IO (Map LibName GInfo)
forall a b. (a -> b) -> a -> b
$ GInfo -> IORef (Map LibName GInfo)
openGraphs GInfo
gInfo'
  case LibName -> Map LibName GInfo -> Maybe GInfo
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup LibName
ln Map LibName GInfo
og of
    Nothing -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Just gInfo :: GInfo
gInfo@(GInfo { graphInfo :: GInfo -> GraphInfo
graphInfo = GraphInfo
gi
                      , options :: GInfo -> IORef Flags
options = IORef Flags
opts }) -> do
      Flags
flags <- IORef Flags -> IO Flags
forall a. IORef a -> IO a
readIORef IORef Flags
opts
      let edges :: [EdgeId]
edges = if Flags -> Bool
flagHideEdges Flags
flags then DGraph -> [EdgeId]
hideEdgesAux DGraph
dg else []
          (nodes :: [NodeId]
nodes, comp :: [(NodeId, NodeId, DGEdgeType, Bool)]
comp) = if Flags -> Bool
flagHideNodes Flags
flags then DGraph
-> [EdgeId] -> ([NodeId], [(NodeId, NodeId, DGEdgeType, Bool)])
hideNodesAux DGraph
dg [EdgeId]
edges
                          else ([], [])
      GraphInfo -> String -> IO ()
GA.showTemporaryMessage GraphInfo
gi
        "Applying development graph calculus proof rule..."
      GraphInfo -> IO ()
GA.deactivateGraphWindow GraphInfo
gi
      GraphInfo
-> [DGChange]
-> [NodeId]
-> [EdgeId]
-> [(NodeId, NodeId, DGEdgeType, Bool)]
-> IO ()
GA.applyChanges GraphInfo
gi ([DGChange] -> [DGChange]
removeContraryChanges [DGChange]
changes) [NodeId]
nodes [EdgeId]
edges [(NodeId, NodeId, DGEdgeType, Bool)]
comp
      GraphInfo -> String -> IO ()
GA.showTemporaryMessage GraphInfo
gi
        "Updating graph..."
      GraphInfo -> IO ()
GA.redisplay GraphInfo
gi
      GInfo -> IO ()
hideNames GInfo
gInfo
      GraphInfo -> IO ()
GA.layoutImproveAll GraphInfo
gi
      GraphInfo -> IO ()
GA.activateGraphWindow GraphInfo
gi
      GraphInfo -> String -> IO ()
GA.showTemporaryMessage GraphInfo
gi
        "Development graph calculus proof rule finished."

-- | Toggles to display internal node names
hideNames :: GInfo -> IO ()
hideNames :: GInfo -> IO ()
hideNames (GInfo { options :: GInfo -> IORef Flags
options = IORef Flags
opts
                 , internalNames :: GInfo -> IORef [(String, (String -> String) -> IO ())]
internalNames = IORef [(String, (String -> String) -> IO ())]
updaterIORef }) = do
  Flags
flags <- IORef Flags -> IO Flags
forall a. IORef a -> IO a
readIORef IORef Flags
opts
  [(String, (String -> String) -> IO ())]
updater <- IORef [(String, (String -> String) -> IO ())]
-> IO [(String, (String -> String) -> IO ())]
forall a. IORef a -> IO a
readIORef IORef [(String, (String -> String) -> IO ())]
updaterIORef
  ((String, (String -> String) -> IO ()) -> IO ())
-> [(String, (String -> String) -> IO ())] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (s :: String
s, upd :: (String -> String) -> IO ()
upd) -> (String -> String) -> IO ()
upd (String -> String -> String
forall a b. a -> b -> a
const (String -> String -> String) -> String -> String -> String
forall a b. (a -> b) -> a -> b
$ if Flags -> Bool
flagHideNames Flags
flags then "" else String
s))
        [(String, (String -> String) -> IO ())]
updater

-- | Toggles to display internal node names
toggleHideNames :: GInfo -> IO ()
toggleHideNames :: GInfo -> IO ()
toggleHideNames gInfo :: GInfo
gInfo@(GInfo { graphInfo :: GInfo -> GraphInfo
graphInfo = GraphInfo
gi
                             , options :: GInfo -> IORef Flags
options = IORef Flags
opts }) = do
  Flags
flags <- IORef Flags -> IO Flags
forall a. IORef a -> IO a
readIORef IORef Flags
opts
  let hide :: Bool
hide = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Flags -> Bool
flagHideNames Flags
flags
  IORef Flags -> Flags -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef Flags
opts (Flags -> IO ()) -> Flags -> IO ()
forall a b. (a -> b) -> a -> b
$ Flags
flags { flagHideNames :: Bool
flagHideNames = Bool
hide }
  GraphInfo -> String -> IO ()
GA.showTemporaryMessage GraphInfo
gi (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ if Bool
hide then "Hiding internal names..."
                               else "Revealing internal names..."
  GInfo -> [DGChange] -> IO ()
updateGraph GInfo
gInfo []

-- | hides all unnamed internal nodes that are proven
hideNodesAux :: DGraph -> [EdgeId]
             -> ([GA.NodeId], [(GA.NodeId, GA.NodeId, DGEdgeType, Bool)])
hideNodesAux :: DGraph
-> [EdgeId] -> ([NodeId], [(NodeId, NodeId, DGEdgeType, Bool)])
hideNodesAux dg :: DGraph
dg ignoreEdges :: [EdgeId]
ignoreEdges =
  let nodes :: [NodeId]
nodes = DGraph -> (DGNodeType -> Bool) -> [NodeId]
selectNodesByType DGraph
dg
        (\ n :: DGNodeType
n -> DGNodeType -> Bool
isInternalSpec DGNodeType
n Bool -> Bool -> Bool
&& DGNodeType -> Bool
isProvenNode DGNodeType
n Bool -> Bool -> Bool
&& DGNodeType -> Bool
isProvenCons DGNodeType
n)
      edges :: [(NodeId, NodeId, DGEdgeType, Bool)]
edges = DGraph
-> [NodeId] -> [EdgeId] -> [(NodeId, NodeId, DGEdgeType, Bool)]
getCompressedEdges DGraph
dg [NodeId]
nodes [EdgeId]
ignoreEdges
  in ([NodeId]
nodes, [(NodeId, NodeId, DGEdgeType, Bool)]
edges)

toggleHideNodes :: GInfo -> IO ()
toggleHideNodes :: GInfo -> IO ()
toggleHideNodes gInfo :: GInfo
gInfo@(GInfo { graphInfo :: GInfo -> GraphInfo
graphInfo = GraphInfo
gi
                             , options :: GInfo -> IORef Flags
options = IORef Flags
opts }) = do
  Flags
flags <- IORef Flags -> IO Flags
forall a. IORef a -> IO a
readIORef IORef Flags
opts
  let hide :: Bool
hide = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Flags -> Bool
flagHideNodes Flags
flags
  IORef Flags -> Flags -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef Flags
opts (Flags -> IO ()) -> Flags -> IO ()
forall a b. (a -> b) -> a -> b
$ Flags
flags { flagHideNodes :: Bool
flagHideNodes = Bool
hide }
  GraphInfo -> String -> IO ()
GA.showTemporaryMessage GraphInfo
gi (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ if Bool
hide then "Hiding unnamed nodes..."
                               else "Revealing hidden nodes..."
  GInfo -> [DGChange] -> IO ()
updateGraph GInfo
gInfo []

hideEdgesAux :: DGraph -> [EdgeId]
hideEdgesAux :: DGraph -> [EdgeId]
hideEdgesAux dg :: DGraph
dg = (DGLinkLab -> EdgeId) -> [DGLinkLab] -> [EdgeId]
forall a b. (a -> b) -> [a] -> [b]
map DGLinkLab -> EdgeId
dgl_id
  ([DGLinkLab] -> [EdgeId]) -> [DGLinkLab] -> [EdgeId]
forall a b. (a -> b) -> a -> b
$ (DGLinkLab -> Bool) -> [DGLinkLab] -> [DGLinkLab]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (DGLink { dgl_type :: DGLinkLab -> DGLinkType
dgl_type = DGLinkType
linktype }) ->
             case DGLinkType
linktype of
               ScopedLink _ (ThmLink s :: ThmLinkStatus
s) c :: ConsStatus
c ->
                 ThmLinkStatus -> Bool
isProvenThmLinkStatus ThmLinkStatus
s Bool -> Bool -> Bool
&& ConsStatus -> Bool
isProvenConsStatusLink ConsStatus
c
               HidingFreeOrCofreeThm _ _ _ s :: ThmLinkStatus
s -> ThmLinkStatus -> Bool
isProvenThmLinkStatus ThmLinkStatus
s
               _ -> Bool
False
           )
  ([DGLinkLab] -> [DGLinkLab]) -> [DGLinkLab] -> [DGLinkLab]
forall a b. (a -> b) -> a -> b
$ ([DGLinkLab] -> DGChange -> [DGLinkLab])
-> [DGLinkLab] -> [DGChange] -> [DGLinkLab]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ e :: [DGLinkLab]
e c :: DGChange
c -> case DGChange
c of
                      InsertEdge (_, _, lbl :: DGLinkLab
lbl) -> DGLinkLab
lbl DGLinkLab -> [DGLinkLab] -> [DGLinkLab]
forall a. a -> [a] -> [a]
: [DGLinkLab]
e
                      DeleteEdge (_, _, lbl :: DGLinkLab
lbl) -> (DGLinkLab -> DGLinkLab -> Bool)
-> DGLinkLab -> [DGLinkLab] -> [DGLinkLab]
forall a. (a -> a -> Bool) -> a -> [a] -> [a]
deleteBy DGLinkLab -> DGLinkLab -> Bool
eqDGLinkLabById DGLinkLab
lbl [DGLinkLab]
e
                      _ -> [DGLinkLab]
e
          ) [] ([DGChange] -> [DGLinkLab]) -> [DGChange] -> [DGLinkLab]
forall a b. (a -> b) -> a -> b
$ [HistElem] -> [DGChange] -> [DGChange]
flattenHistory (SizedList HistElem -> [HistElem]
forall a. SizedList a -> [a]
SizedList.toList (SizedList HistElem -> [HistElem])
-> SizedList HistElem -> [HistElem]
forall a b. (a -> b) -> a -> b
$ DGraph -> SizedList HistElem
proofHistory DGraph
dg) []

toggleHideEdges :: GInfo -> IO ()
toggleHideEdges :: GInfo -> IO ()
toggleHideEdges gInfo :: GInfo
gInfo@(GInfo { graphInfo :: GInfo -> GraphInfo
graphInfo = GraphInfo
gi
                             , options :: GInfo -> IORef Flags
options = IORef Flags
opts }) = do
  Flags
flags <- IORef Flags -> IO Flags
forall a. IORef a -> IO a
readIORef IORef Flags
opts
  let hide :: Bool
hide = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Flags -> Bool
flagHideEdges Flags
flags
  IORef Flags -> Flags -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef Flags
opts (Flags -> IO ()) -> Flags -> IO ()
forall a b. (a -> b) -> a -> b
$ Flags
flags { flagHideEdges :: Bool
flagHideEdges = Bool
hide }
  GraphInfo -> String -> IO ()
GA.showTemporaryMessage GraphInfo
gi (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ if Bool
hide then "Hiding new proven edges..."
                               else "Revealing hidden proven edges..."
  GInfo -> [DGChange] -> IO ()
updateGraph GInfo
gInfo []

-- | generates from list of HistElem one list of DGChanges
flattenHistory :: [HistElem] -> [DGChange] -> [DGChange]
flattenHistory :: [HistElem] -> [DGChange] -> [DGChange]
flattenHistory [] cs :: [DGChange]
cs = [DGChange]
cs
flattenHistory (HistElem c :: DGChange
c : r :: [HistElem]
r) cs :: [DGChange]
cs = [HistElem] -> [DGChange] -> [DGChange]
flattenHistory [HistElem]
r ([DGChange] -> [DGChange]) -> [DGChange] -> [DGChange]
forall a b. (a -> b) -> a -> b
$ DGChange
c DGChange -> [DGChange] -> [DGChange]
forall a. a -> [a] -> [a]
: [DGChange]
cs
flattenHistory (HistGroup _ ph :: SizedList HistElem
ph : r :: [HistElem]
r) cs :: [DGChange]
cs =
  [HistElem] -> [DGChange] -> [DGChange]
flattenHistory [HistElem]
r ([DGChange] -> [DGChange]) -> [DGChange] -> [DGChange]
forall a b. (a -> b) -> a -> b
$ [HistElem] -> [DGChange] -> [DGChange]
flattenHistory (SizedList HistElem -> [HistElem]
forall a. SizedList a -> [a]
SizedList.toList SizedList HistElem
ph) [DGChange]
cs

-- | selects all nodes of a type with outgoing edges
selectNodesByType :: DGraph -> (DGNodeType -> Bool) -> [Node]
selectNodesByType :: DGraph -> (DGNodeType -> Bool) -> [NodeId]
selectNodesByType dg :: DGraph
dg types :: DGNodeType -> Bool
types =
  (NodeId -> Bool) -> [NodeId] -> [NodeId]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ n :: NodeId
n -> Bool -> Bool
not ([LEdge DGLinkLab] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([LEdge DGLinkLab] -> Bool) -> [LEdge DGLinkLab] -> Bool
forall a b. (a -> b) -> a -> b
$ DGraph -> NodeId -> [LEdge DGLinkLab]
outDG DGraph
dg NodeId
n) Bool -> Bool -> Bool
&& DGraph -> NodeId -> Bool
hasUnprovenEdges DGraph
dg NodeId
n) ([NodeId] -> [NodeId]) -> [NodeId] -> [NodeId]
forall a b. (a -> b) -> a -> b
$ ((NodeId, DGNodeLab) -> NodeId)
-> [(NodeId, DGNodeLab)] -> [NodeId]
forall a b. (a -> b) -> [a] -> [b]
map (NodeId, DGNodeLab) -> NodeId
forall a b. (a, b) -> a
fst
  ([(NodeId, DGNodeLab)] -> [NodeId])
-> [(NodeId, DGNodeLab)] -> [NodeId]
forall a b. (a -> b) -> a -> b
$ ((NodeId, DGNodeLab) -> Bool)
-> [(NodeId, DGNodeLab)] -> [(NodeId, DGNodeLab)]
forall a. (a -> Bool) -> [a] -> [a]
filter (DGNodeType -> Bool
types (DGNodeType -> Bool)
-> ((NodeId, DGNodeLab) -> DGNodeType)
-> (NodeId, DGNodeLab)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGNodeLab -> DGNodeType
getRealDGNodeType (DGNodeLab -> DGNodeType)
-> ((NodeId, DGNodeLab) -> DGNodeLab)
-> (NodeId, DGNodeLab)
-> DGNodeType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NodeId, DGNodeLab) -> DGNodeLab
forall a b. (a, b) -> b
snd) ([(NodeId, DGNodeLab)] -> [(NodeId, DGNodeLab)])
-> [(NodeId, DGNodeLab)] -> [(NodeId, DGNodeLab)]
forall a b. (a -> b) -> a -> b
$ DGraph -> [(NodeId, DGNodeLab)]
labNodesDG DGraph
dg

hasUnprovenEdges :: DGraph -> Node -> Bool
hasUnprovenEdges :: DGraph -> NodeId -> Bool
hasUnprovenEdges dg :: DGraph
dg =
  (Bool -> LEdge DGLinkLab -> Bool)
-> Bool -> [LEdge DGLinkLab] -> Bool
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ b :: Bool
b (_, _, l :: DGLinkLab
l) -> case DGEdgeType -> DGEdgeTypeModInc
edgeTypeModInc (DGEdgeType -> DGEdgeTypeModInc) -> DGEdgeType -> DGEdgeTypeModInc
forall a b. (a -> b) -> a -> b
$ DGLinkLab -> DGEdgeType
getRealDGLinkType DGLinkLab
l of
                          ThmType { isProvenEdge :: DGEdgeTypeModInc -> Bool
isProvenEdge = Bool
False } -> Bool
False
                          _ -> Bool
b) Bool
True ([LEdge DGLinkLab] -> Bool)
-> (NodeId -> [LEdge DGLinkLab]) -> NodeId -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\ n :: NodeId
n -> DGraph -> NodeId -> [LEdge DGLinkLab]
innDG DGraph
dg NodeId
n [LEdge DGLinkLab] -> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a. [a] -> [a] -> [a]
++ DGraph -> NodeId -> [LEdge DGLinkLab]
outDG DGraph
dg NodeId
n)

-- | compresses a list of types to the highest one
compressTypes :: Bool -> [DGEdgeType] -> (DGEdgeType, Bool)
compressTypes :: Bool -> [DGEdgeType] -> (DGEdgeType, Bool)
compressTypes _ [] = String -> (DGEdgeType, Bool)
forall a. HasCallStack => String -> a
error "compressTypes: wrong usage"
compressTypes b :: Bool
b (t :: DGEdgeType
t : []) = (DGEdgeType
t, Bool
b)
compressTypes b :: Bool
b (t1 :: DGEdgeType
t1 : t2 :: DGEdgeType
t2 : r :: [DGEdgeType]
r)
  | DGEdgeType
t1 DGEdgeType -> DGEdgeType -> Bool
forall a. Eq a => a -> a -> Bool
== DGEdgeType
t2 = Bool -> [DGEdgeType] -> (DGEdgeType, Bool)
compressTypes Bool
b (DGEdgeType
t1 DGEdgeType -> [DGEdgeType] -> [DGEdgeType]
forall a. a -> [a] -> [a]
: [DGEdgeType]
r)
  | DGEdgeType
t1 DGEdgeType -> DGEdgeType -> Bool
forall a. Ord a => a -> a -> Bool
> DGEdgeType
t2 = Bool -> [DGEdgeType] -> (DGEdgeType, Bool)
compressTypes Bool
False (DGEdgeType
t1 DGEdgeType -> [DGEdgeType] -> [DGEdgeType]
forall a. a -> [a] -> [a]
: [DGEdgeType]
r)
  | Bool
otherwise = Bool -> [DGEdgeType] -> (DGEdgeType, Bool)
compressTypes Bool
False (DGEdgeType
t2 DGEdgeType -> [DGEdgeType] -> [DGEdgeType]
forall a. a -> [a] -> [a]
: [DGEdgeType]
r)

-- | innDG with filter of not shown edges
fInnDG :: [EdgeId] -> DGraph -> Node -> [LEdge DGLinkLab]
fInnDG :: [EdgeId] -> DGraph -> NodeId -> [LEdge DGLinkLab]
fInnDG ignore :: [EdgeId]
ignore dg :: DGraph
dg = (LEdge DGLinkLab -> Bool) -> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (_, _, l :: DGLinkLab
l) -> EdgeId -> [EdgeId] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem (DGLinkLab -> EdgeId
dgl_id DGLinkLab
l) [EdgeId]
ignore) ([LEdge DGLinkLab] -> [LEdge DGLinkLab])
-> (NodeId -> [LEdge DGLinkLab]) -> NodeId -> [LEdge DGLinkLab]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGraph -> NodeId -> [LEdge DGLinkLab]
innDG DGraph
dg

-- | outDG with filter of not shown edges
fOutDG :: [EdgeId] -> DGraph -> Node -> [LEdge DGLinkLab]
fOutDG :: [EdgeId] -> DGraph -> NodeId -> [LEdge DGLinkLab]
fOutDG ignore :: [EdgeId]
ignore dg :: DGraph
dg = (LEdge DGLinkLab -> Bool) -> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (_, _, l :: DGLinkLab
l) -> EdgeId -> [EdgeId] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem (DGLinkLab -> EdgeId
dgl_id DGLinkLab
l) [EdgeId]
ignore) ([LEdge DGLinkLab] -> [LEdge DGLinkLab])
-> (NodeId -> [LEdge DGLinkLab]) -> NodeId -> [LEdge DGLinkLab]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGraph -> NodeId -> [LEdge DGLinkLab]
outDG DGraph
dg

-- | returns a list of compressed edges
getCompressedEdges :: DGraph -> [Node] -> [EdgeId]
                   -> [(Node, Node, DGEdgeType, Bool)]
getCompressedEdges :: DGraph
-> [NodeId] -> [EdgeId] -> [(NodeId, NodeId, DGEdgeType, Bool)]
getCompressedEdges dg :: DGraph
dg hidden :: [NodeId]
hidden ign :: [EdgeId]
ign = [(NodeId, NodeId, DGEdgeType, Bool)]
-> [(NodeId, NodeId, DGEdgeType, Bool)]
filterDuplicates ([(NodeId, NodeId, DGEdgeType, Bool)]
 -> [(NodeId, NodeId, DGEdgeType, Bool)])
-> [(NodeId, NodeId, DGEdgeType, Bool)]
-> [(NodeId, NodeId, DGEdgeType, Bool)]
forall a b. (a -> b) -> a -> b
$ [[LEdge DGLinkLab]] -> [(NodeId, NodeId, DGEdgeType, Bool)]
getShortPaths
  ([[LEdge DGLinkLab]] -> [(NodeId, NodeId, DGEdgeType, Bool)])
-> [[LEdge DGLinkLab]] -> [(NodeId, NodeId, DGEdgeType, Bool)]
forall a b. (a -> b) -> a -> b
$ (LEdge DGLinkLab -> [[LEdge DGLinkLab]])
-> [LEdge DGLinkLab] -> [[LEdge DGLinkLab]]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ e :: LEdge DGLinkLab
e@(_, t :: NodeId
t, _) -> ([LEdge DGLinkLab] -> [LEdge DGLinkLab])
-> [[LEdge DGLinkLab]] -> [[LEdge DGLinkLab]]
forall a b. (a -> b) -> [a] -> [b]
map (LEdge DGLinkLab
e LEdge DGLinkLab -> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a. a -> [a] -> [a]
:) ([[LEdge DGLinkLab]] -> [[LEdge DGLinkLab]])
-> [[LEdge DGLinkLab]] -> [[LEdge DGLinkLab]]
forall a b. (a -> b) -> a -> b
$ DGraph
-> NodeId
-> [NodeId]
-> [NodeId]
-> [EdgeId]
-> [[LEdge DGLinkLab]]
getPaths DGraph
dg NodeId
t [NodeId]
hidden [] [EdgeId]
ign) [LEdge DGLinkLab]
inEdges
  where
    inEdges :: [LEdge DGLinkLab]
inEdges = (LEdge DGLinkLab -> Bool) -> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (_, t :: NodeId
t, _) -> NodeId -> [NodeId] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem NodeId
t [NodeId]
hidden)
                     ([LEdge DGLinkLab] -> [LEdge DGLinkLab])
-> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a b. (a -> b) -> a -> b
$ (NodeId -> [LEdge DGLinkLab]) -> [NodeId] -> [LEdge DGLinkLab]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([EdgeId] -> DGraph -> NodeId -> [LEdge DGLinkLab]
fOutDG [EdgeId]
ign DGraph
dg)
                     ([NodeId] -> [LEdge DGLinkLab]) -> [NodeId] -> [LEdge DGLinkLab]
forall a b. (a -> b) -> a -> b
$ (LEdge DGLinkLab -> [NodeId] -> [NodeId])
-> [NodeId] -> [LEdge DGLinkLab] -> [NodeId]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ (n :: NodeId
n, _, _) i :: [NodeId]
i -> if NodeId -> [NodeId] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem NodeId
n [NodeId]
hidden
                                       Bool -> Bool -> Bool
|| NodeId -> [NodeId] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem NodeId
n [NodeId]
i then [NodeId]
i else NodeId
n NodeId -> [NodeId] -> [NodeId]
forall a. a -> [a] -> [a]
: [NodeId]
i) []
                     ([LEdge DGLinkLab] -> [NodeId]) -> [LEdge DGLinkLab] -> [NodeId]
forall a b. (a -> b) -> a -> b
$ (NodeId -> [LEdge DGLinkLab]) -> [NodeId] -> [LEdge DGLinkLab]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([EdgeId] -> DGraph -> NodeId -> [LEdge DGLinkLab]
fInnDG [EdgeId]
ign DGraph
dg) [NodeId]
hidden

-- | filter duplicate paths
filterDuplicates :: [(Node, Node, DGEdgeType, Bool)]
                 -> [(Node, Node, DGEdgeType, Bool)]
filterDuplicates :: [(NodeId, NodeId, DGEdgeType, Bool)]
-> [(NodeId, NodeId, DGEdgeType, Bool)]
filterDuplicates [] = []
filterDuplicates r :: [(NodeId, NodeId, DGEdgeType, Bool)]
r@((s :: NodeId
s, t :: NodeId
t, _, _) : _) = [(NodeId, NodeId, DGEdgeType, Bool)]
edges [(NodeId, NodeId, DGEdgeType, Bool)]
-> [(NodeId, NodeId, DGEdgeType, Bool)]
-> [(NodeId, NodeId, DGEdgeType, Bool)]
forall a. [a] -> [a] -> [a]
++ [(NodeId, NodeId, DGEdgeType, Bool)]
-> [(NodeId, NodeId, DGEdgeType, Bool)]
filterDuplicates [(NodeId, NodeId, DGEdgeType, Bool)]
others
  where
    (same :: [(NodeId, NodeId, DGEdgeType, Bool)]
same, others :: [(NodeId, NodeId, DGEdgeType, Bool)]
others) = ((NodeId, NodeId, DGEdgeType, Bool) -> Bool)
-> [(NodeId, NodeId, DGEdgeType, Bool)]
-> ([(NodeId, NodeId, DGEdgeType, Bool)],
    [(NodeId, NodeId, DGEdgeType, Bool)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (\ (s' :: NodeId
s', t' :: NodeId
t', _, _) -> NodeId
s NodeId -> NodeId -> Bool
forall a. Eq a => a -> a -> Bool
== NodeId
s' Bool -> Bool -> Bool
&& NodeId
t NodeId -> NodeId -> Bool
forall a. Eq a => a -> a -> Bool
== NodeId
t') [(NodeId, NodeId, DGEdgeType, Bool)]
r
    (mtypes :: [(NodeId, NodeId, DGEdgeType, Bool)]
mtypes, stypes :: [(NodeId, NodeId, DGEdgeType, Bool)]
stypes) = ((NodeId, NodeId, DGEdgeType, Bool) -> Bool)
-> [(NodeId, NodeId, DGEdgeType, Bool)]
-> ([(NodeId, NodeId, DGEdgeType, Bool)],
    [(NodeId, NodeId, DGEdgeType, Bool)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (\ (_, _, _, b :: Bool
b) -> Bool -> Bool
not Bool
b) [(NodeId, NodeId, DGEdgeType, Bool)]
same
    stypes' :: [(NodeId, NodeId, DGEdgeType, Bool)]
stypes' = ((NodeId, NodeId, DGEdgeType, Bool)
 -> [(NodeId, NodeId, DGEdgeType, Bool)]
 -> [(NodeId, NodeId, DGEdgeType, Bool)])
-> [(NodeId, NodeId, DGEdgeType, Bool)]
-> [(NodeId, NodeId, DGEdgeType, Bool)]
-> [(NodeId, NodeId, DGEdgeType, Bool)]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ e :: (NodeId, NodeId, DGEdgeType, Bool)
e es :: [(NodeId, NodeId, DGEdgeType, Bool)]
es -> if (NodeId, NodeId, DGEdgeType, Bool)
-> [(NodeId, NodeId, DGEdgeType, Bool)] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem (NodeId, NodeId, DGEdgeType, Bool)
e [(NodeId, NodeId, DGEdgeType, Bool)]
es then [(NodeId, NodeId, DGEdgeType, Bool)]
es else (NodeId, NodeId, DGEdgeType, Bool)
e (NodeId, NodeId, DGEdgeType, Bool)
-> [(NodeId, NodeId, DGEdgeType, Bool)]
-> [(NodeId, NodeId, DGEdgeType, Bool)]
forall a. a -> [a] -> [a]
: [(NodeId, NodeId, DGEdgeType, Bool)]
es) [] [(NodeId, NodeId, DGEdgeType, Bool)]
stypes
    (et' :: DGEdgeType
et', _) = Bool -> [DGEdgeType] -> (DGEdgeType, Bool)
compressTypes Bool
False ([DGEdgeType] -> (DGEdgeType, Bool))
-> [DGEdgeType] -> (DGEdgeType, Bool)
forall a b. (a -> b) -> a -> b
$ ((NodeId, NodeId, DGEdgeType, Bool) -> DGEdgeType)
-> [(NodeId, NodeId, DGEdgeType, Bool)] -> [DGEdgeType]
forall a b. (a -> b) -> [a] -> [b]
map (\ (_, _, et :: DGEdgeType
et, _) -> DGEdgeType
et) [(NodeId, NodeId, DGEdgeType, Bool)]
mtypes
    edges :: [(NodeId, NodeId, DGEdgeType, Bool)]
edges = if [(NodeId, NodeId, DGEdgeType, Bool)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(NodeId, NodeId, DGEdgeType, Bool)]
mtypes then [(NodeId, NodeId, DGEdgeType, Bool)]
stypes' else (NodeId
s, NodeId
t, DGEdgeType
et', Bool
False) (NodeId, NodeId, DGEdgeType, Bool)
-> [(NodeId, NodeId, DGEdgeType, Bool)]
-> [(NodeId, NodeId, DGEdgeType, Bool)]
forall a. a -> [a] -> [a]
: [(NodeId, NodeId, DGEdgeType, Bool)]
stypes'

-- | returns the pahts of a given node through hidden nodes
getPaths :: DGraph -> Node -> [Node] -> [Node] -> [EdgeId]
         -> [[LEdge DGLinkLab]]
getPaths :: DGraph
-> NodeId
-> [NodeId]
-> [NodeId]
-> [EdgeId]
-> [[LEdge DGLinkLab]]
getPaths dg :: DGraph
dg node :: NodeId
node hidden :: [NodeId]
hidden seen' :: [NodeId]
seen' ign :: [EdgeId]
ign = if NodeId -> [NodeId] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem NodeId
node [NodeId]
hidden then
  if [LEdge DGLinkLab] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [LEdge DGLinkLab]
edges then []
    else (LEdge DGLinkLab -> [[LEdge DGLinkLab]])
-> [LEdge DGLinkLab] -> [[LEdge DGLinkLab]]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ e :: LEdge DGLinkLab
e@(_, t :: NodeId
t, _) -> ([LEdge DGLinkLab] -> [LEdge DGLinkLab])
-> [[LEdge DGLinkLab]] -> [[LEdge DGLinkLab]]
forall a b. (a -> b) -> [a] -> [b]
map (LEdge DGLinkLab
e LEdge DGLinkLab -> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a. a -> [a] -> [a]
:) ([[LEdge DGLinkLab]] -> [[LEdge DGLinkLab]])
-> [[LEdge DGLinkLab]] -> [[LEdge DGLinkLab]]
forall a b. (a -> b) -> a -> b
$ DGraph
-> NodeId
-> [NodeId]
-> [NodeId]
-> [EdgeId]
-> [[LEdge DGLinkLab]]
getPaths DGraph
dg NodeId
t [NodeId]
hidden [NodeId]
seen [EdgeId]
ign)
                   [LEdge DGLinkLab]
edges
  else [[]]
  where
    seen :: [NodeId]
seen = NodeId
node NodeId -> [NodeId] -> [NodeId]
forall a. a -> [a] -> [a]
: [NodeId]
seen'
    edges :: [LEdge DGLinkLab]
edges = (LEdge DGLinkLab -> Bool) -> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (_, t :: NodeId
t, _) -> NodeId -> [NodeId] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem NodeId
t [NodeId]
seen) ([LEdge DGLinkLab] -> [LEdge DGLinkLab])
-> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a b. (a -> b) -> a -> b
$ [EdgeId] -> DGraph -> NodeId -> [LEdge DGLinkLab]
fOutDG [EdgeId]
ign DGraph
dg NodeId
node

-- | returns source and target node of a path with the compressed type
getShortPaths :: [[LEdge DGLinkLab]]
              -> [(Node, Node, DGEdgeType, Bool)]
getShortPaths :: [[LEdge DGLinkLab]] -> [(NodeId, NodeId, DGEdgeType, Bool)]
getShortPaths [] = []
getShortPaths (p :: [LEdge DGLinkLab]
p : r :: [[LEdge DGLinkLab]]
r) =
  (NodeId
s, NodeId
t, DGEdgeType
et, Bool
b)
    (NodeId, NodeId, DGEdgeType, Bool)
-> [(NodeId, NodeId, DGEdgeType, Bool)]
-> [(NodeId, NodeId, DGEdgeType, Bool)]
forall a. a -> [a] -> [a]
: [[LEdge DGLinkLab]] -> [(NodeId, NodeId, DGEdgeType, Bool)]
getShortPaths [[LEdge DGLinkLab]]
r
  where
    (s :: NodeId
s, _, _) = [LEdge DGLinkLab] -> LEdge DGLinkLab
forall a. [a] -> a
head [LEdge DGLinkLab]
p
    (_, t :: NodeId
t, _) = [LEdge DGLinkLab] -> LEdge DGLinkLab
forall a. [a] -> a
last [LEdge DGLinkLab]
p
    (et :: DGEdgeType
et, b :: Bool
b) = Bool -> [DGEdgeType] -> (DGEdgeType, Bool)
compressTypes Bool
True ([DGEdgeType] -> (DGEdgeType, Bool))
-> [DGEdgeType] -> (DGEdgeType, Bool)
forall a b. (a -> b) -> a -> b
$ (LEdge DGLinkLab -> DGEdgeType)
-> [LEdge DGLinkLab] -> [DGEdgeType]
forall a b. (a -> b) -> [a] -> [b]
map (\ (_, _, e :: DGLinkLab
e) -> DGLinkLab -> DGEdgeType
getRealDGLinkType DGLinkLab
e) [LEdge DGLinkLab]
p

-- | Let the user select a Node to focus
focusNode :: GInfo -> IO ()
focusNode :: GInfo -> IO ()
focusNode gInfo :: GInfo
gInfo@(GInfo { graphInfo :: GInfo -> GraphInfo
graphInfo = GraphInfo
gi
                       , libName :: GInfo -> LibName
libName = LibName
ln }) = do
 IntState
ost <- IORef IntState -> IO IntState
forall a. IORef a -> IO a
readIORef (IORef IntState -> IO IntState) -> IORef IntState -> IO IntState
forall a b. (a -> b) -> a -> b
$ GInfo -> IORef IntState
intState GInfo
gInfo
 case IntState -> Maybe IntIState
i_state IntState
ost of
  Nothing -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  Just ist :: IntIState
ist -> do
   let le :: LibEnv
le = IntIState -> LibEnv
i_libEnv IntIState
ist
   [(NodeId, DGNodeLab)]
idsnodes <- ((NodeId, DGNodeLab) -> IO Bool)
-> [(NodeId, DGNodeLab)] -> IO [(NodeId, DGNodeLab)]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM ((Bool -> Bool) -> IO Bool -> IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Bool -> Bool
not (IO Bool -> IO Bool)
-> ((NodeId, DGNodeLab) -> IO Bool)
-> (NodeId, DGNodeLab)
-> IO Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GraphInfo -> NodeId -> IO Bool
GA.isHiddenNode GraphInfo
gi (NodeId -> IO Bool)
-> ((NodeId, DGNodeLab) -> NodeId)
-> (NodeId, DGNodeLab)
-> IO Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NodeId, DGNodeLab) -> NodeId
forall a b. (a, b) -> a
fst)
                    ([(NodeId, DGNodeLab)] -> IO [(NodeId, DGNodeLab)])
-> [(NodeId, DGNodeLab)] -> IO [(NodeId, DGNodeLab)]
forall a b. (a -> b) -> a -> b
$ DGraph -> [(NodeId, DGNodeLab)]
labNodesDG (DGraph -> [(NodeId, DGNodeLab)])
-> DGraph -> [(NodeId, DGNodeLab)]
forall a b. (a -> b) -> a -> b
$ LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln LibEnv
le
   Maybe NodeId
selection <- String -> [String] -> IO (Maybe NodeId)
listBox "Select a node to focus"
     ([String] -> IO (Maybe NodeId)) -> [String] -> IO (Maybe NodeId)
forall a b. (a -> b) -> a -> b
$ ((NodeId, DGNodeLab) -> String)
-> [(NodeId, DGNodeLab)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\ (n :: NodeId
n, l :: DGNodeLab
l) -> NodeId -> String -> String
forall a. Show a => a -> String -> String
shows NodeId
n " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ DGNodeLab -> String
getDGNodeName DGNodeLab
l) [(NodeId, DGNodeLab)]
idsnodes
   case Maybe NodeId
selection of
    Just idx :: NodeId
idx -> GraphInfo -> NodeId -> IO ()
GA.focusNode GraphInfo
gi (NodeId -> IO ()) -> NodeId -> IO ()
forall a b. (a -> b) -> a -> b
$ (NodeId, DGNodeLab) -> NodeId
forall a b. (a, b) -> a
fst ((NodeId, DGNodeLab) -> NodeId) -> (NodeId, DGNodeLab) -> NodeId
forall a b. (a -> b) -> a -> b
$ [(NodeId, DGNodeLab)]
idsnodes [(NodeId, DGNodeLab)] -> NodeId -> (NodeId, DGNodeLab)
forall a. [a] -> NodeId -> a
!! NodeId
idx
    Nothing -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

showLibGraph :: GInfo -> LibFunc -> IO ()
showLibGraph :: GInfo -> (GInfo -> IO ()) -> IO ()
showLibGraph gInfo :: GInfo
gInfo showLib :: GInfo -> IO ()
showLib = do
  GInfo -> IO ()
showLib GInfo
gInfo
  () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

saveProofStatus :: GInfo -> FilePath -> IO ()
saveProofStatus :: GInfo -> String -> IO ()
saveProofStatus gInfo :: GInfo
gInfo@(GInfo { hetcatsOpts :: GInfo -> HetcatsOpts
hetcatsOpts = HetcatsOpts
opts
                             , libName :: GInfo -> LibName
libName = LibName
ln
                             }) file :: String
file = IO () -> IO ()
encapsulateWaitTermAct (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
  IntState
ost <- IORef IntState -> IO IntState
forall a. IORef a -> IO a
readIORef (IORef IntState -> IO IntState) -> IORef IntState -> IO IntState
forall a b. (a -> b) -> a -> b
$ GInfo -> IORef IntState
intState GInfo
gInfo
  case IntState -> Maybe IntIState
i_state IntState
ost of
   Nothing -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
   Just ist :: IntIState
ist -> do
    let proofStatus :: LibEnv
proofStatus = IntIState -> LibEnv
i_libEnv IntIState
ist
    String -> (LibName, SizedList HistElem) -> IO ()
forall a. ShATermLG a => String -> a -> IO ()
writeShATermFile String
file (LibName
ln, LibName -> LibEnv -> SizedList HistElem
lookupHistory LibName
ln LibEnv
proofStatus)
    HetcatsOpts -> NodeId -> String -> IO ()
putIfVerbose HetcatsOpts
opts 2 (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "Wrote " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
file

-- | implementation of open menu, read in a proof status
openProofStatus :: GInfo -> FilePath -> ConvFunc -> LibFunc
                -> IO ()
openProofStatus :: GInfo -> String -> ConvFunc -> (GInfo -> IO ()) -> IO ()
openProofStatus gInfo :: GInfo
gInfo@(GInfo { hetcatsOpts :: GInfo -> HetcatsOpts
hetcatsOpts = HetcatsOpts
opts
                             , libName :: GInfo -> LibName
libName = LibName
ln }) file :: String
file convGraph :: ConvFunc
convGraph showLib :: GInfo -> IO ()
showLib = do
  IntState
ost <- IORef IntState -> IO IntState
forall a. IORef a -> IO a
readIORef (IORef IntState -> IO IntState) -> IORef IntState -> IO IntState
forall a b. (a -> b) -> a -> b
$ GInfo -> IORef IntState
intState GInfo
gInfo
  case IntState -> Maybe IntIState
i_state IntState
ost of
    Nothing -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Just ist :: IntIState
ist -> do
      Maybe (SizedList HistElem)
mh <- LogicGraph
-> HetcatsOpts
-> Maybe LibName
-> String
-> IO (Maybe (SizedList HistElem))
forall a.
ShATermLG a =>
LogicGraph
-> HetcatsOpts -> Maybe LibName -> String -> IO (Maybe a)
readVerbose LogicGraph
logicGraph HetcatsOpts
opts (LibName -> Maybe LibName
forall a. a -> Maybe a
Just LibName
ln) String
file
      case Maybe (SizedList HistElem)
mh of
        Nothing -> String -> String -> IO ()
errorDialog "Error" (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$
                     "Could not read proof status from file '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
file String -> String -> String
forall a. [a] -> [a] -> [a]
++ "'"
        Just h :: SizedList HistElem
h -> do
          let libfile :: String
libfile = LibName -> String
libNameToFile LibName
ln
          Maybe (LibName, LibEnv)
m <- HetcatsOpts -> String -> IO (Maybe (LibName, LibEnv))
anaLib HetcatsOpts
opts { outtypes :: [OutType]
outtypes = [] } String
libfile
          case Maybe (LibName, LibEnv)
m of
            Nothing -> String -> String -> IO ()
errorDialog "Error"
                         (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "Could not read original development graph from '"
                           String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
libfile String -> String -> String
forall a. [a] -> [a] -> [a]
++ "'"
            Just (_, libEnv :: LibEnv
libEnv) -> case LibName -> LibEnv -> Maybe DGraph
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup LibName
ln LibEnv
libEnv of
              Nothing -> String -> String -> IO ()
errorDialog "Error" (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "Could not get original"
                           String -> String -> String
forall a. [a] -> [a] -> [a]
++ "development graph for '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ LibName -> String -> String
forall a. Pretty a => a -> String -> String
showDoc LibName
ln "'"
              Just dg :: DGraph
dg -> do
                GInfo -> IO ()
lockGlobal GInfo
gInfo
                let oldEnv :: LibEnv
oldEnv = IntIState -> LibEnv
i_libEnv IntIState
ist
                    proofStatus :: LibEnv
proofStatus = LibName -> DGraph -> LibEnv -> LibEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert LibName
ln (SizedList HistElem -> DGraph -> DGraph
applyProofHistory SizedList HistElem
h DGraph
dg) LibEnv
oldEnv
                    nwst :: IntState
nwst = IntState
ost { i_state :: Maybe IntIState
i_state = IntIState -> Maybe IntIState
forall a. a -> Maybe a
Just IntIState
ist { i_libEnv :: LibEnv
i_libEnv = LibEnv
proofStatus } }
                IORef IntState -> IntState -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (GInfo -> IORef IntState
intState GInfo
gInfo) IntState
nwst
                GInfo -> IO ()
unlockGlobal GInfo
gInfo
                GInfo
gInfo' <- GInfo -> LibName -> IO GInfo
copyGInfo GInfo
gInfo LibName
ln
                ConvFunc
convGraph GInfo
gInfo' "Proof Status " GInfo -> IO ()
showLib
                let gi :: GraphInfo
gi = GInfo -> GraphInfo
graphInfo GInfo
gInfo'
                GraphInfo -> IO ()
GA.deactivateGraphWindow GraphInfo
gi
                GraphInfo -> IO ()
GA.redisplay GraphInfo
gi
                GraphInfo -> IO ()
GA.layoutImproveAll GraphInfo
gi
                GraphInfo -> IO ()
GA.activateGraphWindow GraphInfo
gi

-- | apply a rule of the development graph calculus
proofMenu :: GInfo
             -> Command
             -> (LibEnv -> IO (Result LibEnv))
             -> IO ()
proofMenu :: GInfo -> Command -> (LibEnv -> IO (Result LibEnv)) -> IO ()
proofMenu gInfo :: GInfo
gInfo@(GInfo { hetcatsOpts :: GInfo -> HetcatsOpts
hetcatsOpts = HetcatsOpts
hOpts
                       , libName :: GInfo -> LibName
libName = LibName
ln
                       }) cmd :: Command
cmd proofFun :: LibEnv -> IO (Result LibEnv)
proofFun = do
  IntState
ost <- IORef IntState -> IO IntState
forall a. IORef a -> IO a
readIORef (IORef IntState -> IO IntState) -> IORef IntState -> IO IntState
forall a b. (a -> b) -> a -> b
$ GInfo -> IORef IntState
intState GInfo
gInfo
  case IntState -> Maybe IntIState
i_state IntState
ost of
    Nothing -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Just ist :: IntIState
ist -> do
      let ost2 :: IntState
ost2 = Command -> IntState -> [UndoRedoElem] -> IntState
add2history Command
cmd IntState
ost []
          ost3 :: IntState
ost3 = Command -> IntState -> [UndoRedoElem] -> IntState
add2history (String -> Command
CommentCmd "") IntState
ost2 []
      IORef IntState -> IntState -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (GInfo -> IORef IntState
intState GInfo
gInfo) IntState
ost3
      GInfo -> IO ()
lockGlobal GInfo
gInfo
      let proofStatus :: LibEnv
proofStatus = IntIState -> LibEnv
i_libEnv IntIState
ist
      HetcatsOpts -> NodeId -> String -> IO ()
putIfVerbose HetcatsOpts
hOpts 4 "Proof started via menu"
      Result ds :: [Diagnosis]
ds res :: Maybe LibEnv
res <- LibEnv -> IO (Result LibEnv)
proofFun LibEnv
proofStatus
      HetcatsOpts -> NodeId -> String -> IO ()
putIfVerbose HetcatsOpts
hOpts 4 "Analyzing result of proof"
      case Maybe LibEnv
res of
        Nothing -> do
          GInfo -> IO ()
unlockGlobal GInfo
gInfo
          NodeId -> [Diagnosis] -> IO ()
printDiags 2 [Diagnosis]
ds
        Just newProofStatus :: LibEnv
newProofStatus -> do
          IntState
ostate <- IORef IntState -> IO IntState
forall a. IORef a -> IO a
readIORef (IORef IntState -> IO IntState) -> IORef IntState -> IO IntState
forall a b. (a -> b) -> a -> b
$ GInfo -> IORef IntState
intState GInfo
gInfo
          let newGr :: DGraph
newGr = LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln LibEnv
newProofStatus
              history :: SizedList HistElem
history = (SizedList HistElem, SizedList HistElem) -> SizedList HistElem
forall a b. (a, b) -> b
snd ((SizedList HistElem, SizedList HistElem) -> SizedList HistElem)
-> (SizedList HistElem, SizedList HistElem) -> SizedList HistElem
forall a b. (a -> b) -> a -> b
$ DGraph -> DGraph -> (SizedList HistElem, SizedList HistElem)
splitHistory (LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln LibEnv
proofStatus) DGraph
newGr
              lln :: [UndoRedoElem]
lln = (LibName -> UndoRedoElem) -> [LibName] -> [UndoRedoElem]
forall a b. (a -> b) -> [a] -> [b]
map LibName -> UndoRedoElem
DgCommandChange ([LibName] -> [UndoRedoElem]) -> [LibName] -> [UndoRedoElem]
forall a b. (a -> b) -> a -> b
$ LibEnv -> LibEnv -> [LibName]
calcGlobalHistory
                                                   LibEnv
proofStatus LibEnv
newProofStatus
              nst :: IntState
nst = Command -> IntState -> [UndoRedoElem] -> IntState
add2history (String -> Command
CommentCmd "") IntState
ostate [UndoRedoElem]
lln
              nwst :: IntState
nwst = IntState
nst { i_state :: Maybe IntIState
i_state = IntIState -> Maybe IntIState
forall a. a -> Maybe a
Just IntIState
ist { i_libEnv :: LibEnv
i_libEnv = LibEnv
newProofStatus}}
          HetcatsOpts -> String -> IO () -> IO ()
doDump HetcatsOpts
hOpts "PrintHistory" (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
            String -> IO ()
putStrLn "History"
            Doc -> IO ()
forall a. Show a => a -> IO ()
print (Doc -> IO ()) -> Doc -> IO ()
forall a b. (a -> b) -> a -> b
$ SizedList HistElem -> Doc
prettyHistory SizedList HistElem
history
          IORef IntState -> IntState -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (GInfo -> IORef IntState
intState GInfo
gInfo) IntState
nwst
          GInfo -> [DGChange] -> IO ()
updateGraph GInfo
gInfo ([DGChange] -> [DGChange]
forall a. [a] -> [a]
reverse ([DGChange] -> [DGChange]) -> [DGChange] -> [DGChange]
forall a b. (a -> b) -> a -> b
$ SizedList HistElem -> [DGChange]
flatHistory SizedList HistElem
history)
          GInfo -> IO ()
unlockGlobal GInfo
gInfo

calcGlobalHistory :: LibEnv -> LibEnv -> [LibName]
calcGlobalHistory :: LibEnv -> LibEnv -> [LibName]
calcGlobalHistory old :: LibEnv
old new :: LibEnv
new = let
    length' :: LibName -> LibEnv -> NodeId
length' ln :: LibName
ln = SizedList HistElem -> NodeId
forall a. SizedList a -> NodeId
SizedList.size (SizedList HistElem -> NodeId)
-> (LibEnv -> SizedList HistElem) -> LibEnv -> NodeId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGraph -> SizedList HistElem
proofHistory (DGraph -> SizedList HistElem)
-> (LibEnv -> DGraph) -> LibEnv -> SizedList HistElem
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln
    changes :: [LibName]
changes = (LibName -> Bool) -> [LibName] -> [LibName]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ ln :: LibName
ln -> LibName -> LibEnv -> NodeId
length' LibName
ln LibEnv
old NodeId -> NodeId -> Bool
forall a. Ord a => a -> a -> Bool
< LibName -> LibEnv -> NodeId
length' LibName
ln LibEnv
new) ([LibName] -> [LibName]) -> [LibName] -> [LibName]
forall a b. (a -> b) -> a -> b
$ LibEnv -> [LibName]
forall k a. Map k a -> [k]
Map.keys LibEnv
old
  in (LibName -> [LibName]) -> [LibName] -> [LibName]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ ln :: LibName
ln -> NodeId -> LibName -> [LibName]
forall a. NodeId -> a -> [a]
replicate (LibName -> LibEnv -> NodeId
length' LibName
ln LibEnv
new NodeId -> NodeId -> NodeId
forall a. Num a => a -> a -> a
- LibName -> LibEnv -> NodeId
length' LibName
ln LibEnv
old) LibName
ln) [LibName]
changes

showNodeInfo :: Int -> DGraph -> IO ()
showNodeInfo :: NodeId -> DGraph -> IO ()
showNodeInfo descr :: NodeId
descr dgraph :: DGraph
dgraph = do
  let dgnode :: DGNodeLab
dgnode = DGraph -> NodeId -> DGNodeLab
labDG DGraph
dgraph NodeId
descr
      title :: String
title = (if DGNodeLab -> Bool
isDGRef DGNodeLab
dgnode then ("reference " String -> String -> String
forall a. [a] -> [a] -> [a]
++) else
               if DGNodeLab -> Bool
isInternalNode DGNodeLab
dgnode then ("internal " String -> String -> String
forall a. [a] -> [a] -> [a]
++) else String -> String
forall a. a -> a
id)
              "node " String -> String -> String
forall a. [a] -> [a] -> [a]
++ DGNodeLab -> String
getDGNodeName DGNodeLab
dgnode String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ NodeId -> String
forall a. Show a => a -> String
show NodeId
descr
  String -> String -> IO ()
createTextDisplay String
title (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
title String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n"
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ GlobalAnnos -> DGNodeLab -> String -> String
forall a. Pretty a => GlobalAnnos -> a -> String -> String
showGlobalDoc (DGraph -> GlobalAnnos
globalAnnos DGraph
dgraph) DGNodeLab
dgnode ""

showDiagMessAux :: Int -> [Diagnosis] -> IO ()
showDiagMessAux :: NodeId -> [Diagnosis] -> IO ()
showDiagMessAux v :: NodeId
v ds :: [Diagnosis]
ds = let es :: [Diagnosis]
es = NodeId -> [Diagnosis] -> [Diagnosis]
filterDiags NodeId
v [Diagnosis]
ds in
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Diagnosis] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Diagnosis]
es) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ (if [Diagnosis] -> Bool
hasErrors [Diagnosis]
es then String -> String -> IO ()
errorDialog "Error"
                        else String -> String -> IO ()
infoDialog "Info") (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (Diagnosis -> String) -> [Diagnosis] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Diagnosis -> String
forall a. Show a => a -> String
show [Diagnosis]
es

showDiagMess :: HetcatsOpts -> [Diagnosis] -> IO ()
showDiagMess :: HetcatsOpts -> [Diagnosis] -> IO ()
showDiagMess = NodeId -> [Diagnosis] -> IO ()
showDiagMessAux (NodeId -> [Diagnosis] -> IO ())
-> (HetcatsOpts -> NodeId) -> HetcatsOpts -> [Diagnosis] -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HetcatsOpts -> NodeId
verbose

{- | outputs the theory of a node in a window;
     used by the node menu -}
getTheoryOfNode :: GInfo -> Int -> DGraph -> IO ()
getTheoryOfNode :: GInfo -> NodeId -> DGraph -> IO ()
getTheoryOfNode gInfo :: GInfo
gInfo descr :: NodeId
descr dgraph :: DGraph
dgraph = do
  IntState
ost <- IORef IntState -> IO IntState
forall a. IORef a -> IO a
readIORef (IORef IntState -> IO IntState) -> IORef IntState -> IO IntState
forall a b. (a -> b) -> a -> b
$ GInfo -> IORef IntState
intState GInfo
gInfo
  case IntState -> Maybe IntIState
i_state IntState
ost of
    Nothing -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Just ist :: IntIState
ist -> case LibEnv -> LibName -> NodeId -> Maybe G_theory
computeTheory (IntIState -> LibEnv
i_libEnv IntIState
ist) (GInfo -> LibName
libName GInfo
gInfo) NodeId
descr of
      Nothing ->
        String -> String -> IO ()
errorDialog "Error" (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "no global theory for node " String -> String -> String
forall a. [a] -> [a] -> [a]
++ NodeId -> String
forall a. Show a => a -> String
show NodeId
descr
      Just th :: G_theory
th -> String -> String -> IO ()
displayTheoryOfNode (NodeId -> DGraph -> String
getNameOfNode NodeId
descr DGraph
dgraph)
          (DGraph -> NodeId -> String
addHasInHidingWarning DGraph
dgraph NodeId
descr
          String -> String -> String
forall a. [a] -> [a] -> [a]
++ GlobalAnnos -> G_theory -> String -> String
forall a. Pretty a => GlobalAnnos -> a -> String -> String
showGlobalDoc (DGraph -> GlobalAnnos
globalAnnos DGraph
dgraph) G_theory
th "\n")

-- | displays a theory with warning in a window
displayTheoryOfNode :: String -- ^ Name of theory
                    -> String -- ^ Body text
                    -> IO ()
displayTheoryOfNode :: String -> String -> IO ()
displayTheoryOfNode n :: String
n = String -> String -> String -> IO ()
createTextSaveDisplay ("Theory of " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
n) (String
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ ".dol")

{- | translate the theory of a node in a window;
     used by the node menu -}
translateTheoryOfNode :: GInfo -> Int -> DGraph -> IO ()
translateTheoryOfNode :: GInfo -> NodeId -> DGraph -> IO ()
translateTheoryOfNode gInfo :: GInfo
gInfo@(GInfo { hetcatsOpts :: GInfo -> HetcatsOpts
hetcatsOpts = HetcatsOpts
opts
                                   , libName :: GInfo -> LibName
libName = LibName
ln }) node :: NodeId
node dgraph :: DGraph
dgraph = do
  IntState
ost <- IORef IntState -> IO IntState
forall a. IORef a -> IO a
readIORef (IORef IntState -> IO IntState) -> IORef IntState -> IO IntState
forall a b. (a -> b) -> a -> b
$ GInfo -> IORef IntState
intState GInfo
gInfo
  case IntState -> Maybe IntIState
i_state IntState
ost of
    Nothing -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Just ist :: IntIState
ist -> do
      let libEnv :: LibEnv
libEnv = IntIState -> LibEnv
i_libEnv IntIState
ist
      case LibEnv -> LibName -> NodeId -> Maybe G_theory
computeTheory LibEnv
libEnv LibName
ln NodeId
node of
        Just th :: G_theory
th@(G_theory lid :: lid
lid _ sign :: ExtSign sign symbol
sign _ sens :: ThSens sentence (AnyComorphism, BasicProof)
sens _) -> do
          -- find all comorphism paths starting from lid
          let paths :: [AnyComorphism]
paths = LogicGraph -> G_sublogics -> [AnyComorphism]
findComorphismPaths LogicGraph
logicGraph (G_theory -> G_sublogics
sublogicOfTh G_theory
th)
          -- let the user choose one
          Maybe NodeId
sel <- String -> [String] -> IO (Maybe NodeId)
listBox "Choose a node logic translation" ([String] -> IO (Maybe NodeId)) -> [String] -> IO (Maybe NodeId)
forall a b. (a -> b) -> a -> b
$ (AnyComorphism -> String) -> [AnyComorphism] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map AnyComorphism -> String
forall a. Show a => a -> String
show [AnyComorphism]
paths
          case Maybe NodeId
sel of
            Nothing -> String -> String -> IO ()
errorDialog "Error" "no node logic translation chosen"
            Just i :: NodeId
i -> do
              Comorphism cid :: cid
cid <- AnyComorphism -> IO AnyComorphism
forall (m :: * -> *) a. Monad m => a -> m a
return ([AnyComorphism]
paths [AnyComorphism] -> NodeId -> AnyComorphism
forall a. [a] -> NodeId -> a
!! NodeId
i)
              -- adjust lid's
              let lidS :: lid1
lidS = cid -> lid1
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid1
sourceLogic cid
cid
                  lidT :: lid2
lidT = cid -> lid2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid2
targetLogic cid
cid
              ExtSign sign1 symbol1
sign' <- lid
-> lid1
-> String
-> ExtSign sign symbol
-> IO (ExtSign sign1 symbol1)
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1
-> lid2
-> String
-> ExtSign sign1 symbol1
-> m (ExtSign sign2 symbol2)
coerceSign lid
lid lid1
lidS "" ExtSign sign symbol
sign
              ThSens sentence1 (AnyComorphism, BasicProof)
sens' <- lid
-> lid1
-> String
-> ThSens sentence (AnyComorphism, BasicProof)
-> IO (ThSens sentence1 (AnyComorphism, BasicProof))
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *) b.
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m, Typeable b) =>
lid1
-> lid2 -> String -> ThSens sentence1 b -> m (ThSens sentence2 b)
coerceThSens lid
lid lid1
lidS "" ThSens sentence (AnyComorphism, BasicProof)
sens
              -- translate theory along chosen comorphism
              let Result es :: [Diagnosis]
es mTh :: Maybe (sign2, [Named sentence2])
mTh = cid
-> (sign1, [Named sentence1]) -> Result (sign2, [Named sentence2])
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid
-> (sign1, [Named sentence1]) -> Result (sign2, [Named sentence2])
wrapMapTheory cid
cid
                    (ExtSign sign1 symbol1 -> sign1
forall sign symbol. ExtSign sign symbol -> sign
plainSign ExtSign sign1 symbol1
sign', ThSens sentence1 (AnyComorphism, BasicProof) -> [Named sentence1]
forall a b. ThSens a b -> [Named a]
toNamedList ThSens sentence1 (AnyComorphism, BasicProof)
sens')
              case Maybe (sign2, [Named sentence2])
mTh of
                Nothing -> HetcatsOpts -> [Diagnosis] -> IO ()
showDiagMess HetcatsOpts
opts [Diagnosis]
es
                Just (sign'' :: sign2
sign'', sens1 :: [Named sentence2]
sens1) -> String -> String -> String -> G_theory -> IO ()
displayTheoryWithWarning
                  "Translated Theory" (NodeId -> DGraph -> String
getNameOfNode NodeId
node DGraph
dgraph)
                  (DGraph -> NodeId -> String
addHasInHidingWarning DGraph
dgraph NodeId
node)
                  (G_theory -> IO ()) -> G_theory -> IO ()
forall a b. (a -> b) -> a -> b
$ lid2
-> Maybe IRI
-> ExtSign sign2 symbol2
-> SigId
-> ThSens sentence2 (AnyComorphism, BasicProof)
-> ThId
-> G_theory
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid
-> Maybe IRI
-> ExtSign sign symbol
-> SigId
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
G_theory lid2
lidT Maybe IRI
forall a. Maybe a
Nothing (sign2 -> ExtSign sign2 symbol2
forall sign symbol. sign -> ExtSign sign symbol
mkExtSign sign2
sign'') SigId
startSigId
                      ([Named sentence2] -> ThSens sentence2 (AnyComorphism, BasicProof)
forall a b. Ord a => [Named a] -> ThSens a b
toThSens [Named sentence2]
sens1) ThId
startThId
        Nothing ->
          String -> String -> IO ()
errorDialog "Error" (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "no global theory for node " String -> String -> String
forall a. [a] -> [a] -> [a]
++ NodeId -> String
forall a. Show a => a -> String
show NodeId
node

-- | Show proof status of a node
showProofStatusOfNode :: GInfo -> Int -> DGraph -> IO ()
showProofStatusOfNode :: GInfo -> NodeId -> DGraph -> IO ()
showProofStatusOfNode _ descr :: NodeId
descr dgraph :: DGraph
dgraph =
  let dgnode :: DGNodeLab
dgnode = DGraph -> NodeId -> DGNodeLab
labDG DGraph
dgraph NodeId
descr
      stat :: String
stat = DGNodeLab -> String
showStatusAux DGNodeLab
dgnode
      title :: String
title = "Proof status of node " String -> String -> String
forall a. [a] -> [a] -> [a]
++ DGNodeLab -> String
getDGNodeName DGNodeLab
dgnode
  in String -> String -> IO ()
createTextDisplay String
title String
stat

showStatusAux :: DGNodeLab -> String
showStatusAux :: DGNodeLab -> String
showStatusAux dgnode :: DGNodeLab
dgnode = case G_theory -> G_theory
simplifyTh (G_theory -> G_theory) -> G_theory -> G_theory
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> G_theory
dgn_theory DGNodeLab
dgnode of
  G_theory _ _ _ _ sens :: ThSens sentence (AnyComorphism, BasicProof)
sens _ ->
     let goals :: ThSens sentence (AnyComorphism, BasicProof)
goals = (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) -> Bool)
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
forall k a. Ord k => (a -> Bool) -> OMap k a -> OMap k a
OMap.filter (Bool -> Bool
not (Bool -> Bool)
-> (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
    -> Bool)
-> SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) -> Bool
forall s a. SenAttr s a -> Bool
isAxiom) ThSens sentence (AnyComorphism, BasicProof)
sens
         (proven :: ThSens sentence (AnyComorphism, BasicProof)
proven, open :: ThSens sentence (AnyComorphism, BasicProof)
open) = (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) -> Bool)
-> ThSens sentence (AnyComorphism, BasicProof)
-> (ThSens sentence (AnyComorphism, BasicProof),
    ThSens sentence (AnyComorphism, BasicProof))
forall k a.
Ord k =>
(a -> Bool) -> OMap k a -> (OMap k a, OMap k a)
OMap.partition SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) -> Bool
forall a. SenStatus a (AnyComorphism, BasicProof) -> Bool
isProvenSenStatus ThSens sentence (AnyComorphism, BasicProof)
goals
         consGoal :: String
consGoal = "\nconservativity of this node"
      in "Proven proof goals:\n"
         String -> String -> String
forall a. [a] -> [a] -> [a]
++ OMap String sentence -> String -> String
forall a. Pretty a => a -> String -> String
showDoc ((SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
 -> sentence)
-> ThSens sentence (AnyComorphism, BasicProof)
-> OMap String sentence
forall k a b. Ord k => (a -> b) -> OMap k a -> OMap k b
OMap.map SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
-> sentence
forall s a. SenAttr s a -> s
sentence ThSens sentence (AnyComorphism, BasicProof)
proven) ""
         String -> String -> String
forall a. [a] -> [a] -> [a]
++ if Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Bool -> DGNodeLab -> Bool
hasOpenNodeConsStatus Bool
True DGNodeLab
dgnode
             then String
consGoal
             else ""
         String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\nOpen proof goals:\n"
         String -> String -> String
forall a. [a] -> [a] -> [a]
++ OMap String sentence -> String -> String
forall a. Pretty a => a -> String -> String
showDoc ((SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
 -> sentence)
-> ThSens sentence (AnyComorphism, BasicProof)
-> OMap String sentence
forall k a b. Ord k => (a -> b) -> OMap k a -> OMap k b
OMap.map SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
-> sentence
forall s a. SenAttr s a -> s
sentence ThSens sentence (AnyComorphism, BasicProof)
open) ""
         String -> String -> String
forall a. [a] -> [a] -> [a]
++ if Bool -> DGNodeLab -> Bool
hasOpenNodeConsStatus Bool
False DGNodeLab
dgnode
             then String
consGoal
             else ""

hidingWarnDiag :: DGNodeLab -> IO Bool
hidingWarnDiag :: DGNodeLab -> IO Bool
hidingWarnDiag dgn :: DGNodeLab
dgn = if DGNodeLab -> Bool
labelHasHiding DGNodeLab
dgn then
  String -> String -> IO Bool
warningDialog "Warning" (String -> IO Bool) -> String -> IO Bool
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [String]
hidingWarning [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ["Try anyway?"]
  else Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True

ensureLockAtNode :: GInfo -> Int -> DGraph
                 -> IO (Maybe (DGraph, DGNodeLab, LibEnv))
ensureLockAtNode :: GInfo -> NodeId -> DGraph -> IO (Maybe (DGraph, DGNodeLab, LibEnv))
ensureLockAtNode gi :: GInfo
gi descr :: NodeId
descr dg :: DGraph
dg = do
  let ln :: LibName
ln = GInfo -> LibName
libName GInfo
gi
      iSt :: IORef IntState
iSt = GInfo -> IORef IntState
intState GInfo
gi
  IntState
ost <- IORef IntState -> IO IntState
forall a. IORef a -> IO a
readIORef IORef IntState
iSt
  case IntState -> Maybe IntIState
i_state IntState
ost of
    Nothing -> Maybe (DGraph, DGNodeLab, LibEnv)
-> IO (Maybe (DGraph, DGNodeLab, LibEnv))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (DGraph, DGNodeLab, LibEnv)
forall a. Maybe a
Nothing
    Just ist :: IntIState
ist -> let
      le :: LibEnv
le = IntIState -> LibEnv
i_libEnv IntIState
ist
      dgn :: DGNodeLab
dgn = DGraph -> NodeId -> DGNodeLab
labDG DGraph
dg NodeId
descr in if DGNodeLab -> Bool
hasLock DGNodeLab
dgn
        then Maybe (DGraph, DGNodeLab, LibEnv)
-> IO (Maybe (DGraph, DGNodeLab, LibEnv))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (DGraph, DGNodeLab, LibEnv)
 -> IO (Maybe (DGraph, DGNodeLab, LibEnv)))
-> Maybe (DGraph, DGNodeLab, LibEnv)
-> IO (Maybe (DGraph, DGNodeLab, LibEnv))
forall a b. (a -> b) -> a -> b
$ (DGraph, DGNodeLab, LibEnv) -> Maybe (DGraph, DGNodeLab, LibEnv)
forall a. a -> Maybe a
Just (DGraph
dg, DGNodeLab
dgn, LibEnv
le)
        else do
          GInfo -> IO ()
lockGlobal GInfo
gi
          (dgraph' :: DGraph
dgraph', dgn' :: DGNodeLab
dgn') <- DGraph -> (NodeId, DGNodeLab) -> IO (DGraph, DGNodeLab)
initLocking (LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln LibEnv
le) (NodeId
descr, DGNodeLab
dgn)
          let nwle :: LibEnv
nwle = LibName -> DGraph -> LibEnv -> LibEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert LibName
ln DGraph
dgraph' LibEnv
le
              nwst :: IntState
nwst = IntState
ost { i_state :: Maybe IntIState
i_state = IntIState -> Maybe IntIState
forall a. a -> Maybe a
Just (IntIState -> Maybe IntIState) -> IntIState -> Maybe IntIState
forall a b. (a -> b) -> a -> b
$ IntIState
ist { i_libEnv :: LibEnv
i_libEnv = LibEnv
nwle} }
          IORef IntState -> IntState -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef IntState
iSt IntState
nwst
          GInfo -> IO ()
unlockGlobal GInfo
gi
          Maybe (DGraph, DGNodeLab, LibEnv)
-> IO (Maybe (DGraph, DGNodeLab, LibEnv))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (DGraph, DGNodeLab, LibEnv)
 -> IO (Maybe (DGraph, DGNodeLab, LibEnv)))
-> Maybe (DGraph, DGNodeLab, LibEnv)
-> IO (Maybe (DGraph, DGNodeLab, LibEnv))
forall a b. (a -> b) -> a -> b
$ (DGraph, DGNodeLab, LibEnv) -> Maybe (DGraph, DGNodeLab, LibEnv)
forall a. a -> Maybe a
Just (DGraph
dgraph', DGNodeLab
dgn', LibEnv
nwle)

-- | start local theorem proving or consistency checking at a node
proveAtNode :: GInfo -> Int -> DGraph -> IO ()
proveAtNode :: GInfo -> NodeId -> DGraph -> IO ()
proveAtNode gInfo :: GInfo
gInfo descr :: NodeId
descr dgraph :: DGraph
dgraph = do
  let ln :: LibName
ln = GInfo -> LibName
libName GInfo
gInfo
      iSt :: IORef IntState
iSt = GInfo -> IORef IntState
intState GInfo
gInfo
  Maybe (DGraph, DGNodeLab, LibEnv)
lockedEnv <- GInfo -> NodeId -> DGraph -> IO (Maybe (DGraph, DGNodeLab, LibEnv))
ensureLockAtNode GInfo
gInfo NodeId
descr DGraph
dgraph
  case Maybe (DGraph, DGNodeLab, LibEnv)
lockedEnv of
    Nothing -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Just (dgraph' :: DGraph
dgraph', dgn' :: DGNodeLab
dgn', le' :: LibEnv
le') -> do
      Bool
acquired <- DGNodeLab -> IO Bool
tryLockLocal DGNodeLab
dgn'
      if Bool
acquired then do
        let action :: IO ()
action = do
              res :: Result G_theory
res@(Result d :: [Diagnosis]
d _) <- LogicGraph
-> LibName
-> DGraph
-> (NodeId, DGNodeLab)
-> LibEnv
-> IORef IntState
-> IO (Result G_theory)
basicInferenceNode LogicGraph
logicGraph LibName
ln DGraph
dgraph'
                                    (NodeId
descr, DGNodeLab
dgn') LibEnv
le' IORef IntState
iSt
              Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([Diagnosis] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Diagnosis]
d Bool -> Bool -> Bool
|| Diagnosis -> String
diagString ([Diagnosis] -> Diagnosis
forall a. [a] -> a
head [Diagnosis]
d) String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= "Proofs.Proofs: selection")
                (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ GInfo -> (NodeId, DGNodeLab) -> Result G_theory -> IO ()
runProveAtNode GInfo
gInfo (NodeId
descr, DGNodeLab
dgn') Result G_theory
res
        Bool
b <- DGNodeLab -> IO Bool
hidingWarnDiag DGNodeLab
dgn'
        Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
b IO ()
action
        DGNodeLab -> IO ()
unlockLocal DGNodeLab
dgn'
        else String -> String -> IO ()
errorDialog "Error" "Proofwindow already open"

runProveAtNode :: GInfo -> LNode DGNodeLab
               -> Result G_theory -> IO ()
runProveAtNode :: GInfo -> (NodeId, DGNodeLab) -> Result G_theory -> IO ()
runProveAtNode gInfo :: GInfo
gInfo (v :: NodeId
v, dgnode :: DGNodeLab
dgnode) (Result ds :: [Diagnosis]
ds mres :: Maybe G_theory
mres) = case Maybe G_theory
mres of
  Just newTh :: G_theory
newTh ->
    let oldTh :: G_theory
oldTh = DGNodeLab -> G_theory
dgn_theory DGNodeLab
dgnode
        rTh :: G_theory
rTh = G_theory -> G_theory -> G_theory
propagateProofs G_theory
oldTh G_theory
newTh in
    Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (G_theory
rTh G_theory -> G_theory -> Bool
forall a. Eq a => a -> a -> Bool
== G_theory
oldTh) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
      NodeId -> [Diagnosis] -> IO ()
showDiagMessAux 2 [Diagnosis]
ds
      GInfo -> IO ()
lockGlobal GInfo
gInfo
      let ln :: LibName
ln = GInfo -> LibName
libName GInfo
gInfo
          iSt :: IORef IntState
iSt = GInfo -> IORef IntState
intState GInfo
gInfo
      IntState
ost <- IORef IntState -> IO IntState
forall a. IORef a -> IO a
readIORef IORef IntState
iSt
      let (ost' :: IntState
ost', hist :: [DGChange]
hist) = LibName
-> IntState
-> (NodeId, DGNodeLab)
-> G_theory
-> (IntState, [DGChange])
updateNodeProof LibName
ln IntState
ost (NodeId
v, DGNodeLab
dgnode) G_theory
rTh
      case IntState -> Maybe IntIState
i_state IntState
ost' of
        Nothing -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        Just _ -> do
          IORef IntState -> IntState -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef IntState
iSt IntState
ost'
          GInfo -> IO () -> IO ()
runAndLock GInfo
gInfo (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ GInfo -> [DGChange] -> IO ()
updateGraph GInfo
gInfo [DGChange]
hist
      GInfo -> IO ()
unlockGlobal GInfo
gInfo
  _ -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

checkconservativityOfNode :: GInfo -> Int -> DGraph -> IO ()
checkconservativityOfNode :: GInfo -> NodeId -> DGraph -> IO ()
checkconservativityOfNode gInfo :: GInfo
gInfo descr :: NodeId
descr dgraph :: DGraph
dgraph = do
  let iSt :: IORef IntState
iSt = GInfo -> IORef IntState
intState GInfo
gInfo
      ln :: LibName
ln = GInfo -> LibName
libName GInfo
gInfo
      nlbl :: DGNodeLab
nlbl = DGraph -> NodeId -> DGNodeLab
labDG DGraph
dgraph NodeId
descr
  IntState
ost <- IORef IntState -> IO IntState
forall a. IORef a -> IO a
readIORef IORef IntState
iSt
  case IntState -> Maybe IntIState
i_state IntState
ost of
    Nothing -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Just iist :: IntIState
iist -> do
      Bool
b <- DGNodeLab -> IO Bool
hidingWarnDiag DGNodeLab
nlbl
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
b (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
        GInfo -> IO ()
lockGlobal GInfo
gInfo
        (str :: String
str, libEnv' :: LibEnv
libEnv', ph :: SizedList HistElem
ph) <- Bool
-> (NodeId, DGNodeLab)
-> LibEnv
-> LibName
-> IO (String, LibEnv, SizedList HistElem)
checkConservativityNode Bool
True (NodeId
descr, DGNodeLab
nlbl)
                                                      (IntIState -> LibEnv
i_libEnv IntIState
iist) LibName
ln
        if String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf "No conservativity" String
str then
          String -> String -> IO ()
errorDialog "Result of conservativity check" String
str
          else do
            String -> String -> IO ()
createTextDisplay "Result of conservativity check" String
str
            let nst :: IntState
nst = Command -> IntState -> [UndoRedoElem] -> IntState
add2history (SelectCmd -> String -> Command
SelectCmd SelectCmd
Node (String -> Command) -> String -> Command
forall a b. (a -> b) -> a -> b
$ NodeId -> String -> String
forall a. Pretty a => a -> String -> String
showDoc NodeId
descr "")
                      IntState
ost [LibName -> UndoRedoElem
DgCommandChange LibName
ln]
                nwst :: IntState
nwst = IntState
nst { i_state :: Maybe IntIState
i_state = IntIState -> Maybe IntIState
forall a. a -> Maybe a
Just (IntIState -> Maybe IntIState) -> IntIState -> Maybe IntIState
forall a b. (a -> b) -> a -> b
$ IntIState
iist { i_libEnv :: LibEnv
i_libEnv = LibEnv
libEnv' }}
            IORef IntState -> IntState -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef IntState
iSt IntState
nwst
            GInfo -> IO () -> IO ()
runAndLock GInfo
gInfo (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ GInfo -> [DGChange] -> IO ()
updateGraph GInfo
gInfo ([DGChange] -> [DGChange]
forall a. [a] -> [a]
reverse ([DGChange] -> [DGChange]) -> [DGChange] -> [DGChange]
forall a b. (a -> b) -> a -> b
$ SizedList HistElem -> [DGChange]
flatHistory SizedList HistElem
ph)
      GInfo -> IO ()
unlockGlobal GInfo
gInfo

edgeErr :: Int -> IO ()
edgeErr :: NodeId -> IO ()
edgeErr descr :: NodeId
descr = String -> String -> IO ()
errorDialog "Error" (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "edge with descriptor " String -> String -> String
forall a. [a] -> [a] -> [a]
++ NodeId -> String
forall a. Show a => a -> String
show NodeId
descr
                String -> String -> String
forall a. [a] -> [a] -> [a]
++ " 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 :: NodeId -> Maybe (LEdge DGLinkLab) -> IO ()
showEdgeInfo descr :: NodeId
descr me :: Maybe (LEdge DGLinkLab)
me = case Maybe (LEdge DGLinkLab)
me of
  Just e :: LEdge DGLinkLab
e@(_, _, l :: DGLinkLab
l) -> let estr :: String
estr = LEdge DGLinkLab -> String
showLEdge LEdge DGLinkLab
e in
    String -> String -> IO ()
createTextDisplay ("Info of " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
estr)
      (String
estr String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ DGLinkLab -> String -> String
forall a. Pretty a => a -> String -> String
showDoc DGLinkLab
l "")
  Nothing -> NodeId -> IO ()
edgeErr NodeId
descr

-- | check conservativity of the edge
checkconservativityOfEdge :: Int -> GInfo -> Maybe (LEdge DGLinkLab) -> IO ()
checkconservativityOfEdge :: NodeId -> GInfo -> Maybe (LEdge DGLinkLab) -> IO ()
checkconservativityOfEdge descr :: NodeId
descr gInfo :: GInfo
gInfo me :: Maybe (LEdge DGLinkLab)
me = case Maybe (LEdge DGLinkLab)
me of
    Nothing -> NodeId -> IO ()
edgeErr NodeId
descr
    Just lnk :: LEdge DGLinkLab
lnk@(_, _, lbl :: DGLinkLab
lbl) -> do
      let iSt :: IORef IntState
iSt = GInfo -> IORef IntState
intState GInfo
gInfo
          ln :: LibName
ln = GInfo -> LibName
libName GInfo
gInfo
      IntState
ost <- IORef IntState -> IO IntState
forall a. IORef a -> IO a
readIORef IORef IntState
iSt
      case IntState -> Maybe IntIState
i_state IntState
ost of
        Nothing -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        Just iist :: IntIState
iist -> do
          GInfo -> IO ()
lockGlobal GInfo
gInfo
          (str :: String
str, nwle :: LibEnv
nwle, _, ph :: SizedList HistElem
ph) <- Bool
-> LEdge DGLinkLab
-> LibEnv
-> LibName
-> IO (String, LibEnv, LEdge DGLinkLab, SizedList HistElem)
checkConservativityEdge Bool
True LEdge DGLinkLab
lnk
                                (IntIState -> LibEnv
i_libEnv IntIState
iist) LibName
ln
          if String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf "No conservativity" String
str
            then
              String -> String -> IO ()
errorDialog "Result of conservativity check" String
str
            else do
              String -> String -> IO ()
createTextDisplay "Result of conservativity check" String
str
              let nst :: IntState
nst = Command -> IntState -> [UndoRedoElem] -> IntState
add2history (SelectCmd -> String -> Command
SelectCmd SelectCmd
Link (String -> Command) -> String -> Command
forall a b. (a -> b) -> a -> b
$ EdgeId -> String -> String
forall a. Pretty a => a -> String -> String
showDoc (DGLinkLab -> EdgeId
dgl_id DGLinkLab
lbl) "")
                        IntState
ost [LibName -> UndoRedoElem
DgCommandChange LibName
ln]
                  nwst :: IntState
nwst = IntState
nst { i_state :: Maybe IntIState
i_state = IntIState -> Maybe IntIState
forall a. a -> Maybe a
Just (IntIState -> Maybe IntIState) -> IntIState -> Maybe IntIState
forall a b. (a -> b) -> a -> b
$ IntIState
iist { i_libEnv :: LibEnv
i_libEnv = LibEnv
nwle}}
              IORef IntState -> IntState -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef IntState
iSt IntState
nwst
              GInfo -> IO () -> IO ()
runAndLock GInfo
gInfo (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ GInfo -> [DGChange] -> IO ()
updateGraph GInfo
gInfo ([DGChange] -> IO ()) -> [DGChange] -> IO ()
forall a b. (a -> b) -> a -> b
$ [DGChange] -> [DGChange]
forall a. [a] -> [a]
reverse ([DGChange] -> [DGChange]) -> [DGChange] -> [DGChange]
forall a b. (a -> b) -> a -> b
$ SizedList HistElem -> [DGChange]
flatHistory SizedList HistElem
ph
          GInfo -> IO ()
unlockGlobal GInfo
gInfo

-- | show development graph for library
showDGraph :: GInfo -> LibName -> ConvFunc -> LibFunc -> IO ()
showDGraph :: GInfo -> LibName -> ConvFunc -> (GInfo -> IO ()) -> IO ()
showDGraph gi :: GInfo
gi ln :: LibName
ln convGraph :: ConvFunc
convGraph showLib :: GInfo -> IO ()
showLib = do
  HetcatsOpts -> NodeId -> String -> IO ()
putIfVerbose (GInfo -> HetcatsOpts
hetcatsOpts GInfo
gi) 3 (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "Converting graph for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ LibName -> String
forall a. Show a => a -> String
show LibName
ln
  Map LibName GInfo
og <- IORef (Map LibName GInfo) -> IO (Map LibName GInfo)
forall a. IORef a -> IO a
readIORef (IORef (Map LibName GInfo) -> IO (Map LibName GInfo))
-> IORef (Map LibName GInfo) -> IO (Map LibName GInfo)
forall a b. (a -> b) -> a -> b
$ GInfo -> IORef (Map LibName GInfo)
openGraphs GInfo
gi
  case LibName -> Map LibName GInfo -> Maybe GInfo
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup LibName
ln Map LibName GInfo
og of
    Nothing -> do
      GInfo -> (NodeId -> NodeId) -> IO ()
updateWindowCount GInfo
gi NodeId -> NodeId
forall a. Enum a => a -> a
succ
      GInfo
gi' <- GInfo -> LibName -> IO GInfo
copyGInfo GInfo
gi LibName
ln
      ConvFunc
convGraph GInfo
gi' "Hets Development Graph" GInfo -> IO ()
showLib
      GraphInfo -> String -> IO ()
GA.showTemporaryMessage (GInfo -> GraphInfo
graphInfo GInfo
gi') "Development Graph initialized."
    Just gi' :: GInfo
gi' ->
      GraphInfo -> String -> IO ()
GA.showTemporaryMessage (GInfo -> GraphInfo
graphInfo GInfo
gi') "Development Graph requested."

-- | show library referened by a DGRef node (=node drawn as a box)
showReferencedLibrary :: Int -> GInfo -> ConvFunc -> LibFunc -> IO ()
showReferencedLibrary :: NodeId -> GInfo -> ConvFunc -> (GInfo -> IO ()) -> IO ()
showReferencedLibrary descr :: NodeId
descr gInfo :: GInfo
gInfo convGraph :: ConvFunc
convGraph showLib :: GInfo -> IO ()
showLib = do
 IntState
ost <- IORef IntState -> IO IntState
forall a. IORef a -> IO a
readIORef (IORef IntState -> IO IntState) -> IORef IntState -> IO IntState
forall a b. (a -> b) -> a -> b
$ GInfo -> IORef IntState
intState GInfo
gInfo
 case IntState -> Maybe IntIState
i_state IntState
ost of
  Nothing -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  Just ist :: IntIState
ist -> do
   let le :: LibEnv
le = IntIState -> LibEnv
i_libEnv IntIState
ist
       ln :: LibName
ln = GInfo -> LibName
libName GInfo
gInfo
       refNode :: DGNodeLab
refNode = DGraph -> NodeId -> DGNodeLab
labDG (LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln LibEnv
le) NodeId
descr
       refLibname :: LibName
refLibname = if DGNodeLab -> Bool
isDGRef DGNodeLab
refNode then DGNodeLab -> LibName
dgn_libname DGNodeLab
refNode
                    else String -> LibName
forall a. HasCallStack => String -> a
error "showReferencedLibrary"
   case LibName -> LibEnv -> Maybe DGraph
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup LibName
refLibname LibEnv
le of
    Just _ -> GInfo -> LibName -> ConvFunc -> (GInfo -> IO ()) -> IO ()
showDGraph GInfo
gInfo LibName
refLibname ConvFunc
convGraph GInfo -> IO ()
showLib
    Nothing -> String -> String -> IO ()
errorDialog "Error"
      (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "The referenced library (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ LibName -> String
forall a. Show a => a -> String
show LibName
refLibname String -> String -> String
forall a. [a] -> [a] -> [a]
++ ") is unknown"

-- | display a window of translated graph with maximal sublogic.
translateGraph :: GInfo -> IO (Maybe LibEnv)
translateGraph :: GInfo -> IO (Maybe LibEnv)
translateGraph gInfo :: GInfo
gInfo@(GInfo { hetcatsOpts :: GInfo -> HetcatsOpts
hetcatsOpts = HetcatsOpts
opts }) = do
  IntState
ost <- IORef IntState -> IO IntState
forall a. IORef a -> IO a
readIORef (IORef IntState -> IO IntState) -> IORef IntState -> IO IntState
forall a b. (a -> b) -> a -> b
$ GInfo -> IORef IntState
intState GInfo
gInfo
  case IntState -> Maybe IntIState
i_state IntState
ost of
    Nothing -> Maybe LibEnv -> IO (Maybe LibEnv)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe LibEnv
forall a. Maybe a
Nothing
    Just ist :: IntIState
ist -> do
      let
        le :: LibEnv
le = IntIState -> LibEnv
i_libEnv IntIState
ist
        Result diagsSl :: [Diagnosis]
diagsSl mSublogic :: Maybe G_sublogics
mSublogic = LibEnv -> Result G_sublogics
getDGLogic LibEnv
le
        myErrMess :: [Diagnosis] -> IO ()
myErrMess = HetcatsOpts -> [Diagnosis] -> IO ()
showDiagMess HetcatsOpts
opts
        error' :: String -> IO ()
error' = String -> String -> IO ()
errorDialog "Error"
      if [Diagnosis] -> Bool
hasErrors [Diagnosis]
diagsSl then do
          [Diagnosis] -> IO ()
myErrMess [Diagnosis]
diagsSl
          Maybe LibEnv -> IO (Maybe LibEnv)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe LibEnv
forall a. Maybe a
Nothing
        else case Maybe G_sublogics
mSublogic of
          Nothing -> do
            String -> IO ()
error' "No maximal sublogic found."
            Maybe LibEnv -> IO (Maybe LibEnv)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe LibEnv
forall a. Maybe a
Nothing
          Just sublogic :: G_sublogics
sublogic -> do
            let paths :: [AnyComorphism]
paths = LogicGraph -> G_sublogics -> [AnyComorphism]
findComorphismPaths LogicGraph
logicGraph G_sublogics
sublogic
            if [AnyComorphism] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [AnyComorphism]
paths then do
                String -> IO ()
error' "This graph has no comorphism to translation."
                Maybe LibEnv -> IO (Maybe LibEnv)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe LibEnv
forall a. Maybe a
Nothing
              else do
                Maybe NodeId
sel <- String -> [String] -> IO (Maybe NodeId)
listBox "Choose a logic translation" ([String] -> IO (Maybe NodeId)) -> [String] -> IO (Maybe NodeId)
forall a b. (a -> b) -> a -> b
$ (AnyComorphism -> String) -> [AnyComorphism] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map AnyComorphism -> String
forall a. Show a => a -> String
show [AnyComorphism]
paths
                case Maybe NodeId
sel of
                  Nothing -> do
                    String -> IO ()
error' "no logic translation chosen"
                    Maybe LibEnv -> IO (Maybe LibEnv)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe LibEnv
forall a. Maybe a
Nothing
                  Just j :: NodeId
j -> do
                    let Result diag :: [Diagnosis]
diag mle :: Maybe LibEnv
mle = LibEnv -> AnyComorphism -> Result LibEnv
libEnv_translation LibEnv
le (AnyComorphism -> Result LibEnv) -> AnyComorphism -> Result LibEnv
forall a b. (a -> b) -> a -> b
$ [AnyComorphism]
paths [AnyComorphism] -> NodeId -> AnyComorphism
forall a. [a] -> NodeId -> a
!! NodeId
j
                    case Maybe LibEnv
mle of
                      Just newLibEnv :: LibEnv
newLibEnv -> do
                        HetcatsOpts -> [Diagnosis] -> IO ()
showDiagMess HetcatsOpts
opts ([Diagnosis] -> IO ()) -> [Diagnosis] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Diagnosis]
diagsSl [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++ [Diagnosis]
diag
                        Maybe LibEnv -> IO (Maybe LibEnv)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe LibEnv -> IO (Maybe LibEnv))
-> Maybe LibEnv -> IO (Maybe LibEnv)
forall a b. (a -> b) -> a -> b
$ LibEnv -> Maybe LibEnv
forall a. a -> Maybe a
Just LibEnv
newLibEnv
                      Nothing -> do
                        [Diagnosis] -> IO ()
myErrMess ([Diagnosis] -> IO ()) -> [Diagnosis] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Diagnosis]
diagsSl [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++ [Diagnosis]
diag
                        Maybe LibEnv -> IO (Maybe LibEnv)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe LibEnv
forall a. Maybe a
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
-> Map DGNodeType (Shape value, String)
-> Map DGEdgeType (EdgePattern EdgeValue, String)
-> IO ()
saveUDGraph gInfo :: GInfo
gInfo@(GInfo { graphInfo :: GInfo -> GraphInfo
graphInfo = GraphInfo
gi
                         , libName :: GInfo -> LibName
libName = LibName
ln }) nodemap :: Map DGNodeType (Shape value, String)
nodemap linkmap :: Map DGEdgeType (EdgePattern EdgeValue, String)
linkmap = do
  IntState
ost <- IORef IntState -> IO IntState
forall a. IORef a -> IO a
readIORef (IORef IntState -> IO IntState) -> IORef IntState -> IO IntState
forall a b. (a -> b) -> a -> b
$ GInfo -> IORef IntState
intState GInfo
gInfo
  case IntState -> Maybe IntIState
i_state IntState
ost of
   Nothing -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
   Just _ -> do
    Maybe String
maybeFilePath <- String
-> [(String, [String])]
-> Maybe (String -> IO ())
-> IO (Maybe String)
fileSaveDialog (LibName -> String
libNameToFile LibName
ln String -> String -> String
forall a. [a] -> [a] -> [a]
++ ".udg")
                                    [ ("uDrawGraph", ["*.udg"])
                                    , ("All Files", ["*"])] Maybe (String -> IO ())
forall a. Maybe a
Nothing
    case Maybe String
maybeFilePath of
     Just filepath :: String
filepath -> do
      GraphInfo -> String -> IO ()
GA.showTemporaryMessage GraphInfo
gi "Converting graph..."
      String
nstring <- GInfo
-> Map DGNodeType (Shape value, String)
-> Map DGEdgeType (EdgePattern EdgeValue, String)
-> IO String
forall value.
GInfo
-> Map DGNodeType (Shape value, String)
-> Map DGEdgeType (EdgePattern EdgeValue, String)
-> IO String
nodes2String GInfo
gInfo Map DGNodeType (Shape value, String)
nodemap Map DGEdgeType (EdgePattern EdgeValue, String)
linkmap
      String -> String -> IO ()
writeFile String
filepath String
nstring
      GraphInfo -> String -> IO ()
GA.showTemporaryMessage GraphInfo
gi (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "Graph stored to " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
filepath String -> String -> String
forall a. [a] -> [a] -> [a]
++ "!"
     Nothing -> GraphInfo -> String -> IO ()
GA.showTemporaryMessage GraphInfo
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
-> Map DGNodeType (Shape value, String)
-> Map DGEdgeType (EdgePattern EdgeValue, String)
-> IO String
nodes2String gInfo :: GInfo
gInfo@(GInfo { graphInfo :: GInfo -> GraphInfo
graphInfo = GraphInfo
gi
                          , libName :: GInfo -> LibName
libName = LibName
ln }) nodemap :: Map DGNodeType (Shape value, String)
nodemap linkmap :: Map DGEdgeType (EdgePattern EdgeValue, String)
linkmap = do
 IntState
ost <- IORef IntState -> IO IntState
forall a. IORef a -> IO a
readIORef (IORef IntState -> IO IntState) -> IORef IntState -> IO IntState
forall a b. (a -> b) -> a -> b
$ GInfo -> IORef IntState
intState GInfo
gInfo
 case IntState -> Maybe IntIState
i_state IntState
ost of
  Nothing -> String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return []
  Just ist :: IntIState
ist -> do
   let le :: LibEnv
le = IntIState -> LibEnv
i_libEnv IntIState
ist
   [(NodeId, DGNodeLab)]
nodes <- ((NodeId, DGNodeLab) -> IO Bool)
-> [(NodeId, DGNodeLab)] -> IO [(NodeId, DGNodeLab)]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM ((Bool -> Bool) -> IO Bool -> IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Bool -> Bool
not (IO Bool -> IO Bool)
-> ((NodeId, DGNodeLab) -> IO Bool)
-> (NodeId, DGNodeLab)
-> IO Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GraphInfo -> NodeId -> IO Bool
GA.isHiddenNode GraphInfo
gi (NodeId -> IO Bool)
-> ((NodeId, DGNodeLab) -> NodeId)
-> (NodeId, DGNodeLab)
-> IO Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NodeId, DGNodeLab) -> NodeId
forall a b. (a, b) -> a
fst)
                    ([(NodeId, DGNodeLab)] -> IO [(NodeId, DGNodeLab)])
-> [(NodeId, DGNodeLab)] -> IO [(NodeId, DGNodeLab)]
forall a b. (a -> b) -> a -> b
$ DGraph -> [(NodeId, DGNodeLab)]
labNodesDG (DGraph -> [(NodeId, DGNodeLab)])
-> DGraph -> [(NodeId, DGNodeLab)]
forall a b. (a -> b) -> a -> b
$ LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln LibEnv
le
   String
nstring <- (String -> (NodeId, DGNodeLab) -> IO String)
-> String -> [(NodeId, DGNodeLab)] -> IO String
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\ s :: String
s ->
                      (String -> String) -> IO String -> IO String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
s then String
s else String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ ",\n") String -> String -> String
forall a. [a] -> [a] -> [a]
++)
                        (IO String -> IO String)
-> ((NodeId, DGNodeLab) -> IO String)
-> (NodeId, DGNodeLab)
-> IO String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GInfo
-> Map DGNodeType (Shape value, String)
-> Map DGEdgeType (EdgePattern EdgeValue, String)
-> (NodeId, DGNodeLab)
-> IO String
forall value.
GInfo
-> Map DGNodeType (Shape value, String)
-> Map DGEdgeType (EdgePattern EdgeValue, String)
-> (NodeId, DGNodeLab)
-> IO String
node2String GInfo
gInfo Map DGNodeType (Shape value, String)
nodemap Map DGEdgeType (EdgePattern EdgeValue, String)
linkmap)
                    "" [(NodeId, DGNodeLab)]
nodes
   String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> IO String) -> String -> IO String
forall a b. (a -> b) -> a -> b
$ "[" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nstring String -> String -> String
forall a. [a] -> [a] -> [a]
++ "]"

-- | 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
-> Map DGNodeType (Shape value, String)
-> Map DGEdgeType (EdgePattern EdgeValue, String)
-> (NodeId, DGNodeLab)
-> IO String
node2String gInfo :: GInfo
gInfo nodemap :: Map DGNodeType (Shape value, String)
nodemap linkmap :: Map DGEdgeType (EdgePattern EdgeValue, String)
linkmap (nid :: NodeId
nid, dgnode :: DGNodeLab
dgnode) = do
  String
label <- GInfo -> DGNodeLab -> IO String
getNodeLabel GInfo
gInfo DGNodeLab
dgnode
  let ntype :: DGNodeType
ntype = DGNodeLab -> DGNodeType
getRealDGNodeType DGNodeLab
dgnode
  (shape :: Shape value
shape, color :: String
color) <- case DGNodeType
-> Map DGNodeType (Shape value, String)
-> Maybe (Shape value, String)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup DGNodeType
ntype Map DGNodeType (Shape value, String)
nodemap of
    Nothing -> String -> IO (Shape value, String)
forall a. HasCallStack => String -> a
error (String -> IO (Shape value, String))
-> String -> IO (Shape value, String)
forall a b. (a -> b) -> a -> b
$ "SaveGraph: can't lookup nodetype: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ DGNodeType -> String
forall a. Show a => a -> String
show DGNodeType
ntype
    Just (s :: Shape value
s, c :: String
c) -> (Shape value, String) -> IO (Shape value, String)
forall (m :: * -> *) a. Monad m => a -> m a
return (Shape value
s, String
c)
  let
    object :: String
object = "a(\"OBJECT\",\"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
label String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\"),"
    color' :: String
color' = "a(\"COLOR\",\"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
color String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\"),"
    shape' :: String
shape' = "a(\"_GO\",\"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower (Shape value -> String
forall a. Show a => a -> String
show Shape value
shape) String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\")"
  String
links <- GInfo
-> Map DGEdgeType (EdgePattern EdgeValue, String)
-> NodeId
-> IO String
links2String GInfo
gInfo Map DGEdgeType (EdgePattern EdgeValue, String)
linkmap NodeId
nid
  String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> IO String) -> String -> IO String
forall a b. (a -> b) -> a -> b
$ "l(\"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ NodeId -> String
forall a. Show a => a -> String
show NodeId
nid String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\",n(\"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ DGNodeType -> String
forall a. Show a => a -> String
show DGNodeType
ntype String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\","
           String -> String -> String
forall a. [a] -> [a] -> [a]
++ "[" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
object String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
color' String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
shape' String -> String -> String
forall a. [a] -> [a] -> [a]
++ "],"
           String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n  [" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
links String -> String -> String
forall a. [a] -> [a] -> [a]
++ "]))"

-- | Converts all links of a node to String representation
links2String :: GInfo -> Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String)
             -> Int -> IO String
links2String :: GInfo
-> Map DGEdgeType (EdgePattern EdgeValue, String)
-> NodeId
-> IO String
links2String gInfo :: GInfo
gInfo@(GInfo { graphInfo :: GInfo -> GraphInfo
graphInfo = GraphInfo
gi
                          , libName :: GInfo -> LibName
libName = LibName
ln }) linkmap :: Map DGEdgeType (EdgePattern EdgeValue, String)
linkmap nodeid :: NodeId
nodeid = do
 IntState
ost <- IORef IntState -> IO IntState
forall a. IORef a -> IO a
readIORef (IORef IntState -> IO IntState) -> IORef IntState -> IO IntState
forall a b. (a -> b) -> a -> b
$ GInfo -> IORef IntState
intState GInfo
gInfo
 case IntState -> Maybe IntIState
i_state IntState
ost of
  Nothing -> String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return []
  Just ist :: IntIState
ist -> do
   let le :: LibEnv
le = IntIState -> LibEnv
i_libEnv IntIState
ist
   [LEdge DGLinkLab]
edges <- (LEdge DGLinkLab -> IO Bool)
-> [LEdge DGLinkLab] -> IO [LEdge DGLinkLab]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (\ (src :: NodeId
src, _, edge :: DGLinkLab
edge) -> do
     let eid :: EdgeId
eid = DGLinkLab -> EdgeId
dgl_id DGLinkLab
edge
     Bool
b <- GraphInfo -> EdgeId -> IO Bool
GA.isHiddenEdge GraphInfo
gi EdgeId
eid
     Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> IO Bool) -> Bool -> IO Bool
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not Bool
b Bool -> Bool -> Bool
&& NodeId
src NodeId -> NodeId -> Bool
forall a. Eq a => a -> a -> Bool
== NodeId
nodeid)
       ([LEdge DGLinkLab] -> IO [LEdge DGLinkLab])
-> [LEdge DGLinkLab] -> IO [LEdge DGLinkLab]
forall a b. (a -> b) -> a -> b
$ DGraph -> [LEdge DGLinkLab]
labEdgesDG (DGraph -> [LEdge DGLinkLab]) -> DGraph -> [LEdge DGLinkLab]
forall a b. (a -> b) -> a -> b
$ LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln LibEnv
le
   (String -> LEdge DGLinkLab -> IO String)
-> String -> [LEdge DGLinkLab] -> IO String
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\ s :: String
s edge :: LEdge DGLinkLab
edge -> do
           String
s' <- Map DGEdgeType (EdgePattern EdgeValue, String)
-> LEdge DGLinkLab -> IO String
link2String Map DGEdgeType (EdgePattern EdgeValue, String)
linkmap LEdge DGLinkLab
edge
           String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> IO String) -> String -> IO String
forall a b. (a -> b) -> a -> b
$ (if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
s then "" else String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ ",\n") String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s') "" [LEdge DGLinkLab]
edges

-- | Converts a link to String representation
link2String :: Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String)
            -> LEdge DGLinkLab -> IO String
link2String :: Map DGEdgeType (EdgePattern EdgeValue, String)
-> LEdge DGLinkLab -> IO String
link2String linkmap :: Map DGEdgeType (EdgePattern EdgeValue, String)
linkmap (nodeid1 :: NodeId
nodeid1, nodeid2 :: NodeId
nodeid2, edge :: DGLinkLab
edge) = do
  let (EdgeId linkid :: NodeId
linkid) = DGLinkLab -> EdgeId
dgl_id DGLinkLab
edge
      ltype :: DGEdgeType
ltype = DGLinkLab -> DGEdgeType
getRealDGLinkType DGLinkLab
edge
  (line :: EdgePattern EdgeValue
line, color :: String
color) <- case DGEdgeType
-> Map DGEdgeType (EdgePattern EdgeValue, String)
-> Maybe (EdgePattern EdgeValue, String)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup DGEdgeType
ltype Map DGEdgeType (EdgePattern EdgeValue, String)
linkmap of
    Nothing -> String -> IO (EdgePattern EdgeValue, String)
forall a. HasCallStack => String -> a
error (String -> IO (EdgePattern EdgeValue, String))
-> String -> IO (EdgePattern EdgeValue, String)
forall a b. (a -> b) -> a -> b
$ "SaveGraph: can't lookup linktype: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ DGEdgeType -> String
forall a. Show a => a -> String
show DGEdgeType
ltype
    Just (l :: EdgePattern EdgeValue
l, c :: String
c) -> (EdgePattern EdgeValue, String)
-> IO (EdgePattern EdgeValue, String)
forall (m :: * -> *) a. Monad m => a -> m a
return (EdgePattern EdgeValue
l, String
c)
  let
    nm :: String
nm = "\"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ NodeId -> String
forall a. Show a => a -> String
show NodeId
linkid String -> String -> String
forall a. [a] -> [a] -> [a]
++ ":" String -> String -> String
forall a. [a] -> [a] -> [a]
++ NodeId -> String
forall a. Show a => a -> String
show NodeId
nodeid1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ "->"
             String -> String -> String
forall a. [a] -> [a] -> [a]
++ NodeId -> String
forall a. Show a => a -> String
show NodeId
nodeid2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\""
    color' :: String
color' = "a(\"EDGECOLOR\",\"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
color String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\"),"
    line' :: String
line' = "a(\"EDGEPATTERN\",\"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower (EdgePattern EdgeValue -> String
forall a. Show a => a -> String
show EdgePattern EdgeValue
line) String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\")"
  String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> IO String) -> String -> IO String
forall a b. (a -> b) -> a -> b
$ "l(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ ",e(\"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ DGEdgeType -> String
forall a. Show a => a -> String
show DGEdgeType
ltype String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\","
           String -> String -> String
forall a. [a] -> [a] -> [a]
++ "[" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
color' String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
line' String -> String -> String
forall a. [a] -> [a] -> [a]
++ "],"
           String -> String -> String
forall a. [a] -> [a] -> [a]
++ "r(\"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ NodeId -> String
forall a. Show a => a -> String
show NodeId
nodeid2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\")))"

-- | Returns the name of the Node
getNodeLabel :: GInfo -> DGNodeLab -> IO String
getNodeLabel :: GInfo -> DGNodeLab -> IO String
getNodeLabel (GInfo { options :: GInfo -> IORef Flags
options = IORef Flags
opts }) dgnode :: DGNodeLab
dgnode = do
  Flags
flags <- IORef Flags -> IO Flags
forall a. IORef a -> IO a
readIORef IORef Flags
opts
  String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> IO String) -> String -> IO String
forall a b. (a -> b) -> a -> b
$ if Flags -> Bool
flagHideNames Flags
flags Bool -> Bool -> Bool
&& DGNodeLab -> Bool
isInternalNode DGNodeLab
dgnode
           then "" else DGNodeLab -> String
getDGNodeName DGNodeLab
dgnode