Fixing #5401 (printing of patterns with bound anonymous variables).

This fixes also #5731, #6035, #5364.

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.