diff --git a/Source/DafnyCore/AST/Types.cs b/Source/DafnyCore/AST/Types.cs index 88282299157..d21098a2b7d 100644 --- a/Source/DafnyCore/AST/Types.cs +++ b/Source/DafnyCore/AST/Types.cs @@ -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; } diff --git a/Source/DafnyCore/Compilers/Compiler-Csharp.cs b/Source/DafnyCore/Compilers/Compiler-Csharp.cs index 8eb11d79aca..de791b58ec2 100644 --- a/Source/DafnyCore/Compilers/Compiler-Csharp.cs +++ b/Source/DafnyCore/Compilers/Compiler-Csharp.cs @@ -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)); @@ -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}"; @@ -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}"); @@ -2390,7 +2390,7 @@ protected override void EmitDatatypeValue(DatatypeValue dtv, string arguments, C // new Dt__Lazy( LAMBDA ) // where LAMBDA is: // () => { return Dt_Cons( ...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("; })"); diff --git a/Source/DafnyCore/Compilers/Compiler-go.cs b/Source/DafnyCore/Compilers/Compiler-go.cs index d680e496e36..832e95b7459 100644 --- a/Source/DafnyCore/Compilers/Compiler-go.cs +++ b/Source/DafnyCore/Compilers/Compiler-go.cs @@ -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(')'); } diff --git a/Source/DafnyCore/Compilers/Compiler-java.cs b/Source/DafnyCore/Compilers/Compiler-java.cs index 6bd526f22af..c180f4c03ee 100644 --- a/Source/DafnyCore/Compilers/Compiler-java.cs +++ b/Source/DafnyCore/Compilers/Compiler-java.cs @@ -841,15 +841,6 @@ protected override string TypeName_UDT(string fullCompileName, List"; } return s; @@ -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}\";"); + } + /// /// 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. @@ -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); @@ -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; }}"); @@ -2623,9 +2628,9 @@ 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/*?*/ typeArgs, bool isCoCall, string arguments, ConcreteSyntaxTree wr) { + void EmitDatatypeValue(DatatypeDecl dt, DatatypeCtor ctor, List 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.create_Cons( args ) @@ -2633,7 +2638,7 @@ void EmitDatatypeValue(DatatypeDecl dt, DatatypeCtor ctor, List/*?*/ typeA } else { wr.Write($"new {dt.CompileName}__Lazy("); wr.Write("() -> { return "); - wr.Write($"new {DtCtorName(ctor)}({arguments})"); + wr.Write($"new {DtCtorName(ctor)}{typeParams}({arguments})"); wr.Write("; })"); } } @@ -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; @@ -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; diff --git a/Source/DafnyCore/Compilers/SinglePassCompiler.cs b/Source/DafnyCore/Compilers/SinglePassCompiler.cs index ee910d2bed8..e271abe5fa7 100644 --- a/Source/DafnyCore/Compilers/SinglePassCompiler.cs +++ b/Source/DafnyCore/Compilers/SinglePassCompiler.cs @@ -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; } @@ -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 to Datatype, + // 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); } } @@ -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). /// - 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(); @@ -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]); diff --git a/Source/DafnyCore/Resolver/Resolver.cs b/Source/DafnyCore/Resolver/Resolver.cs index 4fcb1be2677..f8d0ed889fd 100644 --- a/Source/DafnyCore/Resolver/Resolver.cs +++ b/Source/DafnyCore/Resolver/Resolver.cs @@ -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; @@ -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; diff --git a/Test/comp/DowncastClone.dfy b/Test/comp/DowncastClone.dfy index 65aa4b1a04e..a0ae89eb920 100644 --- a/Test/comp/DowncastClone.dfy +++ b/Test/comp/DowncastClone.dfy @@ -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) diff --git a/Test/comp/DowncastClone.dfy.expect b/Test/comp/DowncastClone.dfy.expect index d89a9ebd309..6c03a049e6c 100644 --- a/Test/comp/DowncastClone.dfy.expect +++ b/Test/comp/DowncastClone.dfy.expect @@ -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) diff --git a/Test/comp/Variance.dfy b/Test/comp/Variance.dfy index 1893cfb5ca9..fb41f0a1732 100644 --- a/Test/comp/Variance.dfy +++ b/Test/comp/Variance.dfy @@ -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; diff --git a/Test/comp/Variance.dfy.expect b/Test/comp/Variance.dfy.expect index 8858ffa1abe..cf08d82ac07 100644 --- a/Test/comp/Variance.dfy.expect +++ b/Test/comp/Variance.dfy.expect @@ -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) diff --git a/Test/dafny0/RuntimeTypeTests0.dfy b/Test/dafny0/RuntimeTypeTests0.dfy index b5013dbb807..b8ce6ad759b 100644 --- a/Test/dafny0/RuntimeTypeTests0.dfy +++ b/Test/dafny0/RuntimeTypeTests0.dfy @@ -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"" is assignable to +// Part of the solution in Java is to use Java's wildcard types: a "Dafny.Sequence"" is assignable to // a "Dafny.Sequence". // // Covariance is not a problem in JavaScript, since JavaScript has no static types. It's also diff --git a/Test/dafny0/RuntimeTypeTests0.dfy.expect b/Test/dafny0/RuntimeTypeTests0.dfy.expect index 914c0b0b7f8..90535aed979 100644 --- a/Test/dafny0/RuntimeTypeTests0.dfy.expect +++ b/Test/dafny0/RuntimeTypeTests0.dfy.expect @@ -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} diff --git a/Test/git-issues/git-issue-1815.dfy b/Test/git-issues/git-issue-1815.dfy index 2cae5e7c597..76c3d35c803 100644 --- a/Test/git-issues/git-issue-1815.dfy +++ b/Test/git-issues/git-issue-1815.dfy @@ -1,21 +1,23 @@ // RUN: %dafny /compile:0 "%s" > "%t" // RUN: %dafny /noVerify /compile:4 /compileTarget:cs "%s" >> "%t" // RUN: %dafny /noVerify /compile:4 /compileTarget:js "%s" >> "%t" -// RUN: %dafny_0 /noVerify /compile:4 /compileTarget:java "%s" >> "%t" -// RUN: %dafny_0 /noVerify /compile:4 /compileTarget:go "%s" >> "%t" +// RUN: %dafny /noVerify /compile:4 /compileTarget:go "%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 X<+U> = X(x: U) +datatype Dt<+U> = Dt(x: U) trait Tr {} class Cl extends Tr { - constructor () {} + constructor () {} } method Main() { - var cl := new Cl(); - var e: X := X(cl); - match e - case X(tr) => return; + var cl: Cl := new Cl(); + var e: Dt := Dt(cl); + match e { + case Dt(tr) => + } + print "done\n"; } diff --git a/Test/git-issues/git-issue-1815.dfy.expect b/Test/git-issues/git-issue-1815.dfy.expect index 359bcf4f99c..7b2651302d9 100644 --- a/Test/git-issues/git-issue-1815.dfy.expect +++ b/Test/git-issues/git-issue-1815.dfy.expect @@ -2,12 +2,16 @@ Dafny program verifier finished with 1 verified, 0 errors Dafny program verifier did not attempt verification +done Dafny program verifier did not attempt verification +done Dafny program verifier did not attempt verification -git-issue-1815.dfy(18,11): Error: compilation does not support trait types as a type parameter (got 'Tr'); consider introducing a ghost -git-issue-1815.dfy(18,11): Error: compilation does not support trait types as a type parameter (got 'Tr'); consider introducing a ghost -Wrote textual form of partial target program to git-issue-1815-java/git_issue_1815.java +done Dafny program verifier did not attempt verification +done + +Dafny program verifier did not attempt verification +done diff --git a/Test/git-issues/git-issue-2013.dfy b/Test/git-issues/git-issue-2013.dfy new file mode 100644 index 00000000000..7705f3d49dc --- /dev/null +++ b/Test/git-issues/git-issue-2013.dfy @@ -0,0 +1,219 @@ +// RUN: %dafny /compile:0 "%s" > "%t" +// 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 /noVerify /compile:4 /compileTarget:java "%s" >> "%t" +// RUN: %dafny /noVerify /compile:4 /compileTarget:py "%s" >> "%t" +// RUN: %diff "%s.expect" "%t" + + +method Main() { + TestTraits(); + TestSiblings(); + TestException(); + MoreTests.Test(); + Conveyance.Test(); + Regression.Test(); +} + +// ----- reference types ----- + +datatype Dt<+U> = Dt(u: U) + +trait Tr { + var y: int +} + +class Cl extends Tr { + constructor () { + y := 15; + } +} + +method Print(e: Dt) { + print e.u.y, "\n"; +} + +method CreateDtForTrait(e: Dt) returns (d: Dt) + ensures d.u == e.u +{ + d := e; // upcast +} + +method TestTraits() { + var cl := new Cl(); + var e: Dt := Dt(cl); + var d: Dt := CreateDtForTrait(e); + cl.y := cl.y + 1; + var f: Dt := d; // downcast + + Print(f); // 16 + Print(e); // 16 +} + +// ----- sibling types ----- + +type Even = x | x % 2 == 0 + +method TestSiblings() { + // downcasts + var a: Dt := Dt(10); + var b: Dt := a; + var c: Dt := a; + + // upcasts + b := Dt(11); + c := Dt(12); + a := b; + a := c; + + // sideway casts + b := Dt(20); + c := b; + c := Dt(30); + b := c; + + print a, " ", b, " ", c, "\n"; // Dt.Dt(12) Dt.Dt(30) Dt.Dt(30) +} + +// ----- Result ----- + +datatype Result<+T, +R> = | Success(value: T) | Failure(error: R) + +trait Exception {} + +class MyClassException extends Exception { } + +class MyClass { + const error: Exception + + constructor () { + error := new MyClassException; + } + + function method Foo(u: int): Result { + if u < 8 then + Success(8) + else + Failure(error) + } +} + +method TestException() { + var c := new MyClass(); + print c.Foo(2), " ", c.Foo(22), "\n"; // Result.Success(8) Result.Failure(_module.MyClassException) +} + +module MoreTests { + type Even = x | x % 2 == 0 + + datatype Dt = Make(T) + datatype DtCovariant<+T> = MakeCovariant(T) + + trait Z { } + trait X extends Z { } + trait Y extends Z { } + class C extends X, Y { } + + method Test() { + var c := new C; + + var s: set := {100}; + var t: set := s; + var u: set := s; + t := u; + u := t; + s := u; + s := t; + print s, " ", t, " ", u, "\n"; // {100} {100} {100} + + var S: set := {c}; + var T: set := S; + var U: set := S; + T := U; + U := T; + S := U; + S := T; + print S, " ", T, " ", U, "\n"; // {_module.C} {_module.C} {_module.C} + + // The assignments in the following example don't need covariance of Dt, because + // Dafny checks that the value with its payload is suitable for the target type. + var k: Dt := Make(100); + var m: Dt := k; + var n: Dt := k; + m := n; + n := m; + k := m; + k := n; + print k, " ", m, " ", n, "\n"; // Dt.Make(100) Dt.Make(100) Dt.Make(100) + + var K: DtCovariant := MakeCovariant(c); + var M: DtCovariant := K; + var N: DtCovariant := K; + M := var u: DtCovariant := N; u; // like M := N, but allowed by Dafny's type system + N := var u: DtCovariant := M; u; // like N := M, but allowed by Dafny's type system + print K, " ", M, " ", N, "\n"; // DtCovariant.MakeCovariant(_module.C) DtCovariant.MakeCovariant(_module.C) DtCovariant.MakeCovariant(_module.C) + } +} + +// ----- Vehicle ----- + +module Conveyance { + trait Vehicle { + } + class Car extends Vehicle { + constructor() {} + } + + trait Error { + } + class FlatTireError extends Error { + constructor() {} + } + + datatype NonVariantResult = NVSuccess(value: T) | NVFailure(error: E) + datatype CovariantResult<+T, +E> = CVSuccess(value: T) | CVFailure(error: E) + + method Test() { + var myCar: Car := new Car(); + var error: Error := new FlatTireError(); + + var cvSuccess: CovariantResult := CVSuccess(myCar); + var cvFailure: CovariantResult := CVFailure(error); + + var nvSuccess: NonVariantResult := NVSuccess(myCar); + var nvFailure: NonVariantResult := NVFailure(error); + + // This was and remains just fine + var nvCarSuccess: NonVariantResult := NVSuccess(myCar); + // The following would not be type correct for the non-variant NonVariantResult: + // var nvVehicleSuccess: NonVariantResult := nvCarSuccess; // RHS (...) not assignable to LHS (...) + + // Once, the following was not support for the Java target, but now it is + var cvCarSuccess: CovariantResult := CVSuccess(myCar); + var cvVehicleSuccess: CovariantResult := cvCarSuccess; + + print nvCarSuccess, " ", cvCarSuccess, "\n"; // NonVariantResult.NVSuccess(_module.Car) CovariantResult.CVSuccess(_module.Car) + } +} + +// ----- Regression test ----- + +module Regression { + module M { + // A previous bug was that the following declaration was not exported correctly (in several compilers). + codatatype Stream = Next(shead: T, stail: Stream) + } + + function method CoUp(n: int, b: bool): M.Stream + { + 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 Test(){ + print CoUp(0, false), "\n"; + } +} diff --git a/Test/git-issues/git-issue-2013.dfy.expect b/Test/git-issues/git-issue-2013.dfy.expect new file mode 100644 index 00000000000..15a160ae382 --- /dev/null +++ b/Test/git-issues/git-issue-2013.dfy.expect @@ -0,0 +1,62 @@ + +Dafny program verifier finished with 12 verified, 0 errors + +Dafny program verifier did not attempt verification +16 +16 +Dt.Dt(12) Dt.Dt(30) Dt.Dt(30) +Result.Success(8) Result.Failure(_module.MyClassException) +{100} {100} {100} +{MoreTests_Compile.C} {MoreTests_Compile.C} {MoreTests_Compile.C} +MoreTests_Compile.Dt.Make(100) MoreTests_Compile.Dt.Make(100) MoreTests_Compile.Dt.Make(100) +MoreTests_Compile.DtCovariant.MakeCovariant(MoreTests_Compile.C) MoreTests_Compile.DtCovariant.MakeCovariant(MoreTests_Compile.C) MoreTests_Compile.DtCovariant.MakeCovariant(MoreTests_Compile.C) +Conveyance_Compile.NonVariantResult.NVSuccess(Conveyance_Compile.Car) Conveyance_Compile.CovariantResult.CVSuccess(Conveyance_Compile.Car) +Regression_mM_Compile.Stream.Next + +Dafny program verifier did not attempt verification +16 +16 +Dt.Dt(12) Dt.Dt(30) Dt.Dt(30) +Result.Success(8) Result.Failure(_module.MyClassException) +{100} {100} {100} +{MoreTests_Compile.C} {MoreTests_Compile.C} {MoreTests_Compile.C} +MoreTests_Compile.Dt.Make(100) MoreTests_Compile.Dt.Make(100) MoreTests_Compile.Dt.Make(100) +MoreTests_Compile.DtCovariant.MakeCovariant(MoreTests_Compile.C) MoreTests_Compile.DtCovariant.MakeCovariant(MoreTests_Compile.C) MoreTests_Compile.DtCovariant.MakeCovariant(MoreTests_Compile.C) +Conveyance_Compile.NonVariantResult.NVSuccess(Conveyance_Compile.Car) Conveyance_Compile.CovariantResult.CVSuccess(Conveyance_Compile.Car) +Regression_mM_Compile.Stream.Next + +Dafny program verifier did not attempt verification +16 +16 +Dt.Dt(12) Dt.Dt(30) Dt.Dt(30) +Result.Success(8) Result.Failure(_module.MyClassException) +{100} {100} {100} +{MoreTests_Compile.C} {MoreTests_Compile.C} {MoreTests_Compile.C} +MoreTests_Compile.Dt.Make(100) MoreTests_Compile.Dt.Make(100) MoreTests_Compile.Dt.Make(100) +MoreTests_Compile.DtCovariant.MakeCovariant(MoreTests_Compile.C) MoreTests_Compile.DtCovariant.MakeCovariant(MoreTests_Compile.C) MoreTests_Compile.DtCovariant.MakeCovariant(MoreTests_Compile.C) +Conveyance_Compile.NonVariantResult.NVSuccess(Conveyance_Compile.Car) Conveyance_Compile.CovariantResult.CVSuccess(Conveyance_Compile.Car) +Regression_mM_Compile.Stream.Next + +Dafny program verifier did not attempt verification +16 +16 +Dt.Dt(12) Dt.Dt(30) Dt.Dt(30) +Result.Success(8) Result.Failure(_module.MyClassException) +{100} {100} {100} +{MoreTests_Compile.C} {MoreTests_Compile.C} {MoreTests_Compile.C} +MoreTests_Compile.Dt.Make(100) MoreTests_Compile.Dt.Make(100) MoreTests_Compile.Dt.Make(100) +MoreTests_Compile.DtCovariant.MakeCovariant(MoreTests_Compile.C) MoreTests_Compile.DtCovariant.MakeCovariant(MoreTests_Compile.C) MoreTests_Compile.DtCovariant.MakeCovariant(MoreTests_Compile.C) +Conveyance_Compile.NonVariantResult.NVSuccess(Conveyance_Compile.Car) Conveyance_Compile.CovariantResult.CVSuccess(Conveyance_Compile.Car) +Regression_mM_Compile.Stream.Next + +Dafny program verifier did not attempt verification +16 +16 +Dt.Dt(12) Dt.Dt(30) Dt.Dt(30) +Result.Success(8) Result.Failure(_module.MyClassException) +{100} {100} {100} +{MoreTests_Compile.C} {MoreTests_Compile.C} {MoreTests_Compile.C} +MoreTests_Compile.Dt.Make(100) MoreTests_Compile.Dt.Make(100) MoreTests_Compile.Dt.Make(100) +MoreTests_Compile.DtCovariant.MakeCovariant(MoreTests_Compile.C) MoreTests_Compile.DtCovariant.MakeCovariant(MoreTests_Compile.C) MoreTests_Compile.DtCovariant.MakeCovariant(MoreTests_Compile.C) +Conveyance_Compile.NonVariantResult.NVSuccess(Conveyance_Compile.Car) Conveyance_Compile.CovariantResult.CVSuccess(Conveyance_Compile.Car) +Regression_mM_Compile.Stream.Next diff --git a/docs/dev/news/3072.feat b/docs/dev/news/3072.feat new file mode 100644 index 00000000000..b7228598a1e --- /dev/null +++ b/docs/dev/news/3072.feat @@ -0,0 +1 @@ +feat: support for traits as type arguments by fully allowing variance on datatypes in Java