ArchDiagram.hs revision 3aad1a996180e6888430cbdf5b1272a14fa89c16
e8eb2b9d68adc3024eb1aa9899b902ed5a3fb460Christian MaederModule : $Header$
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian MaederDescription : Data types and functions for architectural diagrams
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiCopyright : (c) Maciek Makowski, Warsaw University 2004-2006
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiMaintainer : till@informatik.uni-bremen.de
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederStability : provisional
2eeec5240b424984e3ee26296da1eeab6c6d739eChristian MaederPortability : non-portable (Logic)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski Data types and functions for architectural diagrams
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder Follows the CASL Reference Manual, section III.5.6.
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiimport qualified Common.Lib.Graph as Tree
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiimport qualified Data.Map as Map
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski-- (as defined for extended static semantics in Chap. III:5.6.1)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskidata DiagNodeLab = DiagNode { dn_sig :: NodeSig, dn_desc :: String }
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder deriving Show
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maederdata DiagLinkLab = DiagLink { dl_morphism :: GMorphism, dl_number:: Int }
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder deriving Show
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederdata Diag = Diagram {
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder diagGraph :: Tree.Gr DiagNodeLab DiagLinkLab,
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder numberOfEdges :: Int
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder deriving Show
556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaederemptyDiag :: Diag
556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaederemptyDiag = Diagram{diagGraph = Graph.empty, numberOfEdges = 0}
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskidata DiagNodeSig = Diag_node_sig Node NodeSig
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskidata MaybeDiagNode = JustDiagNode DiagNodeSig | EmptyDiagNode AnyLogic
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskitoMaybeNode :: MaybeDiagNode -> MaybeNode
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskitoMaybeNode mdn = case mdn of
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski JustDiagNode dns -> JustNode $ getSigFromDiag dns
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski EmptyDiagNode l -> EmptyNode l
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- | Return a signature stored within given diagram node sig
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaedergetSigFromDiag :: DiagNodeSig -> NodeSig
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaedergetSigFromDiag (Diag_node_sig _ ns) = ns
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskidata BasedUnitSig = Based_unit_sig DiagNodeSig
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski | Based_par_unit_sig MaybeDiagNode UnitSig
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskitype StBasedUnitCtx = Map.Map SIMPLE_ID BasedUnitSig
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederemptyStBasedUnitCtx :: StBasedUnitCtx
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiemptyStBasedUnitCtx = Map.empty
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski-- Since Ps and Bs in the definition of ExtStUnitCtx have disjoint domains
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski-- we can merge them into a single mapping represented by StBasedUnitCtx.
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskitype ExtStUnitCtx = (StBasedUnitCtx, Diag)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiemptyExtStUnitCtx :: ExtStUnitCtx
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiemptyExtStUnitCtx = (emptyStBasedUnitCtx, emptyDiag)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiinstance Pretty Diag where
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder pretty diag =
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maeder let gs (n, dn) =
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder (n, getSig $ dn_sig dn)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski in text "nodes:"
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski <+> sepByCommas (map (pretty . gs) $ labNodes $ diagGraph diag)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski $+$ text "edges:"
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder <+> ppWithCommas (edges $ diagGraph diag)
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maeder-- * Functions
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski-- | return the diagram
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiprintDiag :: a -> String -> Diag -> Result a
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiprintDiag res _ _ = return res
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski-- | A mapping from extended to basic static unit context
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederctx :: ExtStUnitCtx -> StUnitCtx
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskictx (buc, _) =
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski let ctx' [] _ = emptyStUnitCtx
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski ctx' (id1 : ids) buc0 =
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder let uctx = ctx' ids buc0
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski in case Map.lookup id1 buc0 of
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski Just (Based_unit_sig mds) -> Map.insert id1
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder (Sig $ getSigFromDiag mds) uctx
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski Just (Based_par_unit_sig mds usig) -> Map.insert id1
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski (ImpUnitSig (toMaybeNode mds) usig) uctx
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski _ -> uctx -- this should never be the case
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski in ctx' (Map.keys buc) buc
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu-- | Insert the edges from given source nodes to given target node
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu-- into the given diagram. The edges are labelled with inclusions.
a98fd29a06e80e447af26d898044c23497adbc73Mihai CodescuinsInclusionEdges :: LogicGraph
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski -> Diag -- ^ the diagram to insert edges to
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski -> [DiagNodeSig] -- ^ the source nodes
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski -> DiagNodeSig -- ^ the target node
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder -> Result Diag -- ^ the diagram with edges inserted
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiinsInclusionEdges lgraph diag0 srcNodes (Diag_node_sig tn tnsig) = do
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski let inslink diag dns = do
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder let d = diagGraph d1
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski Diag_node_sig n nsig -> do
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder incl <- ginclusion lgraph (getSig nsig) (getSig tnsig)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski return $ Diagram {diagGraph = insEdge (n, tn, DiagLink {
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder dl_morphism = incl,
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski dl_number = numberOfEdges d1 + 1 }) d,
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski numberOfEdges = numberOfEdges d1 + 1}
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder diag' <- foldl inslink (return diag0) srcNodes
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski-- | Insert the edges from given source node to given target nodes
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski-- into the given diagram. The edges are labelled with inclusions.
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiinsInclusionEdgesRev :: LogicGraph
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski -> Diag -- ^ the diagram to insert edges to
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder -> DiagNodeSig -- ^ the source node
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder -> [DiagNodeSig] -- ^ the target nodes
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder -> Result Diag -- ^ the diagram with edges inserted
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederinsInclusionEdgesRev lgraph diag0 (Diag_node_sig sn snsig) targetNodes =
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder do let inslink diag dns = do
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder let d = diagGraph d1
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder Diag_node_sig n nsig -> do
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder incl <- ginclusion lgraph (getSig snsig) (getSig nsig)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder return $ Diagram {diagGraph = insEdge (sn, n, DiagLink {
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder dl_morphism = incl,
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder dl_number = numberOfEdges d1 + 1 }) d,
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder numberOfEdges = numberOfEdges d1 + 1}
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder diag' <- foldl inslink (return diag0) targetNodes
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder{- | Build a diagram that extends given diagram with a node containing
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maedergiven signature and with edges from given set of nodes to the new
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maedernode. The new edges are labelled with sigature inclusions. -}
a98fd29a06e80e447af26d898044c23497adbc73Mihai CodescuextendDiagramIncl :: LogicGraph
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder -> Diag -- ^ the diagram to be extended
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder -> [DiagNodeSig]
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder -- ^ the nodes which should be linked to the new node
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder -- ^ the signature with which the new node should be labelled
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder -> String -- ^ the node description (for diagnostics)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder -> Result (DiagNodeSig, Diag)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- ^ returns the new node and the extended diagram
556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaederextendDiagramIncl lgraph diag srcNodes newNodeSig desc =
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder do let nodeContents = DiagNode {dn_sig = newNodeSig, dn_desc = desc}
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder diagGr = diagGraph diag
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder diag' = Diagram{diagGraph = insNode (node, nodeContents) diagGr,
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder numberOfEdges = numberOfEdges diag}
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder newDiagNode = Diag_node_sig node newNodeSig
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder diag'' <- insInclusionEdges lgraph diag' srcNodes newDiagNode
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder printDiag (newDiagNode, diag'') "extendDiagramIncl" diag''
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- | Extend the development graph with given morphism originating
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- from given NodeSig
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederextendDGraph :: DGraph -- ^ the development graph to be extended
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder -> NodeSig -- ^ the NodeSig from which the morphism originates
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder -> GMorphism -- ^ the morphism to be inserted
4d7d53fec6b551333c79da6ae3b8ca2af0a741abChristian Maeder -> Result (NodeSig, DGraph)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- ^ returns the target signature of the morphism and the resulting DGraph
e8eb2b9d68adc3024eb1aa9899b902ed5a3fb460Christian MaederextendDGraph dg (NodeSig n _) morph orig = case cod morph of
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder targetSig@(G_sign lid tar ind) -> let
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu nodeContents = newNodeLab emptyNodeName orig
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu $ noSensGTheory lid tar ind
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu linkContents = DGLink
c18a07fe36512679e66faa59274bb273e735738aMihai Codescu { dgl_morphism = morph
da955132262baab309a50fdffe228c9efe68251dCui Jian , dgl_type = globalDef
c18a07fe36512679e66faa59274bb273e735738aMihai Codescu , dgl_origin = SeeTarget
c18a07fe36512679e66faa59274bb273e735738aMihai Codescu , dgl_id = getNewEdgeId dg' }
da955132262baab309a50fdffe228c9efe68251dCui Jian node = getNewNodeDG dg
c18a07fe36512679e66faa59274bb273e735738aMihai Codescu dg' = insNodeDG (node, nodeContents) dg
da955132262baab309a50fdffe228c9efe68251dCui Jian dg'' = insEdgeDG (n, node, linkContents) dg'
c18a07fe36512679e66faa59274bb273e735738aMihai Codescu in return (NodeSig node targetSig, dg'')
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- | Extend the development graph with given morphism pointing to
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- given NodeSig
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederextendDGraphRev :: DGraph -- ^ the development graph to be extended
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder -> NodeSig -- ^ the NodeSig to which the morphism points
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder -> GMorphism -- ^ the morphism to be inserted
cd6e5706893519bfcf24539afa252fcbed5097ddKlaus Luettich -> Result (NodeSig, DGraph)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- ^ returns the source signature of the morphism and the resulting DGraph
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederextendDGraphRev dg (NodeSig n _) morph orig = case dom morph of
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sourceSig@(G_sign lid src ind) -> let
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder nodeContents = newNodeLab emptyNodeName orig
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder $ noSensGTheory lid src ind
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder linkContents = DGLink
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder { dgl_morphism = morph
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder , dgl_type = globalDef
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder , dgl_origin = SeeSource
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder , dgl_id = getNewEdgeId dg' }
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder node = getNewNodeDG dg
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder dg' = insNodeDG (node, nodeContents) dg
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder dg'' = insEdgeDG (node, n, linkContents) dg'
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder in return (NodeSig node sourceSig, dg'')
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder{- | Build a diagram that extends the given diagram with a node and an
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederedge to that node. The edge is labelled with a given signature morphism
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederand the node contains the target of this morphism. Extends the
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederdevelopment graph with the given morphism as well. -}
e8eb2b9d68adc3024eb1aa9899b902ed5a3fb460Christian MaederextendDiagramWithMorphism :: Range -- ^ the position (for diagnostics)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder -> LogicGraph
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder -> Diag -- ^ the diagram to be extended
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder -> DGraph -- ^ the development graph
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder -> DiagNodeSig
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder -- ^ the node from which the edge should originate
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder -- ^ the morphism as label for the new edge
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder -> String -- ^ the node description (for diagnostics)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder -> DGOrigin -- ^ the origin of the new node
cd6e5706893519bfcf24539afa252fcbed5097ddKlaus Luettich -> Result (DiagNodeSig, Diag, DGraph)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- ^ returns the new node, the extended diagram and extended development graph
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederextendDiagramWithMorphism pos _ diag dg (Diag_node_sig n nsig) mor desc orig =
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder if getSig nsig == dom mor then
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder do (targetSig, dg') <- extendDGraph dg nsig mor orig
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder let nodeContents = DiagNode {dn_sig = targetSig, dn_desc = desc}
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder diagGr = diagGraph diag
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder diagGr' = insNode (node, nodeContents) diagGr
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder diag' = Diagram{diagGraph = insEdge (n, node, DiagLink {
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder dl_morphism = mor,
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder dl_number = numberOfEdges diag + 1 }) diagGr',
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder numberOfEdges = numberOfEdges diag + 1 }
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder printDiag (Diag_node_sig node targetSig, diag', dg')
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder "extendDiagramWithMorphism" diag'
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder else fatal_error
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder ("Internal error: Static.ArchDiagram.extendDiagramWithMorphism:" ++
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder "\n the morphism domain differs from the signature in given source node")
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder{- | Build a diagram that extends a given diagram with a node and an
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederedge from that node. The edge is labelled with a given signature
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maedermorphism and the node contains the source of this morphism. Extends
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederthe development graph with the given morphism as well. -}
556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaederextendDiagramWithMorphismRev :: Range -- ^ the position (for diagnostics)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder -> LogicGraph
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder -> Diag -- ^ the diagram to be extended
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder -> DGraph -- ^ the development graph
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder -> DiagNodeSig
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder -- ^ the node to which the edge should point
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu -- ^ the morphism as label for the new edge
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu -> String -- ^ a diagnostic node description
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder -> DGOrigin -- ^ the origin of the new node
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder -> Result (DiagNodeSig, Diag, DGraph)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- ^ returns the new node, the extended diagram and extended development graph
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederextendDiagramWithMorphismRev pos _ diag dg (Diag_node_sig n nsig)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder mor desc orig =
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder if getSig nsig == cod mor then
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder do (sourceSig, dg') <- extendDGraphRev dg nsig mor orig
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu let nodeContents = DiagNode {dn_sig = sourceSig, dn_desc = desc}
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu diagGr = diagGraph diag
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu diagGr' = insNode (node, nodeContents) diagGr
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder diag' = Diagram{ diagGraph = insEdge (node, n, DiagLink {
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder dl_morphism = mor ,
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder dl_number = numberOfEdges diag + 1}) diagGr',
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder numberOfEdges = numberOfEdges diag + 1 }
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder printDiag (Diag_node_sig node sourceSig, diag', dg')
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder "extendDiagramWithMorphismRev" diag'
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder else fatal_error
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder ("Internal error: Static.ArchDiagram.extendDiagramWithMorphismRev:\n" ++
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder " the morphism codomain differs from the signature in given target node")
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder{- | Build a diagram that extends given diagram with a node containing
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maedergiven signature and with edge from given nodes to the new node. The
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maedernew edge is labelled with given signature morphism. -}
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederextendDiagram :: Diag -- ^ the diagram to be extended
da955132262baab309a50fdffe228c9efe68251dCui Jian -> DiagNodeSig -- ^ the node from which morphism originates
c18a07fe36512679e66faa59274bb273e735738aMihai Codescu -> GMorphism -- ^ the morphism as label for the new edge
da955132262baab309a50fdffe228c9efe68251dCui Jian -> NodeSig -- ^ the signature as label for the new node
da955132262baab309a50fdffe228c9efe68251dCui Jian -> String -- ^ the node description (for diagnostics)
da955132262baab309a50fdffe228c9efe68251dCui Jian -> Result (DiagNodeSig, Diag)
c18a07fe36512679e66faa59274bb273e735738aMihai Codescu-- ^ returns the new node and the extended diagram
c18a07fe36512679e66faa59274bb273e735738aMihai CodescuextendDiagram diag (Diag_node_sig n _) edgeMorph newNodeSig desc =
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder do let nodeContents = DiagNode {dn_sig = newNodeSig, dn_desc = desc}
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder diagGr = diagGraph diag
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder diagGr' = insNode (node, nodeContents) diagGr
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu diag' = Diagram{diagGraph = insEdge (n, node, DiagLink {
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu dl_morphism = edgeMorph,
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu dl_number = numberOfEdges diag + 1 }) diagGr',
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder numberOfEdges = numberOfEdges diag + 1 }
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder newDiagNode = Diag_node_sig node newNodeSig
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder printDiag (newDiagNode, diag') "extendDiagram" diag'
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder{- | Convert a homogeneous diagram to a simple diagram where all the
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maedersignatures in nodes and morphism on the edges are coerced to a common
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederhomogeniseDiagram :: Logic lid sublogics
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder basic_spec sentence symb_items symb_map_items
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign morphism symbol raw_symbol proof_tree
e8eb2b9d68adc3024eb1aa9899b902ed5a3fb460Christian Maeder => lid -- ^ the target logic to be coerced to
e8eb2b9d68adc3024eb1aa9899b902ed5a3fb460Christian Maeder -> Diag -- ^ the diagram to be homogenised
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder -> Result (Tree.Gr sign (Int,morphism))
e8eb2b9d68adc3024eb1aa9899b902ed5a3fb460Christian Maeder{- The implementation relies on the representation of graph nodes as
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederintegers. We can therefore just obtain a list of all the labelled
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maedernodes from diag, convert all the nodes and insert them to a new
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederdiagram; then copy all the edges from the original to new diagram
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder(coercing the morphisms). -}
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederhomogeniseDiagram targetLid diag =
cd6e5706893519bfcf24539afa252fcbed5097ddKlaus Luettich do let convertNode (n, dn) =
cd6e5706893519bfcf24539afa252fcbed5097ddKlaus Luettich do G_sign srcLid sig _ <- return $ getSig $ dn_sig dn
cd6e5706893519bfcf24539afa252fcbed5097ddKlaus Luettich sig' <- coerceSign srcLid targetLid "" sig
cd6e5706893519bfcf24539afa252fcbed5097ddKlaus Luettich return (n, plainSign sig')
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder convertEdge (n1, n2, DiagLink {
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder dl_morphism = GMorphism cid _ _ mor _, dl_number = nr})
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder = if isIdComorphism (Comorphism cid) then
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder do mor' <- coerceMorphism (targetLogic cid) targetLid "" mor
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder return (n1, n2, (nr,mor'))
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder "Trying to coerce a morphism between different logics.\n" ++
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder "Heterogeneous specifications are not fully supported yet."
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder convertNodes cDiag [] = do return cDiag
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder convertNodes cDiag (lNode : lNodes) =
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder do convNode <- convertNode lNode
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder let cDiag' = insNode convNode cDiag
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder convertNodes cDiag' lNodes
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder convertEdges cDiag [] = do return cDiag
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder convertEdges cDiag (lEdge : lEdges) =
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder do convEdge <- convertEdge lEdge
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder let cDiag' = insEdge convEdge cDiag
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder convertEdges cDiag' lEdges
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder dNodes = labNodes $ diagGraph diag
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder dEdges = labEdges $ diagGraph diag
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder -- insert converted nodes to an empty diagram
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder cDiag <- convertNodes Graph.empty dNodes
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder -- insert converted edges to the diagram containing only nodes
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder cDiag' <- convertEdges cDiag dEdges
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder return cDiag'
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder-- | Create a graph containing descriptions of nodes and edges.
556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaederdiagDesc :: Diag
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder -> Tree.Gr String String
556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaederdiagDesc diag =
in foldl insNodeDesc Graph.empty . labNodes $ diagGraph diag