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

diff --git a/helm/ocaml/metadata/metadataConstraints.ml b/helm/ocaml/metadata/metadataConstraints.ml
index 2c04562d8..73e6f288d 100644
--- a/helm/ocaml/metadata/metadataConstraints.ml
+++ b/helm/ocaml/metadata/metadataConstraints.ml
@@ -85,54 +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
     match metadata with
     | `Obj (uri, positions) ->
-        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) ::
+        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" cur_tbl]) @
+          else [sprintf "table0.source = %s.source" cur_tbl]) @ 
           where
         in
-        ((n+1), from, where)
+        ((n+2), from, where)
     | `Rel positions ->
-        let tbl = MetadataTypes.rel_tbl in
-        let from = (sprintf "%s as %s" tbl cur_tbl) :: 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" cur_tbl]) @
+          else [sprintf "table0.source = %s.source" cur_tbl]) @ 
           where
         in
-        ((n+1), from, where)
+        ((n+2), from, where)
     | `Sort (sort, positions) ->
-        let tbl = MetadataTypes.sort_tbl in
-        let sort_str = MetadataPp.pp_sort sort in
-        let from = (sprintf "%s as %s" tbl cur_tbl) :: from in
+        let sort_str = CicPp.ppsort sort in
+        let from = (sprintf "%s as %s" sort_tbl cur_tbl) :: from in
         let where =
-          (sprintf "%s.h_sort = \"%s\"" cur_tbl sort_str) ::
-          mk_positions positions cur_tbl ::
-          (if n=0 then []
-          else [sprintf "table0.source = %s.source" cur_tbl]) @
-          where
+          (sprintf "%s.h_sort = \"%s\"" cur_tbl sort_str ) ::
+              mk_positions positions cur_tbl ::
+          (if n=0 then 
+            []
+          else 
+            [sprintf "table0.source = %s.source" cur_tbl ]) @ where
         in
-        ((n+1), from, where)
+        ((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
@@ -141,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 =
@@ -384,8 +404,11 @@ let get_constants (dbd:Mysql.dbd) ~where uri =
          "\"MainHypothesis\""]
   in
   let query = 
-    sprintf "select h_occurrence from refObj where source=\"%s\" and (%s)"
-      uri (String.concat " or " positions)
+    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)
+      
   in
   let result = Mysql.exec dbd query in
   let set = ref StringSet.empty in