Handle sort parameters correctly in JSON Kast format#4913
Open
Handle sort parameters correctly in JSON Kast format#4913
Conversation
…_{kast,manip}: bump KAST version 3→4, emit structured KSort params
KSort nodes previously encoded sort parameters in the name string
(e.g. "MInt{Width}"), requiring Outer.parseSort on the Java side to
reconstruct the structured Sort. Now ToJson emits a separate "params"
array alongside the base "name", matching the Scala Sort ADT directly.
JsonParser.toSort gains a legacy fallback for v3 JSON (no "params" key).
Python KSort gains a params field; KSort.from_dict and AnyType._freeze
both handle the old encoded-name format for backward compatibility when
reading pre-v4 JSON (e.g. the prelude-modules.json fixture).
prelude-modules.json is regenerated with the new structured format.
test_kast and test_manip are updated to reflect the new KSort repr.
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
…Kore emission, un-skip test
sort_decl_to_kore now emits canonical sort variables (SortS0, SortS1, ...)
for sorts with parameters (e.g. syntax MInt{Width} → hooked-sort SortMInt{SortS0}).
_sort_app now recursively converts sort params, threading the production context
so that sort variables (params in production.params) correctly become SortVar
in sort applications (e.g. SortMInt{SortWidth} in a symbol with {Width} param).
_no_junk_axioms skips parameterized sorts — Java does not generate no-junk
axioms for them.
All 7 test_module_to_kore cases now pass; @pytest.mark.skip removed.
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
…migrate fixtures to KAST v4 The v3-format backward compat paths in KSort.from_dict, AnyType._freeze, and JsonParser.toSort are not reachable in normal use: both Python (kast_term) and Java (JsonParser.parse) reject any JSON whose version field != 4. The only remaining v3 JSON was in the profiling test fixtures, which are now migrated to v4 format via a direct JSON node walk. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
ehildenb
commented
Apr 24, 2026
| [KApply(KLabel('_Set_'), [KVariable('_'), KVariable('_')])], | ||
| ), | ||
| KVariable('Ceil_fa9c0b54'), | ||
| KVariable('Ceil_db45cd3a'), |
Member
Author
There was a problem hiding this comment.
These changes are because the structure of KSort is now changed internally to have params=() everywhere.
ehildenb
commented
Apr 24, 2026
Comment on lines
213
to
+219
| def sort_decl_to_kore(syntax_sort: KSyntaxSort) -> SortDecl: | ||
| name = _sort_name(syntax_sort.sort.name) | ||
| # Kore sort declarations use canonical indexed sort variable names (SortS0, SortS1, ...) | ||
| sort_vars = tuple(SortVar(f'SortS{i}') for i in range(len(syntax_sort.sort.params))) | ||
| attrs = atts_to_kore(syntax_sort.att) | ||
| hooked = Atts.HOOK in syntax_sort.att | ||
| return SortDecl(name, (), attrs=attrs, hooked=hooked) | ||
| return SortDecl(name, sort_vars, attrs=attrs, hooked=hooked) |
Member
Author
There was a problem hiding this comment.
I'm unsure about this change, should we be using a generated canonical name or passing through the existing name? This is for a syntax sort declaration, and I guess that means the names of the sort variables doesn't matter that much, but maybe the user wants the name they supplied to be preserved?
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
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.
Fixes: #4653
This adds explicit support for sort parameters in the JSON Kast format emitted/read by the Java and Python frontends. In particular:
_module_to_korein Python._module_to_koretest that was skipped because of this.