New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Clarifying the logic of levels in custom and constr entry rules (reopening of #13025) #17117
Clarifying the logic of levels in custom and constr entry rules (reopening of #13025) #17117
Conversation
1e916c8
to
c827679
Compare
@coqbot run full CI |
c827679
to
f696872
Compare
@coqbot run full CI |
This was ready and needing a rebase before I reopened it. @proux01, you might be the best expert for assigning! |
interp/constrexpr.ml
Outdated
type notation_entry_level = InConstrEntrySomeLevel | InCustomEntryLevel of string * entry_level | ||
|
||
(* A notation entry with the level where the notation lives *) | ||
type notation_entry_level = notation_entry * entry_level |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This would have been a good opportunity to use a record IMHO.
interp/constrexpr.ml
Outdated
type notation_entry_level = notation_entry * entry_level | ||
|
||
(* Notation subentries, to be associated to the variables of the notation *) | ||
type notation_entry_relative_level = notation_entry * (entry_relative_level * side option) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Same
| None -> raise No_match | ||
| Some coercion -> | ||
|
||
let scopes = (InConstrEntrySomeLevel, snd scopes) in | ||
let scopes = ((InConstrEntry,(LevelSome (*??*),None)), snd scopes) in |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
?
let level_of_notation ntn = | ||
if is_numeral_in_constr (decompose_notation_key ntn) then | ||
(* A primitive notation *) | ||
(fst ntn, 0, []) (* TODO: string notations*) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Would the string case be hard to complete?
This PR is now at risk of being auto-closed by the bot due to a rebase not happening. We should really be more proactive in merging intermediate cleanup PRs otherwise they just vanish. |
af26871
to
24fa443
Compare
@coqbot run full ci |
terminology already in used).
informations about the subentries: we remember whether we are at any level, at the next level or at the self level. Incidentally, we also take into account option Printing Parentheses in custom entries. This is a more principled fix to coq#12775/coq#13018 than coq#13073 (printing bugs in custom entry rules with no explicit level). Compared to "subentries", the name "entry_relative" insists on the syntactic structure of the type rather than on its semantic origin, since, after all, subentries are promoted as entries in the recursive printing loop.
24fa443
to
48b5178
Compare
We hard-wire a coercion in constr from level 0 to the top level.
48b5178
to
43bface
Compare
@coqbot run full ci |
@coqbot merge now |
@proux01: Please take care of the following overlays:
|
…tuples. See comment at coq#17117 (comment).
…tuples. See comment at coq#17117 (comment).
Kind: cleanup + small enhancements (reopening of #13025)
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.
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 entriesWe 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 usingmax_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
Change log (though it is rather anecdotical, observationally)
Synchronous overlay