]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/metadata/metadataConstraints.ml
New module HMysql (to abstract over Mysql and make profiling easier).
[helm.git] / helm / ocaml / metadata / metadataConstraints.ml
index d18663fadcaea3998f1267915967827c0ce83611..6431513ff3220f4ebdab16cb95d8c6bf82f5c611 100644 (file)
@@ -151,7 +151,7 @@ let add_constraint ?(start=0) ?(tables=default_tables) (n,from,where) metadata =
       in
       ((n+2), from, where)
 
-let exec ~(dbd:Mysql.dbd) ?rating (n,from,where) =
+let exec ~(dbd:HMysql.dbd) ?rating (n,from,where) =
   let from = String.concat ", " from in
   let where = String.concat " and " where in
   let query =
@@ -164,12 +164,12 @@ let exec ~(dbd:Mysql.dbd) ?rating (n,from,where) =
           from where 
   in
 (*  prerr_endline query; *)
-  let result = Mysql.exec dbd query in
-  Mysql.map result
+  let result = HMysql.exec dbd query in
+  HMysql.map result
     (fun row -> match row.(0) with Some s -> UriManager.uri_of_string s | _ -> assert false)
 
 
-let at_least ~(dbd:Mysql.dbd) ?concl_card ?full_card ?diff ?rating tables
+let at_least ~(dbd:HMysql.dbd) ?concl_card ?full_card ?diff ?rating tables
   (metadata: MetadataTypes.constr list)
 =
   let obj_tbl,rel_tbl,sort_tbl, count_tbl = tables 
@@ -185,7 +185,7 @@ let at_least ~(dbd:Mysql.dbd) ?concl_card ?full_card ?diff ?rating tables
   exec ~dbd ?rating (n,from,where)
     
 let at_least  
-  ~(dbd:Mysql.dbd) ?concl_card ?full_card ?diff ?rating
+  ~(dbd:HMysql.dbd) ?concl_card ?full_card ?diff ?rating
       (metadata: MetadataTypes.constr list)
 =
   if are_tables_ownerized () then
@@ -432,7 +432,7 @@ let must_of_prefix ?(where = `Conclusion) m s =
 
 let escape = Str.global_replace (Str.regexp_string "\'") "\\'"
 
-let get_constants (dbd:Mysql.dbd) ~where uri =
+let get_constants (dbd:HMysql.dbd) ~where uri =
   let uri = escape (UriManager.string_of_uri uri) in
   let positions =
     match where with
@@ -452,16 +452,16 @@ let get_constants (dbd:Mysql.dbd) ~where uri =
       MetadataTypes.library_obj_tbl uri pos_predicate
       
   in
-  let result = Mysql.exec dbd query in
+  let result = HMysql.exec dbd query in
   let set = ref UriManagerSet.empty in
-  Mysql.iter result
+  HMysql.iter result
     (fun col ->
       match col.(0) with
       | Some uri -> set := UriManagerSet.add (UriManager.uri_of_string uri) !set
       | _ -> assert false);
   !set
 
-let at_most ~(dbd:Mysql.dbd) ?(where = `Conclusion) only u =
+let at_most ~(dbd:HMysql.dbd) ?(where = `Conclusion) only u =
   let inconcl = get_constants dbd ~where u in
   UriManagerSet.subset inconcl only
 
@@ -479,7 +479,7 @@ let myspeciallist =
    0,UriManager.uri_of_string "cic:/Coq/Init/Logic/f_equal3.con"]
 
 
-let compute_exactly ~(dbd:Mysql.dbd) ?(facts=false) ~where main prefixes =
+let compute_exactly ~(dbd:HMysql.dbd) ?(facts=false) ~where main prefixes =
   List.concat
     (List.map 
       (fun (m,s) -> 
@@ -510,7 +510,7 @@ let compute_exactly ~(dbd:Mysql.dbd) ?(facts=false) ~where main prefixes =
 
   (* critical value reached, fallback to "only" constraints *)
 
-let compute_with_only ~(dbd:Mysql.dbd) ?(facts=false) ?(where = `Conclusion) 
+let compute_with_only ~(dbd:HMysql.dbd) ?(facts=false) ?(where = `Conclusion) 
   main prefixes constants
 =
   let max_prefix_length = 
@@ -545,7 +545,7 @@ let compute_with_only ~(dbd:Mysql.dbd) ?(facts=false) ?(where = `Conclusion)
 
   (* real match query implementation *)
 
-let cmatch ~(dbd:Mysql.dbd)  ?(facts=false) t =
+let cmatch ~(dbd:HMysql.dbd)  ?(facts=false) t =
   let (main, constants) = signature_of t in
   match main with
   | None -> []
@@ -597,7 +597,7 @@ let power consts =
 
 type where = [ `Conclusion | `Statement ]
 
-let sigmatch ~(dbd:Mysql.dbd) ?(facts=false) ?(where = `Conclusion)
+let sigmatch ~(dbd:HMysql.dbd) ?(facts=false) ?(where = `Conclusion)
  (main, constants)
 =
  let main,types =