From ca0e42c0ff9e5cebb734bcb59065a4f55ae4aa4e Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 28 Jul 2020 23:47:11 +0200 Subject: In recursive notations, accept partial application over the recursive pattern. This allows e.g. to support a notation of the form "x <== y <== z <= t" standing for "x <= y /\ y <= z /\ z <= t". --- interp/notation.ml | 4 ++++ interp/notation_ops.ml | 11 ++++++++++- test-suite/output/Notations3.out | 2 ++ test-suite/output/Notations3.v | 10 ++++++++++ 4 files changed, 26 insertions(+), 1 deletion(-) 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. -- cgit v1.2.3 From 5b3b6ee984026981f2fd72cd8c538aee2af22244 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 2 Sep 2020 18:53:58 +0200 Subject: Adding change log for #12765. --- .../03-notations/12765-master+partial-app-in-recursive-notation.rst | 4 ++++ 1 file changed, 4 insertions(+) create mode 100644 doc/changelog/03-notations/12765-master+partial-app-in-recursive-notation.rst 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 `_, + by Hugo Herbelin). -- cgit v1.2.3 From 18269746e59a5f7a698a68d31635e2b81facf2ab Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 28 Oct 2020 20:50:12 +0100 Subject: Ref. man.: showing the x ⪯ y ⪯ .. ⪯ z ⪯ t example of recursive notation. --- doc/sphinx/user-extensions/syntax-extensions.rst | 27 ++++++++++++++++++++---- 1 file changed, 23 insertions(+), 4 deletions(-) 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 `. +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 `. .. _RecursiveNotationsWithBinders: -- cgit v1.2.3