X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fmetadata%2FmetadataConstraints.ml;h=a4267c5fc6825faa3ccd11da33dc7e8d00a789ce;hb=fd0b68d4a811f2938bb045a81ad52c3d1f117e99;hp=c2dee6f5edb40cdc839ea5df43f1d8f56e96f800;hpb=ac741958783108ff31552e533c853e85c2ebb1c5;p=helm.git

diff --git a/helm/software/components/metadata/metadataConstraints.ml b/helm/software/components/metadata/metadataConstraints.ml
index c2dee6f5e..a4267c5fc 100644
--- a/helm/software/components/metadata/metadataConstraints.ml
+++ b/helm/software/components/metadata/metadataConstraints.ml
@@ -153,7 +153,7 @@ let add_constraint ?(start=0) ?(tables=default_tables) (n,from,where) metadata =
       in
       ((n+2), from, where)
 
-let exec ~(dbd:HSql.dbd) ?rating (n,from,where) =
+let exec dbtype ~(dbd:HSql.dbd) ?rating (n,from,where) =
   let from = String.concat ", " from in
   let where = String.concat " and " where in
   let query =
@@ -166,12 +166,14 @@ let exec ~(dbd:HSql.dbd) ?rating (n,from,where) =
           from where 
   in
   (* prerr_endline query; *) 
-  let result = HSql.exec dbd query in
+  let result = HSql.exec dbtype dbd query in
   HSql.map result
-    (fun row -> match row.(0) with Some s -> UriManager.uri_of_string s | _ -> assert false)
-
+    ~f:(fun row -> 
+     match row.(0) with Some s -> UriManager.uri_of_string s 
+     | _ -> assert false)
+;;
 
-let at_least ~(dbd:HSql.dbd) ?concl_card ?full_card ?diff ?rating tables
+let at_least dbtype ~(dbd:HSql.dbd) ?concl_card ?full_card ?diff ?rating tables
   (metadata: MetadataTypes.constr list)
 =
   let obj_tbl,rel_tbl,sort_tbl, count_tbl = tables in
@@ -187,7 +189,7 @@ let at_least ~(dbd:HSql.dbd) ?concl_card ?full_card ?diff ?rating tables
     let (n,from,where) =
       add_all_constr ~tbl:count_tbl (n,from,where) concl_card full_card diff
     in
-    exec ~dbd ?rating (n,from,where)
+    exec dbtype ~dbd ?rating (n,from,where)
 ;;
     
 let at_least  
@@ -195,13 +197,26 @@ let at_least
       (metadata: MetadataTypes.constr list)
 =
   if are_tables_ownerized () then
-    (at_least 
-       ~dbd ?concl_card ?full_card ?diff ?rating default_tables metadata) @
-    (at_least 
-       ~dbd ?concl_card ?full_card ?diff ?rating (current_tables ()) metadata)
+    at_least 
+      HSql.Library ~dbd ?concl_card ?full_card ?diff ?rating 
+        default_tables metadata
+    @
+    at_least 
+      HSql.Legacy ~dbd ?concl_card ?full_card ?diff ?rating 
+        default_tables metadata
+    @
+    at_least 
+      HSql.User ~dbd ?concl_card ?full_card ?diff ?rating 
+        (current_tables ()) metadata
+
   else
     at_least 
-      ~dbd ?concl_card ?full_card ?diff ?rating default_tables metadata 
+      HSql.Library ~dbd ?concl_card ?full_card ?diff ?rating 
+        default_tables metadata 
+    @
+    at_least 
+      HSql.Legacy ~dbd ?concl_card ?full_card ?diff ?rating 
+        default_tables metadata 
   
     
   (** Prefix handling *)
@@ -447,24 +462,30 @@ let get_constants (dbd:HSql.dbd) ~where uri =
         [ MetadataTypes.mainconcl_pos; MetadataTypes.inconcl_pos;
           MetadataTypes.inhyp_pos; MetadataTypes.mainhyp_pos ]
   in
-  let query = 
-    let pos_predicate =
-      String.concat " OR "
-        (List.map (fun pos -> sprintf "(h_position = \"%s\")" pos) positions)
-    in
-    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 pos_predicate
-      MetadataTypes.library_obj_tbl uri pos_predicate
-      
+  let pos_predicate =
+    String.concat " OR "
+      (List.map (fun pos -> sprintf "(h_position = \"%s\")" pos) positions)
+  in
+  let query tbl = 
+    sprintf "SELECT h_occurrence FROM %s WHERE source=\"%s\" AND (%s)"
+      tbl uri pos_predicate
+  in
+  let db = [
+    HSql.Library, MetadataTypes.library_obj_tbl;
+    HSql.Legacy, MetadataTypes.library_obj_tbl;
+    HSql.User, MetadataTypes.obj_tbl ()]
   in
-  let result = HSql.exec dbd query in
   let set = ref UriManagerSet.empty in
-  HSql.iter result
-    (fun col ->
-      match col.(0) with
-      | Some uri -> set := UriManagerSet.add (UriManager.uri_of_string uri) !set
-      | _ -> assert false);
+  List.iter
+    (fun (dbtype, table) ->
+      let result = HSql.exec dbtype dbd (query table) in
+      HSql.iter result
+        (fun col ->
+         match col.(0) with
+         | Some uri -> 
+             set := UriManagerSet.add (UriManager.uri_of_string uri) !set
+         | _ -> assert false)) 
+    db;
   !set
 
 let at_most ~(dbd:HSql.dbd) ?(where = `Conclusion) only u =