Skip to content

Commit

Permalink
Added extendDGraphRev function
Browse files Browse the repository at this point in the history
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@2305 cec4b9c1-7d33-0410-9eda-942365e851bb
  • Loading branch information
mmakowski committed Mar 22, 2004
1 parent cf29cb0 commit 845d5d2
Showing 1 changed file with 26 additions and 1 deletion.
27 changes: 26 additions & 1 deletion Static/DevGraph.hs
Original file line number Diff line number Diff line change
Expand Up @@ -172,7 +172,7 @@ extendDGraph :: DGraph -- ^ the development graph to be extended
-> Result (NodeSig, DGraph)
-- ^ returns 1. the target signature of the morphism and 2. the resulting DGraph
extendDGraph _ n@(EmptyNode _) _ _ =
do fatal_error "Trying to add a morphism originating from an empty node" nullPos
do fatal_error "Internal error: trying to add a morphism originating from an empty node" nullPos
extendDGraph dg (NodeSig (n, G_sign lid _)) morph orig =
let targetSig = cod Grothendieck morph
nodeContents = DGNode {dgn_name = Nothing,
Expand All @@ -188,6 +188,31 @@ extendDGraph dg (NodeSig (n, G_sign lid _)) morph orig =
in do return (NodeSig (node, targetSig), dg'')


-- | Extend the development graph with given morphism pointing to
-- given NodeSig
extendDGraphRev :: DGraph -- ^ the development graph to be extended
-> NodeSig -- ^ the NodeSig to which the morphism points
-> GMorphism -- ^ the morphism to be inserted
-> DGOrigin
-> Result (NodeSig, DGraph)
-- ^ returns 1. the source signature of the morphism and 2. the resulting DGraph
extendDGraphRev _ n@(EmptyNode _) _ _ =
do fatal_error "Internal error: trying to add a morphism pointing to an empty node" nullPos
extendDGraphRev dg (NodeSig (n, G_sign lid _)) morph orig =
let sourceSig = dom Grothendieck morph
nodeContents = DGNode {dgn_name = Nothing,
dgn_sign = sourceSig,
dgn_sens = G_l_sentence_list lid [],
dgn_origin = orig}
linkContents = DGLink {dgl_morphism = morph,
dgl_type = GlobalDef, -- TODO: other type
dgl_origin = orig}
[node] = newNodes 0 dg
dg' = insNode (node, nodeContents) dg
dg'' = insEdge (node, n, linkContents) dg'
in do return (NodeSig (node, sourceSig), dg'')


data ExtNodeSig = ExtNodeSig (Node,G_ext_sign) | ExtEmptyNode AnyLogic
deriving (Eq,Show)

Expand Down

0 comments on commit 845d5d2

Please sign in to comment.