```{- |
Module      :  ./Common/SetColimit.hs
Description :  colimit of an arbitrary diagram in Set
Copyright   :  (c) Mihai Codescu, and Uni Bremen 2002-2006
Maintainer  :  mcodescu@informatik.uni-bremen.de
Stability   :  provisional
Portability :  portable

Computes the colimit of an arbitrary diagram in Set:
- the set is the disjoint union of all sets in the diagram
(which we obtain by pairing elements with the node number)
factored by the equivalence generated by the pairs (x, f_i(x)),
with i an arrow in the diagram
- structural morphisms are factorizations

-}

module Common.SetColimit (
computeColimitSet,
computeColimitRel,
colimitRel,
SymbolName (..)
)
where

import Common.Id
import Common.IRI
import Common.Lib.Graph
import Common.Lib.Rel (leqClasses)

import Data.Graph.Inductive.Graph
import qualified Data.Map as Map
import qualified Data.Set as Set

import qualified Data.Relation as Rel

compose :: (Ord a) => Set.Set (a, Int) ->
Map.Map (a, Int) (a, Int) ->
Map.Map (a, Int) (a, Int) ->
Map.Map (a, Int) (a, Int)
compose :: Set (a, Int)
-> Map (a, Int) (a, Int)
-> Map (a, Int) (a, Int)
-> Map (a, Int) (a, Int)
compose s :: Set (a, Int)
s f :: Map (a, Int) (a, Int)
f g :: Map (a, Int) (a, Int)
g = ((a, Int) -> Map (a, Int) (a, Int) -> Map (a, Int) (a, Int))
-> Map (a, Int) (a, Int) -> Set (a, Int) -> Map (a, Int) (a, Int)
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold ( \ i :: (a, Int)
i h :: Map (a, Int) (a, Int)
h ->
let
i' :: (a, Int)
i' = (a, Int) -> (a, Int) -> Map (a, Int) (a, Int) -> (a, Int)
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (a, Int)
i (a, Int)
i Map (a, Int) (a, Int)
f
j :: (a, Int)
j = (a, Int) -> (a, Int) -> Map (a, Int) (a, Int) -> (a, Int)
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (a, Int)
i' (a, Int)
i' Map (a, Int) (a, Int)
g in
if (a, Int)
i (a, Int) -> (a, Int) -> Bool
forall a. Eq a => a -> a -> Bool
== (a, Int)
j then Map (a, Int) (a, Int)
h else (a, Int)
-> (a, Int) -> Map (a, Int) (a, Int) -> Map (a, Int) (a, Int)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (a, Int)
i (a, Int)
j Map (a, Int) (a, Int)
h)
Map (a, Int) (a, Int)
forall k a. Map k a
Map.empty Set (a, Int)
s

coeq :: (Ord a) =>
Set.Set (a, Int) -> Set.Set (a, Int) ->
Map.Map (a, Int) (a, Int) -> Map.Map (a, Int) (a, Int) ->
(Set.Set (a, Int), Map.Map (a, Int) (a, Int))
coeq :: Set (a, Int)
-> Set (a, Int)
-> Map (a, Int) (a, Int)
-> Map (a, Int) (a, Int)
-> (Set (a, Int), Map (a, Int) (a, Int))
coeq sSet :: Set (a, Int)
sSet tSet :: Set (a, Int)
tSet f1 :: Map (a, Int) (a, Int)
f1 f2 :: Map (a, Int) (a, Int)
f2 =
case Set (a, Int) -> [(a, Int)]
forall a. Set a -> [a]
Set.elems Set (a, Int)
sSet of
[] -> (Set (a, Int)
tSet, Map (a, Int) (a, Int)
forall k a. Map k a
Map.empty)
x :: (a, Int)
x : xs :: [(a, Int)]
xs -> if [(a, Int)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(a, Int)]
xs then let
f1x :: (a, Int)
f1x = (a, Int) -> (a, Int) -> Map (a, Int) (a, Int) -> (a, Int)
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (a, Int)
x (a, Int)
x Map (a, Int) (a, Int)
f1
f2x :: (a, Int)
f2x = (a, Int) -> (a, Int) -> Map (a, Int) (a, Int) -> (a, Int)
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (a, Int)
x (a, Int)
x Map (a, Int) (a, Int)
f2
in if (a, Int)
f1x (a, Int) -> (a, Int) -> Bool
forall a. Eq a => a -> a -> Bool
== (a, Int)
f2x then (Set (a, Int)
tSet, Map (a, Int) (a, Int)
forall k a. Map k a
Map.empty)
else (Set (a, Int) -> Set (a, Int) -> Set (a, Int)
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set (a, Int)
tSet (Set (a, Int) -> Set (a, Int)) -> Set (a, Int) -> Set (a, Int)
forall a b. (a -> b) -> a -> b
\$ (a, Int) -> Set (a, Int)
forall a. a -> Set a
Set.singleton (a, Int)
f2x,
[((a, Int), (a, Int))] -> Map (a, Int) (a, Int)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [((a, Int)
f2x, (a, Int)
f1x)])
else let
a1 :: Set (a, Int)
a1 = (a, Int) -> Set (a, Int)
forall a. a -> Set a
Set.singleton (a, Int)
x
a2 :: Set (a, Int)
a2 = Set (a, Int) -> Set (a, Int) -> Set (a, Int)
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set (a, Int)
sSet Set (a, Int)
a1
(c :: Set (a, Int)
c, cf :: Map (a, Int) (a, Int)
cf) = Set (a, Int)
-> Set (a, Int)
-> Map (a, Int) (a, Int)
-> Map (a, Int) (a, Int)
-> (Set (a, Int), Map (a, Int) (a, Int))
forall a.
Ord a =>
Set (a, Int)
-> Set (a, Int)
-> Map (a, Int) (a, Int)
-> Map (a, Int) (a, Int)
-> (Set (a, Int), Map (a, Int) (a, Int))
coeq Set (a, Int)
a1 Set (a, Int)
tSet Map (a, Int) (a, Int)
f1 Map (a, Int) (a, Int)
f2
cf1 :: Map (a, Int) (a, Int)
cf1 = Set (a, Int)
-> Map (a, Int) (a, Int)
-> Map (a, Int) (a, Int)
-> Map (a, Int) (a, Int)
forall a.
Ord a =>
Set (a, Int)
-> Map (a, Int) (a, Int)
-> Map (a, Int) (a, Int)
-> Map (a, Int) (a, Int)
compose Set (a, Int)
a2 Map (a, Int) (a, Int)
f1 Map (a, Int) (a, Int)
cf
cf2 :: Map (a, Int) (a, Int)
cf2 = Set (a, Int)
-> Map (a, Int) (a, Int)
-> Map (a, Int) (a, Int)
-> Map (a, Int) (a, Int)
forall a.
Ord a =>
Set (a, Int)
-> Map (a, Int) (a, Int)
-> Map (a, Int) (a, Int)
-> Map (a, Int) (a, Int)
compose Set (a, Int)
a2 Map (a, Int) (a, Int)
f2 Map (a, Int) (a, Int)
cf
(d :: Set (a, Int)
d, df :: Map (a, Int) (a, Int)
df) = Set (a, Int)
-> Set (a, Int)
-> Map (a, Int) (a, Int)
-> Map (a, Int) (a, Int)
-> (Set (a, Int), Map (a, Int) (a, Int))
forall a.
Ord a =>
Set (a, Int)
-> Set (a, Int)
-> Map (a, Int) (a, Int)
-> Map (a, Int) (a, Int)
-> (Set (a, Int), Map (a, Int) (a, Int))
coeq Set (a, Int)
a2 Set (a, Int)
c Map (a, Int) (a, Int)
cf1 Map (a, Int) (a, Int)
cf2
coeqf :: Map (a, Int) (a, Int)
coeqf = Set (a, Int)
-> Map (a, Int) (a, Int)
-> Map (a, Int) (a, Int)
-> Map (a, Int) (a, Int)
forall a.
Ord a =>
Set (a, Int)
-> Map (a, Int) (a, Int)
-> Map (a, Int) (a, Int)
-> Map (a, Int) (a, Int)
compose Set (a, Int)
tSet Map (a, Int) (a, Int)
cf Map (a, Int) (a, Int)
df
in (Set (a, Int)
d, Map (a, Int) (a, Int)
coeqf)

computeColimitSet :: (Ord a) =>
Gr (Set.Set a) (Int, Map.Map a a) ->
(Set.Set (a, Node), Map.Map Node (Map.Map a (a, Node)))
computeColimitSet :: Gr (Set a) (Int, Map a a)
-> (Set (a, Int), Map Int (Map a (a, Int)))
computeColimitSet graph :: Gr (Set a) (Int, Map a a)
graph = let
unionSet :: Set (a, Int)
unionSet = (Set (a, Int) -> Set (a, Int) -> Set (a, Int))
-> Set (a, Int) -> [Set (a, Int)] -> Set (a, Int)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Set (a, Int) -> Set (a, Int) -> Set (a, Int)
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set (a, Int)
forall a. Set a
Set.empty ([Set (a, Int)] -> Set (a, Int)) -> [Set (a, Int)] -> Set (a, Int)
forall a b. (a -> b) -> a -> b
\$
((Int, Set a) -> Set (a, Int)) -> [(Int, Set a)] -> [Set (a, Int)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (n :: Int
n, s :: Set a
s) -> (a -> (a, Int)) -> Set a -> Set (a, Int)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (\ x :: a
x -> (a
x, Int
n)) Set a
s) ([(Int, Set a)] -> [Set (a, Int)])
-> [(Int, Set a)] -> [Set (a, Int)]
forall a b. (a -> b) -> a -> b
\$ Gr (Set a) (Int, Map a a) -> [(Int, Set a)]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode a]
labNodes Gr (Set a) (Int, Map a a)
graph
inclMap :: Map Int (Map (a, Int) (a, Int))
inclMap = [(Int, Map (a, Int) (a, Int))] -> Map Int (Map (a, Int) (a, Int))
forall k a. Eq k => [(k, a)] -> Map k a
Map.fromAscList ([(Int, Map (a, Int) (a, Int))] -> Map Int (Map (a, Int) (a, Int)))
-> [(Int, Map (a, Int) (a, Int))]
-> Map Int (Map (a, Int) (a, Int))
forall a b. (a -> b) -> a -> b
\$ ((Int, Set a) -> (Int, Map (a, Int) (a, Int)))
-> [(Int, Set a)] -> [(Int, Map (a, Int) (a, Int))]
forall a b. (a -> b) -> [a] -> [b]
map (\ (n :: Int
n, s :: Set a
s) -> (Int
n, [((a, Int), (a, Int))] -> Map (a, Int) (a, Int)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([((a, Int), (a, Int))] -> Map (a, Int) (a, Int))
-> [((a, Int), (a, Int))] -> Map (a, Int) (a, Int)
forall a b. (a -> b) -> a -> b
\$ (a -> ((a, Int), (a, Int))) -> [a] -> [((a, Int), (a, Int))]
forall a b. (a -> b) -> [a] -> [b]
map (\x :: a
x -> ((a
x,Int
n),(a
x,Int
n))) ([a] -> [((a, Int), (a, Int))]) -> [a] -> [((a, Int), (a, Int))]
forall a b. (a -> b) -> a -> b
\$ Set a -> [a]
forall a. Set a -> [a]
Set.toList Set a
s)) ([(Int, Set a)] -> [(Int, Map (a, Int) (a, Int))])
-> [(Int, Set a)] -> [(Int, Map (a, Int) (a, Int))]
forall a b. (a -> b) -> a -> b
\$ Gr (Set a) (Int, Map a a) -> [(Int, Set a)]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode a]
labNodes Gr (Set a) (Int, Map a a)
graph
(colim :: Set (a, Int)
colim, morMap :: Map Int (Map (a, Int) (a, Int))
morMap) = Gr (Set a) (Int, Map a a)
-> (Set (a, Int), Map Int (Map (a, Int) (a, Int)))
-> [LEdge (Int, Map a a)]
-> (Set (a, Int), Map Int (Map (a, Int) (a, Int)))
forall a.
Ord a =>
Gr (Set a) (Int, Map a a)
-> (Set (a, Int), Map Int (Map (a, Int) (a, Int)))
-> [LEdge (Int, Map a a)]
-> (Set (a, Int), Map Int (Map (a, Int) (a, Int)))
computeCoeqs Gr (Set a) (Int, Map a a)
graph (Set (a, Int)
unionSet, Map Int (Map (a, Int) (a, Int))
inclMap) ([LEdge (Int, Map a a)]
-> (Set (a, Int), Map Int (Map (a, Int) (a, Int))))
-> [LEdge (Int, Map a a)]
-> (Set (a, Int), Map Int (Map (a, Int) (a, Int)))
forall a b. (a -> b) -> a -> b
\$ Gr (Set a) (Int, Map a a) -> [LEdge (Int, Map a a)]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LEdge b]
labEdges Gr (Set a) (Int, Map a a)
graph
morMap' :: Map Int (Map a (a, Int))
morMap' = (Map (a, Int) (a, Int) -> Map a (a, Int))
-> Map Int (Map (a, Int) (a, Int)) -> Map Int (Map a (a, Int))
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map
([(a, (a, Int))] -> Map a (a, Int)
forall k a. Eq k => [(k, a)] -> Map k a
Map.fromAscList ([(a, (a, Int))] -> Map a (a, Int))
-> (Map (a, Int) (a, Int) -> [(a, (a, Int))])
-> Map (a, Int) (a, Int)
-> Map a (a, Int)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (((a, Int), (a, Int)) -> (a, (a, Int)))
-> [((a, Int), (a, Int))] -> [(a, (a, Int))]
forall a b. (a -> b) -> [a] -> [b]
map (\ ((x :: a
x, _), z :: (a, Int)
z) -> (a
x, (a, Int)
z)) ([((a, Int), (a, Int))] -> [(a, (a, Int))])
-> (Map (a, Int) (a, Int) -> [((a, Int), (a, Int))])
-> Map (a, Int) (a, Int)
-> [(a, (a, Int))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map (a, Int) (a, Int) -> [((a, Int), (a, Int))]
forall k a. Map k a -> [(k, a)]
Map.toList)
Map Int (Map (a, Int) (a, Int))
morMap
in (Set (a, Int)
colim, Map Int (Map a (a, Int))
morMap')

computeCoeqs :: (Ord a) =>
Gr (Set.Set a) (Int, Map.Map a a) ->
(Set.Set (a, Node), Map.Map Node (Map.Map (a, Node) (a, Node))) ->
[LEdge (Int, Map.Map a a)] ->
(Set.Set (a, Node), Map.Map Node (Map.Map (a, Node) (a, Node)))
computeCoeqs :: Gr (Set a) (Int, Map a a)
-> (Set (a, Int), Map Int (Map (a, Int) (a, Int)))
-> [LEdge (Int, Map a a)]
-> (Set (a, Int), Map Int (Map (a, Int) (a, Int)))
computeCoeqs graph :: Gr (Set a) (Int, Map a a)
graph (colim :: Set (a, Int)
colim, morMap :: Map Int (Map (a, Int) (a, Int))
morMap) edgeList :: [LEdge (Int, Map a a)]
edgeList =
case [LEdge (Int, Map a a)]
edgeList of
[] -> (Set (a, Int)
colim, Map Int (Map (a, Int) (a, Int))
morMap)
(sn :: Int
sn, tn :: Int
tn, (_, f :: Map a a
f)) : edges' :: [LEdge (Int, Map a a)]
edges' -> let
Just sset :: Set a
sset = Gr (Set a) (Int, Map a a) -> Int -> Maybe (Set a)
forall (gr :: * -> * -> *) a b.
Graph gr =>
gr a b -> Int -> Maybe a
lab Gr (Set a) (Int, Map a a)
graph Int
sn
f1 :: Map (a, Int) (a, Int)
f1 = Map Int (Map (a, Int) (a, Int))
morMap Map Int (Map (a, Int) (a, Int)) -> Int -> Map (a, Int) (a, Int)
forall k a. Ord k => Map k a -> k -> a
Map.! Int
sn
f' :: Map (a, Int) (a, Int)
f' = [((a, Int), (a, Int))] -> Map (a, Int) (a, Int)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([((a, Int), (a, Int))] -> Map (a, Int) (a, Int))
-> [((a, Int), (a, Int))] -> Map (a, Int) (a, Int)
forall a b. (a -> b) -> a -> b
\$ (a -> ((a, Int), (a, Int))) -> [a] -> [((a, Int), (a, Int))]
forall a b. (a -> b) -> [a] -> [b]
map (\ x :: a
x -> ((a
x, Int
sn), (a -> a -> Map a a -> a
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault a
x a
x Map a a
f, Int
tn))) ([a] -> [((a, Int), (a, Int))]) -> [a] -> [((a, Int), (a, Int))]
forall a b. (a -> b) -> a -> b
\$
Set a -> [a]
forall a. Set a -> [a]
Set.toList Set a
sset
f2 :: Map (a, Int) (a, Int)
f2 = ((a, Int) -> (a, Int))
-> Map (a, Int) (a, Int) -> Map (a, Int) (a, Int)
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (\ x :: (a, Int)
x -> (a, Int) -> (a, Int) -> Map (a, Int) (a, Int) -> (a, Int)
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (a, Int)
x (a, Int)
x (Map Int (Map (a, Int) (a, Int))
morMap Map Int (Map (a, Int) (a, Int)) -> Int -> Map (a, Int) (a, Int)
forall k a. Ord k => Map k a -> k -> a
Map.! Int
tn)) Map (a, Int) (a, Int)
f'
(colim' :: Set (a, Int)
colim', coeqMor :: Map (a, Int) (a, Int)
coeqMor) = Set (a, Int)
-> Set (a, Int)
-> Map (a, Int) (a, Int)
-> Map (a, Int) (a, Int)
-> (Set (a, Int), Map (a, Int) (a, Int))
forall a.
Ord a =>
Set (a, Int)
-> Set (a, Int)
-> Map (a, Int) (a, Int)
-> Map (a, Int) (a, Int)
-> (Set (a, Int), Map (a, Int) (a, Int))
coeq ((a -> (a, Int)) -> Set a -> Set (a, Int)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (\ x :: a
x -> (a
x, Int
sn)) Set a
sset) Set (a, Int)
colim Map (a, Int) (a, Int)
f1 Map (a, Int) (a, Int)
f2
morMap' :: Map Int (Map (a, Int) (a, Int))
morMap' = [(Int, Map (a, Int) (a, Int))] -> Map Int (Map (a, Int) (a, Int))
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Int, Map (a, Int) (a, Int))] -> Map Int (Map (a, Int) (a, Int)))
-> [(Int, Map (a, Int) (a, Int))]
-> Map Int (Map (a, Int) (a, Int))
forall a b. (a -> b) -> a -> b
\$
((Int, Map (a, Int) (a, Int)) -> (Int, Map (a, Int) (a, Int)))
-> [(Int, Map (a, Int) (a, Int))] -> [(Int, Map (a, Int) (a, Int))]
forall a b. (a -> b) -> [a] -> [b]
map (\ (n :: Int
n, g :: Map (a, Int) (a, Int)
g) -> let
Just nset :: Set a
nset = Gr (Set a) (Int, Map a a) -> Int -> Maybe (Set a)
forall (gr :: * -> * -> *) a b.
Graph gr =>
gr a b -> Int -> Maybe a
lab Gr (Set a) (Int, Map a a)
graph Int
n
in (Int
n, [((a, Int), (a, Int))] -> Map (a, Int) (a, Int)
forall k a. Eq k => [(k, a)] -> Map k a
Map.fromAscList ([((a, Int), (a, Int))] -> Map (a, Int) (a, Int))
-> [((a, Int), (a, Int))] -> Map (a, Int) (a, Int)
forall a b. (a -> b) -> a -> b
\$
((a, Int) -> ((a, Int), (a, Int)))
-> [(a, Int)] -> [((a, Int), (a, Int))]
forall a b. (a -> b) -> [a] -> [b]
map (\ x :: (a, Int)
x -> let
y :: (a, Int)
y = (a, Int) -> (a, Int) -> Map (a, Int) (a, Int) -> (a, Int)
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (a, Int)
x (a, Int)
x Map (a, Int) (a, Int)
g
in ((a, Int)
x, (a, Int) -> (a, Int) -> Map (a, Int) (a, Int) -> (a, Int)
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (a, Int)
y (a, Int)
y Map (a, Int) (a, Int)
coeqMor)) ([(a, Int)] -> [((a, Int), (a, Int))])
-> [(a, Int)] -> [((a, Int), (a, Int))]
forall a b. (a -> b) -> a -> b
\$
Set (a, Int) -> [(a, Int)]
forall a. Set a -> [a]
Set.toList (Set (a, Int) -> [(a, Int)]) -> Set (a, Int) -> [(a, Int)]
forall a b. (a -> b) -> a -> b
\$ (a -> (a, Int)) -> Set a -> Set (a, Int)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (\ x :: a
x -> (a
x, Int
n)) Set a
nset ))
([(Int, Map (a, Int) (a, Int))] -> [(Int, Map (a, Int) (a, Int))])
-> [(Int, Map (a, Int) (a, Int))] -> [(Int, Map (a, Int) (a, Int))]
forall a b. (a -> b) -> a -> b
\$ Map Int (Map (a, Int) (a, Int)) -> [(Int, Map (a, Int) (a, Int))]
forall k a. Map k a -> [(k, a)]
Map.toList Map Int (Map (a, Int) (a, Int))
morMap
in Gr (Set a) (Int, Map a a)
-> (Set (a, Int), Map Int (Map (a, Int) (a, Int)))
-> [LEdge (Int, Map a a)]
-> (Set (a, Int), Map Int (Map (a, Int) (a, Int)))
forall a.
Ord a =>
Gr (Set a) (Int, Map a a)
-> (Set (a, Int), Map Int (Map (a, Int) (a, Int)))
-> [LEdge (Int, Map a a)]
-> (Set (a, Int), Map Int (Map (a, Int) (a, Int)))
computeCoeqs Gr (Set a) (Int, Map a a)
graph (Set (a, Int)
colim', Map Int (Map (a, Int) (a, Int))
morMap') [LEdge (Int, Map a a)]
edges'

class (Eq a, Ord a) => SymbolName a where
addString :: (a, String) -> a

instance SymbolName Token where
addString :: (Token, String) -> Token
t, s :: String
s) = Token -> String -> Token
t String
s

instance SymbolName Id where
addString :: (Id, String) -> Id
x, y :: String
y) = Id -> String -> Id
appendString Id
x String
y

instance SymbolName IRI where
addString :: (IRI, String) -> IRI
x, y :: String
y) = String -> IRI -> IRI
y IRI
x

(Set.Set (a, Node), Map.Map Node (Map.Map a (a, Node))) ->
(Set.Set a, Map.Map Node (Map.Map a a))
addIntToSymbols :: (Set (a, Int), Map Int (Map a (a, Int)))
-> (Set a, Map Int (Map a a))
addIntToSymbols (set :: Set (a, Int)
set, fun :: Map Int (Map a (a, Int))
fun) = let
fstEqual :: (a, b) -> (a, b) -> Bool
fstEqual (x1 :: a
x1, _) (x2 :: a
x2, _) = a
x1 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
x2
partList :: Set (a, Int) -> [[(a, Int)]]
partList = ((a, Int) -> (a, Int) -> Bool) -> Set (a, Int) -> [[(a, Int)]]
forall a. Ord a => (a -> a -> Bool) -> Set a -> [[a]]
leqClasses (a, Int) -> (a, Int) -> Bool
forall a b b. Eq a => (a, b) -> (a, b) -> Bool
fstEqual
namePartitions :: [[(a, a)]]
-> Map k (Map k (a, a))
-> Set a
-> Map k (Map k a)
-> (Set a, Map k (Map k a))
namePartitions elemList :: [[(a, a)]]
elemList f0 :: Map k (Map k (a, a))
f0 s1 :: Set a
s1 f1 :: Map k (Map k a)
f1 = case [[(a, a)]]
elemList of
[] -> (Set a
s1, Map k (Map k a)
f1)
p :: [(a, a)]
p : ps :: [[(a, a)]]
ps -> if [(a, a)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(a, a)]
p Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 1 then
-- a single element with this name,it can be kept
let s2 :: Set a
s2 = a -> Set a -> Set a
forall a. Ord a => a -> Set a -> Set a
Set.insert ((a, a) -> a
forall a b. (a, b) -> a
fst ((a, a) -> a) -> (a, a) -> a
forall a b. (a -> b) -> a -> b
\$ [(a, a)] -> (a, a)
forall a. [a] -> a
p) Set a
s1
updateF :: k -> Map k a
updateF node :: k
node = Map k a -> Map k a -> Map k a
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (Map k a -> k -> Map k (Map k a) -> Map k a
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> Map k a
forall a. HasCallStack => String -> a
error "f1") k
node Map k (Map k a)
f1) (Map k a -> Map k a) -> Map k a -> Map k a
forall a b. (a -> b) -> a -> b
\$
[(k, a)] -> Map k a
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(k, a)] -> Map k a) -> [(k, a)] -> Map k a
forall a b. (a -> b) -> a -> b
\$ (k -> (k, a)) -> [k] -> [(k, a)]
forall a b. (a -> b) -> [a] -> [b]
map (\ x :: k
x -> (k
x, (a, a) -> a
forall a b. (a, b) -> a
fst ((a, a) -> a) -> (a, a) -> a
forall a b. (a -> b) -> a -> b
\$ [(a, a)] -> (a, a)
forall a. [a] -> a
p)) ([k] -> [(k, a)]) -> [k] -> [(k, a)]
forall a b. (a -> b) -> a -> b
\$
(k -> Bool) -> [k] -> [k]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ x :: k
x -> (a, a) -> k -> Map k (a, a) -> (a, a)
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> (a, a)
forall a. HasCallStack => String -> a
error "fo(node)") k
x
(Map k (a, a) -> k -> Map k (Map k (a, a)) -> Map k (a, a)
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> Map k (a, a)
forall a. HasCallStack => String -> a
error "f0") k
node Map k (Map k (a, a))
f0)
(a, a) -> (a, a) -> Bool
forall a. Eq a => a -> a -> Bool
== [(a, a)] -> (a, a)
forall a. [a] -> a
p) ([k] -> [k]) -> [k] -> [k]
forall a b. (a -> b) -> a -> b
\$
Map k (a, a) -> [k]
forall k a. Map k a -> [k]
Map.keys (Map k (a, a) -> [k]) -> Map k (a, a) -> [k]
forall a b. (a -> b) -> a -> b
\$ Map k (a, a) -> k -> Map k (Map k (a, a)) -> Map k (a, a)
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> Map k (a, a)
forall a. HasCallStack => String -> a
error "f0")
k
node Map k (Map k (a, a))
f0
f2 :: Map k (Map k a)
f2 = [(k, Map k a)] -> Map k (Map k a)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(k, Map k a)] -> Map k (Map k a))
-> [(k, Map k a)] -> Map k (Map k a)
forall a b. (a -> b) -> a -> b
\$ [k] -> [Map k a] -> [(k, Map k a)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Map k (Map k (a, a)) -> [k]
forall k a. Map k a -> [k]
Map.keys Map k (Map k (a, a))
f0) ([Map k a] -> [(k, Map k a)]) -> [Map k a] -> [(k, Map k a)]
forall a b. (a -> b) -> a -> b
\$ (k -> Map k a) -> [k] -> [Map k a]
forall a b. (a -> b) -> [a] -> [b]
map k -> Map k a
updateF ([k] -> [Map k a]) -> [k] -> [Map k a]
forall a b. (a -> b) -> a -> b
\$ Map k (Map k (a, a)) -> [k]
forall k a. Map k a -> [k]
Map.keys Map k (Map k (a, a))
f0
in [[(a, a)]]
-> Map k (Map k (a, a))
-> Set a
-> Map k (Map k a)
-> (Set a, Map k (Map k a))
namePartitions [[(a, a)]]
ps Map k (Map k (a, a))
f0 Set a
s2 Map k (Map k a)
f2
else
-- several elements with same name, the number is added at the end
let s2 :: Set a
s2 = Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set a
s1 (Set a -> Set a) -> Set a -> Set a
forall a b. (a -> b) -> a -> b
\$ [a] -> Set a
forall a. Ord a => [a] -> Set a
Set.fromList ([a] -> Set a) -> [a] -> Set a
forall a b. (a -> b) -> a -> b
\$ ((a, a) -> a) -> [(a, a)] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (\(x :: a
x,y :: a
y) -> (a, String) -> a
forall a. SymbolName a => (a, String) -> a
x, a -> String
forall a. Show a => a -> String
show a
y)) [(a, a)]
p
a2String :: (a, a) -> (a, String)
a2String (x :: a
x,y :: a
y) = (a
x, a -> String
forall a. Show a => a -> String
show a
y)
updateF :: k -> Map k a
updateF node :: k
node = Map k a -> Map k a -> Map k a
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (Map k a -> k -> Map k (Map k a) -> Map k a
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> Map k a
forall a. HasCallStack => String -> a
error "f1") k
node Map k (Map k a)
f1) (Map k a -> Map k a) -> Map k a -> Map k a
forall a b. (a -> b) -> a -> b
\$
[(k, a)] -> Map k a
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(k, a)] -> Map k a) -> [(k, a)] -> Map k a
forall a b. (a -> b) -> a -> b
\$
(k -> (k, a)) -> [k] -> [(k, a)]
forall a b. (a -> b) -> [a] -> [b]
map ( \ x :: k
x -> (k
x, (a, String) -> a
forall a. SymbolName a => (a, String) -> a
addString ((a, String) -> a) -> (a, String) -> a
forall a b. (a -> b) -> a -> b
\$ (a, a) -> (a, String)
forall a a. Show a => (a, a) -> (a, String)
a2String ((a, a) -> (a, String)) -> (a, a) -> (a, String)
forall a b. (a -> b) -> a -> b
\$
(a, a) -> k -> Map k (a, a) -> (a, a)
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> (a, a)
forall a. HasCallStack => String -> a
x
(Map k (a, a) -> k -> Map k (Map k (a, a)) -> Map k (a, a)
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> Map k (a, a)
forall a. HasCallStack => String -> a
error "f0") k
node Map k (Map k (a, a))
f0))) ([k] -> [(k, a)]) -> [k] -> [(k, a)]
forall a b. (a -> b) -> a -> b
\$
(k -> Bool) -> [k] -> [k]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ x :: k
x -> (a, a) -> k -> Map k (a, a) -> (a, a)
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> (a, a)
forall a. HasCallStack => String -> a
error "fo(node)") k
x
(Map k (a, a) -> k -> Map k (Map k (a, a)) -> Map k (a, a)
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> Map k (a, a)
forall a. HasCallStack => String -> a
error "f0") k
node Map k (Map k (a, a))
f0)
(a, a) -> [(a, a)] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [(a, a)]
p) ([k] -> [k]) -> [k] -> [k]
forall a b. (a -> b) -> a -> b
\$
Map k (a, a) -> [k]
forall k a. Map k a -> [k]
Map.keys (Map k (a, a) -> [k]) -> Map k (a, a) -> [k]
forall a b. (a -> b) -> a -> b
\$ Map k (a, a) -> k -> Map k (Map k (a, a)) -> Map k (a, a)
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> Map k (a, a)
forall a. HasCallStack => String -> a
error "f0") k
node Map k (Map k (a, a))
f0
f2 :: Map k (Map k a)
f2 = [(k, Map k a)] -> Map k (Map k a)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(k, Map k a)] -> Map k (Map k a))
-> [(k, Map k a)] -> Map k (Map k a)
forall a b. (a -> b) -> a -> b
\$ [k] -> [Map k a] -> [(k, Map k a)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Map k (Map k (a, a)) -> [k]
forall k a. Map k a -> [k]
Map.keys Map k (Map k (a, a))
f0) ([Map k a] -> [(k, Map k a)]) -> [Map k a] -> [(k, Map k a)]
forall a b. (a -> b) -> a -> b
\$ (k -> Map k a) -> [k] -> [Map k a]
forall a b. (a -> b) -> [a] -> [b]
map k -> Map k a
updateF ([k] -> [Map k a]) -> [k] -> [Map k a]
forall a b. (a -> b) -> a -> b
\$ Map k (Map k (a, a)) -> [k]
forall k a. Map k a -> [k]
Map.keys Map k (Map k (a, a))
f0
in [[(a, a)]]
-> Map k (Map k (a, a))
-> Set a
-> Map k (Map k a)
-> (Set a, Map k (Map k a))
namePartitions [[(a, a)]]
ps Map k (Map k (a, a))
f0 Set a
s2 Map k (Map k a)
f2
in [[(a, Int)]]
-> Map Int (Map a (a, Int))
-> Set a
-> Map Int (Map a a)
-> (Set a, Map Int (Map a a))
forall k k a a.
(Eq a, Ord k, Ord k, SymbolName a, Show a) =>
[[(a, a)]]
-> Map k (Map k (a, a))
-> Set a
-> Map k (Map k a)
-> (Set a, Map k (Map k a))
namePartitions (Set (a, Int) -> [[(a, Int)]]
partList Set (a, Int)
set) Map Int (Map a (a, Int))
fun Set a
forall a. Set a
Set.empty (Map Int (Map a a) -> (Set a, Map Int (Map a a)))
-> Map Int (Map a a) -> (Set a, Map Int (Map a a))
forall a b. (a -> b) -> a -> b
\$
[(Int, Map a a)] -> Map Int (Map a a)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Int, Map a a)] -> Map Int (Map a a))
-> [(Int, Map a a)] -> Map Int (Map a a)
forall a b. (a -> b) -> a -> b
\$ [Int] -> [Map a a] -> [(Int, Map a a)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Map Int (Map a (a, Int)) -> [Int]
forall k a. Map k a -> [k]
Map.keys Map Int (Map a (a, Int))
fun) (Map a a -> [Map a a]
forall a. a -> [a]
repeat Map a a
forall k a. Map k a
Map.empty)

colimitRel :: (Ord a) =>
[(Int, Rel.Relation a a)] -> Map.Map Node (Map.Map a a) ->
Rel.Relation a a
colimitRel :: [(Int, Relation a a)] -> Map Int (Map a a) -> Relation a a
colimitRel rels :: [(Int, Relation a a)]
rels nMaps :: Map Int (Map a a)
nMaps =
(Relation a a -> (Int, Relation a a) -> Relation a a)
-> Relation a a -> [(Int, Relation a a)] -> Relation a a
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\r :: Relation a a
r (n :: Int
n, r' :: Relation a a
r') -> let nf :: Map a a
nf = Map a a -> Int -> Map Int (Map a a) -> Map a a
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> Map a a
forall a. HasCallStack => String -> a
error "nf") Int
n Map Int (Map a a)
nMaps
r'' :: Relation a a
r'' = [(a, a)] -> Relation a a
forall a b. (Ord a, Ord b) => [(a, b)] -> Relation a b
Rel.fromList ([(a, a)] -> Relation a a) -> [(a, a)] -> Relation a a
forall a b. (a -> b) -> a -> b
\$
((a, a) -> (a, a)) -> [(a, a)] -> [(a, a)]
forall a b. (a -> b) -> [a] -> [b]
map (\(x :: a
x,y :: a
y) -> (a -> a -> Map a a -> a
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault a
x a
x Map a a
nf,
a -> a -> Map a a -> a
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault a
y a
y Map a a
nf)) ([(a, a)] -> [(a, a)]) -> [(a, a)] -> [(a, a)]
forall a b. (a -> b) -> a -> b
\$
Relation a a -> [(a, a)]
forall a b. Relation a b -> [(a, b)]
Rel.toList Relation a a
r'
in Relation a a
r Relation a a -> Relation a a -> Relation a a
forall a b.
(Ord a, Ord b) =>
Relation a b -> Relation a b -> Relation a b
`Rel.union` Relation a a
r'')
Relation a a
forall a b. Relation a b
Rel.empty [(Int, Relation a a)]
rels

computeColimitRel :: (Ord a, SymbolName a) =>
Gr (Rel.Relation a a) (Int, Map.Map a a) ->
(Rel.Relation a a, Map.Map Node (Map.Map a a))
computeColimitRel :: Gr (Relation a a) (Int, Map a a)
-> (Relation a a, Map Int (Map a a))
computeColimitRel gr :: Gr (Relation a a) (Int, Map a a)
gr =
let grSet :: Gr (Set a) (Int, Map a a)
grSet = (Relation a a -> Set a)
-> Gr (Relation a a) (Int, Map a a) -> Gr (Set a) (Int, Map a a)
forall (gr :: * -> * -> *) a c b.
DynGraph gr =>
(a -> c) -> gr a b -> gr c b
nmap (\r :: Relation a a
r -> (Relation a a -> Set a
forall a b. Relation a b -> Set a
Rel.dom Relation a a
r) Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` (Relation a a -> Set a
forall a b. Relation a b -> Set b
Rel.ran Relation a a
r)) Gr (Relation a a) (Int, Map a a)
gr
(_cSet :: Set a
_cSet, nMaps :: Map Int (Map a a)
nMaps) = (Set (a, Int), Map Int (Map a (a, Int)))
-> (Set a, Map Int (Map a a))
forall a.
SymbolName a =>
(Set (a, Int), Map Int (Map a (a, Int)))
-> (Set a, Map Int (Map a a))
addIntToSymbols ((Set (a, Int), Map Int (Map a (a, Int)))
-> (Set a, Map Int (Map a a)))
-> (Set (a, Int), Map Int (Map a (a, Int)))
-> (Set a, Map Int (Map a a))
forall a b. (a -> b) -> a -> b
\$ Gr (Set a) (Int, Map a a)
-> (Set (a, Int), Map Int (Map a (a, Int)))
forall a.
Ord a =>
Gr (Set a) (Int, Map a a)
-> (Set (a, Int), Map Int (Map a (a, Int)))
computeColimitSet Gr (Set a) (Int, Map a a)
grSet
rel :: Relation a a
rel = [(Int, Relation a a)] -> Map Int (Map a a) -> Relation a a
forall a.
Ord a =>
[(Int, Relation a a)] -> Map Int (Map a a) -> Relation a a
colimitRel (Gr (Relation a a) (Int, Map a a) -> [(Int, Relation a a)]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode a]
labNodes Gr (Relation a a) (Int, Map a a)
gr) Map Int (Map a a)
nMaps
in (Relation a a
rel, Map Int (Map a a)
nMaps)
```