-
Notifications
You must be signed in to change notification settings - Fork 78
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Restructure modal and with-bounds (fka baggage) in jkind
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.
- Loading branch information
1 parent
8b74119
commit f0911cc
Showing
20 changed files
with
647 additions
and
826 deletions.
There are no files selected for viewing
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
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
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
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
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
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
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
Oops, something went wrong.