Use levels for associativity in refman

[ia0]

This PR changes how SELF on the left of a rule is rendered in the refman.

Before #21071, it was unconditionally rendered as NEXT. After #21071, it was unconditionally rendered as SELF. With this PR, the associativity of the level is taken into account. See examples below.

This PR does not change how SELF on the right of a rule is rendered, since it already takes the associativity of the level into account.

For example SELF op SELF is rendered as (where SELF is rendered as foo4 and NEXT as foo3):

Associativity	Before #21071	After #21071	With this PR
Left	foo3 op foo3	foo4 op foo3	foo4 op foo3
Right	foo3 op foo4	foo4 op foo4	foo3 op foo4
None	foo3 op foo3	foo4 op foo3	foo3 op foo3

Note that the refman currently (V9.1.0) renders like before #21071. So for users, the effective change is from before #21071 to this PR skipping the intermediate step. This means that only the rendering of left-associative rules is changed from foo3 op foo3 to foo4 op foo3 (which affects very few rules, essentially ltac_expr + ltac_expr and ltac_expr || ltac_expr for Ltac1 and a few others for Ltac2). Most users probably never noticed this very minor issue, so it is probably not worth a change log entry. But I'm happy to add one if needed.

Follows #21126. Reverts #21071. Fixes #21029 and #21072.

[ia0]

We can now see from the levels that ; is left-associative and + is right-associative:

[jfehrle]

Please provide a useful succinct description for the PR that explains concretely what is being changed. The PRs you link to are too verbose and rambling for a reviewer to quickly grasp what the change does.

[jfehrle]

Also, how about a change log entry? Users may want to know that the documented grammar has been corrected (maybe).

[ia0]

I've edited the description. Not sure it's worth a log entry.

[proux01]

No need for a changelog entry, docgram is an internal tool.
I'll merge by the end of next week if there are no more comments.

[jfehrle]

one has to also add production rules like foo4 := foo3 for each level. Those are omitted in the refman

They are included in the reference manual when the level is not empty. Look at the grammar for term or, above, ltac_expr.

You could add nonterminals for all the empty levels. It would add some clutter. Including SELF or NEXT in the doc would be a mistake, would make it harder to read.

[ia0]

They are included in the reference manual when the level is not empty. Look at the grammar for term or, above, ltac_expr.

Can you provide a link? I don't see this. Maybe you're referring to foo := fooN which defines the lowest precedence.

If it were the case it would be quite illogical. The foo4 := foo3 should be implicit by the definition of precedence. Otherwise there's no precedence. Doing it half of the time is even worse.

[jfehrle]

Can you provide a link? I don't see this.

https://rocq-prover.org/doc/V9.1.0/refman/language/core/basic.html#grammar-token-term

#21360 (comment)

200, 99, 90, 8 and 1 are not currently shown for term because they're empty levels. Shouldn't be too hard to show all the levels in the doc:

  (* g_constr.mlg *)
  term:
    [ "200" RIGHTA [ ]
    | "100" RIGHTA ...
    | "99" RIGHTA [ ]
    | "90" RIGHTA [ ]
    | "10" LEFTA ...
    | "9" ...
    | "8" [ ]
    | "1" LEFTA ...
    | "0" ...

If you're a reader trying to understand the syntax, the empty levels are often irrelevant. If you're defining a notation, you do want to know them. So it does seem we should show the empty levels that appear in the mlg.

My recollection is that all levels have to be defined in the initial mlg definition of the nonterminal definition, e.g. you can't add "97" as a level for term anywhere else. Is that still true?

[SkySkimmer]

200 is used as the highest level and 8 is used for "constr" but IDK why we declare 99 and 90 in the mlg.

My recollection is that all levels have to be defined in the initial mlg definition of the nonterminal definition, e.g. you can't add "97" as a level for term anywhere else. Is that still true?

It's never been true AFAIK

[jfehrle]

It may allow defining new levels but IINM the productions won't be processed appear in the order you expect. You do know that the following is accepted in the mlg (just tried it)? Precedence isn't limited to numeric values, nor do they have to appear in numeric order in the mlg. My recollection is that extensions can match existing labels but new labels won't be inserted where you expect. I think "NEXT" is relative to the order in which the productions appear, rather than by ordering on the precedence string. But it's been several years since I looked at these details, I may be confused.

    | "1" ...
    | "QQ" [ ]
    | "1000" []
    | "0" ...

[SkySkimmer]

There's some AFTER / BEFORE syntax to insert levels where desired

[ia0]

https://rocq-prover.org/doc/V9.1.0/refman/language/core/basic.html#grammar-token-term

Thanks! I misread the "not empty" as "empty" and only searched for exact "foo4 := foo3" patterns... 😅

So indeed, the refman already takes the approach of elaborating precedence as new non-terminals. So it would be weird to talk about term99 without making explicit somewhere (either in English or in grammar syntax) that foo[n] := foo[n-1] for all foo and n, even those that are never referenced.

Other alternatives to the next(term100) would be term<100 or term100-1. Possibly even writing term≤100 for term100 for consistency, but then you need sharp eyes to distinguish the associativity in the following:

• ltac_expr≤4 ; ltac_expr<4 versus ltac_expr4 ; ltac_expr3 or ltac_expr4 ; ltac_expr4-1
• ltac_expr<2 + ltac_expr≤2 versus ltac_expr1 + ltac_expr2 or ltac_expr<2 + ltac_expr2

But this problem is anyway not specific to NEXT on the left. We already have it with NEXT on the right. It's a problem with NEXT. That should be handled in a different PR.

[jfehrle]

it would be weird to talk about term99 without making explicit somewhere (either in English or in grammar syntax) that foo[n] := foo[n-1] for all foo and n, even those that are never referenced.

It should be done in English in one place in the manual, not in the grammar syntax. We should keep the most common use case (readers trying to understand basic syntax) simple using a familiar way of showing grammars. term<100 or term100-1 or term≤100 are all repellent. I believe the current code includes term99 if it appears on the RHS of a production.

foo[n] := foo[n-1] for all foo and n

I believe that's only true by convention in assigning labels and ordering productions (see my comment just above).

[jfehrle]

That should be handled in a different PR.

It would be less confusing if these various changes were in a single PR rather than, what is it now, 3 or 4 PRs. They're quite technical and the overall change visible to users is what counts.

[ia0]

It should be done in English in one place in the manual, not in the grammar syntax.

I would also prefer this.

I believe the current code includes term99 if it appears on the RHS of a production.

grep -r term99 _build/default/doc/refman-html doesn't give any result.

I believe that's only true by convention in assigning labels and ordering productions (see my comment just above).

Yes, but this is what Rocq exposes to users. The fact that Gramlib uses an ordered list of strings is an implementation detail that doesn't show to users (at least until #21244 where level 1l has been introduced in ltac_expr 😢 ).

It would be less confusing if these various changes were in a single PR rather than, what is it now, 3 or 4 PRs.

I agree, but #21071 was rushed, so now it's too late to have a proper self-contained PR. And I believe some discussions regarding these questions (like whether associativity should be a rule thing instead of a level thing) won't be resolved in a matter of weeks or even months, so it would not be reasonable to delay simple fixes for the sake of major changes.

[jfehrle]

I believe the current code includes term99 if it appears on the RHS of a production.

grep -r term99 _build/default/doc/refman-html doesn't give any result.

I think you're being too hasty. That indicates that term99 doesn't appear anywhere in the document (RHS or LHS).

[ia0]

I think you're being too hasty. That indicates that term99 doesn't appear anywhere in the document (RHS or LHS).

Ah you didn't mean in the refman. Indeed, there's a term99 which contains the rule term98 -> term200 in Print Grammar. Also, term99 is indeed used in casts. I don't know why docgram rewrites it to term10. There's actually a common edit to rewrite term99 <: term200 into term99 <: type, which I guess triggers, but then term99 is converted into term10 somewhere else.

So it seems like docgram is already considering NEXT at level 100 of term to be term99, since the grammar says SELF <: LEVEL 200 at level 100 right-associative, so the SELF means NEXT. So it seems like the intent is there in docgram to do right (use foo3 for NEXT at level 4 of foo), but there's probably a bug that overwrites this.

[ia0]

but then term99 is converted into term10 somewhere else

Here, where we ask to SPLICE term99. I guess I can remove it and see what happens.

[ia0]

Ok, I've pushed a commit that fixes this term99 issue. I also fixed the English text because that's not automatic.

[jfehrle]

Ah you didn't mean in the refman.

I did mean in the refman.

Focus on what users should see in the manual first, not on how it happens. It feels like you're rushing to complete something tonight. Maybe take a break until tomorrow.

[ia0]

I did mean in the refman.

Then my grep was about the refman. There is no occurrence of term99 in the refman. My last commit adds it back.

Focus on what users should see in the manual first

That's exactly what this PR is doing, but not for everything. This PR makes users see associativity using levels (in particular left-associativity). Not all issues in the refman must be fixed in this PR.

It feels like you're rushing to complete something tonight.

No. But I'm making sure this gets merged before the next release of the refman. Otherwise #21071 will get visible to users which is pretty bad. Both #21071 and this PR should be in the same refman diff visible to users.

[ia0]

Not splicing term99 means we now get such an "empty" level:

(This level is only used by a reserved notation in the prelude for the arrow.)

We can't get rid of term99 := term10 otherwise we can't talk about @term99 since it wouldn't reference anything. That's not ideal but at least correct and understandable.

[proux01]

Sorry, I was busy in December and kinda forgot this PR. Apparently, we still don't have a definitive answer on how the extensible grammar should be rendered int the refman, but since this is an improvement over the current situation, let's merge.

[proux01]

@coqbot merge now