helm/matita/matitaDb.ml

   1 (* Copyright (C) 2004-2005, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://helm.cs.unibo.it/
  24  *)
  25
  26 open Printf ;;
  27
  28 let instance =
  29   let dbd = lazy (
  30     Mysql.quick_connect
  31       ~host:(Helm_registry.get "db.host")
  32       ~user:(Helm_registry.get "db.user")
  33       ~database:(Helm_registry.get "db.database")
  34       ())
  35   in
  36   fun () -> Lazy.force dbd
  37
  38
  39 let xpointer_RE = Pcre.regexp "#.*$"
  40
  41 let clean_owner_environment () =
  42   let dbd = instance () in
  43   let owner = (Helm_registry.get "matita.owner") in
  44   let obj_tbl = MetadataTypes.obj_tbl () in
  45   let sort_tbl = MetadataTypes.sort_tbl () in
  46   let rel_tbl = MetadataTypes.rel_tbl () in
  47   let name_tbl =  MetadataTypes.name_tbl () in
  48   let conclno_tbl = MetadataTypes.conclno_tbl () in
  49   let conclno_hyp_tbl = MetadataTypes.fullno_tbl () in
  50   let statements = [
  51     sprintf "DROP TABLE %s ;" obj_tbl;
  52     sprintf "DROP TABLE %s ;" sort_tbl;
  53     sprintf "DROP TABLE %s ;" rel_tbl;
  54     sprintf "DROP TABLE %s ;" name_tbl;
  55     sprintf "DROP TABLE %s ;" conclno_tbl;
  56     sprintf "DROP TABLE %s ;" conclno_hyp_tbl ] in
  57 (*
  58 DROP INDEX refObj_source ON refObj (source);
  59 DROP INDEX refObj_target ON refObj (h_occurrence);
  60 DROP INDEX refObj_position ON refObj (h_position);
  61 DROP INDEX refSort_source ON refSort (source);
  62 DROP INDEX objectName_value ON objectName (value);
  63 DROP INDEX no_inconcl_aux_source ON no_inconcl_aux (source);
  64 DROP INDEX no_inconcl_aux_no ON no_inconcl_aux (no);
  65 DROP INDEX no_concl_hyp_source ON no_concl_hyp (source);
  66 DROP INDEX no_concl_hyp_no ON no_concl_hyp (no);
  67 *)
  68   let owned_uris =
  69     try
  70       MetadataDb.clean ~dbd
  71     with Mysql.Error _ as exn ->
  72       match Mysql.errno dbd with
  73       | Mysql.No_such_table -> []
  74       | _ -> raise exn
  75   in
  76   List.iter
  77     (fun uri ->
  78       let uri = Pcre.replace ~rex:xpointer_RE ~templ:"" uri in
  79       List.iter
  80         (fun suffix -> Http_getter.unregister (uri ^ suffix))
  81         [""; ".body"; ".types"])
  82     owned_uris;
  83   List.iter (fun statement ->
  84     try
  85       ignore (Mysql.exec dbd statement)
  86     with Mysql.Error _ as exn ->
  87       match Mysql.errno dbd with
  88       | Mysql.Bad_table_error -> ()
  89       | _ -> raise exn
  90     ) statements;
  91 ;;
  92
  93 let create_owner_environment () =
  94   let dbd = instance () in
  95   let owner = (Helm_registry.get "matita.owner") in
  96   let obj_tbl = MetadataTypes.obj_tbl () in
  97   let sort_tbl = MetadataTypes.sort_tbl () in
  98   let rel_tbl = MetadataTypes.rel_tbl () in
  99   let name_tbl =  MetadataTypes.name_tbl () in
 100   let conclno_tbl = MetadataTypes.conclno_tbl () in
 101   let conclno_hyp_tbl = MetadataTypes.fullno_tbl () in
 102   let statements = [
 103     sprintf "CREATE TABLE %s (
 104                   source varchar(255) binary not null,
 105                   h_occurrence varchar(255) binary not null,
 106                   h_position varchar(255) binary not null,
 107                   h_depth integer
 108               );" obj_tbl;
 109     sprintf "CREATE TABLE %s (
 110                   source varchar(255) binary not null,
 111                   h_position varchar(255) binary not null,
 112                   h_depth integer not null,
 113                   h_sort varchar(255) binary not null
 114               );" sort_tbl;
 115     sprintf "CREATE TABLE %s (
 116                   source varchar(255) binary not null,
 117                   h_position varchar(255) binary not null,
 118                   h_depth integer not null
 119               );" rel_tbl;
 120     sprintf "CREATE TABLE %s (
 121                   source varchar(255) binary not null,
 122                   value varchar(255) binary not null
 123               );" name_tbl;
 124     sprintf "CREATE TABLE %s (
 125                   source varchar(255) binary not null,
 126                   no tinyint(4) not null
 127               );" conclno_tbl;
 128     sprintf "CREATE TABLE %s (
 129                   source varchar(255) binary not null,
 130                   no tinyint(4) not null
 131               );" conclno_hyp_tbl ] in
 132 (*
 133 CREATE INDEX refObj_source ON refObj (source);
 134 CREATE INDEX refObj_target ON refObj (h_occurrence);
 135 CREATE INDEX refObj_position ON refObj (h_position);
 136 CREATE INDEX refSort_source ON refSort (source);
 137 CREATE INDEX objectName_value ON objectName (value);
 138 CREATE INDEX no_inconcl_aux_source ON no_inconcl_aux (source);
 139 CREATE INDEX no_inconcl_aux_no ON no_inconcl_aux (no);
 140 CREATE INDEX no_concl_hyp_source ON no_concl_hyp (source);
 141 CREATE INDEX no_concl_hyp_no ON no_concl_hyp (no);
 142 *)
 143   List.iter (fun statement ->
 144     try
 145       ignore (Mysql.exec dbd statement)
 146     with
 147       exn ->
 148          let status = Mysql.status dbd in
 149          match status with
 150          | Mysql.StatusError Mysql.Table_exists_error -> ()
 151          | Mysql.StatusError _ -> raise exn
 152          | _ -> ()
 153       ) statements
 154 ;;
 155
 156 (* removes uri from the ownerized tables, and returns the list of other objects
 157  * (theyr uris) that ref the one removed.
 158  * AFAIK there is no need to return it, since the MatitaTypes.staus should
 159  * contain all defined objects. but to double ckeck we do not garbage the
 160  * metadata...
 161  *)
 162 let remove_uri uri =
 163   let obj_tbl = MetadataTypes.obj_tbl () in
 164   let sort_tbl = MetadataTypes.sort_tbl () in
 165   let rel_tbl = MetadataTypes.rel_tbl () in
 166   let name_tbl =  MetadataTypes.name_tbl () in
 167   let conclno_tbl = MetadataTypes.conclno_tbl () in
 168   let conclno_hyp_tbl = MetadataTypes.fullno_tbl () in
 169   let dbd = instance () in
 170   let suri = UriManager.string_of_uri uri in
 171   let query table suri = sprintf
 172     "DELETE FROM %s WHERE source LIKE '%s%%'" table (Mysql.escape suri)
 173   in
 174   List.iter (fun t ->
 175     try
 176       ignore (Mysql.exec dbd (query t suri))
 177     with
 178       exn -> raise exn (* no errors should be accepted *)
 179     ) [obj_tbl;sort_tbl;rel_tbl;name_tbl;conclno_tbl;conclno_hyp_tbl];
 180   (* and now the debug job *)
 181   let dbg_q =
 182     sprintf "SELECT source FROM %s WHERE h_occurrence LIKE '%s%%'" obj_tbl suri
 183   in
 184   try
 185     let rc = Mysql.exec dbd dbg_q in
 186     let l = ref [] in
 187     Mysql.iter rc (fun a -> match a.(0) with None ->()|Some a -> l := a:: !l);
 188     let l = List.sort Pervasives.compare !l in
 189     let rec uniq = function
 190       | [] -> []
 191       | h::[] -> [h]
 192       | h1::h2::tl when h1 = h2 -> uniq (h2 :: tl)
 193       | h1::tl (* when h1 <> h2 *) -> h1 :: uniq tl
 194     in
 195     uniq l
 196   with
 197     exn -> raise exn (* no errors should be accepted *)
 198