doc_grammar should also use levels for left-associativity

[ia0]

Camlp5 simulates left-associativity using a "recovery" mechanism. This is an implementation detail that leaks to the user documentation.

For example, the rule for Ltac sequence (which is left-associative and at level 4 in ltac_expr) should ideally be documented as:

ltac_expr4 ::= ltac_expr4 ; ltac_expr3

In Camlp5, it is implemented as (slightly abusing notations for the parallel):

ltac_expr "4" LEFTA ::= SELF ";" SELF

This has to be understood as:

ltac_expr "4" LEFTA ::= SELF ";" NEXT

But is effectively:

ltac_expr "4" LEFTA ::= NEXT ";" NEXT

It relies on the recovery mechanism to behave like SELF ";" NEXT.

Currently, this is rendered to the user as ltac_expr3 ; ltac_expr3 without explaining the recovery mechanism (there's only a pointer in the documentation of Print Grammar). As written, Ltac sequence should be non-associative, which is incorrect.

This issue is meant to discuss and (if applicable) track the effort of having doc_grammar hide the recovery mechanism (which is a Camlp5 implementation detail) by generating rules with the correct associativity using levels.

Related issues:

• Remaining tasks after the completion of the effort to get the refman checked by doc_grammar. #16652
• Roadmap to improve the documentation of tactics. #8946
• About associativity in camlp5/gramlib: absence of support of no-associativity + ability to mix different associativities in the same level #17859

[proux01]

@ia0 note that we are in the process of getting rid of the recovery mechanism: #17876

[SkySkimmer]

Currently, this is rendered to the user as ltac_expr3 ; ltac_expr3

That's not what I see https://rocq-prover.org/doc/master/refman/proof-engine/ltac.html#syntax

I also don't see where you got that associativity is related to recovery.

[ia0]

That's not what I see https://rocq-prover.org/doc/master/refman/proof-engine/ltac.html#syntax

That's because I point-fixed it in #21025 linked above. But I don't believe this is the correct approach. I believe doc_grammar should do this automatically. That's why I created this issue.

I also don't see where you got that associativity is related to recovery.

From the source of truth which I linked in the original post, namely:

There is no behaviour difference between left and non associative, because, in case of syntax error, the system attempts to recover the error by applying the "continue" function of the previous symbol (if this symbol is a call to an entry).

That said I agree the issue title is not specific enough since right-associativity works fine. Let me update that.

Right now, doc_grammar renders non-associative and left-associative rules the same: as non-associative, because that's how they are implemented where SELF ... SELF means NEXT ... NEXT.

This should probably be coordinated with any effort to have non-associative rules (as Pierre mentioned that there is an effort to disable the recovery mechanism to support such rules), since those should continue to be rendered as non-associative.

[SkySkimmer]

From the source of truth which I linked in the original post, namely:

I think that's saying that non-associativity is turned into left-associativity by the recovery, it doesn't mean that recovery is involved in normal left-associativity.

Right now, doc_grammar renders non-associative and left-associative rules the same: as non-associative, because that's how they are implemented where SELF ... SELF means NEXT ... NEXT.

That's not true though, SELF on the left means the current level not the next level. It seems like just a doc_grammar bug.

[proux01]

Currently non-associative is indeed a lie, it essentially doesn't exist.
As to how doc_grammar should display associativity, that's an interesting question. Maybe it could display the associativity of its level along rules where it matters (with SELF on the left).
I'd like to rework the notation system (c.f. rocq-prover/rfcs#106 ) if we aren't in a hurry, maybe it'd be better to wait for it (will likely take months though).

[SkySkimmer]

#21071

[ia0]

It seems like just a doc_grammar bug.

Sounds good to me to call this a bug rather than a feature request.

I'd like to rework the notation system (c.f. rocq-prover/rfcs#106 ) if we aren't in a hurry, maybe it'd be better to wait for it (will likely take months though).

Ideally we would stop using levels for associativity and use SELF/NEXT directly. That was one of the question in #17859 namely mixing associativity within the same level.

EDIT: But for that we would need to control the recovery mechanism to only trigger in cases where the continuation function of a SELF at the beginning of a production rule is called (since that SELF will be a NEXT in practice but we really want it to be a SELF).

[ia0]

As to how doc_grammar should display associativity, that's an interesting question. Maybe it could display the associativity of its level along rules where it matters (with SELF on the left).

I've given an example of this in #21025 (comment). I don't think it will serve the users. I think the grammar in the documentation should use the usual notations, not Camlp5 encodings. That means:

• foo2 := foo2 op foo1 is left-associative
• foo2 := foo1 op foo2 is right-associative
• foo2 := foo1 op foo1 is non-associative
• foo2 := foo2 op foo2 is ambiguous and should be rejected
• There's no recovery mechanism.

Currently Camlp5 is only mentioned for the syntax extensions in Print Grammar in particular. If we want the whole documentation to use Camlp5 encodings (which I don't think we want), then talking about Camlp5 should come much earlier.

That's not true though, SELF on the left means the current level not the next level.

Then we should update the documentation:

rocq/doc/sphinx/user-extensions/syntax-extensions.rst

Line 784 in 3541a83

- At the beginning of a production, `SELF` means the next level. In the

(Please don't, the documentation is actually correct, but I agree it can be confusing.)