X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic%2FcicUniv.ml;h=58dc5cd6cfc82af8641150ba34168d5281716f4a;hb=2e58d03db0222ac0d885abeaebceac07ac586761;hp=a936c16bf9fb688e399cb5e30c63fe6813323644;hpb=18758ebe381286b4aff2232e837a0256c00b400b;p=helm.git

diff --git a/helm/software/components/cic/cicUniv.ml b/helm/software/components/cic/cicUniv.ml
index a936c16bf..58dc5cd6c 100644
--- a/helm/software/components/cic/cicUniv.ml
+++ b/helm/software/components/cic/cicUniv.ml
@@ -317,7 +317,7 @@ let error arc node1 closure_type node2 closure =
      "   of\n" ^ 
      "\t" ^ (string_of_universe node2) ^ "\n\n" ^
      "  ===== Universe Inconsistency detected =====\n") in
-  prerr_endline (Lazy.force s);
+(*   prerr_endline (Lazy.force s); *)
   raise (UniverseInconsistency s)
 
 
@@ -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)
@@ -380,14 +382,7 @@ let fresh ?uri ?id () =
 let name_universe u uri =
   match u with
   | (i, None) -> (i, Some uri)
-  | (i, Some ouri) when UriManager.eq ouri uri -> u
-  | (i, Some ouri) ->
-      (* inside obj living at uri 'uri' should live only
-       * universes with uri None. Call Unshare.unshare ~fresh_univs:true
-       * if you want to reuse a Type in another object *)
-      prerr_endline ("Offending universe: " ^ string_of_universe u^
-        " found inside object " ^ UriManager.string_of_uri  uri);
-      assert false
+  | u -> u
 ;;
   
 let print_ugraph (g, _, o) = 
@@ -481,33 +476,38 @@ 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 fall =
-     List.fold_left 
-       (fun acc u ->
-         let rec aux k seen = function
-           | [] -> 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
-               let t2, seen = aux (k+1) seen (SOF.elements (repr x b).ge_closure) in
-               let t4, seen = aux k seen tl in
-               max (max t1 t2) 
-                 (max (if SOF.is_empty (repr x b).gt_closure then 0 else t3+1) t4),
-               seen 
-         in
-         let rank, _ = aux 0 SOF.empty [u] in
-         MAL.add u rank acc) 
-       MAL.empty
+   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
-   rank := fall keys;
+   let keys = SOF.elements keys in
+   let rec aux cache l =
+      match l with
+      | [] -> -1,cache
+      | x::tl when List.mem_assoc x cache ->
+          let height = List.assoc x cache in
+          let rest, cache = aux cache tl in
+          max rest height, cache
+      | x::tl -> 
+          let sons = SOF.elements (repr x b).gt_closure in
+          let height,cache = aux cache sons in
+          let height = height + 1 in
+          let cache = (x,height) :: cache in
+          let rest, cache = aux cache tl in
+          max height rest, cache
+   in
+   let _, cache = aux [] keys in
+   rank := List.fold_left (fun m (k,v) -> MAL.add k v m) MAL.empty cache;
+   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 = 
@@ -636,6 +636,9 @@ let write_xml_of_ugraph filename (m,_,_) l =
     Xml.pp ~gzip:true tokens (Some filename)
 
 let univno = fst
+let univuri = function 
+  | _,None -> UriManager.uri_of_string "cic:/fake.con"
+  | _,Some u -> u
 
  
 let rec clean_ugraph m already_contained f =