added depndency of new kernel to metadata to allow to use the DB to calculate the...

[helm.git] / helm / software / components / cic / cicUniv.ml

diff --git a/helm/software/components/cic/cicUniv.ml b/helm/software/components/cic/cicUniv.ml
index 9bd7b9e74800c135082b545504cbc3304907464e..fd0f696d90834118d62eabb7ad9791a9945b5d88 100644 (file)
--- a/helm/software/components/cic/cicUniv.ml
+++ b/helm/software/components/cic/cicUniv.ml
@@ -477,7 +477,14 @@ let fresh ?uri ?id () =
 let name_universe u uri =
   match u with
   | (i, None) -> (i, Some 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
+;;
   
 let print_ugraph (g, _, o) = 
   if o then prerr_endline "oblivion universe" else
@@ -575,6 +582,45 @@ let add_eq ?fast u v b =
   profiler_eq.HExtlib.profile (fun _ -> add_eq ?fast u v b) ()
 *)
 
+(* ugly *)
+let rank = ref MAL.empty;;
+
+let do_rank (b,_,_) =
+  
+   let keys = MAL.fold (fun k _ acc -> k::acc) b [] in
+   let fall =
+     List.fold_left 
+       (fun acc u ->
+         let rec aux seen = function
+           | [] -> 0, seen
+           | x::tl when SOF.mem x seen -> aux seen tl
+           | x::tl ->
+               let seen = SOF.add x seen in
+               let t1, seen = aux seen (SOF.elements (repr x b).one_s_eq) in
+               let t2, seen = aux seen (SOF.elements (repr x b).one_s_ge) in
+               let t3, seen = aux seen (SOF.elements (repr x b).one_s_gt) in
+               let t4, seen = aux seen tl in
+               max (max t1 t2) 
+                 (max (if SOF.is_empty (repr x b).one_s_gt then 0 else t3+1) t4),
+               seen 
+         in
+         let rank, _ = aux SOF.empty [u] in
+         MAL.add u rank acc) 
+       MAL.empty
+   in
+   rank := fall keys;
+   MAL.iter 
+     (fun k v -> 
+       prerr_endline (string_of_universe k ^ " = " ^ string_of_int v)) !rank
+;;
+
+let get_rank u = 
+  try MAL.find u !rank 
+  with Not_found -> 0 
+  (* if the universe is not in the graph it means there are 
+   * no contraints on it! thus it can be freely set to Type0 *)
+;;
+
 (*****************************************************************************)
 (** END: Decomment this for performance comparisons                         **)
 (*****************************************************************************)
@@ -1007,5 +1053,7 @@ let compare (id1, uri1) (id2, uri2) =
     | Some uri1, Some uri2 -> UriManager.compare uri1 uri2
   else
     cmp
+
+let is_anon = function (_,None) -> true | _ -> false
   
 (* EOF *)