{- |

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 Data.Map as Map

import qualified Data.Set as Set

import Data.Graph.Inductive.Graph

computeColimit :: LibName -> LibEnv -> Result LibEnv

computeColimit ln le = do

let dgraph = lookupDGraph ln le

(_, nextDGraph) <- insertColimitInGraph le ln dgraph (nodesDG dgraph)

(labEdgesDG dgraph) $

makeName $

simpleIdToIRI $ genToken "Colimit"

return $ Map.insert ln nextDGraph le

insertColimitInGraph :: LibEnv -> LibName -> DGraph -> [Node] -> [LEdge DGLinkLab] -> NodeName

-> Result (NodeSig, DGraph)

insertColimitInGraph le ln dgraph cNodes cEdges colimName = do

let diag = makeDiagram dgraph cNodes cEdges

(gth, morFun) <- gWeaklyAmalgamableCocone diag

let

newNode = newInfoNodeLab colimName

(newNodeInfo DGProof) gth

newNodeNr = getNewNodeDG dgraph

edgeList = map (\ n -> (n, newNodeNr, globDefLink

(morFun Map.! n) SeeTarget))

cNodes

changes = InsertNode (newNodeNr, newNode) : map InsertEdge edgeList

newDg = changesDGH dgraph changes

newGraph = changeDGH newDg $ SetNodeLab newNode

(newNodeNr, newNode

{ globalTheory = computeLabelTheory le ln newDg (newNodeNr, newNode) })

nsig = NodeSig newNodeNr (signOf gth)

dg = groupHistory dgraph (DGRule "Compute-Colimit") newGraph

return (nsig, 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 dg nl = makeDiagramAux empty dg (nubOrd 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 diagram _ [] [] = diagram

makeDiagramAux diagram dgraph [] ((src, tgt, labl) : list) =

makeDiagramAux (insEdge morphEdge diagram) dgraph [] list

where EdgeId x = dgl_id labl

morphEdge = if isHidingDef $ dgl_type labl

then (tgt, src, (x, dgl_morphism labl))

else (src, tgt, (x, dgl_morphism labl))

makeDiagramAux diagram dgraph (node : list) es =

makeDiagramAux (insNode sigNode diagram) dgraph list es

where sigNode = (node, dgn_theory $ labDG dgraph node)

-- | weakly amalgamable cocones

gWeaklyAmalgamableCocone :: GDiagram

-> Result (G_theory, Map.Map Int GMorphism)

gWeaklyAmalgamableCocone diag

| isHomogeneousGDiagram diag = case head $ labNodes diag of

(_, G_theory lid _ _ _ _ _) -> do

graph <- homogeniseGDiagram lid diag

(sig, mor) <- weakly_amalgamable_colimit lid graph

let esign = (mkExtSign sig) {nonImportedSymbols = foldl Set.union Set.empty $ sym_of lid sig}

gth = noSensGTheory lid esign startSigId

cid = mkIdComorphism lid (top_sublogic lid)

morFun = Map.fromList $

map (\ (n, s) -> (n, GMorphism cid (mkExtSign s) startSigId

(mor Map.! n) startMorId)) $

labNodes graph

return (gth, morFun)

| not $ isConnected diag = fail "Graph is not connected"

| not $ isThin $ removeIdentities diag = fail "Graph is not thin"

| otherwise = do

let funDesc = initDescList diag

-- graph <- observe $ hetWeakAmalgCocone diag funDesc

allGraphs <- runM Nothing $ hetWeakAmalgCocone diag funDesc

case allGraphs of

[] -> fail "could not compute cocone"

_ -> do

let graph = head allGraphs

{- TO DO: modify this function so it would return

all possible answers and offer them as choices to the user -}

buildStrMorphisms diag graph