X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic%2FcicUniv.ml;h=3d92f33358f1b76929027eb0366da95bea03d7ec;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=0ea97404ef66143494999401e91f55e18baf8a8a;hpb=68eea268e230d7eb12cdc416ead471a86a4bb5e4;p=helm.git

diff --git a/helm/ocaml/cic/cicUniv.ml b/helm/ocaml/cic/cicUniv.ml
index 0ea97404e..3d92f3335 100644
--- a/helm/ocaml/cic/cicUniv.ml
+++ b/helm/ocaml/cic/cicUniv.ml
@@ -38,7 +38,7 @@
 (** switch implementation                                                   **)
 (*****************************************************************************)
 
-let fast_implementation = ref false ;;
+let fast_implementation = ref true ;;
 
 (*****************************************************************************)
 (** open                                                                    **)
@@ -272,7 +272,7 @@ and add_ge_arc_fast u v m =
   let rv = repr v m' in
   let rv' = {rv with in_gegt_of = SOF.add u rv.in_gegt_of} in
   let m'' = MAL.add v rv' m' in
-    adjust_fast u m''
+  adjust_fast u m''
 
 and add_eq_arc_fast u v m =
   let ru = repr u m in
@@ -420,7 +420,7 @@ let fill_empty_nodes_with_uri g l uri =
   let fill_empty_set s =
     SOF.fold (fun e s -> SOF.add (fill_empty_universe e) s) s SOF.empty 
   in
-  let fill_empty_entry e = {
+  let fill_empty_entry e = { e with
     eq_closure = (fill_empty_set e.eq_closure) ;
     ge_closure = (fill_empty_set e.ge_closure) ;
     gt_closure = (fill_empty_set e.gt_closure) ;
@@ -465,6 +465,11 @@ let fresh ?uri ?id () =
   in
   (i,uri)
 
+let name_universe u uri =
+  match u with
+  | (i, None) -> (i, Some uri)
+  | _ -> u
+  
 let print_ugraph g = 
   prerr_endline (string_of_bag g)
 
@@ -558,16 +563,19 @@ let merge_ugraphs u v =
           fun k v x -> 
             (SOF.fold (
                fun u x -> 
-                 let m = add_gt k u x in m) v.one_s_gt 
+                 let m = add_gt k u x in m) 
+                  (SOF.union v.one_s_gt v.gt_closure)
                (SOF.fold (
                   fun u x -> 
-                    let m = add_ge k u x in m) v.one_s_ge
+                    let m = add_ge k u x in m) 
+                      (SOF.union v.one_s_ge v.ge_closure)
                   (SOF.fold (
-                     fun u x -> 
-                       let m = add_eq k u x in m) v.one_s_eq x)))
+                     fun u x ->
+                       let m = add_eq k u x in m) 
+                        (SOF.union v.one_s_eq v.eq_closure) x)))
         ) m1 m2
   in
-    merge_brutal u v
+  merge_brutal u v
 
 
 (*****************************************************************************)
@@ -650,12 +658,16 @@ let rec clean_ugraph m f =
     } in 
     MAL.add k v' x ) m' MAL.empty in
   let e_l = 
-    MAL.fold (fun k v l -> if v = empty_entry then k::l else l) m'' []
+    MAL.fold (fun k v l -> if v = empty_entry && not(f k) then
+      begin
+      k::l end else l) m'' []
   in
     if e_l != [] then
       clean_ugraph m'' (fun u -> (f u) && not (List.mem u e_l))
     else
-      m''
+      MAL.fold 
+        (fun k v x -> if v <> empty_entry then MAL.add k v x else x) 
+      m'' MAL.empty
 
 let clean_ugraph g l =
   clean_ugraph g (fun u -> List.mem u l)