Repository navigation
Conversation
This PR stops adding an `unsafe` declaration `T.ctorIdx._impl` and an `@[implemented_by]` attribute to every inductive type `T` with more than one constructor. leanprover#15407 added them so that `T.ctorIdx` reads the constructor tag; the code generator now emits that read itself, so the compiled code stays the same. `toLCNF` compiles a `casesOn` whose alternatives each return the index of their constructor as a raw literal, which is the body of `T.ctorIdx`, to `getObjTagNat`, the way leanprover#16253 substitutes `withPtrEqUnsafe` for `withPtrEq`. The conditions are those of leanprover#15407: the type has more than one constructor and is not a runtime builtin type such as `Nat`. The index is then the tag that every compiled `cases` on the type already switches on, so the rewrite assumes nothing new. Recognizing the body rather than the name `T.ctorIdx` keeps a user definition of `T.ctorIdx`, possible with `set_option genCtorIdx false`, compiled as written. Closes leanprover#16323
Contributor
|
Thank you for your interest in contributing to Lean! This repository currently only accepts pull requests from regular contributors, primarily from the Lean FRO, so this PR has been closed automatically. If you have found a bug or want to propose a change, please open an issue describing it instead; see also our contribution guidelines. A maintainer may reopen this PR if appropriate. |
This file contains hidden or 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
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 PR stops adding an
unsafedeclarationT.ctorIdx._impland an@[implemented_by]attribute to every inductive typeTwith more than one constructor. #15407 added them so thatT.ctorIdxreads the constructor tag; the code generator now emits that read itself, so the compiled code stays the same.toLCNFcompiles acasesOnwhose alternatives each return the index of their constructor as a raw literal, which is the body ofT.ctorIdx, togetObjTagNat, the way #16253 substituteswithPtrEqUnsafeforwithPtrEq. The conditions are those of #15407: the type has more than one constructor and is not a runtime builtin type such asNat. The index is then the tag that every compiledcaseson the type already switches on, so the rewrite assumes nothing new. Recognizing the body rather than the nameT.ctorIdxkeeps a user definition ofT.ctorIdx, possible withset_option genCtorIdx false, compiled as written.Closes #16323
Generative AI assistance: Claude assisted with the investigation, implementation and tests.