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

Don't make Prop inductives template to control eliminator generation #18867

Merged
merged 10 commits into from
Apr 18, 2024
Merged

Don't make Prop inductives template to control eliminator generation #18867

merged 10 commits into from
Apr 18, 2024

Conversation

SkySkimmer
Copy link
Contributor

@SkySkimmer SkySkimmer commented Mar 29, 2024 •
edited
Loading

Instead we register those Prop inductives which should have dependent eliminators in a table.

Next:

  • separate the code from compute_template_inductive done
  • provide a way for users to declare explicit Prop inductives with default dependent elim (eg #[dep_elim] Inductive foo : Prop := . and/or some option)
  • stop automatically putting inductives in Prop when declared with explicit Type (with deprecation phase)

Overlays:

@SkySkimmer SkySkimmer requested review from a team as code owners March 29, 2024 16:01
@coqbot-app coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Mar 29, 2024
@SkySkimmer
Copy link
Contributor Author

@coqbot run full ci

@coqbot-app coqbot-app bot removed the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Mar 29, 2024
@SkySkimmer SkySkimmer added the needs: progress Work in progress: awaiting action from the author. label Mar 29, 2024
@SkySkimmer
Copy link
Contributor Author

separate the code from compute_template_inductive

probably should do this one in this PR, the other points can wait for followups

@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 Apr 1, 2024
@coqbot-app coqbot-app bot added needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. and removed needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. labels Apr 3, 2024
@SkySkimmer SkySkimmer added request: full CI Use this label when you want your next push to trigger a full CI. and removed needs: progress Work in progress: awaiting action from the author. labels Apr 3, 2024
@SkySkimmer SkySkimmer requested a review from a team as a code owner April 3, 2024 15:21
@coqbot-app coqbot-app bot removed request: full CI Use this label when you want your next push to trigger a full CI. needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. labels Apr 3, 2024
@SkySkimmer SkySkimmer added kind: cleanup Code removal, deprecation, refactorings, etc. part: universes The universe system. labels Apr 3, 2024
@SkySkimmer SkySkimmer added this to the 8.20+rc1 milestone Apr 3, 2024
@SkySkimmer
Copy link
Contributor Author

Should be in reasonable shape now.
Probably will need overlays.

@SkySkimmer
Don't make Prop inductives template to control eliminator generation
a2ed7a3 
Instead we register those Prop inductives which should have dependent
eliminators in a table.

Next:
- separate the code from compute_template_inductive
- provide a way for users to declare explicit Prop inductives with
  default dependent elim (eg `#[dep_elim] Inductive foo : Prop := .`
  and/or some option)
- stop automatically putting inductives in Prop when declared with
  explicit Type (with deprecation phase)
@SkySkimmer
Don't use relevance_of_sort_family in rew_fwd_dep scheme
f3f9743 
AFAICT it's only incorrect for sort poly inductives and the code is
probably broken for sort poly inductives but it's still more robust
this way.
@SkySkimmer
comInductive: evar map does not vary while computing prop candidates
aafac42 
(the candidate set is what varies)
@SkySkimmer
cleanup prop lowering computation
309f283
@SkySkimmer
Separate inductive default elim dependency from template computation
e7c7a2c 
This slightly changes behaviour: an inductive which is lowered to Prop
with explicit `#[universes(template=no)]` or auto template turned off
now has default dependent eliminators.

It is unlikely that anyone relies on this.

This also makes record syntax inductives use the default dep elim
table (although by default it's unused since records don't generate
schemes by default)

(NB univ poly inductives uses lbound=Set so never lower to Prop
(`not (check_leq evd Sorts.set s)` in `is_prop_candidate`) and so are unchanged)
@SkySkimmer
Term and EConstr.isArity don't substitute letins
38e6104 
This makes it match destArity such that `if isArity c then destArity c`
is safe.
@SkySkimmer
Don't need env_ar_params in compute_template_inductive
8edd32a 
It's only used for Reduction.dest_arity in a branch where we just
checked Term.isArity, so we can use Term.destArity instead.
@SkySkimmer
Cleanup template poly syntax restriction handling
b8e87c6 
No need to pass an optional pointer to the inferred sort (which is
incorrect when lowering to Prop) around, we just need a boolean to
tell if the syntax was the kind we allow for template poly.

This allows to get rid of special handling of prop lowering in the
auto template branch of compute_template_inductive.

This changes behaviour for records:
~~~coq
Polymorphic Definition typ := Type.

Record foo (A:Type) : typ := { x : A }.
~~~
would be made template poly and now is not.
@ppedrot ppedrot added the needs: changelog entry This should be documented in doc/changelog. label Apr 4, 2024
SkySkimmer added a commit to SkySkimmer/metacoq that referenced this pull request Apr 4, 2024
@SkySkimmer
Adapt to coq/coq#18867 (inductive_sort_family doesn't exist)
29fc39c
SkySkimmer added a commit to SkySkimmer/coq-elpi that referenced this pull request Apr 4, 2024
@SkySkimmer
Adapt to coq/coq#18867 (inductive_sort_family doesn't exist)
d84a979
SkySkimmer added a commit to SkySkimmer/coq-elpi that referenced this pull request Apr 4, 2024
@SkySkimmer
Adapt to coq/coq#18867 (cominductive returns default dep elim)
292c6ff
@SkySkimmer SkySkimmer added request: full CI Use this label when you want your next push to trigger a full CI. and removed needs: changelog entry This should be documented in doc/changelog. labels Apr 4, 2024
@coqbot-app coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 4, 2024
@SkySkimmer
Copy link
Contributor Author

ping @coq/vernac-maintainers

@ppedrot ppedrot self-assigned this Apr 18, 2024
@ppedrot
Copy link
Member

ppedrot commented Apr 18, 2024

I forgot to assign... Even though I'm not a vernac maintainer officially I think this is right in my ballpark.

@SkySkimmer
Copy link
Contributor Author

PS there has been some talk about relaxing the typing rules for template inductives so that they don't induce constraints with the default instance when fully applied (eg fun (A:Type@{u}) a => @eq A a a does not induce u <= eq.u0). This would make constant-Prop template inductives useful again but this PR should still be useful to avoid treating them specially.

ppedrot
ppedrot approved these changes Apr 18, 2024
View reviewed changes
Copy link
Member

@ppedrot ppedrot left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is a welcome cleanup that paves the way out of the template tarpit.

@ppedrot
Copy link
Member

ppedrot commented Apr 18, 2024

@coqbot merge now

@coqbot-app coqbot-app bot merged commit 7f5badd into coq:master Apr 18, 2024
6 checks passed
@coqbot-app coqbot-app
Copy link
Contributor

coqbot-app bot commented Apr 18, 2024

@ppedrot: Please take care of the following overlays:

  • 18867-SkySkimmer-non-prop-template.sh

ppedrot added a commit to MetaCoq/metacoq that referenced this pull request Apr 18, 2024
@ppedrot
Merge pull request #1073 from SkySkimmer/non-prop-template
d8c5fe0 
Adapt to coq/coq#18867 (inductive_sort_family doesn't exist)
ppedrot added a commit to LPCIC/coq-elpi that referenced this pull request Apr 18, 2024
@ppedrot
Merge pull request #617 from SkySkimmer/non-prop-template
0da3196 
Adapt to coq/coq#18867 (cominductive returns default dep elim)
@SkySkimmer SkySkimmer deleted the non-prop-template branch April 19, 2024 11:09
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@ppedrot ppedrot ppedrot approved these changes

Assignees

@ppedrot ppedrot

Labels
kind: cleanup Code removal, deprecation, refactorings, etc. part: universes The universe system.
Projects
None yet
Milestone
8.20+rc1
Development

Successfully merging this pull request may close these issues.

None yet
2 participants
@SkySkimmer @ppedrot