at_least now supports the ownerized tables

diff --git a/helm/ocaml/metadata/metadataConstraints.ml b/helm/ocaml/metadata/metadataConstraints.ml
index 6a30e75d074402edddeac7f78d131bc70a519604..73e6f288dfd3b4e3b5815842684177d929a92717 100644 (file)
--- a/helm/ocaml/metadata/metadataConstraints.ml
+++ b/helm/ocaml/metadata/metadataConstraints.ml
@@ -85,71 +85,53 @@ let add_card_constr tbl (n,from,where) = function
         else [sprintf "table0.source = %s.source" cur_tbl]) @
         where))
 
-let at_least ~(dbd:Mysql.dbd) ?concl_card ?full_card
+let at_least ~(dbd:Mysql.dbd) ?concl_card ?full_card tables
   (metadata: MetadataTypes.constr list)
 =
   if (metadata = []) && concl_card = None && full_card = None then
     failwith "MetadataQuery.at_least: no constraints given";
+  let obj_tbl,rel_tbl,sort_tbl,conclno_tbl,conclno_hyp_tbl = tables in
   let add_constraint (n,from,where) metadata =
     let cur_tbl = tbln n in
-    let cur_ltbl = tbln (n+1) in
     match metadata with
     | `Obj (uri, positions) ->
-        let tbl = MetadataTypes.obj_tbl () in
-        let ltbl = MetadataTypes.library_obj_tbl in
-        let from = 
-          (sprintf "%s AS %s, %s AS %s" tbl cur_tbl ltbl cur_ltbl) :: from 
-        in
-        let where =
-          (sprintf "(%s.h_occurrence = \"%s\" OR %s.h_occurrence = \"%s\")" 
-          cur_tbl uri cur_ltbl uri) ::
+        let from = (sprintf "%s as %s" obj_tbl cur_tbl) :: from in
+        let where = 
+          (sprintf "(%s.h_occurrence = \"%s\")" cur_tbl uri) ::
           mk_positions positions cur_tbl ::
           (if n=0 then []
-          else [sprintf 
-            "(table0.source = %s.source OR table0.source = %s.source)" 
-            cur_tbl cur_ltbl]) @ where
+          else [sprintf "table0.source = %s.source" cur_tbl]) @ 
+          where
         in
         ((n+2), from, where)
     | `Rel positions ->
-        let tbl = MetadataTypes.rel_tbl () in
-        let ltbl = MetadataTypes.library_rel_tbl in
-        let from = 
-          (sprintf "%s AS %s, %s AS %s" tbl cur_tbl ltbl cur_ltbl) :: from 
-        in
+        let from = (sprintf "%s as %s" rel_tbl cur_tbl) :: from in
         let where =
           mk_positions positions cur_tbl ::
           (if n=0 then []
-          else [sprintf 
-            "(table0.source = %s.source OR table0.source = %s.source)" 
-             cur_tbl cur_ltbl]) @ where
+          else [sprintf "table0.source = %s.source" cur_tbl]) @ 
+          where
         in
         ((n+2), from, where)
     | `Sort (sort, positions) ->
-        let tbl = MetadataTypes.sort_tbl () in
-        let ltbl = MetadataTypes.library_sort_tbl in
         let sort_str = CicPp.ppsort sort in
-        let from = 
-          (sprintf "%s AS %s, %s AS %s" tbl cur_tbl ltbl cur_ltbl) :: from 
-        in
+        let from = (sprintf "%s as %s" sort_tbl cur_tbl) :: from in
         let where =
-          (sprintf "(%s.h_sort = \"%s\" OR %s.h_sort = \"%s\")" 
-            cur_tbl sort_str cur_ltbl sort_str) ::
+          (sprintf "%s.h_sort = \"%s\"" cur_tbl sort_str ) ::
               mk_positions positions cur_tbl ::
           (if n=0 then 
             []
           else 
-            [sprintf 
-              "(table0.source = %s.source OR table0.source = %s.source)" 
-              cur_tbl cur_ltbl]) @ where
+            [sprintf "table0.source = %s.source" cur_tbl ]) @ where
         in
         ((n+2), from, where)
   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 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 conclno_hyp_tbl (n,from,where) full_card
   in
   let from = String.concat ", " from in
   let where = String.concat " and " where in
@@ -158,6 +140,27 @@ let at_least ~(dbd:Mysql.dbd) ?concl_card ?full_card
   Mysql.map result
     (fun row -> match row.(0) with Some s -> s | _ -> assert false)
 
+let at_least  
+  ~(dbd:Mysql.dbd) ?concl_card ?full_card (metadata: MetadataTypes.constr list)
+=
+  let module MT = MetadataTypes in
+  if MT.are_tables_ownerized () then
+    (at_least ~dbd ?concl_card ?full_card 
+      (MT.obj_tbl (),MT.rel_tbl (),MT.sort_tbl (),
+       MT.conclno_tbl (),MT.conclno_hyp_tbl ()) 
+        metadata)
+        @
+    (at_least ~dbd ?concl_card ?full_card 
+      (MT.library_obj_tbl,MT.library_rel_tbl,MT.library_sort_tbl,
+       MT.library_conclno_tbl,MT.library_conclno_hyp_tbl) 
+        metadata)
+  else
+    at_least ~dbd ?concl_card ?full_card 
+      (MT.library_obj_tbl,MT.library_rel_tbl,MT.library_sort_tbl,
+       MT.library_conclno_tbl,MT.library_conclno_hyp_tbl) 
+        metadata 
+  
+    
   (** Prefix handling *)
 
 let filter_by_card n =
@@ -401,7 +404,7 @@ let get_constants (dbd:Mysql.dbd) ~where uri =
          "\"MainHypothesis\""]
   in
   let query = 
-    sprintf ("SELECT h_occurrence FROM %s WHERE source=\"%s\" AND (%s) UNION"^^
+    sprintf ("SELECT h_occurrence FROM %s WHERE source=\"%s\" AND (%s) UNION "^^
              "SELECT h_occurrence FROM %s WHERE source=\"%s\" AND (%s)")
       (MetadataTypes.obj_tbl ()) uri (String.concat " OR " positions)
       MetadataTypes.library_obj_tbl uri (String.concat " OR " positions)

diff --git a/helm/ocaml/metadata/metadataTypes.ml b/helm/ocaml/metadata/metadataTypes.ml
index 9e0d7c0b87a48f517cf4b136512469eeeabb30e6..3f55b886f8b2b0ea19ddbbec115b1427a5f3499d 100644 (file)
--- a/helm/ocaml/metadata/metadataTypes.ml
+++ b/helm/ocaml/metadata/metadataTypes.ml
@@ -104,3 +104,6 @@ let library_conclno_tbl = conclno_tbl_original
 let library_conclno_hyp_tbl = conclno_hyp_tbl_original
 let library_name_tbl = name_tbl_original
 
+let are_tables_ownerized () =
+  sort_tbl () <> library_sort_tbl
+  

diff --git a/helm/ocaml/metadata/metadataTypes.mli b/helm/ocaml/metadata/metadataTypes.mli
index c471d167a48014c6cad61a58ba63e28091d80dd0..b20c8ce147dca4eabab50f7f473ac477eb00448e 100644 (file)
--- a/helm/ocaml/metadata/metadataTypes.mli
+++ b/helm/ocaml/metadata/metadataTypes.mli
@@ -60,6 +60,7 @@ val constr_of_metadata: metadata -> constr
   (** invoke this function to set the current owner. Afterwards the functions
   * below will return the name of the table of the set owner *)
 val ownerize_tables : string -> unit
+val are_tables_ownerized : unit -> bool
 
 val sort_tbl: unit -> string  
 val rel_tbl: unit -> string