sig
val disambiguate_term :
?fresh_instances:bool ->
- dbd:Mysql.dbd ->
+ dbd:HMysql.dbd ->
context:Cic.context ->
metasenv:Cic.metasenv ->
?initial_ugraph:CicUniv.universe_graph ->
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 *)
* 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 ->
(** @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 *)
* 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 ->
(* 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
hExtlib.cmo: hExtlib.cmi
hExtlib.cmx: hExtlib.cmi
+hMysql.cmo: hMysql.cmi
+hMysql.cmx: hMysql.cmi
PACKAGE = extlib
-REQUIRES =
+REQUIRES = mysql
PREDICATES =
INTERFACE_FILES = \
- hExtlib.mli
+ hExtlib.mli \
+ hMysql.mli
IMPLEMENTATION_FILES = \
$(INTERFACE_FILES:%.mli=%.ml)
EXTRA_OBJECTS_TO_INSTALL =
--- /dev/null
+(* 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
--- /dev/null
+(* 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
(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
*)
-type connection = MySQL_C of Mysql.dbd
+type connection = MySQL_C of HMysql.dbd
| Postgres_C of Postgres.connection
| No_C
(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
*)
-type connection = MySQL_C of Mysql.dbd
+type connection = MySQL_C of HMysql.dbd
| Postgres_C of Postgres.connection
| No_C
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 =
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
(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
*)
-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
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 =
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
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
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
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
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) ->
(* 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 =
(* 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 -> []
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 =
(** @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 ->
* @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 ->
(** @param where defaults to `Conclusion *)
val at_most:
- dbd:Mysql.dbd ->
+ dbd:HMysql.dbd ->
?where:where -> UriManagerSet.t ->
(UriManager.uri -> bool)
int * string list * string list
val exec:
- dbd:Mysql.dbd ->
+ dbd:HMysql.dbd ->
?rating:[ `Hits ] ->
int * string list * string list ->
UriManager.uri list
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
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 =
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
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
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
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;
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
-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 ] ->
]
;;
-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
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
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
| "" -> []
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")
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) =
(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
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:
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
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
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 "^^
(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 =
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
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
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)) =
(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
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
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
* 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 ->
(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 ->
((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
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
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 ->
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
projects / helm.git / commitdiff