TEST_REQUIRES = \
helm-registry \
- helm-mathql_interpreter \
- helm-mathql_generator \
helm-tactics \
helm-cic_transformations \
helm-cic_textual_parser2 \
+ helm-mathql_interpreter \
+ helm-mathql_generator \
helm-xmldiff \
lablgtk2 \
mathml-editor \
lablgtkmathview \
- dbi.mysql
+ mysql
REQUIRES = $(TEST_REQUIRES) gdome2-xslt helm-hbugs lablgtk2.init lablgtk2.glade
functor (C : DisambiguateTypes.Callbacks) ->
sig
val term_editor :
- dbh:Dbi.connection ->
+ dbd:Mysql.dbd ->
?packing:(GObj.widget -> unit) ->
?width:int ->
?height:int ->
module Make (C : DisambiguateTypes.Callbacks) =
struct
- let disambiguate_term ~(dbh:Dbi.connection) context metasenv term_as_string
+ let disambiguate_term ~(dbd:Mysql.dbd) context metasenv term_as_string
aliases
=
let module Disambiguate' = Disambiguate.Make (C) in
let term =
CicTextualParser2.parse_term (Stream.of_string term_as_string)
in
- Disambiguate'.disambiguate_term ~dbh context metasenv term ~aliases
+ Disambiguate'.disambiguate_term ~dbd context metasenv term ~aliases
end
end
module Make (C : DisambiguateTypes.Callbacks) :
sig
val disambiguate_term :
- dbh:Dbi.connection ->
+ dbd:Mysql.dbd ->
Cic.context ->
Cic.metasenv ->
string ->
<key name="per_user_work_directory">/home/sacerdot/helm/local_stuff</key>
<!-- The URL of the host of the Getter and UWOBO -->
- <!-- <key name="daemons_host">http://mowgli.cs.unibo.it</key> -->
- <key name="daemons_host">http://localhost</key>
+ <key name="daemons_host">http://mowgli.cs.unibo.it</key>
</section>
<!-- From now on it is unlikely that something needs to be changed -->
+ <section name="db">
+ <key name="host">mowgli.cs.unibo.it</key>
+ <key name="user">helm</key>
+ <key name="database">mowgli</key>
+ </section>
<section name="mathql_interpreter">
<key name="db_map">mathql_db_map.txt</key>
<section name="mysql_connection">
open Printf
-(* DEBUGGING *)
-
module MQI = MQueryInterpreter
module MQIC = MQIConn
module MQGT = MQGTypes
module MQGU = MQGUtil
module MQG = MQueryGenerator
-module DB = Dbi_mysql
-
(* first of all let's initialize the Helm_registry *)
let _ =
let configuration_file = "gTopLevel.conf.xml" in
(* GLOBAL CONSTANTS *)
-let mqi_debug_fun s = debug_print ~level:2 s
-let mqi_handle = MQIC.init_if_connected ~log:mqi_debug_fun ()
-let dbh = new DB.connection ~host:"mowgli.cs.unibo.it" ~user:"helm" "mowgli"
+let mqi_handle = MQIC.init_if_connected ()
+
+let dbd =
+ Mysql.quick_connect
+ ~host:(Helm_registry.get "db.host")
+ ~user:(Helm_registry.get "db.user")
+ ~database:(Helm_registry.get "db.database")
+ ()
let xlinkns = Gdome.domString "http://www.w3.org/1999/xlink";;
let decompose_uris_choice_callback = decompose_uris_choice_callback
let mk_fresh_name_callback = mk_fresh_name_callback
let mqi_handle = mqi_handle
- let dbh = dbh
+ let dbd = dbd
end
;;
module InvokeTactics' = InvokeTactics.Make (InvokeTacticsCallbacks);;
;;
let locate_callback id =
- let uris = MetadataQuery.locate ~dbh id in
+ let uris = MetadataQuery.locate ~dbd id in
HelmLogger.log (`Msg (`T ("Locate Query: " ^ id))) ;
HelmLogger.log (`Msg (`T "Result:")) ;
List.iter (fun uri -> HelmLogger.log (`Msg (`T uri))) uris;
~packing:(vbox#pack ~expand:true ~padding:0) () in
let newinputt =
TermEditor'.term_editor
- ~dbh
+ ~dbd
~width:400 ~height:20 ~packing:scrolled_window#add
~share_environment_with:inputt ()
~isnotempty_callback:
~packing:(vbox#pack ~expand:true ~padding:0) () in
let newinputt =
TermEditor'.term_editor
- ~dbh
+ ~dbd
~width:400 ~height:20 ~packing:scrolled_window#add
~share_environment_with:inputt ()
~isnotempty_callback:
(* moved here to have visibility of the ok button *)
let newinputt =
TermEditor'.term_editor
- ~dbh
+ ~dbd
~width:400 ~height:100 ~packing:scrolled_window#add
~share_environment_with:inputt ()
~isnotempty_callback:
match !ProofEngine.goal with
| None -> ()
| Some metano ->
- let uris' = List.map fst (MetadataQuery.hint ~dbh (proof, metano)) in
+ let uris' = List.map fst (MetadataQuery.hint ~dbd (proof, metano)) in
let uri' =
user_uri_choice ~title:"Ambiguous input."
~msg: "Many lemmas can be successfully applied. Please, choose one:"
~packing:frame#add () in
let inputt =
TermEditor'.term_editor
- ~dbh
+ ~dbd
~width:400 ~height:100 ~packing:scrolled_window1#add ()
~isnotempty_callback:
(function b ->
(UriManager.uri * int * 'b list) list
val mk_fresh_name_callback : ProofEngineTypes.mk_fresh_name_type
val mqi_handle : MQIConn.handle
- val dbh: Dbi.connection
+ val dbd:Mysql.dbd
end
;;
(ProofEngine.intros ~mk_fresh_name_callback:C.mk_fresh_name_callback)
let exact = call_tactic_with_input ProofEngine.exact
let apply = call_tactic_with_input ProofEngine.apply
- let auto = call_tactic (ProofEngine.auto C.dbh)
+ let auto = call_tactic (ProofEngine.auto ~dbd:C.dbd)
let elimintrossimpl = call_tactic_with_input ProofEngine.elim_intros_simpl
let elimtype = call_tactic_with_input ProofEngine.elim_type
let whd = call_tactic_with_goal_inputs ProofEngine.whd
(UriManager.uri * int * 'b list) list
val mk_fresh_name_callback : ProofEngineTypes.mk_fresh_name_type
val mqi_handle : MQIConn.handle
- val dbh : Dbi.connection
+ val dbd:Mysql.dbd
end
module type Tactics =
let elim_type term = apply_tactic (EliminationTactics.elim_type_tac ~term)
let ring () = apply_tactic Ring.ring_tac
let fourier () = apply_tactic FourierR.fourier_tac
-let auto dbh () = apply_tactic (VariousTactics.auto_tac ~dbh)
+let auto ~dbd () = apply_tactic (VariousTactics.auto_tac ~dbd)
let rewrite_simpl term = apply_tactic (EqualityTactics.rewrite_simpl_tac ~term)
let rewrite_back_simpl term = apply_tactic (EqualityTactics.rewrite_back_simpl_tac ~term)
val rewrite_simpl : Cic.term -> unit
val rewrite_back_simpl : Cic.term -> unit
val replace : goal_input:Cic.term -> input:Cic.term -> unit
-(* val auto : MQIConn.handle -> unit -> unit *)
-val auto : Dbi.connection -> unit -> unit
+val auto : dbd:Mysql.dbd -> unit -> unit
val reflexivity : unit -> unit
val symmetry : unit -> unit
module Disambiguate' = DisambiguatingParser.Make(C);;
- class term_editor_impl ~(dbh:Dbi.connection) ?packing ?width ?height
+ class term_editor_impl ~(dbd:Mysql.dbd) ?packing ?width ?height
?isnotempty_callback ?share_environment_with () : term_editor
=
let environment =
in
let environment',metasenv,expr =
match
- Disambiguate'.disambiguate_term ~dbh context metasenv
+ Disambiguate'.disambiguate_term ~dbd context metasenv
(input#buffer#get_text ()) !environment
with
[environment',metasenv,expr] -> environment',metasenv,expr
module Make (C : DisambiguateTypes.Callbacks) :
sig
val term_editor :
- dbh:Dbi.connection ->
+ dbd:Mysql.dbd ->
?packing:(GObj.widget -> unit) ->
?width:int ->
?height:int ->
(ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses);
(* self#load_doc ~dom:mml ;
current_mml <- Some mml ; *)
-Misc.domImpl#saveDocumentToFile ~name:"/tmp/prova" ~doc:mml () ;
+ ignore(Misc.domImpl#saveDocumentToFile ~name:"/tmp/prova" ~doc:mml ());
(match current_mml with
None ->
let time1 = Sys.time () in
module Disambiguate' = DisambiguatingParser.Make(C);;
class term_editor_impl
- ~dbh
+ ~dbd
?packing ?width ?height
?isnotempty_callback ?share_environment_with () : term_editor
=
debug_print ("TexTermEditor: Raw Tex: " ^ (Mathml_editor.get_tex tex_editor)) ;
let environment',metasenv,expr =
match
- Disambiguate'.disambiguate_term ~dbh
+ Disambiguate'.disambiguate_term ~dbd
context metasenv (Mathml_editor.get_tex tex_editor) !environment
with
[environment',metasenv,expr] -> environment',metasenv,expr
module Make (C : DisambiguateTypes.Callbacks) :
sig
val term_editor :
- dbh:Dbi.connection ->
+ dbd:Mysql.dbd ->
?packing:(GObj.widget -> unit) ->
?width:int ->
?height:int ->
-requires="dbi helm-cic_proof_checking"
+requires="mysql helm-cic_proof_checking"
version="0.0.1"
archive(byte)="metadata.cma"
archive(native)="metadata.cmxa"
module Make (C: Callbacks) =
struct
- let choices_of_id dbh id =
- let uris = MetadataQuery.locate ~dbh id in
+ let choices_of_id dbd id =
+ let uris = MetadataQuery.locate ~dbd id in
let uris =
match uris with
| [] ->
fun _ _ _ -> term))
uris
- let disambiguate_term ~(dbh:Dbi.connection) context metasenv term
+ let disambiguate_term ~(dbd:Mysql.dbd) context metasenv term
~aliases:current_env
=
debug_print "NEW DISAMBIGUATE INPUT";
(try
Hashtbl.find id_choices id
with Not_found ->
- let choices = choices_of_id dbh id in
+ let choices = choices_of_id dbd id in
Hashtbl.add id_choices id choices;
choices)
| Symbol (symb, _) -> DisambiguateChoices.lookup_symbol_choices symb
module Make (C : Callbacks) :
sig
val disambiguate_term :
- dbh:Dbi.connection ->
+ dbd:Mysql.dbd ->
Cic.context ->
Cic.metasenv ->
CicAst.term ->
PACKAGE = metadata
-REQUIRES = dbi helm-cic_proof_checking
+REQUIRES = mysql helm-cic_proof_checking
PREDICATES =
INTERFACE_FILES = \
all:
test: test.ml $(PACKAGE).cma
- $(OCAMLFIND) ocamlc -thread -package dbi.mysql,helm-metadata -linkpkg -o $@ $<
+ $(OCAMLFIND) ocamlc -thread -package mysql,helm-metadata -linkpkg -o $@ $<
test_query: test_query.ml $(PACKAGE).cma
- $(OCAMLFIND) ocamlc -thread -package dbi.mysql,helm-metadata -linkpkg -o $@ $<
+ $(OCAMLFIND) ocamlc -thread -package mysql,helm-metadata -linkpkg -o $@ $<
include ../Makefile.common
else [sprintf "table0.source = %s.source" cur_tbl]) @
where))
-let at_least ~(dbh:Dbi.connection) ?concl_card ?full_card
+let at_least ~(dbd:Mysql.dbd) ?concl_card ?full_card
(metadata: MetadataTypes.constr list)
=
if (metadata = []) && concl_card = None && full_card = None then
let from = String.concat ", " from in
let where = String.concat " and " where in
let query = sprintf "select table0.source from %s where %s" from where in
- let query = dbh#prepare query in
- query#execute [];
- List.map (function [`String s] -> s | _ -> assert false) (query#fetchall ())
+ let result = Mysql.exec dbd query in
+ Mysql.map result
+ (fun row -> match row.(0) with Some s -> s | _ -> assert false)
(** Prefix handling *)
let escape = Str.global_replace (Str.regexp_string "\'") "\\'"
-let get_constants (dbh:Dbi.connection) ~where uri =
+let get_constants (dbd:Mysql.dbd) ~where uri =
let uri = escape uri in
let positions =
match where with
"\"MainHypothesis\""]
in
let query =
- dbh#prepare
- (sprintf "select h_occurrence from refObj where source=\"%s\" and (%s)"
- uri (String.concat " or " positions))
+ sprintf "select h_occurrence from refObj where source=\"%s\" and (%s)"
+ uri (String.concat " or " positions)
in
- query#execute [];
- query#fold_left (* transform the result in a set *)
- (fun set fields ->
- let uri = match fields with [`String uri] -> uri | _ -> assert false in
- StringSet.add uri set)
- StringSet.empty
-
-let at_most ~(dbh:Dbi.connection) ?(where = `Conclusion) only u =
- let inconcl = get_constants dbh ~where u in
+ let result = Mysql.exec dbd query in
+ let set = ref StringSet.empty in
+ Mysql.iter result
+ (fun col ->
+ match col.(0) with
+ | Some uri -> set := StringSet.add uri !set
+ | _ -> assert false);
+ !set
+
+let at_most ~(dbd:Mysql.dbd) ?(where = `Conclusion) only u =
+ let inconcl = get_constants dbd ~where u in
StringSet.subset inconcl only
(* Special handling of equality. The problem is filtering out theorems just
0,"cic:/Coq/Init/Logic/f_equal2.con";
0,"cic:/Coq/Init/Logic/f_equal3.con"]
-let compute_exactly ~(dbh:Dbi.connection) where main prefixes =
+let compute_exactly ~(dbd:Mysql.dbd) where main prefixes =
List.concat
(List.map
(fun (m,s) ->
let res =
let must = must_of_prefix ~where main s in
match where with
- | `Conclusion -> at_least ~dbh ~concl_card:(Eq (m+1)) must
- | `Statement -> at_least ~dbh ~full_card:(Eq (m+1)) must
+ | `Conclusion -> at_least ~dbd ~concl_card:(Eq (m+1)) must
+ | `Statement -> at_least ~dbd ~full_card:(Eq (m+1)) must
in
List.map (fun uri -> (m, uri)) res)
prefixes)
(* critical value reached, fallback to "only" constraints *)
-let compute_with_only ~(dbh:Dbi.connection) ?(where = `Conclusion) main
+let compute_with_only ~(dbd:Mysql.dbd) ?(where = `Conclusion) main
prefixes constants
=
let max_prefix_length =
let must = must_of_prefix ~where main s in
(let res =
match where with
- | `Conclusion -> at_least ~dbh ~concl_card:(Gt (m+1)) must
- | `Statement -> at_least ~dbh ~full_card:(Gt (m+1)) must
+ | `Conclusion -> at_least ~dbd ~concl_card:(Gt (m+1)) must
+ | `Statement -> at_least ~dbd ~full_card:(Gt (m+1)) must
in
(* we tag the uri with m+1, for sorting purposes *)
List.map (fun uri -> (m+1, uri)) res))
maximal_prefixes)
in
- List.filter (function (_,uri) -> at_most ~dbh ~where constants uri) all in
- let equal_to = compute_exactly ~dbh where main prefixes in
+ List.filter (function (_,uri) -> at_most ~dbd ~where constants uri) all in
+ let equal_to = compute_exactly ~dbd where main prefixes in
greater_than @ equal_to
(* real match query implementation *)
-let cmatch ~(dbh:Dbi.connection) t =
+let cmatch ~(dbd:Mysql.dbd) t =
let (main, constants) = signature_of t in
match main with
| None -> []
let all_constants =
List.fold_right StringSet.add types (StringSet.add main constants)
in
- compute_with_only ~dbh main all_concl all_constants
+ compute_with_only ~dbd main all_concl all_constants
| _, _ -> [])
else
(* in this case we compute all prefixes, and we do not need
(List.map
(fun (m,s) ->
let must = must_of_prefix ~where:`Conclusion main s in
- let res = at_least ~dbh ~concl_card:(Eq (m+1)) must in
+ let res = at_least ~dbd ~concl_card:(Eq (m+1)) must in
List.map (fun uri -> (m, uri)) res)
all_concl)
| _, _ -> [])
type where = [ `Conclusion | `Statement ]
-let sigmatch ~(dbh:Dbi.connection) ?(where = `Conclusion) (main, constants) =
+let sigmatch ~(dbd:Mysql.dbd) ?(where = `Conclusion) (main, constants) =
match main with
None -> []
| Some (main, types) ->
let all_constants =
List.fold_right StringSet.add types (StringSet.add main constants)
in
- compute_with_only ~dbh ~where main subsets all_constants
+ compute_with_only ~dbd ~where main subsets all_constants
else
let subsets =
let subsets = power constants in
let types_no = List.length types in
(0,[]) :: List.map (function (n,l) -> (n+types_no,types@l)) subsets
in
- compute_exactly ~dbh where main subsets
+ compute_exactly ~dbd where main subsets
(* match query wrappers *)
let cmatch' = cmatch
-let cmatch ~dbh term =
+let cmatch ~dbd term =
List.map snd
(List.sort
(fun x y -> Pervasives.compare (fst y) (fst x))
- (cmatch' ~dbh term))
+ (cmatch' ~dbd term))
let constants_of = signature_concl
(** @return sorted list of theorem URIs, first URIs in the least have higher
* relevance *)
-val cmatch: dbh:Dbi.connection -> Cic.term -> string list
+val cmatch: dbd:Mysql.dbd -> Cic.term -> string list
(** as cmatch, but returned list is not sorted but rather tagged with
* relevance information: higher the tag, higher the relevance *)
-val cmatch': dbh:Dbi.connection -> Cic.term -> (int * string) list
+val cmatch': dbd:Mysql.dbd -> Cic.term -> (int * string) list
type where = [ `Conclusion | `Statement ] (** signature matching extent *)
(** @param where defaults to `Conclusion *)
val sigmatch:
- dbh:Dbi.connection ->
+ dbd:Mysql.dbd ->
?where:where -> term_signature ->
(int * string) list
* @param full_card cardinality condition on the whole statement
* @return list of URI satisfying given constraints *)
val at_least:
- dbh:Dbi.connection ->
+ dbd:Mysql.dbd ->
?concl_card:cardinality_condition ->
?full_card:cardinality_condition ->
MetadataTypes.constr list ->
(** @param where defaults to `Conclusion *)
val at_most:
- dbh:Dbi.connection ->
+ dbd:Mysql.dbd ->
?where:where -> StringSet.t ->
(string -> bool)
open Printf
-let prepare_insert (dbh: Dbi.connection) =
- let insert_owner =
- dbh#prepare (sprintf "INSERT INTO %s VALUES (\"?\",\"?\")" owners_tbl)
+let prepare_insert () =
+ let insert_owner a b =
+ sprintf "INSERT %s VALUES (\"%s\", \"%s\")" owners_tbl a b
in
- let insert_sort =
- dbh#prepare (sprintf "INSERT INTO %s VALUES (\"?\",\"?\",?,\"?\")" sort_tbl)
+ let insert_sort a b c d =
+ sprintf "INSERT %s VALUES (\"%s\", \"%s\", %d, \"%s\")" sort_tbl a b c d
in
- let insert_rel =
- dbh#prepare (sprintf "INSERT INTO %s VALUES (\"?\",\"?\",?)" rel_tbl)
+ let insert_rel a b c =
+ sprintf "INSERT %s VALUES (\"%s\", \"%s\", %d)" rel_tbl a b c
in
- let insert_obj =
- dbh#prepare (sprintf "INSERT INTO %s VALUES (\"?\",\"?\",\"?\",?)" obj_tbl)
+ let insert_obj a b c d =
+ sprintf "INSERT %s VALUES (\"%s\", \"%s\", \"%s\", %s)" obj_tbl a b c d
in
(insert_owner, insert_sort, insert_rel, insert_obj)
-let execute_insert dbh (insert_owner, insert_sort, insert_rel, insert_obj)
+let execute_insert dbd (insert_owner, insert_sort, insert_rel, insert_obj)
uri owner (sort_cols, rel_cols, obj_cols)
=
- insert_owner#execute [`String uri; `String owner];
- List.iter insert_sort#execute sort_cols;
- List.iter insert_rel#execute rel_cols;
- List.iter insert_obj#execute obj_cols
+ ignore (Mysql.exec dbd (insert_owner uri owner));
+ List.iter (function
+ | [`String a; `String b; `Int c; `String d] ->
+ ignore (Mysql.exec dbd (insert_sort a b c d))
+ | _ -> assert false)
+ sort_cols;
+ List.iter (function
+ | [`String a; `String b; `Int c] ->
+ ignore (Mysql.exec dbd (insert_rel a b c))
+ | _ -> assert false)
+ rel_cols;
+ List.iter (function
+ | [`String a; `String b; `String c; `Int d] ->
+ ignore (Mysql.exec dbd (insert_obj a b c (string_of_int d)))
+ | [`String a; `String b; `String c; `Null] ->
+ ignore (Mysql.exec dbd (insert_obj a b c "NULL"))
+ | _ -> assert false)
+ obj_cols
-let insert_const_no dbh uri =
+let insert_const_no dbd uri =
let inconcl_no =
- sprintf "INSERT INTO %s SELECT \"%s\", COUNT(DISTINCT h_occurrence) FROM %s WHERE (h_position=\"%s\" OR h_position=\"%s\") AND source LIKE \"%s%%\""
+ sprintf "INSERT %s SELECT \"%s\", COUNT(DISTINCT h_occurrence) FROM %s WHERE (h_position=\"%s\" OR h_position=\"%s\") AND source LIKE \"%s%%\""
conclno_tbl uri obj_tbl inconcl_pos mainconcl_pos uri
in
let concl_hyp =
- sprintf "INSERT INTO %s
+ sprintf "INSERT %s
SELECT \"%s\",COUNT(DISTINCT h_occurrence)
FROM %s
WHERE NOT (h_position=\"%s\") AND (source = \"%s\")"
conclno_hyp_tbl uri obj_tbl inbody_pos uri
in
- (dbh#prepare inconcl_no)#execute [];
- (dbh#prepare concl_hyp)#execute []
+ ignore (Mysql.exec dbd inconcl_no);
+ ignore (Mysql.exec dbd concl_hyp)
-let insert_name ~dbh ~uri ~name =
+let insert_name ~dbd ~uri ~name =
let query =
- dbh#prepare
- (sprintf "INSERT INTO %s VALUES (\"%s\", \"%s\")" name_tbl uri name)
+ sprintf "INSERT %s VALUES (\"%s\", \"%s\")" name_tbl uri name
in
- query#execute []
+ ignore (Mysql.exec dbd query)
-type dbi_columns =
- Dbi.sql_t list list * Dbi.sql_t list list * Dbi.sql_t list list
+type columns =
+ MetadataPp.t list list * MetadataPp.t list list * MetadataPp.t list list
-let index_constant ~dbh =
- let query = prepare_insert dbh in
+let index_constant ~dbd =
+ let query = prepare_insert () in
fun ~owner ~uri ~body ~ty ->
let name = UriManager.name_of_uri uri in
let uri = UriManager.string_of_uri uri in
let metadata = MetadataExtractor.compute ~body ~ty in
let columns = MetadataPp.columns_of_metadata ~about:uri metadata in
- execute_insert dbh query uri owner (columns :> dbi_columns);
- insert_const_no dbh uri;
- insert_name ~dbh ~uri ~name
+ execute_insert dbd query uri owner (columns :> columns);
+ insert_const_no dbd uri;
+ insert_name ~dbd ~uri ~name
-let index_inductive_def ~dbh =
- let query = prepare_insert dbh in
+let index_inductive_def ~dbd =
+ let query = prepare_insert () in
fun ~owner ~uri ~types ->
let metadata = MetadataExtractor.compute_ind ~uri ~types in
let uri_of (a,b,c) = a in
let uris = UriManager.string_of_uri uri :: List.map uri_of metadata in
let uri = UriManager.string_of_uri uri in
let columns = MetadataPp.columns_of_ind_metadata metadata in
- execute_insert dbh query uri owner (columns :> dbi_columns);
- List.iter (insert_const_no dbh) uris;
- List.iter (fun (uri, name, _) -> insert_name ~dbh ~uri ~name) metadata
+ execute_insert dbd query uri owner (columns :> columns);
+ List.iter (insert_const_no dbd) uris;
+ List.iter (fun (uri, name, _) -> insert_name ~dbd ~uri ~name) metadata
-let clean ~(dbh: Dbi.connection) ~owner =
+let clean ~(dbd:Mysql.dbd) ~owner =
let owned_uris = (* list of uris in list-of-columns format *)
let query =
- dbh#prepare (sprintf
- "SELECT source FROM %s WHERE owner = \"%s\"" owners_tbl owner)
+ sprintf "SELECT source FROM %s WHERE owner = \"%s\"" owners_tbl owner
in
- query#execute [];
- List.map
- (function [`String source_col] -> source_col | _ -> assert false)
- (query#fetchall ())
+ let result = Mysql.exec dbd query in
+ Mysql.map result (fun cols ->
+ match cols.(0) with
+ | Some src -> src
+ | None -> assert false)
in
let del_from tbl =
- let query =
- dbh#prepare (sprintf "DELETE FROM %s WHERE source LIKE \"?%%\"" tbl)
- in
- List.iter (fun source_col -> query#execute [`String source_col]) owned_uris
+ let query s = sprintf "DELETE FROM %s WHERE source LIKE \"%s%%\"" tbl s in
+ List.iter
+ (fun source_col -> ignore (Mysql.exec dbd (query source_col)))
+ owned_uris
in
List.iter del_from
[sort_tbl; rel_tbl; obj_tbl; conclno_tbl; conclno_hyp_tbl; name_tbl;
*)
(** index a Cic.Constant object and insert resulting metadata into the db
- * PRE_EVAL(dbh) *)
+ * PRE_EVAL(dbd) *)
val index_constant:
- dbh:Dbi.connection ->
+ dbd:Mysql.dbd ->
owner:string ->
uri:UriManager.uri -> body:Cic.term option -> ty:Cic.term ->
unit
(** index a Cic.InductiveDefinition object and insert resulting metadata into
* the db
- * PRE_EVAL(dbh) *)
+ * PRE_EVAL(dbd) *)
val index_inductive_def:
- dbh:Dbi.connection ->
+ dbd:Mysql.dbd ->
owner:string ->
uri:UriManager.uri -> types:Cic.inductiveType list ->
unit
(* TODO Zack indexing of variables and (perhaps?) incomplete proofs *)
(** remove from the db all metadata pertaining to a given owner *)
-val clean: dbh:Dbi.connection -> owner:string -> unit
+val clean: dbd:Mysql.dbd -> owner:string -> unit
(List.append sort_cols s, List.append rel_cols r, List.append obj_cols o))
([], [], []) ind_metadata
+(*
let pp_columns ?(sep = "\n") (sort_cols, rel_cols, obj_cols) =
String.concat sep
([ "Sort" ] @ List.map Dbi.sdebug (sort_cols :> Dbi.sql_t list list) @
[ "Rel" ] @ List.map Dbi.sdebug (rel_cols :> Dbi.sql_t list list) @
[ "Obj" ] @ List.map Dbi.sdebug (obj_cols :> Dbi.sql_t list list))
+*)
(string * string * MetadataTypes.metadata list) list ->
t list list * t list list * t list list
+(*
val pp_columns: ?sep:string -> t list list * t list list * t list list -> string
+*)
-module DB = Dbi_mysql
-
let _ = Helm_registry.set "getter.mode" "remote";
let _ = Helm_registry.set "getter.url" "http://mowgli.cs.unibo.it:58081/" in
-let dbh = new DB.connection ~host:"mowgli.cs.unibo.it" ~user:"helm" "matita" in
+let dbd =
+ Mysql.quick_connect ~host:"mowgli.cs.unibo.it" ~user:"helm" ~database:"matita"
+ ()
+in
let owner =
try
Sys.argv.(2)
with Invalid_argument _ -> "matita_test"
in
if Sys.argv.(1) = "clean" then
- MetadataDb.clean ~dbh ~owner
+ MetadataDb.clean ~dbd ~owner
else
let uri_str = Sys.argv.(1) in
let uri = UriManager.uri_of_string uri_str in
match CicEnvironment.get_obj uri with
| Cic.Constant (_, body, ty, _) ->
- MetadataDb.index_constant ~body ~ty ~uri ~owner ~dbh
+ MetadataDb.index_constant ~body ~ty ~uri ~owner ~dbd
| Cic.InductiveDefinition (types, _, _) ->
- MetadataDb.index_inductive_def ~dbh ~owner ~uri ~types
+ MetadataDb.index_inductive_def ~dbd ~owner ~uri ~types
| _ -> assert false
REQUIRES = \
pcre helm-cic_proof_checking \
helm-cic_unification helm-mathql_interpreter helm-mathql_generator \
- dbi helm-metadata
+ mysql helm-metadata
INTERFACE_FILES = \
proofEngineTypes.mli \
let suffix = String.sub s (len-4) 4 in
not (suffix = ".var")
-let locate ~(dbh:Dbi.connection) ?(vars = false) name =
+let locate ~(dbd:Mysql.dbd) ?(vars = false) name =
let query =
- dbh#prepare (sprintf "SELECT source FROM %s WHERE value = \"%s\""
- MetadataTypes.name_tbl name)
+ sprintf "SELECT source FROM %s WHERE value = \"%s\""
+ MetadataTypes.name_tbl name
in
- query#execute [];
+ let result = Mysql.exec dbd query in
List.filter nonvar
- (List.map (function [`String s] -> s | _ -> assert false)
- (query#fetchall ()))
+ (Mysql.map result
+ (fun cols -> match cols.(0) with Some s -> s | _ -> assert false))
-let match_term ~(dbh:Dbi.connection) ty =
+let match_term ~(dbd:Mysql.dbd) ty =
let metadata = MetadataExtractor.compute ~body:None ~ty in
let constants_no =
MetadataConstraints.StringSet.cardinal (MetadataConstraints.constants_of ty)
in
let constraints = List.map MetadataTypes.constr_of_metadata metadata in
- Constr.at_least ~dbh ~full_card:(MetadataConstraints.Eq constants_no)
+ Constr.at_least ~dbd ~full_card:(MetadataConstraints.Eq constants_no)
constraints
let ( ** ) x y = int_of_float ((float_of_int x) ** (float_of_int y))
let inter = Constr.StringSet.inter set1 set2 in
List.filter (fun s -> Constr.StringSet.mem s inter) uris
-let filter_uris_forward ~dbh (main, constants) uris =
+let filter_uris_forward ~dbd (main, constants) uris =
let main_uris =
match main with
| None -> []
let full_signature =
List.fold_right Constr.StringSet.add main_uris constants
in
- List.filter (Constr.at_most ~dbh ~where:`Statement full_signature) uris
+ List.filter (Constr.at_most ~dbd ~where:`Statement full_signature) uris
-let filter_uris_backward ~dbh signature uris =
+let filter_uris_backward ~dbd signature uris =
let siguris =
- List.map snd (MetadataConstraints.sigmatch ~dbh ~where:`Statement signature)
+ List.map snd (MetadataConstraints.sigmatch ~dbd ~where:`Statement signature)
in
intersect uris siguris
in
prop1 - prop2
-let hint ~(dbh:Dbi.connection) ?signature ((proof, goal) as status) =
+let hint ~(dbd:Mysql.dbd) ?signature ((proof, goal) as status) =
let (_, metasenv, _, _) = proof in
let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
let (uris, (main, sig_constants)) =
match signature with
- | Some signature -> (Constr.sigmatch ~dbh signature, signature)
- | None -> (Constr.cmatch' ~dbh ty, Constr.signature_of ty)
+ | Some signature -> (Constr.sigmatch ~dbd signature, signature)
+ | None -> (Constr.cmatch' ~dbd ty, Constr.signature_of ty)
in
let uris = List.filter nonvar (List.map snd uris) in
let types_constants =
if ((List.length uris < pow) or (pow <= 0))
then begin
prerr_endline "MetadataQuery: large sig, falling back to old method";
- filter_uris_forward ~dbh (main, other_constants) uris
+ filter_uris_forward ~dbd (main, other_constants) uris
end else
- filter_uris_backward ~dbh (main, other_constants) uris
+ filter_uris_backward ~dbd (main, other_constants) uris
in
let rec aux = function
| [] -> []
Pervasives.compare (List.length goals1) (List.length goals2))
(aux uris)
-let elim ~dbh uri =
+let elim ~dbd uri =
let constraints =
[`Rel [`MainConclusion None];
`Sort (Cic.Prop,[`MainHypothesis (Some 1)]);
`Obj (uri,[`InHypothesis]);
]
in
- MetadataConstraints.at_least ~dbh constraints
+ MetadataConstraints.at_least ~dbd constraints
(** @param vars if set variables (".var" URIs) are considered. Defaults to
* false *)
val locate:
- dbh:Dbi.connection ->
+ dbd:Mysql.dbd ->
?vars:bool -> string -> string list
val hint:
- dbh:Dbi.connection ->
+ dbd:Mysql.dbd ->
?signature:MetadataConstraints.term_signature ->
ProofEngineTypes.status ->
(string * (ProofEngineTypes.proof * ProofEngineTypes.goal list)) list
-val match_term: dbh:Dbi.connection -> Cic.term -> string list
+val match_term: dbd:Mysql.dbd -> Cic.term -> string list
-val elim: dbh:Dbi.connection -> string -> string list
+val elim: dbd:Mysql.dbd -> string -> string list
exception NoOtherChoices;;
-let rec auto_new dbh = function
+let rec auto_new dbd = function
[] -> raise NoOtherChoices
| (proof, [])::tl -> (proof, [])::tl
- | (proof, (goal,0)::gtl)::tl -> auto_new dbh tl
+ | (proof, (goal,0)::gtl)::tl -> auto_new dbd tl
| (proof, (goal,depth)::gtl)::tl ->
let _,metasenv,proof_obj,_ = proof in
let meta_inf =
search_theorems_in_context proof goal (depth-1) gtl in
let global_choices =
new_search_theorems
- (fun status -> List.map snd (MetadataQuery.hint ~dbh status))
+ (fun status -> List.map snd (MetadataQuery.hint ~dbd status))
(* (TacticChaser.searchTheorems mqi_handle) *)
proof goal (depth-1) gtl in
let all_choices =
let reorder =
List.stable_sort sorting_list all_choices
in
- auto_new dbh reorder
- | None -> auto_new dbh ((proof,gtl)::tl)
+ auto_new dbd reorder
+ | None -> auto_new dbd ((proof,gtl)::tl)
;;
-let auto_tac ~(dbh:Dbi.connection) =
+let auto_tac ~(dbd:Mysql.dbd) =
(* CicMetaSubst.reset_counters (); *)
- let auto_tac dbh (proof,goal) =
+ let auto_tac dbd (proof,goal) =
prerr_endline "Entro in Auto";
try
- (match auto_new dbh [(proof, [(goal,depth)])] with
+ (match auto_new dbd [(proof, [(goal,depth)])] with
| (proof,_)::_ ->
prerr_endline "AUTO_TAC HA FINITO";
(* CicMetaSubst.print_counters (); *)
prerr_endline("Auto failed");
raise (ProofEngineTypes.Fail "No Applicable theorem")
in
- ProofEngineTypes.mk_tactic (auto_tac dbh)
+ ProofEngineTypes.mk_tactic (auto_tac dbd)
;;
(* TODO se ce n'e' piu' di una, prende la prima che trova... sarebbe meglio
ProofEngineTypes.tactic
(* val auto_tac : MQIConn.handle -> ProofEngineTypes.tactic *)
-val auto_tac : dbh:Dbi.connection -> ProofEngineTypes.tactic
+val auto_tac : dbd:Mysql.dbd -> ProofEngineTypes.tactic
projects / helm.git / commitdiff