on sqlite3.
-requires="helm-registry mysql helm-extlib"
+requires="helm-registry sqlite3 mysql helm-extlib"
version="0.0.1"
archive(byte)="hmysql.cma"
archive(native)="hmysql.cmxa"
Helm_registry.set "tmp.dir" path;
Http_getter.init ();
let dbd =
- HMysql.quick_connect
+ HSql.quick_connect
~host:(Helm_registry.get "db.host")
~user:(Helm_registry.get "db.user")
~database:(Helm_registry.get "db.database") ()
* choice from the user is needed to disambiguate the term
* @raise Ambiguous_term for ambiguous term *)
val disambiguate_string:
- dbd:HMysql.dbd ->
+ dbd:HSql.dbd ->
?context:Cic.context ->
?metasenv:Cic.metasenv ->
?initial_ugraph:CicUniv.universe_graph ->
let core_notation_script = "../../../matita/core_notation.moo";;
-let get_from_user ~(dbd:HMysql.dbd) =
+let get_from_user ~(dbd:HSql.dbd) =
let rec get () =
match read_line () with
| "" -> []
Helm_registry.load_from !configuration_file;
ignore (CicNotation2.load_notation [] core_notation_script);
ignore (CicNotation2.load_notation [] "../../../matita/library/legacy/coq.ma");
- let dbd = HMysql.quick_connect
+ let dbd = HSql.quick_connect
~host:(Helm_registry.get "db.host")
~user:(Helm_registry.get "db.user")
~database:(Helm_registry.get "db.database")
sig
val disambiguate_term :
?fresh_instances:bool ->
- dbd:HMysql.dbd ->
+ dbd:HSql.dbd ->
context:Cic.context ->
metasenv:Cic.metasenv ->
?initial_ugraph:CicUniv.universe_graph ->
val disambiguate_obj :
?fresh_instances:bool ->
- dbd:HMysql.dbd ->
+ dbd:HSql.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:HMysql.dbd ->
+ dbd:HSql.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:HMysql.dbd ->
+ dbd:HSql.dbd ->
aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
universe:DisambiguateTypes.multiple_environment option ->
uri:UriManager.uri option -> (* required only for inductive types *)
-hMysql.cmo: hMysql.cmi
-hMysql.cmx: hMysql.cmi
+hSql.cmo: hSql.cmi
+hSql.cmx: hSql.cmi
-hMysql.cmo: hMysql.cmi
-hMysql.cmx: hMysql.cmi
+hSql.cmo: hSql.cmi
+hSql.cmx: hSql.cmi
PREDICATES =
INTERFACE_FILES = \
- hMysql.mli
+ hSql.mli
IMPLEMENTATION_FILES = \
$(INTERFACE_FILES:%.mli=%.ml)
EXTRA_OBJECTS_TO_INSTALL =
type dbd = Mysql.dbd option
type result = Mysql.result option
-type error_code = Mysql.error_code
+type error_code =
+ | OK
+ | Table_exists_error
+ | Dup_keyname
+ | No_such_table
+ | No_such_index
+ | Bad_table_error
+ | GENERIC_ERROR of string
+exception Error
let profiler = HExtlib.profile "mysql"
let exec dbd s =
match dbd with
| None -> None
- | Some dbd -> Some (profiler.HExtlib.profile (Mysql.exec dbd) s)
+ | Some dbd ->
+ try
+ Some (profiler.HExtlib.profile (Mysql.exec dbd) s)
+ with Mysql.Error _ -> raise Error
let map res ~f =
match res with
let iter res ~f =
match res with
- | None -> ()
+ | None -> ()
| Some res ->
let iter f = Mysql.iter res ~f in
profiler.HExtlib.profile iter f
let errno = function
- | None -> Mysql.Connection_error
- | Some dbd -> profiler.HExtlib.profile Mysql.errno dbd
+ | None -> GENERIC_ERROR "Mysql.Connection_error"
+ | Some dbd ->
+ match Mysql.errno dbd with
+ | Mysql.No_such_table -> No_such_table
+ | Mysql.Table_exists_error -> Table_exists_error
+ | Mysql.Dup_keyname -> Dup_keyname
+ | Mysql.No_such_table -> No_such_table
+ | Mysql.No_such_index -> No_such_index
+ | Mysql.Bad_table_error -> Bad_table_error
+ | _ -> GENERIC_ERROR "Mysql_generic_error"
+;;
-let status = function
- | None -> Mysql.StatusError Mysql.Connection_error
- | Some dbd -> profiler.HExtlib.profile Mysql.status dbd
+let isMysql = true
+++ /dev/null
-(* Copyright (C) 2005, 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/.
- *)
-
-(**
- * {2 Proxy module around MySQL conection}
- *
- * The behaviour of this module is influenced by the Helm_registry boolean value
- * of the "db.nodb" key. When set to "false" the module works as expected. When
- * set to "true" all functions perform dummy action: connect and disconnect do
- * nothing; exec, iter, and map work like the empty set of results has been
- * returned; errno and status return Mysql.Connection_error
- *)
-
-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 : dbd -> unit
-
-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
-
-val escape: string -> string
-
--- /dev/null
+hMysql.ml
\ No newline at end of file
--- /dev/null
+(* Copyright (C) 2005, 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/.
+ *)
+
+(**
+ * {2 Proxy module around MySQL conection}
+ *
+ * The behaviour of this module is influenced by the Helm_registry boolean value
+ * of the "db.nodb" key. When set to "false" the module works as expected. When
+ * set to "true" all functions perform dummy action: connect and disconnect do
+ * nothing; exec, iter, and map work like the empty set of results has been
+ * returned; errno and status return Mysql.Connection_error
+ *)
+
+type dbd
+type result
+type error_code =
+ | OK
+ | Table_exists_error
+ | Dup_keyname
+ | No_such_table
+ | No_such_index
+ | Bad_table_error
+ | GENERIC_ERROR of string
+exception Error
+
+(* 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 : dbd -> unit
+
+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 -> error_code
+(* val status : dbd -> Mysql.status *)
+
+val escape: string -> string
+
+val isMysql : bool
--- /dev/null
+(* Copyright (C) 2005, 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/.
+ *)
+
+(* $Id: hMysql.ml 5769 2006-01-08 18:00:22Z sacerdot $ *)
+
+(*
+type result = Mysql.result option
+*)
+
+type result = Sqlite3.row list
+type dbd = Sqlite3.db option
+
+type error_code =
+ | OK
+ | Table_exists_error
+ | Dup_keyname
+ | No_such_table
+ | No_such_index
+ | Bad_table_error
+ | GENERIC_ERROR of string
+exception Error
+
+let prerr_endline s = ()(*HLog.debug s;;*)
+
+let profiler = HExtlib.profile "Sqlite3"
+
+let quick_connect ?host ?(database = "sqlite") ?port ?password ?user () =
+ let username = Helm_registry.get "user.name" in
+ let ram_db_name =
+ "/dev/shm/matita.db." ^ username ^ "." ^ string_of_int (Unix.getpid ())
+ in
+ let db_name = Helm_registry.get "matita.basedir" ^ "/" ^ database ^ ".db" in
+ let cp_to_ram_cmd = "cp " ^ db_name ^ " " ^ ram_db_name in
+ ignore (Sys.command cp_to_ram_cmd);
+ let mv_to_disk_cmd _ = ignore (Sys.command ("mv " ^ ram_db_name ^ " " ^ db_name)) in
+ at_exit mv_to_disk_cmd;
+ Some (Sqlite3.db_open ram_db_name)
+;;
+
+let disconnect db =
+ match db with
+ | None -> ()
+ | Some db ->
+ let b = Sqlite3.db_close db in
+ if b=false then prerr_endline "No Closed DataBase"
+;;
+
+let escape s = s
+
+let exec db s =
+ prerr_endline s;
+ let stored_result = ref [] in
+ let store row =
+ stored_result := row :: !stored_result
+ in
+ match db with
+ | None -> []
+ | Some db ->
+ let rc =
+ profiler.HExtlib.profile (Sqlite3.exec_no_headers db ~cb:store) s
+ in
+ match rc with
+ | Sqlite3.Rc.OK -> !stored_result
+ | _ -> raise Error
+;;
+
+let rec map res ~f =
+ let map f = List.map f res in
+ profiler.HExtlib.profile map f
+
+let iter res ~f =
+ let iter f = List.iter f res in
+ profiler.HExtlib.profile iter f
+
+let pp_rc = function
+ |Sqlite3.Rc.OK -> prerr_endline "Sqlite3.Rc.OK"
+ |Sqlite3.Rc.ERROR -> prerr_endline "Sqlite3.Rc.ERROR"
+ |Sqlite3.Rc.INTERNAL -> prerr_endline "Sqlite3.Rc.INTERNAL"
+ |Sqlite3.Rc.PERM -> prerr_endline "Sqlite3.Rc.PERM"
+ |Sqlite3.Rc.ABORT -> prerr_endline "Sqlite3.Rc.ABORT"
+ |Sqlite3.Rc.BUSY -> prerr_endline "Sqlite3.Rc.BUSY"
+ |Sqlite3.Rc.LOCKED -> prerr_endline "Sqlite3.Rc.LOCKED"
+ |Sqlite3.Rc.NOMEM -> prerr_endline "Sqlite3.Rc.NOMEM"
+ |Sqlite3.Rc.READONLY -> prerr_endline "Sqlite3.Rc.READONLY"
+ |Sqlite3.Rc.INTERRUPT -> prerr_endline "Sqlite3.Rc.INTERRUPT"
+ |Sqlite3.Rc.IOERR -> prerr_endline "Sqlite3.Rc.IOERR"
+ |Sqlite3.Rc.CORRUPT -> prerr_endline "Sqlite3.Rc.CORRUPT"
+ |Sqlite3.Rc.NOTFOUND -> prerr_endline "Sqlite3.Rc.NOTFOUND"
+ |Sqlite3.Rc.FULL -> prerr_endline "Sqlite3.Rc.FULL"
+ |Sqlite3.Rc.CANTOPEN -> prerr_endline "Sqlite3.Rc.CANTOPEN"
+ |Sqlite3.Rc.PROTOCOL -> prerr_endline "Sqlite3.Rc.PROTOCOL"
+ |Sqlite3.Rc.EMPTY -> prerr_endline "Sqlite3.Rc.EMPTY"
+ |Sqlite3.Rc.SCHEMA -> prerr_endline "Sqlite3.Rc.SCHEMA"
+ |Sqlite3.Rc.TOOBIG -> prerr_endline "Sqlite3.Rc.TOOBIG"
+ |Sqlite3.Rc.CONSTRAINT -> prerr_endline "Sqlite3.Rc.CONSTRAINT"
+ |Sqlite3.Rc.MISMATCH -> prerr_endline "Sqlite3.Rc.MISMATCH"
+ |Sqlite3.Rc.MISUSE -> prerr_endline "Sqlite3.Rc.MISUSE"
+ |Sqlite3.Rc.NOFLS -> prerr_endline "Sqlite3.Rc.NOFLS"
+ |Sqlite3.Rc.AUTH -> prerr_endline "Sqlite3.Rc.AUTH"
+ |Sqlite3.Rc.FORMAT -> prerr_endline "Sqlite3.Rc.FORMAT"
+ |Sqlite3.Rc.RANGE -> prerr_endline "Sqlite3.Rc.RANGE"
+ |Sqlite3.Rc.NOTADB -> prerr_endline "Sqlite3.Rc.NOTADB"
+ |Sqlite3.Rc.ROW -> prerr_endline "Sqlite3.Rc.ROW"
+ |Sqlite3.Rc.DONE -> prerr_endline "Sqlite3.Rc.DONE"
+ |Sqlite3.Rc.UNKNOWN n ->
+ prerr_endline ("Sqlite3.Rc.UNKNOWN " ^ string_of_int (Sqlite3.Rc.int_of_unknown n))
+;;
+
+let errno = function
+ | None -> OK
+ | Some db ->
+ (* pp_rc (Sqlite3.errcode db); *)
+ (* prerr_endline(Sqlite3.errmsg db); *)
+ match Sqlite3.errcode db with
+ |Sqlite3.Rc.OK -> OK
+ |Sqlite3.Rc.ERROR ->
+ if Pcre.pmatch(Sqlite3.errmsg db) ~pat:"^table .* already exists" then
+ Table_exists_error
+ else
+ if Pcre.pmatch(Sqlite3.errmsg db) ~pat:"^index .* already exists" then
+ Dup_keyname
+ else
+ if Pcre.pmatch(Sqlite3.errmsg db) ~pat:"^no such table: .*" then
+ No_such_table
+ else
+ if Pcre.pmatch(Sqlite3.errmsg db) ~pat:"^no such index: .*" then
+ No_such_index
+ else
+ GENERIC_ERROR "ciao"
+
+ |Sqlite3.Rc.INTERNAL
+ |Sqlite3.Rc.PERM
+ |Sqlite3.Rc.ABORT
+ |Sqlite3.Rc.BUSY
+ |Sqlite3.Rc.LOCKED
+ |Sqlite3.Rc.NOMEM
+ |Sqlite3.Rc.READONLY
+ |Sqlite3.Rc.INTERRUPT
+ |Sqlite3.Rc.IOERR
+ |Sqlite3.Rc.CORRUPT
+ |Sqlite3.Rc.NOTFOUND
+ |Sqlite3.Rc.FULL
+ |Sqlite3.Rc.CANTOPEN
+ |Sqlite3.Rc.PROTOCOL
+ |Sqlite3.Rc.EMPTY
+ |Sqlite3.Rc.SCHEMA
+ |Sqlite3.Rc.TOOBIG
+ |Sqlite3.Rc.CONSTRAINT
+ |Sqlite3.Rc.MISMATCH
+ |Sqlite3.Rc.MISUSE
+ |Sqlite3.Rc.NOFLS
+ |Sqlite3.Rc.AUTH
+ |Sqlite3.Rc.FORMAT
+ |Sqlite3.Rc.RANGE
+ |Sqlite3.Rc.NOTADB
+ |Sqlite3.Rc.ROW
+ |Sqlite3.Rc.DONE
+ |Sqlite3.Rc.UNKNOWN _ -> GENERIC_ERROR "Sqlite3_generic_error"
+;;
+
+let isMysql = false
Hashtbl.add cache_of_processed_baseuri buri true;
let query =
let buri = buri ^ "/" in
- let buri = HMysql.escape buri in
+ let buri = HSql.escape buri in
let obj_tbl = MetadataTypes.obj_tbl () in
- sprintf
- ("SELECT source, h_occurrence FROM %s WHERE " ^^
- "h_occurrence REGEXP '^%s[^/]*$'")
- obj_tbl buri
+ if HSql.isMysql then
+ sprintf ("SELECT source, h_occurrence FROM %s WHERE "
+ ^^ "h_occurrence REGEXP '^%s[^/]*$'") obj_tbl buri
+ else
+ begin
+ HLog.debug "Warning SELECT without REGEXP";
+ sprintf
+ ("SELECT source, h_occurrence FROM %s WHERE " ^^
+ "h_occurrence LIKE '%s%%'")
+ obj_tbl buri
+ end
in
try
- let rc = HMysql.exec (LibraryDb.instance ()) query in
+ let rc = HSql.exec (LibraryDb.instance ()) query in
let l = ref [] in
- HMysql.iter rc (
+ HSql.iter rc (
fun row ->
match row.(0), row.(1) with
| Some uri, Some occ when Filename.dirname occ = buri ->
end;
LibrarySync.remove_obj uri
) l;
- cleaned_no := !cleaned_no + List.length l;
- if !cleaned_no > 30 then
+ if HSql.isMysql then
begin
- cleaned_no := 0;
- List.iter
- (function table ->
- ignore (HMysql.exec (LibraryDb.instance ()) ("OPTIMIZE TABLE " ^ table)))
- [MetadataTypes.name_tbl (); MetadataTypes.rel_tbl ();
- MetadataTypes.sort_tbl (); MetadataTypes.obj_tbl();
- MetadataTypes.count_tbl()]
+ cleaned_no := !cleaned_no + List.length l;
+ if !cleaned_no > 30 then
+ begin
+ cleaned_no := 0;
+ List.iter
+ (function table ->
+ ignore (HSql.exec (LibraryDb.instance ()) ("OPTIMIZE TABLE " ^ table)))
+ [MetadataTypes.name_tbl (); MetadataTypes.rel_tbl ();
+ MetadataTypes.sort_tbl (); MetadataTypes.obj_tbl();
+ MetadataTypes.count_tbl()]
+ end
end
let instance =
let dbd = lazy (
- HMysql.quick_connect
+ HSql.quick_connect
~host:(Helm_registry.get "db.host")
~user:(Helm_registry.get "db.user")
~database:(Helm_registry.get "db.database")
let owned_uris =
try
MetadataDb.clean ~dbd
- with Mysql.Error _ as exn ->
- match HMysql.errno dbd with
- | Mysql.No_such_table -> []
+ with HSql.Error as exn ->
+ match HSql.errno dbd with
+ | HSql.No_such_table -> []
| _ -> raise exn
in
List.iter
owned_uris;
List.iter (fun statement ->
try
- ignore (HMysql.exec dbd statement)
- with Mysql.Error _ as exn ->
- match HMysql.errno dbd with
- | Mysql.Bad_table_error
- | Mysql.No_such_index | Mysql.No_such_table -> ()
+ ignore (HSql.exec dbd statement)
+ with HSql.Error as exn ->
+ match HSql.errno dbd with
+ | HSql.No_such_table
+ | HSql.Bad_table_error
+ | HSql.No_such_index -> prerr_endline statement; ()
| _ -> raise exn
) statements;
;;
in
List.iter (fun statement ->
try
- ignore (HMysql.exec dbd statement)
+ ignore (HSql.exec dbd statement)
with
- exn ->
- let status = HMysql.status dbd in
- match status with
- | Mysql.StatusError Mysql.Table_exists_error -> ()
- | Mysql.StatusError Mysql.Dup_keyname -> ()
- | Mysql.StatusError _ -> raise exn
- | _ -> ()
+ HSql.Error ->
+ let status = HSql.errno dbd in
+ match status with
+ | HSql.Table_exists_error -> ()
+ | HSql.Dup_keyname -> ()
+ | HSql.GENERIC_ERROR _ ->
+ prerr_endline statement;
+ raise HSql.Error
+ | _ -> ()
+
+
) statements
;;
let dbd = instance () in
let suri = UriManager.string_of_uri uri in
- let query table suri = sprintf
- "DELETE QUICK LOW_PRIORITY FROM %s WHERE source='%s'" table (HMysql.escape suri)
+ let query table suri =
+ if HSql.isMysql then
+ sprintf "DELETE QUICK LOW_PRIORITY FROM %s WHERE source='%s'" table (HSql.escape suri)
+ else sprintf "DELETE FROM %s WHERE source='%s'" table (HSql.escape suri)
in
List.iter (fun t ->
try
- ignore (HMysql.exec dbd (query t suri))
+ ignore (HSql.exec dbd (query t suri))
with
exn -> raise exn (* no errors should be accepted *)
)
let name_tbl = MetadataTypes.name_tbl () in
let query = sprintf
"SELECT source FROM %s WHERE source LIKE '%s#xpointer%%'" name_tbl
- (HMysql.escape (UriManager.string_of_uri uri))
+ (HSql.escape (UriManager.string_of_uri uri))
in
- let rc = HMysql.exec dbd query in
+ let rc = HSql.exec dbd query in
let l = ref [] in
- HMysql.iter rc (fun a -> match a.(0) with None ->()|Some a -> l := a:: !l);
+ HSql.iter rc (fun a -> match a.(0) with None ->()|Some a -> l := a:: !l);
List.map UriManager.uri_of_string !l
* http://helm.cs.unibo.it/
*)
-val instance: unit -> HMysql.dbd
+val instance: unit -> HSql.dbd
val create_owner_environment: unit -> unit
val clean_owner_environment: unit -> unit
in
((n+2), from, where)
-let exec ~(dbd:HMysql.dbd) ?rating (n,from,where) =
+let exec ~(dbd:HSql.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 = HMysql.exec dbd query in
- HMysql.map result
+ let result = HSql.exec dbd query in
+ HSql.map result
(fun row -> match row.(0) with Some s -> UriManager.uri_of_string s | _ -> assert false)
-let at_least ~(dbd:HMysql.dbd) ?concl_card ?full_card ?diff ?rating tables
+let at_least ~(dbd:HSql.dbd) ?concl_card ?full_card ?diff ?rating tables
(metadata: MetadataTypes.constr list)
=
let obj_tbl,rel_tbl,sort_tbl, count_tbl = tables in
;;
let at_least
- ~(dbd:HMysql.dbd) ?concl_card ?full_card ?diff ?rating
+ ~(dbd:HSql.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:HMysql.dbd) ~where uri =
+let get_constants (dbd:HSql.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 = HMysql.exec dbd query in
+ let result = HSql.exec dbd query in
let set = ref UriManagerSet.empty in
- HMysql.iter result
+ HSql.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:HMysql.dbd) ?(where = `Conclusion) only u =
+let at_most ~(dbd:HSql.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:HMysql.dbd) ?(facts=false) ~where main prefixes =
+let compute_exactly ~(dbd:HSql.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:HMysql.dbd) ?(facts=false) ?(where = `Conclusion)
+let compute_with_only ~(dbd:HSql.dbd) ?(facts=false) ?(where = `Conclusion)
main prefixes constants
=
let max_prefix_length =
(* real match query implementation *)
-let cmatch ~(dbd:HMysql.dbd) ?(facts=false) t =
+let cmatch ~(dbd:HSql.dbd) ?(facts=false) t =
let (main, constants) = signature_of t in
match main with
| None -> []
type where = [ `Conclusion | `Statement ]
-let sigmatch ~(dbd:HMysql.dbd) ?(facts=false) ?(where = `Conclusion)
+let sigmatch ~(dbd:HSql.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:HMysql.dbd -> ?facts:bool -> Cic.term -> UriManager.uri list
+val cmatch: dbd:HSql.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:HMysql.dbd -> ?facts:bool -> Cic.term -> (int * UriManager.uri) list
+val cmatch': dbd:HSql.dbd -> ?facts:bool -> Cic.term -> (int * UriManager.uri) list
type where = [ `Conclusion | `Statement ] (** signature matching extent *)
(** @param where defaults to `Conclusion *)
val sigmatch:
- dbd:HMysql.dbd ->
+ dbd:HSql.dbd ->
?facts:bool ->
?where:where ->
term_signature ->
* @return list of URI satisfying given constraints *)
val at_least:
- dbd:HMysql.dbd ->
+ dbd:HSql.dbd ->
?concl_card:cardinality_condition ->
?full_card:cardinality_condition ->
?diff:cardinality_condition ->
(** @param where defaults to `Conclusion *)
val at_most:
- dbd:HMysql.dbd ->
+ dbd:HSql.dbd ->
?where:where -> UriManagerSet.t ->
(UriManager.uri -> bool)
int * string list * string list
val exec:
- dbd:HMysql.dbd ->
+ dbd:HSql.dbd ->
?rating:[ `Hits ] ->
int * string list * string list ->
UriManager.uri list
open Printf
+let format_insert tbl tuples =
+ if HSql.isMysql then
+ [sprintf "INSERT %s VALUES %s;" tbl (String.concat "," tuples)]
+ else
+ List.map (fun tup ->
+ sprintf "INSERT INTO %s VALUES %s;" tbl tup) tuples
+;;
+
let execute_insert dbd uri (sort_cols, rel_cols, obj_cols) =
let sort_tuples =
List.fold_left (fun s l -> match l with
if sort_tuples <> [] then
begin
let query_sort =
- sprintf "INSERT %s VALUES %s;" (sort_tbl ()) (String.concat "," sort_tuples)
+ format_insert(sort_tbl ()) sort_tuples
in
- ignore (HMysql.exec dbd query_sort)
+ List.iter (fun query -> ignore (HSql.exec dbd query)) query_sort
end;
if rel_tuples <> [] then
begin
let query_rel =
- sprintf "INSERT %s VALUES %s;" (rel_tbl ()) (String.concat "," rel_tuples)
+ format_insert(rel_tbl ()) rel_tuples
in
- ignore (HMysql.exec dbd query_rel)
+ List.iter (fun query -> ignore (HSql.exec dbd query)) query_rel
end;
if obj_tuples <> [] then
begin
let query_obj =
- sprintf "INSERT %s VALUES %s;" (obj_tbl ()) (String.concat "," obj_tuples)
+ format_insert(obj_tbl ()) obj_tuples
in
- ignore (HMysql.exec dbd query_obj)
+ List.iter (fun query -> ignore (HSql.exec dbd query)) query_obj
end
(UriManager.string_of_uri uri) no_concl no_hyp no_full) :: acc
) [] l in
let insert =
- sprintf "INSERT INTO %s VALUES %s" (count_tbl ()) (String.concat "," data)
+ format_insert(count_tbl ()) data
in
- ignore (HMysql.exec dbd insert)
+ List.iter (fun query -> ignore (HSql.exec dbd query)) insert
let insert_name ~dbd l =
let data =
(sprintf "(\"%s\", \"%s\")" (UriManager.string_of_uri uri) name) :: acc
) [] l in
let insert =
- sprintf "INSERT INTO %s VALUES %s" (name_tbl ()) (String.concat "," data)
+ format_insert(name_tbl ()) data
in
- ignore (HMysql.exec dbd insert)
+ List.iter (fun query -> ignore (HSql.exec dbd query)) insert
type columns =
MetadataPp.t list list * MetadataPp.t list list * MetadataPp.t list list
let eventually_analyze dbd =
incr analyze_index;
if !analyze_index > 30 then
+ if HSql.isMysql then
begin
let analyze t = "OPTIMIZE TABLE " ^ t ^ ";" in
List.iter
- (fun table -> ignore (HMysql.exec dbd (analyze table)))
+ (fun table -> ignore (HSql.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:HMysql.dbd) =
+let clean ~(dbd:HSql.dbd) =
let owned_uris = (* list of uris in list-of-columns format *)
let query = sprintf "SELECT source FROM %s" (name_tbl ()) in
- let result = HMysql.exec dbd query in
- let uris = HMysql.map result (fun cols ->
+ let result = HSql.exec dbd query in
+ let uris = HSql.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 (HMysql.exec dbd (query source_col)))
+ (fun source_col -> ignore (HSql.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 (HMysql.exec dbd (query tbl))
+ ignore (HSql.exec dbd (query tbl))
in
List.iter del_from tables_to_clean
-val index_obj: dbd:HMysql.dbd -> uri:UriManager.uri -> unit
+val index_obj: dbd:HSql.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:HMysql.dbd -> string list
+val clean: dbd:HSql.dbd -> string list
-val unindex: dbd:HMysql.dbd -> uri:UriManager.uri -> unit
+val unindex: dbd:HSql.dbd -> uri:UriManager.uri -> unit
val count_distinct:
[`Conclusion | `Hypothesis | `Statement ] ->
assert false
in
let do_query tbl =
- let res = HMysql.exec dbd (SqlStatements.direct_deps tbl uri) in
+ let res = HSql.exec dbd (SqlStatements.direct_deps tbl uri) in
let deps =
- HMysql.map res (fun row -> unbox_row (obj_metadata_of_row row)) in
+ HSql.map res (fun row -> unbox_row (obj_metadata_of_row row)) in
deps
in
do_query (MetadataTypes.obj_tbl ())
assert false
in
let do_query tbl =
- let res = HMysql.exec dbd (SqlStatements.inverse_deps tbl uri) in
+ let res = HSql.exec dbd (SqlStatements.inverse_deps tbl uri) in
let deps =
- HMysql.map res (fun row -> unbox_row (inv_obj_metadata_of_row row)) in
+ HSql.map res (fun row -> unbox_row (inv_obj_metadata_of_row row)) in
deps
in
do_query (MetadataTypes.obj_tbl ())
(MetadataTypes.name_tbl ()) sql_pat
MetadataTypes.library_name_tbl sql_pat
in
- let result = HMysql.exec dbd query in
+ let result = HSql.exec dbd query in
let map cols = match cols.(0) with
| Some s -> UriManager.uri_of_string s
| _ -> assert false
in
- let uris = HMysql.map result map in
+ let uris = HSql.map result map in
let sorted_uris = topological_sort ~dbd uris in
let filter_map uri =
let s =
(** @return the one step direct dependencies of an object, specified by URI
* (that is, the list of objects on which an given one depends) *)
val direct_deps:
- dbd:HMysql.dbd ->
+ dbd:HSql.dbd ->
UriManager.uri -> (UriManager.uri * MetadataTypes.position) list
(** @return the one step inverse dependencies of an objects, specified by URI
* (that is, the list of objects which depends on a given object) *)
val inverse_deps:
- dbd:HMysql.dbd ->
+ dbd:HSql.dbd ->
UriManager.uri -> (UriManager.uri * MetadataTypes.position) list
val topological_sort:
- dbd:HMysql.dbd -> UriManager.uri list -> UriManager.uri list
+ dbd:HSql.dbd -> UriManager.uri list -> UriManager.uri list
val sorted_uris_of_baseuri:
- dbd:HMysql.dbd -> string -> UriManager.uri list
+ dbd:HSql.dbd -> string -> UriManager.uri list
(** Representation of a (lazy) dependency graph.
* Imperative data structure. *)
val render: Format.formatter -> t -> unit
(** @return the transitive closure of direct_deps *)
- val direct_deps: dbd:HMysql.dbd -> UriManager.uri -> t
+ val direct_deps: dbd:HSql.dbd -> UriManager.uri -> t
(** @return the transitive closure of inverse_deps *)
- val inverse_deps: dbd:HMysql.dbd -> UriManager.uri -> t
+ val inverse_deps: dbd:HSql.dbd -> UriManager.uri -> t
end
let sprintf_refObj_format name = [
sprintf "CREATE TABLE %s (
- source varchar(255) binary not null,
- h_occurrence varchar(255) binary not null,
- h_position varchar(62) binary not null,
+ source varchar(255) not null,
+ h_occurrence varchar(255) not null,
+ h_position varchar(62) not null,
h_depth integer
);" name]
let sprintf_refSort_format name = [
sprintf "CREATE TABLE %s (
- source varchar(255) binary not null,
- h_position varchar(62) binary not null,
+ source varchar(255) not null,
+ h_position varchar(62) not null,
h_depth integer not null,
- h_sort varchar(5) binary not null
+ h_sort varchar(5) not null
);" name]
let sprintf_refRel_format name = [
sprintf "CREATE TABLE %s (
- source varchar(255) binary not null,
- h_position varchar(62) binary not null,
+ source varchar(255) not null,
+ h_position varchar(62) not null,
h_depth integer not null
);" name]
let sprintf_objectName_format name = [
sprintf "CREATE TABLE %s (
- source varchar(255) binary not null,
- value varchar(255) binary not null
+ source varchar(255) not null,
+ value varchar(255) not null
);" name]
let sprintf_hits_format name = [
sprintf "CREATE TABLE %s (
- source varchar(255) binary not null,
+ source varchar(255) not null,
no integer not null
);" name]
let sprintf_count_format name = [
sprintf "CREATE TABLE %s (
- source varchar(255) binary unique not null,
+ source varchar(255) unique not null,
conclusion smallint(6) not null,
hypothesis smallint(6) not null,
statement smallint(6) not null
(* INDEXES *)
let sprintf_refObj_index name = [
-sprintf "CREATE INDEX %s_index ON %s (source(219),h_occurrence(219),h_position);" name name;
+sprintf "CREATE INDEX %s_index ON %s (source,h_occurrence,h_position);" name name;
+(*sprintf "CREATE INDEX %s_index ON %s (source(219),h_occurrence(219),h_position);" name name;*)
sprintf "CREATE INDEX %s_occurrence ON %s (h_occurrence);" name name ]
let sprintf_refSort_index name = [
let sprintf_refRel_index name = [
sprintf "CREATE INDEX %s_index ON %s (source,h_position,h_depth);" name name]
-let sprintf_refObj_index_drop name = [
-sprintf "DROP INDEX %s_index ON %s;" name name ]
+let format_drop name sufix =
+ if HSql.isMysql then
+ (sprintf "DROP INDEX %s_%s ON %s;" name sufix name)
+ else
+ (sprintf "DROP INDEX %s_%s;" name sufix);;
-let sprintf_refSort_index_drop name = [
-sprintf "DROP INDEX %s_index ON %s;" name name ]
+let sprintf_refObj_index_drop name = [(format_drop name "index")]
-let sprintf_objectName_index_drop name = [
-sprintf "DROP INDEX %s_value ON %s;" name name]
+let sprintf_refSort_index_drop name = [(format_drop name "index")]
+
+let sprintf_objectName_index_drop name = [(format_drop name "value")]
let sprintf_hits_index_drop name = [
-sprintf "DROP INDEX %s_source ON %s;" name name ;
-sprintf "DROP INDEX %s_no ON %s;" name name]
+(format_drop name "source");
+(format_drop name "no")]
let sprintf_count_index_drop name = [
-sprintf "DROP INDEX %s_source ON %s;" name name;
-sprintf "DROP INDEX %s_conclusion ON %s;" name name;
-sprintf "DROP INDEX %s_hypothesis ON %s;" name name;
-sprintf "DROP INDEX %s_statement ON %s;" name name]
+(format_drop name "source");
+(format_drop name "conclusion");
+(format_drop name "hypothesis");
+(format_drop name "statement")]
-let sprintf_refRel_index_drop name = [
-sprintf "DROP INDEX %s_index ON %s;" name name]
+let sprintf_refRel_index_drop name = [(format_drop name "index")]
let sprintf_rename_table oldname newname = [
sprintf "RENAME TABLE %s TO %s;" oldname newname
assert (tbl1 = tbl2);
sprintf
"INSERT INTRO %s SELECT * FROM %s WHERE source LIKE \"%s%%\";"
- name2 name1 (HMysql.escape buri)
+ name2 name1 (HSql.escape buri)
let direct_deps refObj uri =
sprintf "SELECT * FROM %s WHERE source = \"%s\";"
- (HMysql.escape refObj) (UriManager.string_of_uri uri)
+ (HSql.escape refObj) (UriManager.string_of_uri uri)
let inverse_deps refObj uri =
sprintf "SELECT * FROM %s WHERE h_occurrence = \"%s\";"
- (HMysql.escape refObj) (UriManager.string_of_uri uri)
+ (HSql.escape refObj) (UriManager.string_of_uri uri)
proof,[goalno]
;;
-let auto_tac ~(dbd:HMysql.dbd) ~params ~universe (proof, goal) =
+let auto_tac ~(dbd:HSql.dbd) ~params ~universe (proof, goal) =
(* argument parsing *)
let string = string params in
let bool = bool params in
(* stops at the first solution *)
val auto_tac:
- dbd:HMysql.dbd ->
+ dbd:HSql.dbd ->
params:(string * string) list ->
universe:Universe.universe ->
ProofEngineTypes.tactic
val applyS_tac:
- dbd:HMysql.dbd ->
+ dbd:HSql.dbd ->
term: Cic.term ->
params:(string * string) list ->
universe:Universe.universe ->
ProofEngineTypes.tactic
val demodulate_tac :
- dbd:HMysql.dbd ->
+ dbd:HSql.dbd ->
universe:Universe.universe ->
ProofEngineTypes.tactic
let default_depth = 5
let default_width = 3
-let auto_tac_old ?(depth=default_depth) ?(width=default_width) ~(dbd:HMysql.dbd)
+let auto_tac_old ?(depth=default_depth) ?(width=default_width) ~(dbd:HSql.dbd)
()
=
let auto_tac dbd (proof,goal) =
raise (ProofEngineTypes.Fail (lazy (name ^ " must be an integer")))
;;
-let auto_tac ~params ~(dbd:HMysql.dbd) ~universe (proof, goal) =
+let auto_tac ~params ~(dbd:HSql.dbd) ~universe (proof, goal) =
(* argument parsing *)
let int = int params in
let bool = bool params in
val auto_tac:
params:(string * string) list
- -> dbd:HMysql.dbd
+ -> dbd:HSql.dbd
-> universe:Universe.universe
-> ProofEngineTypes.tactic
val suppose : Cic.term -> string -> Cic.term option -> ProofEngineTypes.tactic
val by_term_we_proved :
- dbd:HMysql.dbd -> universe:Universe.universe -> Cic.term option -> Cic.term ->
+ dbd:HSql.dbd -> universe:Universe.universe -> Cic.term option -> Cic.term ->
string option -> Cic.term option -> ProofEngineTypes.tactic
-val bydone : dbd:HMysql.dbd -> universe:Universe.universe -> Cic.term option ->
+val bydone : dbd:HSql.dbd -> universe:Universe.universe -> Cic.term option ->
ProofEngineTypes.tactic
val we_need_to_prove :
val case : string -> params:(string * Cic.term) list -> ProofEngineTypes.tactic
val existselim :
- dbd:HMysql.dbd -> universe:Universe.universe ->
+ dbd:HSql.dbd -> universe:Universe.universe ->
Cic.term option -> string -> Cic.term -> string -> Cic.lazy_term -> ProofEngineTypes.tactic
val andelim :
Cic.term -> string -> Cic.term -> string -> Cic.term -> ProofEngineTypes.tactic
val rewritingstep :
- dbd:HMysql.dbd -> universe:Universe.universe ->
+ dbd:HSql.dbd -> universe:Universe.universe ->
(string option * Cic.term) option -> Cic.term ->
[ `Term of Cic.term | `Auto of (string * string) list ] ->
bool (* last step *) -> ProofEngineTypes.tactic
val fwd_simpl_tac:
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
- dbd:HMysql.dbd -> string -> ProofEngineTypes.tactic
+ dbd:HSql.dbd -> string -> ProofEngineTypes.tactic
let cmatch' = Constr.cmatch'
(* used only by te old auto *)
-let signature_of_goal ~(dbd:HMysql.dbd) ((proof, goal) as _status) =
+let signature_of_goal ~(dbd:HSql.dbd) ((proof, goal) as _status) =
let (_, metasenv, _subst, _, _, _) = proof in
let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
let main, sig_constants = Constr.signature_of ty in
close_with_types set metasenv context
-let universe_of_goal ~(dbd:HMysql.dbd) apply_only metasenv goal =
+let universe_of_goal ~(dbd:HSql.dbd) apply_only metasenv goal =
let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
let ty_set = Constr.constants_of ty in
let hyp_set = signature_of_hypothesis context metasenv in
Constr.UriManagerSet.filter (fun u -> not (is_predicate u)) set
;;
-let equations_for_goal ~(dbd:HMysql.dbd) ?signature ((proof, goal) as _status) =
+let equations_for_goal ~(dbd:HSql.dbd) ?signature ((proof, goal) as _status) =
(*
let to_string set =
"{\n" ^
(* else raise Goal_is_not_an_equation *)
let experimental_hint
- ~(dbd:HMysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) =
+ ~(dbd:HSql.dbd) ?(facts=false) ?signature ((proof, goal) as status) =
let (_, metasenv, _subst, _, _, _) = proof in
let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
let (uris, (main, sig_constants)) =
(aux uris)
let new_experimental_hint
- ~(dbd:HMysql.dbd) ?(facts=false) ?signature ~universe
+ ~(dbd:HSql.dbd) ?(facts=false) ?signature ~universe
((proof, goal) as status)
=
let (_, metasenv, _subst, _, _, _) = proof in
(* used only by the old auto *)
val signature_of_goal:
- dbd:HMysql.dbd -> ProofEngineTypes.status ->
+ dbd:HSql.dbd -> ProofEngineTypes.status ->
UriManager.uri list
val signature_of:
MetadataConstraints.UriManagerSet.t
val universe_of_goal:
- dbd:HMysql.dbd ->
+ dbd:HSql.dbd ->
bool -> (* apply only or not *)
Cic.metasenv ->
ProofEngineTypes.goal ->
UriManager.uri list
val equations_for_goal:
- dbd:HMysql.dbd ->
+ dbd:HSql.dbd ->
?signature:MetadataConstraints.term_signature ->
ProofEngineTypes.status -> UriManager.uri list
val experimental_hint:
- dbd:HMysql.dbd ->
+ dbd:HSql.dbd ->
?facts:bool ->
?signature:MetadataConstraints.term_signature ->
ProofEngineTypes.status ->
(ProofEngineTypes.proof * ProofEngineTypes.goal list))) list
val new_experimental_hint:
- dbd:HMysql.dbd ->
+ dbd:HSql.dbd ->
?facts:bool ->
?signature:MetadataConstraints.term_signature ->
universe:UriManager.uri list ->
val absurd : term:Cic.term -> ProofEngineTypes.tactic
val apply : term:Cic.term -> ProofEngineTypes.tactic
val applyS :
- dbd:HMysql.dbd ->
+ dbd:HSql.dbd ->
term:Cic.term ->
params:(string * string) list ->
universe:Universe.universe -> ProofEngineTypes.tactic
val assumption : ProofEngineTypes.tactic
val auto :
params:(string * string) list ->
- dbd:HMysql.dbd -> universe:Universe.universe -> ProofEngineTypes.tactic
+ dbd:HSql.dbd -> universe:Universe.universe -> ProofEngineTypes.tactic
val cases_intros :
?howmany:int ->
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
unit -> ProofEngineTypes.tactic
val demodulate :
- dbd:HMysql.dbd -> universe:Universe.universe -> ProofEngineTypes.tactic
+ dbd:HSql.dbd -> universe:Universe.universe -> ProofEngineTypes.tactic
val destruct : 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:HMysql.dbd -> string -> ProofEngineTypes.tactic
+ dbd:HSql.dbd -> string -> ProofEngineTypes.tactic
val generalize :
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
let from = "genLemma" in
let where =
Printf.sprintf "h_outer = \"%s\""
- (HMysql.escape (UriManager.string_of_uri outer)) in
+ (HSql.escape (UriManager.string_of_uri outer)) in
let query = Printf.sprintf "SELECT %s FROM %s WHERE %s" select from where in
- let result = HMysql.exec dbd query in
- let lemmas = HMysql.map ~f:(map inners) result in
+ let result = HSql.exec dbd query in
+ let lemmas = HSql.map ~f:(map inners) result in
let ranked = List.fold_left rank [] lemmas in
let ordered = List.rev (List.fast_sort compare ranked) in
filter_map_n filter 0 ordered
in
let select, from = "source", "decomposables" in
let query = Printf.sprintf "SELECT %s FROM %s" select from in
- let decomposables = HMysql.map ~f:map (HMysql.exec dbd query) in
+ let decomposables = HSql.map ~f:map (HSql.exec dbd query) in
filter_map_n (fun _ x -> x) 0 decomposables
* http://helm.cs.unibo.it/
*)
-val fwd_simpl: dbd:HMysql.dbd -> Cic.term -> UriManager.uri list
-val decomposables: dbd:HMysql.dbd -> (UriManager.uri * int option) list
+val fwd_simpl: dbd:HSql.dbd -> Cic.term -> UriManager.uri list
+val decomposables: dbd:HSql.dbd -> (UriManager.uri * int option) list
(Pcre.replace ~rex:uscore_RE ~templ:"\\_"
shellglob)))
-let locate ~(dbd:HMysql.dbd) ?(vars = false) pat =
+let locate ~(dbd:HSql.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 = HMysql.exec dbd query in
+ let result = HSql.exec dbd query in
List.filter nonvar
- (HMysql.map result
+ (HSql.map result
(fun cols -> match cols.(0) with Some s -> UriManager.uri_of_string s | _ -> assert false))
-let match_term ~(dbd:HMysql.dbd) ty =
+let match_term ~(dbd:HSql.dbd) ty =
(* debug_print (lazy (CicPp.ppterm ty)); *)
let metadata = MetadataExtractor.compute ~body:None ~ty in
let constants_no =
* http://helm.cs.unibo.it/
*)
-val locate: dbd:HMysql.dbd -> ?vars:bool -> string -> UriManager.uri list
-val elim: dbd:HMysql.dbd -> UriManager.uri -> UriManager.uri list
-val instance: dbd:HMysql.dbd -> Cic.term -> UriManager.uri list
-val match_term: dbd:HMysql.dbd -> Cic.term -> UriManager.uri list
+val locate: dbd:HSql.dbd -> ?vars:bool -> string -> UriManager.uri list
+val elim: dbd:HSql.dbd -> UriManager.uri -> UriManager.uri list
+val instance: dbd:HSql.dbd -> Cic.term -> UriManager.uri list
+val match_term: dbd:HSql.dbd -> Cic.term -> UriManager.uri list
projects / helm.git / commitdiff