From c66e9d17eda5e5defcb363e42d891d2b407cf7c3 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 4 Feb 2005 09:15:10 +0000 Subject: [PATCH] - clean no longer unregister URIs from the getter, but returns them - removed owner table handling --- helm/ocaml/metadata/metadataDb.ml | 66 +++++++++++++----------------- helm/ocaml/metadata/metadataDb.mli | 7 ++-- 2 files changed, 32 insertions(+), 41 deletions(-) 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 -- 2.39.2