From: Stefano Zacchiroli Date: Wed, 3 Nov 2004 16:31:43 +0000 (+0000) Subject: no longer use Dbi module but directly use Mysql module since it's 13 X-Git-Tag: v_0_6_4_1~31 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=282f371ba8533ea0e4e667265f9e4b04856bf972;p=helm.git no longer use Dbi module but directly use Mysql module since it's 13 times faster --- diff --git a/helm/gTopLevel/Makefile.in b/helm/gTopLevel/Makefile.in index 4b44c3418..75340e3aa 100644 --- a/helm/gTopLevel/Makefile.in +++ b/helm/gTopLevel/Makefile.in @@ -2,16 +2,16 @@ BIN_DIR = /usr/local/bin 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 diff --git a/helm/gTopLevel/chosenTermEditor.mli b/helm/gTopLevel/chosenTermEditor.mli index 83eb99e7d..d88932c70 100644 --- a/helm/gTopLevel/chosenTermEditor.mli +++ b/helm/gTopLevel/chosenTermEditor.mli @@ -14,7 +14,7 @@ module Make : functor (C : DisambiguateTypes.Callbacks) -> sig val term_editor : - dbh:Dbi.connection -> + dbd:Mysql.dbd -> ?packing:(GObj.widget -> unit) -> ?width:int -> ?height:int -> diff --git a/helm/gTopLevel/disambiguatingParser.ml.in b/helm/gTopLevel/disambiguatingParser.ml.in index dfab60433..224eb4b6e 100644 --- a/helm/gTopLevel/disambiguatingParser.ml.in +++ b/helm/gTopLevel/disambiguatingParser.ml.in @@ -31,14 +31,14 @@ module AndreaAndZackDisambiguatingParser = 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 diff --git a/helm/gTopLevel/disambiguatingParser.mli b/helm/gTopLevel/disambiguatingParser.mli index 53b885088..a8afd0e65 100644 --- a/helm/gTopLevel/disambiguatingParser.mli +++ b/helm/gTopLevel/disambiguatingParser.mli @@ -36,7 +36,7 @@ module EnvironmentP3 : module Make (C : DisambiguateTypes.Callbacks) : sig val disambiguate_term : - dbh:Dbi.connection -> + dbd:Mysql.dbd -> Cic.context -> Cic.metasenv -> string -> diff --git a/helm/gTopLevel/gTopLevel.conf.xml.sample b/helm/gTopLevel/gTopLevel.conf.xml.sample index 4d5331948..e4f23f7ce 100644 --- a/helm/gTopLevel/gTopLevel.conf.xml.sample +++ b/helm/gTopLevel/gTopLevel.conf.xml.sample @@ -6,11 +6,15 @@ /home/sacerdot/helm/local_stuff - - http://localhost + http://mowgli.cs.unibo.it +
+ mowgli.cs.unibo.it + helm + mowgli +
mathql_db_map.txt
diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 82317959a..b6aa28cae 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -40,16 +40,12 @@ let warning s = prerr_endline ("W: " ^ s) 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 @@ -62,9 +58,14 @@ let _ = (* 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";; @@ -649,7 +650,7 @@ module InvokeTacticsCallbacks = 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);; @@ -913,7 +914,7 @@ let user_uri_choice ~title ~msg uris = ;; 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; @@ -1185,7 +1186,7 @@ let new_inductive () = ~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: @@ -1297,7 +1298,7 @@ let new_inductive () = ~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: @@ -1443,7 +1444,7 @@ let new_proof () = (* 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: @@ -2054,7 +2055,7 @@ let searchPattern () = 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:" @@ -2783,7 +2784,7 @@ class rendering_window output (notebook : notebook) = ~packing:frame#add () in let inputt = TermEditor'.term_editor - ~dbh + ~dbd ~width:400 ~height:100 ~packing:scrolled_window1#add () ~isnotempty_callback: (function b -> diff --git a/helm/gTopLevel/invokeTactics.ml b/helm/gTopLevel/invokeTactics.ml index ecacc9b7c..cbe25219c 100644 --- a/helm/gTopLevel/invokeTactics.ml +++ b/helm/gTopLevel/invokeTactics.ml @@ -62,7 +62,7 @@ module type Callbacks = (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 ;; @@ -306,7 +306,7 @@ module Make (C: Callbacks) : Tactics = (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 diff --git a/helm/gTopLevel/invokeTactics.mli b/helm/gTopLevel/invokeTactics.mli index cf116a542..993199fe4 100644 --- a/helm/gTopLevel/invokeTactics.mli +++ b/helm/gTopLevel/invokeTactics.mli @@ -60,7 +60,7 @@ module type Callbacks = (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 = diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml index b8573da89..25f81e37b 100644 --- a/helm/gTopLevel/proofEngine.ml +++ b/helm/gTopLevel/proofEngine.ml @@ -227,7 +227,7 @@ let fold_simpl term = 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) diff --git a/helm/gTopLevel/proofEngine.mli b/helm/gTopLevel/proofEngine.mli index 3e058cfcf..a38a02947 100644 --- a/helm/gTopLevel/proofEngine.mli +++ b/helm/gTopLevel/proofEngine.mli @@ -71,8 +71,7 @@ val fourier : unit -> unit 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 diff --git a/helm/gTopLevel/termEditor.ml b/helm/gTopLevel/termEditor.ml index e7b50c266..f74e45077 100644 --- a/helm/gTopLevel/termEditor.ml +++ b/helm/gTopLevel/termEditor.ml @@ -56,7 +56,7 @@ module Make(C:DisambiguateTypes.Callbacks) = 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 = @@ -100,7 +100,7 @@ module Make(C:DisambiguateTypes.Callbacks) = 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 diff --git a/helm/gTopLevel/termEditor.mli b/helm/gTopLevel/termEditor.mli index ecb40decd..9ae451e4b 100644 --- a/helm/gTopLevel/termEditor.mli +++ b/helm/gTopLevel/termEditor.mli @@ -39,7 +39,7 @@ class type term_editor = module Make (C : DisambiguateTypes.Callbacks) : sig val term_editor : - dbh:Dbi.connection -> + dbd:Mysql.dbd -> ?packing:(GObj.widget -> unit) -> ?width:int -> ?height:int -> diff --git a/helm/gTopLevel/termViewer.ml b/helm/gTopLevel/termViewer.ml index 4eac2617a..b6ca2a532 100644 --- a/helm/gTopLevel/termViewer.ml +++ b/helm/gTopLevel/termViewer.ml @@ -238,7 +238,7 @@ class proof_viewer ~(mml_of_cic_object:mml_of_cic_object) obj = (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 diff --git a/helm/gTopLevel/texTermEditor.ml b/helm/gTopLevel/texTermEditor.ml index 825b79e12..d0fefdee3 100644 --- a/helm/gTopLevel/texTermEditor.ml +++ b/helm/gTopLevel/texTermEditor.ml @@ -59,7 +59,7 @@ module Make(C:DisambiguateTypes.Callbacks) = module Disambiguate' = DisambiguatingParser.Make(C);; class term_editor_impl - ~dbh + ~dbd ?packing ?width ?height ?isnotempty_callback ?share_environment_with () : term_editor = @@ -219,7 +219,7 @@ module Make(C:DisambiguateTypes.Callbacks) = 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 diff --git a/helm/gTopLevel/texTermEditor.mli b/helm/gTopLevel/texTermEditor.mli index c7709b532..fa2dbb95b 100644 --- a/helm/gTopLevel/texTermEditor.mli +++ b/helm/gTopLevel/texTermEditor.mli @@ -40,7 +40,7 @@ class type term_editor = module Make (C : DisambiguateTypes.Callbacks) : sig val term_editor : - dbh:Dbi.connection -> + dbd:Mysql.dbd -> ?packing:(GObj.widget -> unit) -> ?width:int -> ?height:int -> diff --git a/helm/ocaml/METAS/meta.helm-metadata.src b/helm/ocaml/METAS/meta.helm-metadata.src index 773e8fbd2..9929f1552 100644 --- a/helm/ocaml/METAS/meta.helm-metadata.src +++ b/helm/ocaml/METAS/meta.helm-metadata.src @@ -1,4 +1,4 @@ -requires="dbi helm-cic_proof_checking" +requires="mysql helm-cic_proof_checking" version="0.0.1" archive(byte)="metadata.cma" archive(native)="metadata.cmxa" diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index f93043778..87ff805ad 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -413,8 +413,8 @@ let domain_diff dom1 dom2 = 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 | [] -> @@ -443,7 +443,7 @@ module Make (C: Callbacks) = 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"; @@ -469,7 +469,7 @@ module Make (C: Callbacks) = (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 diff --git a/helm/ocaml/cic_disambiguation/disambiguate.mli b/helm/ocaml/cic_disambiguation/disambiguate.mli index b7ef829a5..4c62c894f 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.mli +++ b/helm/ocaml/cic_disambiguation/disambiguate.mli @@ -32,7 +32,7 @@ exception NoWellTypedInterpretation module Make (C : Callbacks) : sig val disambiguate_term : - dbh:Dbi.connection -> + dbd:Mysql.dbd -> Cic.context -> Cic.metasenv -> CicAst.term -> diff --git a/helm/ocaml/metadata/Makefile b/helm/ocaml/metadata/Makefile index 6505e0f2e..4c8f53fc1 100644 --- a/helm/ocaml/metadata/Makefile +++ b/helm/ocaml/metadata/Makefile @@ -1,5 +1,5 @@ PACKAGE = metadata -REQUIRES = dbi helm-cic_proof_checking +REQUIRES = mysql helm-cic_proof_checking PREDICATES = INTERFACE_FILES = \ @@ -14,8 +14,8 @@ EXTRA_OBJECTS_TO_CLEAN = 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 diff --git a/helm/ocaml/metadata/metadataConstraints.ml b/helm/ocaml/metadata/metadataConstraints.ml index fb782494a..f7707f90f 100644 --- a/helm/ocaml/metadata/metadataConstraints.ml +++ b/helm/ocaml/metadata/metadataConstraints.ml @@ -85,7 +85,7 @@ let add_card_constr tbl (n,from,where) = function 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 @@ -137,9 +137,9 @@ let at_least ~(dbh:Dbi.connection) ?concl_card ?full_card 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 *) @@ -374,7 +374,7 @@ let must_of_prefix ?(where = `Conclusion) m s = 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 @@ -384,19 +384,20 @@ let get_constants (dbh:Dbi.connection) ~where uri = "\"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 @@ -410,7 +411,7 @@ let myspeciallist = 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) -> @@ -420,14 +421,14 @@ let compute_exactly ~(dbh:Dbi.connection) where main prefixes = 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 = @@ -448,19 +449,19 @@ let compute_with_only ~(dbh:Dbi.connection) ?(where = `Conclusion) main 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 -> [] @@ -475,7 +476,7 @@ let cmatch ~(dbh:Dbi.connection) t = 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 @@ -492,7 +493,7 @@ let cmatch ~(dbh:Dbi.connection) t = (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) | _, _ -> []) @@ -515,7 +516,7 @@ let power consts = 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) -> @@ -529,22 +530,22 @@ let sigmatch ~(dbh:Dbi.connection) ?(where = `Conclusion) (main, constants) = 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 diff --git a/helm/ocaml/metadata/metadataConstraints.mli b/helm/ocaml/metadata/metadataConstraints.mli index ecdb3e6b2..3de99469c 100644 --- a/helm/ocaml/metadata/metadataConstraints.mli +++ b/helm/ocaml/metadata/metadataConstraints.mli @@ -35,17 +35,17 @@ type term_signature = (string * string list) option * StringSet.t (** @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 @@ -60,7 +60,7 @@ type cardinality_condition = * @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 -> @@ -68,7 +68,7 @@ val at_least: (** @param where defaults to `Conclusion *) val at_most: - dbh:Dbi.connection -> + dbd:Mysql.dbd -> ?where:where -> StringSet.t -> (string -> bool) diff --git a/helm/ocaml/metadata/metadataDb.ml b/helm/ocaml/metadata/metadataDb.ml index f4ce2dd39..7eaf4d881 100644 --- a/helm/ocaml/metadata/metadataDb.ml +++ b/helm/ocaml/metadata/metadataDb.ml @@ -27,93 +27,106 @@ open MetadataTypes 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; diff --git a/helm/ocaml/metadata/metadataDb.mli b/helm/ocaml/metadata/metadataDb.mli index 074ff7214..a1d7404bb 100644 --- a/helm/ocaml/metadata/metadataDb.mli +++ b/helm/ocaml/metadata/metadataDb.mli @@ -24,18 +24,18 @@ *) (** 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 @@ -43,5 +43,5 @@ val index_inductive_def: (* 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 diff --git a/helm/ocaml/metadata/metadataPp.ml b/helm/ocaml/metadata/metadataPp.ml index e83aa7c86..33f10427f 100644 --- a/helm/ocaml/metadata/metadataPp.ml +++ b/helm/ocaml/metadata/metadataPp.ml @@ -91,9 +91,11 @@ let columns_of_ind_metadata ind_metadata = (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)) +*) diff --git a/helm/ocaml/metadata/metadataPp.mli b/helm/ocaml/metadata/metadataPp.mli index 14a98ba41..4ab5f7e76 100644 --- a/helm/ocaml/metadata/metadataPp.mli +++ b/helm/ocaml/metadata/metadataPp.mli @@ -48,5 +48,7 @@ val columns_of_ind_metadata: (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 +*) diff --git a/helm/ocaml/metadata/test.ml b/helm/ocaml/metadata/test.ml index 27be47c23..b36ba9176 100644 --- a/helm/ocaml/metadata/test.ml +++ b/helm/ocaml/metadata/test.ml @@ -1,23 +1,24 @@ -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 diff --git a/helm/ocaml/tactics/Makefile b/helm/ocaml/tactics/Makefile index 77e61b2f4..439478865 100644 --- a/helm/ocaml/tactics/Makefile +++ b/helm/ocaml/tactics/Makefile @@ -2,7 +2,7 @@ PACKAGE = tactics 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 \ diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml index 3fdecb8c5..c007a1dea 100644 --- a/helm/ocaml/tactics/metadataQuery.ml +++ b/helm/ocaml/tactics/metadataQuery.ml @@ -32,23 +32,23 @@ let nonvar s = 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)) @@ -71,7 +71,7 @@ let intersect uris siguris = 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 -> [] @@ -80,11 +80,11 @@ let filter_uris_forward ~dbh (main, constants) uris = 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 @@ -104,13 +104,13 @@ let compare_goal_list proof goal1 goal2 = 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 = @@ -129,9 +129,9 @@ let hint ~(dbh:Dbi.connection) ?signature ((proof, goal) as status) = 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 | [] -> [] @@ -160,7 +160,7 @@ let hint ~(dbh:Dbi.connection) ?signature ((proof, goal) as status) = 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)]); @@ -168,5 +168,5 @@ let elim ~dbh uri = `Obj (uri,[`InHypothesis]); ] in - MetadataConstraints.at_least ~dbh constraints + MetadataConstraints.at_least ~dbd constraints diff --git a/helm/ocaml/tactics/metadataQuery.mli b/helm/ocaml/tactics/metadataQuery.mli index 54985ef68..f7a08d31f 100644 --- a/helm/ocaml/tactics/metadataQuery.mli +++ b/helm/ocaml/tactics/metadataQuery.mli @@ -26,16 +26,16 @@ (** @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 diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml index f986bc867..0a7544ef8 100644 --- a/helm/ocaml/tactics/variousTactics.ml +++ b/helm/ocaml/tactics/variousTactics.ml @@ -181,10 +181,10 @@ let new_search_theorems f proof goal depth gtl = 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 = @@ -202,7 +202,7 @@ let rec auto_new dbh = function 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 = @@ -216,17 +216,17 @@ let rec auto_new dbh = function 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 (); *) @@ -237,7 +237,7 @@ let auto_tac ~(dbh:Dbi.connection) = 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 diff --git a/helm/ocaml/tactics/variousTactics.mli b/helm/ocaml/tactics/variousTactics.mli index ebbf84332..5c7c9a0a9 100644 --- a/helm/ocaml/tactics/variousTactics.mli +++ b/helm/ocaml/tactics/variousTactics.mli @@ -33,5 +33,5 @@ val generalize_tac: 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