FIXED bug, added assertion in case a universe inside a term T living at URI u

was marked with URI v <> u. Unshare.fresh_types should be called!

added a function to linearize a given graph, imperative interface since
is is used only in the new kernel.

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 *)

diff --git a/helm/software/components/cic/cicUniv.mli b/helm/software/components/cic/cicUniv.mli
index 7a4331905b50ea95689302c90135011e5649ec5d..fd501df8c47c4adfa320d90151ebc07b47c89e74 100644 (file)
--- a/helm/software/components/cic/cicUniv.mli
+++ b/helm/software/components/cic/cicUniv.mli
@@ -72,6 +72,9 @@ val add_ge:
 val add_gt: 
   ?fast:bool -> universe -> universe -> universe_graph -> universe_graph
 
+val do_rank: universe_graph -> unit
+val get_rank: universe -> int
+
 (*
   debug function to print the graph to standard error
 *)
@@ -155,3 +158,4 @@ val eq: universe -> universe -> bool
 val get_spent_time: unit -> float
 val reset_spent_time: unit -> unit
 
+val is_anon: universe -> bool