Notation wish #17845: add support for notations with recursive binders involving "let" and "match" #17856
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
herbelin
added
part: notations
coqbot-app
bot
added
the
needs: full CI
herbelin
added a commit
to herbelin/github-coq
that referenced
this pull request
Jul 14, 2023
herbelin
added
the
request: full CI
herbelin
added a commit
to herbelin/github-coq
that referenced
this pull request
Jul 14, 2023
herbelin
force-pushed
the
master+more-general-form-binders-recursive-notation
branch
from
f831d98
to
80165fa
Compare
coqbot-app
bot
removed
request: full CI
herbelin
added
the
request: full CI
herbelin
added a commit
to herbelin/github-coq
that referenced
this pull request
Jul 16, 2023
herbelin
force-pushed
the
master+more-general-form-binders-recursive-notation
branch
from
80165fa
to
89481c2
Compare
coqbot-app
bot
removed
the
request: full CI
herbelin
added a commit
to herbelin/github-coq
that referenced
this pull request
Jul 17, 2023
herbelin
force-pushed
the
master+more-general-form-binders-recursive-notation
branch
from
89481c2
to
6ce2427
Compare
coqbot-app
bot
added
the
needs: full CI
|
I would say that even if printing does not work symmetrically due to the difficult-to-control interaction with pattern-matching decompilation, I think that this is worth to go. Note: I added a word on the changelog to say that the support is for parsing ("not for printing" implicitly implied). Not rerunning full ci though, as it is already green. |
herbelin
added a commit
to herbelin/github-coq
that referenced
this pull request
Aug 5, 2023
herbelin
force-pushed
the
master+more-general-form-binders-recursive-notation
branch
from
6ce2427
to
f7b49b9
Compare
|
@coqbot run full ci |
coqbot-app
bot
removed
the
needs: full CI
proux01
approved these changes
Nov 3, 2023
|
Rerunning CI just to be safe before merging. @coqbot run full ci |
|
The job library:ci-fiat_crypto_legacy has failed in allow failure mode |
github-actions
bot
added
the
needs: rebase
Probably also fix a bug where the second occurrence of a same pair of recursive binders did not check that the bodies of fun/forall were the same.
Shadowing of variables not treated though (but it cannot arrive in interpretation of notations). Allow to make subst_glob_vars working on other kinds of patterns than lam and prod (such as "match" and "let").
herbelin
added a commit
to herbelin/github-coq
that referenced
this pull request
Nov 16, 2023
herbelin
force-pushed
the
master+more-general-form-binders-recursive-notation
branch
from
f7b49b9
to
16b0e80
Compare
coqbot-app
bot
added
needs: full CI
…/match. Printing notations with complex nesting of pattern-matching that includes variables for recursive binders would typically require to intertwin pattern-matching decompilation with search for notations.
proux01
force-pushed
the
master+more-general-form-binders-recursive-notation
branch
from
16b0e80
to
732a038
Compare
|
@herbelin sorry it appears I completely forget that one. Fixed the compilation issue do tu my delay. |
|
@coqbot run full ci |
coqbot-app
bot
removed
the
needs: full CI
|
@coqbot merge now |
|
@herbelin sorry again for the delay here, I apparently just forgot to merge, feel free to "harass" me in such cases. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This seems to work for parsing.
Recognizing instances of the recursive pattern of the notations for printing is more aleatory: it interacts with pattern-matching decompilation (done earlier in detyping) in ways difficult to control.
Fixes #17845