{- |
Module      :  ./Proofs/ComputeColimit.hs
Description :  Heterogeneous colimit of the displayed graph
Copyright   :  (c) Mihai Codescu, and Uni Bremen 2002-2006
License     :  GPLv2 or higher, see LICENSE.txt
Maintainer  :  mcodescu@informatik.uni-bremen.de
Stability   :  provisional
Portability :  non-portable

Computes the colimit and displays the graph after its insertion.
Improvements:

 - error messages when the algorithm fails to compute
 - insert edges just from a subset of nodes in the original graph
-}

module Proofs.ComputeColimit where

import Static.ComputeTheory
import Static.DevGraph
import Static.DgUtils
import Static.GTheory
import Static.History
import Static.WACocone

import Logic.Comorphism (mkIdComorphism)
import Logic.Grothendieck
import Logic.Logic

import Common.ExtSign
import Common.LibName
import Common.Result
import Common.SFKT
import Common.Id
import Common.IRI
import Common.Utils (nubOrd)
import qualified Control.Monad.Fail as Fail

import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.Graph.Inductive.Graph

-- | computes the colimit of one development graph in a LibEnv
computeColimit :: LibName -> LibEnv -> Result LibEnv
computeColimit :: LibName -> LibEnv -> Result LibEnv
computeColimit ln :: LibName
ln le :: LibEnv
le = do
  let dgraph :: DGraph
dgraph = LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln LibEnv
le
  (_, nextDGraph :: DGraph
nextDGraph) <- LibEnv
-> LibName
-> DGraph
-> [Node]
-> [LEdge DGLinkLab]
-> NodeName
-> Result (NodeSig, DGraph)
insertColimitInGraph LibEnv
le LibName
ln DGraph
dgraph (DGraph -> [Node]
nodesDG DGraph
dgraph)
                                         (DGraph -> [LEdge DGLinkLab]
labEdgesDG DGraph
dgraph) (NodeName -> Result (NodeSig, DGraph))
-> NodeName -> Result (NodeSig, DGraph)
forall a b. (a -> b) -> a -> b
$
                                         IRI -> NodeName
makeName (IRI -> NodeName) -> IRI -> NodeName
forall a b. (a -> b) -> a -> b
$
                                         SIMPLE_ID -> IRI
simpleIdToIRI (SIMPLE_ID -> IRI) -> SIMPLE_ID -> IRI
forall a b. (a -> b) -> a -> b
$ String -> SIMPLE_ID
genToken "Colimit"
  LibEnv -> Result LibEnv
forall (m :: * -> *) a. Monad m => a -> m a
return (LibEnv -> Result LibEnv) -> LibEnv -> Result LibEnv
forall a b. (a -> b) -> a -> b
$ LibName -> DGraph -> LibEnv -> LibEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert LibName
ln DGraph
nextDGraph LibEnv
le

insertColimitInGraph :: LibEnv -> LibName -> DGraph -> [Node] -> [LEdge DGLinkLab] -> NodeName
                     -> Result (NodeSig, DGraph)
insertColimitInGraph :: LibEnv
-> LibName
-> DGraph
-> [Node]
-> [LEdge DGLinkLab]
-> NodeName
-> Result (NodeSig, DGraph)
insertColimitInGraph le :: LibEnv
le ln :: LibName
ln dgraph :: DGraph
dgraph cNodes :: [Node]
cNodes cEdges :: [LEdge DGLinkLab]
cEdges colimName :: NodeName
colimName = do
  let diag :: GDiagram
diag = DGraph -> [Node] -> [LEdge DGLinkLab] -> GDiagram
makeDiagram DGraph
dgraph [Node]
cNodes [LEdge DGLinkLab]
cEdges
  (gth :: G_theory
gth, morFun :: Map Node GMorphism
morFun) <- GDiagram -> Result (G_theory, Map Node GMorphism)
gWeaklyAmalgamableCocone GDiagram
diag
  let
      newNode :: DGNodeLab
newNode = NodeName -> DGNodeInfo -> G_theory -> DGNodeLab
newInfoNodeLab NodeName
colimName
                               (DGOrigin -> DGNodeInfo
newNodeInfo DGOrigin
DGProof) G_theory
gth
      newNodeNr :: Node
newNodeNr = DGraph -> Node
getNewNodeDG DGraph
dgraph
      edgeList :: [LEdge DGLinkLab]
edgeList = (Node -> LEdge DGLinkLab) -> [Node] -> [LEdge DGLinkLab]
forall a b. (a -> b) -> [a] -> [b]
map (\ n :: Node
n -> (Node
n, Node
newNodeNr, GMorphism -> DGLinkOrigin -> DGLinkLab
globDefLink
                      (Map Node GMorphism
morFun Map Node GMorphism -> Node -> GMorphism
forall k a. Ord k => Map k a -> k -> a
Map.! Node
n) DGLinkOrigin
SeeTarget))
                 [Node]
cNodes
      changes :: [DGChange]
changes = LNode DGNodeLab -> DGChange
InsertNode (Node
newNodeNr, DGNodeLab
newNode) DGChange -> [DGChange] -> [DGChange]
forall a. a -> [a] -> [a]
: (LEdge DGLinkLab -> DGChange) -> [LEdge DGLinkLab] -> [DGChange]
forall a b. (a -> b) -> [a] -> [b]
map LEdge DGLinkLab -> DGChange
InsertEdge [LEdge DGLinkLab]
edgeList
      newDg :: DGraph
newDg = DGraph -> [DGChange] -> DGraph
changesDGH DGraph
dgraph [DGChange]
changes
      newGraph :: DGraph
newGraph = DGraph -> DGChange -> DGraph
changeDGH DGraph
newDg (DGChange -> DGraph) -> DGChange -> DGraph
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> LNode DGNodeLab -> DGChange
SetNodeLab DGNodeLab
newNode
        (Node
newNodeNr, DGNodeLab
newNode
        { globalTheory :: Maybe G_theory
globalTheory = LibEnv -> LibName -> DGraph -> LNode DGNodeLab -> Maybe G_theory
computeLabelTheory LibEnv
le LibName
ln DGraph
newDg (Node
newNodeNr, DGNodeLab
newNode) })
      nsig :: NodeSig
nsig = Node -> G_sign -> NodeSig
NodeSig Node
newNodeNr (G_theory -> G_sign
signOf G_theory
gth)
      dg :: DGraph
dg = DGraph -> DGRule -> DGraph -> DGraph
groupHistory DGraph
dgraph (String -> DGRule
DGRule "Compute-Colimit") DGraph
newGraph
  (NodeSig, DGraph) -> Result (NodeSig, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (NodeSig
nsig, DGraph
dg)

{- | creates an GDiagram with the signatures of the given nodes as nodes
   and the morphisms of the given edges as edges -}
makeDiagram :: DGraph -> [Node] -> [LEdge DGLinkLab] -> GDiagram
makeDiagram :: DGraph -> [Node] -> [LEdge DGLinkLab] -> GDiagram
makeDiagram dg :: DGraph
dg nl :: [Node]
nl = GDiagram -> DGraph -> [Node] -> [LEdge DGLinkLab] -> GDiagram
makeDiagramAux GDiagram
forall (gr :: * -> * -> *) a b. Graph gr => gr a b
empty DGraph
dg ([Node] -> [Node]
forall a. Ord a => [a] -> [a]
nubOrd [Node]
nl)

{- | auxiliary method for makeDiagram: first translates all nodes then
   all edges, the descriptors of the nodes are kept in order to make
   retranslation easier -}
makeDiagramAux :: GDiagram -> DGraph -> [Node] -> [LEdge DGLinkLab] -> GDiagram
makeDiagramAux :: GDiagram -> DGraph -> [Node] -> [LEdge DGLinkLab] -> GDiagram
makeDiagramAux diagram :: GDiagram
diagram _ [] [] = GDiagram
diagram
makeDiagramAux diagram :: GDiagram
diagram dgraph :: DGraph
dgraph [] ((src :: Node
src, tgt :: Node
tgt, labl :: DGLinkLab
labl) : list :: [LEdge DGLinkLab]
list) =
  GDiagram -> DGraph -> [Node] -> [LEdge DGLinkLab] -> GDiagram
makeDiagramAux (LEdge (Node, GMorphism) -> GDiagram -> GDiagram
forall (gr :: * -> * -> *) b a.
DynGraph gr =>
LEdge b -> gr a b -> gr a b
insEdge LEdge (Node, GMorphism)
morphEdge GDiagram
diagram) DGraph
dgraph [] [LEdge DGLinkLab]
list
    where EdgeId x :: Node
x = DGLinkLab -> EdgeId
dgl_id DGLinkLab
labl
          morphEdge :: LEdge (Node, GMorphism)
morphEdge = if DGLinkType -> Bool
isHidingDef (DGLinkType -> Bool) -> DGLinkType -> Bool
forall a b. (a -> b) -> a -> b
$ DGLinkLab -> DGLinkType
dgl_type DGLinkLab
labl
                      then (Node
tgt, Node
src, (Node
x, DGLinkLab -> GMorphism
dgl_morphism DGLinkLab
labl))
                      else (Node
src, Node
tgt, (Node
x, DGLinkLab -> GMorphism
dgl_morphism DGLinkLab
labl))

makeDiagramAux diagram :: GDiagram
diagram dgraph :: DGraph
dgraph (node :: Node
node : list :: [Node]
list) es :: [LEdge DGLinkLab]
es =
  GDiagram -> DGraph -> [Node] -> [LEdge DGLinkLab] -> GDiagram
makeDiagramAux (LNode G_theory -> GDiagram -> GDiagram
forall (gr :: * -> * -> *) a b.
DynGraph gr =>
LNode a -> gr a b -> gr a b
insNode LNode G_theory
sigNode GDiagram
diagram) DGraph
dgraph [Node]
list [LEdge DGLinkLab]
es
    where sigNode :: LNode G_theory
sigNode = (Node
node, DGNodeLab -> G_theory
dgn_theory (DGNodeLab -> G_theory) -> DGNodeLab -> G_theory
forall a b. (a -> b) -> a -> b
$ DGraph -> Node -> DGNodeLab
labDG DGraph
dgraph Node
node)

-- | weakly amalgamable cocones
gWeaklyAmalgamableCocone :: GDiagram
                         -> Result (G_theory, Map.Map Int GMorphism)
gWeaklyAmalgamableCocone :: GDiagram -> Result (G_theory, Map Node GMorphism)
gWeaklyAmalgamableCocone diag :: GDiagram
diag
 | GDiagram -> Bool
isHomogeneousGDiagram GDiagram
diag = case [LNode G_theory] -> LNode G_theory
forall a. [a] -> a
head ([LNode G_theory] -> LNode G_theory)
-> [LNode G_theory] -> LNode G_theory
forall a b. (a -> b) -> a -> b
$ GDiagram -> [LNode G_theory]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode a]
labNodes GDiagram
diag of
   (_, G_theory lid :: lid
lid _ _ _ _ _) -> do
    Gr sign (Node, morphism)
graph <- lid -> GDiagram -> Result (Gr sign (Node, morphism))
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 -> GDiagram -> Result (Gr sign (Node, morphism))
homogeniseGDiagram lid
lid GDiagram
diag
    (sig :: sign
sig, mor :: Map Node morphism
mor) <- lid -> Gr sign (Node, morphism) -> Result (sign, Map Node morphism)
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> Gr sign (Node, morphism) -> Result (sign, Map Node morphism)
weakly_amalgamable_colimit lid
lid Gr sign (Node, morphism)
graph
    let esign :: ExtSign sign symbol
esign = (sign -> ExtSign sign Any
forall sign symbol. sign -> ExtSign sign symbol
mkExtSign sign
sig) {nonImportedSymbols :: Set symbol
nonImportedSymbols = (Set symbol -> Set symbol -> Set symbol)
-> Set symbol -> [Set symbol] -> Set symbol
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Set symbol -> Set symbol -> Set symbol
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set symbol
forall a. Set a
Set.empty ([Set symbol] -> Set symbol) -> [Set symbol] -> Set symbol
forall a b. (a -> b) -> a -> b
$ lid -> sign -> [Set symbol]
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> sign -> [Set symbol]
sym_of lid
lid sign
sig}
        gth :: G_theory
gth = 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
esign SigId
startSigId
        cid :: InclComorphism lid sublogics
cid = lid -> sublogics -> InclComorphism lid sublogics
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 -> sublogics -> InclComorphism lid sublogics
mkIdComorphism lid
lid (lid -> sublogics
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 -> sublogics
top_sublogic lid
lid)
        morFun :: Map Node GMorphism
morFun = [(Node, GMorphism)] -> Map Node GMorphism
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Node, GMorphism)] -> Map Node GMorphism)
-> [(Node, GMorphism)] -> Map Node GMorphism
forall a b. (a -> b) -> a -> b
$
         ((Node, sign) -> (Node, GMorphism))
-> [(Node, sign)] -> [(Node, GMorphism)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (n :: Node
n, s :: sign
s) -> (Node
n, InclComorphism lid sublogics
-> ExtSign sign symbol -> SigId -> morphism -> MorId -> GMorphism
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
-> ExtSign sign1 symbol1
-> SigId
-> morphism2
-> MorId
-> GMorphism
GMorphism InclComorphism lid sublogics
cid (sign -> ExtSign sign symbol
forall sign symbol. sign -> ExtSign sign symbol
mkExtSign sign
s) SigId
startSigId
                             (Map Node morphism
mor Map Node morphism -> Node -> morphism
forall k a. Ord k => Map k a -> k -> a
Map.! Node
n) MorId
startMorId)) ([(Node, sign)] -> [(Node, GMorphism)])
-> [(Node, sign)] -> [(Node, GMorphism)]
forall a b. (a -> b) -> a -> b
$
         Gr sign (Node, morphism) -> [(Node, sign)]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode a]
labNodes Gr sign (Node, morphism)
graph
    (G_theory, Map Node GMorphism)
-> Result (G_theory, Map Node GMorphism)
forall (m :: * -> *) a. Monad m => a -> m a
return (G_theory
gth, Map Node GMorphism
morFun)
 | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ GDiagram -> Bool
forall a b. Gr a b -> Bool
isConnected GDiagram
diag = String -> Result (G_theory, Map Node GMorphism)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "Graph is not connected"
 | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ GDiagram -> Bool
forall a b. Gr a b -> Bool
isThin (GDiagram -> Bool) -> GDiagram -> Bool
forall a b. (a -> b) -> a -> b
$ GDiagram -> GDiagram
forall a b. Gr a b -> Gr a b
removeIdentities GDiagram
diag = String -> Result (G_theory, Map Node GMorphism)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "Graph is not thin"
 | Bool
otherwise = do
   let funDesc :: Map Node [LNode G_theory]
funDesc = GDiagram -> Map Node [LNode G_theory]
forall a b. (Eq a, Eq b) => Gr a b -> Map Node [(Node, a)]
initDescList GDiagram
diag
   -- graph <- observe $ hetWeakAmalgCocone diag funDesc
   [GDiagram]
allGraphs <- Maybe Node -> SFKT Result GDiagram -> Result [GDiagram]
forall (m :: * -> *) a. Monad m => Maybe Node -> SFKT m a -> m [a]
runM Maybe Node
forall a. Maybe a
Nothing (SFKT Result GDiagram -> Result [GDiagram])
-> SFKT Result GDiagram -> Result [GDiagram]
forall a b. (a -> b) -> a -> b
$ GDiagram -> Map Node [LNode G_theory] -> SFKT Result GDiagram
forall (m :: * -> *) (t :: (* -> *) -> * -> *).
(MonadFail m, LogicT t, MonadPlus (t m), MonadFail (t m)) =>
GDiagram -> Map Node [LNode G_theory] -> t m GDiagram
hetWeakAmalgCocone GDiagram
diag Map Node [LNode G_theory]
funDesc
   case [GDiagram]
allGraphs of
    [] -> String -> Result (G_theory, Map Node GMorphism)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "could not compute cocone"
    _ -> do
     let graph :: GDiagram
graph = [GDiagram] -> GDiagram
forall a. [a] -> a
head [GDiagram]
allGraphs
     {- TO DO: modify this function so it would return
     all possible answers and offer them as choices to the user -}
     GDiagram -> GDiagram -> Result (G_theory, Map Node GMorphism)
buildStrMorphisms GDiagram
diag GDiagram
graph