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

(*********************************************************************)
(*                                                                   *)
(*                           PROJECT HELM                            *)
(*                                                                   *)
(*                  Andrea Asperti, Matteo Selmi                     *)
(*                           1/04/2004                               *)
(*                                                                   *)
(*                                                                   *)
(*********************************************************************)


(* the file contains:
   - functions executing must, just and only constraints on the mysql
     data base;
   - the general function cmatch for retrieving all statements matching
     a given conclusion
*)

type count_condition =
    NIL | EQ of int | GT of int
;;

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 escape = Str.global_replace (Str.regexp_string "\'") "\\'";;

  
let get_inconcl (conn:Mysql.dbd) uri =
  let uri = escape uri in
  let query = 
    "select h_occurrence from refObj where source='"^uri^
    "' and (h_position="^main_conclusion^" or h_position="^in_conclusion^")" 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
;;

let test_only (conn:Mysql.dbd) only u =
  let inconcl = get_inconcl conn u in
    NewConstraints.StringSet.subset inconcl only
;;

let rec exec_must (conn:Mysql.dbd) (l:MQGTypes.r_obj list) (cc:count_condition) = 
  let add_must (n,from,where) (pos,uri) =
    match pos with
	`MainHypothesis _ -> assert false
      | `MainConclusion None -> 
	  let refObjn = "refObj" ^ (string_of_int n) in
          let new_must =
	    [ refObjn^".h_occurrence = '" ^ uri ^ "'";
	      refObjn^".h_position = " ^ main_conclusion] 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')
      | `MainConclusion(Some(d)) -> 
	  let refObjn = "refObj" ^ (string_of_int n) in
          let new_must =
	    [ refObjn^".h_occurrence = '" ^ uri ^ "'";
	      refObjn^".h_position = " ^ main_conclusion;
	      refObjn^".h_depth = " ^ (string_of_int d)] 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')
      | `InHypothesis -> assert false
      | `InConclusion -> 
	  let refObjn = "refObj" ^ (string_of_int n) in
          let new_must =
	    [ refObjn^".h_occurrence = '" ^ uri ^ "'";
	      refObjn^".h_position = " ^ in_conclusion] 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')
      | `InBody -> assert false
  in
  let (_,from,where) = 
    List.fold_left add_must (0,[],[]) l in
  let from,where = 
    (match cc with
	 NIL -> from, where
       | EQ n -> 
	   "no_inconcl_aux"::from, 
	   ("no=" ^ (string_of_int n))::
	     ("no_inconcl_aux.source = refObj0.source")::where
       | GT n -> 
	   "no_inconcl_aux"::from, 
	   ("no>" ^ (string_of_int n))::
	     ("no_inconcl_aux.source = refObj0.source")::where) in
  let from = String.concat "," from in
  let where = String.concat " and " where in
  let query = "select refObj0.source from " ^ from ^ " where " ^ where in
    prerr_endline query;
    Mysql.exec conn query
;;


let (must_of_prefix m s):MQGTypes.r_obj list =
  let s' = List.map (fun u -> (`InConclusion, u)) s in
  (`MainConclusion None,m)::s'
;;
  
(* 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 critical_value = 6;;
let just_factor = 3;;

let cmatch (conn:Mysql.dbd) t =
  let eq,constants = NewConstraints.constants_of t in
  (* the type of eq is not counted in constants_no *)
  let constants_no = 
    if eq then (NewConstraints.StringSet.cardinal constants)
    else (NewConstraints.StringSet.cardinal constants) in
  if (constants_no > critical_value) then 
    let prefixes = NewConstraints.prefixes just_factor t in
    (match prefixes with
	 Some main, all_concl ->
(*	 
           NewConstraints.pp_prefixes all_concl;
*)
           (* in some cases, max_prefix_length could be less than n *)
	   let max_prefix_length = 
	     match all_concl 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 [] all_concl in
	   let greater_than :(int*string) list=
	     let all =
	       union
		 (List.map 
		    (fun (m,s) -> 
		       (let res = 
			  exec_must conn (must_of_prefix main s) (GT (m+1)) in
			let f a = 
			  match (Array.to_list a) with
			      (* we tag the uri with m+1, for sorting purposes *)
			      [Some uri] -> (m+1,uri)
			    | _ -> assert false in
			  Mysql.map ~f:f res))
		    maximal_prefixes) in
	       List.filter 
		 (function (_,uri) -> test_only conn constants uri) all in
	   let equal_to = 
	     List.concat
	       (List.map 
		  (fun (m,s) -> 
		     (let res = 
			exec_must conn (must_of_prefix main s) (EQ (m+1)) in
		      let f a = 
			match (Array.to_list a) with
			    (* we tag the uri with m, for sorting purposes *)
			    [Some uri] -> (m,uri)
			  | _ -> assert false in
			Mysql.map ~f:f res))
		  all_concl) in
	     greater_than @ equal_to
       | _, _ -> [])
  else if constants_no = 0 then []
  else
    (* in this case we compute all prefixes, and we do not need
       to apply the only constraints *)
    let prefixes = NewConstraints.prefixes constants_no t in
    (match prefixes with
	 Some main, all_concl ->
	   List.concat
	   (List.map 
	      (fun (m,s) -> 
		 (let res = 
		    exec_must conn (must_of_prefix main s) (EQ (m+1)) in
		  let f a = 
		    match (Array.to_list a) with
			(* we tag the uri with m, for sorting purposes *)
			[Some uri] -> (m,uri)
		      | _ -> assert false in
		    Mysql.map ~f:f res))
	      all_concl)
       | _, _ -> [])
;;