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

diff --git a/helm/software/components/cic/cicUniv.ml b/helm/software/components/cic/cicUniv.ml
index fd0f696d9..3074f2a78 100644
--- a/helm/software/components/cic/cicUniv.ml
+++ b/helm/software/components/cic/cicUniv.ml
@@ -36,12 +36,6 @@
 
 (* $Id$ *)
 
-(*****************************************************************************)
-(** switch implementation                                                   **)
-(*****************************************************************************)
-
-let fast_implementation = ref true ;;
-
 (*****************************************************************************)
 (** open                                                                    **)
 (*****************************************************************************)
@@ -52,11 +46,30 @@ open Printf
 (** Types and default values                                                **)
 (*****************************************************************************)
 
+
 type universe = int * UriManager.uri option 
-    
+
+let eq u1 u2 = 
+  match u1,u2 with
+  | (id1, Some uri1),(id2, Some uri2) -> 
+      id1 = id2 && UriManager.eq uri1 uri2
+  | (id1, None),(id2, None) -> id1 = id2
+  | _ -> false
+  
+let compare (id1, uri1) (id2, uri2) = 
+  let cmp = id1 - id2 in
+  if cmp = 0 then
+    match uri1,uri2 with
+    | None, None -> 0 
+    | Some _, None -> 1
+    | None, Some _ -> ~-1
+    | Some uri1, Some uri2 -> UriManager.compare uri1 uri2
+  else
+    cmp
+
 module UniverseType = struct
   type t = universe
-  let compare = Pervasives.compare
+  let compare = compare
 end
   
 module SOF = Set.Make(UniverseType)
@@ -135,29 +148,6 @@ let string_of_mal m =
 let string_of_bag b = 
   string_of_mal b
 
-(*****************************************************************************)
-(** Benchmarking                                                            **)
-(*****************************************************************************)
-let time_spent = ref 0.0;;
-let partial = ref 0.0 ;;
-
-let reset_spent_time () = time_spent := 0.0;;
-let get_spent_time () = !time_spent ;;
-let begin_spending () = ()
-  (*assert (!partial = 0.0);*)
-(*   partial := Unix.gettimeofday () *)
-;;
-
-let end_spending () = ()
-(*
-  assert (!partial > 0.0);
-  let interval = (Unix.gettimeofday ()) -. !partial in
-    partial := 0.0;
-    time_spent := !time_spent +. interval
-*)
-;;
-
-
 (*****************************************************************************)
 (** Helpers                                                                 **)
 (*****************************************************************************)
@@ -227,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 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
@@ -238,7 +230,7 @@ and adjust_fast 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' = {
@@ -251,18 +243,29 @@ and adjust_fast 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  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 = 
+  fst(adjust_fast_aux SOF.empty 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 +275,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 +285,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 *)
@@ -292,108 +297,6 @@ and add_eq_arc_fast u v m =
 ;;
 
 
-(*****************************************************************************)
-(** safe implementation                                                     **)
-(*****************************************************************************)
-
-let closure_of u m =
-  let ru = repr u m in
-  let eq_c =
-    let j = ru.one_s_eq in
-    let _Uj = merge_closures (fun x -> x.eq_closure) j m in
-    let one_step_eq = ru.one_s_eq in
-            (SOF.union one_step_eq _Uj)
-  in
-  let ge_c = 
-    let j = SOF.union ru.one_s_ge (SOF.union ru.one_s_gt ru.one_s_eq) in
-    let _Uj = merge_closures (fun x -> x.ge_closure) j m in
-    let _Ux = j in
-      (SOF.union _Uj _Ux)
-  in
-  let gt_c =
-    let j = ru.one_s_gt in
-    let k = ru.one_s_ge in
-    let l = ru.one_s_eq in
-    let _Uj = merge_closures (fun x -> x.ge_closure) j m in
-    let _Uk = merge_closures (fun x -> x.gt_closure) k m in
-    let _Ul = merge_closures (fun x -> x.gt_closure) l m in
-    let one_step_gt = ru.one_s_gt in
-      (SOF.union (SOF.union (SOF.union _Ul one_step_gt) _Uk) _Uj)
-  in
-    {
-      eq_closure = eq_c;
-      ge_closure = ge_c;
-      gt_closure = gt_c;
-      in_gegt_of = ru.in_gegt_of;
-      one_s_eq = ru.one_s_eq;
-      one_s_ge = ru.one_s_ge;
-      one_s_gt = ru.one_s_gt
-    }
-
-let rec simple_adjust m =
-  let m' = 
-    MAL.mapi (fun x _ -> closure_of x m) m
-  in
-    if not (are_ugraph_eq m  m') then(
-      simple_adjust m')
-    else
-      m'
-
-let add_eq_arc u v m =
-  let ru = repr u m in
-  let rv = repr v m in
-  let ru' = {ru with one_s_eq = SOF.add v ru.one_s_eq} in
-  let m' = MAL.add u ru' m in
-  let rv' = {rv with one_s_eq = SOF.add u rv.one_s_eq} in
-  let m'' = MAL.add v rv' m' in
-    simple_adjust m''
-
-let add_ge_arc u v m =
-  let ru = repr u m in
-  let ru' = { ru with one_s_ge = SOF.add v ru.one_s_ge} in
-  let m' = MAL.add u ru' m in
-    simple_adjust m'
-
-let add_gt_arc u v m =
-  let ru = repr u m in
-  let ru' = {ru with one_s_gt = SOF.add v ru.one_s_gt} in
-  let m' = MAL.add u ru' m in
-    simple_adjust m'
-
-
-(*****************************************************************************)
-(** Outhern interface, that chooses between _fast and safe                  **)
-(*****************************************************************************)
-
-(*                                                                            
-    given the 2 nodes plus the current bag, adds the arc, recomputes the 
-    closures and returns the new map
-*) 
-let add_eq fast u v b =
-  if fast then
-    add_eq_arc_fast u v b
-  else
-    add_eq_arc u v b
-
-(*                                                                            
-    given the 2 nodes plus the current bag, adds the arc, recomputes the 
-    closures and returns the new map
-*) 
-let add_ge fast u v b =
-  if fast then
-    add_ge_arc_fast u v b
-  else
-    add_ge_arc u v b
-(*                                                                            
-    given the 2 nodes plus the current bag, adds the arc, recomputes the 
-    closures and returns the new map
-*)                                                                            
-let add_gt fast u v b =
-  if fast then
-    add_gt_arc_fast u v b
-  else
-    add_gt_arc u v b
-
 
 (*****************************************************************************)
 (** Other real code                                                         **)
@@ -454,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)
@@ -477,20 +382,14 @@ let fresh ?uri ?id () =
 let name_universe u uri =
   match u with
   | (i, None) -> (i, Some uri)
-  | (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) = 
   if o then prerr_endline "oblivion universe" else
   prerr_endline (string_of_bag g)
 
-let add_eq ?(fast=(!fast_implementation)) u v b =
+let add_eq u v b =
   (* should we check to no add twice the same?? *)
   let m = b in
   let ru = repr u m in
@@ -502,19 +401,19 @@ let add_eq ?(fast=(!fast_implementation)) u v b =
     if SOF.mem u rv.gt_closure then
       error ("EQ",u,v) u "GT" v rv.gt_closure
     else
-      add_eq fast u v b
+      add_eq_arc_fast u v b
     end
 
-let add_ge ?(fast=(!fast_implementation)) u v b =
+let add_ge u v b =
   (* should we check to no add twice the same?? *)
   let m = b in
   let rv = repr v m in
   if SOF.mem u rv.gt_closure then
     error ("GE",u,v) u "GT" v rv.gt_closure
   else
-    add_ge fast u v b
+    add_ge_arc_fast u v b
   
-let add_gt ?(fast=(!fast_implementation)) u v b =
+let add_gt u v b =
   (* should we check to no add twice the same?? *)
   (* 
      FIXME : check the thesis... no need to check GT and EQ closure since the 
@@ -538,7 +437,7 @@ let add_gt ?(fast=(!fast_implementation)) u v b =
           if SOF.mem u rv.eq_closure then
             error ("GT",u,v) u "EQ" v rv.eq_closure
           else*)
-            add_gt fast u v b
+            add_gt_arc_fast u v b
 (*        end
     end*)
 
@@ -546,72 +445,73 @@ let add_gt ?(fast=(!fast_implementation)) u v b =
 (** START: Decomment this for performance comparisons                       **)
 (*****************************************************************************)
 
-let add_eq ?(fast=(!fast_implementation))  u v (b,already_contained,oblivion) =
+let add_eq u v (b,already_contained,oblivion) =
         if oblivion then (b,already_contained,oblivion) else
-  (*prerr_endline "add_eq";*)
-  (begin_spending ();
-  let rc = add_eq ~fast u v b in
-  end_spending ();
-    rc,already_contained,false)
+  let rc = add_eq u v b in
+    rc,already_contained,false
 
-let add_ge ?(fast=(!fast_implementation)) u v (b,already_contained,oblivion) =
+let add_ge u v (b,already_contained,oblivion) =
         if oblivion then (b,already_contained,oblivion) else
-(*   prerr_endline "add_ge"; *)
-  (begin_spending ();
-  let rc = add_ge ~fast u v b in
-  end_spending ();
-    rc,already_contained,false)
+  let rc = add_ge u v b in
+    rc,already_contained,false
     
-let add_gt ?(fast=(!fast_implementation)) u v (b,already_contained,oblivion) =
+let add_gt u v (b,already_contained,oblivion) =
         if oblivion then (b,already_contained,oblivion) else
-(*   prerr_endline "add_gt"; *)
-  (begin_spending ();
-  let rc = add_gt ~fast u v b in
-  end_spending ();
-    rc,already_contained,false)
+  let rc = add_gt u v b in
+    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"
-let add_gt ?fast u v b = 
-  profiler_gt.HExtlib.profile (fun _ -> add_gt ?fast u v b) ()
-let add_ge ?fast u v b = 
-  profiler_ge.HExtlib.profile (fun _ -> add_ge ?fast u v b) ()
-let add_eq ?fast u v b = 
-  profiler_eq.HExtlib.profile (fun _ -> add_eq ?fast u v b) ()
-*)
+let add_gt u v b = 
+  profiler_gt.HExtlib.profile (fun _ -> add_gt u v b) ()
+let add_ge u v b = 
+  profiler_ge.HExtlib.profile (fun _ -> add_ge u v b) ()
+let add_eq u v b = 
+  profiler_eq.HExtlib.profile (fun _ -> add_eq 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 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 ->
-         let rec aux seen = function
+         let rec aux k seen = function
            | [] -> 0, seen
-           | x::tl when SOF.mem x seen -> aux seen tl
+           | x::tl when SOF.mem x seen -> aux k 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
+               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
+               let t2, seen = aux (k+1) seen (SOF.elements (repr x b).ge_closure) in
+               let t4, seen = aux k seen tl in
                max (max t1 t2) 
-                 (max (if SOF.is_empty (repr x b).one_s_gt then 0 else t3+1) t4),
+                 (max (if SOF.is_empty (repr x b).gt_closure then 0 else t3+1) t4),
                seen 
          in
-         let rank, _ = aux SOF.empty [u] in
+         let rank, _ = aux 0 SOF.empty [u] in
          MAL.add u rank acc) 
        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 = 
@@ -670,7 +570,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 
@@ -740,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 =
@@ -759,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) 
@@ -772,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 = 
@@ -1036,24 +940,6 @@ let assert_univs_have_uri (graph,_,_) univlist =
   MAL.iter (fun k v -> assert_univ k; assert_entry v)graph;
   List.iter assert_univ univlist
   
-let eq u1 u2 = 
-  match u1,u2 with
-  | (id1, Some uri1),(id2, Some uri2) -> 
-      id1 = id2 && UriManager.eq uri1 uri2
-  | (id1, None),(id2, None) -> id1 = id2
-  | _ -> false
-  
-let compare (id1, uri1) (id2, uri2) = 
-  let cmp = id1 - id2 in
-  if cmp = 0 then
-    match uri1,uri2 with
-    | None, None -> 0 
-    | Some _, None -> 1
-    | None, Some _ -> ~-1
-    | Some uri1, Some uri2 -> UriManager.compare uri1 uri2
-  else
-    cmp
-
 let is_anon = function (_,None) -> true | _ -> false
   
 (* EOF *)