Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

feat: support for traits as type arguments with variance on datatypes in Java #3072

Merged
merged 21 commits into from
Nov 29, 2022
Merged

feat: support for traits as type arguments with variance on datatypes in Java #3072

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
21 commits
Select commit Hold shift + click to select a range
92e1f0b
chore: Improve whitespace in C# output
RustanLeino Nov 17, 2022
00171ec
chore: Remove unused parameter
RustanLeino Nov 17, 2022
6d7bb22
Print class objects as their Dafny names in Java
RustanLeino Nov 17, 2022
b390493
fix: Emit type arguments for codatatypes in Java
RustanLeino Nov 17, 2022
35a5e59
feat: Emit upcasts in Java
RustanLeino Nov 17, 2022
4997593
Update tests
RustanLeino Nov 17, 2022
28e8179
Add new tests
RustanLeino Nov 17, 2022
6f9df38
Add release notes
RustanLeino Nov 18, 2022
01e85e4
Merge branch 'master' into issue-2013
RustanLeino Nov 18, 2022
8c70206
Merge branch 'master' into issue-2013
RustanLeino Nov 21, 2022
f920e18
Merge branch 'master' into issue-2013
RustanLeino Nov 23, 2022
f27a4b2
Merge branch 'master' into issue-2013
RustanLeino Nov 28, 2022
dda06c7
Merge branch 'master' into issue-2013
RustanLeino Nov 28, 2022
ddbf743
Update Source/DafnyCore/Compilers/Compiler-Csharp.cs
RustanLeino Nov 29, 2022
fdb63aa
Update Source/DafnyCore/Compilers/SinglePassCompiler.cs
RustanLeino Nov 29, 2022
bbdfde3
Improve release notes
RustanLeino Nov 29, 2022
52adeac
Update Test/git-issues/git-issue-2013.dfy
RustanLeino Nov 29, 2022
737a6ba
Update Source/DafnyCore/Compilers/Compiler-java.cs
RustanLeino Nov 29, 2022
b84c8f9
Merge branch 'issue-2013' of https://github.com/RustanLeino/dafny int…
RustanLeino Nov 29, 2022
6da83bf
Add some tests
RustanLeino Nov 29, 2022
07d4a44
fix: Qualify codatatype in other module
RustanLeino Nov 29, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 1 addition & 2 deletions Source/DafnyCore/AST/Types.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -944,10 +944,9 @@ public static bool IsSupertype(Type super, Type sub) {
}
}

public static bool FromSameHead_Subtype(Type t, Type u, BuiltIns builtIns, out Type a, out Type b) {
public static bool FromSameHead_Subtype(Type t, Type u, out Type a, out Type b) {
Contract.Requires(t != null);
Contract.Requires(u != null);
Contract.Requires(builtIns != null);
if (FromSameHead(t, u, out a, out b)) {
return true;
}
Expand Down
10 changes: 5 additions & 5 deletions Source/DafnyCore/Compilers/Compiler-Csharp.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -522,7 +522,7 @@ IClassWriter CompileDatatypeBase(DatatypeDecl dt, ConcreteSyntaxTree wr) {
if (dt is CoDatatypeDecl) {
var wCo = wDefault;
wDefault = new ConcreteSyntaxTree();
wCo.Format($"new {dt.CompileName}__Lazy{DtT_TypeArgs}(() => {{ return {wDefault}; }})");
wCo.Format($"new {dt.FullCompileName}__Lazy{DtT_TypeArgs}(() => {{ return {wDefault}; }})");
}

wDefault.Write(DtCreateName(groundingCtor));
Expand Down Expand Up @@ -609,7 +609,7 @@ bool InvalidType(Type ty, bool refTy) =>
var typeArgs = TypeParameters(nonGhostTypeArgs);
var dtArgs = "_I" + datatype.CompileName + uTypeArgs;
var converters = $"{nonGhostTypeArgs.Comma((_, i) => $"converter{i}")}";
var lazyClass = $"{datatype.CompileName}__Lazy";
var lazyClass = $"{datatype.FullCompileName}__Lazy";
string PrintConverter(TypeParameter tArg, int i) {
var name = IdName(tArg);
return $"Func<{name}, __{name}> converter{i}";
Expand Down Expand Up @@ -1743,10 +1743,10 @@ protected void DeclareField(string name, bool isPublic, bool isStatic, bool isCo
if (isPublic) {
if (isConst) {
cw.InstanceMemberWriter.Write(
$"{publik}{konst} {virtuall} {typeName} {name} {{get;}}");
$"{publik}{konst}{virtuall} {typeName} {name} {{get;}}");
} else {
cw.InstanceMemberWriter.Write(
$"{publik} {virtuall} {typeName} {name} {{get; set;}}");
$"{publik}{virtuall} {typeName} {name} {{get; set;}}");
}
} else {
cw.InstanceMemberWriter.WriteLine($"{publik}{konst} {typeName} {name}");
Expand Down Expand Up @@ -2390,7 +2390,7 @@ protected override void EmitDatatypeValue(DatatypeValue dtv, string arguments, C
// new Dt__Lazy<T>( LAMBDA )
// where LAMBDA is:
// () => { return Dt_Cons<T>( ...args... ); }
wr.Write($"new {dtv.DatatypeName}__Lazy{typeParams}(");
wr.Write($"new {dtName}__Lazy{typeParams}(");
wr.Write("() => { return ");
wr.Write("new {0}({1})", DtCtorName(dtv.Ctor, dtv.InferredTypeArgs, wr), arguments);
wr.Write("; })");
Expand Down
3 changes: 2 additions & 1 deletion Source/DafnyCore/Compilers/Compiler-go.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2477,7 +2477,8 @@ void EmitDatatypeValue(DatatypeDecl dt, DatatypeCtor ctor, bool isCoCall, string
} else {
// Co-recursive call
// Generate: Companion_Dt_.LazyDt(func () Dt => Companion_Dt_.CreateCtor(args))
wr.Write("{0}.{1}(func () {2} ", companionName, FormatLazyConstructorName(dt.CompileName), IdName(dt));
wr.Write("{0}.{1}(func () {2} ", companionName, FormatLazyConstructorName(dt.CompileName),
TypeName(UserDefinedType.FromTopLevelDecl(dt.tok, dt), wr, dt.tok));
wr.Write("{{ return {0}.{1}({2}) }}", companionName, FormatDatatypeConstructorName(ctorName), arguments);
wr.Write(')');
}
Expand Down
39 changes: 24 additions & 15 deletions Source/DafnyCore/Compilers/Compiler-java.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -841,15 +841,6 @@ protected override string TypeName_UDT(string fullCompileName, List<TypeParamete
Contract.Assume(variance.Count == typeArgs.Count);
string s = IdProtect(fullCompileName);
if (typeArgs.Count != 0 && !omitTypeArguments) {
for (var i = 0; i < typeArgs.Count; i++) {
var v = variance[i];
var ta = typeArgs[i];
if (ComplicatedTypeParameterForCompilation(v, ta)) {
UnsupportedFeatureError(tok, Feature.TraitTypeParameters,
"compilation does not support trait types as a type parameter (got '{0}'{1}); consider introducing a ghost", wr,
ta, typeArgs.Count == 1 ? "" : $" for type parameter {i}");
}
}
s += "<" + BoxedTypeNames(typeArgs, wr, tok) + ">";
}
return s;
Expand Down Expand Up @@ -938,9 +929,21 @@ protected override IClassWriter CreateClass(string moduleName, string name, bool
var wRestOfBody = wBody.Fork();
var targetTypeName = BoxedTypeName(UserDefinedType.FromTopLevelDecl(cls.tok, cls, null), wTypeMethod, cls.tok);
EmitTypeMethod(cls, javaName, typeParameters, typeParameters, targetTypeName, null, wTypeMethod);

if (fullPrintName != null) {
// By emitting a toString() method, printing an object will give the same output as with other target languages.
EmitToString(fullPrintName, wBody);
}

return new ClassWriter(this, wRestOfBody, wCtorBody);
}

private void EmitToString(string fullPrintName, ConcreteSyntaxTree wr) {
wr.WriteLine("@Override");
wr.NewBlock("public java.lang.String toString()")
.WriteLine($"return \"{fullPrintName}\";");
}

/// <summary>
/// Generate the "_typeDescriptor" method for a generated class.
/// "enclosingType" is allowed to be "null", in which case the target values are assumed to be references.
Expand Down Expand Up @@ -1835,7 +1838,9 @@ IClassWriter CompileDatatypeBase(DatatypeDecl dt, ConcreteSyntaxTree wr) {
} else {
var nonGhostFormals = groundingCtor.Formals.Where(f => !f.IsGhost).ToList();
var args = nonGhostFormals.Comma(f => DefaultValue(f.Type, wDefault, f.tok));
EmitDatatypeValue(dt, groundingCtor, null, dt is CoDatatypeDecl, args, wDefault);
EmitDatatypeValue(dt, groundingCtor,
dt.TypeArgs.ConvertAll(tp => (Type)new UserDefinedType(dt.tok, tp)),
dt is CoDatatypeDecl, args, wDefault);
}

var targetTypeName = BoxedTypeName(UserDefinedType.FromTopLevelDecl(dt.tok, dt, null), wr, dt.tok);
Expand Down Expand Up @@ -1960,7 +1965,7 @@ void CompileDatatypeConstructors(DatatypeDecl dt, ConcreteSyntaxTree wrx) {
wr.WriteLine();
EmitSuppression(wr); //TODO: Fix implementations so they do not need this suppression
var w = wr.NewNamedBlock($"public class {dt.CompileName}__Lazy{typeParams} extends {IdName(dt)}{typeParams}");
w.WriteLine($"interface Computer {{ {dt.CompileName} run(); }}");
w.WriteLine($"public interface Computer {{ {dt.CompileName} run(); }}");
w.WriteLine("Computer c;");
w.WriteLine($"{dt.CompileName}{typeParams} d;");
w.WriteLine($"public {dt.CompileName}__Lazy(Computer c) {{ this.c = c; }}");
Expand Down Expand Up @@ -2623,17 +2628,17 @@ protected override void EmitDatatypeValue(DatatypeValue dtv, string arguments, C
EmitDatatypeValue(dt, dtv.Ctor, typeArgs, dtv.IsCoCall, arguments, wr);
}

void EmitDatatypeValue(DatatypeDecl dt, DatatypeCtor ctor, List<Type>/*?*/ typeArgs, bool isCoCall, string arguments, ConcreteSyntaxTree wr) {
void EmitDatatypeValue(DatatypeDecl dt, DatatypeCtor ctor, List<Type> typeArgs, bool isCoCall, string arguments, ConcreteSyntaxTree wr) {
var dtName = dt is TupleTypeDecl tupleDecl ? DafnyTupleClass(tupleDecl.NonGhostDims) : dt.FullCompileName;
var typeParams = typeArgs == null || typeArgs.Count == 0 ? "" : $"<{BoxedTypeNames(typeArgs, wr, dt.tok)}>";
var typeParams = typeArgs.Count == 0 ? "" : $"<{BoxedTypeNames(typeArgs, wr, dt.tok)}>";
if (!isCoCall) {
// For an ordinary constructor (that is, one that does not guard any co-recursive calls), generate:
// Dt.<T>create_Cons( args )
wr.Write($"{dtName}.{typeParams}{DtCreateName(ctor)}({arguments})");
} else {
wr.Write($"new {dt.CompileName}__Lazy(");
wr.Write("() -> { return ");
wr.Write($"new {DtCtorName(ctor)}({arguments})");
wr.Write($"new {DtCtorName(ctor)}{typeParams}({arguments})");
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This looked fishy to me but is fine; Nevertheless, I found a bug along the way.

module M {
  codatatype Stream<T> = Next(shead: T, stail: Stream)
}

function method CoUp(n: int, b: bool): M.Stream<int>
{
  if b then
    CoUp(n, false)  // recursive, not co-recursive, call
  else
    M.Next(n, CoUp(n+1, true))  // CoUp is co-recursive call
}

method Main(){
  print CoUp(0, false), "\n";
}

It's a one-liner. L1968 needs a public.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Good find! It was handled incorrectly in 3 compilers. I fixed it.

wr.Write("; })");
}
}
Expand Down Expand Up @@ -3731,6 +3736,10 @@ protected override void EmitApplyExpr(Type functionType, IToken tok, Expression

protected override bool NeedsCastFromTypeParameter => true;

protected override bool TargetSubtypingRequiresEqualTypeArguments(Type type) {
return type.AsCollectionType == null;
}

protected override bool IsCoercionNecessary(Type/*?*/ from, Type/*?*/ to) {
if (to == NativeObjectType) {
return false;
Expand Down Expand Up @@ -3802,7 +3811,7 @@ protected override ConcreteSyntaxTree EmitCoercionIfNecessary(Type/*?*/ from, Ty
}

protected override ConcreteSyntaxTree EmitDowncast(Type from, Type to, IToken tok, ConcreteSyntaxTree wr) {
wr.Write($"(({TypeName(to, wr, tok)})(");
wr.Write($"(({TypeName(to, wr, tok)})(java.lang.Object)(");
var w = wr.Fork();
wr.Write("))");
return w;
Expand Down
14 changes: 9 additions & 5 deletions Source/DafnyCore/Compilers/SinglePassCompiler.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -736,6 +736,8 @@ protected virtual ConcreteSyntaxTree EmitSign(Type type, ConcreteSyntaxTree wr)

protected virtual bool NeedsCastFromTypeParameter => false;

protected virtual bool TargetSubtypingRequiresEqualTypeArguments(Type type) => false;

protected virtual bool IsCoercionNecessary(Type /*?*/ from, Type /*?*/ to) {
return NeedsCastFromTypeParameter;
}
Expand All @@ -759,9 +761,11 @@ protected ConcreteSyntaxTree EmitDowncastIfNecessary(Type /*?*/ from, Type /*?*/
Contract.Requires(wr != null);
if (from != null && to != null) {
if (!IsTargetSupertype(to, from)) {
// The following assert is a sanity check. Note, in a language with NeedsCastFromTypeParameter, "to" and "from" may
// contain uninstantiated formal type parameters.
Contract.Assert(NeedsCastFromTypeParameter || IsTargetSupertype(from, to));
// By the way, it is tempting to think that IsTargetSupertype(from, to)) would hold here, but that's not true.
// For one, in a language with NeedsCastFromTypeParameter, "to" and "from" may contain uninstantiated formal type parameters.
// Also, it is possible (subject to a check enforced by the verifier) to assign Datatype<X> to Datatype<Y>,
// where Datatype is co-variant in its argument type and X and Y are two incomparable types with a common supertype.

wr = EmitDowncast(from, to, tok, wr);
}
}
Expand All @@ -774,7 +778,7 @@ protected ConcreteSyntaxTree EmitDowncastIfNecessary(Type /*?*/ from, Type /*?*/
/// This to similar to Type.IsSupertype and Type.Equals, respectively, but ignores subset types (that
/// is, always uses the base type of any subset type).
/// </summary>
public static bool IsTargetSupertype(Type to, Type from, bool typeEqualityOnly = false) {
public bool IsTargetSupertype(Type to, Type from, bool typeEqualityOnly = false) {
Contract.Requires(from != null);
Contract.Requires(to != null);
to = to.NormalizeExpand();
Expand All @@ -786,7 +790,7 @@ public static bool IsTargetSupertype(Type to, Type from, bool typeEqualityOnly =
Contract.Assert(formalTypeParameters != null || to.TypeArgs.Count == 0 || to is CollectionType);
for (var i = 0; i < to.TypeArgs.Count; i++) {
bool okay;
if (typeEqualityOnly) {
if (typeEqualityOnly || TargetSubtypingRequiresEqualTypeArguments(to)) {
okay = IsTargetSupertype(to.TypeArgs[i], from.TypeArgs[i], true);
} else if (formalTypeParameters == null || formalTypeParameters[i].Variance == TypeParameter.TPVariance.Co) {
okay = IsTargetSupertype(to.TypeArgs[i], from.TypeArgs[i]);
Expand Down
4 changes: 2 additions & 2 deletions Source/DafnyCore/Resolver/Resolver.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5329,7 +5329,7 @@ public bool Confirm(Resolver resolver, bool fullstrength, out bool convertedInto
}
}
Type a, b;
satisfied = Type.FromSameHead_Subtype(t, u, resolver.builtIns, out a, out b);
satisfied = Type.FromSameHead_Subtype(t, u, out a, out b);
if (satisfied) {
Contract.Assert(a.TypeArgs.Count == b.TypeArgs.Count);
var cl = a is UserDefinedType ? ((UserDefinedType)a).ResolvedClass : null;
Expand Down Expand Up @@ -5389,7 +5389,7 @@ public bool Confirm(Resolver resolver, bool fullstrength, out bool convertedInto
}
Type a, b;
// okay if t<:u or u<:t (this makes type inference more manageable, though it is more liberal than one might wish)
satisfied = Type.FromSameHead_Subtype(t, u, resolver.builtIns, out a, out b);
satisfied = Type.FromSameHead_Subtype(t, u, out a, out b);
if (satisfied) {
Contract.Assert(a.TypeArgs.Count == b.TypeArgs.Count);
var cl = a is UserDefinedType ? ((UserDefinedType)a).ResolvedClass : null;
Expand Down
4 changes: 1 addition & 3 deletions Test/comp/DowncastClone.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,11 +2,9 @@
// RUN: %dafny /noVerify /compile:4 /compileTarget:cs "%s" >> "%t"
// RUN: %dafny /noVerify /compile:4 /compileTarget:js "%s" >> "%t"
// RUN: %dafny /noVerify /compile:4 /compileTarget:go "%s" >> "%t"
// RUN: %dafny_0 /noVerify /compile:4 /compileTarget:java "%s" >> "%t"
// RUN: %dafny /noVerify /compile:4 /compileTarget:java "%s" >> "%t"
// RUN: %dafny /noVerify /compile:4 /compileTarget:py "%s" >> "%t"
// RUN: %diff "%s.expect" "%t"
// To enable this in cs we needed to implement DowncastClone for datatypes.
// Java avoids this problem by not even allowing traits in datatypes.

datatype Co<+T> = Co(T) | C
datatype ReCo<+T> = ReCo(T)
Expand Down
15 changes: 5 additions & 10 deletions Test/comp/DowncastClone.dfy.expect
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,16 +23,11 @@ _module.Y and _module.Y
Done

Dafny program verifier did not attempt verification
DowncastClone.dfy(24,9): Error: compilation does not support trait types as a type parameter (got 'X'); consider introducing a ghost
DowncastClone.dfy(32,9): Error: compilation does not support trait types as a type parameter (got 'X'); consider introducing a ghost
DowncastClone.dfy(40,9): Error: compilation does not support trait types as a type parameter (got 'X'); consider introducing a ghost
DowncastClone.dfy(42,9): Error: compilation does not support trait types as a type parameter (got 'X'); consider introducing a ghost
DowncastClone.dfy(42,9): Error: compilation does not support trait types as a type parameter (got 'X'); consider introducing a ghost
DowncastClone.dfy(49,9): Error: compilation does not support trait types as a type parameter (got 'X'); consider introducing a ghost
DowncastClone.dfy(51,9): Error: compilation does not support trait types as a type parameter (got 'X'); consider introducing a ghost
DowncastClone.dfy(51,9): Error: compilation does not support trait types as a type parameter (got 'X'); consider introducing a ghost
(0,-1): Error: compilation does not support trait types as a type parameter (got 'X' for type parameter 1); consider introducing a ghost
Wrote textual form of partial target program to DowncastClone-java/DowncastClone.java
Co.Co(_module.Y) and Co.Co(_module.Y)
ReCo.ReCo(_module.Y) and ReCo.ReCo(_module.Y)
false and false
_module.Y and _module.Y
Done

Dafny program verifier did not attempt verification
Co.Co(_module.Y) and Co.Co(_module.Y)
Expand Down
3 changes: 1 addition & 2 deletions Test/comp/Variance.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,10 +2,9 @@
// RUN: %dafny /noVerify /compile:4 /compileTarget:cs "%s" >> "%t"
// RUN: %dafny /noVerify /compile:4 /compileTarget:js "%s" >> "%t"
// RUN: %dafny /noVerify /compile:4 /compileTarget:go "%s" >> "%t"
// RUN: %dafny_0 /noVerify /compile:4 /compileTarget:java "%s" >> "%t"
// RUN: %dafny /noVerify /compile:4 /compileTarget:java "%s" >> "%t"
// RUN: %dafny /noVerify /compile:4 /compileTarget:py "%s" >> "%t"
// RUN: %diff "%s.expect" "%t"
// The Java compiler lacks support for this (see dafny0/RuntimeTypeTests0.dfy).

datatype Co<+T> = Co(z: T) {
const x: int;
Expand Down
20 changes: 13 additions & 7 deletions Test/comp/Variance.dfy.expect
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -47,13 +47,19 @@ _module.Int0[]0000
Done

Dafny program verifier did not attempt verification
Variance.dfy(109,9): Error: compilation does not support trait types as a type parameter (got 'X'); consider introducing a ghost
Variance.dfy(135,9): Error: compilation does not support trait types as a type parameter (got 'X'); consider introducing a ghost
Variance.dfy(140,9): Error: compilation does not support trait types as a type parameter (got 'X'); consider introducing a ghost
Variance.dfy(149,9): Error: compilation does not support trait types as a type parameter (got 'X'); consider introducing a ghost
Variance.dfy(174,9): Error: compilation does not support trait types as a type parameter (got 'X'); consider introducing a ghost
Variance.dfy(179,9): Error: compilation does not support trait types as a type parameter (got 'X'); consider introducing a ghost
Wrote textual form of partial target program to Variance-java/Variance.java
Co.Co(_module.Int) and Co.Co(_module.Int)
true0[]0000
Non.Non(_module.Int) and Non.Non(_module.Int)
true0[]0000
0 and 0
_module.Int0[]0000
CCo.CCo and CCo.CCo
true0[]0000
CNon.CNon and CNon.CNon
true0[]0000
CCon.CCon and CCon.CCon
_module.Int0[]0000
Done

Dafny program verifier did not attempt verification
Co.Co(_module.Int) and Co.Co(_module.Int)
Expand Down
8 changes: 4 additions & 4 deletions Test/dafny0/RuntimeTypeTests0.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,15 +1,15 @@
// UNSUPPORTED: windows
// RUN: %dafny /compile:0 "%s" > "%t"
// RUN: %dafny /noVerify /compile:4 /compileTarget:cs "%s" >> "%t"
// RUN: %dafny_0 /noVerify /compile:4 /compileTarget:java "%s" >> "%t"
// RUN: %dafny /noVerify /compile:4 /compileTarget:java "%s" >> "%t"
// RUN: %dafny /noVerify /compile:4 /compileTarget:js "%s" >> "%t"
// RUN: %dafny /noVerify /compile:4 /compileTarget:go "%s" >> "%t"
// RUN: %dafny /noVerify /compile:4 /compileTarget:py "%s" >> "%t"
// RUN: %diff "%s.expect" "%t"
// The code in this file demonstrates complications in sorting out covariance in some
// compilation target languages. Compilation support is currently spotty, where Java only
// supports collection types (not datatypes), and only in the "upcast" direction.
// compilation target languages.
//
// The solution in Java is to use Java's wildcard types: a "Dafny.Sequence<T>"" is assignable to
// Part of the solution in Java is to use Java's wildcard types: a "Dafny.Sequence<T>"" is assignable to
// a "Dafny.Sequence<? extends T>".
//
// Covariance is not a problem in JavaScript, since JavaScript has no static types. It's also
Expand Down
21 changes: 18 additions & 3 deletions Test/dafny0/RuntimeTypeTests0.dfy.expect
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,9 +12,24 @@ map[7 := _module.Class0] and map[7 := _module.Class0]
[_module.Class0, _module.Class0] and [_module.Class0, _module.Class0]

Dafny program verifier did not attempt verification
RuntimeTypeTests0.dfy(42,9): Error: compilation does not support trait types as a type parameter (got 'object'); consider introducing a ghost
RuntimeTypeTests0.dfy(51,9): Error: compilation does not support trait types as a type parameter (got 'object'); consider introducing a ghost
Wrote textual form of partial target program to RuntimeTypeTests0-java/RuntimeTypeTests0.java
{5, 7} and {5, 7}
Dt.Atom(_module.Class0) and Dt.Atom(_module.Class0)
Dt.Atom(_module.Class0) and Dt.Atom(_module.Class0)
{_module.Class0} and {_module.Class0}
[_module.Class0] and [_module.Class0]
multiset{_module.Class0} and multiset{_module.Class0}
map[7 := _module.Class0] and map[7 := _module.Class0]
[_module.Class0, _module.Class0] and [_module.Class0, _module.Class0]

Dafny program verifier did not attempt verification
{5, 7} and {5, 7}
Dt.Atom(_module.Class0) and Dt.Atom(_module.Class0)
Dt.Atom(_module.Class0) and Dt.Atom(_module.Class0)
{_module.Class0} and {_module.Class0}
[_module.Class0] and [_module.Class0]
multiset{_module.Class0} and multiset{_module.Class0}
map[7 := _module.Class0] and map[7 := _module.Class0]
[_module.Class0, _module.Class0] and [_module.Class0, _module.Class0]

Dafny program verifier did not attempt verification
{5, 7} and {5, 7}
Expand Down
Loading