Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Delete Jkind_axis.Modal in favor of Mode.Alloc.axis #3409

Merged

Conversation

glittershark
Copy link
Member

Per zqian's CR to this effect. Also, this simplifies modality_is_const_for_axis, introduced in the previous PR, to more directly express the property rather than relying on a big ugly pattern match.

See the individual commits for more.

@glittershark glittershark requested a review from riaqn December 26, 2024 20:47
@glittershark glittershark marked this pull request as draft December 26, 2024 21:07
@glittershark glittershark force-pushed the aspsmith/with-kind-modalities branch from e37ec6f to 84008ef Compare December 27, 2024 04:33
@glittershark glittershark force-pushed the aspsmith/normalize-mode-axis-types branch 3 times, most recently from 4c2935f to f2abf37 Compare December 27, 2024 05:10
@glittershark glittershark force-pushed the aspsmith/with-kind-modalities branch from 737a2a8 to c01dc5d Compare December 27, 2024 15:28
@glittershark glittershark force-pushed the aspsmith/normalize-mode-axis-types branch 2 times, most recently from 3b9194f to cb9f1f9 Compare December 27, 2024 16:54
@glittershark glittershark marked this pull request as ready for review December 27, 2024 16:55
@glittershark glittershark force-pushed the aspsmith/normalize-mode-axis-types branch 2 times, most recently from 7f571bb to e8ad948 Compare December 28, 2024 00:10
@glittershark glittershark force-pushed the aspsmith/with-kind-modalities branch from a3a71dc to 9354afe Compare December 28, 2024 17:23
@glittershark glittershark force-pushed the aspsmith/normalize-mode-axis-types branch from e8ad948 to ffeb5de Compare December 28, 2024 17:24
@glittershark glittershark force-pushed the aspsmith/with-kind-modalities branch from 9354afe to 7da1766 Compare December 28, 2024 20:53
Per zqian's CR to this effect. note that this does not do any of the
simplification that this unlocks yet, that'll happen later
Now that the types for jkind axes and mode axes have been unified, we
can express the condition for "modality is const for axis" directly,
without resorting to a huge ugly pattern match on the axis and the
modality's atoms.
@glittershark glittershark force-pushed the aspsmith/normalize-mode-axis-types branch from ffeb5de to 6ab8dcd Compare December 28, 2024 20:54
@lpw25
Copy link
Collaborator

lpw25 commented Dec 29, 2024

I’m currently finishing off a patch that completely rewrites this whole area. If this is blocking you then feel free to go ahead with this change, but if you are just tidying things up then it is probably better to wait for my upcoming PR. I’m out for another week and a bit busy, so it’s probably still 3 weeks away or so.

@riaqn
Copy link
Contributor

riaqn commented Dec 31, 2024

@lpw25 Are you refering to the modality refactor? (adding a record type containing a modality for each axis; Are there other things as well?).

@lpw25
Copy link
Collaborator

lpw25 commented Dec 31, 2024

The modality refactor is the first in a series of patches, the second of which rewrites all the Jaxis stuff.

@glittershark
Copy link
Member Author

Is that not also going to generally conflict pretty badly with with-kinds? If so it'd be nice if you can hold off, since with-kinds landing is a pretty big blocker for us.

Copy link
Contributor

@riaqn riaqn left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Reviewed.

Ideally, I think there are some further opportunity for code removal, I put comments at several places that are easy to do.

Mostly, I think jkind*.ml should avoid mentioning specific mode axes, and instead delegate to mode.ml. Specifically, lots of the pattern match on mode axes are already done in mode.ml.

Does @lpw25 's incoming patch already disentangle mode axes from jkind? If so, then maybe it's not worthwhile to do that in this PR, since that would create more conflicts.

typing/jkind_axis.ml Outdated Show resolved Hide resolved
typing/jkind_axis.ml Outdated Show resolved Hide resolved
typing/mode.ml Outdated Show resolved Hide resolved
typing/mode.ml Outdated Show resolved Hide resolved
typing/mode.ml Outdated Show resolved Hide resolved
@glittershark glittershark force-pushed the aspsmith/normalize-mode-axis-types branch from 5d41237 to 28e90a4 Compare January 1, 2025 20:03
@glittershark glittershark requested a review from riaqn January 1, 2025 20:03
Copy link
Contributor

@riaqn riaqn left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for the changes - look good!

WRT the CI error - I think it's fine to just change Axis.print so it prints locality for Areality. Areality is our internal name to share between locality and regionality, which is not supposed to be seen by the users.

I think further code removal can be done incrementally in future PRs, we can merge this PR as it is.

@lpw25 Maybe instead of a record type containing a modality for each axis, we can have Mode.Value.axis_packed list containing all the axis, and have Mode.Modality.Value.Const.proj that projects an atom modality out of a whole modality? (I'm obsessed with the idea of not mentioning mode axes names in jkind.ml)

@riaqn riaqn merged commit 7df828b into aspsmith/with-kind-modalities Jan 6, 2025
23 checks passed
@riaqn riaqn deleted the aspsmith/normalize-mode-axis-types branch January 6, 2025 11:02
@riaqn
Copy link
Contributor

riaqn commented Jan 6, 2025

@glittershark Hmm I just noticed this PR merged into your branch - I think it's fine to merge into main instead - what do you think?

@glittershark
Copy link
Member Author

@glittershark Hmm I just noticed this PR merged into your branch - I think it's fine to merge into main instead - what do you think?

ah, yeah, this is targeting my branch because it also includes a refactor to a function introduced by that branch. I can cherry-pick only the relevant bits onto a new PR targeting main

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants