Better ImmutableList by wadoon · Pull Request #3816 · KeYProject/key

wadoon · 2026-05-16T14:55:33Z

Issue

We currently have two implementations of immutable sequences with ImmutableList and ImmutableArray. This requires conversions sometimes, but mainly it leads to confusion about which implementation should be taken.

Intended Change

This PR unifies everything under ImmutableList.

There are two fresh children classes: ImmutableListArray and ImmutableListList. Both behave like ImmutableList, but use different data storage (T[] or List<T>) in the background.

Some operations from ImmutableList are quite expensive on this data storages, e.g., tail() or reverse(). Therefore, I introduced views that emulate these operations, without copying the data, i.e.,

ImmutableListConcat as ImmutableList#prepend(other)
ImmutableListReverse for ImmutableList#reverse()
ImmutableListSubList for ImmutableList#take(n), ImmutableList#skip(n), ImmutableList#tail()

These operations are now in $O(1)$.

The class ImmutableArray should be considered obsolete.

Developers should use only the methods and functions of ImmutableList. Implementation may override them if there is a faster implementation, e.g, tail() on ImmutableSList.

Plan

Renaming ImmutableSList to ImmutableList.
More, even more test cases, coverage is not so bad, but could be better.
Update the JavaDoc documentation

Type of pull request

Refactoring (behaviour should not change or only minimally change)
New feature (non-breaking change which adds functionality)
There are changes to the (Java) code

Ensuring quality

I made sure that introduced/changed code is well documented (javadoc and inline comments).

wadoon · 2026-05-18T20:34:52Z

There is one stupid error in DependencyTracker happening. Currently unclear where it comes from.

# Conflicts: # key.core/src/main/java/de/uka/ilkd/key/proof/init/InitConfig.java # key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/TacletLoader.java

Drodt

Nice work! Do you have any idea why tests are failing?

Drodt · 2026-06-16T13:15:28Z

     */
    protected void fireProofGoalsAdded(Goal goal) {
-        fireProofGoalsAdded(ImmutableSLList.<Goal>nil().prepend(goal));
+        fireProofGoalsAdded(ImmutableList.<Goal>nil().prepend(goal));


Probably singleton is better here

I know. On the other side, I wanted to limit my impact. More changes => more errors => more debugging.

Let us wait, until it is green again.

Drodt · 2026-06-16T13:16:44Z

                    : "p_toMatch and assumes sequent must have same number of elements";
            newMC = matchAssumes(
-                ImmutableSLList.<AssumesFormulaInstantiation>nil().prepend(candidateInst),
+                ImmutableList.<AssumesFormulaInstantiation>nil().prepend(candidateInst),


singleton

Drodt · 2026-06-16T13:18:28Z

                .createProgramSV(new ProgramElementName("#res_sv"), ProgramSVSort.VARIABLE, false);

-        final ImmutableList<KeYJavaType> sig = ImmutableSLList.<KeYJavaType>nil()
+        final ImmutableList<KeYJavaType> sig = ImmutableList.<KeYJavaType>nil()


singleton

Drodt · 2026-06-16T13:19:39Z

                tb.apply(update, tb.prog(modality.kind(), newJavaBlock, target.sub(0)))),
            ruleApp.pio);
-        return ImmutableSLList.<Goal>nil().append(goal);
+        return ImmutableList.<Goal>nil().append(goal);


Suggested change

return ImmutableList.<Goal>nil().append(goal);

return ImmutableList.<Goal>singleton(goal);

Drodt · 2026-06-16T13:20:09Z

            ifInsts.toArray(new PosInOccurrence[0]);
        ImmutableList<PosInOccurrence> immutableIfInsts =
-            ImmutableSLList.<PosInOccurrence>nil().append(ifInstsArr);
+            ImmutableList.<PosInOccurrence>nil().append(ifInstsArr);


Suggested change

ImmutableList.<PosInOccurrence>nil().append(ifInstsArr);

ImmutableList.<PosInOccurrence>singleton(ifInstsArr);

Drodt · 2026-06-16T13:33:00Z


        protected SubIterator(Term t, MutableState mState, LogicServices services) {
-            termStack = ImmutableSLList.<Term>nil().prepend(t);
+            termStack = ImmutableList.<Term>nil().prepend(t);


Suggested change

termStack = ImmutableList.<Term>nil().prepend(t);

termStack = ImmutableList.<Term>singleton(t);

Drodt · 2026-06-16T13:34:07Z

            // No functionality is allowed in this method body!
            mediator.getUI().getProofControl().startAutoMode(r.getSelectedProof(),
-                ImmutableSLList.<Goal>nil().prepend(invokedGoal));
+                ImmutableList.<Goal>nil().prepend(invokedGoal));


Suggested change

ImmutableList.<Goal>nil().prepend(invokedGoal));

ImmutableList.<Goal>singleton(invokedGoal));

Drodt · 2026-06-16T13:34:56Z

            PosInOccurrence pos) {
        if (pos == null) {
-            return ImmutableSLList.<Integer>nil().prepend(0);
+            return ImmutableList.<Integer>nil().prepend(0);


Suggested change

return ImmutableList.<Integer>nil().prepend(0);

return ImmutableList.<Integer>singleton(0);

Drodt · 2026-06-16T13:35:35Z

     */
    private DefaultImmutableSet(T element) {
-        elementList = (ImmutableSLList.<T>nil()).prepend(element);
+        elementList = (ImmutableList.<T>nil()).prepend(element);


Suggested change

elementList = (ImmutableList.<T>nil()).prepend(element);

elementList = ImmutableList.<T>singleton(element);

Drodt · 2026-06-16T13:56:11Z

-     */
-    ImmutableList<T> append(@SuppressWarnings("unchecked") T... array);
+    default ImmutableList<T> append(ImmutableList<T> list) {
+        return new ImmutableListConcat<>(this, ImmutableList.fromList(list));


Suggested change

return new ImmutableListConcat<>(this, ImmutableList.fromList(list));

return new ImmutableListConcat<>(this, list);

Would this not also work?

Drodt

Nice work! Do you have any idea why tests are failing?

unp1 · 2026-06-17T13:31:45Z

    public ImmutableList<T> take(int n) {
+        List<T> seq = new ArrayList<>(Math.min(size(), n));
+        ImmutableList<T> list = this;
+        for (int i = 0; i < seq.size(); i++) {


seq.size() is 0 here so the loop is never executed

unp1 · 2026-06-17T14:15:08Z

+
+    @Override
+    public ImmutableList<T> removeAll(T obj) {
+        return stream().filter(it -> Objects.equals(obj, it)).collect(ImmutableList.collector());


!Object.equals

unp1 · 2026-06-17T14:34:25Z

+    @Override
+    public int hashCode() {
+        return Objects.hash(list, start, end);
+    }


here and in ListConcat and ListReverse the hascode is structural, while in Cons and ListList element-wise

equals is always element-wise

wadoon requested a review from unp1 May 16, 2026 14:55

wadoon force-pushed the weigl/ilist branch from 60527e9 to c0a0df4 Compare May 16, 2026 15:09

wadoon self-assigned this May 16, 2026

wadoon added the Java Pull requests that update Java code label May 16, 2026

wadoon added this to the v3.1.0 milestone May 16, 2026

wadoon force-pushed the weigl/ilist branch from c0a0df4 to 818f148 Compare May 16, 2026 15:30

wadoon marked this pull request as ready for review May 18, 2026 20:34

wadoon force-pushed the weigl/ilist branch from 00c9abe to eebcea5 Compare June 13, 2026 14:21

wadoon added 6 commits June 13, 2026 16:29

better and faster ImmutableList

e9bcd3f

# Conflicts: # key.core/src/main/java/de/uka/ilkd/key/proof/init/InitConfig.java # key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/TacletLoader.java

added test cases

c8870be

fix rebasing

612998c

fix wrong usage of take()

d0253a2

spotless

84484d4

fix checkerframework

c08f219

wadoon force-pushed the weigl/ilist branch from 55024a9 to c08f219 Compare June 13, 2026 14:29

spotless

47e99cc

Drodt requested changes Jun 16, 2026

View reviewed changes

unp1 reviewed Jun 17, 2026

View reviewed changes

	return ImmutableList.<Goal>nil().append(goal);
	return ImmutableList.<Goal>singleton(goal);

	ImmutableList.<PosInOccurrence>nil().append(ifInstsArr);
	ImmutableList.<PosInOccurrence>singleton(ifInstsArr);

	termStack = ImmutableList.<Term>nil().prepend(t);
	termStack = ImmutableList.<Term>singleton(t);

	ImmutableList.<Goal>nil().prepend(invokedGoal));
	ImmutableList.<Goal>singleton(invokedGoal));

	return ImmutableList.<Integer>nil().prepend(0);
	return ImmutableList.<Integer>singleton(0);

	elementList = (ImmutableList.<T>nil()).prepend(element);
	elementList = ImmutableList.<T>singleton(element);

	return new ImmutableListConcat<>(this, ImmutableList.fromList(list));
	return new ImmutableListConcat<>(this, list);

Conversation

wadoon commented May 16, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Issue

Intended Change

Plan

Type of pull request

Ensuring quality

Uh oh!

wadoon commented May 18, 2026

Uh oh!

Drodt 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!

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!

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!

Drodt 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!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

wadoon commented May 16, 2026 •

edited

Loading