ArchDiagram.hs revision 878d0086bd0aae2d7ad64451035c4e78047b1cff
57221209d11b05aa0373cc3892d5df89ba96ebf9Christian Maeder Module : $Header$
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Copyright : (c) Maciek Makowski, Warsaw University 2004
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder License : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowski Maintainer : till@tzi.de
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescu Stability : provisional
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Portability : non-portable (Logic)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederData types and functions for architectural diagrams.
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder Follows the CASL Reference Manual, section III.5.6.
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederimport qualified Data.Graph.Inductive.Tree as Tree
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederimport qualified Common.Lib.Map as Map
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder-- (as defined for extended static semantics in Chap. III:5.6.1)
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederdata DiagNodeLab = DiagNode { dn_sig :: NodeSig,
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder dn_desc :: String }
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederdata DiagLinkLab = DiagLink { dl_morphism :: GMorphism }
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maedertype Diag = Tree.Gr DiagNodeLab DiagLinkLab
351391e0e3226210e7ffb183b334da9f96de36eaChristian MaederemptyDiag :: Diag
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederdata DiagNodeSig = Diag_node_sig Node NodeSig
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederdata MaybeDiagNode = JustDiagNode DiagNodeSig
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder | EmptyDiagNode AnyLogic
351391e0e3226210e7ffb183b334da9f96de36eaChristian MaedertoMaybeNode :: MaybeDiagNode -> MaybeNode
351391e0e3226210e7ffb183b334da9f96de36eaChristian MaedertoMaybeNode mdn = case mdn of
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder JustDiagNode dns -> JustNode $ getSigFromDiag dns
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder EmptyDiagNode l -> EmptyNode l
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder-- | Return a signature stored within given diagram node sig
351391e0e3226210e7ffb183b334da9f96de36eaChristian MaedergetSigFromDiag :: DiagNodeSig -> NodeSig
351391e0e3226210e7ffb183b334da9f96de36eaChristian MaedergetSigFromDiag (Diag_node_sig _ ns) = ns
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederdata BasedUnitSig = Based_unit_sig DiagNodeSig
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder | Based_par_unit_sig MaybeDiagNode UnitSig
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maedertype StBasedUnitCtx = Map.Map SIMPLE_ID BasedUnitSig
351391e0e3226210e7ffb183b334da9f96de36eaChristian MaederemptyStBasedUnitCtx :: StBasedUnitCtx
351391e0e3226210e7ffb183b334da9f96de36eaChristian MaederemptyStBasedUnitCtx = Map.empty
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder-- Since Ps and Bs in the definition of ExtStUnitCtx have disjoint domains
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder-- we can merge them into a single mapping represented by StBasedUnitCtx.
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maedertype ExtStUnitCtx = (StBasedUnitCtx, Diag)
f8b715ab2993083761c0aedb78f1819bcf67b6ccChristian MaederemptyExtStUnitCtx :: ExtStUnitCtx
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederemptyExtStUnitCtx = (emptyStBasedUnitCtx, emptyDiag)
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder-- * Instances
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski-- PrettyPrint
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wanginstance PrettyPrint Diag where
23a00c966f2aa8da525d7a7c51933c99964426c0Christian Maeder printText0 ga diag =
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder let gs (n, dn) =
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder (n, getSig $ dn_sig dn)
8e9c3881fb6e710b1e08bf5ac8ff9d393df2e74eChristian Maeder in ptext "nodes: "
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang <+> (printText0 ga (map gs (labNodes diag)))
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder <+> ptext "\nedges: "
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder <+> (printText0 ga (edges diag))
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski-- * Functions
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder-- | Pretty print the diagram
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederprintDiag :: a -> String -> Diag -> Result a
90c174bac60a72ffd81bc3bf5ae2dd9a61943b8bChristian Maeder--printDiag res t diag = warning res (showPretty diag t) nullRange
2561b4bfc45d280ee2be8a7870314670e4e682e4Christian MaederprintDiag res _ _ = do return res
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder-- | A mapping from extended to basic static unit context
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettichctx :: ExtStUnitCtx -> StUnitCtx
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maederctx (buc, _) =
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski let ctx' [] _ = emptyStUnitCtx
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder ctx' (id1 : ids) buc0 =
c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu let uctx = ctx' ids buc0
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder in case Map.lookup id1 buc0 of
986d3f255182539098a97ac86da9eeee5b7a72e3Christian Maeder Just (Based_unit_sig mds) -> Map.insert id1
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder (Sig $ getSigFromDiag mds) uctx
8e80792f474d154ff11762fac081a422e34f1accChristian Maeder Just (Based_par_unit_sig mds usig) -> Map.insert id1
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (Imp_unit_sig (toMaybeNode mds) usig) uctx
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder _ -> uctx -- this should never be the case
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder in ctx' (Map.keys buc) buc
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder-- | Insert the edges from given source nodes to given target node
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder-- into the given diagram. The edges are labelled with inclusions.
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian MaederinsInclusionEdges :: LogicGraph
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder -> Diag -- ^ the diagram to which the edges should be inserted
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder -> [DiagNodeSig] -- ^ the source nodes
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder -> DiagNodeSig -- ^ the target node
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder -> Result Diag
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder-- ^ returns the diagram with edges inserted
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian MaederinsInclusionEdges lgraph diag0 srcNodes (Diag_node_sig tn tnsig) =
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder do let inslink diag dns = do d <- diag
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder Diag_node_sig n nsig ->
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder do incl <- ginclusion lgraph (getSig nsig) (getSig tnsig)
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder return (insEdge (n, tn, DiagLink { dl_morphism = incl }) d)
e6dccba746efe07338d3107fed512e713fd50b28Christian Maeder diag' <- foldl inslink (return diag0) srcNodes
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder-- | Insert the edges from given source node to given target nodes
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder-- into the given diagram. The edges are labelled with inclusions.
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian MaederinsInclusionEdgesRev :: LogicGraph
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder -> Diag -- ^ the diagram to which the edges should be inserted
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder -> DiagNodeSig -- ^ the source node
9a6779c8495854bdf36e4a87f98f095e8d0a6e45Christian Maeder -> [DiagNodeSig] -- ^ the target nodes
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder -> Result Diag
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder-- ^ returns the diagram with edges inserted
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian MaederinsInclusionEdgesRev lgraph diag0 (Diag_node_sig sn snsig) targetNodes =
656f17ae9b7610ff2de1b6eedeeadea0c3bcdc8dChristian Maeder do let inslink diag dns = do d <- diag
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder Diag_node_sig n nsig ->
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder do incl <- ginclusion lgraph (getSig snsig) (getSig nsig)
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder return (insEdge (sn, n, DiagLink { dl_morphism = incl }) d)
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder diag' <- foldl inslink (return diag0) targetNodes
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder-- | Build a diagram that extends given diagram with a node containing
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder-- given signature and with edges from given set of nodes to the new node.
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder-- The new edges are labelled with sigature inclusions.
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian MaederextendDiagramIncl :: LogicGraph
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder -> Diag -- ^ the diagram to be extended
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder -> [DiagNodeSig] -- ^ the nodes which should be linked to the new node
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder -> NodeSig -- ^ the signature with which the new node should be labelled
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder -> String -- ^ the node description (for diagnostics)
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder -> Result (DiagNodeSig, Diag)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder-- ^ returns the new node and the extended diagram
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaederextendDiagramIncl lgraph diag srcNodes newNodeSig desc =
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder do let nodeContents = DiagNode {dn_sig = newNodeSig, dn_desc = desc}
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder node = getNewNode diag
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder diag' = insNode (node, nodeContents) diag
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder newDiagNode = Diag_node_sig node newNodeSig
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder diag'' <- insInclusionEdges lgraph diag' srcNodes newDiagNode
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder printDiag (newDiagNode, diag'') "extendDiagramIncl" diag''
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder return (newDiagNode, diag'')
fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder-- | Build a diagram that extends given diagram with a node and an
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder-- edge to that node. The edge is labelled with given signature morphism and
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder-- the node contains the target of this morphism. Extends the development graph
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder-- with given morphis as well.
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian MaederextendDiagramWithMorphism :: Range -- ^ the position (for diagnostics)
6a22b2854c3bc9cb4877cb7d29049d6559238639Christian Maeder -> LogicGraph
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder -> Diag -- ^ the diagram to be extended
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder -> DGraph -- ^ the development graph
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -> DiagNodeSig -- ^ the node from which the edge should originate
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder -> GMorphism -- ^ the morphism with which the new edge should be labelled
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -> String -- ^ the node description (for diagnostics)
4e14c1bc2b97679b84c6ad996fa11c273b74ea02Christian Maeder -> DGOrigin -- ^ the origin of the new node
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -> Result (DiagNodeSig, Diag, DGraph)
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder-- ^ returns the new node, the extended diagram and extended development graph
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaederextendDiagramWithMorphism pos _ diag dg (Diag_node_sig n nsig) morph desc orig =
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder if (getSig nsig) == (dom Grothendieck morph) then
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder do (targetSig, dg') <- extendDGraph dg nsig morph orig
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder let nodeContents = DiagNode {dn_sig = targetSig, dn_desc = desc}
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder node = getNewNode diag
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder diag' = insNode (node, nodeContents) diag
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder diag'' = insEdge (n, node, DiagLink { dl_morphism = morph }) diag'
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder printDiag (Diag_node_sig node targetSig, diag'', dg') "extendDiagramWithMorphism" diag''
26d11a256b1433604a3dbc69913b520fff7586acChristian Maeder return (Diag_node_sig node targetSig, diag'', dg')
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder else do fatal_error ("Internal error: Static.AnalysisArchitecture.extendDiagramWithMorphism: the morphism domain differs from the signature in given source node")
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder-- | Build a diagram that extends given diagram with a node and an
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder-- edge from that node. The edge is labelled with given signature morphism and
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder-- the node contains the source of this morphism. Extends the development graph
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder-- with given morphis as well.
b5056cf24da461ee868c4be7b803a76b677fa21dChristian MaederextendDiagramWithMorphismRev :: Range -- ^ the position (for diagnostics)
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder -> LogicGraph
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder -> Diag -- ^ the diagram to be extended
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder -> DGraph -- ^ the development graph
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder -> DiagNodeSig -- ^ the node to which the edge should point
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder -> GMorphism -- ^ the morphism with which the new edge should be labelled
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder -> String -- ^ the node description (for diagnostics)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder -> DGOrigin -- ^ the origin of the new node
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder -> Result (DiagNodeSig, Diag, DGraph)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder-- ^ returns the new node, the extended diagram and extended development graph
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederextendDiagramWithMorphismRev pos _ diag dg (Diag_node_sig n nsig) morph desc orig =
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder if (getSig nsig) == (cod Grothendieck morph) then
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder do (sourceSig, dg') <- extendDGraphRev dg nsig morph orig
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder let nodeContents = DiagNode {dn_sig = sourceSig, dn_desc = desc}
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder node = getNewNode diag
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder diag' = insNode (node, nodeContents) diag
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder diag'' = insEdge (node, n, DiagLink { dl_morphism = morph }) diag'
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski printDiag (Diag_node_sig node sourceSig, diag'', dg') "extendDiagramWithMorphismRev" diag''
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder return (Diag_node_sig node sourceSig, diag'', dg')
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder else do fatal_error ("Internal error: Static.AnalysisArchitecture.extendDiagramWithMorphismRev: the morphism codomain differs from the signature in given target node")
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder-- | Build a diagram that extends given diagram with a node containing
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder-- given signature and with edge from given nodes to the new node.
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder-- The new edge is labelled with given signature morphism.
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst SchulzextendDiagram :: Diag -- ^ the diagram to be extended
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder -> DiagNodeSig -- ^ the node from which morphism originates
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder -> GMorphism -- ^ the morphism with which new edge should be labelled
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz -> NodeSig -- ^ the signature with which the new node should be labelled
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder -> String -- ^ the node description (for diagnostics)
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder -> Result (DiagNodeSig, Diag)
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder-- ^ returns the new node and the extended diagram
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian MaederextendDiagram diag (Diag_node_sig n _) edgeMorph newNodeSig desc =
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder do let nodeContents = DiagNode {dn_sig = newNodeSig, dn_desc = desc}
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder node = getNewNode diag
4e3c46a1ca40d50a045342c5fab25b5db4fa9a87Christian Maeder diag' = insNode (node, nodeContents) diag
4e3c46a1ca40d50a045342c5fab25b5db4fa9a87Christian Maeder diag'' = insEdge (n, node, DiagLink { dl_morphism = edgeMorph }) diag'
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder newDiagNode = Diag_node_sig node newNodeSig
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder printDiag (newDiagNode, diag'') "extendDiagram" diag''
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz return (newDiagNode, diag'')
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz-- | Convert a homogeneous diagram to a simple diagram where
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz-- all the signatures in nodes and morphism on the edges are
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder-- coerced to a common logic.
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian MaederhomogeniseDiagram :: Logic lid sublogics
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder basic_spec sentence symb_items symb_map_items
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder sign morphism symbol raw_symbol proof_tree
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder => lid -- ^ the target logic to which signatures and morphisms will be coerced
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder -> Diag -- ^ the diagram to be homogenised
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder -> Result (Tree.Gr sign morphism)
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian MaederhomogeniseDiagram targetLid diag =
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder -- The implementation relies on the representation of graph nodes as
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder -- integers. We can therefore just obtain a list of all the labelled nodes
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder -- from diag, convert all the nodes and insert them to a new diagram; then
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder -- copy all the edges from the original to new diagram (coercing the morphisms).
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder do let convertNode (n, dn) =
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder do G_sign srcLid sig <- return $ getSig $ dn_sig dn
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder sig' <- coerceSign srcLid targetLid "" sig
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder return (n, sig')
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder convertEdge (n1, n2, DiagLink { dl_morphism = GMorphism cid _ mor }) =
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder if isIdComorphism (Comorphism cid) then
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder do mor' <- coerceMorphism (targetLogic cid) targetLid "" mor
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder return (n1, n2, mor')
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder else do fatal_error "Trying to coerce a morphism between different logics. Heterogeneous specifications are not fully supported yet."
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder convertNodes cDiag [] = do return cDiag
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder convertNodes cDiag (lNode : lNodes) =
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder do convNode <- convertNode lNode
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder let cDiag' = insNode convNode cDiag
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder convertNodes cDiag' lNodes
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder convertEdges cDiag [] = do return cDiag
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder convertEdges cDiag (lEdge : lEdges) =
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder do convEdge <- convertEdge lEdge
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder let cDiag' = insEdge convEdge cDiag
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder convertEdges cDiag' lEdges
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder dNodes = labNodes diag
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder dEdges = labEdges diag
4e144aa4be1f50519f8fa377a7883edfbc76d406Christian Maeder -- insert converted nodes to an empty diagram
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder cDiag <- convertNodes Graph.empty dNodes
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder -- insert converted edges to the diagram containing only nodes
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder cDiag' <- convertEdges cDiag dEdges
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder return cDiag'
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder-- | Coerce GMorphisms in the list of (diagram node, GMorphism) pairs
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder-- to morphisms in given logic
8cceb39f451593f3904acbf9d64bea6af9860b57Christian MaederhomogeniseSink :: Logic lid sublogics
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder basic_spec sentence symb_items symb_map_items
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder sign morphism symbol raw_symbol proof_tree
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder => lid -- ^ the target logic to which morphisms will be coerced
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder -> [(Node, GMorphism)] -- ^ the list of edges to be homogenised
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder -> Result [(Node, morphism)]
8cceb39f451593f3904acbf9d64bea6af9860b57Christian MaederhomogeniseSink targetLid dEdges =
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder -- See homogeniseDiagram for comments on implementation.
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder do let convertMorphism (n, GMorphism cid _ mor) =
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder if isIdComorphism (Comorphism cid) then
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder do mor' <- coerceMorphism (targetLogic cid) targetLid "" mor
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder return (n, mor')
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder else do fatal_error "Trying to coerce a morphism between different logics. Heterogeneous specifications are not fully supported yet."
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder convEdges [] = do return []
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder convEdges (e : es) = do ce <- convertMorphism e
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder ces <- convEdges es
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder return (ce : ces)
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder convEdges dEdges
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder-- | Create a graph containing descriptions of nodes and edges.
99476ac2689c74251219db4782e57fe713a24a52Christian MaederdiagDesc :: Diag
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder -> Tree.Gr String String
99476ac2689c74251219db4782e57fe713a24a52Christian MaederdiagDesc diag =
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder let insNodeDesc g (n, DiagNode { dn_desc = desc }) =
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder if desc == "" then g else insNode (n, desc) g
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder in foldl insNodeDesc Graph.empty (labNodes diag)
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder-- | Create a sink consisting of incusion morphisms between
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder-- signatures from given set of nodes and given signature.
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian MaederinclusionSink :: LogicGraph
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder -> [DiagNodeSig] -- ^ the source nodes
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder -> NodeSig -- ^ the target signature
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder -> Result [(Node, GMorphism)]
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder-- ^ returns the diagram with edges inserted
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian MaederinclusionSink lgraph srcNodes tnsig =
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder do let insmorph ls dns = do l <- ls
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder Diag_node_sig n nsig ->
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder do incl <- ginclusion lgraph (getSig nsig) (getSig tnsig)
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder return ((n, incl): l)
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder sink <- foldl insmorph (return []) srcNodes