Purge sort depending functions in favor of parametric functions by Drodt · Pull Request #3773 · KeYProject/key

Drodt · 2026-03-16T13:58:52Z

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.

wadoon · 2026-03-18T22:13:30Z

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`?

Drodt · 2026-03-19T05:05:27Z

This java.lang.Object::<created> is not a sort-independent function.

It is a constant, not a SortDependingFunction.

I am also not aware, way the <..> are back again. Should the new syntax not ``java.lang.Object::#$created`?

This branch is not yet based on Java Parser. I thought, JP would take a bit longer than this PR.

Drodt · 2026-03-27T13:11:57Z

Delayed until #3120 is merged and invariants are changed from <int> to $inv

Drodt · 2026-04-10T13:28:23Z

Per the KeY meeting: This PR is truly ready. Eventual syntax improvements are left for future PR (but should be discussed soon!)

WolframPfeifer

I reviewed the code and it looks mostly fine, except for a few minor complaints (mostly about comments).

However, when trying to test the PR the GUI, already at start of KeY I get the following exception (even when removing the .key directory):

[16:35:05.483] ERROR XMLResources - Cannot not load help messages in info viewjava.util.InvalidPropertiesFormatException: jdk.internal.org.xml.sax.SAXParseException; 
	at java.base/jdk.internal.util.xml.PropertiesDefaultHandler.load(PropertiesDefaultHandler.java:85)
	at java.base/java.util.Properties.loadFromXML(Properties.java:1003)
	at de.uka.ilkd.key.util.XMLResources.getResource(XMLResources.java:58)
	at de.uka.ilkd.key.util.XMLResources.<init>(XMLResources.java:36)
	at de.uka.ilkd.key.gui.InfoView.<init>(InfoView.java:55)
	at de.uka.ilkd.key.gui.InfoView.<init>(InfoView.java:149)
	at de.uka.ilkd.key.gui.MainWindow.<init>(MainWindow.java:329)
	at de.uka.ilkd.key.gui.MainWindow.getInstance(MainWindow.java:417)

I am not sure if the reason lies really in the PR, also KeY does not crash.

Apart from that and the minor comments, it seems to work fine.

WolframPfeifer · 2026-04-17T13:20:58Z

@@ -238,7 +238,7 @@ private void printArraySelect(LogicPrinter lp, JTerm heapTerm, JTerm objectTerm,

    /*
     * Print a select-term of the following form: T::select( ... , ... , java.lang.Object::<...>)


Suggested change

* Print a select-term of the following form: T::select( ... , ... , java.lang.Object::<...>)

* Print a select-term of the following form: select<[T]>( ... , ... , Classname::#fieldname)

I think this comment should also be updated.

WolframPfeifer · 2026-04-17T13:25:36Z

Suggested change

* Creates an <tt>instance<[T]>(..)</tt> term for the component type "T" of the array. The component

more comment updating

WolframPfeifer · 2026-04-17T13:50:27Z

Suggested change

* returns an <tt>instance<[G]>(term.sub(1))</tt> term for the element sort of the given array.

* It is assumed that <tt>term.sub(0)</tt> is either a term of reference array sort or a term

* with an <tt>exactInstance</tt> symbol as top level parameterized with the reference array sort.

I think this comment can be updated as well

WolframPfeifer · 2026-04-17T14:10:37Z

-     * Determine whether the field constant is a generic object property. Those are surrounded by
-     * angle brackets, e.g. o.$created
+     * Determine whether the field constant is a generic object property. Those are prefixed by the
+     * separator `#` and the implicit symbol `$`, e.g. o.$created


Suggested change

* separator `#` and the implicit symbol `$`, e.g. o.$created

* separator `::`, the field prefix `#`, and the marker for implicit symbols `$`, e.g. `java.lang.Object::#$created`

I think this comment mixed in a weird way the input that is checked (that is, the field name), and the output that is printed. The latter does not play any role in this method. If at all, an output example should be given in the caller. My suggestion changes the example here such that it refers to the input.

WolframPfeifer · 2026-04-17T14:48:58Z


 WS:  [ \t\n\r\u00a0]+ -> channel(HIDDEN); //U+00A0 = non breakable whitespace
 STRING_LITERAL:'"' ('\\' . | ~( '"' | '\\') )* '"' ;
 LESS: '<';
 LESSEQUAL: '<' '=' | '\u2264';
 LGUILLEMETS: '<' '<' | '«' | '‹';
 RGUILLEMETS: '>''>' | '»' | '›';
-IMPLICIT_IDENT: '<' '$'? (LETTER)+ '>' ('$lmtd')? -> type(IDENT);


Until doing this review, I was not aware that we have 11 ANTLR .g4 files now (3 * lexer, 8 * parser), instead of 4 which I remember from a while ago. How many different parsers are there, and how do they work together? Is this documented or at least outlined anywhere?

In my opinion, this makes it more difficult to find token/rule declarations, and also opens possibilities for inconsistencies: Here, IMPLICIT_IDENT was removed because it was already in the ncore KeYLexer, right?

WolframPfeifer · 2026-04-17T14:51:49Z

@@ -178,6 +179,11 @@ public record SplitFieldName(String className, String attributeName) {
     * @return the split field name
     */
    public static @Nullable SplitFieldName trySplitFieldName(Named symbol) {
+        if (symbol instanceof ParametricFunctionInstance pfi) {
+            // e.g., $classErroneous<[A]>


Is this not one of our implicit field names? Why is it used as an example for a parametric function here?

WolframPfeifer · 2026-04-17T15:01:05Z

-            SortDependingFunction firstInstance =
-                SortDependingFunction.getFirstInstance(kind, services);
-            if (firstInstance != null) {
+            final String nameWithoutFieldPrefix = kind.toString().substring(1);


Instead of substring(1), I think something like substring(JavaDLFieldNames.FIELD_PREFIX.length()) would be more robust.

WolframPfeifer · 2026-04-17T15:18:34Z

+                // TODO(DD): Extend to more complex parametric functions; ask RB what is expected
+                // here


Did you want to fix or remove this TODO?

Drodt added 14 commits March 13, 2026 18:05

Remove SortDependingFunction class

e83ca5e

Simplify parser

d5b5d48

Remove some sort depending fns

6d63c6e

Merge branch 'main' into purge-sort-depending-fn

d0dff83

Fix rewriting of .key files, field resolution, and grammar

ec93a6f

Fix tests & pp

5c07d77

Fix more .key files

8e53992

Replace more sort dep fns

3acacc7

Fix more .key files, taclets.old.txt, and SMT files

f50ce80

Fix SMT translation

7999173

Try to fix SMT lemma parsing

7a53e5d

Fix LogicPrinter when services == null

ebbd1d7

Fix oracle translation

70607d7

Fix some tests

46212b5

Drodt force-pushed the purge-sort-depending-fn branch from 8256cc5 to 46212b5 Compare March 17, 2026 15:34

Drodt added 9 commits March 17, 2026 16:38

Fix some tests

1852859

Fix quicksort

00accc7

Fix BM

3acb868

Fix Observer functions

19daf1c

Fix permission translation

b214f1e

Fix proof

03a4688

Fix field name splitting

a7d24d2

Fix rule

8c2b4e9

Fix same update level

e9fc560

Drodt mentioned this pull request Mar 18, 2026

Add Polymorphic Sorts and Functions #3652

Merged

2 tasks

Drodt added 3 commits March 18, 2026 15:18

Fix taclet proofs

abda47f

Update taclet oracle (same update level follow-up)

45fec3d

Fix escaping in XML

0e6cd44

Drodt marked this pull request as ready for review March 18, 2026 17:21

Drodt self-assigned this Mar 18, 2026

Drodt added Review Request Waiting for review Breaking Change labels Mar 18, 2026

Drodt and others added 3 commits March 19, 2026 07:43

Merge branch 'main' into purge-sort-depending-fn

46b2227

Merge branch 'main' into purge-sort-depending-fn

97e3166

Merge branch 'main' into purge-sort-depending-fn

355063b

wadoon added this to the v3.0.0 milestone Mar 22, 2026

Merge branch 'main' into purge-sort-depending-fn

7b25367

Drodt and others added 12 commits March 29, 2026 18:55

Merge branch 'main' into purge-sort-depending-fn

526d8fd

Fix select w/ old syntax

dc42f0e

Fix field name splitting

7e4eff0

Fix more .key and proof files

2092755

Fix BM proof

1be766d

Fix parser proof

e104444

Update taclet equality oracle

6aa7f8f

Rename polymorphic implicit fields

a11861c

Fix conversion of fields

6d182bd

Fix lookup for fields named instance

e5307d3

Merge branch 'main' into purge-sort-depending-fn

07ca9df

Remove implicit idents from lexer

c13286c

unp1 self-requested a review April 10, 2026 13:23

WolframPfeifer approved these changes Apr 17, 2026

View reviewed changes

		@@ -238,7 +238,7 @@ private void printArraySelect(LogicPrinter lp, JTerm heapTerm, JTerm objectTerm,

		/*
		* Print a select-term of the following form: T::select( ... , ... , java.lang.Object::<...>)


	* Creates an <tt>instance<[T]>(..)</tt> term for the component type "T" of the array. The component

+    * returns an <tt>instance<[G]>(term.sub(1))</tt> term for the element sort of the given array.
+    * It is assumed that <tt>term.sub(0)</tt> is either a term of reference array sort or a term
+    * with an <tt>exactInstance</tt> symbol as top level parameterized with the reference array sort.

	* separator `#` and the implicit symbol `$`, e.g. o.$created
	* separator `::`, the field prefix `#`, and the marker for implicit symbols `$`, e.g. `java.lang.Object::#$created`

		// TODO(DD): Extend to more complex parametric functions; ask RB what is expected
		// here

Conversation

Drodt commented Mar 16, 2026 • edited by unp1 Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Intended Change

Plan

Type of pull request

Ensuring quality

Additional information and contact(s)

Uh oh!

wadoon commented Mar 18, 2026

Uh oh!

Drodt commented Mar 19, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Drodt commented Mar 27, 2026

Uh oh!

Drodt commented Apr 10, 2026

Uh oh!

WolframPfeifer left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Drodt commented Mar 16, 2026 •

edited by unp1

Loading

Drodt commented Mar 19, 2026 •

edited

Loading