Ajout option 'using lemmas' Ã auto/trivial/eauto

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7937 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 86 insertions, 61 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 3aaf3443ea..edda5c25b9 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -567,11 +567,11 @@ let unify_resolve (c,clenv) gls =
 (* builds a hint database from a constr signature *)
 (* typically used with (lid, ltyp) = pf_hyps_types <some goal> *)
 
-let make_local_hint_db g = 
+let make_local_hint_db lems g =
   let sign = pf_hyps g in
-  let hintlist = list_map_append (make_resolve_hyp (pf_env g) (project g)) sign
-  in Hint_db.add_list hintlist Hint_db.empty
-
+  let hintlist = list_map_append (pf_apply make_resolve_hyp g) sign in
+  let hintlist' = list_map_append (pf_apply make_resolves g true) lems in
+  Hint_db.add_list hintlist' (Hint_db.add_list hintlist Hint_db.empty)
 
 (* Serait-ce possible de compiler d'abord la tactique puis de faire la
    substitution sans passer par bdize dont l'objectif est de préparer un
@@ -648,7 +648,7 @@ and trivial_resolve db_list local_db cl =
   with Bound | Not_found -> 
     []
 
-let trivial dbnames gl =
+let trivial lems dbnames gl =
   let db_list = 
     List.map
       (fun x -> 
@@ -658,19 +658,20 @@ let trivial dbnames gl =
 	   error ("trivial: "^x^": No such Hint database"))
       ("core"::dbnames) 
   in
-  tclTRY (trivial_fail_db db_list (make_local_hint_db gl)) gl 
+  tclTRY (trivial_fail_db db_list (make_local_hint_db lems gl)) gl 
     
-let full_trivial gl =
+let full_trivial lems gl =
   let dbnames = Hintdbmap.dom !searchtable in
   let dbnames = list_subtract dbnames ["v62"] in
   let db_list = List.map (fun x -> searchtable_map x) dbnames in
-  tclTRY (trivial_fail_db db_list (make_local_hint_db gl)) gl
+  tclTRY (trivial_fail_db db_list (make_local_hint_db lems gl)) gl
 
-let gen_trivial = function
-  | None -> full_trivial
-  | Some l -> trivial l
+let gen_trivial lems = function
+  | None -> full_trivial lems
+  | Some l -> trivial lems l
 
-let h_trivial l = Refiner.abstract_tactic (TacTrivial l) (gen_trivial l)
+let h_trivial lems l =
+  Refiner.abstract_tactic (TacTrivial (lems,l)) (gen_trivial lems l)
 
 (**************************************************************************)
 (*                       The classical Auto tactic                        *)
@@ -746,8 +747,8 @@ let rec search_gen decomp n db_list local_db extra_sign goal =
 let search = search_gen 0
 
 let default_search_depth = ref 5
-			     
-let auto n dbnames gl = 
+
+let auto n lems dbnames gl =
   let db_list = 
     List.map
       (fun x -> 
@@ -758,29 +759,29 @@ let auto n dbnames gl =
       ("core"::dbnames) 
   in
   let hyps = pf_hyps gl in
-  tclTRY (search n db_list (make_local_hint_db gl) hyps) gl
+  tclTRY (search n db_list (make_local_hint_db lems gl) hyps) gl
 
-let default_auto = auto !default_search_depth []
+let default_auto = auto !default_search_depth [] []
 
-let full_auto n gl = 
+let full_auto n lems gl = 
   let dbnames = Hintdbmap.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
+  tclTRY (search n db_list (make_local_hint_db lems gl) hyps) gl
   
-let default_full_auto gl = full_auto !default_search_depth gl
+let default_full_auto gl = full_auto !default_search_depth [] gl
 
-let gen_auto n dbnames =
+let gen_auto n lems dbnames =
   let n = match n with None -> !default_search_depth | Some n -> n in
   match dbnames with
-  | None -> full_auto n
-  | Some l -> auto n l
+  | None -> full_auto n lems
+  | Some l -> auto n lems l
 
 let inj_or_var = option_app (fun n -> Genarg.ArgArg n)
 
-let h_auto n l =
-  Refiner.abstract_tactic (TacAuto (inj_or_var n,l)) (gen_auto n l)
+let h_auto n lems l =
+  Refiner.abstract_tactic (TacAuto (inj_or_var n,lems,l)) (gen_auto n lems l)
 
 (**************************************************************************)
 (*                  The "destructing Auto" from Eduardo                   *)
@@ -795,7 +796,7 @@ let default_search_decomp = ref 1
 let destruct_auto des_opt n gl = 
   let hyps = pf_hyps gl in
   search_gen des_opt n [searchtable_map "core"] 
-    (make_local_hint_db gl) hyps gl
+    (make_local_hint_db [] gl) hyps gl
     
 let dautomatic des_opt n = tclTRY (destruct_auto des_opt n)
 
@@ -880,7 +881,7 @@ let search_superauto n to_add argl g =
       (fun (id,c) -> add_named_decl (id, None, pf_type_of g c))
       to_add empty_named_context in
   let db0 = list_map_append (make_resolve_hyp (pf_env g) (project g)) sigma in
-  let db = Hint_db.add_list db0 (make_local_hint_db g) in
+  let db = Hint_db.add_list db0 (make_local_hint_db [] g) in
   super_search n [Hintdbmap.find "core" !searchtable] db argl g
 
 let superauto n to_add argl  = 
diff --git a/tactics/auto.mli b/tactics/auto.mli
index ee638499f1..0e702a65b1 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -127,7 +127,7 @@ val set_extern_subst_tactic :
 (* Create a Hint database from the pairs (name, constr).
    Useful to take the current goal hypotheses as hints *)
 
-val make_local_hint_db : goal sigma -> Hint_db.t
+val make_local_hint_db : constr list -> goal sigma -> Hint_db.t
 
 val priority : (int * 'a) list -> 'a list
 
@@ -145,29 +145,29 @@ val conclPattern : constr -> constr_pattern -> Tacexpr.glob_tactic_expr -> tacti
 
 (* The Auto tactic *)
 
-val auto : int -> hint_db_name list -> tactic
+val auto : int -> constr list -> hint_db_name list -> tactic
 
 (* auto with default search depth and with the hint database "core" *)
 val default_auto : tactic
 
 (* auto with all hint databases except the "v62" compatibility database *)
-val full_auto : int -> tactic
+val full_auto : int -> constr list -> tactic
 
 (* auto with default search depth and with all hint databases 
    except the "v62" compatibility database *)
 val default_full_auto : tactic
 
 (* The generic form of auto (second arg [None] means all bases) *)
-val gen_auto : int option -> hint_db_name list option -> tactic
+val gen_auto : int option -> constr list -> hint_db_name list option -> tactic
 
 (* The hidden version of auto *)
-val h_auto   : int option -> hint_db_name list option -> tactic
+val h_auto   : int option -> constr list -> hint_db_name list option -> tactic
 
 (* Trivial *)
-val trivial : hint_db_name list -> tactic
-val gen_trivial : hint_db_name list option -> tactic
-val full_trivial : tactic
-val h_trivial : hint_db_name list option -> tactic
+val trivial : constr list -> hint_db_name list -> tactic
+val gen_trivial : constr list -> hint_db_name list option -> tactic
+val full_trivial : constr list -> tactic
+val h_trivial : constr list -> hint_db_name list option -> tactic
 
 val fmt_autotactic : auto_tactic -> Pp.std_ppcmds
 
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index d92c4f2ed2..fd1f38786a 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -354,14 +354,14 @@ let e_breadth_search debug n db_list local_db gl =
     s.SearchProblem.tacres
   with Not_found -> error "EAuto: breadth first search failed"
 
-let e_search_auto debug (in_depth,p) db_list gl = 
-  let local_db = make_local_hint_db gl in 
+let e_search_auto debug (in_depth,p) lems db_list gl = 
+  let local_db = make_local_hint_db lems gl in 
   if in_depth then 
     e_depth_search debug p db_list local_db gl
   else 
     e_breadth_search debug p db_list local_db gl
 
-let eauto debug np dbnames = 
+let eauto debug np lems dbnames =
   let db_list =
     List.map
       (fun x -> 
@@ -369,18 +369,17 @@ let eauto debug np dbnames =
 	 with Not_found -> error ("EAuto: "^x^": No such Hint database"))
       ("core"::dbnames) 
   in
-  tclTRY (e_search_auto debug np db_list)
+  tclTRY (e_search_auto debug np lems db_list)
 
-let full_eauto debug n gl = 
+let full_eauto debug n lems gl = 
   let dbnames = current_db_names () in
   let dbnames =  list_subtract dbnames ["v62"] in
   let db_list = List.map searchtable_map dbnames in
-  let local_db = make_local_hint_db gl in
-  tclTRY (e_search_auto debug n db_list) gl
+  tclTRY (e_search_auto debug n lems db_list) gl
 
-let gen_eauto d np = function
-  | None -> full_eauto d np
-  | Some l -> eauto d np l
+let gen_eauto d np lems = function
+  | None -> full_eauto d np lems
+  | Some l -> eauto d np lems l
 
 let make_depth = function
   | None -> !default_search_depth 
@@ -396,10 +395,7 @@ open Genarg
 
 (* Hint bases *)
 
-let pr_hintbases _prc _prlc _prt = function 
-  | None -> str " with *"
-  | Some [] -> mt ()
-  | Some l -> str " with " ++ Util.prlist_with_sep spc str l
+let pr_hintbases _prc _prlc _prt = Pptactic.pr_hintbases
 
 ARGUMENT EXTEND hintbases
   TYPED AS preident_list_opt
@@ -409,7 +405,26 @@ ARGUMENT EXTEND hintbases
 | [ ] -> [ Some [] ]
 END
 
+let pr_constr_coma_sequence prc _ _ = prlist_with_sep pr_coma prc
+
+ARGUMENT EXTEND constr_coma_sequence
+  TYPED AS constr_list
+  PRINTED BY pr_constr_coma_sequence
+| [ constr(c) "," constr_coma_sequence(l) ] -> [ c::l ]
+| [ constr(c) ] -> [ [c] ]
+END
+
+let pr_auto_using prc _prlc _prt = Pptactic.pr_auto_using prc
+
+ARGUMENT EXTEND auto_using
+  TYPED AS constr_list
+  PRINTED BY pr_auto_using
+| [ "using" constr_coma_sequence(l) ] -> [ l ]
+| [ ] -> [ [] ]
+END
+
 TACTIC EXTEND eauto
-| [ "eauto" int_or_var_opt(n) int_or_var_opt(p) hintbases(db) ] ->
-    [ gen_eauto false (make_dimension n p) db ]
+| [ "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems) 
+    hintbases(db) ] ->
+    [ gen_eauto false (make_dimension n p) lems db ]
 END
diff --git a/tactics/eauto.mli b/tactics/eauto.mli
index 57f6a4171f..4621088e25 100644
--- a/tactics/eauto.mli
+++ b/tactics/eauto.mli
@@ -11,10 +11,13 @@ open Term
 open Proof_type
 open Tacexpr
 open Auto
+open Topconstr
 (*i*)
 
 val rawwit_hintbases : hint_db_name list option raw_abstract_argument_type
 
+val rawwit_auto_using : constr_expr list raw_abstract_argument_type
+
 val e_assumption : tactic
 
 val registered_e_assumption : tactic
@@ -25,5 +28,6 @@ val vernac_e_resolve_constr :  constr -> tactic
 
 val e_give_exact_constr : constr -> tactic
 
-val gen_eauto : bool -> bool * int -> hint_db_name list option -> tactic
+val gen_eauto : bool -> bool * int -> constr list -> 
+  hint_db_name list option -> tactic
 
diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4
index 1ef4b928d4..4bd83c6729 100644
--- a/tactics/eqdecide.ml4
+++ b/tactics/eqdecide.ml4
@@ -114,7 +114,7 @@ let diseqCase =
   (tclTHEN  (intro_using absurd)
   (tclTHEN  (h_simplest_apply (mkVar diseq))
   (tclTHEN  (Extratactics.h_injHyp (Rawterm.NamedHyp absurd))
-            full_trivial))))))
+            (full_trivial [])))))))
 
 let solveArg a1 a2 tac  g = 
   let rectype = pf_type_of g a1 in
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 476332bdaa..7eff2b69fe 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -234,8 +234,8 @@ let _ =
         "intros", TacIntroPattern [];
         "assumption", TacAssumption;
         "cofix", TacCofix None;
-        "trivial", TacTrivial None;
-        "auto", TacAuto(None,None);
+        "trivial", TacTrivial ([],None);
+        "auto", TacAuto(None,[],None);
         "left", TacLeft NoBindings;
         "right", TacRight NoBindings;
         "split", TacSplit(false,NoBindings);
@@ -655,8 +655,10 @@ let rec intern_atomic lf ist x =
 *)
 
   (* Automation tactics *)
-  | TacTrivial l -> TacTrivial l
-  | TacAuto (n,l) -> TacAuto (option_app (intern_int_or_var ist) n,l)
+  | TacTrivial (lems,l) -> TacTrivial (List.map (intern_constr ist) lems,l)
+  | TacAuto (n,lems,l) ->
+      TacAuto (option_app (intern_int_or_var ist) n,
+        List.map (intern_constr ist) lems,l)
   | TacAutoTDB n -> TacAutoTDB n
   | TacDestructHyp (b,id) -> TacDestructHyp(b,intern_hyp ist id)
   | TacDestructConcl -> TacDestructConcl
@@ -1750,9 +1752,12 @@ and interp_atomic ist gl = function
 	     HypLocation(interp_hyp ist gl id,hloc))
 *)
   (* Automation tactics *)
-  | TacTrivial l -> Auto.h_trivial (option_app (List.map (interp_hint_base ist)) l)
-  | TacAuto (n, l) ->
+  | TacTrivial (lems,l) -> 
+      Auto.h_trivial (List.map (pf_interp_constr ist gl) lems)
+	(option_app (List.map (interp_hint_base ist)) l)
+  | TacAuto (n,lems,l) ->
       Auto.h_auto (option_app (interp_int_or_var ist) n)
+      (List.map (pf_interp_constr ist gl) lems)
       (option_app (List.map (interp_hint_base ist)) l)
   | TacAutoTDB n -> Dhyp.h_auto_tdb n
   | TacDestructHyp (b,id) -> Dhyp.h_destructHyp b (interp_hyp ist gl id)
@@ -2012,8 +2017,8 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
 (*| TacInstantiate (n,c,ido) -> TacInstantiate (n,subst_rawconstr subst c,ido)
 *)
   (* Automation tactics *)
-  | TacTrivial l -> TacTrivial l
-  | TacAuto (n,l) -> TacAuto (n,l)
+  | TacTrivial (lems,l) -> TacTrivial (List.map (subst_rawconstr subst) lems,l)
+  | TacAuto (n,lems,l) -> TacAuto (n,List.map (subst_rawconstr subst) lems,l)
   | TacAutoTDB n -> TacAutoTDB n
   | TacDestructHyp (b,id) -> TacDestructHyp(b,id)
   | TacDestructConcl -> TacDestructConcl