X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmetadata%2FmetadataConstraints.ml;h=73e6f288dfd3b4e3b5815842684177d929a92717;hb=7e9904185ceff75884783dbf0bad506b8521b857;hp=bedc2db86f20ec1be0301fb96cd75b476f7d2144;hpb=fdb1857ede8fb5a72d50cd71774c81c86aede162;p=helm.git

diff --git a/helm/ocaml/metadata/metadataConstraints.ml b/helm/ocaml/metadata/metadataConstraints.ml
index bedc2db86..73e6f288d 100644
--- 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 AND 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 AND 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 AND 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)