Array encoding #69
Closed
Array encoding #69
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
Aurel300
force-pushed
the
feature/arrays
branch
2 times, most recently
from
6124755 to
391d7c8
Compare
Owner
Author
|
(Superseded by #117.) |
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 will add the type encoding (snapshots and predicates) for arrays and slices. The snapshot in both cases is a sequence of
s_Paramvalues. The array type additionally constrains this sequence to have a particular length.The primitive MIR "index" access (i.e., when not using the stdlib
Indextrait for slicing) is similar to anunfoldfor struct field access: when the PCG informs us that theIndexplace is accessible, we call a method that trades the array predicate for a "borrowed" array predicate and the predicate for the specific index. Another method then corresponds to thefoldthat trades these predicates back for the original array.To support arrays properly we also need support for const generics. In our encoding, these are special instances of
Typethat wrap a value ofs_Param. These are then passed around like any other generic argument and can even be mentioned in method specifications as values. (Update: this was merged separately in #93.)