Ltac2 precedence of field access is not consistent with Gallina

[JasonGross]

Description of the problem

In Gallina, foo bar.(baz) means foo (bar.(baz)). In Ltac2, it seems to mean (foo bar).(baz).

Coq Version

8.15

[JasonGross]

Test case:

Require Import Ltac2.Ltac2.
Set Implicit Arguments.
Record ref a := { contents : a }.
Ltac2 Type 'a ref := { mutable contents : 'a }.
Check fun (f : nat -> nat) (x : ref nat) => f (x.(contents)).
Ltac2 Eval fun (f : int -> int) (x : int ref) => f (x.(contents)).
Fail Check fun (f : nat -> nat) (x : ref nat) => (f x).(contents).
Fail Ltac2 Eval fun (f : int -> int) (x : int ref) => (f x).(contents).
Check fun (f : nat -> nat) (x : ref nat) => f x.(contents).
Ltac2 Eval fun (f : int -> int) (x : int ref) => f x.(contents).
(* fails with Error: This expression has type int ref but an expression was expected of type int *)

[SkySkimmer]

I don't understand the parser level stuff, @ppedrot can you handle this?

[samuelgruetter]

It seems that function application and projection both are at level 1:

ltac2_expr1 ::= ltac2_expr0 ltac2_expr0^+
            |   ltac2_expr0 .( qualid )
            |   ltac2_expr0 .( qualid ) := ltac2_expr5
            |   ltac2_expr0

This seems undesirable: The level of projection should be a strictly smaller number than the level of application. But Ltac2 uses only a small number of densely populated levels, unlike Gallina, so there are no unused levels around level 1. But at least, level 4 is unused. So one fix might be: level 3 becomes level 4, level 2 becomes level 3, and then, level 2 can be used for application, and level 1 can be used for projection.

But it seems that there's another problem: Currently, at level 1, there's projection as well as updating a projection. And I guess (??) this is intended because otherwise the grammar factorization magic can't automatically implement the lookahead that's needed to disambiguate between projection and updating a projection.

So we might have the following set of unsatisfiable constraints:

• level of projection < level of application (to fix the current issue)
• level of application <= level of updating a projection (otherwise f x.(field) := val, which should be rejected, is parsed as f (x.(field) := val))
• level of updating a projection = level of projection (otherwise, can't disambiguate between projection and updating a projection)

Is the situation that bad? I'd hope my analysis is wrong and @ppedrot or someone else knows how to fix this...