aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--intf/tacexpr.mli5
-rw-r--r--pretyping/constr_matching.ml46
-rw-r--r--pretyping/constr_matching.mli9
-rw-r--r--pretyping/glob_ops.ml60
-rw-r--r--pretyping/glob_ops.mli1
-rw-r--r--tactics/tacinterp.ml7
-rw-r--r--tactics/tactic_matching.mli4
-rw-r--r--test-suite/output/ltac.v9
8 files changed, 108 insertions, 33 deletions
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 2b37c580e..eb4e5ae7d 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -114,6 +114,7 @@ type glob_constr_and_expr = Glob_term.glob_constr * constr_expr option
type open_constr_expr = unit * constr_expr
type open_glob_constr = unit * glob_constr_and_expr
+type binding_bound_vars = Id.Set.t
type glob_constr_pattern_and_expr = glob_constr_and_expr * constr_pattern
type delayed_open_constr_with_bindings =
@@ -325,7 +326,7 @@ constraint 'a = <
type g_trm = glob_constr_and_expr
type g_utrm = g_trm
-type g_pat = glob_constr_and_expr * constr_pattern
+type g_pat = glob_constr_pattern_and_expr
type g_cst = evaluable_global_reference and_short_name or_var
type g_ref = ltac_constant located or_var
type g_nam = Id.t located
@@ -386,7 +387,7 @@ type raw_tactic_arg =
type t_trm = Term.constr
type t_utrm = Glob_term.closed_glob_constr
-type t_pat = glob_constr_and_expr * constr_pattern
+type t_pat = glob_constr_pattern_and_expr
type t_cst = evaluable_global_reference and_short_name
type t_ref = ltac_constant located
type t_nam = Id.t
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 585be9c72..19c85c9e2 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -56,10 +56,6 @@ let warn_bound_meta name =
let warn_bound_bound name =
msg_warning (str "Collision between bound variables of name " ++ pr_id name)
-let warn_bound_again name =
- msg_warning (str "Collision between bound variable " ++ pr_id name ++
- str " and another bound variable of same name.")
-
let constrain n (ids, m as x) (names, terms as subst) =
try
let (ids', m') = Id.Map.find n terms in
@@ -69,16 +65,17 @@ let constrain n (ids, m as x) (names, terms as subst) =
let () = if Id.Map.mem n names then warn_bound_meta n in
(names, Id.Map.add n x terms)
-let add_binders na1 na2 (names, terms as subst) = match na1, na2 with
-| Name id1, Name id2 ->
- if Id.Map.mem id1 names then
- let () = warn_bound_bound id1 in
- (names, terms)
- else
- let names = Id.Map.add id1 id2 names in
- let () = if Id.Map.mem id1 terms then warn_bound_again id1 in
- (names, terms)
-| _ -> subst
+let add_binders na1 na2 binding_vars (names, terms as subst) =
+ match na1, na2 with
+ | Name id1, Name id2 when Id.Set.mem id1 binding_vars ->
+ if Id.Map.mem id1 names then
+ let () = warn_bound_bound id1 in
+ (names, terms)
+ else
+ let names = Id.Map.add id1 id2 names in
+ let () = if Id.Map.mem id1 terms then warn_bound_meta id1 in
+ (names, terms)
+ | _ -> subst
let rec build_lambda vars ctx m = match vars with
| [] ->
@@ -155,7 +152,8 @@ let merge_binding allow_bound_rels ctx n cT subst =
in
constrain n c subst
-let matches_core env sigma convert allow_partial_app allow_bound_rels pat c =
+let matches_core env sigma convert allow_partial_app allow_bound_rels
+ (binding_vars,pat) c =
let convref ref c =
match ref, kind_of_term c with
| VarRef id, Var id' -> Names.id_eq id id'
@@ -258,15 +256,15 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels pat c =
| PProd (na1,c1,d1), Prod(na2,c2,d2) ->
sorec ((na1,na2,c2)::ctx) (Environ.push_rel (na2,None,c2) env)
- (add_binders na1 na2 (sorec ctx env subst c1 c2)) d1 d2
+ (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2
| PLambda (na1,c1,d1), Lambda(na2,c2,d2) ->
sorec ((na1,na2,c2)::ctx) (Environ.push_rel (na2,None,c2) env)
- (add_binders na1 na2 (sorec ctx env subst c1 c2)) d1 d2
+ (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2
| PLetIn (na1,c1,d1), LetIn(na2,c2,t2,d2) ->
sorec ((na1,na2,t2)::ctx) (Environ.push_rel (na2,Some c2,t2) env)
- (add_binders na1 na2 (sorec ctx env subst c1 c2)) d1 d2
+ (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2
| PIf (a1,b1,b1'), Case (ci,_,a2,[|b2;b2'|]) ->
let ctx_b2,b2 = decompose_lam_n_assum ci.ci_cstr_ndecls.(0) b2 in
@@ -319,7 +317,8 @@ let matches_core_closed env sigma convert allow_partial_app pat c =
let extended_matches env sigma = matches_core env sigma false true true
-let matches env sigma pat c = snd (matches_core_closed env sigma false true pat c)
+let matches env sigma pat c =
+ snd (matches_core_closed env sigma false true (Id.Set.empty,pat) c)
let special_meta = (-1)
@@ -464,10 +463,10 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c =
let result () = aux env c (fun x -> x) lempty in
IStream.thunk result
-let match_subterm env sigma pat c = sub_match env sigma pat c
+let match_subterm env sigma pat c = sub_match env sigma (Id.Set.empty,pat) c
let match_appsubterm env sigma pat c =
- sub_match ~partial_app:true env sigma pat c
+ sub_match ~partial_app:true env sigma (Id.Set.empty,pat) c
let match_subterm_gen env sigma app pat c =
sub_match ~partial_app:app env sigma pat c
@@ -481,11 +480,12 @@ let is_matching_head env sigma pat c =
with PatternMatchingFailure -> false
let is_matching_appsubterm ?(closed=true) env sigma pat c =
+ let pat = (Id.Set.empty,pat) in
let results = sub_match ~partial_app:true ~closed env sigma pat c in
not (IStream.is_empty results)
-let matches_conv env sigma c p =
- snd (matches_core_closed env sigma true false c p)
+let matches_conv env sigma p c =
+ snd (matches_core_closed env sigma true false (Id.Set.empty,p) c)
let is_matching_conv env sigma pat n =
try let _ = matches_conv env sigma pat n in true
diff --git a/pretyping/constr_matching.mli b/pretyping/constr_matching.mli
index 67854a893..b9dcb0af2 100644
--- a/pretyping/constr_matching.mli
+++ b/pretyping/constr_matching.mli
@@ -41,7 +41,8 @@ val matches_head : env -> Evd.evar_map -> constr_pattern -> constr -> patvar_map
variables or metavariables have the same name, the metavariable,
or else the rightmost bound variable, takes precedence *)
val extended_matches :
- env -> Evd.evar_map -> constr_pattern -> constr -> bound_ident_map * extended_patvar_map
+ env -> Evd.evar_map -> Tacexpr.binding_bound_vars * constr_pattern ->
+ constr -> bound_ident_map * extended_patvar_map
(** [is_matching pat c] just tells if [c] matches against [pat] *)
val is_matching : env -> Evd.evar_map -> constr_pattern -> constr -> bool
@@ -72,8 +73,10 @@ val match_subterm : env -> Evd.evar_map -> constr_pattern -> constr -> matching_
val match_appsubterm : env -> Evd.evar_map -> constr_pattern -> constr -> matching_result IStream.t
(** [match_subterm_gen] calls either [match_subterm] or [match_appsubterm] *)
-val match_subterm_gen : env -> Evd.evar_map -> bool (** true = with app context *) ->
- constr_pattern -> constr -> matching_result IStream.t
+val match_subterm_gen : env -> Evd.evar_map ->
+ bool (** true = with app context *) ->
+ Tacexpr.binding_bound_vars * constr_pattern -> constr ->
+ matching_result IStream.t
(** [is_matching_appsubterm pat c] tells if a subterm of [c] matches
against [pat] taking partial subterms into consideration *)
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 5b02c8cd1..3a76e8bd7 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -8,6 +8,7 @@
open Util
open Names
+open Nameops
open Globnames
open Misctypes
open Glob_term
@@ -323,6 +324,65 @@ let free_glob_vars =
let vs = vars Id.Set.empty Id.Set.empty rt in
Id.Set.elements vs
+let add_and_check_ident id set =
+ if Id.Set.mem id set then
+ Pp.(msg_warning
+ (str "Collision between bound variables of name " ++ Id.print id));
+ Id.Set.add id set
+
+let bound_glob_vars =
+ let rec vars bound = function
+ | GLambda (_,na,_,_,_) | GProd (_,na,_,_,_) | GLetIn (_,na,_,_) as c ->
+ let bound = name_fold add_and_check_ident na bound in
+ fold_glob_constr vars bound c
+ | GCases (loc,sty,rtntypopt,tml,pl) ->
+ let bound = vars_option bound rtntypopt in
+ let bound =
+ List.fold_left (fun bound (tm,_) -> vars bound tm) bound tml in
+ List.fold_left vars_pattern bound pl
+ | GLetTuple (loc,nal,rtntyp,b,c) ->
+ let bound = vars_return_type bound rtntyp in
+ let bound = vars bound b in
+ let bound = List.fold_right (name_fold add_and_check_ident) nal bound in
+ vars bound c
+ | GIf (loc,c,rtntyp,b1,b2) ->
+ let bound = vars_return_type bound rtntyp in
+ let bound = vars bound c in
+ let bound = vars bound b1 in
+ vars bound b2
+ | GRec (loc,fk,idl,bl,tyl,bv) ->
+ let bound = Array.fold_right Id.Set.add idl bound in
+ let vars_fix i bound fid =
+ let bound =
+ List.fold_left
+ (fun bound (na,k,bbd,bty) ->
+ let bound = vars_option bound bbd in
+ let bound = vars bound bty in
+ name_fold add_and_check_ident na bound
+ )
+ bound
+ bl.(i)
+ in
+ let bound = vars bound tyl.(i) in
+ vars bound bv.(i)
+ in
+ Array.fold_left_i vars_fix bound idl
+ | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GVar _) -> bound
+ | GApp _ | GCast _ as c -> fold_glob_constr vars bound c
+
+ and vars_pattern bound (loc,idl,p,c) =
+ let bound = List.fold_right add_and_check_ident idl bound in
+ vars bound c
+
+ and vars_option bound = function None -> bound | Some p -> vars bound p
+
+ and vars_return_type bound (na,tyopt) =
+ let bound = name_fold add_and_check_ident na bound in
+ vars_option bound tyopt
+ in
+ fun rt ->
+ vars Id.Set.empty rt
+
(** Mapping of names in binders *)
(* spiwack: I used a smartmap-style kind of mapping here, because the
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index e514fd529..25746323f 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -38,6 +38,7 @@ val fold_glob_constr : ('a -> glob_constr -> 'a) -> 'a -> glob_constr -> 'a
val iter_glob_constr : (glob_constr -> unit) -> glob_constr -> unit
val occur_glob_constr : Id.t -> glob_constr -> bool
val free_glob_vars : glob_constr -> Id.t list
+val bound_glob_vars : glob_constr -> Id.Set.t
val loc_of_glob_constr : glob_constr -> Loc.t
(** [map_pattern_binders f m c] applies [f] to all the binding names
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 593e46b05..96d0b592b 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1038,11 +1038,12 @@ let interp_context ctxt = in_gen (topwit wit_constr_context) ctxt
(* Reads a pattern by substituting vars of lfun *)
let use_types = false
-let eval_pattern lfun ist env sigma (_,pat as c) =
+let eval_pattern lfun ist env sigma ((glob,_),pat as c) =
+ let bound_names = bound_glob_vars glob in
if use_types then
- pi3 (interp_typed_pattern ist env sigma c)
+ (bound_names,pi3 (interp_typed_pattern ist env sigma c))
else
- instantiate_pattern env sigma lfun pat
+ (bound_names,instantiate_pattern env sigma lfun pat)
let read_pattern lfun ist env sigma = function
| Subterm (b,ido,c) -> Subterm (b,ido,eval_pattern lfun ist env sigma c)
diff --git a/tactics/tactic_matching.mli b/tactics/tactic_matching.mli
index abeb47c3b..d8e6dd0ae 100644
--- a/tactics/tactic_matching.mli
+++ b/tactics/tactic_matching.mli
@@ -32,7 +32,7 @@ val match_term :
Environ.env ->
Evd.evar_map ->
Term.constr ->
- (Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list ->
+ (Tacexpr.binding_bound_vars * Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list ->
Tacexpr.glob_tactic_expr t Proofview.tactic
(** [match_goal env sigma hyps concl rules] matches the goal
@@ -45,5 +45,5 @@ val match_goal:
Evd.evar_map ->
Context.named_context ->
Term.constr ->
- (Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list ->
+ (Tacexpr.binding_bound_vars * Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list ->
Tacexpr.glob_tactic_expr t Proofview.tactic
diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v
index 567e21edb..9a60afe5f 100644
--- a/test-suite/output/ltac.v
+++ b/test-suite/output/ltac.v
@@ -6,3 +6,12 @@ Fail let T := constr:((fun a b : nat => a+b) 1 1) in
=> pose ((fun x _ => y) 1 1)
end.
Abort.
+
+(* This should not raise a warning (see #4317) *)
+Goal True.
+assert (H:= eq_refl ((fun x => x) 1)).
+let HT := type of H in
+lazymatch goal with
+| H1 : HT |- _ => idtac "matched"
+end.
+Abort.
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-02 04:26:52 +0000