X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic%2FcicUniv.ml;h=9bd7b9e74800c135082b545504cbc3304907464e;hb=42f2dc48b4fef5b404f406bf512d6a0cde35c067;hp=8ae118c9b1bb5ecf1d4c656ffcfb2bfb4ba15c86;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git diff --git a/components/cic/cicUniv.ml b/components/cic/cicUniv.ml index 8ae118c9b..9bd7b9e74 100644 --- a/components/cic/cicUniv.ml +++ b/components/cic/cicUniv.ml @@ -143,16 +143,18 @@ let partial = ref 0.0 ;; let reset_spent_time () = time_spent := 0.0;; let get_spent_time () = !time_spent ;; -let begin_spending () = +let begin_spending () = () (*assert (!partial = 0.0);*) - partial := Unix.gettimeofday () +(* partial := Unix.gettimeofday () *) ;; -let end_spending () = +let end_spending () = () +(* assert (!partial > 0.0); let interval = (Unix.gettimeofday ()) -. !partial in partial := 0.0; time_spent := !time_spent +. interval +*) ;; @@ -397,24 +399,26 @@ 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) -let fill_empty_nodes_with_uri (g, already_contained) l uri = +let fill_empty_nodes_with_uri (g, already_contained,o) l uri = let fill_empty_universe u = match u with (i,None) -> (i,Some uri) @@ -438,17 +442,18 @@ let fill_empty_nodes_with_uri (g, already_contained) l uri = MAL.add (fill_empty_universe k) (fill_empty_entry v) m) m MAL.empty in let l' = List.map fill_empty_universe l in - (m', already_contained),l' + (m', already_contained,o),l' (*****************************************************************************) (** World interface **) (*****************************************************************************) -type universe_graph = bag * UriManager.UriSet.t -(* the graph , the cache of already merged ugraphs *) +type universe_graph = bag * UriManager.UriSet.t * bool +(* the graph , the cache of already merged ugraphs, oblivion? *) -let empty_ugraph = empty_bag, UriManager.UriSet.empty +let empty_ugraph = empty_bag, UriManager.UriSet.empty, false +let oblivion_ugraph = empty_bag, UriManager.UriSet.empty, true let current_index_anon = ref (-1) let current_index_named = ref (-1) @@ -474,7 +479,8 @@ let name_universe u uri = | (i, None) -> (i, Some uri) | _ -> u -let print_ugraph (g, _) = +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 = @@ -533,27 +539,31 @@ 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) = +let add_eq ?(fast=(!fast_implementation)) u v (b,already_contained,oblivion) = + if oblivion then (b,already_contained,oblivion) else (*prerr_endline "add_eq";*) - begin_spending (); + (begin_spending (); let rc = add_eq ~fast u v b in end_spending (); - rc,already_contained + rc,already_contained,false) -let add_ge ?(fast=(!fast_implementation)) u v (b,already_contained) = +let add_ge ?(fast=(!fast_implementation)) u v (b,already_contained,oblivion) = + if oblivion then (b,already_contained,oblivion) else (* prerr_endline "add_ge"; *) - begin_spending (); + (begin_spending (); let rc = add_ge ~fast u v b in end_spending (); - rc,already_contained + rc,already_contained,false) -let add_gt ?(fast=(!fast_implementation)) u v (b,already_contained) = +let add_gt ?(fast=(!fast_implementation)) u v (b,already_contained,oblivion) = + if oblivion then (b,already_contained,oblivion) else (* prerr_endline "add_gt"; *) - begin_spending (); + (begin_spending (); let rc = add_gt ~fast u v b in end_spending (); - rc,already_contained + rc,already_contained,false) +(* 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,13 +573,17 @@ 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 **) (*****************************************************************************) -let merge_ugraphs ~base_ugraph ~increment:(increment, uri_of_increment) = - let merge_brutal (u,_) v = +(* TODO: uncomment l to gain a small speedup *) +let merge_ugraphs ~base_ugraph ~increment:(increment, uri_of_increment(*,l*)) = + let merge_brutal (u,a,_) v = +(* prerr_endline ("merging graph: "^UriManager.string_of_uri + * uri_of_increment); *) let m1 = u in let m2 = v in MAL.fold ( @@ -586,24 +600,36 @@ let merge_ugraphs ~base_ugraph ~increment:(increment, uri_of_increment) = fun u x -> let m = add_eq k u x in m) (SOF.union v.one_s_eq v.eq_closure) x))) - ) m1 m2 + ) m1 m2 in - let base, already_contained = base_ugraph in - if MAL.is_empty base then + let base, already_contained, oblivion = base_ugraph in + let inc,_,oblivion2 = increment in + if oblivion then + base_ugraph + else if oblivion2 then + increment + else if MAL.is_empty base then increment else if - MAL.is_empty (fst increment) || + MAL.is_empty inc || UriManager.UriSet.mem uri_of_increment already_contained then base_ugraph - else - fst (merge_brutal increment base_ugraph), - UriManager.UriSet.add uri_of_increment already_contained - -let profiler_merge = HExtlib.profile "CicUniv.merge_graphs" + else + (fun (x,_,_) -> x) (merge_brutal increment base_ugraph), +(* + List.fold_right UriManager.UriSet.add + (List.map (fun (_,x) -> HExtlib.unopt x) 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 +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 **) @@ -656,7 +682,7 @@ let xml_of_entry u e = let content = xml_of_entry_content e in ent content -let write_xml_of_ugraph filename (m,_) l = +let write_xml_of_ugraph filename (m,_,_) l = let tokens = [< Xml.xml_cdata "\n"; @@ -670,7 +696,7 @@ let write_xml_of_ugraph filename (m,_) l = let univno = fst -let rec clean_ugraph (m,already_contained) f = +let rec clean_ugraph m already_contained f = let m' = MAL.fold (fun k v x -> if (f k) then MAL.add k v x else x ) m MAL.empty in let m'' = MAL.fold (fun k v x -> @@ -691,15 +717,17 @@ let rec clean_ugraph (m,already_contained) f = in if 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 (List.mem u e_l)) else MAL.fold (fun k v x -> if v <> empty_entry then MAL.add k v x else x) m'' MAL.empty, already_contained -let clean_ugraph g l = - clean_ugraph g (fun u -> List.mem u l) +let clean_ugraph (m,a,o) l = + assert(not o); + let m, a = clean_ugraph m a (fun u -> List.mem u l) in + m, a, o let assigner_of = function @@ -756,7 +784,7 @@ let ugraph_and_univlist_of_xml filename = let xml_source = `Gzip_file filename in (try XPP.parse xml_parser xml_source with (XPP.Parse_error err) as exn -> raise exn); - (!result_map,UriManager.UriSet.empty), !result_list + (!result_map,UriManager.UriSet.empty,false), !result_list (*****************************************************************************) @@ -928,7 +956,7 @@ let recons_entry entry = one_s_gt = recons_set entry.one_s_gt; } -let recons_graph (graph,uriset) = +let recons_graph (graph,uriset,o) = MAL.fold (fun universe entry map -> MAL.add (recons_univ universe) (recons_entry entry) map) @@ -938,14 +966,15 @@ let recons_graph (graph,uriset) = (fun u acc -> UriManager.UriSet.add (UriManager.uri_of_string (UriManager.string_of_uri u)) acc) - uriset UriManager.UriSet.empty + uriset UriManager.UriSet.empty, o 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 = +let assert_univs_have_uri (graph,_,_) univlist = let assert_set s = SOF.iter (fun u -> assert_univ u) s in