Handle VarType

Author: Drodt

key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYConverter.java

@@ -2158,7 +2158,8 @@ public Object visit(ReceiverParameter n, Void arg) {
 
     @Override
     public Object visit(VarType n, Void arg) {
-        return getKeYJavaType(n.resolve());
+        var kjt = getKeYJavaType(n.resolve());
+        return new TypeRef(kjt);
     }
 
     @Override

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

@@ -433,20 +433,6 @@
         \displayname "variableDeclaration"
     };
 
-    variableDeclarationAssignVar {
-        \find(\modality{#allmodal}{.. var #v0 = #vi; ...}\endmodality (post))
-        \replacewith(\modality{#allmodal}{.. #typeof(#v0) #v0; #v0 = #vi ...}\endmodality (post))
-        \heuristics(simplify_prog, simplify_prog_subset)
-        \displayname "variableDeclaration"
-    };
-
-    variableDeclarationFinalAssignVar {
-        \find(\modality{#allmodal}{.. final var #v0 = #vi; ...}\endmodality (post))
-        \replacewith(\modality{#allmodal}{.. final #typeof(#v0) #v0; #v0 = #vi ...}\endmodality (post))
-        \heuristics(simplify_prog, simplify_prog_subset)
-        \displayname "variableDeclaration"
-    };
-
     /*
     variableDeclarationNullable {
             \find(\modality{#allmodal}{.. nullable #t #v0; ...}\endmodality (post))

key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java

@@ -653,6 +653,7 @@ public static ProofCollection automaticJavaDL() throws IOException {
         g.provable("../../key.core/src/test/resources/testcase/classpath/classpath.key");
         g.notprovable("heap/inconsistent_represents/MyClass_m.key");
         g.notprovable("heap/inconsistent_represents/MyClass_n.key");
+        g.provable("standard_key/java_dl/typeInference.key");
 
 
         g = c.group("FOL");

key.ui/examples/standard_key/java_dl/typeInference.key

@@ -6,5 +6,5 @@
 }
 
 \problem {
-    _a + _b + 3 = m(_a, _b)
+    _a + _b + 3 = TypeInference.m(_a, _b)
 }