Merge PR #12765: In recursive notations, accept partial application over the recursive pattern

Reviewed-by: gares
Ack-by: maximedenes
Ack-by: jfehrle

6 files changed, 53 insertions, 5 deletions

diff --git a/doc/changelog/03-notations/12765-master+partial-app-in-recursive-notation.rst b/doc/changelog/03-notations/12765-master+partial-app-in-recursive-notation.rst
new file mode 100644
index 0000000000..82cbefc60b
--- /dev/null
+++ b/doc/changelog/03-notations/12765-master+partial-app-in-recursive-notation.rst
@@ -0,0 +1,4 @@
+- **Added:**
+  Added support for encoding notations of the form :g:`x ⪯ y ⪯ .. ⪯ z ⪯ t`
+  (`#12765 <https://github.com/coq/coq/pull/12765>`_,
+  by Hugo Herbelin).
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index f36767b207..56b14d0935 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -787,20 +787,39 @@ nested iterating pattern, the second placeholder is finally filled with the
 terminating expression.
 
 In the example above, the iterator :math:`φ([~]_E , [~]_I)` is :math:`cons [~]_E\, [~]_I`
-and the terminating expression is ``nil``. Here are other examples:
+and the terminating expression is ``nil``.
+
+Here is another example with the pattern associating on the left:
 
 .. coqtop:: in
 
    Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) (at level 0).
 
+Here is an example with more involved recursive patterns:
+
+.. coqtop:: in
+
    Notation "[| t * ( x , y , .. , z ) ; ( a , b , .. , c )  * u |]" :=
      (pair (pair .. (pair (pair t x) (pair t y)) .. (pair t z))
            (pair .. (pair (pair a u) (pair b u)) .. (pair c u)))
      (t at level 39).
 
-Notations with recursive patterns can be reserved like standard
-notations, they can also be declared within
-:ref:`notation scopes <Scopes>`.
+To give a flavor of the extent and limits of the mechanism, here is an
+example showing a notation for a chain of equalities. It relies on an
+artificial expansion of the intended denotation so as to expose a
+``φ(x, .. φ(y,t) ..)`` structure, with the drawback that if ever the
+beta-redexes are contracted, the notations stops to be used for
+printing.
+
+.. coqtop:: in
+
+   Notation "x  ⪯ y  ⪯ ..  ⪯ z  ⪯ t" :=
+     ((fun b A a => a <= b /\ A b) y .. ((fun b A a => a <= b /\ A b) z (fun b => b <= t)) .. x)
+     (at level 70, y at next level, z at next level, t at next level).
+
+Note finally that notations with recursive patterns can be reserved like
+standard notations, they can also be declared within :ref:`notation
+scopes <Scopes>`.
 
 .. _RecursiveNotationsWithBinders:
 
diff --git a/interp/notation.ml b/interp/notation.ml
index 948ebe9640..1a361dc1a6 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -391,6 +391,10 @@ let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *)
   | NBinderList (_,_,NApp (NRef ref,args),_,_) ->
       RefKey (canonical_gr ref), AppBoundedNotation (List.length args)
   | NRef ref -> RefKey(canonical_gr ref), NotAppNotation
+  | NApp (NList (_,_,NApp (NRef ref,args),_,_), args') ->
+      RefKey (canonical_gr ref), AppBoundedNotation (List.length args + List.length args')
+  | NApp (NList (_,_,NApp (_,args),_,_), args') ->
+      Oth, AppBoundedNotation (List.length args + List.length args')
   | NApp (_,args) -> Oth, AppBoundedNotation (List.length args)
   | NList (_,_,NApp (NVar x,_),_,_) when x = Notation_ops.ldots_var -> Oth, AppUnboundedNotation
   | _ -> Oth, NotAppNotation
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 2e3fa0aa0e..7cb3ca25ee 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -275,6 +275,12 @@ type found_variables = {
 let add_id r id = r := { !r with vars = id :: (!r).vars }
 let add_name r = function Anonymous -> () | Name id -> add_id r id
 
+let mkNApp1 (g,a) =
+  match g with
+  (* Ensure flattening of nested applicative nodes *)
+  | NApp (g,args') -> NApp (g,args'@[a])
+  | _ -> NApp (g,[a])
+
 let is_gvar id c = match DAst.get c with
 | GVar id' -> Id.equal id id'
 | _ -> false
@@ -443,7 +449,10 @@ let notation_constr_and_vars_of_glob_constr recvars a =
         aux' c
   and aux' x = DAst.with_val (function
   | GVar id -> if not (Id.equal id ldots_var) then add_id found id; NVar id
-  | GApp (g,args) -> NApp (aux g, List.map aux args)
+  | GApp (g,[]) -> NApp (aux g,[]) (* Encoding @foo *)
+  | GApp (g,args) ->
+     (* Treat applicative notes as binary nodes *)
+     let a,args = List.sep_last args in mkNApp1 (aux (DAst.make (GApp (g, args))), aux a)
   | GLambda (na,bk,ty,c) -> add_name found na; NLambda (na,aux ty,aux c)
   | GProd (na,bk,ty,c) -> add_name found na; NProd (na,aux ty,aux c)
   | GLetIn (na,b,t,c) -> add_name found na; NLetIn (na,aux b,Option.map aux t, aux c)
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index bd22d45059..623ca316c9 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -249,3 +249,5 @@ myfoo01 tt
      : nat
 myfoo01 tt
      : nat
+1 ⪯ 2 ⪯ 3 ⪯ 4
+     : Prop
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index 839df99ea7..ce97d909a7 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -410,3 +410,13 @@ Check myfoo0 1 tt. (* was printing [myfoo0 1 HI], but should print [myfoo01 HI]
 Check myfoo01 tt. (* was printing [myfoo0 1 HI], but should print [myfoo01 HI]  *)
 
 End Issue8126.
+
+Module RecursiveNotationPartialApp.
+
+(* Discussed on Coq Club, 28 July 2020 *)
+Notation "x  ⪯ y  ⪯ ..  ⪯ z  ⪯ t" :=
+  ((fun b A a => a <= b /\ A b) y .. ((fun b A a => a <= b /\ A b) z (fun b => b <= t)) .. x)
+  (at level 70, y at next level, z at next level, t at next level).
+Check 1 ⪯ 2 ⪯ 3 ⪯ 4.
+
+End RecursiveNotationPartialApp.