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