From 50c2c99822f7ebe75ce23bab13d207dce5f57633 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Tue, 29 Nov 2022 08:44:50 -0800 Subject: [PATCH] feat: support for traits as type arguments with variance on datatypes in Java (#3072) This PR removes that pesky "not supported" error for Java where it wouldn't allow a `trait` to be passed in as a variant type parameter of a (co)datatype. Fixes #2013 The solution is pretty simple. Basically, it just emits casts when needed. To be accepted by Java's static type checker, these casts first upcast to `Object` and then downcast to the desired type. Since the JVM doesn't keep track of type parameters, it'll never know what hit it. (In particular, this means that we don't need the expensive `DowncastClone` mechanism that we're using for C# to satisfy .NET's more informed runtime.) To make it work, this PR also makes more precise the `IsTargetSupertype` method for Java. In particular, to check if `A` is a supertype of `B`, first keep converting the latter up the `trait` parents of `B` until it gets to `A` (if ever). This is already done for all the compilers. Call the result `A`. For the other compilers, one would now start to see if the parameters `X, Y` are target supertypes of `X', Y'` with variance in mind (for example, if the first type parameter is contravariant, we would actually check if `X'` is a supertype of `X`). For Java, however, we continue with variance in mind only if `A` is a collection type (because those already have run-time support for variance, using Java's bounded existential types). For non-collection types, we instead check if `X, Y` are target-type equal to `X', Y'`. If they are not, the compiler calls `EmitDowncast`. (To read these in the code, look at `EmitDowncastIfNecessary` in `SinglePassCompiler.cs`.) We could have used simple casts like this for collection types, too. But since I already have those, I left those alone. 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). Co-authored-by: Fabio Madge --- Source/DafnyCore/AST/Types.cs | 3 +- Source/DafnyCore/Compilers/Compiler-Csharp.cs | 10 +- Source/DafnyCore/Compilers/Compiler-go.cs | 3 +- Source/DafnyCore/Compilers/Compiler-java.cs | 39 ++-- .../DafnyCore/Compilers/SinglePassCompiler.cs | 14 +- Source/DafnyCore/Resolver/Resolver.cs | 4 +- Test/comp/DowncastClone.dfy | 4 +- Test/comp/DowncastClone.dfy.expect | 15 +- Test/comp/Variance.dfy | 3 +- Test/comp/Variance.dfy.expect | 20 +- Test/dafny0/RuntimeTypeTests0.dfy | 8 +- Test/dafny0/RuntimeTypeTests0.dfy.expect | 21 +- Test/git-issues/git-issue-1815.dfy | 20 +- Test/git-issues/git-issue-1815.dfy.expect | 10 +- Test/git-issues/git-issue-2013.dfy | 219 ++++++++++++++++++ Test/git-issues/git-issue-2013.dfy.expect | 62 +++++ docs/dev/news/3072.feat | 1 + 17 files changed, 385 insertions(+), 71 deletions(-) create mode 100644 Test/git-issues/git-issue-2013.dfy create mode 100644 Test/git-issues/git-issue-2013.dfy.expect create mode 100644 docs/dev/news/3072.feat 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