Support more attributes in pyk, skip polymorphic rule handling in frontend#4916
Draft
Support more attributes in pyk, skip polymorphic rule handling in frontend#4916
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>
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.