diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-10-11 14:36:29 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-10-11 15:21:33 +0200 |
commit | e9995f6e9f9523d4738d9ee494703b6f96bf995d (patch) | |
tree | ce5297379247c6af9e6c16ba45b5b7e479b96d3c /pretyping | |
parent | ae5305a4837cce3c7fd61b92ce8110ac66ec2750 (diff) |
Fixing untimely unexpected warning "Collision between bound variables" (#4317).
Collecting the bound variables is now done on the glob_constr, before
interpretation, so that only variables given explicitly by the user
are used for binding bound variables.
Diffstat (limited to 'pretyping')
-rw-r--r-- | pretyping/constr_matching.ml | 46 | ||||
-rw-r--r-- | pretyping/constr_matching.mli | 9 | ||||
-rw-r--r-- | pretyping/glob_ops.ml | 60 | ||||
-rw-r--r-- | pretyping/glob_ops.mli | 1 |
4 files changed, 90 insertions, 26 deletions
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 |