From: Enrico Tassi Date: Thu, 3 Feb 2005 14:31:59 +0000 (+0000) Subject: new metadataTypes interface (with ownerize function) X-Git-Tag: V_0_1_0~58 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a36baf354f63f6749dba7a8cc67caf3b888ba8cf;p=helm.git new metadataTypes interface (with ownerize function) --- diff --git a/helm/ocaml/metadata/.depend b/helm/ocaml/metadata/.depend index 15500d2c4..bb47a0559 100644 --- a/helm/ocaml/metadata/.depend +++ b/helm/ocaml/metadata/.depend @@ -1,15 +1,17 @@ -metadataExtractor.cmi: metadataTypes.cmo -metadataPp.cmi: metadataTypes.cmo -metadataConstraints.cmi: metadataTypes.cmo -metadataExtractor.cmo: metadataTypes.cmo metadataExtractor.cmi +metadataExtractor.cmi: metadataTypes.cmi +metadataPp.cmi: metadataTypes.cmi +metadataConstraints.cmi: metadataTypes.cmi +metadataTypes.cmo: metadataTypes.cmi +metadataTypes.cmx: metadataTypes.cmi +metadataExtractor.cmo: metadataTypes.cmi metadataExtractor.cmi metadataExtractor.cmx: metadataTypes.cmx metadataExtractor.cmi -metadataPp.cmo: metadataTypes.cmo metadataPp.cmi +metadataPp.cmo: metadataTypes.cmi metadataPp.cmi metadataPp.cmx: metadataTypes.cmx metadataPp.cmi -metadataDb.cmo: metadataExtractor.cmi metadataPp.cmi metadataTypes.cmo \ +metadataDb.cmo: metadataExtractor.cmi metadataPp.cmi metadataTypes.cmi \ metadataDb.cmi metadataDb.cmx: metadataExtractor.cmx metadataPp.cmx metadataTypes.cmx \ metadataDb.cmi -metadataConstraints.cmo: metadataPp.cmi metadataTypes.cmo \ +metadataConstraints.cmo: metadataPp.cmi metadataTypes.cmi \ metadataConstraints.cmi metadataConstraints.cmx: metadataPp.cmx metadataTypes.cmx \ metadataConstraints.cmi diff --git a/helm/ocaml/metadata/Makefile b/helm/ocaml/metadata/Makefile index 4c8f53fc1..e6b35738f 100644 --- a/helm/ocaml/metadata/Makefile +++ b/helm/ocaml/metadata/Makefile @@ -3,11 +3,12 @@ REQUIRES = mysql helm-cic_proof_checking PREDICATES = INTERFACE_FILES = \ + metadataTypes.mli \ metadataExtractor.mli \ metadataPp.mli \ metadataDb.mli \ - metadataConstraints.mli -IMPLEMENTATION_FILES = metadataTypes.ml $(INTERFACE_FILES:%.mli=%.ml) + metadataConstraints.mli +IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) EXTRA_OBJECTS_TO_INSTALL = EXTRA_OBJECTS_TO_CLEAN = diff --git a/helm/ocaml/metadata/metadataConstraints.ml b/helm/ocaml/metadata/metadataConstraints.ml index 1b28e44d0..25803dc5c 100644 --- a/helm/ocaml/metadata/metadataConstraints.ml +++ b/helm/ocaml/metadata/metadataConstraints.ml @@ -94,7 +94,7 @@ let at_least ~(dbd:Mysql.dbd) ?concl_card ?full_card let cur_tbl = tbln n in match metadata with | `Obj (uri, positions) -> - let tbl = MetadataTypes.obj_tbl in + let tbl = MetadataTypes.obj_tbl () in let from = (sprintf "%s as %s" tbl cur_tbl) :: from in let where = (sprintf "%s.h_occurrence = \"%s\"" cur_tbl uri) :: @@ -105,7 +105,7 @@ let at_least ~(dbd:Mysql.dbd) ?concl_card ?full_card in ((n+1), from, where) | `Rel positions -> - let tbl = MetadataTypes.rel_tbl in + let tbl = MetadataTypes.rel_tbl () in let from = (sprintf "%s as %s" tbl cur_tbl) :: from in let where = mk_positions positions cur_tbl :: @@ -115,7 +115,7 @@ let at_least ~(dbd:Mysql.dbd) ?concl_card ?full_card in ((n+1), from, where) | `Sort (sort, positions) -> - let tbl = MetadataTypes.sort_tbl in + let tbl = MetadataTypes.sort_tbl () in let sort_str = CicPp.ppsort sort in let from = (sprintf "%s as %s" tbl cur_tbl) :: from in let where = @@ -129,10 +129,10 @@ let at_least ~(dbd:Mysql.dbd) ?concl_card ?full_card in let (n,from,where) = List.fold_left add_constraint (0,[],[]) metadata in let (n,from,where) = - add_card_constr MetadataTypes.conclno_tbl (n,from,where) concl_card + add_card_constr (MetadataTypes.conclno_tbl ()) (n,from,where) concl_card in let (n,from,where) = - add_card_constr MetadataTypes.conclno_hyp_tbl (n,from,where) full_card + add_card_constr (MetadataTypes.conclno_hyp_tbl ()) (n,from,where) full_card in let from = String.concat ", " from in let where = String.concat " and " where in diff --git a/helm/ocaml/metadata/metadataDb.ml b/helm/ocaml/metadata/metadataDb.ml index df79118f2..441609a1d 100644 --- a/helm/ocaml/metadata/metadataDb.ml +++ b/helm/ocaml/metadata/metadataDb.ml @@ -29,16 +29,16 @@ open Printf let prepare_insert () = let insert_owner a b = - sprintf "INSERT %s VALUES (\"%s\", \"%s\")" owners_tbl 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 + 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 + 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 + sprintf "INSERT %s VALUES (\"%s\", \"%s\", \"%s\", %s)" (obj_tbl ()) a b c d in (insert_owner, insert_sort, insert_rel, insert_obj) @@ -67,21 +67,21 @@ let execute_insert dbd (insert_owner, insert_sort, insert_rel, insert_obj) 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%%\"" - conclno_tbl uri obj_tbl inconcl_pos mainconcl_pos uri + (conclno_tbl ()) uri (obj_tbl ()) inconcl_pos mainconcl_pos uri in let concl_hyp = sprintf "INSERT %s 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 + (conclno_hyp_tbl ()) uri (obj_tbl ()) inbody_pos uri in ignore (Mysql.exec dbd inconcl_no); ignore (Mysql.exec dbd concl_hyp) 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 ()) uri name in ignore (Mysql.exec dbd query) @@ -114,7 +114,7 @@ let index_inductive_def ~dbd = let clean ~(dbd:Mysql.dbd) ~owner = 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 WHERE owner = \"%s\"" (owners_tbl ()) owner in let result = Mysql.exec dbd query in Mysql.map result (fun cols -> @@ -123,7 +123,9 @@ let clean ~(dbd:Mysql.dbd) ~owner = | None -> assert false) in let del_from tbl = - let query s = sprintf "DELETE FROM %s WHERE source LIKE \"%s%%\"" tbl s in + let query s = + sprintf "DELETE FROM %s WHERE source LIKE \"%s%%\"" (tbl ()) s + in List.iter (fun source_col -> ignore (Mysql.exec dbd (query source_col))) owned_uris diff --git a/helm/ocaml/metadata/metadataTypes.ml b/helm/ocaml/metadata/metadataTypes.ml index 719ba508c..b52f52246 100644 --- a/helm/ocaml/metadata/metadataTypes.ml +++ b/helm/ocaml/metadata/metadataTypes.ml @@ -63,11 +63,42 @@ let constr_of_metadata: metadata -> constr = function | `Rel pos -> `Rel [pos] | `Obj (uri, pos) -> `Obj (uri, [pos]) -let sort_tbl = "refSort" -let rel_tbl = "refRel" -let obj_tbl = "refObj" -let owners_tbl = "owners" -let conclno_tbl = "no_inconcl_aux" -let conclno_hyp_tbl = "no_concl_hyp" -let name_tbl = "objectName" + (** the name of the tables in the DB *) +let sort_tbl_original = "refSort" +let rel_tbl_original = "refRel" +let obj_tbl_original = "refObj" +let owners_tbl_original = "owners" +let conclno_tbl_original = "no_inconcl_aux" +let conclno_hyp_tbl_original = "no_concl_hyp" +let name_tbl_original = "objectName" + + (** the names currently used *) +let sort_tbl_real = ref sort_tbl_original +let rel_tbl_real = ref rel_tbl_original +let obj_tbl_real = ref obj_tbl_original +let owners_tbl_real = ref owners_tbl_original +let conclno_tbl_real = ref conclno_tbl_original +let conclno_hyp_tbl_real = ref conclno_hyp_tbl_original +let name_tbl_real = ref name_tbl_original + + (** the exported symbols *) +let sort_tbl () = ! sort_tbl_real ;; +let rel_tbl () = ! rel_tbl_real ;; +let obj_tbl () = ! obj_tbl_real ;; +let owners_tbl () = ! owners_tbl_real ;; +let conclno_tbl () = ! conclno_tbl_real ;; +let conclno_hyp_tbl () = ! conclno_hyp_tbl_real ;; +let name_tbl () = ! name_tbl_real ;; + + (** to use the owned tables *) +let ownerize_tables owner = + sort_tbl_real := ( sort_tbl_original ^ "_" ^ owner) ; + rel_tbl_real := ( rel_tbl_original ^ "_" ^ owner) ; + obj_tbl_real := ( obj_tbl_original ^ "_" ^ owner) ; + owners_tbl_real := ( owners_tbl_original ^ "_" ^ owner) ; + conclno_tbl_real := ( conclno_tbl_original ^ "_" ^ owner) ; + conclno_hyp_tbl_real := ( conclno_hyp_tbl_original ^ "_" ^ owner) ; + name_tbl_real := ( name_tbl_original ^ "_" ^ owner) +;; + diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml index 52bd953a9..4df0de08b 100644 --- a/helm/ocaml/tactics/metadataQuery.ml +++ b/helm/ocaml/tactics/metadataQuery.ml @@ -50,7 +50,7 @@ let locate ~(dbd:Mysql.dbd) ?(vars = false) pat = let sql_pat = sqlpat_of_shellglob pat in let query = sprintf "SELECT source FROM %s WHERE value LIKE \"%s\"" - MetadataTypes.name_tbl sql_pat + (MetadataTypes.name_tbl ()) sql_pat in let result = Mysql.exec dbd query in List.filter nonvar