{- |
Module      :  ./Static/ArchDiagram.hs
Description :  Data types and functions for architectural diagrams
Copyright   :  (c) Maciek Makowski, Warsaw University 2004-2006
License     :  GPLv2 or higher, see LICENSE.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.

   Extended to the new rules for lambda expressions(WADT2010).

-}

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 Control.Monad (foldM)
import Data.List (nub)
import Data.Maybe (fromMaybe)
import Common.IRI
import qualified Control.Monad.Fail as Fail


import Static.GTheory
import Static.DevGraph
import Static.DgUtils

{- * Types
(as defined for extended static semantics in Chap. III:5.6.1) -}

-- moved in Static.DevGraph

emptyDiag :: Diag
emptyDiag :: Diag
emptyDiag = Diagram :: Gr DiagNodeLab DiagLinkLab -> Int -> Diag
Diagram {diagGraph :: Gr DiagNodeLab DiagLinkLab
diagGraph = Gr DiagNodeLab DiagLinkLab
forall (gr :: * -> * -> *) a b. Graph gr => gr a b
Graph.empty, numberOfEdges :: Int
numberOfEdges = 0}

data DiagNodeSig = Diag_node_sig Node NodeSig deriving Int -> DiagNodeSig -> ShowS
[DiagNodeSig] -> ShowS
DiagNodeSig -> String
(Int -> DiagNodeSig -> ShowS)
-> (DiagNodeSig -> String)
-> ([DiagNodeSig] -> ShowS)
-> Show DiagNodeSig
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DiagNodeSig] -> ShowS
$cshowList :: [DiagNodeSig] -> ShowS
show :: DiagNodeSig -> String
$cshow :: DiagNodeSig -> String
showsPrec :: Int -> DiagNodeSig -> ShowS
$cshowsPrec :: Int -> DiagNodeSig -> ShowS
Show

instance Show MaybeDiagNode where
 show :: MaybeDiagNode -> String
show (EmptyDiagNode _) = "empty"
 show (JustDiagNode dns :: DiagNodeSig
dns) = DiagNodeSig -> String
forall a. Show a => a -> String
show DiagNodeSig
dns

data MaybeDiagNode = JustDiagNode DiagNodeSig | EmptyDiagNode AnyLogic

toMaybeNode :: MaybeDiagNode -> MaybeNode
toMaybeNode :: MaybeDiagNode -> MaybeNode
toMaybeNode mdn :: MaybeDiagNode
mdn = case MaybeDiagNode
mdn of
    JustDiagNode dns :: DiagNodeSig
dns -> NodeSig -> MaybeNode
JustNode (NodeSig -> MaybeNode) -> NodeSig -> MaybeNode
forall a b. (a -> b) -> a -> b
$ DiagNodeSig -> NodeSig
getSigFromDiag DiagNodeSig
dns
    EmptyDiagNode l :: AnyLogic
l -> AnyLogic -> MaybeNode
EmptyNode AnyLogic
l

-- | Return a signature stored within given diagram node sig
getSigFromDiag :: DiagNodeSig -> NodeSig
getSigFromDiag :: DiagNodeSig -> NodeSig
getSigFromDiag (Diag_node_sig _ ns :: NodeSig
ns) = NodeSig
ns

data BasedUnitSig = Based_unit_sig DiagNodeSig RefSig
                  | Based_par_unit_sig MaybeDiagNode RefSig
                  | Based_lambda_unit_sig [DiagNodeSig] RefSig
                    {- the list is always non-empty,
                    actually has at least 2 elems, and the
                    head stores the "result" node -}

instance Show BasedUnitSig where
 show :: BasedUnitSig -> String
show (Based_unit_sig dns :: DiagNodeSig
dns _) = DiagNodeSig -> String
forall a. Show a => a -> String
show DiagNodeSig
dns
 show (Based_par_unit_sig mdn :: MaybeDiagNode
mdn _) = MaybeDiagNode -> String
forall a. Show a => a -> String
show MaybeDiagNode
mdn
 show (Based_lambda_unit_sig _ usig :: RefSig
usig) = RefSig -> String
forall a. Show a => a -> String
show RefSig
usig

type StBasedUnitCtx = Map.Map IRI BasedUnitSig
emptyStBasedUnitCtx :: StBasedUnitCtx
emptyStBasedUnitCtx :: StBasedUnitCtx
emptyStBasedUnitCtx = StBasedUnitCtx
forall k a. Map k a
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 :: ExtStUnitCtx
emptyExtStUnitCtx = (StBasedUnitCtx
emptyStBasedUnitCtx, Diag
emptyDiag)

-- Instance
instance Pretty Diag where
    pretty :: Diag -> Doc
pretty diag :: Diag
diag =
        let gs :: (a, DiagNodeLab) -> (a, G_sign)
gs (n :: a
n, dn :: DiagNodeLab
dn) =
                (a
n, NodeSig -> G_sign
getSig (NodeSig -> G_sign) -> NodeSig -> G_sign
forall a b. (a -> b) -> a -> b
$ DiagNodeLab -> NodeSig
dn_sig DiagNodeLab
dn)
        in String -> Doc
text "nodes:"
           Doc -> Doc -> Doc
<+> [Doc] -> Doc
sepByCommas (((Int, DiagNodeLab) -> Doc) -> [(Int, DiagNodeLab)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map ((Int, G_sign) -> Doc
forall a. Pretty a => a -> Doc
pretty ((Int, G_sign) -> Doc)
-> ((Int, DiagNodeLab) -> (Int, G_sign))
-> (Int, DiagNodeLab)
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, DiagNodeLab) -> (Int, G_sign)
forall a. (a, DiagNodeLab) -> (a, G_sign)
gs) ([(Int, DiagNodeLab)] -> [Doc]) -> [(Int, DiagNodeLab)] -> [Doc]
forall a b. (a -> b) -> a -> b
$ Gr DiagNodeLab DiagLinkLab -> [(Int, DiagNodeLab)]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode a]
labNodes (Gr DiagNodeLab DiagLinkLab -> [(Int, DiagNodeLab)])
-> Gr DiagNodeLab DiagLinkLab -> [(Int, DiagNodeLab)]
forall a b. (a -> b) -> a -> b
$ Diag -> Gr DiagNodeLab DiagLinkLab
diagGraph Diag
diag)
           Doc -> Doc -> Doc
$+$ String -> Doc
text "edges:"
           Doc -> Doc -> Doc
<+> [Edge] -> Doc
forall a. Pretty a => [a] -> Doc
ppWithCommas (Gr DiagNodeLab DiagLinkLab -> [Edge]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [Edge]
edges (Gr DiagNodeLab DiagLinkLab -> [Edge])
-> Gr DiagNodeLab DiagLinkLab -> [Edge]
forall a b. (a -> b) -> a -> b
$ Diag -> Gr DiagNodeLab DiagLinkLab
diagGraph Diag
diag)

-- * Functions

-- | return the diagram
printDiag :: a -> String -> Diag -> Result a
printDiag :: a -> String -> Diag -> Result a
printDiag res :: a
res _ _ = a -> Result a
forall (m :: * -> *) a. Monad m => a -> m a
return a
res

-- | A mapping from extended to basic static unit context
ctx :: ExtStUnitCtx -> RefStUnitCtx
ctx :: ExtStUnitCtx -> RefStUnitCtx
ctx (buc :: StBasedUnitCtx
buc, _) =
    let ctx' :: [IRI] -> StBasedUnitCtx -> RefStUnitCtx
ctx' [] _ = RefStUnitCtx
emptyRefStUnitCtx
        ctx' (id1 :: IRI
id1 : ids :: [IRI]
ids) buc0 :: StBasedUnitCtx
buc0 =
            let uctx :: RefStUnitCtx
uctx = [IRI] -> StBasedUnitCtx -> RefStUnitCtx
ctx' [IRI]
ids StBasedUnitCtx
buc0
            in case IRI -> StBasedUnitCtx -> Maybe BasedUnitSig
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup IRI
id1 StBasedUnitCtx
buc0 of
                    Just (Based_unit_sig _ rsig :: RefSig
rsig) -> IRI -> RefSig -> RefStUnitCtx -> RefStUnitCtx
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert IRI
id1
                           RefSig
rsig RefStUnitCtx
uctx
                    Just (Based_par_unit_sig _ rsig :: RefSig
rsig) -> IRI -> RefSig -> RefStUnitCtx -> RefStUnitCtx
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert IRI
id1
                           RefSig
rsig RefStUnitCtx
uctx
                    Just (Based_lambda_unit_sig _ rsig :: RefSig
rsig) -> IRI -> RefSig -> RefStUnitCtx -> RefStUnitCtx
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert IRI
id1
                          RefSig
rsig RefStUnitCtx
uctx
                    _ -> RefStUnitCtx
uctx -- this should never be the case
    in [IRI] -> StBasedUnitCtx -> RefStUnitCtx
ctx' (StBasedUnitCtx -> [IRI]
forall k a. Map k a -> [k]
Map.keys StBasedUnitCtx
buc) StBasedUnitCtx
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 :: LogicGraph -> Diag -> [DiagNodeSig] -> DiagNodeSig -> Result Diag
insInclusionEdges lgraph :: LogicGraph
lgraph diag0 :: Diag
diag0 srcNodes :: [DiagNodeSig]
srcNodes (Diag_node_sig tn :: Int
tn tnsig :: NodeSig
tnsig) = do
 let inslink :: Result Diag -> DiagNodeSig -> Result Diag
inslink diag :: Result Diag
diag dns :: DiagNodeSig
dns = do
      Diag
d1 <- Result Diag
diag
      let d :: Gr DiagNodeLab DiagLinkLab
d = Diag -> Gr DiagNodeLab DiagLinkLab
diagGraph Diag
d1
      case DiagNodeSig
dns of
        Diag_node_sig n :: Int
n nsig :: NodeSig
nsig -> do
          GMorphism
incl <- LogicGraph -> G_sign -> G_sign -> Result GMorphism
ginclusion LogicGraph
lgraph (NodeSig -> G_sign
getSig NodeSig
nsig) (NodeSig -> G_sign
getSig NodeSig
tnsig)
          Diag -> Result Diag
forall (m :: * -> *) a. Monad m => a -> m a
return Diagram :: Gr DiagNodeLab DiagLinkLab -> Int -> Diag
Diagram {diagGraph :: Gr DiagNodeLab DiagLinkLab
diagGraph = LEdge DiagLinkLab
-> Gr DiagNodeLab DiagLinkLab -> Gr DiagNodeLab DiagLinkLab
forall (gr :: * -> * -> *) b a.
DynGraph gr =>
LEdge b -> gr a b -> gr a b
insEdge (Int
n, Int
tn, DiagLink :: GMorphism -> Int -> DiagLinkLab
DiagLink {
                                  dl_morphism :: GMorphism
dl_morphism = GMorphism
incl,
                                  dl_number :: Int
dl_number = Diag -> Int
numberOfEdges Diag
d1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1 }) Gr DiagNodeLab DiagLinkLab
d,
                            numberOfEdges :: Int
numberOfEdges = Diag -> Int
numberOfEdges Diag
d1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1}
 (Result Diag -> DiagNodeSig -> Result Diag)
-> Result Diag -> [DiagNodeSig] -> Result Diag
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Result Diag -> DiagNodeSig -> Result Diag
inslink (Diag -> Result Diag
forall (m :: * -> *) a. Monad m => a -> m a
return Diag
diag0) [DiagNodeSig]
srcNodes

{- | 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 :: LogicGraph -> Diag -> DiagNodeSig -> [DiagNodeSig] -> Result Diag
insInclusionEdgesRev lgraph :: LogicGraph
lgraph diag0 :: Diag
diag0 (Diag_node_sig sn :: Int
sn snsig :: NodeSig
snsig) targetNodes :: [DiagNodeSig]
targetNodes =
    do let inslink :: Result Diag -> DiagNodeSig -> Result Diag
inslink diag :: Result Diag
diag dns :: DiagNodeSig
dns = do
               Diag
d1 <- Result Diag
diag
               let d :: Gr DiagNodeLab DiagLinkLab
d = Diag -> Gr DiagNodeLab DiagLinkLab
diagGraph Diag
d1
               case DiagNodeSig
dns of
                 Diag_node_sig n :: Int
n nsig :: NodeSig
nsig -> do
                   GMorphism
incl <- LogicGraph -> G_sign -> G_sign -> Result GMorphism
ginclusion LogicGraph
lgraph (NodeSig -> G_sign
getSig NodeSig
snsig) (NodeSig -> G_sign
getSig NodeSig
nsig)
                   Diag -> Result Diag
forall (m :: * -> *) a. Monad m => a -> m a
return Diagram :: Gr DiagNodeLab DiagLinkLab -> Int -> Diag
Diagram {diagGraph :: Gr DiagNodeLab DiagLinkLab
diagGraph = LEdge DiagLinkLab
-> Gr DiagNodeLab DiagLinkLab -> Gr DiagNodeLab DiagLinkLab
forall (gr :: * -> * -> *) b a.
DynGraph gr =>
LEdge b -> gr a b -> gr a b
insEdge (Int
sn, Int
n, DiagLink :: GMorphism -> Int -> DiagLinkLab
DiagLink {
                      dl_morphism :: GMorphism
dl_morphism = GMorphism
incl,
                      dl_number :: Int
dl_number = Diag -> Int
numberOfEdges Diag
d1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1 }) Gr DiagNodeLab DiagLinkLab
d,
                                     numberOfEdges :: Int
numberOfEdges = Diag -> Int
numberOfEdges Diag
d1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1}
       (Result Diag -> DiagNodeSig -> Result Diag)
-> Result Diag -> [DiagNodeSig] -> Result Diag
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Result Diag -> DiagNodeSig -> Result Diag
inslink (Diag -> Result Diag
forall (m :: * -> *) a. Monad m => a -> m a
return Diag
diag0) [DiagNodeSig]
targetNodes

{- | 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 :: LogicGraph
-> Diag
-> [DiagNodeSig]
-> NodeSig
-> String
-> Result (DiagNodeSig, Diag)
extendDiagramIncl lgraph :: LogicGraph
lgraph diag :: Diag
diag srcNodes :: [DiagNodeSig]
srcNodes newNodeSig :: NodeSig
newNodeSig desc :: String
desc =
  do let nodeContents :: DiagNodeLab
nodeContents = DiagNode :: NodeSig -> String -> DiagNodeLab
DiagNode {dn_sig :: NodeSig
dn_sig = NodeSig
newNodeSig, dn_desc :: String
dn_desc = String
desc}
         diagGr :: Gr DiagNodeLab DiagLinkLab
diagGr = Diag -> Gr DiagNodeLab DiagLinkLab
diagGraph Diag
diag
         node :: Int
node = Gr DiagNodeLab DiagLinkLab -> Int
forall a b. Gr a b -> Int
Tree.getNewNode Gr DiagNodeLab DiagLinkLab
diagGr
         diag' :: Diag
diag' = Diagram :: Gr DiagNodeLab DiagLinkLab -> Int -> Diag
Diagram {diagGraph :: Gr DiagNodeLab DiagLinkLab
diagGraph = (Int, DiagNodeLab)
-> Gr DiagNodeLab DiagLinkLab -> Gr DiagNodeLab DiagLinkLab
forall (gr :: * -> * -> *) a b.
DynGraph gr =>
LNode a -> gr a b -> gr a b
insNode (Int
node, DiagNodeLab
nodeContents) Gr DiagNodeLab DiagLinkLab
diagGr,
                         numberOfEdges :: Int
numberOfEdges = Diag -> Int
numberOfEdges Diag
diag}
         newDiagNode :: DiagNodeSig
newDiagNode = Int -> NodeSig -> DiagNodeSig
Diag_node_sig Int
node NodeSig
newNodeSig
     Diag
diag'' <- LogicGraph -> Diag -> [DiagNodeSig] -> DiagNodeSig -> Result Diag
insInclusionEdges LogicGraph
lgraph Diag
diag' [DiagNodeSig]
srcNodes DiagNodeSig
newDiagNode
     (DiagNodeSig, Diag) -> String -> Diag -> Result (DiagNodeSig, Diag)
forall a. a -> String -> Diag -> Result a
printDiag (DiagNodeSig
newDiagNode, Diag
diag'') "extendDiagramIncl" Diag
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
             -> IRI       -- ^ the name of the node to be inserted
             -> DGOrigin
             -> Result (NodeSig, DGraph)
-- ^ returns the target signature of the morphism and the resulting DGraph
extendDGraph :: DGraph
-> NodeSig
-> GMorphism
-> IRI
-> DGOrigin
-> Result (NodeSig, DGraph)
extendDGraph dg :: DGraph
dg (NodeSig n :: Int
n _) morph :: GMorphism
morph i :: IRI
i orig :: DGOrigin
orig = case GMorphism -> G_sign
forall object morphism.
Category object morphism =>
morphism -> object
cod GMorphism
morph of
    targetSig :: G_sign
targetSig@(G_sign lid :: lid
lid tar :: ExtSign sign symbol
tar ind :: SigId
ind) -> let
      name :: NodeName
name = DGraph -> IRI -> Int -> NodeName
ensureUniqueNames DGraph
dg IRI
i 1
      nodeContents :: DGNodeLab
nodeContents = NodeName -> DGOrigin -> G_theory -> DGNodeLab
newNodeLab NodeName
name DGOrigin
orig
        (G_theory -> DGNodeLab) -> G_theory -> DGNodeLab
forall a b. (a -> b) -> a -> b
$ lid -> ExtSign sign symbol -> SigId -> G_theory
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> ExtSign sign symbol -> SigId -> G_theory
noSensGTheory lid
lid ExtSign sign symbol
tar SigId
ind
      linkContents :: DGLinkLab
linkContents = GMorphism -> DGLinkOrigin -> DGLinkLab
globDefLink GMorphism
morph DGLinkOrigin
SeeTarget
      node :: Int
node = DGraph -> Int
getNewNodeDG DGraph
dg
      dg' :: DGraph
dg' = LNode DGNodeLab -> DGraph -> DGraph
insNodeDG (Int
node, DGNodeLab
nodeContents) DGraph
dg
      dg'' :: DGraph
dg'' = (LEdge DGLinkLab, DGraph) -> DGraph
forall a b. (a, b) -> b
snd ((LEdge DGLinkLab, DGraph) -> DGraph)
-> (LEdge DGLinkLab, DGraph) -> DGraph
forall a b. (a -> b) -> a -> b
$ LEdge DGLinkLab -> DGraph -> (LEdge DGLinkLab, DGraph)
insLEdgeDG (Int
n, Int
node, DGLinkLab
linkContents) DGraph
dg'
      in (NodeSig, DGraph) -> Result (NodeSig, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> G_sign -> NodeSig
NodeSig Int
node G_sign
targetSig, DGraph
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
             -> IRI       -- ^ the name of the node to be inserted
             -> DGOrigin
             -> Result (NodeSig, DGraph)
-- ^ returns the source signature of the morphism and the resulting DGraph
extendDGraphRev :: DGraph
-> NodeSig
-> GMorphism
-> IRI
-> DGOrigin
-> Result (NodeSig, DGraph)
extendDGraphRev dg :: DGraph
dg (NodeSig n :: Int
n _) morph :: GMorphism
morph i :: IRI
i orig :: DGOrigin
orig = case GMorphism -> G_sign
forall object morphism.
Category object morphism =>
morphism -> object
dom GMorphism
morph of
    sourceSig :: G_sign
sourceSig@(G_sign lid :: lid
lid src :: ExtSign sign symbol
src ind :: SigId
ind) -> let
      nodeContents :: DGNodeLab
nodeContents = NodeName -> DGOrigin -> G_theory -> DGNodeLab
newNodeLab (DGraph -> IRI -> Int -> NodeName
ensureUniqueNames DGraph
dg IRI
i 1) DGOrigin
orig
        (G_theory -> DGNodeLab) -> G_theory -> DGNodeLab
forall a b. (a -> b) -> a -> b
$ lid -> ExtSign sign symbol -> SigId -> G_theory
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> ExtSign sign symbol -> SigId -> G_theory
noSensGTheory lid
lid ExtSign sign symbol
src SigId
ind
      linkContents :: DGLinkLab
linkContents = GMorphism -> DGLinkOrigin -> DGLinkLab
globDefLink GMorphism
morph DGLinkOrigin
SeeSource
      node :: Int
node = DGraph -> Int
getNewNodeDG DGraph
dg
      dg' :: DGraph
dg' = LNode DGNodeLab -> DGraph -> DGraph
insNodeDG (Int
node, DGNodeLab
nodeContents) DGraph
dg
      dg'' :: DGraph
dg'' = (LEdge DGLinkLab, DGraph) -> DGraph
forall a b. (a, b) -> b
snd ((LEdge DGLinkLab, DGraph) -> DGraph)
-> (LEdge DGLinkLab, DGraph) -> DGraph
forall a b. (a -> b) -> a -> b
$ LEdge DGLinkLab -> DGraph -> (LEdge DGLinkLab, DGraph)
insLEdgeDG (Int
node, Int
n, DGLinkLab
linkContents) DGraph
dg'
      in (NodeSig, DGraph) -> Result (NodeSig, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> G_sign -> NodeSig
NodeSig Int
node G_sign
sourceSig, DGraph
dg'')

{- | Extend the development graph with given morphism pointing to
given NodeSig -}
extendDGraphRevHide :: DGraph    -- ^ the development graph to be extended
             -> NodeSig   -- ^ the NodeSig to which the morphism points
             -> GMorphism -- ^ the morphism to be inserted
             -> IRI       -- ^ the name of the node to be inserted
             -> DGOrigin
             -> Result (NodeSig, DGraph)
-- ^ returns the source signature of the morphism and the resulting DGraph
extendDGraphRevHide :: DGraph
-> NodeSig
-> GMorphism
-> IRI
-> DGOrigin
-> Result (NodeSig, DGraph)
extendDGraphRevHide dg :: DGraph
dg (NodeSig n :: Int
n _) morph :: GMorphism
morph i :: IRI
i orig :: DGOrigin
orig = case GMorphism -> G_sign
forall object morphism.
Category object morphism =>
morphism -> object
dom GMorphism
morph of
    sourceSig :: G_sign
sourceSig@(G_sign lid :: lid
lid src :: ExtSign sign symbol
src ind :: SigId
ind) -> let
      nodeContents :: DGNodeLab
nodeContents = NodeName -> DGOrigin -> G_theory -> DGNodeLab
newNodeLab (DGraph -> IRI -> Int -> NodeName
ensureUniqueNames DGraph
dg IRI
i 1) DGOrigin
orig
        (G_theory -> DGNodeLab) -> G_theory -> DGNodeLab
forall a b. (a -> b) -> a -> b
$ lid -> ExtSign sign symbol -> SigId -> G_theory
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> ExtSign sign symbol -> SigId -> G_theory
noSensGTheory lid
lid ExtSign sign symbol
src SigId
ind
      linkContents :: DGLinkLab
linkContents = GMorphism -> DGLinkType -> DGLinkOrigin -> DGLinkLab
defDGLink GMorphism
morph DGLinkType
HidingDefLink
                                      DGLinkOrigin
DGLinkProof
      node :: Int
node = DGraph -> Int
getNewNodeDG DGraph
dg
      dg' :: DGraph
dg' = LNode DGNodeLab -> DGraph -> DGraph
insNodeDG (Int
node, DGNodeLab
nodeContents) DGraph
dg
      dg'' :: DGraph
dg'' = (LEdge DGLinkLab, DGraph) -> DGraph
forall a b. (a, b) -> b
snd ((LEdge DGLinkLab, DGraph) -> DGraph)
-> (LEdge DGLinkLab, DGraph) -> DGraph
forall a b. (a -> b) -> a -> b
$ LEdge DGLinkLab -> DGraph -> (LEdge DGLinkLab, DGraph)
insLEdgeDG (Int
n, Int
node, DGLinkLab
linkContents) DGraph
dg'
      in (NodeSig, DGraph) -> Result (NodeSig, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> G_sign -> NodeSig
NodeSig Int
node G_sign
sourceSig, DGraph
dg'')

extendDiagramWithMorphismRevHide :: 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
                             -> IRI       
                             -- ^ the name of the node to be inserted
                             -> 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
extendDiagramWithMorphismRevHide :: Range
-> LogicGraph
-> Diag
-> DGraph
-> DiagNodeSig
-> GMorphism
-> IRI
-> String
-> DGOrigin
-> Result (DiagNodeSig, Diag, DGraph)
extendDiagramWithMorphismRevHide pos :: Range
pos _ diag :: Diag
diag dg :: DGraph
dg (Diag_node_sig n :: Int
n nsig :: NodeSig
nsig)
                             mor :: GMorphism
mor i :: IRI
i desc :: String
desc orig :: DGOrigin
orig =
  if NodeSig -> G_sign
getSig NodeSig
nsig G_sign -> G_sign -> Bool
forall a. Eq a => a -> a -> Bool
== GMorphism -> G_sign
forall object morphism.
Category object morphism =>
morphism -> object
cod GMorphism
mor then
     do (sourceSig :: NodeSig
sourceSig, dg' :: DGraph
dg') <- DGraph
-> NodeSig
-> GMorphism
-> IRI
-> DGOrigin
-> Result (NodeSig, DGraph)
extendDGraphRevHide DGraph
dg NodeSig
nsig GMorphism
mor IRI
i DGOrigin
orig
        let nodeContents :: DiagNodeLab
nodeContents = DiagNode :: NodeSig -> String -> DiagNodeLab
DiagNode {dn_sig :: NodeSig
dn_sig = NodeSig
sourceSig, dn_desc :: String
dn_desc = String
desc}
            diagGr :: Gr DiagNodeLab DiagLinkLab
diagGr = Diag -> Gr DiagNodeLab DiagLinkLab
diagGraph Diag
diag
            node :: Int
node = Gr DiagNodeLab DiagLinkLab -> Int
forall a b. Gr a b -> Int
Tree.getNewNode Gr DiagNodeLab DiagLinkLab
diagGr
            diagGr' :: Gr DiagNodeLab DiagLinkLab
diagGr' = (Int, DiagNodeLab)
-> Gr DiagNodeLab DiagLinkLab -> Gr DiagNodeLab DiagLinkLab
forall (gr :: * -> * -> *) a b.
DynGraph gr =>
LNode a -> gr a b -> gr a b
insNode (Int
node, DiagNodeLab
nodeContents) Gr DiagNodeLab DiagLinkLab
diagGr
            diag' :: Diag
diag' = Diagram :: Gr DiagNodeLab DiagLinkLab -> Int -> Diag
Diagram { diagGraph :: Gr DiagNodeLab DiagLinkLab
diagGraph = LEdge DiagLinkLab
-> Gr DiagNodeLab DiagLinkLab -> Gr DiagNodeLab DiagLinkLab
forall (gr :: * -> * -> *) b a.
DynGraph gr =>
LEdge b -> gr a b -> gr a b
insEdge (Int
node, Int
n, DiagLink :: GMorphism -> Int -> DiagLinkLab
DiagLink {
                                dl_morphism :: GMorphism
dl_morphism = GMorphism
mor ,
                                dl_number :: Int
dl_number = Diag -> Int
numberOfEdges Diag
diag Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1}) Gr DiagNodeLab DiagLinkLab
diagGr',
                              numberOfEdges :: Int
numberOfEdges = Diag -> Int
numberOfEdges Diag
diag Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1 }
        (DiagNodeSig, Diag, DGraph)
-> String -> Diag -> Result (DiagNodeSig, Diag, DGraph)
forall a. a -> String -> Diag -> Result a
printDiag (Int -> NodeSig -> DiagNodeSig
Diag_node_sig Int
node NodeSig
sourceSig, Diag
diag', DGraph
dg')
               "extendDiagramWithMorphismRev" Diag
diag'
     else String -> Range -> Result (DiagNodeSig, Diag, DGraph)
forall a. String -> Range -> Result a
fatal_error
     ("Internal error: Static.ArchDiagram.extendDiagramWithMorphismRev:\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++
      " the morphism codomain differs from the signature in given target node")
     Range
pos


{- | 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
                          -> IRI     
                          -- ^ the name of the node to be inserted         
                          -> 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 :: Range
-> LogicGraph
-> Diag
-> DGraph
-> DiagNodeSig
-> GMorphism
-> IRI
-> String
-> DGOrigin
-> Result (DiagNodeSig, Diag, DGraph)
extendDiagramWithMorphism pos :: Range
pos _ diag :: Diag
diag dg :: DGraph
dg (Diag_node_sig n :: Int
n nsig :: NodeSig
nsig) mor :: GMorphism
mor i :: IRI
i desc :: String
desc orig :: DGOrigin
orig =
  if NodeSig -> G_sign
getSig NodeSig
nsig G_sign -> G_sign -> Bool
forall a. Eq a => a -> a -> Bool
== GMorphism -> G_sign
forall object morphism.
Category object morphism =>
morphism -> object
dom GMorphism
mor then
     do (targetSig :: NodeSig
targetSig, dg' :: DGraph
dg') <- DGraph
-> NodeSig
-> GMorphism
-> IRI
-> DGOrigin
-> Result (NodeSig, DGraph)
extendDGraph DGraph
dg NodeSig
nsig GMorphism
mor IRI
i DGOrigin
orig
        let nodeContents :: DiagNodeLab
nodeContents = DiagNode :: NodeSig -> String -> DiagNodeLab
DiagNode {dn_sig :: NodeSig
dn_sig = NodeSig
targetSig, dn_desc :: String
dn_desc = String
desc}
            diagGr :: Gr DiagNodeLab DiagLinkLab
diagGr = Diag -> Gr DiagNodeLab DiagLinkLab
diagGraph Diag
diag
            node :: Int
node = Gr DiagNodeLab DiagLinkLab -> Int
forall a b. Gr a b -> Int
Tree.getNewNode Gr DiagNodeLab DiagLinkLab
diagGr
            diagGr' :: Gr DiagNodeLab DiagLinkLab
diagGr' = (Int, DiagNodeLab)
-> Gr DiagNodeLab DiagLinkLab -> Gr DiagNodeLab DiagLinkLab
forall (gr :: * -> * -> *) a b.
DynGraph gr =>
LNode a -> gr a b -> gr a b
insNode (Int
node, DiagNodeLab
nodeContents) Gr DiagNodeLab DiagLinkLab
diagGr
            diag' :: Diag
diag' = Diagram :: Gr DiagNodeLab DiagLinkLab -> Int -> Diag
Diagram {diagGraph :: Gr DiagNodeLab DiagLinkLab
diagGraph = LEdge DiagLinkLab
-> Gr DiagNodeLab DiagLinkLab -> Gr DiagNodeLab DiagLinkLab
forall (gr :: * -> * -> *) b a.
DynGraph gr =>
LEdge b -> gr a b -> gr a b
insEdge (Int
n, Int
node, DiagLink :: GMorphism -> Int -> DiagLinkLab
DiagLink {
                               dl_morphism :: GMorphism
dl_morphism = GMorphism
mor,
                               dl_number :: Int
dl_number = Diag -> Int
numberOfEdges Diag
diag Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1 }) Gr DiagNodeLab DiagLinkLab
diagGr',
                            numberOfEdges :: Int
numberOfEdges = Diag -> Int
numberOfEdges Diag
diag Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1 }
        (DiagNodeSig, Diag, DGraph)
-> String -> Diag -> Result (DiagNodeSig, Diag, DGraph)
forall a. a -> String -> Diag -> Result a
printDiag (Int -> NodeSig -> DiagNodeSig
Diag_node_sig Int
node NodeSig
targetSig, Diag
diag', DGraph
dg')
                      "extendDiagramWithMorphism" Diag
diag'
     else String -> Range -> Result (DiagNodeSig, Diag, DGraph)
forall a. String -> Range -> Result a
fatal_error
     ("Internal error: Static.ArchDiagram.extendDiagramWithMorphism:" String -> ShowS
forall a. [a] -> [a] -> [a]
++
      "\n the morphism domain differs from the signature in given source node")
                         Range
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
                             -> IRI       -- ^ the name of the node to be inserted
                             -> DGOrigin      -- ^ the origin of the new node
                             -> Result (DiagNodeSig, Diag, DGraph)
-- ^ returns the new node, the extended diagram and extended development graph
extendDiagramWithMorphismRev :: Range
-> LogicGraph
-> Diag
-> DGraph
-> DiagNodeSig
-> GMorphism
-> String
-> IRI
-> DGOrigin
-> Result (DiagNodeSig, Diag, DGraph)
extendDiagramWithMorphismRev pos :: Range
pos _ diag :: Diag
diag dg :: DGraph
dg (Diag_node_sig n :: Int
n nsig :: NodeSig
nsig)
                             mor :: GMorphism
mor desc :: String
desc i :: IRI
i orig :: DGOrigin
orig =
  if NodeSig -> G_sign
getSig NodeSig
nsig G_sign -> G_sign -> Bool
forall a. Eq a => a -> a -> Bool
== GMorphism -> G_sign
forall object morphism.
Category object morphism =>
morphism -> object
cod GMorphism
mor then
     do (sourceSig :: NodeSig
sourceSig, dg' :: DGraph
dg') <- DGraph
-> NodeSig
-> GMorphism
-> IRI
-> DGOrigin
-> Result (NodeSig, DGraph)
extendDGraphRev DGraph
dg NodeSig
nsig GMorphism
mor IRI
i DGOrigin
orig
        let nodeContents :: DiagNodeLab
nodeContents = DiagNode :: NodeSig -> String -> DiagNodeLab
DiagNode {dn_sig :: NodeSig
dn_sig = NodeSig
sourceSig, dn_desc :: String
dn_desc = String
desc}
            diagGr :: Gr DiagNodeLab DiagLinkLab
diagGr = Diag -> Gr DiagNodeLab DiagLinkLab
diagGraph Diag
diag
            node :: Int
node = Gr DiagNodeLab DiagLinkLab -> Int
forall a b. Gr a b -> Int
Tree.getNewNode Gr DiagNodeLab DiagLinkLab
diagGr
            diagGr' :: Gr DiagNodeLab DiagLinkLab
diagGr' = (Int, DiagNodeLab)
-> Gr DiagNodeLab DiagLinkLab -> Gr DiagNodeLab DiagLinkLab
forall (gr :: * -> * -> *) a b.
DynGraph gr =>
LNode a -> gr a b -> gr a b
insNode (Int
node, DiagNodeLab
nodeContents) Gr DiagNodeLab DiagLinkLab
diagGr
            diag' :: Diag
diag' = Diagram :: Gr DiagNodeLab DiagLinkLab -> Int -> Diag
Diagram { diagGraph :: Gr DiagNodeLab DiagLinkLab
diagGraph = LEdge DiagLinkLab
-> Gr DiagNodeLab DiagLinkLab -> Gr DiagNodeLab DiagLinkLab
forall (gr :: * -> * -> *) b a.
DynGraph gr =>
LEdge b -> gr a b -> gr a b
insEdge (Int
node, Int
n, DiagLink :: GMorphism -> Int -> DiagLinkLab
DiagLink {
                                dl_morphism :: GMorphism
dl_morphism = GMorphism
mor ,
                                dl_number :: Int
dl_number = Diag -> Int
numberOfEdges Diag
diag Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1}) Gr DiagNodeLab DiagLinkLab
diagGr',
                              numberOfEdges :: Int
numberOfEdges = Diag -> Int
numberOfEdges Diag
diag Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1 }
        (DiagNodeSig, Diag, DGraph)
-> String -> Diag -> Result (DiagNodeSig, Diag, DGraph)
forall a. a -> String -> Diag -> Result a
printDiag (Int -> NodeSig -> DiagNodeSig
Diag_node_sig Int
node NodeSig
sourceSig, Diag
diag', DGraph
dg')
               "extendDiagramWithMorphismRev" Diag
diag'
     else String -> Range -> Result (DiagNodeSig, Diag, DGraph)
forall a. String -> Range -> Result a
fatal_error
     ("Internal error: Static.ArchDiagram.extendDiagramWithMorphismRev:\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++
      " the morphism codomain differs from the signature in given target node")
     Range
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
-> DiagNodeSig
-> GMorphism
-> NodeSig
-> String
-> Result (DiagNodeSig, Diag)
extendDiagram diag :: Diag
diag (Diag_node_sig n :: Int
n _) edgeMorph :: GMorphism
edgeMorph newNodeSig :: NodeSig
newNodeSig desc :: String
desc =
  do let nodeContents :: DiagNodeLab
nodeContents = DiagNode :: NodeSig -> String -> DiagNodeLab
DiagNode {dn_sig :: NodeSig
dn_sig = NodeSig
newNodeSig, dn_desc :: String
dn_desc = String
desc}
         diagGr :: Gr DiagNodeLab DiagLinkLab
diagGr = Diag -> Gr DiagNodeLab DiagLinkLab
diagGraph Diag
diag
         node :: Int
node = Gr DiagNodeLab DiagLinkLab -> Int
forall a b. Gr a b -> Int
Tree.getNewNode Gr DiagNodeLab DiagLinkLab
diagGr
         diagGr' :: Gr DiagNodeLab DiagLinkLab
diagGr' = (Int, DiagNodeLab)
-> Gr DiagNodeLab DiagLinkLab -> Gr DiagNodeLab DiagLinkLab
forall (gr :: * -> * -> *) a b.
DynGraph gr =>
LNode a -> gr a b -> gr a b
insNode (Int
node, DiagNodeLab
nodeContents) Gr DiagNodeLab DiagLinkLab
diagGr
         diag' :: Diag
diag' = Diagram :: Gr DiagNodeLab DiagLinkLab -> Int -> Diag
Diagram {diagGraph :: Gr DiagNodeLab DiagLinkLab
diagGraph = LEdge DiagLinkLab
-> Gr DiagNodeLab DiagLinkLab -> Gr DiagNodeLab DiagLinkLab
forall (gr :: * -> * -> *) b a.
DynGraph gr =>
LEdge b -> gr a b -> gr a b
insEdge (Int
n, Int
node, DiagLink :: GMorphism -> Int -> DiagLinkLab
DiagLink {
                             dl_morphism :: GMorphism
dl_morphism = GMorphism
edgeMorph,
                             dl_number :: Int
dl_number = Diag -> Int
numberOfEdges Diag
diag Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1 }) Gr DiagNodeLab DiagLinkLab
diagGr',
                         numberOfEdges :: Int
numberOfEdges = Diag -> Int
numberOfEdges Diag
diag Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1 }
         newDiagNode :: DiagNodeSig
newDiagNode = Int -> NodeSig -> DiagNodeSig
Diag_node_sig Int
node NodeSig
newNodeSig
     (DiagNodeSig, Diag) -> String -> Diag -> Result (DiagNodeSig, Diag)
forall a. a -> String -> Diag -> Result a
printDiag (DiagNodeSig
newDiagNode, Diag
diag') "extendDiagram" Diag
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 :: lid -> Diag -> Result (Gr sign (Int, morphism))
homogeniseDiagram targetLid :: lid
targetLid diag :: Diag
diag =
    do let convertNode :: (a, DiagNodeLab) -> m (a, b)
convertNode (n :: a
n, dn :: DiagNodeLab
dn) =
               do G_sign srcLid :: lid
srcLid sig :: ExtSign sign symbol
sig _ <- G_sign -> m G_sign
forall (m :: * -> *) a. Monad m => a -> m a
return (G_sign -> m G_sign) -> G_sign -> m G_sign
forall a b. (a -> b) -> a -> b
$ NodeSig -> G_sign
getSig (NodeSig -> G_sign) -> NodeSig -> G_sign
forall a b. (a -> b) -> a -> b
$ DiagNodeLab -> NodeSig
dn_sig DiagNodeLab
dn
                  ExtSign b symbol
sig' <- lid -> lid -> String -> ExtSign sign symbol -> m (ExtSign b symbol)
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1
-> lid2
-> String
-> ExtSign sign1 symbol1
-> m (ExtSign sign2 symbol2)
coerceSign lid
srcLid lid
targetLid "" ExtSign sign symbol
sig
                  (a, b) -> m (a, b)
forall (m :: * -> *) a. Monad m => a -> m a
return (a
n, ExtSign b symbol -> b
forall sign symbol. ExtSign sign symbol -> sign
plainSign ExtSign b symbol
sig')
           convertEdge :: (a, b, DiagLinkLab) -> m (a, b, (Int, b))
convertEdge (n1 :: a
n1, n2 :: b
n2, DiagLink {
                   dl_morphism :: DiagLinkLab -> GMorphism
dl_morphism = GMorphism cid :: cid
cid _ _ mor :: morphism2
mor _, dl_number :: DiagLinkLab -> Int
dl_number = Int
nr})
               = if AnyComorphism -> Bool
isIdComorphism (cid -> AnyComorphism
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> AnyComorphism
Comorphism cid
cid) then
                 do b
mor' <- lid2 -> lid -> String -> morphism2 -> m b
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1 -> lid2 -> String -> morphism1 -> m morphism2
coerceMorphism (cid -> lid2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid2
targetLogic cid
cid) lid
targetLid "" morphism2
mor
                    (a, b, (Int, b)) -> m (a, b, (Int, b))
forall (m :: * -> *) a. Monad m => a -> m a
return (a
n1, b
n2, (Int
nr, b
mor'))
                 else String -> m (a, b, (Int, b))
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> m (a, b, (Int, b))) -> String -> m (a, b, (Int, b))
forall a b. (a -> b) -> a -> b
$
                  "Trying to coerce a morphism between different logics.\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++
                  "Heterogeneous specifications are not fully supported yet."
           convertNodes :: gr b b -> [(Int, DiagNodeLab)] -> m (gr b b)
convertNodes cDiag :: gr b b
cDiag [] = gr b b -> m (gr b b)
forall (m :: * -> *) a. Monad m => a -> m a
return gr b b
cDiag
           convertNodes cDiag :: gr b b
cDiag (lNode :: (Int, DiagNodeLab)
lNode : lNodes :: [(Int, DiagNodeLab)]
lNodes) =
               do (Int, b)
convNode <- (Int, DiagNodeLab) -> m (Int, b)
forall (m :: * -> *) sublogics2 basic_spec2 sentence2 symb_items2
       symb_map_items2 b morphism2 symbol raw_symbol2 proof_tree2 a.
(Logic
   lid
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   b
   morphism2
   symbol
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
(a, DiagNodeLab) -> m (a, b)
convertNode (Int, DiagNodeLab)
lNode
                  let cDiag' :: gr b b
cDiag' = (Int, b) -> gr b b -> gr b b
forall (gr :: * -> * -> *) a b.
DynGraph gr =>
LNode a -> gr a b -> gr a b
insNode (Int, b)
convNode gr b b
cDiag
                  gr b b -> [(Int, DiagNodeLab)] -> m (gr b b)
convertNodes gr b b
cDiag' [(Int, DiagNodeLab)]
lNodes
           convertEdges :: gr a (Int, b) -> [LEdge DiagLinkLab] -> m (gr a (Int, b))
convertEdges cDiag :: gr a (Int, b)
cDiag [] = gr a (Int, b) -> m (gr a (Int, b))
forall (m :: * -> *) a. Monad m => a -> m a
return gr a (Int, b)
cDiag
           convertEdges cDiag :: gr a (Int, b)
cDiag (lEdge :: LEdge DiagLinkLab
lEdge : lEdges :: [LEdge DiagLinkLab]
lEdges) =
               do (Int, Int, (Int, b))
convEdge <- LEdge DiagLinkLab -> m (Int, Int, (Int, b))
forall sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 b symbol2 raw_symbol2 proof_tree2 (m :: * -> *) a b.
(Logic
   lid
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   b
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
(a, b, DiagLinkLab) -> m (a, b, (Int, b))
convertEdge LEdge DiagLinkLab
lEdge
                  let cDiag' :: gr a (Int, b)
cDiag' = (Int, Int, (Int, b)) -> gr a (Int, b) -> gr a (Int, b)
forall (gr :: * -> * -> *) b a.
DynGraph gr =>
LEdge b -> gr a b -> gr a b
insEdge (Int, Int, (Int, b))
convEdge gr a (Int, b)
cDiag
                  gr a (Int, b) -> [LEdge DiagLinkLab] -> m (gr a (Int, b))
convertEdges gr a (Int, b)
cDiag' [LEdge DiagLinkLab]
lEdges
           dNodes :: [(Int, DiagNodeLab)]
dNodes = Gr DiagNodeLab DiagLinkLab -> [(Int, DiagNodeLab)]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode a]
labNodes (Gr DiagNodeLab DiagLinkLab -> [(Int, DiagNodeLab)])
-> Gr DiagNodeLab DiagLinkLab -> [(Int, DiagNodeLab)]
forall a b. (a -> b) -> a -> b
$ Diag -> Gr DiagNodeLab DiagLinkLab
diagGraph Diag
diag
           dEdges :: [LEdge DiagLinkLab]
dEdges = Gr DiagNodeLab DiagLinkLab -> [LEdge DiagLinkLab]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LEdge b]
labEdges (Gr DiagNodeLab DiagLinkLab -> [LEdge DiagLinkLab])
-> Gr DiagNodeLab DiagLinkLab -> [LEdge DiagLinkLab]
forall a b. (a -> b) -> a -> b
$ Diag -> Gr DiagNodeLab DiagLinkLab
diagGraph Diag
diag
       -- insert converted nodes to an empty diagram
       Gr sign (Int, morphism)
cDiag <- Gr sign (Int, morphism)
-> [(Int, DiagNodeLab)] -> Result (Gr sign (Int, morphism))
forall (m :: * -> *) sublogics2 basic_spec2 sentence2 symb_items2
       symb_map_items2 b morphism2 symbol raw_symbol2 proof_tree2
       (gr :: * -> * -> *) b.
(Logic
   lid
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   b
   morphism2
   symbol
   raw_symbol2
   proof_tree2,
 MonadFail m, DynGraph gr) =>
gr b b -> [(Int, DiagNodeLab)] -> m (gr b b)
convertNodes Gr sign (Int, morphism)
forall (gr :: * -> * -> *) a b. Graph gr => gr a b
Graph.empty [(Int, DiagNodeLab)]
dNodes
       -- insert converted edges to the diagram containing only nodes
       Gr sign (Int, morphism)
-> [LEdge DiagLinkLab] -> Result (Gr sign (Int, morphism))
forall (m :: * -> *) sublogics2 basic_spec2 sentence2 symb_items2
       symb_map_items2 sign2 b symbol2 raw_symbol2 proof_tree2
       (gr :: * -> * -> *) a.
(Logic
   lid
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   b
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m, DynGraph gr) =>
gr a (Int, b) -> [LEdge DiagLinkLab] -> m (gr a (Int, b))
convertEdges Gr sign (Int, morphism)
cDiag [LEdge DiagLinkLab]
dEdges

-- | Create a graph containing descriptions of nodes and edges.
diagDesc :: Diag
         -> Tree.Gr String String
diagDesc :: Diag -> Gr String String
diagDesc diag :: Diag
diag =
    let insNodeDesc :: gr String b -> (Int, DiagNodeLab) -> gr String b
insNodeDesc g :: gr String b
g (n :: Int
n, DiagNode { dn_desc :: DiagNodeLab -> String
dn_desc = String
desc }) =
            if String
desc String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "" then gr String b
g else LNode String -> gr String b -> gr String b
forall (gr :: * -> * -> *) a b.
DynGraph gr =>
LNode a -> gr a b -> gr a b
insNode (Int
n, String
desc) gr String b
g
    in (Gr String String -> (Int, DiagNodeLab) -> Gr String String)
-> Gr String String -> [(Int, DiagNodeLab)] -> Gr String String
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Gr String String -> (Int, DiagNodeLab) -> Gr String String
forall (gr :: * -> * -> *) b.
DynGraph gr =>
gr String b -> (Int, DiagNodeLab) -> gr String b
insNodeDesc Gr String String
forall (gr :: * -> * -> *) a b. Graph gr => gr a b
Graph.empty ([(Int, DiagNodeLab)] -> Gr String String)
-> (Gr DiagNodeLab DiagLinkLab -> [(Int, DiagNodeLab)])
-> Gr DiagNodeLab DiagLinkLab
-> Gr String String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Gr DiagNodeLab DiagLinkLab -> [(Int, DiagNodeLab)]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode a]
labNodes (Gr DiagNodeLab DiagLinkLab -> Gr String String)
-> Gr DiagNodeLab DiagLinkLab -> Gr String String
forall a b. (a -> b) -> a -> b
$ Diag -> Gr DiagNodeLab DiagLinkLab
diagGraph Diag
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 :: LogicGraph -> [DiagNodeSig] -> NodeSig -> Result [(Int, GMorphism)]
inclusionSink lgraph :: LogicGraph
lgraph srcNodes :: [DiagNodeSig]
srcNodes tnsig :: NodeSig
tnsig =
    do let insmorph :: Result [(Int, GMorphism)]
-> DiagNodeSig -> Result [(Int, GMorphism)]
insmorph ls :: Result [(Int, GMorphism)]
ls dns :: DiagNodeSig
dns = do
             [(Int, GMorphism)]
l <- Result [(Int, GMorphism)]
ls
             case DiagNodeSig
dns of
               Diag_node_sig n :: Int
n nsig :: NodeSig
nsig -> do
                 GMorphism
incl <- LogicGraph -> G_sign -> G_sign -> Result GMorphism
ginclusion LogicGraph
lgraph (NodeSig -> G_sign
getSig NodeSig
nsig) (NodeSig -> G_sign
getSig NodeSig
tnsig)
                 [(Int, GMorphism)] -> Result [(Int, GMorphism)]
forall (m :: * -> *) a. Monad m => a -> m a
return ((Int
n, GMorphism
incl) (Int, GMorphism) -> [(Int, GMorphism)] -> [(Int, GMorphism)]
forall a. a -> [a] -> [a]
: [(Int, GMorphism)]
l)
       (Result [(Int, GMorphism)]
 -> DiagNodeSig -> Result [(Int, GMorphism)])
-> Result [(Int, GMorphism)]
-> [DiagNodeSig]
-> Result [(Int, GMorphism)]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Result [(Int, GMorphism)]
-> DiagNodeSig -> Result [(Int, GMorphism)]
insmorph ([(Int, GMorphism)] -> Result [(Int, GMorphism)]
forall (m :: * -> *) a. Monad m => a -> m a
return []) [DiagNodeSig]
srcNodes

{- | Build a diagram that extends the given diagram with an
edge between existing nodes.
The edge is labelled with a given signature morphism. Extends the
development graph with the given morphism as well. -}
extendDiagramWithEdge :: 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
                          -> DiagNodeSig
                          -- ^ the target node of the edge
                          -> GMorphism
                          -- ^ the morphism as label for the new edge
                          -> DGLinkOrigin -- ^ the origin of the new edge
                          -> Result (Diag, DGraph)
-- ^ returns the extended diagram and extended development graph
extendDiagramWithEdge :: Range
-> LogicGraph
-> Diag
-> DGraph
-> DiagNodeSig
-> DiagNodeSig
-> GMorphism
-> DGLinkOrigin
-> Result (Diag, DGraph)
extendDiagramWithEdge pos :: Range
pos _ diag :: Diag
diag dg :: DGraph
dg
                          (Diag_node_sig s :: Int
s ssig :: NodeSig
ssig)
                          (Diag_node_sig t :: Int
t tsig :: NodeSig
tsig)
                          mor :: GMorphism
mor orig :: DGLinkOrigin
orig =
  if NodeSig -> G_sign
getSig NodeSig
tsig G_sign -> G_sign -> Bool
forall a. Eq a => a -> a -> Bool
== GMorphism -> G_sign
forall object morphism.
Category object morphism =>
morphism -> object
cod GMorphism
mor then
   if NodeSig -> G_sign
getSig NodeSig
ssig G_sign -> G_sign -> Bool
forall a. Eq a => a -> a -> Bool
== GMorphism -> G_sign
forall object morphism.
Category object morphism =>
morphism -> object
dom GMorphism
mor then
     do
        let linkContents :: DGLinkLab
linkContents = GMorphism -> DGLinkOrigin -> DGLinkLab
globDefLink GMorphism
mor DGLinkOrigin
orig
            s' :: Int
s' = NodeSig -> Int
getNode NodeSig
ssig
            t' :: Int
t' = NodeSig -> Int
getNode NodeSig
tsig
            dg' :: DGraph
dg' = (LEdge DGLinkLab, DGraph) -> DGraph
forall a b. (a, b) -> b
snd ((LEdge DGLinkLab, DGraph) -> DGraph)
-> (LEdge DGLinkLab, DGraph) -> DGraph
forall a b. (a -> b) -> a -> b
$ LEdge DGLinkLab -> DGraph -> (LEdge DGLinkLab, DGraph)
insLEdgeDG (Int
s', Int
t', DGLinkLab
linkContents) DGraph
dg
            diagGr :: Gr DiagNodeLab DiagLinkLab
diagGr = Diag -> Gr DiagNodeLab DiagLinkLab
diagGraph Diag
diag
            diag' :: Diag
diag' = Diagram :: Gr DiagNodeLab DiagLinkLab -> Int -> Diag
Diagram {diagGraph :: Gr DiagNodeLab DiagLinkLab
diagGraph = LEdge DiagLinkLab
-> Gr DiagNodeLab DiagLinkLab -> Gr DiagNodeLab DiagLinkLab
forall (gr :: * -> * -> *) b a.
DynGraph gr =>
LEdge b -> gr a b -> gr a b
insEdge (Int
s, Int
t, DiagLink :: GMorphism -> Int -> DiagLinkLab
DiagLink {
                               dl_morphism :: GMorphism
dl_morphism = GMorphism
mor,
                               dl_number :: Int
dl_number = Diag -> Int
numberOfEdges Diag
diag Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1 }) Gr DiagNodeLab DiagLinkLab
diagGr,
                            numberOfEdges :: Int
numberOfEdges = Diag -> Int
numberOfEdges Diag
diag Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1 }
        (Diag, DGraph) -> String -> Diag -> Result (Diag, DGraph)
forall a. a -> String -> Diag -> Result a
printDiag (Diag
diag', DGraph
dg')
                      "extendDiagramWithMorphism" Diag
diag'
      else String -> Range -> Result (Diag, DGraph)
forall a. String -> Range -> Result a
fatal_error
     ("Internal error: Static.ArchDiagram.extendDiagramWithMorphism:" String -> ShowS
forall a. [a] -> [a] -> [a]
++
      "\n the morphism domain differs from the signature in given source node")
                         Range
pos
   else String -> Range -> Result (Diag, DGraph)
forall a. String -> Range -> Result a
fatal_error
     ("Internal error: Static.ArchDiagram.extendDiagramWithMorphism:" String -> ShowS
forall a. [a] -> [a] -> [a]
++
      "\n the morphism domain differs from the signature in given target node")
                         Range
pos

matchDiagram :: Node -> Diag -> (Graph.MContext DiagNodeLab DiagLinkLab, Diag)
matchDiagram :: Int -> Diag -> (MContext DiagNodeLab DiagLinkLab, Diag)
matchDiagram n :: Int
n diag :: Diag
diag =
 let (mc :: MContext DiagNodeLab DiagLinkLab
mc, b :: Gr DiagNodeLab DiagLinkLab
b) = Int
-> Gr DiagNodeLab DiagLinkLab
-> (MContext DiagNodeLab DiagLinkLab, Gr DiagNodeLab DiagLinkLab)
forall (gr :: * -> * -> *) a b.
Graph gr =>
Int -> gr a b -> Decomp gr a b
match Int
n (Gr DiagNodeLab DiagLinkLab
 -> (MContext DiagNodeLab DiagLinkLab, Gr DiagNodeLab DiagLinkLab))
-> Gr DiagNodeLab DiagLinkLab
-> (MContext DiagNodeLab DiagLinkLab, Gr DiagNodeLab DiagLinkLab)
forall a b. (a -> b) -> a -> b
$ Diag -> Gr DiagNodeLab DiagLinkLab
diagGraph Diag
diag in (MContext DiagNodeLab DiagLinkLab
mc, Diag
diag {diagGraph :: Gr DiagNodeLab DiagLinkLab
diagGraph = Gr DiagNodeLab DiagLinkLab
b})

copyDiagram :: LogicGraph -> [Node] -> Diag ->
               Result (Diag, Map.Map Node Node)
copyDiagram :: LogicGraph -> [Int] -> Diag -> Result (Diag, Map Int Int)
copyDiagram lg :: LogicGraph
lg ns :: [Int]
ns diag :: Diag
diag = do
 (diag1 :: Diag
diag1, c :: Map Int Int
c) <- Map Int Int
-> LogicGraph -> [Int] -> Diag -> Result (Diag, Map Int Int)
copyDiagramAux Map Int Int
forall k a. Map k a
Map.empty LogicGraph
lg [Int]
ns Diag
diag
 let (_, diag2 :: Diag
diag2) = [Int]
-> Diag -> Map Int Int -> Map Edge Bool -> (Map Edge Bool, Diag)
copyEdges [Int]
ns Diag
diag1 Map Int Int
c Map Edge Bool
forall k a. Map k a
Map.empty
 (Diag, Map Int Int) -> Result (Diag, Map Int Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (Diag
diag2, Map Int Int
c)

copyEdges :: [Node] -> Diag -> Map.Map Node Node -> Map.Map Edge Bool ->
             (Map.Map Edge Bool, Diag)
copyEdges :: [Int]
-> Diag -> Map Int Int -> Map Edge Bool -> (Map Edge Bool, Diag)
copyEdges ns :: [Int]
ns diag :: Diag
diag c :: Map Int Int
c visit :: Map Edge Bool
visit =
 case [Int]
ns of
   [] -> (Map Edge Bool
visit, Diag
diag)
   _ -> let sucs :: [Int]
sucs = [Int] -> [Int]
forall a. Eq a => [a] -> [a]
nub ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ (Int -> [Int]) -> [Int] -> [Int]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Gr DiagNodeLab DiagLinkLab -> Int -> [Int]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> Int -> [Int]
suc (Diag -> Gr DiagNodeLab DiagLinkLab
diagGraph Diag
diag)) [Int]
ns
            sEdges :: [LEdge DiagLinkLab]
sEdges = (Int -> [LEdge DiagLinkLab]) -> [Int] -> [LEdge DiagLinkLab]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Gr DiagNodeLab DiagLinkLab -> Int -> [LEdge DiagLinkLab]
forall (gr :: * -> * -> *) a b.
Graph gr =>
gr a b -> Int -> [LEdge b]
inn (Diag -> Gr DiagNodeLab DiagLinkLab
diagGraph Diag
diag)) [Int]
sucs
            (visit' :: Map Edge Bool
visit', diag' :: Diag
diag') = ((Map Edge Bool, Diag)
 -> LEdge DiagLinkLab -> (Map Edge Bool, Diag))
-> (Map Edge Bool, Diag)
-> [LEdge DiagLinkLab]
-> (Map Edge Bool, Diag)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ (v :: Map Edge Bool
v, d :: Diag
d) e :: LEdge DiagLinkLab
e -> Diag
-> Map Int Int
-> LEdge DiagLinkLab
-> Map Edge Bool
-> (Map Edge Bool, Diag)
copyEdge Diag
d Map Int Int
c LEdge DiagLinkLab
e Map Edge Bool
v) (Map Edge Bool
visit, Diag
diag) [LEdge DiagLinkLab]
sEdges
          in [Int]
-> Diag -> Map Int Int -> Map Edge Bool -> (Map Edge Bool, Diag)
copyEdges [Int]
sucs Diag
diag' Map Int Int
c Map Edge Bool
visit'

copyEdge :: Diag -> Map.Map Node Node -> LEdge DiagLinkLab -> Map.Map Edge Bool ->
            (Map.Map Edge Bool, Diag)
copyEdge :: Diag
-> Map Int Int
-> LEdge DiagLinkLab
-> Map Edge Bool
-> (Map Edge Bool, Diag)
copyEdge diag :: Diag
diag c :: Map Int Int
c (s :: Int
s, t :: Int
t, llab :: DiagLinkLab
llab) visit :: Map Edge Bool
visit =
 if (Int
s, Int
t) Edge -> [Edge] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Map Edge Bool -> [Edge]
forall k a. Map k a -> [k]
Map.keys Map Edge Bool
visit then (Map Edge Bool
visit, Diag
diag)
  else
    -- visit edge
    let visit' :: Map Edge Bool
visit' = Edge -> Bool -> Map Edge Bool -> Map Edge Bool
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Int
s, Int
t) Bool
True Map Edge Bool
visit
        s' :: Int
s' = Int -> Int -> Map Int Int -> Int
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Int
s Int
s Map Int Int
c
        t' :: Int
t' = Int -> Int -> Map Int Int -> Int
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> Int
forall a. HasCallStack => String -> a
error "t") Int
t Map Int Int
c
        diag' :: Diag
diag' = Diagram :: Gr DiagNodeLab DiagLinkLab -> Int -> Diag
Diagram {diagGraph :: Gr DiagNodeLab DiagLinkLab
diagGraph = LEdge DiagLinkLab
-> Gr DiagNodeLab DiagLinkLab -> Gr DiagNodeLab DiagLinkLab
forall (gr :: * -> * -> *) b a.
DynGraph gr =>
LEdge b -> gr a b -> gr a b
insEdge (Int
s', Int
t', DiagLinkLab
llab {
                               dl_number :: Int
dl_number = Diag -> Int
numberOfEdges Diag
diag Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1 }) (Gr DiagNodeLab DiagLinkLab -> Gr DiagNodeLab DiagLinkLab)
-> Gr DiagNodeLab DiagLinkLab -> Gr DiagNodeLab DiagLinkLab
forall a b. (a -> b) -> a -> b
$ Diag -> Gr DiagNodeLab DiagLinkLab
diagGraph Diag
diag,
                            numberOfEdges :: Int
numberOfEdges = Diag -> Int
numberOfEdges Diag
diag Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1 }
    in (Map Edge Bool
visit', Diag
diag')

copyDiagramAux :: Map.Map Node Node -> LogicGraph -> [Node] -> Diag ->
                  Result (Diag, Map.Map Node Node)
copyDiagramAux :: Map Int Int
-> LogicGraph -> [Int] -> Diag -> Result (Diag, Map Int Int)
copyDiagramAux c :: Map Int Int
c lgraph :: LogicGraph
lgraph ns :: [Int]
ns diag :: Diag
diag =
 case [Int]
ns of
  [] -> (Diag, Map Int Int) -> Result (Diag, Map Int Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (Diag
diag, Map Int Int
c)
  _ -> do
    (diag' :: Diag
diag', c' :: Map Int Int
c') <- ((Diag, Map Int Int) -> Int -> Result (Diag, Map Int Int))
-> (Diag, Map Int Int) -> [Int] -> Result (Diag, Map Int Int)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\ (d :: Diag
d, c0 :: Map Int Int
c0) x :: Int
x -> do
                            let DiagNode nsig :: NodeSig
nsig desc :: String
desc = DiagNodeLab -> Maybe DiagNodeLab -> DiagNodeLab
forall a. a -> Maybe a -> a
fromMaybe
                                 (String -> DiagNodeLab
forall a. HasCallStack => String -> a
error (String -> DiagNodeLab) -> String -> DiagNodeLab
forall a b. (a -> b) -> a -> b
$ "copy:" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
x) (Maybe DiagNodeLab -> DiagNodeLab)
-> Maybe DiagNodeLab -> DiagNodeLab
forall a b. (a -> b) -> a -> b
$
                                 Gr DiagNodeLab DiagLinkLab -> Int -> Maybe DiagNodeLab
forall (gr :: * -> * -> *) a b.
Graph gr =>
gr a b -> Int -> Maybe a
lab (Diag -> Gr DiagNodeLab DiagLinkLab
diagGraph Diag
d) Int
x
                            (Diag_node_sig y :: Int
y _, d' :: Diag
d') <- LogicGraph
-> Diag
-> [DiagNodeSig]
-> NodeSig
-> String
-> Result (DiagNodeSig, Diag)
extendDiagramIncl
                                LogicGraph
lgraph Diag
d [] NodeSig
nsig (String -> Result (DiagNodeSig, Diag))
-> String -> Result (DiagNodeSig, Diag)
forall a b. (a -> b) -> a -> b
$ String
desc String -> ShowS
forall a. [a] -> [a] -> [a]
++ "copy"
                            (Diag, Map Int Int) -> Result (Diag, Map Int Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (Diag
d', Int -> Int -> Map Int Int -> Map Int Int
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Int
x Int
y Map Int Int
c0)) (Diag
diag, Map Int Int
c) [Int]
ns
    let sucs :: [Int]
sucs = (Int -> Bool) -> [Int] -> [Int]
forall a. (a -> Bool) -> [a] -> [a]
filter (Int -> [Int] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` Map Int Int -> [Int]
forall k a. Map k a -> [k]
Map.keys Map Int Int
c') ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ [Int] -> [Int]
forall a. Eq a => [a] -> [a]
nub ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ (Int -> [Int]) -> [Int] -> [Int]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap
               (Gr DiagNodeLab DiagLinkLab -> Int -> [Int]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> Int -> [Int]
suc (Diag -> Gr DiagNodeLab DiagLinkLab
diagGraph Diag
diag)) [Int]
ns
    Map Int Int
-> LogicGraph -> [Int] -> Diag -> Result (Diag, Map Int Int)
copyDiagramAux Map Int Int
c' LogicGraph
lgraph [Int]
sucs Diag
diag'


insertFormalParamAndVerifCond :: 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
                             -> NodeSig -- ^ the dg node where the param is based
                             -> DiagNodeSig -- ^ the union of the params
                             -> GMorphism
                             -- ^ the morphism as label for the new edge
                             -> String -- ^ a diagnostic node description
                             -> DGOrigin      -- ^ the origin of the new node
                             -> Result (Diag, DGraph)
-- ^ returns the new node, the extended diagram and extended development graph
insertFormalParamAndVerifCond :: Range
-> LogicGraph
-> Diag
-> DGraph
-> DiagNodeSig
-> NodeSig
-> DiagNodeSig
-> GMorphism
-> String
-> DGOrigin
-> Result (Diag, DGraph)
insertFormalParamAndVerifCond
                                 _pos :: Range
_pos lgraph :: LogicGraph
lgraph
                                 diag0 :: Diag
diag0 dg0 :: DGraph
dg0
                                 _targetNode :: DiagNodeSig
_targetNode@(Diag_node_sig tNode :: Int
tNode tSig :: NodeSig
tSig) fpi :: NodeSig
fpi qB :: DiagNodeSig
qB
                                 mor :: GMorphism
mor
                                 argStr :: String
argStr _origin :: DGOrigin
_origin = do
  let nodeContents :: DiagNodeLab
nodeContents = DiagNode :: NodeSig -> String -> DiagNodeLab
DiagNode {dn_sig :: NodeSig
dn_sig = NodeSig
fpi, dn_desc :: String
dn_desc = String
argStr}
      diagGr :: Gr DiagNodeLab DiagLinkLab
diagGr = Diag -> Gr DiagNodeLab DiagLinkLab
diagGraph Diag
diag0
      node :: Int
node = Gr DiagNodeLab DiagLinkLab -> Int
forall a b. Gr a b -> Int
Tree.getNewNode Gr DiagNodeLab DiagLinkLab
diagGr
      diagGr' :: Gr DiagNodeLab DiagLinkLab
diagGr' = (Int, DiagNodeLab)
-> Gr DiagNodeLab DiagLinkLab -> Gr DiagNodeLab DiagLinkLab
forall (gr :: * -> * -> *) a b.
DynGraph gr =>
LNode a -> gr a b -> gr a b
insNode (Int
node, DiagNodeLab
nodeContents) Gr DiagNodeLab DiagLinkLab
diagGr
       -- this inserts p^F_i
      diag' :: Diag
diag' = Diagram :: Gr DiagNodeLab DiagLinkLab -> Int -> Diag
Diagram { diagGraph :: Gr DiagNodeLab DiagLinkLab
diagGraph = LEdge DiagLinkLab
-> Gr DiagNodeLab DiagLinkLab -> Gr DiagNodeLab DiagLinkLab
forall (gr :: * -> * -> *) b a.
DynGraph gr =>
LEdge b -> gr a b -> gr a b
insEdge (Int
node, Int
tNode, DiagLink :: GMorphism -> Int -> DiagLinkLab
DiagLink {
                                dl_morphism :: GMorphism
dl_morphism = GMorphism
mor ,
                                dl_number :: Int
dl_number = Diag -> Int
numberOfEdges Diag
diag0 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1}) Gr DiagNodeLab DiagLinkLab
diagGr',
                              numberOfEdges :: Int
numberOfEdges = Diag -> Int
numberOfEdges Diag
diag0 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1 }
       -- this inserts mor : p^F_i -> p^A_i
  (dnsig :: DiagNodeSig
dnsig, diag'' :: Diag
diag'', dg'' :: DGraph
dg'') <- (DiagNodeSig, Diag, DGraph)
-> String -> Diag -> Result (DiagNodeSig, Diag, DGraph)
forall a. a -> String -> Diag -> Result a
printDiag (Int -> NodeSig -> DiagNodeSig
Diag_node_sig Int
node NodeSig
fpi, Diag
diag', DGraph
dg0)
               "extendDiagramWithMorphismRev" Diag
diag'
  Diag
diag''' <- LogicGraph -> Diag -> [DiagNodeSig] -> DiagNodeSig -> Result Diag
insInclusionEdges LogicGraph
lgraph Diag
diag'' [DiagNodeSig
dnsig] DiagNodeSig
qB
        {- this inserts incl : p^F_i -> q^B
  now we add the verification condition
  as a theorem link from
  fpi with mor
  to
  tNode -}
  case GMorphism -> G_sign
forall object morphism.
Category object morphism =>
morphism -> object
cod GMorphism
mor of
    cmor :: G_sign
cmor@(G_sign lid :: lid
lid tar :: ExtSign sign symbol
tar ind :: SigId
ind) -> do
      let f :: Int
f = NodeSig -> Int
getNode NodeSig
fpi
          fpiLab :: DGNodeLab
fpiLab = DGraph -> Int -> DGNodeLab
labDG DGraph
dg'' Int
f
          name :: IRI
name = NodeName -> IRI
getName (NodeName -> IRI) -> NodeName -> IRI
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> NodeName
dgn_name DGNodeLab
fpiLab
          k :: Int
k = DGraph -> Int
getNewNodeDG DGraph
dg''
          nodeName :: NodeName
nodeName = (DGraph -> IRI -> Int -> NodeName
ensureUniqueNames DGraph
dg'' (String -> IRI -> IRI
addSuffixToIRI ("_verif_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
argStr) IRI
name) 1){extIndex :: Int
extIndex = 1} 
          labelK :: DGNodeLab
labelK = NodeName -> DGNodeInfo -> G_theory -> DGNodeLab
newInfoNodeLab
                    NodeName
nodeName
                    (DGOrigin -> DGNodeInfo
newNodeInfo DGOrigin
DGVerificationGeneric) (G_theory -> DGNodeLab) -> G_theory -> DGNodeLab
forall a b. (a -> b) -> a -> b
$ lid -> ExtSign sign symbol -> SigId -> G_theory
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> ExtSign sign symbol -> SigId -> G_theory
noSensGTheory lid
lid ExtSign sign symbol
tar SigId
ind
          dgK :: DGraph
dgK = LNode DGNodeLab -> DGraph -> DGraph
insNodeDG (Int
k, DGNodeLab
labelK) DGraph
dg''
          (_, dg''' :: DGraph
dg''') = LEdge DGLinkLab -> DGraph -> (LEdge DGLinkLab, DGraph)
insLEdgeDG (Int
f, Int
k, GMorphism -> DGLinkOrigin -> DGLinkLab
globDefLink GMorphism
mor DGLinkOrigin
DGLinkProof) DGraph
dgK
          {- inserts the node for fpi with sigma and
          a definition link from fpi to it -}
      GMorphism
incl <- LogicGraph -> G_sign -> G_sign -> Result GMorphism
ginclusion LogicGraph
lgraph G_sign
cmor (NodeSig -> G_sign
getSig NodeSig
tSig)
      let linkLabel :: DGLinkLab
linkLabel = GMorphism -> DGLinkType -> DGLinkOrigin -> DGLinkLab
defDGLink GMorphism
incl DGLinkType
globalThm DGLinkOrigin
DGLinkVerif
          (_, dg2 :: DGraph
dg2) = LEdge DGLinkLab -> DGraph -> (LEdge DGLinkLab, DGraph)
insLEdgeDG (Int
k, NodeSig -> Int
getNode NodeSig
tSig, DGLinkLab
linkLabel) DGraph
dg'''
           -- inserts the theorem link from fpi with sigma to p^A_i
      (Diag, DGraph) -> Result (Diag, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (Diag
diag''', DGraph
dg2)