positivity check fixed, a MutInd not applied (but with an exp-named-subst)

[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 fae784d369a9c59d295b72ba87907d66fdf395ff..d3ae5c960f5169531f952b43bcbf86d15d1b930d 100644 (file)
--- a/helm/software/components/cic/cicUniv.ml
+++ b/helm/software/components/cic/cicUniv.ml
@@ -227,7 +227,7 @@ and print_rec_status u ru =
   print_endline ("Aggiusto " ^ (string_of_universe u) ^ 
                  "e ottengo questa chiusura\n " ^ (string_of_node ru))
 
-and adjust_fast u m =
+and adjust_fast_aux u m =
   let ru = repr u m in
   let gt_c = closure_gt_fast ru m in
   let ge_c = closure_ge_fast ru m in
@@ -252,7 +252,7 @@ and adjust_fast u m =
         in
         let m = MAL.add u ru' m in
         let m =
-            SOF.fold (fun x m -> adjust_fast  x m) 
+            SOF.fold (fun x m -> adjust_fast_aux  x m) 
               (SOF.union ru'.eq_closure ru'.in_gegt_of) m
               (* TESI: 
                    ru'.in_gegt_of m 
@@ -260,9 +260,16 @@ and adjust_fast u m =
         in
           m (*adjust_fast  u m*)
       end
+
+(*
+and profiler_adj = HExtlib.profile "CicUniv.adjust_fast"
+and adjust_fast x y = profiler_adj.HExtlib.profile (adjust_fast_aux x) y
+*)
+and adjust_fast x y = adjust_fast_aux x y
         
 and add_gt_arc_fast u v m =
   let ru = repr u m in
+  if SOF.mem v ru.gt_closure then m else
   let ru' = {ru with one_s_gt = SOF.add v ru.one_s_gt} in
   let m' = MAL.add u ru' m in
   let rv = repr v m' in
@@ -272,6 +279,7 @@ and add_gt_arc_fast u v m =
       
 and add_ge_arc_fast u v m =
   let ru = repr u m in
+  if SOF.mem v ru.ge_closure then m else
   let ru' = { ru with one_s_ge = SOF.add v ru.one_s_ge} in
   let m' = MAL.add u ru' m in
   let rv = repr v m' in
@@ -281,6 +289,7 @@ and add_ge_arc_fast u v m =
 
 and add_eq_arc_fast u v m =
   let ru = repr u m in
+  if SOF.mem v ru.eq_closure then m else
   let rv = repr v m in 
   let ru' = {ru  with one_s_eq = SOF.add v ru.one_s_eq} in
   (*TESI: let ru' = {ru' with in_gegt_of = SOF.add v ru.in_gegt_of} in *)
@@ -477,7 +486,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
@@ -563,7 +579,7 @@ let add_gt ?(fast=(!fast_implementation)) u v (b,already_contained,oblivion) =
   end_spending ();
     rc,already_contained,false)
     
-(* profiling code
+(* profiling code 
 let profiler_eq = HExtlib.profile "CicUniv.add_eq"
 let profiler_ge = HExtlib.profile "CicUniv.add_ge"
 let profiler_gt = HExtlib.profile "CicUniv.add_gt"
@@ -575,6 +591,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                         **)
 (*****************************************************************************)
@@ -582,7 +637,8 @@ let add_eq ?fast u v b =
 (* TODO: uncomment l to gain a small speedup *)
 let merge_ugraphs ~base_ugraph ~increment:(increment, uri_of_increment(*,l*)) =
   let merge_brutal (u,a,_) v = 
-    prerr_endline (UriManager.string_of_uri uri_of_increment);
+(*     prerr_endline ("merging graph: "^UriManager.string_of_uri
+ *     uri_of_increment); *)
     let m1 = u in 
     let m2 = v in 
       MAL.fold (
@@ -623,7 +679,7 @@ let merge_ugraphs ~base_ugraph ~increment:(increment, uri_of_increment(*,l*)) =
     (UriManager.UriSet.add uri_of_increment already_contained), false
 
 (* profiling code; WARNING: the time spent during profiling can be
-   greater than the profiled time
+   greater than the profiled time 
 let profiler_merge = HExtlib.profile "CicUniv.merge_ugraphs"
 let merge_ugraphs ~base_ugraph ~increment =
   profiler_merge.HExtlib.profile 
@@ -1006,5 +1062,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 *)