new metadataTypes interface (with ownerize function)

diff --git a/helm/ocaml/metadata/.depend b/helm/ocaml/metadata/.depend
index 15500d2c4c06a43c4726de0b6d4caf5dab89e9be..bb47a05591208e1f17a00b69f435d656e01660db 100644 (file)
--- 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 4c8f53fc10033f236e2746031b85145b3c00617f..e6b35738f6e82db7a27c216e7e8dfd7460fd0d52 100644 (file)
--- 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 1b28e44d0b03632ffaec79d66b37f4948d679e58..25803dc5c6e6647fe88e1c9bc7e85a066501c2d5 100644 (file)
--- 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 df79118f2cb796dbc2233c9115c3b79e46ee3c9c..441609a1ddd4d0423afd6f8dc4cb70e2c5b0180c 100644 (file)
--- 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 719ba508c1ae37d5e40f364939c4dec35fe8658a..b52f522468584789df867f3cc4124c6cd897f50c 100644 (file)
--- 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 52bd953a9c842e80da3ef6f4045142f6ec7e9251..4df0de08b93c5add8d741cfd17136898c56be249 100644 (file)
--- 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