]> matita.cs.unibo.it Git - helm.git/blobdiff - components/whelp/whelp.ml
maxipatch for support of multiple DBs.
[helm.git] / components / whelp / whelp.ml
index 4a863eba8ea50ac9c6880045067b48b7b7c34096..ef544f8502630cfe965f1a2dc4fbabcccd0c3368 100644 (file)
@@ -43,22 +43,30 @@ let sqlpat_of_shellglob =
             shellglob)))
 
 let locate ~(dbd:HSql.dbd) ?(vars = false) pat =
-  let escape s = HSql.escape s in
+  let escape dbtype dbd s = HSql.escape dbtype dbd s in
   let sql_pat = sqlpat_of_shellglob pat in
-  let query =
+  let query dbtype tbl =
         sprintf 
           ("SELECT source FROM %s WHERE value LIKE \"%s\" "
-           ^^ HSql.escape_string_for_like
-           ^^ " UNION " ^^
-           "SELECT source FROM %s WHERE value LIKE \"%s\" "
-           ^^ HSql.escape_string_for_like)
-          (MetadataTypes.name_tbl ()) (escape sql_pat)
-           MetadataTypes.library_name_tbl (escape sql_pat)
+           ^^ HSql.escape_string_for_like dbtype dbd)
+          tbl (escape dbtype dbd sql_pat)
   in
-  let result = HSql.exec dbd query in
-  List.filter nonvar
-    (HSql.map result
-      (fun cols -> match cols.(0) with Some s -> UriManager.uri_of_string s | _ -> assert false))
+  let tbls = 
+    [HSql.User, MetadataTypes.name_tbl ();
+     HSql.Library, MetadataTypes.library_name_tbl;
+     HSql.Legacy, MetadataTypes.library_name_tbl]
+  in
+  let map cols =
+    match cols.(0) with 
+    | Some s -> UriManager.uri_of_string s | _ -> assert false
+  in
+  let result = 
+    List.fold_left
+      (fun acc (dbtype,tbl) -> 
+         acc @ HSql.map ~f:map (HSql.exec dbtype dbd (query dbtype tbl)))
+      [] tbls
+  in
+  List.filter nonvar result
 
 let match_term ~(dbd:HSql.dbd) ty =
 (*   debug_print (lazy (CicPp.ppterm ty)); *)
@@ -181,7 +189,7 @@ let instance ~dbd t =
         let constraints_for_dummy_type =
            List.map MetadataTypes.constr_of_metadata metadata_for_dummy_type in
         (* start with the dummy constant in main conlusion *)
-        let from = ["refObj as table0"] in
+        let from = ["refObj as table0"] in (* XXX table hardcoded *)
         let where = 
           [sprintf "table0.h_position = \"%s\"" MetadataTypes.mainconcl_pos;
                  sprintf "table0.h_depth >= %d" depth] in
@@ -202,11 +210,15 @@ let instance ~dbd t =
           sprintf "table0.h_depth - table%d.h_depth = %d" 
             n (depth - depth')::where
         in
+        (* XXX performed only in library and legacy not user *)
         let (m,from,where) =
           List.fold_left 
             (MetadataConstraints.add_constraint ~start:n)
-            (n,from,where) constraints_for_dummy_type in
-        MetadataConstraints.exec ~dbd (m,from,where)
+            (n,from,where) constraints_for_dummy_type 
+        in
+        MetadataConstraints.exec HSql.Library ~dbd (m,from,where)
+        @
+        MetadataConstraints.exec HSql.Legacy ~dbd (m,from,where)
 
 let elim ~dbd uri =
   let constraints =