Deactivate gramlib (camlp5) automatic right associativity fallback

[herbelin]

Kind: towards compliance to specification

Depends on #12743

The purpose of this PR is to experiment with a use of camlp5 which follows more closely its specification, i.e. which does not allow right associativity when it is not explicitly asked to do so. (I believe that it is saner and lead to easier to explain semantics.)

At the current stage, the purpose is to observe the effect on CI.

Unfortunately, I'm not able to find an example of notation whose semantics would be changed. I guess this is due to the other heuristics "recover" of camlp5. (There are however failures with GRAMMAR EXTEND, see #12743, but I don't understand why "recover" does not apply to them.)

An example which should fail but does not:

Notation "--- y" := (y+0) (at level 33, left associativity).   
Check fun z => --- --- z. 
(* --- (--- z) *)

An example which is interpreted in contradiction with its specification:

Notation "x +++ y" := (x+y) (at level 33, left associativity). 
Notation "--- y" := (y+0) (at level 33).   
Check fun y z => --- --- y +++ z. 
(* "--- (--- y +++ z)", that is "--- ((--- y) +++ z)", should be a failure *)

• Added / updated test-suite (find a failing test)
• No documentation needed a priori since it is about complying to the specification
• Entry added in the changelog (tell that extra RIGHTA/RIGHT ASSOCIATIVITY may be needed - see Adding support for recursive blocs and associativity in ARGUMENT EXTEND #12743)

[coqbot]

For your complete information, the job build:quick in allow failure mode has failed for commit 3c82463: Getting rid of an "optimization" of camlp5 which does not respect non-rightA.

[coqbot]

For your complete information, the job test-suite:4.11+trunk+dune in allow failure mode has failed for commit 3c82463: Getting rid of an "optimization" of camlp5 which does not respect non-rightA.

[coqbot]

For your complete information, the job build:base+async in allow failure mode has failed for commit 3c82463: Getting rid of an "optimization" of camlp5 which does not respect non-rightA.

[coqbot]

For your complete information, the job library:ci-fiat_crypto_legacy in allow failure mode has failed for commit 7cd85a4: Allow ARGUMENT EXTEND grammar to be printed with Print Grammar.
ping @JasonGross

[coqbot]

For your complete information, the job test-suite:base+async in allow failure mode has failed for commit 7cd85a4: Allow ARGUMENT EXTEND grammar to be printed with Print Grammar.

[coqbot]

For your complete information, the job test-suite:4.11+trunk+dune in allow failure mode has failed for commit 7cd85a4: Allow ARGUMENT EXTEND grammar to be printed with Print Grammar.

[jfehrle]

A couple thoughts:

• If --- and +++ are both at level 33, then parsing is ambiguous, right? If they're at different levels and they don't parse as expected, that would be interesting.
• I'm not entirely convinced that --- --- y +++ z gives the parse you suggest. It may be completely clear to you since you've worked on the parsing and printing so much. Showing output for an example that computes an integer expression would be more persuasive, akin to parsing 1+2*3 is 7 (correct) vs 9.

[herbelin]

If --- and +++ are both at level 33, then parsing is ambiguous, right? If they're at different levels and they don't parse as expected, that would be interesting.

No, no, I don't think so. If they have the same associativity, it is ok to have several infix/misfix at the same level, in the sense that there is only one possible interpretation which satisfies the required associativity.

I'm not entirely convinced that --- --- y +++ z gives the parse you suggest. It may be completely clear to you since you've worked on the parsing and printing so much. Showing output for an example that computes an integer expression would be more persuasive, akin to parsing 1+2*3 is 7 (correct) vs 9.

Here is an example with integers:

Notation "x +++ y" := (x+y) (at level 33, left associativity). 
Notation "--- y" := (y*10) (at level 33).   
Eval compute in --- --- 2 +++ 3. 
(* 230 *)

Now, there are a lot of failures, which let me think that it would better to compensate the change with au automatic setting of notations without specified associativity to a right associativity.

Also, if you are interested, we may have a call on how camlp5 works and about what would be worth to make evolve.

[jfehrle]

Someone who's not an expert could expect --- --- y +++ z to parse as --- --- (y +++ z) or as (--- --- y) +++ z. We could define a standard behavior for this case, but then it should be clearly documented. We don't have a lot of detail on the level mechanism. Or we could complain about it since could be confused even if it's in the manual.

towards compliance to specification

The Camlp5 specification?? Can you provide the reference?

Also, if you are interested, we may have a call on how camlp5 works and about what would be worth to make evolve.

Sure. I'd be interested to hear your thoughts. Please pick a time between 9AM and 11 PM PDT are workable for me (= 6 PM to 8 AM Paris time) and let me know.

[herbelin]

Someone who's not an expert could expect --- --- y +++ z to parse as --- --- (y +++ z) or as (--- --- y) +++ z.

Then, what parsing trees would you think are reasonable for x +++ y +++ --- ---- z +++ t +++ u?

towards compliance to specification

The Camlp5 specification?? Can you provide the reference?

I meant compliance to the expected associativity, i.e. than when you write no associativity, it is really no associativity and when you when you write left associativity, it is really only left associativity.

If you look at the camlp5 manual though, it is explicitly written page 54 that "There is no behaviour difference between left and non associative, because, in case of syntax error, the systemattempts to recover the error by applying the ”continue” function of the previous symbol (if this symbol isa call to an entry)." But I don't want to rely on this recovery behavior which precisely breaks associativity as the --- ((--- y) +++ z)) shows.

Also, if you are interested, we may have a call on how camlp5 works and about what would be worth to make evolve.

Sure. I'd be interested to hear your thoughts. Please pick a time between 9AM and 11 PM PDT are workable for me (= 6 PM to 8 AM Paris time) and let me know.

Then, if you can join, I'll be tonight at 8 PM Paris / 11 AM PDT on jch . irif . fr : 8081 / group / coq (https).

[jfehrle]

Then, what parsing trees would you think are reasonable for x +++ y +++ --- ---- z +++ t +++ u?

My natural guesses would be ``x +++ y +++ (--- --- z) +++ t +++ uorx +++ y +++ --- ---- (z +++ t +++ u)`

I meant compliance to the expected associativity, i.e. than when you write no associativity, it is really no associativity and when you when you write left associativity, it is really only left associativity.

I think of associativity the same way yacc does:

"The associativity of an operator op determines how repeated uses of the operator nest: whether ‘x op y op z’ is parsed by grouping x with y first or by grouping y with z first. %left specifies left-associativity (grouping x with y first) and %right specifies right-associativity (grouping y with z first). %nonassoc specifies no associativity, which means that ‘x op y op z’ is considered a syntax error."

Then, if you can join, I'll be tonight at 8 PM Paris / 11 AM PDT on jch . irif . fr : 8081 / group / coq (https).

I just saw your message a few minutes ago. Perhaps we can try for the same time tomorrow?

[herbelin]

Then, what parsing trees would you think are reasonable for x +++ y +++ --- ---- z +++ t +++ u?

My natural guesses would be ``x +++ y +++ (--- --- z) +++ t +++ uorx +++ y +++ --- ---- (z +++ t +++ u)`

But you did not put all parentheses...

I meant compliance to the expected associativity, i.e. than when you write no associativity, it is really no associativity and when you when you write left associativity, it is really only left associativity.

I think of associativity the same way yacc does:

"The associativity of an operator op determines how repeated uses of the operator nest: whether ‘x op y op z’ is parsed by grouping x with y first or by grouping y with z first. %left specifies left-associativity (grouping x with y first) and %right specifies right-associativity (grouping y with z first). %nonassoc specifies no associativity, which means that ‘x op y op z’ is considered a syntax error."

I think it the same but camlp5 is a bit more tolerant... (which it should not I think).

Then, if you can join, I'll be tonight at 8 PM Paris / 11 AM PDT on jch . irif . fr : 8081 / group / coq (https).

I just saw your message a few minutes ago. Perhaps we can try for the same time tomorrow?

Tomorrow will not be possible. Thursday or Friday should be possible. Tonight for about 30 minutes is also possible.

[jfehrle]

I forgot to respond to this after our phone call:

Then, what parsing trees would you think are reasonable for x +++ y +++ --- ---- z +++ t +++ u?

My natural guesses would be ``x +++ y +++ (--- --- z) +++ t +++ uorx +++ y +++ --- ---- (z +++ t +++ u)`

But you did not put all parentheses...

I meant one of these:

• ((((x +++ y) +++ (--- (--- z))) +++ t) +++ u) or
• ((x +++ y) +++ (--- (--- ((z +++ t) +++ u)))).

But I might want to include parentheses myself depending on how often I use +++ and ---.

I think of associativity the same way yacc does:
"The associativity of an operator op determines how repeated uses of the operator nest: whether ‘x op y op z’ is parsed by grouping x with y first or by grouping y with z first. %left specifies left-associativity (grouping x with y first) and %right specifies right-associativity (grouping y with z first). %nonassoc specifies no associativity, which means that ‘x op y op z’ is considered a syntax error."

I think it the same but camlp5 is a bit more tolerant... (which it should not I think).

Sounds reasonable. But would the benefit justify the compatibility impact on users? I think it would likely break proofs and it may not be obvious that this change is the underlying cause.

[coqbot-app]

The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.

[coqbot-app]

This PR was not rebased after 30 days despite the warning, it is now closed.