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 count_tbl = MetadataTypes.count_tbl () in
  51   let statements = [
  52     sprintf "DROP TABLE %s ;" obj_tbl;
  53     sprintf "DROP TABLE %s ;" sort_tbl;
  54     sprintf "DROP TABLE %s ;" rel_tbl;
  55     sprintf "DROP TABLE %s ;" name_tbl;
  56     sprintf "DROP TABLE %s ;" count_tbl
  57     (*sprintf "DROP TABLE %s ;" conclno_tbl;
  58     sprintf "DROP TABLE %s ;" conclno_hyp_tbl*) ] in
  59 (*
  60 DROP INDEX refObj_source ON refObj (source);
  61 DROP INDEX refObj_target ON refObj (h_occurrence);
  62 DROP INDEX refObj_position ON refObj (h_position);
  63 DROP INDEX refSort_source ON refSort (source);
  64 DROP INDEX objectName_value ON objectName (value);
  65 DROP INDEX no_inconcl_aux_source ON no_inconcl_aux (source);
  66 DROP INDEX no_inconcl_aux_no ON no_inconcl_aux (no);
  67 DROP INDEX no_concl_hyp_source ON no_concl_hyp (source);
  68 DROP INDEX no_concl_hyp_no ON no_concl_hyp (no);
  69 *)
  70   let owned_uris =
  71     try
  72       MetadataDb.clean ~dbd
  73     with Mysql.Error _ as exn ->
  74       match Mysql.errno dbd with
  75       | Mysql.No_such_table -> []
  76       | _ -> raise exn
  77   in
  78   List.iter
  79     (fun uri ->
  80       let uri = Pcre.replace ~rex:xpointer_RE ~templ:"" uri in
  81       List.iter
  82         (fun suffix -> Http_getter.unregister (uri ^ suffix))
  83         [""; ".body"; ".types"])
  84     owned_uris;
  85   List.iter (fun statement ->
  86     try
  87       ignore (Mysql.exec dbd statement)
  88     with Mysql.Error _ as exn ->
  89       match Mysql.errno dbd with
  90       | Mysql.Bad_table_error -> ()
  91       | _ -> raise exn
  92     ) statements;
  93 ;;
  94
  95 let create_owner_environment () =
  96   let dbd = instance () in
  97   let owner = (Helm_registry.get "matita.owner") in
  98   let obj_tbl = MetadataTypes.obj_tbl () in
  99   let sort_tbl = MetadataTypes.sort_tbl () in
 100   let rel_tbl = MetadataTypes.rel_tbl () in
 101   let name_tbl =  MetadataTypes.name_tbl () in
 102   (*let conclno_tbl = MetadataTypes.conclno_tbl () in
 103   let conclno_hyp_tbl = MetadataTypes.fullno_tbl ()*)
 104   let count_tbl = MetadataTypes.count_tbl () in
 105   let statements = [
 106     sprintf "CREATE TABLE %s (
 107                   source varchar(255) binary not null,
 108                   h_occurrence varchar(255) binary not null,
 109                   h_position varchar(255) binary not null,
 110                   h_depth integer
 111               );" obj_tbl;
 112     sprintf "CREATE TABLE %s (
 113                   source varchar(255) binary not null,
 114                   h_position varchar(255) binary not null,
 115                   h_depth integer not null,
 116                   h_sort varchar(255) binary not null
 117               );" sort_tbl;
 118     sprintf "CREATE TABLE %s (
 119                   source varchar(255) binary not null,
 120                   h_position varchar(255) binary not null,
 121                   h_depth integer not null
 122               );" rel_tbl;
 123     sprintf "CREATE TABLE %s (
 124                   source varchar(255) binary not null,
 125                   value varchar(255) binary not null
 126               );" name_tbl;
 127    sprintf "CREATE TABLE %s (
 128     source varchar(255) binary unique not null,
 129     conclusion smallint(6) not null,
 130     hypothesis smallint(6) not null,
 131     statement smallint(6) not null
 132 );" count_tbl
 133
 134    (* sprintf "CREATE TABLE %s (
 135                   source varchar(255) binary not null,
 136                   no tinyint(4) not null
 137               );" conclno_tbl;
 138     sprintf "CREATE TABLE %s (
 139                   source varchar(255) binary not null,
 140                   no tinyint(4) not null
 141               );" conclno_hyp_tbl *)] in
 142 (*
 143 CREATE INDEX refObj_source ON refObj (source);
 144 CREATE INDEX refObj_target ON refObj (h_occurrence);
 145 CREATE INDEX refObj_position ON refObj (h_position);
 146 CREATE INDEX refSort_source ON refSort (source);
 147 CREATE INDEX objectName_value ON objectName (value);
 148 CREATE INDEX no_inconcl_aux_source ON no_inconcl_aux (source);
 149 CREATE INDEX no_inconcl_aux_no ON no_inconcl_aux (no);
 150 CREATE INDEX no_concl_hyp_source ON no_concl_hyp (source);
 151 CREATE INDEX no_concl_hyp_no ON no_concl_hyp (no);
 152 *)
 153   List.iter (fun statement ->
 154     try
 155       ignore (Mysql.exec dbd statement)
 156     with
 157       exn ->
 158          let status = Mysql.status dbd in
 159          match status with
 160          | Mysql.StatusError Mysql.Table_exists_error -> ()
 161          | Mysql.StatusError _ -> raise exn
 162          | _ -> ()
 163       ) statements
 164 ;;
 165
 166 (* removes uri from the ownerized tables, and returns the list of other objects
 167  * (theyr uris) that ref the one removed.
 168  * AFAIK there is no need to return it, since the MatitaTypes.staus should
 169  * contain all defined objects. but to double ckeck we do not garbage the
 170  * metadata...
 171  *)
 172 let remove_uri uri =
 173   let obj_tbl = MetadataTypes.obj_tbl () in
 174   let sort_tbl = MetadataTypes.sort_tbl () in
 175   let rel_tbl = MetadataTypes.rel_tbl () in
 176   let name_tbl =  MetadataTypes.name_tbl () in
 177   (*let conclno_tbl = MetadataTypes.conclno_tbl () in
 178   let conclno_hyp_tbl = MetadataTypes.fullno_tbl () in*)
 179   let count_tbl = MetadataTypes.count_tbl () in
 180
 181   let dbd = instance () in
 182   let suri = UriManager.string_of_uri uri in
 183   let query table suri = sprintf
 184     "DELETE FROM %s WHERE source LIKE '%s%%'" table (Mysql.escape suri)
 185   in
 186   List.iter (fun t ->
 187     try
 188       ignore (Mysql.exec dbd (query t suri))
 189     with
 190       exn -> raise exn (* no errors should be accepted *)
 191     )
 192   [obj_tbl;sort_tbl;rel_tbl;name_tbl;(*conclno_tbl;conclno_hyp_tbl*)count_tbl];
 193   (* and now the debug job *)
 194   let dbg_q =
 195     sprintf "SELECT source FROM %s WHERE h_occurrence LIKE '%s%%'" obj_tbl suri
 196   in
 197   try
 198     let rc = Mysql.exec dbd dbg_q in
 199     let l = ref [] in
 200     Mysql.iter rc (fun a -> match a.(0) with None ->()|Some a -> l := a:: !l);
 201     let l = List.sort Pervasives.compare !l in
 202     let rec uniq = function
 203       | [] -> []
 204       | h::[] -> [h]
 205       | h1::h2::tl when h1 = h2 -> uniq (h2 :: tl)
 206       | h1::tl (* when h1 <> h2 *) -> h1 :: uniq tl
 207     in
 208     uniq l
 209   with
 210     exn -> raise exn (* no errors should be accepted *)
 211