Taking into account binding patterns when agglutinating sequences of binders.

Supporting accordingly printing of sequences of binders including binding
patterns.

5 files changed, 49 insertions, 14 deletions

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 1b84ccff48..12da344623 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -864,8 +864,14 @@ let rec match_cases_pattern_binders metas acc pat1 pat2 =
 let glue_letin_with_decls = true
 
 let rec match_iterated_binders islambda decls = function
+  | GLambda (_,Name p,bk,t,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],b)]))
+      when islambda && Id.equal p e ->
+      match_iterated_binders islambda ((Inr cp,bk,None,t)::decls) b
   | GLambda (_,na,bk,t,b) when islambda ->
       match_iterated_binders islambda ((Inl na,bk,None,t)::decls) b
+  | GLambda (_,Name p,bk,t,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],b)]))
+      when not islambda && Id.equal p e ->
+      match_iterated_binders islambda ((Inr cp,bk,None,t)::decls) b
   | GProd (_,(Name _ as na),bk,t,b) when not islambda ->
       match_iterated_binders islambda ((Inl na,bk,None,t)::decls) b
   | GLetIn (loc,na,c,b) when glue_letin_with_decls ->
@@ -947,11 +953,11 @@ let rec match_ inner u alp metas sigma a1 a2 =
       match_termlist (match_hd u alp) alp metas sigma r1 x y iter termin lassoc
 
   (* "λ p, let 'cp = p in t" -> "λ 'cp, t" *)
-  | GLambda (_,Name p,bk,t1,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],t)])),
-    NBinderList (x,_,NLambda (Name id2,_,b2),(NVar v as termin)) when p = e ->
-      let decls = [(Inr cp,bk,None,t1)] in
+  | GLambda (_,Name p,bk,t1,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],b1)])),
+    NBinderList (x,_,NLambda (Name _id2,_,b2),termin) when Id.equal p e ->
+      let (decls,b) = match_iterated_binders true [(Inr cp,bk,None,t1)] b1 in
       let alp,sigma = bind_bindinglist_env alp sigma x decls in
-      match_in u alp metas sigma t termin
+      match_in u alp metas sigma b termin
 
   (* Matching recursive notations for binders: ad hoc cases supporting let-in *)
   | GLambda (_,na1,bk,t1,b1), NBinderList (x,_,NLambda (Name _id2,_,b2),termin)->
@@ -961,11 +967,11 @@ let rec match_ inner u alp metas sigma a1 a2 =
       match_in u alp metas sigma b termin
 
   (* "∀ p, let 'cp = p in t" -> "∀ 'cp, t" *)
-  | GProd (_,Name p,bk,t1,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],t)])),
-    NBinderList (x,_,NProd (Name id2,_,b2),(NVar v as termin)) when p = e ->
-      let decls = [(Inr cp,bk,None,t1)] in
+  | GProd (_,Name p,bk,t1,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],b1)])),
+    NBinderList (x,_,NProd (Name _id2,_,b2),(NVar v as termin)) when Id.equal p e ->
+      let (decls,b) = match_iterated_binders true [(Inr cp,bk,None,t1)] b1 in
       let alp,sigma = bind_bindinglist_env alp sigma x decls in
-      match_in u alp metas sigma t termin
+      match_in u alp metas sigma b termin
 
   | GProd (_,na1,bk,t1,b1), NBinderList (x,_,NProd (Name _id2,_,b2),termin)
       when na1 != Anonymous ->
@@ -978,6 +984,11 @@ let rec match_ inner u alp metas sigma a1 a2 =
       match_binderlist_with_app (match_hd u) alp metas sigma r x y iter termin
 
   (* Matching individual binders as part of a recursive pattern *)
+  | GLambda (_,Name p,bk,t,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],b1)])),
+    NLambda (Name id,_,b2)
+      when is_bindinglist_meta id metas ->
+      let alp,sigma = bind_bindinglist_env alp sigma id [(Inr cp,bk,None,t)] in
+      match_in u alp metas sigma b1 b2
   | GLambda (_,na,bk,t,b1), NLambda (Name id,_,b2)
       when is_bindinglist_meta id metas ->
       let alp,sigma = bind_bindinglist_env alp sigma id [(Inl na,bk,None,t)] in
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index be92372aca..7aa6d4858c 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -349,8 +349,8 @@ end) = struct
         | _ -> c, CHole (Loc.ghost, None, Misctypes.IntroAnonymous, None) in
       surround (pr_lname na ++ pr_opt_type pr_c topt ++
                   str":=" ++ cut() ++ pr_c c)
-    | LocalPattern _ ->
-      assert false
+    | LocalPattern (loc,p,tyo) ->
+        str "'" ++ pr_patt lsimplepatt p
 
   let pr_undelimited_binders sep pr_c =
     prlist_with_sep sep (pr_binder_among_many pr_c)
@@ -360,10 +360,8 @@ end) = struct
     match bl with
       | [LocalRawAssum (nal,k,t)] ->
         pr_com_at n ++ kw() ++ pr_binder false pr_c (nal,k,t)
-      | LocalRawAssum _ :: _ as bdl ->
+      | (LocalRawAssum _ | LocalPattern _) :: _ as bdl ->
         pr_com_at n ++ kw() ++ pr_undelimited_binders sep pr_c bdl
-      | LocalPattern (loc,p,tyo) :: _ ->
-        str "'" ++ pr_patt ltop p
       | _ -> assert false
 
   let pr_binders_gen pr_c sep is_open =
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index 950382d572..360f379676 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -96,3 +96,5 @@ fun n : nat => foo4 n (fun _ _ : nat => ETA z : nat, (fun _ : nat => z = 0))
      : nat -> Prop
 fun n : nat => foo4 n (fun _ y : nat => ETA z : nat, (fun _ : nat => y = 0))
      : nat -> Prop
+tele (t : Type) '(y, z) (x : t0) := tt
+     : forall t : Type, nat * nat -> t -> fpack
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index 9efac6508c..4b8bfe3124 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -115,3 +115,27 @@ Check fun n => foo4 n (fun x y z => (fun _ => x=0) z).
 Check fun n => foo4 n (fun x y z => (fun _ => z=0) z).
 Check fun n => foo4 n (fun x y z => (fun _ => y=0) z).
 
+(**********************************************************************)
+(* Test printing of #4932                                             *)
+
+Inductive ftele : Type :=
+| fb {T:Type} : T -> ftele
+| fr {T} : (T -> ftele) -> ftele.
+
+Fixpoint args ftele : Type :=
+  match ftele with
+    | fb _ => unit
+    | fr f => sigT (fun t => args (f t))
+  end.
+
+Definition fpack := sigT args.
+Definition pack fp fa : fpack := existT _ fp fa.
+
+Notation "'tele' x .. z := b" :=
+  (fun x => .. (fun z =>
+     pack (fr (fun x => .. ( fr (fun z => fb b) ) .. ) )
+          (existT _ x .. (existT _ z tt) .. )
+                ) ..)
+  (at level 85, x binder, z binder).
+
+Check tele (t:Type) '((y,z):nat*nat) (x:t) := tt.
diff --git a/test-suite/output/PatternsInBinders.out b/test-suite/output/PatternsInBinders.out
index 5f9ea9e3d6..6acaa0ccec 100644
--- a/test-suite/output/PatternsInBinders.out
+++ b/test-suite/output/PatternsInBinders.out
@@ -23,7 +23,7 @@ Arguments A, B are implicit and maximally inserted
 Argument scopes are [type_scope type_scope _]
 forall (A B : Type) (pat : A * B), let '(x, y) := pat in swap (x, y) = (y, x)
      : Prop
-exists pat : A * A, let '(x, y) := pat in swap (x, y) = (y, x)
+exists '(x, y), swap (x, y) = (y, x)
      : Prop
 both_z = 
 fun pat : nat * nat =>