pyk: context-aware sort-parameter inference in add_sort_params (port of Java AddSortInjections) by ehildenb · Pull Request #4915 · runtimeverification/k

Commits on Apr 27, 2026

test_definition: add unit tests for KDefinition sort(), resolve_sorts(), add_sort_params()

ehildenb
and
claude
committed
test_definition: convert to pytest parametrization, add extra test cases

ehildenb
and
claude
committed
test_definition: add unit tests for add_cell_map_items guard

ehildenb
and
claude
committed
outer: sort() handles KAs and unfilled KApply; resolve_sorts() recursive substitution

ehildenb
and
claude
committed
outer: add_sort_params() handles nested sort params and ML pred result sort sentinel

ehildenb
and
claude
committed
outer: add_cell_map_items wraps only when parent expects cell map sort

ehildenb
and
claude
committed

Commits on Apr 28, 2026

outer: assert at most one unbound sort param when using ML pred sentinel

ehildenb
and
claude
committed

Commits on May 8, 2026

Commits on May 11, 2026

outer, test_definition: port Java AddSortInjections direct sort param inference

ehildenb
and
claude
committed

Commits on May 12, 2026

Merge remote-tracking branch 'upstream/develop' into sort-handling-improvements
ehildenb
committed

Commits on May 27, 2026

Commits on Jun 1, 2026

Commits on Jun 2, 2026

Commits on Jun 4, 2026

Merge remote-tracking branch 'upstream/develop' into sort-handling-improvements
ehildenb
committed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

pyk: context-aware sort-parameter inference in add_sort_params (port of Java AddSortInjections)#4915

pyk: context-aware sort-parameter inference in add_sort_params (port of Java AddSortInjections)#4915
ehildenb wants to merge 25 commits into
developfrom
sort-handling-improvements

Commits on Apr 27, 2026

test_definition: add unit tests for KDefinition sort(), resolve_sorts(), add_sort_params()

test_definition: convert to pytest parametrization, add extra test cases

test_definition: add unit tests for add_cell_map_items guard

outer: sort() handles KAs and unfilled KApply; resolve_sorts() recursive substitution

outer: add_sort_params() handles nested sort params and ML pred result sort sentinel

outer: add_cell_map_items wraps only when parent expects cell map sort

Commits on Apr 28, 2026

outer: assert at most one unbound sort param when using ML pred sentinel

Commits on May 8, 2026

Merge remote-tracking branch 'upstream/develop' into sort-handling-improvements

outer, test_definition: replace assert with NotImplementedError for multi-unbound ML pred sort params

outer, test_definition: warn when user-defined label has unresolvable sort params

Commits on May 11, 2026

outer, test_definition: port Java AddSortInjections direct sort param inference

Commits on May 12, 2026

Merge remote-tracking branch 'upstream/develop' into sort-handling-improvements

Commits on May 27, 2026

outer, test_definition: infer_sort_params returns (bindings, inferred_sort) tuple

outer: fix _resolve_sort_partial docstring for pydocstyle

Commits on Jun 1, 2026

Merge remote-tracking branch 'upstream/develop' into sort-handling-improvements

test_definition: add regression tests for sort-inference bugs (infer_sort_params, add_sort_params)

outer: report ML-predicate sort conflicts in add_sort_params instead of raising

outer: fix infer_sort_params matchExpected to test declared argument sorts

outer: add set-based least_upper_bound, use it for infer_sort_params resolution

Commits on Jun 2, 2026

prelude/k, konvert/_kast_to_kore, outer: fail clearly on #SortParam sentinel; document full fix

pyk/docs: date-prefix pipeline, regression-triage filenames for chronological sorting

inner, outer, test_{inner,definition}: replace _sort_contains helper with KSort.contains method

outer, test_definition: rewrite add_sort_params as top-down/bottom-up sweep with fresh sort vars

outer, test_definition: drop dead infer_sort_params/_resolve_sort_partial; test least_upper_bound directly

Commits on Jun 4, 2026

Merge remote-tracking branch 'upstream/develop' into sort-handling-improvements