{- |

Module : $Header$

Author : Maciek Makowski

Year : 2004

Copyright : (c) Maciek Makowski, Warsaw University 2004

Licence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt

Maintainer : hets@tzi.de

Stability : provisional

Portability : non-portable (Logic)

Data types and functions for architectural diagrams.

Follows the CASL Reference Manual, section III.5.6.

-}

module Static.ArchDiagram

where

import Logic.Comorphism

import Logic.Logic

import Logic.Grothendieck

import Common.PrettyPrint

import Common.Lib.Graph

import Common.Lib.Pretty

import Static.DevGraph

--import Static.AnalysisStructured

import Common.Result

import Common.Id

import qualified Common.Lib.Graph as Graph

import qualified Common.Lib.Map as Map

-- * Types

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

data DiagNodeLab = DiagNode { dn_sig :: NodeSig,

dn_desc :: String }

deriving Show

emptyDiagNodeLab :: AnyLogic -> DiagNodeLab

emptyDiagNodeLab l = DiagNode { dn_sig = EmptyNode l, dn_desc = "" }

data DiagLinkLab = DiagLink { dl_morphism :: GMorphism }

deriving (Eq, Show)

type BasedParUnitSig = (DiagNodeSig, ParUnitSig)

type Diag = Diagram DiagNodeLab DiagLinkLab

emptyDiag :: Diag

emptyDiag = Graph.empty

data DiagNodeSig = Diag_node_sig Node NodeSig

| Empty_node AnyLogic

deriving Show

emptyDiagNodeSig :: AnyLogic -> DiagNodeSig

emptyDiagNodeSig l = Empty_node l

-- | Return a signature stored within given diagram node sig

getSigFromDiag :: DiagNodeSig -> NodeSig

getSigFromDiag (Diag_node_sig _ ns) = ns

getSigFromDiag (Empty_node l) = EmptyNode l

data BasedUnitSig = Based_unit_sig DiagNodeSig

| Based_par_unit_sig BasedParUnitSig

deriving Show

type StBasedUnitCtx = Map.Map SIMPLE_ID BasedUnitSig

emptyStBasedUnitCtx :: StBasedUnitCtx

emptyStBasedUnitCtx = Map.empty

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

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

type ExtStUnitCtx = (StBasedUnitCtx, Diag)

emptyExtStUnitCtx :: ExtStUnitCtx

emptyExtStUnitCtx = (emptyStBasedUnitCtx, emptyDiag)

-- * Instances

-- PrettyPrint

instance PrettyPrint Diag where

printText0 ga diag =

let gs (n, DiagNode {dn_sig = nsig}) =

(n, getSig nsig)

in ptext "nodes: "

<+> (printText0 ga (map gs (labNodes diag)))

<+> ptext "\nedges: "

<+> (printText0 ga (edges diag))

-- * Functions

-- | Pretty print the diagram

printDiag :: a -> String -> Diag -> Result a

--printDiag res t diag = warning res (showPretty diag t) nullPos

printDiag res _ _ = do return res

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

ctx :: ExtStUnitCtx -> StUnitCtx

ctx (buc, _) =

let ctx' [] _ = emptyStUnitCtx

ctx' (id : ids) buc =

let uctx = ctx' ids buc

in case Map.lookup id buc of

Just (Based_unit_sig (Diag_node_sig _ nsig))

-> Map.insert id (Sig nsig) uctx

Just (Based_par_unit_sig ((Diag_node_sig _ nsig), usig))

-> Map.insert id (Imp_unit_sig (nsig, Par_unit_sig usig)) uctx

_ -> uctx -- this should never be the case

in ctx' (Map.keys buc) buc

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

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

insInclusionEdges :: LogicGraph

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

-> [DiagNodeSig] -- ^ the source nodes

-> DiagNodeSig -- ^ the target node

-> Result Diag

-- ^ returns the diagram with edges inserted

insInclusionEdges lgraph diag srcNodes (Diag_node_sig tn tnsig) =

do let inslink diag dns = do d <- diag

case dns of

Empty_node _ -> return d

Diag_node_sig n nsig ->

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

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

diag' <- foldl inslink (return diag) srcNodes

return diag'

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

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

insInclusionEdgesRev :: LogicGraph

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

-> DiagNodeSig -- ^ the source node

-> [DiagNodeSig] -- ^ the target nodes

-> Result Diag

-- ^ returns the diagram with edges inserted

insInclusionEdgesRev lgraph diag (Diag_node_sig sn snsig) targetNodes =

do let inslink diag dns = do d <- diag

case dns of

Empty_node _ -> return d

Diag_node_sig n nsig ->

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

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

diag' <- foldl inslink (return diag) 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}

[node] = newNodes 0 diag

diag' = insNode (node, nodeContents) diag

newDiagNode = Diag_node_sig node newNodeSig

diag'' <- insInclusionEdges lgraph diag' srcNodes newDiagNode

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

return (newDiagNode, diag'')

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

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

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

-- with given morphis as well.

extendDiagramWithMorphism :: Pos -- ^ 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 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] = newNodes 0 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 :: Pos -- ^ 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] = newNodes 0 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] = newNodes 0 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 (Diagram 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, DiagNode { dn_sig = NodeSig (_, G_sign srcLid sig) }) =

do sig' <- rcoerce targetLid srcLid nullPos sig

return (n, sig')

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

let srcLid = sourceLogic cid

in if isIdComorphism (Comorphism cid) then

do mor' <- rcoerce targetLid srcLid nullPos mor

return (n1, n2, mor')

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

nullPos

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

nodes = labNodes diag

edges = labEdges diag

-- insert converted nodes to an empty diagram

cDiag <- convertNodes Graph.empty nodes

-- insert converted edges to the diagram containing only nodes

cDiag' <- convertEdges cDiag edges

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

-- See homogeniseDiagram for comments on implementation.

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

let srcLid = sourceLogic cid

in if isIdComorphism (Comorphism cid) then

do mor' <- rcoerce targetLid srcLid nullPos mor

return (n, mor')

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

nullPos

convEdges [] = do return []

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

ces <- convEdges es

return (ce : ces)

convEdges edges

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

diagDesc :: Diag

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

Empty_node _ -> return l

Diag_node_sig n nsig ->

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

return ((n, incl): l)

sink <- foldl insmorph (return []) srcNodes

return sink