helm/matita/matitaDb.ml

   1 (* Copyright (C) 2004, 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 xpointer_RE = Pcre.regexp "#.*$"
  29
  30 let clean_owner_environment () =
  31   let dbd = MatitaMisc.dbd_instance () in
  32   let owner = (Helm_registry.get "matita.owner") in
  33   let obj_tbl = MetadataTypes.obj_tbl () in
  34   let sort_tbl = MetadataTypes.sort_tbl () in
  35   let rel_tbl = MetadataTypes.rel_tbl () in
  36   let name_tbl =  MetadataTypes.name_tbl () in
  37   let conclno_tbl = MetadataTypes.conclno_tbl () in
  38   let conclno_hyp_tbl = MetadataTypes.conclno_hyp_tbl () in
  39   let statements = [
  40     sprintf "DROP TABLE %s ;" obj_tbl;
  41     sprintf "DROP TABLE %s ;" sort_tbl;
  42     sprintf "DROP TABLE %s ;" rel_tbl;
  43     sprintf "DROP TABLE %s ;" name_tbl;
  44     sprintf "DROP TABLE %s ;" conclno_tbl;
  45     sprintf "DROP TABLE %s ;" conclno_hyp_tbl ] in
  46 (*
  47 DROP INDEX refObj_source ON refObj (source);
  48 DROP INDEX refObj_target ON refObj (h_occurrence);
  49 DROP INDEX refObj_position ON refObj (h_position);
  50 DROP INDEX refSort_source ON refSort (source);
  51 DROP INDEX objectName_value ON objectName (value);
  52 DROP INDEX no_inconcl_aux_source ON no_inconcl_aux (source);
  53 DROP INDEX no_inconcl_aux_no ON no_inconcl_aux (no);
  54 DROP INDEX no_concl_hyp_source ON no_concl_hyp (source);
  55 DROP INDEX no_concl_hyp_no ON no_concl_hyp (no);
  56 *)
  57   let owned_uris =
  58     try
  59       MetadataDb.clean ~dbd
  60     with Mysql.Error _ as exn ->
  61       match Mysql.errno dbd with
  62       | Mysql.No_such_table -> []
  63       | _ -> raise exn
  64   in
  65   List.iter
  66     (fun uri ->
  67       let uri = Pcre.replace ~rex:xpointer_RE ~templ:"" uri in
  68       List.iter
  69         (fun suffix -> Http_getter.unregister (uri ^ suffix))
  70         [""; ".body"; ".types"])
  71     owned_uris;
  72   List.iter (fun statement ->
  73     try
  74       ignore (Mysql.exec dbd statement)
  75     with Mysql.Error _ as exn ->
  76       match Mysql.errno dbd with
  77       | Mysql.Bad_table_error -> ()
  78       | _ -> raise exn
  79     ) statements;
  80 ;;
  81
  82 let create_owner_environment () =
  83   let dbd = MatitaMisc.dbd_instance () in
  84   let owner = (Helm_registry.get "matita.owner") in
  85   let obj_tbl = MetadataTypes.obj_tbl () in
  86   let sort_tbl = MetadataTypes.sort_tbl () in
  87   let rel_tbl = MetadataTypes.rel_tbl () in
  88   let name_tbl =  MetadataTypes.name_tbl () in
  89   let conclno_tbl = MetadataTypes.conclno_tbl () in
  90   let conclno_hyp_tbl = MetadataTypes.conclno_hyp_tbl () in
  91   let statements = [
  92     sprintf "CREATE TABLE %s (
  93                   source varchar(255) binary not null,
  94                   h_occurrence varchar(255) binary not null,
  95                   h_position varchar(255) binary not null,
  96                   h_depth integer
  97               );" obj_tbl;
  98     sprintf "CREATE TABLE %s (
  99                   source varchar(255) binary not null,
 100                   h_position varchar(255) binary not null,
 101                   h_depth integer not null,
 102                   h_sort varchar(255) binary not null
 103               );" sort_tbl;
 104     sprintf "CREATE TABLE %s (
 105                   source varchar(255) binary not null,
 106                   h_position varchar(255) binary not null,
 107                   h_depth integer not null
 108               );" rel_tbl;
 109     sprintf "CREATE TABLE %s (
 110                   source varchar(255) binary not null,
 111                   value varchar(255) binary not null
 112               );" name_tbl;
 113     sprintf "CREATE TABLE %s (
 114                   source varchar(255) binary not null,
 115                   no tinyint(4) not null
 116               );" conclno_tbl;
 117     sprintf "CREATE TABLE %s (
 118                   source varchar(255) binary not null,
 119                   no tinyint(4) not null
 120               );" conclno_hyp_tbl ] in
 121 (*
 122 CREATE INDEX refObj_source ON refObj (source);
 123 CREATE INDEX refObj_target ON refObj (h_occurrence);
 124 CREATE INDEX refObj_position ON refObj (h_position);
 125 CREATE INDEX refSort_source ON refSort (source);
 126 CREATE INDEX objectName_value ON objectName (value);
 127 CREATE INDEX no_inconcl_aux_source ON no_inconcl_aux (source);
 128 CREATE INDEX no_inconcl_aux_no ON no_inconcl_aux (no);
 129 CREATE INDEX no_concl_hyp_source ON no_concl_hyp (source);
 130 CREATE INDEX no_concl_hyp_no ON no_concl_hyp (no);
 131 *)
 132   List.iter (fun statement ->
 133     try
 134       ignore (Mysql.exec dbd statement)
 135     with
 136       exn ->
 137          let status = Mysql.status dbd in
 138          match status with
 139          | Mysql.StatusError Mysql.Table_exists_error -> ()
 140          | Mysql.StatusError _ -> raise exn
 141          | _ -> ()
 142       ) statements
 143 ;;
 144