X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic%2FcicUniv.ml;h=d48772c27a40a0bea41d14eeb0e55de644fb1976;hb=81ef66d9ad4cf863a770664190f96653e9777a57;hp=8ae118c9b1bb5ecf1d4c656ffcfb2bfb4ba15c86;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git

diff --git a/helm/software/components/cic/cicUniv.ml b/helm/software/components/cic/cicUniv.ml
index 8ae118c9b..d48772c27 100644
--- a/helm/software/components/cic/cicUniv.ml
+++ b/helm/software/components/cic/cicUniv.ml
@@ -397,20 +397,22 @@ let add_gt fast u v b =
 (** Other real code                                                         **)
 (*****************************************************************************)
 
-exception UniverseInconsistency of string 
+exception UniverseInconsistency of string Lazy.t
 
 let error arc node1 closure_type node2 closure =
-  let s = "\n  ===== Universe Inconsistency detected =====\n\n" ^
-   "   Unable to add\n" ^ 
-   "\t" ^ (string_of_arc arc) ^ "\n" ^
-   "   cause\n" ^ 
-   "\t" ^ (string_of_universe node1) ^ "\n" ^
-   "   is in the " ^ closure_type ^ " closure\n" ^
-   "\t{" ^ (string_of_universe_set closure) ^ "}\n" ^ 
-   "   of\n" ^ 
-   "\t" ^ (string_of_universe node2) ^ "\n\n" ^
-   "  ===== Universe Inconsistency detected =====\n" in
-  prerr_endline s;
+  let s =
+   lazy
+    ("\n  ===== Universe Inconsistency detected =====\n\n" ^
+     "   Unable to add\n" ^ 
+     "\t" ^ (string_of_arc arc) ^ "\n" ^
+     "   cause\n" ^ 
+     "\t" ^ (string_of_universe node1) ^ "\n" ^
+     "   is in the " ^ closure_type ^ " closure\n" ^
+     "\t{" ^ (string_of_universe_set closure) ^ "}\n" ^ 
+     "   of\n" ^ 
+     "\t" ^ (string_of_universe node2) ^ "\n\n" ^
+     "  ===== Universe Inconsistency detected =====\n") in
+  prerr_endline (Lazy.force s);
   raise (UniverseInconsistency s)
 
 
@@ -554,6 +556,7 @@ let add_gt ?(fast=(!fast_implementation)) u v (b,already_contained) =
   end_spending ();
     rc,already_contained
     
+(* 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"
@@ -563,6 +566,7 @@ 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) ()
+*)
 
 (*****************************************************************************)
 (** END: Decomment this for performance comparisons                         **)
@@ -600,10 +604,13 @@ let merge_ugraphs ~base_ugraph ~increment:(increment, uri_of_increment) =
     fst (merge_brutal increment base_ugraph), 
     UriManager.UriSet.add uri_of_increment already_contained
 
-let profiler_merge = HExtlib.profile "CicUniv.merge_graphs"
+(* profiling code; WARNING: the time spent during profiling can be
+   greater than the profiled time
+let profiler_merge = HExtlib.profile "CicUniv.merge_ugraphs"
 let merge_ugraphs ~base_ugraph ~increment =
   profiler_merge.HExtlib.profile 
   (fun _ -> merge_ugraphs ~base_ugraph ~increment) ()
+*)
 
 (*****************************************************************************)
 (** Xml sesialization and parsing                                           **)
@@ -942,7 +949,8 @@ let recons_graph (graph,uriset) =
 
 let assert_univ u =
     match u with 
-    | (_,None) -> raise (UniverseInconsistency "This universe graph has a hole")
+    | (_,None) ->
+       raise (UniverseInconsistency (lazy "This universe graph has a hole"))
     | _ -> ()
     
 let assert_univs_have_uri (graph,_) univlist =