55cf6e01272ec475edea32aa9b7923de2d36cb42Christian Maeder{- |

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai CodescuModule : $Header$

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerDescription : heterogeneous signatures colimits approximations

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai CodescuCopyright : (c) Mihai Codescu, and Uni Bremen 2002-2006

1e09f2a31712311820bd128b55ab4792603959bbJonathan von SchroederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai CodescuMaintainer : mcodescu@informatik.uni-bremen.de

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai CodescuStability : provisional

1e09f2a31712311820bd128b55ab4792603959bbJonathan von SchroederPortability : non-portable

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu

1e09f2a31712311820bd128b55ab4792603959bbJonathan von SchroederHeterogeneous version of weakly_amalgamable_cocones.

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai CodescuNeeds some improvements (see TO DO).

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu-}

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescumodule Static.WACocone(GDiagram,

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu isHomogeneousGDiagram,

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu homogeniseGDiagram,

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu isConnected,

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu isAcyclic,

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu removeIdentities,

3dfdf17a4bbad3dde93fab8ac588d5acda8a6f42Jonathan von Schroeder hetWeakAmalgCocone,

9e30b0e74760a90c03c444cd290ba9af9d917f6eChristian Maeder initDescList,

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu buildStrMorphisms

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu ) where

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescuimport Data.Graph.Inductive.Graph as Graph

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescuimport Data.List(nub)

a6c883b6eaec47ce57e62656b09577cab13e1be7Jonathan von Schroederimport Common.Lib.Graph

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescuimport Common.Result

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescuimport Logic.Logic

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescuimport Logic.Comorphism

31d6d9286988dc31639d105841296759aeb743e0Jonathan von Schroederimport Logic.Modification

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescuimport Logic.Grothendieck

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescuimport Logic.Coerce

6164cea1d448f9e9dccd9b4c79e57763b2758ddeJonathan von Schroederimport Static.GTheory

6164cea1d448f9e9dccd9b4c79e57763b2758ddeJonathan von Schroederimport Common.ExtSign

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescuimport qualified Data.Map as Map

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescuimport qualified Data.Set as Set

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescuimport Control.Monad

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescuimport Common.LogicT

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescuimport Comorphisms.LogicGraph

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu-- | Grothendieck diagrams

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescutype GDiagram = Gr G_theory (Int, GMorphism)

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu-- | checks whether a connected GDiagram is homogeneous

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai CodescuisHomogeneousGDiagram :: GDiagram -> Bool

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai CodescuisHomogeneousGDiagram diag = foldl (&&) True $ map isHomogeneous $

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu map (\(_,_,(_,phi)) -> phi) $ labEdges diag

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu-- | homogenise a GDiagram to a targeted logic

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai CodescuhomogeniseGDiagram :: Logic lid sublogics

34626ff7551c3ceead22d049427a0b0e0d33a2e6Christian Maeder basic_spec sentence symb_items symb_map_items

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu sign morphism symbol raw_symbol proof_tree

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu => lid -- ^ the target logic to be coerced to

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu -> GDiagram -- ^ the GDiagram to be homogenised

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu -> Result (Gr sign (Int,morphism))

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai CodescuhomogeniseGDiagram targetLid diag = do

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu let convertNode (n, gth) = do

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu G_sign srcLid extSig _ <- return $ signOf gth

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu extSig' <- coerceSign srcLid targetLid "" extSig

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu return (n, plainSign extSig')

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu convertEdge (n1, n2, (nr,GMorphism cid _ _ mor _ ))

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu = if isIdComorphism (Comorphism cid) then

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu do mor' <- coerceMorphism (targetLogic cid) targetLid "" mor

34626ff7551c3ceead22d049427a0b0e0d33a2e6Christian Maeder return (n1, n2, (nr,mor'))

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu else fail $

34626ff7551c3ceead22d049427a0b0e0d33a2e6Christian Maeder "Trying to coerce a morphism between different logics.\n" ++

34626ff7551c3ceead22d049427a0b0e0d33a2e6Christian Maeder "Heterogeneous specifications are not fully supported yet."

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder convertNodes cDiag [] = do return cDiag

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu convertNodes cDiag (lNode : lNodes) =

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu do convNode <- convertNode lNode

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu let cDiag' = insNode convNode cDiag

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu convertNodes cDiag' lNodes

34626ff7551c3ceead22d049427a0b0e0d33a2e6Christian Maeder convertEdges cDiag [] = do return cDiag

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu convertEdges cDiag (lEdge : lEdges) =

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu do convEdge <- convertEdge lEdge

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu let cDiag' = insEdge convEdge cDiag

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu convertEdges cDiag' lEdges

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu dNodes = labNodes diag

3dfdf17a4bbad3dde93fab8ac588d5acda8a6f42Jonathan von Schroeder dEdges = labEdges diag

34626ff7551c3ceead22d049427a0b0e0d33a2e6Christian Maeder -- insert converted nodes to an empty diagram

34626ff7551c3ceead22d049427a0b0e0d33a2e6Christian Maeder cDiag <- convertNodes Graph.empty dNodes

34626ff7551c3ceead22d049427a0b0e0d33a2e6Christian Maeder -- insert converted edges to the diagram containing only nodes

1dfa74e3151ce63c12483d7268fe096d82e82076Jonathan von Schroeder cDiag' <- convertEdges cDiag dEdges

1dfa74e3151ce63c12483d7268fe096d82e82076Jonathan von Schroeder return cDiag'

1dfa74e3151ce63c12483d7268fe096d82e82076Jonathan von Schroeder

34626ff7551c3ceead22d049427a0b0e0d33a2e6Christian Maeder-- | checks whether a graph is connected

34626ff7551c3ceead22d049427a0b0e0d33a2e6Christian Maeder

34626ff7551c3ceead22d049427a0b0e0d33a2e6Christian MaederisConnected :: Gr a b -> Bool

34626ff7551c3ceead22d049427a0b0e0d33a2e6Christian MaederisConnected graph = let

34626ff7551c3ceead22d049427a0b0e0d33a2e6Christian Maeder nodeList = nodes graph

34626ff7551c3ceead22d049427a0b0e0d33a2e6Christian Maeder root = head nodeList

1dfa74e3151ce63c12483d7268fe096d82e82076Jonathan von Schroeder availNodes = Map.fromList $ zip nodeList (repeat True)

1dfa74e3151ce63c12483d7268fe096d82e82076Jonathan von Schroeder bfs queue avail = case queue of

3dfdf17a4bbad3dde93fab8ac588d5acda8a6f42Jonathan von Schroeder [] -> avail

3dfdf17a4bbad3dde93fab8ac588d5acda8a6f42Jonathan von Schroeder n:ns -> let

a6c883b6eaec47ce57e62656b09577cab13e1be7Jonathan von Schroeder avail1 = Map.insert n False avail

34626ff7551c3ceead22d049427a0b0e0d33a2e6Christian Maeder nbs = filter ((Map.!) avail) $ neighbors graph n

a6c883b6eaec47ce57e62656b09577cab13e1be7Jonathan von Schroeder in bfs (ns++nbs) avail1

69fd87e4b078ee518487bbfa5f4589392a132993Jonathan von Schroeder in filter ((Map.!) (bfs [root] availNodes)) nodeList == []

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

69fd87e4b078ee518487bbfa5f4589392a132993Jonathan von Schroeder-- | checks whether a graph is acyclic

6164cea1d448f9e9dccd9b4c79e57763b2758ddeJonathan von Schroeder

a6c883b6eaec47ce57e62656b09577cab13e1be7Jonathan von SchroederisAcyclic :: (Eq b) => Gr a b -> Bool

34626ff7551c3ceead22d049427a0b0e0d33a2e6Christian MaederisAcyclic graph = let

1dfa74e3151ce63c12483d7268fe096d82e82076Jonathan von Schroeder filterIns gr = filter (\ x -> indeg gr x == 0)

6164cea1d448f9e9dccd9b4c79e57763b2758ddeJonathan von Schroeder queue = filterIns graph $ nodes graph

6164cea1d448f9e9dccd9b4c79e57763b2758ddeJonathan von Schroeder topologicalSort q gr = case q of

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder [] -> null $ edges gr

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder n : ns -> let

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder oEdges = lsuc gr n

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder graph1 = foldl (flip Graph.delLEdge) gr

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder $ map (\ (y, label) -> (n, y, label)) oEdges

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder succs = filterIns graph1 $ suc gr n

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder in topologicalSort (ns ++ succs) graph1

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder in topologicalSort queue graph

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder-- | auxiliary for removing the identity edges from a graph

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von SchroederremoveIdentities :: Gr a b -> Gr a b

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von SchroederremoveIdentities graph = let

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder addEdges gr eList = case eList of

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder [] -> gr

3f232df590a3fafc60a218589c3a3f0a3c359b44Jonathan von Schroeder (sn, tn, label):eList1 -> if sn == tn then addEdges gr eList1

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder else addEdges (insEdge (sn, tn, label) gr) eList1

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder in (addEdges $ insNodes (labNodes graph) Graph.empty)

3f232df590a3fafc60a218589c3a3f0a3c359b44Jonathan von Schroeder $ labEdges graph

3f232df590a3fafc60a218589c3a3f0a3c359b44Jonathan von Schroeder

ae20fe3ef7832827a9ee018899f30eeae98a706dJonathan von Schroeder-- assigns to a node all proper descendants

34626ff7551c3ceead22d049427a0b0e0d33a2e6Christian MaederinitDescList :: Gr a b -> Map.Map Node [(Node, a)]

3f232df590a3fafc60a218589c3a3f0a3c359b44Jonathan von SchroederinitDescList graph = let

3f232df590a3fafc60a218589c3a3f0a3c359b44Jonathan von Schroeder isProperDescOf gr n x = let

3f232df590a3fafc60a218589c3a3f0a3c359b44Jonathan von Schroeder existsPath diag snode nlist = if snode `elem` nlist then True

3f232df590a3fafc60a218589c3a3f0a3c359b44Jonathan von Schroeder else let

3f232df590a3fafc60a218589c3a3f0a3c359b44Jonathan von Schroeder nlist1 = foldl (++) [] $ map (pre diag) nlist

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder in if nlist1 == [] then False

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder else existsPath diag snode nlist1

3f232df590a3fafc60a218589c3a3f0a3c359b44Jonathan von Schroeder in if n == x then False

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder else existsPath gr x [n]

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder descsOf n = filter (\(x,_) -> isProperDescOf graph n x)$ labNodes graph

3f232df590a3fafc60a218589c3a3f0a3c359b44Jonathan von Schroeder in Map.fromList$ map (\node -> (node, descsOf node)) $ nodes graph

34626ff7551c3ceead22d049427a0b0e0d33a2e6Christian Maeder

3f232df590a3fafc60a218589c3a3f0a3c359b44Jonathan von SchroedercommonBounds :: (Eq a) => Map.Map Node [(Node, a)] -> Node -> Node -> [(Node,a)]

87836973cf6a4ed22295454c58242fc926a83f42Jonathan von SchroedercommonBounds funDesc n1 n2 = filter

3f232df590a3fafc60a218589c3a3f0a3c359b44Jonathan von Schroeder (\x -> x `elem` ((Map.!) funDesc n1) && x `elem` ((Map.!) funDesc n2) )

87836973cf6a4ed22295454c58242fc926a83f42Jonathan von Schroeder $ nub $ (Map.!) funDesc n1 ++ (Map.!) funDesc n2

ae20fe3ef7832827a9ee018899f30eeae98a706dJonathan von Schroeder

3f232df590a3fafc60a218589c3a3f0a3c359b44Jonathan von Schroeder-- returns the greatest lower bound of two maximal nodes,if it exists

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroederglb :: (Eq a) => Map.Map Node [(Node, a)] -> Node -> Node -> Maybe (Node,a)

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroederglb funDesc n1 n2 = let

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder cDescs = commonBounds funDesc n1 n2

1dfa74e3151ce63c12483d7268fe096d82e82076Jonathan von Schroeder subList [] _ = True

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder subList (x:xs) l2 = x `elem` l2 && subList xs l2

1dfa74e3151ce63c12483d7268fe096d82e82076Jonathan von Schroeder glbList = filter (\(n, x) -> subList

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder (filter (\(n0,x0) -> (n,x)/= (n0,x0)) cDescs) (funDesc Map.! n)

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder ) cDescs

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder -- a node n is glb of n1 and n2 iff

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder -- all common bounds of n1 and n2 are also descendants of n

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder in case glbList of

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder [] -> Nothing

1dfa74e3151ce63c12483d7268fe096d82e82076Jonathan von Schroeder x:_ -> Just x -- because if it exists, there can be only one

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder-- if no greatest lower bound exists, compute all maximal bounds of the nodes

1dfa74e3151ce63c12483d7268fe096d82e82076Jonathan von SchroedermaxBounds :: (Eq a) => Map.Map Node [(Node, a)] -> Node -> Node -> [(Node, a)]

1dfa74e3151ce63c12483d7268fe096d82e82076Jonathan von SchroedermaxBounds funDesc n1 n2 = let

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder cDescs = commonBounds funDesc n1 n2

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder isDesc n0 (n,y) = (n,y) `elem` funDesc Map.! n0

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder noDescs (n,y) = filter (\(n0, _) -> isDesc n0 (n,y)) cDescs == []

ab148c20add4ca4c956e36f56859dcc5c4dde187Jonathan von Schroeder in filter noDescs cDescs

ab148c20add4ca4c956e36f56859dcc5c4dde187Jonathan von Schroeder

ab148c20add4ca4c956e36f56859dcc5c4dde187Jonathan von Schroeder-- dijsktra algorithm for finding the the shortest path between two nodes

ab148c20add4ca4c956e36f56859dcc5c4dde187Jonathan von Schroederdijkstra :: GDiagram -> Node -> Node -> Result GMorphism

ab148c20add4ca4c956e36f56859dcc5c4dde187Jonathan von Schroederdijkstra graph source target = let

ab148c20add4ca4c956e36f56859dcc5c4dde187Jonathan von Schroeder dist = Map.insert source 0 $ Map.fromList $

34626ff7551c3ceead22d049427a0b0e0d33a2e6Christian Maeder zip (nodes graph) $ repeat $ 2 * (length $ edges graph)

ab148c20add4ca4c956e36f56859dcc5c4dde187Jonathan von Schroeder prev = Map.empty

ab148c20add4ca4c956e36f56859dcc5c4dde187Jonathan von Schroeder q = nodes graph

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder com = case lab graph source of

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder Nothing -> Map.empty --shouldnt be the case

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Just gt -> Map.insert source (ide $ signOf gt) Map.empty

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (nodeList, com1) = mainloop graph source target q dist prev com

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder extractMin queue dMap = let

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder u = head $

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder filter (\x -> (Map.!) dMap x == (minimum $ map ((Map.!)dMap) queue)) queue

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder in ( Set.toList $ Set.difference (Set.fromList queue) (Set.fromList [u]) , u)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder updateNeighbors d p c u gr = let

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder outEdges = out gr u

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder upNeighbor dMap pMap cMap uNode edgeList = case edgeList of

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder [] -> (dMap, pMap, cMap)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (_, v, (_, gmor)):edgeL -> let

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder alt = (Map.!) dMap uNode + 1

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder in if (alt >= (Map.!) dMap v) then upNeighbor dMap pMap cMap uNode edgeL

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder else let

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder d1 = Map.insert v alt dMap

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder p1 = Map.insert v uNode pMap

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder c1 = Map.insert v gmor cMap

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder in upNeighbor d1 p1 c1 uNode edgeL

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder in upNeighbor d p c u outEdges

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder -- for each neighbor of u, if d(u)+1 < d(v), modify p(v) = u, d(v) = d(u)+1

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder mainloop gr sn tn qL d p c = let

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (q1, u) = extractMin qL d

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (d1, p1, c1) = updateNeighbors d p c u gr

ab148c20add4ca4c956e36f56859dcc5c4dde187Jonathan von Schroeder in if (u == tn) then shortPath gr sn p1 c [] tn

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder else mainloop gr sn tn q1 d1 p1 c1

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder shortPath gr sn p1 c s u = if (Map.!) p1 u == sn then (u:s, c)

87836973cf6a4ed22295454c58242fc926a83f42Jonathan von Schroeder else shortPath gr sn p1 c (u:s) $(Map.!) p1 u

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder in foldM comp ((Map.!) com1 source) $ map ((Map.!)com1) nodeList

ab148c20add4ca4c956e36f56859dcc5c4dde187Jonathan von Schroeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- builds the arrows from the nodes of the original graph

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- to the unique maximal node of the obtained graph

87836973cf6a4ed22295454c58242fc926a83f42Jonathan von Schroeder-- TO DO:different cases if the new graph is the same as the old one

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder-- (i.e. a graph with a single maximal node)?

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder

ab148c20add4ca4c956e36f56859dcc5c4dde187Jonathan von SchroederbuildStrMorphisms :: GDiagram -> GDiagram

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder ->Result (G_theory, Map.Map Node GMorphism)

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von SchroederbuildStrMorphisms initGraph newGraph = do

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu let (maxNode, sigma) = head $ filter (\(node,_) -> outdeg newGraph node == 0) $

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu labNodes newGraph

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu buildMor pairList solList = do

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu case pairList of

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu (n, _):pairs -> do nMor <- dijkstra newGraph n maxNode

34626ff7551c3ceead22d049427a0b0e0d33a2e6Christian Maeder buildMor pairs (solList ++ [(n,nMor)])

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu [] -> return solList

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu morList <- buildMor (labNodes initGraph) []

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu return $ (sigma, Map.fromList morList)

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu

ae20fe3ef7832827a9ee018899f30eeae98a706dJonathan von Schroeder-- computes the colimit and inserts it into the graph

9e30b0e74760a90c03c444cd290ba9af9d917f6eChristian MaederaddNodeToGraph :: GDiagram -> G_theory -> G_theory -> G_theory -> Int -> Int

9e30b0e74760a90c03c444cd290ba9af9d917f6eChristian Maeder -> Int -> GMorphism -> GMorphism

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu -> Map.Map Node [(Node, G_theory)] -> [(Int, G_theory)]

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder -> Result (GDiagram, Map.Map Node [(Node, G_theory)])

6f3b0aa6cccf5105b22a1ae366ff59706538d937Jonathan von SchroederaddNodeToGraph oldGraph

6f3b0aa6cccf5105b22a1ae366ff59706538d937Jonathan von Schroeder (G_theory lid extSign _ _ _)

6f3b0aa6cccf5105b22a1ae366ff59706538d937Jonathan von Schroeder gt1@(G_theory lid1 extSign1 idx1 _ _)

6f3b0aa6cccf5105b22a1ae366ff59706538d937Jonathan von Schroeder gt2@(G_theory lid2 extSign2 idx2 _ _)

6f3b0aa6cccf5105b22a1ae366ff59706538d937Jonathan von Schroeder n

6f3b0aa6cccf5105b22a1ae366ff59706538d937Jonathan von Schroeder n1

6164cea1d448f9e9dccd9b4c79e57763b2758ddeJonathan von Schroeder n2

34626ff7551c3ceead22d049427a0b0e0d33a2e6Christian Maeder (GMorphism cid1 _ _ mor1 _)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (GMorphism cid2 _ _ mor2 _)

abbba0121ac69d254389160a7b92c52dc279b960Mihai Codescu funDesc maxNodes = do

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu let newNode = 1 + (maximum $ nodes oldGraph) --get a new node

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder s1 <- coerceSign lid1 lid "addToNodeGraph" extSign1

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder s2 <- coerceSign lid2 lid "addToNodeGraph" extSign2

9e30b0e74760a90c03c444cd290ba9af9d917f6eChristian Maeder m1 <- coerceMorphism (targetLogic cid1) lid "addToNodeGraph" mor1

9e30b0e74760a90c03c444cd290ba9af9d917f6eChristian Maeder m2 <- coerceMorphism (targetLogic cid2) lid "addToNodeGraph" mor2

9e30b0e74760a90c03c444cd290ba9af9d917f6eChristian Maeder let spanGr = Graph.mkGraph

3dfdf17a4bbad3dde93fab8ac588d5acda8a6f42Jonathan von Schroeder [(n, plainSign extSign), (n1, plainSign s1), (n2, plainSign s2)]

9e30b0e74760a90c03c444cd290ba9af9d917f6eChristian Maeder [(n, n1, (1, m1)), (n, n2, (1, m2))]

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu (s, morMap) <- weakly_amalgamable_colimit lid spanGr

b93d7514eff107392e0ee8d7b659320fed06d64cJonathan von Schroeder let gtheory = noSensGTheory lid (mkExtSign s) startSigId

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder -- must coerce here

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder m11 <- coerceMorphism lid (targetLogic cid1) "addToNodeGraph" $

b93d7514eff107392e0ee8d7b659320fed06d64cJonathan von Schroeder morMap Map.! n1

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder m22 <- coerceMorphism lid (targetLogic cid2) "addToNodeGraph" $

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder morMap Map.! n2

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder s11 <- coerceSign lid (sourceLogic cid1) "addToNodeGraph" s1

34626ff7551c3ceead22d049427a0b0e0d33a2e6Christian Maeder s22 <- coerceSign lid (sourceLogic cid2) "addToNodeGraph" s2

34626ff7551c3ceead22d049427a0b0e0d33a2e6Christian Maeder let gmor1 = GMorphism cid1 s11 idx1 m11 startMorId

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu let gmor2 = GMorphism cid2 s22 idx2 m22 startMorId

0fa7a99c279b7b59df56d86c3ada137b191fe8ebJonathan von Schroeder case maxNodes of

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu [] -> do

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu let newGraph = insEdges [(n1, newNode,(1, gmor1)),(n2, newNode,(1,gmor2))] $

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu insNode (newNode, gtheory) oldGraph

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu funDesc1 = Map.insert newNode

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu (nub $ (Map.!)funDesc n1 ++ (Map.!) funDesc n2 ) funDesc

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu return (newGraph, funDesc1)

34626ff7551c3ceead22d049427a0b0e0d33a2e6Christian Maeder _ -> computeCoeqs oldGraph funDesc (n1, gt1) (n2, gt2)

(newNode, gtheory) gmor1 gmor2 maxNodes

-- for each node in the list, check whether the coequalizer can be computed

-- if so, modify the maximal node of graph and the edges to it from n1 and n2

computeCoeqs :: GDiagram -> Map.Map Node [(Node, G_theory)]

-> (Node,G_theory) -> (Node,G_theory) -> (Node, G_theory)

-> GMorphism -> GMorphism -> [(Node, G_theory)]->

Result (GDiagram, Map.Map Node [(Node, G_theory)])

computeCoeqs oldGraph funDesc (n1,_) (n2,_) (newN, newGt) gmor1 gmor2 [] = do

let newGraph = insEdges [(n1, newN, (1, gmor1)),(n2, newN, (1, gmor2))] $

insNode (newN, newGt) oldGraph

descFun1 = Map.insert newN

(nub $ (Map.!)funDesc n1 ++ (Map.!) funDesc n2 ) funDesc

return $ (newGraph, descFun1)

computeCoeqs graph funDesc (n1,gt1) (n2,gt2)

(newN, _newGt@(G_theory tlid tsign _ _ _))

_gmor1@(GMorphism cid1 sig1 idx1 mor1 _ )

_gmor2@(GMorphism cid2 sig2 idx2 mor2 _ ) ((n,gt):descs)= do

_rho1@(GMorphism cid3 _ _ mor3 _)<- dijkstra graph n n1

_rho2@(GMorphism cid4 _ _ mor4 _)<- dijkstra graph n n2

com1 <- compComorphism (Comorphism cid1) (Comorphism cid3)

com2 <- compComorphism (Comorphism cid1) (Comorphism cid3)

if com1 /= com2 then fail "Unable to compute coequalizer" else do

_gtM@(G_theory lidM signM _idxM _ _)<- mapG_theory com1 gt

s1 <- coerceSign lidM tlid "coequalizers" signM

mor3' <- coerceMorphism (targetLogic cid3) (sourceLogic cid1) "coeqs" mor3

mor4' <- coerceMorphism (targetLogic cid4) (sourceLogic cid2) "coeqs" mor4

m1 <- map_morphism cid1 mor3'

m2 <- map_morphism cid2 mor4'

phi1' <- comp m1 mor1

phi2' <- comp m2 mor2

phi1 <- coerceMorphism (targetLogic cid1) tlid "coeqs" phi1'

phi2 <- coerceMorphism (targetLogic cid2) tlid "coeqs" phi2'

-- build the double arrow for computing the coequalizers

let doubleArrow = Graph.mkGraph

[(n, plainSign s1), (newN, plainSign tsign)]

[(n, newN, (1, phi1)), (n, newN, (1, phi2))]

(colS, colM) <- weakly_amalgamable_colimit tlid doubleArrow

let newGt1 = noSensGTheory tlid (mkExtSign colS) startSigId

mor11' <- coerceMorphism tlid (targetLogic cid1) "coeqs" $ (Map.!) colM newN

mor11 <- comp mor1 mor11'

mor22' <- coerceMorphism tlid (targetLogic cid2) "coeqs" $ (Map.!) colM newN

mor22 <- comp mor2 mor22'

let gMor11 = GMorphism cid1 sig1 idx1 mor11 startMorId

let gMor22 = GMorphism cid2 sig2 idx2 mor22 startMorId

computeCoeqs graph funDesc (n1, gt1) (n2,gt2) (newN, newGt1)

gMor11 gMor22 descs

-- returns a maximal node available

pickMaxNode :: (MonadPlus t) => Gr a b -> t (Node,a)

pickMaxNode graph = msum $ map return $

filter (\(node,_) -> outdeg graph node == 0) $

labNodes graph

-- returns a list of common descendants of two maximal nodes:

-- one node if a glb exists, or all maximal descendants otherwise

commonDesc :: Map.Map Node [(Node,G_theory)] -> Node -> Node

-> [(Node, G_theory)]

commonDesc funDesc n1 n2 = case glb funDesc n1 n2 of

Just x -> [x]

Nothing -> maxBounds funDesc n1 n2

-- returns a weakly amalgamable square of lax triangles

pickSquare :: (MonadPlus t) => Result GMorphism -> Result GMorphism -> t Square

pickSquare (Result _ (Just phi1@(GMorphism cid1 _ _ _ _)))

(Result _ (Just phi2@(GMorphism cid2 _ _ _ _))) =

if (isHomogeneous phi1 && isHomogeneous phi2) then

return $ mkIdSquare $ Logic $ sourceLogic cid1

--since they have the same target, both homogeneous implies same logic

else

case maybeResult $ lookupSquare_in_LG (Comorphism cid1)(Comorphism cid2) of

Nothing -> mzero

Just sqList -> msum $ map return sqList

pickSquare (Result _ Nothing) _ = fail "Error computing comorphisms"

pickSquare _ (Result _ Nothing) = fail "Error computing comorphisms"

-- builds the span for which the colimit is computed

buildSpan :: GDiagram ->

Map.Map Node [(Node, G_theory)] ->

AnyComorphism ->

AnyComorphism ->

AnyComorphism ->

AnyComorphism ->

AnyComorphism ->

AnyModification ->

AnyModification ->

G_theory ->

G_theory ->

G_theory ->

GMorphism ->

GMorphism ->

Int -> Int -> Int ->

[(Int, G_theory)]->

Result (GDiagram, Map.Map Node [(Node,G_theory)])

buildSpan graph

funDesc

d@(Comorphism _cidD)

e1@(Comorphism cidE1)

e2@(Comorphism cidE2)

_d1@(Comorphism _cidD1)

_d2@(Comorphism _cidD2)

_m1@(Modification cidM1)

_m2@(Modification cidM2)

gt@(G_theory lid sign _ _ _)

gt1@(G_theory _lid1 _sign1 _ _ _)

gt2@(G_theory _lid2 _sign2 _ _ _)

_phi1@(GMorphism cid1 _ _ mor1 _)

_phi2@(GMorphism cid2 _ _ mor2 _)

n n1 n2

maxNodes

= do

sig@(G_theory lid0 sign0 _ _ _) <- mapG_theory d gt -- phi^d(Sigma)

sig1 <- mapG_theory e1 gt1 -- phi^e1(Sigma1)

sig2 <- mapG_theory e2 gt2 -- phi^e2(Sigma2)

mor1' <- coerceMorphism (targetLogic cid1) (sourceLogic cidE1) "buildSpan" mor1

eps1 <- map_morphism cidE1 mor1' -- phi^e1(sigma1)

sign' <- coerceSign lid (sourceLogic$ sourceComorphism cidM1) "buildSpan" sign

tau1 <- tauSigma cidM1 (plainSign sign') -- I^u1_Sigma

tau1' <- coerceMorphism (targetLogic$ sourceComorphism cidM1)

(targetLogic cidE1) "buildSpan" tau1

rho1 <- comp tau1' eps1

mor2' <- coerceMorphism (targetLogic cid2) (sourceLogic cidE2) "buildSpan" mor2

eps2 <- map_morphism cidE2 mor2' --phi^e2(sigma2)

sign'' <- coerceSign lid (sourceLogic$ sourceComorphism cidM2) "buildSpan" sign

tau2 <- tauSigma cidM2 (plainSign sign'') -- I^u2_Sigma

tau2' <- coerceMorphism (targetLogic$ sourceComorphism cidM2)

(targetLogic cidE2) "buildSpan" tau2

rho2 <- comp tau2' eps2

signE1 <- coerceSign lid0 (sourceLogic cidE1) " " sign0

signE2 <- coerceSign lid0 (sourceLogic cidE2) " " sign0

(graph1, funDesc1) <- addNodeToGraph graph sig sig1 sig2 n n1 n2

(GMorphism cidE1 signE1 startSigId rho1 startMorId)

(GMorphism cidE2 signE2 startSigId rho2 startMorId) funDesc maxNodes

return (graph1, funDesc1)

pickMaximalDesc :: (MonadPlus t) => [(Node, G_theory)] -> t (Node, G_theory)

pickMaximalDesc descList = msum$ map return descList

nrMaxNodes :: Gr a b -> Int

nrMaxNodes graph = length $ filter (\n -> outdeg graph n == 0) $ nodes graph

-- | backtracking function for heterogeneous weak amalgamable cocones

hetWeakAmalgCocone :: (Monad m, LogicT t, MonadPlus (t m)) =>

GDiagram -> Map.Map Int [(Int, G_theory)] -> t m GDiagram

hetWeakAmalgCocone graph funDesc =

if nrMaxNodes graph == 1 then return graph

else once $ do

(n1,gt1) <- pickMaxNode graph

(n2,gt2) <- pickMaxNode graph

guard (n1 < n2) -- to consider each pair of maximal nodes only once

let descList = commonDesc funDesc n1 n2

case length descList of

0 -> mzero -- no common descendants for n1 and n2

_ -> do -- just one common descendant implies greatest lower bound

-- for several, the tail is not empty and we compute coequalizers

(n,gt) <- pickMaximalDesc descList

let phi1 = dijkstra graph n n1

phi2 = dijkstra graph n n2

square <- pickSquare phi1 phi2

let d = laxTarget $ leftTriangle square

e1 = laxFst $ leftTriangle square

d1 = laxSnd $ leftTriangle square

e2 = laxFst $ rightTriangle square

d2 = laxSnd $ rightTriangle square

m1 = laxModif $ leftTriangle square

m2 = laxModif $ rightTriangle square

case maybeResult phi1 of

Nothing -> mzero

Just phi1' -> case maybeResult phi2 of

Nothing -> mzero

Just phi2' -> do

let mGraph = buildSpan graph funDesc d e1 e2 d1 d2 m1 m2 gt gt1 gt2

phi1' phi2' n n1 n2 $ filter (\(nx,_) -> nx /=n) descList

case maybeResult mGraph of

Nothing -> mzero

Just (graph1, funDesc1) -> hetWeakAmalgCocone graph1 funDesc1