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