(* 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 
  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 
    find 1 context
  with Failure s -> 
    []
;;     

let depth = 6;;

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

exception NoOtherChoices;;
let rec auto dbd = function
    [] -> []
  | (proof, [], sign)::tl -> (proof, [], sign)::tl
  | (proof, (goal,0)::_, _)::tl -> auto dbd tl
  | (proof, (((goal,depth)::gtl) as allg), sign)::tl -> 
      (* first we check if the metavariable has not been already
         closed as a side effect by some other application *)
      let facts = (depth = 1) in 
      let name,metasenv,p,statement = 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) ->
            (* the goal is still there *)
            (* 
	    prerr_endline ("CURRENT GOAL = " ^ (CicPp.ppterm ty));
	    prerr_endline ("CURRENT PROOF = " ^ (CicPp.ppterm p));
	    prerr_endline ("CURRENT HYP = " ^ (fst (print_context ey)));
            *)
            (* if the goal contains metavariables we use the input
               signature for at_most constraints *)
            let is_meta_closed = CicUtil.is_meta_closed ty in
	    let sign, new_sign =
	      if is_meta_closed then
		None, Some (MetadataConstraints.signature_of ty)
	      else sign,sign in (* maybe the union ? *)
	    let local_choices =
	      new_search_theorems 
		search_theorems_in_context 
		proof goal (depth-1) [] new_sign in
	    let global_choices =
	      new_search_theorems 
		(fun status -> 
		   List.map snd 
		   (MetadataQuery.hint 
		      ~dbd ~facts:facts ?signature:sign status))
		proof goal (depth-1) [] new_sign in
            (* we proceed depth-first on the current goal. This is
               a MAJOR optimization, since in case of success, and
               if the goal is meta_closed, we may just drop the alternatives
	       tl1, avoiding useless backtracking. *)
	    let all_choices =
	      local_choices@global_choices in
	      (match (auto dbd all_choices) 
	       with
		   [] -> auto dbd tl
		 | (proof,[],_)::tl1 -> 
		     let all_choices =
		       let gtl' = List.map fst gtl in
			 if (gtl = [] || is_meta_closed) then 
			   (proof,gtl,sign)::tl
			 else
			   let tl2 = 
			     (List.map 
				(function (p,l,s) -> (p,l@gtl,s)) tl1)
			   in			 
			     (proof,gtl,sign)::tl2@tl in
		       auto dbd all_choices
		 | _ -> assert false)
	| None -> auto dbd ((proof,gtl,sign)::tl) 
;; 


let auto_tac  ~(dbd:Mysql.dbd) =
  let auto_tac dbh (proof,goal) =
  prerr_endline "Entro in Auto";
  match (auto dbd [(proof, [(goal,depth)],None)]) with
      [] ->  prerr_endline("Auto failed");
	raise (ProofEngineTypes.Fail "No Applicable theorem")
    | (proof,[],_)::_ ->  
	prerr_endline "AUTO_TAC HA FINITO";
	(proof,[])
    | _ -> assert false
  in
  ProofEngineTypes.mk_tactic (auto_tac dbd)
;;


(************************** EXPERIMENTAL VERSION ****************************)

(* In this versions of auto_tac we maintain an hash table of all inspected
   goals. We assume that the context is invariant for application. 
   To this aim, it is essential to sall hint_verbose, that in turns calls
   apply_verbose. *)
   

type exitus = 
    No of int 
  | Yes of Cic.term * int 
  | NotYetInspected
	
let inspected_goals = Hashtbl.create 503;;

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 
  let _,metasenv,_,_ = proof in
  let _,context,ty = CicUtil.lookup_meta goal metasenv in
  let rec find n = function 
      [] -> []
    | hd::tl ->
	let res =
	  try 
            Some (PT.apply_tac_verbose ~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 
    find 1 context
  with Failure s -> 
    []
;;     

let new_search_theorems f proof goal depth subst sign =
  let choices = f (proof,goal)
  in 
  List.map 
    (function (local_subst,(proof, goallist)) ->
       let new_subst t= local_subst (subst t) in
       (new_subst,(proof,(List.map (function g -> (g,depth)) goallist), sign)))
    choices 
;;

exception NoOtherChoices;;
let rec auto_new dbd = function
    [] -> []
  | (subst,(proof, [], sign))::tl -> (subst,(proof, [], sign))::tl
  | (subst,(proof, (goal,0)::_, _))::tl -> auto_new dbd tl
  | (subst,(proof, (((goal,depth)::gtl) as allg), sign))::tl ->
      let facts = (depth = 1) in  
      let name,metasenv,p,statement = 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) ->
            (* first of all we check if the goal has been already
               inspected *)
	    let exitus =
	      try Hashtbl.find inspected_goals ty
	      with Not_found -> NotYetInspected in
            let is_meta_closed = CicUtil.is_meta_closed ty in
	    begin
            match exitus with
		Yes (bo,_) ->
                  (*
                  prerr_endline "ALREADY PROVED!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
		  prerr_endline (CicPp.ppterm ty);
                  *)
                  let subst_in =
                    (* if we just apply the subtitution, the type 
                       is irrelevant: we may use Implicit, since it will 
                       be dropped *)
		    CicMetaSubst.apply_subst 
	              [(goal,(ey, bo, Cic.Implicit None))] in
		  let (proof,_) = 
		    ProofEngineHelpers.subst_meta_and_metasenv_in_proof 
		      proof goal subst_in metasenv in
                  let new_subst t = (subst_in (subst t)) in
		  auto_new dbd ((new_subst,(proof,gtl,sign))::tl)
              | No d when (d >= depth) -> 
                  (*
		  prerr_endline "PRUNED!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
                  *)
		  auto_new dbd tl
               
	      | No _ 
	      | NotYetInspected -> 
                  (*
		  prerr_endline ("CURRENT GOAL = " ^ (CicPp.ppterm ty));
		  prerr_endline ("CURRENT PROOF = " ^ (CicPp.ppterm p));
		  prerr_endline ("CURRENT HYP = " ^ (fst (print_context ey)));
                  *)
		  let sign, new_sign =
		    if is_meta_closed then
		      None, Some (MetadataConstraints.signature_of ty)
		    else sign,sign in (* maybe the union ? *)
		  let local_choices =
		    new_search_theorems 
		      search_theorems_in_context 
		      proof goal (depth-1) subst new_sign in
		  let global_choices =
		    new_search_theorems 
		      (fun status -> 
			 List.map snd 
			 (MetadataQuery.experimental_hint 
			    ~dbd ~facts:facts ?signature:sign status))
		      proof goal (depth-1) subst new_sign in
		  let all_choices =
		    local_choices@global_choices in
		  (match (auto_new dbd all_choices) 
		   with
		       [] -> 
			 (* no proof has been found; we update the
			    hastable *)
			 Hashtbl.add inspected_goals ty (No depth);
			 auto_new dbd tl
		     | (new_subst,(proof,[],_))::tl1 -> 
			 (* a proof for goal has been found:
			    in order to get the proof we apply subst to
			    Meta[goal] *)
			 if is_meta_closed  then
			   begin 
			     let irl = 
			       CicMkImplicit.identity_relocation_list_for_metavariable ey in
			     let meta_proof = 
			       new_subst (Cic.Meta(goal,irl)) in
			       Hashtbl.add inspected_goals 
				 ty (Yes (meta_proof,depth));
			   end;
			 let all_choices =
			   let gtl' = List.map fst gtl in
			     if (gtl = [] || is_meta_closed) then 
			       (new_subst,(proof,gtl,sign))::tl
			     else
			       let tl2 = 
				 (List.map 
				    (function (f,(p,l,s)) 
					 -> (f,(p,l@gtl,s))) tl1)
			       in			 
			       (new_subst,(proof,gtl,sign))::tl2@tl in
		       auto_new dbd all_choices
		 | _ -> assert false)
	    end
	| None -> auto_new dbd ((subst,(proof,gtl,sign))::tl) 
;; 


let auto_tac_new  ~(dbd:Mysql.dbd) =
  let auto_tac dbd (proof,goal) =
  Hashtbl.clear inspected_goals;
  prerr_endline "Entro in Auto";
  let id t = t in
  match (auto_new dbd [id,(proof, [(goal,depth)],None)]) with
      [] ->  prerr_endline("Auto failed");
	raise (ProofEngineTypes.Fail "No Applicable theorem")
    | (_,(proof,[],_))::_ ->  
	prerr_endline "AUTO_TAC HA FINITO";
	(proof,[])
    | _ -> assert false
  in
  ProofEngineTypes.mk_tactic (auto_tac dbd)
;;