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.

Drodt

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

Drodt

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

wadoon · 2026-06-19T10:26:57Z

Thanks for the help. The tests is green now. The null pointer warning will be fixed.

WolframPfeifer · 2026-06-19T17:24:42Z

Can we stay with Java's name scheme and call it ImmutableArrayList and ImmutableLinkedList? In particular ListList, but also ListArray really sound wrong.

wadoon · 2026-06-19T19:02:18Z

Can we stay with Java's name scheme and call it ImmutableArrayList and ImmutableLinkedList? In particular, ListList, but also ListArray really sound wrong.

It depends on how you read this. My reading is: ImmutableList backed by an array or by a java.util.List. ImmutableArrayList could lead you on a false track, that there is an java.util.ArrayList as the internal data structure, which is not the case.

The main idea of this PR is to get rid of ImmutableArray (which have nearly the same interface as ImmutableSLList). In many cases, ImmutableArray has memory and performance advantages, but some operations of ImmutableList are expensive on arrays (e.g., tail()).

To tackle this, the PR also contains operational wrappers for ImmutableList, providing views on lists, e.g., tail() resolves into new ImmutableListSlice(old, 1) which just hides the first element. No lists are copied.

mattulbrich · 2026-06-19T20:03:20Z

Nice idea! Appears to make a lot of sense indeed!
I agreed with Wolfram's impression of the strange names, but I can now also see why you named them like this.
Still: Strange names and people will be puzzled at first contact.

So: Could you or Claude (& you checking) please provide a lot of documentation on the public interface, the static methods and the new classes?

Perhaps you can also mention there: Why does ImultabeListList exist? Can the array class not do the same job?

# 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 # Conflicts: # key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java # key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletBuilder.java # key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletGenerator.java

wadoon · 2026-06-21T23:30:01Z

I agreed with Wolfram's impression of the strange names,

You should never need to use the names in your snippets. You should always use the interface ImmutableList. You get the most appropriate representation via the factory methods, e.g.,

ImmutableList.of() => ImmutableSLList.NIL
ImmutableList.of(a,b,c) => ImmutableListArray (b/c array is already created by Java/varargs)
Immutable.from(Iterable) => ImmutableListList (b/c of unknown length and wrong order for ImmutableSList)

The impl classes are package-private!

Perhaps you can also mention there: Why does ImultabeListList exist? Can the array class not do the same job?

There is one use case: The cases in which you have a list, and you are knowing that the list is fresh and has not leaked, i.e., in stream()....collect(Immutable.collector()). In these cases you can spare copying.

In all other cases, you should copy the list to an "unmodifiable" list, and in this cases you have not won anything in contrast to an array (except for one layer unmodifiability).

mattulbrich · 2026-06-22T20:33:07Z

Thanks for the response.

I agreed with Wolfram's impression of the strange names,

You should never need to use the names in your snippets. You should always use the interface ImmutableList. You get the most appropriate representation via the factory methods

OK, I can see this. I like that they are package private; this is good.

Perhaps you can also mention there: Why does ImultabeListList exist? Can the array class not do the same job?

There is one use case: The cases in which you have a list, and you are knowing that the list is fresh and has not leaked, i.e., in stream()....collect(Immutable.collector()). In these cases you can spare copying.

Currently, the only constructor does not spare copying.
Perhaps it makes sense to add code that uses the ListList implementation. ImmutableListList.COLLECTOR or something of the kind.
The class does not convince me yet.

In all other cases, you should copy the list to an "unmodifiable" list, and in this cases you have not won anything in contrast to an array (except for one layer unmodifiability).

... and one or two layers of additional call complexity.

mattulbrich · 2026-06-22T20:38:37Z

@@ -15,9 +15,6 @@

 public class ImmutableArray<S extends @Nullable Object>


You mentioned this class is covered by ImmutableListArray

Consider adding @Deprecated

mattulbrich · 2026-06-22T20:39:21Z

+ * @author Alexander Weigl
+ * @version 1 (25.04.26)
+ */
+final class ImmutableListConcat<T extends @Nullable Object>


Documentation please.

mattulbrich · 2026-06-22T20:39:34Z

+ * @version 1 (25.04.26)
+ */
+@SuppressWarnings("unchecked")
+final class ImmutableListList<T extends @Nullable Object> implements ImmutableList<T> {


Documentation please.

mattulbrich · 2026-06-22T20:40:06Z

+final class ImmutableListList<T extends @Nullable Object> implements ImmutableList<T> {
+    private final List<T> data;
+
+    public ImmutableListList(Collection<T> data) {


If this is the only constructor, this class does not really make sense.

mattulbrich · 2026-06-22T20:40:28Z

+ * @author Alexander Weigl
+ * @version 1 (25.04.26)
+ */
+final class ImmutableListReverse<T extends @Nullable Object> implements ImmutableList<T> {


Documentation for this class, please.

mattulbrich · 2026-06-22T20:40:45Z

+ * @author Alexander Weigl
+ * @version 1 (25.04.26)
+ */
+final class ImmutableListSubList<T extends @Nullable Object>


Documentation please

mattulbrich · 2026-06-22T20:45:28Z

 /**
 * List interface to be implemented by non-destructive lists
 */
+@SuppressWarnings("unchecked")


Please document the class and all methods because they are API toplevel.

The methods like of(T e1, T e2) with a fixed number of arguments are usually a lot faster than creating an intermediate array. Perhaps keep them?

mattulbrich · 2026-06-22T20:48:27Z

-     * @return IList<T> the new list
-     */
-    ImmutableList<T> prepend(@SuppressWarnings("unchecked") T... array);
+    default ImmutableList<T> prepend(ImmutableList<T> list) {


Suggest <? extends T>

This applies also to the next method signatures ...

mattulbrich · 2026-06-22T20:51:00Z

+ */
+final class ImmutableListConcat<T extends @Nullable Object>
+        implements ImmutableList<T> {
+    private final ImmutableList<T> left;


Do they really need to have the same type parameter?
I think ? extends T should actually do for both of them?

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 2 times, most recently from 55024a9 to c08f219 Compare June 13, 2026 14:29

Drodt requested changes Jun 16, 2026

View reviewed changes

unp1 reviewed Jun 17, 2026

View reviewed changes

wadoon force-pushed the weigl/ilist branch from 72c1aec to 0612254 Compare June 19, 2026 07:49

wadoon enabled auto-merge June 20, 2026 11:03

wadoon added 8 commits June 20, 2026 13:03

added test cases

9926796

fix rebasing

7ea1e48

fix wrong usage of take()

a29955b

fix checkerframework

edfca46

add reviewer comments

3dbdd29

fix rebase

af8016d

fix checkerframework

d167aec

wadoon force-pushed the weigl/ilist branch from 474d258 to d167aec Compare June 20, 2026 11:03

wadoon disabled auto-merge June 20, 2026 11:04

mattulbrich requested changes Jun 22, 2026

View reviewed changes

		@@ -15,9 +15,6 @@

		public class ImmutableArray<S extends @Nullable Object>

Uh oh!

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!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Drodt left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

wadoon commented Jun 19, 2026

Uh oh!

WolframPfeifer commented Jun 19, 2026

Uh oh!

wadoon commented Jun 19, 2026

Uh oh!

mattulbrich commented Jun 19, 2026

Uh oh!

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

Uh oh!

Uh oh!

mattulbrich commented Jun 22, 2026

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!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

wadoon commented May 16, 2026 •

edited

Loading

wadoon commented Jun 21, 2026 •

edited

Loading