Implement the record_lazy_assume primop #1211
Merged
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
yannham
force-pushed
the
task/record-lazy-assume
branch
from
b9312d3
to
7eb7140
Compare
vkleen
approved these changes
Mar 29, 2023
yannham
commented
Mar 29, 2023
The contract.Equal requires a new primop, akin to the existing array_lazy_assume, which adds a contract to the `pending_contracts` of each field of a record. This primop also reverts recursive records, as this new contract may alter fields, and thus trigger a recomputation of the recursive record's fixpoint. Doing so, we got rid of the `dictionary_assume` contract, which can be subsumed (more easily and more efficiently!) by this new primop.
yannham
force-pushed
the
task/record-lazy-assume
branch
from
5a56e6d
to
8939cc1
Compare
|
I have no idea why the CI won't run anymore 🤷♂️ |
|
I ran |
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.
Follow-up of #1203. Preliminary PR to make the
Equalcontract lazy.This PR introduces a new primop, akin to the existing
array_lazy_assume, which adds a contract to thepending_contractsof each field of a record. This primop also reverts recursive records, as this new contract may alter fields (e.g. by adding a default value), and thus triggers a recomputation of the recursive record's fixpoint.Doing so, we got rid of the
dictionary_assumecontract, which can be subsumed (more easily and more efficiently!) by this new primop.