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

diff --git a/helm/ocaml/cic/cicUniv.ml b/helm/ocaml/cic/cicUniv.ml
index 0ea97404e..1ab577ec8 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
@@ -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)