NormalForm.hs revision d11391a2447a2005329a95b5d770f24e62bf5b63
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederModule : $Header$
782d5365e084a40e4f717dafbe00fc41476a7cfeChristian MaederDescription : compute the normal forms of all nodes in development graphs
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederCopyright : (c) Christian Maeder, DFKI GmbH 2009
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederMaintainer : Christian.Maeder@dfki.de
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederStability : provisional
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederPortability : non-portable(Logic)
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maedercompute normal forms
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder ( normalFormLibEnv
fe216849cef7b87c6800aad21178d1e686575d8fChristian Maederimport Logic.Prover(toNamedList, toThSens)
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maederimport qualified Data.Map as Map
782d5365e084a40e4f717dafbe00fc41476a7cfeChristian MaedernormalFormRule :: DGRule
782d5365e084a40e4f717dafbe00fc41476a7cfeChristian MaedernormalFormRule = DGRule "NormalForm"
782d5365e084a40e4f717dafbe00fc41476a7cfeChristian Maeder-- | compute normal form for a library and imported libs
782d5365e084a40e4f717dafbe00fc41476a7cfeChristian MaedernormalForm :: LibName -> LibEnv -> Result LibEnv
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian MaedernormalForm ln le = normalFormLNS (dependentLibs ln le) le
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder-- | compute norm form for all libraries
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian MaedernormalFormLibEnv :: LibEnv -> Result LibEnv
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian MaedernormalFormLibEnv le = normalFormLNS (getTopsortedLibs le) le
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian MaedernormalFormLNS :: [LibName] -> LibEnv -> Result LibEnv
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian MaedernormalFormLNS lns libEnv = foldM (\ le ln -> do
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder let dg = lookupDGraph ln le
fe216849cef7b87c6800aad21178d1e686575d8fChristian Maeder newDg <- normalFormDG le dg
fe216849cef7b87c6800aad21178d1e686575d8fChristian Maeder (groupHistory dg normalFormRule newDg) le)
fe216849cef7b87c6800aad21178d1e686575d8fChristian MaedernormalFormDG :: LibEnv -> DGraph -> Result DGraph
fe216849cef7b87c6800aad21178d1e686575d8fChristian MaedernormalFormDG libEnv dgraph = foldM (\ dg (node, nodelab) ->
fe216849cef7b87c6800aad21178d1e686575d8fChristian Maeder if labelHasHiding nodelab then case dgn_nf nodelab of
fe216849cef7b87c6800aad21178d1e686575d8fChristian Maeder Just _ -> return dg -- already computed
bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian Maeder Nothing -> if isDGRef nodelab then do
bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian Maeder -- the normal form of the node
bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian Maeder -- is a reference to the normal form of the node it references
bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian Maeder -- careful: here not refNf, but a new Node which references refN
bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian Maeder let refLib = dgn_libname nodelab
bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian Maeder refNode = dgn_node nodelab
bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian Maeder refGraph' = lookupDGraph refLib libEnv
bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian Maeder refLabel = labDG refGraph' refNode
bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian Maeder case dgn_nf refLabel of
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Nothing -> warning dg
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder (getDGNodeName refLabel ++ " (node " ++ show refNode
fe216849cef7b87c6800aad21178d1e686575d8fChristian Maeder ++ ") from '" ++ show (getLibId refLib)
fe216849cef7b87c6800aad21178d1e686575d8fChristian Maeder ++ "' without normal form") nullRange
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Just refNf -> do
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder let refNodelab = labDG refGraph' refNf
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder -- the label of the normal form ^
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder nfNode = getNewNodeDG dg
f7d2e793728bbb7fd185e027eb9dfd7b9dd11c21Christian Maeder -- the new reference node in the old graph ^
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder refLab = refNodelab
fe216849cef7b87c6800aad21178d1e686575d8fChristian Maeder { dgn_name = extName "NormalForm" $ dgn_name nodelab
f7d2e793728bbb7fd185e027eb9dfd7b9dd11c21Christian Maeder , dgn_nf = Just nfNode
02a2037f53b925617df45eb62ca743d777672265Klaus Luettich , dgn_sigma = Just $ ide $ dgn_sign refNodelab
02a2037f53b925617df45eb62ca743d777672265Klaus Luettich , nodeInfo = newRefInfo refLib refNf
02a2037f53b925617df45eb62ca743d777672265Klaus Luettich , dgn_lock = Nothing }
02a2037f53b925617df45eb62ca743d777672265Klaus Luettich newLab = nodelab
02a2037f53b925617df45eb62ca743d777672265Klaus Luettich { dgn_nf = Just nfNode,
f7d2e793728bbb7fd185e027eb9dfd7b9dd11c21Christian Maeder dgn_sigma = dgn_sigma refLabel }
5908cc06d7a3f4dd46d2d7c7fe0fad43b6cd921fChristian Maeder chLab = SetNodeLab nodelab (node, newLab)
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder changes = [InsertNode (nfNode, refLab), chLab]
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder newGraph = changesDGH dgraph changes
5908cc06d7a3f4dd46d2d7c7fe0fad43b6cd921fChristian Maeder return newGraph
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder let gd = insNode (node, dgn_theory nodelab) empty
02a2037f53b925617df45eb62ca743d777672265Klaus Luettich g0 = Map.fromList [(node, node)]
e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder (diagram, g) = computeDiagram dg [node] (gd, g0)
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder fsub = finalSubcateg diagram
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder Result ds res = gWeaklyAmalgamableCocone fsub
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder es = map (\ d -> if isErrorDiag d then d { diagKind = Warning }
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder appendDiags es
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder Nothing -> warning dg
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder ("cocone failure for " ++ getDGNodeName nodelab
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder ++ " (node " ++ shows node ")") nullRange
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder Just (sign, mmap) -> do
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder -- we don't know that node is in fsub
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder -- if it's not, we have to find a tip accessible from node
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder -- and dgn_sigma = edgeLabel(node, tip); mmap (g Map.! tip)
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder morNode <- if node `elem` nodes fsub then let
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder gn = Map.findWithDefault (error "gn") node g
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder phi = Map.findWithDefault (error "mor") gn mmap
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder in return phi else let
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder leaves = filter (\x -> outdeg fsub x == 0) $
f7d2e793728bbb7fd185e027eb9dfd7b9dd11c21Christian Maeder paths = map (\(x, Result _ (Just f)) -> (x,f)) $
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder (x, dijkstra diagram node x)) $
f7d2e793728bbb7fd185e027eb9dfd7b9dd11c21Christian Maeder filter (\x -> node `elem` subgraph
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder diagram x) leaves
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder case paths of
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder [] -> fail "node should reach a tip"
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder (xn, xf) : _ -> comp xf $ mmap Map.! xn
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder let nfNode = getNewNodeDG dg -- new node for normal form
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder info = nodeInfo nodelab
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder ConsStatus c cp pr = node_cons_status info
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder nfLabel = newInfoNodeLab
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder (extName "NormalForm" $ dgn_name nodelab)
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder { node_origin = DGNormalForm node
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder , node_cons_status = mkConsStatus c }
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder newLab = nodelab -- the new label for node
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder { dgn_nf = Just nfNode
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder , dgn_sigma = Just morNode
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder , nodeInfo = info
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder { node_cons_status = ConsStatus None cp pr }
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder -- add the nf to the label of node
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder chLab = SetNodeLab nodelab (node, newLab)
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder -- insert the new node and add edges from the predecessors
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder insNNF = InsertNode (nfNode, nfLabel)
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder makeEdge src tgt m = (src, tgt, globDefLink m DGLinkProof)
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder insStrMor = map (\ (x, f) -> InsertEdge $ makeEdge x nfNode f)
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder $ nub $ map (\ (x, y) -> (g Map.! x, y))
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder $ (node, morNode) : Map.toList mmap
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder allChanges = insNNF : chLab : insStrMor
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder newDG = changesDGH dg allChanges
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder return $ changeDGH newDG $ SetNodeLab nfLabel (nfNode, nfLabel
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder { globalTheory = computeLabelTheory libEnv newDG
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder (nfNode, nfLabel) })
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder else return dg) dgraph $ topsortedNodes dgraph -- only change relevant nodes
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder{- | computes the diagram associated to a node N in a development graph,
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder adding common origins for multiple occurences of nodes, whenever
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian MaedercomputeDiagram :: DGraph -> [Node] -> (GDiagram, Map.Map Node Node)
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder -> (GDiagram, Map.Map Node Node)
36fcac4cf0f6a1f8a0fee696ac7f4b91d769843cChristian Maeder -- as described in the paper for now
0678d323bee844db79af13113ae252546629a594Christian MaedercomputeDiagram dgraph nodeList (gd, g) =
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder case nodeList of
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder [] -> (gd, g)
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder let -- defInEdges is list of pairs (n, edges of target g(n))
0678d323bee844db79af13113ae252546629a594Christian Maeder defInEdges = map (\n -> (n,filter (\e@(s,t,_) -> s /= t &&
0678d323bee844db79af13113ae252546629a594Christian Maeder liftE (liftOr isGlobalDef isHidingDef) e) $
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder innDG dgraph $ g Map.! n)) nodeList
0678d323bee844db79af13113ae252546629a594Christian Maeder -- TO DO: no local links, and why edges with s=t are removed
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder -- add normal form nodes
36fcac4cf0f6a1f8a0fee696ac7f4b91d769843cChristian Maeder -- sources of each edge must be added as new nodes
0678d323bee844db79af13113ae252546629a594Christian Maeder nodeIds = zip (newNodes (length $ concatMap snd defInEdges) gd)
0678d323bee844db79af13113ae252546629a594Christian Maeder $ concatMap (\(n,l) -> map (\x -> (n,x)) l ) defInEdges
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder newLNodes = zip (map fst nodeIds) $
b7b2eb9d574f5ed3ac3e9e1d7a5f168ed78a0604Till Mossakowski map (\ (s,_,_) -> dgn_theory $ labDG dgraph s) $
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder concatMap snd defInEdges
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder map (\ (newS, (_newT, (s,_t, _))) -> (newS,s)) nodeIds
0678d323bee844db79af13113ae252546629a594Christian Maeder morphEdge (n1,(n2, (_, _, el))) =
0678d323bee844db79af13113ae252546629a594Christian Maeder if isHidingDef $ dgl_type el
0678d323bee844db79af13113ae252546629a594Christian Maeder then (n2, n1, (x, dgl_morphism el))
0678d323bee844db79af13113ae252546629a594Christian Maeder else (n1, n2, (x, dgl_morphism el))
0678d323bee844db79af13113ae252546629a594Christian Maeder where EdgeId x = dgl_id el
0678d323bee844db79af13113ae252546629a594Christian Maeder newLEdges = map morphEdge nodeIds
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder gd' = insEdges newLEdges $ insNodes newLNodes gd
b7b2eb9d574f5ed3ac3e9e1d7a5f168ed78a0604Till Mossakowski in computeDiagram dgraph (map fst nodeIds) (gd', g')
0678d323bee844db79af13113ae252546629a594Christian MaederfinalSubcateg :: GDiagram -> GDiagram
0678d323bee844db79af13113ae252546629a594Christian MaederfinalSubcateg graph = let
0678d323bee844db79af13113ae252546629a594Christian Maeder leaves = filter (\(n,_) -> outdeg graph n == 0)$ labNodes graph
0678d323bee844db79af13113ae252546629a594Christian Maeder in buildGraph graph (map fst leaves) leaves [] $ nodes graph
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maedersubgraph :: Gr a b -> Node -> [Node]
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maedersubgraph graph node = let
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder descs nList descList =
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder case nList of
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder [] -> descList
0678d323bee844db79af13113ae252546629a594Christian Maeder newDescs = concatMap (\x -> pre graph x) nList
0678d323bee844db79af13113ae252546629a594Christian Maeder nList' = filter (\x -> not $ x `elem` nList) newDescs
0678d323bee844db79af13113ae252546629a594Christian Maeder descList' = nub $ descList ++ newDescs
0678d323bee844db79af13113ae252546629a594Christian Maeder in descs nList' descList'
fe216849cef7b87c6800aad21178d1e686575d8fChristian Maeder in descs [node] []
0678d323bee844db79af13113ae252546629a594Christian MaederbuildGraph :: GDiagram -> [Node]
0678d323bee844db79af13113ae252546629a594Christian Maeder -> [LNode G_theory]
0678d323bee844db79af13113ae252546629a594Christian Maeder -> [LEdge (Int, GMorphism)]
0678d323bee844db79af13113ae252546629a594Christian MaederbuildGraph oGraph leaves nList eList nodeList =
0678d323bee844db79af13113ae252546629a594Christian Maeder case nodeList of
0678d323bee844db79af13113ae252546629a594Christian Maeder [] -> mkGraph nList eList
0678d323bee844db79af13113ae252546629a594Christian Maeder n:nodeList' ->
0678d323bee844db79af13113ae252546629a594Christian Maeder case outdeg oGraph n of
0678d323bee844db79af13113ae252546629a594Christian Maeder 1 -> buildGraph oGraph leaves nList eList nodeList'
0678d323bee844db79af13113ae252546629a594Christian Maeder -- the node is simply removed
0678d323bee844db79af13113ae252546629a594Christian Maeder 0 -> buildGraph oGraph leaves nList eList nodeList'
0678d323bee844db79af13113ae252546629a594Christian Maeder -- the leaves have already been added to nList
0678d323bee844db79af13113ae252546629a594Christian Maeder Just l = lab oGraph n
0678d323bee844db79af13113ae252546629a594Christian Maeder nList' = (n, l):nList
0678d323bee844db79af13113ae252546629a594Christian Maeder accesLeaves = filter (\x -> n `elem` subgraph oGraph x) leaves
0678d323bee844db79af13113ae252546629a594Christian Maeder eList' = map ( \(x, Result _ (Just y)) -> (n,x,(1::Int,y))) $
0678d323bee844db79af13113ae252546629a594Christian Maeder map (\x -> (x, dijkstra oGraph n x)) accesLeaves
0678d323bee844db79af13113ae252546629a594Christian Maeder in buildGraph oGraph leaves nList' (eList ++ eList') nodeList'
0678d323bee844db79af13113ae252546629a594Christian Maeder -- branch, must add n to the nList and edges in eList
0678d323bee844db79af13113ae252546629a594Christian Maederfreeness :: LibName -> LibEnv -> Result LibEnv
f7d2e793728bbb7fd185e027eb9dfd7b9dd11c21Christian Maederfreeness ln le = do
0678d323bee844db79af13113ae252546629a594Christian Maeder let dg = lookupDGraph ln le
0678d323bee844db79af13113ae252546629a594Christian Maeder newDg <- freenessDG le dg
0678d323bee844db79af13113ae252546629a594Christian Maeder (groupHistory dg normalFormRule newDg) le
0678d323bee844db79af13113ae252546629a594Christian MaederfreenessDG :: LibEnv -> DGraph -> Result DGraph
0678d323bee844db79af13113ae252546629a594Christian MaederfreenessDG _le dgraph = do
0678d323bee844db79af13113ae252546629a594Christian Maeder foldM handleEdge dgraph $ labEdgesDG dgraph
0678d323bee844db79af13113ae252546629a594Christian MaederhandleEdge :: DGraph -> LEdge DGLinkLab -> Result DGraph
0678d323bee844db79af13113ae252546629a594Christian MaederhandleEdge dg edge@(m,n,x) = do
0678d323bee844db79af13113ae252546629a594Christian Maeder case dgl_type x of
0678d323bee844db79af13113ae252546629a594Christian Maeder FreeOrCofreeDefLink _ _ -> do
0678d323bee844db79af13113ae252546629a594Christian Maeder let phi = dgl_morphism x
0678d323bee844db79af13113ae252546629a594Christian Maeder gth= dgn_theory $ labDG dg m
0678d323bee844db79af13113ae252546629a594Christian Maeder G_theory lid sig _ sen _ -> do
0678d323bee844db79af13113ae252546629a594Christian Maeder GMorphism cid _ _ mor1 _ -> do
0678d323bee844db79af13113ae252546629a594Christian Maeder mor <- coerceMorphism (targetLogic cid) lid "free" mor1
0678d323bee844db79af13113ae252546629a594Christian Maeder let res = quotient_term_algebra lid mor $ toNamedList sen
3ef9708a35cddb7ba66458ad4a065de549ce7db6Till Mossakowski case maybeResult res of
0678d323bee844db79af13113ae252546629a594Christian Maeder Just (sigK, axK) -> do
0678d323bee844db79af13113ae252546629a594Christian Maeder -- success in logic lid
0678d323bee844db79af13113ae252546629a594Christian Maeder let thK = G_theory lid (makeExtSign lid sigK)
0678d323bee844db79af13113ae252546629a594Christian Maeder startSigId (toThSens axK) startThId
0678d323bee844db79af13113ae252546629a594Christian Maeder incl <- subsig_inclusion lid (plainSign sig) sigK
0678d323bee844db79af13113ae252546629a594Christian Maeder let inclM = gEmbed $ mkG_morphism lid incl
0678d323bee844db79af13113ae252546629a594Christian Maeder -- k with signature = sigK, sentences axK
f7d2e793728bbb7fd185e027eb9dfd7b9dd11c21Christian Maeder -- global def link from m to k, labeled with inclusion
0678d323bee844db79af13113ae252546629a594Christian Maeder -- hiding def link from k to n, labeled with inclusion
0678d323bee844db79af13113ae252546629a594Christian Maeder -- m' = getNewNodeDG dg -- new node
0678d323bee844db79af13113ae252546629a594Christian Maeder nodelab = labDG dg m
0678d323bee844db79af13113ae252546629a594Christian Maeder info = nodeInfo nodelab