Restructure modal and with-bounds (fka baggage) in jkind #3457
+882
−972
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
glittershark
added
the
modes
glittershark
commented
Jan 9, 2025
glittershark
changed the title
glittershark
force-pushed
the
aspsmith/untype-jkind
branch
from
aaa1601 to
1af69a4
Compare
glittershark
force-pushed
the
aspsmith/transpose-jkind
branch
from
5ce9f8b to
6270b24
Compare
goldfirere
reviewed
Jan 15, 2025
|
I have reviewed the latest four commits ("Apply suggestions from code review"..."remove pointless magic"), with no further comments. |
Move the current version of Jkind_axis.Axis_collection, which wraps a type indexed on the specific axis, into `Axis_collection.Indexed`, and make `Axis_collection.t` unindexed. I already have one use case (in printing for jkinds) which doesn't care about the specific axis in the type, and I'm about to introduce another, and this feels like a natural structure.
glittershark
force-pushed
the
aspsmith/transpose-jkind
branch
from
1f20220 to
970e1f4
Compare
glittershark
force-pushed
the
aspsmith/untype-jkind
branch
from
1af69a4 to
20d0d08
Compare
Parser Change ChecklistThis PR modifies the parser. Please check that the following tests are updated:
This test should have examples of every new bit of syntax you are adding. Feel free to just check the box if your PR does not actually change the syntax (because it is refactoring the parser, say). |
glittershark
force-pushed
the
aspsmith/transpose-jkind
branch
from
970e1f4 to
1571935
Compare
This commit contains a significant restructuring of the modal upper bounds and with-bounds (which is the new name for what was previously called "baggage") in the innards of Jkind.t Previously, jkinds morally consisted of: - a layout - a map from axis, to a pair of upper bound and a list of types (the with-bounds for that axis) now, we instead have, morally: - a layout - a map from axis to the upper bound for that axis - a list of (type, modality) pairs, where the modality is effectively providing us the way that the type operates on the axis This behavior is both much closer to the syntactic representation of jkinds, making it simpler both to construct and to print, and probably more efficient, since the usual behavior is that a type appears on the with-bounds for all axes (this is only not the case in the presence of modalities) The test changes are mostly innocuous: 1. Printing changed slightly when illegal crossing is used - actually I'm reasonably sure that this change *fixed* printing of kind annotations for types with illegal crossing 2. We're no longer deduplicating types for printing kinds (we used to do this only when constructing outcometrees); this will come back later as we do deduplication of with-bounds at construction time. 3. We actually got better at printing kinds in general, eg we're now better at figuring out built-in aliases to print under some with-bounds. Past the actual internals of with-bounds, we frequently /reconstruct/ the list-of-types-per-axis shape, eg in subsumption - this is mostly done to avoid this commit getting too large and hairy, and in follow-up I plan on refactoring to do more algorithms such as bound extension holistically rather than per-axis, which ought to also realize more performance gains here.
[CI] Use setup-ocaml v3 for ocamlformat workflow
Co-authored-by: Richard Eisenberg <[email protected]>
glittershark
force-pushed
the
aspsmith/transpose-jkind
branch
from
1571935 to
3ea7efe
Compare
This comment was marked as resolved.
This comment was marked as resolved.
glittershark
force-pushed
the
aspsmith/transpose-jkind
branch
from
fb3f76c to
e6c6bc4
Compare
|
4f424dc needs review (by @goldfirere ) |
goldfirere
approved these changes
Jan 27, 2025
| let bound1 = Bounds.get ~axis sub.jkind.upper_bounds in | ||
| let bound2 = Bounds.get ~axis super.jkind.upper_bounds in | ||
| let with_bounds1 = | ||
| With_bounds.types_on_axis ~axis sub.jkind.with_bounds |
There was a problem hiding this comment.
This does some work, and it will be wasted effort if the second shortcut below is taken.
| With_bounds.types_on_axis ~axis sub.jkind.with_bounds | ||
| in | ||
| (* If bound1 is min and has no with-bounds, we're good. *) | ||
| (Bound_ops.le bound1 Bound_ops.min && List.length with_bounds1 = 0) |
There was a problem hiding this comment.
List.compare_length_with is a tad more efficient. (Basically any use of List.length is probably wrong, in my book.)
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 commit contains a significant restructuring of the modal upper bounds and with-bounds (which is the new name for what was previously called "baggage") in the innards of
Jkind.tPreviously, jkinds morally consisted of:
for that axis)
now, we instead have, morally:
This behavior is both much closer to the syntactic representation of jkinds, making it simpler both to construct and to print, and probably more efficient, since the usual behavior is that a type appears on the with-bounds for all axes (this is only not the case in the presence of modalities)
The test changes are mostly innocuous:
Past the actual internals of with-bounds, we frequently /reconstruct/ the list-of-types-per-axis shape, eg in subsumption - this is mostly done to avoid this commit getting too large and hairy, and in follow-up I plan on refactoring to do more algorithms such as bound extension holistically rather than per-axis, which ought to also realize more performance gains here.
note for reviewers: the last commit is a cherry-pick from main to get CI passing, and can be ignored. The two other commits can easily be reviewed separately.