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

diff --git a/helm/software/components/cic/cicUniv.ml b/helm/software/components/cic/cicUniv.ml
index 8570c0c15..a936c16bf 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