95242ab07e9aa13b37c16cac36a75d190e1766e4Heng JiangDescription : heterogeneous signatures colimits approximations
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng JiangCopyright : (c) Mihai Codescu, and Uni Bremen 2002-2006
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng JiangLicense : GPLv2 or higher, see LICENSE.txt
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng JiangMaintainer : mcodescu@informatik.uni-bremen.de
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng JiangStability : provisional
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng JiangPortability : non-portable
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng JiangHeterogeneous version of weakly_amalgamable_cocones.
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng JiangNeeds some improvements (see TO DO).
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiangmodule Static.WACocone (isConnected,
67d5e49547d78aa56a8f9ba5e64a950b730eba66Till Mossakowski removeIdentities,
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang hetWeakAmalgCocone,
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang initDescList,
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang buildStrMorphisms,
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang weakly_amalgamable_colimit
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiangimport qualified Data.Map as Map
806bce66335c88260a63e7524b1efc68d8dfacc1Heng Jiangimport qualified Data.Set as Set
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiangweakly_amalgamable_colimit :: StaticAnalysis lid
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang basic_spec sentence symb_items symb_map_items
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang sign morphism symbol raw_symbol
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang => lid -> Tree.Gr sign (Int, morphism)
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang -> Result (sign, Map.Map Int morphism)
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiangweakly_amalgamable_colimit l diag = do
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang (sig, sink) <- signature_colimit l diag
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang return (sig, sink)
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang{- until amalgamability check is fixed, just return a colimit
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiangget (commented out) code from rev:11881 -}
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang-- | checks whether a graph is connected
806bce66335c88260a63e7524b1efc68d8dfacc1Heng JiangisConnected :: Gr a b -> Bool
806bce66335c88260a63e7524b1efc68d8dfacc1Heng JiangisConnected graph = let
806bce66335c88260a63e7524b1efc68d8dfacc1Heng Jiang nodeList = nodes graph
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang root = head nodeList
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang availNodes = Map.fromList $ zip nodeList (repeat True)
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang bfs queue avail = case queue of
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang n : ns -> let
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang avail1 = Map.insert n False avail
806bce66335c88260a63e7524b1efc68d8dfacc1Heng Jiang nbs = filter (\ x -> Map.findWithDefault (error "isconnected") x avail)
806bce66335c88260a63e7524b1efc68d8dfacc1Heng Jiang $ neighbors graph n
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang in bfs (ns ++ nbs) avail1
806bce66335c88260a63e7524b1efc68d8dfacc1Heng Jiang in not $ any (\ x -> Map.findWithDefault (error "iscon 2") x
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang (bfs [root] availNodes)) nodeList
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang-- | checks whether the graph is thin
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng JiangisThin :: Gr a b -> Bool
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng JiangisThin = checkThinness Map.empty . edges
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng JiangcheckThinness :: Map.Map Edge Int -> [Edge] -> Bool
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng JiangcheckThinness paths eList =
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang case eList of
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang (sn, tn) : eList' ->
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang (sn, tn) `notElem` Map.keys paths &&
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang -- multiple paths between (sn, tn)
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang let pathsToS = filter (\ (_, y) -> y == sn) $ Map.keys paths
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang updatePaths pathF dest pList =
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang case pList of
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang [] -> Just pathF
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang (x, _) : pList' ->
0b31ea5ec0e20f17d55845a5d803c48466e01ca3Heng Jiang if (x, dest) `elem` Map.keys pathF then Nothing
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang else updatePaths (Map.insert (x, dest) 1 pathF) dest pList'
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang in case updatePaths paths tn pathsToS of
f0a4ace924cef940ca4cc646fa180df70ef405d8Klaus Luettich Nothing -> False
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang Just paths' -> checkThinness (Map.insert (sn, tn) 1 paths') eList'
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang-- | checks whether a graph is acyclic
0b31ea5ec0e20f17d55845a5d803c48466e01ca3Heng JiangisAcyclic :: (Eq b) => Gr a b -> Bool
0b31ea5ec0e20f17d55845a5d803c48466e01ca3Heng JiangisAcyclic graph = let
0b31ea5ec0e20f17d55845a5d803c48466e01ca3Heng Jiang filterIns gr = filter (\ x -> indeg gr x == 0)
0b31ea5ec0e20f17d55845a5d803c48466e01ca3Heng Jiang queue = filterIns graph $ nodes graph
0b31ea5ec0e20f17d55845a5d803c48466e01ca3Heng Jiang topologicalSort q gr = case q of
0b31ea5ec0e20f17d55845a5d803c48466e01ca3Heng Jiang [] -> null $ edges gr
0b31ea5ec0e20f17d55845a5d803c48466e01ca3Heng Jiang n : ns -> let
0b31ea5ec0e20f17d55845a5d803c48466e01ca3Heng Jiang oEdges = lsuc gr n
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang graph1 = foldl (flip Graph.delLEdge) gr
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang $ map (\ (y, label) -> (n, y, label)) oEdges
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang succs = filterIns graph1 $ suc gr n
31ac08a9e5233b83a63fd5aaac494c32305c4c77Heng Jiang in topologicalSort (ns ++ succs) graph1
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang in topologicalSort queue graph
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang-- | auxiliary for removing the identity edges from a graph
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng JiangremoveIdentities :: Gr a b -> Gr a b
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng JiangremoveIdentities graph = let
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang addEdges gr eList = case eList of
0b31ea5ec0e20f17d55845a5d803c48466e01ca3Heng Jiang (sn, tn, label) : eList1 -> if sn == tn then addEdges gr eList1
0b31ea5ec0e20f17d55845a5d803c48466e01ca3Heng Jiang else addEdges (insEdge (sn, tn, label) gr) eList1
0b31ea5ec0e20f17d55845a5d803c48466e01ca3Heng Jiang in addEdges (insNodes (labNodes graph) Graph.empty) $ labEdges graph
0b31ea5ec0e20f17d55845a5d803c48466e01ca3Heng Jiang-- assigns to a node all proper descendents
0b31ea5ec0e20f17d55845a5d803c48466e01ca3Heng JianginitDescList :: (Eq a, Eq b) => Gr a b -> Map.Map Node [(Node, a)]
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng JianginitDescList graph = let
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang descsOf n = let
0b31ea5ec0e20f17d55845a5d803c48466e01ca3Heng Jiang nodeList = filter (n /=) $ pre graph n
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang f = Map.fromList $ zip nodeList (repeat False)
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang precs nList nList' avail =
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang case nList of
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang [] -> nList'
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang nList'' = concatMap (\ y -> filter
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang (\ x -> x `notElem` Map.keys avail ||
0b31ea5ec0e20f17d55845a5d803c48466e01ca3Heng Jiang Map.findWithDefault (error "iDL") x avail) $
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang filter (y /=) $ pre graph y) nList
31ac08a9e5233b83a63fd5aaac494c32305c4c77Heng Jiang avail' = Map.union avail $
31ac08a9e5233b83a63fd5aaac494c32305c4c77Heng Jiang Map.fromList $ zip nList'' (repeat False)
806bce66335c88260a63e7524b1efc68d8dfacc1Heng Jiang in precs (nub nList'') (nub $ nList' ++ nList'') avail'
806bce66335c88260a63e7524b1efc68d8dfacc1Heng Jiang in precs nodeList nodeList f
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang in Map.fromList $ map (\ node -> (node, filter (\ x -> fst x `elem`
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang descsOf node)
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang $ labNodes graph )) $ nodes graph
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng JiangcommonBounds :: (Eq a) => Map.Map Node [(Node, a)] -> Node -> Node -> [(Node, a)]
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng JiangcommonBounds funDesc n1 n2 = filter
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang (\ x -> x `elem` (Map.!) funDesc n1 && x `elem` (Map.!) funDesc n2 )
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang $ nub $ (Map.!) funDesc n1 ++ (Map.!) funDesc n2
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang-- returns the greatest lower bound of two maximal nodes,if it exists
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiangglb :: (Eq a) => Map.Map Node [(Node, a)] -> Node -> Node -> Maybe (Node, a)
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiangglb funDesc n1 n2 = let
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang cDescs = commonBounds funDesc n1 n2
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang subList [] _ = True
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang subList (x : xs) l2 = x `elem` l2 && subList xs l2
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang glbList = filter (\ (n, x) -> subList
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang (filter (\ (n0, x0) -> (n, x) /= (n0, x0)) cDescs) (funDesc Map.! n)
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang {- a node n is glb of n1 and n2 iff
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang all common bounds of n1 and n2 are also descendants of n -}
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang in case glbList of
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang [] -> Nothing
806bce66335c88260a63e7524b1efc68d8dfacc1Heng Jiang x : _ -> Just x -- because if it exists, there can be only one
806bce66335c88260a63e7524b1efc68d8dfacc1Heng Jiang-- if no greatest lower bound exists, compute all maximal bounds of the nodes
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng JiangmaxBounds :: (Eq a) => Map.Map Node [(Node, a)] -> Node -> Node -> [(Node, a)]
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng JiangmaxBounds funDesc n1 n2 = let
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang cDescs = commonBounds funDesc n1 n2
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang isDesc n0 (n, y) = (n, y) `elem` funDesc Map.! n0
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang noDescs (n, y) = not $ any (\ (n0, _) -> isDesc n0 (n, y)) cDescs
f0a4ace924cef940ca4cc646fa180df70ef405d8Klaus Luettich in filter noDescs cDescs
f0a4ace924cef940ca4cc646fa180df70ef405d8Klaus Luettich-- dijsktra algorithm for finding the the shortest path between two nodes
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiangdijkstra :: GDiagram -> Node -> Node -> Result GMorphism
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiangdijkstra graph source target = do
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang zip (nodes graph) $ repeat $ 2 * length (edges graph)
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang prev = if source == target then Map.insert source source Map.empty
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang q = nodes graph
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang com = case lab graph source of
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang Nothing -> Map.empty -- shouldnt be the case
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang Just gt -> Map.insert source (ide $ signOf gt) Map.empty
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang extractMin queue dMap = let
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang filter (\ x -> Map.findWithDefault (error "dijkstra") x dMap ==
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang (map (\ x1 -> Map.findWithDefault (error "dijkstra") x1 dMap)
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang in ( Set.toList $ Set.difference (Set.fromList queue) (Set.fromList [u]) , u)
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang updateNeighbors d p c u gr = let
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang outEdges = out gr u
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang upNeighbor dMap pMap cMap uNode edgeList = case edgeList of
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang [] -> (dMap, pMap, cMap)
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang (_, v, (_, gmor)) : edgeL -> let
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang alt = Map.findWithDefault (error "dijkstra") uNode dMap + 1
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang if alt >= Map.findWithDefault (error "dijsktra") v dMap then
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang upNeighbor dMap pMap cMap uNode edgeL
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang d1 = Map.insert v alt dMap
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang p1 = Map.insert v uNode pMap
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang c1 = Map.insert v gmor cMap
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang in upNeighbor d1 p1 c1 uNode edgeL
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang in upNeighbor d p c u outEdges
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang -- for each neighbor of u, if d(u)+1 < d(v), modify p(v) = u, d(v) = d(u)+1
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang mainloop gr sn tn qL d p c = let
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang (q1, u) = extractMin qL d
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang (d1, p1, c1) = updateNeighbors d p c u gr
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang in if u == tn then shortPath sn p1 c1 [] tn
175c9e5fde43fc804a8d25198133288669b9d54cKlaus Luettich else mainloop gr sn tn q1 d1 p1 c1
175c9e5fde43fc804a8d25198133288669b9d54cKlaus Luettich shortPath sn p1 c s u =
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang if u `notElem` Map.keys p1 then fail "path not found"
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang x = Map.findWithDefault (error $ show u) u p1 in
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang if x == sn then return (u : s, c)
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang else shortPath sn p1 c (u : s) x
b91c4dbd00294ce29ab1ae84ad4e8c93ca5ad943Heng Jiang (nodeList, com1) <- mainloop graph source target q dist prev com
b91c4dbd00294ce29ab1ae84ad4e8c93ca5ad943Heng Jiang foldM comp ((Map.!) com1 source) . map ((Map.!) com1) $ nodeList
b91c4dbd00294ce29ab1ae84ad4e8c93ca5ad943Heng Jiang{- builds the arrows from the nodes of the original graph
b91c4dbd00294ce29ab1ae84ad4e8c93ca5ad943Heng Jiangto the unique maximal node of the obtained graph -}
b91c4dbd00294ce29ab1ae84ad4e8c93ca5ad943Heng JiangbuildStrMorphisms :: GDiagram -> GDiagram
b91c4dbd00294ce29ab1ae84ad4e8c93ca5ad943Heng Jiang -> Result (G_theory, Map.Map Node GMorphism)
b91c4dbd00294ce29ab1ae84ad4e8c93ca5ad943Heng JiangbuildStrMorphisms initGraph newGraph = do
b91c4dbd00294ce29ab1ae84ad4e8c93ca5ad943Heng Jiang let (maxNode, sigma) = head $ filter (\ (node, _) -> outdeg newGraph node == 0) $
b91c4dbd00294ce29ab1ae84ad4e8c93ca5ad943Heng Jiang labNodes newGraph
b91c4dbd00294ce29ab1ae84ad4e8c93ca5ad943Heng Jiang buildMor pairList solList =
b91c4dbd00294ce29ab1ae84ad4e8c93ca5ad943Heng Jiang case pairList of
b91c4dbd00294ce29ab1ae84ad4e8c93ca5ad943Heng Jiang (n, _) : pairs -> do nMor <- dijkstra newGraph n maxNode
b91c4dbd00294ce29ab1ae84ad4e8c93ca5ad943Heng Jiang buildMor pairs (solList ++ [(n, nMor)])
b91c4dbd00294ce29ab1ae84ad4e8c93ca5ad943Heng Jiang [] -> return solList
b91c4dbd00294ce29ab1ae84ad4e8c93ca5ad943Heng Jiang morList <- buildMor (labNodes initGraph) []
b91c4dbd00294ce29ab1ae84ad4e8c93ca5ad943Heng Jiang return (sigma, Map.fromList morList)
b91c4dbd00294ce29ab1ae84ad4e8c93ca5ad943Heng Jiang-- computes the colimit and inserts it into the graph
b91c4dbd00294ce29ab1ae84ad4e8c93ca5ad943Heng JiangaddNodeToGraph :: GDiagram -> G_theory -> G_theory -> G_theory -> Int -> Int
b91c4dbd00294ce29ab1ae84ad4e8c93ca5ad943Heng Jiang -> Int -> GMorphism -> GMorphism
b91c4dbd00294ce29ab1ae84ad4e8c93ca5ad943Heng Jiang -> Map.Map Node [(Node, G_theory)] -> [(Int, G_theory)]
b91c4dbd00294ce29ab1ae84ad4e8c93ca5ad943Heng Jiang -> Result (GDiagram, Map.Map Node [(Node, G_theory)])
b91c4dbd00294ce29ab1ae84ad4e8c93ca5ad943Heng JiangaddNodeToGraph oldGraph
b91c4dbd00294ce29ab1ae84ad4e8c93ca5ad943Heng Jiang (G_theory lid _ extSign _ _ _)
b91c4dbd00294ce29ab1ae84ad4e8c93ca5ad943Heng Jiang gt1@(G_theory lid1 _ extSign1 idx1 _ _)
b91c4dbd00294ce29ab1ae84ad4e8c93ca5ad943Heng Jiang gt2@(G_theory lid2 _ extSign2 idx2 _ _)
b91c4dbd00294ce29ab1ae84ad4e8c93ca5ad943Heng Jiang (GMorphism cid1 ss1 _ mor1 _)
c51b5677113ce7260c44afb3c5932eea6c875e27Heng Jiang (GMorphism cid2 ss2 _ mor2 _)
67d5e49547d78aa56a8f9ba5e64a950b730eba66Till Mossakowski funDesc maxNodes = do
67d5e49547d78aa56a8f9ba5e64a950b730eba66Till Mossakowski let newNode = 1 + maximum (nodes oldGraph) -- get a new node
67d5e49547d78aa56a8f9ba5e64a950b730eba66Till Mossakowski s1 <- coerceSign lid1 lid "addToNodeGraph" extSign1
67d5e49547d78aa56a8f9ba5e64a950b730eba66Till Mossakowski s2 <- coerceSign lid2 lid "addToNodeGraph" extSign2
67d5e49547d78aa56a8f9ba5e64a950b730eba66Till Mossakowski m1 <- coerceMorphism (targetLogic cid1) lid "addToNodeGraph" mor1
67d5e49547d78aa56a8f9ba5e64a950b730eba66Till Mossakowski m2 <- coerceMorphism (targetLogic cid2) lid "addToNodeGraph" mor2
67d5e49547d78aa56a8f9ba5e64a950b730eba66Till Mossakowski [(n, plainSign extSign), (n1, plainSign s1), (n2, plainSign s2)]
67d5e49547d78aa56a8f9ba5e64a950b730eba66Till Mossakowski [(n, n1, (1, m1)), (n, n2, (1, m2))]
67d5e49547d78aa56a8f9ba5e64a950b730eba66Till Mossakowski (sig, morMap) <- weakly_amalgamable_colimit lid spanGr
67d5e49547d78aa56a8f9ba5e64a950b730eba66Till Mossakowski -- must coerce here
67d5e49547d78aa56a8f9ba5e64a950b730eba66Till Mossakowski m11 <- coerceMorphism lid (targetLogic cid1) "addToNodeGraph" $
67d5e49547d78aa56a8f9ba5e64a950b730eba66Till Mossakowski morMap Map.! n1
67d5e49547d78aa56a8f9ba5e64a950b730eba66Till Mossakowski m22 <- coerceMorphism lid (targetLogic cid2) "addToNodeGraph" $
67d5e49547d78aa56a8f9ba5e64a950b730eba66Till Mossakowski morMap Map.! n2
67d5e49547d78aa56a8f9ba5e64a950b730eba66Till Mossakowski let gth = noSensGTheory lid (mkExtSign sig) startSigId
67d5e49547d78aa56a8f9ba5e64a950b730eba66Till Mossakowski gmor1 = GMorphism cid1 ss1 idx1 m11 startMorId
67d5e49547d78aa56a8f9ba5e64a950b730eba66Till Mossakowski gmor2 = GMorphism cid2 ss2 idx2 m22 startMorId
67d5e49547d78aa56a8f9ba5e64a950b730eba66Till Mossakowski case maxNodes of
67d5e49547d78aa56a8f9ba5e64a950b730eba66Till Mossakowski let newGraph = insEdges [(n1, newNode, (1, gmor1)), (n2, newNode, (1, gmor2))] $
67d5e49547d78aa56a8f9ba5e64a950b730eba66Till Mossakowski insNode (newNode, gth) oldGraph
b91c4dbd00294ce29ab1ae84ad4e8c93ca5ad943Heng Jiang funDesc1 = Map.insert newNode
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang (nub $ (Map.!) funDesc n1 ++ (Map.!) funDesc n2 ) funDesc
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang return (newGraph, funDesc1)
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang _ -> computeCoeqs oldGraph funDesc (n1, gt1) (n2, gt2)
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang (newNode, gth) gmor1 gmor2 maxNodes
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang{- for each node in the list, check whether the coequalizer can be computed
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiangif so, modify the maximal node of graph and the edges to it from n1 and n2 -}
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng JiangcomputeCoeqs :: GDiagram -> Map.Map Node [(Node, G_theory)]
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang -> (Node, G_theory) -> (Node, G_theory) -> (Node, G_theory)
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang -> GMorphism -> GMorphism -> [(Node, G_theory)] ->
b3c65285705f6d184b5f8b00b1a328d96b6b19c5Heng Jiang Result (GDiagram, Map.Map Node [(Node, G_theory)])
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng JiangcomputeCoeqs oldGraph funDesc (n1, _) (n2, _) (newN, newGt) gmor1 gmor2 [] = do
b91c4dbd00294ce29ab1ae84ad4e8c93ca5ad943Heng Jiang let newGraph = insEdges [(n1, newN, (1, gmor1)), (n2, newN, (1, gmor2))] $
c51b5677113ce7260c44afb3c5932eea6c875e27Heng Jiang insNode (newN, newGt) oldGraph
b91c4dbd00294ce29ab1ae84ad4e8c93ca5ad943Heng Jiang descFun1 = Map.insert newN
b3c65285705f6d184b5f8b00b1a328d96b6b19c5Heng Jiang (nub $ (Map.!) funDesc n1 ++ (Map.!) funDesc n2 ) funDesc
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang return (newGraph, descFun1)
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng JiangcomputeCoeqs graph funDesc (n1, gt1) (n2, gt2)
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang (newN, _newGt@(G_theory tlid _ tsign _ _ _))
b91c4dbd00294ce29ab1ae84ad4e8c93ca5ad943Heng Jiang _gmor1@(GMorphism cid1 sig1 idx1 mor1 _ )
b3c65285705f6d184b5f8b00b1a328d96b6b19c5Heng Jiang _gmor2@(GMorphism cid2 sig2 idx2 mor2 _ ) ((n, gt) : descs) = do
c51b5677113ce7260c44afb3c5932eea6c875e27Heng Jiang _rho1@(GMorphism cid3 _ _ mor3 _) <- dijkstra graph n n1
c51b5677113ce7260c44afb3c5932eea6c875e27Heng Jiang _rho2@(GMorphism cid4 _ _ mor4 _) <- dijkstra graph n n2
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang com1 <- compComorphism (Comorphism cid1) (Comorphism cid3)
b91c4dbd00294ce29ab1ae84ad4e8c93ca5ad943Heng Jiang com2 <- compComorphism (Comorphism cid1) (Comorphism cid3)
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang if com1 /= com2 then fail "Unable to compute coequalizer" else do
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang _gtM@(G_theory lidM _ signM _idxM _ _) <- mapG_theory com1 gt
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang s1 <- coerceSign lidM tlid "coequalizers" signM
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang mor3' <- coerceMorphism (targetLogic cid3) (sourceLogic cid1) "coeqs" mor3
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang mor4' <- coerceMorphism (targetLogic cid4) (sourceLogic cid2) "coeqs" mor4
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang m1 <- map_morphism cid1 mor3'
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang m2 <- map_morphism cid2 mor4'
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang phi1' <- comp m1 mor1
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang phi2' <- comp m2 mor2
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang phi1 <- coerceMorphism (targetLogic cid1) tlid "coeqs" phi1'
b91c4dbd00294ce29ab1ae84ad4e8c93ca5ad943Heng Jiang phi2 <- coerceMorphism (targetLogic cid2) tlid "coeqs" phi2'
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang -- build the double arrow for computing the coequalizers
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang let doubleArrow = Graph.mkGraph
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang [(n, plainSign s1), (newN, plainSign tsign)]
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang [(n, newN, (1, phi1)), (n, newN, (1, phi2))]
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang (colS, colM) <- weakly_amalgamable_colimit tlid doubleArrow
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang let newGt1 = noSensGTheory tlid (mkExtSign colS) startSigId
b3c65285705f6d184b5f8b00b1a328d96b6b19c5Heng Jiang mor11' <- coerceMorphism tlid (targetLogic cid1) "coeqs" $ (Map.!) colM newN
c51b5677113ce7260c44afb3c5932eea6c875e27Heng Jiang mor11 <- comp mor1 mor11'
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang mor22' <- coerceMorphism tlid (targetLogic cid2) "coeqs" $ (Map.!) colM newN
b3c65285705f6d184b5f8b00b1a328d96b6b19c5Heng Jiang mor22 <- comp mor2 mor22'
b3c65285705f6d184b5f8b00b1a328d96b6b19c5Heng Jiang let gMor11 = GMorphism cid1 sig1 idx1 mor11 startMorId
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang let gMor22 = GMorphism cid2 sig2 idx2 mor22 startMorId
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang computeCoeqs graph funDesc (n1, gt1) (n2, gt2) (newN, newGt1)
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang gMor11 gMor22 descs
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang-- returns a maximal node available
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng JiangpickMaxNode :: (MonadPlus t) => Gr a b -> t (Node, a)
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng JiangpickMaxNode graph = msum $ map return $
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang filter (\ (node, _) -> outdeg graph node == 0) $
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang labNodes graph
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang{- returns a list of common descendants of two maximal nodes:
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiangone node if a glb exists, or all maximal descendants otherwise -}
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng JiangcommonDesc :: Map.Map Node [(Node, G_theory)] -> Node -> Node
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang -> [(Node, G_theory)]
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng JiangcommonDesc funDesc n1 n2 = case glb funDesc n1 n2 of
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang Just x -> [x]
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang Nothing -> maxBounds funDesc n1 n2
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang-- returns a weakly amalgamable square of lax triangles
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng JiangpickSquare :: (MonadPlus t) => Result GMorphism -> Result GMorphism -> t Square
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng JiangpickSquare (Result _ (Just phi1@(GMorphism cid1 _ _ _ _)))
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang (Result _ (Just phi2@(GMorphism cid2 _ _ _ _))) =
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang if isHomogeneous phi1 && isHomogeneous phi2 then
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang return $ mkIdSquare $ Logic $ sourceLogic cid1
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang -- since they have the same target, both homogeneous implies same logic
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang {- if one of them is homogeneous, build the square
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang with identity modification of the other comorphism -}
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang let defaultSquare
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang | isHomogeneous phi1 = [mkDefSquare $ Comorphism cid2]
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang | isHomogeneous phi2 = [mirrorSquare $ mkDefSquare $ Comorphism cid1]
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang | otherwise = []
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang case maybeResult $ lookupSquare_in_LG (Comorphism cid1) (Comorphism cid2) of
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang Nothing -> msum $ map return defaultSquare
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang Just sqList -> msum $ map return $ sqList ++ defaultSquare
Map.Map Node [(Node, G_theory)] ->
Result (GDiagram, Map.Map Node [(Node, G_theory)])
GDiagram -> Map.Map Int [(Int, G_theory)] -> t m GDiagram