[RFC005] Lazy propagation #1086
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
feature/rfc005-lazy-propagation
branch
from
29d4ef6
to
bb4d423
Compare
yannham
force-pushed
the
task/rfc005-implem-draft
branch
from
04309dd
to
029a1e6
Compare
The apply_contract phase doesn't make sense anymore in the lazy propagation model of RFC005. However, we still need to convert "static" annotations (the one provided by the user) to pending contracts, the data that the runtime manipulates and cares about. This commit update the contract application phase to become a pending contract generation phase.
Continue the implementation of lazy propagation. Patch the various record destructors (field access, force, equality, etc.) to apply potential pending contracts when elements are requested.
Eager application of contracts acted directly on the annotation attached to a field. Those were thus transformed by the share_normal_form to make it work with recursive overriding. Now, runtime contracts are all conained in the new pending_contracts field. We can let metadata alone (that is, we don't have to transform them anymore), while we have to transform pending_contracts, which is what this commit does.
Co-authored-by: Oghenevwogaga Ebresafe <[email protected]>
Co-authored-by: Oghenevwogaga Ebresafe <[email protected]>
Co-authored-by: Oghenevwogaga Ebresafe <[email protected]>
Co-authored-by: Oghenevwogaga Ebresafe <[email protected]>
Co-authored-by: Oghenevwogaga Ebresafe <[email protected]>
Co-authored-by: Oghenevwogaga Ebresafe <[email protected]>
Co-authored-by: Oghenevwogaga Ebresafe <[email protected]>
4 tasks
ebresafegaga
approved these changes
Feb 14, 2023
vkleen
reviewed
Feb 15, 2023
Co-authored-by: Viktor Kleen <[email protected]>
vkleen
approved these changes
Feb 16, 2023
vkleen
reviewed
Feb 16, 2023
Co-authored-by: Viktor Kleen <[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.
Follow-up of #990.
Implement the second part of RFC005, namely getting rid of eager cross application of contracts during merging, and implement lazy propagation instead. All the bogus examples from RFC005 now gives the desired result within this PR.
The idea and challenges are in fact quite similar to the ones of lazy array contracts (#809). We probably should use
%force%instead of%deep_seq%even more. We also have the same potential performance issue that contract application aren't cached as long as we don't destruct a record (same happen with arrays):Here, the
Numcontract is applied lazily at each field access, and thus recomputed 3 times (the contract application, not1 + 1which is in its own thunk). Somehow,1 + 1 | Numdoesn't have a proper intermediate thunk to be cached. However, this is not something very hard to solve (namely by introducing this intermediate level of thunk/cache). It's just postponed to future work.In the end, the net diff is negative, and this PR gets rid of a lot of complexities from the merging function, transformation and the overall pipeline. Retrospectively, beside the user-centric motivations of RFC005, it also seems to be the better choice with respect to maintainability.