Support more attributes in pyk, skip polymorphic rule handling in frontend - #4916
Merged
Conversation
… frontend-only attributes from Kore emission Add `frontend_only: bool` flag to `AttKey` mirroring Java's `KeyRange.FrontendOnly`. Add `Atts.HYBRID`, `Atts.PUBLIC`, `Atts.STREAM`, `Atts.UNUSED` with `frontend_only=True` and proper types matching `KeyParameter.Optional`/`KeyParameter.Forbidden` in `Att.scala`. Include these in `DiscardSymbolAtts` in `simplified_module()` so they are stripped before Kore emission, matching Java's `ModuleToKORE.java` `shouldEmit()` filter. Add integration test cases `unused.k` and `frontend-only.k` (covering all four attributes) to the `module-to-kore` test-data suite. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
The frontend_only field on AttKey was purely decorative — DiscardSymbolAtts is the actual suppression mechanism and its explicit list is the source of truth. Remove the field to keep AttKey simple. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
…ctions
Java's ComputeTransitiveFunctionDependencies groups function rules by their
post-sort-injection KLabel (e.g. ite{K}), which doesn't match the parametric
production entry in attributesFor() (ite{SortSort}). The mismatch causes Java
to silently skip dependency-graph edges for polymorphic function rules, so
polymorphic functions are never marked impure transitively.
Mirror this behavior in AddImpureAtts._callers() by excluding productions with
non-empty klabel.params from the set of labels whose rules are processed.
Fixes a false-positive impure{} annotation on ite in coverage-instrumented
compilations (81/82 regression-new dirs now agree with Java, up from 78/82).
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
…polymorphic rule skipping Add a warning log in AddImpureAtts._callers() when a rule for a polymorphic function (klabel.params non-empty) is encountered and skipped. This makes the silent Java-parity behavior visible at run time. Add coverage.k to the module-to-kore integration test suite: a definition compiled with --coverage that uses #if...#fi (desugaring to the polymorphic ite function). With coverage instrumentation, ite gets rules calling #logToFile (impure), but must NOT be marked impure because Java's dependency analysis also skips polymorphic function rules. The test directly exercises the fix from the previous commit and verifies Python/Java structural-axiom agreement. EXTRA_KOMPILE_ARGS in the test fixture maps filenames to non-default kompile options, keeping all test data files using auto-derived module names. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
…compat pass Add DiscardPolymorphicSentences(SingleModulePass) that removes KRule sentences whose LHS applies a polymorphic function label (klabel.params non-empty and FUNCTION attribute present), mirroring the silent Java behaviour where ComputeTransitiveFunctionDependencies finds no rules for such labels due to the post-sort-injection KLabel / parametric attributesFor() key mismatch. Inserting this pass before AddImpureAtts lets that pass revert to simple function_labels logic with no poly_labels special-case or warning log. All Java compatibility concern is now in one named, documented place. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
ehildenb
marked this pull request as ready for review
May 8, 2026 00:22
tothtamas28
approved these changes
May 8, 2026
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
2 participants
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.
pyk's
simplified_module()was diverging from Java'sModuleToKORE.javain two distinct ways, both of which caused Kore output mismatches when cross-validating against the Java backend. This addresses that.Changes:
kast/att: add frontend-only attributesHYBRID,PUBLIC,STREAM, andUNUSED; strip them inDiscardSymbolAttsduring simplified_module(), matching Java's shouldEmit() filterkonvert/_module_to_kore: fix impurity propagation for polymorphic functions — Java'sComputeTransitiveFunctionDependencieslooks up rules by post-sort-injection KLabel (e.g.ite{K}), which never matches the parametricattributesFor()key (ite{SortSort}), so polymorphic functions are silently skipped. An extra passDiscardPolymorphicSentencesis added in pyk to match this behavior. The intention is that eventually we should probably not discard polymorphic sentences, so it's factored into its own pass with a comment.frontend-only.kandcoverage.kto the module-to-kore test-data suite covering all four frontend-only attributes and the polymorphic rule skipping behaviorkompile.py.