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