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.

diff --git a/helm/ocaml/cic/cicUniv.ml b/helm/ocaml/cic/cicUniv.ml
index cfcbaf74178d2a2839d64b4bfede2e52abee19e3..87839d8a39d12ae18c4e7524dfae26ca7e7951e0 100644 (file)
--- 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 "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\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
 
 \f
 (*****************************************************************************)
@@ -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 be8c28bf3e105c20ac17a6673ae5fa6ecbd637e0..cdeaa378ea9bc78e5d0994e9ea1ae5d15430d92f 100644 (file)
--- 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 22845725ac05e983aec69d23bc133bd5265e2274..1f6789e76895156311b0cc7470f89fb1b8fb7813 100644 (file)
--- 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 a44c63469916549214738b1620eeba27eaf380ae..951f68dbd84b28043a100fe3c72c114d4f5927a7 100644 (file)
--- 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