X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic%2FcicUniv.ml;h=3074f2a78778143141bcb79dd516df2f69af1110;hb=987627a48b2a3c2345d1af2c2a6b1ab78aa90b58;hp=beb8a233fb58b3f56fb516131ca1b14188182bf0;hpb=c031aa4ca97d0d563a772d7bd247ff7814c51b04;p=helm.git

diff --git a/helm/software/components/cic/cicUniv.ml b/helm/software/components/cic/cicUniv.ml
index beb8a233f..3074f2a78 100644
--- a/helm/software/components/cic/cicUniv.ml
+++ b/helm/software/components/cic/cicUniv.ml
@@ -357,6 +357,8 @@ type universe_graph = bag * UriManager.UriSet.t * bool
 
 let empty_ugraph = empty_bag, UriManager.UriSet.empty, false
 let oblivion_ugraph = empty_bag, UriManager.UriSet.empty, true
+(* FG: default choice for a ugraph ??? *)
+let default_ugraph = oblivion_ugraph   
 
 let current_index_anon = ref (-1)
 let current_index_named = ref (-1)
@@ -474,8 +476,14 @@ let add_eq u v b =
 let rank = ref MAL.empty;;
 
 let do_rank (b,_,_) =
-(*         print_ugraph ugraph; *)
-   let keys = MAL.fold (fun k _ acc -> k::acc) b [] in
+   let keys = 
+     MAL.fold 
+       (fun k v acc -> 
+          SOF.union acc (SOF.union (SOF.singleton k) 
+            (SOF.union v.eq_closure (SOF.union v.gt_closure v.ge_closure))))
+       b SOF.empty 
+   in
+   let keys = SOF.elements keys in
    let fall =
      List.fold_left 
        (fun acc u ->
@@ -483,7 +491,6 @@ let do_rank (b,_,_) =
            | [] -> 0, seen
            | x::tl when SOF.mem x seen -> aux k seen tl
            | x::tl ->
-(*                prerr_endline (String.make k '.' ^ string_of_universe x); *)
                let seen = SOF.add x seen in
                let t1, seen = aux (k+1) seen (SOF.elements (repr x b).eq_closure) in
                let t3, seen = aux (k+1) seen (SOF.elements (repr x b).gt_closure) in
@@ -498,9 +505,13 @@ let do_rank (b,_,_) =
        MAL.empty
    in
    rank := fall keys;
+   let res = ref [] in
+   let resk = ref [] in
    MAL.iter 
      (fun k v -> 
-       prerr_endline (string_of_universe k ^ " = " ^ string_of_int v)) !rank
+       if not (List.mem v !res) then res := v::!res;
+       resk := k :: !resk) !rank;
+   !res, !resk
 ;;
 
 let get_rank u = 
@@ -630,7 +641,7 @@ let write_xml_of_ugraph filename (m,_,_) l =
 
 let univno = fst
 let univuri = function 
-  | _,None -> assert false
+  | _,None -> UriManager.uri_of_string "cic:/fake.con"
   | _,Some u -> u