1N/A{- |

1N/AModule : $Header$

1N/ADescription : Data types and functions for architectural diagrams

1N/ACopyright : (c) Maciek Makowski, Warsaw University 2004-2006

1N/ALicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

1N/AMaintainer : till@informatik.uni-bremen.de

1N/AStability : provisional

1N/APortability : non-portable (Logic)

1N/A

1N/A Data types and functions for architectural diagrams

1N/A Follows the CASL Reference Manual, section III.5.6.

1N/A

1N/A-}

1N/A

1N/Amodule Static.ArchDiagram where

1N/A

1N/Aimport Logic.Comorphism

1N/Aimport Logic.Logic

1N/Aimport Logic.Grothendieck

1N/Aimport Logic.Coerce

1N/A

1N/Aimport Data.Graph.Inductive.Graph as Graph

1N/Aimport qualified Common.Lib.Graph as Tree

1N/A

1N/Aimport qualified Data.Map as Map

1N/Aimport Common.Doc

1N/Aimport Common.DocUtils

1N/Aimport Common.ExtSign

1N/Aimport Common.Result

1N/Aimport Common.Id

1N/A

1N/Aimport Static.GTheory

1N/Aimport Static.DevGraph

1N/A

1N/A-- * Types

1N/A-- (as defined for extended static semantics in Chap. III:5.6.1)

1N/A

1N/Adata DiagNodeLab = DiagNode { dn_sig :: NodeSig, dn_desc :: String }

1N/A deriving Show

1N/A

1N/Adata DiagLinkLab = DiagLink { dl_morphism :: GMorphism, dl_number:: Int }

1N/A deriving Show

1N/A

1N/Adata Diag = Diagram {

1N/A diagGraph :: Tree.Gr DiagNodeLab DiagLinkLab,

1N/A numberOfEdges :: Int

1N/A }

1N/A deriving Show

1N/A

1N/AemptyDiag :: Diag

1N/AemptyDiag = Diagram{diagGraph = Graph.empty, numberOfEdges = 0}

1N/A

1N/Adata DiagNodeSig = Diag_node_sig Node NodeSig

1N/A

1N/Adata MaybeDiagNode = JustDiagNode DiagNodeSig | EmptyDiagNode AnyLogic

1N/A

1N/AtoMaybeNode :: MaybeDiagNode -> MaybeNode

1N/AtoMaybeNode mdn = case mdn of

1N/A JustDiagNode dns -> JustNode $ getSigFromDiag dns

1N/A EmptyDiagNode l -> EmptyNode l

1N/A

1N/A-- | Return a signature stored within given diagram node sig

1N/AgetSigFromDiag :: DiagNodeSig -> NodeSig

1N/AgetSigFromDiag (Diag_node_sig _ ns) = ns

1N/A

1N/Adata BasedUnitSig = Based_unit_sig DiagNodeSig

1N/A | Based_par_unit_sig MaybeDiagNode UnitSig

1N/A

1N/Atype StBasedUnitCtx = Map.Map SIMPLE_ID BasedUnitSig

1N/AemptyStBasedUnitCtx :: StBasedUnitCtx

1N/AemptyStBasedUnitCtx = Map.empty

1N/A

1N/A-- Since Ps and Bs in the definition of ExtStUnitCtx have disjoint domains

1N/A-- we can merge them into a single mapping represented by StBasedUnitCtx.

1N/Atype ExtStUnitCtx = (StBasedUnitCtx, Diag)

1N/AemptyExtStUnitCtx :: ExtStUnitCtx

1N/AemptyExtStUnitCtx = (emptyStBasedUnitCtx, emptyDiag)

1N/A

1N/A-- Instance

1N/Ainstance Pretty Diag where

1N/A pretty diag =

1N/A let gs (n, dn) =

1N/A (n, getSig $ dn_sig dn)

1N/A in text "nodes:"

1N/A <+> sepByCommas (map (pretty . gs) $ labNodes $ diagGraph diag)

1N/A $+$ text "edges:"

1N/A <+> ppWithCommas (edges $ diagGraph diag)

1N/A

1N/A-- * Functions

1N/A

1N/A-- | return the diagram

1N/AprintDiag :: a -> String -> Diag -> Result a

1N/AprintDiag res _ _ = return res

1N/A

1N/A-- | A mapping from extended to basic static unit context

1N/Actx :: ExtStUnitCtx -> StUnitCtx

1N/Actx (buc, _) =

1N/A let ctx' [] _ = emptyStUnitCtx

1N/A ctx' (id1 : ids) buc0 =

1N/A let uctx = ctx' ids buc0

1N/A in case Map.lookup id1 buc0 of

1N/A Just (Based_unit_sig mds) -> Map.insert id1

1N/A (Sig $ getSigFromDiag mds) uctx

1N/A Just (Based_par_unit_sig mds usig) -> Map.insert id1

1N/A (ImpUnitSig (toMaybeNode mds) usig) uctx

1N/A _ -> uctx -- this should never be the case

1N/A in ctx' (Map.keys buc) buc

1N/A

1N/A-- | Insert the edges from given source nodes to given target node

1N/A-- into the given diagram. The edges are labelled with inclusions.

1N/AinsInclusionEdges :: LogicGraph

1N/A -> Diag -- ^ the diagram to insert edges to

1N/A -> [DiagNodeSig] -- ^ the source nodes

1N/A -> DiagNodeSig -- ^ the target node

1N/A -> Result Diag -- ^ the diagram with edges inserted

1N/AinsInclusionEdges lgraph diag0 srcNodes (Diag_node_sig tn tnsig) = do

1N/A let inslink diag dns = do

1N/A d1 <- diag

1N/A let d = diagGraph d1

1N/A case dns of

1N/A Diag_node_sig n nsig -> do

1N/A incl <- ginclusion lgraph (getSig nsig) (getSig tnsig)

1N/A return $ Diagram {diagGraph = insEdge (n, tn, DiagLink {

1N/A dl_morphism = incl,

1N/A dl_number = numberOfEdges d1 + 1 }) d,

1N/A numberOfEdges = numberOfEdges d1 + 1}

1N/A diag' <- foldl inslink (return diag0) srcNodes

1N/A return diag'

1N/A

1N/A-- | Insert the edges from given source node to given target nodes

1N/A-- into the given diagram. The edges are labelled with inclusions.

1N/AinsInclusionEdgesRev :: LogicGraph

1N/A -> Diag -- ^ the diagram to insert edges to

1N/A -> DiagNodeSig -- ^ the source node

1N/A -> [DiagNodeSig] -- ^ the target nodes

1N/A -> Result Diag -- ^ the diagram with edges inserted

1N/AinsInclusionEdgesRev lgraph diag0 (Diag_node_sig sn snsig) targetNodes =

1N/A do let inslink diag dns = do

1N/A d1 <- diag

let d = diagGraph d1

case dns of

Diag_node_sig n nsig -> do

incl <- ginclusion lgraph (getSig snsig) (getSig nsig)

return $ Diagram {diagGraph = insEdge (sn, n, DiagLink {

dl_morphism = incl,

dl_number = numberOfEdges d1 + 1 }) d,

numberOfEdges = numberOfEdges d1 + 1}

diag' <- foldl inslink (return diag0) targetNodes

return diag'

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

given signature and with edges from given set of nodes to the new

node. The new edges are labelled with sigature inclusions. -}

extendDiagramIncl :: LogicGraph

-> Diag -- ^ the diagram to be extended

-> [DiagNodeSig]

-- ^ the nodes which should be linked to the new node

-> 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

extendDiagramIncl lgraph diag srcNodes newNodeSig desc =

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

diagGr = diagGraph diag

node = Tree.getNewNode diagGr

diag' = Diagram{diagGraph = insNode (node, nodeContents) diagGr,

numberOfEdges = numberOfEdges diag}

newDiagNode = Diag_node_sig node newNodeSig

diag'' <- insInclusionEdges lgraph diag' srcNodes newDiagNode

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

-- | Extend the development graph with given morphism originating

-- from given NodeSig

extendDGraph :: DGraph -- ^ the development graph to be extended

-> NodeSig -- ^ the NodeSig from which the morphism originates

-> GMorphism -- ^ the morphism to be inserted

-> DGOrigin

-> Result (NodeSig, DGraph)

-- ^ returns the target signature of the morphism and the resulting DGraph

extendDGraph dg (NodeSig n _) morph orig = case cod morph of

targetSig@(G_sign lid tar ind) -> let

nodeContents = newNodeLab emptyNodeName orig

$ noSensGTheory lid tar ind

linkContents = DGLink

{ dgl_morphism = morph

, dgl_type = globalDef

, dgl_origin = SeeTarget

, dgl_id = getNewEdgeId dg' }

node = getNewNodeDG dg

dg' = insNodeDG (node, nodeContents) dg

dg'' = insEdgeDG (n, node, linkContents) dg'

in return (NodeSig node targetSig, dg'')

-- | Extend the development graph with given morphism pointing to

-- given NodeSig

extendDGraphRev :: DGraph -- ^ the development graph to be extended

-> NodeSig -- ^ the NodeSig to which the morphism points

-> GMorphism -- ^ the morphism to be inserted

-> DGOrigin

-> Result (NodeSig, DGraph)

-- ^ returns the source signature of the morphism and the resulting DGraph

extendDGraphRev dg (NodeSig n _) morph orig = case dom morph of

sourceSig@(G_sign lid src ind) -> let

nodeContents = newNodeLab emptyNodeName orig

$ noSensGTheory lid src ind

linkContents = DGLink

{ dgl_morphism = morph

, dgl_type = globalDef

, dgl_origin = SeeSource

, dgl_id = getNewEdgeId dg' }

node = getNewNodeDG dg

dg' = insNodeDG (node, nodeContents) dg

dg'' = insEdgeDG (node, n, linkContents) dg'

in return (NodeSig node sourceSig, dg'')

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

edge to that node. The edge is labelled with a given signature morphism

and the node contains the target of this morphism. Extends the

development graph with the given morphism as well. -}

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

-> LogicGraph

-> Diag -- ^ the diagram to be extended

-> DGraph -- ^ the development graph

-> DiagNodeSig

-- ^ the node from which the edge should originate

-> GMorphism

-- ^ the morphism as label for the new edge

-> 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) mor desc orig =

if getSig nsig == dom mor then

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

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

diagGr = diagGraph diag

node = Tree.getNewNode diagGr

diagGr' = insNode (node, nodeContents) diagGr

diag' = Diagram{diagGraph = insEdge (n, node, DiagLink {

dl_morphism = mor,

dl_number = numberOfEdges diag + 1 }) diagGr',

numberOfEdges = numberOfEdges diag + 1 }

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

"extendDiagramWithMorphism" diag'

else fatal_error

("Internal error: Static.ArchDiagram.extendDiagramWithMorphism:" ++

"\n the morphism domain differs from the signature in given source node")

pos

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

edge from that node. The edge is labelled with a given signature

morphism and the node contains the source of this morphism. Extends

the development graph with the given morphism 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 as label for the new edge

-> String -- ^ a diagnostic node description

-> 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)

mor desc orig =

if getSig nsig == cod mor then

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

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

diagGr = diagGraph diag

node = Tree.getNewNode diagGr

diagGr' = insNode (node, nodeContents) diagGr

diag' = Diagram{ diagGraph = insEdge (node, n, DiagLink {

dl_morphism = mor ,

dl_number = numberOfEdges diag + 1}) diagGr',

numberOfEdges = numberOfEdges diag + 1 }

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

"extendDiagramWithMorphismRev" diag'

else fatal_error

("Internal error: Static.ArchDiagram.extendDiagramWithMorphismRev:\n" ++

" 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 as label for the new edge

-> NodeSig -- ^ the signature as label for the new node

-> 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}

diagGr = diagGraph diag

node = Tree.getNewNode diagGr

diagGr' = insNode (node, nodeContents) diagGr

diag' = Diagram{diagGraph = insEdge (n, node, DiagLink {

dl_morphism = edgeMorph,

dl_number = numberOfEdges diag + 1 }) diagGr',

numberOfEdges = numberOfEdges diag + 1 }

newDiagNode = Diag_node_sig node newNodeSig

printDiag (newDiagNode, diag') "extendDiagram" 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 be coerced to

-> Diag -- ^ the diagram to be homogenised

-> Result (Tree.Gr sign (Int,morphism))

{- 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). -}

homogeniseDiagram targetLid diag =

do let convertNode (n, dn) =

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

sig' <- coerceSign srcLid targetLid "" sig

return (n, plainSign sig')

convertEdge (n1, n2, DiagLink {

dl_morphism = GMorphism cid _ _ mor _, dl_number = nr})

= if isIdComorphism (Comorphism cid) then

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

return (n1, n2, (nr,mor'))

else fail $

"Trying to coerce a morphism between different logics.\n" ++

"Heterogeneous specifications are not fully supported yet."

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 $ diagGraph diag

dEdges = labEdges $ diagGraph 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'

-- | 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 $ diagGraph 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