| 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 |
| Safe Haskell | None |
Proofs.ComputeColimit
Description
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
Synopsis
- computeColimit :: LibName -> LibEnv -> Result LibEnv
- insertColimitInGraph :: LibEnv -> LibName -> DGraph -> [Node] -> [LEdge DGLinkLab] -> NodeName -> Result (NodeSig, DGraph)
- makeDiagram :: DGraph -> [Node] -> [LEdge DGLinkLab] -> GDiagram
- makeDiagramAux :: GDiagram -> DGraph -> [Node] -> [LEdge DGLinkLab] -> GDiagram
- gWeaklyAmalgamableCocone :: GDiagram -> Result (G_theory, Map Int GMorphism)
Documentation
computeColimit :: LibName -> LibEnv -> Result LibEnv Source #
computes the colimit of one development graph in a LibEnv
insertColimitInGraph :: LibEnv -> LibName -> DGraph -> [Node] -> [LEdge DGLinkLab] -> NodeName -> Result (NodeSig, DGraph) Source #
makeDiagram :: DGraph -> [Node] -> [LEdge DGLinkLab] -> GDiagram Source #
creates an GDiagram with the signatures of the given nodes as nodes and the morphisms of the given edges as edges