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

 
(* Da rimuovere, solo per debug*)
let print_context ctx =
    let print_name =
     function
        Cic.Name n -> n
      | Cic.Anonymous -> "_"
    in
     List.fold_right
      (fun i (output,context) ->
        let (newoutput,context') =
         match i with
            Some (n,Cic.Decl t) ->
              print_name n ^ ":" ^ CicPp.pp t context ^ "\n", (Some n)::context
          | Some (n,Cic.Def (t,None)) ->
              print_name n ^ ":=" ^ CicPp.pp t context ^ "\n", (Some n)::context
          | None ->
              "_ ?= _\n", None::context
          | Some (_,Cic.Def (_,Some _)) -> assert false
        in
         output^newoutput,context'
      ) ctx ("",[])
  ;;





let search_theorems_in_context status =
  let (proof, goal) = status in
  let module C = Cic in
  let module R = CicReduction in
  let module S = CicSubstitution in
  let module PET = ProofEngineTypes in 
  let module PT = PrimitiveTactics in 
  prerr_endline "Entro in search_context";
  let _,metasenv,_,_ = proof in
  let _,context,ty = CicUtil.lookup_meta goal metasenv in
  let rec find n = function 
      [] -> []
    | hd::tl ->
	let res =
	  try 
            Some (PET.apply_tactic (PT.apply_tac ~term:(C.Rel n)) status ) 
	  with 
	    PET.Fail _ -> None in
	(match res with
	  Some res -> res::(find (n+1) tl)
	| None -> find (n+1) tl)
  in
  try 
    let res = find 1 context in
    prerr_endline "Ho finito context";
    res 
  with Failure s -> 
    prerr_endline ("SIAM QUI = " ^ s); []
;;     

exception NotAProposition;;
exception NotApplicableTheorem;;
exception MaxDepth;;

let depth = 3;;

(*
let rec auto_tac_aux mqi_handle level proof goal = 
prerr_endline ("Entro in Auto_rec; level = " ^ (string_of_int level));
if level = 0 then
  (* (proof, [goal]) *)
  (prerr_endline ("MaxDepth");
   raise MaxDepth)
else 
  (* let us verify that the metavariable is still an open goal --
     it could have been closed by closing other goals -- and that
     it is of sort Prop *)
  let _,metasenv,_,_ = proof in
  let meta_inf = 
    (try 
       let (_, ey ,ty) = CicUtil.lookup_meta goal metasenv in
	 Some (ey, ty)
     with _ -> None) in
  match meta_inf with
      Some (ey, ty) ->
        prerr_endline ("CURRENT GOAL = " ^ (CicPp.ppterm ty));
        prerr_endline ("CURRENT HYP = " ^ (fst (print_context ey)));
        (* if the goal does not have a sort Prop we return the
	   current proof and a list containing the goal *)
	let ty_sort = CicTypeChecker.type_of_aux' metasenv ey ty in
	  if CicReduction.are_convertible 
	    ey (Cic.Sort Cic.Prop) ty_sort then
	    (* sort Prop *)
	    (* choices is a list of pairs proof and goallist *)
	    let choices  =
	      (search_theorems_in_context (proof,goal))@ 
	      (TacticChaser.searchTheorems mqi_handle (proof,goal)) 
	    in
	    let rec try_choices = function
		[] -> raise NotApplicableTheorem
	      | (proof,goallist)::tl ->
prerr_endline ("GOALLIST = " ^ string_of_int (List.length goallist));
		  (try 
		     List.fold_left 
		       (fun proof goal ->
			    auto_tac_aux mqi_handle (level-1) proof goal)
		       proof goallist
		   with 
		     | MaxDepth
		     | NotApplicableTheorem 
                     | NotAProposition ->
			 try_choices tl) in
	      try_choices choices
	  else
            (* CUT AND PASTE DI PROVA !! *)
            let choices  =
	      (search_theorems_in_context (proof,goal))@ 
	      (TacticChaser.searchTheorems mqi_handle (proof,goal)) 
	    in
	    let rec try_choices = function
		[] -> raise NotApplicableTheorem
	      | (proof,[])::tl -> proof
              | _::tl -> try_choices tl in
	    try_choices choices
	    (* raise NotAProposition *)
    | None -> proof
;;

let auto_tac mqi_handle =
 let module PET = ProofEngineTypes in
 let auto_tac mqi_handle (proof,goal) =
  prerr_endline "Entro in Auto";
  try 
    let proof = auto_tac_aux mqi_handle depth proof goal in
    prerr_endline "AUTO_TAC HA FINITO";
     (proof,[])
  with 
  | MaxDepth -> assert false (* this should happens only if depth is 0 above *)
  | NotApplicableTheorem -> 
      prerr_endline("No applicable theorem");
      raise (ProofEngineTypes.Fail "No Applicable theorem")
 in
  PET.mk_tactic (auto_tac mqi_handle)
;;

*)

(**** ESPERIMENTO ************************)

let new_search_theorems f proof goal depth gtl =
  let local_choices = f (proof,goal)
  in 
  List.map 
    (function (proof, goallist) ->
       (proof, (List.map (function g -> (g,depth)) goallist)@gtl))
    local_choices 
;;

exception NoOtherChoices;;

let rec auto_new dbh = function
    [] -> raise NoOtherChoices
  | (proof, [])::tl -> (proof, [])::tl
  | (proof, (goal,0)::gtl)::tl -> auto_new dbh tl
  | (proof, (goal,depth)::gtl)::tl ->
      let _,metasenv,proof_obj,_ = proof in
      let meta_inf = 
	(try 
	   let (_, ey ,ty) = CicUtil.lookup_meta goal metasenv in
	     Some (ey, ty)
	 with _ -> None) in
	match meta_inf with
	    Some (ey, ty) ->
	       prerr_endline ("CURRENT GOAL = " ^ (CicPp.ppterm ty));
               prerr_endline ("CURRENT HYP = " ^ (fst (print_context ey)));
               prerr_endline ("CURRENT PROOF = " ^ (CicPp.ppterm proof_obj));
	      let local_choices =
		new_search_theorems 
		  search_theorems_in_context proof goal (depth-1) gtl in
	      let global_choices =
		new_search_theorems 
                  (fun status -> List.map snd (MetadataQuery.hint ~dbh status))
(* 		  (TacticChaser.searchTheorems mqi_handle)  *)
		  proof goal (depth-1) gtl in
	      let all_choices =
		local_choices@global_choices@tl in
	      let sorting_list (_,g1) (_,g2) =
	        let l1 = List.length g1 in
	        let l2 = List.length g2 in
		if (l1 = l2 && not(l1 = 0)) then
		(snd(List.nth g2 0)) - (snd(List.nth g1 0))
		else l1 - l2 in
	      let reorder = 
	        List.stable_sort sorting_list all_choices
	      in
		auto_new dbh reorder
	  | None -> auto_new dbh ((proof,gtl)::tl)
;;


let auto_tac ~(dbh:Dbi.connection) =
(*   CicMetaSubst.reset_counters (); *)
 let auto_tac dbh (proof,goal) =
  prerr_endline "Entro in Auto";
  try 
    (match auto_new dbh [(proof, [(goal,depth)])] with
    | (proof,_)::_  ->
      prerr_endline "AUTO_TAC HA FINITO";
  (*     CicMetaSubst.print_counters (); *)
      (proof,[])
    | _ -> assert false)
  with 
  | NoOtherChoices ->
      prerr_endline("Auto failed");
      raise (ProofEngineTypes.Fail "No Applicable theorem")
 in
  ProofEngineTypes.mk_tactic (auto_tac dbh)
;;

(* TODO se ce n'e' piu' di una, prende la prima che trova... sarebbe meglio
chiedere: find dovrebbe restituire una lista di hyp (?) da passare all'utonto con una
funzione di callback che restituisce la (sola) hyp da applicare *)

let assumption_tac =
 let module PET = ProofEngineTypes in
 let assumption_tac status =
  let (proof, goal) = status in
  let module C = Cic in
  let module R = CicReduction in
  let module S = CicSubstitution in
  let module PT = PrimitiveTactics in
   let _,metasenv,_,_ = proof in
    let _,context,ty = CicUtil.lookup_meta goal metasenv in
     let rec find n = function 
        hd::tl -> 
         (match hd with
             (Some (_, C.Decl t)) when
               (R.are_convertible context (S.lift n t) ty) -> n
           | (Some (_, C.Def (_,Some ty'))) when
               (R.are_convertible context ty' ty) -> n
           | (Some (_, C.Def (t,None))) when
               (R.are_convertible context
                (CicTypeChecker.type_of_aux' metasenv context (S.lift n t)) ty) -> n 
           | _ -> find (n+1) tl
         )
      | [] -> raise (PET.Fail "Assumption: No such assumption")
     in PET.apply_tactic (PT.apply_tac ~term:(C.Rel (find 1 context))) status
 in
  PET.mk_tactic assumption_tac
;;

(* ANCORA DA DEBUGGARE *)

exception AllSelectedTermsMustBeConvertible;;

(* serve una funzione che cerchi nel ty dal basso a partire da term, i lambda
e li aggiunga nel context, poi si conta la lunghezza di questo nuovo
contesto e si lifta di tot... COSA SIGNIFICA TUTTO CIO'?????? *)

let generalize_tac 
 ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name) terms
 =
  let module PET = ProofEngineTypes in
  let generalize_tac mk_fresh_name_callback terms status =
   let (proof, goal) = status in
   let module C = Cic in
   let module P = PrimitiveTactics in
   let module T = Tacticals in
    let _,metasenv,_,_ = proof in
    let _,context,ty = CicUtil.lookup_meta goal metasenv in
     let typ =
      match terms with
         [] -> assert false
       | he::tl ->
          (* We need to check that all the convertibility of all the terms *)
          List.iter
           (function t ->
             if not (CicReduction.are_convertible context he t) then 
              raise AllSelectedTermsMustBeConvertible
           ) tl ;
          (CicTypeChecker.type_of_aux' metasenv context he)
     in
      PET.apply_tactic 
      (T.thens 
       ~start:
         (P.cut_tac 
          (C.Prod(
            (mk_fresh_name_callback metasenv context C.Anonymous ~typ:typ), 
            typ,
            (ProofEngineReduction.replace_lifting_csc 1
              ~equality:(==) 
              ~what:terms
              ~with_what:(List.map (function _ -> C.Rel 1) terms)
              ~where:ty)
          )))
       ~continuations: [(P.apply_tac ~term:(C.Rel 1)) ; T.id_tac])
       status
 in
  PET.mk_tactic (generalize_tac mk_fresh_name_callback terms)
;;