From 259a4a2080cc5af5b20da1cd9133eb32f28c5d8f Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 23 Sep 2005 17:43:59 +0000 Subject: [PATCH] New module HMysql (to abstract over Mysql and make profiling easier). --- helm/ocaml/cic_disambiguation/disambiguate.ml | 4 +- .../ocaml/cic_disambiguation/disambiguate.mli | 6 +- helm/ocaml/cic_notation/grafiteAst.ml | 11 ++++ helm/ocaml/extlib/.depend | 2 + helm/ocaml/extlib/Makefile | 5 +- helm/ocaml/extlib/hMysql.ml | 57 +++++++++++++++++++ helm/ocaml/extlib/hMysql.mli | 48 ++++++++++++++++ helm/ocaml/mathql_interpreter/mQIConn.ml | 2 +- helm/ocaml/mathql_interpreter/mQIConn.mli | 2 +- helm/ocaml/mathql_interpreter/mQIMySql.ml | 6 +- helm/ocaml/mathql_interpreter/mQIMySql.mli | 6 +- helm/ocaml/metadata/metadataConstraints.ml | 26 ++++----- helm/ocaml/metadata/metadataConstraints.mli | 12 ++-- helm/ocaml/metadata/metadataDb.ml | 22 +++---- helm/ocaml/metadata/metadataDb.mli | 6 +- helm/ocaml/paramodulation/inference.ml | 2 +- helm/ocaml/paramodulation/inference.mli | 2 +- helm/ocaml/paramodulation/saturate_main.ml | 4 +- helm/ocaml/tactics/autoTactic.ml | 4 +- helm/ocaml/tactics/autoTactic.mli | 4 +- helm/ocaml/tactics/eliminationTactics.mli | 2 +- helm/ocaml/tactics/fwdSimplTactic.mli | 2 +- helm/ocaml/tactics/metadataQuery.ml | 24 ++++---- helm/ocaml/tactics/metadataQuery.mli | 20 +++---- helm/ocaml/tactics/tactics.mli | 6 +- 25 files changed, 202 insertions(+), 83 deletions(-) create mode 100644 helm/ocaml/extlib/hMysql.ml create mode 100644 helm/ocaml/extlib/hMysql.mli diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index 0679b9aee..05a15691e 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -631,7 +631,7 @@ module type Disambiguator = sig val disambiguate_term : ?fresh_instances:bool -> - dbd:Mysql.dbd -> + dbd:HMysql.dbd -> context:Cic.context -> metasenv:Cic.metasenv -> ?initial_ugraph:CicUniv.universe_graph -> @@ -646,7 +646,7 @@ sig val disambiguate_obj : ?fresh_instances:bool -> - dbd:Mysql.dbd -> + dbd:HMysql.dbd -> aliases:DisambiguateTypes.environment ->(* previous interpretation status *) universe:DisambiguateTypes.multiple_environment option -> uri:UriManager.uri option -> (* required only for inductive types *) diff --git a/helm/ocaml/cic_disambiguation/disambiguate.mli b/helm/ocaml/cic_disambiguation/disambiguate.mli index 1c6d4bbe7..356b5e117 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.mli +++ b/helm/ocaml/cic_disambiguation/disambiguate.mli @@ -39,7 +39,7 @@ sig * input AST will be ignored. Defaults to false. *) val disambiguate_term : ?fresh_instances:bool -> - dbd:Mysql.dbd -> + dbd:HMysql.dbd -> context:Cic.context -> metasenv:Cic.metasenv -> ?initial_ugraph:CicUniv.universe_graph -> @@ -55,7 +55,7 @@ sig (** @param fresh_instances as per disambiguate_term *) val disambiguate_obj : ?fresh_instances:bool -> - dbd:Mysql.dbd -> + dbd:HMysql.dbd -> aliases:DisambiguateTypes.environment ->(* previous interpretation status *) universe:DisambiguateTypes.multiple_environment option -> uri:UriManager.uri option -> (* required only for inductive types *) @@ -77,7 +77,7 @@ sig * choice from the user is needed to disambiguate the term * @raise Ambiguous_term for ambiguous term *) val disambiguate_string: - dbd:Mysql.dbd -> + dbd:HMysql.dbd -> ?context:Cic.context -> ?metasenv:Cic.metasenv -> ?initial_ugraph:CicUniv.universe_graph -> diff --git a/helm/ocaml/cic_notation/grafiteAst.ml b/helm/ocaml/cic_notation/grafiteAst.ml index f406c44a8..45f7c1aea 100644 --- a/helm/ocaml/cic_notation/grafiteAst.ml +++ b/helm/ocaml/cic_notation/grafiteAst.ml @@ -162,6 +162,17 @@ type ('term,'obj) command = (* DEBUGGING *) | Render of loc * UriManager.uri (* render library object *) +let reash_uris = + function + | Default (loc, name, uris) -> + let uris = + List.map + (fun uri -> UriManager.uri_of_string (UriManager.string_of_uri uri)) + uris + in + Default (loc, name, uris) + | cmd -> cmd + type ('term, 'lazy_term, 'reduction, 'ident) tactical = | Tactic of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic | Do of loc * int * ('term, 'lazy_term, 'reduction, 'ident) tactical diff --git a/helm/ocaml/extlib/.depend b/helm/ocaml/extlib/.depend index cbb3fcdfe..3ca72a4d9 100644 --- a/helm/ocaml/extlib/.depend +++ b/helm/ocaml/extlib/.depend @@ -1,2 +1,4 @@ hExtlib.cmo: hExtlib.cmi hExtlib.cmx: hExtlib.cmi +hMysql.cmo: hMysql.cmi +hMysql.cmx: hMysql.cmi diff --git a/helm/ocaml/extlib/Makefile b/helm/ocaml/extlib/Makefile index 6dccb5a90..703541520 100644 --- a/helm/ocaml/extlib/Makefile +++ b/helm/ocaml/extlib/Makefile @@ -1,9 +1,10 @@ PACKAGE = extlib -REQUIRES = +REQUIRES = mysql PREDICATES = INTERFACE_FILES = \ - hExtlib.mli + hExtlib.mli \ + hMysql.mli IMPLEMENTATION_FILES = \ $(INTERFACE_FILES:%.mli=%.ml) EXTRA_OBJECTS_TO_INSTALL = diff --git a/helm/ocaml/extlib/hMysql.ml b/helm/ocaml/extlib/hMysql.ml new file mode 100644 index 000000000..77d788ee2 --- /dev/null +++ b/helm/ocaml/extlib/hMysql.ml @@ -0,0 +1,57 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +type dbd = Mysql.dbd +type result = Mysql.result +type error_code = Mysql.error_code + +let profiler = HExtlib.profile "mysql" + +let quick_connect ?host ?database ?port ?password ?user () = + profiler.HExtlib.profile + (Mysql.quick_connect ?host ?database ?port ?password ?user) () + +let disconnect dbd = + profiler.HExtlib.profile Mysql.disconnect dbd + +let escape s = + profiler.HExtlib.profile Mysql.escape s + +let exec dbd s = + profiler.HExtlib.profile (Mysql.exec dbd) s + +let map res ~f = + let map f = Mysql.map res ~f in + profiler.HExtlib.profile map f + +let iter res ~f = + let iter f = Mysql.iter res ~f in + profiler.HExtlib.profile iter f + +let errno dbd = + profiler.HExtlib.profile Mysql.errno dbd + +let status dbd = + profiler.HExtlib.profile Mysql.status dbd diff --git a/helm/ocaml/extlib/hMysql.mli b/helm/ocaml/extlib/hMysql.mli new file mode 100644 index 000000000..df8ac0bbe --- /dev/null +++ b/helm/ocaml/extlib/hMysql.mli @@ -0,0 +1,48 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +type dbd +type result + +(* the exceptions raised are from the Mysql module *) + +val quick_connect : + ?host:string -> + ?database:string -> + ?port:int -> ?password:string -> ?user:string -> unit -> dbd + +val disconnect : Mysql.dbd -> unit + +val escape: string -> string + +val exec: dbd -> string -> result + +val map : result -> f:(string option array -> 'a) -> 'a list + +val iter : result -> f:(string option array -> unit) -> unit + +val errno : dbd -> Mysql.error_code + +val status : dbd -> Mysql.status diff --git a/helm/ocaml/mathql_interpreter/mQIConn.ml b/helm/ocaml/mathql_interpreter/mQIConn.ml index d4a0b067f..aaf16fac4 100644 --- a/helm/ocaml/mathql_interpreter/mQIConn.ml +++ b/helm/ocaml/mathql_interpreter/mQIConn.ml @@ -26,7 +26,7 @@ (* AUTOR: Ferruccio Guidi *) -type connection = MySQL_C of Mysql.dbd +type connection = MySQL_C of HMysql.dbd | Postgres_C of Postgres.connection | No_C diff --git a/helm/ocaml/mathql_interpreter/mQIConn.mli b/helm/ocaml/mathql_interpreter/mQIConn.mli index 94ea83f76..35c8b3ef0 100644 --- a/helm/ocaml/mathql_interpreter/mQIConn.mli +++ b/helm/ocaml/mathql_interpreter/mQIConn.mli @@ -26,7 +26,7 @@ (* AUTOR: Ferruccio Guidi *) -type connection = MySQL_C of Mysql.dbd +type connection = MySQL_C of HMysql.dbd | Postgres_C of Postgres.connection | No_C diff --git a/helm/ocaml/mathql_interpreter/mQIMySql.ml b/helm/ocaml/mathql_interpreter/mQIMySql.ml index 4a68c9398..46f350e21 100644 --- a/helm/ocaml/mathql_interpreter/mQIMySql.ml +++ b/helm/ocaml/mathql_interpreter/mQIMySql.ml @@ -38,10 +38,10 @@ let init () = HR.get_opt HR.get_int "mathql_interpreter.mysql_connection.port" in let password = HR.get_opt HR.get_string "mathql_interpreter.mysql_connection.password" in - try Mysql.quick_connect ?host ?database ?user ?port ?password () + try HMysql.quick_connect ?host ?database ?user ?port ?password () with _ -> raise (Failure "mqi_connecion") -let close c = Mysql.disconnect c +let close c = HMysql.disconnect c let quote s = let rec quote_aux s = @@ -56,7 +56,7 @@ let quote s = let exec (c, out) q = let g = function None -> "" | Some v -> v in let f a = List.map g (Array.to_list a) in - out q; Mysql.map ~f:f (Mysql.exec c q) + out q; HMysql.map ~f:f (Mysql.exec c q) let exec c table cols ct cfl = let rec iter f last sep = function diff --git a/helm/ocaml/mathql_interpreter/mQIMySql.mli b/helm/ocaml/mathql_interpreter/mQIMySql.mli index 36e8f18d9..8afaf401d 100644 --- a/helm/ocaml/mathql_interpreter/mQIMySql.mli +++ b/helm/ocaml/mathql_interpreter/mQIMySql.mli @@ -26,11 +26,11 @@ (* AUTOR: Ferruccio Guidi *) -val init : unit -> Mysql.dbd +val init : unit -> HMysql.dbd -val close : Mysql.dbd -> unit +val close : HMysql.dbd -> unit -val exec : Mysql.dbd * (MQITypes.query -> unit) -> +val exec : HMysql.dbd * (MQITypes.query -> unit) -> MQITypes.table -> MQITypes.columns -> string MQITypes.con_true -> string MQITypes.con_false -> MQITypes.result diff --git a/helm/ocaml/metadata/metadataConstraints.ml b/helm/ocaml/metadata/metadataConstraints.ml index d18663fad..6431513ff 100644 --- a/helm/ocaml/metadata/metadataConstraints.ml +++ b/helm/ocaml/metadata/metadataConstraints.ml @@ -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 = diff --git a/helm/ocaml/metadata/metadataConstraints.mli b/helm/ocaml/metadata/metadataConstraints.mli index 4f84ce9a7..63757ae47 100644 --- a/helm/ocaml/metadata/metadataConstraints.mli +++ b/helm/ocaml/metadata/metadataConstraints.mli @@ -36,17 +36,17 @@ type term_signature = (UriManager.uri * UriManager.uri list) option * UriManager (** @return sorted list of theorem URIs, first URIs in the least have higher * relevance *) -val cmatch: dbd:Mysql.dbd -> ?facts:bool -> Cic.term -> UriManager.uri list +val cmatch: dbd:HMysql.dbd -> ?facts:bool -> Cic.term -> UriManager.uri list (** as cmatch, but returned list is not sorted but rather tagged with * relevance information: higher the tag, higher the relevance *) -val cmatch': dbd:Mysql.dbd -> ?facts:bool -> Cic.term -> (int * UriManager.uri) list +val cmatch': dbd:HMysql.dbd -> ?facts:bool -> Cic.term -> (int * UriManager.uri) list type where = [ `Conclusion | `Statement ] (** signature matching extent *) (** @param where defaults to `Conclusion *) val sigmatch: - dbd:Mysql.dbd -> + dbd:HMysql.dbd -> ?facts:bool -> ?where:where -> term_signature -> @@ -78,7 +78,7 @@ val add_constraint: * @return list of URI satisfying given constraints *) val at_least: - dbd:Mysql.dbd -> + dbd:HMysql.dbd -> ?concl_card:cardinality_condition -> ?full_card:cardinality_condition -> ?diff:cardinality_condition -> @@ -88,7 +88,7 @@ val at_least: (** @param where defaults to `Conclusion *) val at_most: - dbd:Mysql.dbd -> + dbd:HMysql.dbd -> ?where:where -> UriManagerSet.t -> (UriManager.uri -> bool) @@ -101,7 +101,7 @@ val add_all_constr: int * string list * string list val exec: - dbd:Mysql.dbd -> + dbd:HMysql.dbd -> ?rating:[ `Hits ] -> int * string list * string list -> UriManager.uri list diff --git a/helm/ocaml/metadata/metadataDb.ml b/helm/ocaml/metadata/metadataDb.ml index 8d963bfc4..c5fbb79a8 100644 --- a/helm/ocaml/metadata/metadataDb.ml +++ b/helm/ocaml/metadata/metadataDb.ml @@ -55,21 +55,21 @@ let execute_insert dbd uri (sort_cols, rel_cols, obj_cols) = let query_sort = sprintf "INSERT %s VALUES %s;" (sort_tbl ()) (String.concat "," sort_tuples) in - ignore (Mysql.exec dbd query_sort) + ignore (HMysql.exec dbd query_sort) end; if rel_tuples <> [] then begin let query_rel = sprintf "INSERT %s VALUES %s;" (rel_tbl ()) (String.concat "," rel_tuples) in - ignore (Mysql.exec dbd query_rel) + ignore (HMysql.exec dbd query_rel) end; if obj_tuples <> [] then begin let query_obj = sprintf "INSERT %s VALUES %s;" (obj_tbl ()) (String.concat "," obj_tuples) in - ignore (Mysql.exec dbd query_obj) + ignore (HMysql.exec dbd query_obj) end @@ -109,7 +109,7 @@ let insert_const_no ~dbd l = let insert = sprintf "INSERT INTO %s VALUES %s" (count_tbl ()) (String.concat "," data) in - ignore (Mysql.exec dbd insert) + ignore (HMysql.exec dbd insert) let insert_name ~dbd l = let data = @@ -120,7 +120,7 @@ let insert_name ~dbd l = let insert = sprintf "INSERT INTO %s VALUES %s" (name_tbl ()) (String.concat "," data) in - ignore (Mysql.exec dbd insert) + ignore (HMysql.exec dbd insert) type columns = MetadataPp.t list list * MetadataPp.t list list * MetadataPp.t list list @@ -136,7 +136,7 @@ let eventually_analyze dbd = begin let analyze t = "OPTIMIZE TABLE " ^ t ^ ";" in List.iter - (fun table -> ignore (Mysql.exec dbd (analyze table))) + (fun table -> ignore (HMysql.exec dbd (analyze table))) [name_tbl (); rel_tbl (); sort_tbl (); obj_tbl(); count_tbl()] end @@ -157,11 +157,11 @@ let index_obj ~dbd ~uri = let tables_to_clean = [sort_tbl; rel_tbl; obj_tbl; name_tbl; count_tbl] -let clean ~(dbd:Mysql.dbd) = +let clean ~(dbd:HMysql.dbd) = let owned_uris = (* list of uris in list-of-columns format *) let query = sprintf "SELECT source FROM %s" (name_tbl ()) in - let result = Mysql.exec dbd query in - let uris = Mysql.map result (fun cols -> + let result = HMysql.exec dbd query in + let uris = HMysql.map result (fun cols -> match cols.(0) with | Some src -> src | None -> assert false) in @@ -173,7 +173,7 @@ let clean ~(dbd:Mysql.dbd) = sprintf "DELETE FROM %s WHERE source LIKE \"%s%%\"" (tbl ()) s in List.iter - (fun source_col -> ignore (Mysql.exec dbd (query source_col))) + (fun source_col -> ignore (HMysql.exec dbd (query source_col))) owned_uris in List.iter del_from tables_to_clean; @@ -185,7 +185,7 @@ let unindex ~dbd ~uri = let query tbl = sprintf "DELETE FROM %s WHERE source LIKE \"%s%%\"" (tbl ()) uri in - ignore (Mysql.exec dbd (query tbl)) + ignore (HMysql.exec dbd (query tbl)) in List.iter del_from tables_to_clean diff --git a/helm/ocaml/metadata/metadataDb.mli b/helm/ocaml/metadata/metadataDb.mli index d70ec4a34..86820aafb 100644 --- a/helm/ocaml/metadata/metadataDb.mli +++ b/helm/ocaml/metadata/metadataDb.mli @@ -25,15 +25,15 @@ -val index_obj: dbd:Mysql.dbd -> uri:UriManager.uri -> unit +val index_obj: dbd:HMysql.dbd -> uri:UriManager.uri -> unit (* TODO Zack indexing of variables and (perhaps?) incomplete proofs *) (** remove from the db all metadata pertaining to a given owner * @return list of uris removed from the db *) -val clean: dbd:Mysql.dbd -> string list +val clean: dbd:HMysql.dbd -> string list -val unindex: dbd:Mysql.dbd -> uri:UriManager.uri -> unit +val unindex: dbd:HMysql.dbd -> uri:UriManager.uri -> unit val count_distinct: [`Conclusion | `Hypothesis | `Statement ] -> diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml index 4f1b43bdb..8118c369a 100644 --- a/helm/ocaml/paramodulation/inference.ml +++ b/helm/ocaml/paramodulation/inference.ml @@ -1118,7 +1118,7 @@ let equations_blacklist = ] ;; -let find_library_equalities ~(dbd:Mysql.dbd) context status maxmeta = +let find_library_equalities ~(dbd:HMysql.dbd) context status maxmeta = let module C = Cic in let module S = CicSubstitution in let module T = CicTypeChecker in diff --git a/helm/ocaml/paramodulation/inference.mli b/helm/ocaml/paramodulation/inference.mli index 2011dd979..4bb43ea8f 100644 --- a/helm/ocaml/paramodulation/inference.mli +++ b/helm/ocaml/paramodulation/inference.mli @@ -108,5 +108,5 @@ val extract_differing_subterms: val build_proof_term: equality -> Cic.term val find_library_equalities: - dbd:Mysql.dbd -> Cic.context -> ProofEngineTypes.status -> int -> + dbd:HMysql.dbd -> Cic.context -> ProofEngineTypes.status -> int -> equality list * int diff --git a/helm/ocaml/paramodulation/saturate_main.ml b/helm/ocaml/paramodulation/saturate_main.ml index 9766b79f6..1870a5137 100644 --- a/helm/ocaml/paramodulation/saturate_main.ml +++ b/helm/ocaml/paramodulation/saturate_main.ml @@ -2,7 +2,7 @@ let configuration_file = ref "../../matita/matita.conf.xml";; let core_notation_script = "../../matita/core_notation.moo";; -let get_from_user ~(dbd:Mysql.dbd) = +let get_from_user ~(dbd:HMysql.dbd) = let rec get () = match read_line () with | "" -> [] @@ -52,7 +52,7 @@ in Helm_registry.load_from !configuration_file; CicNotation.load_notation core_notation_script; CicNotation.load_notation "../../matita/coq.moo"; -let dbd = Mysql.quick_connect +let dbd = HMysql.quick_connect ~host:(Helm_registry.get "db.host") ~user:(Helm_registry.get "db.user") ~database:(Helm_registry.get "db.database") diff --git a/helm/ocaml/tactics/autoTactic.ml b/helm/ocaml/tactics/autoTactic.ml index e89608cd4..a0835a9b8 100644 --- a/helm/ocaml/tactics/autoTactic.ml +++ b/helm/ocaml/tactics/autoTactic.ml @@ -279,7 +279,7 @@ let default_depth = 5 let default_width = 3 (* -let auto_tac ?(depth=default_depth) ?(width=default_width) ~(dbd:Mysql.dbd) +let auto_tac ?(depth=default_depth) ?(width=default_width) ~(dbd:HMysql.dbd) () = let auto_tac dbd (proof,goal) = @@ -311,7 +311,7 @@ let term_is_equality = ref (fun term -> debug_print (lazy "term_is_equality E` DUMMY!!!!"); false);; -let auto_tac ?(depth=default_depth) ?(width=default_width) ?paramodulation ~(dbd:Mysql.dbd) () = +let auto_tac ?(depth=default_depth) ?(width=default_width) ?paramodulation ~(dbd:HMysql.dbd) () = let auto_tac dbd (proof, goal) = let normal_auto () = let universe = MetadataQuery.signature_of_goal ~dbd (proof, goal) in diff --git a/helm/ocaml/tactics/autoTactic.mli b/helm/ocaml/tactics/autoTactic.mli index d9061c1ef..e2f20f787 100644 --- a/helm/ocaml/tactics/autoTactic.mli +++ b/helm/ocaml/tactics/autoTactic.mli @@ -26,11 +26,11 @@ val auto_tac: ?depth:int -> ?width:int -> ?paramodulation:string -> - dbd:Mysql.dbd -> unit -> + dbd:HMysql.dbd -> unit -> ProofEngineTypes.tactic val paramodulation_tactic: - (Mysql.dbd -> ProofEngineTypes.status -> + (HMysql.dbd -> ProofEngineTypes.status -> ProofEngineTypes.proof * ProofEngineTypes.goal list) ref val term_is_equality: diff --git a/helm/ocaml/tactics/eliminationTactics.mli b/helm/ocaml/tactics/eliminationTactics.mli index 5074f8134..cf6589f9a 100644 --- a/helm/ocaml/tactics/eliminationTactics.mli +++ b/helm/ocaml/tactics/eliminationTactics.mli @@ -30,4 +30,4 @@ val elim_type_tac: val decompose_tac: ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> ?user_types:((UriManager.uri * int) list) -> - dbd:Mysql.dbd -> string -> ProofEngineTypes.tactic + dbd:HMysql.dbd -> string -> ProofEngineTypes.tactic diff --git a/helm/ocaml/tactics/fwdSimplTactic.mli b/helm/ocaml/tactics/fwdSimplTactic.mli index e16bd5719..d75b83320 100644 --- a/helm/ocaml/tactics/fwdSimplTactic.mli +++ b/helm/ocaml/tactics/fwdSimplTactic.mli @@ -29,4 +29,4 @@ val lapply_tac: val fwd_simpl_tac: ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> - dbd:Mysql.dbd -> string -> ProofEngineTypes.tactic + dbd:HMysql.dbd -> string -> ProofEngineTypes.tactic diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml index ddeab3e6e..c266502cb 100644 --- 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 diff --git a/helm/ocaml/tactics/metadataQuery.mli b/helm/ocaml/tactics/metadataQuery.mli index b2bd57bf3..747844226 100644 --- a/helm/ocaml/tactics/metadataQuery.mli +++ b/helm/ocaml/tactics/metadataQuery.mli @@ -29,17 +29,17 @@ * is interpreted as 0 or more characters and "?" as exactly one character *) val signature_of_goal: - dbd:Mysql.dbd -> ProofEngineTypes.status -> UriManager.uri list + dbd:HMysql.dbd -> ProofEngineTypes.status -> UriManager.uri list val equations_for_goal: - dbd:Mysql.dbd -> ProofEngineTypes.status -> UriManager.uri list + dbd:HMysql.dbd -> ProofEngineTypes.status -> UriManager.uri list val locate: - dbd:Mysql.dbd -> + dbd:HMysql.dbd -> ?vars:bool -> string -> UriManager.uri list val experimental_hint: - dbd:Mysql.dbd -> + dbd:HMysql.dbd -> ?facts:bool -> ?signature:MetadataConstraints.term_signature -> ProofEngineTypes.status -> @@ -48,7 +48,7 @@ val experimental_hint: (ProofEngineTypes.proof * ProofEngineTypes.goal list))) list val new_experimental_hint: - dbd:Mysql.dbd -> + dbd:HMysql.dbd -> ?facts:bool -> ?signature:MetadataConstraints.term_signature -> universe:UriManager.uri list -> @@ -57,13 +57,13 @@ val new_experimental_hint: ((Cic.term -> Cic.term) * (ProofEngineTypes.proof * ProofEngineTypes.goal list))) list -val match_term: dbd:Mysql.dbd -> Cic.term -> UriManager.uri list +val match_term: dbd:HMysql.dbd -> Cic.term -> UriManager.uri list (** @param string is an uri *) -val elim: dbd:Mysql.dbd -> UriManager.uri -> UriManager.uri list +val elim: dbd:HMysql.dbd -> UriManager.uri -> UriManager.uri list -val instance: dbd:Mysql.dbd -> Cic.term -> UriManager.uri list +val instance: dbd:HMysql.dbd -> Cic.term -> UriManager.uri list -val fwd_simpl: dbd:Mysql.dbd -> Cic.term -> UriManager.uri list +val fwd_simpl: dbd:HMysql.dbd -> Cic.term -> UriManager.uri list -val decomposables: dbd:Mysql.dbd -> (UriManager.uri * int) list +val decomposables: dbd:HMysql.dbd -> (UriManager.uri * int) list diff --git a/helm/ocaml/tactics/tactics.mli b/helm/ocaml/tactics/tactics.mli index 5ac63b07e..8ea9f641c 100644 --- a/helm/ocaml/tactics/tactics.mli +++ b/helm/ocaml/tactics/tactics.mli @@ -5,7 +5,7 @@ val assumption : ProofEngineTypes.tactic val auto : ?depth:int -> ?width:int -> - ?paramodulation:string -> dbd:Mysql.dbd -> unit -> ProofEngineTypes.tactic + ?paramodulation:string -> dbd:HMysql.dbd -> unit -> ProofEngineTypes.tactic val change : pattern:ProofEngineTypes.pattern -> ProofEngineTypes.lazy_term -> ProofEngineTypes.tactic @@ -21,7 +21,7 @@ val decide_equality : ProofEngineTypes.tactic val decompose : ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> ?user_types:(UriManager.uri * int) list -> - dbd:Mysql.dbd -> string -> ProofEngineTypes.tactic + dbd:HMysql.dbd -> string -> ProofEngineTypes.tactic val discriminate : term:Cic.term -> ProofEngineTypes.tactic val elim_intros : ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> @@ -42,7 +42,7 @@ val fold : val fourier : ProofEngineTypes.tactic val fwd_simpl : ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> - dbd:Mysql.dbd -> string -> ProofEngineTypes.tactic + dbd:HMysql.dbd -> string -> ProofEngineTypes.tactic val generalize : ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> ProofEngineTypes.pattern -> ProofEngineTypes.tactic -- 2.39.2