4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder{- |

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederModule : $Header$

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederCopyright : (c) Maciek Makowski, Warsaw University 2004-2006

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

f3cd81f98592d1dbf301f48af31677a6a0cc666aChristian Maeder

eca29a7be76eb73944ec19b06eda3d6a9e6e543dChristian MaederMaintainer : till@tzi.de

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederStability : provisional

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederPortability : non-portable (Logic)

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder

f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederData types and functions for architectural diagrams.

f3cd81f98592d1dbf301f48af31677a6a0cc666aChristian Maeder Follows the CASL Reference Manual, section III.5.6.

f3cd81f98592d1dbf301f48af31677a6a0cc666aChristian Maeder-}

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder

f3cd81f98592d1dbf301f48af31677a6a0cc666aChristian Maedermodule Static.ArchDiagram where

1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maeder

1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maederimport Logic.Comorphism

1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maederimport Logic.Logic

1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maederimport Logic.Grothendieck

23f8d286586ff38a9e73052b2c7c04c62c5c638fChristian Maederimport Logic.Coerce

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maederimport Data.Graph.Inductive.Graph as Graph

1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maederimport qualified Common.Lib.Graph as Tree

1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maeder

1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maederimport qualified Common.Lib.Map as Map

1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maederimport Common.Lib.Pretty

62925f4a144f45b5ed1e7c841f891d13f51e553dChristian Maederimport Common.PrettyPrint

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maederimport Common.Result

53301de22afd7190981b363b57c48df86fcb50f7Christian Maederimport Common.Id

cdaff0507c1b7240e2660dbb311f9c4646a6d14aChristian Maeder

f3cd81f98592d1dbf301f48af31677a6a0cc666aChristian Maederimport Static.DevGraph

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder

d17834302eaa101395b4b806cd73670fd864445fChristian Maeder-- * Types

0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian Maeder-- (as defined for extended static semantics in Chap. III:5.6.1)

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maederdata DiagNodeLab = DiagNode { dn_sig :: NodeSig,

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder dn_desc :: String }

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maederdata DiagLinkLab = DiagLink { dl_morphism :: GMorphism }

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder

836e72a3c413366ba9801726f3b249c7791cb9caChristian Maedertype Diag = Tree.Gr DiagNodeLab DiagLinkLab

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian MaederemptyDiag :: Diag

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaederemptyDiag = Graph.empty

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maederdata DiagNodeSig = Diag_node_sig Node NodeSig

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maederdata MaybeDiagNode = JustDiagNode DiagNodeSig

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder | EmptyDiagNode AnyLogic

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaedertoMaybeNode :: MaybeDiagNode -> MaybeNode

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaedertoMaybeNode mdn = case mdn of

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder JustDiagNode dns -> JustNode $ getSigFromDiag dns

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder EmptyDiagNode l -> EmptyNode l

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder

53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder-- | Return a signature stored within given diagram node sig

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaedergetSigFromDiag :: DiagNodeSig -> NodeSig

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaedergetSigFromDiag (Diag_node_sig _ ns) = ns

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maederdata BasedUnitSig = Based_unit_sig DiagNodeSig

fa45d098e1c9d468f128be9505eb7e5b2705b304Christian Maeder | Based_par_unit_sig MaybeDiagNode UnitSig

25612a7b3ce708909298d5426406592473880a20Christian Maeder

c1db3d36c29a6324745a86dbcba18b8e4cd9f338Christian Maedertype StBasedUnitCtx = Map.Map SIMPLE_ID BasedUnitSig

c1db3d36c29a6324745a86dbcba18b8e4cd9f338Christian MaederemptyStBasedUnitCtx :: StBasedUnitCtx

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaederemptyStBasedUnitCtx = Map.empty

c1db3d36c29a6324745a86dbcba18b8e4cd9f338Christian Maeder

25612a7b3ce708909298d5426406592473880a20Christian Maeder-- Since Ps and Bs in the definition of ExtStUnitCtx have disjoint domains

25612a7b3ce708909298d5426406592473880a20Christian Maeder-- we can merge them into a single mapping represented by StBasedUnitCtx.

c1db3d36c29a6324745a86dbcba18b8e4cd9f338Christian Maedertype ExtStUnitCtx = (StBasedUnitCtx, Diag)

18b709ce961d68328da768318dcc70067f066d86Christian MaederemptyExtStUnitCtx :: ExtStUnitCtx

18b709ce961d68328da768318dcc70067f066d86Christian MaederemptyExtStUnitCtx = (emptyStBasedUnitCtx, emptyDiag)

18b709ce961d68328da768318dcc70067f066d86Christian Maeder

18b709ce961d68328da768318dcc70067f066d86Christian Maeder

18b709ce961d68328da768318dcc70067f066d86Christian Maeder-- * Instances

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

18b709ce961d68328da768318dcc70067f066d86Christian Maeder-- PrettyPrint

18b709ce961d68328da768318dcc70067f066d86Christian Maederinstance PrettyPrint Diag where

18b709ce961d68328da768318dcc70067f066d86Christian Maeder printText0 ga diag =

b814fecd0a2dbdeae62402903783d08e4206b4d2Christian Maeder let gs (n, dn) =

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder (n, getSig $ dn_sig dn)

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder in ptext "nodes: "

18b709ce961d68328da768318dcc70067f066d86Christian Maeder <+> (printText0 ga (map gs (labNodes diag)))

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder <+> ptext "\nedges: "

18b709ce961d68328da768318dcc70067f066d86Christian Maeder <+> (printText0 ga (edges diag))

9c5b1136299d9052e4e995614a3a36a051a2682fChristian Maeder

18b709ce961d68328da768318dcc70067f066d86Christian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder-- * Functions

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

9c5b1136299d9052e4e995614a3a36a051a2682fChristian Maeder-- | Pretty print the diagram

9c5b1136299d9052e4e995614a3a36a051a2682fChristian MaederprintDiag :: a -> String -> Diag -> Result a

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder--printDiag res t diag = warning res (showPretty diag t) nullRange

76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian MaederprintDiag res _ _ = do return res

9c5b1136299d9052e4e995614a3a36a051a2682fChristian Maeder

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder-- | A mapping from extended to basic static unit context

797f811e57952d59e73b8cd03b667eef276db972Christian Maederctx :: ExtStUnitCtx -> StUnitCtx

18b709ce961d68328da768318dcc70067f066d86Christian Maederctx (buc, _) =

fe5dbb45b6a8abf34375b4bc5f2a81cda664c0e4Christian Maeder let ctx' [] _ = emptyStUnitCtx

797f811e57952d59e73b8cd03b667eef276db972Christian Maeder ctx' (id1 : ids) buc0 =

797f811e57952d59e73b8cd03b667eef276db972Christian Maeder let uctx = ctx' ids buc0

18b709ce961d68328da768318dcc70067f066d86Christian Maeder in case Map.lookup id1 buc0 of

18b709ce961d68328da768318dcc70067f066d86Christian Maeder Just (Based_unit_sig mds) -> Map.insert id1

369454f9b2dbea113cbb40544a9b0f31425b2c69Christian Maeder (Sig $ getSigFromDiag mds) uctx

fe5dbb45b6a8abf34375b4bc5f2a81cda664c0e4Christian Maeder Just (Based_par_unit_sig mds usig) -> Map.insert id1

18b709ce961d68328da768318dcc70067f066d86Christian Maeder (Imp_unit_sig (toMaybeNode mds) usig) uctx

18b709ce961d68328da768318dcc70067f066d86Christian Maeder _ -> uctx -- this should never be the case

18b709ce961d68328da768318dcc70067f066d86Christian Maeder in ctx' (Map.keys buc) buc

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder

3f7009c892b16d172314abbba83d663fa0d87a65Christian Maeder

369454f9b2dbea113cbb40544a9b0f31425b2c69Christian Maeder

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder-- | Insert the edges from given source nodes to given target node

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder-- into the given diagram. The edges are labelled with inclusions.

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaederinsInclusionEdges :: LogicGraph

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder -> Diag -- ^ the diagram to which the edges should be inserted

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder -> [DiagNodeSig] -- ^ the source nodes

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder -> DiagNodeSig -- ^ the target node

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder -> Result Diag

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder-- ^ returns the diagram with edges inserted

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaederinsInclusionEdges lgraph diag0 srcNodes (Diag_node_sig tn tnsig) =

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder do let inslink diag dns = do d <- diag

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder case dns of

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder Diag_node_sig n nsig ->

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder do incl <- ginclusion lgraph (getSig nsig) (getSig tnsig)

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder return (insEdge (n, tn, DiagLink { dl_morphism = incl }) d)

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder diag' <- foldl inslink (return diag0) srcNodes

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder return diag'

dfa74d066ea0f00a70276aedecc624c6b3c86deaChristian Maeder

dfa74d066ea0f00a70276aedecc624c6b3c86deaChristian Maeder

9c5b1136299d9052e4e995614a3a36a051a2682fChristian Maeder-- | Insert the edges from given source node to given target nodes

9c5b1136299d9052e4e995614a3a36a051a2682fChristian Maeder-- into the given diagram. The edges are labelled with inclusions.

9c5b1136299d9052e4e995614a3a36a051a2682fChristian MaederinsInclusionEdgesRev :: LogicGraph

9c5b1136299d9052e4e995614a3a36a051a2682fChristian Maeder -> Diag -- ^ the diagram to which the edges should be inserted

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder -> DiagNodeSig -- ^ the source node

9c5b1136299d9052e4e995614a3a36a051a2682fChristian Maeder -> [DiagNodeSig] -- ^ the target nodes

369454f9b2dbea113cbb40544a9b0f31425b2c69Christian Maeder -> Result Diag

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder-- ^ returns the diagram with edges inserted

9c5b1136299d9052e4e995614a3a36a051a2682fChristian MaederinsInclusionEdgesRev lgraph diag0 (Diag_node_sig sn snsig) targetNodes =

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder do let inslink diag dns = do d <- diag

f8f78a2c8796a387a4348cc672ae08e8d9f69315Christian Maeder case dns of

f8f78a2c8796a387a4348cc672ae08e8d9f69315Christian Maeder Diag_node_sig n nsig ->

f8f78a2c8796a387a4348cc672ae08e8d9f69315Christian Maeder do incl <- ginclusion lgraph (getSig snsig) (getSig nsig)

f8f78a2c8796a387a4348cc672ae08e8d9f69315Christian Maeder return (insEdge (sn, n, DiagLink { dl_morphism = incl }) d)

fcec1ffa4a95dbc47cf23f75e6843ceff93a925eChristian Maeder diag' <- foldl inslink (return diag0) targetNodes

fcec1ffa4a95dbc47cf23f75e6843ceff93a925eChristian Maeder return diag'

fcec1ffa4a95dbc47cf23f75e6843ceff93a925eChristian Maeder

c64d33a7fbeae730cbe65193fe3cc24e7aa1ddd6Christian Maeder

53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder-- | Build a diagram that extends given diagram with a node containing

fcec1ffa4a95dbc47cf23f75e6843ceff93a925eChristian Maeder-- given signature and with edges from given set of nodes to the new node.

fcec1ffa4a95dbc47cf23f75e6843ceff93a925eChristian Maeder-- The new edges are labelled with sigature inclusions.

fcec1ffa4a95dbc47cf23f75e6843ceff93a925eChristian MaederextendDiagramIncl :: LogicGraph

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder -> Diag -- ^ the diagram to be extended

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder -> [DiagNodeSig] -- ^ the nodes which should be linked to the new node

dfa74d066ea0f00a70276aedecc624c6b3c86deaChristian Maeder -> NodeSig -- ^ the signature with which the new node should be labelled

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder -> String -- ^ the node description (for diagnostics)

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder -> Result (DiagNodeSig, Diag)

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder-- ^ returns the new node and the extended diagram

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaederextendDiagramIncl lgraph diag srcNodes newNodeSig desc =

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder do let nodeContents = DiagNode {dn_sig = newNodeSig, dn_desc = desc}

fcec1ffa4a95dbc47cf23f75e6843ceff93a925eChristian Maeder node = getNewNode diag

fcec1ffa4a95dbc47cf23f75e6843ceff93a925eChristian Maeder diag' = insNode (node, nodeContents) diag

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder newDiagNode = Diag_node_sig node newNodeSig

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder diag'' <- insInclusionEdges lgraph diag' srcNodes newDiagNode

fcec1ffa4a95dbc47cf23f75e6843ceff93a925eChristian Maeder printDiag (newDiagNode, diag'') "extendDiagramIncl" diag''

fcec1ffa4a95dbc47cf23f75e6843ceff93a925eChristian Maeder return (newDiagNode, diag'')

f8f78a2c8796a387a4348cc672ae08e8d9f69315Christian Maeder

2f3c4316d3979a76918f0a93206b9dc75d46a1d4Christian Maeder

2f3c4316d3979a76918f0a93206b9dc75d46a1d4Christian Maeder-- | Build a diagram that extends given diagram with a node and an

2f3c4316d3979a76918f0a93206b9dc75d46a1d4Christian Maeder-- edge to that node. The edge is labelled with given signature morphism and

f8a03685d9184046e88e1d76aabdab4f714db440Christian Maeder-- the node contains the target of this morphism. Extends the development graph

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder-- with given morphis as well.

f8a03685d9184046e88e1d76aabdab4f714db440Christian MaederextendDiagramWithMorphism :: Range -- ^ the position (for diagnostics)

2f3c4316d3979a76918f0a93206b9dc75d46a1d4Christian Maeder -> LogicGraph

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder -> Diag -- ^ the diagram to be extended

2f3c4316d3979a76918f0a93206b9dc75d46a1d4Christian Maeder -> DGraph -- ^ the development graph

2f3c4316d3979a76918f0a93206b9dc75d46a1d4Christian Maeder -> DiagNodeSig -- ^ the node from which the edge should originate

2f3c4316d3979a76918f0a93206b9dc75d46a1d4Christian Maeder -> GMorphism -- ^ the morphism with which the new edge should be labelled

-> String -- ^ the node description (for diagnostics)

-> DGOrigin -- ^ the origin of the new node

-> Result (DiagNodeSig, Diag, DGraph)

-- ^ returns the new node, the extended diagram and extended development graph

extendDiagramWithMorphism pos _ diag dg (Diag_node_sig n nsig) morph desc orig =

if (getSig nsig) == (dom Grothendieck morph) then

do (targetSig, dg') <- extendDGraph dg nsig morph orig

let nodeContents = DiagNode {dn_sig = targetSig, dn_desc = desc}

node = getNewNode diag

diag' = insNode (node, nodeContents) diag

diag'' = insEdge (n, node, DiagLink { dl_morphism = morph }) diag'

printDiag (Diag_node_sig node targetSig, diag'', dg') "extendDiagramWithMorphism" diag''

return (Diag_node_sig node targetSig, diag'', dg')

else do fatal_error ("Internal error: Static.AnalysisArchitecture.extendDiagramWithMorphism: the morphism domain differs from the signature in given source node")

pos

-- | Build a diagram that extends given diagram with a node and an

-- edge from that node. The edge is labelled with given signature morphism and

-- the node contains the source of this morphism. Extends the development graph

-- with given morphis as well.

extendDiagramWithMorphismRev :: Range -- ^ the position (for diagnostics)

-> LogicGraph

-> Diag -- ^ the diagram to be extended

-> DGraph -- ^ the development graph

-> DiagNodeSig -- ^ the node to which the edge should point

-> GMorphism -- ^ the morphism with which the new edge should be labelled

-> String -- ^ the node description (for diagnostics)

-> DGOrigin -- ^ the origin of the new node

-> Result (DiagNodeSig, Diag, DGraph)

-- ^ returns the new node, the extended diagram and extended development graph

extendDiagramWithMorphismRev pos _ diag dg (Diag_node_sig n nsig) morph desc orig =

if (getSig nsig) == (cod Grothendieck morph) then

do (sourceSig, dg') <- extendDGraphRev dg nsig morph orig

let nodeContents = DiagNode {dn_sig = sourceSig, dn_desc = desc}

node = getNewNode diag

diag' = insNode (node, nodeContents) diag

diag'' = insEdge (node, n, DiagLink { dl_morphism = morph }) diag'

printDiag (Diag_node_sig node sourceSig, diag'', dg') "extendDiagramWithMorphismRev" diag''

return (Diag_node_sig node sourceSig, diag'', dg')

else do fatal_error ("Internal error: Static.AnalysisArchitecture.extendDiagramWithMorphismRev: the morphism codomain differs from the signature in given target node")

pos

-- | Build a diagram that extends given diagram with a node containing

-- given signature and with edge from given nodes to the new node.

-- The new edge is labelled with given signature morphism.

extendDiagram :: Diag -- ^ the diagram to be extended

-> DiagNodeSig -- ^ the node from which morphism originates

-> GMorphism -- ^ the morphism with which new edge should be labelled

-> NodeSig -- ^ the signature with which the new node should be labelled

-> String -- ^ the node description (for diagnostics)

-> Result (DiagNodeSig, Diag)

-- ^ returns the new node and the extended diagram

extendDiagram diag (Diag_node_sig n _) edgeMorph newNodeSig desc =

do let nodeContents = DiagNode {dn_sig = newNodeSig, dn_desc = desc}

node = getNewNode diag

diag' = insNode (node, nodeContents) diag

diag'' = insEdge (n, node, DiagLink { dl_morphism = edgeMorph }) diag'

newDiagNode = Diag_node_sig node newNodeSig

printDiag (newDiagNode, diag'') "extendDiagram" diag''

return (newDiagNode, diag'')

-- | Convert a homogeneous diagram to a simple diagram where

-- all the signatures in nodes and morphism on the edges are

-- coerced to a common logic.

homogeniseDiagram :: Logic lid sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree

=> lid -- ^ the target logic to which signatures and morphisms will be coerced

-> Diag -- ^ the diagram to be homogenised

-> Result (Tree.Gr sign morphism)

homogeniseDiagram targetLid diag =

-- The implementation relies on the representation of graph nodes as

-- integers. We can therefore just obtain a list of all the labelled nodes

-- from diag, convert all the nodes and insert them to a new diagram; then

-- copy all the edges from the original to new diagram (coercing the morphisms).

do let convertNode (n, dn) =

do G_sign srcLid sig <- return $ getSig $ dn_sig dn

sig' <- coerceSign srcLid targetLid "" sig

return (n, sig')

convertEdge (n1, n2, DiagLink { dl_morphism = GMorphism cid _ mor }) =

if isIdComorphism (Comorphism cid) then

do mor' <- coerceMorphism (targetLogic cid) targetLid "" mor

return (n1, n2, mor')

else do fatal_error "Trying to coerce a morphism between different logics. Heterogeneous specifications are not fully supported yet."

nullRange

convertNodes cDiag [] = do return cDiag

convertNodes cDiag (lNode : lNodes) =

do convNode <- convertNode lNode

let cDiag' = insNode convNode cDiag

convertNodes cDiag' lNodes

convertEdges cDiag [] = do return cDiag

convertEdges cDiag (lEdge : lEdges) =

do convEdge <- convertEdge lEdge

let cDiag' = insEdge convEdge cDiag

convertEdges cDiag' lEdges

dNodes = labNodes diag

dEdges = labEdges diag

-- insert converted nodes to an empty diagram

cDiag <- convertNodes Graph.empty dNodes

-- insert converted edges to the diagram containing only nodes

cDiag' <- convertEdges cDiag dEdges

return cDiag'

-- | Coerce GMorphisms in the list of (diagram node, GMorphism) pairs

-- to morphisms in given logic

homogeniseSink :: Logic lid sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree

=> lid -- ^ the target logic to which morphisms will be coerced

-> [(Node, GMorphism)] -- ^ the list of edges to be homogenised

-> Result [(Node, morphism)]

homogeniseSink targetLid dEdges =

-- See homogeniseDiagram for comments on implementation.

do let convertMorphism (n, GMorphism cid _ mor) =

if isIdComorphism (Comorphism cid) then

do mor' <- coerceMorphism (targetLogic cid) targetLid "" mor

return (n, mor')

else do fatal_error "Trying to coerce a morphism between different logics. Heterogeneous specifications are not fully supported yet."

nullRange

convEdges [] = do return []

convEdges (e : es) = do ce <- convertMorphism e

ces <- convEdges es

return (ce : ces)

convEdges dEdges

-- | Create a graph containing descriptions of nodes and edges.

diagDesc :: Diag

-> Tree.Gr String String

diagDesc diag =

let insNodeDesc g (n, DiagNode { dn_desc = desc }) =

if desc == "" then g else insNode (n, desc) g

in foldl insNodeDesc Graph.empty (labNodes diag)

-- | Create a sink consisting of incusion morphisms between

-- signatures from given set of nodes and given signature.

inclusionSink :: LogicGraph

-> [DiagNodeSig] -- ^ the source nodes

-> NodeSig -- ^ the target signature

-> Result [(Node, GMorphism)]

-- ^ returns the diagram with edges inserted

inclusionSink lgraph srcNodes tnsig =

do let insmorph ls dns = do l <- ls

case dns of

Diag_node_sig n nsig ->

do incl <- ginclusion lgraph (getSig nsig) (getSig tnsig)

return ((n, incl): l)

sink <- foldl insmorph (return []) srcNodes

return sink