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

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

1 files changed, 29 insertions, 19 deletions

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