Handle KAs in sort inference, basic sort parameter inference, and better cell map handling#4915
Draft
Handle KAs in sort inference, basic sort parameter inference, and better cell map handling#4915
Conversation
…(), add_sort_params()
Adjacent tests (already pass): sort for KVariable, KApply with direct result sort,
resolve_sorts direct substitution, add_sort_params with already-filled or direct params.
New-feature tests (fail at HEAD, committed with the fixes that make them pass):
sort for unfilled KApply (should return None not raise), sort for nested result sort
(MInt{N} → MInt{Int}), sort for KAs, resolve_sorts nested substitution, add_sort_params
with nested param (MInt{N} ~ MInt{Int} → N=Int), add_sort_params ML pred sentinel.
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Three parametrized test functions (test_sort, test_resolve_sorts, test_add_sort_params) replace the eleven individual test functions. Each has a *_DATA tuple at module scope so new cases can be added by appending one tuple element. New cases added: - test_sort: ktoken, ksequence, kapply_unknown_label (KeyError → None), kas_unsorted_alias (alias with no sort annotation → None) - test_add_sort_params: unsortable_arg_unchanged (arg with no sort annotation prevents param filling — returns term unchanged) Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Tests both the positive path (wrap when parent production expects the cell map sort) and the negative path (no wrap when parent expects the individual cell element sort) introduced in 78bfdab101. The cell-map productions are merged into the existing single DEFN to keep the fixture count low. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
…ive substitution
sort() gains a KAs case that returns the alias variable's sort, and the KApply case
is now wrapped in try/except so unfilled sort params (e.g. when label.params=[] but
the production requires params) return None instead of raising ValueError.
resolve_sorts() now recurses into nested compound sorts, enabling N → Int to also
substitute inside MInt{N} → MInt{Int}. The old code used sorts.get(sort, sort)
which only handled the case where sort IS a parameter, not nested inside one.
Makes test_definition tests pass: test_sort_kas, test_sort_kapply_unfilled_params_returns_none,
test_sort_kapply_nested_result_sort, test_resolve_sorts_nested.
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
…t sort sentinel
The old implementation only extracted sort-param bindings when the production
argument sort was exactly a sort parameter (psort in prod.params). This missed
cases like MInt{Width} ~ MInt{8} where the parameter is nested.
New helper _unify_sort_params recursively matches a parametric sort against an
actual sort, extracting {Width: 8} from MInt{Width} ~ MInt{8}. _merge_binding
handles conflicts and LUB computation when the same parameter appears in multiple
argument positions.
ML predicates (#Equals, #Ceil, #Floor, #In) have a context-dependent result sort
that cannot be inferred from arguments alone. When Sort1 (the operand sort) is
determined but Sort2 (the axiom result sort) is not, Sort2 is filled with the
sentinel KSort('#SortParam'). Downstream code (_ksort_to_kore) maps this sentinel
to SortVar('Q0') to emit the correct axiom{R,Q0} universally-quantified form.
Makes test_definition tests pass: test_add_sort_params_nested_param,
test_add_sort_params_ml_pred_sentinel.
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
The old _wrap_elements unconditionally wrapped any KApply matching a cell label, even when the parent production expected the individual cell sort (not the map sort). This caused double-wrapping in productions like EntryCellMapKey(<entry>(...)) where the argument sort is EntryCell, not EntryCellMap. The new implementation inspects the parent production's expected argument sorts and only wraps when the expected sort matches the cell map sort (e.g. EntryCellMap). Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
ehildenb
commented
Apr 27, 2026
Comment on lines
1496
to
+1504
| def add_sort_params(self, kast: KInner) -> KInner: | ||
| """Return a given term with the sort parameters on the `KLabel` filled in (which may be missing because of how the frontend works), best effort.""" | ||
| # ML predicate labels whose result sort (Sort2) is context-dependent and not inferable | ||
| # from the arguments alone. When Sort1 can be determined but Sort2 cannot, we fill Sort2 | ||
| # with the sentinel KSort('#SortParam') so that downstream Kore emission can introduce a | ||
| # universally-quantified sort variable (Q0) in the axiom. | ||
| _ML_PRED_RESULT_SORT_PARAM = KSort('#SortParam') # noqa: N806 | ||
| _ML_PRED_LABELS = frozenset({'#Equals', '#Ceil', '#Floor', '#In'}) # noqa: N806 | ||
|
|
Member
Author
There was a problem hiding this comment.
Unclear how this algorithm ends up handling cases with multiple sort parameters, since it uses just one sentinel value.
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
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.
No description provided.