[abbreviation] user syntax to set interp scope of argument

[gares]

Turn the error about an inconsistent inference of scopes into a warning.
We enable Notation abbr X Y Z := t (X, Z in scope foo_scope) to force a scope and silence the warning.

Internally Abbreviations and Notations accept the same modifiers, but "in scope" is for now only supported by Abbreviations. At the grammar level I've shared the whole syntax of modifiers, even if abbreviations only support "in scope" and "only parsing" (only parsing was duplicate). It seems the right thing to do if we consider supporting "in scope" also in regular Notations, or conversely any other modifier on Abbreviations.

Overlay PRs:
rocq-community/paramcoq#65
mattam82/Coq-Equations#355
LPCIC/coq-elpi#224

Fix #13957

[coqbot-app]

The job library:ci-fiat_crypto_legacy has failed in allow failure mode
ping @JasonGross

[gares]

OK, I think it is ready for review. I'm not very happy with my first commit, the old code was a spaghetti of control flow, but it is not the case that the new one is much better.

[herbelin]

No strong opinion. The syntax Notation abbr X%foo := ... looks rather intuitive and I'd be rather happy to have this feature. Don't know if others have more to comment.

No strong opinion either on what to do in the presence of a clash, but if a warning, it should tell which is finally chosen.

One could wonder what to do with Notation "..." then?

Notation "2⨉ y%nat" := (Nat.add y y).

or

Notation "2⨉ y" := (Nat.add y y) (y in scope nat_scope).

The former may (rarely?) break existing notations? The latter would suggest that the syntax for Notation abbr should also be:

Notation abbr X := ... (X in scope foo_scope).

Both are ok to me, but it is might be worth to anticipate a consistency.

[gares]

Notation abbr X := ... (X in scope foo_scope).

This is a good suggestion, I may give it a try.

What about:

[ ] decide what to do when scopes are inconsistent, right now we keep the one we found first

I don't know enough scopes to know if other options are reasonable, eg concatenating the lists

[herbelin]

[ ] decide what to do when scopes are inconsistent, right now we keep the one we found first

I don't know enough scopes to know if other options are reasonable, eg concatenating the lists

Since a list is ordered, there would still be an arbitrariness when the notation exists in both scopes, however, concatenating the lists could indeed be done. Some work would be needed too, because there is currently an optional "temporary" scope and it would have to be changed everywhere in constrintern.ml and constrextern.ml to a list of "temporary" scopes.

[gares]

Oh, I see, then it seems too hard. I'll just fix the warning message to spell out which scope is finally chosen.

[gares]

done. I've adopted the syntax you proposed and shared it with standard notations (that for now don't support it)

[gares]

@herbelin I did change the parser so that both notations and syndefs accepts all modifiers, then syndefs only really accept two and notations don't implement yet "in scope" (but you seemed to like the idea, so I paved the way for this).

At the grammar level, this means that both commands parse a superset of the options they really accept, the error comes later.

[jfehrle]

Let me know if you have questions about using make doc_gram_rsts.

[jashug]

The examples look good, and I think the feature moves in the right direction. For the future, there are probably questions about how to set multiple scopes on an argument. I didn't review the code; herbelin is the expert here.

[gares]

Anyone taking care of this PR?

[ppedrot]

@gares this needs a rebase

[gares]

done

[ppedrot]

Merging soon then.

[herbelin]

Even if the decision is to no change, if I could get an answer to my comment above just to be sure that it has been seen, that'll be nice.

[gares]

You are right, I did forget to implement the empty scope syntax.
I did open #14134 .
I think it is better to merge this one, which has overlays, ASAP, and leave #14134 as a bonus. (I don't have much time these days)

[ppedrot]

@herbelin is that fine with you?

[herbelin]

@ppedrot: Yes.

outdated