Skip to content

Purge sort depending functions in favor of parametric functions#3773

Open
Drodt wants to merge 26 commits intomainfrom
purge-sort-depending-fn
Open

Purge sort depending functions in favor of parametric functions#3773
Drodt wants to merge 26 commits intomainfrom
purge-sort-depending-fn

Conversation

@Drodt
Copy link
Member

@Drodt Drodt commented Mar 16, 2026

Intended Change

Replace all sort depending functions from KeY and replace them with parametric functions, e.g., int::select -> select<[int]>.

This PR does not affect behavior. In particular, sequences are not (yet) made parametric and the grammar is not really modified.

SortDependingFunction is removed.

Plan

  • The grammar cannot be improved, because the sort depending function syntax is also used for fields, especially java.lang.Object::<created>
  • Fix all the tests that are sure to break

Type of pull request

  • Breaking change (fix or feature that would cause existing functionality to change)
  • There are changes to the (Java) code
  • There are changes to the taclet rule base

Ensuring quality

  • I made sure that introduced/changed code is well documented (javadoc and inline comments).
  • I made sure that new/changed end-user features are well documented (https://github.com/KeYProject/key-docs).
  • I added new test case(s) for new functionality.
  • I have tested the feature as follows: ...
  • I have checked that runtime performance has not deteriorated.
  • For new Gradle modules: I added the Gradle module to the test matrix in
    .github/workflows/tests.yml

Additional information and contact(s)

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.

@Drodt Drodt force-pushed the purge-sort-depending-fn branch from 8256cc5 to 46212b5 Compare March 17, 2026 15:34
@Drodt Drodt mentioned this pull request Mar 18, 2026
2 tasks
@Drodt Drodt marked this pull request as ready for review March 18, 2026 17:21
@Drodt Drodt self-assigned this Mar 18, 2026
@wadoon
Copy link
Member

wadoon commented Mar 18, 2026

This java.lang.Object::<created> is not a sort-independent function. I am also not aware, way the <..> are back again. Should the new syntax not ``java.lang.Object::#$created`?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants