(* Copyright (C) 2000-2002, 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://cs.unibo.it/helm/.
 *)


let in_hypothesis = "'http://www.cs.unibo.it/helm/schemas/schema-helm#InHypothesis'" ;;

let main_hypothesis = "'http://www.cs.unibo.it/helm/schemas/schema-helm#MainHypothesis'" ;;

let main_conclusion = "'http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion'" ;;

let in_conclusion = "'http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion'" ;;

let in_body = "'http://www.cs.unibo.it/helm/schemas/schema-helm#InBody'";;

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

let hyp_const (conn:Mysql.dbd) uri =
  let uri = escape uri in
  (*query to obtain all the constants in the hypothesis and conclusion of the theorem*)
  let query =
     "select h_occurrence from refObj where source='"^uri^
    "' and (not (h_position ="^in_body^"))" in
  (*prerr_endline ("$$$$$$$$$$$$$$$"^query);*)
  let result = Mysql.exec conn query in 
  (* now we transform the result in a set *)
  let f a = 
    match (Array.to_list a) with
	[Some uri] -> uri
      | _ -> assert false in
  let result = Mysql.map ~f:f result in
  List.fold_left 
    (fun set uri ->
       NewConstraints.StringSet.add uri set)
    NewConstraints.StringSet.empty result
;;

(* for each uri check if its costants are a subset of
   const, the set of the costants of the proof *)
let filter_new_constants (conn:Mysql.dbd) const (_,uri) =
   let hyp = hyp_const conn uri in
 (*  prerr_endline (NewConstraints.pp_StringSet hyp);*)
    NewConstraints.StringSet.subset hyp const
;;




let rec exec_query (conn:Mysql.dbd) (uris,main) k  = 
  let add_must (n,from,where) uri =
    let refObjn = "refObj" ^ (string_of_int n) in
    let new_must =
      [ refObjn^".h_occurrence = '" ^ uri ^ "'";
        "(not ("^refObjn^".h_position ="^in_body^"))"] in
    let where' = 
      if n = 0 then new_must@where
      else 
       (refObjn^".source = refObj" ^ (string_of_int (n-1)) 
       ^ ".source")::new_must@where in
  (n+1,("refObj as "^refObjn)::from,where')
  in
  let (_,from,where) = 
    List.fold_left add_must (0,[],[]) uris in
  let from,where = 
    ["no_concl_hyp";"refObj as main"]@from, 
    ["no=" ^ (string_of_int k);
     "no_concl_hyp.source = refObj0.source";
     "main.source = refObj0.source";
     "main.h_occurrence = '" ^ main ^ "'";
     "main.h_position = " ^ main_conclusion]@where
  in
  let from = String.concat "," from in
  let where = String.concat " and " where in
  let query = "select distinct(refObj0.source) from " ^ from ^ " where " ^ where in
     (*prerr_endline query;*)
    Mysql.exec conn query
;;

let powerset set =
  let rec powerset_r set sub =
    if (NewConstraints.StringSet.is_empty set) then sub
    else 
      let a = NewConstraints.StringSet.min_elt set in
      let newset = NewConstraints.StringSet.remove a set in
      let newsub = NewConstraints.SetSet.union (NewConstraints.SetSet.add (NewConstraints.StringSet.singleton a)
                   (NewConstraints.SetSet.fold 
		       (fun s t -> (NewConstraints.SetSet.add (NewConstraints.StringSet.add a s) t)) 
		            sub NewConstraints.SetSet.empty)) sub in
      powerset_r newset newsub in
powerset_r set NewConstraints.SetSet.empty
;;

let setset_to_listlist setset =
  let listset = NewConstraints.SetSet.elements setset in
  let res = 
    List.map 
      (fun set -> 
	 let el = NewConstraints.StringSet.elements set in
	 (List.length el, el)) listset in
    (* ordered by descending cardinality *)
List.sort (fun (n,_) (m,_) -> m - n) res

let exist_element list_of_uris (_,uri) =
  let ex u =
    if u = uri then true
    else false
  in
List.exists ex list_of_uris
;;
    

let filter_uris (conn:Mysql.dbd) const uris main =
  let subsets_of_consts = 
    setset_to_listlist (powerset const) in
  let ex u =
    if u = main then true
    else false
  in
  let subsets_of_consts =
  List.filter 
  	(fun (_,b) -> (List.exists ex b)) 
		subsets_of_consts in
  let uris_of_const =
    List.concat
     (List.map 
	      (fun (m,s) -> 
		 (let res = 
		    exec_query conn (s,main) m in
		  let f a = 
		    match (Array.to_list a) with
			[Some uri] -> uri
		        | _ -> assert false in
		    Mysql.map ~f:f res))
	      subsets_of_consts)
      in
List.filter (exist_element uris_of_const) uris
;;  
   
let rec power n m =
  if (m = 1) then n
  else n*(power n (m-1))
;;