(* 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                                 *)
(*                                                                            *)
(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
(*                                 18/02/2003                                 *)
(*                                                                            *)
(*                                                                            *)
(******************************************************************************)

module MQI = MQueryInterpreter
module MQIC = MQIConn
module I = MQueryInterpreter
module U = MQGUtil
module G = MQueryGenerator

  (* search arguments on which Apply tactic doesn't fail *)
let matchConclusion mqi_handle ?(output_html = (fun _ -> ())) ~choose_must() ~status =
 let ((_, metasenv, _, _), metano) = status in
 let (_, ey ,ty) = CicUtil.lookup_meta metano metasenv in
  let list_of_must, only = CGMatchConclusion.get_constraints metasenv ey ty in
match list_of_must with
  [] -> []
|_ ->
  let must = choose_must list_of_must only in
  let result =
   I.execute mqi_handle 
      (G.query_of_constraints
        (Some CGMatchConclusion.universe)
        (must,[],[]) (Some only,None,None)) in 
  let uris =
   List.map
    (function uri,_ ->
      MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri
    ) result
  in
  let uris =
    (* TODO ristretto per ragioni di efficienza *)
    prerr_endline "STO FILTRANDO";
    List.filter (fun uri -> Pcre.pmatch ~pat:"^cic:/Coq/" uri) uris
  in
  prerr_endline "HO FILTRATO";
  let uris',exc =
    let rec filter_out =
     function
        [] -> [],""
      | uri::tl ->
         let tl',exc = filter_out tl in
          try
           if
            (try
             ignore
              (PrimitiveTactics.apply_tac
               ~term:(MQueryMisc.term_of_cic_textual_parser_uri
                (MQueryMisc.cic_textual_parser_uri_of_string uri))
               ~status);
             true
            with ProofEngineTypes.Fail _ -> false)
           then
            uri::tl',exc
           else
            tl',exc
          with
           (ProofEngineTypes.Fail _) as e ->
             let exc' =
              "<h1 color=\"red\"> ^ Exception raised trying to apply " ^
               uri ^ ": " ^ Printexc.to_string e ^ " </h1>" ^ exc
             in
              tl',exc'
    in
     filter_out uris
  in
    let html' =
     " <h1>Objects that can actually be applied: </h1> " ^
     String.concat "<br>" uris' ^ exc ^
     " <h1>Number of false matches: " ^
      string_of_int (List.length uris - List.length uris') ^ "</h1>" ^
     " <h1>Number of good matches: " ^
      string_of_int (List.length uris') ^ "</h1>"
    in
     output_html html' ;
     uris'
;;


(*funzione che sceglie il penultimo livello di profondita' dei must*)

(*
let choose_must list_of_must only=
let n = (List.length list_of_must) - 1 in
   List.nth list_of_must n
;;*)

let choose_must list_of_must only =
   List.nth list_of_must 0

(* OLD CODE: TO BE REMOVED
(*Funzione position prende una lista e un elemento e mi ritorna la posizione dell'elem nella lista*)
(*Mi serve per ritornare la posizione del teo che produce meno subgoal*)

exception NotInTheList;;


let position n =
        let rec aux k =
         function
             [] -> raise NotInTheList
            | m::_ when m=n -> k
            | _::tl -> aux (k+1) tl in
        aux 1
;;



(*function taking a status and returning a new status after having searching a theorem to apply ,theorem which *)
(*generate the less number of subgoals*)

let  searchTheorem ~status:(proof,goal) =
  let mqi_flags = [MQIC.Postgres ; MQIC.Stat ; MQIC.Warn ; MQIC.Log] (* default MathQL interpreter options *)
  in
    let mqi_handle = MQIC.init mqi_flags prerr_string
in
  let uris' =
    matchConclusion
      mqi_handle ~choose_must() ~status:(proof, goal)
  in
  let list_of_termin =
    List.map
    (function string ->
    (MQueryMisc.term_of_cic_textual_parser_uri
    (MQueryMisc.cic_textual_parser_uri_of_string string))
    )
    uris'
  in
  let list_proofgoal =
    List.map
    (function term ->
      PrimitiveTactics.apply_tac ~term ~status:(proof,goal))
    list_of_termin
  in
  let (list_of_subgoal: int  list list) =
  List.map  snd list_proofgoal
  in
  let list_of_num =
  List.map List.length list_of_subgoal
  in
  let list_sort =
  List.sort Pervasives.compare list_of_num
  in                                   (*ordino la lista in modo cresc*)
  let min= List.nth  list_sort 0   (*prendo il minimo*)
  in
  let uri' =              (*cerco il teo di pos k*)
  List.nth list_of_termin (position  min list_of_num)
  in
  (* let teo=
    String.sub uri' 4 (String.length uri' - 4)

  (* modifico la str in modo che sia accettata da apply*)
  in*)
  PrimitiveTactics.apply_tac ~term:uri' ~status:(proof,goal)
;;
*)


let  searchTheorems mqi_handle ~status:(proof,goal) =
prerr_endline "1";
  let uris' =
    matchConclusion mqi_handle ~choose_must() ~status:(proof, goal) in
prerr_endline "2";
  let list_of_termin =
    List.map
      (function string ->
         (MQueryMisc.term_of_cic_textual_parser_uri
         (MQueryMisc.cic_textual_parser_uri_of_string string)))
    uris' in
prerr_endline "3";
  let list_proofgoal =
    List.map
      (function term ->
         PrimitiveTactics.apply_tac ~term ~status:(proof,goal)) list_of_termin in
prerr_endline "4";
let res =
  List.sort 
    (fun (_,gl1) (_,gl2) -> 
        Pervasives.compare (List.length gl1) (List.length gl2)) 
    list_proofgoal
    in
prerr_endline "5";
res
;;