diff options
-rw-r--r-- | engine/namegen.ml | 13 | ||||
-rw-r--r-- | engine/namegen.mli | 7 | ||||
-rw-r--r-- | interp/constrextern.ml | 48 | ||||
-rw-r--r-- | pretyping/patternops.ml | 25 | ||||
-rw-r--r-- | pretyping/patternops.mli | 2 | ||||
-rw-r--r-- | test-suite/bugs/closed/5401.v | 21 |
6 files changed, 93 insertions, 23 deletions
diff --git a/engine/namegen.ml b/engine/namegen.ml index 2e62b8901..a38c73ed0 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -376,15 +376,22 @@ let next_name_for_display sigma flags = | RenamingElsewhereFor env_t -> next_name_away_for_default_printing sigma env_t (* Remark: Anonymous var may be dependent in Evar's contexts *) -let compute_displayed_name_in sigma flags avoid na c = +let compute_displayed_name_in_gen_poly noccurn_fun sigma flags avoid na c = match na with - | Anonymous when noccurn sigma 1 c -> + | Anonymous when noccurn_fun sigma 1 c -> (Anonymous,avoid) | _ -> let fresh_id = next_name_for_display sigma flags na avoid in - let idopt = if noccurn sigma 1 c then Anonymous else Name fresh_id in + let idopt = if noccurn_fun sigma 1 c then Anonymous else Name fresh_id in (idopt, Id.Set.add fresh_id avoid) +let compute_displayed_name_in = compute_displayed_name_in_gen_poly noccurn + +let compute_displayed_name_in_gen f sigma = + (* only flag which does not need a constr, maybe to be refined *) + let flag = RenamingForGoal in + compute_displayed_name_in_gen_poly f sigma flag + let compute_and_force_displayed_name_in sigma flags avoid na c = match na with | Anonymous when noccurn sigma 1 c -> diff --git a/engine/namegen.mli b/engine/namegen.mli index 6fde90a39..d29b69259 100644 --- a/engine/namegen.mli +++ b/engine/namegen.mli @@ -106,10 +106,15 @@ val compute_displayed_name_in : val compute_and_force_displayed_name_in : evar_map -> renaming_flags -> Id.Set.t -> Name.t -> constr -> Name.t * Id.Set.t val compute_displayed_let_name_in : - evar_map -> renaming_flags -> Id.Set.t -> Name.t -> constr -> Name.t * Id.Set.t + evar_map -> renaming_flags -> Id.Set.t -> Name.t -> 'a -> Name.t * Id.Set.t val rename_bound_vars_as_displayed : evar_map -> Id.Set.t -> Name.t list -> types -> types +(* Generic function expecting a "not occurn" function *) +val compute_displayed_name_in_gen : + (evar_map -> int -> 'a -> bool) -> + evar_map -> Id.Set.t -> Name.t -> 'a -> Name.t * Id.Set.t + (**********************************************************************) (* Naming strategy for arguments in Prop when eliminating inductive types *) diff --git a/interp/constrextern.ml b/interp/constrextern.ml index f1bee65ef..bb4227b4a 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -1120,7 +1120,11 @@ let any_any_branch = (* | _ => _ *) Loc.tag ([],[DAst.make @@ PatVar Anonymous], DAst.make @@ GHole (Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None)) -let rec glob_of_pat env sigma pat = DAst.make @@ match pat with +let compute_displayed_name_in_pattern sigma avoid na c = + let open Namegen in + compute_displayed_name_in_gen (fun _ -> Patternops.noccurn_pattern) sigma avoid na c + +let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with | PRef ref -> GRef (ref,None) | PVar id -> GVar id | PEvar (evk,l) -> @@ -1130,7 +1134,7 @@ let rec glob_of_pat env sigma pat = DAst.make @@ match pat with | None -> Id.of_string "__" | Some id -> id in - GEvar (id,List.map (on_snd (glob_of_pat env sigma)) l) + GEvar (id,List.map (on_snd (glob_of_pat avoid env sigma)) l) | PRel n -> let id = try match lookup_name_of_rel n env with | Name id -> id @@ -1141,30 +1145,36 @@ let rec glob_of_pat env sigma pat = DAst.make @@ match pat with | PMeta None -> GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous,None) | PMeta (Some n) -> GPatVar (Evar_kinds.FirstOrderPatVar n) | PProj (p,c) -> GApp (DAst.make @@ GRef (ConstRef (Projection.constant p),None), - [glob_of_pat env sigma c]) + [glob_of_pat avoid env sigma c]) | PApp (f,args) -> - GApp (glob_of_pat env sigma f,Array.map_to_list (glob_of_pat env sigma) args) + GApp (glob_of_pat avoid env sigma f,Array.map_to_list (glob_of_pat avoid env sigma) args) | PSoApp (n,args) -> GApp (DAst.make @@ GPatVar (Evar_kinds.SecondOrderPatVar n), - List.map (glob_of_pat env sigma) args) + List.map (glob_of_pat avoid env sigma) args) | PProd (na,t,c) -> - GProd (na,Explicit,glob_of_pat env sigma t,glob_of_pat (na::env) sigma c) + let na',avoid' = compute_displayed_name_in_pattern sigma avoid na c in + let env' = Termops.add_name na' env in + GProd (na',Explicit,glob_of_pat avoid env sigma t,glob_of_pat avoid' env' sigma c) | PLetIn (na,b,t,c) -> - GLetIn (na,glob_of_pat env sigma b, Option.map (glob_of_pat env sigma) t, - glob_of_pat (na::env) sigma c) + let na',avoid' = Namegen.compute_displayed_let_name_in sigma Namegen.RenamingForGoal avoid na c in + let env' = Termops.add_name na' env in + GLetIn (na',glob_of_pat avoid env sigma b, Option.map (glob_of_pat avoid env sigma) t, + glob_of_pat avoid' env' sigma c) | PLambda (na,t,c) -> - GLambda (na,Explicit,glob_of_pat env sigma t, glob_of_pat (na::env) sigma c) + let na',avoid' = compute_displayed_name_in_pattern sigma avoid na c in + let env' = Termops.add_name na' env in + GLambda (na',Explicit,glob_of_pat avoid env sigma t, glob_of_pat avoid' env' sigma c) | PIf (c,b1,b2) -> - GIf (glob_of_pat env sigma c, (Anonymous,None), - glob_of_pat env sigma b1, glob_of_pat env sigma b2) + GIf (glob_of_pat avoid env sigma c, (Anonymous,None), + glob_of_pat avoid env sigma b1, glob_of_pat avoid env sigma b2) | PCase ({cip_style=LetStyle; cip_ind_tags=None},PMeta None,tm,[(0,n,b)]) -> - let nal,b = it_destRLambda_or_LetIn_names n (glob_of_pat env sigma b) in - GLetTuple (nal,(Anonymous,None),glob_of_pat env sigma tm,b) + let nal,b = it_destRLambda_or_LetIn_names n (glob_of_pat avoid env sigma b) in + GLetTuple (nal,(Anonymous,None),glob_of_pat avoid env sigma tm,b) | PCase (info,p,tm,bl) -> let mat = match bl, info.cip_ind with | [], _ -> [] | _, Some ind -> - let bl' = List.map (fun (i,n,c) -> (i,n,glob_of_pat env sigma c)) bl in + let bl' = List.map (fun (i,n,c) -> (i,n,glob_of_pat avoid env sigma c)) bl in simple_cases_matrix_of_branches ind bl' | _, None -> anomaly (Pp.str "PCase with some branches but unknown inductive.") in @@ -1173,16 +1183,16 @@ let rec glob_of_pat env sigma pat = DAst.make @@ match pat with let indnames,rtn = match p, info.cip_ind, info.cip_ind_tags with | PMeta None, _, _ -> (Anonymous,None),None | _, Some ind, Some nargs -> - return_type_of_predicate ind nargs (glob_of_pat env sigma p) + return_type_of_predicate ind nargs (glob_of_pat avoid env sigma p) | _ -> anomaly (Pp.str "PCase with non-trivial predicate but unknown inductive.") in - GCases (RegularStyle,rtn,[glob_of_pat env sigma tm,indnames],mat) - | PFix f -> DAst.get (Detyping.detype_names false Id.Set.empty env (Global.env()) sigma (EConstr.of_constr (mkFix f))) (** FIXME bad env *) - | PCoFix c -> DAst.get (Detyping.detype_names false Id.Set.empty env (Global.env()) sigma (EConstr.of_constr (mkCoFix c))) + GCases (RegularStyle,rtn,[glob_of_pat avoid env sigma tm,indnames],mat) + | PFix f -> DAst.get (Detyping.detype_names false avoid env (Global.env()) sigma (EConstr.of_constr (mkFix f))) (** FIXME bad env *) + | PCoFix c -> DAst.get (Detyping.detype_names false avoid env (Global.env()) sigma (EConstr.of_constr (mkCoFix c))) | PSort s -> GSort s let extern_constr_pattern env sigma pat = - extern true (None,[]) Id.Set.empty (glob_of_pat env sigma pat) + extern true (None,[]) Id.Set.empty (glob_of_pat Idset.empty env sigma pat) let extern_rel_context where env sigma sign = let a = detype_rel_context Detyping.Later where Id.Set.empty (names_of_rel_context env,env) sigma sign in diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 3b3ad021e..aaa946706 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -96,6 +96,31 @@ let rec occur_meta_pattern = function | PMeta _ | PSoApp _ -> true | PEvar _ | PVar _ | PRef _ | PRel _ | PSort _ | PFix _ | PCoFix _ -> false +let rec occurn_pattern n = function + | PRel p -> Int.equal n p + | PApp (f,args) -> + (occurn_pattern n f) || (Array.exists (occurn_pattern n) args) + | PProj (_,arg) -> occurn_pattern n arg + | PLambda (na,t,c) -> (occurn_pattern n t) || (occurn_pattern (n+1) c) + | PProd (na,t,c) -> (occurn_pattern n t) || (occurn_pattern (n+1) c) + | PLetIn (na,b,t,c) -> + Option.fold_left (fun b t -> b || occurn_pattern n t) (occurn_pattern n b) t || + (occurn_pattern (n+1) c) + | PIf (c,c1,c2) -> + (occurn_pattern n c) || + (occurn_pattern n c1) || (occurn_pattern n c2) + | PCase(_,p,c,br) -> + (occurn_pattern n p) || + (occurn_pattern n c) || + (List.exists (fun (_,_,p) -> occurn_pattern n p) br) + | PMeta _ | PSoApp _ -> true + | PEvar (_,args) -> Array.exists (occurn_pattern n) args + | PVar _ | PRef _ | PSort _ -> false + | PFix fix -> not (noccurn n (mkFix fix)) + | PCoFix cofix -> not (noccurn n (mkCoFix cofix)) + +let noccurn_pattern n c = not (occurn_pattern n c) + exception BoundPattern;; let rec head_pattern_bound t = diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli index ffe0186af..2d1ce1dbc 100644 --- a/pretyping/patternops.mli +++ b/pretyping/patternops.mli @@ -22,6 +22,8 @@ val occur_meta_pattern : constr_pattern -> bool val subst_pattern : substitution -> constr_pattern -> constr_pattern +val noccurn_pattern : int -> constr_pattern -> bool + exception BoundPattern (** [head_pattern_bound t] extracts the head variable/constant of the diff --git a/test-suite/bugs/closed/5401.v b/test-suite/bugs/closed/5401.v new file mode 100644 index 000000000..95193b993 --- /dev/null +++ b/test-suite/bugs/closed/5401.v @@ -0,0 +1,21 @@ +(* Testing printing of bound unnamed variables in pattern printer *) + +Module A. +Parameter P : nat -> Type. +Parameter v : forall m, P m. +Parameter f : forall (P : nat -> Type), (forall a, P a) -> P 0. +Class U (R : P 0) (m : forall x, P x) : Prop. +Instance w : U (f _ (fun _ => v _)) v. +Print HintDb typeclass_instances. +End A. + +(* #5731 *) + +Module B. +Axiom rel : Type -> Prop. +Axiom arrow_rel : forall {A1}, A1 -> rel A1. +Axiom forall_rel : forall E, (forall v1 : Type, E v1 -> rel v1) -> Prop. +Axiom inl_rel: forall_rel _ (fun _ => arrow_rel). +Hint Resolve inl_rel : foo. +Print HintDb foo. +End B. |