aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/funind/functional_principles_proofs.ml2
-rw-r--r--plugins/funind/recdef.ml2
-rw-r--r--pretyping/namegen.mli3
-rw-r--r--pretyping/termops.ml16
-rw-r--r--pretyping/termops.mli2
-rw-r--r--tactics/auto.ml54
-rw-r--r--tactics/auto.mli30
-rw-r--r--tactics/eauto.ml416
-rw-r--r--tactics/eauto.mli7
-rw-r--r--tactics/tacinterp.ml13
-rw-r--r--test-suite/success/auto.v8
11 files changed, 108 insertions, 45 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 43658e802..e047f13d5 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1450,7 +1450,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic =
Eauto.eauto_with_bases
false
(true,5)
- [Lazy.force refl_equal]
+ [Evd.empty,Lazy.force refl_equal]
[Auto.Hint_db.empty empty_transparent_state false]
)
)
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 057ffb9b3..f066e39d0 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1005,7 +1005,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
Eauto.eauto_with_bases
false
(true,5)
- [delayed_force refl_equal]
+ [Evd.empty,delayed_force refl_equal]
[Auto.Hint_db.empty empty_transparent_state false]
]
)
diff --git a/pretyping/namegen.mli b/pretyping/namegen.mli
index 8849c9ed3..0c9fc4f6b 100644
--- a/pretyping/namegen.mli
+++ b/pretyping/namegen.mli
@@ -39,6 +39,9 @@ val it_mkLambda_or_LetIn_name : env -> constr -> rel_context -> constr
(*********************************************************************
Fresh names *)
+(** Avoid clashing with a name satisfying some predicate *)
+val next_ident_away_from : identifier -> (identifier -> bool) -> identifier
+
(** Avoid clashing with a name of the given list *)
val next_ident_away : identifier -> identifier list -> identifier
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index d31242aa2..9888821d1 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -262,6 +262,14 @@ let rec strip_head_cast c = match kind_of_term c with
| Cast (c,_,_) -> strip_head_cast c
| _ -> c
+let rec drop_extra_implicit_args c = match kind_of_term c with
+ (* Removed trailing extra implicit arguments, what improves compatibility
+ for constants with recently added maximal implicit arguments *)
+ | App (f,args) when isEvar (array_last args) ->
+ drop_extra_implicit_args
+ (mkApp (f,fst (array_chop (Array.length args - 1) args)))
+ | _ -> c
+
(* Get the last arg of an application *)
let last_arg c = match kind_of_term c with
| App (f,cl) -> array_last cl
@@ -526,6 +534,14 @@ let collect_metas c =
in
List.rev (collrec [] c)
+(* collects all vars; warning: this is only visible vars, not dependencies in
+ all section variables; for the latter, use global_vars_set *)
+let collect_vars c =
+ let rec aux vars c = match kind_of_term c with
+ | Var id -> Idset.add id vars
+ | _ -> fold_constr aux vars c in
+ aux Idset.empty c
+
(* Tests whether [m] is a subterm of [t]:
[m] is appropriately lifted through abstractions of [t] *)
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 385bd3022..1350743d5 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -91,6 +91,7 @@ val iter_constr_with_full_binders :
(**********************************************************************)
val strip_head_cast : constr -> constr
+val drop_extra_implicit_args : constr -> constr
(** occur checks *)
exception Occur
@@ -107,6 +108,7 @@ val free_rels : constr -> Intset.t
val dependent : constr -> constr -> bool
val dependent_no_evar : constr -> constr -> bool
val collect_metas : constr -> int list
+val collect_vars : constr -> Idset.t (** for visible vars only *)
val occur_term : constr -> constr -> bool (** Synonymous
of dependent
Substitution of metavariables *)
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 8e77bb53f..440f92b7f 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -569,17 +569,43 @@ type hints_entry =
| HintsDestructEntry of identifier * int * (bool,unit) location *
(patvar list * constr_pattern) * glob_tactic_expr
-let rec drop_extra_args c = match kind_of_term c with
- (* Removed trailing extra implicit arguments, what improves compatibility
- for constants with recently added maximal implicit arguments *)
- | App (f,args) when isEvar (array_last args) ->
- drop_extra_args (mkApp (f,fst (array_chop (Array.length args - 1) args)))
- | _ -> c
+let h = id_of_string "H"
+
+exception Found of constr * types
+
+let prepare_hint env (sigma,c) =
+ let sigma = Typeclasses.resolve_typeclasses ~fail:false env sigma in
+ (* We re-abstract over uninstantiated evars.
+ It is actually a bit stupid to generalize over evars since the first
+ thing make_resolves will do is to re-instantiate the products *)
+ let c = drop_extra_implicit_args (Evarutil.nf_evar sigma c) in
+ let vars = ref (collect_vars c) in
+ let subst = ref [] in
+ let rec find_next_evar c = match kind_of_term c with
+ | Evar (evk,args as ev) ->
+ (* We skip the test whether args is the identity or not *)
+ let t = Evarutil.nf_evar sigma (existential_type sigma ev) in
+ let t = List.fold_right (fun (e,id) c -> replace_term e id c) !subst t in
+ if free_rels t <> Intset.empty then
+ error "Hints with holes dependent on a bound variable not supported.";
+ if occur_existential t then
+ (* Not clever enough to construct dependency graph of evars *)
+ error "Not clever enough to deal with evars dependent in other evars.";
+ raise (Found (c,t))
+ | _ -> iter_constr find_next_evar c in
+ let rec iter c =
+ try find_next_evar c; c
+ with Found (evar,t) ->
+ let id = next_ident_away_from h (fun id -> Idset.mem id !vars) in
+ vars := Idset.add id !vars;
+ subst := (evar,mkVar id)::!subst;
+ mkNamedLambda id t (iter (replace_term evar (mkVar id) c)) in
+ iter c
let interp_hints h =
let f c =
let evd,c = Constrintern.interp_open_constr Evd.empty (Global.env()) c in
- let c = drop_extra_args c in
+ let c = prepare_hint (Global.env()) (evd,c) in
Evarutil.check_evars (Global.env()) Evd.empty evd c;
c in
let fr r =
@@ -785,19 +811,19 @@ let unify_resolve_gen = function
(* Util *)
-let expand_constructor_hints lems =
- list_map_append (fun lem ->
+let expand_constructor_hints env lems =
+ list_map_append (fun (sigma,lem) ->
match kind_of_term lem with
| Ind ind ->
list_tabulate (fun i -> mkConstruct (ind,i+1)) (nconstructors ind)
| _ ->
- [lem]) lems
+ [prepare_hint env (sigma,lem)]) lems
(* builds a hint database from a constr signature *)
(* typically used with (lid, ltyp) = pf_hyps_types <some goal> *)
let add_hint_lemmas eapply lems hint_db gl =
- let lems = expand_constructor_hints lems in
+ let lems = expand_constructor_hints (pf_env gl) lems in
let hintlist' =
list_map_append (pf_apply make_resolves gl (eapply,true,false) None) lems in
Hint_db.add_list hintlist' hint_db
@@ -958,7 +984,7 @@ let gen_trivial lems = function
| Some l -> trivial lems l
let h_trivial lems l =
- Refiner.abstract_tactic (TacTrivial (lems,l))
+ Refiner.abstract_tactic (TacTrivial (List.map snd lems,l))
(gen_trivial lems l)
(**************************************************************************)
@@ -1088,7 +1114,7 @@ let gen_auto n lems dbnames =
let inj_or_var = Option.map (fun n -> ArgArg n)
let h_auto n lems l =
- Refiner.abstract_tactic (TacAuto (inj_or_var n,lems,l))
+ Refiner.abstract_tactic (TacAuto (inj_or_var n,List.map snd lems,l))
(gen_auto n lems l)
(**************************************************************************)
@@ -1117,7 +1143,7 @@ let dauto (n,p) lems =
let default_dauto = dauto (None,None) []
let h_dauto (n,p) lems =
- Refiner.abstract_tactic (TacDAuto (inj_or_var n,p,lems))
+ Refiner.abstract_tactic (TacDAuto (inj_or_var n,p,List.map snd lems))
(dauto (n,p) lems)
(***************************************)
diff --git a/tactics/auto.mli b/tactics/auto.mli
index f4f7b9dfa..fa6f1d9ca 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -96,6 +96,8 @@ val interp_hints : hints_expr -> hints_entry
val add_hints : locality_flag -> hint_db_name list -> hints_entry -> unit
+val prepare_hint : env -> open_constr -> constr
+
val print_searchtable : unit -> unit
val print_applicable_hint : unit -> unit
@@ -112,7 +114,7 @@ val print_hint_db : Hint_db.t -> unit
val make_exact_entry : evar_map -> int option -> constr * constr -> hint_entry
-(** [make_apply_entry (eapply,verbose) pri (c,cty)].
+(** [make_apply_entry (eapply,hnf,verbose) pri (c,cty)].
[eapply] is true if this hint will be used only with EApply;
[hnf] should be true if we should expand the head of cty before searching for
products;
@@ -163,7 +165,7 @@ val set_extern_subst_tactic :
Useful to take the current goal hypotheses as hints;
Boolean tells if lemmas with evars are allowed *)
-val make_local_hint_db : bool -> constr list -> goal sigma -> hint_db
+val make_local_hint_db : bool -> open_constr list -> goal sigma -> hint_db
val priority : ('a * pri_auto_tactic) list -> ('a * pri_auto_tactic) list
@@ -185,48 +187,48 @@ val conclPattern : constr -> constr_pattern option -> Tacexpr.glob_tactic_expr -
(** The Auto tactic *)
-val auto : int -> constr list -> hint_db_name list -> tactic
+val auto : int -> open_constr list -> hint_db_name list -> tactic
(** Auto with more delta. *)
-val new_auto : int -> constr list -> hint_db_name list -> tactic
+val new_auto : int -> open_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 -> constr list -> tactic
+val full_auto : int -> open_constr list -> tactic
(** auto with all hint databases except the "v62" compatibility database
and doing delta *)
-val new_full_auto : int -> constr list -> tactic
+val new_full_auto : int -> open_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 -> constr list -> hint_db_name list option -> tactic
+val gen_auto : int option -> open_constr list -> hint_db_name list option -> tactic
(** The hidden version of auto *)
-val h_auto : int option -> constr list -> hint_db_name list option -> tactic
+val h_auto : int option -> open_constr list -> hint_db_name list option -> tactic
(** Trivial *)
-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 trivial : open_constr list -> hint_db_name list -> tactic
+val gen_trivial : open_constr list -> hint_db_name list option -> tactic
+val full_trivial : open_constr list -> tactic
+val h_trivial : open_constr list -> hint_db_name list option -> tactic
val pr_autotactic : auto_tactic -> Pp.std_ppcmds
(** {6 The following is not yet up to date -- Papageno. } *)
(** DAuto *)
-val dauto : int option * int option -> constr list -> tactic
+val dauto : int option * int option -> open_constr list -> tactic
val default_search_decomp : int ref
val default_dauto : tactic
-val h_dauto : int option * int option -> constr list -> tactic
+val h_dauto : int option * int option -> open_constr list -> tactic
(** SuperAuto *)
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index fab8d2d45..6f4d90ab4 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -68,6 +68,7 @@ let rec prolog l n gl =
(tclFIRST (List.map (fun t -> (tclTHEN t prol)) (one_step l gl))) gl
let prolog_tac l n gl =
+ let l = List.map (prepare_hint (pf_env gl)) l in
let n =
match n with
| ArgArg n -> n
@@ -78,7 +79,7 @@ let prolog_tac l n gl =
errorlabstrm "Prolog.prolog" (str "Prolog failed.")
TACTIC EXTEND prolog
-| [ "prolog" "[" constr_list(l) "]" int_or_var(n) ] -> [ prolog_tac l n ]
+| [ "prolog" "[" open_constr_list(l) "]" int_or_var(n) ] -> [ prolog_tac l n ]
END
open Auto
@@ -345,19 +346,20 @@ ARGUMENT EXTEND hintbases
| [ ] -> [ Some [] ]
END
-let pr_constr_coma_sequence prc _ _ = prlist_with_sep pr_comma prc
+let pr_constr_coma_sequence prc _ _ =
+ prlist_with_sep pr_comma (fun (_,c) -> prc c)
ARGUMENT EXTEND constr_coma_sequence
- TYPED AS constr_list
+ TYPED AS open_constr_list
PRINTED BY pr_constr_coma_sequence
-| [ constr(c) "," constr_coma_sequence(l) ] -> [ c::l ]
-| [ constr(c) ] -> [ [c] ]
+| [ open_constr(c) "," constr_coma_sequence(l) ] -> [ c::l ]
+| [ open_constr(c) ] -> [ [c] ]
END
-let pr_auto_using prc _prlc _prt = Pptactic.pr_auto_using prc
+let pr_auto_using prc _prlc _prt = Pptactic.pr_auto_using (fun (_,c) -> prc c)
ARGUMENT EXTEND auto_using
- TYPED AS constr_list
+ TYPED AS open_constr_list
PRINTED BY pr_auto_using
| [ "using" constr_coma_sequence(l) ] -> [ l ]
| [ ] -> [ [] ]
diff --git a/tactics/eauto.mli b/tactics/eauto.mli
index 093cd56e1..68ec42f4e 100644
--- a/tactics/eauto.mli
+++ b/tactics/eauto.mli
@@ -19,7 +19,7 @@ val hintbases : hint_db_name list option Pcoq.Gram.entry
val wit_hintbases : hint_db_name list option typed_abstract_argument_type
val rawwit_hintbases : hint_db_name list option raw_abstract_argument_type
-val rawwit_auto_using : constr_expr list raw_abstract_argument_type
+val rawwit_auto_using : Genarg.open_constr_expr list raw_abstract_argument_type
val e_assumption : tactic
@@ -27,13 +27,12 @@ val registered_e_assumption : tactic
val e_give_exact : ?flags:Unification.unify_flags -> constr -> tactic
-val gen_eauto : bool -> bool * int -> constr list ->
+val gen_eauto : bool -> bool * int -> open_constr list ->
hint_db_name list option -> tactic
-
val eauto_with_bases :
bool ->
bool * int ->
- Term.constr list -> Auto.hint_db list -> Proof_type.tactic
+ open_constr list -> Auto.hint_db list -> Proof_type.tactic
val autounfold : hint_db_name list -> Tacticals.clause -> tactic
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index a2caec7c5..d4ac859ad 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1351,6 +1351,10 @@ let interp_open_constr_list =
interp_constr_in_compound_list (fun x -> x) (fun x -> x)
(interp_open_constr None)
+let interp_auto_lemmas ist env sigma lems =
+ let local_sigma, lems = interp_open_constr_list ist env sigma lems in
+ List.map (fun lem -> (local_sigma,lem)) lems
+
(* Interprets a type expression *)
let pf_interp_type ist gl =
interp_type ist (pf_env gl) (project gl)
@@ -2289,19 +2293,20 @@ and interp_atomic ist gl tac =
(* Automation tactics *)
| TacTrivial (lems,l) ->
- Auto.h_trivial (interp_constr_list ist env sigma lems)
+ Auto.h_trivial
+ (interp_auto_lemmas ist env sigma lems)
(Option.map (List.map (interp_hint_base ist)) l)
| TacAuto (n,lems,l) ->
Auto.h_auto (Option.map (interp_int_or_var ist) n)
- (interp_constr_list ist env sigma lems)
- (Option.map (List.map (interp_hint_base ist)) l)
+ (interp_auto_lemmas ist env sigma lems)
+ (Option.map (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)
| TacDestructConcl -> Dhyp.h_destructConcl
| TacSuperAuto (n,l,b1,b2) -> Auto.h_superauto n l b1 b2
| TacDAuto (n,p,lems) ->
Auto.h_dauto (Option.map (interp_int_or_var ist) n,p)
- (interp_constr_list ist env sigma lems)
+ (interp_auto_lemmas ist env sigma lems)
(* Derived basic tactics *)
| TacSimpleInductionDestruct (isrec,h) ->
diff --git a/test-suite/success/auto.v b/test-suite/success/auto.v
index a2701f8bb..9b691e253 100644
--- a/test-suite/success/auto.v
+++ b/test-suite/success/auto.v
@@ -16,3 +16,11 @@ Goal G unit Q -> F (Q tt).
intro.
auto.
Qed.
+
+(* Test implicit arguments in "using" clause *)
+
+Goal forall n:nat, nat * nat.
+auto using (pair O).
+Undo.
+eauto using (pair O).
+Qed.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 18:32:54 +0000