Skip to content

Commit b43e17e

Browse files
committed
Fixed rebase issues, e.g. Readded final ext set for sorts that got lost during rebase
1 parent 0927362 commit b43e17e

File tree

4 files changed

+12
-79
lines changed

4 files changed

+12
-79
lines changed

key.core/src/main/java/de/uka/ilkd/key/ldt/JavaDLTheory.java

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -56,6 +56,7 @@ public class JavaDLTheory extends LDT {
5656
public static final Sort TERMLABEL = new SortImpl(new Name("TermLabel"), null, "", "");
5757
/**
5858
* Any is a supersort of all sorts.
59+
* Important that is declared as last
5960
*/
6061
public static final Sort ANY = new SortImpl(new Name("any"), null, "", "");
6162

key.core/src/main/java/de/uka/ilkd/key/logic/sort/AbstractSort.java

Lines changed: 0 additions & 64 deletions
This file was deleted.

key.core/src/main/java/de/uka/ilkd/key/logic/sort/NullSort.java

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -33,7 +33,7 @@ public final class NullSort extends Sort {
3333

3434

3535
public NullSort(Sort objectSort) {
36-
super(NAME, null, false);
36+
super(NAME, null, false, "", "");
3737
assert objectSort != null;
3838
this.objectSort = objectSort;
3939
}

key.core/src/main/java/de/uka/ilkd/key/logic/sort/Sort.java

Lines changed: 10 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,6 @@
33
* SPDX-License-Identifier: GPL-2.0-only */
44
package de.uka.ilkd.key.logic.sort;
55

6-
import javax.annotation.Nullable;
7-
86
import de.uka.ilkd.key.java.Services;
97
import de.uka.ilkd.key.ldt.JavaDLTheory;
108
import de.uka.ilkd.key.rule.HasOrigin;
@@ -13,30 +11,28 @@
1311
import org.key_project.util.collection.DefaultImmutableSet;
1412
import org.key_project.util.collection.ImmutableSet;
1513

14+
import javax.annotation.Nonnull;
15+
1616
/**
1717
* Abstract base class for implementations of the Sort interface.
1818
*/
1919
public abstract class Sort extends org.key_project.logic.sort.AbstractSort<Sort>
2020
implements HasOrigin {
2121

22-
private ImmutableSet<Sort> ext;
22+
private final ImmutableSet<Sort> ext;
2323

24-
public Sort(Name name, ImmutableSet<Sort> ext, boolean isAbstract, String origin, String documentation) {
24+
public Sort(@Nonnull Name name, ImmutableSet<Sort> extendedSorts, boolean isAbstract, String origin, String documentation) {
2525
super(name, isAbstract, documentation, origin);
26-
this.ext = ext;
26+
if (extendedSorts != null && extendedSorts.isEmpty()) {
27+
this.ext = DefaultImmutableSet.<Sort>nil().add(JavaDLTheory.ANY);
28+
} else {
29+
this.ext = extendedSorts == null ? DefaultImmutableSet.<Sort>nil() : extendedSorts;
30+
}
2731
}
2832

2933
@Override
3034
public ImmutableSet<Sort> extendsSorts() {
31-
if (this == JavaDLTheory.FORMULA || this == JavaDLTheory.UPDATE
32-
|| this == JavaDLTheory.ANY) {
33-
return DefaultImmutableSet.nil();
34-
} else {
35-
if (ext.isEmpty()) {
36-
ext = DefaultImmutableSet.<Sort>nil().add(JavaDLTheory.ANY);
37-
}
38-
return ext;
39-
}
35+
return ext;
4036
}
4137

4238
public ImmutableSet<Sort> extendsSorts(Services services) {

0 commit comments

Comments
 (0)