Purge sort depending functions in favor of parametric functions

key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleGenerator.java

@@ -363,21 +363,14 @@ private OracleTerm translateFunction(Term term, boolean initialSelect) {
 
                 return new OracleMethodCall(m, args);
             }
-        } else if (name.endsWith("::instance")) {
-
-            if (fun instanceof SortDependingFunction sdf) {
-                Sort s = sdf.getSortDependingOn();
-
-
-                OracleTerm arg = generateOracle(term.sub(0), initialSelect);
-                OracleType type = new OracleType(s);
-
-                return new OracleBinTerm("instanceof", arg, type);
-
-
-            }
+        } else if (fun instanceof ParametricFunctionInstance pfi
+                && pfi.getBase() == services.getJavaDLTheory().getInstanceofSymbol(services)) {
+            Sort s = pfi.getArgs().head().sort();
 
+            OracleTerm arg = generateOracle(term.sub(0), initialSelect);
+            OracleType type = new OracleType(s);
 
+            return new OracleBinTerm("instanceof", arg, type);
         } else if (op instanceof ProgramMethod) {
 
             return translateQuery(term, initialSelect, op);

key.core.testgen/src/test/resources/testcase/smt/ce/types1.key

@@ -6,5 +6,5 @@
 }
 
 \problem {
-a != null -> (I3::instance(a) = TRUE -> I1::instance(a) = TRUE)
+a != null -> (instance<[I3]>(a) = TRUE -> instance<[I1]>(a) = TRUE)
 } 

key.core.testgen/src/test/resources/testcase/smt/ce/types2.key

@@ -6,5 +6,5 @@
 }
 
 \problem {
-a != null  -> (C1::instance(a) = TRUE -> C2::instance(a) = FALSE)
+a != null  -> (instance<[C1]>(a) = TRUE -> instance<[C2]>(a) = FALSE)
 } 

key.core.testgen/src/test/resources/testcase/smt/ce/types3.key

@@ -6,5 +6,5 @@
 }
 
 \problem {
-a != null  -> (C1::instance(a) = TRUE -> I2::instance(a) = FALSE)
+a != null  -> (instance<[C1]>(a) = TRUE -> instance<[I2]>(a) = FALSE)
 } 

key.core.testgen/src/test/resources/testcase/smt/ce/types4.key

@@ -6,5 +6,5 @@
 }
 
 \problem {
-a != null  -> (C2::instance(a) = TRUE -> (I2::instance(a) = TRUE & I1::instance(a) = TRUE & I4::instance(a) = TRUE))
+a != null  -> (instance<[C2]>(a) = TRUE -> (instance<[I2]>(a) = TRUE & instance<[I1]>(a) = TRUE & instance<[I4]>(a) = TRUE))
 } 

key.core.testgen/src/test/resources/testcase/smt/ce/types5.key

@@ -6,5 +6,5 @@
 }
 
 \problem {
-a != null  -> (A::instance(a) = TRUE -> (C2::instance(a) = TRUE | C3::instance(a) = TRUE))
+a != null  -> (instance<[A]>(a) = TRUE -> (instance<[C2]>(a) = TRUE | instance<[C3]>(a) = TRUE))
 } 

key.core.testgen/src/test/resources/testcase/smt/ce/types6.key

@@ -6,5 +6,5 @@
 }
 
 \problem {
-a != null  -> (C3::instance(a) = TRUE -> I3::instance(a) = FALSE)
+a != null  -> (instance<[C3]>(a) = TRUE -> instance<[I3]>(a) = FALSE)
 } 

key.core.testgen/src/test/resources/testcase/smt/ce/types7.key

@@ -6,5 +6,5 @@
 }
 
 \problem {
-I3::exactInstance(a) = FALSE
+exactInstance<[I3]>(a) = FALSE
 } 

key.core.testgen/src/test/resources/testcase/smt/ce/types8.key

@@ -6,5 +6,5 @@
 }
 
 \problem {
-(C4::exactInstance(a) = TRUE -> C2::exactInstance(a) = FALSE)
+(exactInstance<[C4]>(a) = TRUE -> exactInstance<[C2]>(a) = FALSE)
 } 

key.core.testgen/src/test/resources/testcase/smt/ce/types9.key

@@ -6,5 +6,5 @@
 }
 
 \problem {
-(C2::exactInstance(a) = TRUE -> C4::exactInstance(a) = FALSE)
+(exactInstance<[C2]>(a) = TRUE -> exactInstance<[C4]>(a) = FALSE)
 } 

key.core.wd/src/main/resources/de/uka/ilkd/key/proof/rules/wdGeneralRules.key

@@ -118,18 +118,18 @@
     wd_Type_Cast {
 
         \find(
-            wd(alpha::cast(t))
+            wd(cast<[alpha]>(t))
         )
         \replacewith(
-            wd(t) & (alpha::instance(t) = TRUE)
+            wd(t) & (instance<[alpha]>(t) = TRUE)
         )
         \heuristics(simplify)
     };
 
     wd_Type_ExactInstance {
 
         \find(
-            wd(alpha::exactInstance(t))
+            wd(exactInstance<[alpha]>(t))
         )
         \replacewith(
             wd(t)
@@ -140,7 +140,7 @@
     wd_Type_Instance {
 
         \find(
-            wd(alpha::instance(t))
+            wd(instance<[alpha]>(t))
         )
         \replacewith(
             wd(t)

key.core.wd/src/main/resources/de/uka/ilkd/key/proof/rules/wdHeapRules.key

@@ -40,7 +40,7 @@
     wd_Heap_Reference_Created {
 
         \find(
-            wd(alpha::select(h, o, java.lang.Object::<created>))
+            wd(select<[alpha]>(h, o, java.lang.Object::<created>))
         )
         \replacewith(
             wd(h) & wd(o) & wellFormed(h) & o != null
@@ -51,23 +51,23 @@
     wd_Heap_Reference {
 
         \find(
-            wd(alpha::select(h, o, f))
+            wd(select<[alpha]>(h, o, f))
         )
         \varcond(
             \not \isArray(o),
             \not \isStaticField(f)
         )
         \replacewith(
             wd(h) & wd(o) & wd(f) & wellFormed(h) & o != null
-            & (f = java.lang.Object::<created> | boolean::select(h, o, java.lang.Object::<created>) = TRUE)
+            & (f = java.lang.Object::<created> | select<[boolean]>(h, o, java.lang.Object::<created>) = TRUE)
         )
         \heuristics(simplify)
     };
 
     wd_Heap_Reference_Static {
 
         \find(
-            wd(alpha::select(h, o, f))
+            wd(select<[alpha]>(h, o, f))
         )
         \varcond(
             \not \isArray(o),
@@ -82,14 +82,14 @@
     wd_Heap_Reference_Array {
 
         \find(
-            wd(alpha::select(h, o, arr(i)))
+            wd(select<[alpha]>(h, o, arr(i)))
         )
         \varcond(
             \isArray(o)
         )
         \replacewith(
             wd(h) & wd(o) & wd(i) & wellFormed(h) & o != null
-            & boolean::select(h, o, java.lang.Object::<created>) = TRUE
+            & select<[boolean]>(h, o, java.lang.Object::<created>) = TRUE
             & leq(0, i) & lt(i, length(o))
         )
         \heuristics(simplify)
@@ -124,7 +124,7 @@
         )
         \replacewith(
             wd(h) & wd(o) & wd(f) & wd(a) & wellFormed(h) & o != null
-            & boolean::select(h, o, java.lang.Object::<created>) = TRUE
+            & select<[boolean]>(h, o, java.lang.Object::<created>) = TRUE
         )
         \heuristics(simplify)
     };

key.core.wd/src/main/resources/de/uka/ilkd/key/proof/rules/wdLocSetRules.key

@@ -178,7 +178,7 @@
         )
         \replacewith(
             wd(h) & wd(o) & wd(l) & wellFormed(h) & o != null
-            & boolean::select(h, o, java.lang.Object::<created>) = TRUE
+            & select<[boolean]>(h, o, java.lang.Object::<created>) = TRUE
         )
         \heuristics(simplify)
     };
@@ -193,7 +193,7 @@
         )
         \replacewith(
             wd(h) & wd(o) & wd(l) & wellFormed(h) & o != null
-            & boolean::select(h, o, java.lang.Object::<created>) = TRUE
+            & select<[boolean]>(h, o, java.lang.Object::<created>) = TRUE
         )
         \heuristics(simplify)
     };

key.core.wd/src/main/resources/de/uka/ilkd/key/proof/rules/wdSeqRules.key

@@ -57,7 +57,7 @@
     wd_Seq_Get {
 
         \find(
-            wd(alpha::seqGet(s, n))
+            wd(seqGet<[alpha]>(s, n))
         )
         \replacewith(
             wd(s) & wd(n) & leq(0, n) & lt(n, seqLen(s))

key.core/src/main/java/de/uka/ilkd/key/java/TypeConverter.java

@@ -569,11 +569,11 @@ public Expression convertToProgramElement(JTerm term) {
 
     private Expression translateJavaCast(JTerm term, ExtList children) {
         if (term.op() instanceof Function function) {
-            if (function instanceof SortDependingFunction sdf) {
-                SortDependingFunction castFunction =
-                    SortDependingFunction.getFirstInstance(JavaDLTheory.CAST_NAME, services);
-                if (sdf.isSimilar(castFunction)) {
-                    Sort s = sdf.getSortDependingOn();
+            if (function instanceof ParametricFunctionInstance pfi) {
+                ParametricFunctionDecl castFunction =
+                    services.getJavaDLTheory().getCastSymbol(services);
+                if (pfi.getBase() == (castFunction)) {
+                    Sort s = pfi.getArgs().head().sort();
                     KeYJavaType kjt = services.getJavaInfo().getKeYJavaType(s);
                     if (kjt != null) {
                         children.add(new TypeRef(kjt));