(* 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 ())