SetColimit.hs revision 90d7cac36f60438bd35124e3389b5bce6d114b46
{- |
Module : $Header$
Description : colimit of an arbitrary diagram in Set
Copyright : (c) Mihai Codescu, and Uni Bremen 2002-2006
License : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
Maintainer : mcodescu@informatik.uni-bremen.de
Stability : provisional
Portability : non-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
- the structural morphisms are factorizations
-}
module Common.SetColimit(
computeColimitSet
, updateComp
, initialDegrees
, updateDegrees
, orderByIncomingEdges
, EndoMap
)
where
import Common.Lib.Graph
import Data.Graph.Inductive.Graph
import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.List
import Logic.Logic(EndoMap)
--the colimit is initially the empty set
--and the functions from each nod to this set are defined as empty
initColimit :: Gr (Set.Set a) (Int, EndoMap a) ->
--each element of the sets is marked as visited or not
--initial marking of the elements of a set
--flag is set to false by default and it becomes true
--for the elements that are in the image of some set via some function
initialMarking gr = let nodeList = nodes gr
in Map.fromList $ zip nodeList $ map (markNode gr) nodeList
markNode gr n = case lab gr n of
Nothing -> Map.empty --shouldnt be the case
Just m -> Map.fromList $ zip (Set.elems m) (repeat False)
--mapping assigning to each node the number of incoming edges
--will be updated when choosing a node
initialDegrees :: Gr a b -> Map.Map Node Int
initialDegrees graph = let nodeList = nodes graph in
Map.fromList $ zip nodeList $ map (indeg graph) nodeList
computeColimitSet :: (Ord a) => Gr (Set.Set a) (Int, EndoMap a) ->
computeColimitSet graph =
if isEmpty graph then initColimit graph
else
let mark = initialMarking graph
(cset, cfct) = initColimit graph
incomEdges = initialDegrees graph
nodeList = orderedList graph incomEdges
in iterateNodes graph mark nodeList incomEdges cset cfct
--algorithm performed:
-- take the node of the graph with the least number of incoming edges
-- add its unmarked elements to the colimit and mark their images
-- update the incoming edges number for the node's succesors and
-- re-order the list according to updated function
iterateNodes :: (Ord a ) =>
Gr (Set.Set a) (Int, EndoMap a) ->
[Node]->
Map.Map Node Int ->
(Set.Set (a,Node)) ->
iterateNodes graph mark nodeList incomEdges cset cfct =
if nodeList == [] then (cset, cfct)
else let
hnode = head nodeList
(cset1, cfct1, mark1) = case lab graph hnode of
Nothing -> (cset, cfct, mark)
Just m -> addUnmarked (Set.elems m) hnode graph mark cset cfct
incomEdges1 = updateDegrees graph hnode incomEdges
newList = orderByIncomingEdges (tail nodeList) graph incomEdges1
in iterateNodes graph mark1 newList incomEdges1 cset1 cfct1
--decrease the number of incoming edges for all the successors of a node
updateDegrees graph hnode incomEdges = let
nList = suc graph hnode
insertFromList f list = case list of
[] -> f
x:xs -> let oldValue = (Map.!) f x
f1 = Map.insert x (oldValue-1) f
in insertFromList f1 xs
in insertFromList incomEdges nList
-- adds the equivalence classes of the elements of a set to the colimit
addUnmarked :: (Ord a) => [a] -> Node -> Gr (Set.Set a)(Int, EndoMap a)
-> ((Set.Set (a,Node)),
addUnmarked elemlist node graph mark cset cfct = case elemlist of
[] -> (cset, cfct, mark)
a:xs -> if (Map.!) ((Map.!) mark node) a then
addUnmarked xs node graph mark cset cfct
-- do not remove test, because the graph may have cycles
else let
(cset1, cfct1, mark1) = addClass (a,node) graph mark (cset,cfct)
in addUnmarked xs node graph mark1 cset1 cfct1
orderedList :: (Ord a) => Gr a b -> Map.Map Node Int -> [Node]
orderedList gr incomEdges = orderByIncomingEdges (nodes gr) gr incomEdges
orderByIncomingEdges :: [Node] -> Gr a b -> Map.Map Node Int -> [Node]
orderByIncomingEdges [] _ _ = []
orderByIncomingEdges (x:xs) gr incomEdges =
( orderByIncomingEdges
(filter (\z->((Map.!) incomEdges z) <= ((Map.!) incomEdges x))xs)
gr incomEdges) ++ [x] ++
( orderByIncomingEdges
(filter (\z->((Map.!) incomEdges z) > ((Map.!) incomEdges x))xs)
gr incomEdges)
--updates the value in a key
-- of a function assigned to a key by a higher order function
updateComp x1 y1 x f =
let fx = Map.insert x1 y1 ((Map.!) f x)
in Map.insert x fx f
markElem el node mark = updateComp el True node mark
-- adds recursively the elements of an equivalence class to the colimit
-- and builds the functions
addClass :: (Ord a) => (a,Node) -> Gr (Set.Set a) (Int, EndoMap a)
((Set.Set (a,Node)),
addClass (a,node) graph mark (cset,cfct) = let
cset1 = Set.insert (a, node) cset;--add a new element to the colimit
(cfct1, mark1) = equivClass [(a,node)] (a,node) graph cfct mark
--define the functions
in (cset1, cfct1, mark1)
--defines the functions
-- take the first element of the list
-- mark it as visited
-- add it to the function corresponding to its node
-- take the incoming edges and the outgoing edges
-- compute its preimage via the functions labeling the incoming edges
-- and its image via the functions labeling the outgoing edges
-- filter the already marked elements out (for preventing infinite loops)
-- and add them to the elements to be marked
equivClass :: (Ord a) => [(a,Node)] -> (a,Node) ->
equivClass elemList (a,node) graph cfct mark=
if elemList == [] then (cfct, mark)
else let
(h,nh) = head elemList
mark1 = markElem h nh mark
applyWithDefault f x = if x `elem` Map.keys f then (Map.!) f x else x
cfct1 = updateComp h (a,node) nh cfct
oEdges = lsuc graph nh
iEdges = lpre graph nh
preimage y nx label = case lab graph nx of
Nothing -> []
Just m -> filter (\x -> applyWithDefault label x == y) $ Set.elems m
intermValues = (map (\(ny, l) -> (applyWithDefault (snd l) h,ny)) oEdges)
++
(foldl (++) [] $
map (\(nx, l) -> map (\x -> (x,nx)) (preimage h nx $ snd l))
iEdges)
oValues = nub $ filter (\(x,nx) -> not $ (mark1 Map.! nx) Map.! x)
intermValues
newList = (tail elemList) ++ oValues
in equivClass newList (a,node) graph cfct1 mark1