(scratch) For mathlib CI #7646
Closed
(scratch) For mathlib CI #7646
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
… are flat (leanprover#7302) This PR changes how fields are elaborated in the `structure`/`class` commands and also makes default values respect the structure resolution order when there is diamond inheritance. Before, the details of subobjects were exposed during elaboration, and in the local context any fields that came from a subobject were defined to be projections of the subobject field. Now, every field is represented as a local variable. All parents (not just subobject parents) are now represented in the local context, and they are now local variables defined to be parent constructors applied to field variables (inverting the previous relationship). Other notes: - The entire collection of parents is processed, and all parent projection names are checked for consistency. Every parent appears in the local context now. - For classes, every parent now contributes an instance, not just the parents represented as subobjects. - Default values are now processed according to the parent resolution order. Default value definition/override auxiliary definitions are stored at `StructName.fieldName._default`, and inherited values are stored at `StructName.fieldName._inherited_default`. Metaprograms no longer need to look at parents when doing calculations on default values. - Default value omission for structure instance notation pretty printing has been updated in consideration of this. - Now the elaborator generates a `_flat_ctor` constructor that will be used for structure instance elaboration. All types in this constructor are put in "field normal form" (projections of parent constructors are reduced, and parent constructors are eta reduced), and all fields with autoParams are annotated as such. This is not meant for users, but it may be useful for metaprogramming. - While elaborating fields, any metavariables whose type is one of the parents is assigned to that parent. The hypothesis is that, for the purpose of elaborating structure fields, parents are fixed: there is only *one* instance of any given parent under consideration. See the `Magma` test for an example of this being necessary. The hypothesis may not be true when there are recursive structures, since different values of the structure might not agree on parent fields. Other notes: - The elaborator has been refactored, and it now uses a monad to keep track of the elaboration state. - This PR was motivation for leanprover#7100, since we need to be able to make all parents have consistent projection names when there is diamond inheritance. Still to do: - Handle autoParams like we do default values. Inheritance for these is not correct when there is diamond inheritance. - Avoid splitting apart parents if the overlap is only on proof fields. - Non-subobject parent projections do not have parameter binder kinds that are consistent with other projections (i.e., all implicit by default, no inst implicits). This needs to wait on adjustments to the synthOrder algorithm. - We could elide parents with no fields, letting their projections be constant functions. This causes some trouble for defeq checking however (maybe leanprover#2258 would address this).
This PR implements the main logic for inheriting and overriding autoParam fields in the `structure`/`class` commands, pending being enabled in the structure instance notation elaborator. Adds term info to overridden fields, so they now can be hovered over, and "go to definition" goes to the structure the field is originally defined in. Implementation notes: - The inherited autoParams are all recorded in the flat constructor. Defined/overridden autoParam auxiliary tactic declarations now have names of the form `StructName.fieldName._autoParam` - The field `StructureFieldInfo.autoParam?` is soon to be deprecated. The elaborator is still setting it for now, since the structure instance notation elaborator is still using it.
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.
For testing new features while waiting for next nightly-with-mathlib