{- |

Module : $Header$

Description : Data types and functions for architectural diagrams

Copyright : (c) Maciek Makowski, Warsaw University 2004-2006

License : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

Maintainer : till@informatik.uni-bremen.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 Logic.Coerce

import Data.Graph.Inductive.Graph as Graph

import qualified Common.Lib.Graph as Tree

import qualified Data.Map as Map

import Common.Doc

import Common.DocUtils

import Common.ExtSign

import Common.Result

import Common.Id

import Static.GTheory

import Static.DevGraph

-- * Types

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

data DiagNodeLab = DiagNode { dn_sig :: NodeSig, dn_desc :: String }

deriving Show

data DiagLinkLab = DiagLink { dl_morphism :: GMorphism, dl_number:: Int }

deriving Show

data Diag = Diagram {

diagGraph :: Tree.Gr DiagNodeLab DiagLinkLab,

numberOfEdges :: Int

}

deriving Show

emptyDiag :: Diag

emptyDiag = Diagram{diagGraph = Graph.empty, numberOfEdges = 0}

data DiagNodeSig = Diag_node_sig Node NodeSig

data MaybeDiagNode = JustDiagNode DiagNodeSig | EmptyDiagNode AnyLogic

toMaybeNode :: MaybeDiagNode -> MaybeNode

toMaybeNode mdn = case mdn of

JustDiagNode dns -> JustNode $ getSigFromDiag dns

EmptyDiagNode l -> EmptyNode l

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

getSigFromDiag :: DiagNodeSig -> NodeSig

getSigFromDiag (Diag_node_sig _ ns) = ns

data BasedUnitSig = Based_unit_sig DiagNodeSig

| Based_par_unit_sig MaybeDiagNode UnitSig

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)

-- Instance

instance Pretty Diag where

pretty diag =

let gs (n, dn) =

(n, getSig $ dn_sig dn)

in text "nodes:"

<+> sepByCommas (map (pretty . gs) $ labNodes $ diagGraph diag)

$+$ text "edges:"

<+> ppWithCommas (edges $ diagGraph diag)

-- * Functions

-- | return the diagram

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

printDiag res _ _ = return res

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

ctx :: ExtStUnitCtx -> StUnitCtx

ctx (buc, _) =

let ctx' [] _ = emptyStUnitCtx

ctx' (id1 : ids) buc0 =

let uctx = ctx' ids buc0

in case Map.lookup id1 buc0 of

Just (Based_unit_sig mds) -> Map.insert id1

(Sig $ getSigFromDiag mds) uctx

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

(ImpUnitSig (toMaybeNode mds) 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 insert edges to

-> [DiagNodeSig] -- ^ the source nodes

-> DiagNodeSig -- ^ the target node

-> Result Diag -- ^ the diagram with edges inserted

insInclusionEdges lgraph diag0 srcNodes (Diag_node_sig tn tnsig) = do

let inslink diag dns = do

d1 <- diag

let d = diagGraph d1

case dns of

Diag_node_sig n nsig -> do

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

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

dl_morphism = incl,

dl_number = numberOfEdges d1 + 1 }) d,

numberOfEdges = numberOfEdges d1 + 1}

diag' <- foldl inslink (return diag0) 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 insert edges to

-> DiagNodeSig -- ^ the source node

-> [DiagNodeSig] -- ^ the target nodes

-> Result Diag -- ^ the diagram with edges inserted

insInclusionEdgesRev lgraph diag0 (Diag_node_sig sn snsig) targetNodes =

do let inslink diag dns = do

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