Skip to content
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.

Sign up for GitHub

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

Jump to bottom

More parsing/printing notation/abbreviation consistency for mixed terms and pattern #12099

Merged
merged 7 commits into from
Nov 5, 2020
Merged

More parsing/printing notation/abbreviation consistency for mixed terms and pattern #12099

merged 7 commits into from
Nov 5, 2020

Conversation

herbelin
Copy link
Member

@herbelin herbelin commented Apr 15, 2020 •
edited
Loading

Kind: bug fix / cleanup

Depends on #8808 (now merged).

This is a continuation of #8808 about mixed binders and terms in notations and abbreviations. It ensures consistency of printing and parsing for both notations and abbreviations in the different possible configurations (see test-suite file Notations4.v).

For the record, the typical application of such mixed terms and binders notations is the "maximal group such that" used in MathComp or the "forcing" modality:

Definition force n (P:nat -> Prop) := forall n', n' >= n -> P n'.
Notation "▢_ n P" := (force n (fun n => P))
   (at level 0, n ident, P at level 9, format "▢_ n  P").
Check exists p, ▢_p (p >= 1).

It does not fix the printing order issue that #9311 is trying to fix.

@herbelin herbelin requested review from a team as code owners April 15, 2020 16:53
@herbelin herbelin added kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. kind: fix This fixes a bug or incorrect documentation. needs: merge of dependency This PR depends on another PR being merged first. part: notations The notation system. labels Apr 15, 2020
@herbelin herbelin added this to the 8.12+beta1 milestone Apr 15, 2020
herbelin added a commit to herbelin/github-coq that referenced this pull request Apr 15, 2020
@herbelin
Added change log for coq#8808 and coq#12099.
fe27652
@herbelin herbelin mentioned this pull request Apr 15, 2020
Merged
2 tasks
@Zimmi48
Copy link
Member

Zimmi48 commented Apr 19, 2020

I'm turning this PR in draft mode because of the dependency. If you expect feedback from some specific groups of maintainers, please say so. With PR dependencies, try to always use the draft mechanism, otherwise the code owner mechanism is generating review spam.

@Zimmi48 Zimmi48 marked this pull request as draft April 19, 2020 11:51
@Zimmi48 Zimmi48 removed the request for review from a team April 19, 2020 11:51
@Zimmi48
Copy link
Member

Zimmi48 commented May 12, 2020

Dear PR author(s) and contributors, it seems to us this PR may need additional work beyond the 8.12 branching deadline on May 15th.

We are thus removing the 8.12+beta1 milestone; please retarget as appropriate, and also consider updating labels to reflect current status, etc.

We apologize in advance if we misunderstood the PR status.

@Zimmi48 Zimmi48 removed this from the 8.12+beta1 milestone May 12, 2020
@herbelin
Copy link
Member Author

It depends on #8808 which depends on @mattam82 who seems to have other priorities these days. I just asked @ejgallego instead.

@herbelin
Copy link
Member Author

I just found the time to rebase this PR after #8808 is merged. It is basically a refinement of #8808, see the ▢_ n P notation example.

herbelin added a commit to herbelin/github-coq that referenced this pull request Jul 12, 2020
@herbelin
Added change log for coq#12099.
d292b29
@herbelin herbelin force-pushed the master+constraining-terms-occurring-also-as-pattern-in-notations branch from fe27652 to d292b29 Compare July 12, 2020 09:00
@herbelin herbelin removed the needs: merge of dependency This PR depends on another PR being merged first. label Jul 12, 2020
@herbelin herbelin added this to the 8.13+beta1 milestone Jul 12, 2020
@herbelin herbelin marked this pull request as ready for review July 12, 2020 09:01
herbelin added a commit to herbelin/github-coq that referenced this pull request Aug 18, 2020
@herbelin
Added change log for coq#12099.
3dd380b
@herbelin herbelin force-pushed the master+constraining-terms-occurring-also-as-pattern-in-notations branch from d292b29 to 3dd380b Compare August 18, 2020 21:37
@github-actions github-actions bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Aug 25, 2020
herbelin added a commit to herbelin/github-coq that referenced this pull request Aug 30, 2020
@herbelin
Added change log for coq#12099.
f8e26c3
@herbelin herbelin force-pushed the master+constraining-terms-occurring-also-as-pattern-in-notations branch from 3dd380b to f8e26c3 Compare August 30, 2020 15:03
@coqbot-app coqbot-app bot removed the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Aug 30, 2020
@herbelin herbelin mentioned this pull request Aug 30, 2020
Closed
@herbelin
Copy link
Member Author

@ejgallego: Is it asking a lot to possibly review this PR?

@herbelin herbelin mentioned this pull request Oct 2, 2020
Open
@herbelin
Copy link
Member Author

Rebased and dependencies merged.

herbelin added a commit to herbelin/github-coq that referenced this pull request Oct 28, 2020
@herbelin
Added change log for coq#12099.
8ec6aae
@herbelin herbelin force-pushed the master+constraining-terms-occurring-also-as-pattern-in-notations branch from f8e26c3 to 8ec6aae Compare October 28, 2020 20:13
@ejgallego ejgallego self-assigned this Oct 28, 2020
@ejgallego
Copy link
Member

@herbelin I'm reviewing, sadly the CI didn't run due to the limits, please rebase and push.

herbelin added a commit to herbelin/github-coq that referenced this pull request Nov 3, 2020
@herbelin
Added change log for coq#12099.
6b8e2d7
@herbelin herbelin force-pushed the master+constraining-terms-occurring-also-as-pattern-in-notations branch from 8ec6aae to 6b8e2d7 Compare November 3, 2020 18:58
@github-actions github-actions bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Nov 5, 2020
@ejgallego
Copy link
Member

@herbelin unfortunately this got a conflict :S please rebase, and hopefully we can merge.

@herbelin
Notations: Giving a consistent role to global references occurring pa…
cb105b6 
…tterns.

Currently, global references in patterns used also as terms were
accepted for parsing but not for printing.

We accept section variables for both parsing and printing. We reject
constant and inductive types for both parsing and printing.

Among other, this also fixes a hole in interpreting variables used
both patterns and terms: the term part was not interpreted.
@herbelin
Passing full interning env to pattern interning, for better control.
4b8a87b 
This will allow for instance to check the status of a variable name
used both as a term and binder in notations.
@herbelin
Accept section variables in notations with mixed terms and binders.
c893dc5
@herbelin
Accept local variables in mixed terms and binders of notations.
8376231
@herbelin
Regression tests for the various combinations of mixed terms and bind…
eaa25fb 
…ers in notations.

This also includes tests for abbreviations.
@herbelin
Minor cut elimination in the code of constrintern.ml.
7dcd829
@herbelin
Added change log for coq#12099.
6521021
@herbelin herbelin force-pushed the master+constraining-terms-occurring-also-as-pattern-in-notations branch from 6b8e2d7 to 6521021 Compare November 5, 2020 18:09
@coqbot-app coqbot-app bot removed the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Nov 5, 2020
@herbelin
Copy link
Member Author

herbelin commented Nov 5, 2020

OK, rebased.

@ejgallego
Copy link
Member

Failure are unrelated, merging.

@coqbot: merge now

@coqbot-app
Copy link
Contributor

coqbot-app bot commented Nov 5, 2020

@ejgallego: You can't merge the PR because it hasn't been approved yet.

@ejgallego
Copy link
Member

@coqbot: merge now

@coqbot-app
Copy link
Contributor

coqbot-app bot commented Nov 5, 2020

@ejgallego: Could not find merge comment. cc @Zimmi48

@ejgallego
Copy link
Member

@coqbot: merge now (sudo)

@coqbot-app
Copy link
Contributor

coqbot-app bot commented Nov 5, 2020

@ejgallego: Could not find merge comment. cc @Zimmi48

@ejgallego ejgallego merged commit 16144a4 into coq:master Nov 5, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@ejgallego ejgallego ejgallego approved these changes

Assignees

@ejgallego ejgallego

Labels
kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. kind: fix This fixes a bug or incorrect documentation. part: notations The notation system.
Projects
None yet
Milestone
8.13+beta1
Development

Successfully merging this pull request may close these issues.
3 participants
@herbelin @Zimmi48 @ejgallego