X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic%2FcicUniv.ml;h=fe9f01d532af2c65866fb1b9a34d6cf223ed76dd;hb=0805c61933df87f5cfae63b94456a1f0518b06d0;hp=699af7847a029b05345ef2c49817561ca92a6e59;hpb=ca1359de73c1c9deda30c9aaff2606b8dd5253bc;p=helm.git

diff --git a/helm/software/components/cic/cicUniv.ml b/helm/software/components/cic/cicUniv.ml
index 699af7847..fe9f01d53 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                                                                    **)
 (*****************************************************************************)
@@ -56,7 +50,15 @@ type universe = int * UriManager.uri option
     
 module UniverseType = struct
   type t = universe
-  let compare = Pervasives.compare
+  let compare (n1,u1) (n2,u2) =
+   let ndiff = n1 - n2 in
+    if ndiff <> 0 then ndiff
+    else
+     match u1,u2 with
+        None, None -> 0
+      | Some u1, Some u2 -> UriManager.compare u1 u2
+      | None, Some _ -> 1
+      | Some _, None -> -1
 end
   
 module SOF = Set.Make(UniverseType)
@@ -135,29 +137,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                                                                 **)
 (*****************************************************************************)
@@ -301,108 +280,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                                                         **)
@@ -500,7 +377,7 @@ 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
@@ -512,19 +389,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 
@@ -548,7 +425,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*)
 
@@ -556,65 +433,57 @@ 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,_,_) =
-  
+(*         print_ugraph ugraph; *)
    let keys = MAL.fold (fun k _ acc -> k::acc) b [] 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 ->
+(*                prerr_endline (String.make k '.' ^ string_of_universe x); *)
                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