helm/ocaml/metadata/metadataQuery.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 type cardinality_condition =
  29   | Eq of int
  30   | Gt of int
  31
  32 let tbln n = "table" ^ string_of_int n
  33
  34 let add_depth_constr depth_opt cur_tbl where =
  35   match depth_opt with
  36   | None -> where
  37   | Some depth -> (sprintf "%s.h_depth = %d" cur_tbl depth) :: where
  38
  39 let add_card_constr tbl (n,from,where) = function
  40   | None -> (n,from,where)
  41   | Some (Eq card) ->
  42       (n+1,
  43        (sprintf "%s as %s" tbl (tbln n) :: from),
  44        (sprintf "no=%d" card ::
  45         (if n=0 then []
  46         else [sprintf "table0.source = %s.source" (tbln n)]) @
  47         where))
  48   | Some (Gt card) ->
  49       (n+1,
  50        (sprintf "%s as %s" tbl (tbln n) :: from),
  51        (sprintf "no>%d" card ::
  52         (if n=0 then []
  53         else [sprintf "table0.source = %s.source" (tbln n)]) @
  54         where))
  55
  56 let at_least ~(dbh:Dbi.connection) ?concl_card ?full_card
  57   (metadata: MetadataTypes.metadata list)
  58 =
  59   if (metadata = []) && concl_card = None && full_card = None then
  60     failwith "MetadataQuery.at_least: no constraints given";
  61   let add_constraint (n,from,where) metadata =
  62     let cur_tbl = tbln n in
  63     match metadata with
  64     | `Obj (uri, pos, depth_opt) ->
  65         let tbl = MetadataTypes.obj_tbl in
  66         let pos_str = MetadataPp.pp_position pos in
  67         let from = (sprintf "%s as %s" tbl cur_tbl) :: from in
  68         let where =
  69           (sprintf "%s.h_position = \"%s\"" cur_tbl pos_str) ::
  70           (sprintf "%s.h_occurrence = \"%s\"" cur_tbl uri) ::
  71           (if n=0 then []
  72           else [sprintf "table0.source = %s.source" cur_tbl]) @
  73           where
  74         in
  75         let where = add_depth_constr depth_opt cur_tbl where in
  76         ((n+1), from, where)
  77     | `Rel (pos, depth) ->
  78         let tbl = MetadataTypes.rel_tbl in
  79         let pos_str = MetadataPp.pp_position (pos :> MetadataTypes.position) in
  80         let from = (sprintf "%s as %s" tbl cur_tbl) :: from in
  81         let where =
  82           (sprintf "%s.h_position = \"%s\"" cur_tbl pos_str) ::
  83           (if n=0 then []
  84           else [sprintf "table0.source = %s.source" cur_tbl]) @
  85           where
  86         in
  87         let where = add_depth_constr (Some depth) cur_tbl where in
  88         ((n+1), from, where)
  89     | `Sort (sort, pos, depth) ->
  90         let tbl = MetadataTypes.sort_tbl in
  91         let pos_str = MetadataPp.pp_position (pos :> MetadataTypes.position) in
  92         let sort_str = MetadataPp.pp_sort sort in
  93         let from = (sprintf "%s as %s" tbl cur_tbl) :: from in
  94         let where =
  95           (sprintf "%s.h_position = \"%s\"" cur_tbl pos_str) ::
  96           (sprintf "%s.h_sort = \"%s\"" cur_tbl sort_str) ::
  97           (if n=0 then []
  98           else [sprintf "table0.source = %s.source" cur_tbl]) @
  99           where
 100         in
 101         let where = add_depth_constr (Some depth) cur_tbl where in
 102         ((n+1), from, where)
 103   in
 104   let (n,from,where) = List.fold_left add_constraint (0,[],[]) metadata in
 105   let (n,from,where) =
 106     add_card_constr MetadataTypes.conclno_tbl (n,from,where) concl_card
 107   in
 108   let (n,from,where) =
 109     add_card_constr MetadataTypes.conclno_hyp_tbl (n,from,where) full_card
 110   in
 111   let from = String.concat ", " from in
 112   let where = String.concat " and " where in
 113   let query = sprintf "select table0.source from %s where %s" from where in
 114 prerr_endline query;
 115   let query = dbh#prepare query in
 116   query#execute [];
 117   List.map (function [`String s] -> s | _ -> assert false) (query#fetchall ())
 118