]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/metadata/metadataDb.ml
changed default parameter values...
[helm.git] / helm / ocaml / metadata / metadataDb.ml
index e20e000023e87b8f96a58a9ac629d63fc7e6e2b0..84e8fad7147e6331b6683081c1f9a3ce4a4a2f8a 100644 (file)
@@ -74,27 +74,27 @@ let execute_insert dbd uri (sort_cols, rel_cols, obj_cols) =
   
     
 let count_distinct position l =
-  MetadataConstraints.StringSet.cardinal
+  MetadataConstraints.UriManagerSet.cardinal
   (List.fold_left (fun acc d -> 
     match position with
     | `Conclusion -> 
          (match d with
          | `Obj (name,`InConclusion) 
          | `Obj (name,`MainConclusion _ ) -> 
-             MetadataConstraints.StringSet.add name acc
+             MetadataConstraints.UriManagerSet.add name acc
          | _ -> acc)
     | `Hypothesis ->
         (match d with
         | `Obj (name,`InHypothesis) 
         | `Obj (name,`MainHypothesis _) -> 
-            MetadataConstraints.StringSet.add name acc
+            MetadataConstraints.UriManagerSet.add name acc
         | _ -> acc)
     | `Statement ->
         (match d with
         | `Obj (name,`InBody) -> acc
-        | `Obj (name,_) -> MetadataConstraints.StringSet.add name acc
+        | `Obj (name,_) -> MetadataConstraints.UriManagerSet.add name acc
         | _ -> acc)
-    ) MetadataConstraints.StringSet.empty l)
+    ) MetadataConstraints.UriManagerSet.empty l)
 (*    
 let insert_const_no dbd uri =
   let term = CicUtil.term_of_uri uri in 
@@ -119,13 +119,13 @@ let insert_const_no dbd (uri,metadata) =
   let no_full = count_distinct `Statement metadata in
   let insert = 
     sprintf "INSERT INTO %s VALUES (\"%s\", %d, %d, %d)" 
-      (count_tbl ()) uri no_concl no_hyp no_full
+      (count_tbl ()) (UriManager.string_of_uri uri) no_concl no_hyp no_full
   in
   ignore (Mysql.exec dbd insert)
   
 let insert_name ~dbd ~uri ~name =
   let query =
-    sprintf "INSERT %s VALUES (\"%s\", \"%s\")" (name_tbl ()) uri name
+    sprintf "INSERT %s VALUES (\"%s\", \"%s\")" (name_tbl ()) (UriManager.string_of_uri uri) name
   in
   ignore (Mysql.exec dbd query)
 
@@ -138,7 +138,7 @@ let already_indexed _ = false
 let index_constant ~dbd =
   let query = prepare_insert () in
   fun ~uri ~body ~ty  ->
-    if not (already_indexed uri) then begin
+    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
@@ -162,8 +162,24 @@ let index_inductive_def ~dbd =
       List.iter (fun (uri, name, _) -> insert_name ~dbd ~uri ~name) metadata
     end
 *)
+
+(***** TENTATIVE HACK FOR THE DB SLOWDOWN - BEGIN *******)
+let analyze_index = ref 0
+let eventually_analyze dbd =
+  incr analyze_index;
+  if !analyze_index > 30 then
+    begin
+      let analyze t = "OPTIMIZE TABLE " ^ t ^ ";" in
+      List.iter 
+        (fun table -> ignore (Mysql.exec dbd (analyze table)))
+        [name_tbl (); rel_tbl (); sort_tbl (); obj_tbl(); count_tbl()]
+    end
+  
+(***** TENTATIVE HACK FOR THE DB SLOWDOWN - END *******)
+
 let index_obj ~dbd ~uri = 
   if not (already_indexed uri) then begin
+    eventually_analyze dbd;
     let metadata = MetadataExtractor.compute_obj uri in
     let uri_of (a,b,c) = (a,c) in
     let uri = UriManager.string_of_uri uri in
@@ -175,12 +191,11 @@ let index_obj ~dbd ~uri =
   
 
 let tables_to_clean =
-  [sort_tbl; rel_tbl; obj_tbl; (*conclno_tbl; fullno_tbl; hypno_tbl;*) name_tbl;
-  count_tbl]
+  [sort_tbl; rel_tbl; obj_tbl; name_tbl; count_tbl]
 
 let clean ~(dbd:Mysql.dbd) =
   let owned_uris =  (* list of uris in list-of-columns format *)
-    let query = sprintf "SELECT source FROM %s" (obj_tbl ()) in
+    let query = sprintf "SELECT source FROM %s" (name_tbl ()) in
     let result = Mysql.exec dbd query in
     let uris = Mysql.map result (fun cols ->
       match cols.(0) with