From 26c3b57c2142bfd2242571109374c3203c7980dd Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 28 Apr 2005 13:30:40 +0000 Subject: [PATCH] single INSERT on multiple tuples cosmetic changes vars are now indexed --- helm/ocaml/metadata/metadataDb.ml | 89 ++++++++++++++--------- helm/ocaml/metadata/metadataDb.mli | 15 +--- helm/ocaml/metadata/metadataExtractor.ml | 69 +++++++++++++++--- helm/ocaml/metadata/metadataExtractor.mli | 17 ++--- helm/ocaml/metadata/metadataPp.ml | 12 +-- helm/ocaml/metadata/metadataPp.mli | 8 +- helm/ocaml/metadata/test.ml | 11 +-- 7 files changed, 130 insertions(+), 91 deletions(-) diff --git a/helm/ocaml/metadata/metadataDb.ml b/helm/ocaml/metadata/metadataDb.ml index 6cbfeb1ff..a4e6008a8 100644 --- a/helm/ocaml/metadata/metadataDb.ml +++ b/helm/ocaml/metadata/metadataDb.ml @@ -27,45 +27,51 @@ open MetadataTypes open Printf -let prepare_insert () = - (* - let insert_owner a b = - sprintf "INSERT %s VALUES (\"%s\", \"%s\")" (owners_tbl ())a b +let execute_insert dbd uri (sort_cols, rel_cols, obj_cols) = + let sort_tuples = + List.fold_left (fun s l -> match l with + | [`String a; `String b; `Int c; `String d] -> + sprintf "(\"%s\", \"%s\", %d, \"%s\")" a b c d :: s + | _ -> assert false ) + [] sort_cols in - *) - let insert_sort a b c d = - sprintf "INSERT %s VALUES (\"%s\", \"%s\", %d, \"%s\")" (sort_tbl ())a b c d - in - let insert_rel a b c = - sprintf "INSERT %s VALUES (\"%s\", \"%s\", %d)" (rel_tbl ()) a b c - in - 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) - -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)); *) - List.iter (function - | [`String a; `String b; `Int c; `String d] -> - ignore (Mysql.exec dbd (insert_sort a b c d)) - | _ -> assert false) - sort_cols; - List.iter (function + let rel_tuples = + List.fold_left (fun s l -> match l with | [`String a; `String b; `Int c] -> - ignore (Mysql.exec dbd (insert_rel a b c)) + sprintf "(\"%s\", \"%s\", %d)" a b c :: s | _ -> assert false) - rel_cols; - List.iter (function + [] rel_cols + in + let obj_tuples = List.fold_left (fun s l -> match l with | [`String a; `String b; `String c; `Int d] -> - ignore (Mysql.exec dbd (insert_obj a b c (string_of_int d))) + sprintf "(\"%s\", \"%s\", \"%s\", %d)" a b c d :: s | [`String a; `String b; `String c; `Null] -> - ignore (Mysql.exec dbd (insert_obj a b c "NULL")) + sprintf "(\"%s\", \"%s\", \"%s\", %s)" a b c "NULL" :: s | _ -> assert false) - obj_cols - + [] obj_cols + in + if sort_tuples <> [] then + begin + let query_sort = + sprintf "INSERT %s VALUES %s;" (sort_tbl ()) (String.concat "," sort_tuples) + in + ignore (Mysql.exec dbd query_sort) + end; + if rel_tuples <> [] then + begin + let query_rel = + sprintf "INSERT %s VALUES %s;" (rel_tbl ()) (String.concat "," rel_tuples) + in + ignore (Mysql.exec dbd query_rel) + end; + if obj_tuples <> [] then + begin + let query_obj = + sprintf "INSERT %s VALUES %s;" (obj_tbl ()) (String.concat "," obj_tuples) + in + ignore (Mysql.exec dbd query_obj) + end + let insert_const_no dbd uri = 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%%\"" @@ -92,7 +98,7 @@ type columns = (* 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 -> @@ -110,7 +116,7 @@ let index_inductive_def ~dbd = let query = prepare_insert () in fun ~uri ~types -> if not (already_indexed uri) then begin - let metadata = MetadataExtractor.compute_ind ~uri ~types in + 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 @@ -119,6 +125,19 @@ let index_inductive_def ~dbd = List.iter (insert_const_no dbd) uris; List.iter (fun (uri, name, _) -> insert_name ~dbd ~uri ~name) metadata end +*) +let index_obj ~dbd ~uri = + 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_metadata metadata in + execute_insert dbd 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] diff --git a/helm/ocaml/metadata/metadataDb.mli b/helm/ocaml/metadata/metadataDb.mli index a5b0d2753..20f618f8d 100644 --- a/helm/ocaml/metadata/metadataDb.mli +++ b/helm/ocaml/metadata/metadataDb.mli @@ -23,21 +23,10 @@ * http://helm.cs.unibo.it/ *) - (** index a Cic.Constant object and insert resulting metadata into the db - * PRE_EVAL(dbd) *) -val index_constant: - dbd:Mysql.dbd -> - uri:UriManager.uri -> body:Cic.term option -> ty:Cic.term -> - unit - (** index a Cic.InductiveDefinition object and insert resulting metadata into - * the db - * PRE_EVAL(dbd) *) -val index_inductive_def: - dbd:Mysql.dbd -> - uri:UriManager.uri -> types:Cic.inductiveType list -> - unit +val index_obj: dbd:Mysql.dbd -> uri:UriManager.uri -> unit + (* TODO Zack indexing of variables and (perhaps?) incomplete proofs *) (** remove from the db all metadata pertaining to a given owner diff --git a/helm/ocaml/metadata/metadataExtractor.ml b/helm/ocaml/metadata/metadataExtractor.ml index 784de4db6..fdb1114fa 100644 --- a/helm/ocaml/metadata/metadataExtractor.ml +++ b/helm/ocaml/metadata/metadataExtractor.ml @@ -69,12 +69,12 @@ let incr_depth = function let compute_term pos term = let rec aux (pos: position) set = function - | Cic.Rel _ -> + | Cic.Rel _ + | Cic.Var _ -> if is_main_pos pos then S.add (`Rel (main_pos pos)) set else set - | Cic.Var _ -> set | Cic.Meta (_, local_context) -> List.fold_left (fun set context -> @@ -106,9 +106,9 @@ let compute_term pos term = let set = aux pos set source in aux pos set target) | Cic.Lambda (_, source, target) -> - assert (not (is_main_pos pos)); - let set = aux pos set source in - aux pos set target + (*assert (not (is_main_pos pos));*) + let set = aux (next_pos pos) set source in + aux (next_pos pos) set target | Cic.LetIn (_, term, target) -> if is_main_pos pos then aux pos set (CicSubstitution.subst term target) @@ -229,28 +229,32 @@ let compute_metas term = in aux false (IntSet.empty, IntSet.empty) term -let compute_type uri typeno (name, _, ty, constructors) = + (** type of inductiveType *) +let compute_type pos uri typeno (name, _, ty, constructors) = let consno = ref 0 in let type_metadata = (UriManager.string_of_uriref (uri, [typeno]), name, - S.elements (compute_term (`MainConclusion (Some 0)) ty)) + S.elements (compute_term pos ty)) in let constructors_metadata = List.map (fun (name, term) -> incr consno; let uri = UriManager.string_of_uriref (uri, [typeno; !consno]) in - (uri, name, S.elements (compute_term (`MainConclusion (Some 0)) term))) + (uri, name, S.elements + (compute_term pos term))) constructors in type_metadata :: constructors_metadata -let compute_ind ~uri ~types = +let compute_ind pos ~uri ~types = let idx = ref ~-1 in - List.concat (List.map (fun ty -> incr idx; compute_type uri !idx ty) types) + List.concat + (List.map + (fun ty -> incr idx; compute_type pos uri !idx ty) types) -let compute ~body ~ty = - let type_metadata = compute_term (`MainConclusion (Some 0)) ty in +let compute (pos:position) ~body ~ty = + let type_metadata = compute_term pos ty in let body_metadata = match body with | None -> S.empty @@ -275,3 +279,44 @@ let compute ~body ~ty = let compute_term start_pos term = S.elements (compute_term start_pos term) +let rec compute_var pos uri = + let o, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + match o with + | Cic.Variable (_, body, ty, params, _) -> + let metadata_of_vars = + List.flatten + (List.map (compute_var (next_pos pos)) params) in + (match pos with + | `MainHypothesis (Some 0) -> + let pos = `MainHypothesis(Some (List.length params)) in + (compute pos ~body ~ty)@metadata_of_vars + | `InHypothesis -> + (compute pos ~body ~ty)@metadata_of_vars + | _ -> assert false) + | _ -> assert false + +let compute_obj uri = + let o, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + match o with + | Cic.Variable (_, body, ty, params, _) + | Cic.Constant (_, body, ty, params, _) -> + let pos = `MainConclusion(Some (List.length params)) in + let metadata = compute pos ~body ~ty + in + let metadata_of_vars = + List.flatten + (List.map (compute_var (`MainHypothesis (Some 0))) params) + in + [UriManager.string_of_uri uri, + UriManager.name_of_uri uri,metadata @ metadata_of_vars] + | Cic.InductiveDefinition (types, params, _, _) -> + let pos = `MainConclusion(Some (List.length params)) in + let metadata_of_vars = + List.flatten + (List.map (compute_var (`MainHypothesis (Some 0))) params) in + let metadata = compute_ind pos ~uri ~types in + List.map (fun (uri,name,md) -> (uri,name,md@metadata_of_vars)) metadata + | Cic.CurrentProof _ -> assert false + + +let compute ~body ~ty = compute (`MainConclusion (Some 0)) ~body ~ty diff --git a/helm/ocaml/metadata/metadataExtractor.mli b/helm/ocaml/metadata/metadataExtractor.mli index 450c3a525..8308c0ee0 100644 --- a/helm/ocaml/metadata/metadataExtractor.mli +++ b/helm/ocaml/metadata/metadataExtractor.mli @@ -23,17 +23,16 @@ * http://helm.cs.unibo.it/ *) -val compute: body:Cic.term option -> ty:Cic.term -> MetadataTypes.metadata list - - (** @return tuples *) -val compute_ind: - uri:UriManager.uri -> types:Cic.inductiveType list -> - (string * string * MetadataTypes.metadata list) list - -val compute_term: - MetadataTypes.position -> Cic.term -> +val compute: + body:Cic.term option -> + ty:Cic.term -> MetadataTypes.metadata list + (** @return tuples *) +val compute_obj: + UriManager.uri -> + (string * string * MetadataTypes.metadata list) list + module IntSet: Set.S with type elt = int (** given a term, returns a pair of sets corresponding respectively to the set diff --git a/helm/ocaml/metadata/metadataPp.ml b/helm/ocaml/metadata/metadataPp.ml index e2e21662b..5fc05b91d 100644 --- a/helm/ocaml/metadata/metadataPp.ml +++ b/helm/ocaml/metadata/metadataPp.ml @@ -59,7 +59,7 @@ let uri_of_pos pos = String.concat "#" [metadata_ns; pp_position pos] type t = [ `Int of int | `String of string | `Null ] -let columns_of_metadata ~about metadatas = +let columns_of_metadata_aux ~about metadata = let sort s = `String (CicPp.ppsort s) in let source = `String about in let occurrence u = `String u in @@ -76,14 +76,14 @@ let columns_of_metadata ~about metadatas = let (p, d) = columns_of_position p in sort_cols, rel_cols, [source; occurrence o; p; d] :: obj_cols) - ([], [], []) metadatas + ([], [], []) metadata -let columns_of_ind_metadata ind_metadata = +let columns_of_metadata metadata = List.fold_left - (fun (sort_cols, rel_cols, obj_cols) (uri, _, metadatas) -> - let (s, r, o) = columns_of_metadata ~about:uri metadatas in + (fun (sort_cols, rel_cols, obj_cols) (uri, _, metadata) -> + let (s, r, o) = columns_of_metadata_aux ~about:uri metadata in (List.append sort_cols s, List.append rel_cols r, List.append obj_cols o)) - ([], [], []) ind_metadata + ([], [], []) metadata (* let pp_columns ?(sep = "\n") (sort_cols, rel_cols, obj_cols) = diff --git a/helm/ocaml/metadata/metadataPp.mli b/helm/ocaml/metadata/metadataPp.mli index bd37a9959..39ccd6c32 100644 --- a/helm/ocaml/metadata/metadataPp.mli +++ b/helm/ocaml/metadata/metadataPp.mli @@ -36,14 +36,8 @@ type t = | `String of string | `Null ] - (** @param about uri of object whose metadata are about - * @return columns for Sort, Rel, and Obj respectively *) -val columns_of_metadata: - about:string -> MetadataTypes.metadata list -> - t list list * t list list * t list list - (** @return columns for Sort, Rel, and Obj respectively *) -val columns_of_ind_metadata: +val columns_of_metadata: (string * string * MetadataTypes.metadata list) list -> t list list * t list list * t list list diff --git a/helm/ocaml/metadata/test.ml b/helm/ocaml/metadata/test.ml index 21274a585..8e805840a 100644 --- a/helm/ocaml/metadata/test.ml +++ b/helm/ocaml/metadata/test.ml @@ -8,7 +8,7 @@ in let owner = try Sys.argv.(2) - with Invalid_argument _ -> "matita_test" + with Invalid_argument _ -> "matita_test2" in let _ = MetadataTypes.ownerize_tables owner in if Sys.argv.(1) = "clean" then begin @@ -24,14 +24,7 @@ end else incr n; Printf.printf "%d\t%s\n" !n line; flush stdout; let uri = UriManager.uri_of_string line in - (match CicEnvironment.get_obj CicUniv.empty_ugraph uri with - | Cic.Constant (_, body, ty, _, _), _ -> - MetadataDb.index_constant ~body ~ty ~uri ~dbd - | Cic.Variable (_, body, ty, _, _), _ -> - MetadataDb.index_constant ~body ~ty ~uri ~dbd - | Cic.InductiveDefinition (types, _, _, _), _ -> - MetadataDb.index_inductive_def ~dbd ~uri ~types - | _ -> assert false) + MetadataDb.index_obj ~dbd ~uri done with End_of_file -> close_in ic -- 2.39.2