(* Une tactique qui tente de dmontrer toute seule le but courant,
   interruptible par pcoq (si dans le fichier C:\WINDOWS\free il y a un A)
*)
open Ctast;;
open Termops;;
open Nameops;;
open Auto;;
open Clenv;;
open Command;;
open Ctast;;
open Declarations;;
open Declare;;
open Eauto;;
open Environ;;
open Equality;;
open Evd;;
open Hipattern;;
open Inductive;;
open Names;;
open Pattern;;
open Pbp;;
open Pfedit;;
open Pp;;
open Printer
open Proof_trees;;
open Proof_type;;
open Rawterm;;
open Reduction;;
open Refiner;;
open Sign;;
open String;;
open Tacmach;;
open Tacred;;
open Tacticals;;
open Tactics;;
open Term;;
open Typing;;
open Util;;
open Vernacentries;;
open Vernacinterp;;
open Evar_refiner;;


let parse_com   = Pcoq.parse_string Pcoq.Constr.constr;;
let parse_tac  t =
    try (Pcoq.parse_string Pcoq.Tactic.tactic t)
    with _ -> (msgnl (hov 0 (str"pas pars: " ++ str t));
	       failwith "tactic")
;;

let is_free () =
   let st =open_in_bin ((Sys.getenv "HOME")^"/.free") in
   let c=input_char st in
   close_in st;
   c = 'A'
;;

(* marche pas *)
(*
let is_free () =
   msgnl (hov 0 [< 'str"Isfree========= "; 'fNL >]);
   let s = Stream.of_channel stdin in
   msgnl (hov 0 [< 'str"Isfree s "; 'fNL >]);
   try (Stream.empty s;
        msgnl (hov 0 [< 'str"Isfree empty "; 'fNL >]);
        true)
   with _ -> (msgnl (hov 0 [< 'str"Isfree not empty "; 'fNL >]);
              false)
;;
*)
let free_try tac g =
    if is_free()
    then (tac g)
    else (failwith "not free")
;;
let adrel (x,t) e =
    match x with 
      Name(xid) -> Environ.push_rel (x,None,t) e
    | Anonymous -> Environ.push_rel (x,None,t) e
(* les constantes ayant une dfinition apparaissant dans x *)
let rec def_const_in_term_rec vl x = 
     match (kind_of_term x) with
     Prod(n,t,c)->
        let vl = (adrel (n,t) vl) in def_const_in_term_rec vl c
   | Lambda(n,t,c) ->
        let vl = (adrel (n,t) vl) in def_const_in_term_rec vl c
   | App(f,args) -> def_const_in_term_rec vl f
   | Sort(Prop(Null)) -> Prop(Null)
   | Sort(c) -> c
   | Ind(ind) ->
          let (mib, mip) = Global.lookup_inductive ind in
          mip.mind_sort
   | Construct(c) ->
          def_const_in_term_rec vl (mkInd (inductive_of_constructor c))
   | Case(_,x,t,a) 
        -> def_const_in_term_rec vl x
   | Cast(x,t)-> def_const_in_term_rec vl t
   | Const(c)  -> def_const_in_term_rec vl (lookup_constant c vl).const_type
   | _ -> def_const_in_term_rec vl (type_of vl Evd.empty x)
;;
let def_const_in_term_ x =
    def_const_in_term_rec  (Global.env()) (strip_outer_cast x)
;;
(*************************************************************************
 recopis de refiner.ml, car print_subscript pas exporte dans refiner.mli 
 modif de print_info_script avec pr_bar
*)

let pr_bar () = str "|"

let rec print_info_script sigma osign pf =
  let {evar_hyps=sign; evar_concl=cl} = pf.goal in
  match pf.ref with
    | None -> (mt ())
    | Some(r,spfl) ->
        pr_rule r ++
           match spfl with
             | [] ->
		   (str " " ++ fnl())
             | [pf1] ->
                 if pf1.ref = None then 
		   (str " " ++ fnl())
                 else 
		   (str";" ++ brk(1,3) ++
		      print_info_script sigma sign pf1)
             | _ -> ( str";[" ++ fnl() ++
                       prlist_with_sep pr_bar
                         (print_info_script sigma sign) spfl ++
                       str"]")

let format_print_info_script sigma osign pf = 
  hov 0 (print_info_script sigma osign pf)
    
let print_subscript sigma sign pf = 
 (* if is_tactic_proof pf then 
    format_print_info_script sigma sign (subproof_of_proof pf)
  else *)
    format_print_info_script sigma sign pf
(****************)

let pp_string x =
   msgnl_with Format.str_formatter x;
   Format.flush_str_formatter ()
;;

(***********************************************************************
   copi de tactics/eauto.ml
*)

(***************************************************************************)
(* A tactic similar to Auto, but using EApply, Assumption and e_give_exact *)
(***************************************************************************)

let unify_e_resolve  (c,clenv) gls = 
  let (wc,kONT) = startWalk gls in
  let clenv' = connect_clenv wc clenv in
  let _ = clenv_unique_resolver false clenv' gls in
  vernac_e_resolve_constr c gls

let rec e_trivial_fail_db db_list local_db goal =
  let tacl = 
    registered_e_assumption ::
    (tclTHEN Tactics.intro 
       (function g'->
	  let d = pf_last_hyp g' in
	  let hintl = make_resolve_hyp (pf_env g') (project g') d in
          (e_trivial_fail_db db_list
	     (Hint_db.add_list hintl local_db) g'))) ::
    (List.map fst (e_trivial_resolve db_list local_db (pf_concl goal)) )
  in 
  tclFIRST (List.map tclCOMPLETE tacl) goal 

and e_my_find_search db_list local_db hdc concl = 
  let hdc = head_of_constr_reference hdc in
  let hintl =
    if occur_existential concl then 
      list_map_append (Hint_db.map_all hdc) (local_db::db_list)
    else 
      list_map_append (Hint_db.map_auto (hdc,concl)) (local_db::db_list)
  in 
  let tac_of_hint = 
    fun ({pri=b; pat = p; code=t} as patac) -> 
      (b, 
       let tac =
	 match t with
	   | Res_pf (term,cl) -> unify_resolve (term,cl)
	   | ERes_pf (term,cl) -> unify_e_resolve (term,cl)
	   | Give_exact (c) -> e_give_exact_constr c
	   | Res_pf_THEN_trivial_fail (term,cl) ->
               tclTHEN (unify_e_resolve (term,cl)) 
		 (e_trivial_fail_db db_list local_db)
	   | Unfold_nth c -> unfold_constr c
	   | Extern tacast -> Auto.conclPattern concl 
	       (out_some p) tacast
       in 
       (free_try tac,fmt_autotactic t))
       (*i
	 fun gls -> pPNL (fmt_autotactic t); Format.print_flush (); 
                     try tac gls
		     with e when Logic.catchable_exception(e) -> 
                            (Format.print_string "Fail\n"; 
			     Format.print_flush (); 
			     raise e)
       i*)
  in 
  List.map tac_of_hint hintl
    
and e_trivial_resolve db_list local_db gl = 
  try 
    Auto.priority 
      (e_my_find_search db_list local_db 
	 (List.hd (head_constr_bound gl [])) gl)
  with Bound | Not_found -> []

let e_possible_resolve db_list local_db gl =
  try List.map snd (e_my_find_search db_list local_db 
		      (List.hd (head_constr_bound gl [])) gl)
  with Bound | Not_found -> []

let assumption_tac_list id = apply_tac_list (e_give_exact_constr (mkVar id))

let find_first_goal gls = 
  try first_goal gls with UserError _ -> assert false

(*s The following module [SearchProblem] is used to instantiate the generic
    exploration functor [Explore.Make]. *)
      
module MySearchProblem = struct

  type state = { 
    depth : int; (*r depth of search before failing *)
    tacres : goal list sigma * validation;
    last_tactic : std_ppcmds;
    dblist : Auto.Hint_db.t list;
    localdb :  Auto.Hint_db.t list }
		 
  let success s = (sig_it (fst s.tacres)) = []

  let rec filter_tactics (glls,v) = function
    | [] -> []
    | (tac,pptac) :: tacl -> 
	try 
	  let (lgls,ptl) = apply_tac_list tac glls in 
	  let v' p = v (ptl p) in
	  ((lgls,v'),pptac) :: filter_tactics (glls,v) tacl
	with e when Logic.catchable_exception e ->
	  filter_tactics (glls,v) tacl

  let rec list_addn n x l = 
    if n = 0 then l else x :: (list_addn (pred n) x l)

  (* Ordering of states is lexicographic on depth (greatest first) then
     number of remaining goals. *)
  let compare s s' =
    let d = s'.depth - s.depth in
    let nbgoals s = List.length (sig_it (fst s.tacres)) in
    if d <> 0 then d else nbgoals s - nbgoals s'

  let branching s = 
    if s.depth = 0 then 
      []
    else      
      let lg = fst s.tacres in
      let nbgl = List.length (sig_it lg) in
      assert (nbgl > 0);
      let g = find_first_goal lg in
      let assumption_tacs = 
	let l = 
	  filter_tactics s.tacres
	    (List.map 
	       (fun id -> (e_give_exact_constr (mkVar id),
			   (str "Exact" ++ spc()++ pr_id id)))
	       (pf_ids_of_hyps g))
	in
	List.map (fun (res,pp) -> { depth = s.depth; tacres = res;
				    last_tactic = pp; dblist = s.dblist;
				    localdb = List.tl s.localdb }) l
      in
      let intro_tac = 
	List.map 
	  (fun ((lgls,_) as res,pp) -> 
	     let g' = first_goal lgls in 
	     let hintl = 
	       make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g')
	     in
             let ldb = Hint_db.add_list hintl (List.hd s.localdb) in
	     { depth = s.depth; tacres = res; 
	       last_tactic = pp; dblist = s.dblist;
	       localdb = ldb :: List.tl s.localdb })
	  (filter_tactics s.tacres [Tactics.intro,(str "Intro" )])
      in
      let rec_tacs = 
	let l = 
	  filter_tactics s.tacres
	    (e_possible_resolve s.dblist (List.hd s.localdb) (pf_concl g))
	in
	List.map 
	  (fun ((lgls,_) as res, pp) -> 
	     let nbgl' = List.length (sig_it lgls) in
	     if nbgl' < nbgl then
	       { depth = s.depth; tacres = res; last_tactic = pp;
		 dblist = s.dblist; localdb = List.tl s.localdb }
	     else 
	       { depth = pred s.depth; tacres = res; 
		 dblist = s.dblist; last_tactic = pp;
		 localdb = 
		   list_addn (nbgl'-nbgl) (List.hd s.localdb) s.localdb })
	  l
      in
      List.sort compare (assumption_tacs @ intro_tac @ rec_tacs)

  let pp s = 
    msg (hov 0 (str " depth="++ int s.depth ++ spc() ++
		  s.last_tactic ++ str "\n"))

end

module MySearch = Explore.Make(MySearchProblem)

let make_initial_state n gl dblist localdb =
  { MySearchProblem.depth = n;
    MySearchProblem.tacres = tclIDTAC gl;
    MySearchProblem.last_tactic = (mt ());
    MySearchProblem.dblist = dblist;
    MySearchProblem.localdb = [localdb] }

let e_depth_search debug p db_list local_db gl =
  try
    let tac = if debug then MySearch.debug_depth_first else MySearch.depth_first in
    let s = tac (make_initial_state p gl db_list local_db) in
    s.MySearchProblem.tacres
  with Not_found -> error "EAuto: depth first search failed"

let e_breadth_search debug n db_list local_db gl =
  try
    let tac = 
      if debug then MySearch.debug_breadth_first else MySearch.breadth_first 
    in
    let s = tac (make_initial_state n gl db_list local_db) in
    s.MySearchProblem.tacres
  with Not_found -> error "EAuto: breadth first search failed"

let e_search_auto debug (n,p) db_list gl = 
  let local_db = make_local_hint_db gl in 
  if n = 0 then 
    e_depth_search debug p db_list local_db gl
  else 
    e_breadth_search debug n db_list local_db gl

let eauto debug np dbnames = 
  let db_list =
    List.map
      (fun x -> 
	 try Stringmap.find x !searchtable
	 with Not_found -> error ("EAuto: "^x^": No such Hint database"))
      ("core"::dbnames) 
  in
  tclTRY (e_search_auto debug np db_list)

let full_eauto debug n gl = 
  let dbnames = stringmap_dom !searchtable in
  let dbnames =  list_subtract dbnames ["v62"] in
  let db_list = List.map (fun x -> Stringmap.find x !searchtable) dbnames in
  let local_db = make_local_hint_db gl in
  tclTRY (e_search_auto debug n db_list) gl

let my_full_eauto n gl = full_eauto false (n,0) gl

(**********************************************************************
   copi de tactics/auto.ml on a juste modifi search_gen
*)
let searchtable_map name = 
  Stringmap.find name !searchtable

(* local_db is a Hint database containing the hypotheses of current goal *)
(* Papageno : cette fonction a t pas mal simplifie depuis que la base
  de Hint imprative a t remplace par plusieurs bases fonctionnelles *)

let rec trivial_fail_db db_list local_db gl =
  let intro_tac = 
    tclTHEN intro 
      (fun g'->
	 let hintl = make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g')
	 in trivial_fail_db db_list (Hint_db.add_list hintl local_db) g')
  in
  tclFIRST 
    (assumption::intro_tac::
     (List.map tclCOMPLETE 
	(trivial_resolve db_list local_db (pf_concl gl)))) gl

and my_find_search db_list local_db hdc concl =
  let tacl = 
    if occur_existential concl then 
      list_map_append (fun db -> Hint_db.map_all hdc db) (local_db::db_list)
    else 
      list_map_append (fun db -> Hint_db.map_auto (hdc,concl) db)
      	(local_db::db_list)
  in
  List.map 
    (fun ({pri=b; pat=p; code=t} as patac) -> 
       (b,
	match t with
	  | Res_pf (term,cl)  -> unify_resolve (term,cl)
	  | ERes_pf (_,c) -> (fun gl -> error "eres_pf")
	  | Give_exact c  -> exact_check c
	  | Res_pf_THEN_trivial_fail (term,cl) -> 
	      tclTHEN 
		(unify_resolve (term,cl)) 
		(trivial_fail_db db_list local_db)
	  | Unfold_nth c -> unfold_constr c
	  | Extern tacast -> 
	      conclPattern concl (out_some p) tacast))
    tacl

and trivial_resolve db_list local_db cl = 
  try 
    let hdconstr = List.hd (head_constr_bound cl []) in
    priority 
      (my_find_search db_list local_db (head_of_constr_reference hdconstr) cl)
  with Bound | Not_found -> 
    []

(**************************************************************************)
(*                       The classical Auto tactic                        *)
(**************************************************************************)

let possible_resolve db_list local_db cl =
  try 
    let hdconstr = List.hd (head_constr_bound cl []) in
    List.map snd 
      (my_find_search db_list local_db (head_of_constr_reference hdconstr) cl)
  with Bound | Not_found -> 
    []

let decomp_unary_term c gls = 
  let typc = pf_type_of gls c in 
  let hd = List.hd (head_constr typc) in 
  if Hipattern.is_conjunction hd then 
    simplest_case c gls 
  else 
    errorlabstrm "Auto.decomp_unary_term" (str "not a unary type")

let decomp_empty_term c gls = 
  let typc = pf_type_of gls c in 
  let (hd,_) = decompose_app typc in 
  if Hipattern.is_empty_type hd then 
    simplest_case c gls 
  else 
    errorlabstrm "Auto.decomp_empty_term" (str "not an empty type")


(* decomp is an natural number giving an indication on decomposition 
   of conjunction in hypotheses, 0 corresponds to no decomposition *)
(* n is the max depth of search *)
(* local_db contains the local Hypotheses *)

let rec search_gen decomp n db_list local_db extra_sign goal =
  if n=0 then error "BOUND 2";
  let decomp_tacs = match decomp with 
    | 0 -> [] 
    | p -> 
	(tclTRY_sign decomp_empty_term extra_sign)
	::
	(List.map 
	   (fun id -> tclTHEN (decomp_unary_term (mkVar id)) 
		(tclTHEN 
		   (clear [id])
		   (free_try (search_gen decomp p db_list local_db []))))
	   (pf_ids_of_hyps goal)) 
  in
  let intro_tac = 
    tclTHEN intro 
      (fun g' -> 
	 let (hid,_,htyp as d) = pf_last_hyp g' in
	 let hintl = 
	   try 
	     [make_apply_entry (pf_env g') (project g')
		(true,false) 
		hid (mkVar hid,body_of_type htyp)]
	   with Failure _ -> [] 
	 in
         (free_try
	  (search_gen decomp n db_list (Hint_db.add_list hintl local_db) [d])
	  g'))
  in
  let rec_tacs = 
    List.map 
      (fun ntac -> 
	 tclTHEN ntac
	   (free_try
	    (search_gen decomp (n-1) db_list local_db empty_named_context)))
      (possible_resolve db_list local_db (pf_concl goal))
  in 
  tclFIRST (assumption::(decomp_tacs@(intro_tac::rec_tacs))) goal


let search = search_gen 0

let default_search_depth = ref 5
			     
let full_auto n gl = 
  let dbnames = stringmap_dom !searchtable in
  let dbnames = list_subtract dbnames ["v62"] in
  let db_list = List.map (fun x -> searchtable_map x) dbnames in
  let hyps = pf_hyps gl in
  tclTRY (search n db_list (make_local_hint_db gl) hyps) gl
  
let default_full_auto gl = full_auto !default_search_depth gl
(************************************************************************)

let blast_tactic = ref (free_try default_full_auto)
;;

let blast_auto = (free_try default_full_auto)
(*                  (tclTHEN (free_try default_full_auto)
			  (free_try (my_full_eauto 2)))
*)
;;
let blast_simpl = (free_try (reduce (Simpl None) onConcl))
;;
let blast_induction1 = 
    (free_try (tclTHEN (tclTRY intro)
		       (tclTRY (tclLAST_HYP simplest_elim))))
;;
let blast_induction2 = 
    (free_try (tclTHEN (tclTRY (tclTHEN intro intro))
		       (tclTRY (tclLAST_HYP simplest_elim))))
;;
let blast_induction3 = 
    (free_try (tclTHEN (tclTRY (tclTHEN intro (tclTHEN intro intro)))
		       (tclTRY (tclLAST_HYP simplest_elim))))
;;

blast_tactic :=
  (tclORELSE (tclCOMPLETE blast_auto)
  (tclORELSE (tclCOMPLETE (tclTHEN blast_simpl blast_auto))
  (tclORELSE (tclCOMPLETE (tclTHEN blast_induction1
                          (tclTHEN blast_simpl blast_auto)))
  (tclORELSE (tclCOMPLETE (tclTHEN blast_induction2
                          (tclTHEN blast_simpl blast_auto)))
             (tclCOMPLETE (tclTHEN blast_induction3
                          (tclTHEN blast_simpl blast_auto)))))))
;;
(*
blast_tactic := (tclTHEN (free_try default_full_auto)
			 (free_try (my_full_eauto 4)))
;;
*)

let vire_extvar s =
   let interro = ref false in
   let interro_pos = ref 0 in
   for i=0 to (length s)-1 do
     if get s i = '?'
     then (interro := true;
           interro_pos := i)
     else if (!interro && 
              (List.mem (get s i)
			['0';'1';'2';'3';'4';'5';'6';'7';'8';'9']))
     then set s i ' '
     else interro:=false
   done;
   s
;;

let blast gls =
   let leaf g = {
      open_subgoals = 1;
      goal = g;
      ref = None } in
     try (let (sgl,v) as res = !blast_tactic gls in
	  let {it=lg} = sgl in
          if lg = [] 
          then (let pf = v (List.map leaf (sig_it sgl)) in
                let sign = (sig_it gls).evar_hyps in
                let x = print_subscript 
                     (sig_sig gls) sign pf in
		msgnl (hov 0 (str"Blast ==> " ++ x));
                let x = print_subscript 
                     (sig_sig gls) sign pf in
                let tac_string =
                pp_string  (hov 0 x ) in
    (* on remplace les ?1 ?2 ... de refine par ? *)
		parse_tac ((vire_extvar tac_string)
			   ^ ".")
	  )
	  else (msgnl (hov 0 (str"Blast failed to prove the goal..."));
		failwith "echec de blast"))
     with _ -> failwith "echec de blast"
;;

let blast_tac display_function = function 
          | (n::_) as l -> 
                 (function g ->
                    let exp_ast = (blast g) in
                     (display_function exp_ast;
                       tclIDTAC g))
          |  _ -> failwith "expecting other arguments";;

let blast_tac_txt = 
  blast_tac
    (function x -> msgnl(Pptactic.pr_glob_tactic (Tacinterp.glob_tactic x)));;

(* Obsolte ?
overwriting_add_tactic "Blast1" blast_tac_txt;;
*)

(*
Grammar tactic ne_numarg_list : list :=
  ne_numarg_single [numarg($n)] ->[$n]
| ne_numarg_cons [numarg($n) ne_numarg_list($ns)] -> [ $n ($LIST $ns) ].
Grammar tactic simple_tactic : ast :=
  blast1 [ "Blast1" ne_numarg_list($ns) ] ->
         [ (Blast1 ($LIST $ns)) ].



PATH=/usr/local/bin:/usr/bin:$PATH
COQTOP=d:/Tools/coq-7.0-3mai
CAMLLIB=/usr/local/lib/ocaml
CAMLP4LIB=/usr/local/lib/camlp4
export CAMLLIB
export COQTOP
export CAMLP4LIB 
d:/Tools/coq-7.0-3mai/bin/coqtop.byte.exe 
Drop.
#use "/cygdrive/D/Tools/coq-7.0-3mai/dev/base_include";;
*)