Properly pass the Ltac2 notation level to the gramlib API.

[ppedrot]

For some reason I was confusing the position and the level in the previous version of the code.

I am leaving this as a draft for now since we may seize the opportunity to have a richer level language for Ltac2 notations.

Fixes #11866: Ltac2 Notations do not respect precedence.

• Added / updated test-suite
• Entry added in the changelog (see https://github.com/coq/coq/tree/master/doc/changelog#unreleased-changelog for details).

[ppedrot]

I am leaving this as a draft for now since we may seize the opportunity to have a richer level language for Ltac2 notations.

I changed my mind since we can alway introduce a backwards-compatible syntax using numbers for the built-in levels and combinators for user-defined levels. The camlp5 API actually provides something similar with the AFTER / BEFORE / FIRST / LAST / LIKE combinators so it's only a matter of exposing those constructs.

[ppedrot]

@JasonGross would you assign?

[JasonGross]

Should this error message be documented?

[ppedrot]

I have added an entry in the refman.

[JasonGross]

I can assign if you'd like me to, but I don't feel competent to review the code changes and the current test in the test-suite is not adequate to convince me that the levels are working as intended.

If you can design some test that will fail if the levels are not correctly associated, such that I no longer need to care what the code is doing, I'd be happy to take this.

Alternatively, if you want to merge it under the premise that what's going on is not worse than what was happening before, I can merge it from that perspective too.

[ppedrot]

If you can design some test that will fail if the levels are not correctly associated

Not sure how to do that. Now that we can print the Ltac2 grammar we might try to rely on an output test but it'd be very fragile.

[JasonGross]

If you can design some test that will fail if the levels are not correctly associated

Not sure how to do that. Now that we can print the Ltac2 grammar we might try to rely on an output test but it'd be very fragile.

Add some Ltac2 notations that parse into an embedded AST and check for equality. e.g.,

Ltac2 Type tree := [ Leaf | Node (tree * tree) ]
Ltac2 Notation tactic4(a) "node456" tactic6(b) : 5 := node (a, b).

or something like that, and then do stuff like Leaf node456 Leaf node456 Leaf and make sure that the tree you get is the one that you expect. Granted, this seems pretty tedious, so maybe it's worth writing a small script to write the Ltac2 for you to test all of the expected outputs.

[SkySkimmer]

You can do something with types. eg in ocaml

let f (+) x y z = (x + y) + z
(* f : ('a -> 'b -> 'a) -> 'a -> 'b -> 'b -> 'a *)
 
let f (+) x y z = x + (y + z)
(* f : ('a -> 'b -> 'b) -> 'a -> 'a -> 'b -> 'b *)

[jfehrle]

Wording suggestions

[ppedrot]

@JasonGross I am too lazy to write this kind of test when 1. it's unlikely to break again because of this API and 2. there are other Ltac2 parsing issues lurking around that were not yet observed because parsing has an explosive combinatoric flavour to it. I have added the test you suggested in the bug report, that was failing before and is now properly working. If by a very unfortunate mistake we use the wrong API again it will be caught anyways, the rest seems like we would need a complete parsing test suite for the language which is kind of unrelated to the PR.

[JasonGross]

@coqbot merge now

[coqbot-app]

@JasonGross: You can't merge the PR because you're not among the assignees.

[JasonGross]

@coqbot merge now