New module HMysql (to abstract over Mysql and make profiling easier).

[helm.git] / helm / ocaml / tactics / metadataQuery.ml

diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index ddeab3e6e685892cda6ada1eab64db1cfdc0473a..c266502cb16fa50378252228c2f3c7af2e9dea7c 100644 (file)
--- a/helm/ocaml/tactics/metadataQuery.ml
+++ b/helm/ocaml/tactics/metadataQuery.ml
@@ -48,7 +48,7 @@ let sqlpat_of_shellglob =
 
 let nonvar uri = not (UriManager.uri_is_var uri)
 
-let locate ~(dbd:Mysql.dbd) ?(vars = false) pat =
+let locate ~(dbd:HMysql.dbd) ?(vars = false) pat =
   let sql_pat = sqlpat_of_shellglob pat in
   let query =
         sprintf ("SELECT source FROM %s WHERE value LIKE \"%s\" UNION "^^
@@ -56,12 +56,12 @@ let locate ~(dbd:Mysql.dbd) ?(vars = false) pat =
           (MetadataTypes.name_tbl ()) sql_pat
            MetadataTypes.library_name_tbl sql_pat
   in
-  let result = Mysql.exec dbd query in
+  let result = HMysql.exec dbd query in
   List.filter nonvar
-    (Mysql.map result
+    (HMysql.map result
       (fun cols -> match cols.(0) with Some s -> UriManager.uri_of_string s | _ -> assert false))
 
-let match_term ~(dbd:Mysql.dbd) ty =
+let match_term ~(dbd:HMysql.dbd) ty =
 (*   debug_print (lazy (CicPp.ppterm ty)); *)
   let metadata = MetadataExtractor.compute ~body:None ~ty in
   let constants_no =
@@ -236,7 +236,7 @@ let cmatch' =
  fun ~dbd ~facts signature -> profiler.profile (Constr.cmatch' ~dbd ~facts) signature
 *) let apply_tac_verbose = PrimitiveTactics.apply_tac_verbose let cmatch' = Constr.cmatch'
 
-let signature_of_goal ~(dbd:Mysql.dbd) ((proof, goal) as status) =
+let signature_of_goal ~(dbd:HMysql.dbd) ((proof, goal) as status) =
  let (_, metasenv, _, _) = proof in
  let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
  let main, sig_constants = Constr.signature_of ty in
@@ -254,7 +254,7 @@ let signature_of_goal ~(dbd:Mysql.dbd) ((proof, goal) as status) =
  let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in
   uris
 
-let equations_for_goal ~(dbd:Mysql.dbd) ((proof, goal) as status) =
+let equations_for_goal ~(dbd:HMysql.dbd) ((proof, goal) as status) =
  let (_, metasenv, _, _) = proof in
  let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
  let main, sig_constants = Constr.signature_of ty in
@@ -275,7 +275,7 @@ let equations_for_goal ~(dbd:Mysql.dbd) ((proof, goal) as status) =
        else raise Goal_is_not_an_equation
 
 let experimental_hint 
-  ~(dbd:Mysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) =
+  ~(dbd:HMysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) =
   let (_, metasenv, _, _) = proof in
   let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
   let (uris, (main, sig_constants)) =
@@ -357,7 +357,7 @@ let experimental_hint
     (aux uris)
 
 let new_experimental_hint 
-  ~(dbd:Mysql.dbd) ?(facts=false) ?signature ~universe
+  ~(dbd:HMysql.dbd) ?(facts=false) ?signature ~universe
   ((proof, goal) as status)
 =
   let (_, metasenv, _, _) = proof in
@@ -583,10 +583,10 @@ let fwd_simpl ~dbd t =
         let from = "genLemma" in
         let where =
           Printf.sprintf "h_outer = \"%s\""
-           (Mysql.escape (UriManager.string_of_uri outer)) in
+           (HMysql.escape (UriManager.string_of_uri outer)) in
          let query = Printf.sprintf "SELECT %s FROM %s WHERE %s" select from where in
-        let result = Mysql.exec dbd query in
-         let lemmas = Mysql.map ~f:(map inners) result in
+        let result = HMysql.exec dbd query in
+         let lemmas = HMysql.map ~f:(map inners) result in
         let ranked = List.fold_left rank [] lemmas in
         let ordered = List.rev (List.fast_sort compare ranked) in
          map_filter filter 0 ordered
@@ -604,5 +604,5 @@ let decomposables ~dbd =
    in
    let select, from = "source", "decomposables" in
    let query = Printf.sprintf "SELECT %s FROM %s" select from in
-   let decomposables = Mysql.map ~f:map (Mysql.exec dbd query) in
+   let decomposables = HMysql.map ~f:map (HMysql.exec dbd query) in
    map_filter (fun _ x -> x) 0 decomposables