hets/Common/SetColimit.hs

	SetColimit.hs revision c7e03d0708369f944b6f235057b39142a21599f2
2b873214c9ab511bbca437c036371ab664aedaceChristian Maeder{- |
f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian MaederModule      :  $Header$
c63ebf815c8a874525cf18670ad74847f7fc7b26Christian MaederDescription :  colimit of an arbitrary diagram in Set
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian MaederCopyright   :  (c) Mihai Codescu, and Uni Bremen 2002-2006
54ed6a6b1a6c7d27fadb39ec5b59d0806c81f7c8Christian MaederLicense     :  similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
75a6279dbae159d018ef812185416cf6df386c10Till MossakowskiMaintainer  :  mcodescu@informatik.uni-bremen.de
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederStability   :  provisional
75a6279dbae159d018ef812185416cf6df386c10Till MossakowskiPortability :  non-portable
75a6279dbae159d018ef812185416cf6df386c10Till Mossakowski
f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian MaederComputes the colimit of an arbitrary diagram in Set:
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maeder  - the set is the disjoint union of all sets in the diagram
dda5ab793f1615c1ba1dcaa97a4346b0878da6b1Christian Maeder    (which we obtain by pairing elements with the node number)
f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maeder    factored by the equivalence generated by the pairs (x, f_i(x)),
f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maeder    with i an arrow in the diagram
da955132262baab309a50fdffe228c9efe68251dCui Jian  - the structural morphisms are factorizations
dda5ab793f1615c1ba1dcaa97a4346b0878da6b1Christian Maeder-}
dda5ab793f1615c1ba1dcaa97a4346b0878da6b1Christian Maeder
f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maedermodule Common.SetColimit(
f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maeder              computeColimitSet
0799b5dc3f06d2640e66e9ab54b8b217348fd719Christian Maeder            , updateComp
0799b5dc3f06d2640e66e9ab54b8b217348fd719Christian Maeder            , initialDegrees
52d922076b89f12234f721974e82531bc69a6f69Christian Maeder            , updateDegrees
52d922076b89f12234f721974e82531bc69a6f69Christian Maeder            , orderByIncomingEdges
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder            , EndoMap
4c8d3c5a9e938633f6147b5a595b9b93bfca99e6Christian Maeder    )
fbc4f8708092d571a45cb483f37cc6b674da45a7Christian Maeder where
fbc4f8708092d571a45cb483f37cc6b674da45a7Christian Maeder
fbc4f8708092d571a45cb483f37cc6b674da45a7Christian Maederimport Common.Lib.Graph
14c89b2d830777bf4db2850f038c9f60acaca486Christian Maederimport Data.Graph.Inductive.Graph
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowskiimport qualified Data.Map as Map
f77f29e84b3f6e791c82e61b13fbf76582bedd2fChristian Maederimport qualified Data.Set as Set
dda5ab793f1615c1ba1dcaa97a4346b0878da6b1Christian Maederimport Data.List
9175e29c044318498a40f323f189f9dfd50378efChristian Maederimport Logic.Logic(EndoMap)
f77f29e84b3f6e791c82e61b13fbf76582bedd2fChristian Maeder
f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maeder--the colimit is initially the empty set
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder--and the functions from each nod to this set are defined as empty
da333ffa6336cf59a4071fcddad358c5eafd3e61Sonja Gröning
c0c2380bced8159ff0297ece14eba948bd236471Christian MaederinitColimit :: Gr (Set.Set a) (Int, EndoMap a) ->
6352f3c31da3043783a13be6594aacb2147378baRazvan Pascanu               ((Set.Set (a,Node)), Map.Map Node (Map.Map a (a,Node)))
8ef91a173e69219fc2ebd45c76a35891c7785abdMarkus GrossinitColimit gr = (Set.empty, Map.fromList $ zip (nodes gr) (repeat Map.empty))
fc1a590cd3ee36797c0a032ff41e07f8e2469341Christian Maeder
a2b04db3e156312a8596d8084f7f0f51acf8a96bChristian Maeder--each element of the sets is marked as visited or not
0c885f1348fd58f7cb706472a3ff20b52dbef0a7Jonathan von Schroeder
fc1a590cd3ee36797c0a032ff41e07f8e2469341Christian Maeder--initial marking of the elements of a set
66a774f13272fde036481edd2298081ab3d04678Razvan Pascanu--flag is set to false by default and it becomes true
834c2e71b8e390e5b05c8d02bb6eb22621125133Markus Gross--for the elements that are in the image of some set via some function
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederinitialMarking :: (Ord a) => Gr (Set.Set a) b -> Map.Map Node (Map.Map a Bool)
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederinitialMarking gr = let nodeList = nodes gr
6e52f1dfc0da4bc4a7701cf856641c9dce08fc7dChristian Maeder                    in Map.fromList $ zip nodeList $ map (markNode gr) nodeList
923e25bb8c7cf9f2978c7844ad173704482cc3b0Martin Kühl
9f85afecbd79b3df5a0bb17bd28cd0b288dc3213Kristina SojakovamarkNode :: (Ord a) => Gr (Set.Set a) b -> Node -> Map.Map a Bool
63da71bfb4226f504944b293fb77177ebcaea7d4Ewaryst SchulzmarkNode gr n = case lab gr n of
e1ea9a046e9640148ca876dfe47e391559a9fdf3Christian Maeder  Nothing -> Map.empty --shouldnt be the case
14c89b2d830777bf4db2850f038c9f60acaca486Christian Maeder  Just m -> Map.fromList $ zip (Set.elems m) (repeat False)
57026bc09337d158b89775048a9bcc9c17d825caChristian Maeder
57026bc09337d158b89775048a9bcc9c17d825caChristian Maeder--mapping assigning to each node the number of incoming edges
57026bc09337d158b89775048a9bcc9c17d825caChristian Maeder--will be updated when choosing a node
9175e29c044318498a40f323f189f9dfd50378efChristian MaederinitialDegrees :: Gr a b -> Map.Map Node Int
e1ea9a046e9640148ca876dfe47e391559a9fdf3Christian MaederinitialDegrees graph = let nodeList = nodes graph in
923e25bb8c7cf9f2978c7844ad173704482cc3b0Martin Kühl  Map.fromList $ zip nodeList $ map (indeg graph) nodeList
f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maeder
2b873214c9ab511bbca437c036371ab664aedaceChristian MaedercomputeColimitSet :: (Ord a) =>  Gr (Set.Set a) (Int, EndoMap a) ->
52d922076b89f12234f721974e82531bc69a6f69Christian Maeder                     ((Set.Set (a, Node)), Map.Map Node (Map.Map a (a,Node)))
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaedercomputeColimitSet graph =
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder  if isEmpty graph then initColimit graph
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder  else
52d922076b89f12234f721974e82531bc69a6f69Christian Maeder   let  mark = initialMarking graph
8ef91a173e69219fc2ebd45c76a35891c7785abdMarkus Gross        (cset, cfct) = initColimit graph
8ef91a173e69219fc2ebd45c76a35891c7785abdMarkus Gross        incomEdges = initialDegrees graph
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder        nodeList = orderedList graph incomEdges
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder   in iterateNodes  graph mark nodeList incomEdges cset cfct
52d922076b89f12234f721974e82531bc69a6f69Christian Maeder
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder--algorithm performed:
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder-- take the node of the graph with the least number of incoming edges
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder-- add its unmarked elements to the colimit and mark their images
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder-- update the incoming edges number for the node's succesors and
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder-- re-order the list according to updated function
9175e29c044318498a40f323f189f9dfd50378efChristian MaederiterateNodes :: (Ord a ) =>
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder                Gr (Set.Set a) (Int, EndoMap a) ->
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder                Map.Map Node (Map.Map a Bool) ->
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder                [Node]->
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder                Map.Map Node Int ->
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder                (Set.Set (a,Node)) ->
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder                Map.Map Node (Map.Map a (a,Node))
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder                -> ((Set.Set (a,Node)), Map.Map Node (Map.Map a (a,Node)))
9175e29c044318498a40f323f189f9dfd50378efChristian MaederiterateNodes graph mark nodeList incomEdges cset cfct =
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder if nodeList == [] then (cset, cfct)
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder else let
ee1c7c5796832536932d7b06cbfb1ca13f9a0d7bMartin Kühl  hnode = head nodeList
ee1c7c5796832536932d7b06cbfb1ca13f9a0d7bMartin Kühl  (cset1, cfct1, mark1) = case lab graph hnode of
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder     Nothing -> (cset, cfct, mark)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder     Just m -> addUnmarked (Set.elems m) hnode graph mark cset cfct
52d922076b89f12234f721974e82531bc69a6f69Christian Maeder  incomEdges1 = updateDegrees graph hnode incomEdges
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder  newList = orderByIncomingEdges (tail nodeList) graph incomEdges1
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder in iterateNodes  graph mark1 newList incomEdges1 cset1 cfct1
bdc103981a28a51938de98a956d8a3767f6cf43dAivaras Jakubauskas
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder--decrease the number of incoming edges for all the successors of a node
e1ea9a046e9640148ca876dfe47e391559a9fdf3Christian MaederupdateDegrees :: Gr a b -> Node -> Map.Map Node Int -> Map.Map Node Int
e1ea9a046e9640148ca876dfe47e391559a9fdf3Christian MaederupdateDegrees graph hnode incomEdges = let
57026bc09337d158b89775048a9bcc9c17d825caChristian Maeder  nList = suc graph hnode
57026bc09337d158b89775048a9bcc9c17d825caChristian Maeder  insertFromList f list = case list of
22b772f8753f0cdb4508ba460356c238de2ee375Jonathan von Schroeder    [] -> f
7bbfb15142ab4286dfc6fcde2fc94a5512297e41Jonathan von Schroeder    x:xs -> let oldValue = (Map.!) f x
fa388aea9cef5f9734fec346159899a74432ce26Christian Maeder                f1 = Map.insert x (oldValue-1) f
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder            in insertFromList f1 xs
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder in insertFromList incomEdges nList
0c885f1348fd58f7cb706472a3ff20b52dbef0a7Jonathan von Schroeder
52d922076b89f12234f721974e82531bc69a6f69Christian Maeder-- adds the equivalence classes of the elements of a set to the colimit
52d922076b89f12234f721974e82531bc69a6f69Christian MaederaddUnmarked :: (Ord a) => [a] -> Node -> Gr (Set.Set a)(Int, EndoMap a)
923e25bb8c7cf9f2978c7844ad173704482cc3b0Martin Kühl -> Map.Map Node (Map.Map a Bool) -> (Set.Set (a,Node))
9f85afecbd79b3df5a0bb17bd28cd0b288dc3213Kristina Sojakova ->  Map.Map Node (Map.Map a (a,Node))
72079df98b3cb7cc1fd82a0a24984893dcd05ecaEwaryst Schulz -> ((Set.Set (a,Node)),
a461314c811f4187dff85c8be079a41b2f13f176Christian Maeder     Map.Map Node (Map.Map a (a,Node)),
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder     Map.Map Node (Map.Map a Bool))
fbc4f8708092d571a45cb483f37cc6b674da45a7Christian MaederaddUnmarked  elemlist node graph mark cset cfct = case elemlist of
8a77240a809197c92c0736c431b4b88947a7bac1Christian Maeder  [] -> (cset, cfct, mark)
8a77240a809197c92c0736c431b4b88947a7bac1Christian Maeder  a:xs -> if (Map.!) ((Map.!) mark node) a then
fbc4f8708092d571a45cb483f37cc6b674da45a7Christian Maeder            addUnmarked xs node graph mark cset cfct
bb63f684c4f5f33ffcd1dcc02c58d6a703900fafJonathan von Schroeder          -- do not remove test, because the graph may have cycles
b0234f0a84fcd3587073fbc11d38759108997c3cChristian Maeder          else let
b0234f0a84fcd3587073fbc11d38759108997c3cChristian Maeder     (cset1, cfct1, mark1) = addClass (a,node) graph mark (cset,cfct)
8ef91a173e69219fc2ebd45c76a35891c7785abdMarkus Gross               in addUnmarked xs node graph mark1 cset1 cfct1
8ef91a173e69219fc2ebd45c76a35891c7785abdMarkus Gross
d56ece59c372cb887355825901222b9f3377f7e6Thiemo WiedemeyerorderedList :: (Ord a) => Gr a b -> Map.Map Node Int -> [Node]
d56ece59c372cb887355825901222b9f3377f7e6Thiemo WiedemeyerorderedList gr incomEdges = orderByIncomingEdges (nodes gr) gr incomEdges
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder
9175e29c044318498a40f323f189f9dfd50378efChristian MaederorderByIncomingEdges :: [Node] -> Gr a b -> Map.Map Node Int -> [Node]
f1dec6898638ba1131a9fadbc4d1544c93dfabb0Klaus LuettichorderByIncomingEdges [] _ _ = []
9175e29c044318498a40f323f189f9dfd50378efChristian MaederorderByIncomingEdges (x:xs) gr incomEdges =
f77f29e84b3f6e791c82e61b13fbf76582bedd2fChristian Maeder ( 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 :: (Ord a, Ord c) => a -> b -> c -> Map.Map c (Map.Map a b)
  -> Map.Map c (Map.Map a b)
updateComp x1 y1 x f =
  let fx = Map.insert x1 y1 ((Map.!) f x)
  in Map.insert x fx f

markElem :: (Ord a) => a -> Node -> Map.Map Node (Map.Map a Bool)
  -> Map.Map Node (Map.Map a Bool)
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)
  ->  Map.Map Node (Map.Map a Bool) ->
  ((Set.Set (a,Node)), Map.Map Node (Map.Map a (a,Node))) ->
  ((Set.Set (a,Node)),
   Map.Map Node(Map.Map a (a,Node)),
   Map.Map Node (Map.Map a Bool) )
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) ->
 Gr (Set.Set a) (Int, EndoMap a) -> Map.Map Node(Map.Map a (a,Node))->
 Map.Map Node (Map.Map a Bool) ->
 (Map.Map Node(Map.Map a (a,Node)),Map.Map Node (Map.Map a Bool) )
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