From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 4 Feb 2005 09:15:10 +0000 (+0000)
Subject: - clean no longer unregister URIs from the getter, but returns them
X-Git-Tag: V_0_1_0~37
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c66e9d17eda5e5defcb363e42d891d2b407cf7c3;p=helm.git

- clean no longer unregister URIs from the getter, but returns them
- removed owner table handling
---

diff --git a/helm/ocaml/metadata/metadataDb.ml b/helm/ocaml/metadata/metadataDb.ml
index c56a1a027..170d02d77 100644
--- a/helm/ocaml/metadata/metadataDb.ml
+++ b/helm/ocaml/metadata/metadataDb.ml
@@ -45,7 +45,7 @@ let prepare_insert () =
   ((*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)
+  uri (sort_cols, rel_cols, obj_cols)
 =
   (* ignore (Mysql.exec dbd (insert_owner uri owner)); *)
   List.iter (function
@@ -90,53 +90,46 @@ 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 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*)
-      sprintf "SELECT source FROM %s" (obj_tbl ())
-    in
+    let query = sprintf "SELECT source FROM %s" (obj_tbl ()) in
     let result = Mysql.exec dbd query in
     let uris = Mysql.map result (fun cols ->
       match cols.(0) with
       | Some src -> src
       | None -> assert false) in
     (* and now some stuff to remove #xpointers and duplicates *)
-    let cleaned_uris = 
-      List.map (fun x -> Str.replace_first (Str.regexp "\#.*$") "" x) uris
-    in
-    let sorted_uris = List.fast_sort Pervasives.compare cleaned_uris in
-    match sorted_uris with
-    | [] -> sorted_uris
-    | he::tl -> 
-        (* no List.remove dups ?? *)
-        snd(List.fold_left (fun (last,l) cur -> if cur <> last then
-        (cur,cur::l) else (last,l)) (he,[he]) tl)
+    uris
   in
   let del_from tbl =
     let query s = 
@@ -147,7 +140,6 @@ let clean ~(dbd:Mysql.dbd) =
       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  
+    [sort_tbl; rel_tbl; obj_tbl; conclno_tbl; conclno_hyp_tbl; name_tbl];
+  owned_uris
 
diff --git a/helm/ocaml/metadata/metadataDb.mli b/helm/ocaml/metadata/metadataDb.mli
index 79bc82240..17d6fc094 100644
--- a/helm/ocaml/metadata/metadataDb.mli
+++ b/helm/ocaml/metadata/metadataDb.mli
@@ -27,7 +27,6 @@
   * PRE_EVAL(dbd) *)
 val index_constant:
   dbd:Mysql.dbd ->
-  owner:string ->
   uri:UriManager.uri -> body:Cic.term option -> ty:Cic.term ->
     unit
 
@@ -36,12 +35,12 @@ val index_constant:
   * PRE_EVAL(dbd) *)
 val index_inductive_def:
   dbd:Mysql.dbd ->
-  owner:string ->
   uri:UriManager.uri -> types:Cic.inductiveType list ->
     unit
 
 (* TODO Zack indexing of variables and (perhaps?) incomplete proofs *)
 
-  (** remove from the db all metadata pertaining to a given owner *)
-val clean: dbd:Mysql.dbd -> unit
+  (** remove from the db all metadata pertaining to a given owner
+  * @return list of uris removed from the db *)
+val clean: dbd:Mysql.dbd -> string list