--- /dev/null
+(* Copyright (C) 2004, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+open Printf
+
+type cardinality_condition =
+ | Eq of int
+ | Gt of int
+
+let tbln n = "table" ^ string_of_int n
+
+let add_depth_constr depth_opt cur_tbl where =
+ match depth_opt with
+ | None -> where
+ | Some depth -> (sprintf "%s.h_depth = %d" cur_tbl depth) :: where
+
+let add_card_constr tbl (n,from,where) = function
+ | None -> (n,from,where)
+ | Some (Eq card) ->
+ (n+1,
+ (sprintf "%s as %s" tbl (tbln n) :: from),
+ (sprintf "no=%d" card ::
+ (if n=0 then []
+ else [sprintf "table0.source = %s.source" (tbln n)]) @
+ where))
+ | Some (Gt card) ->
+ (n+1,
+ (sprintf "%s as %s" tbl (tbln n) :: from),
+ (sprintf "no>%d" card ::
+ (if n=0 then []
+ else [sprintf "table0.source = %s.source" (tbln n)]) @
+ where))
+
+let at_least ~(dbh:Dbi.connection) ?concl_card ?full_card
+ (metadata: MetadataTypes.metadata list)
+=
+ if (metadata = []) && concl_card = None && full_card = None then
+ failwith "MetadataQuery.at_least: no constraints given";
+ let add_constraint (n,from,where) metadata =
+ let cur_tbl = tbln n in
+ match metadata with
+ | `Obj (uri, pos, depth_opt) ->
+ let tbl = MetadataTypes.obj_tbl in
+ let pos_str = MetadataPp.pp_position pos in
+ let from = (sprintf "%s as %s" tbl cur_tbl) :: from in
+ let where =
+ (sprintf "%s.h_position = \"%s\"" cur_tbl pos_str) ::
+ (sprintf "%s.h_occurrence = \"%s\"" cur_tbl uri) ::
+ (if n=0 then []
+ else [sprintf "table0.source = %s.source" cur_tbl]) @
+ where
+ in
+ let where = add_depth_constr depth_opt cur_tbl where in
+ ((n+1), from, where)
+ | `Rel (pos, depth) ->
+ let tbl = MetadataTypes.rel_tbl in
+ let pos_str = MetadataPp.pp_position (pos :> MetadataTypes.position) in
+ let from = (sprintf "%s as %s" tbl cur_tbl) :: from in
+ let where =
+ (sprintf "%s.h_position = \"%s\"" cur_tbl pos_str) ::
+ (if n=0 then []
+ else [sprintf "table0.source = %s.source" cur_tbl]) @
+ where
+ in
+ let where = add_depth_constr (Some depth) cur_tbl where in
+ ((n+1), from, where)
+ | `Sort (sort, pos, depth) ->
+ let tbl = MetadataTypes.sort_tbl in
+ let pos_str = MetadataPp.pp_position (pos :> MetadataTypes.position) in
+ let sort_str = MetadataPp.pp_sort sort in
+ let from = (sprintf "%s as %s" tbl cur_tbl) :: from in
+ let where =
+ (sprintf "%s.h_position = \"%s\"" cur_tbl pos_str) ::
+ (sprintf "%s.h_sort = \"%s\"" cur_tbl sort_str) ::
+ (if n=0 then []
+ else [sprintf "table0.source = %s.source" cur_tbl]) @
+ where
+ in
+ let where = add_depth_constr (Some depth) cur_tbl where in
+ ((n+1), from, where)
+ in
+ let (n,from,where) = List.fold_left add_constraint (0,[],[]) metadata in
+ let (n,from,where) =
+ add_card_constr MetadataTypes.conclno_tbl (n,from,where) concl_card
+ in
+ let (n,from,where) =
+ add_card_constr MetadataTypes.conclno_hyp_tbl (n,from,where) full_card
+ in
+ let from = String.concat ", " from in
+ let where = String.concat " and " where in
+ let query = sprintf "select table0.source from %s where %s" from where in
+prerr_endline query;
+ let query = dbh#prepare query in
+ query#execute [];
+ List.map (function [`String s] -> s | _ -> assert false) (query#fetchall ())
+
--- /dev/null
+(* Copyright (C) 2004, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+ (** constraing on the number of distinct constants *)
+type cardinality_condition =
+ | Eq of int
+ | Gt of int
+
+ (** @param concl_card cardinality condition on conclusion only
+ * @param full_card cardinality condition on the whole statement
+ * @return list of URI satisfying given constraints *)
+val at_least:
+ dbh:Dbi.connection ->
+ ?concl_card:cardinality_condition ->
+ ?full_card:cardinality_condition ->
+ MetadataTypes.metadata list ->
+ string list
+
projects / helm.git / commitdiff