Skip to content

Commit 99723e9

Browse files
authored
fix: Bad cast in target Java code (#3958)
Fixes #3956 This PR removes a cast that was not accepted by the Java compiler. It seems the cast is needed at all. <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
1 parent 9d78625 commit 99723e9

File tree

4 files changed

+20
-8
lines changed

4 files changed

+20
-8
lines changed

Source/DafnyCore/Compilers/Java/Compiler-java.cs

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1003,10 +1003,10 @@ private void EmitTypeDescriptorMethod([CanBeNull] TopLevelDecl enclosingTypeDecl
10031003
// we're looking for).
10041004
var tp = targetTypeIgnoringConstraints.AsTypeParameter;
10051005
if (tp == null) {
1006-
typeDescriptorExpr = $"{DafnyTypeDescriptor}.referenceWithInitializer({StripTypeParameters(targetTypeName)}.class, () -> ({targetTypeName}){d})";
1006+
typeDescriptorExpr = $"{DafnyTypeDescriptor}.<{targetTypeName}>referenceWithInitializer({StripTypeParameters(targetTypeName)}.class, () -> {d})";
10071007
} else {
10081008
var td = FormatTypeDescriptorVariable(tp.GetCompileName(Options));
1009-
typeDescriptorExpr = $"{DafnyTypeDescriptor}.referenceWithInitializerAndTypeDescriptor({td}, () -> {d})";
1009+
typeDescriptorExpr = $"{DafnyTypeDescriptor}.<{targetTypeName}>referenceWithInitializerAndTypeDescriptor({td}, () -> {d})";
10101010
}
10111011
}
10121012
break;
@@ -1018,7 +1018,7 @@ private void EmitTypeDescriptorMethod([CanBeNull] TopLevelDecl enclosingTypeDecl
10181018

10191019
if (typeParams.Count == 0) {
10201020
// a static context in Java does not see the enclosing type parameters
1021-
wr.WriteLine($"private static final {DafnyTypeDescriptor}<{StripTypeParameters(targetTypeName)}> _TYPE = {typeDescriptorExpr};");
1021+
wr.WriteLine($"private static final {DafnyTypeDescriptor}<{targetTypeName}> _TYPE = {typeDescriptorExpr};");
10221022
typeDescriptorExpr = "_TYPE";
10231023
}
10241024
wr.Write($"public static {TypeParameters(typeParams, " ")}{DafnyTypeDescriptor}<{targetTypeName}> {TypeMethodName}(");

Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/TypeDescriptor.java

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -11,14 +11,14 @@
1111
import java.util.function.Function;
1212

1313
public abstract class TypeDescriptor<T> {
14-
final Class<T> boxedClass;
14+
final Class<?> boxedClass;
1515
final Class<?> unboxedClass;
1616

17-
TypeDescriptor(Class<T> javaClass) {
17+
TypeDescriptor(Class<?> javaClass) {
1818
this(javaClass, javaClass);
1919
}
2020

21-
TypeDescriptor(Class<T> boxedClass, Class<?> unboxedClass) {
21+
TypeDescriptor(Class<?> boxedClass, Class<?> unboxedClass) {
2222
this.boxedClass = boxedClass;
2323
this.unboxedClass = unboxedClass;
2424
}
@@ -94,7 +94,7 @@ public static <T> TypeDescriptor<T> referenceWithDefault(
9494
}
9595

9696
public static <T> TypeDescriptor<T> referenceWithInitializer(
97-
Class<T> javaClass, Initializer<T> initializer) {
97+
Class<?> javaClass, Initializer<T> initializer) {
9898
return new ReferenceType<T>(javaClass, initializer);
9999
}
100100

@@ -200,7 +200,7 @@ private static final class ReferenceType<T> extends TypeDescriptor<T> {
200200
private final Initializer<T> initializer;
201201
private TypeDescriptor<?> arrayType;
202202

203-
public ReferenceType(Class<T> javaClass, Initializer<T> initializer) {
203+
public ReferenceType(Class<?> javaClass, Initializer<T> initializer) {
204204
super(javaClass);
205205

206206
assert !javaClass.isPrimitive();

Test/git-issues/git-issue-3956.dfy

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
// RUN: %testDafnyForEachCompiler "%s"
2+
3+
datatype AAA<X> = CtorA
4+
datatype BBB<Y> = CtorB
5+
type AaaBbb<R> = AAA<BBB<R>>
6+
datatype MyType<W> = MyType(n: AaaBbb<W>)
7+
8+
method Main() {
9+
var m: MyType<char> := MyType(CtorA);
10+
print m, "\n"; // AAA.CtorA
11+
}
Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
AAA.CtorA

0 commit comments

Comments
 (0)