Hets - the Heterogeneous Tool Set

Copyright(c) Till Mossakowski, Uni Bremen 2002-2006
LicenseGPLv2 or higher, see LICENSE.txt
Maintainertill@informatik.uni-bremen.de
Stabilityprovisional
Portabilitynon-portable(Logic)
Safe HaskellNone

Static.DevGraph

Contents

Description

Central datastructures for development graphs Follows Sect. IV:4.2 of the CASL Reference Manual.

We also provide functions for constructing and modifying development graphs. However note that these changes need to be propagated to the GUI if they also shall be visible in the displayed development graph.

Synopsis

types for structured specification analysis

basic types

data NodeSig

Node with signature in a DG

Constructors

NodeSig 

Fields

getNode :: Node
 
getSig :: G_sign
 

Instances

data MaybeNode

NodeSig or possibly the empty sig in a logic (but since we want to avoid lots of vsacuous nodes with empty sig, we do not assign a real node in the DG here)

Constructors

JustNode NodeSig 
EmptyNode AnyLogic 

Instances

getMaybeNodes :: MaybeNode -> Set Node

newtype Renamed

a wrapper for renamings with a trivial Ord instance

Constructors

Renamed RENAMING 

Instances

data MaybeRestricted

a wrapper for restrictions with a trivial Ord instance

Constructors

NoRestriction 
Restricted RESTRICTION 

Instances

data DGOrigin

Data type indicating the origin of nodes and edges in the input language This is not used in the DG calculus, only may be used in the future for reconstruction of input and management of change.

Constructors

DGEmpty 
DGBasic 
DGBasicSpec (Maybe G_basic_spec) G_sign (Set G_symbol) 
DGExtension 
DGLogicCoercion 
DGTranslation Renamed 
DGUnion 
DGRestriction MaybeRestricted (Set G_symbol) 
DGRevealTranslation 
DGFreeOrCofree FreeOrCofree 
DGLocal 
DGClosed 
DGLogicQual 
DGData 
DGFormalParams 
DGImports 
DGInst IRI 
DGFitSpec 
DGFitView IRI 
DGProof 
DGNormalForm Node 
DGintegratedSCC 
DGFlattening 
DGAlignment 
DGTest 

Instances

data DGNodeInfo

node content or reference to another library's node

Constructors

DGNode 

Fields

node_origin :: DGOrigin
 
node_cons_status :: ConsStatus
 
DGRef 

Fields

ref_libname :: LibName
 
ref_node :: Node
 

Instances

data DGNodeLab

node inscriptions in development graphs. Nothing entries indicate "not computed yet"

Constructors

DGNodeLab 

Fields

dgn_name :: NodeName
 
dgn_theory :: G_theory
 
globalTheory :: Maybe G_theory
 
labelHasHiding :: Bool
 
labelHasFree :: Bool
 
dgn_nf :: Maybe Node
 
dgn_sigma :: Maybe GMorphism
 
dgn_freenf :: Maybe Node
 
dgn_phi :: Maybe GMorphism
 
nodeInfo :: DGNodeInfo
 
nodeMod :: NodeMod
 
xnode :: Maybe XNode
 
dgn_lock :: Maybe (MVar ())
 
dgn_symbolpathlist :: G_symbolmap [SLinkPath]
 

Instances

isDGRef :: DGNodeLab -> Bool

sensWithKind :: (forall a. SenStatus a (AnyComorphism, BasicProof) -> Bool) -> G_theory -> [String]

hasSenKind :: (forall a. SenStatus a (AnyComorphism, BasicProof) -> Bool) -> DGNodeLab -> Bool

hasOpenGoals :: DGNodeLab -> Bool

test if a given node label has local open goals

isInternalNode :: DGNodeLab -> Bool

check if the node has an internal name

getNodeConsStatus :: DGNodeLab -> ConsStatus

getNodeCons :: DGNodeLab -> Conservativity

getNodeConservativity :: LNode DGNodeLab -> Conservativity

returns the Conservativity if the given node has one, otherwise none

hasOpenNodeConsStatus :: Bool -> DGNodeLab -> Bool

test if a node conservativity is open, return input for refs or nodes with normal forms

markNodeConsistency :: Conservativity -> String -> DGNodeLab -> DGNodeLab

markNodeConsistent :: String -> DGNodeLab -> DGNodeLab

markNodeInconsistent :: String -> DGNodeLab -> DGNodeLab

getRealDGNodeType :: DGNodeLab -> DGNodeType

creates a DGNodeType from a DGNodeLab

newtype Fitted

a wrapper for fitting morphisms with a trivial Eq instance

Constructors

Fitted [G_mapping] 

Instances

data DGLinkOrigin

Constructors

SeeTarget 
SeeSource 
TEST 
DGLinkVerif 
DGImpliesLink 
DGLinkExtension 
DGLinkTranslation 
DGLinkClosedLenv 
DGLinkImports 
DGLinkMorph IRI 
DGLinkInst IRI Fitted 
DGLinkInstArg IRI 
DGLinkView IRI Fitted 
DGLinkAlign IRI 
DGLinkFitView IRI 
DGLinkFitViewImp IRI 
DGLinkProof 
DGLinkFlatteningUnion 
DGLinkFlatteningRename 
DGLinkRefinement IRI 

Instances

data DGLinkType

Link types of development graphs, Sect. IV:4.2 of the CASL Reference Manual explains them in depth.

Constructors

ScopedLink Scope LinkKind ConsStatus 
HidingDefLink 
FreeOrCofreeDefLink FreeOrCofree MaybeNode 
HidingFreeOrCofreeThm (Maybe FreeOrCofree) Node GMorphism ThmLinkStatus 

Instances

thmLinkStatus :: DGLinkType -> Maybe ThmLinkStatus

extract theorem link status from link type

thmProofBasis :: DGLinkType -> ProofBasis

extract proof basis from link type

updThmProofBasis :: DGLinkType -> ProofBasis -> DGLinkType

data DGLinkLab

link inscriptions in development graphs

Constructors

DGLink 

Fields

dgl_morphism :: GMorphism
 
dgl_type :: DGLinkType
 
dgl_origin :: DGLinkOrigin
 
dglPending :: Bool
 
dgl_id :: EdgeId
 
dglName :: String
 

Instances

mkDGLink :: GMorphism -> DGLinkType -> DGLinkOrigin -> String -> EdgeId -> DGLinkLab

nameDGLink :: String -> DGLinkLab -> DGLinkLab

name a link

defDGLink :: GMorphism -> DGLinkType -> DGLinkOrigin -> DGLinkLab

defDGLinkId :: GMorphism -> DGLinkType -> DGLinkOrigin -> EdgeId -> DGLinkLab

globDefLink :: GMorphism -> DGLinkOrigin -> DGLinkLab

getDGLinkType :: DGLinkLab -> String

describe the link type of the label

getHomEdgeType :: Bool -> Bool -> DGLinkType -> DGEdgeTypeModInc

getRealDGLinkType :: DGLinkLab -> DGEdgeType

creates a DGEdgeType from a DGLinkLab

getProofBasis :: DGLinkLab -> ProofBasis

return the proof basis of the given linklab

setProof :: ThmLinkStatus -> DGLinkType -> DGLinkType

set proof for theorem links

methods to check the type of an edge

isProven :: DGLinkType -> Bool

isGlobalEdge :: DGLinkType -> Bool

isGlobalThm :: DGLinkType -> Bool

isUnprovenGlobalThm :: DGLinkType -> Bool

isLocalThm :: DGLinkType -> Bool

isUnprovenLocalThm :: DGLinkType -> Bool

isUnprovenHidingThm :: DGLinkType -> Bool

isFreeEdge :: DGLinkType -> Bool

isCofreeEdge :: DGLinkType -> Bool

types for global environments

data GenSig

import, formal parameters and united signature of formal params

Constructors

GenSig MaybeNode [NodeSig] MaybeNode 

Instances

getGenSigNodes :: GenSig -> Set Node

data ExtGenSig

genericity and body

Constructors

ExtGenSig 

Fields

genericity :: GenSig
 
extGenBody :: NodeSig
 

Instances

getExtGenSigNodes :: ExtGenSig -> Set Node

data ExtViewSig

source, morphism, parameterized target

Constructors

ExtViewSig NodeSig GMorphism ExtGenSig 

Instances

getExtViewSigNodes :: ExtViewSig -> Set Node

types for architectural and unit specification analysis (as defined for basic static semantics in Chap. III:5.1)

data UnitSig

Constructors

UnitSig [NodeSig] NodeSig (Maybe NodeSig) 

Instances

getUnitSigNodes :: UnitSig -> Set Node

data ImpUnitSigOrSig

Constructors

ImpUnitSig MaybeNode UnitSig 
Sig NodeSig 

Instances

type StUnitCtx = Map IRI ImpUnitSigOrSig

emptyStUnitCtx :: StUnitCtx

type RefSigMap = Map IRI RefSig

getSigMapNodes :: RefSigMap -> Set Node

type BStContext = Map IRI RefSig

getBStContextNodes :: BStContext -> Set Node

data RefSig

Constructors

BranchRefSig RTPointer (UnitSig, Maybe BranchSig) 
ComponentRefSig RTPointer RefSigMap 

Instances

getRefSigNodes :: RefSig -> Set Node

getPointerFromRef :: RefSig -> RTPointer

setPointerInRef :: RefSig -> RTPointer -> RefSig

setUnitSigInRef :: RefSig -> UnitSig -> RefSig

getUnitSigFromRef :: RefSig -> Result UnitSig

mkRefSigFromUnit :: UnitSig -> RefSig

mkBotSigFromUnit :: UnitSig -> RefSig

data BranchSig

Constructors

UnitSigAsBranchSig UnitSig 
BranchStaticContext BStContext 

Instances

getBranchSigNodes :: BranchSig -> Set Node

type RefStUnitCtx = Map IRI RefSig

emptyRefStUnitCtx :: RefStUnitCtx

matchesContext :: RefSigMap -> BStContext -> Bool

equalSigs :: UnitSig -> UnitSig -> Bool

namesMatchCtx :: [IRI] -> BStContext -> RefSigMap -> Bool

modifyCtx :: [IRI] -> RefSigMap -> BStContext -> BStContext

refSigComposition :: RefSig -> RefSig -> Result RefSig

data GlobalEntry

an entry of the global environment

Constructors

SpecEntry ExtGenSig 
ViewOrStructEntry Bool ExtViewSig 
ArchOrRefEntry Bool RefSig 
AlignEntry AlignSig 
UnitEntry UnitSig 

Instances

getGlobEntryNodes :: GlobalEntry -> Set Node

data AlignSig

Constructors

AlignMor NodeSig GMorphism NodeSig 
AlignSpan NodeSig GMorphism NodeSig GMorphism NodeSig 
WAlign NodeSig GMorphism GMorphism NodeSig GMorphism GMorphism NodeSig NodeSig NodeSig 

Instances

type GlobalEnv = Map IRI GlobalEntry

getGlobNodes :: GlobalEnv -> Set Node

change and history types

data DGChange

the edit operations of the DGraph

Constructors

InsertNode (LNode DGNodeLab) 
DeleteNode (LNode DGNodeLab) 
InsertEdge (LEdge DGLinkLab) 
DeleteEdge (LEdge DGLinkLab) 
SetNodeLab DGNodeLab (LNode DGNodeLab) 

Instances

data HistElem

Constructors

HistElem DGChange 
HistGroup DGRule ProofHistory 

Instances

type ProofHistory = SizedList HistElem

data RTNodeType

Constructors

RTPlain UnitSig 
RTRef Node 

Instances

data RTNodeLab

Constructors

RTNodeLab 

Fields

rtn_type :: RTNodeType
 
rtn_name :: String
 
rtn_diag :: String
 

Instances

data RTLinkType

Constructors

RTRefine 
RTComp 

Instances

data RTLinkLab

Constructors

RTLink 

Fields

rtl_type :: RTLinkType
 

Instances

addNodeRT :: DGraph -> UnitSig -> String -> (Node, DGraph)

addSpecNodeRT :: DGraph -> UnitSig -> String -> (Node, DGraph)

updateNodeNameRT :: DGraph -> Node -> Bool -> String -> DGraph

updateSigRT :: DGraph -> Node -> UnitSig -> DGraph

updateNodeNameSpecRT :: DGraph -> Node -> String -> DGraph

addSubTree :: DGraph -> Maybe RTLeaves -> RTPointer -> (DGraph, RTPointer)

copySubTree :: DGraph -> Node -> Maybe Node -> (DGraph, Map Node Node)

copySubTreeN :: DGraph -> [Node] -> Map Node Node -> (DGraph, Map Node Node)

copyNode :: Node -> (DGraph, Map Node Node) -> LNode RTLinkLab -> (DGraph, Map Node Node)

addRefEdgeRT :: DGraph -> Node -> Node -> DGraph

addEdgesToNodeRT :: DGraph -> [Node] -> Node -> DGraph

data DiagNodeLab

Constructors

DiagNode 

Fields

dn_sig :: NodeSig
 
dn_desc :: String
 

Instances

data DiagLinkLab

Constructors

DiagLink 

Fields

dl_morphism :: GMorphism
 
dl_number :: Int
 

Instances

data Diag

Constructors

Diagram 

Fields

diagGraph :: Gr DiagNodeLab DiagLinkLab
 
numberOfEdges :: Int
 

Instances

data DGraph

the actual development graph with auxiliary information. A G_sign should be stored in sigMap under its gSignSelfIdx. The same applies to G_morphism with morMap and gMorphismSelfIdx resp. G_theory with thMap and gTheorySelfIdx.

Constructors

DGraph 

Fields

globalAnnos :: GlobalAnnos

global annos of library

optLibDefn :: Maybe LIB_DEFN
 
globalEnv :: GlobalEnv

name entities (specs, views) of a library

dgBody :: Gr DGNodeLab DGLinkLab

actual DGraph tree

currentBaseTheory :: Maybe NodeSig
 
refTree :: Gr RTNodeLab RTLinkLab

the refinement tree

specRoots :: Map String Node

root nodes for named specs

nameMap :: MapSet String Node

all nodes by name

archSpecDiags :: Map String Diag

dependency diagrams between units

getNewEdgeId :: EdgeId

edge counter

allRefNodes :: Map (LibName, Node) Node

all DGRef's

sigMap :: Map SigId G_sign

signature map

thMap :: Map ThId G_theory

theory map

morMap :: Map MorId G_morphism

morphism map

proofHistory :: ProofHistory

applied proof steps

redoHistory :: ProofHistory

undone proofs steps

Instances

emptyDG :: DGraph

type LibEnv = Map LibName DGraph

emptyLibEnv :: LibEnv

an empty environment

utility functions

for node signatures

emptyG_sign :: AnyLogic -> G_sign

getMaybeSig :: MaybeNode -> G_sign

getLogic :: MaybeNode -> AnyLogic

getNodeLogic :: NodeSig -> AnyLogic

accessing node label

dgn_origin :: DGNodeLab -> DGOrigin

get the origin of a non-reference node (partial)

dgn_libname :: DGNodeLab -> LibName

get the referenced library (partial)

dgn_node :: DGNodeLab -> Node

get the referenced node (partial)

dgn_sign :: DGNodeLab -> G_sign

get the signature of a node's theory (total)

getDGNodeName :: DGNodeLab -> String

gets the name of a development graph node as a string (total)

globOrLocTh :: DGNodeLab -> G_theory

get the global theory of a node or the local one if missing

creating node content and label

newConsNodeInfo :: DGOrigin -> Conservativity -> DGNodeInfo

create node info

newNodeInfo :: DGOrigin -> DGNodeInfo

create default content

newRefInfo :: LibName -> Node -> DGNodeInfo

create a reference node part

newInfoNodeLab :: NodeName -> DGNodeInfo -> G_theory -> DGNodeLab

create a new node label

newNodeLab :: NodeName -> DGOrigin -> G_theory -> DGNodeLab

create a new node label using newNodeInfo and newInfoNodeLab

handle the lock of a node

treatNodeLock :: (MVar () -> a) -> DGNodeLab -> a

wrapper to access the maybe lock

tryLockLocal :: DGNodeLab -> IO Bool

Tries to acquire the local lock. Return False if already acquired.

unlockLocal :: DGNodeLab -> IO ()

Releases the local lock.

hasLock :: DGNodeLab -> Bool

checks if locking MVar is initialized

edge label equalities

eqDGLinkLabContent :: DGLinkLab -> DGLinkLab -> Bool

equality without comparing the edge ids

eqDGLinkLabById :: DGLinkLab -> DGLinkLab -> Bool

equality comparing ids only

setting index maps

cpIndexMaps :: DGraph -> DGraph -> DGraph

setSigMapDG :: Map SigId G_sign -> DGraph -> DGraph

setThMapDG :: Map ThId G_theory -> DGraph -> DGraph

setMorMapDG :: Map MorId G_morphism -> DGraph -> DGraph

looking up in index maps

lookupSigMapDG :: SigId -> DGraph -> Maybe G_sign

lookupThMapDG :: ThId -> DGraph -> Maybe G_theory

lookupMorMapDG :: MorId -> DGraph -> Maybe G_morphism

getting index maps and their maximal index

sigMapI :: DGraph -> (Map SigId G_sign, SigId)

thMapI :: DGraph -> (Map ThId G_theory, ThId)

morMapI :: DGraph -> (Map MorId G_morphism, MorId)

lookup other graph parts

lookupGlobalEnvDG :: IRI -> DGraph -> Maybe GlobalEntry

lookupInAllRefNodesDG :: DGNodeInfo -> DGraph -> Maybe Node

lookup a reference node for a given libname and node

lookup nodes by their names or other properties

lookupNodeByName :: String -> DGraph -> [LNode DGNodeLab]

lookup a node in the graph by its name, using showName to convert nodenames.

lookupUniqueNodeByName :: String -> DGraph -> Maybe (LNode DGNodeLab)

filterLocalNodesByName :: String -> DGraph -> [LNode DGNodeLab]

filters all local nodes in the graph by their names, using showName to convert nodenames. See also lookupNodeByName.

filterRefNodesByName :: String -> LibName -> DGraph -> [LNode DGNodeLab]

filter all ref nodes in the graph by their names, using showName to convert nodenames. See also lookupNodeByName.

lookupLocalNodeByNameInEnv :: LibEnv -> String -> Maybe (DGraph, LNode DGNodeLab)

Given a LibEnv we search each DGraph in it for a (maybe referenced) node with the given name. We return the labeled node and the Graph where this node resides as local node. See also lookupLocalNode.

lookupLocalNodeByName :: LibEnv -> DGraph -> String -> Maybe (DGraph, LNode DGNodeLab)

We search only the given DGraph for a (maybe referenced) node with the given name. We return the labeled node and the Graph where this node resides as local node. See also lookupLocalNode.

lookupLocalNode :: LibEnv -> DGraph -> Node -> (DGraph, LNode DGNodeLab)

Given a Node and a DGraph we follow the node to the graph where it is defined as a local node.

lookupRefNode :: LibEnv -> LibName -> DGraph -> Node -> (LibName, DGraph, LNode DGNodeLab)

Given a Node and a DGraph we follow the node to the graph where it is defined .

lookupRefNodeM :: LibEnv -> Maybe LibName -> DGraph -> Node -> (Maybe LibName, DGraph, LNode DGNodeLab)

accessing the actual graph

getNewNodeDG :: DGraph -> Node

get the next available node id

labNodesDG :: DGraph -> [LNode DGNodeLab]

get all the nodes

labEdgesDG :: DGraph -> [LEdge DGLinkLab]

get all the edges

isEmptyDG :: DGraph -> Bool

checks if a DG is empty or not.

gelemDG :: Node -> DGraph -> Bool

checks if a given node belongs to a given DG

innDG :: DGraph -> Node -> [LEdge DGLinkLab]

get all the incoming ledges of the given node in a given DG

outDG :: DGraph -> Node -> [LEdge DGLinkLab]

get all the outgoing ledges of the given node in a given DG

nodesDG :: DGraph -> [Node]

get all the nodes of the given DG

labDG :: DGraph -> Node -> DGNodeLab

tries to get the label of the given node in a given DG

labRT :: DGraph -> Node -> RTNodeLab

tries to get the label of the given node in a given RT

getNameOfNode :: Node -> DGraph -> String

get the name of a node from the number of node

newNodesDG :: Int -> DGraph -> [Node]

gets the given number of new node-ids in a given DG.

safeContextDG :: String -> DGraph -> Node -> Context DGNodeLab DGLinkLab

get the context and throw input string as error message

manipulate graph

labelNodeDG :: LNode DGNodeLab -> DGraph -> (DGraph, DGNodeLab)

sets the node with new label and returns the new graph and the old label

delNodeDG :: Node -> DGraph -> DGraph

delete the node out of the given DG

delNodesDG :: [Node] -> DGraph -> DGraph

delete a list of nodes out of the given DG

insNodeDG :: LNode DGNodeLab -> DGraph -> DGraph

insert a new node into given DGraph

insLNodeDG :: LNode DGNodeLab -> DGraph -> DGraph

inserts a lnode into a given DG

insNodesDG :: [LNode DGNodeLab] -> DGraph -> DGraph

insert a new node with the given node content into a given DGraph

delLEdgeDG :: LEdge DGLinkLab -> DGraph -> DGraph

delete a labeled edge out of the given DG

insInclEdgeDG :: LogicGraph -> DGraph -> NodeSig -> NodeSig -> Result DGraph

inserts an edge between two nodes, labelled with inclusion

insLEdgeDG :: LEdge DGLinkLab -> DGraph -> (LEdge DGLinkLab, DGraph)

insert a labeled edge into a given DG, return possibly new id of edge

compareLinks :: DGLinkLab -> DGLinkLab -> Ordering

insLEdgeNubDG :: LEdge DGLinkLab -> DGraph -> DGraph

tries to insert a labeled edge into a given DG, but if this edge already exists, then does nothing.

insEdgeAsIs :: LEdge DGLinkLab -> DGraph -> DGraph

inserts a new edge into the DGraph using it's own edgeId. ATTENTION: the caller must ensure that an edgeId is not used twice

insEdgesDG :: [LEdge DGLinkLab] -> DGraph -> DGraph

insert a list of labeled edge into a given DG

mkGraphDG :: [LNode DGNodeLab] -> [LEdge DGLinkLab] -> DGraph -> DGraph

merge a list of lnodes and ledges into a given DG

getDGLinksById :: EdgeId -> DGraph -> [LEdge DGLinkLab]

get links by id (inefficiently)

lookupUniqueLink :: Monad m => Node -> EdgeId -> DGraph -> m (LEdge DGLinkLab)

find a unique link given its source node and edgeId

top-level functions

initLocking :: DGraph -> LNode DGNodeLab -> IO (DGraph, DGNodeLab)

initializes the MVar for locking if nessesary

lookupDGraph :: LibName -> LibEnv -> DGraph

returns the DGraph that belongs to the given library name

computeLocalTheory :: Monad m => LibEnv -> LibName -> Node -> m G_theory

compute the theory of a given node. If this node is a DGRef, the referenced node is looked up first.

computeLocalNodeTheory :: Monad m => LibEnv -> DGraph -> Node -> m G_theory

computeLocalLabelTheory :: Monad m => LibEnv -> DGNodeLab -> m G_theory

test link types

liftE :: (DGLinkType -> a) -> LEdge DGLinkLab -> a

isGlobalDef :: DGLinkType -> Bool

isLocalDef :: DGLinkType -> Bool

isHidingDef :: DGLinkType -> Bool

isDefEdge :: DGLinkType -> Bool

isLocalEdge :: DGLinkType -> Bool

isHidingEdge :: DGLinkType -> Bool

create link types

hidingThm :: Node -> GMorphism -> DGLinkType

globalThm :: DGLinkType

localThm :: DGLinkType

globalConsThm :: Conservativity -> DGLinkType

localConsThm :: Conservativity -> DGLinkType

localOrGlobalThm :: Scope -> Conservativity -> DGLinkType

localOrGlobalDef :: Scope -> Conservativity -> DGLinkType

globalConsDef :: Conservativity -> DGLinkType

globalDef :: DGLinkType

localDef :: DGLinkType

link conservativity

getLinkConsStatus :: DGLinkType -> ConsStatus

getEdgeConsStatus :: DGLinkLab -> ConsStatus

getCons :: DGLinkType -> Conservativity

getConservativity :: LEdge DGLinkLab -> Conservativity

returns the Conservativity if the given edge has one, otherwise none

getConservativityOfPath :: [LEdge DGLinkLab] -> Conservativity

returns the conservativity of the given path

bottom up traversal

getLibDepRel :: LibEnv -> Rel LibName

Creates a LibName relation wrt dependencies via reference nodes

getTopsortedLibs :: LibEnv -> [LibName]

dependentLibs :: LibName -> LibEnv -> [LibName]

Get imported libs in topological order, i.e. lib(s) without imports first. The input lib-name will be last

topsortedNodes :: DGraph -> [LNode DGNodeLab]

changedPendingEdges :: DGraph -> [LEdge DGLinkLab]

changedLocalTheorems :: DGraph -> LNode DGNodeLab -> [LEdge DGLinkLab]

duplicateDefEdges :: DGraph -> [Edge]