Clarifying the logic of levels in custom and constr entry rules

[herbelin]

Kind: cleanup + small enhancements

Note: This PR was originally to fix #13018 and #12775 but those were finally fixed by #13073. This PR is thus now about small enhancements and a more principled code. The header has been updated.

Synchronous overlay for elpi at LPCIC/coq-elpi#184

• We introduce a type notation_subentry_level to preserve more informations about the subentries: we remember whether we are at any level, at the next level or at the self level.

• We take into account option Printing Parentheses in custom entries

• We provide a more principled fix to custom entry without explicit level prints as constr instead #13018 and Parens not printing right in custom grammar #12775 which subsumes the quicker fix done in A temporary fix of #13018 and #12775 for branch 8.12 (bis) #13073 (the loss of the any level information was the cause of the bug; A temporary fix of #13018 and #12775 for branch 8.12 (bis) #13073 hackily fixed it by using max_int as the default possible highest level in a custom entry)

• We warn about coercions not used for printing

• Added / updated test-suite

• Documented API change

[LasseBlaauwbroek]

I just ran into the same issue as #13018. I tested your branch, but it seems that there has been a regression. The following prints nicely in 8.12, but does not in master and this branch:

Declare Custom Entry S.
Notation "[ x ]" := x (x custom S at level 0).
Notation "[ x # .. # y ]" := (plus x .. (plus y 0) ..)
  (in custom S at level 0, x constr, y constr).

Check [[1 # 2 # 3 # 4]].
(* v8.12: [[1# 2# 3# 4]]
  master: 1 + (2 + (3 + [[4]])) *)

And now that I am here, there is another printing problem (let me know if I should open a separate issue):

Declare Custom Entry S.

Notation "[ x ]" := x (x custom S at level 0).
Notation "# x" := (id x) (in custom S at level 0, x bigint).
Notation "& x" := (id x) (in custom S at level 0, x global).

Check [# 4]. (* [& 4] *)
Check [& I]. (* [& I] *)

Two problems here:

• Note that I have to wrap variables in id. This is needed because otherwise, Coq won't print them. This seems unnecessary in a custom entry.
• When printing, Coq is not checking that a variable in a notation has the correct entry. Therefore, [# 4] gets printed as [& 4], which is not parsable.

[herbelin]

I'd bet you're using CoqIDE! The first problem is related to option Printing Parentheses being on by default, thus bypassing the use of the recursive notation. See #13067 for a fix.

The second issue is known: there is no support for bigint and numeral simultaneously, sorry (this should eventually be addressed by #11561).

Thanks for your feedback.

[LasseBlaauwbroek]

Ah, I see, that explains it. I'll change my settings. Thanks.

[ejgallego]

cc @maximedenes as I understand he's familiar with the code.

Would be good not to delay this a bit as otherwise 8.12 will have the fix but not master.

[herbelin]

I updated the title and the header to adjust to the new status of this PR. It is now going out of the list of PRs suspended for a while, that were needing an update and an extra rebase.

[SkySkimmer]

IIUC this is just missing review/assignee.
@maximedenes if you have more time now can you self-assign again?

[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.

[herbelin]

Reopened in #17117.