Repository navigation
Misc fixes parser word enum - #280
Merged
hanno-becker merged 4 commits intoSep 23, 2026
Merged
Conversation
A plugin can first see an enum when independently developed theory branches merge. Its stored terms, types, and theorems still belong to the declaration theory, so using them in the merged target can fail. Morphism-transform every semantic field in the enum payload and transfer it into the active theory before running an interpretation. Signed-off-by: Ike Mulder <[email protected]>
The code evaluator has a substantial fixed startup cost. It makes single-variant and other small simple word enums slower to declare than equivalent datatypes, despite scaling better for large enums. Use direct simplification for enums with fewer than 100 variants. Keep the merge-sort and evaluation proof for larger enums, where direct simplification grows quadratically and merge-sort simplification creates large intermediate proof terms. Document the benchmark-derived cutoff as a heuristic. Signed-off-by: Ike Mulder <[email protected]>
Nested uRust pattern parsing accepts constructor heads only when `Code.is_constr` recognizes them. Simple word enum variants instead use Isabelle's case-translation registry, so nested leaves are mistaken for pattern binders. Resolve the constant type and also consult `Case_Translation.lookup_by_constr_permissive`, retaining the existing code-constructor check. Share the resolver between the basic case and shallow uRust parsers, and add a nested-match regression for bare simple word enum variants. Signed-off-by: Ike Mulder <[email protected]>
The `urust:` name of a simple word enum is used as the prefix for its variant and conversion paths. Validation nevertheless required one plain identifier, rejecting paths already accepted by the uRust grammar. Recognize nonempty `::`-separated identifier paths and use the shared check for notation grammar and simple word enum names. Reject malformed paths and syntax that still requires bespoke productions. Add coverage for path-qualified variants and conversion functions. Keep nested match leaves limited to bare HOL variant constants; this does not add notation-table resolution for path-qualified patterns. Signed-off-by: Ike Mulder <[email protected]>
hanno-becker
approved these changes
Sep 23, 2026
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
2 participants
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 fixes four (minor) problems:
plugins defined forsimple_word_enums will work for enums defined in parallel defined theories. Ie, if you have a plugin defined in theory P, and enums defined in theory E, and now you have a new theory that imports both P and E, the plugin should still run on the enums defined in E. This happens at theory merging (AFAIU), and requires somemorphismincantations. Previously, this would cause an error at theory import.simple_word_enums is discharged back to a plainsimpwhen there is less than 100 constructors. The start-up time forevalis significant, and not worth it for small enums.simple_word_enums are constructors too. Previously, this only intrepreted things that satisfyCode.is_constras constructors.urust:names forsimple_word_enums to allow path names. In particular, this means theseurust:names may now contain the path separator::.By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.