From 7e81f44475f0bfeb23bff4edeaa34cd0f1600900 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Mon, 8 Jul 2024 19:02:55 -0700 Subject: [PATCH] feat: Add bounded polymorphism (#5547) # Description This PR adds bounded polymorphism to the Dafny language. This feature allows any formal type parameter to be declared with a suffix of any number of ``` extends Type ``` clauses, where `Type` is any trait or subset type thereof. At call sites, the actual type arguments are checked to be subtypes of the listed type bounds. Where the formal type parameters are in scope, an expression whose type is the type parameter can be converted to a supertype of any of the type bounds by an explicit type conversion (`as`). In some cases, the type conversion is inferred automatically and can then be omitted from the program text. The feature requires `--type-system-refresh` for full functionality. Closes #5211 # Example For `test.dfy` being the program ``` dafny trait Printable { method Print() } method SelectPrintReturn(operateOnLeft: bool, left: T, right: T) returns (r: T) { r := if operateOnLeft then left else right; (r as Printable).Print(); } datatype Dt extends Printable = Dt(u: int) { method Print() { print u, "\n"; } } method Main() { var d0 := Dt(500); var d1 := Dt(702); var e0 := SelectPrintReturn(true, d0, d1); // 500 var e1 := SelectPrintReturn(false, d0, d1); // 702 print (d0, d1) == (d0, d1), "\n"; // true } ``` we get: ``` > dafny run test.dfy --type-system-refresh --general-traits=datatype Dafny program verifier finished with 3 verified, 0 errors 500 702 true ``` # Bonus The PR also * suppresses near-identical error messages (in particular, it reports only one error for conditions that split into several checks, like the type equality `A==B` which turns into both `A :> B` and `B >: A`) 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). --- Source/DafnyCore/AST/Cloner.cs | 2 +- .../Applications/MemberSelectExpr.cs | 3 +- .../DafnyCore/AST/Grammar/Printer/Printer.cs | 10 +- .../AST/TypeDeclarations/NonNullTypeDecl.cs | 8 +- .../AST/TypeDeclarations/SubsetTypeDecl.cs | 2 +- .../AST/TypeDeclarations/TopLevelDecl.cs | 4 +- .../TopLevelDeclWithMembers.cs | 4 +- Source/DafnyCore/AST/Types/TypeParameter.cs | 32 +- Source/DafnyCore/AST/Types/Types.cs | 10 +- Source/DafnyCore/AST/Types/UserDefinedType.cs | 4 +- .../Backends/CSharp/CsharpCodeGenerator.cs | 18 +- .../Backends/Dafny/DafnyCodeGenerator.cs | 2 +- .../Backends/GoLang/GoCodeGenerator.cs | 16 +- .../Backends/Java/JavaCodeGenerator.cs | 23 +- .../SinglePassCodeGenerator.Expression.cs | 7 +- .../SinglePassCodeGenerator.cs | 20 +- Source/DafnyCore/Dafny.atg | 53 +-- .../CheckTypeCharacteristics_Visitor.cs | 16 +- Source/DafnyCore/Resolver/ExpressionTester.cs | 7 +- Source/DafnyCore/Resolver/ModuleResolver.cs | 122 +++++- .../NameResolutionAndTypeInference.cs | 5 +- .../Resolver/PreType/PreTypeConstraints.cs | 12 + .../PreType/PreTypeResolve.Expressions.cs | 14 + .../PreType/PreTypeResolve.Statements.cs | 21 +- .../Resolver/PreType/PreTypeResolve.cs | 26 +- .../PreType/PreTypeSubtypeConstraint.cs | 2 +- .../DafnyCore/Resolver/ResolutionContext.cs | 4 +- Source/DafnyCore/Resolver/TypeConstraint.cs | 4 +- .../DafnyCore/Rewriters/RefinementErrors.cs | 2 + .../Rewriters/RefinementTransformer.cs | 26 +- .../BoogieGenerator.ExpressionTranslator.cs | 8 +- .../BoogieGenerator.ExpressionWellformed.cs | 4 +- .../Verifier/BoogieGenerator.Fields.cs | 5 + .../Verifier/BoogieGenerator.Functions.cs | 16 +- .../Verifier/BoogieGenerator.Methods.cs | 50 +++ .../Verifier/BoogieGenerator.TrStatement.cs | 8 +- .../Verifier/BoogieGenerator.Types.cs | 13 +- Source/DafnyCore/Verifier/BoogieGenerator.cs | 14 +- .../DafnyRuntimeGo/dafny/dafnyFromDafny.go | 70 ++-- .../LitTest/dafny0/AsIs-Resolve.dfy.expect | 9 +- .../dafny0/BoundedPolymorphismCompilation.dfy | 331 +++++++++++++++ .../BoundedPolymorphismCompilation.dfy.expect | 14 + ...oundedPolymorphismCompilation.dfy.rs.check | 1 + .../dafny0/BoundedPolymorphismResolution.dfy | 325 +++++++++++++++ .../BoundedPolymorphismResolution.dfy.expect | 84 ++++ ...dPolymorphismResolution.dfy.refresh.expect | 56 +++ .../BoundedPolymorphismVerification.dfy | 392 ++++++++++++++++++ ...BoundedPolymorphismVerification.dfy.expect | 16 + .../LitTest/dafny0/LiberalEquality.dfy.expect | 8 +- .../LitTest/dafny0/PrettyPrinting.dfy | 30 ++ .../LitTest/dafny0/PrettyPrinting.dfy.expect | 40 ++ .../dafny0/ResolutionErrors2.dfy.expect | 3 +- .../LitTest/dafny4/Bug140.dfy.rs.check | 2 +- .../git-issues/git-issue-1637.dfy.expect | 3 +- .../LitTest/git-issues/git-issue-5570.dfy | 30 ++ .../git-issues/git-issue-5570.dfy.expect | 2 + .../git-issues/git-issue-697j.dfy.rs.check | 2 +- docs/HowToFAQ/Errors-Refinement.md | 26 ++ 58 files changed, 1854 insertions(+), 187 deletions(-) create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BoundedPolymorphismCompilation.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BoundedPolymorphismCompilation.dfy.expect create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BoundedPolymorphismCompilation.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BoundedPolymorphismResolution.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BoundedPolymorphismResolution.dfy.expect create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BoundedPolymorphismResolution.dfy.refresh.expect create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BoundedPolymorphismVerification.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BoundedPolymorphismVerification.dfy.expect create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5570.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5570.dfy.expect diff --git a/Source/DafnyCore/AST/Cloner.cs b/Source/DafnyCore/AST/Cloner.cs index 0726f4831a..fcceee4356 100644 --- a/Source/DafnyCore/AST/Cloner.cs +++ b/Source/DafnyCore/AST/Cloner.cs @@ -194,7 +194,7 @@ public DatatypeCtor CloneCtor(DatatypeCtor ct) { public TypeParameter CloneTypeParam(TypeParameter tp) { return (TypeParameter)typeParameterClones.GetOrCreate(tp, () => new TypeParameter(Range(tp.RangeToken), tp.NameNode.Clone(this), tp.VarianceSyntax, - CloneTPChar(tp.Characteristics))); + CloneTPChar(tp.Characteristics), tp.TypeBounds.ConvertAll(CloneType))); } public virtual MemberDecl CloneMember(MemberDecl member, bool isReference) { diff --git a/Source/DafnyCore/AST/Expressions/Applications/MemberSelectExpr.cs b/Source/DafnyCore/AST/Expressions/Applications/MemberSelectExpr.cs index c546405b9f..f98620fddd 100644 --- a/Source/DafnyCore/AST/Expressions/Applications/MemberSelectExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Applications/MemberSelectExpr.cs @@ -238,7 +238,6 @@ public MemberSelectExpr(IToken tok, Expression obj, Field field) var receiverType = obj.Type.NormalizeExpand(); this.TypeApplication_AtEnclosingClass = receiverType.TypeArgs; this.TypeApplication_JustMember = new List(); - this.ResolvedOutparameterTypes = new List(); var typeMap = new Dictionary(); if (receiverType is UserDefinedType udt) { @@ -299,4 +298,4 @@ public IEnumerable GetReferences() { } public IToken NavigationToken => tok; -} \ No newline at end of file +} diff --git a/Source/DafnyCore/AST/Grammar/Printer/Printer.cs b/Source/DafnyCore/AST/Grammar/Printer/Printer.cs index 8ed0acedbe..0eef9a9e4d 100644 --- a/Source/DafnyCore/AST/Grammar/Printer/Printer.cs +++ b/Source/DafnyCore/AST/Grammar/Printer/Printer.cs @@ -290,7 +290,7 @@ public void PrintTopLevelDecls(CompilationData compilation, IEnumerable()); + PrintClassMethodHelper("newtype", dd.Attributes, dd.Name, dd.TypeArgs); PrintExtendsClause(dd); wr.Write(" = "); if (dd.Var == null) { @@ -663,7 +663,7 @@ public void PrintClass(ClassLikeDecl c, int indent, string fileBeingPrinted) { Contract.Requires(c != null); Indent(indent); - PrintClassMethodHelper((c is TraitDecl) ? "trait" : "class", c.Attributes, c.Name, c.TypeArgs); + PrintClassMethodHelper(c is TraitDecl ? "trait" : "class", c.Attributes, c.Name, c.TypeArgs); if (c.IsRefining) { wr.Write(" ..."); } else { @@ -795,7 +795,11 @@ public string TypeParamString(TypeParameter tp) { Contract.Assert(false); // unexpected VarianceSyntax throw new cce.UnreachableException(); } - return variance + tp.Name + TPCharacteristicsSuffix(tp.Characteristics); + var paramString = variance + tp.Name + TPCharacteristicsSuffix(tp.Characteristics); + foreach (var typeBound in tp.TypeBounds) { + paramString += $" extends {typeBound.TypeName(options, null, true)}"; + } + return paramString; } private void PrintArrowType(string arrow, string internalName, List typeArgs) { diff --git a/Source/DafnyCore/AST/TypeDeclarations/NonNullTypeDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/NonNullTypeDecl.cs index 4ec1f51275..f3f735ccef 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/NonNullTypeDecl.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/NonNullTypeDecl.cs @@ -13,7 +13,7 @@ public class NonNullTypeDecl : SubsetTypeDecl { /// in order to build values that depend on previously computed parameters. /// public NonNullTypeDecl(ClassLikeDecl cl) - : this(cl, cl.TypeArgs.ConvertAll(tp => new TypeParameter(tp.RangeToken, tp.NameNode, tp.VarianceSyntax, tp.Characteristics))) { + : this(cl, TypeParameter.CloneTypeParameters(cl.TypeArgs)) { Contract.Requires(cl != null); } @@ -34,10 +34,10 @@ private NonNullTypeDecl(ClassLikeDecl cl, List tps, BoundVar id) Class = cl; } - public override List ParentTypes(List typeArgs) { - List result = new List(base.ParentTypes(typeArgs)); + public override List ParentTypes(List typeArgs, bool includeTypeBounds) { + List result = new List(base.ParentTypes(typeArgs, includeTypeBounds)); - foreach (var rhsParentType in Class.ParentTypes(typeArgs)) { + foreach (var rhsParentType in Class.ParentTypes(typeArgs, includeTypeBounds)) { var rhsParentUdt = (UserDefinedType)rhsParentType; // all parent types of .Class are expected to be possibly-null class types Contract.Assert(rhsParentUdt.ResolvedClass is TraitDecl); result.Add(UserDefinedType.CreateNonNullTypeIfReferenceType(rhsParentUdt)); diff --git a/Source/DafnyCore/AST/TypeDeclarations/SubsetTypeDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/SubsetTypeDecl.cs index f9d0970a25..15c2a5a2e8 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/SubsetTypeDecl.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/SubsetTypeDecl.cs @@ -54,7 +54,7 @@ public SubsetTypeDecl(RangeToken rangeToken, Name name, TypeParameter.TypeParame WKind RedirectingTypeDecl.WitnessKind => WitnessKind; Expression RedirectingTypeDecl.Witness => Witness; - public override List ParentTypes(List typeArgs) { + public override List ParentTypes(List typeArgs, bool includeTypeBounds) { return new List { RhsWithArgument(typeArgs) }; } public bool ShouldVerify => true; // This could be made more accurate diff --git a/Source/DafnyCore/AST/TypeDeclarations/TopLevelDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/TopLevelDecl.cs index 79b485c04e..6eafb30f1f 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/TopLevelDecl.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/TopLevelDecl.cs @@ -98,8 +98,10 @@ public TopLevelDecl ViewAsClass { /// class C extends J /// C.ParentTypes(real) = J // non-null types C and J /// C?.ParentTypes(real) = J? // possibly-null type C? and J? + /// + /// If "includeTypeBounds" is "true", then for a type parameter, ParentTypes() returns the type bounds. /// - public virtual List ParentTypes(List typeArgs) { + public virtual List ParentTypes(List typeArgs, bool includeTypeBounds) { Contract.Requires(typeArgs != null); Contract.Requires(this.TypeArgs.Count == typeArgs.Count); return new List(); diff --git a/Source/DafnyCore/AST/TypeDeclarations/TopLevelDeclWithMembers.cs b/Source/DafnyCore/AST/TypeDeclarations/TopLevelDeclWithMembers.cs index e83436c2db..52c691164a 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/TopLevelDeclWithMembers.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/TopLevelDeclWithMembers.cs @@ -104,7 +104,7 @@ public void SetMembersBeforeResolution() { MembersBeforeResolution = Members.ToImmutableList(); } - public List RawTraitsWithArgument(List typeArgs) { + private List RawTraitsWithArgument(List typeArgs) { Contract.Requires(typeArgs != null); Contract.Requires(typeArgs.Count == TypeArgs.Count); // Instantiate with the actual type arguments @@ -115,7 +115,7 @@ public List RawTraitsWithArgument(List typeArgs) { }); } - public override List ParentTypes(List typeArgs) { + public override List ParentTypes(List typeArgs, bool includeTypeBounds) { return RawTraitsWithArgument(typeArgs); } diff --git a/Source/DafnyCore/AST/Types/TypeParameter.cs b/Source/DafnyCore/AST/Types/TypeParameter.cs index 1e5548ffc2..9faeb2dcef 100644 --- a/Source/DafnyCore/AST/Types/TypeParameter.cs +++ b/Source/DafnyCore/AST/Types/TypeParameter.cs @@ -171,16 +171,30 @@ public bool SupportsEquality { } public int PositionalIndex; // which type parameter this is (ie. in C, S is 0, T is 1 and U is 2). - public TypeParameter(RangeToken rangeToken, Name name, TPVarianceSyntax varianceS, TypeParameterCharacteristics characteristics) + public readonly List TypeBounds; + + public IEnumerable TypeBoundHeads { + get { + foreach (var typeBound in TypeBounds) { + if (typeBound is UserDefinedType { ResolvedClass: { } parentDecl }) { + yield return parentDecl; + } + } + } + } + + public TypeParameter(RangeToken rangeToken, Name name, TPVarianceSyntax varianceS, TypeParameterCharacteristics characteristics, + List typeBounds) : base(rangeToken, name, null, new List(), null, false) { Contract.Requires(rangeToken != null); Contract.Requires(name != null); Characteristics = characteristics; VarianceSyntax = varianceS; + TypeBounds = typeBounds; } public TypeParameter(RangeToken rangeToken, Name name, TPVarianceSyntax varianceS) - : this(rangeToken, name, varianceS, new TypeParameterCharacteristics(false)) { + : this(rangeToken, name, varianceS, new TypeParameterCharacteristics(false), new List()) { Contract.Requires(rangeToken != null); Contract.Requires(name != null); } @@ -191,6 +205,17 @@ public TypeParameter(RangeToken tok, Name name, int positionalIndex, ParentType Parent = parent; } + /// + /// Return a list of unresolved clones of the type parameters in "typeParameters". + /// + public static List CloneTypeParameters(List typeParameters) { + var cloner = new Cloner(); + return typeParameters.ConvertAll(tp => { + var typeBounds = tp.TypeBounds.ConvertAll(cloner.CloneType); + return new TypeParameter(tp.RangeToken, tp.NameNode, tp.VarianceSyntax, tp.Characteristics, typeBounds); + }); + } + public override string FullName { get { // when debugging, print it all: @@ -231,4 +256,7 @@ public static Dictionary SubstitutionMap(List ParentTypes(List typeArgs, bool includeTypeBounds) { + return includeTypeBounds ? TypeBounds : new List(); + } } \ No newline at end of file diff --git a/Source/DafnyCore/AST/Types/Types.cs b/Source/DafnyCore/AST/Types/Types.cs index 22317360fd..1995098912 100644 --- a/Source/DafnyCore/AST/Types/Types.cs +++ b/Source/DafnyCore/AST/Types/Types.cs @@ -1665,7 +1665,7 @@ public bool ContainsProxy(TypeProxy proxy) { } } - public virtual List ParentTypes() { + public virtual List ParentTypes(bool includeTypeBounds) { return new List(); } @@ -1692,7 +1692,13 @@ public virtual bool IsSubtypeOf(Type super, bool ignoreTypeArguments, bool ignor return ignoreTypeArguments || CompatibleTypeArgs(super, sub); } - return sub.ParentTypes().Any(parentType => parentType.IsSubtypeOf(super, ignoreTypeArguments, ignoreNullity)); + // There is a special case, namely when super is the non-null "object". Since "sub.ParentTypes()" only gives + // back the explicitly declared parent traits, the general case below may miss it. + if (super.IsObject) { + return sub.IsNonNullRefType; + } + + return sub.ParentTypes(true).Any(parentType => parentType.IsSubtypeOf(super, ignoreTypeArguments, ignoreNullity)); } public static bool CompatibleTypeArgs(Type super, Type sub) { diff --git a/Source/DafnyCore/AST/Types/UserDefinedType.cs b/Source/DafnyCore/AST/Types/UserDefinedType.cs index cc97c154dc..f0fd965e16 100644 --- a/Source/DafnyCore/AST/Types/UserDefinedType.cs +++ b/Source/DafnyCore/AST/Types/UserDefinedType.cs @@ -503,8 +503,8 @@ public override bool ComputeMayInvolveReferences(ISet visitedDatat return true; } - public override List ParentTypes() { - return ResolvedClass != null ? ResolvedClass.ParentTypes(TypeArgs) : base.ParentTypes(); + public override List ParentTypes(bool includeTypeBounds) { + return ResolvedClass != null ? ResolvedClass.ParentTypes(TypeArgs, includeTypeBounds) : base.ParentTypes(includeTypeBounds); } public override bool IsSubtypeOf(Type super, bool ignoreTypeArguments, bool ignoreNullity) { diff --git a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs index bb16e29127..076c247c6d 100644 --- a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs +++ b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs @@ -2748,18 +2748,24 @@ protected override void EmitIndexCollectionSelect(Expression source, Expression protected override void EmitIndexCollectionUpdate(Expression source, Expression index, Expression value, CollectionType resultCollectionType, bool inLetExprBody, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) { - if (resultCollectionType is SeqType or MapType) { + if (resultCollectionType is SeqType) { wr.Write(TypeHelperName(resultCollectionType, wr, source.tok) + ".Update"); wr.Append(ParensList( Expr(source, inLetExprBody, wStmts), Expr(index, inLetExprBody, wStmts), CoercedExpr(value, resultCollectionType.ValueArg, inLetExprBody, wStmts))); + } else if (resultCollectionType is MapType resultMapType) { + wr.Write(TypeHelperName(resultCollectionType, wr, source.tok) + ".Update"); + wr.Append(ParensList( + Expr(source, inLetExprBody, wStmts), + CoercedExpr(index, resultMapType.Domain, inLetExprBody, wStmts), + CoercedExpr(value, resultMapType.Range, inLetExprBody, wStmts))); } else { TrParenExpr(source, wr, inLetExprBody, wStmts); wr.Write(".Update"); wr.Append(ParensList( - Expr(index, inLetExprBody, wStmts), - CoercedExpr(value, resultCollectionType.ValueArg, inLetExprBody, wStmts))); + CoercedExpr(index, resultCollectionType.ValueArg, inLetExprBody, wStmts), + Expr(value, inLetExprBody, wStmts))); } } @@ -2890,12 +2896,14 @@ protected override ConcreteSyntaxTree ToFatPointer(Type type, ConcreteSyntaxTree protected override ConcreteSyntaxTree EmitDowncast(Type from, Type to, IToken tok, ConcreteSyntaxTree wr) { from = from.NormalizeExpand(); to = to.NormalizeExpand(); - Contract.Assert(Options.Get(CommonOptionBag.GeneralTraits) != CommonOptionBag.GeneralTraitsOptions.Legacy || from.IsRefType == to.IsRefType); + Contract.Assert(Options.Get(CommonOptionBag.GeneralTraits) != CommonOptionBag.GeneralTraitsOptions.Legacy || + from.IsRefType == to.IsRefType || + (from.IsTypeParameter && to.IsTraitType)); var w = new ConcreteSyntaxTree(); if (from.IsTraitType && to.AsNewtype != null) { wr.Format($"(({to.AsNewtype.GetFullCompileName(Options)})({w}))"); - } else if (to.IsRefType || to.IsTraitType || from.IsTraitType) { + } else if (to.IsRefType || to.IsTraitType || from.IsTraitType || to.IsTypeParameter) { wr.Format($"(({TypeName(to, wr, tok)})({w}))"); } else { Contract.Assert(Type.SameHead(from, to)); diff --git a/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs b/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs index 0bb731ae39..ec1c5d5ae6 100644 --- a/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs +++ b/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs @@ -168,7 +168,7 @@ protected override ConcreteSyntaxTree EmitCoercionIfNecessary(Type from, Type to to = toNonNull.RhsWithArgument(toUdt.TypeArgs); } - return EmitCoercionIfNecessary(from, to, tok, new BuilderSyntaxTree(nullConvert, this)); + return base.EmitCoercionIfNecessary(from, to, tok, new BuilderSyntaxTree(nullConvert, this)); } else { return base.EmitCoercionIfNecessary(from, to, tok, wr); } diff --git a/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs b/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs index a8007611a2..10616daf19 100644 --- a/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs +++ b/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs @@ -2488,6 +2488,10 @@ private string IdName(Declaration decl) { protected override string PrefixForForcedCapitalization => "Go_"; + public override Type ResultTypeAsViewedByFunctionBody(Function f) { + return f.Original.ResultType; + } + protected override string IdMemberName(MemberSelectExpr mse) { return Capitalize(mse.MemberName); } @@ -3899,7 +3903,7 @@ protected override ConcreteSyntaxTree EmitCoercionIfNecessary(Type/*?*/ from, Ty } else if (to.IsTypeParameter || (from != null && EqualsUpToParameters(from, to))) { // do nothing return wr; - } else if (from != null && from.IsSubtypeOf(to, true, true)) { + } else if (from != null && !from.IsTypeParameter && from.IsSubtypeOf(to, true, true)) { // upcast return wr; } else if (from == null || from.IsTypeParameter || to.IsSubtypeOf(from, true, true)) { @@ -3934,6 +3938,16 @@ protected override ConcreteSyntaxTree EmitCoercionIfNecessary(Type/*?*/ from, Ty } } + protected override ConcreteSyntaxTree EmitDowncast(Type from, Type to, IToken tok, ConcreteSyntaxTree wr) { + if (to.IsTraitType) { + wr.Write("{0}.CastTo_(", TypeName_Companion(to.AsTraitType, wr, tok)); + var w = wr.Fork(); + wr.Write(")"); + return w; + } + return base.EmitDowncast(from, to, tok, wr); + } + protected override ConcreteSyntaxTree EmitCoercionToNativeInt(ConcreteSyntaxTree wr) { var w = wr.Fork(); wr.Write(".(int)"); diff --git a/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs b/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs index 8fd4afa98c..465fc2bad3 100644 --- a/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs +++ b/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs @@ -1697,11 +1697,10 @@ protected override void EmitIndexCollectionSelect(Expression source, Expression ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) { // Taken from C# compiler, assuming source is a DafnySequence type. if (source.Type.NormalizeToAncestorType().AsMultiSetType is { } multiSetType) { - wr = EmitCoercionIfNecessary(from: NativeObjectType, to: Type.Int, tok: source.tok, wr: wr); wr.Write($"{DafnyMultiSetClass}.<{BoxedTypeName(multiSetType.Arg, wr, Token.NoToken)}>multiplicity("); TrParenExpr(source, wr, inLetExprBody, wStmts); wr.Write(", "); - wr.Append(Expr(index, inLetExprBody, wStmts)); + wr.Append(JavaCoercedExpr(index, multiSetType.Arg, inLetExprBody, wStmts)); wr.Write(")"); } else if (source.Type.NormalizeToAncestorType().AsMapType is { } mapType) { wr = EmitCoercionIfNecessary(from: NativeObjectType, to: mapType.Range, tok: source.tok, wr: wr); @@ -1731,21 +1730,31 @@ protected override void EmitIndexCollectionUpdate(Expression source, Expression wr.Append(Expr(source, inLetExprBody, wStmts)); wr.Write(", "); TrExprAsInt(index, wr, inLetExprBody, wStmts); + wr.Write(", "); + wr.Append(JavaCoercedExpr(value, resultCollectionType.ValueArg, inLetExprBody, wStmts)); + wr.Write(")"); } else if (resultCollectionType.AsMapType is { } mapType) { wr.Write($"{DafnyMapClass}.<{BoxedTypeName(mapType.Domain, wr, Token.NoToken)}, {BoxedTypeName(mapType.Range, wr, Token.NoToken)}>update("); wr.Append(Expr(source, inLetExprBody, wStmts)); wr.Write(", "); - wr.Append(Expr(index, inLetExprBody, wStmts)); + wr.Append(JavaCoercedExpr(index, mapType.Domain, inLetExprBody, wStmts)); + wr.Write(", "); + wr.Append(JavaCoercedExpr(value, mapType.Range, inLetExprBody, wStmts)); + wr.Write(")"); } else { Contract.Assert(resultCollectionType.AsMultiSetType != null); wr.Write($"{DafnyMultiSetClass}.<{BoxedTypeName(resultCollectionType.Arg, wr, Token.NoToken)}>update("); wr.Append(Expr(source, inLetExprBody, wStmts)); wr.Write(", "); - wr.Append(Expr(index, inLetExprBody, wStmts)); + wr.Append(JavaCoercedExpr(index, resultCollectionType.ValueArg, inLetExprBody, wStmts)); + wr.Write(", "); + wr.Append(Expr(value, inLetExprBody, wStmts)); + wr.Write(")"); } - wr.Write(", "); - wr.Append(CoercedExpr(value, NativeObjectType, inLetExprBody, wStmts)); - wr.Write(")"); + } + + private ConcreteSyntaxTree JavaCoercedExpr(Expression expr, Type toType, bool inLetExprBody, ConcreteSyntaxTree wStmts) { + return CoercedExpr(expr, expr.Type.IsTypeParameter ? toType : NativeObjectType, inLetExprBody, wStmts); } protected override void EmitRotate(Expression e0, Expression e1, bool isRotateLeft, ConcreteSyntaxTree wr, diff --git a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Expression.cs b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Expression.cs index 654a5af662..ee1742881e 100644 --- a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Expression.cs +++ b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Expression.cs @@ -290,11 +290,16 @@ void EmitExpr(Expression e2, ConcreteSyntaxTree wr2, bool inLetExpr, ConcreteSyn var fromType = e.E.Type.GetRuntimeType(); var toType = e.ToType.GetRuntimeType(); Contract.Assert(Options.Get(CommonOptionBag.GeneralTraits) != CommonOptionBag.GeneralTraitsOptions.Legacy || - toType.IsRefType == fromType.IsRefType); + toType.IsRefType == fromType.IsRefType || + (fromType.IsTypeParameter && toType.IsTraitType)); if (toType.IsRefType || toType.IsTraitType || fromType.IsTraitType) { var w = EmitCoercionIfNecessary(e.E.Type, e.ToType, e.tok, wr); w = EmitDowncastIfNecessary(e.E.Type, e.ToType, e.tok, w); EmitExpr(e.E, inLetExprBody, w, wStmts); + } else if (e.E.Type.IsSubtypeOf(e.ToType, false, false)) { + // conversion is a no-op -- almost, because it may need a cast to deal with bounded type parameters + var w = EmitDowncastIfNecessary(e.E.Type, e.ToType, e.tok, wr); + EmitExpr(e.E, inLetExprBody, w, wStmts); } else { EmitConversionExpr(e.E, fromType, toType, inLetExprBody, wr, wStmts); } diff --git a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs index 7ad99fe4a9..f47502681b 100644 --- a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs +++ b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs @@ -576,7 +576,9 @@ protected virtual void EmitSetterParameter(ConcreteSyntaxTree wr) { protected virtual void EmitReturnExpr(Expression expr, Type resultType, bool inLetExprBody, ConcreteSyntaxTree wr) { // emits "return ;" for function bodies var wStmts = wr.Fork(); var w = EmitReturnExpr(wr); - EmitExpr(expr, inLetExprBody, EmitCoercionIfNecessary(expr.Type, resultType, null, w), wStmts); + w = EmitCoercionIfNecessary(expr.Type, resultType, expr.tok, w); + w = EmitDowncastIfNecessary(expr.Type, resultType, expr.tok, w); + EmitExpr(expr, inLetExprBody, w, wStmts); } protected virtual void EmitReturnExpr(string returnExpr, ConcreteSyntaxTree wr) { // emits "return ;" for function bodies var w = EmitReturnExpr(wr); @@ -936,7 +938,7 @@ public bool IsTargetSupertype(Type to, Type from, bool typeEqualityOnly = false) } else if (to.IsObjectQ) { return true; } else { - return from.ParentTypes().Any(fromParentType => IsTargetSupertype(to, fromParentType)); + return from.ParentTypes(false).Any(fromParentType => IsTargetSupertype(to, fromParentType)); } } @@ -2746,12 +2748,16 @@ private void CompileFunction(Function f, IClassWriter cw, bool lookasideBody) { Coverage.Instrument(f.Body.tok, $"entry to function {f.FullName}", w); Contract.Assert(enclosingFunction == null); enclosingFunction = f; - CompileReturnBody(f.Body, f.Original.ResultType, w, accVar); + CompileReturnBody(f.Body, ResultTypeAsViewedByFunctionBody(f), w, accVar); Contract.Assert(enclosingFunction == f); enclosingFunction = null; } } + public virtual Type ResultTypeAsViewedByFunctionBody(Function f) { + return f.ResultType; + } + public const string STATIC_ARGS_NAME = "args"; private void CompileMethod(Program program, Method m, IClassWriter cw, bool lookasideBody) { @@ -2869,6 +2875,7 @@ void TrCasePatternOpt(CasePattern pat, Expression rhs, Action = Name . -GenericParameters<.List/*!*/ typeArgs, bool allowVariance.> -= (. Contract.Requires(cce.NonNullElements(typeArgs)); - TypeParameter.TypeParameterCharacteristics characteristics; - TypeParameter.TPVarianceSyntax variance = TypeParameter.TPVarianceSyntax.NonVariant_Strict; // assignment is to please compiler - characteristics = new TypeParameter.TypeParameterCharacteristics(false); - - Name name; - .) +GenericParameters<.List typeParameters, bool allowVariance.> += (. Contract.Requires(cce.NonNullElements(typeParameters)); .) // If a "<" combined with a Variance symbol could be a new token, then the parser here will need to be more complex, // since, for example, a < followed immediately by a Variance symbol would scan as the wrong token. // Fortunately that is not currently the case. // (Only because we parse the new "<-" symbol as separate "<" "-" tokens precisely to avoid this issue :) - "<" (. IToken startToken = t.Next; .) - [ Variance (. - if (!allowVariance) { SemErr(ErrorId.p_type_parameter_variance_forbidden, t, "type-parameter variance is not allowed to be specified in this context"); } - .) + "<" + OneTypeParameter + { "," + OneTypeParameter + } + ">" + . + +OneTypeParameter<.List typeParameters, bool allowVariance.> += (. var variance = TypeParameter.TPVarianceSyntax.NonVariant_Strict; // assignment is to please compiler + var characteristics = new TypeParameter.TypeParameterCharacteristics(false); + Name name; + Type typeBound; + var typeBounds = new List(); + var startToken = t.Next; + .) + [ Variance + (. if (!allowVariance) { + SemErr(ErrorId.p_type_parameter_variance_forbidden, t, "type-parameter variance is not allowed to be specified in this context"); + } + .) ] TypeVariableName { TypeParameterCharacteristics } - (. typeArgs.Add(new TypeParameter(new RangeToken(startToken, t), name, variance, characteristics)); .) - { "," - (. variance = TypeParameter.TPVarianceSyntax.NonVariant_Strict; - characteristics = new TypeParameter.TypeParameterCharacteristics(false); - startToken = t.Next; - .) - [ Variance (. - if (!allowVariance) { SemErr(ErrorId.p_type_parameter_variance_forbidden, t, "type-parameter variance is not allowed to be specified in this context"); } - .) - ] - TypeVariableName - { TypeParameterCharacteristics } - (. typeArgs.Add(new TypeParameter(new RangeToken(startToken, t), name, variance, characteristics)); .) + { "extends" + Type + (. typeBounds.Add(typeBound); .) } - ">" + (. typeParameters.Add(new TypeParameter(new RangeToken(startToken, t), name, variance, characteristics, typeBounds)); .) . /*------------------------------------------------------------------------*/ diff --git a/Source/DafnyCore/Resolver/CheckTypeCharacteristics_Visitor.cs b/Source/DafnyCore/Resolver/CheckTypeCharacteristics_Visitor.cs index b183a06771..e9c14c057b 100644 --- a/Source/DafnyCore/Resolver/CheckTypeCharacteristics_Visitor.cs +++ b/Source/DafnyCore/Resolver/CheckTypeCharacteristics_Visitor.cs @@ -280,7 +280,7 @@ bool VisitPattern(CasePattern pat, bool patternGhostContext) { public void VisitType(IToken tok, Type type, bool inGhostContext) { Contract.Requires(tok != null); Contract.Requires(type != null); - type = type.Normalize(); // we only do a .Normalize() here, because we want to keep stop at any type synonym or subset type + type = type.Normalize(); // we only do a .Normalize() here, because we want to stop at any type synonym or subset type if (type is BasicType) { // fine } else if (type is SetType) { @@ -332,14 +332,24 @@ void CheckTypeInstantiation(IToken tok, string what, string className, List rtd.tok, rtd => rtd.Name, "cycle among redirecting types (newtypes, subset types, type synonyms)"); } } + private void ResolveAllTypeParameterBounds(List declarations) { + foreach (var decl in declarations) { + allTypeParameters.PushMarker(); + ResolveTypeParameterBounds(decl.tok, decl.TypeArgs, decl as ICodeContext ?? new NoContext(decl.EnclosingModuleDefinition)); + if (decl is TopLevelDeclWithMembers topLevelDeclWithMembers) { + foreach (var member in topLevelDeclWithMembers.Members) { + if (member is Function function) { + var ec = reporter.Count(ErrorLevel.Error); + allTypeParameters.PushMarker(); + ResolveTypeParameterBounds(function.tok, function.TypeArgs, function); + allTypeParameters.PopMarker(); + if (reporter.Count(ErrorLevel.Error) == ec && function is ExtremePredicate { PrefixPredicate: { } prefixPredicate }) { + allTypeParameters.PushMarker(); + ResolveTypeParameterBounds(prefixPredicate.tok, prefixPredicate.TypeArgs, prefixPredicate); + allTypeParameters.PopMarker(); + } + } else if (member is Method m) { + var ec = reporter.Count(ErrorLevel.Error); + allTypeParameters.PushMarker(); + ResolveTypeParameterBounds(m.tok, m.TypeArgs, m); + allTypeParameters.PopMarker(); + if (reporter.Count(ErrorLevel.Error) == ec && m is ExtremeLemma { PrefixLemma: { } prefixLemma }) { + allTypeParameters.PushMarker(); + ResolveTypeParameterBounds(prefixLemma.tok, prefixLemma.TypeArgs, prefixLemma); + allTypeParameters.PopMarker(); + } + } + } + } + allTypeParameters.PopMarker(); + } + } + + /// + /// This method pushes the typeParameters to "allTypeParameters" (reporting no errors for any duplicates) and then + /// type checks the type-bound types of each type parameter. + /// As a side effect, this method leaves "allTypeParameters" in the state after the pushes. + /// + void ResolveTypeParameterBounds(IToken tok, List typeParameters, ICodeContext context) { + foreach (var typeParameter in typeParameters) { + allTypeParameters.Push(typeParameter.Name, typeParameter); + } + foreach (var typeParameter in typeParameters) { + foreach (var typeBound in typeParameter.TypeBounds) { + var prevErrorCount = reporter.ErrorCount; + ResolveType(tok, typeBound, context, ResolveTypeOptionEnum.DontInfer, null); + if (reporter.ErrorCount == prevErrorCount && !typeBound.IsTraitType) { + reporter.Error(MessageSource.Resolver, tok, $"type bound must be a trait or a subset type based on a trait (got {typeBound})"); + } + } + } + } + public static readonly List NativeTypes = new List() { new NativeType("byte", 0, 0x100, 8, NativeType.Selection.Byte), new NativeType("sbyte", -0x80, 0x80, 0, NativeType.Selection.SByte), @@ -2462,7 +2518,8 @@ public void CheckOverride_MethodParameters(Method nw, Method old, Dictionary CheckOverride_TypeParameters(IToken tok, List old, List nw, string name, string thing, Dictionary classTypeMap) { + private Dictionary CheckOverride_TypeParameters(IToken tok, List old, List nw, + string name, string thing, Dictionary classTypeMap) { Contract.Requires(tok != null); Contract.Requires(old != null); Contract.Requires(nw != null); @@ -2473,28 +2530,63 @@ private Dictionary CheckOverride_TypeParameters(IToken tok, reporter.Error(MessageSource.Resolver, tok, "{0} '{1}' is declared with a different number of type parameters ({2} instead of {3}) than in the overridden {0}", thing, name, nw.Count, old.Count); } else { - for (int i = 0; i < old.Count; i++) { + var checkNames = old.Concat(nw).Any(typeParameter => typeParameter.TypeBounds.Count != 0); + for (var i = 0; i < old.Count; i++) { var o = old[i]; var n = nw[i]; typeMap.Add(o, new UserDefinedType(tok, n)); - // Check type characteristics - if (o.Characteristics.EqualitySupport != TypeParameter.EqualitySupportValue.InferredRequired && o.Characteristics.EqualitySupport != n.Characteristics.EqualitySupport) { - reporter.Error(MessageSource.Resolver, n.tok, "type parameter '{0}' is not allowed to change the requirement of supporting equality", n.Name); - } - if (o.Characteristics.HasCompiledValue != n.Characteristics.HasCompiledValue) { - reporter.Error(MessageSource.Resolver, n.tok, "type parameter '{0}' is not allowed to change the requirement of supporting auto-initialization", n.Name); - } else if (o.Characteristics.IsNonempty != n.Characteristics.IsNonempty) { - reporter.Error(MessageSource.Resolver, n.tok, "type parameter '{0}' is not allowed to change the requirement of being nonempty", n.Name); - } - if (o.Characteristics.ContainsNoReferenceTypes != n.Characteristics.ContainsNoReferenceTypes) { - reporter.Error(MessageSource.Resolver, n.tok, "type parameter '{0}' is not allowed to change the no-reference-type requirement", n.Name); + if (checkNames && o.Name != n.Name) { // if checkNames is false, then just treat the parameters positionally. + reporter.Error(MessageSource.Resolver, n.tok, + $"type parameters in this {thing} override are not allowed to be renamed from the names given in the the {thing} it overrides" + + $" (expected '{o.Name}', got '{n.Name}')"); + } else { + // Check type characteristics + if (o.Characteristics.EqualitySupport != TypeParameter.EqualitySupportValue.InferredRequired && + o.Characteristics.EqualitySupport != n.Characteristics.EqualitySupport) { + reporter.Error(MessageSource.Resolver, n.tok, "type parameter '{0}' is not allowed to change the requirement of supporting equality", + n.Name); + } + if (o.Characteristics.HasCompiledValue != n.Characteristics.HasCompiledValue) { + reporter.Error(MessageSource.Resolver, n.tok, + "type parameter '{0}' is not allowed to change the requirement of supporting auto-initialization", n.Name); + } else if (o.Characteristics.IsNonempty != n.Characteristics.IsNonempty) { + reporter.Error(MessageSource.Resolver, n.tok, "type parameter '{0}' is not allowed to change the requirement of being nonempty", + n.Name); + } + if (o.Characteristics.ContainsNoReferenceTypes != n.Characteristics.ContainsNoReferenceTypes) { + reporter.Error(MessageSource.Resolver, n.tok, "type parameter '{0}' is not allowed to change the no-reference-type requirement", + n.Name); + } } - + } + for (var i = 0; i < old.Count; i++) { + var o = old[i]; + var n = nw[i]; + CheckOverride_TypeBounds(tok, o, n, name, thing, typeMap); } } return typeMap; } + void CheckOverride_TypeBounds(IToken tok, TypeParameter old, TypeParameter nw, string name, string thing, Dictionary typeMap) { + if (old.TypeBounds.Count != nw.TypeBounds.Count) { + reporter.Error(MessageSource.Resolver, tok, + $"type parameter '{nw.Name}' of {thing} '{name}' is declared with a different number of type bounds than in the " + + $"{thing} it overrides (expected {old.TypeBounds.Count}, found {nw.TypeBounds.Count})"); + return; + } + + for (var i = 0; i < old.TypeBounds.Count; i++) { + var oldBound = old.TypeBounds[i].NormalizeExpandKeepConstraints(); + var newBound = nw.TypeBounds[i].NormalizeExpandKeepConstraints(); + if (!oldBound.Subst(typeMap).Equals(newBound, true)) { + reporter.Error(MessageSource.Resolver, tok, + $"type bound for type parameter '{nw.Name}' of {thing} '{name}' is different from the corresponding type bound of the " + + $"corresponding type parameter of the {thing} it overrides (expected '{oldBound}', found '{newBound}')"); + } + } + } + private void CheckOverride_ResolvedParameters(IToken tok, List old, List nw, string name, string thing, string parameterKind, Dictionary typeMap) { Contract.Requires(tok != null); Contract.Requires(old != null); @@ -2987,7 +3079,7 @@ void ResolveIteratorSignature(IteratorDecl iter) { Contract.Assert(initiallyNoTypeArguments); Contract.Assert(iter.NonNullTypeDecl.TypeArgs.Count == 0); var nnt = iter.NonNullTypeDecl; - nnt.TypeArgs.AddRange(iter.TypeArgs.ConvertAll(tp => new TypeParameter(tp.RangeToken, tp.NameNode, tp.VarianceSyntax, tp.Characteristics))); + nnt.TypeArgs.AddRange(TypeParameter.CloneTypeParameters(iter.TypeArgs)); var varUdt = (UserDefinedType)nnt.Var.Type; Contract.Assert(varUdt.TypeArgs.Count == 0); varUdt.TypeArgs = nnt.TypeArgs.ConvertAll(tp => (Type)new UserDefinedType(tp)); diff --git a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs index 2238c6aa75..e6101c0511 100644 --- a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs +++ b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs @@ -1676,7 +1676,7 @@ private static List ConstrainTypeHead_Recursive(Type super, ref Type sub) { return polarities; } - foreach (var subParentType in sub.ParentTypes()) { + foreach (var subParentType in sub.ParentTypes(true)) { sub = subParentType; polarities = ConstrainTypeHead_Recursive(super, ref sub); if (polarities != null) { @@ -5579,7 +5579,7 @@ void ResolveNameSegment_Type(NameSegment expr, ResolutionContext resolutionConte // We have found a module name or a type name, neither of which is a type expression. However, the NameSegment we're // looking at may be followed by a further suffix that makes this into a type expresion. We postpone the rest of the // resolution to any such suffix. For now, we create a temporary expression that will never be seen by the compiler - // or verifier, just to have a placeholder where we can recorded what we have found. + // or verifier, just to have a placeholder where we can record what we have found. r = CreateResolver_IdentifierExpr(expr.tok, expr.Name, expr.OptTypeArguments, decl); } @@ -5914,7 +5914,6 @@ Expression ResolveExprDotCall(IToken tok, Expression receiver, Type receiverType subst.Add(m.TypeArgs[i], ta); } subst = BuildTypeArgumentSubstitute(subst, receiverTypeBound ?? receiver.Type); - rr.ResolvedOutparameterTypes = m.Outs.ConvertAll(f => f.Type.Subst(subst)); rr.Type = new InferredTypeProxy(); // fill in this field, in order to make "rr" resolved } return rr; diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeConstraints.cs b/Source/DafnyCore/Resolver/PreType/PreTypeConstraints.cs index 900b0b6fcf..b4cc603db6 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeConstraints.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeConstraints.cs @@ -398,11 +398,14 @@ public static int Height(TopLevelDecl decl) { // object is at height 0 return 0; } + if (decl is TopLevelDeclWithMembers { ParentTraitHeads: { Count: > 0 } } topLevelDeclWithMembers) { // Note, if "decl" is a reference type, then its parents include "object", whether or not "object" is explicitly // included in "ParentTraitHeads". Since the "Max" in the following line will return a number 0 or // higher, the "Max" would be the same whether or not "object" is in the "ParentTraitHeads" list. return topLevelDeclWithMembers.ParentTraitHeads.Max(Height) + 1; + } else if (decl is TypeParameter { TypeBounds: { Count: > 0 } } typeParameter) { + return typeParameter.TypeBoundHeads.Max(Height) + 1; } else { // Other other declarations have height 1. // Note, an ostensibly parent-less reference type still has the implicit "object" as a parent trait, but @@ -754,6 +757,15 @@ public List GetTypeArgumentsForSuperType(TopLevelDecl super, DPreType s } } + if (sub.Decl is TypeParameter typeParameter) { + foreach (var preTypeBound in PreTypeResolver.TypeParameterBounds2PreTypes(typeParameter)) { + var arguments = GetTypeArgumentsForSuperType(super, preTypeBound, allowBaseTypeCast); + if (arguments != null) { + return arguments; + } + } + } + if (allowBaseTypeCast && sub.Decl is NewtypeDecl newtypeDecl) { var subst = PreType.PreTypeSubstMap(newtypeDecl.TypeArgs, sub.Arguments); var basePreType = (DPreType)newtypeDecl.BasePreType.Substitute(subst); diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs index 98ec7e2665..4981f472e0 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs @@ -1652,6 +1652,7 @@ Expression ResolveExprDotCall(IToken tok, Expression receiver, DPreType receiver subst.Add(function.TypeArgs[i], ta); } subst = BuildPreTypeArgumentSubstitute(subst, receiverPreTypeBound); + AddTypeBoundConstraints(tok, function.TypeArgs, subst); var inParamTypes = function.Ins.ConvertAll(f => f.PreType.Substitute(subst)); var resultType = Type2PreType(function.ResultType).Substitute(subst); rr.PreType = BuiltInArrowType(inParamTypes, resultType); @@ -1679,11 +1680,24 @@ Expression ResolveExprDotCall(IToken tok, Expression receiver, DPreType receiver rr.PreTypeApplication_JustMember.Add(ta); subst.Add(method.TypeArgs[i], ta); } + subst = BuildPreTypeArgumentSubstitute(subst, receiverPreTypeBound); + AddTypeBoundConstraints(tok, method.TypeArgs, subst); rr.PreType = new MethodPreType($"call to {method.WhatKind} {method.Name}"); // fill in this field, in order to make "rr" resolved } return rr; } + void AddTypeBoundConstraints(IToken tok, List typeParameters, Dictionary subst) { + foreach (var typeParameter in typeParameters) { + foreach (var preTypeBound in TypeParameterBounds2PreTypes(typeParameter)) { + var preTypeBoundWithSubst = preTypeBound.Substitute(subst); + var actualPreType = subst[typeParameter]; + AddSubtypeConstraint(preTypeBoundWithSubst, actualPreType, tok, + $"actual type parameter '{{1}}' for formal type parameter '{typeParameter.Name}' must satisfy the type bound '{{0}}'"); + } + } + } + public MethodCallInformation ResolveApplySuffix(ApplySuffix e, ResolutionContext resolutionContext, bool allowMethodCall) { Contract.Requires(e != null); Contract.Requires(resolutionContext != null); diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs index b3e4551a0e..8748248038 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs @@ -798,6 +798,8 @@ void ResolveCallStmt(CallStmt s, ResolutionContext resolutionContext, Type recei if (tryToResolve) { var typeMap = s.MethodSelect.PreTypeArgumentSubstitutionsAtMemberDeclaration(); + AddTypeBoundConstraints(s.Tok, callee.EnclosingClass.TypeArgs, typeMap); + AddTypeBoundConstraints(s.Tok, callee.TypeArgs, typeMap); // resolve arguments ResolveActualParameters(s.Bindings, callee.Ins, s.Tok, callee, resolutionContext, typeMap, callee.IsStatic ? null : s.Receiver); @@ -816,25 +818,6 @@ void ResolveCallStmt(CallStmt s, ResolutionContext resolutionContext, Type recei CheckIsLvalue(lhs.Resolved, resolutionContext); } -#if SOON - // Resolution termination check - ModuleDefinition callerModule = resolutionContext.EnclosingModule; - ModuleDefinition calleeModule = ((ICodeContext)callee).EnclosingModule; - if (callerModule == calleeModule) { - // intra-module call; add edge in module's call graph - var caller = CodeContextWrapper.Unwrap(resolutionContext) as ICallable; - if (caller == null) { - // don't add anything to the call graph after all - } else if (caller is IteratorDecl) { - callerModule.CallGraph.AddEdge(((IteratorDecl)caller).Member_MoveNext, callee); - } else { - callerModule.CallGraph.AddEdge(caller, callee); - if (caller == callee) { - callee.IsRecursive = true; // self recursion (mutual recursion is determined elsewhere) - } - } - } -#endif } if (Contract.Exists(callee.Decreases.Expressions, e => e is WildcardExpr) && !resolutionContext.CodeContext.AllowsNontermination) { ReportError(s.Tok, "a call to a possibly non-terminating method is allowed only if the calling method is also declared (with 'decreases *') to be possibly non-terminating"); diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs index c160ef4dcd..ae4bfffdc8 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs @@ -251,6 +251,13 @@ public TopLevelDecl Type2Decl(Type type) { return decl; } + public IEnumerable TypeParameterBounds2PreTypes(TypeParameter typeParameter) { + foreach (var typeBound in typeParameter.TypeBounds) { + var preTypeBound = Type2PreType(typeBound, $"type bound for type parameter '{typeParameter.Name}'"); + yield return (DPreType)preTypeBound; + } + } + /// /// Returns the non-newtype ancestor of "decl". /// This method assumes that the ancestors of "decl" do not form any cycles. That is, any such cycle detection must already @@ -329,7 +336,7 @@ public static bool HasTraitSupertypes(DPreType dp) { } /// - /// Add to "ancestors" every TopLevelDecl that is a reflexive, transitive parent of "d", + /// Add to "ancestors" every TopLevelDecl that is a reflexive, transitive parent of "decl", /// but not exploring past any TopLevelDecl that is already in "ancestors". /// public static void ComputeAncestors(TopLevelDecl decl, ISet ancestors, SystemModuleManager systemModuleManager) { @@ -337,7 +344,12 @@ public static void ComputeAncestors(TopLevelDecl decl, ISet ancest ancestors.Add(decl); if (decl is TopLevelDeclWithMembers topLevelDeclWithMembers) { topLevelDeclWithMembers.ParentTraitHeads.ForEach(parent => ComputeAncestors(parent, ancestors, systemModuleManager)); + } else if (decl is TypeParameter typeParameter) { + typeParameter.TypeBoundHeads.ToList().ForEach(parent => ComputeAncestors(parent, ancestors, systemModuleManager)); + } else if (decl is TypeSynonymDecl { Rhs: UserDefinedType { ResolvedClass: TopLevelDecl rhs } }) { + ComputeAncestors(rhs, ancestors, systemModuleManager); } + if (decl is TraitDecl { IsObjectTrait: true }) { // we're done } else if (DPreType.IsReferenceTypeDecl(decl)) { @@ -353,6 +365,18 @@ public static void ComputeAncestors(TopLevelDecl decl, ISet ancest /// Note, if either "super" or "sub" contains a type proxy, then "false" is returned. /// public bool IsSuperPreTypeOf(DPreType super, DPreType sub) { + if (sub.Decl is TypeParameter typeParameter) { + if (PreType.Same(super, sub)) { + return true; + } + foreach (var preTypeBound in TypeParameterBounds2PreTypes(typeParameter)) { + if (IsSuperPreTypeOf(super, preTypeBound)) { + return true; + } + } + return false; + } + var subAncestors = new HashSet(); ComputeAncestors(sub.Decl, subAncestors, resolver.SystemModuleManager); if (!subAncestors.Contains(super.Decl)) { diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeSubtypeConstraint.cs b/Source/DafnyCore/Resolver/PreType/PreTypeSubtypeConstraint.cs index 90556b0c0a..deb900f052 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeSubtypeConstraint.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeSubtypeConstraint.cs @@ -41,7 +41,7 @@ public SubtypeConstraint Normalize() { if (object.ReferenceEquals(super, Super) && object.ReferenceEquals(sub, Sub)) { return this; } else { - return new SubtypeConstraint(super, sub, Token.NoToken, ErrorFormatString, null, ReportErrors); + return new SubtypeConstraint(super, sub, tok, ErrorFormatString, null, ReportErrors); } } diff --git a/Source/DafnyCore/Resolver/ResolutionContext.cs b/Source/DafnyCore/Resolver/ResolutionContext.cs index 9cddc1297c..b9671cc3fc 100644 --- a/Source/DafnyCore/Resolver/ResolutionContext.cs +++ b/Source/DafnyCore/Resolver/ResolutionContext.cs @@ -18,9 +18,9 @@ public ResolutionContext(ICodeContext codeContext, bool isTwoState) /// public static ResolutionContext FromCodeContext(ICodeContext codeContext) { bool isTwoState; - if (codeContext is NoContext || codeContext is DatatypeDecl || codeContext is ConstantField) { + if (codeContext is NoContext or DatatypeDecl or ConstantField) { isTwoState = false; - } else if (codeContext is Function && !(codeContext is TwoStateFunction)) { + } else if (codeContext is Function and not TwoStateFunction) { isTwoState = false; } else { isTwoState = true; diff --git a/Source/DafnyCore/Resolver/TypeConstraint.cs b/Source/DafnyCore/Resolver/TypeConstraint.cs index 80a2cda33b..b6cdb2cd14 100644 --- a/Source/DafnyCore/Resolver/TypeConstraint.cs +++ b/Source/DafnyCore/Resolver/TypeConstraint.cs @@ -44,7 +44,9 @@ private void Reporting(ErrorReporter reporter, string suffix) { reporter.Error(MessageSource.Resolver, err.Tok, err.Msg + suffix, RemoveAmbiguity(err.MsgArgs)); } else { var err = (ErrorMsgWithBase)this; - err.BaseMsg.Reporting(reporter, " (" + string.Format(err.Msg, RemoveAmbiguity(err.MsgArgs)) + ")" + suffix); + if (!err.BaseMsg.reported) { + err.BaseMsg.Reporting(reporter, " (" + string.Format(err.Msg, RemoveAmbiguity(err.MsgArgs)) + ")" + suffix); + } } reported = true; } diff --git a/Source/DafnyCore/Rewriters/RefinementErrors.cs b/Source/DafnyCore/Rewriters/RefinementErrors.cs index 1ea8cf6e2a..7491042b90 100644 --- a/Source/DafnyCore/Rewriters/RefinementErrors.cs +++ b/Source/DafnyCore/Rewriters/RefinementErrors.cs @@ -66,6 +66,8 @@ public enum ErrorId { ref_mismatched_type_parameter_nonempty, ref_mismatched_type_parameter_not_reference, ref_mismatched_type_parameter_variance, + ref_mismatched_type_bounds_count, + ref_mismatched_type_parameter_bound, ref_mismatched_kind_count, ref_mismatched_kind_name, ref_mismatched_kind_ghost, diff --git a/Source/DafnyCore/Rewriters/RefinementTransformer.cs b/Source/DafnyCore/Rewriters/RefinementTransformer.cs index 235ce68261..6239675d23 100644 --- a/Source/DafnyCore/Rewriters/RefinementTransformer.cs +++ b/Source/DafnyCore/Rewriters/RefinementTransformer.cs @@ -367,7 +367,9 @@ private void MergeTopLevelDecls(ModuleDefinition m, IPointer nwPoi "a {0} ({1}) cannot declare members, so it cannot refine an abstract type with members", nw.WhatKind, nw.Name); } else { - CheckAgreement_TypeParameters(nw.tok, d.TypeArgs, nw.TypeArgs, nw.Name, "type", false); + // If there are any type bounds, then the names of the type parameters matter + var checkNames = d.TypeArgs.Concat(nw.TypeArgs).Any(typeParameter => typeParameter.TypeBounds.Count != 0); + CheckAgreement_TypeParameters(nw.tok, d.TypeArgs, nw.TypeArgs, nw.Name, "type", checkNames); } } } else if (nw is AbstractTypeDecl) { @@ -840,7 +842,7 @@ void CheckAgreement_TypeParameters(IToken tok, List old, List old, List old, List nw, string name, string thing, string parameterKind) { Contract.Requires(tok != null); Contract.Requires(old != null); diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs index d8bfd2eef8..a204a9a3c6 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs @@ -724,7 +724,7 @@ public Boogie.Expr TrExpr(Expression expr) { Type t = dtv.Ctor.Formals[i].Type; var bArg = TrExpr(arg); argsAreLit = argsAreLit && BoogieGenerator.IsLit(bArg); - args.Add(BoogieGenerator.CondApplyBox(GetToken(value), bArg, cce.NonNull(arg.Type), t)); + args.Add(BoogieGenerator.AdaptBoxing(GetToken(value), bArg, cce.NonNull(arg.Type), t)); } Boogie.IdentifierExpr id = new Boogie.IdentifierExpr(GetToken(dtv), dtv.Ctor.FullName, predef.DatatypeType); Boogie.Expr ret = new Boogie.NAryExpr(GetToken(dtv), new Boogie.FunctionCall(id), args); @@ -1459,8 +1459,8 @@ public Boogie.Expr TrExpr(Expression expr) { case ITEExpr iteExpr: { ITEExpr e = iteExpr; var g = BoogieGenerator.RemoveLit(TrExpr(e.Test)); - var thn = BoogieGenerator.RemoveLit(TrExpr(e.Thn)); - var els = BoogieGenerator.RemoveLit(TrExpr(e.Els)); + var thn = BoogieGenerator.AdaptBoxing(e.Thn.tok, BoogieGenerator.RemoveLit(TrExpr(e.Thn)), e.Thn.Type, e.Type); + var els = BoogieGenerator.AdaptBoxing(e.Els.tok, BoogieGenerator.RemoveLit(TrExpr(e.Els)), e.Els.Type, e.Type); return new NAryExpr(GetToken(iteExpr), new IfThenElse(GetToken(iteExpr)), new List { g, thn, els }); } case MatchExpr matchExpr: { @@ -1746,7 +1746,7 @@ public Boogie.Expr TrBoundVariablesRename(List boundVars, List Bpl.Expr.Eq(result, CondApplyBox(expr.tok, e, expr.Type, resultType)), + e => Bpl.Expr.Eq(result, AdaptBoxing(expr.tok, e, expr.Type, resultType)), resultDescription)); builder.Add(TrAssumeCmd(expr.tok, etran.CanCallAssumption(expr))); builder.Add(new CommentCmd("CheckWellformedWithResult: any expression")); diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Fields.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Fields.cs index 5584794f6d..2ef1fa11fc 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Fields.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Fields.cs @@ -188,6 +188,11 @@ void AddWellformednessCheck(ConstantField decl) { var req = new List(); // free requires mh == ModuleContextHeight && fh == TypeContextHeight; req.Add(Requires(decl.tok, true, null, etran.HeightContext(decl), null, null, null)); + + foreach (var typeBoundAxiom in TypeBoundAxioms(decl.tok, decl.EnclosingClass.TypeArgs)) { + req.Add(Requires(decl.tok, true, null, typeBoundAxiom, null, null, null)); + } + var heapVar = new Bpl.IdentifierExpr(decl.tok, "$Heap", false); var varlist = new List { heapVar }; var name = MethodName(decl, MethodTranslationKind.SpecWellformedness); diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Functions.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Functions.cs index 762593495f..2dd812c60b 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Functions.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Functions.cs @@ -80,6 +80,10 @@ void AddWellformednessCheck(Function f) { req.Add(Requires(f.tok, true, null, BplAnd(a0, BplAnd(a1, a2)), null, null, null)); } + foreach (var typeBoundAxiom in TypeBoundAxioms(f.tok, Concat(f.EnclosingClass.TypeArgs, f.TypeArgs))) { + req.Add(Requires(f.tok, true, null, typeBoundAxiom, null, null, null)); + } + // modifies $Heap var mod = new List { ordinaryEtran.HeapCastToIdentifierExpr, @@ -451,6 +455,11 @@ void AddFunctionConsequenceAxiom(Boogie.Function boogieFunction, Function f, Lis anteIsAlloc = BplAnd(anteIsAlloc, f.ReadsHeap ? heapSucc : Bpl.Expr.True); } } + // ante: conditions on bounded type parameters + foreach (var typeBoundAxiom in TypeBoundAxioms(f.tok, Concat(f.EnclosingClass.TypeArgs, f.TypeArgs))) { + ante = BplAnd(ante, typeBoundAxiom); + anteIsAlloc = BplAnd(anteIsAlloc, typeBoundAxiom); + } if (!f.IsStatic) { var bvThis = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, etran.This, TrReceiverType(f))); @@ -722,6 +731,11 @@ private Axiom GetFunctionAxiom(Function f, Expression body, List lits) { ante = BplAnd(ante, HeapSucc(etran.Old.HeapExpr, etran.HeapExpr)); } + // ante: conditions on bounded type parameters + foreach (var typeBoundAxiom in TypeBoundAxioms(f.tok, Concat(f.EnclosingClass.TypeArgs, f.TypeArgs))) { + ante = BplAnd(ante, typeBoundAxiom); + } + Expression receiverReplacement = null; if (!f.IsStatic) { var bvThis = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, etran.This, TrReceiverType(f))); @@ -883,7 +897,7 @@ private Axiom GetFunctionAxiom(Function f, Expression body, List lits) { } var etranBody = layer == null ? etran : etran.LimitedFunctions(f, ly); - var trbody = CondApplyBox(f.tok, etranBody.TrExpr(bodyWithSubst), f.Body.Type, f.ResultType); + var trbody = AdaptBoxing(f.tok, etranBody.TrExpr(bodyWithSubst), f.Body.Type, f.ResultType); tastyVegetarianOption = BplAnd(etranBody.CanCallAssumption(bodyWithSubst), BplAnd(TrFunctionSideEffect(bodyWithSubst, etranBody), Bpl.Expr.Eq(funcAppl, trbody))); } diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs index 8fb5d82c79..8bd75fda71 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs @@ -982,6 +982,10 @@ private void AddFunctionOverrideCheckImpl(Function f) { var a2 = FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, currHeap); req.Add(Requires(f.tok, true, null, BplAnd(a0, BplAnd(a1, a2)), null, null, null)); } + foreach (var typeBoundAxiom in TypeBoundAxioms(f.tok, Concat(f.EnclosingClass.TypeArgs, f.TypeArgs))) { + req.Add(Requires(f.tok, true, null, typeBoundAxiom, null, null, null)); + } + // modifies $Heap var mod = new List { ordinaryEtran.HeapCastToIdentifierExpr, @@ -1719,6 +1723,10 @@ private Boogie.Procedure AddMethod(Method m, MethodTranslationKind kind) { var a2 = FunctionCall(m.tok, BuiltinFunction.IsGoodHeap, null, currHeap); req.Add(Requires(m.tok, true, null, BplAnd(a0, BplAnd(a1, a2)), null, null, null)); } + + foreach (var typeBoundAxiom in TypeBoundAxioms(m.tok, Concat(m.EnclosingClass.TypeArgs, m.TypeArgs))) { + req.Add(Requires(m.tok, true, null, typeBoundAxiom, null, null, null)); + } } if (m is TwoStateLemma) { // Checked preconditions that old parameters really existed in previous state @@ -1848,5 +1856,47 @@ private void InsertChecksum(Method m, Boogie.Declaration decl, bool specificatio InsertChecksum(decl, data); } + + internal IEnumerable TypeBoundAxioms(IToken tok, List typeParameters) { + foreach (var typeParameter in typeParameters.Where(typeParameter => typeParameter.TypeBounds.Any())) { + { + // (forall bx: Box :: + // { $IsBox(bx, X) } + // $IsBox(bx, X) ==> + // $IsBox(bx, Bound0) && $IsBox(bx, Bound1) && ...); + var vars = new List(); + var bx = BplBoundVar("bx", predef.BoxType, vars); + var isBox = MkIs(bx, new UserDefinedType(typeParameter)); + Bpl.Expr bounds = Bpl.Expr.True; + foreach (var typeBound in typeParameter.TypeBounds) { + bounds = BplAnd(bounds, MkIs(bx, TypeToTy(typeBound), true)); + } + + var body = BplImp(isBox, bounds); + var q = new Bpl.ForallExpr(tok, vars, BplTrigger(isBox), body); + yield return q; + } + + { + // (forall bx: Box, $Heap: Heap :: + // { $IsAllocBox(bx, X, $h) } + // $IsAllocBox(bx, X, $h) && $IsGoodHeap($h) ==> + // $IsAllocBox(bx, Bound0, $h) && $IsAllocBox(bx, Bound1, $h) && ...); + var vars = new List(); + var bx = BplBoundVar("bx", predef.BoxType, vars); + var heap = BplBoundVar("$h", predef.HeapType, vars); + var isGoodHeap = FunctionCall(tok, BuiltinFunction.IsGoodHeap, null, heap); + var isAllocBox = MkIsAlloc(bx, new UserDefinedType(typeParameter), heap); + Bpl.Expr bounds = Bpl.Expr.True; + foreach (var typeBound in typeParameter.TypeBounds) { + bounds = BplAnd(bounds, MkIsAlloc(bx, TypeToTy(typeBound), heap, true)); + } + + var body = BplImp(BplAnd(isAllocBox, isGoodHeap), bounds); + var q = new Bpl.ForallExpr(tok, vars, BplTrigger(isAllocBox), body); + yield return q; + } + } + } } } diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs b/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs index 3e03c89318..cbcd0d4214 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs @@ -1826,13 +1826,13 @@ void ProcessCallStmt(CallStmt cs, Dictionary tySubst, Bpl.E // Check the subrange without boxing var beforeBox = etran.TrExpr(actual); CheckSubrange(actual.tok, beforeBox, actual.Type, formal.Type.Subst(tySubst), actual, builder); - bActual = CondApplyBox(actual.tok, beforeBox, actual.Type, formal.Type.Subst(tySubst)); + bActual = AdaptBoxing(actual.tok, beforeBox, actual.Type, formal.Type.Subst(tySubst)); dActual = actual; } directSubstMap.Add(formal, dActual); Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(formal.tok, param, bActual); builder.Add(cmd); - ins.Add(CondApplyBox(ToDafnyToken(flags.ReportRanges, param.tok), param, formal.Type.Subst(tySubst), formal.Type)); + ins.Add(AdaptBoxing(ToDafnyToken(flags.ReportRanges, param.tok), param, formal.Type.Subst(tySubst), formal.Type)); } // Check that every parameter is available in the state in which the method is invoked; this means checking that it has @@ -2574,13 +2574,13 @@ Bpl.Expr TrAssignmentRhs(IToken tok, Bpl.IdentifierExpr bGivenLhs, IVariable lhs if (bGivenLhs != null) { Contract.Assert(bGivenLhs == bLhs); // box the RHS, then do the assignment - var cmd = Bpl.Cmd.SimpleAssign(tok, bGivenLhs, CondApplyBox(tok, bRhs, e.Expr.Type, lhsType)); + var cmd = Bpl.Cmd.SimpleAssign(tok, bGivenLhs, AdaptBoxing(tok, bRhs, e.Expr.Type, lhsType)); proofDependencies?.AddProofDependencyId(cmd, tok, new AssignmentDependency(stmt.RangeToken)); builder.Add(cmd); return bGivenLhs; } else { // box from RHS type to tmp-var type, then do the assignment; then return LHS, boxed from tmp-var type to result type - var cmd = Bpl.Cmd.SimpleAssign(tok, bLhs, CondApplyBox(tok, bRhs, e.Expr.Type, rhsTypeConstraint)); + var cmd = Bpl.Cmd.SimpleAssign(tok, bLhs, AdaptBoxing(tok, bRhs, e.Expr.Type, rhsTypeConstraint)); proofDependencies?.AddProofDependencyId(cmd, tok, new AssignmentDependency(stmt.RangeToken)); builder.Add(cmd); return CondApplyBox(tok, bLhs, rhsTypeConstraint, lhsType); diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Types.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Types.cs index 9d7ad9f807..19fb90bce3 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Types.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Types.cs @@ -1030,7 +1030,9 @@ Bpl.Expr ConvertExpression(IToken tok, Bpl.Expr r, Type fromType, Type toType) { Contract.Requires(toType != null); toType = toType.NormalizeToAncestorType(); fromType = fromType.NormalizeToAncestorType(); - if (fromType.IsNumericBased(Type.NumericPersuasion.Int)) { + if (fromType.IsTypeParameter) { + return UnboxUnlessInherentlyBoxed(r, toType); + } else if (fromType.IsNumericBased(Type.NumericPersuasion.Int)) { if (toType.IsNumericBased(Type.NumericPersuasion.Int)) { // do nothing } else if (toType.IsNumericBased(Type.NumericPersuasion.Real)) { @@ -1152,6 +1154,11 @@ Bpl.Expr ConvertExpression(IToken tok, Bpl.Expr r, Type fromType, Type toType) { } else if (fromType.IsTraitType) { // cast from a non-reference trait return UnboxUnlessInherentlyBoxed(r, toType); + } else if (fromType.IsSubtypeOf(toType, false, false)) { + return AdaptBoxing(r.tok, r, fromType, toType); + } else if (fromType is CollectionType && toType is CollectionType) { + // the Boogie representation of collection types is the same for all element types + return r; } else if (fromType.Equals(toType) || fromType.AsNewtype != null || toType.AsNewtype != null) { return r; } else { @@ -1205,7 +1212,9 @@ void PutSourceIntoLocal() { } } - Contract.Assert(options.Get(CommonOptionBag.GeneralTraits) != CommonOptionBag.GeneralTraitsOptions.Legacy || fromType.IsRefType == toType.IsRefType); + Contract.Assert(options.Get(CommonOptionBag.GeneralTraits) != CommonOptionBag.GeneralTraitsOptions.Legacy || + fromType.IsRefType == toType.IsRefType || + (fromType.IsTypeParameter && toType.IsTraitType)); if (toType.IsRefType) { PutSourceIntoLocal(); CheckSubrange(tok, o, fromType, toType, expr, builder, errorMsgPrefix); diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.cs b/Source/DafnyCore/Verifier/BoogieGenerator.cs index 7821bad63d..4e71ebbf24 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.cs @@ -803,6 +803,8 @@ public Bpl.Program DoTranslation(Program p, ModuleDefinition forModule) { filterOnlyMembers = false; + AddTraitParentAxioms(); + foreach (var c in tytagConstants.Values) { sink.AddTopLevelDeclaration(c); } @@ -810,8 +812,6 @@ public Bpl.Program DoTranslation(Program p, ModuleDefinition forModule) { sink.AddTopLevelDeclaration(c); } - AddTraitParentAxioms(); - if (InsertChecksums) { foreach (var impl in sink.Implementations) { if (impl.FindAttribute("checksum") == null) { @@ -3231,6 +3231,14 @@ Bpl.Type TrType(Type type) { } } + public Bpl.Expr AdaptBoxing(Bpl.IToken tok, Bpl.Expr e, Type fromType, Type toType) { + if (fromType.IsTypeParameter) { + return CondApplyUnbox(tok, e, fromType, toType); + } else { + return CondApplyBox(tok, e, fromType, toType); + } + } + public Bpl.Expr CondApplyBox(Bpl.IToken tok, Bpl.Expr e, Type fromType, Type toType) { Contract.Requires(tok != null); Contract.Requires(e != null); @@ -3866,7 +3874,7 @@ Bpl.Expr GetWhereClause(IToken tok, Bpl.Expr x, Type type, ExpressionTranslator if (alwaysUseSymbolicName) { // go for the symbolic name isPred = MkIs(x, normType); - } else if (normType is BoolType || normType is IntType || normType is RealType || normType is BigOrdinalType) { + } else if (normType is BoolType or IntType or RealType or BigOrdinalType) { // nothing to do } else if (normType is BitvectorType) { var t = (BitvectorType)normType; diff --git a/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafnyFromDafny.go b/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafnyFromDafny.go index c0f9d4d687..0b92f44150 100644 --- a/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafnyFromDafny.go +++ b/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafnyFromDafny.go @@ -66,15 +66,15 @@ func (_static *CompanionStruct_Default___) AppendRecursive(builder *Vector, e Se var _out0 interface{} _ = _out0 _out0 = ((_1_lazy).Box()).Get() - _2_boxed = Companion_Sequence_.CastTo_(_out0) + _2_boxed = Companion_Sequence_.CastTo_(Companion_Sequence_.CastTo_(_out0)) Companion_Default___.AppendRecursive(builder, _2_boxed) } else { var _3_a ImmutableArray _ = _3_a var _out1 ImmutableArray _ = _out1 - _out1 = (e).ToArray() - _3_a = _out1 + _out1 = Companion_ImmutableArray_.CastTo_((e).ToArray()) + _3_a = Companion_ImmutableArray_.CastTo_(_out1) (builder).Append(_3_a) } } @@ -116,7 +116,7 @@ TAIL_CALL_START: var _out2 interface{} _ = _out2 _out2 = ((_5_lazy).Box()).Get() - _6_boxed = Companion_Sequence_.CastTo_(_out2) + _6_boxed = Companion_Sequence_.CastTo_(Companion_Sequence_.CastTo_(_out2)) var _in3 *Vector = builder _ = _in3 var _in4 Sequence = _6_boxed @@ -140,7 +140,7 @@ TAIL_CALL_START: var _out3 interface{} _ = _out3 _out3 = (stack).RemoveLast() - _8_next = Companion_Sequence_.CastTo_(_out3) + _8_next = Companion_Sequence_.CastTo_(Companion_Sequence_.CastTo_(_out3)) { var _in6 *Vector = builder _ = _in6 @@ -263,8 +263,8 @@ func (_static *CompanionStruct_Sequence_) Subsequence(_this Sequence, lo uint32, _ = _11_subarray var _out8 ImmutableArray _ = _out8 - _out8 = (_10_a).Subarray(lo, hi) - _11_subarray = _out8 + _out8 = Companion_ImmutableArray_.CastTo_((_10_a).Subarray(lo, hi)) + _11_subarray = Companion_ImmutableArray_.CastTo_(_out8) var _nw0 *ArraySequence = New_ArraySequence_() _ = _nw0 _nw0.Ctor__(_11_subarray, false) @@ -284,18 +284,18 @@ func (_static *CompanionStruct_Sequence_) Create(cardinality uint32, initFn func _ = _12_a var _out9 NativeArray _ = _out9 - _out9 = Companion_NativeArray_.MakeWithInit(cardinality, func(coer0 func(uint32) interface{}) func(uint32) interface{} { + _out9 = Companion_NativeArray_.CastTo_(Companion_NativeArray_.MakeWithInit(cardinality, func(coer0 func(uint32) interface{}) func(uint32) interface{} { return func(arg0 uint32) interface{} { return coer0(arg0) } - }(initFn)) - _12_a = _out9 + }(initFn))) + _12_a = Companion_NativeArray_.CastTo_(_out9) var _13_frozen ImmutableArray _ = _13_frozen var _out10 ImmutableArray _ = _out10 - _out10 = (_12_a).Freeze(cardinality) - _13_frozen = _out10 + _out10 = Companion_ImmutableArray_.CastTo_((_12_a).Freeze(cardinality)) + _13_frozen = Companion_ImmutableArray_.CastTo_(_out10) var _nw1 *ArraySequence = New_ArraySequence_() _ = _nw1 _nw1.Ctor__(_13_frozen, false) @@ -396,21 +396,21 @@ func (_static *CompanionStruct_Sequence_) Update(s Sequence, i uint32, t interfa _ = _19_a var _out17 ImmutableArray _ = _out17 - _out17 = (s).ToArray() - _19_a = _out17 + _out17 = Companion_ImmutableArray_.CastTo_((s).ToArray()) + _19_a = Companion_ImmutableArray_.CastTo_(_out17) var _20_newValue NativeArray _ = _20_newValue var _out18 NativeArray _ = _out18 - _out18 = Companion_NativeArray_.Copy(_19_a) - _20_newValue = _out18 + _out18 = Companion_NativeArray_.CastTo_(Companion_NativeArray_.Copy(_19_a)) + _20_newValue = Companion_NativeArray_.CastTo_(_out18) (_20_newValue).Update(i, t) var _21_newValueFrozen ImmutableArray _ = _21_newValueFrozen var _out19 ImmutableArray _ = _out19 - _out19 = (_20_newValue).Freeze((_20_newValue).Length()) - _21_newValueFrozen = _out19 + _out19 = Companion_ImmutableArray_.CastTo_((_20_newValue).Freeze((_20_newValue).Length())) + _21_newValueFrozen = Companion_ImmutableArray_.CastTo_(_out19) var _nw2 *ArraySequence = New_ArraySequence_() _ = _nw2 _nw2.Ctor__(_21_newValueFrozen, false) @@ -435,7 +435,7 @@ func (_static *CompanionStruct_Sequence_) Concatenate(left Sequence, right Seque var _out20 interface{} _ = _out20 _out20 = ((_23_lazyLeft).Box()).Get() - _22_left_k = Companion_Sequence_.CastTo_(_out20) + _22_left_k = Companion_Sequence_.CastTo_(Companion_Sequence_.CastTo_(_out20)) } var _24_right_k Sequence _ = _24_right_k @@ -449,7 +449,7 @@ func (_static *CompanionStruct_Sequence_) Concatenate(left Sequence, right Seque var _out21 interface{} _ = _out21 _out21 = ((_25_lazyRight).Box()).Get() - _24_right_k = Companion_Sequence_.CastTo_(_out21) + _24_right_k = Companion_Sequence_.CastTo_(Companion_Sequence_.CastTo_(_out21)) } var _26_c *ConcatSequence _ = _26_c @@ -788,8 +788,8 @@ func (_this *Vector) Ctor__(length uint32) { _ = _28_storage var _out22 NativeArray _ = _out22 - _out22 = Companion_NativeArray_.Make(length) - _28_storage = _out22 + _out22 = Companion_NativeArray_.CastTo_(Companion_NativeArray_.Make(length)) + _28_storage = Companion_NativeArray_.CastTo_(_out22) (_this).Storage = _28_storage (_this).Size = uint32(0) } @@ -835,14 +835,14 @@ func (_this *Vector) EnsureCapacity(newMinCapacity uint32) { _ = _30_newStorage var _out23 NativeArray _ = _out23 - _out23 = Companion_NativeArray_.Make(_29_newCapacity) - _30_newStorage = _out23 + _out23 = Companion_NativeArray_.CastTo_(Companion_NativeArray_.Make(_29_newCapacity)) + _30_newStorage = Companion_NativeArray_.CastTo_(_out23) var _31_values ImmutableArray _ = _31_values var _out24 ImmutableArray _ = _out24 - _out24 = (_this.Storage).Freeze(_this.Size) - _31_values = _out24 + _out24 = Companion_ImmutableArray_.CastTo_((_this.Storage).Freeze(_this.Size)) + _31_values = Companion_ImmutableArray_.CastTo_(_out24) (_30_newStorage).UpdateSubarray(uint32(0), _31_values) (_this).Storage = _30_newStorage } @@ -872,8 +872,8 @@ func (_this *Vector) Freeze() ImmutableArray { _ = ret var _out25 ImmutableArray _ = _out25 - _out25 = (_this.Storage).Freeze(_this.Size) - ret = _out25 + _out25 = Companion_ImmutableArray_.CastTo_((_this.Storage).Freeze(_this.Size)) + ret = Companion_ImmutableArray_.CastTo_(_out25) return ret } } @@ -1126,8 +1126,8 @@ func (_this *ConcatSequence) ToArray() ImmutableArray { Companion_Default___.AppendOptimized(_33_builder, _this, _34_stack) var _out36 ImmutableArray _ = _out36 - _out36 = (_33_builder).Freeze() - ret = _out36 + _out36 = Companion_ImmutableArray_.CastTo_((_33_builder).Freeze()) + ret = Companion_ImmutableArray_.CastTo_(_out36) return ret } } @@ -1237,8 +1237,8 @@ func (_this *LazySequence) Ctor__(wrapped Sequence) { _ = _35_box var _out42 AtomicBox _ = _out42 - _out42 = Companion_AtomicBox_.Make(wrapped) - _35_box = _out42 + _out42 = Companion_AtomicBox_.CastTo_(Companion_AtomicBox_.Make(wrapped)) + _35_box = Companion_AtomicBox_.CastTo_(_out42) (_this)._box = _35_box (_this)._length = (wrapped).Cardinality() (_this)._isString = wrapped.IsString() @@ -1258,11 +1258,11 @@ func (_this *LazySequence) ToArray() ImmutableArray { var _out43 interface{} _ = _out43 _out43 = ((_this).Box()).Get() - _36_expr = Companion_Sequence_.CastTo_(_out43) + _36_expr = Companion_Sequence_.CastTo_(Companion_Sequence_.CastTo_(_out43)) var _out44 ImmutableArray _ = _out44 - _out44 = (_36_expr).ToArray() - ret = _out44 + _out44 = Companion_ImmutableArray_.CastTo_((_36_expr).ToArray()) + ret = Companion_ImmutableArray_.CastTo_(_out44) var _37_arraySeq *ArraySequence _ = _37_arraySeq var _nw7 *ArraySequence = New_ArraySequence_() diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AsIs-Resolve.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AsIs-Resolve.dfy.expect index e0446296fd..a2a9906566 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AsIs-Resolve.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AsIs-Resolve.dfy.expect @@ -54,10 +54,7 @@ AsIs-Resolve.dfy(212,11): Error: type test for type 'int -> real' must be from a AsIs-Resolve.dfy(213,11): Error: type test for type 'int -> Odd' must be from an expression assignable to it (got 'int -> nat') (covariant type parameter 1 would require nat <: Odd) AsIs-Resolve.dfy(220,11): Error: type test for type 'int ~> real' must be from an expression assignable to it (got 'int ~> nat') (covariant type parameter 1 would require nat <: real) AsIs-Resolve.dfy(185,11): Error: type cast to reference type 'C<(int, real)>' must be from an expression assignable to it (got 'M') (non-variant type parameter would require (int, real) = (string, string)) (covariant type parameter 0 would require string <: int) -AsIs-Resolve.dfy(185,11): Error: type cast to reference type 'C<(int, real)>' must be from an expression assignable to it (got 'M') (non-variant type parameter would require (int, real) = (string, string)) (covariant type parameter 0 would require int <: string) AsIs-Resolve.dfy(196,9): Error: incorrect argument type at index 0 for datatype constructor parameter (expected real, found int) -AsIs-Resolve.dfy(211,11): Error: type test for type 'real -> nat' must be from an expression assignable to it (got 'int -> nat') (contravariance for type parameter at index 0 expects int <: real) -AsIs-Resolve.dfy(221,11): Error: type test for type 'real --> nat' must be from an expression assignable to it (got 'int ~> nat') (contravariance for type parameter at index 0 expects int <: real) AsIs-Resolve.dfy(229,15): Error: type test for type 'object' must be from an expression assignable to it (got 'T') AsIs-Resolve.dfy(230,18): Error: type test for type 'array' must be from an expression assignable to it (got 'array') (nonvariance for type parameter expects object = T) AsIs-Resolve.dfy(231,18): Error: type test for type 'array' must be from an expression assignable to it (got 'array') (nonvariance for type parameter expects int = T) @@ -65,16 +62,12 @@ AsIs-Resolve.dfy(232,16): Error: type test for type 'T' must be from an expressi AsIs-Resolve.dfy(234,16): Error: type test for type 'object' must be from an expression assignable to it (got 'U') AsIs-Resolve.dfy(235,16): Error: type test for type 'object?' must be from an expression assignable to it (got 'U') AsIs-Resolve.dfy(238,20): Error: type test for type 'U' must be from an expression assignable to it (got 'object') -AsIs-Resolve.dfy(230,18): Error: type test for type 'array' must be from an expression assignable to it (got 'array') (non-variant type parameter would require object = T) -AsIs-Resolve.dfy(231,18): Error: type test for type 'array' must be from an expression assignable to it (got 'array') (non-variant type parameter would require int = T) AsIs-Resolve.dfy(247,18): Error: type test for type 'array' must be from an expression assignable to it (got 'array') (nonvariance for type parameter expects TraitX = ClassX) AsIs-Resolve.dfy(248,18): Error: type test for type 'array' must be from an expression assignable to it (got 'array') (nonvariance for type parameter expects ClassX = TraitX) -AsIs-Resolve.dfy(247,18): Error: type test for type 'array' must be from an expression assignable to it (got 'array') (non-variant type parameter would require TraitX = ClassX) -AsIs-Resolve.dfy(248,18): Error: type test for type 'array' must be from an expression assignable to it (got 'array') (non-variant type parameter would require ClassX = TraitX) AsIs-Resolve.dfy(270,12): Error: an expression of type 'D' is not run-time checkable to be a 'F' AsIs-Resolve.dfy(273,12): Error: an expression of type 'T' is not run-time checkable to be a 'I' AsIs-Resolve.dfy(280,12): Error: an expression of type 'D' is not run-time checkable to be a 'F' AsIs-Resolve.dfy(283,12): Error: an expression of type 'T' is not run-time checkable to be a 'I' AsIs-Resolve.dfy(306,11): Error: an expression of type 'object' is not run-time checkable to be a 'TriviallyObject' AsIs-Resolve.dfy(308,21): Error: an expression of type 'object' is not run-time checkable to be a 'TriviallyObject' -79 resolution/type errors detected in AsIs-Resolve.dfy +72 resolution/type errors detected in AsIs-Resolve.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BoundedPolymorphismCompilation.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BoundedPolymorphismCompilation.dfy new file mode 100644 index 0000000000..238514cd8e --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BoundedPolymorphismCompilation.dfy @@ -0,0 +1,331 @@ +// RUN: %testDafnyForEachCompiler "%s" -- --type-system-refresh --general-traits=datatype + +method Main() { + As.Test(); + Is.Test(); + Basic.Test(); + Bounds.Test(); + BoundsAndCasts.Test(); + Conversions.Test(); + Operators.Test(); + ReturnExpr.Test(); +} + +module As { + trait Parent { + const k: int + } + trait Trait extends Parent { } + class Class extends Trait { + constructor (n: int) { + k := n; + } + } + + method Test() { + var c := new Class(14); + M(c); + var b := N(c); + O(c); + P(c); + } + + method M(x: X) { + var a0 := x as X; + var a1 := x as Trait; + var a2 := x as Parent; + print a1.k, " "; // 14 + } + + method N(x: X) returns (b: bool) { + var t: Trait := x as Trait; + b := x == t as X; + print b, " "; // true + } + + method O(z: Z) { + var a := z as object?; + print a != null, " "; // true + } + + method P(z: Z) { + var a := z as object?; + var b := z as object; + print b == a != null, "\n"; // true + } +} + +module Is { + trait Parent { + const k: int + } + trait Trait extends Parent { } + class Class extends Trait { + constructor (n: int) { + k := n; + } + } + + method Test() { + var c := new Class(14); + M(c); + O(c); // true true + O(null); // true false + P(c); + } + + method M(x: X) { + print x is X, " "; // true + print x is Trait, " "; // true + print x is Parent, " "; // true + print (x as Trait) is Class, "\n"; // false + } + + method O(z: Z) { + print z is object?, " "; + print z is object, " "; + } + + method P(z: Z) { + print z is object?, " "; // true + print z is object, "\n"; // true + } +} + +module Basic { + trait Parent extends object { + const k: int + } + trait Trait extends Parent { } + class Class extends Trait { + constructor (n: int) { + k := n; + } + } + + method TestMethod(x: X) returns (obj: object?) + ensures obj != null + { + var b := x is Trait; + assert b; + print b, " "; // true + + b := x is Parent; + assert b; + print b, " "; // true + + var t: Trait := x as Trait; + obj := t; + } + + method Test() { + var c := new Class(18); + var obj := TestMethod(c); + print obj != null, "\n"; // true + } +} + +module Bounds { + trait Trait { + function Value(): X + } + + datatype Dt extends Trait = Dt(s: string) + { + function Value(): string { s } + } + + method MyMethod>(y: Y) { + var s := (y as Trait).Value(); + print "(", s, ")\n"; + } + + class RandomClass extends Trait { + const r: R + constructor (r: R) { + this.r := r; + } + function Value(): R { r } + } + + method Test() { + var d := Dt("hello"); + MyMethod(d); + + var c := new RandomClass("you don't say"); + MyMethod(c); + + var v := *; // inferred to be of type string (pretty cool, huh!) + var i := new RandomClass(v); + MyMethod(i); + } +} + +module BoundsAndCasts { + method Test() { + var rx := Record("X thing"); + var ry := Record("Y thing"); + var rp := Record("P thing"); + var d := Dt(rx); + d.M(ry, rp); + print d.F(ry, rp), "\n"; + print d.K(rp), "\n"; + } + + trait Parent { } + trait XTrait extends Parent { } + trait YTrait extends Parent { } + + datatype Record extends XTrait, YTrait = Record(s: string) + + datatype Dt = Dt(x: X) + { + method M(y: Y, p: X) { + var parent: Parent; + + parent := x; + print parent, "\n"; + assert parent is XTrait; + + parent := p; + assert parent is XTrait; + print parent, "\n"; + + parent := y; + assert parent is YTrait; + print parent, "\n"; + } + + function F(y: Y, p: X): int { + var parentX: Parent := x; + assert parentX is XTrait; + var parentP: Parent := p; + assert parentP is XTrait; + var parentY: Parent := y; + assert parentY is YTrait; + 15 + } + + const K := (p: X) => + var parentX: Parent := x; + assert parentX is XTrait; + var parentP: Parent := p; + assert parentP is XTrait; + 17 + } +} + +module Conversions { + trait Trait { + function F(): int + } + + datatype Dt extends Trait = Dt(u: int) { + function F(): int { + u + } + } + + datatype Covariant<+X> = Make(value: X) + + method TestCovarianceZ(z: Z) { + var h: Covariant := Covariant.Make(z); + + var g: Covariant; + g := h; + g := h as Covariant; + print (z as Trait).F(), " ", g, " ", h, "\n"; // 5 Dt.Dt(5) Dt.Dt(5) + } + + method Test() { + var d := Dt(5); + TestCovarianceZ(d); + } +} + +module Operators { + trait Trait extends object { } + + method P8(z: Z, t: Trait) returns (s: seq) { + s := [z]; + s := [z as Trait, t]; + s := s[0 := z]; + s := s[0 := z as Trait]; + var zt: Trait := s[0]; + } + + method P9(z: Z, t: Trait) returns (m: map, mi: map) { + m := map[z := z]; + m := m[z := z]; + mi := map[z := z]; + mi := mi[z := z]; + + m := map[z as Trait := t]; + m := m[z as Trait := t]; + mi := map[z as Trait := t]; + mi := mi[z as Trait := t]; + + m := map[t := z as Trait]; + m := m[t := z as Trait]; + mi := map[t := z as Trait]; + mi := mi[t := z as Trait]; + + var zt: Trait := m[t]; + zt := mi[t]; + } + + method P10(z: Z, t: Trait) returns (m: multiset) { + m := multiset{z, z}; + m := multiset{z as Trait, t}; // TODO: this cast should not be needed + m := m[z := 13]; + + var count := m[z]; + count := m[t]; + } + + class CC extends Trait { } + + method Test() { + var cc := new CC; + var _ := P8(cc, cc); + var _, _ := P9(cc, cc); + var _ := P10(cc, cc); + print "done\n"; + } +} + +module ReturnExpr { + trait Trait {} + + function F(x: X): Trait { + assert x is Trait; + x + } + + function G(x: X): Trait { + x as Trait + } + + trait ReferenceTrait extends object {} + + function H(x: X): ReferenceTrait { + assert x is ReferenceTrait; + x + } + + class C extends Trait, ReferenceTrait { + } + + method Test() { + var c := new C; + for i := 0 to 2 { + var t: Trait := if i == 0 then F(c) else G(c); + assert c == t; + var tc: C := t as C; + expect c == tc; + } + + var h: ReferenceTrait := H(c); + expect c == h; + } +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BoundedPolymorphismCompilation.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BoundedPolymorphismCompilation.dfy.expect new file mode 100644 index 0000000000..0d195fb86e --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BoundedPolymorphismCompilation.dfy.expect @@ -0,0 +1,14 @@ +14 true true true +true true true true +true true true false true true +true true true +(hello) +(you don't say) +() +BoundsAndCasts.Record.Record("X thing") +BoundsAndCasts.Record.Record("P thing") +BoundsAndCasts.Record.Record("Y thing") +15 +17 +5 Conversions.Dt.Dt(5) Conversions.Dt.Dt(5) +done diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BoundedPolymorphismCompilation.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BoundedPolymorphismCompilation.dfy.rs.check new file mode 100644 index 0000000000..ccd8552494 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BoundedPolymorphismCompilation.dfy.rs.check @@ -0,0 +1 @@ +// L-CHECK: error: `_` cannot be a raw identifier \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BoundedPolymorphismResolution.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BoundedPolymorphismResolution.dfy new file mode 100644 index 0000000000..22dda39f0e --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BoundedPolymorphismResolution.dfy @@ -0,0 +1,325 @@ +// RUN: %testDafnyForEachResolver --expect-exit-code=2 "%s" -- --general-traits=datatype + +module BadTypeNames { + datatype DT = Dt(w: W) // error: what is Unknown? + + type Syn = DT // error: what is Unknown? + + class Class { // error: what is Unknown? + } + + trait AnotherTrait { // error: what is Unknown? + } + + type Abstract // error: what is Unknown? + + trait Generic { } + + codatatype Mutual, B extends Generic> = More(Mutual) // error: what is Z? + + function Function(k: K): int { 2 } // error: what is Unknown? + + method Method(l: L) { } // error: what is Unknown? + + least predicate Least(m: M) { true } // error: what is Unknown? + + greatest lemma Greatest(n: N) { } // error: what is Unknown? + + iterator Iter(o: O) { } // error: what is Unknown? +} + +module AsIsResolve0 { + trait Trait extends object { + const n: int + } + trait AnotherTrait { } + + method M(x: X) returns (b: bool, t: Trait, u: int) { + t := x; // (legacy error) + b := x is Trait; // (legacy error) + b := x is AnotherTrait; // error: AnotherTrait is not compatible with X + b := x is object; // (legacy error) + t := x as Trait; // (legacy error) + u := t.n; + assert x == t; // (legacy error) + } +} + +module AsIsResolve1 { + trait Trait { + const n: int + } + + method Q(y: Y) returns (t: Trait, u: int) { + t := y as Trait; // (legacy error) + u := (y as Trait).n; // (legacy error) + u := y.n; // error: y needs to be cast to Trait before .n can be accessed + } + + method Nullable(z: Z) returns (b: bool) { + var n; + n := z; + b := (z as object) as object? == null; // (legacy error) + n := null; // error: although n is a reference type, there is no type Z? + } + + method T(z: Z) { + var n; + n := z; + n := null; // error: although n extends object?, Z may have constraints that exclude "null" + } + + trait XTrait { } + + method U>(t: T) { + var a := t as XTrait; // (legacy error) + var b := t as XTrait; // error: non-compatible types + } +} + +module AsIsResolve2 { + trait Trait { + const n: int + } + + method A(x: X, t: Trait) returns (b: bool) { + b := x is X; + b := x is Trait; // (legacy error) + b := t is X; // error: not allowed in compiled code + b := t is Trait; + } + + method B(x: X, t: Trait) returns (ghost g: bool, b: bool) { + b := x is X; + b := x is Trait; // (legacy error) + g := t is X; // (legacy error) + b := t is Trait; + } + + method N(x: X) returns (b: bool, t: Trait) { + t := x as Trait; // (legacy error) + assert x == t; // (legacy error) + ghost var gb := t is X; // (legacy error) + b := t is X; // error: this is not allowed in compiled code + } +} + +module AsIsResolve3 { + trait Trait { + const n: int + } + + method P(y: Y) returns (b: bool, t: Trait) { + t := y as Trait; // (legacy error) + assert y == t; // (legacy error) + b := y == t; // error: we don't know if y supports equality + } + + method R(y: Y) returns (b: bool, t: Trait) { + t := y as Trait; // (legacy error) + b := y == t; // error: Trait not known to support equality + } + + method S(y: Y) returns (b: bool, obj: object) { + obj := y as object; // (legacy error) + b := y == obj; // error: Y not known to support equality + } + + method Finally(y: Y) returns (b: bool, obj: object) { + obj := y as object; // (legacy error) + b := y == obj; // both Y and object support equality, so we're good // (legacy error) + } +} + +module AsIsResolve4 { + trait Trait { } + class Class extends Trait { } + + method M(x: X) { + var a0 := x as X; // (legacy error) + var a1 := x as Trait; // (legacy error) + var a2 := x as Class; // error + var a3 := x as int; // error + } +} + +module BoundMustBeTrait { + trait Trait extends object { + const n: int + } + + datatype Color = Brown | Peach + class Class { } + type Synonym = Trait + type Subset = t: Trait | t.n == 8 witness * + + datatype D0 = Make(w: W) // error: bound must be a trait + datatype D1> = Make(w: W) // error: bound must be a trait + datatype D2 = Make(w: W) // error: bound must be a trait + datatype D3 = Make(w: W) // error: bound must be a trait + datatype D4 = Make(w: W) + datatype D5 = Make(w: W) + datatype D6 = Make(w: W) + datatype D7 = Make(w: W) +} + +module Refinement { + module AA { + trait Trait { } + trait GenericTrait { } + + type SoonSubsetType0 + type SoonSubsetType1 + type SoonSubsetType2 + + type AbstractType0 + type AbstractType1 + type AbstractType2 + + type AbstractType3 + type AbstractType4 + type AbstractType5 + type AbstractType6 + + type AbstractType7, B extends GenericTrait> + + type ToBeReplaced0 + type ToBeReplaced1 + type ToBeReplaced2 + type ToBeReplaced3 + type ToBeReplaced4 + type ToBeReplaced5 + + method M0(u: int) + method M1(u: int) + } + + module BB refines AA { + type SoonSubsetType0 = int // here, the name is allowed to be changed + type SoonSubsetType1 = int // error: name change not allowed + type SoonSubsetType2 = int // error: name change not allowed + + type AbstractType0 // error: name change not allowed + type AbstractType1 // error: name change not allowed + type AbstractType2 // error: name change not allowed + + type AbstractType3 // error: wrong number of type bounds + type AbstractType4 + type AbstractType5 // error: mismatched bound + type AbstractType6 // error (x2): the order has to be the same (because the checking is rather simplistic) + + type AbstractType7, B extends GenericTrait> + + datatype ToBeReplaced0 = Record(a: A) + datatype ToBeReplaced1 = Record(a: A) // error: mismatched bound + type ToBeReplaced2 = int + type ToBeReplaced3 = int // error: mismatched bound + class ToBeReplaced4 { } + class ToBeReplaced5 { } // error: mismatched bound + + method M0(u: int) // error: mismatched bound + method M1(u: int) + } +} + +module CheckArguments { + trait Trait { + function Value(): X + } + + datatype Dt extends Trait = Dt(s: string) + { + function Value(): string { s } + } + + class RandomClass extends Trait { + const r: R + constructor (r: R) { + this.r := r; + } + function Value(): R { r } + } + + method MyMethod>(y0: Y) + function MyFunction>(y1: Y): int + class MyClass> { + constructor (y2: Y) + } + + method Test() { + var m := new RandomClass(3.14); + MyMethod(m); // error: type parameter is RandomClass, which is not a Trait as required by type bound + + var n := new RandomClass('x'); + var _ := MyFunction(n); // error: type parameter is RandomClass, which is not a Trait as required by type bound + + var o := new RandomClass(500); + var oo := new MyClass(o); // error: type parameter is RandomClass, which is not a Trait as required by type bound + } +} + +module Overrides { + trait Base { + function F(): int + method M() + } + + class Class extends Base { + function F(): int { 2 } // error: number of bounds is different + method M() { } // error: bound is different + } + + type ObjectSynonym = object + + type AbstractType extends Base { + function F(): int { 2 } // error: type parameter has been renamed + method M() { } // the synonym here is okay + } + + // --- + + trait GenericBound { } + + trait Parent { + function F, Y extends GenericBound>(): int + method M, Y extends GenericBound>() + greatest lemma L, Y extends IntGenericBound>() + } + + type IntGenericBound = GenericBound + + codatatype SomeGood extends Parent = More + { + function F, Y extends GenericBound>(): int { 2 } + method M, Y extends GenericBound>() { } // error: bound of Y is different + greatest lemma L>() { } + } + + datatype CoSomeGood extends Parent = More + { + function F, X extends GenericBound>(): int { 2 } // error (x2): type parameters have been renamed + method M>() { } // error: bound is different + greatest lemma L, Y extends IntGenericBound>() { } // error: bound is different + } + + trait AnotherTrait extends Parent { + greatest lemma L, Y extends GenericBound>() { } // error: bound is different + } +} + +module VariousBounds { + trait Parent { } + trait XTrait extends Parent { } + trait YTrait extends Parent { } + + datatype Dt = Dt(x: X) + { + method M(y: Y) { + var parent: Parent; + parent := x; // (legacy error) + assert parent is XTrait; // (legacy error) + parent := y; // (legacy error) + assert parent is YTrait; // (legacy error) + } + } +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BoundedPolymorphismResolution.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BoundedPolymorphismResolution.dfy.expect new file mode 100644 index 0000000000..d749cd107a --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BoundedPolymorphismResolution.dfy.expect @@ -0,0 +1,84 @@ +BoundedPolymorphismResolution.dfy(20,30): Error: Type or type parameter is not declared in this scope: Unknown (did you forget to qualify a name or declare a module import 'opened'?) (note that names in outer modules are not visible in contained modules) +BoundedPolymorphismResolution.dfy(22,26): Error: Type or type parameter is not declared in this scope: Unknown (did you forget to qualify a name or declare a module import 'opened'?) (note that names in outer modules are not visible in contained modules) +BoundedPolymorphismResolution.dfy(24,34): Error: Type or type parameter is not declared in this scope: Unknown (did you forget to qualify a name or declare a module import 'opened'?) (note that names in outer modules are not visible in contained modules) +BoundedPolymorphismResolution.dfy(26,36): Error: Type or type parameter is not declared in this scope: Unknown (did you forget to qualify a name or declare a module import 'opened'?) (note that names in outer modules are not visible in contained modules) +BoundedPolymorphismResolution.dfy(4,24): Error: Type or type parameter is not declared in this scope: Unknown (did you forget to qualify a name or declare a module import 'opened'?) (note that names in outer modules are not visible in contained modules) +BoundedPolymorphismResolution.dfy(6,21): Error: Type or type parameter is not declared in this scope: Unknown (did you forget to qualify a name or declare a module import 'opened'?) (note that names in outer modules are not visible in contained modules) +BoundedPolymorphismResolution.dfy(8,24): Error: Type or type parameter is not declared in this scope: Unknown (did you forget to qualify a name or declare a module import 'opened'?) (note that names in outer modules are not visible in contained modules) +BoundedPolymorphismResolution.dfy(8,24): Error: Type or type parameter is not declared in this scope: Unknown (did you forget to qualify a name or declare a module import 'opened'?) (note that names in outer modules are not visible in contained modules) +BoundedPolymorphismResolution.dfy(11,31): Error: Type or type parameter is not declared in this scope: Unknown (did you forget to qualify a name or declare a module import 'opened'?) (note that names in outer modules are not visible in contained modules) +BoundedPolymorphismResolution.dfy(14,26): Error: Type or type parameter is not declared in this scope: Unknown (did you forget to qualify a name or declare a module import 'opened'?) (note that names in outer modules are not visible in contained modules) +BoundedPolymorphismResolution.dfy(18,38): Error: Type or type parameter is not declared in this scope: Z (did you forget to qualify a name or declare a module import 'opened'?) (note that names in outer modules are not visible in contained modules) +BoundedPolymorphismResolution.dfy(28,26): Error: Type or type parameter is not declared in this scope: Unknown (did you forget to qualify a name or declare a module import 'opened'?) (note that names in outer modules are not visible in contained modules) +BoundedPolymorphismResolution.dfy(28,26): Error: Type or type parameter is not declared in this scope: Unknown (did you forget to qualify a name or declare a module import 'opened'?) (note that names in outer modules are not visible in contained modules) +BoundedPolymorphismResolution.dfy(38,6): Error: RHS (of type X) not assignable to LHS (of type Trait) +BoundedPolymorphismResolution.dfy(39,11): Error: type test for type 'Trait' must be from an expression assignable to it (got 'X') +BoundedPolymorphismResolution.dfy(40,11): Error: type test for type 'AnotherTrait' must be from an expression assignable to it (got 'X') +BoundedPolymorphismResolution.dfy(41,11): Error: type test for type 'object' must be from an expression assignable to it (got 'X') +BoundedPolymorphismResolution.dfy(42,11): Error: type cast to reference type 'Trait' must be from an expression assignable to it (got 'X') +BoundedPolymorphismResolution.dfy(44,13): Error: arguments must have comparable types (got X and Trait) +BoundedPolymorphismResolution.dfy(56,11): Error: type Y does not have a member n +BoundedPolymorphismResolution.dfy(54,11): Error: type cast to trait type 'Trait' must be from an expression assignable to it (got 'Y') +BoundedPolymorphismResolution.dfy(55,12): Error: type cast to trait type 'Trait' must be from an expression assignable to it (got 'Y') +BoundedPolymorphismResolution.dfy(62,12): Error: type cast to reference type 'object' must be from an expression assignable to it (got 'Z') +BoundedPolymorphismResolution.dfy(63,9): Error: type of 'null' is a reference type, but it is used as Z +BoundedPolymorphismResolution.dfy(69,9): Error: type of 'null' is a reference type, but it is used as Z +BoundedPolymorphismResolution.dfy(75,15): Error: type cast to trait type 'XTrait' must be from an expression assignable to it (got 'T') +BoundedPolymorphismResolution.dfy(76,15): Error: type cast to trait type 'XTrait' must be from an expression assignable to it (got 'T') +BoundedPolymorphismResolution.dfy(87,11): Error: type test for type 'Trait' must be from an expression assignable to it (got 'X') +BoundedPolymorphismResolution.dfy(88,11): Error: type test for type 'X' must be from an expression assignable to it (got 'Trait') +BoundedPolymorphismResolution.dfy(94,11): Error: type test for type 'Trait' must be from an expression assignable to it (got 'X') +BoundedPolymorphismResolution.dfy(95,11): Error: type test for type 'X' must be from an expression assignable to it (got 'Trait') +BoundedPolymorphismResolution.dfy(100,11): Error: type cast to trait type 'Trait' must be from an expression assignable to it (got 'X') +BoundedPolymorphismResolution.dfy(101,13): Error: arguments must have comparable types (got X and Trait) +BoundedPolymorphismResolution.dfy(102,22): Error: type test for type 'X' must be from an expression assignable to it (got 'Trait') +BoundedPolymorphismResolution.dfy(103,11): Error: type test for type 'X' must be from an expression assignable to it (got 'Trait') +BoundedPolymorphismResolution.dfy(113,11): Error: type cast to trait type 'Trait' must be from an expression assignable to it (got 'Y') +BoundedPolymorphismResolution.dfy(114,13): Error: arguments must have comparable types (got Y and Trait) +BoundedPolymorphismResolution.dfy(115,11): Error: arguments must have comparable types (got Y and Trait) +BoundedPolymorphismResolution.dfy(119,11): Error: type cast to trait type 'Trait' must be from an expression assignable to it (got 'Y') +BoundedPolymorphismResolution.dfy(120,11): Error: arguments must have comparable types (got Y and Trait) +BoundedPolymorphismResolution.dfy(124,13): Error: type cast to reference type 'object' must be from an expression assignable to it (got 'Y') +BoundedPolymorphismResolution.dfy(125,11): Error: arguments must have comparable types (got Y and object) +BoundedPolymorphismResolution.dfy(129,13): Error: type cast to reference type 'object' must be from an expression assignable to it (got 'Y') +BoundedPolymorphismResolution.dfy(130,11): Error: arguments must have comparable types (got Y and object) +BoundedPolymorphismResolution.dfy(139,16): Error: type conversions are not supported to this type (got X) +BoundedPolymorphismResolution.dfy(140,16): Error: type cast to trait type 'Trait' must be from an expression assignable to it (got 'X') +BoundedPolymorphismResolution.dfy(141,16): Error: type cast to reference type 'Class' must be from an expression assignable to it (got 'X') +BoundedPolymorphismResolution.dfy(142,16): Error: type conversion to an int-based type is allowed only from numeric and bitvector types, char, and ORDINAL (got X) +BoundedPolymorphismResolution.dfy(156,11): Error: type bound must be a trait or a subset type based on a trait (got int) +BoundedPolymorphismResolution.dfy(157,11): Error: type bound must be a trait or a subset type based on a trait (got array) +BoundedPolymorphismResolution.dfy(158,11): Error: type bound must be a trait or a subset type based on a trait (got Color) +BoundedPolymorphismResolution.dfy(159,11): Error: type bound must be a trait or a subset type based on a trait (got Class?) +BoundedPolymorphismResolution.dfy(220,11): Error: type bound for type parameter 'A' of method 'M0' is different from the corresponding type bound of the corresponding type parameter of the corresponding method in the module it refines (expected 'Trait', found 'object') +BoundedPolymorphismResolution.dfy(199,25): Error: type parameters are not allowed to be renamed from the names given in the type in the module being refined (expected 'A', found 'B') +BoundedPolymorphismResolution.dfy(200,25): Error: type parameters are not allowed to be renamed from the names given in the type in the module being refined (expected 'A', found 'B') +BoundedPolymorphismResolution.dfy(202,23): Error: type parameters are not allowed to be renamed from the names given in the abstract type in the module being refined (expected 'A', found 'B') +BoundedPolymorphismResolution.dfy(203,23): Error: type parameters are not allowed to be renamed from the names given in the abstract type in the module being refined (expected 'A', found 'B') +BoundedPolymorphismResolution.dfy(204,23): Error: type parameters are not allowed to be renamed from the names given in the abstract type in the module being refined (expected 'A', found 'B') +BoundedPolymorphismResolution.dfy(206,9): Error: type parameter 'A' of abstract type 'AbstractType3' is declared with a different number of type bounds than in the corresponding abstract type in the module it refines (expected 2, found 1) +BoundedPolymorphismResolution.dfy(208,9): Error: type bound for type parameter 'A' of abstract type 'AbstractType5' is different from the corresponding type bound of the corresponding type parameter of the corresponding abstract type in the module it refines (expected 'object', found 'Trait') +BoundedPolymorphismResolution.dfy(209,9): Error: type bound for type parameter 'A' of abstract type 'AbstractType6' is different from the corresponding type bound of the corresponding type parameter of the corresponding abstract type in the module it refines (expected 'Trait', found 'object') +BoundedPolymorphismResolution.dfy(209,9): Error: type bound for type parameter 'A' of abstract type 'AbstractType6' is different from the corresponding type bound of the corresponding type parameter of the corresponding abstract type in the module it refines (expected 'object', found 'Trait') +BoundedPolymorphismResolution.dfy(214,13): Error: type bound for type parameter 'A' of datatype 'ToBeReplaced1' is different from the corresponding type bound of the corresponding type parameter of the corresponding datatype in the module it refines (expected 'Trait', found 'object') +BoundedPolymorphismResolution.dfy(216,9): Error: type parameter 'A' of type 'ToBeReplaced3' is declared with a different number of type bounds than in the corresponding type in the module it refines (expected 1, found 0) +BoundedPolymorphismResolution.dfy(218,10): Error: type bound for type parameter 'A' of class 'ToBeReplaced5' is different from the corresponding type bound of the corresponding type parameter of the corresponding class in the module it refines (expected 'Trait', found 'object') +BoundedPolymorphismResolution.dfy(218,10): Error: type parameter ('A') passed to type 'ToBeReplaced5' must meet type bound 'object' (got 'A') +BoundedPolymorphismResolution.dfy(251,12): Error: type parameter ('Y') passed to method 'MyMethod' must meet type bound 'Trait' (got 'RandomClass') +BoundedPolymorphismResolution.dfy(254,13): Error: type parameter ('Y') passed to function 'MyFunction' must meet type bound 'Trait' (got 'RandomClass') +BoundedPolymorphismResolution.dfy(257,18): Error: type parameter ('Y') passed to type 'MyClass' must meet type bound 'Trait' (got 'RandomClass') +BoundedPolymorphismResolution.dfy(257,18): Error: type parameter ('Y') passed to type 'MyClass' must meet type bound 'Trait' (got 'RandomClass') +BoundedPolymorphismResolution.dfy(268,13): Error: type parameter 'X' of function 'F' is declared with a different number of type bounds than in the function it overrides (expected 1, found 2) +BoundedPolymorphismResolution.dfy(269,11): Error: type bound for type parameter 'X' of method 'M' is different from the corresponding type bound of the corresponding type parameter of the method it overrides (expected 'object', found 'object?') +BoundedPolymorphismResolution.dfy(275,15): Error: type parameters in this function override are not allowed to be renamed from the names given in the the function it overrides (expected 'X', got 'Y') +BoundedPolymorphismResolution.dfy(294,11): Error: type bound for type parameter 'Y' of method 'M' is different from the corresponding type bound of the corresponding type parameter of the method it overrides (expected 'GenericBound', found 'GenericBound') +BoundedPolymorphismResolution.dfy(300,15): Error: type parameters in this function override are not allowed to be renamed from the names given in the the function it overrides (expected 'X', got 'Y') +BoundedPolymorphismResolution.dfy(300,42): Error: type parameters in this function override are not allowed to be renamed from the names given in the the function it overrides (expected 'Y', got 'X') +BoundedPolymorphismResolution.dfy(301,11): Error: type bound for type parameter 'X' of method 'M' is different from the corresponding type bound of the corresponding type parameter of the method it overrides (expected 'GenericBound', found 'GenericBound') +BoundedPolymorphismResolution.dfy(302,19): Error: type bound for type parameter 'X' of method 'L' is different from the corresponding type bound of the corresponding type parameter of the method it overrides (expected 'GenericBound', found 'GenericBound') +BoundedPolymorphismResolution.dfy(306,19): Error: type bound for type parameter 'Y' of method 'L' is different from the corresponding type bound of the corresponding type parameter of the method it overrides (expected 'GenericBound', found 'GenericBound') +BoundedPolymorphismResolution.dfy(319,13): Error: RHS (of type X) not assignable to LHS (of type Parent) +BoundedPolymorphismResolution.dfy(320,20): Error: type test for type 'XTrait' must be from an expression assignable to it (got 'Parent') +BoundedPolymorphismResolution.dfy(321,13): Error: RHS (of type Y) not assignable to LHS (of type Parent) +BoundedPolymorphismResolution.dfy(322,20): Error: type test for type 'YTrait' must be from an expression assignable to it (got 'Parent') +83 resolution/type errors detected in BoundedPolymorphismResolution.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BoundedPolymorphismResolution.dfy.refresh.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BoundedPolymorphismResolution.dfy.refresh.expect new file mode 100644 index 0000000000..c8a7771295 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BoundedPolymorphismResolution.dfy.refresh.expect @@ -0,0 +1,56 @@ +BoundedPolymorphismResolution.dfy(20,30): Error: Type or type parameter is not declared in this scope: Unknown (did you forget to qualify a name or declare a module import 'opened'?) (note that names in outer modules are not visible in contained modules) +BoundedPolymorphismResolution.dfy(22,26): Error: Type or type parameter is not declared in this scope: Unknown (did you forget to qualify a name or declare a module import 'opened'?) (note that names in outer modules are not visible in contained modules) +BoundedPolymorphismResolution.dfy(24,34): Error: Type or type parameter is not declared in this scope: Unknown (did you forget to qualify a name or declare a module import 'opened'?) (note that names in outer modules are not visible in contained modules) +BoundedPolymorphismResolution.dfy(26,36): Error: Type or type parameter is not declared in this scope: Unknown (did you forget to qualify a name or declare a module import 'opened'?) (note that names in outer modules are not visible in contained modules) +BoundedPolymorphismResolution.dfy(4,24): Error: Type or type parameter is not declared in this scope: Unknown (did you forget to qualify a name or declare a module import 'opened'?) (note that names in outer modules are not visible in contained modules) +BoundedPolymorphismResolution.dfy(6,21): Error: Type or type parameter is not declared in this scope: Unknown (did you forget to qualify a name or declare a module import 'opened'?) (note that names in outer modules are not visible in contained modules) +BoundedPolymorphismResolution.dfy(8,24): Error: Type or type parameter is not declared in this scope: Unknown (did you forget to qualify a name or declare a module import 'opened'?) (note that names in outer modules are not visible in contained modules) +BoundedPolymorphismResolution.dfy(8,24): Error: Type or type parameter is not declared in this scope: Unknown (did you forget to qualify a name or declare a module import 'opened'?) (note that names in outer modules are not visible in contained modules) +BoundedPolymorphismResolution.dfy(11,31): Error: Type or type parameter is not declared in this scope: Unknown (did you forget to qualify a name or declare a module import 'opened'?) (note that names in outer modules are not visible in contained modules) +BoundedPolymorphismResolution.dfy(14,26): Error: Type or type parameter is not declared in this scope: Unknown (did you forget to qualify a name or declare a module import 'opened'?) (note that names in outer modules are not visible in contained modules) +BoundedPolymorphismResolution.dfy(18,38): Error: Type or type parameter is not declared in this scope: Z (did you forget to qualify a name or declare a module import 'opened'?) (note that names in outer modules are not visible in contained modules) +BoundedPolymorphismResolution.dfy(28,26): Error: Type or type parameter is not declared in this scope: Unknown (did you forget to qualify a name or declare a module import 'opened'?) (note that names in outer modules are not visible in contained modules) +BoundedPolymorphismResolution.dfy(28,26): Error: Type or type parameter is not declared in this scope: Unknown (did you forget to qualify a name or declare a module import 'opened'?) (note that names in outer modules are not visible in contained modules) +BoundedPolymorphismResolution.dfy(40,11): Error: type test for type 'AnotherTrait' must be from an expression assignable to it (got 'X') +BoundedPolymorphismResolution.dfy(56,11): Error: member 'n' does not exist in type parameter 'Y' +BoundedPolymorphismResolution.dfy(63,9): Error: type of 'null' is a reference type, but it is used as Z +BoundedPolymorphismResolution.dfy(69,9): Error: type of 'null' is a reference type, but it is used as Z +BoundedPolymorphismResolution.dfy(76,15): Error: type cast to trait type 'XTrait' must be from an expression of a compatible type (got 'T') +BoundedPolymorphismResolution.dfy(88,11): Error: an expression of type 'Trait' is not run-time checkable to be a 'X' +BoundedPolymorphismResolution.dfy(103,11): Error: an expression of type 'Trait' is not run-time checkable to be a 'X' +BoundedPolymorphismResolution.dfy(115,9): Error: == can only be applied to expressions of types that support equality (got Y) (perhaps try declaring type parameter 'Y' on line 112 as 'Y(==)', which says it can only be instantiated with a type that supports equality) +BoundedPolymorphismResolution.dfy(120,14): Error: == can only be applied to expressions of types that support equality (got Trait) +BoundedPolymorphismResolution.dfy(125,9): Error: == can only be applied to expressions of types that support equality (got Y) (perhaps try declaring type parameter 'Y' on line 123 as 'Y(==)', which says it can only be instantiated with a type that supports equality) +BoundedPolymorphismResolution.dfy(141,16): Error: type cast to reference type 'Class' must be from an expression of a compatible type (got 'X') +BoundedPolymorphismResolution.dfy(142,16): Error: type conversion to an int-based type is allowed only from numeric and bitvector types, char, and ORDINAL (got X) +BoundedPolymorphismResolution.dfy(156,11): Error: type bound must be a trait or a subset type based on a trait (got int) +BoundedPolymorphismResolution.dfy(157,11): Error: type bound must be a trait or a subset type based on a trait (got array) +BoundedPolymorphismResolution.dfy(158,11): Error: type bound must be a trait or a subset type based on a trait (got Color) +BoundedPolymorphismResolution.dfy(159,11): Error: type bound must be a trait or a subset type based on a trait (got Class?) +BoundedPolymorphismResolution.dfy(220,11): Error: type bound for type parameter 'A' of method 'M0' is different from the corresponding type bound of the corresponding type parameter of the corresponding method in the module it refines (expected 'Trait', found 'object') +BoundedPolymorphismResolution.dfy(199,25): Error: type parameters are not allowed to be renamed from the names given in the type in the module being refined (expected 'A', found 'B') +BoundedPolymorphismResolution.dfy(200,25): Error: type parameters are not allowed to be renamed from the names given in the type in the module being refined (expected 'A', found 'B') +BoundedPolymorphismResolution.dfy(202,23): Error: type parameters are not allowed to be renamed from the names given in the abstract type in the module being refined (expected 'A', found 'B') +BoundedPolymorphismResolution.dfy(203,23): Error: type parameters are not allowed to be renamed from the names given in the abstract type in the module being refined (expected 'A', found 'B') +BoundedPolymorphismResolution.dfy(204,23): Error: type parameters are not allowed to be renamed from the names given in the abstract type in the module being refined (expected 'A', found 'B') +BoundedPolymorphismResolution.dfy(206,9): Error: type parameter 'A' of abstract type 'AbstractType3' is declared with a different number of type bounds than in the corresponding abstract type in the module it refines (expected 2, found 1) +BoundedPolymorphismResolution.dfy(208,9): Error: type bound for type parameter 'A' of abstract type 'AbstractType5' is different from the corresponding type bound of the corresponding type parameter of the corresponding abstract type in the module it refines (expected 'object', found 'Trait') +BoundedPolymorphismResolution.dfy(209,9): Error: type bound for type parameter 'A' of abstract type 'AbstractType6' is different from the corresponding type bound of the corresponding type parameter of the corresponding abstract type in the module it refines (expected 'Trait', found 'object') +BoundedPolymorphismResolution.dfy(209,9): Error: type bound for type parameter 'A' of abstract type 'AbstractType6' is different from the corresponding type bound of the corresponding type parameter of the corresponding abstract type in the module it refines (expected 'object', found 'Trait') +BoundedPolymorphismResolution.dfy(214,13): Error: type bound for type parameter 'A' of datatype 'ToBeReplaced1' is different from the corresponding type bound of the corresponding type parameter of the corresponding datatype in the module it refines (expected 'Trait', found 'object') +BoundedPolymorphismResolution.dfy(216,9): Error: type parameter 'A' of type 'ToBeReplaced3' is declared with a different number of type bounds than in the corresponding type in the module it refines (expected 1, found 0) +BoundedPolymorphismResolution.dfy(218,10): Error: type bound for type parameter 'A' of class 'ToBeReplaced5' is different from the corresponding type bound of the corresponding type parameter of the corresponding class in the module it refines (expected 'Trait', found 'object') +BoundedPolymorphismResolution.dfy(218,10): Error: type parameter ('A') passed to type 'ToBeReplaced5' must meet type bound 'object' (got 'A') +BoundedPolymorphismResolution.dfy(251,12): Error: incorrect argument type for method in-parameter 'y0' (expected RandomClass?, found RandomClass?) (non-variant type parameter 'R' would require string = real) +BoundedPolymorphismResolution.dfy(254,23): Error: incorrect argument type for function parameter 'y1' (expected RandomClass?, found RandomClass?) (non-variant type parameter 'R' would require string = char) +BoundedPolymorphismResolution.dfy(257,14): Error: incorrect argument type for constructor in-parameter 'y2' (expected RandomClass?, found RandomClass?) (non-variant type parameter 'R' would require string = int) +BoundedPolymorphismResolution.dfy(268,13): Error: type parameter 'X' of function 'F' is declared with a different number of type bounds than in the function it overrides (expected 1, found 2) +BoundedPolymorphismResolution.dfy(269,11): Error: type bound for type parameter 'X' of method 'M' is different from the corresponding type bound of the corresponding type parameter of the method it overrides (expected 'object', found 'object?') +BoundedPolymorphismResolution.dfy(275,15): Error: type parameters in this function override are not allowed to be renamed from the names given in the the function it overrides (expected 'X', got 'Y') +BoundedPolymorphismResolution.dfy(294,11): Error: type bound for type parameter 'Y' of method 'M' is different from the corresponding type bound of the corresponding type parameter of the method it overrides (expected 'GenericBound', found 'GenericBound') +BoundedPolymorphismResolution.dfy(300,15): Error: type parameters in this function override are not allowed to be renamed from the names given in the the function it overrides (expected 'X', got 'Y') +BoundedPolymorphismResolution.dfy(300,42): Error: type parameters in this function override are not allowed to be renamed from the names given in the the function it overrides (expected 'Y', got 'X') +BoundedPolymorphismResolution.dfy(301,11): Error: type bound for type parameter 'X' of method 'M' is different from the corresponding type bound of the corresponding type parameter of the method it overrides (expected 'GenericBound', found 'GenericBound') +BoundedPolymorphismResolution.dfy(302,19): Error: type bound for type parameter 'X' of method 'L' is different from the corresponding type bound of the corresponding type parameter of the method it overrides (expected 'GenericBound', found 'GenericBound') +BoundedPolymorphismResolution.dfy(306,19): Error: type bound for type parameter 'Y' of method 'L' is different from the corresponding type bound of the corresponding type parameter of the method it overrides (expected 'GenericBound', found 'GenericBound') +55 resolution/type errors detected in BoundedPolymorphismResolution.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BoundedPolymorphismVerification.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BoundedPolymorphismVerification.dfy new file mode 100644 index 0000000000..fd8961e3a2 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BoundedPolymorphismVerification.dfy @@ -0,0 +1,392 @@ +// RUN: %exits-with 4 %verify --type-system-refresh --general-traits=datatype "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +module As { + trait Parent { } + trait Trait extends Parent { } + trait TheOther extends Parent { } + + method M(x: X) { + var a0 := x as X; + var a1 := x as Trait; + var a2 := x as Parent; + var a3 := (x as Parent) as TheOther; // error: cannot prove "as TheOther" + } + + method N(x: X) returns (b: bool) { + var t: Trait := x as Trait; + if * { + b := x == t as X; // fine + } else { + t := *; + b := x == t as X; // error: cannot prove the cast, because not every Trait is an X + } + } + + method O(z: Z) { + var a := z as object?; + var b := z as object; // error: cannot verify correctness of cast + } + + method P(z: Z) { + var a := z as object?; + var b := z as object; + } +} + +module Is { + trait Parent { } + trait Trait extends Parent { } + trait TheOther extends Parent { } + + method M(x: X) { + var a0 := x is X; + var a1 := x is Trait; + var a2 := x is Parent; + var a3 := (x as Parent) is TheOther; + + assert a0 && a1 && a2; + assert a3; // error: not known if a3 is a TheOther + } + + method N(x: X) returns (ghost b: bool) { + var t: Trait := x as Trait; + if * { + b := t is X; + assert b; + } else { + t := *; + b := t is X; + assert b; // error: not every Trait is an X + } + } + + method O(z: Z) { + var a := z is object?; + assert a; + var b := z is object; + assert b; // error: assertion not provable + } + + method P(z: Z) { + var a := z is object?; + var b := z is object; + assert a && b; + } +} + +module Equality { + method Eq(y: Y) returns (b: bool, obj: object) { + obj := y as object; + b := y == obj; // both Y and object support equality, so we're good to compare + assert b; + } +} + +module TypeBoundKnowledge { + trait Parent { } + trait XTrait extends Parent { } + trait YTrait extends Parent { } + + datatype Dt = Dt(x: X) + { + method M(y: Y) { + var parent: Parent; + parent := x; + assert parent is XTrait; + parent := y; + assert parent is YTrait; + } + + function F(y: Y): int { + var parentX: Parent := x; + assert parentX is XTrait; + var parentY: Parent := y; + assert parentY is YTrait; + 15 + } + + const K := (x: X) => + var parentX: Parent := x; + assert parentX is XTrait; + 17 + + method Negative(xtrait: XTrait) { + assert xtrait is X; // error + } + } + + trait Base { + method M(z: int, y: Y, x: X, w: W) + requires z == 5 + requires x is Parent && w is XTrait // this is always true + twostate function F(z: int, y: Y, x: X, w: W): int + requires z == 5 + } + + class XClass extends XTrait { } + + class Class extends Base { + method M(z: int, y: Y, x: XX, w: XClass) + requires z == if y is YTrait then 5 else 7 + requires z == if x is XTrait then 5 else 7 + { + } + twostate function F(z: int, y: Y, x: XX, w: XClass): int + requires z == if y is YTrait then 5 else 7 + requires z == if x is XTrait then 5 else 7 + { + 17 + } + } + + class Nope extends Base { + method M(z: int, y: Y, x: XX, w: XClass) // error: precondition does not follow from parent trait + requires z == if y as Parent is YTrait then 100 else 700 + { + } + twostate function F(z: int, y: Y, x: XX, w: XClass): int // error: precondition does not follow from parent trait + requires z == if y as Parent is XTrait then 100 else 700 + { + 17 + } + } +} + +module Boxing { + trait Trait extends object { } + + method P(z: Z) { + var a := z as Trait?; + var b := z as Trait; + + var obj: object? := z; + assert obj is Trait?; + assert obj is Trait; + } + + method O(z: Z) { + var a := z as Trait?; + if z as object? != null { + var b0 := z as Trait; + } + var b1 := z as Trait; // error: since z may be null + } +} + +module MoreBoxing { + trait Trait extends object { } + + method P0(z: Z) returns (obj: object?) { + obj := z; + assert true; + } + + class Cell { var obj: object? } + + method P1(z: Z) returns (c: Cell) { + c := new Cell; + c.obj := z; + assert true; + } + + method P2(z: Z) returns (obj: array) { + obj := new object?[1]; + obj[0] := z as object?; // TODO: this cast should not be needed + assert true; + } + + method P3(z: Z) returns (obj: array2) { + obj := new object?[1, 1]; + obj[0, 0] := z as object?; // TODO: this cast should not be needed + assert true; + } + + datatype Record = Record(obj: object?) + + method P4(z: Z) returns (r: Record) { + r := Record(z); + r := r.(obj := z); + assert true; + } + + method M(obj: object?, z: Z) returns (r: object?) { + return z; + } + + method P5(z: Z) returns (obj: object?) { + obj := M(z, z); + assert true; + } + + function F(obj: object?): int { 4 } + + method P6(z: Z) returns (u: int) { + u := F(z); + assert true; + } + + method P7(z: Z) returns (u: int) { + u := var obj: object? := z; + assert obj == null || obj != null; + 14; + assert true; + } + + method P8(z: Z, t: Trait) returns (s: seq) { + s := [z]; + s := [z as Trait, t]; // TODO: this cast should not be needed + s := s[0 := z]; + assert s[0] == z as Trait; + assert z in s; + assert !(z !in s); + assert true; + } + + method P9(z: Z, t: Trait) returns (m: map, mi: map) { + m := map[z := z]; + m := m[z := z]; + mi := map[z := z]; + mi := mi[z := z]; + + m := map[z as Trait := t]; + m := m[z as Trait := t]; + mi := map[z as Trait := t]; + mi := mi[z as Trait := t]; + + m := map[t := z as Trait]; + m := m[t := z as Trait]; + mi := map[t := z as Trait]; + mi := mi[t := z as Trait]; + + if t == z as Trait { + assert z in m; + assert !(z !in m); + assert z in mi; + assert !(z !in mi); + } + } + + method P10(z: Z, t: Trait) returns (m: multiset) { + m := multiset{z, z}; + m := multiset{z as Trait, t}; // TODO: this cast should not be needed + m := m[z := 13]; + assert z in m; + assert !(z !in m); + } + + method P11(z: Z, t: Trait) returns (s: set, si: iset) { + s := {z}; + s := {z as Trait, t}; // TODO: this cast should not be needed + assert z in s; + assert !(z !in s); + + si := iset{z}; + si := iset{z as Trait, t}; // TODO: this cast should not be needed + assert z in si; + assert !(z !in si); + } + + method P12(z: Z, t: Trait) returns (s: set, si: iset) { + var A := {z}; + var B := {z as Trait, t}; + s := set u: Trait | u in A; + s := set u: Trait | u in B; // TODO: this cast should not be needed + si := iset u: Trait | u in A; + si := iset u: Trait | u in B; // TODO: this cast should not be needed + } + + method P14(z: Z, t: Trait) { + assert allocated(z); + } + + method P15(s: set) + modifies s as set + { + } + + function F16(s: set): int + reads s as set + { + 10 + } +} + +module TestThatOverrideCheckHasEnoughInformationAboutTypeBounds { + trait TrTrParent { } + trait TrTr extends TrTrParent { } + + trait Parent extends object { + function F(u: nat, w: W): W + requires u % 5 == 0 + reads this + ensures w == w + + method M(u: nat, w: W) returns (wo: W) + requires u % 5 == 0 + modifies this + ensures w == wo + } + + class Cell extends Parent { + var data: int + + function F(u: nat, w: W): W + requires u % 5 == 0 + requires w as TrTrParent is TrTr // the proof that this condition is "true" requires the type-bound axioms + reads this + ensures w == w + { + var m := u + data; + var o := 2 * if m < 0 then -m else m; + w + } + + method M(u: nat, w: W) returns (wo: W) + requires u % 5 == 0 + modifies this + ensures wo as TrTrParent is TrTr ==> wo == w + { + return w; + } + } +} + +module Variance { + class Generic { } + datatype Covariant<+X> = Make(value: X) + + method TestAutoConversions() + { + var g: Generic := new Generic; + var h: Generic := new Generic; + if * { + g := h; // error: non-compatible types + } else { + h := g; // error: non-compatible types + } + } + + method TestExplicitConversions() + { + var g: Generic := new Generic; + var h: Generic := new Generic; + if * { + g := h as Generic; // error: non-compatible types + } else { + h := g as Generic; // error: non-compatible types + } + } + + method TestCovariance() { + var g: Covariant := Covariant.Make(5); + var h: Covariant := Covariant.Make(5); + if * { + g := h; + g := h as Covariant; // (legacy error) + } else { + h := g; + h := g as Covariant; // (legacy error) + } + } +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BoundedPolymorphismVerification.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BoundedPolymorphismVerification.dfy.expect new file mode 100644 index 0000000000..4f117487e1 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BoundedPolymorphismVerification.dfy.expect @@ -0,0 +1,16 @@ +BoundedPolymorphismVerification.dfy(13,28): Error: value of expression (of type 'Parent') is not known to be an instance of type 'TheOther' +BoundedPolymorphismVerification.dfy(22,18): Error: value of expression (of type 'Trait') is not known to be an instance of type 'X' +BoundedPolymorphismVerification.dfy(28,15): Error: value of expression (of type 'Z') is not known to be an instance of type 'object' +BoundedPolymorphismVerification.dfy(49,11): Error: assertion might not hold +BoundedPolymorphismVerification.dfy(60,13): Error: assertion might not hold +BoundedPolymorphismVerification.dfy(68,11): Error: assertion might not hold +BoundedPolymorphismVerification.dfy(115,20): Error: assertion might not hold +BoundedPolymorphismVerification.dfy(144,4): Error: the method must provide an equal or more permissive precondition than in its parent trait +BoundedPolymorphismVerification.dfy(148,22): Error: the function must provide an equal or more permissive precondition than in its parent trait +BoundedPolymorphismVerification.dfy(173,16): Error: value of expression (of type 'Z') is not known to be an instance of type 'Trait' +BoundedPolymorphismVerification.dfy(364,11): Error: value of expression (of type 'Generic') is not known to be an instance of type 'Generic' +BoundedPolymorphismVerification.dfy(366,11): Error: value of expression (of type 'Generic') is not known to be an instance of type 'Generic' +BoundedPolymorphismVerification.dfy(375,13): Error: value of expression (of type 'Generic') is not known to be an instance of type 'Generic' +BoundedPolymorphismVerification.dfy(377,13): Error: value of expression (of type 'Generic') is not known to be an instance of type 'Generic' + +Dafny program verifier finished with 32 verified, 14 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/LiberalEquality.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/LiberalEquality.dfy.expect index 769250d135..321b6cdf46 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/LiberalEquality.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/LiberalEquality.dfy.expect @@ -11,15 +11,9 @@ LiberalEquality.dfy(73,13): Error: arguments must have comparable types (got T ~ LiberalEquality.dfy(74,13): Error: arguments must have comparable types (got int ~> T and int ~> int) LiberalEquality.dfy(84,13): Error: arguments must have comparable types (got Syn and Syn) LiberalEquality.dfy(95,13): Error: arguments must have comparable types (got array> and array>) (non-variant type parameter would require int = bool) -LiberalEquality.dfy(95,13): Error: arguments must have comparable types (got array> and array>) (non-variant type parameter would require bool = int) LiberalEquality.dfy(97,13): Error: arguments must have comparable types (got array> and array>) (non-variant type parameter would require bool = int) -LiberalEquality.dfy(97,13): Error: arguments must have comparable types (got array> and array>) (non-variant type parameter would require int = bool) LiberalEquality.dfy(99,13): Error: arguments must have comparable types (got array> and array>) (non-variant type parameter would require int = T) -LiberalEquality.dfy(99,13): Error: arguments must have comparable types (got array> and array>) (non-variant type parameter would require T = int) LiberalEquality.dfy(100,13): Error: arguments must have comparable types (got array> and array>) (non-variant type parameter would require bool = T) -LiberalEquality.dfy(100,13): Error: arguments must have comparable types (got array> and array>) (non-variant type parameter would require T = bool) LiberalEquality.dfy(101,13): Error: arguments must have comparable types (got array> and array>) (non-variant type parameter would require int = T) -LiberalEquality.dfy(101,13): Error: arguments must have comparable types (got array> and array>) (non-variant type parameter would require T = int) LiberalEquality.dfy(103,13): Error: arguments must have comparable types (got array> and array>>) (non-variant type parameter would require bool = Wrapper) -LiberalEquality.dfy(103,13): Error: arguments must have comparable types (got array> and array>>) (non-variant type parameter would require Wrapper = bool) -24 resolution/type errors detected in LiberalEquality.dfy +18 resolution/type errors detected in LiberalEquality.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/PrettyPrinting.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/PrettyPrinting.dfy index 76911f0b87..1044d73d40 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/PrettyPrinting.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/PrettyPrinting.dfy @@ -168,3 +168,33 @@ module New { a := new [] [20, 50, 70]; } } + +module BoundedPolymorphism { + trait Trait { } + + datatype DT = Dt(w: W) + + type Syn = DT + + class Class { + } + + trait AnotherTrait { + } + + type Abstract> + + trait Generic { } + + codatatype Mutual, B extends Generic> = More(Mutual) + + function Function(k: K): int { 2 } + + method Method(l: L) { } + + least predicate Least(m: M) { true } + + greatest lemma Greatest(n: N) { } + + iterator Iter(o: O) { } +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/PrettyPrinting.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/PrettyPrinting.dfy.expect index 3c1e5bb11e..0bb2e869e4 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/PrettyPrinting.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/PrettyPrinting.dfy.expect @@ -189,6 +189,46 @@ module New { a := new [] [20, 50, 70]; } } + +module BoundedPolymorphism { + function Function(k: K): int + { + 2 + } + + method Method(l: L) + { + } + + least predicate Least(m: M) + { + true + } + + greatest lemma Greatest(n: N) + { + } + + trait Trait { } + + datatype DT = Dt(w: W) + + type Syn = DT + + class Class { } + + trait AnotherTrait { } + + type Abstract> + + trait Generic { } + + codatatype Mutual, B extends Generic> = More(Mutual) + + iterator Iter(o: O) + { + } +} PrettyPrinting.dfy(20,4): Error: skeleton statements are allowed only in refining methods PrettyPrinting.dfy(21,4): Error: skeleton statements are allowed only in refining methods PrettyPrinting.dfy(75,16): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors2.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors2.dfy.expect index 9144d802d5..acb24b31d1 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors2.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors2.dfy.expect @@ -29,7 +29,6 @@ ResolutionErrors2.dfy(291,28): Error: member 'x' does not exist in datatype '_tu ResolutionErrors2.dfy(290,18): Error: condition is expected to be of type bool, but is int ResolutionErrors2.dfy(284,39): Error: RHS (of type (int, real, int)) not assignable to LHS (of type (int, real, int, real)) ResolutionErrors2.dfy(283,34): Error: RHS (of type (int, int, real)) not assignable to LHS (of type (int, real, int)) (covariant type parameter 1 would require int <: real) -ResolutionErrors2.dfy(283,34): Error: RHS (of type (int, int, real)) not assignable to LHS (of type (int, real, int)) (covariant type parameter 2 would require real <: int) ResolutionErrors2.dfy(315,12): Error: type of left argument to % (int) must agree with the result type (real) ResolutionErrors2.dfy(315,12): Error: arguments to % must be integer-numeric or bitvector types (got real) ResolutionErrors2.dfy(314,19): Error: type of right argument to / (int) must agree with the result type (real) @@ -70,4 +69,4 @@ ResolutionErrors2.dfy(489,27): Error: set comprehensions in non-ghost contexts m ResolutionErrors2.dfy(497,15): Error: arguments to / must be numeric or bitvector types (got set) ResolutionErrors2.dfy(504,20): Error: a call to a possibly non-terminating method is allowed only if the calling method is also declared (with 'decreases *') to be possibly non-terminating ResolutionErrors2.dfy(519,16): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating -70 resolution/type errors detected in ResolutionErrors2.dfy +69 resolution/type errors detected in ResolutionErrors2.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug140.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug140.dfy.rs.check index d59836f7d8..dae9bb332a 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug140.dfy.rs.check +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug140.dfy.rs.check @@ -1 +1 @@ -// CHECK-L: error[E0308]: mismatched types \ No newline at end of file +// CHECK-L: error[E0308]: mismatched types diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1637.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1637.dfy.expect index e2f5f60300..60f35b398d 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1637.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1637.dfy.expect @@ -1,3 +1,2 @@ git-issue-1637.dfy(19,5): Error: incorrect argument type for predicate parameter 'f' (expected Thing -> seq, found Thing -> Fii) (covariance for type parameter at index 1 expects seq :> Fii) -git-issue-1637.dfy(19,5): Error: incorrect argument type for predicate parameter 'f' (expected Thing -> seq, found Thing -> Fii) (covariance for type parameter at index 1 expects real :> seq) -2 resolution/type errors detected in git-issue-1637.dfy +1 resolution/type errors detected in git-issue-1637.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5570.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5570.dfy new file mode 100644 index 0000000000..0d48531a01 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5570.dfy @@ -0,0 +1,30 @@ +// RUN: %verify --type-system-refresh --general-traits=datatype "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +module Class { + trait Parent { } + + class Record extends Parent {} + + function Pick(b: bool, r: Record, d: Parent): Parent { + if b then r else d + } + + method Select(b: bool, r: Record, d: Parent) returns (p: Parent) { + p := if b then r else d; + } +} + +module Datatype { + trait Parent { } + + datatype Record extends Parent = Record + + function Pick(b: bool, r: Record, d: Parent): Parent { + if b then r else d + } + + method Select(b: bool, r: Record, d: Parent) returns (p: Parent) { + p := if b then r else d; + } +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5570.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5570.dfy.expect new file mode 100644 index 0000000000..ebe2328e07 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5570.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 2 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-697j.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-697j.dfy.rs.check index 323dbedbaf..45270a849b 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-697j.dfy.rs.check +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-697j.dfy.rs.check @@ -1 +1 @@ -// CHECK-L: Unhandled exception: System.InvalidOperationException: Operation is not valid due to the current state of the object. \ No newline at end of file +// CHECK: .*Unsupported: Cannot assign null value to variable.* \ No newline at end of file diff --git a/docs/HowToFAQ/Errors-Refinement.md b/docs/HowToFAQ/Errors-Refinement.md index 8bde41d77e..eb4b6dd714 100644 --- a/docs/HowToFAQ/Errors-Refinement.md +++ b/docs/HowToFAQ/Errors-Refinement.md @@ -765,6 +765,32 @@ There are restrictions on what can be changed in a refinement. In particular, the variance of type parameters must remain the same. +## **Error: type parameter '_name_' of _what_ '_declarationname_' is declared with a different number of type bounds than in the corresponding _what_ in the module it refines (expected _oldnum_, found _num_)** {#ref_mismatched_type_bounds_count} + +``` dafny +module A { + type AbstrType +} + +module B refines A { + type AbstrType +} +``` + +## **Error: type bound for type parameter '_name_' of _what_ '_declarationname_' is different from the corresponding type bound of the corresponding type parameter of the corresponding _what_ in the module it refines (expected '_oldbound_', found '_bound_'** {#ref_mismatched_type_parameter_bound} + +``` dafny +module A { + type AbstrType +} + +module B refines A { + trait Trait { } + type AbstrType +} +``` + + ## **Error: _kind_ '_name_' is declared with a different number of _what_ (_num_ instead of _oldnum_) than the corresponding _kind_ in the module it refines** {#ref_mismatched_kind_count} ```dafny