helm/ocaml/metadata/metadataDb.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 MetadataTypes
  27
  28 open Printf
  29
  30 module DB = Dbi_mysql
  31
  32 (* let baseuri = "http://www.cs.unibo.it/helm/schemas/schema-helm#" *)
  33 let baseuri = ""
  34 let inconcl_uri = baseuri ^ "InConclusion"
  35 let mainconcl_uri = baseuri ^ "MainConclusion"
  36 let mainhyp_uri = baseuri ^ "MainHypothesis"
  37 let inhyp_uri = baseuri ^ "InHypothesis"
  38 let inbody_uri = baseuri ^ "InBody"
  39
  40 let prepare_insert (dbh: Dbi.connection) =
  41   let insert_owner =
  42     dbh#prepare (sprintf "INSERT INTO %s VALUES (\"?\",\"?\")" owners_tbl)
  43   in
  44   let insert_sort =
  45     dbh#prepare (sprintf "INSERT INTO %s VALUES (\"?\",\"?\",?,\"?\")" sort_tbl)
  46   in
  47   let insert_rel =
  48     dbh#prepare (sprintf "INSERT INTO %s VALUES (\"?\",\"?\",?)" rel_tbl)
  49   in
  50   let insert_obj =
  51     dbh#prepare (sprintf "INSERT INTO %s VALUES (\"?\",\"?\",\"?\",?)" obj_tbl)
  52   in
  53   (insert_owner, insert_sort, insert_rel, insert_obj)
  54
  55 let execute_insert dbh (insert_owner, insert_sort, insert_rel, insert_obj)
  56   uri owner (sort_cols, rel_cols, obj_cols)
  57 =
  58   insert_owner#execute [`String uri; `String owner];
  59   List.iter insert_sort#execute sort_cols;
  60   List.iter insert_rel#execute rel_cols;
  61   List.iter insert_obj#execute obj_cols
  62
  63 let insert_const_no dbh uri =
  64   let inconcl_no =
  65     sprintf "INSERT INTO %s SELECT \"%s\", COUNT(DISTINCT h_occurrence) FROM %s WHERE (h_position=\"%s\" OR h_position=\"%s\") AND source LIKE \"%s%%\""
  66       conclno_tbl uri obj_tbl inconcl_uri mainconcl_uri uri
  67   in
  68   let concl_hyp =
  69     sprintf "INSERT INTO %s
  70         SELECT \"%s\",COUNT(DISTINCT h_occurrence)
  71         FROM %s
  72         WHERE NOT (h_position=\"%s\") AND (source = \"%s\")"
  73       conclno_hyp_tbl uri obj_tbl inbody_uri uri
  74   in
  75   (dbh#prepare inconcl_no)#execute [];
  76   (dbh#prepare concl_hyp)#execute []
  77
  78 let insert_name ~dbh ~uri ~name =
  79   let query =
  80     dbh#prepare
  81       (sprintf "INSERT INTO %s VALUES (\"%s\", \"%s\")" name_tbl uri name)
  82   in
  83   query#execute []
  84
  85 type dbi_columns =
  86   Dbi.sql_t list list * Dbi.sql_t list list * Dbi.sql_t list list
  87
  88 let index_constant ~dbh =
  89   let query = prepare_insert dbh in
  90   fun ~owner ~uri ~body ~ty  ->
  91     let name = UriManager.name_of_uri uri in
  92     let uri = UriManager.string_of_uri uri in
  93     let metadata = MetadataExtractor.compute ~body ~ty in
  94     let columns = MetadataPp.columns_of_metadata ~about:uri metadata in
  95     execute_insert dbh query uri owner (columns :> dbi_columns);
  96     insert_const_no dbh uri;
  97     insert_name ~dbh ~uri ~name
  98
  99 let index_inductive_def ~dbh =
 100   let query = prepare_insert dbh in
 101   fun ~owner ~uri ~types ->
 102     let metadata = MetadataExtractor.compute_ind ~uri ~types in
 103     let uri_of (a,b,c) = a in
 104     let uris = UriManager.string_of_uri uri :: List.map uri_of metadata in
 105     let uri = UriManager.string_of_uri uri in
 106     let columns = MetadataPp.columns_of_ind_metadata metadata in
 107     execute_insert dbh query uri owner (columns :> dbi_columns);
 108     List.iter (insert_const_no dbh) uris;
 109     List.iter (fun (uri, name, _) -> insert_name ~dbh ~uri ~name) metadata
 110
 111 let clean ~(dbh: Dbi.connection) ~owner =
 112   let owned_uris =  (* list of uris in list-of-columns format *)
 113     let query =
 114       dbh#prepare (sprintf
 115         "SELECT source FROM %s WHERE owner = \"%s\"" owners_tbl owner)
 116     in
 117     query#execute [];
 118     List.map
 119       (function [`String source_col] -> source_col | _ -> assert false)
 120       (query#fetchall ())
 121   in
 122   let del_from tbl =
 123     let query =
 124       dbh#prepare (sprintf "DELETE FROM %s WHERE source LIKE \"?%%\"" tbl)
 125     in
 126     List.iter (fun source_col -> query#execute [`String source_col]) owned_uris
 127   in
 128   List.iter del_from
 129     [sort_tbl; rel_tbl; obj_tbl; conclno_tbl; conclno_hyp_tbl; name_tbl;
 130     owners_tbl]
 131