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

diff --git a/helm/software/components/cic/cicUniv.ml b/helm/software/components/cic/cicUniv.ml
index 25f70bc0f..3074f2a78 100644
--- a/helm/software/components/cic/cicUniv.ml
+++ b/helm/software/components/cic/cicUniv.ml
@@ -46,6 +46,7 @@ open Printf
 (** Types and default values                                                **)
 (*****************************************************************************)
 
+
 type universe = int * UriManager.uri option 
 
 let eq u1 u2 = 
@@ -216,7 +217,9 @@ 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_aux u m =
+and adjust_fast_aux adjusted u m =
+  if SOF.mem u adjusted then m, adjusted else
+  let adjusted = SOF.add u adjusted in
   let ru = repr u m in
   let gt_c = closure_gt_fast ru m in
   let ge_c = closure_ge_fast ru m in
@@ -227,7 +230,7 @@ and adjust_fast_aux u m =
     (not (are_set_eq ge_c ru.ge_closure))
   in
     if ((not changed_gegt) &&  (not changed_eq)) then
-      m
+      m, adjusted
     else
       begin
         let ru' = {
@@ -240,21 +243,25 @@ and adjust_fast_aux u m =
           one_s_gt = ru.one_s_gt}
         in
         let m = MAL.add u ru' m in
-        let 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 
-              *)
+        let m, adjusted  =
+          SOF.fold (fun x (m,adjusted) -> MAL.add x ru' m, SOF.add x adjusted) 
+            (SOF.diff ru'.eq_closure adjusted) 
+            (m,adjusted)
+        in
+        let m, adjusted  =
+            SOF.fold (fun x (m,adjusted) -> adjust_fast_aux adjusted x m) 
+              (SOF.diff ru'.in_gegt_of adjusted) 
+              (m,adjusted)
         in
-          m (*adjust_fast  u m*)
+          m, adjusted 
       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 adjust_fast x y = 
+  fst(adjust_fast_aux SOF.empty x y)
         
 and add_gt_arc_fast u v m =
   let ru = repr u m in
@@ -350,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)
@@ -373,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) = 
@@ -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 = 
@@ -629,6 +640,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 =
@@ -648,11 +662,11 @@ let rec clean_ugraph m already_contained f =
   let e_l = 
     MAL.fold (fun k v l -> if v = empty_entry && not(f k) then
       begin
-      k::l end else l) m'' []
+      SOF.add k l end else l) m'' SOF.empty
   in
-    if e_l != [] then
+    if not (SOF.is_empty e_l) then
       clean_ugraph 
-        m'' already_contained (fun u -> (f u) && not (List.mem u e_l))
+        m'' already_contained (fun u -> (f u) && not (SOF.mem u e_l))
     else
       MAL.fold 
         (fun k v x -> if v <> empty_entry then MAL.add k v x else x) 
@@ -661,7 +675,8 @@ let rec clean_ugraph m already_contained f =
 
 let clean_ugraph (m,a,o) l =
   assert(not o);
-  let m, a = clean_ugraph m a (fun u -> List.mem u l) in
+  let l = List.fold_right SOF.add l SOF.empty in
+  let m, a = clean_ugraph m a (fun u -> SOF.mem u l) in
   m, a, o
 
 let assigner_of =