checked in new version of matita from svn

[helm.git] / helm / ocaml / metadata / metadataDb.ml

diff --git a/helm/ocaml/metadata/metadataDb.ml b/helm/ocaml/metadata/metadataDb.ml
index 441609a1ddd4d0423afd6f8dc4cb70e2c5b0180c..6cbfeb1ff12e3a47d464d02da468c2d428258538 100644 (file)
--- a/helm/ocaml/metadata/metadataDb.ml
+++ b/helm/ocaml/metadata/metadataDb.ml
@@ -28,9 +28,11 @@ open MetadataTypes
 open Printf
 
 let prepare_insert () =
+  (*
   let insert_owner a b =
     sprintf "INSERT %s VALUES (\"%s\", \"%s\")" (owners_tbl ())a b
   in
+  *)
   let insert_sort  a b c d =
     sprintf "INSERT %s VALUES (\"%s\", \"%s\", %d, \"%s\")" (sort_tbl ())a b c d
   in
@@ -40,12 +42,12 @@ let prepare_insert () =
   let insert_obj a b c d =
     sprintf "INSERT %s VALUES (\"%s\", \"%s\", \"%s\", %s)" (obj_tbl ()) a b c d
   in
-  (insert_owner, insert_sort, insert_rel, insert_obj)
+  ((*insert_owner, *)insert_sort, insert_rel, insert_obj)
 
-let execute_insert dbd (insert_owner, insert_sort, insert_rel, insert_obj)
-  uri owner (sort_cols, rel_cols, obj_cols)
+let execute_insert dbd ((*insert_owner, *)insert_sort, insert_rel, insert_obj)
+  uri (sort_cols, rel_cols, obj_cols)
 =
-  ignore (Mysql.exec dbd (insert_owner uri owner));
+  (* ignore (Mysql.exec dbd (insert_owner uri owner)); *)
   List.iter (function
       | [`String a; `String b; `Int c; `String d] ->
           ignore (Mysql.exec dbd (insert_sort a b c d))
@@ -74,7 +76,7 @@ let insert_const_no dbd uri =
         SELECT \"%s\",COUNT(DISTINCT h_occurrence)
         FROM %s
         WHERE NOT (h_position=\"%s\") AND (source = \"%s\")"
-      (conclno_hyp_tbl ()) uri (obj_tbl ()) inbody_pos uri
+      (fullno_tbl ()) uri (obj_tbl ()) inbody_pos uri
   in
   ignore (Mysql.exec dbd inconcl_no);
   ignore (Mysql.exec dbd concl_hyp)
@@ -88,39 +90,49 @@ let insert_name ~dbd ~uri ~name =
 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 ~owner ~uri ~body ~ty  ->
-    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 owner (columns :> columns);
-    insert_const_no dbd uri;
-    insert_name ~dbd ~uri ~name
+  fun ~uri ~body ~ty  ->
+    if not (already_indexed uri) then begin
+      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 ~owner ~uri ~types ->
-    let metadata = MetadataExtractor.compute_ind ~uri ~types 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 owner (columns :> columns);
-    List.iter (insert_const_no dbd) uris;
-    List.iter (fun (uri, name, _) -> insert_name ~dbd ~uri ~name) metadata
+  fun ~uri ~types ->
+    if not (already_indexed uri) then begin
+      let metadata = MetadataExtractor.compute_ind ~uri ~types 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
+
+let tables_to_clean =
+  [sort_tbl; rel_tbl; obj_tbl; conclno_tbl; fullno_tbl; name_tbl; hypno_tbl]
 
-let clean ~(dbd:Mysql.dbd) ~owner =
+let clean ~(dbd:Mysql.dbd) =
   let owned_uris =  (* list of uris in list-of-columns format *)
-    let query =
-      sprintf "SELECT source FROM %s WHERE owner = \"%s\"" (owners_tbl ()) owner
-    in
+    let query = sprintf "SELECT source FROM %s" (obj_tbl ()) in
     let result = Mysql.exec dbd query in
-    Mysql.map result (fun cols ->
+    let uris = Mysql.map result (fun cols ->
       match cols.(0) with
       | Some src -> src
-      | None -> assert false)
+      | None -> assert false) in
+    (* and now some stuff to remove #xpointers and duplicates *)
+    uris
   in
   let del_from tbl =
     let query s = 
@@ -130,8 +142,16 @@ let clean ~(dbd:Mysql.dbd) ~owner =
       (fun source_col -> ignore (Mysql.exec dbd (query source_col)))
       owned_uris
   in
-  List.iter del_from
-    [sort_tbl; rel_tbl; obj_tbl; conclno_tbl; conclno_hyp_tbl; name_tbl;
-    owners_tbl];
-  List.iter Http_getter.unregister owned_uris  
+  List.iter del_from tables_to_clean;
+  owned_uris
+
+let unindex ~dbd ~uri =
+  let uri = UriManager.string_of_uri uri in
+  let del_from tbl =
+    let query tbl =
+      sprintf "DELETE FROM %s WHERE source LIKE \"%s%%\"" (tbl ()) uri
+    in
+    ignore (Mysql.exec dbd (query tbl))
+  in
+  List.iter del_from tables_to_clean