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

let critical_value = 7
let just_factor = 4

module StringSet = Set.Make (String)
module SetSet = Set.Make (StringSet)

type term_signature = (string * string list) option * StringSet.t

type cardinality_condition =
  | Eq of int
  | Gt of int
  | Lt of int

type rating_criterion =
  [ `Hits   (** order by number of hits, most used objects first *)
  ]

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 mk_positions positions cur_tbl =
  "(" ^
  String.concat " or "
    (List.map
      (fun pos ->
        let pos_str = MetadataPp.pp_position_tag pos in
        match pos with
        | `InBody
        | `InConclusion
        | `InHypothesis
        | `MainConclusion None
        | `MainHypothesis None ->
            sprintf "%s.h_position = \"%s\"" cur_tbl pos_str
        | `MainConclusion (Some d)
        | `MainHypothesis (Some d) ->
            sprintf "(%s.h_position = \"%s\" and %s.h_depth = %d)"
              cur_tbl pos_str cur_tbl d)
      (positions :> MetadataTypes.position list)) ^
  ")"

let explode_card_constr = function
  | Eq card -> "=", card
  | Gt card -> ">", card
  | Lt card -> "<", card

let add_card_constr tbl col where = function
  | None -> where
  | Some constr ->
      let op, card = explode_card_constr constr in
      (* count(_utente).hypothesis = 3 *)
      (sprintf "%s.%s %s %d" tbl col op card :: where)

let add_diff_constr tbl where = function
  | None -> where
  | Some constr ->
      let op, card = explode_card_constr constr in
      (sprintf "%s.hypothesis - %s.conclusion %s %d" tbl tbl op card :: where)
      
let add_all_constr tbl (n,from,where) concl full diff =
  match (concl, full, diff) with
  | None, None, None -> (n,from,where)
  | _ -> 
      let where = add_card_constr tbl "conclusion" where concl in
      let where = add_card_constr tbl "statement" where full in
      let where = add_diff_constr tbl where diff in
      (n,tbl :: from, 
        (if n > 0 then 
          sprintf "table0.source = %s.source" tbl :: where 
        else
          where))
      

let add_constraint tables (n,from,where) metadata =
  let obj_tbl,rel_tbl,sort_tbl,count_tbl = tables 
  in
  let cur_tbl = tbln n in
  match metadata with
  | `Obj (uri, positions) ->
      let from = (sprintf "%s as %s" obj_tbl cur_tbl) :: from in
      let where = 
        (sprintf "(%s.h_occurrence = \"%s\")" cur_tbl uri) ::
        mk_positions positions cur_tbl ::
        (if n=0 then []
        else [sprintf "table0.source = %s.source" cur_tbl]) @ 
        where
      in
      ((n+2), from, where)
  | `Rel positions ->
      let from = (sprintf "%s as %s" rel_tbl cur_tbl) :: from in
      let where =
        mk_positions positions cur_tbl ::
        (if n=0 then []
        else [sprintf "table0.source = %s.source" cur_tbl]) @ 
        where
      in
      ((n+2), from, where)
  | `Sort (sort, positions) ->
      let sort_str = CicPp.ppsort sort in
      let from = (sprintf "%s as %s" sort_tbl cur_tbl) :: from in
      let where =
        (sprintf "%s.h_sort = \"%s\"" cur_tbl sort_str ) ::
            mk_positions positions cur_tbl ::
        (if n=0 then 
          []
        else 
          [sprintf "table0.source = %s.source" cur_tbl ]) @ where
      in
      ((n+2), from, where)


let at_least ~(dbd:Mysql.dbd) ?concl_card ?full_card ?diff ?rating tables
  (metadata: MetadataTypes.constr list)
=
  let obj_tbl,rel_tbl,sort_tbl, count_tbl = tables 
  in
  if (metadata = []) && concl_card = None && full_card = None then
    failwith "MetadataQuery.at_least: no constraints given";
  let (n,from,where) =
    List.fold_left (add_constraint tables) (0,[],[]) metadata
  in
  let selected = if metadata = [] then count_tbl else "table0" in
  let (n,from,where) =
    add_all_constr count_tbl (n,from,where) concl_card full_card diff
  in
  let from = String.concat ", " from in
  let where = String.concat " and " where in
  let query =
    match rating with
    | None -> sprintf "select %s.source from %s where %s" selected from where
    | Some `Hits ->
        sprintf
          ("select %s.source from %s, hits where %s"
           ^^ " and hits.source = %s.source order by hits.no desc")
          selected from where selected
  in
  prerr_endline query; 
  let result = Mysql.exec dbd query in
  Mysql.map result
    (fun row -> match row.(0) with Some s -> s | _ -> assert false)

    
let at_least  
  ~(dbd:Mysql.dbd) ?concl_card ?full_card ?diff ?rating
      (metadata: MetadataTypes.constr list)
=
  let module MT = MetadataTypes in
  if MT.are_tables_ownerized () then
    (at_least ~dbd ?concl_card ?full_card ?diff ?rating
      (MT.obj_tbl (),MT.rel_tbl (),MT.sort_tbl (), MT.count_tbl ())
        metadata)
        @
    (at_least ~dbd ?concl_card ?full_card ?diff ?rating
      (MT.library_obj_tbl,MT.library_rel_tbl,MT.library_sort_tbl,
      MT.library_count_tbl) 
        metadata)
  else
    at_least ~dbd ?concl_card ?full_card ?diff ?rating
      (MT.library_obj_tbl,MT.library_rel_tbl,MT.library_sort_tbl,
       MT.library_count_tbl) 
        metadata 
  
    
  (** Prefix handling *)

let filter_by_card n =
  SetSet.filter (fun t -> (StringSet.cardinal t) <= n)
  
let merge n a b = 
  let init = SetSet.union a b in
  let merge_single_set s1 b = 
    SetSet.fold 
      (fun s2 res -> SetSet.add (StringSet.union s1 s2) res)
      b SetSet.empty in
  let res = 
    SetSet.fold (fun s1 res -> SetSet.union (merge_single_set s1 b) res) a init
  in
  filter_by_card n res 

let rec inspect_children n childs =
  List.fold_left 
    (fun res term -> merge n (inspect_conclusion n term) res)
    SetSet.empty childs 

and add_root n root childs =
  let childunion = inspect_children n childs in
  let addroot = StringSet.add root in
    SetSet.fold 
      (fun child newsets -> SetSet.add (addroot child) newsets)
      childunion 
      (SetSet.singleton (StringSet.singleton root))

and inspect_conclusion n t = 
  if n = 0 then SetSet.empty
  else match t with
      Cic.Rel _                    
    | Cic.Meta _                     
    | Cic.Sort _ 
    | Cic.Implicit _ -> SetSet.empty 
    | Cic.Var (u,exp_named_subst) -> SetSet.empty
    | Cic.Const (u,exp_named_subst) -> 
        SetSet.singleton (StringSet.singleton (UriManager.string_of_uri u))
    | Cic.MutInd (u, t, exp_named_subst) -> 
	SetSet.singleton (StringSet.singleton
          (UriManager.string_of_uriref (u, [t])))
    | Cic.MutConstruct (u, t, c, exp_named_subst) -> 
	SetSet.singleton (StringSet.singleton
          (UriManager.string_of_uriref (u, [t; c])))
    | Cic.Cast (t, _) -> inspect_conclusion n t
    | Cic.Prod (_, s, t) -> 
	merge n (inspect_conclusion n s) (inspect_conclusion n t)
    | Cic.Lambda (_, s, t) ->
	merge n (inspect_conclusion n s) (inspect_conclusion n t)
    | Cic.LetIn (_, s, t) ->
	merge n (inspect_conclusion n s) (inspect_conclusion n t)
    | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
        let suri = UriManager.string_of_uri u in
	add_root (n-1) suri l
    | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
        let suri = UriManager.string_of_uriref (u, [t]) in
	add_root (n-1) suri l
    | Cic.Appl ((Cic.MutConstruct (u, t, c, exp_named_subst))::l)  ->
	let suri = UriManager.string_of_uriref (u, [t; c]) in
	add_root (n-1) suri l
    | Cic.Appl l -> 
	SetSet.empty
    | Cic.MutCase (u, t, tt, uu, m) ->
	SetSet.empty
    | Cic.Fix (_, m) -> 
	SetSet.empty
    | Cic.CoFix (_, m) -> 
	SetSet.empty

let rec inspect_term n t = 
  if n = 0 then
    assert false
  else
    match t with
      Cic.Rel _                    
    | Cic.Meta _                     
    | Cic.Sort _ 
    | Cic.Implicit _ -> None, SetSet.empty 
    | Cic.Var (u,exp_named_subst) -> None, SetSet.empty
    | Cic.Const (u,exp_named_subst) -> 
        Some (UriManager.string_of_uri u), SetSet.empty
    | Cic.MutInd (u, t, exp_named_subst) -> 
        let uri = UriManager.string_of_uriref (u, [t]) in
	Some uri, SetSet.empty
    | Cic.MutConstruct (u, t, c, exp_named_subst) -> 
        let uri = UriManager.string_of_uriref (u, [t; c]) in
	Some uri, SetSet.empty
    | Cic.Cast (t, _) -> inspect_term n t
    | Cic.Prod (_, _, t) -> inspect_term n t
    | Cic.LetIn (_, _, t) -> inspect_term n t
    | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
	let suri = UriManager.string_of_uri u in
	let childunion = inspect_children (n-1) l in
	Some suri, childunion
    | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
	let suri = UriManager.string_of_uriref (u, [t]) in
	if u = HelmLibraryObjects.Logic.eq_URI && n>1 then
	  (* equality is handled in a special way: in particular, 
             the type, if defined, is always added to the prefix, 
	     and n is not decremented - it should have been n-2 *)
	  match l with
	      Cic.Const (u1,exp_named_subst1)::l1 ->
		let suri1 = UriManager.string_of_uri u1 in
		let inconcl = add_root (n-1) suri1 l1 in
		Some suri, inconcl
	    | Cic.MutInd (u1, t1, exp_named_subst1)::l1 ->
		let suri1 = UriManager.string_of_uriref (u1, [t1]) in
		let inconcl = add_root (n-1) suri1 l1 in  
		Some suri, inconcl
	    | Cic.MutConstruct (u1, t1, c1, exp_named_subst1)::l1 ->
                let suri1 = UriManager.string_of_uriref (u1, [t1; c1]) in
		let inconcl = add_root (n-1) suri1 l1 in  
		Some suri, inconcl
	    | _ :: _ -> Some suri, SetSet.empty
	    | _ -> assert false (* args number must be > 0 *)
	else
	  let childunion = inspect_children (n-1) l in
	  Some suri, childunion
    | Cic.Appl ((Cic.MutConstruct (u, t, c, exp_named_subst))::l)  ->
	let suri = UriManager.string_of_uriref (u, [t; c]) in
	let childunion = inspect_children (n-1) l in
	Some suri, childunion
    | _ -> None, SetSet.empty

let add_cardinality s =
  let l = SetSet.elements s in
  let res = 
    List.map 
      (fun set -> 
	 let el = StringSet.elements set in
	 (List.length el, el)) l in
    (* ordered by descending cardinality *)
    List.sort (fun (n,_) (m,_) -> m - n) ((0,[])::res)

let prefixes n t =
  match inspect_term n t with
      Some a, set -> Some a, add_cardinality set
    | None, set when (SetSet.is_empty set) -> None, []
    | _, _ -> assert false


let rec add children =
  List.fold_left
    (fun acc t -> StringSet.union (signature_concl t) acc)
    (StringSet.empty) children
  
(* this function creates the set of all different constants appearing in 
   the conclusion of the term *)
and signature_concl = 
  function
      Cic.Rel _                    
    | Cic.Meta _                     
    | Cic.Sort _ 
    | Cic.Implicit _ -> StringSet.empty 
    | Cic.Var (u,exp_named_subst) -> StringSet.empty
    | Cic.Const (u,exp_named_subst) -> 
        StringSet.singleton (UriManager.string_of_uri u)
    | Cic.MutInd (u, t, exp_named_subst) -> 
        let uri = UriManager.string_of_uriref (u, [t]) in
	StringSet.singleton uri
    | Cic.MutConstruct (u, t, c, exp_named_subst) -> 
        let uri = UriManager.string_of_uriref (u, [t;c]) in
	StringSet.singleton uri
    | Cic.Cast (t, _) -> signature_concl t
    | Cic.Prod (_, s, t) -> 
	StringSet.union (signature_concl s) (signature_concl t)
    | Cic.Lambda (_, s, t) ->
	StringSet.union (signature_concl s) (signature_concl t)
    | Cic.LetIn (_, s, t) ->
	StringSet.union (signature_concl s) (signature_concl t)
    | Cic.Appl l  -> add l
    | Cic.MutCase _
    | Cic.Fix _
    | Cic.CoFix _ ->
	StringSet.empty

let rec signature_of = function
  | Cic.Cast (t, _)      -> signature_of t
  | Cic.Prod (_, _, t)   -> signature_of t               
  | Cic.LetIn (_, _, t) -> signature_of t
  | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
      let suri = UriManager.string_of_uri u in
      Some (suri, []), add l
  | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
      let suri = UriManager.string_of_uriref (u, [t]) in
      if u = HelmLibraryObjects.Logic.eq_URI then
	  (* equality is handled in a special way: in particular, 
             the type, if defined, is always added to the prefix, 
	     and n is not decremented - it should have been n-2 *)
      match l with
	  Cic.Const (u1,exp_named_subst1)::l1 ->
	    let suri1 = UriManager.string_of_uri u1 in
	    let inconcl = StringSet.remove suri1 (add l1) in
            Some (suri, [suri1]), inconcl
	| Cic.MutInd (u1, t1, exp_named_subst1)::l1 ->
	    let suri1 = UriManager.string_of_uriref (u1, [t1]) in
	    let inconcl =  StringSet.remove suri1 (add l1) in
	      Some (suri, [suri1]), inconcl
	| Cic.MutConstruct (u1, t1, c1, exp_named_subst1)::l1 ->
            let suri1 = UriManager.string_of_uriref (u1, [t1;c1]) in
	    let inconcl =  StringSet.remove suri1 (add l1) in
            Some (suri, [suri1]), inconcl
	| _ :: _ -> Some (suri, []), StringSet.empty
	| _ -> assert false (* args number must be > 0 *)
      else
	Some (suri, []), add l
  | Cic.Appl ((Cic.MutConstruct (u, t, c, exp_named_subst))::l)  ->
      let suri = UriManager.string_of_uriref (u, [t;c]) in
      Some (suri, []), add l
  | t -> None, signature_concl t

(* takes a list of lists and returns the list of all elements
   without repetitions *)
let union l = 
  let rec drop_repetitions = function
      [] -> []
    | [a] -> [a]
    | u1::u2::l when u1 = u2 -> drop_repetitions (u2::l)
    | u::l -> u::(drop_repetitions l) in
  drop_repetitions (List.sort Pervasives.compare (List.concat l))

let must_of_prefix ?(where = `Conclusion) m s =
  let positions =
    match where with
    | `Conclusion -> [`InConclusion]
    | `Statement -> [`InConclusion; `InHypothesis; `MainHypothesis None]
  in
  let s' = List.map (fun u -> `Obj (u, positions)) s in
  `Obj (m, [`MainConclusion None]) :: s'

let escape = Str.global_replace (Str.regexp_string "\'") "\\'"

let get_constants (dbd:Mysql.dbd) ~where uri =
  let uri = escape uri in
  let positions =
    match where with
    | `Conclusion -> [ MetadataTypes.mainconcl_pos; MetadataTypes.inconcl_pos ]
    | `Statement ->
        [ MetadataTypes.mainconcl_pos; MetadataTypes.inconcl_pos;
          MetadataTypes.inhyp_pos; MetadataTypes.mainhyp_pos ]
  in
  let query = 
    let pos_predicate =
      String.concat " OR "
        (List.map (fun pos -> sprintf "(h_position = \"%s\")" pos) positions)
    in
    sprintf ("SELECT h_occurrence FROM %s WHERE source=\"%s\" AND (%s) UNION "^^
             "SELECT h_occurrence FROM %s WHERE source=\"%s\" AND (%s)")
      (MetadataTypes.obj_tbl ()) uri pos_predicate
      MetadataTypes.library_obj_tbl uri pos_predicate
      
  in
  let result = Mysql.exec dbd query in
  let set = ref StringSet.empty in
  Mysql.iter result
    (fun col ->
      match col.(0) with
      | Some uri -> set := StringSet.add uri !set
      | _ -> assert false);
  !set

let at_most ~(dbd:Mysql.dbd) ?(where = `Conclusion) only u =
  let inconcl = get_constants dbd ~where u in
  StringSet.subset inconcl only

  (* Special handling of equality. The problem is filtering out theorems just
  * containing variables (e.g. all the theorems in cic:/Coq/Ring/). Really
  * ad-hoc, no better solution found at the moment *)
let myspeciallist_of_facts  =
  [0,"cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)"]
let myspeciallist =
  [0,"cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)";
(*   0,"cic:/Coq/Init/Logic/sym_eq.con"; *)
   0,"cic:/Coq/Init/Logic/trans_eq.con";
   0,"cic:/Coq/Init/Logic/f_equal.con";
   0,"cic:/Coq/Init/Logic/f_equal2.con";
   0,"cic:/Coq/Init/Logic/f_equal3.con"]


let compute_exactly ~(dbd:Mysql.dbd) ?(facts=false) ~where main prefixes =
  List.concat
    (List.map 
      (fun (m,s) -> 
        if ((m = 0) && (main = HelmLibraryObjects.Logic.eq_XURI)) then
          (if facts then myspeciallist_of_facts
	   else myspeciallist)
        else
          let res =
            let must = must_of_prefix ~where main s in
            match where with
            | `Conclusion -> at_least ~dbd ~concl_card:(Eq (m+1)) must
            | `Statement -> at_least ~dbd ~full_card:(Eq (m+1)) must
          in
          List.map (fun uri -> (m, uri)) res)
      prefixes)

  (* critical value reached, fallback to "only" constraints *)

let compute_with_only ~(dbd:Mysql.dbd) ?(facts=false) ?(where = `Conclusion) 
  main prefixes constants
=
  let max_prefix_length = 
    match prefixes with
    | [] -> assert false 
    | (max,_)::_ -> max in
  let maximal_prefixes = 
    let rec filter res = function 
        [] -> res
      | (n,s)::l when n = max_prefix_length -> filter ((n,s)::res) l
      | _::_-> res in
    filter [] prefixes in
  let greater_than =
    let all =
      union
        (List.map 
          (fun (m,s) -> 
            let must = must_of_prefix ~where main s in
            (let res = 
              match where with
              | `Conclusion -> at_least ~dbd ~concl_card:(Gt (m+1)) must
              | `Statement -> at_least ~dbd ~full_card:(Gt (m+1)) must
            in
            (* we tag the uri with m+1, for sorting purposes *)
            List.map (fun uri -> (m+1, uri)) res))
          maximal_prefixes)
    in
    List.filter (function (_,uri) -> at_most ~dbd ~where constants uri) all in
    let equal_to = compute_exactly ~dbd ~facts ~where main prefixes in
    greater_than @ equal_to

  (* real match query implementation *)

let cmatch ~(dbd:Mysql.dbd)  ?(facts=false) t =
  let (main, constants) = signature_of t in
  match main with
  | None -> []
  | Some (main, types) ->
      (* the type of eq is not counted in constants_no *)
      let types_no = List.length types in
      let constants_no = StringSet.cardinal constants in
      if (constants_no > critical_value) then 
        let prefixes = prefixes just_factor t in
        (match prefixes with
        | Some main, all_concl ->
            let all_constants = 
              List.fold_right StringSet.add types (StringSet.add main constants)
            in
            compute_with_only ~dbd ~facts main all_concl all_constants
         | _, _ -> [])
      else
        (* in this case we compute all prefixes, and we do not need
           to apply the only constraints *)
        let prefixes =
          if constants_no = 0 then
	    (if types_no = 0 then
	       Some main, [0, []]
	     else
	       Some main, [0, []; types_no, types])
          else
            prefixes (constants_no+types_no+1) t
        in
        (match prefixes with
           Some main, all_concl ->
	     compute_exactly ~dbd ~facts ~where:`Conclusion main all_concl
(*
             List.concat
               (List.map 
                  (fun (m,s) -> 
                    let must = must_of_prefix ~where:`Conclusion main s in
                    let res = at_least ~dbd ~concl_card:(Eq (m+1)) must in
                    List.map (fun uri -> (m, uri)) res)
                  all_concl) *)
         | _, _ -> [])

let power_upto upto consts =
  let l = StringSet.elements consts in
  List.sort (fun (n,_) (m,_) -> m - n)
  (List.fold_left 
    (fun res a ->
       List.filter (function (n,l) -> n <= upto)
       res@(List.map (function (n,l) -> (n+1,a::l)) res)) 
     [(0,[])] l)

let power consts =
  let l = StringSet.elements consts in
  List.sort (fun (n,_) (m,_) -> m - n)
  (List.fold_left 
    (fun res a -> res@(List.map (function (n,l) -> (n+1,a::l)) res)) 
     [(0,[])] l)

type where = [ `Conclusion | `Statement ]

let sigmatch ~(dbd:Mysql.dbd) 
  ?(facts=false) ?(where = `Conclusion) (main, constants) =
  match main with
    None -> []
  | Some (main, types) ->
      let constants_no = StringSet.cardinal constants in
      if (constants_no > critical_value) then 
        let subsets = 
          let subsets = power_upto just_factor constants in
          let types_no = List.length types in
          List.map (function (n,l) -> (n+types_no,types@l)) subsets
        in
        let all_constants = 
          List.fold_right StringSet.add types (StringSet.add main constants)
        in
        compute_with_only ~dbd ~where main subsets all_constants
      else
        let subsets = 
          let subsets = power constants in
          let types_no = List.length types in
	  if types_no > 0 then  
          (0,[]) :: List.map (function (n,l) -> (n+types_no,types@l)) subsets
	  else subsets
        in
        compute_exactly ~dbd ~facts ~where main subsets

  (* match query wrappers *)

let cmatch'= cmatch 

let cmatch ~dbd ?(facts=false) term =
  List.map snd
    (List.sort
      (fun x y -> Pervasives.compare (fst y) (fst x))
      (cmatch' ~dbd ~facts term))

let constants_of = signature_concl