From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 4 Feb 2005 15:47:40 +0000 (+0000)
Subject: added library table and owner tables handling in the SQL code
X-Git-Tag: V_0_1_0~14
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fdb1857ede8fb5a72d50cd71774c81c86aede162;p=helm.git

added library table and owner tables handling in the SQL code
---

diff --git a/helm/ocaml/metadata/metadataConstraints.ml b/helm/ocaml/metadata/metadataConstraints.ml
index 25803dc5c..bedc2db86 100644
--- a/helm/ocaml/metadata/metadataConstraints.ml
+++ b/helm/ocaml/metadata/metadataConstraints.ml
@@ -92,40 +92,57 @@ let at_least ~(dbd:Mysql.dbd) ?concl_card ?full_card
     failwith "MetadataQuery.at_least: no constraints given";
   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 from = (sprintf "%s as %s" tbl cur_tbl) :: from 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\"" cur_tbl uri) ::
+          (sprintf "(%s.h_occurrence = \"%s\" OR %s.h_occurrence = \"%s\")" 
+          cur_tbl uri cur_ltbl uri) ::
           mk_positions positions cur_tbl ::
           (if n=0 then []
-          else [sprintf "table0.source = %s.source" cur_tbl]) @
-          where
+          else [sprintf 
+            "(table0.source = %s.source AND table0.source = %s.source)" 
+            cur_tbl cur_ltbl]) @ 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 ltbl = MetadataTypes.library_rel_tbl in
+        let from = 
+          (sprintf "%s AS %s, %s AS %s" tbl cur_tbl ltbl cur_ltbl) :: from 
+        in
         let where =
           mk_positions positions cur_tbl ::
           (if n=0 then []
-          else [sprintf "table0.source = %s.source" cur_tbl]) @
-          where
+          else [sprintf 
+            "(table0.source = %s.source AND table0.source = %s.source)" 
+             cur_tbl cur_ltbl]) @ where
         in
-        ((n+1), from, where)
+        ((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" tbl cur_tbl) :: from in
+        let from = 
+          (sprintf "%s AS %s, %s AS %s" tbl cur_tbl ltbl cur_ltbl) :: 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\" OR %s.h_sort = \"%s\")" 
+            cur_tbl sort_str cur_ltbl 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
         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) =
@@ -384,8 +401,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