Compset values #1766
Open
Compset values #1766
Conversation
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
Compsets now support a "sealed" flag that prevents mutation of existing constant entries while still allowing new constants to be added. This enables base compsets (like bool_compset) to be safely shared as values rather than generated fresh via unit -> compset functions. Key changes: - Add sealed flag to compset datatype - seal: marks a compset as sealed - copy: creates an unsealed copy with fresh refs for all constants - assoc_clause raises an exception when trying to add rules for an existing constant in a sealed compset Most operations that produce a new compset (add_thms, add_conv, etc.) produce an unsealed compset. The seal operation protects against accidental pollution of shared base compsets. When you need to extend rules for existing constants in a sealed compset, use copy first to get a modifiable compset. Selftests added to verify: - Sealed compsets reject additions to existing constants - Sealed compsets accept additions for new constants - Copy creates a modifiable compset with same evaluation behavior - bool_compset is properly sealed Co-Authored-By: Claude <[email protected]>
The previous code was too aggressive, preventing merely reading existing constants. And some of the previous tests were using the wrong constant. Co-Authored-By: Claude <[email protected]>
Co-Authored-By: Claude <[email protected]>
Co-Authored-By: Claude <[email protected]>
Co-Authored-By: Claude <[email protected]>
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 is an addition to #1764 that makes more significant design decisions on how to handle the fact that compsets, even with a functional computeLib API, are still mutable. See discussion on that PR.