```{- |
Module      :  ./Proofs/EdgeUtils.hs
Description :  utility functions for edges of development graphs
Copyright   :  (c) Jorina F. Gerken, Till Mossakowski, Uni Bremen 2002-2006

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  non-portable(Logic)

utility functions for edges of development graphs
-}

module Proofs.EdgeUtils where

import Logic.Grothendieck
import Logic.Logic

import Static.DevGraph
import Static.DgUtils
import Static.History

import Common.Consistency
import Common.Result
import qualified Common.Lib.Rel as Rel
import qualified Common.Lib.Graph as Tree

import Data.Graph.Inductive.Graph
import Data.Graph.Inductive.Basic (elfilter)
import Data.List
import Data.Maybe (isNothing)
import qualified Data.Set as Set
import qualified Data.Map as Map
import Control.Exception (assert)

-- * other methods on edges

f (v :: Node
v, w :: Node
l) (v2 :: Node
v2, w2 :: Node
l2) = Node
v Node -> Node -> Bool
forall a. Eq a => a -> a -> Bool
== Node
v2 Bool -> Bool -> Bool
&& Node
w Node -> Node -> Bool
forall a. Eq a => a -> a -> Bool
== Node
w2 Bool -> Bool -> Bool
l2

l of
e2] -> Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
e2
_ -> Bool
True

{- | try to get the given edge from the given DGraph or the given list of
DGChange to advoid duplicate inserting of an edge. -}
tryToGetEdge (src :: Node
src, tgt :: Node
lb) dgraph :: DGraph
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
l -> (Node
src, Node
l))
forall a b. (a -> b) -> a -> b
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
forall a b. (a -> b) -> a -> b
forall a b. Node -> Node -> Gr a b -> [b]
Tree.getLEdges Node
src Node
forall a b. (a -> b) -> a -> b
\$ DGraph -> Gr DGNodeLab DGLinkLab
dgBody DGraph
dgraph

{- | try to insert an edge into the given dgraph, if the edge exists, the
edge's id should match, too. -}
insertDGLEdge :: LEdge DGLinkLab -> DGraph -> DGraph
insertDGLEdge :: LEdge DGLinkLab -> DGraph -> DGraph
edge dgraph :: DGraph
dgraph =
edge DGraph
dgraph of
Nothing -> DGraph -> DGChange -> DGraph
changeDGH DGraph
dgraph (DGChange -> DGraph) -> DGChange -> DGraph
forall a b. (a -> b) -> a -> b
edge
Just _ -> DGraph
dgraph

-- | get the edge id out of a given edge
getEdgeId :: LEdge DGLinkLab -> EdgeId
getEdgeId :: LEdge DGLinkLab -> EdgeId
getEdgeId (_, _, label :: DGLinkLab
label

-- * methods that calculate paths of certain types

getAllPathsOfTypeFromGoalList :: DGraph -> (DGLinkType -> Bool)
getAllPathsOfTypeFromGoalList :: DGraph
getAllPathsOfTypeFromGoalList dgraph :: DGraph
dgraph isType :: DGLinkType -> Bool
ls = let
sources :: [Node]
sources = Set Node -> [Node]
forall a. Set a -> [a]
Set.toList (Set Node -> [Node]) -> Set Node -> [Node]
forall a b. (a -> b) -> a -> b
\$ [Node] -> Set Node
forall a. Ord a => [a] -> Set a
Set.fromList ([Node] -> Set Node) -> [Node] -> Set Node
forall a b. (a -> b) -> a -> b
forall a b. (a -> b) -> [a] -> [b]
map (\ (s :: Node
s, _, _) -> Node
ls
targets :: [Node]
targets = Set Node -> [Node]
forall a. Set a -> [a]
Set.toList (Set Node -> [Node]) -> Set Node -> [Node]
forall a b. (a -> b) -> a -> b
\$ [Node] -> Set Node
forall a. Ord a => [a] -> Set a
Set.fromList ([Node] -> Set Node) -> [Node] -> Set Node
forall a b. (a -> b) -> a -> b
forall a b. (a -> b) -> [a] -> [b]
map (\ (_, t :: Node
t, _) -> Node
ls
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ source :: Node
source ->
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (DGraph
getAllPathsOfTypeBetween DGraph
isType Node
source) [Node]
targets)
[Node]
sources

{- | returns all paths consisting of edges of the given type in the given
development graph -}
getAllPathsOfType dgraph :: DGraph
dgraph isType :: DGLinkType -> Bool
isType =
DGraph
getAllPathsOfTypeFromGoalList DGraph
forall a b. (a -> b) -> a -> b
labEdgesDG DGraph
dgraph

-- | morphisms of (co)free definitions are identities
realMorphism :: DGLinkLab -> Maybe GMorphism
realMorphism :: DGLinkLab -> Maybe GMorphism
lbl = let mor :: GMorphism
lbl of
ScopedLink {} -> GMorphism -> Maybe GMorphism
forall (m :: * -> *) a. Monad m => a -> m a
return GMorphism
mor
HidingDefLink -> String -> Maybe GMorphism
forall (m :: * -> *) a. MonadFail m => String -> m a
FreeOrCofreeDefLink _ _ -> GMorphism -> Maybe GMorphism
forall (m :: * -> *) a. Monad m => a -> m a
return (GMorphism -> Maybe GMorphism) -> GMorphism -> Maybe GMorphism
forall a b. (a -> b) -> a -> b
\$ G_sign -> GMorphism
forall object morphism.
Category object morphism =>
object -> morphism
ide (G_sign -> GMorphism) -> G_sign -> GMorphism
forall a b. (a -> b) -> a -> b
\$ GMorphism -> G_sign
forall object morphism.
Category object morphism =>
morphism -> object
cod GMorphism
mor
HidingFreeOrCofreeThm {} -> String -> Maybe GMorphism
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "hiding or free thm link"

-- | determines the morphism of a given path
calculateMorphismOfPath :: [LEdge DGLinkLab] -> Maybe GMorphism
calculateMorphismOfPath :: [LEdge DGLinkLab] -> Maybe GMorphism
p of
lbl) : r :: [LEdge DGLinkLab]
r -> do
GMorphism
morphism <- DGLinkLab -> Maybe GMorphism
lbl
forall (t :: * -> *) a. Foldable t => t a -> Bool
r then GMorphism -> Maybe GMorphism
forall (m :: * -> *) a. Monad m => a -> m a
return GMorphism
morphism else do
GMorphism
rmor <- [LEdge DGLinkLab] -> Maybe GMorphism
r
Result GMorphism -> Maybe GMorphism
forall a. Result a -> Maybe a
resultToMaybe (Result GMorphism -> Maybe GMorphism)
-> Result GMorphism -> Maybe GMorphism
forall a b. (a -> b) -> a -> b
\$ GMorphism -> GMorphism -> Result GMorphism
forall object morphism.
Category object morphism =>
morphism -> morphism -> Result morphism
composeMorphisms GMorphism
morphism GMorphism
rmor
[] -> String -> Maybe GMorphism
forall a. HasCallStack => String -> a
error "calculateMorphismOfPath"

{- | returns all paths from the given list whose morphism is equal to the
given one -}
filterPathsByMorphism :: GMorphism -> [[LEdge DGLinkLab]]
filterPathsByMorphism morphism :: GMorphism
morphism =
forall a. (a -> Bool) -> [a] -> [a]
filter ((Maybe GMorphism -> Maybe GMorphism -> Bool
forall a. Eq a => a -> a -> Bool
== GMorphism -> Maybe GMorphism
forall a. a -> Maybe a
Just GMorphism
morphism) (Maybe GMorphism -> Bool)
-> ([LEdge DGLinkLab] -> Maybe GMorphism)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [LEdge DGLinkLab] -> Maybe GMorphism
calculateMorphismOfPath)

{- | returns all paths consisting of global edges only
or of one local edge followed by any number of global edges -}
getAllLocGlobPathsBetween :: DGraph -> Node -> Node -> [[LEdge DGLinkLab]]
getAllLocGlobPathsBetween :: DGraph -> Node -> Node -> [[LEdge DGLinkLab]]
getAllLocGlobPathsBetween dgraph :: DGraph
dgraph src :: Node
src tgt :: Node
tgt = let
outEdges = DGraph -> Node -> [LEdge DGLinkLab]
outDG DGraph
dgraph Node
src
forall a. (a -> Bool) -> [a] -> [a]
outEdges
locGlobPaths =
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ edge :: LEdge DGLinkLab
edge@(_, node :: Node
forall a b. (a -> b) -> [a] -> [b]
forall a. a -> [a] -> [a]
:)
forall a b. (a -> b) -> a -> b
\$ DGraph -> Node -> Node -> [[LEdge DGLinkLab]]
getAllGlobPathsBetween DGraph
dgraph Node
node Node
locEdges
globPaths = DGraph -> Node -> Node -> [[LEdge DGLinkLab]]
getAllGlobPathsBetween DGraph
dgraph Node
src Node
tgt
forall a. [a] -> [a] -> [a]
globPaths

{- | returns all paths of globalDef edges or globalThm edges
between the given source and target node -}
getAllGlobPathsBetween :: DGraph -> Node -> Node -> [[LEdge DGLinkLab]]
getAllGlobPathsBetween :: DGraph -> Node -> Node -> [[LEdge DGLinkLab]]
getAllGlobPathsBetween dgraph :: DGraph
dgraph = DGraph
getAllPathsOfTypeBetween DGraph
isGlobalEdge

{- | returns all cyclic paths consisting of edges of the given type between the
given two nodes -}
getAllPathsOfTypeBetween :: DGraph -> (DGLinkType -> Bool) -> Node
getAllPathsOfTypeBetween :: DGraph
getAllPathsOfTypeBetween dgraph :: DGraph
dgraph isType :: DGLinkType -> Bool
isType src :: Node
src tgt :: Node
tgt =
forall a b. Node -> Node -> Gr a b -> [[LEdge b]]
Tree.getPathsTo Node
src Node
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall (gr :: * -> * -> *) b a.
DynGraph gr =>
(b -> Bool) -> gr a b -> gr a b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall a b. (a -> b) -> a -> b
\$ DGraph -> Gr DGNodeLab DGLinkLab
dgBody DGraph
dgraph

-- | return all non-cyclic paths starting from the given node
getAllPathsOfTypeFrom :: DGraph -> Node -> [[LEdge DGLinkLab]]
getAllPathsOfTypeFrom :: DGraph -> Node -> [[LEdge DGLinkLab]]
getAllPathsOfTypeFrom dgraph :: DGraph
dgraph src :: Node
src =
forall a b. Node -> Gr a b -> [[LEdge b]]
Tree.getPaths Node
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall (gr :: * -> * -> *) b a.
DynGraph gr =>
(b -> Bool) -> gr a b -> gr a b
elfilter (Bool -> Bool
not (Bool -> Bool) -> (DGLinkLab -> Bool) -> DGLinkLab -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall a b. (a -> b) -> a -> b
\$ DGraph -> Gr DGNodeLab DGLinkLab
dgBody DGraph
dgraph

-- * methods to check and select proof basis

checkEdgeIds :: DGraph -> Maybe [EdgeId]
checkEdgeIds :: DGraph -> Maybe [EdgeId]
checkEdgeIds dg :: DGraph
dg =
let pBl :: [EdgeId]
forall a b. (a -> b) -> [a] -> [b]
map (\ (_, _, l :: DGLinkLab
forall a b. (a -> b) -> a -> b
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LEdge b]
forall a b. (a -> b) -> a -> b
\$ DGraph -> Gr DGNodeLab DGLinkLab
dgBody DGraph
dg
pBs :: Set EdgeId
pBs = [EdgeId] -> Set EdgeId
forall a. Ord a => [a] -> Set a
Set.fromList [EdgeId]
pBl
pBl2 :: [EdgeId]
pBl2 = Set EdgeId -> [EdgeId]
forall a. Set a -> [a]
Set.toList Set EdgeId
pBs
in case [EdgeId]
pBl [EdgeId] -> [EdgeId] -> [EdgeId]
forall a. Eq a => [a] -> [a] -> [a]
\\ [EdgeId]
pBl2 of
[] -> if EdgeId -> Set EdgeId -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member EdgeId
defaultEdgeId Set EdgeId
pBs
then [EdgeId] -> Maybe [EdgeId]
forall a. a -> Maybe a
Just [EdgeId
defaultEdgeId] else Maybe [EdgeId]
forall a. Maybe a
Nothing
l :: [EdgeId]
l -> [EdgeId] -> Maybe [EdgeId]
forall a. a -> Maybe a
Just [EdgeId]
l

{- | determines all proven paths in the given list and tries to select a
proof basis from these (s. selectProofBasisAux);
if this fails the same is done for the rest of the given paths, i.e.
for the unproven ones -}
-> ProofBasis
selectProofBasis dg :: DGraph
paths = let
unprovenPaths) = ([LEdge DGLinkLab] -> Bool)
forall a. (a -> Bool) -> [a] -> ([a], [a])
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
forall a b. (a -> b) -> a -> b
paths
pBl :: [(EdgeId, Set EdgeId)]
pBl = (LEdge DGLinkLab -> (EdgeId, Set EdgeId))
-> [LEdge DGLinkLab] -> [(EdgeId, Set EdgeId)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (_, _, l :: DGLinkLab
l) ->
l, ProofBasis -> Set EdgeId
proofBasis (ProofBasis -> Set EdgeId) -> ProofBasis -> Set EdgeId
forall a b. (a -> b) -> a -> b
l))
([LEdge DGLinkLab] -> [(EdgeId, Set EdgeId)])
-> [LEdge DGLinkLab] -> [(EdgeId, Set EdgeId)]
forall a b. (a -> b) -> a -> b
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LEdge b]
forall a b. (a -> b) -> a -> b
\$ DGraph -> Gr DGNodeLab DGLinkLab
dgBody DGraph
dg
rel :: Map EdgeId (Set EdgeId)
rel = Bool -> Map EdgeId (Set EdgeId) -> Map EdgeId (Set EdgeId)
forall a. HasCallStack => Bool -> a -> a
assert (Maybe [EdgeId] -> Bool
forall a. Maybe a -> Bool
isNothing (DGraph -> Maybe [EdgeId]
checkEdgeIds DGraph
dg) Bool -> Bool -> Bool
&&
((EdgeId, Set EdgeId) -> Bool) -> [(EdgeId, Set EdgeId)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\ (e :: EdgeId
e, pB :: Set EdgeId
pB) -> Bool -> Bool
not (EdgeId -> Set EdgeId -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member EdgeId
e Set EdgeId
pB)) [(EdgeId, Set EdgeId)]
pBl) (Map EdgeId (Set EdgeId) -> Map EdgeId (Set EdgeId))
-> Map EdgeId (Set EdgeId) -> Map EdgeId (Set EdgeId)
forall a b. (a -> b) -> a -> b
\$
Rel EdgeId -> Map EdgeId (Set EdgeId)
forall a. Rel a -> Map a (Set a)
Rel.toMap (Rel EdgeId -> Map EdgeId (Set EdgeId))
-> Rel EdgeId -> Map EdgeId (Set EdgeId)
forall a b. (a -> b) -> a -> b
\$ Rel EdgeId -> Rel EdgeId
forall a. Ord a => Rel a -> Rel a
Rel.transClosure (Rel EdgeId -> Rel EdgeId) -> Rel EdgeId -> Rel EdgeId
forall a b. (a -> b) -> a -> b
\$ Map EdgeId (Set EdgeId) -> Rel EdgeId
forall a. Map a (Set a) -> Rel a
Rel.fromMap (Map EdgeId (Set EdgeId) -> Rel EdgeId)
-> Map EdgeId (Set EdgeId) -> Rel EdgeId
forall a b. (a -> b) -> a -> b
\$ [(EdgeId, Set EdgeId)] -> Map EdgeId (Set EdgeId)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(EdgeId, Set EdgeId)]
pBl
in Map EdgeId (Set EdgeId)
selectProofBasisAux Map EdgeId (Set EdgeId)
forall a b. (a -> b) -> a -> b
forall a. [a] -> [a] -> [a]
unprovenPaths

{- | selects the first path that does not form a proof cycle with the given
label (if such a path exits) and returns the labels of its edges -}
selectProofBasisAux :: Map.Map EdgeId (Set.Set EdgeId) -> LEdge DGLinkLab
selectProofBasisAux :: Map EdgeId (Set EdgeId)
selectProofBasisAux _ _ [] = ProofBasis
emptyProofBasis
selectProofBasisAux rel :: Map EdgeId (Set EdgeId)
path : list :: [[LEdge DGLinkLab]]
list) =
let b :: ProofBasis
b = Map EdgeId (Set EdgeId) -> [LEdge DGLinkLab] -> ProofBasis
calculateProofBasis Map EdgeId (Set EdgeId)
path in
if EdgeId -> ProofBasis -> Bool
ledge) ProofBasis
b
then Map EdgeId (Set EdgeId)
selectProofBasisAux Map EdgeId (Set EdgeId)
list
else ProofBasis
b               -- OK, no cyclic proof

{- | calculates the proofBasis of the given path,
i.e. (recursively) close the list of DGLinkLabs under the relation
'is proved using'. If a DGLinkLab has proof status LeftOpen,
look up in the development graph for its current status -}
calculateProofBasis :: Map.Map EdgeId (Set.Set EdgeId) -> [LEdge DGLinkLab]
-> ProofBasis
calculateProofBasis :: Map EdgeId (Set EdgeId) -> [LEdge DGLinkLab] -> ProofBasis
calculateProofBasis rel :: Map EdgeId (Set EdgeId)
rel = Set EdgeId -> ProofBasis
ProofBasis (Set EdgeId -> ProofBasis)
-> ([LEdge DGLinkLab] -> Set EdgeId)
-> ProofBasis
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LEdge DGLinkLab -> Set EdgeId -> Set EdgeId)
-> Set EdgeId -> [LEdge DGLinkLab] -> Set EdgeId
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr
(\ (_, _, l :: DGLinkLab
l) -> let eid :: EdgeId
l in EdgeId -> Set EdgeId -> Set EdgeId
forall a. Ord a => a -> Set a -> Set a
Set.insert EdgeId
eid
(Set EdgeId -> Set EdgeId)
-> (Set EdgeId -> Set EdgeId) -> Set EdgeId -> Set EdgeId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set EdgeId -> Set EdgeId -> Set EdgeId
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Set EdgeId -> EdgeId -> Map EdgeId (Set EdgeId) -> Set EdgeId
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Set EdgeId
forall a. Set a
Set.empty EdgeId
eid Map EdgeId (Set EdgeId)
rel))
Set EdgeId
forall a. Set a
Set.empty

t of
dl (ConsStatus c :: Conservativity
c _ _) ->
dl of
LeftOpen
forall a b. (a -> b) -> a -> b
\$ Conservativity -> Conservativity -> ThmLinkStatus -> ConsStatus
ConsStatus Conservativity
c Conservativity
LeftOpen
HidingFreeOrCofreeThm mh :: Maybe FreeOrCofree
mh n :: Node
n gm :: GMorphism
gm _ -> Maybe FreeOrCofree
HidingFreeOrCofreeThm Maybe FreeOrCofree
mh Node
n GMorphism
LeftOpen
t

-- | adopts the edges of the old node to the new node
adoptEdges :: DGraph -> Node -> Node -> DGraph
adoptEdges :: DGraph -> Node -> Node -> DGraph
dgraph oldNode :: Node
oldNode newNode :: Node
newNode =
if Node
oldNode Node -> Node -> Bool
forall a. Eq a => a -> a -> Bool
== Node
newNode then DGraph
dgraph else
outEdges') = String
-> DGraph
-> Node
dgraph Node
oldNode
forall a b. (a -> b) -> [a] -> [b]
map ( \ (l :: DGLinkLab
l, v :: Node
v) -> (Node
v, Node
inEdges'
forall a b. (a -> b) -> [a] -> [b]
map ( \ (l :: DGLinkLab
l, v :: Node
v) -> (Node
oldNode, Node
outEdges'
forall a b. (a -> b) -> [a] -> [b]
newNode Bool
inEdges
forall a b. (a -> b) -> [a] -> [b]
newNode Bool
outEdges
allChanges :: [DGChange]
forall a b. (a -> b) -> [a] -> [b]
forall a. [a] -> [a] -> [a]
outEdges)
[DGChange] -> [DGChange] -> [DGChange]
forall a. [a] -> [a] -> [a]
forall a b. (a -> b) -> [a] -> [b]
forall a. [a] -> [a] -> [a]
newOut)
in DGraph -> [DGChange] -> DGraph
changesDGH DGraph
dgraph [DGChange]
allChanges

-- | auxiliary method for adoptEdges
node areIngoingEdges :: Bool
areIngoingEdges (src :: Node
src, tgt :: Node
edgelab) =
let (newSrc :: Node
newSrc, newTgt :: Node
newTgt) = if Node
src Node -> Node -> Bool
forall a. Eq a => a -> a -> Bool
== Node
tgt then (Node
node, Node
node) else (Node
src, Node
tgt)
in if Bool
areIngoingEdges then (Node
newSrc, Node
edgelab)
else (Node
node, Node
edgelab)

getAllOpenNodeGoals :: [DGNodeLab] -> [DGNodeLab]
getAllOpenNodeGoals :: [DGNodeLab] -> [DGNodeLab]
getAllOpenNodeGoals = (DGNodeLab -> Bool) -> [DGNodeLab] -> [DGNodeLab]
forall a. (a -> Bool) -> [a] -> [a]
filter DGNodeLab -> Bool
hasOpenGoals

{- | return a warning text if the given label has incoming hiding edge,
otherwise just an empty string. -}
hidingLabelWarning :: DGNodeLab -> String
hidingLabelWarning :: DGNodeLab -> String
hidingLabelWarning lbl :: DGNodeLab
lbl = if DGNodeLab -> Bool
labelHasHiding DGNodeLab
lbl then
[String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
\$ "<Warning>" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ("  " String -> String -> String
forall a. [a] -> [a] -> [a]
++) [String]
hidingWarning [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ["</Warning>"]
else ""

{- | return a warning text if the given node has incoming hiding edge,
otherwise just an empty string. -}
addHasInHidingWarning :: DGraph -> Node -> String
addHasInHidingWarning :: DGraph -> Node -> String
dgraph = DGNodeLab -> String
hidingLabelWarning (DGNodeLab -> String) -> (Node -> DGNodeLab) -> Node -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGraph -> Node -> DGNodeLab
labDG DGraph
dgraph

hidingWarning :: [String]
hidingWarning :: [String]
hidingWarning =
[ "This node has incoming hiding links!"
, "The theory shown may be too weak for proving."
, "A consistency check may wrongly succeed."
, "If possible use the normal form of this node." ]
```