From 9262517c80e17d46b9bf9931dc879ac653a633e9 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 18 Jan 2006 11:49:14 +0000 Subject: [PATCH] Universes speedup: 1) the merging is done thinking that the working graph is probably bigger than a cleaned ugraph 2) a cache of already merged ugraph is added. --- helm/ocaml/cic/cicUniv.ml | 72 ++++++++++++------- helm/ocaml/cic/cicUniv.mli | 3 +- .../cic_proof_checking/cicEnvironment.ml | 22 +++--- .../cic_proof_checking/cicTypeChecker.ml | 2 +- 4 files changed, 60 insertions(+), 39 deletions(-) diff --git a/helm/ocaml/cic/cicUniv.ml b/helm/ocaml/cic/cicUniv.ml index cfcbaf741..87839d8a3 100644 --- a/helm/ocaml/cic/cicUniv.ml +++ b/helm/ocaml/cic/cicUniv.ml @@ -413,7 +413,7 @@ let error arc node1 closure_type node2 closure = raise (UniverseInconsistency s) -let fill_empty_nodes_with_uri g l uri = +let fill_empty_nodes_with_uri (g, already_contained) l uri = let fill_empty_universe u = match u with (i,None) -> (i,Some uri) @@ -437,16 +437,17 @@ let fill_empty_nodes_with_uri g 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',l' + (m', already_contained),l' (*****************************************************************************) (** World interface **) (*****************************************************************************) -type universe_graph = bag +type universe_graph = bag * UriManager.UriSet.t +(* the graph , the cache of already merged ugraphs *) -let empty_ugraph = empty_bag +let empty_ugraph = empty_bag, UriManager.UriSet.empty let current_index_anon = ref (-1) let current_index_named = ref (-1) @@ -472,7 +473,7 @@ let name_universe u uri = | (i, None) -> (i, Some uri) | _ -> u -let print_ugraph g = +let print_ugraph (g, _) = prerr_endline (string_of_bag g) let add_eq ?(fast=(!fast_implementation)) u v b = @@ -531,34 +532,40 @@ let add_gt ?(fast=(!fast_implementation)) u v b = (** START: Decomment this for performance comparisons **) (*****************************************************************************) -let add_eq ?(fast=(!fast_implementation)) u v b = +let add_eq ?(fast=(!fast_implementation)) u v (b,already_contained) = + (*prerr_endline "add_eq";*) begin_spending (); let rc = add_eq ~fast u v b in end_spending(); - rc + rc,already_contained -let add_ge ?(fast=(!fast_implementation)) u v b = +let add_ge ?(fast=(!fast_implementation)) u v (b,already_contained) = +(* prerr_endline "add_ge"; *) begin_spending (); let rc = add_ge ~fast u v b in end_spending(); - rc + rc,already_contained -let add_gt ?(fast=(!fast_implementation)) u v b = +let add_gt ?(fast=(!fast_implementation)) u v (b,already_contained) = +(* prerr_endline "add_gt"; *) begin_spending (); let rc = add_gt ~fast u v b in end_spending(); - rc + rc,already_contained (*****************************************************************************) (** END: Decomment this for performance comparisons **) (*****************************************************************************) -let merge_ugraphs u v = +let merge_ugraphs ~base_ugraph ~increment:(increment, uri_of_increment) = (* this sucks *) - let merge_brutal u v = - if u = empty_bag then v - else if v = empty_bag then u + let merge_brutal (u,_) v = + if u = empty_bag then + ((*prerr_endline "HIT2";*)v) + else if fst v = empty_bag then + ((*prerr_endline "HIT3";*) u, snd v) else + ((*prerr_endline "MISS";*) let m1 = u in let m2 = v in MAL.fold ( @@ -575,10 +582,15 @@ let merge_ugraphs u v = 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 - merge_brutal v u - + let _, already_contained = base_ugraph in + if UriManager.UriSet.mem uri_of_increment already_contained then + ((*prerr_endline "HIT1";*) + base_ugraph) + else + fst (merge_brutal increment base_ugraph), + UriManager.UriSet.add uri_of_increment already_contained (*****************************************************************************) (** Xml sesialization and parsing **) @@ -631,7 +643,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"; @@ -645,7 +657,7 @@ let write_xml_of_ugraph filename m l = let univno = fst -let rec clean_ugraph m 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 -> @@ -665,11 +677,13 @@ let rec clean_ugraph m f = k::l end else l) m'' [] in if e_l != [] then - clean_ugraph m'' (fun u -> (f u) && not (List.mem u e_l)) + clean_ugraph + (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 + m'' MAL.empty, + already_contained let clean_ugraph g l = clean_ugraph g (fun u -> List.mem u l) @@ -729,7 +743,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, !result_list + (!result_map,UriManager.UriSet.empty), !result_list (*****************************************************************************) @@ -901,18 +915,24 @@ let recons_entry entry = one_s_gt = recons_set entry.one_s_gt; } -let recons_graph graph = +let recons_graph (graph,uriset) = MAL.fold (fun universe entry map -> MAL.add (recons_univ universe) (recons_entry entry) map) - graph MAL.empty + graph + MAL.empty, + UriManager.UriSet.fold + (fun u acc -> + UriManager.UriSet.add + (UriManager.uri_of_string (UriManager.string_of_uri u)) acc) + uriset UriManager.UriSet.empty let assert_univ u = match u with | (_,None) -> raise (UniverseInconsistency "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 diff --git a/helm/ocaml/cic/cicUniv.mli b/helm/ocaml/cic/cicUniv.mli index be8c28bf3..cdeaa378e 100644 --- a/helm/ocaml/cic/cicUniv.mli +++ b/helm/ocaml/cic/cicUniv.mli @@ -106,7 +106,8 @@ val fill_empty_nodes_with_uri: already merged graph) *) val merge_ugraphs: - universe_graph -> universe_graph -> universe_graph + base_ugraph:universe_graph -> + increment:(universe_graph * UriManager.uri) -> universe_graph (* ugraph to xml file and viceversa diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml index 22845725a..1f6789e76 100644 --- a/helm/ocaml/cic_proof_checking/cicEnvironment.ml +++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml @@ -452,17 +452,17 @@ let add_trusted_uri_to_cache uri = ;; (* get the uri, if we trust it will be added to the cacheOfCookedObjects *) -let get_cooked_obj_with_univlist ?(trust=true) base_univ uri = +let get_cooked_obj_with_univlist ?(trust=true) base_ugraph uri = try (* the object should be in the cacheOfCookedObjects *) let o,u,l = Cache.find_cooked uri in - o,(CicUniv.merge_ugraphs base_univ u),l + o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri)),l with Not_found -> (* this should be an error case, but if we trust the uri... *) if trust && trust_obj uri then (* trusting means that we will fetch cook it on the fly *) let o,u,l = add_trusted_uri_to_cache uri in - o,(CicUniv.merge_ugraphs base_univ u),l + o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri)),l else (* we don't trust the uri, so we fail *) begin @@ -470,8 +470,8 @@ let get_cooked_obj_with_univlist ?(trust=true) base_univ uri = raise Not_found end -let get_cooked_obj ?trust base_univ uri = - let o,g,_ = get_cooked_obj_with_univlist ?trust base_univ uri in +let get_cooked_obj ?trust base_ugraph uri = + let o,g,_ = get_cooked_obj_with_univlist ?trust base_ugraph uri in o,g (* This has not the old semantic :( but is what the name suggests @@ -488,16 +488,16 @@ let get_cooked_obj ?trust base_univ uri = * as the get_cooked_obj but returns a type_checked_obj * *) -let is_type_checked ?(trust=true) base_univ uri = +let is_type_checked ?(trust=true) base_ugraph uri = try let o,u,_ = Cache.find_cooked uri in - CheckedObj (o,(CicUniv.merge_ugraphs base_univ u)) + CheckedObj (o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri))) with Not_found -> (* this should return UncheckedObj *) if trust && trust_obj uri then (* trusting means that we will fetch cook it on the fly *) let o,u,_ = add_trusted_uri_to_cache uri in - CheckedObj ( o, CicUniv.merge_ugraphs u base_univ ) + CheckedObj ( o, CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri)) else let o,u,_ = find_or_add_to_unchecked uri in Cache.unchecked_to_frozen uri; @@ -507,15 +507,15 @@ let is_type_checked ?(trust=true) base_univ uri = (* as the get cooked, but if not present the object is only fetched, * not unfreezed and committed *) -let get_obj base_univ uri = +let get_obj base_ugraph uri = try (* the object should be in the cacheOfCookedObjects *) let o,u,_ = Cache.find_cooked uri in - o,(CicUniv.merge_ugraphs base_univ u) + o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri)) with Not_found -> (* this should be an error case, but if we trust the uri... *) let o,u,_ = find_or_add_to_unchecked uri in - o,(CicUniv.merge_ugraphs base_univ u) + o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri)) ;; let in_cache uri = diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml index a44c63469..951f68dbd 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml @@ -44,7 +44,7 @@ let debug t context = raise (TypeCheckerFailure (lazy (List.fold_right debug_aux (t::context) ""))) ;; -let debug_print = fun _ -> () ;; +let debug_print = fun _ -> ();; let rec split l n = match (l,n) with -- 2.39.2