A (significant) simplification in printing notations with recursive binders.

For historical reasons (this was one of the first examples of
notations with binders), there was a special treatment for notations
whose right-hand side had the form "forall x, P" or "fun x => P". Not
only this is not necessary, but this prevents notations binding to
expressions such as "forall x, x>0 -> P" to be used in printing.

We let the general case absorb this particular case.

We add the integration of "let x:=c in ..." in the middle of a
notation with recursive binders as part of the binder list, reprinting
it "(x:=c)" (this was formerly the case only for the above particular
case).

Note that integrating "let" in sequence of binders is stil not the
case for the regular "forall"/"fun". Should we?

5 files changed, 24 insertions, 77 deletions

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index b7c1d84f13..0480a93e27 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -975,36 +975,9 @@ let rec match_cases_pattern_binders metas (alp,sigma as acc) pat1 pat2 =
   | PatCstr (c1,patl1,na1), PatCstr (c2,patl2,na2)
       when eq_constructor c1 c2 && Int.equal (List.length patl1) (List.length patl2) ->
       List.fold_left2 (match_cases_pattern_binders metas)
-	(match_names metas acc na1 na2) patl1 patl2
+        (match_names metas acc na1 na2) patl1 patl2
   | _ -> raise No_match
 
-let glue_letin_with_decls = true
-
-let rec match_iterated_binders islambda decls bi revert = DAst.(with_loc_val (fun ?loc -> function
-  | GLambda (na,bk,t,b) as b0 ->
-    begin match na, DAst.get b with
-    | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(ids,[cp],b))])
-      when islambda && is_gvar p e && not (occur_glob_constr p b) ->
-      match_iterated_binders islambda ((DAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t))::decls) b revert
-    | _, _ when islambda ->
-      match_iterated_binders islambda ((DAst.make ?loc @@ GLocalAssum(na,bk,t))::decls) b revert
-    | _ -> (decls, DAst.make ?loc b0)
-    end
-  | GProd (na,bk,t,b) as b0 ->
-    begin match na, DAst.get b with
-    | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(ids,[cp],b))])
-      when not islambda && is_gvar p e && not (occur_glob_constr p b) ->
-      match_iterated_binders islambda ((DAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t))::decls) b revert
-    | Name _, _ when not islambda ->
-      match_iterated_binders islambda ((DAst.make ?loc @@ GLocalAssum(na,bk,t))::decls) b revert
-    | _ -> (decls, DAst.make ?loc b0)
-    end
-  | GLetIn (na,c,t,b) when glue_letin_with_decls ->
-      match_iterated_binders islambda
-        ((DAst.make ?loc @@ GLocalDef (na,Explicit (*?*), c,t))::decls) b revert
-  | b -> (decls, DAst.make ?loc b)
-  )) bi
-
 let remove_sigma x (terms,termlists,binders,binderlists) =
   (Id.List.remove_assoc x terms,termlists,binders,binderlists)
 
@@ -1015,7 +988,9 @@ let add_ldots_var metas = (ldots_var,((None,[]),NtnTypeConstr))::metas
 
 let add_meta_bindinglist x metas = (x,((None,[]),NtnTypeBinderList))::metas
 
-let match_binderlist_with_app match_fun alp metas sigma rest x y iter termin revert =
+let glue_letin_with_decls = true
+
+let match_binderlist match_fun alp metas sigma rest x y iter termin revert =
   let rec aux sigma bl rest =
     try
       let metas = add_ldots_var (add_meta_bindinglist y metas) in
@@ -1028,8 +1003,12 @@ let match_binderlist_with_app match_fun alp metas sigma rest x y iter termin rev
       (* In case y is bound not only to a binder but also to a term *)
       let sigma = remove_sigma y sigma in
       aux sigma (b::bl) rest
-    with No_match when not (List.is_empty bl) ->
-      bl, rest, sigma in
+    with No_match ->
+    match DAst.get rest with
+    | GLetIn (na,c,t,rest) when glue_letin_with_decls ->
+       let b = DAst.make ?loc:rest.CAst.loc @@ GLocalDef (na,Explicit (*?*), c,t) in
+       aux sigma (b::bl) rest
+    | _ -> if not (List.is_empty bl) then bl, rest, sigma else raise No_match in
   let bl,rest,sigma = aux sigma [] rest in
   let bl = if revert then List.rev bl else bl in
   let alp,sigma = bind_bindinglist_env alp sigma x bl in
@@ -1096,46 +1075,9 @@ let rec match_ inner u alp metas sigma a1 a2 =
   | r1, NList (x,y,iter,termin,revert) ->
       match_termlist (match_hd u alp) alp metas sigma a1 x y iter termin revert
 
-  | GLambda (na1, bk, t1, b1), NBinderList (x,y,iter,termin,revert) ->
-    begin match na1, DAst.get b1, iter with
-    (* "λ p, let 'cp = p in t" -> "λ 'cp, t" *)
-    | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(ids,[cp],b1))]), NLambda (Name _, _, _)
-      when is_gvar p e && not (occur_glob_constr p b1) ->
-      let (decls,b) = match_iterated_binders true [DAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t1)] b1 revert in
-      let alp,sigma = bind_bindinglist_env alp sigma x decls in
-      match_in u alp metas sigma b termin
-    (* Matching recursive notations for binders: ad hoc cases supporting let-in *)
-    | _, _, NLambda (Name _,_,_) ->
-      let (decls,b) = match_iterated_binders true [DAst.make ?loc @@ GLocalAssum (na1,bk,t1)] b1 revert in
-      (* TODO: address the possibility that termin is a Lambda itself *)
-      let alp,sigma = bind_bindinglist_env alp sigma x decls in
-      match_in u alp metas sigma b termin
-    (* Matching recursive notations for binders: general case *)
-    | _, _, _ ->
-      match_binderlist_with_app (match_hd u) alp metas sigma a1 x y iter termin revert
-    end
-
-  | GProd (na1, bk, t1, b1), NBinderList (x,y,iter,termin,revert) ->
-    (* "∀ p, let 'cp = p in t" -> "∀ 'cp, t" *)
-    begin match na1, DAst.get b1, iter, termin with
-    | Name p, GCases (LetPatternStyle,None,[(e, _)],[(_,(ids,[cp],b1))]), NProd (Name _,_,_), NVar _
-      when is_gvar p e && not (occur_glob_constr p b1) ->
-      let (decls,b) = match_iterated_binders true [DAst.make ?loc @@ GLocalPattern ((cp,ids),p,bk,t1)] b1 revert in
-      let alp,sigma = bind_bindinglist_env alp sigma x decls in
-      match_in u alp metas sigma b termin
-    | _, _,  NProd (Name _,_,_), _ when na1 != Anonymous ->
-      let (decls,b) = match_iterated_binders false [DAst.make ?loc @@ GLocalAssum (na1,bk,t1)] b1 revert in
-      (* TODO: address the possibility that termin is a Prod itself *)
-      let alp,sigma = bind_bindinglist_env alp sigma x decls in
-      match_in u alp metas sigma b termin
-    (* Matching recursive notations for binders: general case *)
-    | _, _, _, _ ->
-      match_binderlist_with_app (match_hd u) alp metas sigma a1 x y iter termin revert
-    end
-
   (* Matching recursive notations for binders: general case *)
   | _r, NBinderList (x,y,iter,termin,revert) ->
-       match_binderlist_with_app (match_hd u) alp metas sigma a1 x y iter termin revert
+      match_binderlist (match_hd u) alp metas sigma a1 x y iter termin revert
 
   (* Matching compositionally *)
   | GVar id1, NVar id2 when alpha_var id1 id2 (fst alp) -> sigma
diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out
index 121a369a94..0e5f399036 100644
--- a/test-suite/output/Notations2.out
+++ b/test-suite/output/Notations2.out
@@ -17,10 +17,8 @@ fun (P : nat -> nat -> Prop) (x : nat) => exists y, P x y
 ∃ n p : nat, n + p = 0
      : Prop
 let a := 0 in
-∃ x y : nat,
-let b := 1 in
-let c := b in
-let d := 2 in ∃ z : nat, let e := 3 in let f := 4 in x + y = z + d
+∃ (x y : nat) (b := 1) (c := b) (d := 2) (z : nat) (e := 3) (f := 4), 
+x + y = z + d
      : Prop
 ∀ n p : nat, n + p = 0
      : Prop
diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v
index 531398bb0b..923caedace 100644
--- a/test-suite/output/Notations2.v
+++ b/test-suite/output/Notations2.v
@@ -36,8 +36,9 @@ Check fun P:nat->nat->Prop => fun x:nat => ex (P x).
 
 (* Test notations with binders *)
 
-Notation "∃  x .. y , P":= (ex (fun x => .. (ex (fun y => P)) ..))
-  (x binder, y binder, at level 200, right associativity).
+Notation "∃ x .. y , P":= (ex (fun x => .. (ex (fun y => P)) ..))
+  (x binder, y binder, at level 200, right associativity,
+  format "'[  ' ∃  x  ..  y ']' ,  P").
 
 Check (∃ n p, n+p=0).
 
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index 7c47c0885d..cb18fa3564 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -152,8 +152,7 @@ exists x : nat,
     nat ->
     exists '{{z, t}}, forall z2 : nat, z2 = 0 /\ x + y = 0 /\ z + t = 0
      : Prop
-exists_true '{{x, y}},
-(let u := 0 in exists_true '{{z, t}}, x + y = 0 /\ z + t = 0)
+exists_true '{{x, y}} (u := 0) '{{z, t}}, x + y = 0 /\ z + t = 0
      : Prop
 exists_true (A : Type) (R : A -> A -> Prop) (_ : Reflexive R),
 (forall x : A, R x x)
@@ -173,6 +172,8 @@ exists_true (x : nat) (A : Type) (R : A -> A -> Prop)
      : Prop * Prop
 exists_non_null x y z t : nat , x = y /\ z = t
      : Prop
+forall_non_null x y z t : nat , x = y /\ z = t
+     : Prop
 {{RL 1, 2}}
      : nat * (nat * nat)
 {{RR 1, 2}}
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index ee6f0a09e0..d768b9ba49 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -308,6 +308,11 @@ Notation "'exists_non_null' x .. y  , P" :=
   (at level 200, x binder).
 Check exists_non_null x y z t , x=y/\z=t.
 
+Notation "'forall_non_null' x .. y  , P" :=
+  (forall x, x <> 0 -> .. (forall y, y <> 0 -> P) ..)
+  (at level 200, x binder).
+Check forall_non_null x y z t , x=y/\z=t.
+
 (* Examples where the recursive pattern is in reverse order *)
 
 Notation "{{RL  c , .. , d }}" := (pair d .. (pair c 0) ..).