ArchDiagram.hs revision ae8052003e1ec7247597f034069db0939a7387e1
8267b99c0d7a187abe6f87ad50530dc08f5d1cdcAndy GimblettModule : $Header$
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettCopyright : (c) Maciek Makowski, Warsaw University 2004-2006
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachMaintainer : till@tzi.de
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettStability : provisional
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachPortability : non-portable (Logic)
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachData types and functions for architectural diagrams.
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett Follows the CASL Reference Manual, section III.5.6.
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblettimport qualified Common.Lib.Graph as Tree
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reillyimport qualified Common.Lib.Map as Map
1538a6e8d77301d6de757616ffc69ee61f1482e4Andy Gimblett-- (as defined for extended static semantics in Chap. III:5.6.1)
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachdata DiagNodeLab = DiagNode { dn_sig :: NodeSig, dn_desc :: String }
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder deriving Show
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reillydata DiagLinkLab = DiagLink { dl_morphism :: GMorphism }
0ea916d1e6aea10fd7b84f802fb5148a79d8c20aAndy Gimbletttype Diag = Tree.Gr DiagNodeLab DiagLinkLab
04ceed96d1528b939f2e592d0656290d81d1c045Andy GimblettemptyDiag :: Diag
06dd4e7c29f33f6122a910719e3bd9062256e397Andy Gimblettdata DiagNodeSig = Diag_node_sig Node NodeSig
c4b2418421546a337f83332fe0db04742dcd735dAndy Gimblettdata MaybeDiagNode = JustDiagNode DiagNodeSig | EmptyDiagNode AnyLogic
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillytoMaybeNode :: MaybeDiagNode -> MaybeNode
e54c5af823b9775dd2c058185ea5bdf7593950faAndy GimbletttoMaybeNode mdn = case mdn of
5858e6262048894b0e933b547852f04aed009b58Andy Gimblett JustDiagNode dns -> JustNode $ getSigFromDiag dns
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly EmptyDiagNode l -> EmptyNode l
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder-- | Return a signature stored within given diagram node sig
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian MaedergetSigFromDiag :: DiagNodeSig -> NodeSig
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian MaedergetSigFromDiag (Diag_node_sig _ ns) = ns
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maederdata BasedUnitSig = Based_unit_sig DiagNodeSig
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly | Based_par_unit_sig MaybeDiagNode UnitSig
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reillytype StBasedUnitCtx = Map.Map SIMPLE_ID BasedUnitSig
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillyemptyStBasedUnitCtx :: StBasedUnitCtx
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillyemptyStBasedUnitCtx = Map.empty
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly-- Since Ps and Bs in the definition of ExtStUnitCtx have disjoint domains
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly-- we can merge them into a single mapping represented by StBasedUnitCtx.
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimbletttype ExtStUnitCtx = (StBasedUnitCtx, Diag)
e54c5af823b9775dd2c058185ea5bdf7593950faAndy GimblettemptyExtStUnitCtx :: ExtStUnitCtx
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy GimblettemptyExtStUnitCtx = (emptyStBasedUnitCtx, emptyDiag)
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblettinstance Pretty Diag where
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett pretty diag =
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett let gs (n, dn) =
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett (n, getSig $ dn_sig dn)
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett in text "nodes:"
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett <+> sepByCommas (map (pretty . gs) $ labNodes diag)
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett $+$ text "edges:"
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett <+> ppWithCommas (edges diag)
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett-- * Functions
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett-- | return the diagram
61051521e4d82769a47f23aecb5fb477de47d534Andy GimblettprintDiag :: a -> String -> Diag -> Result a
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettprintDiag res _ _ = return res
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett-- | A mapping from extended to basic static unit context
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblettctx :: ExtStUnitCtx -> StUnitCtx
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblettctx (buc, _) =
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett let ctx' [] _ = emptyStUnitCtx
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett ctx' (id1 : ids) buc0 =
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett let uctx = ctx' ids buc0
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett in case Map.lookup id1 buc0 of
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett Just (Based_unit_sig mds) -> Map.insert id1
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett (Sig $ getSigFromDiag mds) uctx
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly Just (Based_par_unit_sig mds usig) -> Map.insert id1
fbc0c2baf563fe5b664f0152674a8d3acecca58cAndy Gimblett (Imp_unit_sig (toMaybeNode mds) usig) uctx
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett _ -> uctx -- this should never be the case
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett in ctx' (Map.keys buc) buc
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett-- | Insert the edges from given source nodes to given target node
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett-- into the given diagram. The edges are labelled with inclusions.
820947bd01ca952c3909eaa0366c6914c87cc1cbTill MossakowskiinsInclusionEdges :: LogicGraph
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett -> Diag -- ^ the diagram to insert edges to
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett -> [DiagNodeSig] -- ^ the source nodes
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett -> DiagNodeSig -- ^ the target node
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly -> Result Diag -- ^ the diagram with edges inserted
90047eafd2de482c67bcd13103c6064e9b0cb254Andy GimblettinsInclusionEdges lgraph diag0 srcNodes (Diag_node_sig tn tnsig) =
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett do let inslink diag dns = do
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett Diag_node_sig n nsig -> do
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett incl <- ginclusion lgraph (getSig nsig) (getSig tnsig)
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett return $ insEdge (n, tn, DiagLink { dl_morphism = incl }) d
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett diag' <- foldl inslink (return diag0) srcNodes
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett-- | Insert the edges from given source node to given target nodes
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett-- into the given diagram. The edges are labelled with inclusions.
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettinsInclusionEdgesRev :: LogicGraph
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett -> Diag -- ^ the diagram to insert edges to
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett -> DiagNodeSig -- ^ the source node
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett -> [DiagNodeSig] -- ^ the target nodes
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett -> Result Diag -- ^ the diagram with edges inserted
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettinsInclusionEdgesRev lgraph diag0 (Diag_node_sig sn snsig) targetNodes =
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett do let inslink diag dns = do
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett Diag_node_sig n nsig -> do
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach incl <- ginclusion lgraph (getSig snsig) (getSig nsig)
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett return $ insEdge (sn, n, DiagLink { dl_morphism = incl }) d
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett diag' <- foldl inslink (return diag0) targetNodes
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett{- | Build a diagram that extends given diagram with a node containing
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblettgiven signature and with edges from given set of nodes to the new
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblettnode. The new edges are labelled with sigature inclusions. -}
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettextendDiagramIncl :: LogicGraph
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett -> Diag -- ^ the diagram to be extended
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett -> [DiagNodeSig]
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett -- ^ the nodes which should be linked to the new node
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett -- ^ the signature with which the new node should be labelled
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett -> String -- ^ the node description (for diagnostics)
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett -> Result (DiagNodeSig, Diag)
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett-- ^ returns the new node and the extended diagram
31f039ffdb33d78cb31d24b71d3155b11a323975Andy GimblettextendDiagramIncl lgraph diag srcNodes newNodeSig desc =
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett do let nodeContents = DiagNode {dn_sig = newNodeSig, dn_desc = desc}
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett node = getNewNode diag
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett diag' = insNode (node, nodeContents) diag
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett newDiagNode = Diag_node_sig node newNodeSig
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett diag'' <- insInclusionEdges lgraph diag' srcNodes newDiagNode
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett printDiag (newDiagNode, diag'') "extendDiagramIncl" diag''
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett{- | Build a diagram that extends given diagram with a node and an
9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblettedge to that node. The edge is labelled with given signature morphism
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblettand the node contains the target of this morphism. Extends the
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblettdevelopment graph with given morphis as well. -}
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy GimblettextendDiagramWithMorphism :: Range -- ^ the position (for diagnostics)
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett -> LogicGraph
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett -> Diag -- ^ the diagram to be extended
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett -> DGraph -- ^ the development graph
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblett -> DiagNodeSig
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett -- ^ the node from which the edge should originate
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett -- ^ the morphism as label for the new edge
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett -> String -- ^ the node description (for diagnostics)
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett -> DGOrigin -- ^ the origin of the new node
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett -> Result (DiagNodeSig, Diag, DGraph)
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett-- ^ returns the new node, the extended diagram and extended development graph
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy GimblettextendDiagramWithMorphism pos _ diag dg (Diag_node_sig n nsig) mor desc orig =
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly if (getSig nsig) == (dom Grothendieck mor) then
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett do (targetSig, dg') <- extendDGraph dg nsig mor orig
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett let nodeContents = DiagNode {dn_sig = targetSig, dn_desc = desc}
e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett node = getNewNode diag
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly diag' = insNode (node, nodeContents) diag
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly diag'' = insEdge (n, node, DiagLink { dl_morphism = mor }) diag'
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly printDiag (Diag_node_sig node targetSig, diag'', dg')
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly "extendDiagramWithMorphism" diag''
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly else fatal_error
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly ("Internal error: Static.ArchDiagram.extendDiagramWithMorphism:" ++
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly "\n the morphism domain differs from the signature in given source node")
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly{- | Build a diagram that extends given diagram with a node and an
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reillyedge from that node. The edge is labelled with given signature
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reillymorphism and the node contains the source of this morphism. Extends
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reillythe development graph with given morphis as well. -}
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillyextendDiagramWithMorphismRev :: Range -- ^ the position (for diagnostics)
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly -> LogicGraph
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly -> Diag -- ^ the diagram to be extended
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly -> DGraph -- ^ the development graph
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly -> DiagNodeSig
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly -- ^ the node to which the edge should point
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly -- ^ the morphism as label for the new edge
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly -> String -- ^ a diagnostic node description
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly -> DGOrigin -- ^ the origin of the new node
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblett -> Result (DiagNodeSig, Diag, DGraph)
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett-- ^ returns the new node, the extended diagram and extended development graph
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettextendDiagramWithMorphismRev pos _ diag dg (Diag_node_sig n nsig)
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett mor desc orig =
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly if (getSig nsig) == (cod Grothendieck mor) then
e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett do (sourceSig, dg') <- extendDGraphRev dg nsig mor orig
e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett let nodeContents = DiagNode {dn_sig = sourceSig, dn_desc = desc}
e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett node = getNewNode diag
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly diag' = insNode (node, nodeContents) diag
e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett diag'' = insEdge (node, n, DiagLink { dl_morphism = mor }) diag'
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly printDiag (Diag_node_sig node sourceSig, diag'', dg')
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly "extendDiagramWithMorphismRev" diag''
e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett else fatal_error
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett ("Internal error: Static.ArchDiagram.extendDiagramWithMorphismRev:\n" ++
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly " the morphism codomain differs from the signature in given target node")
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly{- | Build a diagram that extends given diagram with a node containing
e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblettgiven signature and with edge from given nodes to the new node. The
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reillynew edge is labelled with given signature morphism. -}
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy GimblettextendDiagram :: Diag -- ^ the diagram to be extended
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett -> DiagNodeSig -- ^ the node from which morphism originates
fbc0c2baf563fe5b664f0152674a8d3acecca58cAndy Gimblett -> GMorphism -- ^ the morphism as label for the new edge
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly -> NodeSig -- ^ the signature as label for the new node
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly -> String -- ^ the node description (for diagnostics)
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett -> Result (DiagNodeSig, Diag)
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly-- ^ returns the new node and the extended diagram
5858e6262048894b0e933b547852f04aed009b58Andy GimblettextendDiagram diag (Diag_node_sig n _) edgeMorph newNodeSig desc =
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly do let nodeContents = DiagNode {dn_sig = newNodeSig, dn_desc = desc}
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett node = getNewNode diag
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly diag' = insNode (node, nodeContents) diag
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett diag'' = insEdge (n, node, DiagLink { dl_morphism = edgeMorph }) diag'
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett newDiagNode = Diag_node_sig node newNodeSig
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly printDiag (newDiagNode, diag'') "extendDiagram" diag''
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly{- | Convert a homogeneous diagram to a simple diagram where all the
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblettsignatures in nodes and morphism on the edges are coerced to a common
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillyhomogeniseDiagram :: Logic lid sublogics
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly basic_spec sentence symb_items symb_map_items
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett sign morphism symbol raw_symbol proof_tree
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly => lid -- ^ the target logic to be coerced to
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly -> Diag -- ^ the diagram to be homogenised
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly -> Result (Tree.Gr sign morphism)
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett{- The implementation relies on the representation of graph nodes as
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reillyintegers. We can therefore just obtain a list of all the labelled
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reillynodes from diag, convert all the nodes and insert them to a new
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reillydiagram; then copy all the edges from the original to new diagram
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett(coercing the morphisms). -}
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy GimbletthomogeniseDiagram targetLid diag =
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly do let convertNode (n, dn) =
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly do G_sign srcLid sig <- return $ getSig $ dn_sig dn
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly sig' <- coerceSign srcLid targetLid "" sig
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett return (n, sig')
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett convertEdge (n1, n2, DiagLink { dl_morphism = GMorphism cid _ mor })
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly = if isIdComorphism (Comorphism cid) then
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly do mor' <- coerceMorphism (targetLogic cid) targetLid "" mor
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly return (n1, n2, mor')
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett "Trying to coerce a morphism between different logics.\n" ++
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly "Heterogeneous specifications are not fully supported yet."
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly convertNodes cDiag [] = do return cDiag
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly convertNodes cDiag (lNode : lNodes) =
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly do convNode <- convertNode lNode
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett let cDiag' = insNode convNode cDiag
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett convertNodes cDiag' lNodes
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly convertEdges cDiag [] = do return cDiag
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly convertEdges cDiag (lEdge : lEdges) =
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly do convEdge <- convertEdge lEdge
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly let cDiag' = insEdge convEdge cDiag
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett convertEdges cDiag' lEdges
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett dNodes = labNodes diag
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly dEdges = labEdges diag
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly -- insert converted nodes to an empty diagram
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly cDiag <- convertNodes Graph.empty dNodes
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly -- insert converted edges to the diagram containing only nodes
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett cDiag' <- convertEdges cDiag dEdges
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly return cDiag'
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly-- | Coerce GMorphisms in the list of (diagram node, GMorphism) pairs
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly-- to morphisms in given logic
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillyhomogeniseSink :: Logic lid sublogics
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett basic_spec sentence symb_items symb_map_items
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly sign morphism symbol raw_symbol proof_tree
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly => lid -- ^ the target logic to which morphisms will be coerced
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly -> [(Node, GMorphism)] -- ^ the list of edges to be homogenised
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly -> Result [(Node, morphism)]
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillyhomogeniseSink targetLid dEdges =
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett -- See homogeniseDiagram for comments on implementation.
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly do let convertMorphism (n, GMorphism cid _ mor) =
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly if isIdComorphism (Comorphism cid) then
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly do mor' <- coerceMorphism (targetLogic cid) targetLid "" mor
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly return (n, mor')
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett "Trying to coerce a morphism between different logics.\n" ++
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly "Heterogeneous specifications are not fully supported yet."
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly convEdges [] = do return []
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly convEdges (e : es) = do ce <- convertMorphism e
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly ces <- convEdges es
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly return (ce : ces)
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett convEdges dEdges
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly-- | Create a graph containing descriptions of nodes and edges.
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillydiagDesc :: Diag
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly -> Tree.Gr String String
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillydiagDesc diag =
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett let insNodeDesc g (n, DiagNode { dn_desc = desc }) =
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly if desc == "" then g else insNode (n, desc) g
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett in foldl insNodeDesc Graph.empty (labNodes diag)
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly-- | Create a sink consisting of incusion morphisms between
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly-- signatures from given set of nodes and given signature.
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillyinclusionSink :: LogicGraph
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett -> [DiagNodeSig] -- ^ the source nodes
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly -> NodeSig -- ^ the target signature
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett -> Result [(Node, GMorphism)]
5858e6262048894b0e933b547852f04aed009b58Andy Gimblett-- ^ returns the diagram with edges inserted
5858e6262048894b0e933b547852f04aed009b58Andy GimblettinclusionSink lgraph srcNodes tnsig =
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett do let insmorph ls dns = do
5858e6262048894b0e933b547852f04aed009b58Andy Gimblett Diag_node_sig n nsig -> do
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly incl <- ginclusion lgraph (getSig nsig) (getSig tnsig)
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly return ((n, incl): l)
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly sink <- foldl insmorph (return []) srcNodes