ListNotations breaks primitive array syntax

[JasonGross]

Description of the problem

From Coq Require Import Uint63 List PArray.
Open Scope uint63_scope.
Open Scope list_scope.
Check [| 1; 2 | 0 : int |].
Import ListNotations.
Check [| 1; 2 | 0 : int |]. (* Error: Syntax error: [term level 200] expected after '[' (in [term]). *)

cc @coq/parsing-maintainers

Coq Version

8.17

[Blaisorblade]

There's also discussion in https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Notation.20for.20Explicit.20Arrays/near/341669885 :

We could consider that a Coq bug too but I don't know how to fix it then. (and ListNotations is well known to be troublesome, that's why it is in a module in the first place I guess)

[SkySkimmer]

The source of the problem is that we want notations that parse [ | to parse [| the same (for instance tac; [|tac']).
To do this we avoid making [| a keyword and instead we use lookahead to check that the [ is followed by | with no space in the rule for arrays. Then the notation for lists introduces something which starts with [ and the parser stops trying the array rule.
If we had different keywords depending on the grammar entry (not sure that's actually possible) we could have [| be a keyword for constr and not for ltac.
Alternatively we could try making [| a keyword and add adhoc rules for all the cases where we want to parse [| as [ | (not sure how practical that is either)

[Blaisorblade]

As the simplest option, it might be worth changing the syntax for primitive arrays, or just adding alternative options that don't conflict with lists. If you add named constructors, then people could wrap their own notations on top.

Primitive arrays are relatively young, after all.

Then the notation for lists introduces something which starts with [ and the parser stops trying the array rule.

Could the parser left-factor the two rules that start with the [ token? Could left-factoring hardcode a special case for array syntax?

If we had different keywords depending on the grammar entry (not sure that's actually possible) we could have [| be a keyword for constr and not for ltac.

AFAIK, astandard way to have grammar-dependent lexing/scanning is scannerless parsing, that is, drop the lexing and just use a parser; I'm not aware of alternatives (but I'm not a parsing specialist, I just worked with some). The main downside is that LL(1)/LR(1) doesn't suffice in general but you need at least more lookahead (in the Spoofax work from the late Eelco Visser & C, authors argue that in general you need some small extensions over CFGs — that can still be parsed wirh GLR variants); you might get away with less in specific cases (not sure).

[SkySkimmer]

Could the parser left-factor the two rules that start with the [ token? Could left-factoring hardcode a special case for array syntax?

The parser doesn't see the array rule as starting with [, it sees test_array_opening; "[" where test_array_opening is some ocaml code which does lookahead.

[Janno]

Is there a workaround for this issue? Apart from fixing the actual problem it might be worth supporting literal arrays in recursive notation so that people can define their own syntax. Something like

Notation "'[arr' x ; .. ; y | d : t ]" := [| x; .. ; y | d : t|].

could be defined before ListNotations is imported and that might be enough to work around the problem.