From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 23 Sep 2005 13:57:57 +0000 (+0000)
Subject: several "INSERT VALUE" ==> "INSERT VALUES" (more efficient)
X-Git-Tag: LAST_BEFORE_NEW~31
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a18be43f8f1cdde43b5b2c79c2c8968c11d4804f;p=helm.git

several "INSERT VALUE" ==> "INSERT VALUES" (more efficient)
---

diff --git a/helm/ocaml/metadata/metadataDb.ml b/helm/ocaml/metadata/metadataDb.ml
index 84e8fad71..2fdfb49fd 100644
--- a/helm/ocaml/metadata/metadataDb.ml
+++ b/helm/ocaml/metadata/metadataDb.ml
@@ -95,73 +95,38 @@ let count_distinct position l =
         | `Obj (name,_) -> MetadataConstraints.UriManagerSet.add name acc
         | _ -> acc)
     ) MetadataConstraints.UriManagerSet.empty l)
-(*    
-let insert_const_no dbd uri =
-  let term = CicUtil.term_of_uri uri in 
-  let ty = CicTypeChecker.type_of_aux' 
-  let inconcl_no =
-    sprintf "INSERT %s SELECT \"%s\", COUNT(DISTINCT h_occurrence) FROM %s WHERE (h_position=\"%s\" OR h_position=\"%s\") AND source LIKE \"%s%%\""
-      (conclno_tbl ()) uri (obj_tbl ()) inconcl_pos mainconcl_pos uri
-  in
-  let concl_hyp =
-    sprintf "INSERT %s
-        SELECT \"%s\",COUNT(DISTINCT h_occurrence)
-        FROM %s
-        WHERE NOT (h_position=\"%s\") AND (source = \"%s\")"
-      (fullno_tbl ()) uri (obj_tbl ()) inbody_pos uri
-  in
-  ignore (Mysql.exec dbd inconcl_no);
-  ignore (Mysql.exec dbd concl_hyp)
-*)
-let insert_const_no dbd (uri,metadata) =
-  let no_concl = count_distinct `Conclusion metadata in
-  let no_hyp = count_distinct `Hypothesis metadata in
-  let no_full = count_distinct `Statement metadata in
-  let insert = 
-    sprintf "INSERT INTO %s VALUES (\"%s\", %d, %d, %d)" 
-      (count_tbl ()) (UriManager.string_of_uri uri) no_concl no_hyp no_full
-  in
+
+let insert_const_no ~dbd l =
+ let data =
+  List.fold_left
+   (fun acc (uri,_,metadata) -> 
+     let no_concl = count_distinct `Conclusion metadata in
+     let no_hyp = count_distinct `Hypothesis metadata in
+     let no_full = count_distinct `Statement metadata in
+      (sprintf "(\"%s\", %d, %d, %d)" 
+       (UriManager.string_of_uri uri) no_concl no_hyp no_full) :: acc
+   ) [] l in
+ let insert =
+  sprintf "INSERT INTO %s VALUES %s" (count_tbl ()) (String.concat "," data)
+ in
   ignore (Mysql.exec dbd insert)
   
-let insert_name ~dbd ~uri ~name =
-  let query =
-    sprintf "INSERT %s VALUES (\"%s\", \"%s\")" (name_tbl ()) (UriManager.string_of_uri uri) name
-  in
-  ignore (Mysql.exec dbd query)
+let insert_name ~dbd l =
+ let data =
+  List.fold_left
+   (fun acc (uri,name,_) -> 
+      (sprintf "(\"%s\", \"%s\")" (UriManager.string_of_uri uri) name) :: acc
+   ) [] l in
+ let insert =
+  sprintf "INSERT INTO %s VALUES %s" (name_tbl ()) (String.concat "," data)
+ in
+  ignore (Mysql.exec dbd insert)
 
 type columns =
   MetadataPp.t list list * MetadataPp.t list list * MetadataPp.t list list
 
   (* TODO ZACK: verify if an object has already been indexed *)
 let already_indexed _ = false
-(*
-let index_constant ~dbd =
-  let query = prepare_insert () in
-  fun ~uri ~body ~ty  ->
-    if not (already_indexed uri) then beginrel_tbl ()
-      let name = UriManager.name_of_uri uri in
-      let uri = UriManager.string_of_uri uri in
-      let metadata = MetadataExtractor.compute ~body ~ty in
-      let columns = MetadataPp.columns_of_metadata ~about:uri metadata in
-      execute_insert dbd query uri (columns :> columns);
-      insert_const_no dbd uri;
-      insert_name ~dbd ~uri ~name
-    end
-
-let index_inductive_def ~dbd =
-  let query = prepare_insert () in
-  fun ~uri ~types ->
-    if not (already_indexed uri) then begin
-      let metadata = MetadataExtractor.compute_obj uri in
-      let uri_of (a,b,c) = a in
-      let uris = UriManager.string_of_uri uri :: List.map uri_of metadata in
-      let uri = UriManager.string_of_uri uri in
-      let columns = MetadataPp.columns_of_ind_metadata metadata in
-      execute_insert dbd query uri (columns :> columns);
-      List.iter (insert_const_no dbd) uris;
-      List.iter (fun (uri, name, _) -> insert_name ~dbd ~uri ~name) metadata
-    end
-*)
 
 (***** TENTATIVE HACK FOR THE DB SLOWDOWN - BEGIN *******)
 let analyze_index = ref 0
@@ -177,16 +142,27 @@ let eventually_analyze dbd =
   
 (***** TENTATIVE HACK FOR THE DB SLOWDOWN - END *******)
 
+let profile = (CicUtil.profile "foo").CicUtil.profile
+let profile2 = (CicUtil.profile "foo2").CicUtil.profile
+let profile3 = (CicUtil.profile "foo3").CicUtil.profile
+
 let index_obj ~dbd ~uri = 
   if not (already_indexed uri) then begin
+let foo () =
     eventually_analyze dbd;
-    let metadata = MetadataExtractor.compute_obj uri in
-    let uri_of (a,b,c) = (a,c) in
+in profile3 foo ();
+    let metadata =
+let foo () =
+MetadataExtractor.compute_obj uri in
+profile2 foo () in
     let uri = UriManager.string_of_uri uri in
-    let columns = MetadataPp.columns_of_metadata metadata in
+    let columns =
+MetadataPp.columns_of_metadata metadata in
+let foo () =
     execute_insert dbd uri (columns :> columns);
-    List.iter (insert_const_no dbd) (List.map uri_of metadata);
-    List.iter (fun (uri, name, _) -> insert_name ~dbd ~uri ~name) metadata
+    insert_const_no ~dbd metadata;
+    insert_name ~dbd metadata
+in profile foo ()
   end