From ac741958783108ff31552e533c853e85c2ebb1c5 Mon Sep 17 00:00:00 2001
From: lzingare <??>
Date: Fri, 18 May 2007 14:45:00 +0000
Subject: [PATCH] added alternative implementation for hMysql relying on
 sqlite3.

---
 .../components/METAS/meta.helm-hmysql.src     |   2 +-
 .../binaries/extractor/extractor.ml           |   2 +-
 .../binaries/saturate/saturate_main.ml        |   6 +-
 .../cic_disambiguation/disambiguate.ml        |   4 +-
 .../cic_disambiguation/disambiguate.mli       |   4 +-
 helm/software/components/hmysql/.depend       |   4 +-
 helm/software/components/hmysql/.depend.opt   |   4 +-
 helm/software/components/hmysql/Makefile      |   2 +-
 helm/software/components/hmysql/hMysql.ml     |  34 +++-
 helm/software/components/hmysql/hSql.ml       |   1 +
 .../hmysql/{hMysql.mli => hSql.mli}           |  15 +-
 helm/software/components/hmysql/hSqlite3.ml   | 183 ++++++++++++++++++
 .../components/library/libraryClean.ml        |  42 ++--
 helm/software/components/library/libraryDb.ml |  53 ++---
 .../software/components/library/libraryDb.mli |   2 +-
 .../metadata/metadataConstraints.ml           |  26 +--
 .../metadata/metadataConstraints.mli          |  12 +-
 .../components/metadata/metadataDb.ml         |  41 ++--
 .../components/metadata/metadataDb.mli        |   6 +-
 .../components/metadata/metadataDeps.ml       |  12 +-
 .../components/metadata/metadataDeps.mli      |  12 +-
 .../components/metadata/sqlStatements.ml      |  63 +++---
 helm/software/components/tactics/auto.ml      |   2 +-
 helm/software/components/tactics/auto.mli     |   6 +-
 .../software/components/tactics/autoTactic.ml |   4 +-
 .../components/tactics/autoTactic.mli         |   2 +-
 .../components/tactics/declarative.mli        |   8 +-
 .../components/tactics/fwdSimplTactic.mli     |   2 +-
 .../components/tactics/metadataQuery.ml       |  10 +-
 .../components/tactics/metadataQuery.mli      |  10 +-
 helm/software/components/tactics/tactics.mli  |   8 +-
 helm/software/components/whelp/fwdQueries.ml  |   8 +-
 helm/software/components/whelp/fwdQueries.mli |   4 +-
 helm/software/components/whelp/whelp.ml       |   8 +-
 helm/software/components/whelp/whelp.mli      |   8 +-
 35 files changed, 426 insertions(+), 184 deletions(-)
 create mode 120000 helm/software/components/hmysql/hSql.ml
 rename helm/software/components/hmysql/{hMysql.mli => hSql.mli} (88%)
 create mode 100644 helm/software/components/hmysql/hSqlite3.ml

diff --git a/helm/software/components/METAS/meta.helm-hmysql.src b/helm/software/components/METAS/meta.helm-hmysql.src
index 144141e28..21841b5ca 100644
--- a/helm/software/components/METAS/meta.helm-hmysql.src
+++ b/helm/software/components/METAS/meta.helm-hmysql.src
@@ -1,4 +1,4 @@
-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"
diff --git a/helm/software/components/binaries/extractor/extractor.ml b/helm/software/components/binaries/extractor/extractor.ml
index 418d5ff7c..832fc0cb3 100644
--- a/helm/software/components/binaries/extractor/extractor.ml
+++ b/helm/software/components/binaries/extractor/extractor.ml
@@ -32,7 +32,7 @@ let main () =
   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") ()
diff --git a/helm/software/components/binaries/saturate/saturate_main.ml b/helm/software/components/binaries/saturate/saturate_main.ml
index afe8fbb83..abb23a67a 100644
--- a/helm/software/components/binaries/saturate/saturate_main.ml
+++ b/helm/software/components/binaries/saturate/saturate_main.ml
@@ -32,7 +32,7 @@ sig
     * 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 -> 
@@ -73,7 +73,7 @@ let configuration_file = ref "../../../matita/matita.conf.xml";;
 
 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
     | "" -> []
@@ -144,7 +144,7 @@ let main () =
   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")
diff --git a/helm/software/components/cic_disambiguation/disambiguate.ml b/helm/software/components/cic_disambiguation/disambiguate.ml
index 64a469cab..e93c54808 100644
--- a/helm/software/components/cic_disambiguation/disambiguate.ml
+++ b/helm/software/components/cic_disambiguation/disambiguate.ml
@@ -814,7 +814,7 @@ module type Disambiguator =
 sig
   val disambiguate_term :
     ?fresh_instances:bool ->
-    dbd:HMysql.dbd ->
+    dbd:HSql.dbd ->
     context:Cic.context ->
     metasenv:Cic.metasenv ->
     ?initial_ugraph:CicUniv.universe_graph -> 
@@ -829,7 +829,7 @@ sig
 
   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 *)
diff --git a/helm/software/components/cic_disambiguation/disambiguate.mli b/helm/software/components/cic_disambiguation/disambiguate.mli
index c1a50aceb..4fe40da91 100644
--- a/helm/software/components/cic_disambiguation/disambiguate.mli
+++ b/helm/software/components/cic_disambiguation/disambiguate.mli
@@ -52,7 +52,7 @@ sig
    * 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 -> 
@@ -68,7 +68,7 @@ sig
   (** @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 *)
diff --git a/helm/software/components/hmysql/.depend b/helm/software/components/hmysql/.depend
index e67a0660c..d0d29cbd2 100644
--- a/helm/software/components/hmysql/.depend
+++ b/helm/software/components/hmysql/.depend
@@ -1,2 +1,2 @@
-hMysql.cmo: hMysql.cmi 
-hMysql.cmx: hMysql.cmi 
+hSql.cmo: hSql.cmi 
+hSql.cmx: hSql.cmi 
diff --git a/helm/software/components/hmysql/.depend.opt b/helm/software/components/hmysql/.depend.opt
index e67a0660c..d0d29cbd2 100644
--- a/helm/software/components/hmysql/.depend.opt
+++ b/helm/software/components/hmysql/.depend.opt
@@ -1,2 +1,2 @@
-hMysql.cmo: hMysql.cmi 
-hMysql.cmx: hMysql.cmi 
+hSql.cmo: hSql.cmi 
+hSql.cmx: hSql.cmi 
diff --git a/helm/software/components/hmysql/Makefile b/helm/software/components/hmysql/Makefile
index 8a83eb23e..7474507e3 100644
--- a/helm/software/components/hmysql/Makefile
+++ b/helm/software/components/hmysql/Makefile
@@ -2,7 +2,7 @@ PACKAGE = hmysql
 PREDICATES =
 
 INTERFACE_FILES = \
-        hMysql.mli 
+        hSql.mli 
 IMPLEMENTATION_FILES = \
 	$(INTERFACE_FILES:%.mli=%.ml)
 EXTRA_OBJECTS_TO_INSTALL =
diff --git a/helm/software/components/hmysql/hMysql.ml b/helm/software/components/hmysql/hMysql.ml
index 94f3efe03..041f43922 100644
--- a/helm/software/components/hmysql/hMysql.ml
+++ b/helm/software/components/hmysql/hMysql.ml
@@ -27,7 +27,15 @@
 
 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"
 
@@ -54,7 +62,10 @@ let escape s =
 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 
@@ -65,16 +76,23 @@ let map res ~f =
 
 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
 
diff --git a/helm/software/components/hmysql/hSql.ml b/helm/software/components/hmysql/hSql.ml
new file mode 120000
index 000000000..3230ae532
--- /dev/null
+++ b/helm/software/components/hmysql/hSql.ml
@@ -0,0 +1 @@
+hMysql.ml
\ No newline at end of file
diff --git a/helm/software/components/hmysql/hMysql.mli b/helm/software/components/hmysql/hSql.mli
similarity index 88%
rename from helm/software/components/hmysql/hMysql.mli
rename to helm/software/components/hmysql/hSql.mli
index a5b90593e..23761a2b6 100644
--- a/helm/software/components/hmysql/hMysql.mli
+++ b/helm/software/components/hmysql/hSql.mli
@@ -35,6 +35,15 @@
 
 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 *)
 
@@ -49,8 +58,10 @@ 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 errno : dbd -> error_code
+(* val status : dbd -> Mysql.status *)
 
 val escape: string -> string
 
+val isMysql : bool
diff --git a/helm/software/components/hmysql/hSqlite3.ml b/helm/software/components/hmysql/hSqlite3.ml
new file mode 100644
index 000000000..a9e8a46ae
--- /dev/null
+++ b/helm/software/components/hmysql/hSqlite3.ml
@@ -0,0 +1,183 @@
+(* 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
diff --git a/helm/software/components/library/libraryClean.ml b/helm/software/components/library/libraryClean.ml
index a544991e8..f61fc89c2 100644
--- a/helm/software/components/library/libraryClean.ml
+++ b/helm/software/components/library/libraryClean.ml
@@ -49,17 +49,24 @@ let one_step_depend suri =
       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 -> 
@@ -240,14 +247,17 @@ let clean_baseuris ?(verbose=true) buris =
       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
diff --git a/helm/software/components/library/libraryDb.ml b/helm/software/components/library/libraryDb.ml
index d3e7e9831..78cff7948 100644
--- a/helm/software/components/library/libraryDb.ml
+++ b/helm/software/components/library/libraryDb.ml
@@ -29,7 +29,7 @@ open Printf ;;
 
 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")
@@ -58,9 +58,9 @@ let clean_owner_environment () =
   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
@@ -76,11 +76,12 @@ let clean_owner_environment () =
     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;
 ;;
@@ -113,15 +114,19 @@ let create_owner_environment () =
   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
 ;;
 
@@ -142,12 +147,14 @@ let remove_uri uri =
   
   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 *)
     )
@@ -159,10 +166,10 @@ let xpointers_of_ind uri =
   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
 
diff --git a/helm/software/components/library/libraryDb.mli b/helm/software/components/library/libraryDb.mli
index fc3dc969a..ce653795a 100644
--- a/helm/software/components/library/libraryDb.mli
+++ b/helm/software/components/library/libraryDb.mli
@@ -23,7 +23,7 @@
  * 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
diff --git a/helm/software/components/metadata/metadataConstraints.ml b/helm/software/components/metadata/metadataConstraints.ml
index d7192bd7e..c2dee6f5e 100644
--- a/helm/software/components/metadata/metadataConstraints.ml
+++ b/helm/software/components/metadata/metadataConstraints.ml
@@ -153,7 +153,7 @@ let add_constraint ?(start=0) ?(tables=default_tables) (n,from,where) metadata =
       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 =
@@ -166,12 +166,12 @@ let exec ~(dbd:HMysql.dbd) ?rating (n,from,where) =
           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
@@ -191,7 +191,7 @@ let at_least ~(dbd:HMysql.dbd) ?concl_card ?full_card ?diff ?rating tables
 ;;
     
 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
@@ -438,7 +438,7 @@ let must_of_prefix ?(where = `Conclusion) m s =
 
 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
@@ -458,16 +458,16 @@ let get_constants (dbd:HMysql.dbd) ~where uri =
       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
 
@@ -485,7 +485,7 @@ let myspeciallist =
    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) -> 
@@ -516,7 +516,7 @@ let compute_exactly ~(dbd:HMysql.dbd) ?(facts=false) ~where main prefixes =
 
   (* 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 = 
@@ -557,7 +557,7 @@ let compute_with_only ~(dbd:HMysql.dbd) ?(facts=false) ?(where = `Conclusion)
 
   (* 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 -> []
@@ -611,7 +611,7 @@ let power consts =
 
 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 =
diff --git a/helm/software/components/metadata/metadataConstraints.mli b/helm/software/components/metadata/metadataConstraints.mli
index 5b13f57a1..a76c1fed7 100644
--- a/helm/software/components/metadata/metadataConstraints.mli
+++ b/helm/software/components/metadata/metadataConstraints.mli
@@ -36,17 +36,17 @@ type term_signature = (UriManager.uri * UriManager.uri list) option * UriManager
 
   (** @return sorted list of theorem URIs, first URIs in the least have higher
   * relevance *)
-val cmatch: dbd: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 ->
@@ -78,7 +78,7 @@ val add_constraint:
   * @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 ->
@@ -88,7 +88,7 @@ val at_least:
 
   (** @param where defaults to `Conclusion *)
 val at_most:
-  dbd:HMysql.dbd ->
+  dbd:HSql.dbd ->
   ?where:where -> UriManagerSet.t ->
     (UriManager.uri -> bool)
 
@@ -101,7 +101,7 @@ val add_all_constr:
   int * string list * string list
 
 val exec: 
-  dbd:HMysql.dbd ->
+  dbd:HSql.dbd ->
   ?rating:[ `Hits ] -> 
   int * string list * string list -> 
   UriManager.uri list
diff --git a/helm/software/components/metadata/metadataDb.ml b/helm/software/components/metadata/metadataDb.ml
index 457545dee..6358df5b0 100644
--- a/helm/software/components/metadata/metadataDb.ml
+++ b/helm/software/components/metadata/metadataDb.ml
@@ -29,6 +29,14 @@ open MetadataTypes
 
 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
@@ -55,23 +63,23 @@ let execute_insert dbd uri (sort_cols, rel_cols, obj_cols) =
   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
   
     
@@ -109,9 +117,9 @@ let insert_const_no ~dbd l =
        (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 =
@@ -120,9 +128,9 @@ let insert_name ~dbd l =
       (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
@@ -135,10 +143,11 @@ let analyze_index = ref 0
 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
   
@@ -159,11 +168,11 @@ let index_obj ~dbd ~uri =
 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
@@ -175,7 +184,7 @@ let clean ~(dbd:HMysql.dbd) =
       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;
@@ -187,7 +196,7 @@ let unindex ~dbd ~uri =
     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
 
diff --git a/helm/software/components/metadata/metadataDb.mli b/helm/software/components/metadata/metadataDb.mli
index 86820aafb..b1acc4cbe 100644
--- a/helm/software/components/metadata/metadataDb.mli
+++ b/helm/software/components/metadata/metadataDb.mli
@@ -25,15 +25,15 @@
 
 
 
-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 ] -> 
diff --git a/helm/software/components/metadata/metadataDeps.ml b/helm/software/components/metadata/metadataDeps.ml
index 330984350..745466340 100644
--- a/helm/software/components/metadata/metadataDeps.ml
+++ b/helm/software/components/metadata/metadataDeps.ml
@@ -65,9 +65,9 @@ let direct_deps ~dbd uri =
           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 ())
@@ -83,9 +83,9 @@ let inverse_deps ~dbd uri =
           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 ())
@@ -112,12 +112,12 @@ let sorted_uris_of_baseuri ~dbd baseuri =
          (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 =
diff --git a/helm/software/components/metadata/metadataDeps.mli b/helm/software/components/metadata/metadataDeps.mli
index 4def88d9e..12b502cd0 100644
--- a/helm/software/components/metadata/metadataDeps.mli
+++ b/helm/software/components/metadata/metadataDeps.mli
@@ -26,20 +26,20 @@
   (** @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. *)
@@ -54,9 +54,9 @@ sig
   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
 
diff --git a/helm/software/components/metadata/sqlStatements.ml b/helm/software/components/metadata/sqlStatements.ml
index 86cffbd1b..ddc494c4a 100644
--- a/helm/software/components/metadata/sqlStatements.ml
+++ b/helm/software/components/metadata/sqlStatements.ml
@@ -32,42 +32,42 @@ type tbl = [ `RefObj| `RefSort| `RefRel| `ObjectName| `Hits| `Count]
 
 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
@@ -88,7 +88,8 @@ let sprintf_count_drop name = [sprintf "DROP TABLE %s;" name]
 (* 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 = [
@@ -109,27 +110,29 @@ sprintf "CREATE INDEX %s_statement ON %s (statement);" name 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 
@@ -202,13 +205,13 @@ let move_content (name1, tbl1) (name2, tbl2) buri =
   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)
 
diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml
index 6f293ff4a..c16c41152 100644
--- a/helm/software/components/tactics/auto.ml
+++ b/helm/software/components/tactics/auto.ml
@@ -1844,7 +1844,7 @@ let superposition_tac ~target ~table ~subterms_only ~demod_table status =
   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
diff --git a/helm/software/components/tactics/auto.mli b/helm/software/components/tactics/auto.mli
index f0bc752f6..e8b2fc038 100644
--- a/helm/software/components/tactics/auto.mli
+++ b/helm/software/components/tactics/auto.mli
@@ -25,20 +25,20 @@
 
 (* 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
 
diff --git a/helm/software/components/tactics/autoTactic.ml b/helm/software/components/tactics/autoTactic.ml
index 12041b2bc..964959ea9 100644
--- a/helm/software/components/tactics/autoTactic.ml
+++ b/helm/software/components/tactics/autoTactic.ml
@@ -270,7 +270,7 @@ and auto_new_aux dbd width already_seen_goals universe = function
 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) =
@@ -318,7 +318,7 @@ let int params name default =
         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
diff --git a/helm/software/components/tactics/autoTactic.mli b/helm/software/components/tactics/autoTactic.mli
index d96a82615..44209bc02 100644
--- a/helm/software/components/tactics/autoTactic.mli
+++ b/helm/software/components/tactics/autoTactic.mli
@@ -26,7 +26,7 @@
 
 val auto_tac:
  params:(string * string) list 
-  -> dbd:HMysql.dbd 
+  -> dbd:HSql.dbd 
   -> universe:Universe.universe
   -> ProofEngineTypes.tactic
 
diff --git a/helm/software/components/tactics/declarative.mli b/helm/software/components/tactics/declarative.mli
index a42faac4b..97514b684 100644
--- a/helm/software/components/tactics/declarative.mli
+++ b/helm/software/components/tactics/declarative.mli
@@ -28,10 +28,10 @@ val assume : string -> Cic.term -> 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 :
@@ -48,14 +48,14 @@ val thesisbecomes : Cic.term -> ProofEngineTypes.tactic
 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
diff --git a/helm/software/components/tactics/fwdSimplTactic.mli b/helm/software/components/tactics/fwdSimplTactic.mli
index 3dbcf6c9c..f130fe7b4 100644
--- a/helm/software/components/tactics/fwdSimplTactic.mli
+++ b/helm/software/components/tactics/fwdSimplTactic.mli
@@ -30,4 +30,4 @@ val lapply_tac:
 
 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
diff --git a/helm/software/components/tactics/metadataQuery.ml b/helm/software/components/tactics/metadataQuery.ml
index 6b87de349..abe192b94 100644
--- a/helm/software/components/tactics/metadataQuery.ml
+++ b/helm/software/components/tactics/metadataQuery.ml
@@ -194,7 +194,7 @@ let apply_tac_verbose = PrimitiveTactics.apply_tac_verbose
 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
@@ -275,7 +275,7 @@ let signature_of metasenv goal =
     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
@@ -334,7 +334,7 @@ let filter_out_predicate set ctx menv =
   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" ^
@@ -393,7 +393,7 @@ let equations_for_goal ~(dbd:HMysql.dbd) ?signature ((proof, goal) as _status) =
    (*        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)) =
@@ -475,7 +475,7 @@ let experimental_hint
     (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
diff --git a/helm/software/components/tactics/metadataQuery.mli b/helm/software/components/tactics/metadataQuery.mli
index 1bc9fa363..a1b533601 100644
--- a/helm/software/components/tactics/metadataQuery.mli
+++ b/helm/software/components/tactics/metadataQuery.mli
@@ -30,7 +30,7 @@
 
 (* 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:
@@ -39,19 +39,19 @@ 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 ->
@@ -60,7 +60,7 @@ val experimental_hint:
        (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 ->
diff --git a/helm/software/components/tactics/tactics.mli b/helm/software/components/tactics/tactics.mli
index 6cc96c74b..6decc44cc 100644
--- a/helm/software/components/tactics/tactics.mli
+++ b/helm/software/components/tactics/tactics.mli
@@ -2,14 +2,14 @@
 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 ->
@@ -29,7 +29,7 @@ val decompose :
   ?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 ->
@@ -56,7 +56,7 @@ val fold :
 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
diff --git a/helm/software/components/whelp/fwdQueries.ml b/helm/software/components/whelp/fwdQueries.ml
index 5387d3aeb..67cc46941 100644
--- a/helm/software/components/whelp/fwdQueries.ml
+++ b/helm/software/components/whelp/fwdQueries.ml
@@ -89,10 +89,10 @@ let fwd_simpl ~dbd t =
 	 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
@@ -111,5 +111,5 @@ let decomposables ~dbd =
    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   
diff --git a/helm/software/components/whelp/fwdQueries.mli b/helm/software/components/whelp/fwdQueries.mli
index 200670335..3e4936dec 100644
--- a/helm/software/components/whelp/fwdQueries.mli
+++ b/helm/software/components/whelp/fwdQueries.mli
@@ -23,6 +23,6 @@
  * 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
 
diff --git a/helm/software/components/whelp/whelp.ml b/helm/software/components/whelp/whelp.ml
index 5e63bcfc4..e1d8306cc 100644
--- a/helm/software/components/whelp/whelp.ml
+++ b/helm/software/components/whelp/whelp.ml
@@ -42,7 +42,7 @@ let sqlpat_of_shellglob =
           (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 "^^
@@ -50,12 +50,12 @@ let locate ~(dbd:HMysql.dbd) ?(vars = false) pat =
           (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 =
diff --git a/helm/software/components/whelp/whelp.mli b/helm/software/components/whelp/whelp.mli
index 9ff03ea20..80c4d6522 100644
--- a/helm/software/components/whelp/whelp.mli
+++ b/helm/software/components/whelp/whelp.mli
@@ -23,8 +23,8 @@
  * 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
 
-- 
2.39.2