From e1ccb16be65ae873e987bdcbf1ab8bb909488133 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Wed, 28 Aug 2024 12:36:22 -0700 Subject: [PATCH] feat: Allow type parameters on newtypes (#5495) This PR adds the following language features: * type parameters of `newtype` declarations * optional `witness` clause of constraint-less `newtype` declarations * tool tips show auto-completed type parameters * tool tips show inferred `(==)` characteristics Along the way, the PR also fixes two previous soundness issues: * fix: Check the emptiness status of constraint-less `newtype` declarations (#5520) * fix: Don't let `newtype` well-formedness checking affect witness checking (#5521) Fixes #5520 Fixes #5521 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 | 7 +- .../DafnyCore/AST/Grammar/Printer/Printer.cs | 55 +- Source/DafnyCore/AST/Members/ICodeContext.cs | 2 + .../AST/TypeDeclarations/NewtypeDecl.cs | 42 +- .../AST/TypeDeclarations/SubsetTypeDecl.cs | 2 + .../TypeDeclarations/TypeSynonymDeclBase.cs | 2 + Source/DafnyCore/AST/Types/TypeParameter.cs | 3 + Source/DafnyCore/AST/Types/Types.cs | 5 +- .../Backends/CSharp/CsharpCodeGenerator.cs | 12 +- .../Backends/CodeGeneratorTypeExtensions.cs | 3 +- .../Backends/Cplusplus/CppCodeGenerator.cs | 10 +- .../Backends/GoLang/GoCodeGenerator.cs | 14 +- .../Backends/Java/JavaCodeGenerator.cs | 12 +- .../JavaScript/JavaScriptCodeGenerator.cs | 12 +- .../Backends/Python/PythonCodeGenerator.cs | 8 +- Source/DafnyCore/Dafny.atg | 52 +- Source/DafnyCore/Resolver/ModuleResolver.cs | 10 +- .../NameResolutionAndTypeInference.cs | 5 +- .../Resolver/PreType/PreType2TypeUtil.cs | 20 +- .../Resolver/PreType/PreTypeConstraints.cs | 9 +- .../PreType/PreTypeResolve.Expressions.cs | 61 ++- .../Resolver/PreType/PreTypeResolve.cs | 50 +- .../PreType/UnderspecificationDetector.cs | 4 +- .../Resolver/TypeCharacteristicChecker.cs | 69 ++- .../Rewriters/RefinementTransformer.cs | 10 +- .../BoogieGenerator.ExpressionTranslator.cs | 2 +- .../Verifier/BoogieGenerator.TrStatement.cs | 2 +- .../Verifier/BoogieGenerator.Types.cs | 64 ++- Source/DafnyCore/Verifier/BoogieGenerator.cs | 35 +- .../DafnyPipeline.Test/expectedProverLog.smt2 | 27 +- .../LitTests/LitTest/comp/GeneralNewtypes.dfy | 79 +++ .../LitTest/comp/GeneralNewtypes.dfy.expect | 7 + .../dafny0/AsIs-UnusedTypeParameters.dfy | 70 +++ .../AsIs-UnusedTypeParameters.dfy.expect | 5 + ...Is-UnusedTypeParameters.dfy.refresh.expect | 8 + .../dafny0/BoundedPolymorphismResolution.dfy | 100 +++- .../BoundedPolymorphismResolution.dfy.expect | 49 +- ...dPolymorphismResolution.dfy.refresh.expect | 49 +- .../GeneralNewtypeCollectionsGeneric.dfy | 513 ++++++++++++++++++ ...eneralNewtypeCollectionsGeneric.dfy.expect | 52 ++ .../dafny0/GeneralNewtypeResolution.dfy | 258 +++++++++ .../GeneralNewtypeResolution.dfy.expect | 104 +++- .../LitTest/dafny0/GeneralNewtypeVerify.dfy | 110 ++++ .../dafny0/GeneralNewtypeVerify.dfy.expect | 14 +- .../LitTests/LitTest/dafny0/Newtypes.dfy | 13 + .../LitTest/dafny0/Newtypes.dfy.expect | 5 +- .../LitTest/dafny0/NonZeroInitialization.dfy | 2 +- .../dafny0/NonZeroInitialization.dfy.expect | 2 +- .../LitTest/dafny0/PrettyPrinting.dfy | 10 + .../LitTest/dafny0/PrettyPrinting.dfy.expect | 21 + .../LitTest/dafny0/SubsetTypes.dfy.expect | 2 +- .../LitTests/LitTest/dafny0/Tooltips.dfy | 23 + .../LitTest/dafny0/Tooltips.dfy.expect | 18 + .../LitTest/dafny0/TypeInstantiations.dfy | 12 +- .../dafny0/TypeInstantiations.dfy.expect | 2 +- .../git-issues/git-issue-3962.dfy.expect | 1 + .../git-issues/git-issue-4188.dfy.expect | 2 +- .../LitTest/git-issues/git-issue-5520.dfy | 73 +++ .../git-issues/git-issue-5520.dfy.expect | 6 + .../LitTest/git-issues/git-issue-5521.dfy | 73 +++ .../git-issues/git-issue-5521.dfy.expect | 7 + docs/dev/news/5495.feat | 6 + 62 files changed, 1979 insertions(+), 326 deletions(-) create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AsIs-UnusedTypeParameters.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AsIs-UnusedTypeParameters.dfy.expect create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AsIs-UnusedTypeParameters.dfy.refresh.expect create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GeneralNewtypeCollectionsGeneric.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GeneralNewtypeCollectionsGeneric.dfy.expect create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Tooltips.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Tooltips.dfy.expect create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5520.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5520.dfy.expect create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5521.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5521.dfy.expect create mode 100644 docs/dev/news/5495.feat diff --git a/Source/DafnyCore/AST/Cloner.cs b/Source/DafnyCore/AST/Cloner.cs index fcceee43562..d42e6358abc 100644 --- a/Source/DafnyCore/AST/Cloner.cs +++ b/Source/DafnyCore/AST/Cloner.cs @@ -86,12 +86,13 @@ public virtual TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition ne } else if (d is NewtypeDecl) { var dd = (NewtypeDecl)d; if (dd.Var == null) { - return new NewtypeDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), newParent, CloneType(dd.BaseType), + return new NewtypeDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), dd.TypeArgs.ConvertAll(CloneTypeParam), newParent, + CloneType(dd.BaseType), dd.WitnessKind, CloneExpr(dd.Witness), dd.ParentTraits.ConvertAll(CloneType), dd.Members.ConvertAll(d => CloneMember(d, false)), CloneAttributes(dd.Attributes), dd.IsRefining); } else { - return new NewtypeDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), newParent, CloneBoundVar(dd.Var, false), - CloneExpr(dd.Constraint), dd.WitnessKind, CloneExpr(dd.Witness), + return new NewtypeDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), dd.TypeArgs.ConvertAll(CloneTypeParam), newParent, + CloneBoundVar(dd.Var, false), CloneExpr(dd.Constraint), dd.WitnessKind, CloneExpr(dd.Witness), dd.ParentTraits.ConvertAll(CloneType), dd.Members.ConvertAll(d => CloneMember(d, false)), CloneAttributes(dd.Attributes), dd.IsRefining); } diff --git a/Source/DafnyCore/AST/Grammar/Printer/Printer.cs b/Source/DafnyCore/AST/Grammar/Printer/Printer.cs index fd1b2dfb940..5cd7c07e953 100644 --- a/Source/DafnyCore/AST/Grammar/Printer/Printer.cs +++ b/Source/DafnyCore/AST/Grammar/Printer/Printer.cs @@ -308,11 +308,11 @@ public void PrintTopLevelDecls(CompilationData compilation, IEnumerable typeArgs) { Contract.Requires(typeArgs != null); Contract.Requires( - typeArgs.All(tp => tp.Name.StartsWith("_")) || - typeArgs.All(tp => !tp.Name.StartsWith("_"))); + typeArgs.All(tp => tp.IsAutoCompleted) || + typeArgs.All(tp => !tp.IsAutoCompleted)); - if (typeArgs.Count != 0 && !typeArgs[0].Name.StartsWith("_")) { + if (typeArgs.Count != 0 && !typeArgs[0].IsAutoCompleted) { wr.Write("<{0}>", Util.Comma(typeArgs, TypeParamString)); } } + public static string TypeParameterToString(TypeParameter tp) { + return TypeParamVariance(tp) + tp.Name + TPCharacteristicsSuffix(tp.Characteristics, true); + } + public string TypeParamString(TypeParameter tp) { Contract.Requires(tp != null); - string variance; + var paramString = TypeParamVariance(tp) + tp.Name + TPCharacteristicsSuffix(tp.Characteristics); + foreach (var typeBound in tp.TypeBounds) { + paramString += $" extends {typeBound.TypeName(options, null, true)}"; + } + return paramString; + } + + public static string TypeParamVariance(TypeParameter tp) { switch (tp.VarianceSyntax) { case TypeParameter.TPVarianceSyntax.Covariant_Permissive: - variance = "*"; - break; + return "*"; case TypeParameter.TPVarianceSyntax.Covariant_Strict: - variance = "+"; - break; + return "+"; case TypeParameter.TPVarianceSyntax.NonVariant_Permissive: - variance = "!"; - break; + return "!"; case TypeParameter.TPVarianceSyntax.NonVariant_Strict: - variance = ""; - break; + return ""; case TypeParameter.TPVarianceSyntax.Contravariance: - variance = "-"; - break; + return "-"; default: Contract.Assert(false); // unexpected VarianceSyntax throw new cce.UnreachableException(); } - 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) { @@ -1184,9 +1185,13 @@ public void PrintType(string prefix, Type ty) { } public string TPCharacteristicsSuffix(TypeParameter.TypeParameterCharacteristics characteristics) { + return TPCharacteristicsSuffix(characteristics, options.DafnyPrintResolvedFile != null); + } + + public static string TPCharacteristicsSuffix(TypeParameter.TypeParameterCharacteristics characteristics, bool printInferredTypeCharacteristics) { string s = null; if (characteristics.EqualitySupport == TypeParameter.EqualitySupportValue.Required || - (characteristics.EqualitySupport == TypeParameter.EqualitySupportValue.InferredRequired && options.DafnyPrintResolvedFile != null)) { + (characteristics.EqualitySupport == TypeParameter.EqualitySupportValue.InferredRequired && printInferredTypeCharacteristics)) { s = "=="; } if (characteristics.HasCompiledValue) { diff --git a/Source/DafnyCore/AST/Members/ICodeContext.cs b/Source/DafnyCore/AST/Members/ICodeContext.cs index a5ab7e0886e..d01e78f5b6f 100644 --- a/Source/DafnyCore/AST/Members/ICodeContext.cs +++ b/Source/DafnyCore/AST/Members/ICodeContext.cs @@ -145,6 +145,8 @@ public interface RedirectingTypeDecl : ICallable { Attributes Attributes { get; } ModuleDefinition Module { get; } BoundVar/*?*/ Var { get; } + PreType BasePreType { get; } + Type BaseType { get; } Expression/*?*/ Constraint { get; } SubsetTypeDecl.WKind WitnessKind { get; } Expression/*?*/ Witness { get; } // non-null iff WitnessKind is Compiled or Ghost diff --git a/Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs index ba3f7a8ab20..ba9804f4edd 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs @@ -9,6 +9,7 @@ public class NewtypeDecl : TopLevelDeclWithMembers, RevealableTypeDecl, Redirect public override string WhatKind { get { return "newtype"; } } public override bool CanBeRevealed() { return true; } public PreType BasePreType; + PreType RedirectingTypeDecl.BasePreType => BasePreType; public Type BaseType { get; set; } // null when refining public BoundVar Var { get; set; } // can be null (if non-null, then object.ReferenceEquals(Var.Type, BaseType)) public Expression Constraint { get; set; } // is null iff Var is @@ -31,19 +32,25 @@ bool RedirectingTypeDecl.ConstraintIsCompilable { [FilledInDuringResolution] public bool TargetTypeCoversAllBitPatterns; // "target complete" -- indicates that any bit pattern that can fill the target type is a value of the newtype - public NewtypeDecl(RangeToken rangeToken, Name name, ModuleDefinition module, Type baseType, List parentTraits, - List members, Attributes attributes, bool isRefining) - : base(rangeToken, name, module, new List(), members, attributes, isRefining, parentTraits) { + public NewtypeDecl(RangeToken rangeToken, Name name, List typeParameters, ModuleDefinition module, + Type baseType, + SubsetTypeDecl.WKind witnessKind, Expression witness, List parentTraits, List members, Attributes attributes, bool isRefining) + : base(rangeToken, name, module, typeParameters, members, attributes, isRefining, parentTraits) { Contract.Requires(rangeToken != null); Contract.Requires(name != null); Contract.Requires(module != null); Contract.Requires(isRefining ^ (baseType != null)); + Contract.Requires((witnessKind == SubsetTypeDecl.WKind.Compiled || witnessKind == SubsetTypeDecl.WKind.Ghost) == (witness != null)); Contract.Requires(members != null); BaseType = baseType; + Witness = witness; + WitnessKind = witnessKind; this.NewSelfSynonym(); } - public NewtypeDecl(RangeToken rangeToken, Name name, ModuleDefinition module, BoundVar bv, Expression constraint, - SubsetTypeDecl.WKind witnessKind, Expression witness, List parentTraits, List members, Attributes attributes, bool isRefining) : base(rangeToken, name, module, new List(), members, attributes, isRefining, parentTraits) { + public NewtypeDecl(RangeToken rangeToken, Name name, List typeParameters, ModuleDefinition module, + BoundVar bv, Expression constraint, + SubsetTypeDecl.WKind witnessKind, Expression witness, List parentTraits, List members, Attributes attributes, bool isRefining) + : base(rangeToken, name, module, typeParameters, members, attributes, isRefining, parentTraits) { Contract.Requires(rangeToken != null); Contract.Requires(name != null); Contract.Requires(module != null); @@ -60,11 +67,16 @@ public NewtypeDecl(RangeToken rangeToken, Name name, ModuleDefinition module, Bo public Type ConcreteBaseType(List typeArguments) { Contract.Requires(TypeArgs.Count == typeArguments.Count); + if (typeArguments.Count == 0) { + // this optimization seems worthwhile + return BaseType; + } var subst = TypeParameter.SubstitutionMap(TypeArgs, typeArguments); return BaseType.Subst(subst); } - /// /// Return .BaseType instantiated with "typeArgs", but only look at the part of .BaseType that is in scope. + /// + /// Return .BaseType instantiated with "typeArgs", but only look at the part of .BaseType that is in scope. /// public Type RhsWithArgument(List typeArgs) { Contract.Requires(typeArgs != null); @@ -78,21 +90,7 @@ public Type RhsWithArgument(List typeArgs) { return rtd.SelfSynonym(typeArgs); } } - return RhsWithArgumentIgnoringScope(typeArgs); - } - /// - /// Returns the declared .BaseType but with formal type arguments replaced by the given actuals. - /// - public Type RhsWithArgumentIgnoringScope(List typeArgs) { - Contract.Requires(typeArgs != null); - Contract.Requires(typeArgs.Count == TypeArgs.Count); - // Instantiate with the actual type arguments - if (typeArgs.Count == 0) { - // this optimization seems worthwhile - return BaseType; - } else { - return ConcreteBaseType(typeArgs); - } + return ConcreteBaseType(typeArgs); } public TopLevelDecl AsTopLevelDecl => this; @@ -121,7 +119,7 @@ public TypeParameter.EqualitySupportValue EqualitySupport { bool ICodeContext.IsGhost { get { throw new NotSupportedException(); } // if .IsGhost is needed, the object should always be wrapped in an CodeContextWrapper } - List ICodeContext.TypeArgs { get { return new List(); } } + List ICodeContext.TypeArgs { get { return TypeArgs; } } List ICodeContext.Ins { get { return new List(); } } ModuleDefinition IASTVisitorContext.EnclosingModule { get { return EnclosingModuleDefinition; } } bool ICodeContext.MustReverify { get { return false; } } diff --git a/Source/DafnyCore/AST/TypeDeclarations/SubsetTypeDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/SubsetTypeDecl.cs index 15c2a5a2e82..d5c473087ac 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/SubsetTypeDecl.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/SubsetTypeDecl.cs @@ -50,6 +50,8 @@ public SubsetTypeDecl(RangeToken rangeToken, Name name, TypeParameter.TypeParame ); BoundVar RedirectingTypeDecl.Var => Var; + PreType RedirectingTypeDecl.BasePreType => Var.PreType; + Type RedirectingTypeDecl.BaseType => Var.Type; Expression RedirectingTypeDecl.Constraint => Constraint; WKind RedirectingTypeDecl.WitnessKind => WitnessKind; Expression RedirectingTypeDecl.Witness => Witness; diff --git a/Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDeclBase.cs b/Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDeclBase.cs index 57f35075f3e..3466a7113f6 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDeclBase.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDeclBase.cs @@ -64,6 +64,8 @@ public Type RhsWithArgumentIgnoringScope(List typeArgs) { Attributes RedirectingTypeDecl.Attributes { get { return Attributes; } } ModuleDefinition RedirectingTypeDecl.Module { get { return EnclosingModuleDefinition; } } BoundVar RedirectingTypeDecl.Var { get { return null; } } + PreType RedirectingTypeDecl.BasePreType { get { return null; } } + Type RedirectingTypeDecl.BaseType { get { return null; } } Expression RedirectingTypeDecl.Constraint { get { return null; } } bool RedirectingTypeDecl.ConstraintIsCompilable { diff --git a/Source/DafnyCore/AST/Types/TypeParameter.cs b/Source/DafnyCore/AST/Types/TypeParameter.cs index 9faeb2dcefe..7b4a5e1d70d 100644 --- a/Source/DafnyCore/AST/Types/TypeParameter.cs +++ b/Source/DafnyCore/AST/Types/TypeParameter.cs @@ -7,10 +7,13 @@ namespace Microsoft.Dafny; public class TypeParameter : TopLevelDecl { public interface ParentType { string FullName { get; } + IToken Tok { get; } } public override string WhatKind => "type parameter"; + public bool IsAutoCompleted => Name.StartsWith("_"); + ParentType parent; public ParentType Parent { get { diff --git a/Source/DafnyCore/AST/Types/Types.cs b/Source/DafnyCore/AST/Types/Types.cs index 19950989125..7c49af62df7 100644 --- a/Source/DafnyCore/AST/Types/Types.cs +++ b/Source/DafnyCore/AST/Types/Types.cs @@ -338,11 +338,10 @@ public bool IsNumericBased(NumericPersuasion p) { } else if (t.IsRealType) { return p == NumericPersuasion.Real; } - var d = t.AsNewtype; - if (d == null) { + if (t.AsNewtype is not { } newtypeDecl) { return false; } - t = d.BaseType; + t = newtypeDecl.RhsWithArgument(t.TypeArgs); } } diff --git a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs index 7db21e91763..f6e21f77093 100644 --- a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs +++ b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs @@ -1572,7 +1572,7 @@ internal override string TypeName(Type type, ConcreteSyntaxTree wr, IToken tok, return "bool"; } else if (xType is CharType) { return CharTypeName; - } else if (xType is IntType || xType is BigOrdinalType) { + } else if (xType is IntType or BigOrdinalType) { return "BigInteger"; } else if (xType is RealType) { return "Dafny.BigRational"; @@ -1580,11 +1580,11 @@ internal override string TypeName(Type type, ConcreteSyntaxTree wr, IToken tok, var t = (BitvectorType)xType; return t.NativeType != null ? GetNativeTypeName(t.NativeType) : "BigInteger"; } else if (xType.AsNewtype != null && member == null) { // when member is given, use UserDefinedType case below - var nativeType = xType.AsNewtype.NativeType; - if (nativeType != null) { + var newtypeDecl = xType.AsNewtype; + if (newtypeDecl.NativeType is { } nativeType) { return GetNativeTypeName(nativeType); } - return TypeName(xType.AsNewtype.BaseType, wr, tok); + return TypeName(newtypeDecl.ConcreteBaseType(xType.TypeArgs), wr, tok); } else if (xType.IsObjectQ) { return "object"; } else if (xType.IsArrayType) { @@ -1679,7 +1679,7 @@ protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree return "false"; } else if (xType is CharType) { return UnicodeCharEnabled ? $"new {CharTypeName}({CharType.DefaultValueAsString})" : CharType.DefaultValueAsString; - } else if (xType is IntType || xType is BigOrdinalType) { + } else if (xType is IntType or BigOrdinalType) { return "BigInteger.Zero"; } else if (xType is RealType) { return "Dafny.BigRational.ZERO"; @@ -1708,7 +1708,7 @@ protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree } else if (td.NativeType != null) { return "0"; } else { - return TypeInitializationValue(td.BaseType, wr, tok, usePlaceboValue, constructTypeParameterDefaultsFromTypeDescriptors); + return TypeInitializationValue(td.ConcreteBaseType(udt.TypeArgs), wr, tok, usePlaceboValue, constructTypeParameterDefaultsFromTypeDescriptors); } } else if (cl is SubsetTypeDecl) { var td = (SubsetTypeDecl)cl; diff --git a/Source/DafnyCore/Backends/CodeGeneratorTypeExtensions.cs b/Source/DafnyCore/Backends/CodeGeneratorTypeExtensions.cs index e72ebd608c2..1fae5747c3e 100644 --- a/Source/DafnyCore/Backends/CodeGeneratorTypeExtensions.cs +++ b/Source/DafnyCore/Backends/CodeGeneratorTypeExtensions.cs @@ -14,8 +14,7 @@ public static class CompilerTypeExtensions { /// public static Type GetRuntimeType(this Type typ) { while (typ.AsNewtype is { NativeType: null } newtypeDecl) { - var subst = TypeParameter.SubstitutionMap(newtypeDecl.TypeArgs, typ.TypeArgs); - typ = newtypeDecl.BaseType.Subst(subst); + typ = newtypeDecl.ConcreteBaseType(typ.TypeArgs); } return typ.NormalizeExpand(); } diff --git a/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs b/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs index 30c188ebc8c..8eada0edcdf 100644 --- a/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs +++ b/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs @@ -923,7 +923,7 @@ protected string TypeName(Type type, ConcreteSyntaxTree wr, IToken tok, MemberDe return "bool"; } else if (xType is CharType) { return "char"; - } else if (xType is IntType || xType is BigOrdinalType) { + } else if (xType is IntType or BigOrdinalType) { UnsupportedFeatureError(tok, Feature.UnboundedIntegers); return "BigNumber"; } else if (xType is RealType) { @@ -933,11 +933,11 @@ protected string TypeName(Type type, ConcreteSyntaxTree wr, IToken tok, MemberDe var t = (BitvectorType)xType; return t.NativeType != null ? GetNativeTypeName(t.NativeType) : "BigNumber"; } else if (xType.AsNewtype != null) { - NativeType nativeType = xType.AsNewtype.NativeType; - if (nativeType != null) { + var newtypeDecl = xType.AsNewtype; + if (newtypeDecl.NativeType is { } nativeType) { return GetNativeTypeName(nativeType); } - return TypeName(xType.AsNewtype.BaseType, wr, tok); + return TypeName(newtypeDecl.ConcreteBaseType(xType.TypeArgs), wr, tok, member); } else if (xType.IsObjectQ) { return "object"; } else if (xType.IsArrayType) { @@ -1046,7 +1046,7 @@ protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree } else if (td.NativeType != null) { return "0"; } else { - return TypeInitializationValue(td.BaseType, wr, tok, usePlaceboValue, constructTypeParameterDefaultsFromTypeDescriptors); + return TypeInitializationValue(td.ConcreteBaseType(udt.TypeArgs), wr, tok, usePlaceboValue, constructTypeParameterDefaultsFromTypeDescriptors); } } else if (cl is SubsetTypeDecl) { var td = (SubsetTypeDecl)cl; diff --git a/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs b/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs index dd5b3574d6b..55ddecdc1e5 100644 --- a/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs +++ b/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs @@ -1593,11 +1593,11 @@ internal override string TypeName(Type type, ConcreteSyntaxTree wr, IToken tok, var t = (BitvectorType)xType; return t.NativeType != null ? GetNativeTypeName(t.NativeType) : "_dafny.BV"; } else if (xType.AsNewtype != null && member == null) { // when member is given, use UserDefinedType case below - NativeType nativeType = xType.AsNewtype.NativeType; - if (nativeType != null) { + var newtypeDecl = xType.AsNewtype; + if (newtypeDecl.NativeType is { } nativeType) { return GetNativeTypeName(nativeType); } - return TypeName(xType.AsNewtype.BaseType, wr, tok); + return TypeName(newtypeDecl.ConcreteBaseType(xType.TypeArgs), wr, tok); } else if (xType.IsObjectQ) { return AnyType; } else if (xType.IsArrayType) { @@ -1652,7 +1652,7 @@ string nil() { return "false"; } else if (xType is CharType) { return $"{CharTypeName}({CharType.DefaultValueAsString})"; - } else if (xType is IntType || xType is BigOrdinalType) { + } else if (xType is IntType or BigOrdinalType) { return "_dafny.Zero"; } else if (xType is RealType) { return "_dafny.ZeroReal"; @@ -1696,7 +1696,7 @@ string nil() { } else if (td.NativeType != null) { return GetNativeTypeName(td.NativeType) + "(0)"; } else { - return TypeInitializationValue(td.BaseType, wr, tok, usePlaceboValue, constructTypeParameterDefaultsFromTypeDescriptors); + return TypeInitializationValue(td.ConcreteBaseType(udt.TypeArgs), wr, tok, usePlaceboValue, constructTypeParameterDefaultsFromTypeDescriptors); } } else if (cl is SubsetTypeDecl) { var td = (SubsetTypeDecl)cl; @@ -3915,9 +3915,7 @@ protected override ConcreteSyntaxTree EmitCoercionIfNecessary(Type/*?*/ from, Ty return w; } } else if (from.AsNewtype is { } fromNewtypeDecl) { - var subst = TypeParameter.SubstitutionMap(fromNewtypeDecl.TypeArgs, from.TypeArgs); - from = fromNewtypeDecl.BaseType.Subst(subst); - return EmitCoercionIfNecessary(from, to, tok, wr, toOrig); + return EmitCoercionIfNecessary(fromNewtypeDecl.ConcreteBaseType(from.TypeArgs), to, tok, wr, toOrig); } else { // It's unclear to me whether it's possible to hit this case with a valid Dafny program, // so I'm not using UnsupportedFeatureError for now. diff --git a/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs b/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs index 28dd059e6c8..c7ee9c2c663 100644 --- a/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs +++ b/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs @@ -710,7 +710,7 @@ private string TypeName(Type type, ConcreteSyntaxTree wr, IToken tok, bool boxed return boxed ? "Boolean" : "boolean"; } else if (xType is CharType) { return CharTypeName(boxed); - } else if (xType is IntType || xType is BigOrdinalType) { + } else if (xType is IntType or BigOrdinalType) { return "java.math.BigInteger"; } else if (xType is RealType) { return DafnyBigRationalClass; @@ -718,11 +718,11 @@ private string TypeName(Type type, ConcreteSyntaxTree wr, IToken tok, bool boxed var t = (BitvectorType)xType; return t.NativeType != null ? GetNativeTypeName(t.NativeType, boxed) : "java.math.BigInteger"; } else if (member == null && xType.AsNewtype != null) { - var nativeType = xType.AsNewtype.NativeType; - if (nativeType != null) { + var newtypeDecl = xType.AsNewtype; + if (newtypeDecl.NativeType is { } nativeType) { return GetNativeTypeName(nativeType, boxed); } - return TypeName(xType.AsNewtype.BaseType, wr, tok, boxed, erased); + return TypeName(newtypeDecl.ConcreteBaseType(xType.TypeArgs), wr, tok, boxed, erased); } else if (xType.IsObjectQ) { return "Object"; } else if (xType.IsArrayType) { @@ -3200,7 +3200,7 @@ protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree return "false"; } else if (xType is CharType) { return UnicodeCharEnabled ? $"((int){CharType.DefaultValueAsString})" : CharType.DefaultValueAsString; - } else if (xType is IntType || xType is BigOrdinalType) { + } else if (xType is IntType or BigOrdinalType) { return "java.math.BigInteger.ZERO"; } else if (xType is RealType) { return $"{DafnyBigRationalClass}.ZERO"; @@ -3240,7 +3240,7 @@ protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree } else if (td.NativeType != null) { return GetNativeDefault(td.NativeType); } else { - return TypeInitializationValue(td.BaseType, wr, tok, usePlaceboValue, constructTypeParameterDefaultsFromTypeDescriptors); + return TypeInitializationValue(td.ConcreteBaseType(udt.TypeArgs), wr, tok, usePlaceboValue, constructTypeParameterDefaultsFromTypeDescriptors); } } else if (cl is SubsetTypeDecl) { var td = (SubsetTypeDecl)cl; diff --git a/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs b/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs index 87d4b5b4835..ad1b85bd8f7 100644 --- a/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs +++ b/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs @@ -914,7 +914,7 @@ internal override string TypeName(Type type, ConcreteSyntaxTree wr, IToken tok, return "bool"; } else if (xType is CharType) { return "char"; - } else if (xType is IntType || xType is BigOrdinalType) { + } else if (xType is IntType or BigOrdinalType) { return "BigNumber"; } else if (xType is RealType) { return "Dafny.BigRational"; @@ -922,11 +922,11 @@ internal override string TypeName(Type type, ConcreteSyntaxTree wr, IToken tok, var t = (BitvectorType)xType; return t.NativeType != null ? GetNativeTypeName(t.NativeType) : "BigNumber"; } else if (xType.AsNewtype != null && member == null) { // when member is given, use UserDefinedType case below - NativeType nativeType = xType.AsNewtype.NativeType; - if (nativeType != null) { + var newtypeDecl = xType.AsNewtype; + if (newtypeDecl.NativeType is { } nativeType) { return GetNativeTypeName(nativeType); } - return TypeName(xType.AsNewtype.BaseType, wr, tok); + return TypeName(newtypeDecl.ConcreteBaseType(xType.TypeArgs), wr, tok); } else if (xType.IsObjectQ) { return "object"; } else if (xType.IsArrayType) { @@ -961,7 +961,7 @@ protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree return "false"; } else if (xType is CharType) { return $"{CharFromNumberMethodName()}({CharType.DefaultValueAsString}.codePointAt(0))"; - } else if (xType is IntType || xType is BigOrdinalType) { + } else if (xType is IntType or BigOrdinalType) { return IntegerLiteral(0); } else if (xType is RealType) { return "_dafny.BigRational.ZERO"; @@ -1003,7 +1003,7 @@ protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree } else if (td.NativeType != null) { return "0"; } else { - return TypeInitializationValue(td.BaseType, wr, tok, usePlaceboValue, constructTypeParameterDefaultsFromTypeDescriptors); + return TypeInitializationValue(td.ConcreteBaseType(udt.TypeArgs), wr, tok, usePlaceboValue, constructTypeParameterDefaultsFromTypeDescriptors); } } else if (cl is SubsetTypeDecl) { var td = (SubsetTypeDecl)cl; diff --git a/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs b/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs index 222a98aa2be..7783c33a038 100644 --- a/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs +++ b/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs @@ -755,11 +755,11 @@ internal override string TypeName(Type type, ConcreteSyntaxTree wr, IToken tok, if (xType.AsNewtype != null && member == null) { // when member is given, use UserDefinedType case below - var nativeType = xType.AsNewtype.NativeType; - if (nativeType != null) { + var newtypeDecl = xType.AsNewtype; + if (newtypeDecl.NativeType is { } nativeType) { return GetNativeTypeName(nativeType); } - return TypeName(xType.AsNewtype.BaseType, wr, tok, member); + return TypeName(newtypeDecl.ConcreteBaseType(xType.TypeArgs), wr, tok); } switch (xType) { @@ -855,7 +855,7 @@ protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree if (td.Witness != null) { return TypeName_UDT(FullName(cl), udt, wr, udt.tok) + ".default()"; } else { - return TypeInitializationValue(td.BaseType, wr, tok, usePlaceboValue, constructTypeParameterDefaultsFromTypeDescriptors); + return TypeInitializationValue(td.ConcreteBaseType(udt.TypeArgs), wr, tok, usePlaceboValue, constructTypeParameterDefaultsFromTypeDescriptors); } case DatatypeDecl dt: diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg index d069d01cb73..5873add2c99 100644 --- a/Source/DafnyCore/Dafny.atg +++ b/Source/DafnyCore/Dafny.atg @@ -771,10 +771,12 @@ NewtypeDecl CheckDeclModifiers(ref dmod, "newtype", AllowedDeclModifiers.None); List parentTraits = new List(); var members = new List(); + var typeParameters = new List(); .) "newtype" (. CheckAndSetTokenOnce(ref dmod.FirstToken); .) { Attribute } NewtypeName + [ GenericParameters ] [ ExtendsClause ] ( "=" @@ -786,29 +788,25 @@ NewtypeDecl [ ":" Type ] "|" Expression - (. var witnessKind = SubsetTypeDecl.WKind.CompiledZero; .) - [ IF(IsWitness()) - ( "ghost" "witness" (. witnessKind = SubsetTypeDecl.WKind.Ghost; .) - Expression - | "witness" - ( "*" (. witnessKind = SubsetTypeDecl.WKind.OptOut; .) - | Expression (. witnessKind = SubsetTypeDecl.WKind.Compiled; .) - ) - ) - ] + WitnessClause [ TypeMembers ] - (. td = new NewtypeDecl(new RangeToken(dmod.FirstToken, t), name, module, - new BoundVar(bvId, bvId.val, baseType), + (. td = new NewtypeDecl(new RangeToken(dmod.FirstToken, t), name, typeParameters, module, + new BoundVar(bvId, bvId.val, baseType), constraint, witnessKind, witness, parentTraits, members, attrs, isRefining: false); .) | Type + WitnessClause [ TypeMembers ] - (. td = new NewtypeDecl(new RangeToken(dmod.FirstToken, t), name, module, baseType, parentTraits, members, attrs, isRefining: false); .) + (. td = new NewtypeDecl(new RangeToken(dmod.FirstToken, t), name, typeParameters, module, + baseType, witnessKind, witness, parentTraits, members, attrs, isRefining: false); + .) ) | ellipsis [ TypeMembers ] (. baseType = null; // Base type is not known yet - td = new NewtypeDecl(new RangeToken(dmod.FirstToken, t), name, module, baseType, parentTraits, members, attrs, isRefining: true); + td = new NewtypeDecl(new RangeToken(dmod.FirstToken, t), name, typeParameters, module, baseType, + SubsetTypeDecl.WKind.CompiledZero, null, + parentTraits, members, attrs, isRefining: true); .) ) (. if (td != null) { td.TokenWithTrailingDocString = t; @@ -844,16 +842,7 @@ SynonymTypeDecl ] "|" Expression - (. var witnessKind = SubsetTypeDecl.WKind.CompiledZero; .) - [ IF(IsWitness()) - ( "ghost" "witness" (. witnessKind = SubsetTypeDecl.WKind.Ghost; .) - Expression - | "witness" - ( "*" (. witnessKind = SubsetTypeDecl.WKind.OptOut; .) - | Expression (. witnessKind = SubsetTypeDecl.WKind.Compiled; .) - ) - ) - ] + WitnessClause (. td = new SubsetTypeDecl(new RangeToken(dmod.FirstToken, t), name, characteristics, typeArgs, module, new BoundVar(bvId, bvId.val, ty), constraint, witnessKind, witness, attrs); kind = "subset type"; @@ -882,6 +871,21 @@ SynonymTypeDecl += (. witnessKind = SubsetTypeDecl.WKind.CompiledZero; + witness = null; + .) + [ IF(IsWitness()) + ( "ghost" "witness" (. witnessKind = SubsetTypeDecl.WKind.Ghost; .) + Expression + | "witness" + ( "*" (. witnessKind = SubsetTypeDecl.WKind.OptOut; .) + | Expression (. witnessKind = SubsetTypeDecl.WKind.Compiled; .) + ) + ) + ] + . + /*------------------------------------------------------------------------*/ GIdentType diff --git a/Source/DafnyCore/Resolver/ModuleResolver.cs b/Source/DafnyCore/Resolver/ModuleResolver.cs index e86b26eaf30..7dd234f7f03 100644 --- a/Source/DafnyCore/Resolver/ModuleResolver.cs +++ b/Source/DafnyCore/Resolver/ModuleResolver.cs @@ -431,7 +431,7 @@ public void ResolveModuleExport(LiteralModuleDecl literalDecl, ModuleSignature s } } - if (e.Opaque && (decl is DatatypeDecl or TypeSynonymDecl)) { + if (e.Opaque && (decl is DatatypeDecl or TypeSynonymDecl or NewtypeDecl)) { // Datatypes and type synonyms are marked as _provided when they appear in any provided export. If a // declaration is never provided, then either it isn't visible outside the module at all or its whole // definition is. Datatype and type-synonym declarations undergo some inference from their definitions. @@ -2156,8 +2156,8 @@ public void RegisterInheritedMembers(TopLevelDeclWithMembers cl, [CanBeNull] DPr // ignore any subset types, since they have no members and thus we don't need their type-parameter mappings var baseType = newtypeDecl.BaseType.NormalizeExpand(); baseTypeArguments = baseType.TypeArgs; - if (baseType is UserDefinedType udtBaseType) { - baseTypeDecl = (TopLevelDeclWithMembers)udtBaseType.ResolvedClass; + if (baseType is UserDefinedType { ResolvedClass: TopLevelDeclWithMembers topLevelDeclWithMembers }) { + baseTypeDecl = topLevelDeclWithMembers; } else if (Options.Get(CommonOptionBag.GeneralNewtypes) || baseType.IsIntegerType || baseType.IsRealType) { baseTypeDecl = GetSystemValuetypeDecl(baseType); } @@ -2576,7 +2576,7 @@ private Dictionary CheckOverride_TypeParameters(IToken tok, for (var i = 0; i < old.Count; i++) { var o = old[i]; var n = nw[i]; - CheckOverride_TypeBounds(tok, o, n, name, thing, typeMap); + CheckOverride_TypeBounds(n.tok, o, n, name, thing, typeMap); } } return typeMap; @@ -3619,7 +3619,7 @@ Expression CombineConstraints(Type baseType, BoundVar boundVar, Expression const } if (udt.ResolvedClass is NewtypeDecl newtypeDecl) { - return CombineConstraints(newtypeDecl.BaseType, newtypeDecl.Var, newtypeDecl.Constraint); + return CombineConstraints(newtypeDecl.RhsWithArgument(udt.TypeArgs), newtypeDecl.Var, newtypeDecl.Constraint); } if (udt.ResolvedClass is SubsetTypeDecl subsetTypeDecl) { return CombineConstraints(subsetTypeDecl.RhsWithArgument(udt.TypeArgs), subsetTypeDecl.Var, subsetTypeDecl.Constraint); diff --git a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs index 66a27e333de..6312718c3ef 100644 --- a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs +++ b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs @@ -130,7 +130,7 @@ void ResolveNamesAndInferTypesForOneDeclaration(TopLevelDecl topd) { scope.AllowInstance = false; ResolveExpression(newtypeDecl.Witness, new ResolutionContext(codeContext, false)); scope.PopMarker(); - ConstrainSubtypeRelation(newtypeDecl.Var.Type, newtypeDecl.Witness.Type, newtypeDecl.Witness, "witness expression must have type '{0}' (got '{1}')", newtypeDecl.Var.Type, newtypeDecl.Witness.Type); + ConstrainSubtypeRelation(newtypeDecl.BaseType, newtypeDecl.Witness.Type, newtypeDecl.Witness, "witness expression must have type '{0}' (got '{1}')", newtypeDecl.BaseType, newtypeDecl.Witness.Type); } SolveAllTypeConstraints(); @@ -4305,7 +4305,8 @@ static void FillInTypeArguments(IToken tok, int n, List typeArgs, List GetTypeArgumentsForSuperType(TopLevelDecl super, DPreType s if (allowBaseTypeCast && sub.Decl is NewtypeDecl newtypeDecl) { var subst = PreType.PreTypeSubstMap(newtypeDecl.TypeArgs, sub.Arguments); - var basePreType = (DPreType)newtypeDecl.BasePreType.Substitute(subst); - var arguments = GetTypeArgumentsForSuperType(super, basePreType, true); - if (arguments != null) { - return arguments; + if (newtypeDecl.BasePreType.Substitute(subst) is DPreType basePreType) { + var arguments = GetTypeArgumentsForSuperType(super, basePreType, true); + if (arguments != null) { + return arguments; + } } } diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs index 5a8488c60b1..7eb68bc7b62 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs @@ -250,8 +250,7 @@ public void ResolveExpression(Expression expr, ResolutionContext resolutionConte ResolveExpression(e.Index, resolutionContext); ResolveExpression(e.Value, resolutionContext); Constraints.AddGuardedConstraint(() => { - var sourcePreType = e.Seq.PreType.NormalizeWrtScope() as DPreType; - var ancestorPreType = sourcePreType == null ? null : AncestorPreType(sourcePreType); + var ancestorPreType = e.Seq.PreType.NormalizeWrtScope() is not DPreType sourcePreType ? null : AncestorPreType(sourcePreType); var familyDeclName = ancestorPreType?.Decl.Name; if (familyDeclName == PreType.TypeNameSeq) { var elementPreType = ancestorPreType.Arguments[0]; @@ -384,8 +383,7 @@ public void ResolveExpression(Expression expr, ResolutionContext resolutionConte Constraints.AddGuardedConstraint(() => { if (e.E.PreType.NormalizeWrtScope() is DPreType dp) { var familyDeclName = AncestorName(dp); - if (familyDeclName is PreType.TypeNameSet or PreType.TypeNameSeq) { - var ancestorPreType = AncestorPreType(dp); + if (familyDeclName is PreType.TypeNameSet or PreType.TypeNameSeq && AncestorPreType(dp) is { } ancestorPreType) { Contract.Assert(ancestorPreType.Arguments.Count == 1); var sourceElementPreType = ancestorPreType.Arguments[0]; AddSubtypeConstraint(targetElementPreType, sourceElementPreType, e.E.tok, "expecting element type {0} (got {1})"); @@ -467,28 +465,34 @@ resolutionContext.CodeContext is ConstantField || var prevErrorCount = ErrorCount; resolver.ResolveType(e.tok, e.ToType, resolutionContext, new ModuleResolver.ResolveTypeOption(ResolveTypeOptionEnum.InferTypeProxies), null); if (ErrorCount == prevErrorCount) { - string errorMessageFormat; - var toPreType = (DPreType)Type2PreType(e.ToType); - var ancestorDecl = AncestorDecl(toPreType.Decl); - var familyDeclName = ancestorDecl.Name; - if (familyDeclName == PreType.TypeNameInt) { - errorMessageFormat = "type conversion to an int-based type is allowed only from numeric and bitvector types, char, and ORDINAL (got {1})"; - } else if (familyDeclName == PreType.TypeNameReal) { - errorMessageFormat = "type conversion to a real-based type is allowed only from numeric and bitvector types, char, and ORDINAL (got {1})"; - } else if (IsBitvectorName(familyDeclName)) { - errorMessageFormat = "type conversion to a bitvector-based type is allowed only from numeric and bitvector types, char, and ORDINAL (got {1})"; - } else if (familyDeclName == PreType.TypeNameChar) { - errorMessageFormat = "type conversion to a char type is allowed only from numeric and bitvector types, char, and ORDINAL (got {1})"; - } else if (familyDeclName == PreType.TypeNameORDINAL) { - errorMessageFormat = "type conversion to an ORDINAL type is allowed only from numeric and bitvector types, char, and ORDINAL (got {1})"; - } else if (DPreType.IsReferenceTypeDecl(ancestorDecl)) { - errorMessageFormat = "type cast to reference type '{0}' must be from an expression of a compatible type (got '{1}')"; - } else if (ancestorDecl is TraitDecl) { - errorMessageFormat = "type cast to trait type '{0}' must be from an expression of a compatible type (got '{1}')"; - } else { - errorMessageFormat = "type cast to type '{0}' must be from an expression of a compatible type (got '{1}')"; - } - AddComparableConstraint(toPreType, e.E.PreType, conversionExpr.tok, true, errorMessageFormat); + var toPreType = Type2PreType(e.ToType); + var errorMessage = () => { + string errorMessageFormat; + if (toPreType.Normalize() is DPreType dtoPreType && AncestorPreType(dtoPreType)?.Decl is { } ancestorDecl) { + var familyDeclName = ancestorDecl.Name; + if (familyDeclName == PreType.TypeNameInt) { + errorMessageFormat = "type conversion to an int-based type is allowed only from numeric and bitvector types, char, and ORDINAL (got {1})"; + } else if (familyDeclName == PreType.TypeNameReal) { + errorMessageFormat = "type conversion to a real-based type is allowed only from numeric and bitvector types, char, and ORDINAL (got {1})"; + } else if (IsBitvectorName(familyDeclName)) { + errorMessageFormat = "type conversion to a bitvector-based type is allowed only from numeric and bitvector types, char, and ORDINAL (got {1})"; + } else if (familyDeclName == PreType.TypeNameChar) { + errorMessageFormat = "type conversion to a char type is allowed only from numeric and bitvector types, char, and ORDINAL (got {1})"; + } else if (familyDeclName == PreType.TypeNameORDINAL) { + errorMessageFormat = "type conversion to an ORDINAL type is allowed only from numeric and bitvector types, char, and ORDINAL (got {1})"; + } else if (DPreType.IsReferenceTypeDecl(ancestorDecl)) { + errorMessageFormat = "type cast to reference type '{0}' must be from an expression of a compatible type (got '{1}')"; + } else if (ancestorDecl is TraitDecl) { + errorMessageFormat = "type cast to trait type '{0}' must be from an expression of a compatible type (got '{1}')"; + } else { + errorMessageFormat = "type cast to type '{0}' must be from an expression of a compatible type (got '{1}')"; + } + } else { + errorMessageFormat = "type conversion target type not determined (got '{0}')"; + } + return string.Format(errorMessageFormat, toPreType, e.E.PreType); + }; + AddComparableConstraint(toPreType, e.E.PreType, expr.tok, true, errorMessage); e.PreType = toPreType; } else { e.PreType = CreatePreTypeProxy("'as' target type"); @@ -2141,8 +2145,7 @@ PreType ResolveSingleSelectionExpr(IToken tok, PreType collectionPreType, Expres var resultPreType = CreatePreTypeProxy("selection []"); Constraints.AddGuardedConstraint(() => { var sourcePreType = Constraints.ApproximateReceiverType(collectionPreType, null); - if (sourcePreType != null) { - var ancestorPreType = AncestorPreType(sourcePreType); + if (sourcePreType != null && AncestorPreType(sourcePreType) is { } ancestorPreType) { var familyDeclName = ancestorPreType.Decl.Name; switch (familyDeclName) { case PreType.TypeNameArray: @@ -2195,7 +2198,7 @@ void ResolveRangeSelectionExpr(IToken tok, PreType sourceCollectionPreType, Expr "resulting sequence ({0}) type does not agree with source sequence type ({1})"); break; case PreType.TypeNameArray: - AddSubtypeConstraint(resultElementPreType, AncestorPreType(sourcePreType).Arguments[0], tok, + AddSubtypeConstraint(resultElementPreType, AncestorPreType(sourcePreType)!.Arguments[0], tok, "type does not agree with element type {1} (got {0})"); break; default: diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs index c3f1c519459..33a43991bda 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs @@ -258,36 +258,28 @@ public IEnumerable TypeParameterBounds2PreTypes(TypeParameter typePara } } - /// - /// 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 - /// have been done. - /// - public static TopLevelDecl AncestorDecl(TopLevelDecl decl) { - while (decl is NewtypeDecl newtypeDecl) { - var parent = newtypeDecl.BasePreType.Normalize(); - decl = ((DPreType)parent).Decl; - } - return decl; - } - /// /// Returns the non-newtype ancestor pre-type of "preType". /// This method assumes that the ancestors of "preType.Decl" do not form any cycles. That is, any such cycle detection must already /// have been done. + /// If the base type is a type parameter (of the newtype's) and that type parameter is not determined, then this method returns null. /// + [CanBeNull] public static DPreType AncestorPreType(DPreType preType) { while (preType.Decl is NewtypeDecl newtypeDecl) { var subst = PreType.PreTypeSubstMap(newtypeDecl.TypeArgs, preType.Arguments); - preType = (DPreType)newtypeDecl.BasePreType.Substitute(subst); + if (newtypeDecl.BasePreType.Substitute(subst).Normalize() is DPreType baseWithSubstitution) { + preType = baseWithSubstitution; + } else { + return null; + } } return preType; } [CanBeNull] public static string AncestorName(PreType preType) { - var dp = preType.Normalize() as DPreType; - return dp == null ? null : AncestorDecl(dp.Decl).Name; + return preType.Normalize() is not DPreType dp ? null : AncestorPreType(dp)?.Decl.Name; } /// @@ -305,13 +297,19 @@ public static DPreType NewTypeAncestor(DPreType preType) { break; } visited.Add(newtypeDecl); - var parent = newtypeDecl.BasePreType.Normalize() as DPreType; - if (parent == null) { + if (newtypeDecl.BasePreType.Normalize() is not DPreType parent) { // The parent type of this newtype apparently hasn't been inferred yet, so stop traversal here break; } var subst = PreType.PreTypeSubstMap(newtypeDecl.TypeArgs, preType.Arguments); - preType = (DPreType)parent.Substitute(subst); + if (parent.Substitute(subst) is not DPreType parentWithSubstitutions) { + // The head type of result of the substitution into the parent is not yet inferred. This must have been because + // the parent is a type parameter of the newtype and the actual type argument hasn't been inferred yet. So, we + // stop here and return the type-parameter parent. + Contract.Assert(parent.Decl is TypeParameter); + break; + } + preType = parentWithSubstitutions; } return preType; } @@ -512,12 +510,17 @@ void AddConfirmation(PreTypeConstraints.CommonConfirmationBag check, PreType pre } void AddComparableConstraint(PreType a, PreType b, IToken tok, bool allowBaseTypeCast, string errorFormatString) { + AddComparableConstraint(a, b, tok, allowBaseTypeCast, () => string.Format(errorFormatString, a, b)); + } + + void AddComparableConstraint(PreType a, PreType b, IToken tok, bool allowBaseTypeCast, Func errorMessage) { // A "comparable types" constraint involves a disjunction. This can get gnarly for inference, so the full disjunction // is checked post inference. The constraint can, however, be of use during inference, so we also add an approximate // constraint (which is set up NOT to generate any error messages by itself, since otherwise errors would be duplicated). Constraints.AddGuardedConstraint(() => ApproximateComparableConstraints(a, b, tok, allowBaseTypeCast, - "(Duplicate error message) " + errorFormatString, false)); - Constraints.AddConfirmation(tok, () => CheckComparableTypes(a, b, allowBaseTypeCast), () => string.Format(errorFormatString, a, b)); + "(Duplicate error message) " + errorMessage(), false)); + Constraints.AddConfirmation(tok, () => CheckComparableTypes(a, b, allowBaseTypeCast), errorMessage); + //Func errorMessage } /// @@ -562,6 +565,9 @@ bool CheckComparableTypes(PreType a, PreType b, bool allowConversion) { bool IsConversionCompatible(DPreType fromType, DPreType toType) { var fromAncestor = AncestorPreType(fromType); var toAncestor = AncestorPreType(toType); + if (fromAncestor == null || toAncestor == null) { + return false; + } if (PreType.Same(fromAncestor, toAncestor)) { return true; @@ -1049,7 +1055,7 @@ void ResolveConstraintAndWitness(RedirectingTypeDecl dd, bool initialResolutionP scope.AllowInstance = false; ResolveExpression(dd.Witness, new ResolutionContext(codeContext, false)); scope.PopMarker(); - AddSubtypeConstraint(dd.Var.PreType, dd.Witness.PreType, dd.Witness.tok, "witness expression must have type '{0}' (got '{1}')"); + AddSubtypeConstraint(dd.BasePreType, dd.Witness.PreType, dd.Witness.tok, "witness expression must have type '{0}' (got '{1}')"); Constraints.SolveAllTypeConstraints($"{dd.WhatKind} '{dd.Name}' witness"); } } diff --git a/Source/DafnyCore/Resolver/PreType/UnderspecificationDetector.cs b/Source/DafnyCore/Resolver/PreType/UnderspecificationDetector.cs index d320863b6ef..27d33b0978b 100644 --- a/Source/DafnyCore/Resolver/PreType/UnderspecificationDetector.cs +++ b/Source/DafnyCore/Resolver/PreType/UnderspecificationDetector.cs @@ -426,7 +426,7 @@ static BinaryExpr.ResolvedOpcode ResolveOp(BinaryExpr.Opcode op, PreType leftOpe case BinaryExpr.Opcode.Disjoint: return operandFamilyName == PreType.TypeNameMultiset ? BinaryExpr.ResolvedOpcode.MultiSetDisjoint : BinaryExpr.ResolvedOpcode.Disjoint; case BinaryExpr.Opcode.Lt: { - if (operandPreType is DPreType dp && PreTypeResolver.AncestorDecl(dp.Decl) is IndDatatypeDecl) { + if (operandPreType is DPreType dp && PreTypeResolver.AncestorPreType(dp)?.Decl is IndDatatypeDecl) { return BinaryExpr.ResolvedOpcode.RankLt; } return operandFamilyName switch { @@ -475,7 +475,7 @@ static BinaryExpr.ResolvedOpcode ResolveOp(BinaryExpr.Opcode op, PreType leftOpe _ => BinaryExpr.ResolvedOpcode.Mul }; case BinaryExpr.Opcode.Gt: { - if (operandPreType is DPreType dp && PreTypeResolver.AncestorDecl(dp.Decl) is IndDatatypeDecl) { + if (operandPreType is DPreType dp && PreTypeResolver.AncestorPreType(dp)?.Decl is IndDatatypeDecl) { return BinaryExpr.ResolvedOpcode.RankGt; } return operandFamilyName switch { diff --git a/Source/DafnyCore/Resolver/TypeCharacteristicChecker.cs b/Source/DafnyCore/Resolver/TypeCharacteristicChecker.cs index 1b0c06aa84f..52cef103e65 100644 --- a/Source/DafnyCore/Resolver/TypeCharacteristicChecker.cs +++ b/Source/DafnyCore/Resolver/TypeCharacteristicChecker.cs @@ -21,14 +21,14 @@ public class TypeCharacteristicChecker { /// Note that this method can only be called after determining which expressions are ghosts. /// public static void InferAndCheck(List declarations, bool isAnExport, ErrorReporter reporter) { - InferEqualitySupport(declarations); + InferEqualitySupport(declarations, reporter); Check(declarations, isAnExport, reporter); } /// /// Inferred required equality support for datatypes and type synonyms, and for Function and Method signatures. /// - private static void InferEqualitySupport(List declarations) { + private static void InferEqualitySupport(List declarations, ErrorReporter reporter) { // First, do datatypes and type synonyms until a fixpoint is reached. bool inferredSomething; do { @@ -43,8 +43,7 @@ private static void InferEqualitySupport(List declarations) { // here's our chance to infer the need for equality support foreach (var ctor in dt.Ctors) { foreach (var arg in ctor.Formals) { - if (InferRequiredEqualitySupport(tp, arg.Type)) { - tp.Characteristics.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired; + if (InferAndSetEqualitySupport(tp, arg.Type, reporter)) { inferredSomething = true; goto DONE_DT; // break out of the doubly-nested loop } @@ -57,8 +56,16 @@ private static void InferEqualitySupport(List declarations) { foreach (var tp in syn.TypeArgs) { if (tp.Characteristics.EqualitySupport == TypeParameter.EqualitySupportValue.Unspecified) { // here's our chance to infer the need for equality support - if (InferRequiredEqualitySupport(tp, syn.Rhs)) { - tp.Characteristics.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired; + if (InferAndSetEqualitySupport(tp, syn.Rhs, reporter)) { + inferredSomething = true; + } + } + } + } else if (d is NewtypeDecl newtypeDecl) { + foreach (var tp in newtypeDecl.TypeArgs) { + if (tp.Characteristics.EqualitySupport == TypeParameter.EqualitySupportValue.Unspecified) { + // here's our chance to infer the need for equality support + if (InferAndSetEqualitySupport(tp, newtypeDecl.BaseType, reporter)) { inferredSomething = true; } } @@ -79,10 +86,8 @@ private static void InferEqualitySupport(List declarations) { if (tp.Characteristics.EqualitySupport == TypeParameter.EqualitySupportValue.Unspecified) { // here's our chance to infer the need for equality support foreach (var p in iter.Ins) { - if (InferRequiredEqualitySupport(tp, p.Type)) { - tp.Characteristics.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired; - correspondingNonnullIterTypeParameter.Characteristics.EqualitySupport = - TypeParameter.EqualitySupportValue.InferredRequired; + if (InferAndSetEqualitySupport(tp, p.Type, reporter)) { + correspondingNonnullIterTypeParameter.Characteristics.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired; done = true; break; } @@ -92,10 +97,8 @@ private static void InferEqualitySupport(List declarations) { if (done) { break; } - if (InferRequiredEqualitySupport(tp, p.Type)) { - tp.Characteristics.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired; - correspondingNonnullIterTypeParameter.Characteristics.EqualitySupport = - TypeParameter.EqualitySupportValue.InferredRequired; + if (InferAndSetEqualitySupport(tp, p.Type, reporter)) { + correspondingNonnullIterTypeParameter.Characteristics.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired; break; } } @@ -104,16 +107,17 @@ private static void InferEqualitySupport(List declarations) { } else if (d is ClassLikeDecl or DefaultClassDecl) { var cl = (TopLevelDeclWithMembers)d; foreach (var member in cl.Members.Where(member => !member.IsGhost)) { + List memberTypeArguments = null; if (member is Function function) { + memberTypeArguments = function.TypeArgs; foreach (var tp in function.TypeArgs) { if (tp.Characteristics.EqualitySupport == TypeParameter.EqualitySupportValue.Unspecified) { // here's our chance to infer the need for equality support - if (InferRequiredEqualitySupport(tp, function.ResultType)) { - tp.Characteristics.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired; + if (InferAndSetEqualitySupport(tp, function.ResultType, reporter)) { + // the call to InferAndSetEqualitySupport made the necessary updates } else { foreach (var p in function.Ins) { - if (InferRequiredEqualitySupport(tp, p.Type)) { - tp.Characteristics.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired; + if (InferAndSetEqualitySupport(tp, p.Type, reporter)) { break; } } @@ -121,13 +125,13 @@ private static void InferEqualitySupport(List declarations) { } } } else if (member is Method method) { + memberTypeArguments = method.TypeArgs; bool done = false; foreach (var tp in method.TypeArgs) { if (tp.Characteristics.EqualitySupport == TypeParameter.EqualitySupportValue.Unspecified) { // here's our chance to infer the need for equality support foreach (var p in method.Ins) { - if (InferRequiredEqualitySupport(tp, p.Type)) { - tp.Characteristics.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired; + if (InferAndSetEqualitySupport(tp, p.Type, reporter)) { done = true; break; } @@ -137,19 +141,38 @@ private static void InferEqualitySupport(List declarations) { if (done) { break; } - if (InferRequiredEqualitySupport(tp, p.Type)) { - tp.Characteristics.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired; + if (InferAndSetEqualitySupport(tp, p.Type, reporter)) { break; } } } } } + + // Now that type characteristics have been inferred for any method/function type parameters, generate a tool tip + // if the type parameters were added as part of type-parameter completion. + if (memberTypeArguments != null && memberTypeArguments.Count != 0 && memberTypeArguments[0].IsAutoCompleted) { + var toolTip = $"<{memberTypeArguments.Comma(Printer.TypeParameterToString)}>"; + reporter.Info(MessageSource.Resolver, member.tok, toolTip); + } + } } } } + private static bool InferAndSetEqualitySupport(TypeParameter tp, Type type, ErrorReporter reporter) { + var requiresEqualitySupport = InferRequiredEqualitySupport(tp, type); + if (requiresEqualitySupport) { + tp.Characteristics.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired; + // Note, auto-completed type parameters already get a tool tip for the enclosing method/function + if (reporter is not ErrorReporterWrapper && !tp.IsAutoCompleted) { + reporter.Info(MessageSource.Resolver, tp.tok, "(==)"); + } + } + return requiresEqualitySupport; + } + private static bool InferRequiredEqualitySupport(TypeParameter tp, Type type) { Contract.Requires(tp != null); Contract.Requires(type != null); @@ -231,6 +254,8 @@ private static void Check(List declarations, bool isAnExport, Erro syn.Rhs); } } + } else if (d is NewtypeDecl { BaseType: { } baseType }) { + visitor.VisitType(d.tok, baseType, false); } if (d is RedirectingTypeDecl rtd) { diff --git a/Source/DafnyCore/Rewriters/RefinementTransformer.cs b/Source/DafnyCore/Rewriters/RefinementTransformer.cs index 6239675d231..e3d14e3d44e 100644 --- a/Source/DafnyCore/Rewriters/RefinementTransformer.cs +++ b/Source/DafnyCore/Rewriters/RefinementTransformer.cs @@ -367,9 +367,7 @@ 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 { - // 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); + CheckAgreement_TypeParameters(nw.tok, d.TypeArgs, nw.TypeArgs, nw.Name, "type"); } } } else if (nw is AbstractTypeDecl) { @@ -830,7 +828,7 @@ TopLevelDeclWithMembers MergeClass(TopLevelDeclWithMembers nw, TopLevelDeclWithM return nw; } - void CheckAgreement_TypeParameters(IToken tok, List old, List nw, string name, string thing, bool checkNames = true) { + void CheckAgreement_TypeParameters(IToken tok, List old, List nw, string name, string thing) { Contract.Requires(tok != null); Contract.Requires(old != null); Contract.Requires(nw != null); @@ -842,7 +840,7 @@ void CheckAgreement_TypeParameters(IToken tok, List old, List old, List boundVars, List tySubst, Bpl.E ins.Add(etran.HeapExpr); } // Add type arguments - ins.AddRange(trTypeArgs(tySubst, tyArgs)); + ins.AddRange(TrTypeArgs(tySubst, tyArgs)); // Translate receiver argument, if any Expression receiver = bReceiver == null ? dafnyReceiver : new BoogieWrapper(bReceiver, dafnyReceiver.Type); diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Types.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Types.cs index 7ec946ea67e..8b8ea4c8011 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Types.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Types.cs @@ -862,6 +862,8 @@ Expression Zero(IToken tok, Type typ) { } else if (typ.IsTraitType) { Contract.Assert(options.Get(CommonOptionBag.GeneralTraits) != CommonOptionBag.GeneralTraitsOptions.Legacy); return null; + } else if (typ.IsTypeParameter) { + return null; } else { Contract.Assume(false); // unexpected type return null; @@ -921,9 +923,7 @@ void AddTypeDecl(NewtypeDecl dd) { FuelContext oldFuelContext = this.fuelContext; this.fuelContext = FuelSetting.NewFuelContext(dd); - if (dd.Var != null) { - AddWellformednessCheck(dd); - } + AddWellformednessCheck(dd); // Add $Is and $IsAlloc axioms for the newtype currentModule = dd.EnclosingModuleDefinition; @@ -1424,24 +1424,24 @@ void AddWellformednessCheck(RedirectingTypeDecl decl) { return; } - // If there's no constraint, there's nothing to do - if (decl.Var == null) { - Contract.Assert(decl.Constraint == null); // there's a constraint only if there's a variable to be constrained - Contract.Assert(decl.WitnessKind == SubsetTypeDecl.WKind.CompiledZero); // a witness makes sense only if there is a constraint - Contract.Assert(decl.Witness == null); // a witness makes sense only if there is a constraint - return; - } - Contract.Assert(decl.Constraint != null); // follows from the test above and the RedirectingTypeDecl class invariant - currentModule = decl.Module; codeContext = new CallableWrapper(decl, true); var etran = new ExpressionTranslator(this, predef, decl.tok, null); // parameters of the procedure var inParams = MkTyParamFormals(decl.TypeArgs, true); - Bpl.Type varType = TrType(decl.Var.Type); - Bpl.Expr wh = GetWhereClause(decl.Var.tok, new Bpl.IdentifierExpr(decl.Var.tok, decl.Var.AssignUniqueName(decl.IdGenerator), varType), decl.Var.Type, etran, NOALLOC); - inParams.Add(new Bpl.Formal(decl.Var.tok, new Bpl.TypedIdent(decl.Var.tok, decl.Var.AssignUniqueName(decl.IdGenerator), varType, wh), true)); + Type baseType; + Bpl.Expr wh; + if (decl.Var != null) { + baseType = decl.Var.Type; + Bpl.Type varType = TrType(baseType); + wh = GetWhereClause(decl.Var.tok, new Bpl.IdentifierExpr(decl.Var.tok, decl.Var.AssignUniqueName(decl.IdGenerator), varType), baseType, etran, NOALLOC); + // Do NOT use a where-clause in this declaration, because that would spoil the witness checking. + inParams.Add(new Bpl.Formal(decl.Var.tok, new Bpl.TypedIdent(decl.Var.tok, decl.Var.AssignUniqueName(decl.IdGenerator), varType), true)); + } else { + baseType = ((NewtypeDecl)decl).BaseType; + wh = null; + } // the procedure itself var req = new List(); @@ -1477,6 +1477,7 @@ void AddWellformednessCheck(RedirectingTypeDecl decl) { // define frame; // if (*) { // // The following is collected in constraintCheckBuilder: + // assume the where-clause for the bound variable // check constraint is well-formed; // assume constraint; // do reads checks; @@ -1488,15 +1489,24 @@ void AddWellformednessCheck(RedirectingTypeDecl decl) { // check well-formedness of the constraint (including termination, and delayed reads checks) var constraintCheckBuilder = new BoogieStmtListBuilder(this, options, context); var builderInitializationArea = new BoogieStmtListBuilder(this, options, context); - var delayer = new ReadsCheckDelayer(etran, null, locals, builderInitializationArea, constraintCheckBuilder); - delayer.DoWithDelayedReadsChecks(false, wfo => { - CheckWellformedAndAssume(decl.Constraint, wfo, locals, constraintCheckBuilder, etran, "predicate subtype constraint"); - }); + if (decl.Constraint == null) { + constraintCheckBuilder.Add(new Bpl.CommentCmd($"well-formedness of {decl.WhatKind} constraint is trivial")); + } else { + constraintCheckBuilder.Add(new Bpl.CommentCmd($"check well-formedness of {decl.WhatKind} constraint")); + if (wh != null) { + constraintCheckBuilder.Add(new Bpl.AssumeCmd(decl.tok, wh)); + } + var delayer = new ReadsCheckDelayer(etran, null, locals, builderInitializationArea, constraintCheckBuilder); + delayer.DoWithDelayedReadsChecks(false, wfo => { + CheckWellformedAndAssume(decl.Constraint, wfo, locals, constraintCheckBuilder, etran, "predicate subtype constraint"); + }); + } // Check that the type is inhabited. // Note, the possible witness in this check should be coordinated with the compiler, so the compiler knows how to do the initialization Expression witnessExpr = null; var witnessCheckBuilder = new BoogieStmtListBuilder(this, options, context); + witnessCheckBuilder.Add(new Bpl.CommentCmd($"check well-formedness of {decl.WhatKind} witness, and that it satisfies the constraint")); string witnessString = null; if (decl.Witness != null) { // check well-formedness of the witness expression (including termination, and reads checks) @@ -1505,28 +1515,24 @@ void AddWellformednessCheck(RedirectingTypeDecl decl) { CheckWellformed(decl.Witness, new WFOptions(null, true), locals, witnessCheckBuilder, etran); codeContext = ghostCodeContext; // check that the witness is assignable to the type of the given bound variable - if (decl is SubsetTypeDecl) { - // Note, for new-types, this has already been checked by CheckWellformed. - CheckResultToBeInType(decl.Witness.tok, decl.Witness, decl.Var.Type, locals, witnessCheckBuilder, etran); - } + CheckResultToBeInType(decl.Witness.tok, decl.Witness, baseType, locals, witnessCheckBuilder, etran); // check that the witness expression checks out - witnessExpr = Substitute(decl.Constraint, decl.Var, decl.Witness); + witnessExpr = decl.Constraint != null ? Substitute(decl.Constraint, decl.Var, decl.Witness) : null; } else if (decl.WitnessKind == SubsetTypeDecl.WKind.CompiledZero) { - var witness = Zero(decl.tok, decl.Var.Type); + var witness = Zero(decl.tok, baseType); if (witness == null) { witnessString = ""; witnessCheckBuilder.Add(Assert(decl.tok, Bpl.Expr.False, new PODesc.WitnessCheck(witnessString))); } else { - // before trying 0 as a witness, check that 0 can be assigned to decl.Var + // before trying 0 as a witness, check that 0 can be assigned to baseType witnessString = Printer.ExprToString(options, witness); - CheckResultToBeInType(decl.tok, witness, decl.Var.Type, locals, witnessCheckBuilder, etran, $"trying witness {witnessString}: "); - witnessExpr = Substitute(decl.Constraint, decl.Var, witness); + CheckResultToBeInType(decl.tok, witness, baseType, locals, witnessCheckBuilder, etran, $"trying witness {witnessString}: "); + witnessExpr = decl.Constraint != null ? Substitute(decl.Constraint, decl.Var, witness) : null; } } if (witnessExpr != null) { var witnessCheckTok = decl.Witness != null ? GetToken(decl.Witness) : decl.tok; witnessCheckBuilder.Add(new Bpl.AssumeCmd(witnessCheckTok, etran.CanCallAssumption(witnessExpr))); - var witnessCheck = etran.TrExpr(witnessExpr); bool splitHappened; var ss = TrSplitExpr(context, witnessExpr, etran, true, out splitHappened); diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.cs b/Source/DafnyCore/Verifier/BoogieGenerator.cs index 6a4da1fa878..36d7b25f04d 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.cs @@ -3173,26 +3173,30 @@ public BoilerplateTriple(IToken tok, bool isFree, Bpl.Expr expr, string errorMes return new Bpl.ForallExpr(tok, new List(), new List { oVar, fVar }, null, tr, BplImp(ante, consequent)); } // ----- Type --------------------------------------------------------------------------------- - // Translates a type into the representation Boogie type, - // c.f. TypeToTy which translates a type to its Boogie expression - // to be used in $Is and $IsAlloc. - Bpl.Type TrType(Type type) { - Contract.Requires(type != null); - Contract.Requires(predef != null); - Contract.Ensures(Contract.Result() != null); + static Type NormalizeToVerificationTypeRepresentation(Type type) { while (true) { type = type.NormalizeExpand(); if (type is TypeProxy) { - Contract.Assume(false); // we assume that all proxies should have been dealt with in the resolver + Contract.Assume(false); // we assume that all proxies have been dealt with in the resolver } - var d = type.AsNewtype; - if (d == null) { + if (type.AsNewtype is not { } newtypeDecl) { break; - } else { - type = d.BaseType; // the Boogie type to be used for the newtype is the same as for the base type } + type = newtypeDecl.RhsWithArgument(type.TypeArgs); // the Boogie type to be used for the newtype is the same as for the base type } + return type; + } + + // Translates a type into the representation Boogie type, + // c.f. TypeToTy which translates a type to its Boogie expression + // to be used in $Is and $IsAlloc. + Bpl.Type TrType(Type type) { + Contract.Requires(type != null); + Contract.Requires(predef != null); + Contract.Ensures(Contract.Result() != null); + + type = NormalizeToVerificationTypeRepresentation(type); if (type is BoolType) { return Bpl.Type.Bool; @@ -3356,7 +3360,7 @@ public Boogie.Expr BoxifyForTraitParent(Bpl.IToken tok, Boogie.Expr obj, TopLeve public static bool ModeledAsBoxType(Type t) { Contract.Requires(t != null); - t = t.NormalizeExpand(); + t = NormalizeToVerificationTypeRepresentation(t); if (t is TypeProxy) { // unresolved proxy return false; @@ -3572,7 +3576,7 @@ private void ReportAssertion(IToken tok, PODesc.ProofObligationDescription descr delegate void BodyTranslator(BoogieStmtListBuilder builder, ExpressionTranslator etr); - List trTypeArgs(Dictionary tySubst, List tyArgs) { + List TrTypeArgs(Dictionary tySubst, List tyArgs) { var res = new List(); foreach (var p in tyArgs) { res.Add(TypeToTy(tySubst[p])); @@ -3864,6 +3868,7 @@ Bpl.Expr GetWhereClause(IToken tok, Bpl.Expr x, Type type, ExpressionTranslator } var normType = type.NormalizeExpandKeepConstraints(); + var verificationType = NormalizeToVerificationTypeRepresentation(type); Bpl.Expr isAlloc; if (type.IsNumericBased() || type.IsBitVectorType || type.IsBoolType || type.IsCharType || type.IsBigOrdinalType) { isAlloc = null; @@ -3889,7 +3894,7 @@ Bpl.Expr GetWhereClause(IToken tok, Bpl.Expr x, Type type, ExpressionTranslator return Bpl.Expr.Eq(BplBvLiteralExpr(tok, BaseTypes.BigNum.ZERO, t), x); } } else if ((normType.AsTypeSynonym != null || normType.AsNewtype != null) && - (normType.IsNumericBased() || normType.IsBitVectorType || normType.IsBoolType)) { + (verificationType.IsNumericBased() || verificationType.IsBitVectorType || verificationType.IsBoolType)) { var constraint = ModuleResolver.GetImpliedTypeConstraint(new BoogieWrapper(x, normType), normType); isPred = etran.TrExpr(constraint); } else { diff --git a/Source/DafnyPipeline.Test/expectedProverLog.smt2 b/Source/DafnyPipeline.Test/expectedProverLog.smt2 index cff4b0e4b68..583449687ca 100644 --- a/Source/DafnyPipeline.Test/expectedProverLog.smt2 +++ b/Source/DafnyPipeline.Test/expectedProverLog.smt2 @@ -1873,7 +1873,6 @@ $generated@@295))))))))) (declare-fun $generated@@426 () T@U) (declare-fun $generated@@427 () T@U) (declare-fun $generated@@428 (T@U) Bool) -(declare-fun $generated@@429 () T@U) (set-option :timeout 0) (set-option :rlimit 0) (set-option :auto_config false) @@ -1889,19 +1888,19 @@ $generated@@295))))))))) (set-option :pp.bv_literals false) (set-option :smt.arith.solver 2) (assert (not - (=> (= (ControlFlow 0 0) 14) (let (($generated@@430 true)) -(let (($generated@@431 (=> (and (= ($generated@@32 $generated@@33 $generated@@78) $generated@@78) (= (ControlFlow 0 8) (- 0 7))) false))) -(let (($generated@@432 (=> ($generated@@19 ($generated@@32 $generated@@15 ($generated@@18 false))) (and (=> (= (ControlFlow 0 10) 8) $generated@@431) (=> (= (ControlFlow 0 10) 9) $generated@@430))))) -(let (($generated@@433 true)) -(let (($generated@@434 (=> (and (not ($generated@@19 ($generated@@32 $generated@@15 ($generated@@18 false)))) (= (ControlFlow 0 6) 4)) $generated@@433))) -(let (($generated@@435 (=> (and (and ($generated@@44 $generated@@419 $generated@@420) ($generated@@148 $generated@@419 $generated@@420 $generated@@421)) (= $generated@@422 ($generated@@324 $generated@@90 $generated@@421 $generated@@1 false))) (and (=> (= (ControlFlow 0 11) 10) $generated@@432) (=> (= (ControlFlow 0 11) 6) $generated@@434))))) -(let (($generated@@436 (=> (and (not (and ($generated@@44 $generated@@419 $generated@@420) ($generated@@148 $generated@@419 $generated@@420 $generated@@421))) (= (ControlFlow 0 5) 4)) $generated@@433))) -(let (($generated@@437 (=> (and ($generated@@34 $generated@@421) (or (= $generated@@423 $generated@@421) ($generated@@100 $generated@@423 $generated@@421))) (and (=> (= (ControlFlow 0 12) 11) $generated@@435) (=> (= (ControlFlow 0 12) 5) $generated@@436))))) -(let (($generated@@438 (=> (and (and ($generated@@35 $generated@@420 $generated@@424 ($generated@@32 $generated@@33 ($generated@@123 ($generated@@32 ($generated@@46 $generated@@42 $generated@@15) $generated@@322) ($generated@@32 $generated@@47 ($generated@@138 $generated@@47 ($generated@@215 ($generated@@170 ($generated@@410 $generated@@425) ($generated@@414 $generated@@420 ($generated@@19 ($generated@@32 $generated@@15 ($generated@@18 false)))) ($generated@@406 ($generated@@135 ($generated@@212 false))))) ($generated@@308 $generated@@426)))))) (= (ControlFlow 0 3) (- 0 2))) ($generated@@35 $generated@@420 $generated@@424 ($generated@@32 $generated@@33 ($generated@@123 ($generated@@32 ($generated@@46 $generated@@42 $generated@@15) $generated@@322) ($generated@@32 $generated@@47 ($generated@@138 $generated@@47 ($generated@@215 ($generated@@170 ($generated@@410 $generated@@425) ($generated@@414 $generated@@420 ($generated@@19 ($generated@@32 $generated@@15 ($generated@@18 false)))) ($generated@@406 ($generated@@135 ($generated@@212 false))))) ($generated@@308 $generated@@426))))))) ($generated@@19 ($generated@@32 $generated@@15 ($generated@@18 ($generated@@31 $generated@@420 $generated@@424 ($generated@@32 $generated@@33 ($generated@@123 ($generated@@32 ($generated@@46 $generated@@42 $generated@@15) $generated@@322) ($generated@@32 $generated@@47 ($generated@@138 $generated@@47 ($generated@@215 ($generated@@170 ($generated@@410 $generated@@425) ($generated@@414 $generated@@420 ($generated@@19 ($generated@@32 $generated@@15 ($generated@@18 false)))) ($generated@@406 ($generated@@135 ($generated@@212 false))))) ($generated@@308 $generated@@426)))))))))))) -(let (($generated@@439 true)) -(let (($generated@@440 (=> (= $generated@@427 ($generated@@324 $generated@@90 $generated@@423 $generated@@1 false)) (and (and (=> (= (ControlFlow 0 13) 1) $generated@@439) (=> (= (ControlFlow 0 13) 12) $generated@@437)) (=> (= (ControlFlow 0 13) 3) $generated@@438))))) -(let (($generated@@441 (=> (and (and (and ($generated@@34 $generated@@423) ($generated@@428 $generated@@423)) ($generated@@36 $generated@@33 $generated@@429 ($generated@@37 $generated@@420 $generated@@424))) (and (= 1 $generated@@30) (= (ControlFlow 0 14) 13))) $generated@@440))) -$generated@@441))))))))))))) + (=> (= (ControlFlow 0 0) 14) (let (($generated@@429 true)) +(let (($generated@@430 (=> (and (= ($generated@@32 $generated@@33 $generated@@78) $generated@@78) (= (ControlFlow 0 8) (- 0 7))) false))) +(let (($generated@@431 (=> ($generated@@19 ($generated@@32 $generated@@15 ($generated@@18 false))) (and (=> (= (ControlFlow 0 10) 8) $generated@@430) (=> (= (ControlFlow 0 10) 9) $generated@@429))))) +(let (($generated@@432 true)) +(let (($generated@@433 (=> (and (not ($generated@@19 ($generated@@32 $generated@@15 ($generated@@18 false)))) (= (ControlFlow 0 6) 4)) $generated@@432))) +(let (($generated@@434 (=> (and (and ($generated@@44 $generated@@419 $generated@@420) ($generated@@148 $generated@@419 $generated@@420 $generated@@421)) (= $generated@@422 ($generated@@324 $generated@@90 $generated@@421 $generated@@1 false))) (and (=> (= (ControlFlow 0 11) 10) $generated@@431) (=> (= (ControlFlow 0 11) 6) $generated@@433))))) +(let (($generated@@435 (=> (and (not (and ($generated@@44 $generated@@419 $generated@@420) ($generated@@148 $generated@@419 $generated@@420 $generated@@421))) (= (ControlFlow 0 5) 4)) $generated@@432))) +(let (($generated@@436 (=> (and ($generated@@34 $generated@@421) (or (= $generated@@423 $generated@@421) ($generated@@100 $generated@@423 $generated@@421))) (and (=> (= (ControlFlow 0 12) 11) $generated@@434) (=> (= (ControlFlow 0 12) 5) $generated@@435))))) +(let (($generated@@437 (=> (and (and ($generated@@35 $generated@@420 $generated@@424 ($generated@@32 $generated@@33 ($generated@@123 ($generated@@32 ($generated@@46 $generated@@42 $generated@@15) $generated@@322) ($generated@@32 $generated@@47 ($generated@@138 $generated@@47 ($generated@@215 ($generated@@170 ($generated@@410 $generated@@425) ($generated@@414 $generated@@420 ($generated@@19 ($generated@@32 $generated@@15 ($generated@@18 false)))) ($generated@@406 ($generated@@135 ($generated@@212 false))))) ($generated@@308 $generated@@426)))))) (= (ControlFlow 0 3) (- 0 2))) ($generated@@35 $generated@@420 $generated@@424 ($generated@@32 $generated@@33 ($generated@@123 ($generated@@32 ($generated@@46 $generated@@42 $generated@@15) $generated@@322) ($generated@@32 $generated@@47 ($generated@@138 $generated@@47 ($generated@@215 ($generated@@170 ($generated@@410 $generated@@425) ($generated@@414 $generated@@420 ($generated@@19 ($generated@@32 $generated@@15 ($generated@@18 false)))) ($generated@@406 ($generated@@135 ($generated@@212 false))))) ($generated@@308 $generated@@426))))))) ($generated@@19 ($generated@@32 $generated@@15 ($generated@@18 ($generated@@31 $generated@@420 $generated@@424 ($generated@@32 $generated@@33 ($generated@@123 ($generated@@32 ($generated@@46 $generated@@42 $generated@@15) $generated@@322) ($generated@@32 $generated@@47 ($generated@@138 $generated@@47 ($generated@@215 ($generated@@170 ($generated@@410 $generated@@425) ($generated@@414 $generated@@420 ($generated@@19 ($generated@@32 $generated@@15 ($generated@@18 false)))) ($generated@@406 ($generated@@135 ($generated@@212 false))))) ($generated@@308 $generated@@426)))))))))))) +(let (($generated@@438 true)) +(let (($generated@@439 (=> (= $generated@@427 ($generated@@324 $generated@@90 $generated@@423 $generated@@1 false)) (and (and (=> (= (ControlFlow 0 13) 1) $generated@@438) (=> (= (ControlFlow 0 13) 12) $generated@@436)) (=> (= (ControlFlow 0 13) 3) $generated@@437))))) +(let (($generated@@440 (=> (and (and ($generated@@34 $generated@@423) ($generated@@428 $generated@@423)) (and (= 1 $generated@@30) (= (ControlFlow 0 14) 13))) $generated@@439))) +$generated@@440))))))))))))) )) (check-sat) (get-info :rlimit) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/GeneralNewtypes.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/GeneralNewtypes.dfy index 0f1d5f4004f..ca101365541 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/GeneralNewtypes.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/GeneralNewtypes.dfy @@ -11,6 +11,10 @@ method Main() { SubsetTypeIsTests.Test(); NewtypeIsTests.Test(); NewBehaviors.Test(); + TypeParameters.Test(); + AutoInit.Test(); + RefinementB.Test(2.0, 3.0); + SimpleNewtypeWitness.Test(); } module Numerics { @@ -580,3 +584,78 @@ module NewBehaviors { print mIs, " ", mAs, " ", w0, " ", w1, "\n"; // true false true false } } + +module TypeParameters { + newtype Wrapper = g: G | true witness * + newtype int32 = x: int | -0x8000_0000 <= x < 0x8000_0000 + + method Test() { + var b: Wrapper; + b := true ==> false; + var i: Wrapper>; + i := Wrap3(25) as Wrapper>; + var j: Wrapper>>; + j := Wrap3(30); + print b, " ", i, " ", j, "\n"; // false 25 30 + + print Unwrap3(j) < 2, " "; // false + print Unwrap3(j) < 32, " | "; // true | + var w: int32 := 299; + b := Unwrap3(j) < w; + print b, "\n"; // true + } + + function Wrap3(x: int32): Wrapper>> { + x as Wrapper as Wrapper> as Wrapper>> + } + + function Unwrap3(x: Wrapper>>): int32 { + x as Wrapper> as Wrapper as int32 + } +} + +module AutoInit { + newtype A = x: int | 5 <= x witness 5 + newtype B = z: real | true + newtype Int32 = x | -0x8000_0000 <= x < 0x8000_0000 witness 7 + + newtype pos = x: int | 0 < x witness 19 + + method TestOne() { + var x: X := *; + print x, "\n"; + } + + method Test() { + TestOne>(); // 5 + TestOne>(); // 0.0 + TestOne>(); // 7 + } +} + +abstract module RefinementA { + type AbstractType + newtype NAT = AbstractType witness * + newtype NATx = x: AbstractType | true witness * + + method Test(n: NAT, nx: NATx) { + print n, " ", nx, "\n"; + } +} + +module RefinementB refines RefinementA { + type AbstractType = real +} + +module SimpleNewtypeWitness { + newtype A = x: int | 100 <= x witness 102 + newtype B = a: A | true witness 103 + newtype C = A witness 104 + + method Test() { + var a: A := *; + var b: B := *; + var c: C := *; + print a, " ", b, " ", c, "\n"; // 102 103 104 + } +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/GeneralNewtypes.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/GeneralNewtypes.dfy.expect index 5ef914b2c22..50bff3e3a2e 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/GeneralNewtypes.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/GeneralNewtypes.dfy.expect @@ -59,3 +59,10 @@ done true true false false true false false false false done true false true false +false 25 30 +false true | true +5 +0.0 +7 +2.0 3.0 +102 103 104 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AsIs-UnusedTypeParameters.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AsIs-UnusedTypeParameters.dfy new file mode 100644 index 00000000000..96479ca5f70 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AsIs-UnusedTypeParameters.dfy @@ -0,0 +1,70 @@ +// RUN: %testDafnyForEachResolver --expect-exit-code=2 --refresh-exit-code=4 "%s" + +module UnusedTypeParametersOfSubtypeTypes { + trait T { } + class D extends T<(int, seq)> { } + type F = d: D | true witness * // the legacy resolver treats F as a reference type, and bogusly wants all parameters to be equal in order to have type compatibility + + method Test(f: F, g: F) { + if * { + var h: F; + h := f; + h := g; + } else { + var h: F; + h := g; + h := f; + } + + var s0: seq> := [f, f, f]; + var s1: seq> := [g, g, g]; + if * { + s0 := s1; + } else { + s1 := s0; + } + } + + method Test1(f: F, g: F) { + var c0: C> := new C>(g); + var c1: C> := new C>(f); + + // The resolver should treat the following three consistently. That is, it should either disallow all three + // or allow all three. (It allows all three.) The verifier should also treat the three consistently (which, + // for the way unused type parameters in subset types are currently treated, is to say that all three branches + // causes a verification error). + if + case true => + var b: bool := c1 is C>; + assert b; // error: this may not hold + case true => + c0 := c1; // error: RHS value not assignable to LHS + case true => + c0 := c1 as C>; // error: precondition of "as" may not be satisfied + } + + method Test2(f: F, g: F) { + var c0: C> := new C>(g); + var c1: C> := new C>(f); + + // The resolver should treat the following three consistently. That is, it should either disallow all three + // or allow all three. (It allows all three.) The verifier should also treat the three consistently (which, + // for the way unused type parameters in subset types are currently treated, is to say that all three branches + // causes a verification error). + if + case true => + var b: bool := c0 is C>; + assert b; // error: this may not hold + case true => + c1 := c0; // error: RHS value not assignable to LHS + case true => + c1 := c0 as C>; // error: precondition of "as" may not be satisfied + } + + class C { + var y: Y + constructor (y: Y) { + this.y := y; + } + } +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AsIs-UnusedTypeParameters.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AsIs-UnusedTypeParameters.dfy.expect new file mode 100644 index 00000000000..92bf8181aef --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AsIs-UnusedTypeParameters.dfy.expect @@ -0,0 +1,5 @@ +AsIs-UnusedTypeParameters.dfy(38,24): Error: a type test to 'C>' must be from a compatible type (got 'C>') +AsIs-UnusedTypeParameters.dfy(43,15): Error: a type cast to a reference type (C>) must be from a compatible type (got C>); this cast could never succeed +AsIs-UnusedTypeParameters.dfy(56,24): Error: a type test to 'C>' must be from a compatible type (got 'C>') +AsIs-UnusedTypeParameters.dfy(61,15): Error: a type cast to a reference type (C>) must be from a compatible type (got C>); this cast could never succeed +4 resolution/type errors detected in AsIs-UnusedTypeParameters.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AsIs-UnusedTypeParameters.dfy.refresh.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AsIs-UnusedTypeParameters.dfy.refresh.expect new file mode 100644 index 00000000000..9ab8dec464b --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AsIs-UnusedTypeParameters.dfy.refresh.expect @@ -0,0 +1,8 @@ +AsIs-UnusedTypeParameters.dfy(39,13): Error: assertion might not hold +AsIs-UnusedTypeParameters.dfy(41,12): Error: value of expression (of type 'C>') is not known to be an instance of type 'C>' +AsIs-UnusedTypeParameters.dfy(43,15): Error: value of expression (of type 'C>') is not known to be an instance of type 'C>' +AsIs-UnusedTypeParameters.dfy(57,13): Error: assertion might not hold +AsIs-UnusedTypeParameters.dfy(59,12): Error: value of expression (of type 'C>') is not known to be an instance of type 'C>' +AsIs-UnusedTypeParameters.dfy(61,15): Error: value of expression (of type 'C>') is not known to be an instance of type 'C>' + +Dafny program verifier finished with 2 verified, 6 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BoundedPolymorphismResolution.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BoundedPolymorphismResolution.dfy index 22dda39f0eb..64314162006 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BoundedPolymorphismResolution.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BoundedPolymorphismResolution.dfy @@ -195,13 +195,13 @@ module Refinement { } module BB refines AA { - type SoonSubsetType0 = int // here, the name is allowed to be changed + type SoonSubsetType0 = int // error: name change not allowed 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 AbstractType0 // error: name change not allowed + type AbstractType1 // error: type bounds don't match the ones in AA.AbstractType1 + type AbstractType2 // error: type bounds don't match the ones in AAAbstractType2 type AbstractType3 // error: wrong number of type bounds type AbstractType4 @@ -323,3 +323,95 @@ module VariousBounds { } } } + +module MoreRefinement { + module AA { + trait Trait { } + trait G { } + trait H { } + + type AbstractType0, B> + type AbstractType1> + type AbstractType2, B extends G> + type AbstractType3, B extends G> + + function F0>(): int + function F1>(): int + function F2(): A + function F3(a: A): int + function F4(a: A): A + + method M0>() + method M1>() + method M2() returns (a: A) + method M3(a: A) + method M4(a: A) returns (r: A) + } + + module BB refines AA { + type AbstractType0, B> // error: the type bounds are not the same + type AbstractType1> // error: the type bounds are not the same + type AbstractType2, B extends G> + type AbstractType3, B extends H> // error: the type bounds are not the same + + function F0>(): int // error: the type bounds are not the same + function F1>(): int + function F2(): B // error: mismatched result type + function F3(b: B): int // error: mismatched in-parameter type + function F4(a: A): A + + method M0>() // error: the type bounds are not the same + method M1>() + method M2() returns (b: B) // error: mismatched out-parameter type + method M3(b: B) // error: mismatched in-parameter type + method M4(a: A) returns (r: A) + } +} + +module RefinementRegressions { + module AA { + datatype D = D(x: X) + } + + module BB refines AA { + type X = int + datatype D ... // error: not allowed to rename type parameter + } + + abstract module XX { + type D + class C { + var x: X + constructor Orig(x: X) { + this.x := x; + } + method Print() { + print x, "\n"; + } + } + + method G() returns (r: C) { + r := new C.Orig('h'); // error (reported as part of YY): 'h' used when an 'int' is expected (strange error, caused by the renaming error in YY) + } + } + + module YY refines XX { + type D = X // error: not allowed to rename type parameter + type X = int + class C ... { // error: not allowed to rename type parameter + var y: Y + constructor Alt(y: Y) { + this.x := 15; + this.y := y; + } + } + + method Test() { + var c := new C.Alt(3.2); + var d := new C.Orig(3); + c.Print(); + d.Print(); + } + } + +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BoundedPolymorphismResolution.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BoundedPolymorphismResolution.dfy.expect index d749cd107a8..97fb6721306 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BoundedPolymorphismResolution.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BoundedPolymorphismResolution.dfy.expect @@ -50,35 +50,48 @@ BoundedPolymorphismResolution.dfy(156,11): Error: type bound must be a trait or 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(220,14): 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(198,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(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(203,23): Error: type parameter 'A' of abstract type 'AbstractType1' is declared with a different number of type bounds than in the corresponding abstract type in the module it refines (expected 1, found 0) +BoundedPolymorphismResolution.dfy(204,23): Error: type parameter 'A' of abstract type 'AbstractType2' is declared with a different number of type bounds than in the corresponding abstract type in the module it refines (expected 0, found 1) +BoundedPolymorphismResolution.dfy(206,23): 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,23): 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,23): 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,23): 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,27): 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,23): 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,24): 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(268,15): 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,13): 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(294,40): 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(301,13): 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,21): 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,50): 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 +BoundedPolymorphismResolution.dfy(357,19): Error: type bound for type parameter 'B' of function 'F0' is different from the corresponding type bound of the corresponding type parameter of the corresponding function in the module it refines (expected 'G', found 'G') +BoundedPolymorphismResolution.dfy(359,13): Error: the result type of function 'F2' (B) differs from the result type of the corresponding function in the module it refines (A) +BoundedPolymorphismResolution.dfy(360,22): Error: there is a difference in name of parameter 0 ('b' versus 'a') of function F3 compared to corresponding function in the module it refines +BoundedPolymorphismResolution.dfy(363,17): Error: type bound for type parameter 'B' 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 'G', found 'G') +BoundedPolymorphismResolution.dfy(365,31): Error: there is a difference in name of out-parameter 0 ('b' versus 'a') of method M2 compared to corresponding method in the module it refines +BoundedPolymorphismResolution.dfy(366,20): Error: there is a difference in name of in-parameter 0 ('b' versus 'a') of method M3 compared to corresponding method in the module it refines +BoundedPolymorphismResolution.dfy(352,23): Error: type bound for type parameter 'A' of abstract type 'AbstractType0' is different from the corresponding type bound of the corresponding type parameter of the corresponding abstract type in the module it refines (expected 'G', found 'G') +BoundedPolymorphismResolution.dfy(353,26): Error: type bound for type parameter 'B' of abstract type 'AbstractType1' is different from the corresponding type bound of the corresponding type parameter of the corresponding abstract type in the module it refines (expected 'G', found 'G') +BoundedPolymorphismResolution.dfy(355,39): Error: type bound for type parameter 'B' of abstract type 'AbstractType3' is different from the corresponding type bound of the corresponding type parameter of the corresponding abstract type in the module it refines (expected 'G', found 'H') +BoundedPolymorphismResolution.dfy(378,15): Error: type parameters are not allowed to be renamed from the names given in the datatype in the module being refined (expected 'X', found 'Y') +BoundedPolymorphismResolution.dfy(399,11): Error: type parameters are not allowed to be renamed from the names given in the type in the module being refined (expected 'X', found 'Z') +BoundedPolymorphismResolution.dfy(401,12): Error: type parameters are not allowed to be renamed from the names given in the class in the module being refined (expected 'X', found 'Y') +BoundedPolymorphismResolution.dfy[YY](394,23): Error: incorrect argument type for constructor in-parameter 'x' (expected X, found char) +96 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 index c8a7771295b..ca8fdd5e2ca 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BoundedPolymorphismResolution.dfy.refresh.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BoundedPolymorphismResolution.dfy.refresh.expect @@ -27,30 +27,43 @@ BoundedPolymorphismResolution.dfy(156,11): Error: type bound must be a trait or 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(220,14): 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(198,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(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(203,23): Error: type parameter 'A' of abstract type 'AbstractType1' is declared with a different number of type bounds than in the corresponding abstract type in the module it refines (expected 1, found 0) +BoundedPolymorphismResolution.dfy(204,23): Error: type parameter 'A' of abstract type 'AbstractType2' is declared with a different number of type bounds than in the corresponding abstract type in the module it refines (expected 0, found 1) +BoundedPolymorphismResolution.dfy(206,23): 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,23): 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,23): 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,23): 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,27): 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,23): 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,24): 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(268,15): 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,13): 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(294,40): 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 +BoundedPolymorphismResolution.dfy(301,13): 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,21): 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,50): 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(357,19): Error: type bound for type parameter 'B' of function 'F0' is different from the corresponding type bound of the corresponding type parameter of the corresponding function in the module it refines (expected 'G', found 'G') +BoundedPolymorphismResolution.dfy(359,13): Error: the result type of function 'F2' (B) differs from the result type of the corresponding function in the module it refines (A) +BoundedPolymorphismResolution.dfy(360,22): Error: there is a difference in name of parameter 0 ('b' versus 'a') of function F3 compared to corresponding function in the module it refines +BoundedPolymorphismResolution.dfy(363,17): Error: type bound for type parameter 'B' 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 'G', found 'G') +BoundedPolymorphismResolution.dfy(365,31): Error: there is a difference in name of out-parameter 0 ('b' versus 'a') of method M2 compared to corresponding method in the module it refines +BoundedPolymorphismResolution.dfy(366,20): Error: there is a difference in name of in-parameter 0 ('b' versus 'a') of method M3 compared to corresponding method in the module it refines +BoundedPolymorphismResolution.dfy(352,23): Error: type bound for type parameter 'A' of abstract type 'AbstractType0' is different from the corresponding type bound of the corresponding type parameter of the corresponding abstract type in the module it refines (expected 'G', found 'G') +BoundedPolymorphismResolution.dfy(353,26): Error: type bound for type parameter 'B' of abstract type 'AbstractType1' is different from the corresponding type bound of the corresponding type parameter of the corresponding abstract type in the module it refines (expected 'G', found 'G') +BoundedPolymorphismResolution.dfy(355,39): Error: type bound for type parameter 'B' of abstract type 'AbstractType3' is different from the corresponding type bound of the corresponding type parameter of the corresponding abstract type in the module it refines (expected 'G', found 'H') +BoundedPolymorphismResolution.dfy(378,15): Error: type parameters are not allowed to be renamed from the names given in the datatype in the module being refined (expected 'X', found 'Y') +BoundedPolymorphismResolution.dfy(399,11): Error: type parameters are not allowed to be renamed from the names given in the type in the module being refined (expected 'X', found 'Z') +BoundedPolymorphismResolution.dfy(401,12): Error: type parameters are not allowed to be renamed from the names given in the class in the module being refined (expected 'X', found 'Y') +BoundedPolymorphismResolution.dfy[YY](394,28): Error: character literal used as if it had type int +68 resolution/type errors detected in BoundedPolymorphismResolution.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GeneralNewtypeCollectionsGeneric.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GeneralNewtypeCollectionsGeneric.dfy new file mode 100644 index 00000000000..2eb418a17df --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GeneralNewtypeCollectionsGeneric.dfy @@ -0,0 +1,513 @@ +// RUN: %testDafnyForEachCompiler "%s" -- --type-system-refresh --general-newtypes --general-traits=datatype --reads-clauses-on-methods + +method Main() { + Set.Test(); + Set.TestSpecialCase(); + Iset.Test(); + Frames.CallEm(); + Decreases.Test(); + Multiset.Test(); + Seq.Test(); + SeqToMultisetConversion.Test(); + Map.Test(); + Imap.Test(); +} + +module Set { + newtype IntSet = s: set | true + + method Test() { + var s: IntSet; + s := {}; + print s, " "; // {} + s := {6, 19}; + print |s|, " "; // 2 + s := set x: int | 6 <= x < 10 && 2 * x < 300; + print |s|, " ", 7 in s, " "; // 4 true + s := set x: int | 6 <= x < 10 :: 2 * x; + print |s|, " ", 7 in s, "\n"; // 4 false + + var bb := [5 in s, 12 in s, 19 !in s]; + + var t: IntSet := s; + + s := s + t; + s := s - t; + s := s * t; + var disjoint := s !! t; + + print bb, " ", s, " ", disjoint, "\n"; // [false, true, true] {} true + + var u: set; + u := s as set; + s := u as IntSet; + var b0 := s is set; + var b1 := u is IntSet; + + print |s|, " ", |u|, " ", b0, " ", b1, "\n"; // 0 0 true true + + b0 := s <= t; + b1 := s < t; + var b2 := s > s; + var b3 := s >= s; + print b0, " ", b1, " ", b2, " ", b3, "\n"; // true true false true + + b0 := s == t; + b1 := s != t; + print b0, " ", b1, "\n"; // false true + } + + method TestSpecialCase() { + var dt := Dt; + print |dt.FFF(15)|, "\n"; // 15 + } + + // auto-accumulator tail recursive function in trait (this has a special case in the compiler code) + trait Trait { + function FFF(n: nat): IntSet { + if n == 0 then {} else {n} + FFF(n - 1) + } + } + + datatype Dt extends Trait = Dt +} + +module Iset { + newtype IntIset = s: iset | true + + method Test() { + var s: IntIset; + s := iset{}; + print "iset: ", s, " "; // {} + s := iset{6, 19}; + print s - iset{6}, " "; // {19} + s := iset x: int | 6 <= x < 10 && 2 * x < 300; + s := iset x: int | 6 <= x < 10 :: 2 * x; + + var t: IntIset := s; + + s := s + t; + s := s - t; + s := s * t; + var disjoint := s !! t; + + print s, " ", disjoint, "\n"; // {} true + + var u: iset; + u := s as iset; + s := u as IntIset; + var b0 := s is iset; + var b1 := u is IntIset; + + print s, " ", u, " ", b0, " ", b1, "\n"; // {} {} true true + + b0 := s <= t; + b1 := s < t; + var b2 := s > s; + var b3 := s >= s; + print b0, " ", b1, " ", b2, " ", b3, "\n"; // true true false true + + b0 := s == t; + b1 := s != t; + print b0, " ", b1, "\n"; // false true + } +} + +module Frames { + method CallEm() { + var o := new object; + label Recently: + M({o}, iset{o}, multiset{o, o}, [o, o, o]); + var u := F({o}, iset{o}, multiset{o, o}, [o, o, o]); + ghost var b := P2@Recently({o}, iset{o}, multiset{o, o}, [o, o, o]); + } + + newtype ObjectSet = s: set | true + newtype ObjectISet = ss: iset | true + newtype ObjectMultiset = m: multiset | true + newtype ObjectSeq = q: seq | true + + function R(x: int): ObjectSet { + {} + } + + method M(s: ObjectSet, ss: ObjectISet, m: ObjectMultiset, q: ObjectSeq) + modifies s + modifies ss + modifies m + modifies q + reads s + reads ss + reads m + reads q + { + assert unchanged(s); + assert unchanged(ss); + assert unchanged(m); + assert unchanged(q); + modify s; + modify ss; + modify m; + modify q; + for i := 0 to 100 + modifies s + modifies ss + modifies m + modifies q + { + } + ghost var g: bool; + g := fresh(s); + g := fresh(ss); + g := fresh(q); + } + + function F(s: ObjectSet, ss: ObjectISet, m: ObjectMultiset, q: ObjectSeq): int + reads s + reads ss + reads m + reads q + reads R + { + 6 + } + + twostate predicate P2(s: ObjectSet, ss: ObjectISet, m: ObjectMultiset, q: ObjectSeq) + reads s + reads ss + reads m + reads q + reads R + { + true + } +} + +module Decreases { + newtype MyInt = int + newtype BoundedInt = x: int | 0 <= x < 10_000 + newtype BoolSet = s: set | true + + method Test() { + A(100); + K({true, true}); + } + + method A(x: int) + requires x < 10_000 + decreases x + { + if 0 < x { + B((x - 1) as MyInt); + } else if x == 0 { + print "Ends in A\n"; + } + } + + method B(y: MyInt) + requires y < 10_000 + decreases y + { + if 0 < y { + C((y - 1) as BoundedInt); + } else if y == 0 { + print "Ends in B\n"; + } + } + + method C(z: BoundedInt) + decreases z + { + if 0 < z { + A((z - 1) as int); + } else if z == 0 { + print "Ends in C\n"; + } + } + + method K(s: set) + decreases s + { + if s == {} { + print "K is done\n"; + } else { + L(s as BoolSet); + } + } + + method L(t: BoolSet) + requires t != {} + decreases t, 0 as MyInt + { + var b :| b in t; + var t' := t - {b}; + K(t' as set); + } +} + +module Multiset { + newtype IntMultiset = s: multiset | true + + method Test() { + var s: IntMultiset; + s := multiset{}; + print s, " "; // multiset{} + s := multiset{6, 19, 6}; + print |s|, " "; // 3 + print 7 in s, " ", 6 in s, "\n"; // false true + print s[6], " ", s[19], " ", s[20], "\n"; // 2 1 0 + s := s[17 := 3][1800 := 0][6 := 1]; + print s[6], " ", s[17], " ", s[20], "\n"; // 1 3 0 + + var t: IntMultiset := s; + + s := s + t; + s := s - t; + s := s * t; + expect s == t; + print |s|, "\n"; // 5 + s := s - t; + + var disjoint := s !! t; + print s, " ", disjoint, "\n"; // multiset{} true + + var u: multiset; + u := s as multiset; + s := u as IntMultiset; + var b0 := s is multiset; + var b1 := u is IntMultiset; + + print |s|, " ", |u|, " ", b0, " ", b1, "\n"; // 0 0 true true + + b0 := s <= t; + b1 := s < t; + var b2 := s > s; + var b3 := s >= s; + print b0, " ", b1, " ", b2, " ", b3, "\n"; // true true false true + + b0 := s == t; + b1 := s != t; + print b0, " ", b1, "\n"; // false true + } +} + +module Seq { + newtype IntSeq = s: seq | true + + method Test() { + var s: IntSeq; + s := []; + print s, " "; // [] + s := [6, 19, 6]; + print |s|, " "; // 3 + print 7 in s, " ", 6 in s, "\n"; // false true + print s[0], " ", s[1], " ", s[2], "\n"; // 6 19 6 + s := s[1 := 3][0 := 0][2 := 1]; + print s[0], " ", s[1], " ", s[2], "\n"; // 0 3 1 + + var t: IntSeq := s; + + s := s + t; + print |s|, " ", s, "\n"; // 6 [0, 3, 1, 0, 3, 1] + + var u: seq; + u := s as seq; + s := u as IntSeq; + var b0 := s is seq; + var b1 := u is IntSeq; + + print |s|, " ", |u|, " ", |t|, " ", b0, " ", b1, "\n"; // 6 6 3 true true + + b0 := s <= t; + b1 := s < t; + var b2 := s <= s; + var b3 := t < s; + print b0, " ", b1, " ", b2, " ", b3, "\n"; // false false true true + + b0 := s == t; + b1 := s != t; + print b0, " ", b1, "\n"; // false true + + s := seq(4, i => 8 * i + 3); + print s, "\n"; // [3, 11, 19, 27] + + SubSequences(s); + } + + method SubSequences(s: IntSeq) + requires |s| == 4 + { + Print(s[..2], " "); // [3, 11] + Print(s[2..], " "); // [19, 27] + Print(s[1..3], " "); // [11, 19] + Print(s[..], "\n"); // [3, 11, 19, 27] + + var arr := new int[4] [11, 13, 17, 19]; + Print(arr[..2], " "); // [11, 13] + Print(arr[2..], " "); // [17, 19] + Print(arr[1..3], " "); // [13, 17] + Print(arr[..], "\n"); // [11, 13, 17, 19]; + } + + method Print(s: IntSeq, suffix: string) { + print s, suffix; + } +} + +module SeqToMultisetConversion { + newtype XSet = s: set | true + newtype XSeq = s: seq | true + newtype XMultiset = s: multiset | true + + method Test() { + TestFromSet(); + TestFromSeq(); + } + + method TestFromSet() { + var s: set; + var s': XSet; + var m0: multiset; + var m1: multiset; + var m0': XMultiset; + var m1': XMultiset; + + s := {37, 43, 37, 47}; + s' := {47, 43, 37}; + + m0 := multiset(s); + m1 := multiset(s'); + assert m0 == m1; + print m0 == m1, " ", |m0|, "\n"; // true 3 + + m0' := multiset(s); + m1' := multiset(s'); + assert m0' == m1'; + print m0' == m1', " ", |m0'|, "\n"; // true 3 + } + + method TestFromSeq() { + var s: seq; + var s': XSeq; + var m0: multiset; + var m1: multiset; + var m0': XMultiset; + var m1': XMultiset; + + s := [37, 43, 37, 47]; + s' := s as XSeq; + s' := s'[0 := s'[1]][1 := s'[0]]; // swap elements 0 and 1, just to be a little different + + m0 := multiset(s); + m1 := multiset(s'); + assert m0 == m1; + print m0 == m1, " ", |m0|, "\n"; // true 4 + + m0' := multiset(s); + m1' := multiset(s'); + assert m0' == m1'; + print m0' == m1', " ", |m0'|, "\n"; // true 4 + } +} + +module Map { + newtype IntMap = m: map | true + newtype IntSet = s: set | true + + method Test() { + var m: IntMap; + m := map[]; + print m, " "; // map[] + m := map[6 := 2.0, 19 := 2.1]; + var n: IntMap := m; + print |m|, " "; // 2 + print 7 in m, " ", 6 in m, "\n"; // false true + print m[6], " ", m[19], "\n"; // 2.0 2.1 + m := m[17 := 3.0][1800 := 0.0][6 := 1.0]; + print m[6], " ", m[19], " ", m[17], "\n"; // 1.0 2.1 3.0 + + m := m + n; + // m is now: map[6 := 2.0, 17 := 3.0, 19 := 2.1, 1800 := 0.0] + print |m|, " ", m[6], "\n"; // 4 2.0 + + var sf: set := {3, 4, 5, 17, 20}; + m := m - sf; + var nf: IntSet := {3, 1800, 4, 5}; + m := m - nf; + // m is now: map[6 := 2.0, 19 := 2.1] + print |m|, " ", m[6] + m[19], "\n"; // 2 4.1 + + var u: map; + u := m as map; + m := u as IntMap; + var b0 := m is map; + var b1 := u is IntMap; + + print |m|, " ", |u|, " ", b0, " ", b1, "\n"; // 2 2 true true + + b0 := m == n; + b1 := m != n; + print b0, " ", b1, "\n"; // true false + + TestComprehensions(); + } + + method TestComprehensions() { + var m: IntMap := map x: int | 2 <= x < 5 :: (2 * x) as real; + var n: IntMap := map x: int | 2 <= x < 5 :: 2 * x := 10.0 - x as real; + expect |m| == |n| == 3; + print 2 in m, " ", 2 in n, " ", 4 in m, " ", 4 in n, "\n"; // true false true true + assert 2 * 3 in n; + print m[3], " ", n[6], "\n"; // 6.0 7.0 + } +} + +module Imap { + newtype IntImap = m: imap | true + newtype IntSet = s: set | true + + method Test() { + var m: IntImap; + m := imap[]; + print m, " "; // imap[] + m := imap[6 := 2.0, 19 := 2.1]; + var n: IntImap := m; + print 7 in m, " ", 6 in m, "\n"; // false true + print m[6], " ", m[19], "\n"; // 2.0 2.1 + m := m[17 := 3.0][1800 := 0.0][6 := 1.0]; + print m[6], " ", m[19], " ", m[17], "\n"; // 1.0 2.1 3.0 + + m := m + n; + // m is now: imap[6 := 2.0, 17 := 3.0, 19 := 2.1, 1800 := 0.0] + print m[6], "\n"; // 2.0 + + var sf: set := {3, 4, 5, 17, 20}; + m := m - sf; + var nf: IntSet := {3, 1800, 4, 5}; + m := m - nf; + // m is now: imap[6 := 2.0, 19 := 2.1] + print m[6] + m[19], "\n"; // 4.1 + + var u: imap; + u := m as imap; + m := u as IntImap; + var b0 := m is imap; + var b1 := u is IntImap; + + print b0, " ", b1, "\n"; // true true + + b0 := m == n; + b1 := m != n; + print b0, " ", b1, "\n"; // true false + + TestComprehensions(); + } + + method TestComprehensions() { + var m: IntImap := imap x: int | 2 <= x < 5 :: (2 * x) as real; + var n: IntImap := imap x: int | 2 <= x < 5 :: 2 * x := 10.0 - x as real; + print 2 in m, " ", 2 in n, " ", 4 in m, " ", 4 in n, "\n"; // true false true true + assert 2 * 3 in n; + print m[3], " ", n[6], "\n"; // 6.0 7.0 + } +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GeneralNewtypeCollectionsGeneric.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GeneralNewtypeCollectionsGeneric.dfy.expect new file mode 100644 index 00000000000..5b1d5d665c3 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GeneralNewtypeCollectionsGeneric.dfy.expect @@ -0,0 +1,52 @@ +{} 2 4 true 4 false +[false, true, true] {} true +0 0 true true +true true false true +false true +15 +iset: {} {19} {} true +{} {} true true +true true false true +false true +Ends in B +K is done +multiset{} 3 false true +2 1 0 +1 3 0 +5 +multiset{} true +0 0 true true +true true false true +false true +[] 3 false true +6 19 6 +0 3 1 +6 [0, 3, 1, 0, 3, 1] +6 6 3 true true +false false true true +false true +[3, 11, 19, 27] +[3, 11] [19, 27] [11, 19] [3, 11, 19, 27] +[11, 13] [17, 19] [13, 17] [11, 13, 17, 19] +true 3 +true 3 +true 4 +true 4 +map[] 2 false true +2.0 2.1 +1.0 2.1 3.0 +4 2.0 +2 4.1 +2 2 true true +true false +true false true true +6.0 7.0 +map[] false true +2.0 2.1 +1.0 2.1 3.0 +2.0 +4.1 +true true +true false +true false true true +6.0 7.0 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GeneralNewtypeResolution.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GeneralNewtypeResolution.dfy index 33cec4e01a1..b5354f3711d 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GeneralNewtypeResolution.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GeneralNewtypeResolution.dfy @@ -696,3 +696,261 @@ module TLAStyleOperators { (&& b) as bool } } + +module TypeParametersForNewtypes { + newtype Wrapper = g: G | true witness * // (error under /generalNewtypes:0) + + method Test0() { + var wb: Wrapper; + wb := true; // error: cannot assign bool to a Wrapper + } + + method Test1(b: bool) { + var wb: Wrapper; + wb := b; // error: cannot assign bool to a Wrapper + } + + method Test2(b: bool) { + var wb: Wrapper; + wb := b; // error: cannot assign bool to a Wrapper + } + + method Test3(b: bool) { + var wb: Wrapper; + wb := b as Wrapper; // error: not enough is known about the target type to determine if this is legal + } + + method Test4(b: bool) { + var wb: Wrapper; + wb := b as Wrapper; + } + + method Test5(b: bool) { + var wb: Wrapper; + wb := b as Wrapper; + } + + method Test6(b: bool) { + var wb: Wrapper; + wb := b as Wrapper; + } +} + +module TypeParametersForSubsetTypes { + type Wrapper = g: G | true witness * + + method Test0() { + var wb: Wrapper; + wb := true; + } + + method Test1(b: bool) { + var wb: Wrapper; + wb := b; + } + + method Test2(b: bool) { + var wb: Wrapper; + wb := b; + } + + method Test3(b: bool) { + var wb: Wrapper; + wb := b as Wrapper; // error: not enough is known about the target type to determine if this is legal + } + + method Test4(b: bool) { + var wb: Wrapper; + wb := b as Wrapper; + } + + method Test5(b: bool) { + var wb: Wrapper; + wb := b as Wrapper; + } + + method Test6(b: bool) { + var wb: Wrapper; + wb := b as Wrapper; + } +} + +module TypeParametersForTypeSynonyms { + type Wrapper = G + + method Test0() { + var wb: Wrapper; + wb := true; + } + + method Test1(b: bool) { + var wb: Wrapper; + wb := b; + } + + method Test2(b: bool) { + var wb: Wrapper; + wb := b; + } + + method Test3(b: bool) { + var wb: Wrapper; + wb := b as Wrapper; // error: not enough is known about the target type to determine if this is legal + } + + method Test4(b: bool) { + var wb: Wrapper; + wb := b as Wrapper; + } + + method Test5(b: bool) { + var wb: Wrapper; + wb := b as Wrapper; + } + + method Test6(b: bool) { + var wb: Wrapper; + wb := b as Wrapper; + } +} + +module TypeVarianceIsUsedCorrectly { + datatype P0 = R(f: int -> X) + datatype P1 = R(f: int -> X) + datatype P2<+X> = R(f: int -> X) + datatype P3<*X> = R(f: int -> X) + datatype P4<-X> = R(f: int -> X) // error + + datatype M0 = R(f: X -> int) // error + datatype M1 = R(f: X -> int) + datatype M2<+X> = R(f: X -> int) // error + datatype M3<*X> = R(f: X -> int) // error + datatype M4<-X> = R(f: X -> int) + + newtype Co0 = s: seq X> | true + newtype Co1 = s: seq X> | true + newtype Co2<+X> = s: seq X> | true + newtype Co3<*X> = s: seq X> | true + newtype Co4<-X> = s: seq X> | true // error: X is not used properly + + newtype Contra0 = s: seq int> | true // error: X is not used properly + newtype Contra1 = s: seq int> | true + newtype Contra2<+X> = s: seq int> | true // error: X is not used properly + newtype Contra3<*X> = s: seq int> | true // error: X is not used properly + newtype Contra4<-X> = s: seq int> | true +} + +module TypeCharacteristicsAreUsedCorrectly { + export + provides A0, A1, A2, A3, B0, B1, B2, B3 + provides G0, G1, G2, G3, H0, H1, H2, H3 + + type NeedsEq + type NeedsAutoInit + type NeedsNonempty + type NeedsNoReferences + + newtype A0 = NeedsEq // error: Y does not support (==) + newtype A1 = NeedsAutoInit // error: Y does not support (0) + newtype A2 = NeedsNonempty // error: Y does not support (00) + newtype A3 = NeedsNoReferences // error: Y does not support (!new) + + newtype B0 = NeedsEq + newtype B1 = NeedsAutoInit + newtype B2 = NeedsNonempty + newtype B3 = NeedsNoReferences + + type G0 = NeedsEq // error: Y does not support (==) + type G1 = NeedsAutoInit // error: Y does not support (0) + type G2 = NeedsNonempty // error: Y does not support (00) + type G3 = NeedsNoReferences // error: Y does not support (!new) + + type H0 = NeedsEq + type H1 = NeedsAutoInit + type H2 = NeedsNonempty + type H3 = NeedsNoReferences +} + +module EqualitySupportInference { + export + reveals * + + type NeedsEq + + type Z0 = NeedsEq // no problem, because Y is inferred to be (==) + newtype A0 = NeedsEq // no problem, because Y is inferred to be (==) +} + +module RefinementBase { + type A + + type N + type O + + type V<+A, B, -C> + type W<+A, B, -C> +} + +module RefinementSubsetTypes refines RefinementBase { + type A = x: int | true // error: type-parameter renaming is not allowed in refinement + + type N = x: int | true + type O< + V(0), // error: refinement cannot change type characteristics + W(00), // error: refinement cannot change type characteristics + X, // error: refinement cannot change type characteristics + Y, // error: refinement cannot change type characteristics + YY(==), // error: refinement cannot change type characteristics + Z, // error: refinement cannot change type characteristics + ZZ(!new) // error: refinement cannot change type characteristics + > = x: int | true + + type V<+A, B, -C> = x: int | true + type W< + -A, // error: refinement cannot change variance + +B, // error: refinement cannot change variance + C // error: refinement cannot change variance + > = x: int | true +} + +module RefinementNewtypes refines RefinementBase { + newtype A = x: int | true // error: type-parameter renaming is not allowed in refinement + + newtype N = x: int | true + newtype O< + V(0), // error: refinement cannot change type characteristics + W(00), // error: refinement cannot change type characteristics + X, // error: refinement cannot change type characteristics + Y, // error: refinement cannot change type characteristics + YY(==), // error: refinement cannot change type characteristics + Z, // error: refinement cannot change type characteristics + ZZ(!new) // error: refinement cannot change type characteristics + > = x: int | true + + newtype V<+A, B, -C> = x: int | true + newtype W< + -A, // error: refinement cannot change variance + +B, // error: refinement cannot change variance + C // error: refinement cannot change variance + > = x: int | true +} + +module Cycle0 { + newtype W = X + newtype A = w: W | true // error: cycle: A -> A +} + +module Cycle1 { + newtype W = X + newtype A = W // error: cycle: A -> A +} + +module Cycle2 { + newtype W = X + type A = W // error: cycle: A -> A +} + +module Cycle3 { + type W = X + newtype A = W // error: cycle: A -> A +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GeneralNewtypeResolution.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GeneralNewtypeResolution.dfy.expect index 57f21b5d8cb..60ec73a31a3 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GeneralNewtypeResolution.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GeneralNewtypeResolution.dfy.expect @@ -143,7 +143,59 @@ GeneralNewtypeResolution.dfy(670,11): Error: Function body type mismatch (expect GeneralNewtypeResolution.dfy(675,12): Error: Function body type mismatch (expected bool, got MyBool) GeneralNewtypeResolution.dfy(679,12): Error: Function body type mismatch (expected bool, got MyBool) GeneralNewtypeResolution.dfy(683,12): Error: Function body type mismatch (expected bool, got MyBool) -145 resolution/type errors detected in GeneralNewtypeResolution.dfy +GeneralNewtypeResolution.dfy(701,10): Error: a newtype ('Wrapper') must be based on some numeric type (got G) +GeneralNewtypeResolution.dfy(705,10): Error: boolean literal used as if it had type Wrapper +GeneralNewtypeResolution.dfy(710,7): Error: RHS (of type bool) not assignable to LHS (of type Wrapper) +GeneralNewtypeResolution.dfy(715,7): Error: RHS (of type bool) not assignable to LHS (of type Wrapper) +GeneralNewtypeResolution.dfy(720,12): Error: type conversion target type not determined (got 'Wrapper') +GeneralNewtypeResolution.dfy(759,12): Error: type conversion target type not determined (got '?4') +GeneralNewtypeResolution.dfy(798,12): Error: type conversion target type not determined (got '?4') +GeneralNewtypeResolution.dfy(830,10): Error: a newtype ('Co0') must be based on some numeric type (got seq X>) +GeneralNewtypeResolution.dfy(831,10): Error: a newtype ('Co1') must be based on some numeric type (got seq X>) +GeneralNewtypeResolution.dfy(832,10): Error: a newtype ('Co2') must be based on some numeric type (got seq X>) +GeneralNewtypeResolution.dfy(833,10): Error: a newtype ('Co3') must be based on some numeric type (got seq X>) +GeneralNewtypeResolution.dfy(834,10): Error: a newtype ('Co4') must be based on some numeric type (got seq X>) +GeneralNewtypeResolution.dfy(836,10): Error: a newtype ('Contra0') must be based on some numeric type (got seq int>) +GeneralNewtypeResolution.dfy(837,10): Error: a newtype ('Contra1') must be based on some numeric type (got seq int>) +GeneralNewtypeResolution.dfy(838,10): Error: a newtype ('Contra2') must be based on some numeric type (got seq int>) +GeneralNewtypeResolution.dfy(839,10): Error: a newtype ('Contra3') must be based on some numeric type (got seq int>) +GeneralNewtypeResolution.dfy(840,10): Error: a newtype ('Contra4') must be based on some numeric type (got seq int>) +GeneralNewtypeResolution.dfy(853,10): Error: a newtype ('A0') must be based on some numeric type (got NeedsEq) +GeneralNewtypeResolution.dfy(854,10): Error: a newtype ('A1') must be based on some numeric type (got NeedsAutoInit) +GeneralNewtypeResolution.dfy(855,10): Error: a newtype ('A2') must be based on some numeric type (got NeedsNonempty) +GeneralNewtypeResolution.dfy(856,10): Error: a newtype ('A3') must be based on some numeric type (got NeedsNoReferences) +GeneralNewtypeResolution.dfy(858,10): Error: a newtype ('B0') must be based on some numeric type (got NeedsEq) +GeneralNewtypeResolution.dfy(859,10): Error: a newtype ('B1') must be based on some numeric type (got NeedsAutoInit) +GeneralNewtypeResolution.dfy(860,10): Error: a newtype ('B2') must be based on some numeric type (got NeedsNonempty) +GeneralNewtypeResolution.dfy(861,10): Error: a newtype ('B3') must be based on some numeric type (got NeedsNoReferences) +GeneralNewtypeResolution.dfy(881,10): Error: a newtype ('A0') must be based on some numeric type (got NeedsEq) +GeneralNewtypeResolution.dfy(895,9): Error: type parameters are not allowed to be renamed from the names given in the type in the module being refined (expected 'T', found 'U') +GeneralNewtypeResolution.dfy(899,4): Error: type parameter 'V' is not allowed to change the requirement of supporting auto-initialization +GeneralNewtypeResolution.dfy(900,4): Error: type parameter 'W' is not allowed to change the requirement of supporting auto-initialization +GeneralNewtypeResolution.dfy(901,4): Error: type parameter 'X' is not allowed to change the requirement of being nonempty +GeneralNewtypeResolution.dfy(902,4): Error: type parameter 'Y' is not allowed to change the requirement of supporting equality +GeneralNewtypeResolution.dfy(903,4): Error: type parameter 'YY' is not allowed to change the requirement of supporting equality +GeneralNewtypeResolution.dfy(904,4): Error: type parameter 'Z' is not allowed to change the no-reference-type requirement +GeneralNewtypeResolution.dfy(905,4): Error: type parameter 'ZZ' is not allowed to change the no-reference-type requirement +GeneralNewtypeResolution.dfy(910,5): Error: type parameter 'A' is not allowed to change variance (here, from '+' to '-') +GeneralNewtypeResolution.dfy(911,5): Error: type parameter 'B' is not allowed to change variance (here, from '=' to '+') +GeneralNewtypeResolution.dfy(912,4): Error: type parameter 'C' is not allowed to change variance (here, from '-' to '=') +GeneralNewtypeResolution.dfy(917,12): Error: type parameters are not allowed to be renamed from the names given in the newtype in the module being refined (expected 'T', found 'U') +GeneralNewtypeResolution.dfy(921,4): Error: type parameter 'V' is not allowed to change the requirement of supporting auto-initialization +GeneralNewtypeResolution.dfy(922,4): Error: type parameter 'W' is not allowed to change the requirement of supporting auto-initialization +GeneralNewtypeResolution.dfy(923,4): Error: type parameter 'X' is not allowed to change the requirement of being nonempty +GeneralNewtypeResolution.dfy(924,4): Error: type parameter 'Y' is not allowed to change the requirement of supporting equality +GeneralNewtypeResolution.dfy(925,4): Error: type parameter 'YY' is not allowed to change the requirement of supporting equality +GeneralNewtypeResolution.dfy(926,4): Error: type parameter 'Z' is not allowed to change the no-reference-type requirement +GeneralNewtypeResolution.dfy(927,4): Error: type parameter 'ZZ' is not allowed to change the no-reference-type requirement +GeneralNewtypeResolution.dfy(932,5): Error: type parameter 'A' is not allowed to change variance (here, from '+' to '-') +GeneralNewtypeResolution.dfy(933,5): Error: type parameter 'B' is not allowed to change variance (here, from '=' to '+') +GeneralNewtypeResolution.dfy(934,4): Error: type parameter 'C' is not allowed to change variance (here, from '-' to '=') +GeneralNewtypeResolution.dfy(940,10): Error: recursive constraint dependency involving a newtype: A -> A +GeneralNewtypeResolution.dfy(945,10): Error: recursive constraint dependency involving a newtype: A -> A +GeneralNewtypeResolution.dfy(950,7): Error: type-synonym cycle: A -> A +GeneralNewtypeResolution.dfy(955,10): Error: recursive constraint dependency involving a newtype: A -> A +197 resolution/type errors detected in GeneralNewtypeResolution.dfy GeneralNewtypeResolution.dfy(34,10): Error: a newtype ('MyOrdinal') must be based on some non-reference, non-trait, non-arrow, non-ORDINAL, non-datatype type (got ORDINAL) GeneralNewtypeResolution.dfy(40,10): Error: a newtype ('MyObject') must be based on some non-reference, non-trait, non-arrow, non-ORDINAL, non-datatype type (got object) GeneralNewtypeResolution.dfy(41,10): Error: a newtype ('MyTrait') must be based on some non-reference, non-trait, non-arrow, non-ORDINAL, non-datatype type (got Trait) @@ -262,4 +314,52 @@ GeneralNewtypeResolution.dfy(670,11): Error: Function body type mismatch (expect GeneralNewtypeResolution.dfy(675,12): Error: Function body type mismatch (expected bool, got MyBool) GeneralNewtypeResolution.dfy(679,12): Error: Function body type mismatch (expected bool, got MyBool) GeneralNewtypeResolution.dfy(683,12): Error: Function body type mismatch (expected bool, got MyBool) -117 resolution/type errors detected in GeneralNewtypeResolution.dfy +GeneralNewtypeResolution.dfy(705,10): Error: boolean literal used as if it had type Wrapper +GeneralNewtypeResolution.dfy(710,7): Error: RHS (of type bool) not assignable to LHS (of type Wrapper) +GeneralNewtypeResolution.dfy(715,7): Error: RHS (of type bool) not assignable to LHS (of type Wrapper) +GeneralNewtypeResolution.dfy(720,12): Error: type conversion target type not determined (got 'Wrapper') +GeneralNewtypeResolution.dfy(759,12): Error: type conversion target type not determined (got '?4') +GeneralNewtypeResolution.dfy(798,12): Error: type conversion target type not determined (got '?4') +GeneralNewtypeResolution.dfy(822,32): Error: formal type parameter 'X' is not used according to its variance specification +GeneralNewtypeResolution.dfy(824,24): Error: formal type parameter 'X' is not used according to its variance specification (it is used left of an arrow) (perhaps try declaring 'X' as '-X' or '!X') +GeneralNewtypeResolution.dfy(826,25): Error: formal type parameter 'X' is not used according to its variance specification +GeneralNewtypeResolution.dfy(827,25): Error: formal type parameter 'X' is not used according to its variance specification +GeneralNewtypeResolution.dfy(834,34): Error: formal type parameter 'X' is not used according to its variance specification +GeneralNewtypeResolution.dfy(836,30): Error: formal type parameter 'X' is not used according to its variance specification (it is used left of an arrow) (perhaps try declaring 'X' as '-X' or '!X') +GeneralNewtypeResolution.dfy(838,31): Error: formal type parameter 'X' is not used according to its variance specification +GeneralNewtypeResolution.dfy(839,31): Error: formal type parameter 'X' is not used according to its variance specification +GeneralNewtypeResolution.dfy(853,18): Error: type parameter (X) passed to type NeedsEq must support equality (got Y) (perhaps try declaring type parameter 'Y' on line 853 as 'Y(==)', which says it can only be instantiated with a type that supports equality) +GeneralNewtypeResolution.dfy(854,18): Error: type parameter (X) passed to type NeedsAutoInit must support auto-initialization (got Y) (perhaps try declaring type parameter 'Y' on line 854 as 'Y(0)', which says it can only be instantiated with a type that supports auto-initialization) +GeneralNewtypeResolution.dfy(855,18): Error: type parameter (X) passed to type NeedsNonempty must be nonempty (got Y) (perhaps try declaring type parameter 'Y' on line 855 as 'Y(00)', which says it can only be instantiated with a nonempty type) +GeneralNewtypeResolution.dfy(856,18): Error: type parameter (X) passed to type NeedsNoReferences must contain no references (got Y) (perhaps try declaring type parameter 'Y' on line 856 as 'Y(!new)', which says it can only be instantiated with a type that contains no references) +GeneralNewtypeResolution.dfy(863,15): Error: type parameter (X) passed to type NeedsEq must support equality (got Y) (perhaps try declaring type parameter 'Y' on line 863 as 'Y(==)', which says it can only be instantiated with a type that supports equality) +GeneralNewtypeResolution.dfy(864,15): Error: type parameter (X) passed to type NeedsAutoInit must support auto-initialization (got Y) (perhaps try declaring type parameter 'Y' on line 864 as 'Y(0)', which says it can only be instantiated with a type that supports auto-initialization) +GeneralNewtypeResolution.dfy(865,15): Error: type parameter (X) passed to type NeedsNonempty must be nonempty (got Y) (perhaps try declaring type parameter 'Y' on line 865 as 'Y(00)', which says it can only be instantiated with a nonempty type) +GeneralNewtypeResolution.dfy(866,15): Error: type parameter (X) passed to type NeedsNoReferences must contain no references (got Y) (perhaps try declaring type parameter 'Y' on line 866 as 'Y(!new)', which says it can only be instantiated with a type that contains no references) +GeneralNewtypeResolution.dfy(895,9): Error: type parameters are not allowed to be renamed from the names given in the type in the module being refined (expected 'T', found 'U') +GeneralNewtypeResolution.dfy(899,4): Error: type parameter 'V' is not allowed to change the requirement of supporting auto-initialization +GeneralNewtypeResolution.dfy(900,4): Error: type parameter 'W' is not allowed to change the requirement of supporting auto-initialization +GeneralNewtypeResolution.dfy(901,4): Error: type parameter 'X' is not allowed to change the requirement of being nonempty +GeneralNewtypeResolution.dfy(902,4): Error: type parameter 'Y' is not allowed to change the requirement of supporting equality +GeneralNewtypeResolution.dfy(903,4): Error: type parameter 'YY' is not allowed to change the requirement of supporting equality +GeneralNewtypeResolution.dfy(904,4): Error: type parameter 'Z' is not allowed to change the no-reference-type requirement +GeneralNewtypeResolution.dfy(905,4): Error: type parameter 'ZZ' is not allowed to change the no-reference-type requirement +GeneralNewtypeResolution.dfy(910,5): Error: type parameter 'A' is not allowed to change variance (here, from '+' to '-') +GeneralNewtypeResolution.dfy(911,5): Error: type parameter 'B' is not allowed to change variance (here, from '=' to '+') +GeneralNewtypeResolution.dfy(912,4): Error: type parameter 'C' is not allowed to change variance (here, from '-' to '=') +GeneralNewtypeResolution.dfy(917,12): Error: type parameters are not allowed to be renamed from the names given in the newtype in the module being refined (expected 'T', found 'U') +GeneralNewtypeResolution.dfy(921,4): Error: type parameter 'V' is not allowed to change the requirement of supporting auto-initialization +GeneralNewtypeResolution.dfy(922,4): Error: type parameter 'W' is not allowed to change the requirement of supporting auto-initialization +GeneralNewtypeResolution.dfy(923,4): Error: type parameter 'X' is not allowed to change the requirement of being nonempty +GeneralNewtypeResolution.dfy(924,4): Error: type parameter 'Y' is not allowed to change the requirement of supporting equality +GeneralNewtypeResolution.dfy(925,4): Error: type parameter 'YY' is not allowed to change the requirement of supporting equality +GeneralNewtypeResolution.dfy(926,4): Error: type parameter 'Z' is not allowed to change the no-reference-type requirement +GeneralNewtypeResolution.dfy(927,4): Error: type parameter 'ZZ' is not allowed to change the no-reference-type requirement +GeneralNewtypeResolution.dfy(932,5): Error: type parameter 'A' is not allowed to change variance (here, from '+' to '-') +GeneralNewtypeResolution.dfy(933,5): Error: type parameter 'B' is not allowed to change variance (here, from '=' to '+') +GeneralNewtypeResolution.dfy(934,4): Error: type parameter 'C' is not allowed to change variance (here, from '-' to '=') +GeneralNewtypeResolution.dfy(940,10): Error: recursive constraint dependency involving a newtype: A -> A +GeneralNewtypeResolution.dfy(945,10): Error: recursive constraint dependency involving a newtype: A -> A +GeneralNewtypeResolution.dfy(950,7): Error: type-synonym cycle: A -> A +GeneralNewtypeResolution.dfy(955,10): Error: recursive constraint dependency involving a newtype: A -> A +165 resolution/type errors detected in GeneralNewtypeResolution.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GeneralNewtypeVerify.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GeneralNewtypeVerify.dfy index a848c77e646..38df2d5f333 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GeneralNewtypeVerify.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GeneralNewtypeVerify.dfy @@ -451,6 +451,116 @@ module Bitvectors { se3 := set x | x in dd; } } + +module TypeParametersForNewtype { + newtype Wrapper = g: G | true witness * + method CallMe(u: Wrapper) returns (v: Wrapper) + + method Test(x: bool) returns (y: Wrapper) { + var b: Wrapper; + b := x as Wrapper; + y := CallMe(b); + } +} + +module TypeParametersForSubsetType { + type Wrapper = g: G | true witness * + method CallMe(u: Wrapper) returns (v: Wrapper) + + method Test(x: bool) returns (y: Wrapper) { + var b: Wrapper; + b := x as Wrapper; + y := CallMe(b); + } +} + +module TypeParametersForTypeSynonym { + type Wrapper = G + method CallMe(u: Wrapper) returns (v: Wrapper) + + method Test(x: bool) returns (y: Wrapper) { + var b: Wrapper; + b := x as Wrapper; + y := CallMe(b); + } +} + +module ExpandToTypeParameterWithoutWitness { + // The following two lines once had caused a crash in the verifier + type A = y: Y | true // error: + newtype B = z: Z | true // error: +} + +module AutoInitValueSubsetType { + type Never = x: int | false witness * + type Impossible = n: Never | true // error: default witness 0 does not satisfy constraint of base type + + method Test() { + var x: Impossible := *; + assert false; + print 10 / x; + } +} + +module AutoInitValueNewtype { + newtype Never = x: int | false witness * + newtype Impossible = n: Never | true // error: default witness 0 does not satisfy constraint of base type + + method Test() { + var x: Impossible := *; + assert false; + print 10 / x; + } +} + +module AutoInitValueNewtypeWithoutVar { + newtype Never = x: int | false witness * + newtype Impossible = Never // error: default witness 0 does not satisfy constraint of base type + + method Test() { + var x: Impossible := *; + assert false; + print 10 / x; + } +} + +module BaseTypeConstraintHelpsWellformednessSubsetType { + predicate P(x: NotSeven) + requires x != 6 + { + true + } + + type NotSeven = x: int | x != 7 witness * + type Okay = n: NotSeven | P(if 8 <= n then n else n - 1) + type NotWellformed = n: NotSeven | P(n) // error: precondition violation +} + +module BaseTypeConstraintHelpsWellformednessNewtype { + predicate P(x: NotSeven) + requires x != 6 + { + true + } + + newtype NotSeven = x: int | x != 7 witness * + newtype Okay = n: NotSeven | P(if 8 <= n then n else n - 1) + newtype NotWellformed = n: NotSeven | P(n) // error: precondition violation +} + +module SimpleNewtypeWitness { + newtype A = x: int | 100 <= x witness 102 + newtype B = a: A | true witness 103 + + newtype C = A // error: default witness 0 does not satisfy constraint + newtype D = A witness 104 + newtype E = A ghost witness 104 + newtype F = A witness * + + newtype G = A witness 13 // error: 13 does not satisfy constraint + newtype H = A ghost witness 13 // error: 13 does not satisfy constraint +} + /* module RealConversions { method TestRealIsInt0(r: real) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GeneralNewtypeVerify.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GeneralNewtypeVerify.dfy.expect index 5996628cae8..d5c70f936c9 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GeneralNewtypeVerify.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GeneralNewtypeVerify.dfy.expect @@ -36,5 +36,17 @@ GeneralNewtypeVerify.dfy(361,13): Error: rotate amount must be non-negative GeneralNewtypeVerify.dfy(364,11): Error: rotate amount must not exceed the width of the result (5) GeneralNewtypeVerify.dfy(367,27): Error: result of operation might violate subset type constraint for 'nat' GeneralNewtypeVerify.dfy(371,35): Error: result of operation might violate newtype constraint for 'BV' +GeneralNewtypeVerify.dfy(490,7): Error: cannot find witness that shows type is inhabited; try giving a hint through a 'witness' or 'ghost witness' clause, or use 'witness *' to treat as a possibly empty type +GeneralNewtypeVerify.dfy(491,10): Error: cannot find witness that shows type is inhabited; try giving a hint through a 'witness' or 'ghost witness' clause, or use 'witness *' to treat as a possibly empty type +GeneralNewtypeVerify.dfy(496,7): Error: trying witness 0: result of operation might violate subset type constraint for 'Never' +GeneralNewtypeVerify.dfy(507,10): Error: trying witness 0: result of operation might violate newtype constraint for 'Never' +GeneralNewtypeVerify.dfy(518,10): Error: trying witness 0: result of operation might violate newtype constraint for 'Never' +GeneralNewtypeVerify.dfy(536,37): Error: function precondition could not be proved +GeneralNewtypeVerify.dfy(529,15): Related location +GeneralNewtypeVerify.dfy(548,40): Error: function precondition could not be proved +GeneralNewtypeVerify.dfy(541,15): Related location +GeneralNewtypeVerify.dfy(555,10): Error: trying witness 0: result of operation might violate newtype constraint for 'A' +GeneralNewtypeVerify.dfy(560,24): Error: result of operation might violate newtype constraint for 'A' +GeneralNewtypeVerify.dfy(561,30): Error: result of operation might violate newtype constraint for 'A' -Dafny program verifier finished with 27 verified, 38 errors +Dafny program verifier finished with 40 verified, 48 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Newtypes.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Newtypes.dfy index ea451650a30..7252276c91f 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Newtypes.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Newtypes.dfy @@ -359,3 +359,16 @@ module SeqTests { { } } + +module SimpleNewtypeWitness { + newtype A = x: int | 100 <= x witness 102 + newtype B = a: A | true witness 103 + + newtype C = A // error: default witness 0 does not satisfy constraint + newtype D = A witness 104 + newtype E = A ghost witness 104 + newtype F = A witness * + + newtype G = A witness 13 // error: 13 does not satisfy constraint + newtype H = A ghost witness 13 // error: 13 does not satisfy constraint +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Newtypes.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Newtypes.dfy.expect index 227ebc833a3..ebbd5134d99 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Newtypes.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Newtypes.dfy.expect @@ -11,5 +11,8 @@ Newtypes.dfy(223,21): Error: new number of occurrences might be negative Newtypes.dfy(226,39): Error: result of operation might violate newtype constraint for 'Even' Newtypes.dfy(238,18): Error: result of operation might violate newtype constraint for 'N' Newtypes.dfy(278,18): Error: result of operation might violate newtype constraint for 'R' +Newtypes.dfy(367,10): Error: trying witness 0: result of operation might violate newtype constraint for 'A' +Newtypes.dfy(372,24): Error: result of operation might violate newtype constraint for 'A' +Newtypes.dfy(373,30): Error: result of operation might violate newtype constraint for 'A' -Dafny program verifier finished with 37 verified, 13 errors +Dafny program verifier finished with 43 verified, 16 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/NonZeroInitialization.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/NonZeroInitialization.dfy index 005c03bd5e0..2dd7714219f 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/NonZeroInitialization.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/NonZeroInitialization.dfy @@ -22,7 +22,7 @@ ghost predicate Yes(six: NewSix) { 4 <= six as int } -newtype YetAnotherNewSix = NewSix +newtype YetAnotherNewSix = NewSix witness 80 // Now with some type parameters datatype List = Nil | Cons(G, List) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/NonZeroInitialization.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/NonZeroInitialization.dfy.expect index a89662782f9..c87e2c2e5f0 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/NonZeroInitialization.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/NonZeroInitialization.dfy.expect @@ -12,4 +12,4 @@ NonZeroInitialization.dfy(39,5): Error: cannot find witness that shows type is i NonZeroInitialization.dfy(53,0): Error: out-parameter 'g', which is subject to definite-assignment rules, might be uninitialized at this return point NonZeroInitialization.dfy(58,7): Error: unless an initializer is provided for the array elements, a new array of 'Yt' must have empty size -Dafny program verifier finished with 11 verified, 13 errors +Dafny program verifier finished with 12 verified, 13 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/PrettyPrinting.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/PrettyPrinting.dfy index 1044d73d40b..1e7910c7da8 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/PrettyPrinting.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/PrettyPrinting.dfy @@ -198,3 +198,13 @@ module BoundedPolymorphism { iterator Iter(o: O) { } } + +module SimpleNewtypeWitness { + newtype A = x: int | 100 <= x witness 102 + newtype B = a: A | true witness 103 + + newtype C = A + newtype D = A witness 104 + newtype E = A ghost witness 104 + newtype F = A witness * +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/PrettyPrinting.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/PrettyPrinting.dfy.expect index 0bb2e869e44..3d419383a24 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/PrettyPrinting.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/PrettyPrinting.dfy.expect @@ -229,6 +229,27 @@ module BoundedPolymorphism { { } } + +module SimpleNewtypeWitness { + newtype A = x: int + | 100 <= x + witness 102 + + newtype B = a: A + | true + witness 103 + + newtype C = A + + newtype D = A + witness 104 + + newtype E = A + ghost witness 104 + + newtype F = A + witness * +} 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/SubsetTypes.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy.expect index f627136c12e..69fdfc5c714 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy.expect @@ -91,5 +91,5 @@ SubsetTypes.dfy(459,15): Error: assertion might not hold SubsetTypes.dfy(464,13): Error: assertion might not hold Dafny program verifier finished with 13 verified, 91 errors -Total resources used is 738270 +Total resources used is 738370 Max resources used by VC is 67520 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Tooltips.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Tooltips.dfy new file mode 100644 index 00000000000..2f490445ec4 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Tooltips.dfy @@ -0,0 +1,23 @@ +// RUN: %dafny /compile:0 /typeSystemRefresh:1 /generalNewtypes:1 /printTooltips "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +type D = set + +type B0 = (int, B1) +type B1 = y: set | true + +newtype NN = iset +datatype B2 = Something(NN) + +newtype OO = y: iset | true +codatatype B3 = Something(OO) + +method M(s: set) +method N() returns (s: set) +function F(s: set): U +function G(x: U): set + +method M'(s: set) +method N'() returns (s: set) +function F'(s: set): int +function G'(x: int): set diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Tooltips.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Tooltips.dfy.expect new file mode 100644 index 00000000000..db3d6ab324c --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Tooltips.dfy.expect @@ -0,0 +1,18 @@ +Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format +Tooltips.dfy(4,7): Info: (==) +Tooltips.dfy(6,8): Info: (==) +Tooltips.dfy(7,8): Info: (==) +Tooltips.dfy(9,12): Info: (==) +Tooltips.dfy(10,13): Info: (==) +Tooltips.dfy(12,12): Info: (==) +Tooltips.dfy(13,15): Info: (==) +Tooltips.dfy(15,9): Info: (==) +Tooltips.dfy(16,9): Info: (==) +Tooltips.dfy(17,11): Info: (==) +Tooltips.dfy(18,11): Info: (==) +Tooltips.dfy(20,7): Info: <_T0(==)> +Tooltips.dfy(21,7): Info: <_T0(==)> +Tooltips.dfy(22,9): Info: <_T0(==)> +Tooltips.dfy(23,9): Info: <_T0(==)> + +Dafny program verifier finished with 2 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeInstantiations.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeInstantiations.dfy index 623ae9c3717..54aad21f2cc 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeInstantiations.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeInstantiations.dfy @@ -44,17 +44,17 @@ module M1 refines M0 { type K0 = List // error: change in (==) type K1 // error: change in (==) type L = List // error: change in (==) - type M = int // fine, because M does support equality - type N = List // error: N does not support equality - type O = List // error: change in (==) - type P = List // fine + type M = int // fine, because M does support equality + type N = List // error: N does not support equality + type O = List // error: change in (==) + type P = List // fine class R { } // error: wrong number of type arguments - class S { } // error: not allowed to rename type parameter (U -> T) + class S { } // error: in refinements, not allowed to rename type parameter (U -> T) class T { } // error: wrong number of type arguments type TP0 // error: wrong number of type arguments type TP1 // error: wrong number of type arguments - type TP2 // error: not allowed to rename type parameter (Y1 -> E1) + type TP2 // error: in refinements, not allowed to rename type parameter (Y1 -> E1) } module ListLibrary { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeInstantiations.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeInstantiations.dfy.expect index 76f43160f7e..505d7f7f15a 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeInstantiations.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeInstantiations.dfy.expect @@ -5,7 +5,7 @@ TypeInstantiations.dfy(42,7): Error: type 'J' is declared with a different numbe TypeInstantiations.dfy(44,10): Error: type parameter 'W' is not allowed to change the requirement of supporting equality TypeInstantiations.dfy(45,10): Error: type parameter 'W' is not allowed to change the requirement of supporting equality TypeInstantiations.dfy(46,9): Error: type parameter 'V' is not allowed to change the requirement of supporting equality -TypeInstantiations.dfy(49,9): Error: type parameter 'U'' is not allowed to change the requirement of supporting equality +TypeInstantiations.dfy(49,9): Error: type parameter 'U' is not allowed to change the requirement of supporting equality TypeInstantiations.dfy(51,8): Error: class 'R' is declared with a different number of type parameters (0 instead of 1) than the corresponding class in the module it refines TypeInstantiations.dfy(52,10): Error: type parameters are not allowed to be renamed from the names given in the class in the module being refined (expected 'U', found 'T') TypeInstantiations.dfy(53,8): Error: class 'T' is declared with a different number of type parameters (1 instead of 0) than the corresponding class in the module it refines diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3962.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3962.dfy.expect index 4cec2d6e258..76775842353 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3962.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3962.dfy.expect @@ -6,6 +6,7 @@ git-issue-3962.dfy(18,4): Info: == git-issue-3962.dfy(20,4): Info: == git-issue-3962.dfy(22,4): Info: == git-issue-3962.dfy(24,4): Info: == +git-issue-3962.dfy(4,7): Info: <_T0(==)> git-issue-3962.dfy(20,16): Error: the calculation step between the previous line and this line could not be proved git-issue-3962.dfy(24,17): Error: the calculation step between the previous line and this line could not be proved diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4188.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4188.dfy.expect index 00a51f822da..ba00363fc08 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4188.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4188.dfy.expect @@ -1,2 +1,2 @@ -Dafny program verifier finished with 3 verified, 0 errors +Dafny program verifier finished with 4 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5520.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5520.dfy new file mode 100644 index 00000000000..4dfe5c0982e --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5520.dfy @@ -0,0 +1,73 @@ +// RUN: %testDafnyForEachResolver --expect-exit-code=4 "%s" + +module SubsetTypeSubsetType { + type Empty = x: int | false witness * + + method OperateOnEmpty(x: Empty) + ensures false + { + } + + type PurportsToBeNonempty = x: Empty | true + witness 506 // error: this is not a witness + + method Test() { + var x: PurportsToBeNonempty := *; + OperateOnEmpty(x); + print 10 / 0; + } +} + +module SubsetTypeNewtype { + type Empty = x: int | false witness * + + newtype PurportsToBeNonempty = x: Empty | true + witness 506 // error: this is not a witness + + method OperateOnEmpty(x: PurportsToBeNonempty) + ensures false + { + } + + method Test() { + var x: PurportsToBeNonempty := *; + OperateOnEmpty(x); + print 10 / 0; + } +} + +module NewtypeSubsetType { + type Empty = x: int | false witness * + + method OperateOnEmpty(x: Empty) + ensures false + { + } + + type PurportsToBeNonempty = x: Empty | true + witness 506 // error: this is not a witness + + method Test() { + var x: PurportsToBeNonempty := *; + OperateOnEmpty(x); + print 10 / 0; + } +} + +module NewtypeNewtype { + type Empty = x: int | false witness * + + newtype PurportsToBeNonempty = x: Empty | true + witness 506 // error: this is not a witness + + method OperateOnEmpty(x: PurportsToBeNonempty) + ensures false + { + } + + method Test() { + var x: PurportsToBeNonempty := *; + OperateOnEmpty(x); + print 10 / 0; + } +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5520.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5520.dfy.expect new file mode 100644 index 00000000000..4d932b10f8b --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5520.dfy.expect @@ -0,0 +1,6 @@ +git-issue-5520.dfy(12,12): Error: result of operation might violate subset type constraint for 'Empty' +git-issue-5520.dfy(25,12): Error: result of operation might violate subset type constraint for 'Empty' +git-issue-5520.dfy(48,12): Error: result of operation might violate subset type constraint for 'Empty' +git-issue-5520.dfy(61,12): Error: result of operation might violate subset type constraint for 'Empty' + +Dafny program verifier finished with 8 verified, 4 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5521.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5521.dfy new file mode 100644 index 00000000000..514b6470ac3 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5521.dfy @@ -0,0 +1,73 @@ +// RUN: %testDafnyForEachResolver --expect-exit-code=4 "%s" + +module WithoutWitnessClause { + type Empty = x: int | false witness * + + newtype NewEmpty = Empty // error: the default-witness 0 is not a witness + + method OperateOnNewEmpty(x: NewEmpty) + ensures false + { + var y: Empty := x as Empty; + } + + method Test() { + var x: NewEmpty := *; + OperateOnNewEmpty(x); + print 10 / 0; + } +} + +module WithWitnessClause { + type Empty = x: int | false witness * + + newtype NewEmpty = Empty witness 506 // error: 506 is not a witness + + method OperateOnNewEmpty(x: NewEmpty) + ensures false + { + var y: Empty := x as Empty; + } + + method Test() { + var x: NewEmpty := *; + OperateOnNewEmpty(x); + print 10 / 0; + } +} + +module WithGhostWitnessClause { + type Empty = x: int | false witness * + + newtype NewEmpty = Empty ghost witness 506 // error: 506 is not a ghost witness + + method OperateOnNewEmpty(x: NewEmpty) + ensures false + { + var y: Empty := x as Empty; + } + + method Test() { + var x: NewEmpty := *; + OperateOnNewEmpty(x); // error: x is used before it has really been initialized + print 10 / 0; + } +} + +module DeclaredAsPossiblyEmpty { + type Empty = x: int | false witness * + + newtype NewEmpty = Empty witness * + + method OperateOnNewEmpty(x: NewEmpty) + ensures false + { + var y: Empty := x as Empty; + } + + method Test() { + var x: NewEmpty := *; + OperateOnNewEmpty(x); // error: x is used before it has really been initialized + print 10 / 0; + } +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5521.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5521.dfy.expect new file mode 100644 index 00000000000..38696de0ef1 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5521.dfy.expect @@ -0,0 +1,7 @@ +git-issue-5521.dfy(6,10): Error: trying witness 0: result of operation might violate subset type constraint for 'Empty' +git-issue-5521.dfy(24,35): Error: result of operation might violate subset type constraint for 'Empty' +git-issue-5521.dfy(42,41): Error: result of operation might violate subset type constraint for 'Empty' +git-issue-5521.dfy(52,22): Error: variable 'x', which is subject to definite-assignment rules, might be uninitialized here +git-issue-5521.dfy(70,22): Error: variable 'x', which is subject to definite-assignment rules, might be uninitialized here + +Dafny program verifier finished with 6 verified, 5 errors diff --git a/docs/dev/news/5495.feat b/docs/dev/news/5495.feat new file mode 100644 index 00000000000..bd115483951 --- /dev/null +++ b/docs/dev/news/5495.feat @@ -0,0 +1,6 @@ +feat: allow type parameters of `newtype` declarations +feat: support optional `witness` clause of constraint-less `newtype` declarations +feat: show tool tips for auto-completed type parameters +feat: show tool tips for inferred `(==)` characteristics +fix: Don't let `newtype` well-formedness checking affect witness checking (fixes ##5520) +fix: Check the emptiness status of constraint-less `newtype` declarations (fixes #5521)