From ade4272e03ac94508a264b72efcfb81ae008128b Mon Sep 17 00:00:00 2001 From: davidcok Date: Wed, 10 May 2023 16:36:41 -0400 Subject: [PATCH 1/9] Changing opaque type to abstract type --- Source/DafnyCore/AST/Grammar/ParseErrors.cs | 8 ++++---- Source/DafnyCore/AST/TopLevelDeclarations.cs | 2 +- Source/DafnyCore/AST/Types/Types.cs | 6 +++--- .../DafnyCore/Compilers/CSharp/Compiler-Csharp.cs | 6 +++--- Source/DafnyCore/Compilers/SinglePassCompiler.cs | 2 +- Source/DafnyCore/Dafny.atg | 4 ++-- Source/DafnyCore/DafnyOptions.cs | 4 ++-- .../Resolver/NameResolutionAndTypeInference.cs | 4 ++-- .../DafnyCore/Rewriters/RefinementTransformer.cs | 14 +++++++------- Test/cloudmake/CloudMake-ParallelBuilds.dfy | 2 +- Test/dafny0/AttributeChecks.dfy | 2 +- Test/dafny0/CompilationErrors.dfy | 2 +- Test/dafny0/DTypes.dfy | 4 ++-- Test/dafny0/EqualityTypesModuleExports.dfy | 2 +- Test/dafny0/ParseErrors.dfy | 2 +- Test/dafny0/ResolutionErrors.dfy | 2 +- Test/dafny0/TypeConstraints.dfy | 2 +- Test/dafny0/TypeInstantiations.dfy | 2 +- Test/exports/ExportResolve.dfy | 2 +- Test/git-issues/git-issue-1074.dfy | 4 ++-- Test/git-issues/git-issue-1151-more.dfy | 4 ++-- Test/git-issues/git-issue-1180a.dfy | 12 ++++++------ Test/git-issues/git-issue-2100.dfy | 4 ++-- Test/git-issues/git-issue-3461.dfy | 2 +- 24 files changed, 49 insertions(+), 49 deletions(-) diff --git a/Source/DafnyCore/AST/Grammar/ParseErrors.cs b/Source/DafnyCore/AST/Grammar/ParseErrors.cs index 6d15bcc3ba9..742313c5fa0 100644 --- a/Source/DafnyCore/AST/Grammar/ParseErrors.cs +++ b/Source/DafnyCore/AST/Grammar/ParseErrors.cs @@ -204,7 +204,7 @@ declared identifier. Add(ErrorId.p_misplaced_ellipsis_in_newtype, @" -There are limitations on refining a newtype, namely that the base type cannot be changed. You can change an opaque type into a newtype, however. +There are limitations on refining a newtype, namely that the base type cannot be changed. You can change an abstract type into a newtype, however. "); Add(ErrorId.p_output_of_function_not_ghost, @@ -282,7 +282,7 @@ its control flow produces (yields) a value, but the execution continues from tha Add(ErrorId.p_unexpected_type_characteristic, @" [Type characteristics](https://dafny.org/latest/DafnyRef/DafnyRef#sec-type-parameters), -indicated in parentheses after the type name, state properties of the otherwise uninterpreted or opaque type. +indicated in parentheses after the type name, state properties of the otherwise uninterpreted or abstract type. The currently defined type characteristics are designated by `==` (equality-supporting), `0` (auto-initializable), `00` (non-empty), and `!new` (non-reference). ", Replacements(new[] { ("==", "replace with '==' - this type supports equality"), @@ -294,7 +294,7 @@ [Type characteristics](https://dafny.org/latest/DafnyRef/DafnyRef#sec-type-param Add(ErrorId.p_missing_type_characteristic, @" [Type characteristics](https://dafny.org/latest/DafnyRef/DafnyRef#sec-type-parameters), -state properties of the otherwise uninterpreted or opaque type. +state properties of the otherwise uninterpreted or abstract type. They are given in a parentheses-enclosed, comma-separated list after the type name. The currently defined type characteristics are designated by `==` (equality - supporting), `0` (auto - initializable), `00` (non - empty), and `!new` (non - reference). "); @@ -302,7 +302,7 @@ state properties of the otherwise uninterpreted or opaque type. Add(ErrorId.p_illegal_type_characteristic, @" [Type characteristics](https://dafny.org/latest/DafnyRef/DafnyRef#sec-type-parameters), -indicated in parentheses after the type name, state properties of the otherwise uninterpreted or opaque type. +indicated in parentheses after the type name, state properties of the otherwise uninterpreted or abstract type. The currently defined type characteristics are designated by `==` (equality - supporting), `0` (auto - initializable), `00` (non - empty), and `!new` (non - reference). Type parameters are given in a parentheses-enclosed, comma-separated list after the type name. "); diff --git a/Source/DafnyCore/AST/TopLevelDeclarations.cs b/Source/DafnyCore/AST/TopLevelDeclarations.cs index 05180f2c9eb..fbe2e180d6e 100644 --- a/Source/DafnyCore/AST/TopLevelDeclarations.cs +++ b/Source/DafnyCore/AST/TopLevelDeclarations.cs @@ -2082,7 +2082,7 @@ public NoContext(ModuleDefinition module) { } public class OpaqueTypeDecl : TopLevelDeclWithMembers, TypeParameter.ParentType, RevealableTypeDecl, ICanFormat, IHasDocstring { - public override string WhatKind { get { return "opaque type"; } } + public override string WhatKind { get { return "abstract type"; } } public override bool CanBeRevealed() { return true; } public readonly TypeParameter.TypeParameterCharacteristics Characteristics; public bool SupportsEquality { diff --git a/Source/DafnyCore/AST/Types/Types.cs b/Source/DafnyCore/AST/Types/Types.cs index 158f336d9fc..69f6ab045d1 100644 --- a/Source/DafnyCore/AST/Types/Types.cs +++ b/Source/DafnyCore/AST/Types/Types.cs @@ -1423,7 +1423,7 @@ public static Type JoinX(Type a, Type b, BuiltIns builtIns) { var udtA = (UserDefinedType)a; return !b.IsRefType ? null : abNonNullTypes ? UserDefinedType.CreateNonNullType(udtA) : udtA; } else { - // "a" is a class, trait, or opaque type + // "a" is a class, trait, or abstract type var aa = ((UserDefinedType)a).ResolvedClass; Contract.Assert(aa != null); if (!(b is UserDefinedType)) { @@ -1647,7 +1647,7 @@ public static Type MeetX(Type a, Type b, BuiltIns builtIns) { } else if (a.IsObjectQ) { return b.IsRefType ? b : null; } else { - // "a" is a class, trait, or opaque type + // "a" is a class, trait, or abstract type var aa = ((UserDefinedType)a).ResolvedClass; Contract.Assert(aa != null); if (!(b is UserDefinedType)) { @@ -2371,7 +2371,7 @@ public UserDefinedType(TypeParameter tp) /// /// This constructor constructs a resolved type parameter (but shouldn't be called if "tp" denotes - /// the .TheType of an opaque type -- use the (OpaqueType_AsParameter, OpaqueTypeDecl, List(Type)) + /// the .TheType of an abstract type -- use the (OpaqueType_AsParameter, OpaqueTypeDecl, List(Type)) /// constructor for that). /// public UserDefinedType(IToken tok, TypeParameter tp) { diff --git a/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs b/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs index a080520dc57..101ee733b88 100644 --- a/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs +++ b/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs @@ -49,13 +49,13 @@ public CsharpCompiler(DafnyOptions options, ErrorReporter reporter) : base(optio string FormatDefaultTypeParameterValue(TopLevelDecl tp) { Contract.Requires(tp is TypeParameter || tp is OpaqueTypeDecl); if (tp is OpaqueTypeDecl) { - // This is unusual. Typically, the compiler never needs to compile an opaque type, but this opaque type + // This is unusual. Typically, the compiler never needs to compile an abstract type, but this abstract type // is apparently an :extern (or a compiler error has already been reported and we're just trying to get to // the end of compilation without crashing). It's difficult to say what the compiler could do in this situation, since - // it doesn't know how to generate code that produces a legal value of the opaque type. If we don't do + // it doesn't know how to generate code that produces a legal value of the abstract type. If we don't do // anything different from the common case (the "else" branch below), then the code emitted will not // compile (see github issue #1151). So, to do something a wee bit better, we emit a placebo value. This - // will only work when the opaque type is in the same module and has no type parameters. + // will only work when the abstract type is in the same module and has no type parameters. return $"default({tp.EnclosingModuleDefinition.GetCompileName(Options) + "." + tp.GetCompileName(Options)})"; } else { // this is the common case diff --git a/Source/DafnyCore/Compilers/SinglePassCompiler.cs b/Source/DafnyCore/Compilers/SinglePassCompiler.cs index 5297c69f756..71c37e25795 100644 --- a/Source/DafnyCore/Compilers/SinglePassCompiler.cs +++ b/Source/DafnyCore/Compilers/SinglePassCompiler.cs @@ -1731,7 +1731,7 @@ public static bool IsPermittedAsMain(Program program, Method m, out String reaso return false; } if (cl is OpaqueTypeDecl) { - reason = "the enclosing type is an opaque type"; + reason = "the enclosing type is an abstract type"; return false; } if (!m.IsStatic) { diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg index 528887255a9..fc34dfa7f86 100644 --- a/Source/DafnyCore/Dafny.atg +++ b/Source/DafnyCore/Dafny.atg @@ -1629,7 +1629,7 @@ SynonymTypeDecl(); var isRefining = false; .) @@ -1670,7 +1670,7 @@ SynonymTypeDecl ConstrainTypeHead(Type super, Type sub) { } else if (super.IsObjectQ) { return sub.IsRefType ? new List() : null; } else { - // The only remaining cases are that "super" is a (co)datatype, opaque type, or non-object trait/class. + // The only remaining cases are that "super" is a (co)datatype, abstract type, or non-object trait/class. // In each of these cases, "super" is a UserDefinedType. var udfSuper = (UserDefinedType)super; var clSuper = udfSuper.ResolvedClass; @@ -4817,7 +4817,7 @@ public ResolveTypeReturn ResolveTypeLenient(IToken tok, Type type, ResolutionCon } else if (r.Type is Resolver_IdentifierExpr.ResolverType_Type) { var d = r.Decl; if (d is OpaqueTypeDecl) { - // resolve like a type parameter, and it may have type parameters if it's an opaque type + // resolve like a type parameter, and it may have type parameters if it's an abstract type t.ResolvedClass = d; // Store the decl, so the compiler will generate the fully qualified name } else if (d is RedirectingTypeDecl) { var dd = (RedirectingTypeDecl)d; diff --git a/Source/DafnyCore/Rewriters/RefinementTransformer.cs b/Source/DafnyCore/Rewriters/RefinementTransformer.cs index 5a629ea2030..5733909aa3c 100644 --- a/Source/DafnyCore/Rewriters/RefinementTransformer.cs +++ b/Source/DafnyCore/Rewriters/RefinementTransformer.cs @@ -73,7 +73,7 @@ public override string Filename { /// there are four kinds of transformations. /// /// 0. "Y" can fill in some definitions that "X" omitted. For example, if "X" defines - /// an opaque type "type T", then "Y" can define "T" to be a particular type, like + /// an abstract type "type T", then "Y" can define "T" to be a particular type, like /// "type T = int". As another example, if "X" omits the body of a function, then /// "Y" can give it a body. /// @@ -302,7 +302,7 @@ private void MergeModuleExports(ModuleExportDecl nw, ModuleExportDecl d) { } private void MergeTopLevelDecls(ModuleDefinition m, TopLevelDecl nw, TopLevelDecl d, int index) { - var commonMsg = "a {0} declaration ({1}) in a refinement module can only refine a {0} declaration or replace an opaque type declaration"; + var commonMsg = "a {0} declaration ({1}) in a refinement module can only refine a {0} declaration or replace an abstract type declaration"; if (d is ModuleDecl) { if (!(nw is ModuleDecl)) { @@ -348,7 +348,7 @@ private void MergeTopLevelDecls(ModuleDefinition m, TopLevelDecl nw, TopLevelDec var udt = UserDefinedType.FromTopLevelDecl(nw.tok, nw); postTasks.Enqueue(() => { if (!udt.SupportsEquality) { - Reporter.Error(MessageSource.RefinementTransformer, udt.tok, "type '{0}', which does not support equality, is used to refine an opaque type with equality support", udt.Name); + Reporter.Error(MessageSource.RefinementTransformer, udt.tok, "type '{0}', which does not support equality, is used to refine an abstract type with equality support", udt.Name); } }); } @@ -359,7 +359,7 @@ private void MergeTopLevelDecls(ModuleDefinition m, TopLevelDecl nw, TopLevelDec var udt = UserDefinedType.FromTopLevelDecl(nw.tok, nw); postTasks.Enqueue(() => { if (!udt.HasCompilableValue) { - Reporter.Error(MessageSource.RefinementTransformer, udt.tok, "type '{0}', which does not support auto-initialization, is used to refine an opaque type that expects auto-initialization", udt.Name); + Reporter.Error(MessageSource.RefinementTransformer, udt.tok, "type '{0}', which does not support auto-initialization, is used to refine an abstract type that expects auto-initialization", udt.Name); } }); } else if (od.Characteristics.IsNonempty) { @@ -368,7 +368,7 @@ private void MergeTopLevelDecls(ModuleDefinition m, TopLevelDecl nw, TopLevelDec var udt = UserDefinedType.FromTopLevelDecl(nw.tok, nw); postTasks.Enqueue(() => { if (!udt.IsNonempty) { - Reporter.Error(MessageSource.RefinementTransformer, udt.tok, "type '{0}', which may be empty, is used to refine an opaque type expected to be nonempty", udt.Name); + Reporter.Error(MessageSource.RefinementTransformer, udt.tok, "type '{0}', which may be empty, is used to refine an abstract type expected to be nonempty", udt.Name); } }); } @@ -377,7 +377,7 @@ private void MergeTopLevelDecls(ModuleDefinition m, TopLevelDecl nw, TopLevelDec m.TopLevelDecls[index] = MergeClass((TopLevelDeclWithMembers)nw, od); } else if (od.Members.Count != 0) { Reporter.Error(MessageSource.RefinementTransformer, nw, - "a {0} ({1}) cannot declare members, so it cannot refine an opaque type with members", + "a {0} ({1}) cannot declare members, so it cannot refine an abstract type with members", nw.WhatKind, nw.Name); } else { CheckAgreement_TypeParameters(nw.tok, d.TypeArgs, nw.TypeArgs, nw.Name, "type", false); @@ -385,7 +385,7 @@ private void MergeTopLevelDecls(ModuleDefinition m, TopLevelDecl nw, TopLevelDec } } else if (nw is OpaqueTypeDecl) { Reporter.Error(MessageSource.RefinementTransformer, nw, - "an opaque type declaration ({0}) in a refining module cannot replace a more specific type declaration in the refinement base", nw.Name); + "an abstract type declaration ({0}) in a refining module cannot replace a more specific type declaration in the refinement base", nw.Name); } else if ((d is IndDatatypeDecl && nw is IndDatatypeDecl) || (d is CoDatatypeDecl && nw is CoDatatypeDecl)) { var (dd, nwd) = ((DatatypeDecl)d, (DatatypeDecl)nw); Contract.Assert(!nwd.Ctors.Any()); diff --git a/Test/cloudmake/CloudMake-ParallelBuilds.dfy b/Test/cloudmake/CloudMake-ParallelBuilds.dfy index 79bbdd6e63f..ae9070ed483 100644 --- a/Test/cloudmake/CloudMake-ParallelBuilds.dfy +++ b/Test/cloudmake/CloudMake-ParallelBuilds.dfy @@ -760,7 +760,7 @@ abstract module M2 refines M1 { } } -// Finally, this module defines any remaining opaque types and function bodies and proves any +// Finally, this module defines any remaining abstract types and function bodies and proves any // remaining lemmas about these. The actual definitions are not so interesting and are not meant // to suggest that a deployed CloudMake use these definitions. Rather, these definitions are here // only to establish mathematical feasibility of previously axiomatized properties. diff --git a/Test/dafny0/AttributeChecks.dfy b/Test/dafny0/AttributeChecks.dfy index 94fd1022d6b..7e21e032d15 100644 --- a/Test/dafny0/AttributeChecks.dfy +++ b/Test/dafny0/AttributeChecks.dfy @@ -415,7 +415,7 @@ module TopLevelAttributes { Iterator(x: int, arr: array) yields (y: int) requires arr.Length != 0 - // ---- opaque type + // ---- abstract type type {:myAttr this} // error: this is not allowed here diff --git a/Test/dafny0/CompilationErrors.dfy b/Test/dafny0/CompilationErrors.dfy index 969ce4fc31f..aa1b4468949 100644 --- a/Test/dafny0/CompilationErrors.dfy +++ b/Test/dafny0/CompilationErrors.dfy @@ -1,7 +1,7 @@ // RUN: %exits-with 3 %dafny "%s" > "%t" // RUN: %diff "%s.expect" "%t" -type MyType // compile error: opaque type +type MyType // compile error: abstract type iterator Iter() // compile error: body-less iterator ghost method M() // compile error: body-less ghost method method P() // compile error: body-less method diff --git a/Test/dafny0/DTypes.dfy b/Test/dafny0/DTypes.dfy index 1f5076b8ac7..db4b7cf82c6 100644 --- a/Test/dafny0/DTypes.dfy +++ b/Test/dafny0/DTypes.dfy @@ -157,7 +157,7 @@ class DatatypeInduction { } } -// --- opaque types with type parameters --- +// --- abstract types with type parameters --- abstract module OpaqueTypesWithParameters { type P @@ -173,7 +173,7 @@ abstract module OpaqueTypesWithParameters { // would be different types, and then the types of 'a' and 'b' would be different, // which would imply that the following postcondition would hold. // However, it is NOT necessarily the case that the type parameters of an opaque - // type actually make the opaque type different. For example, see the refinement + // type actually make the abstract type different. For example, see the refinement // module CaseInPoint below. ensures a != b; // error { diff --git a/Test/dafny0/EqualityTypesModuleExports.dfy b/Test/dafny0/EqualityTypesModuleExports.dfy index 6ac69c21498..d895e973635 100644 --- a/Test/dafny0/EqualityTypesModuleExports.dfy +++ b/Test/dafny0/EqualityTypesModuleExports.dfy @@ -394,7 +394,7 @@ module ScopeRegressions { } } module B { - // To the outside world, "BType" is just an opaque type + // To the outside world, "BType" is just an abstract type export provides BType datatype BType = X | Y } diff --git a/Test/dafny0/ParseErrors.dfy b/Test/dafny0/ParseErrors.dfy index 172bd09d106..89654065cb4 100644 --- a/Test/dafny0/ParseErrors.dfy +++ b/Test/dafny0/ParseErrors.dfy @@ -167,7 +167,7 @@ newtype Pos = x | 0 < x witness 1 var x: int // error: mutable fields not allowed in newtypes } type Opaque { - var x: int // error: mutable field not allowed in opaque type + var x: int // error: mutable field not allowed in abstract type } // ------------------------- nameonly parameters ------------------------------ diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index bf101ba3151..99df5efea67 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -1092,7 +1092,7 @@ module MiscIterator { module {:myAttribute x} Modulette { // error: x does not refer to anything } -// --- opaque types with type parameters --- +// --- abstract types with type parameters --- module OpaqueTypes0 { type P diff --git a/Test/dafny0/TypeConstraints.dfy b/Test/dafny0/TypeConstraints.dfy index 2ecfb774932..9d95e3c5b20 100644 --- a/Test/dafny0/TypeConstraints.dfy +++ b/Test/dafny0/TypeConstraints.dfy @@ -224,7 +224,7 @@ module SimpleClassesAndTraits { } } -module TypeParameters { // and opaque types +module TypeParameters { // and abstract types type A type B type C diff --git a/Test/dafny0/TypeInstantiations.dfy b/Test/dafny0/TypeInstantiations.dfy index ec86feff5bb..f69231fe085 100644 --- a/Test/dafny0/TypeInstantiations.dfy +++ b/Test/dafny0/TypeInstantiations.dfy @@ -30,7 +30,7 @@ abstract module M0 { } module M1 refines M0 { type A = int - type B // error: cannot change a type synonym into an opaque type + type B // error: cannot change a type synonym into an abstract type datatype C = MakeC(ghost x: int, y: int) // error: this type does not support equality type D = C // error: this type does not support equality codatatype E = More(bool, E) // error: this type does not support equality diff --git a/Test/exports/ExportResolve.dfy b/Test/exports/ExportResolve.dfy index 3e42c315d72..9225f900bbe 100644 --- a/Test/exports/ExportResolve.dfy +++ b/Test/exports/ExportResolve.dfy @@ -100,7 +100,7 @@ module NamesThatDontExist { } module ConsistencyErrors { - // Providing a type exports the type name as an opaque type, along with any + // Providing a type exports the type name as an abstract type, along with any // type characteristics, type parameters, and the variance of the type parameters. // In the case of a class C, only type C can be provided, not C? (but both can be revealed). // Export a type does not automatically export datatype constructors, discriminators, or diff --git a/Test/git-issues/git-issue-1074.dfy b/Test/git-issues/git-issue-1074.dfy index d10ea4ffcfa..ea8b7e0ad54 100644 --- a/Test/git-issues/git-issue-1074.dfy +++ b/Test/git-issues/git-issue-1074.dfy @@ -2,12 +2,12 @@ // RUN: %diff "%s.expect" "%t" module A { - // This test uses an opaque type as the type of "children" below. This once caused + // This test uses an abstract type as the type of "children" below. This once caused // a crash in the compiler. // To distinguish the crashing test output from the correct test output, we need to // get to a point where the compiler prints some output. If the compilation succeeds, - // there will be some output. But to make the opaque type compile, it needs to be + // there will be some output. But to make the abstract type compile, it needs to be // marked with an :extern that redirects it to some existing type. Rather than relying // on some type in the C#-or-other-target runtime library, this test declares a class // MyCollection, which is then named in the :extern attribute. (This relies on that diff --git a/Test/git-issues/git-issue-1151-more.dfy b/Test/git-issues/git-issue-1151-more.dfy index bd55c8dc02a..609b7e4b9bf 100644 --- a/Test/git-issues/git-issue-1151-more.dfy +++ b/Test/git-issues/git-issue-1151-more.dfy @@ -8,9 +8,9 @@ // RUN: %diff "%s.expect" "%t" // The following example should produce a compilation error, since there's -// an opaque type. It should not, however, crash. +// an abstract type. It should not, however, crash. -type Opaque(0) // compilation error: this is an opaque type +type Opaque(0) // compilation error: this is an abstract type datatype E = E(Opaque) diff --git a/Test/git-issues/git-issue-1180a.dfy b/Test/git-issues/git-issue-1180a.dfy index 06045c2331c..781254d5d03 100644 --- a/Test/git-issues/git-issue-1180a.dfy +++ b/Test/git-issues/git-issue-1180a.dfy @@ -89,10 +89,10 @@ module StartingFromDatatype { } } module OpaqueType refines A { - type Ty ... // error: cannot refine a datatype with an opaque type + type Ty ... // error: cannot refine a datatype with an abstract type } module OpaqueType' refines A { - type Ty ... { } // error: cannot refine a datatype with an opaque type + type Ty ... { } // error: cannot refine a datatype with an abstract type } module Datatype refines A { datatype Ty ... { @@ -124,7 +124,7 @@ module StartingFromCodatatype { } } module OpaqueType refines A { - type Ty ... // error: cannot refine a codatatype with an opaque type + type Ty ... // error: cannot refine a codatatype with an abstract type } module Datatype refines A { datatype Ty ... // error: cannot refine a codatatype with a datatype @@ -156,7 +156,7 @@ module StartingFromNewtype { } } module OpaqueType refines A { - type Ty ... // error: cannot refine a newtype with an opaque type + type Ty ... // error: cannot refine a newtype with an abstract type } module Datatype refines A { datatype Ty ... // error: cannot refine a newtype with a datatype @@ -185,7 +185,7 @@ module StartingFromClass { } } module OpaqueType refines A { - type Ty ... // error: cannot refine a class with an opaque type + type Ty ... // error: cannot refine a class with an abstract type } module Datatype refines A { datatype Ty ... // error: cannot refine a class with a datatype @@ -214,7 +214,7 @@ module StartingFromTrait { } } module OpaqueType refines A { - type Ty ... // error: cannot refine a trait with an opaque type + type Ty ... // error: cannot refine a trait with an abstract type } module Datatype refines A { datatype Ty ... // error: cannot refine a trait with a datatype diff --git a/Test/git-issues/git-issue-2100.dfy b/Test/git-issues/git-issue-2100.dfy index affa34cdebf..1b69603d482 100644 --- a/Test/git-issues/git-issue-2100.dfy +++ b/Test/git-issues/git-issue-2100.dfy @@ -14,9 +14,9 @@ module Client { // The mention of the export-provided Cl below (in the case where // its parent type, Tr, is not exported) once generated malformed - // Boogie. In particular, Cl should be treated as an opaque type in + // Boogie. In particular, Cl should be treated as an abstract type in // this Client module, but in some places in the translation to Boogie, - // the type was still treated as a non-opaque type. + // the type was still treated as a non-abstract type. method Test(cl: Library.Cl) { } } diff --git a/Test/git-issues/git-issue-3461.dfy b/Test/git-issues/git-issue-3461.dfy index 0407894b7ae..69903f02fa7 100644 --- a/Test/git-issues/git-issue-3461.dfy +++ b/Test/git-issues/git-issue-3461.dfy @@ -11,7 +11,7 @@ opaque predicate p() { true } // OK opaque class A {} // NO opaque datatype D = D // NO opaque newtype N = int // NO -opaque type P = i | i >= 0 // NO +abstract type P = i | i >= 0 // NO method z() { opaque var j: int // NO From 553806abebda2c64e28ea25056456bff65a19d2a Mon Sep 17 00:00:00 2001 From: davidcok Date: Wed, 10 May 2023 16:42:01 -0400 Subject: [PATCH 2/9] Editing .md files --- docs/Compilation/AutoInitialization.md | 2 +- docs/DafnyRef/Attributes.md | 4 ++-- docs/DafnyRef/GrammarDetails.md | 2 +- docs/DafnyRef/Modules.md | 4 ++-- docs/DafnyRef/Programs.md | 2 +- docs/DafnyRef/Refinement.md | 4 ++-- docs/DafnyRef/Types.md | 8 ++++---- docs/DafnyRef/UserGuide.md | 2 +- docs/HowToFAQ/Errors-Parser.md | 8 ++++---- docs/HowToFAQ/FAQDefaultInitialValue.md | 2 +- docs/HowToFAQ/onepage.md | 2 +- docs/OnlineTutorial/Modules.md | 4 ++-- 12 files changed, 22 insertions(+), 22 deletions(-) diff --git a/docs/Compilation/AutoInitialization.md b/docs/Compilation/AutoInitialization.md index 3510ff2bc8f..50ec819cabf 100644 --- a/docs/Compilation/AutoInitialization.md +++ b/docs/Compilation/AutoInitialization.md @@ -35,7 +35,7 @@ Dafny supports the following kinds of types: subset is characterized by a constraint on `B`) In addition, there are _type synonyms_ (which are just that--synonyms for other types) and -_opaque types_ (which cannot be compiled, so they don't play a role here). +_abstract types_ (which cannot be compiled, so they don't play a role here). Notes: * `nat` is a built-in subset type of `int` diff --git a/docs/DafnyRef/Attributes.md b/docs/DafnyRef/Attributes.md index 3733b0cecf8..f9c500a7510 100644 --- a/docs/DafnyRef/Attributes.md +++ b/docs/DafnyRef/Attributes.md @@ -151,7 +151,7 @@ Ignore the declaration (after checking for duplicate names). * to alter the `CompileName` of entities such as modules, classes, methods, etc., * to alter the `ReferenceName` of the entities, -* to decide how to define external opaque types, +* to decide how to define external abstract types, * to decide whether to emit target code or not, and * to decide whether a declaration is allowed not to have a body. @@ -163,7 +163,7 @@ A common use case of `{:extern}` is to avoid name clashes with existing library - `{:extern}`: Dafny will use the Dafny-determined name as the `CompileName` and not affect the `ReferenceName` - `{:extern s1}`: Dafny will use `s1` as the `CompileName`, and replaces the last portion of the `ReferenceName` by `s1`. - When used on an opaque type, s1 is used as a hint as to how to declare that type when compiling. + When used on an abstract type, s1 is used as a hint as to how to declare that type when compiling. - `{:extern s1, s2}` Dafny will use `s2` as the `CompileName`. Dafny will use a combination of `s1` and `s2` such as for example `s1.s2` as the `ReferenceName` It may also be the case that one of the arguments is simply ignored. diff --git a/docs/DafnyRef/GrammarDetails.md b/docs/DafnyRef/GrammarDetails.md index 371dc3c118e..ac80b5d22b1 100644 --- a/docs/DafnyRef/GrammarDetails.md +++ b/docs/DafnyRef/GrammarDetails.md @@ -214,7 +214,7 @@ TopDecl(isTopLevel, isAbstract) = | ClassDecl | DatatypeDecl | NewtypeDecl - | SynonymTypeDecl // includes opaque types + | SynonymTypeDecl // includes abstract types | IteratorDecl | TraitDecl | ClassMemberDecl(allowConstructors: false, isValueType: true, moduleLevelDecl: true) diff --git a/docs/DafnyRef/Modules.md b/docs/DafnyRef/Modules.md index 647f507449f..abd3f447f9a 100644 --- a/docs/DafnyRef/Modules.md +++ b/docs/DafnyRef/Modules.md @@ -628,11 +628,11 @@ by importers to have two implicit heap parameters), and an exported importers can use both `P` and its prefix predicate `P#`). If `C` is a `class`, `trait`, or `iterator`, then `provides C` exports -the non-null reference type `C` as an opaque type. This does not reveal +the non-null reference type `C` as an abstract type. This does not reveal that `C` is a reference type, nor does it export the nullable type `C?`. In most cases, exporting a `class`, `trait`, `datatype`, `codatatype`, or -opaque type does not automatically export its members. Instead, any member +abstract type does not automatically export its members. Instead, any member to be exported must be listed explicitly. For example, consider the type declaration diff --git a/docs/DafnyRef/Programs.md b/docs/DafnyRef/Programs.md index ec28b75a0f9..c579160ed5f 100644 --- a/docs/DafnyRef/Programs.md +++ b/docs/DafnyRef/Programs.md @@ -3,7 +3,7 @@ At the top level, a Dafny program (stored as files with extension `.dfy`) is a set of declarations. The declarations introduce (module-level) constants, methods, functions, lemmas, types (classes, traits, inductive and -coinductive datatypes, newtypes, type synonyms, opaque types, and +coinductive datatypes, newtypes, type synonyms, abstract types, and iterators) and modules, where the order of introduction is irrelevant. Some types, notably classes, also may contain a set of declarations, introducing fields, methods, and functions. diff --git a/docs/DafnyRef/Refinement.md b/docs/DafnyRef/Refinement.md index 5beaec1e88d..000b7f226be 100644 --- a/docs/DafnyRef/Refinement.md +++ b/docs/DafnyRef/Refinement.md @@ -289,7 +289,7 @@ module X refines P { Types can be refined in two ways: -- Turning an opaque type into a concrete type; +- Turning an abstract type into a concrete type; - Adding members to a datatype or a newtype. For example, consider the following abstract module: @@ -359,7 +359,7 @@ refinement. This means that a type declaration `type T(!new)` cannot be refined by a `class T`, for example. Similarly, a `type T(00)` cannot be refined by a subset type with a `witness *` clause. -The refinement of an opaque type with body-less members can include both a definition +The refinement of an abstract type with body-less members can include both a definition for the type along with a body for the member, as in this example: ```dafny diff --git a/docs/DafnyRef/Types.md b/docs/DafnyRef/Types.md index a8f920732ae..13b94e6e534 100644 --- a/docs/DafnyRef/Types.md +++ b/docs/DafnyRef/Types.md @@ -772,7 +772,7 @@ the instantiation `Result` satisfies `(!new)`, whereas Note that this characteristic of a type parameter is operative for both verification and compilation. -Also, opaque types at the topmost scope are always implicitly `(!new)`. +Also, abstract types at the topmost scope are always implicitly `(!new)`. Here are some examples: @@ -1366,7 +1366,7 @@ It is sometimes useful to know a type by several names or to treat a type abstractly. There are several mechanisms in Dafny to do this: * ([Section 5.6.1](#sec-synonym-type)) A typical _synonym type_, in which a type name is a synonym for another type -* ([Section 5.6.2](#sec-opaque-types)) An _opaque type_, in which a new type name is declared as an uninterpreted type +* ([Section 5.6.2](#sec-opaque-types)) An _abstract type_, in which a new type name is declared as an uninterpreted type * ([Section 5.6.3](#sec-subset-types)) A _subset type_, in which a new type name is given to a subset of the values of a given type * ([Section 0.0){#sec-newtypes)) A _newtype_, in which a subset type is declared, but with restrictions on converting to and from its base type @@ -1439,7 +1439,7 @@ type T type Q { function toString(t: T): string } ``` -An opaque type is a special case of a type synonym that is underspecified. Such +An abstract type is a special case of a type synonym that is underspecified. Such a type is declared simply by: ```dafny @@ -1466,7 +1466,7 @@ type Monad ``` can be used abstractly to represent an arbitrary parameterized monad. -Even as an opaque type, the type +Even as an abstract type, the type may be given members such as constants, methods or functions. For example, diff --git a/docs/DafnyRef/UserGuide.md b/docs/DafnyRef/UserGuide.md index 15327480bf2..5485b9a8a07 100644 --- a/docs/DafnyRef/UserGuide.md +++ b/docs/DafnyRef/UserGuide.md @@ -1375,7 +1375,7 @@ would in turn need to be changed to `charseq.UnicodeFromString` to return the correct type. Most declarations, including those for modules, classes, traits, member -variables, constructors, methods, function methods, and opaque types, +variables, constructors, methods, function methods, and abstract types, can be marked with `{:extern}`. Marking a module with `{:extern}` indicates that the declarations diff --git a/docs/HowToFAQ/Errors-Parser.md b/docs/HowToFAQ/Errors-Parser.md index b26a49eb304..6dc031b068b 100644 --- a/docs/HowToFAQ/Errors-Parser.md +++ b/docs/HowToFAQ/Errors-Parser.md @@ -222,7 +222,7 @@ abstract module M { newtype T = int } module N refines M { newtype T = ... int } ``` -There are limitations on refining a newtype, namely that the base type cannot be changed. You can change an opaque type into a newtype, however. +There are limitations on refining a newtype, namely that the base type cannot be changed. You can change an abstract type into a newtype, however. ## **Error: formal cannot be declared 'ghost' in this context** {#p_output_of_function_not_ghost} @@ -359,7 +359,7 @@ type T(000) ``` [Type parameters](../DafnyRef/DafnyRef#sec-type-parameters), -indicated in parentheses after the type name, state properties of the otherwise uninterpreted or opaque type. +indicated in parentheses after the type name, state properties of the otherwise uninterpreted or abstract type. The currently defined type parameters are designated by `==` (equality-supporting), `0` (auto-initializable), `00` (non-empty), and `!new` (non-reference). ## **Error: extra comma or missing type characteristic: should be one of == or 0 or 00 or !new** {#p_missing_type_characteristic} @@ -370,7 +370,7 @@ type T(0,,0) ``` [Type parameters](../DafnyRef/DafnyRef#sec-type-parameters), -indicated in parentheses after the type name, state properties of the otherwise uninterpreted or opaque type. +indicated in parentheses after the type name, state properties of the otherwise uninterpreted or abstract type. The currently defined type parameters are designated by `==` (equality-supporting), `0` (auto-initializable), `00` (non-empty), and `!new` (non-reference). @@ -381,7 +381,7 @@ type T(X) ``` [Type parameters](../DafnyRef/DafnyRef#sec-type-parameters), -indicated in parentheses after the type name, state properties of the otherwise uninterpreted or opaque type. +indicated in parentheses after the type name, state properties of the otherwise uninterpreted or abstract type. The currently defined type parameters are designated by `==` (equality-supporting), `0` (auto-initializable), `00` (non-empty), and `!new` (non-reference). ## **Warning: the old keyword 'colemma' has been renamed to the keyword phrase 'greatest lemma'** {#p_deprecated_colemma} diff --git a/docs/HowToFAQ/FAQDefaultInitialValue.md b/docs/HowToFAQ/FAQDefaultInitialValue.md index 8b032b8e71e..892b0fd7335 100644 --- a/docs/HowToFAQ/FAQDefaultInitialValue.md +++ b/docs/HowToFAQ/FAQDefaultInitialValue.md @@ -10,7 +10,7 @@ How does one declare a type to have a "default" initial value, say a type tagged There is no general way to do this. Subset types and newtypes have [witness](../DafnyRef/DafnyRef/#sec-witness-clauses) clauses and types that are [auto-initializable](../DafnyRef/DafnyRef#sec-auto-init) have a default, but those rules do not apply to anonymous extern types. -Particularly for opaque types, there is not even a way to infer such a value. +Particularly for abstract types, there is not even a way to infer such a value. You can manually initialize like this: ```dafny diff --git a/docs/HowToFAQ/onepage.md b/docs/HowToFAQ/onepage.md index e7cc5b0123c..8decfe9ebf3 100644 --- a/docs/HowToFAQ/onepage.md +++ b/docs/HowToFAQ/onepage.md @@ -1427,7 +1427,7 @@ How does one declare a type to have a "default" initial value, say a type tagged There is no general way to do this. Subset types and newtypes have [witness](../DafnyRef/DafnyRef/#sec-witness-clauses) clauses and types that are [auto-initializable](../DafnyRef/DafnyRef#sec-auto-init) have a default, but those rules do not apply to anonymous extern types. -Particularly for opaque types, there is not even a way to infer such a value. +Particularly for abstract types, there is not even a way to infer such a value. You can manually initialize like this: ```dafny diff --git a/docs/OnlineTutorial/Modules.md b/docs/OnlineTutorial/Modules.md index 67da8a2e582..ce309cd7ba4 100644 --- a/docs/OnlineTutorial/Modules.md +++ b/docs/OnlineTutorial/Modules.md @@ -217,7 +217,7 @@ module Mod3 { } ``` -We may also use `export` sets to control which type definitions are available. All type declarations (i.e. `newtype`, `type`, `datatype`, etc.) can be exported as `provides` or `reveals`. In the former case, modules which `import` that type will treat it as an opaque type. +We may also use `export` sets to control which type definitions are available. All type declarations (i.e. `newtype`, `type`, `datatype`, etc.) can be exported as `provides` or `reveals`. In the former case, modules which `import` that type will treat it as an abstract type. ```dafny @@ -234,7 +234,7 @@ module Mod { } ``` -Once an `export` has been imported that `reveals` a previously opaque type, all existing uses of it are known to be the inner type. +Once an `export` has been imported that `reveals` a previously abstract type, all existing uses of it are known to be the inner type. ```dafny From 4057a8c54f75d8ddfe4471277899a1fe1e5db689 Mon Sep 17 00:00:00 2001 From: davidcok Date: Wed, 10 May 2023 16:44:13 -0400 Subject: [PATCH 3/9] Adding a news item --- docs/dev/news/3990.fix | 1 + 1 file changed, 1 insertion(+) create mode 100644 docs/dev/news/3990.fix diff --git a/docs/dev/news/3990.fix b/docs/dev/news/3990.fix new file mode 100644 index 00000000000..905317e7e1c --- /dev/null +++ b/docs/dev/news/3990.fix @@ -0,0 +1 @@ +The terminology 'opaque type' is changed to 'abstract type (for uninterpreted type declarations), to avoid ambiguity with used of the 'opaque' keyword and revealing declarations From 8358e29b362b3561af2aaf0e4930101323cb2809 Mon Sep 17 00:00:00 2001 From: davidcok Date: Wed, 10 May 2023 16:48:10 -0400 Subject: [PATCH 4/9] More instances of opaque type --- docs/DafnyRef/Types.md | 6 +++--- docs/DafnyRef/UserGuide.md | 2 +- docs/HowToFAQ/Errors-Compiler.md | 6 +++--- 3 files changed, 7 insertions(+), 7 deletions(-) diff --git a/docs/DafnyRef/Types.md b/docs/DafnyRef/Types.md index 13b94e6e534..3382ca01a0a 100644 --- a/docs/DafnyRef/Types.md +++ b/docs/DafnyRef/Types.md @@ -1366,7 +1366,7 @@ It is sometimes useful to know a type by several names or to treat a type abstractly. There are several mechanisms in Dafny to do this: * ([Section 5.6.1](#sec-synonym-type)) A typical _synonym type_, in which a type name is a synonym for another type -* ([Section 5.6.2](#sec-opaque-types)) An _abstract type_, in which a new type name is declared as an uninterpreted type +* ([Section 5.6.2](#sec-abstract-types)) An _abstract type_, in which a new type name is declared as an uninterpreted type * ([Section 5.6.3](#sec-subset-types)) A _subset type_, in which a new type name is given to a subset of the values of a given type * ([Section 0.0){#sec-newtypes)) A _newtype_, in which a subset type is declared, but with restrictions on converting to and from its base type @@ -1385,7 +1385,7 @@ type Y = G ``` declares `Y` to be a synonym for the type `G`. If the `= G` is omitted then the declaration just declares a name as an uninterpreted -_opaque_ type, as described in [Section 5.6.2](#sec-opaque-types). Such types may be +_opaque_ type, as described in [Section 5.6.2](#sec-abstract-types). Such types may be given a definition elsewhere in the Dafny program. Here, `T` is a @@ -1430,7 +1430,7 @@ const q: IntPair := IntPair(3,4) // Error In the declaration of `q`, `IntPair` is the name of a type, not the name of a function or datatype constructor. -### 5.6.2. Opaque types ([grammar](#g-type-definition)) {#sec-opaque-types} +### 5.6.2. Abstract types ([grammar](#g-type-definition)) {#sec-abstract-types} Examples: diff --git a/docs/DafnyRef/UserGuide.md b/docs/DafnyRef/UserGuide.md index 5485b9a8a07..69279b04e00 100644 --- a/docs/DafnyRef/UserGuide.md +++ b/docs/DafnyRef/UserGuide.md @@ -1321,7 +1321,7 @@ additional forms for the `{:extern}` attribute. The form `{:extern }` instructs `dafny` to compile references to most declarations using the name `s1` instead of the Dafny name. For [opaque -types](#sec-opaque-types), however, `s1` is sometimes used as a hint as +types](#sec-abstract-types), however, `s1` is sometimes used as a hint as to how to declare that type when compiling. This hint is interpreted differently by each compiler. diff --git a/docs/HowToFAQ/Errors-Compiler.md b/docs/HowToFAQ/Errors-Compiler.md index 09982535395..15b244011e4 100644 --- a/docs/HowToFAQ/Errors-Compiler.md +++ b/docs/HowToFAQ/Errors-Compiler.md @@ -36,18 +36,18 @@ so the program will need to be revised to avoid this feature; The latter is a (minor) bug in the in-tool documentation. Please report this error message and the part of the program provoking it to the Dafny team's [issue tracker](https://github.com/davidcok/dafny/issues). -## **Error: Opaque type ('_type_') with extern attribute requires a compile hint. Expected {:extern compile_type_hint}** +## **Error: Abstract type ('_type_') with extern attribute requires a compile hint. Expected {:extern compile_type_hint}** _Documentation of extern and compile hints is in progress._ -## **Error: Opaque type (_name_) cannot be compiled; perhaps make it a type synonym or use :extern.** +## **Error: Abstract type (_name_) cannot be compiled; perhaps make it a type synonym or use :extern.** ```dafny type T ``` -[Opaque types](../DafnyRef/DafnyRef#sec-opaque-types) are declared like `type T`. +[Abstract types](../DafnyRef/DafnyRef#sec-abstract-types) are declared like `type T`. They can be useful in programs where the particular characteristics of the type do not matter, such as in manipulating generic collections. Such programs can be verified, but in order to be compiled to something executable, From 396c81c7e5a975d705edc3a134f90cb132fd390d Mon Sep 17 00:00:00 2001 From: davidcok Date: Wed, 10 May 2023 17:16:38 -0400 Subject: [PATCH 5/9] More edits --- Test/dafny0/EqualityTypes.dfy.expect | 12 ++-- .../EqualityTypesModuleExports.dfy.expect | 6 +- Test/dafny0/Modules0.dfy.expect | 2 +- Test/dafny0/RefinementErrors.dfy.expect | 2 +- Test/dafny0/ResolutionErrors.dfy.expect | 10 ++-- Test/dafny0/TypeInstantiations.dfy.expect | 12 ++-- Test/git-issues/git-issue-1180a.dfy.expect | 56 +++++++++---------- Test/git-issues/git-issue-3461.dfy | 2 +- Test/git-issues/git-issue-MainE.dfy.expect | 4 +- 9 files changed, 53 insertions(+), 53 deletions(-) diff --git a/Test/dafny0/EqualityTypes.dfy.expect b/Test/dafny0/EqualityTypes.dfy.expect index 324ffc3bf85..c4921897c37 100644 --- a/Test/dafny0/EqualityTypes.dfy.expect +++ b/Test/dafny0/EqualityTypes.dfy.expect @@ -1,9 +1,9 @@ EqualityTypes.dfy(34,13): Error: a type declaration that requires equality support cannot be replaced by a codatatype -EqualityTypes.dfy(35,11): Error: type 'Y', which does not support equality, is used to refine an opaque type with equality support +EqualityTypes.dfy(35,11): Error: type 'Y', which does not support equality, is used to refine an abstract type with equality support EqualityTypes.dfy(40,11): Error: datatype 'X' is declared with a different number of type parameters (1 instead of 0) than the corresponding datatype in the module it refines EqualityTypes.dfy(41,8): Error: class 'Y' is declared with a different number of type parameters (1 instead of 0) than the corresponding class in the module it refines -EqualityTypes.dfy(45,11): Error: type 'X', which does not support equality, is used to refine an opaque type with equality support -EqualityTypes.dfy(46,11): Error: type 'Y', which does not support equality, is used to refine an opaque type with equality support +EqualityTypes.dfy(45,11): Error: type 'X', which does not support equality, is used to refine an abstract type with equality support +EqualityTypes.dfy(46,11): Error: type 'Y', which does not support equality, is used to refine an abstract type with equality support EqualityTypes.dfy(66,7): Error: == can only be applied to expressions of types that support equality (got Dt) EqualityTypes.dfy(85,9): Error: type parameter (T) passed to method M must support equality (got _T0) (perhaps try declaring type parameter '_T0' on line 81 as '_T0(==)', which says it can only be instantiated with a type that supports equality) EqualityTypes.dfy(109,7): Error: == can only be applied to expressions of types that support equality (got D) @@ -66,9 +66,9 @@ EqualityTypes.dfy(331,31): Error: set argument type must support equality (got S EqualityTypes.dfy(334,7): Error: == can only be applied to expressions of types that support equality (got seq int>) EqualityTypes.dfy(337,14): Error: in can only be applied to expressions of sequence types that support equality (got seq int>) EqualityTypes.dfy(340,16): Error: in can only be applied to expressions of sequence types that support equality (got seq int>) -EqualityTypes.dfy(359,11): Error: type parameter (A) passed to type JustOpaque must support equality (got ABC) (perhaps try declaring opaque type 'ABC' on line 354 as 'ABC(==)', which says it can only be instantiated with a type that supports equality) -EqualityTypes.dfy(360,11): Error: type parameter (A) passed to type Synonym must support equality (got ABC) (perhaps try declaring opaque type 'ABC' on line 354 as 'ABC(==)', which says it can only be instantiated with a type that supports equality) -EqualityTypes.dfy(361,11): Error: type parameter (A) passed to type Subset must support equality (got ABC) (perhaps try declaring opaque type 'ABC' on line 354 as 'ABC(==)', which says it can only be instantiated with a type that supports equality) +EqualityTypes.dfy(359,11): Error: type parameter (A) passed to type JustOpaque must support equality (got ABC) (perhaps try declaring abstract type 'ABC' on line 354 as 'ABC(==)', which says it can only be instantiated with a type that supports equality) +EqualityTypes.dfy(360,11): Error: type parameter (A) passed to type Synonym must support equality (got ABC) (perhaps try declaring abstract type 'ABC' on line 354 as 'ABC(==)', which says it can only be instantiated with a type that supports equality) +EqualityTypes.dfy(361,11): Error: type parameter (A) passed to type Subset must support equality (got ABC) (perhaps try declaring abstract type 'ABC' on line 354 as 'ABC(==)', which says it can only be instantiated with a type that supports equality) EqualityTypes.dfy(376,9): Error: == can only be applied to expressions of types that support equality (got List) EqualityTypes.dfy(378,9): Error: == can only be applied to expressions of types that support equality (got List) EqualityTypes.dfy(381,9): Error: == can only be applied to expressions of types that support equality (got List) diff --git a/Test/dafny0/EqualityTypesModuleExports.dfy.expect b/Test/dafny0/EqualityTypesModuleExports.dfy.expect index 56e9e49764f..0a68ba24c61 100644 --- a/Test/dafny0/EqualityTypesModuleExports.dfy.expect +++ b/Test/dafny0/EqualityTypesModuleExports.dfy.expect @@ -20,7 +20,7 @@ EqualityTypesModuleExports.dfy(121,11): Error: type parameter (A) passed to type EqualityTypesModuleExports.dfy(123,11): Error: type parameter (A) passed to type Subset2 must support equality (got M) (perhaps try declaring type parameter 'M' on line 94 as 'M(==)', which says it can only be instantiated with a type that supports equality) EqualityTypesModuleExports.dfy(133,11): Error: type parameter (A) passed to type Syn5 must support equality (got ListWithALittlExtra) EqualityTypesModuleExports.dfy(134,11): Error: type parameter (A) passed to type Syn5 must support equality (got Co2) -EqualityTypesModuleExports.dfy(135,11): Error: type parameter (A) passed to type Syn5 must support equality (got Opaque0) (perhaps try declaring opaque type 'Opaque0' on line 73 as 'Opaque0(==)', which says it can only be instantiated with a type that supports equality) +EqualityTypesModuleExports.dfy(135,11): Error: type parameter (A) passed to type Syn5 must support equality (got Opaque0) (perhaps try declaring abstract type 'Opaque0' on line 73 as 'Opaque0(==)', which says it can only be instantiated with a type that supports equality) EqualityTypesModuleExports.dfy(139,11): Error: type parameter (A) passed to type Syn5 must support equality (got Syn1 int>) EqualityTypesModuleExports.dfy(153,11): Error: type parameter (A) passed to type MyClass must support equality (got Noeq) EqualityTypesModuleExports.dfy(154,11): Error: type parameter (A) passed to type Dt must support equality (got Noeq) @@ -38,8 +38,8 @@ EqualityTypesModuleExports.dfy(188,22): Error: set argument type must support eq EqualityTypesModuleExports.dfy(189,24): Error: iset argument type must support equality (got A) (perhaps try declaring type parameter 'A' on line 189 as 'A(==)', which says it can only be instantiated with a type that supports equality) EqualityTypesModuleExports.dfy(195,11): Error: type parameter (A) passed to type MyClass must support equality (got Noeq) EqualityTypesModuleExports.dfy(191,7): Error: recursive constraint dependency involving a subset type: SubsetCo -> Co -> SubsetCo -EqualityTypesModuleExports.dfy(214,7): Error: type 'Opa', which does not support equality, is used to refine an opaque type with equality support -EqualityTypesModuleExports.dfy(230,12): Error: type parameter (A) passed to type S must support equality (got GGG.Opa') (perhaps try declaring opaque type 'Opa'' on line 208 as 'Opa'(==)', which says it can only be instantiated with a type that supports equality) +EqualityTypesModuleExports.dfy(214,7): Error: type 'Opa', which does not support equality, is used to refine an abstract type with equality support +EqualityTypesModuleExports.dfy(230,12): Error: type parameter (A) passed to type S must support equality (got GGG.Opa') (perhaps try declaring abstract type 'Opa'' on line 208 as 'Opa'(==)', which says it can only be instantiated with a type that supports equality) EqualityTypesModuleExports.dfy(231,12): Error: type parameter (A) passed to type S must support equality (got GGG.Syn') EqualityTypesModuleExports.dfy(232,12): Error: type parameter (A) passed to type S must support equality (got GGG.Sub') EqualityTypesModuleExports.dfy(249,7): Error: == can only be applied to expressions of types that support equality (got WWW0.XT) diff --git a/Test/dafny0/Modules0.dfy.expect b/Test/dafny0/Modules0.dfy.expect index 6584a1ad947..b527c9c0dfb 100644 --- a/Test/dafny0/Modules0.dfy.expect +++ b/Test/dafny0/Modules0.dfy.expect @@ -35,5 +35,5 @@ Modules0.dfy(323,13): Error: new can be applied only to class types (got Q_Imp.L Modules0.dfy(324,23): Error: member 'Create' does not exist in class 'Klassy' Modules0.dfy(324,10): Error: when allocating an object of type 'Klassy', one of its constructor methods must be called Modules0.dfy(318,13): Error: arguments must have comparable types (got Q_Imp.Node and Node) -Modules0.dfy(349,11): Error: a datatype declaration (T) in a refinement module can only refine a datatype declaration or replace an opaque type declaration +Modules0.dfy(349,11): Error: a datatype declaration (T) in a refinement module can only refine a datatype declaration or replace an abstract type declaration 35 resolution/type errors detected in Modules0.dfy diff --git a/Test/dafny0/RefinementErrors.dfy.expect b/Test/dafny0/RefinementErrors.dfy.expect index 5a87bbbf17c..4a43a60dacc 100644 --- a/Test/dafny0/RefinementErrors.dfy.expect +++ b/Test/dafny0/RefinementErrors.dfy.expect @@ -10,7 +10,7 @@ RefinementErrors.dfy(39,23): Error: the type of parameter 'z' is different from RefinementErrors.dfy(40,9): Error: there is a difference in name of parameter 3 ('k' versus 'b') of function F compared to corresponding function in the module it refines RefinementErrors.dfy(57,13): Error: a ghost function can be changed into a compiled function in a refining module only if the function has not yet been given a body: G RefinementErrors.dfy(94,10): Error: refinement method cannot assign to a field defined in parent module ('a') -RefinementErrors.dfy(114,7): Error: opaque type 'T' is declared with a different number of type parameters (3 instead of 2) than the corresponding opaque type in the module it refines +RefinementErrors.dfy(114,7): Error: abstract type 'T' is declared with a different number of type parameters (3 instead of 2) than the corresponding abstract type in the module it refines RefinementErrors.dfy(121,11): Error: type parameter 'B' is not allowed to change the requirement of supporting auto-initialization RefinementErrors.dfy(121,13): Error: type parameter 'C' is not allowed to change the requirement of being nonempty RefinementErrors.dfy(121,15): Error: type parameter 'D' is not allowed to change the requirement of supporting auto-initialization diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect index 76956707d1c..cdae25664b4 100644 --- a/Test/dafny0/ResolutionErrors.dfy.expect +++ b/Test/dafny0/ResolutionErrors.dfy.expect @@ -147,7 +147,7 @@ ResolutionErrors.dfy(1085,25): Error: unresolved identifier: x ResolutionErrors.dfy(1087,21): Error: unresolved identifier: x ResolutionErrors.dfy(1089,21): Error: unresolved identifier: x ResolutionErrors.dfy(1092,21): Error: unresolved identifier: x -ResolutionErrors.dfy(1099,35): Error: Wrong number of type arguments (2 instead of 1) passed to opaque type: P +ResolutionErrors.dfy(1099,35): Error: Wrong number of type arguments (2 instead of 1) passed to abstract type: P ResolutionErrors.dfy(1111,13): Error: Type or type parameter is not declared in this scope: BX (did you forget to qualify a name or declare a module import 'opened'? names in outer modules are not visible in nested modules) ResolutionErrors.dfy(1121,6): Error: RHS (of type P) not assignable to LHS (of type P) (non-variant type parameter would require bool = int) ResolutionErrors.dfy(1126,6): Error: RHS (of type P) not assignable to LHS (of type P) (non-variant type parameter would require B = A) @@ -277,7 +277,7 @@ ResolutionErrors.dfy(1891,15): Error: 'this' is not allowed in a 'static' contex ResolutionErrors.dfy(1893,16): Error: 'this' is not allowed in a 'static' context ResolutionErrors.dfy(1909,8): Error: return statement is not allowed before 'new;' in a constructor ResolutionErrors.dfy(1935,5): Error: type parameter (G) passed to method P must support auto-initialization (got F) (perhaps try declaring type parameter 'F' on line 1928 as 'F(0)', which says it can only be instantiated with a type that supports auto-initialization) -ResolutionErrors.dfy(1937,5): Error: type parameter (G) passed to method P must support auto-initialization (got Y) (perhaps try declaring opaque type 'Y' on line 1925 as 'Y(0)', which says it can only be instantiated with a type that supports auto-initialization) +ResolutionErrors.dfy(1937,5): Error: type parameter (G) passed to method P must support auto-initialization (got Y) (perhaps try declaring abstract type 'Y' on line 1925 as 'Y(0)', which says it can only be instantiated with a type that supports auto-initialization) ResolutionErrors.dfy(1974,5): Error: type parameter (G) passed to method P must support auto-initialization (got SixOrMore) ResolutionErrors.dfy(1975,5): Error: type parameter (G) passed to method P must support auto-initialization (got AnotherSixOrMore) ResolutionErrors.dfy(1976,5): Error: type parameter (G) passed to method P must support auto-initialization (got MySixOrMore) @@ -286,9 +286,9 @@ ResolutionErrors.dfy(1993,17): Error: type parameter (G) passed to method P must ResolutionErrors.dfy(1994,24): Error: type parameter (G) passed to method P must support auto-initialization (got SAnotherSixOrMore) ResolutionErrors.dfy(1995,19): Error: type parameter (G) passed to method P must support auto-initialization (got SMySixOrMore) ResolutionErrors.dfy(1996,16): Error: type parameter (G) passed to method P must support auto-initialization (got SUnclearA) -ResolutionErrors.dfy(2026,7): Error: type 'B2', which does not support auto-initialization, is used to refine an opaque type that expects auto-initialization -ResolutionErrors.dfy(2027,7): Error: type 'B3', which does not support auto-initialization, is used to refine an opaque type that expects auto-initialization -ResolutionErrors.dfy(2031,7): Error: type 'C3', which may be empty, is used to refine an opaque type expected to be nonempty +ResolutionErrors.dfy(2026,7): Error: type 'B2', which does not support auto-initialization, is used to refine an abstract type that expects auto-initialization +ResolutionErrors.dfy(2027,7): Error: type 'B3', which does not support auto-initialization, is used to refine an abstract type that expects auto-initialization +ResolutionErrors.dfy(2031,7): Error: type 'C3', which may be empty, is used to refine an abstract type expected to be nonempty ResolutionErrors.dfy(2051,7): Error: type declaration 'A1' is not allowed to change the requirement of supporting auto-initialization ResolutionErrors.dfy(2052,7): Error: type declaration 'A2' is not allowed to change the requirement of being nonempty ResolutionErrors.dfy(2053,7): Error: type declaration 'B0' is not allowed to change the requirement of supporting auto-initialization diff --git a/Test/dafny0/TypeInstantiations.dfy.expect b/Test/dafny0/TypeInstantiations.dfy.expect index 0d8bc1a79fc..ee469a723d7 100644 --- a/Test/dafny0/TypeInstantiations.dfy.expect +++ b/Test/dafny0/TypeInstantiations.dfy.expect @@ -10,12 +10,12 @@ TypeInstantiations.dfy(49,9): Error: type parameter 'U'' is not allowed to chang 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 -TypeInstantiations.dfy(55,7): Error: opaque type 'TP0' is declared with a different number of type parameters (1 instead of 0) than the corresponding opaque type in the module it refines -TypeInstantiations.dfy(56,7): Error: opaque type 'TP1' is declared with a different number of type parameters (0 instead of 1) than the corresponding opaque type in the module it refines -TypeInstantiations.dfy(57,15): Error: type parameters are not allowed to be renamed from the names given in the opaque type in the module being refined (expected 'Y1', found 'E1') -TypeInstantiations.dfy(34,11): Error: type 'C', which does not support equality, is used to refine an opaque type with equality support -TypeInstantiations.dfy(35,7): Error: type 'D', which does not support equality, is used to refine an opaque type with equality support -TypeInstantiations.dfy(48,7): Error: type 'N', which does not support equality, is used to refine an opaque type with equality support +TypeInstantiations.dfy(55,7): Error: abstract type 'TP0' is declared with a different number of type parameters (1 instead of 0) than the corresponding abstract type in the module it refines +TypeInstantiations.dfy(56,7): Error: abstract type 'TP1' is declared with a different number of type parameters (0 instead of 1) than the corresponding abstract type in the module it refines +TypeInstantiations.dfy(57,15): Error: type parameters are not allowed to be renamed from the names given in the abstract type in the module being refined (expected 'Y1', found 'E1') +TypeInstantiations.dfy(34,11): Error: type 'C', which does not support equality, is used to refine an abstract type with equality support +TypeInstantiations.dfy(35,7): Error: type 'D', which does not support equality, is used to refine an abstract type with equality support +TypeInstantiations.dfy(48,7): Error: type 'N', which does not support equality, is used to refine an abstract type with equality support TypeInstantiations.dfy(69,29): Error: RHS (of type List) not assignable to LHS (of type MyList.List) (non-variant type parameter would require real = int) TypeInstantiations.dfy(81,8): Error: the type of this variable is underspecified TypeInstantiations.dfy(82,8): Error: the type of this variable is underspecified diff --git a/Test/git-issues/git-issue-1180a.dfy.expect b/Test/git-issues/git-issue-1180a.dfy.expect index 51a7ee4a778..f68b46a6018 100644 --- a/Test/git-issues/git-issue-1180a.dfy.expect +++ b/Test/git-issues/git-issue-1180a.dfy.expect @@ -14,7 +14,7 @@ git-issue-1180a.dfy(23,10): Error: declaration 'Newtype' indicates refining (not git-issue-1180a.dfy(24,8): Error: declaration 'Class' indicates refining (notation `...`), but does not refine anything git-issue-1180a.dfy(25,8): Error: declaration 'Trait' indicates refining (notation `...`), but does not refine anything git-issue-1180a.dfy(23,10): Info: defaulting to 'int' for unspecified base type of 'Newtype' -git-issue-1180a.dfy(37,9): Error: opaque type 'Ty' is declared with a different number of type parameters (2 instead of 1) than the corresponding opaque type in the module it refines +git-issue-1180a.dfy(37,9): Error: abstract type 'Ty' is declared with a different number of type parameters (2 instead of 1) than the corresponding abstract type in the module it refines git-issue-1180a.dfy(38,15): Error: function 'F' is declared with a different number of type parameters (1 instead of 0) than the corresponding function in the module it refines git-issue-1180a.dfy(38,15): Error: the result type of function 'F' (Z) differs from the result type of the corresponding function in the module it refines (nat) git-issue-1180a.dfy(39,13): Error: method 'M' is declared with a different number of type parameters (1 instead of 0) than the corresponding method in the module it refines @@ -50,40 +50,40 @@ git-issue-1180a.dfy(74,15): Error: function 'F' is declared with a different num git-issue-1180a.dfy(74,15): Error: the result type of function 'F' (Z) differs from the result type of the corresponding function in the module it refines (nat) git-issue-1180a.dfy(75,13): Error: method 'M' is declared with a different number of type parameters (1 instead of 0) than the corresponding method in the module it refines git-issue-1180a.dfy(75,35): Error: the type of out-parameter 'r' is different from the type of the same out-parameter in the corresponding method in the module it refines ('Z' instead of 'nat') -git-issue-1180a.dfy(79,9): Error: a type synonym (Ty) cannot declare members, so it cannot refine an opaque type with members -git-issue-1180a.dfy(92,9): Error: an opaque type declaration (Ty) in a refining module cannot replace a more specific type declaration in the refinement base -git-issue-1180a.dfy(95,9): Error: an opaque type declaration (Ty) in a refining module cannot replace a more specific type declaration in the refinement base -git-issue-1180a.dfy(102,15): Error: a codatatype declaration (Ty) in a refinement module can only refine a codatatype declaration or replace an opaque type declaration -git-issue-1180a.dfy(105,12): Error: a newtype declaration (Ty) in a refinement module can only refine a newtype declaration or replace an opaque type declaration +git-issue-1180a.dfy(79,9): Error: a type synonym (Ty) cannot declare members, so it cannot refine an abstract type with members +git-issue-1180a.dfy(92,9): Error: an abstract type declaration (Ty) in a refining module cannot replace a more specific type declaration in the refinement base +git-issue-1180a.dfy(95,9): Error: an abstract type declaration (Ty) in a refining module cannot replace a more specific type declaration in the refinement base +git-issue-1180a.dfy(102,15): Error: a codatatype declaration (Ty) in a refinement module can only refine a codatatype declaration or replace an abstract type declaration +git-issue-1180a.dfy(105,12): Error: a newtype declaration (Ty) in a refinement module can only refine a newtype declaration or replace an abstract type declaration git-issue-1180a.dfy(105,12): Info: defaulting to 'int' for unspecified base type of 'Ty' -git-issue-1180a.dfy(108,10): Error: a class declaration (Ty) in a refinement module can only refine a class declaration or replace an opaque type declaration -git-issue-1180a.dfy(111,10): Error: a trait declaration (Ty) in a refinement module can only refine a trait declaration or replace an opaque type declaration +git-issue-1180a.dfy(108,10): Error: a class declaration (Ty) in a refinement module can only refine a class declaration or replace an abstract type declaration +git-issue-1180a.dfy(111,10): Error: a trait declaration (Ty) in a refinement module can only refine a trait declaration or replace an abstract type declaration git-issue-1180a.dfy(114,9): Error: a type synonym (Ty) is not allowed to replace a datatype from the refined module (A), even if it denotes the same type -git-issue-1180a.dfy(127,9): Error: an opaque type declaration (Ty) in a refining module cannot replace a more specific type declaration in the refinement base -git-issue-1180a.dfy(130,13): Error: a datatype declaration (Ty) in a refinement module can only refine a datatype declaration or replace an opaque type declaration -git-issue-1180a.dfy(137,12): Error: a newtype declaration (Ty) in a refinement module can only refine a newtype declaration or replace an opaque type declaration +git-issue-1180a.dfy(127,9): Error: an abstract type declaration (Ty) in a refining module cannot replace a more specific type declaration in the refinement base +git-issue-1180a.dfy(130,13): Error: a datatype declaration (Ty) in a refinement module can only refine a datatype declaration or replace an abstract type declaration +git-issue-1180a.dfy(137,12): Error: a newtype declaration (Ty) in a refinement module can only refine a newtype declaration or replace an abstract type declaration git-issue-1180a.dfy(137,12): Info: defaulting to 'int' for unspecified base type of 'Ty' -git-issue-1180a.dfy(140,10): Error: a class declaration (Ty) in a refinement module can only refine a class declaration or replace an opaque type declaration -git-issue-1180a.dfy(143,10): Error: a trait declaration (Ty) in a refinement module can only refine a trait declaration or replace an opaque type declaration +git-issue-1180a.dfy(140,10): Error: a class declaration (Ty) in a refinement module can only refine a class declaration or replace an abstract type declaration +git-issue-1180a.dfy(143,10): Error: a trait declaration (Ty) in a refinement module can only refine a trait declaration or replace an abstract type declaration git-issue-1180a.dfy(146,9): Error: a type synonym (Ty) is not allowed to replace a codatatype from the refined module (A), even if it denotes the same type -git-issue-1180a.dfy(159,9): Error: an opaque type declaration (Ty) in a refining module cannot replace a more specific type declaration in the refinement base -git-issue-1180a.dfy(162,13): Error: a datatype declaration (Ty) in a refinement module can only refine a datatype declaration or replace an opaque type declaration -git-issue-1180a.dfy(165,15): Error: a codatatype declaration (Ty) in a refinement module can only refine a codatatype declaration or replace an opaque type declaration -git-issue-1180a.dfy(169,10): Error: a class declaration (Ty) in a refinement module can only refine a class declaration or replace an opaque type declaration -git-issue-1180a.dfy(172,10): Error: a trait declaration (Ty) in a refinement module can only refine a trait declaration or replace an opaque type declaration +git-issue-1180a.dfy(159,9): Error: an abstract type declaration (Ty) in a refining module cannot replace a more specific type declaration in the refinement base +git-issue-1180a.dfy(162,13): Error: a datatype declaration (Ty) in a refinement module can only refine a datatype declaration or replace an abstract type declaration +git-issue-1180a.dfy(165,15): Error: a codatatype declaration (Ty) in a refinement module can only refine a codatatype declaration or replace an abstract type declaration +git-issue-1180a.dfy(169,10): Error: a class declaration (Ty) in a refinement module can only refine a class declaration or replace an abstract type declaration +git-issue-1180a.dfy(172,10): Error: a trait declaration (Ty) in a refinement module can only refine a trait declaration or replace an abstract type declaration git-issue-1180a.dfy(175,9): Error: a type synonym (Ty) is not allowed to replace a newtype from the refined module (A), even if it denotes the same type -git-issue-1180a.dfy(188,9): Error: an opaque type declaration (Ty) in a refining module cannot replace a more specific type declaration in the refinement base -git-issue-1180a.dfy(191,13): Error: a datatype declaration (Ty) in a refinement module can only refine a datatype declaration or replace an opaque type declaration -git-issue-1180a.dfy(194,15): Error: a codatatype declaration (Ty) in a refinement module can only refine a codatatype declaration or replace an opaque type declaration -git-issue-1180a.dfy(198,12): Error: a newtype declaration (Ty) in a refinement module can only refine a newtype declaration or replace an opaque type declaration +git-issue-1180a.dfy(188,9): Error: an abstract type declaration (Ty) in a refining module cannot replace a more specific type declaration in the refinement base +git-issue-1180a.dfy(191,13): Error: a datatype declaration (Ty) in a refinement module can only refine a datatype declaration or replace an abstract type declaration +git-issue-1180a.dfy(194,15): Error: a codatatype declaration (Ty) in a refinement module can only refine a codatatype declaration or replace an abstract type declaration +git-issue-1180a.dfy(198,12): Error: a newtype declaration (Ty) in a refinement module can only refine a newtype declaration or replace an abstract type declaration git-issue-1180a.dfy(198,12): Info: defaulting to 'int' for unspecified base type of 'Ty' -git-issue-1180a.dfy(201,10): Error: a trait declaration (Ty) in a refinement module can only refine a trait declaration or replace an opaque type declaration +git-issue-1180a.dfy(201,10): Error: a trait declaration (Ty) in a refinement module can only refine a trait declaration or replace an abstract type declaration git-issue-1180a.dfy(204,9): Error: a type synonym (Ty) is not allowed to replace a class from the refined module (A), even if it denotes the same type -git-issue-1180a.dfy(217,9): Error: an opaque type declaration (Ty) in a refining module cannot replace a more specific type declaration in the refinement base -git-issue-1180a.dfy(220,13): Error: a datatype declaration (Ty) in a refinement module can only refine a datatype declaration or replace an opaque type declaration -git-issue-1180a.dfy(223,15): Error: a codatatype declaration (Ty) in a refinement module can only refine a codatatype declaration or replace an opaque type declaration -git-issue-1180a.dfy(227,12): Error: a newtype declaration (Ty) in a refinement module can only refine a newtype declaration or replace an opaque type declaration +git-issue-1180a.dfy(217,9): Error: an abstract type declaration (Ty) in a refining module cannot replace a more specific type declaration in the refinement base +git-issue-1180a.dfy(220,13): Error: a datatype declaration (Ty) in a refinement module can only refine a datatype declaration or replace an abstract type declaration +git-issue-1180a.dfy(223,15): Error: a codatatype declaration (Ty) in a refinement module can only refine a codatatype declaration or replace an abstract type declaration +git-issue-1180a.dfy(227,12): Error: a newtype declaration (Ty) in a refinement module can only refine a newtype declaration or replace an abstract type declaration git-issue-1180a.dfy(227,12): Info: defaulting to 'int' for unspecified base type of 'Ty' -git-issue-1180a.dfy(230,10): Error: a class declaration (Ty) in a refinement module can only refine a class declaration or replace an opaque type declaration +git-issue-1180a.dfy(230,10): Error: a class declaration (Ty) in a refinement module can only refine a class declaration or replace an abstract type declaration git-issue-1180a.dfy(233,9): Error: a type synonym (Ty) is not allowed to replace a trait from the refined module (A), even if it denotes the same type 82 resolution/type errors detected in git-issue-1180a.dfy diff --git a/Test/git-issues/git-issue-3461.dfy b/Test/git-issues/git-issue-3461.dfy index 69903f02fa7..0407894b7ae 100644 --- a/Test/git-issues/git-issue-3461.dfy +++ b/Test/git-issues/git-issue-3461.dfy @@ -11,7 +11,7 @@ opaque predicate p() { true } // OK opaque class A {} // NO opaque datatype D = D // NO opaque newtype N = int // NO -abstract type P = i | i >= 0 // NO +opaque type P = i | i >= 0 // NO method z() { opaque var j: int // NO diff --git a/Test/git-issues/git-issue-MainE.dfy.expect b/Test/git-issues/git-issue-MainE.dfy.expect index 03763963b73..278da6e1377 100644 --- a/Test/git-issues/git-issue-MainE.dfy.expect +++ b/Test/git-issues/git-issue-MainE.dfy.expect @@ -40,7 +40,7 @@ Dafny program verifier did not attempt verification git-issue-MainE.dfy(60,9): Error: The method 'Tr.Instance' is not permitted as a main method (the method is not static and the enclosing type does not support auto-initialization). Dafny program verifier did not attempt verification -git-issue-MainE.dfy(79,16): Error: The method 'Opaque.Static' is not permitted as a main method (the enclosing type is an opaque type). +git-issue-MainE.dfy(79,16): Error: The method 'Opaque.Static' is not permitted as a main method (the enclosing type is an abstract type). Dafny program verifier did not attempt verification -git-issue-MainE.dfy(80,9): Error: The method 'Opaque.Instance' is not permitted as a main method (the enclosing type is an opaque type). +git-issue-MainE.dfy(80,9): Error: The method 'Opaque.Instance' is not permitted as a main method (the enclosing type is an abstract type). From 8692f987d07803f1800ea7df98ab349b024b8da0 Mon Sep 17 00:00:00 2001 From: davidcok Date: Wed, 10 May 2023 17:33:42 -0400 Subject: [PATCH 6/9] Renaming references in code --- Source/DafnyCore/AST/Cloner.cs | 8 ++-- Source/DafnyCore/AST/Grammar/Printer.cs | 4 +- Source/DafnyCore/AST/TopLevelDeclarations.cs | 8 ++-- Source/DafnyCore/AST/Types/Types.cs | 26 ++++++------ .../Compilers/CSharp/Compiler-Csharp.cs | 6 +-- .../Compilers/Cplusplus/Compiler-cpp.cs | 8 ++-- .../DafnyCore/Compilers/GoLang/Compiler-go.cs | 4 +- .../DafnyCore/Compilers/Java/Compiler-java.cs | 2 +- .../Compilers/JavaScript/Compiler-js.cs | 4 +- .../Compilers/Python/Compiler-python.cs | 4 +- .../DafnyCore/Compilers/SinglePassCompiler.cs | 8 ++-- Source/DafnyCore/Generic/Util.cs | 2 +- Source/DafnyCore/Resolver/BoundsDiscovery.cs | 2 +- .../NameResolutionAndTypeInference.cs | 6 +-- Source/DafnyCore/Resolver/Resolver.cs | 8 ++-- .../DafnyCore/Rewriters/InductionRewriter.cs | 2 +- .../Rewriters/RefinementTransformer.cs | 16 ++++---- Source/DafnyCore/Verifier/Translator.cs | 40 +++++++++---------- .../Language/SyntaxTreeVisitor.cs | 2 +- Source/DafnyPipeline.Test/DocstringTest.cs | 12 +++--- Test/git-issues/git-issue-2100.dfy | 4 +- 21 files changed, 88 insertions(+), 88 deletions(-) diff --git a/Source/DafnyCore/AST/Cloner.cs b/Source/DafnyCore/AST/Cloner.cs index 361aa3dcc29..7672e139c23 100644 --- a/Source/DafnyCore/AST/Cloner.cs +++ b/Source/DafnyCore/AST/Cloner.cs @@ -53,9 +53,9 @@ public virtual TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition m) Contract.Requires(d != null); Contract.Requires(m != null); - if (d is OpaqueTypeDecl) { - var dd = (OpaqueTypeDecl)d; - return new OpaqueTypeDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), m, CloneTPChar(dd.Characteristics), dd.TypeArgs.ConvertAll(CloneTypeParam), dd.Members.ConvertAll(d => CloneMember(d, false)), CloneAttributes(dd.Attributes), dd.IsRefining); + if (d is AbstractTypeDecl) { + var dd = (AbstractTypeDecl)d; + return new AbstractTypeDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), m, CloneTPChar(dd.Characteristics), dd.TypeArgs.ConvertAll(CloneTypeParam), dd.Members.ConvertAll(d => CloneMember(d, false)), CloneAttributes(dd.Attributes), dd.IsRefining); } else if (d is SubsetTypeDecl) { Contract.Assume(!(d is NonNullTypeDecl)); // don't clone the non-null type declaration; close the class, which will create a new non-null type declaration var dd = (SubsetTypeDecl)d; @@ -804,7 +804,7 @@ public override TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition m var tps = d.TypeArgs.ConvertAll(CloneTypeParam); var characteristics = TypeParameter.GetExplicitCharacteristics(d); var members = based is TopLevelDeclWithMembers tm ? tm.Members : new List(); - var otd = new OpaqueTypeDecl(Range(d.RangeToken), d.NameNode.Clone(this), m, characteristics, tps, members, CloneAttributes(d.Attributes), d.IsRefining); + var otd = new AbstractTypeDecl(Range(d.RangeToken), d.NameNode.Clone(this), m, characteristics, tps, members, CloneAttributes(d.Attributes), d.IsRefining); based = otd; if (d is ClassDecl) { reverseMap.Add(based, ((ClassDecl)d).NonNullTypeDecl); diff --git a/Source/DafnyCore/AST/Grammar/Printer.cs b/Source/DafnyCore/AST/Grammar/Printer.cs index d1b454aef7c..d0158b15d39 100644 --- a/Source/DafnyCore/AST/Grammar/Printer.cs +++ b/Source/DafnyCore/AST/Grammar/Printer.cs @@ -272,8 +272,8 @@ public void PrintTopLevelDecls(List decls, int indent, List true; } -public class OpaqueTypeDecl : TopLevelDeclWithMembers, TypeParameter.ParentType, RevealableTypeDecl, ICanFormat, IHasDocstring { +public class AbstractTypeDecl : TopLevelDeclWithMembers, TypeParameter.ParentType, RevealableTypeDecl, ICanFormat, IHasDocstring { public override string WhatKind { get { return "abstract type"; } } public override bool CanBeRevealed() { return true; } public readonly TypeParameter.TypeParameterCharacteristics Characteristics; @@ -2089,7 +2089,7 @@ public bool SupportsEquality { get { return Characteristics.EqualitySupport != TypeParameter.EqualitySupportValue.Unspecified; } } - public OpaqueTypeDecl(RangeToken rangeToken, Name name, ModuleDefinition module, TypeParameter.TypeParameterCharacteristics characteristics, List typeArgs, List members, Attributes attributes, bool isRefining) + public AbstractTypeDecl(RangeToken rangeToken, Name name, ModuleDefinition module, TypeParameter.TypeParameterCharacteristics characteristics, List typeArgs, List members, Attributes attributes, bool isRefining) : base(rangeToken, name, module, typeArgs, members, attributes, isRefining) { Contract.Requires(rangeToken != null); Contract.Requires(name != null); diff --git a/Source/DafnyCore/AST/Types/Types.cs b/Source/DafnyCore/AST/Types/Types.cs index 69f6ab045d1..9d7d00f680c 100644 --- a/Source/DafnyCore/AST/Types/Types.cs +++ b/Source/DafnyCore/AST/Types/Types.cs @@ -173,7 +173,7 @@ public Type NormalizeExpand(bool keepConstraints = false) { Contract.Assert(cl.NonNullTypeDecl != null); Contract.Assert(cl.NonNullTypeDecl.IsVisibleInScope(scope)); } else { - Contract.Assert(rtd is OpaqueTypeDecl); + Contract.Assert(rtd is AbstractTypeDecl); } } @@ -354,8 +354,8 @@ AutoInitInfo CharacteristicToAutoInitInfo(TypeParameter.TypeParameterCharacteris var udt = (UserDefinedType)t; var cl = udt.ResolvedClass; Contract.Assert(cl != null); - if (cl is OpaqueTypeDecl) { - var otd = (OpaqueTypeDecl)cl; + if (cl is AbstractTypeDecl) { + var otd = (AbstractTypeDecl)cl; return CharacteristicToAutoInitInfo(otd.Characteristics); } else if (cl is TypeParameter) { var tp = (TypeParameter)cl; @@ -814,13 +814,13 @@ public TypeParameter AsTypeParameter { return ct?.ResolvedClass as TypeParameter; } } - public bool IsOpaqueType { - get { return AsOpaqueType != null; } + public bool IsAbstractType { + get { return AsAbstractType != null; } } - public OpaqueTypeDecl AsOpaqueType { + public AbstractTypeDecl AsAbstractType { get { var udt = this.Normalize() as UserDefinedType; // note, it is important to use 'this.Normalize()' here, not 'this.NormalizeExpand()' - return udt?.ResolvedClass as OpaqueTypeDecl; + return udt?.ResolvedClass as AbstractTypeDecl; } } @@ -869,7 +869,7 @@ public OpaqueTypeDecl AsOpaqueType { public bool IsOrdered { get { var ct = NormalizeExpand(); - return !ct.IsTypeParameter && !ct.IsOpaqueType && !ct.IsInternalTypeSynonym && !ct.IsCoDatatype && !ct.IsArrowType && !ct.IsIMapType && !ct.IsISetType; + return !ct.IsTypeParameter && !ct.IsAbstractType && !ct.IsInternalTypeSynonym && !ct.IsCoDatatype && !ct.IsArrowType && !ct.IsIMapType && !ct.IsISetType; } } @@ -2371,7 +2371,7 @@ public UserDefinedType(TypeParameter tp) /// /// This constructor constructs a resolved type parameter (but shouldn't be called if "tp" denotes - /// the .TheType of an abstract type -- use the (OpaqueType_AsParameter, OpaqueTypeDecl, List(Type)) + /// the .TheType of an abstract type -- use the (AbstractType_AsParameter, AbstractTypeDecl, List(Type)) /// constructor for that). /// public UserDefinedType(IToken tok, TypeParameter tp) { @@ -2549,8 +2549,8 @@ public override bool SupportsEquality { } } else if (ResolvedClass is TypeParameter) { return ((TypeParameter)ResolvedClass).SupportsEquality; - } else if (ResolvedClass is OpaqueTypeDecl) { - return ((OpaqueTypeDecl)ResolvedClass).SupportsEquality; + } else if (ResolvedClass is AbstractTypeDecl) { + return ((AbstractTypeDecl)ResolvedClass).SupportsEquality; } Contract.Assume(false); // the SupportsEquality getter requires the Type to have been successfully resolved return true; @@ -2634,7 +2634,7 @@ public override bool ComputeMayInvolveReferences(ISet visitedDatat } else { return !typeParameter.Characteristics.ContainsNoReferenceTypes; } - } else if (ResolvedClass is OpaqueTypeDecl opaqueTypeDecl) { + } else if (ResolvedClass is AbstractTypeDecl opaqueTypeDecl) { return !opaqueTypeDecl.Characteristics.ContainsNoReferenceTypes; } Contract.Assume(false); // unexpected or not successfully resolved Type @@ -2769,7 +2769,7 @@ public static Family GetFamily(Type t) { return Family.ValueType; } else if (t.IsRefType) { return Family.Ref; - } else if (t.IsTypeParameter || t.IsOpaqueType || t.IsInternalTypeSynonym) { + } else if (t.IsTypeParameter || t.IsAbstractType || t.IsInternalTypeSynonym) { return Family.Opaque; } else if (t is TypeProxy) { return ((TypeProxy)t).family; diff --git a/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs b/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs index 101ee733b88..259f789c61f 100644 --- a/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs +++ b/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs @@ -47,8 +47,8 @@ public CsharpCompiler(DafnyOptions options, ErrorReporter reporter) : base(optio const string TypeDescriptorMethodName = "_TypeDescriptor"; string FormatDefaultTypeParameterValue(TopLevelDecl tp) { - Contract.Requires(tp is TypeParameter || tp is OpaqueTypeDecl); - if (tp is OpaqueTypeDecl) { + Contract.Requires(tp is TypeParameter || tp is AbstractTypeDecl); + if (tp is AbstractTypeDecl) { // This is unusual. Typically, the compiler never needs to compile an abstract type, but this abstract type // is apparently an :extern (or a compiler error has already been reported and we're just trying to get to // the end of compilation without crashing). It's difficult to say what the compiler could do in this situation, since @@ -1511,7 +1511,7 @@ protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree } else { return FormatDefaultTypeParameterValue(tp); } - } else if (cl is OpaqueTypeDecl opaque) { + } else if (cl is AbstractTypeDecl opaque) { return FormatDefaultTypeParameterValue(opaque); } else if (cl is NewtypeDecl) { var td = (NewtypeDecl)cl; diff --git a/Source/DafnyCore/Compilers/Cplusplus/Compiler-cpp.cs b/Source/DafnyCore/Compilers/Cplusplus/Compiler-cpp.cs index d9c5c28863b..f96300010e4 100644 --- a/Source/DafnyCore/Compilers/Cplusplus/Compiler-cpp.cs +++ b/Source/DafnyCore/Compilers/Cplusplus/Compiler-cpp.cs @@ -958,7 +958,7 @@ protected string TypeName(Type type, ConcreteSyntaxTree wr, IToken tok, MemberDe if (cl != null && Attributes.ContainsBool(cl.Attributes, "handle", ref isHandle) && isHandle) { return "ulong"; } - if (class_name || xType.IsTypeParameter || xType.IsOpaqueType || xType.IsDatatype) { // Don't add pointer decorations to class names or type parameters + if (class_name || xType.IsTypeParameter || xType.IsAbstractType || xType.IsDatatype) { // Don't add pointer decorations to class names or type parameters return IdProtect(s) + ActualTypeArgs(xType.TypeArgs); } else { return TypeName_UDT(s, udt, wr, udt.tok); @@ -1034,8 +1034,8 @@ protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree var udt = (UserDefinedType)xType; var cl = udt.ResolvedClass; Contract.Assert(cl != null); - if (cl is TypeParameter || cl is OpaqueTypeDecl) { - var hasCompiledValue = (cl is TypeParameter ? ((TypeParameter)cl).Characteristics : ((OpaqueTypeDecl)cl).Characteristics).HasCompiledValue; + if (cl is TypeParameter || cl is AbstractTypeDecl) { + var hasCompiledValue = (cl is TypeParameter ? ((TypeParameter)cl).Characteristics : ((AbstractTypeDecl)cl).Characteristics).HasCompiledValue; if (Attributes.Contains(udt.ResolvedClass.Attributes, "extern")) { // Assume the external definition includes a default value return String.Format("{1}::get_{0}_default()", IdProtect(udt.Name), udt.ResolvedClass.EnclosingModuleDefinition.GetCompileName(Options)); @@ -1133,7 +1133,7 @@ protected override string TypeName_Companion(Type type, ConcreteSyntaxTree wr, I } // ----- Declarations ------------------------------------------------------------- - protected override void DeclareExternType(OpaqueTypeDecl d, Expression compileTypeHint, ConcreteSyntaxTree wr) { + protected override void DeclareExternType(AbstractTypeDecl d, Expression compileTypeHint, ConcreteSyntaxTree wr) { if (compileTypeHint.AsStringLiteral() == "struct") { modDeclWr.WriteLine("// Extern declaration of {1}\n{0} struct {1};", DeclareTemplate(d.TypeArgs), d.Name); } else { diff --git a/Source/DafnyCore/Compilers/GoLang/Compiler-go.cs b/Source/DafnyCore/Compilers/GoLang/Compiler-go.cs index fdbf2d58294..a71b88efda8 100644 --- a/Source/DafnyCore/Compilers/GoLang/Compiler-go.cs +++ b/Source/DafnyCore/Compilers/GoLang/Compiler-go.cs @@ -31,7 +31,7 @@ public GoCompiler(DafnyOptions options, ErrorReporter reporter) : base(options, }; string FormatDefaultTypeParameterValue(TopLevelDecl tp) { - Contract.Requires(tp is TypeParameter || tp is OpaqueTypeDecl); + Contract.Requires(tp is TypeParameter || tp is AbstractTypeDecl); return $"_default_{tp.GetCompileName(Options)}"; } @@ -1516,7 +1516,7 @@ string nil() { } else { return FormatDefaultTypeParameterValue(tp); } - } else if (cl is OpaqueTypeDecl opaque) { + } else if (cl is AbstractTypeDecl opaque) { return FormatDefaultTypeParameterValue(opaque); } else if (cl is NewtypeDecl) { var td = (NewtypeDecl)cl; diff --git a/Source/DafnyCore/Compilers/Java/Compiler-java.cs b/Source/DafnyCore/Compilers/Java/Compiler-java.cs index 6cf5c00d740..f1bd3fc742b 100644 --- a/Source/DafnyCore/Compilers/Java/Compiler-java.cs +++ b/Source/DafnyCore/Compilers/Java/Compiler-java.cs @@ -3073,7 +3073,7 @@ protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree } else { return FormatDefaultTypeParameterValue(tp); } - } else if (cl is OpaqueTypeDecl opaque) { + } else if (cl is AbstractTypeDecl opaque) { return FormatDefaultTypeParameterValueName(opaque.GetCompileName(Options)); } else if (cl is NewtypeDecl) { var td = (NewtypeDecl)cl; diff --git a/Source/DafnyCore/Compilers/JavaScript/Compiler-js.cs b/Source/DafnyCore/Compilers/JavaScript/Compiler-js.cs index 810eb3947fa..d538cbd0d94 100644 --- a/Source/DafnyCore/Compilers/JavaScript/Compiler-js.cs +++ b/Source/DafnyCore/Compilers/JavaScript/Compiler-js.cs @@ -34,7 +34,7 @@ public JavaScriptCompiler(DafnyOptions options, ErrorReporter reporter) : base(o const string DafnyMapClass = "_dafny.Map"; string FormatDefaultTypeParameterValue(TopLevelDecl tp) { - Contract.Requires(tp is TypeParameter || tp is OpaqueTypeDecl); + Contract.Requires(tp is TypeParameter || tp is AbstractTypeDecl); return $"_default_{tp.GetCompileName(Options)}"; } @@ -927,7 +927,7 @@ protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree } else { return FormatDefaultTypeParameterValue((TypeParameter)udt.ResolvedClass); } - } else if (cl is OpaqueTypeDecl opaque) { + } else if (cl is AbstractTypeDecl opaque) { return FormatDefaultTypeParameterValue(opaque); } else if (cl is NewtypeDecl) { var td = (NewtypeDecl)cl; diff --git a/Source/DafnyCore/Compilers/Python/Compiler-python.cs b/Source/DafnyCore/Compilers/Python/Compiler-python.cs index 4b28d452cb7..675f29886b0 100644 --- a/Source/DafnyCore/Compilers/Python/Compiler-python.cs +++ b/Source/DafnyCore/Compilers/Python/Compiler-python.cs @@ -48,7 +48,7 @@ public PythonCompiler(DafnyOptions options, ErrorReporter reporter) : base(optio const string DafnyMapClass = $"{DafnyRuntimeModule}.Map"; const string DafnyDefaults = $"{DafnyRuntimeModule}.defaults"; string FormatDefaultTypeParameterValue(TopLevelDecl tp) { - Contract.Requires(tp is TypeParameter or OpaqueTypeDecl); + Contract.Requires(tp is TypeParameter or AbstractTypeDecl); return $"default_{tp.GetCompileName(Options)}"; } protected override string StmtTerminator { get => ""; } @@ -730,7 +730,7 @@ protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree ? $"{TypeDescriptor(udt, wr, tok)}()" : $"{FormatDefaultTypeParameterValue(tp)}()"; - case OpaqueTypeDecl opaque: + case AbstractTypeDecl opaque: return FormatDefaultTypeParameterValue(opaque); case ClassDecl: diff --git a/Source/DafnyCore/Compilers/SinglePassCompiler.cs b/Source/DafnyCore/Compilers/SinglePassCompiler.cs index 71c37e25795..c7259e0a008 100644 --- a/Source/DafnyCore/Compilers/SinglePassCompiler.cs +++ b/Source/DafnyCore/Compilers/SinglePassCompiler.cs @@ -1323,7 +1323,7 @@ protected abstract void EmitSingleValueGenerator(Expression e, bool inLetExprBod ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts); protected virtual void FinishModule() { } - protected virtual void DeclareExternType(OpaqueTypeDecl d, Expression compileTypeHint, ConcreteSyntaxTree wr) { } + protected virtual void DeclareExternType(AbstractTypeDecl d, Expression compileTypeHint, ConcreteSyntaxTree wr) { } protected virtual void OrganizeModules(Program program, out List modules) { modules = program.CompileModules; @@ -1364,8 +1364,8 @@ public void Compile(Program program, ConcreteSyntaxTree wrx) { continue; } var newLineWriter = wr.Fork(); - if (d is OpaqueTypeDecl) { - var at = (OpaqueTypeDecl)d; + if (d is AbstractTypeDecl) { + var at = (AbstractTypeDecl)d; bool externP = Attributes.Contains(at.Attributes, "extern"); if (externP) { var exprs = Attributes.FindExpressions(at.Attributes, "extern"); @@ -1730,7 +1730,7 @@ public static bool IsPermittedAsMain(Program program, Method m, out String reaso reason = "the method has type parameters"; return false; } - if (cl is OpaqueTypeDecl) { + if (cl is AbstractTypeDecl) { reason = "the enclosing type is an abstract type"; return false; } diff --git a/Source/DafnyCore/Generic/Util.cs b/Source/DafnyCore/Generic/Util.cs index d366bacfdae..05ebb1c5e47 100644 --- a/Source/DafnyCore/Generic/Util.cs +++ b/Source/DafnyCore/Generic/Util.cs @@ -775,7 +775,7 @@ public bool Traverse(TopLevelDecl topd) { var d = topd is ClassDecl classDecl && classDecl.NonNullTypeDecl != null ? classDecl.NonNullTypeDecl : topd; if (d is TopLevelDeclWithMembers tdm) { - // ClassDecl, DatatypeDecl, OpaqueTypeDecl, NewtypeDecl + // ClassDecl, DatatypeDecl, AbstractTypeDecl, NewtypeDecl if (tdm.Members.Any(memberDecl => Traverse(memberDecl, "Members", tdm))) { return true; } diff --git a/Source/DafnyCore/Resolver/BoundsDiscovery.cs b/Source/DafnyCore/Resolver/BoundsDiscovery.cs index b5088d937d2..9113f8ceffd 100644 --- a/Source/DafnyCore/Resolver/BoundsDiscovery.cs +++ b/Source/DafnyCore/Resolver/BoundsDiscovery.cs @@ -201,7 +201,7 @@ protected override bool VisitOneExpression(Expression expr, BoundsDiscoveryConte var message = $"a {e.WhatKind} involved in a {context.Kind} {how}is not allowed to depend on the set of allocated references," + $" but values of '{bv.Name}' (of type '{bv.Type}') may contain references"; - if (bv.Type.IsTypeParameter || bv.Type.IsOpaqueType) { + if (bv.Type.IsTypeParameter || bv.Type.IsAbstractType) { message += $" (perhaps declare its type as '{bv.Type}(!new)')"; } message += " (see documentation for 'older' parameters)"; diff --git a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference.cs b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference.cs index e5c6bd3f360..f9ebb9502b2 100644 --- a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference.cs +++ b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference.cs @@ -1354,7 +1354,7 @@ void DetermineRootLeaf(Type t, out bool isRoot, out bool isLeaf, out bool headIs headIsRoot = false; headIsLeaf = false; } else if (cl is ClassDecl) { headIsRoot = false; headIsLeaf = true; - } else if (cl is OpaqueTypeDecl) { + } else if (cl is AbstractTypeDecl) { headIsRoot = true; headIsLeaf = true; } else if (cl is InternalTypeSynonymDecl) { Contract.Assert(object.ReferenceEquals(t, t.NormalizeExpand())); // should be opaque in scope @@ -2142,7 +2142,7 @@ public bool Confirm(Resolver resolver, bool fullstrength, out bool convertedInto return false; // not enough information } } - if (moreExactThis.TreatTypeParamAsWild && (t.IsTypeParameter || u.IsTypeParameter || t.IsOpaqueType || u.IsOpaqueType)) { + if (moreExactThis.TreatTypeParamAsWild && (t.IsTypeParameter || u.IsTypeParameter || t.IsAbstractType || u.IsAbstractType)) { return true; } else if (!moreExactThis.AllowSuperSub) { resolver.ConstrainSubtypeRelation_Equal(t, u, errorMsg); @@ -4816,7 +4816,7 @@ public ResolveTypeReturn ResolveTypeLenient(IToken tok, Type type, ResolutionCon reporter.Error(MessageSource.Resolver, t.tok, "expected type"); } else if (r.Type is Resolver_IdentifierExpr.ResolverType_Type) { var d = r.Decl; - if (d is OpaqueTypeDecl) { + if (d is AbstractTypeDecl) { // resolve like a type parameter, and it may have type parameters if it's an abstract type t.ResolvedClass = d; // Store the decl, so the compiler will generate the fully qualified name } else if (d is RedirectingTypeDecl) { diff --git a/Source/DafnyCore/Resolver/Resolver.cs b/Source/DafnyCore/Resolver/Resolver.cs index 54b978be97e..3535cc28408 100644 --- a/Source/DafnyCore/Resolver/Resolver.cs +++ b/Source/DafnyCore/Resolver/Resolver.cs @@ -1744,7 +1744,7 @@ ModuleSignature RegisterTopLevelDecls(ModuleDefinition moduleDef, bool useImport // nothing to do } else if (d is TypeSynonymDecl) { // nothing more to register - } else if (d is NewtypeDecl || d is OpaqueTypeDecl) { + } else if (d is NewtypeDecl || d is AbstractTypeDecl) { var cl = (TopLevelDeclWithMembers)d; // register the names of the type members var members = new Dictionary(); @@ -4567,7 +4567,7 @@ bool CheckCharacteristics(TypeParameter.TypeParameterCharacteristics formal, Typ return false; } var cl = (actual.Normalize() as UserDefinedType)?.ResolvedClass; - var tp = (TopLevelDecl)(cl as TypeParameter) ?? cl as OpaqueTypeDecl; + var tp = (TopLevelDecl)(cl as TypeParameter) ?? cl as AbstractTypeDecl; if (formal.HasCompiledValue && (inGhostContext ? !actual.IsNonempty : !actual.HasCompilableValue)) { whatIsWrong = "auto-initialization"; hint = tp == null ? "" : @@ -4594,7 +4594,7 @@ bool CheckCharacteristics(TypeParameter.TypeParameterCharacteristics formal, Typ string TypeEqualityErrorMessageHint(Type argType) { Contract.Requires(argType != null); var cl = (argType.Normalize() as UserDefinedType)?.ResolvedClass; - var tp = (TopLevelDecl)(cl as TypeParameter) ?? cl as OpaqueTypeDecl; + var tp = (TopLevelDecl)(cl as TypeParameter) ?? cl as AbstractTypeDecl; if (tp != null) { return string.Format(" (perhaps try declaring {2} '{0}' on line {1} as '{0}(==)', which says it can only be instantiated with a type that supports equality)", tp.Name, tp.tok.line, tp.WhatKind); } @@ -5413,7 +5413,7 @@ bool CheckCanBeConstructed(Type type, ISet typeParametersUsed) { // treat a type parameter like a ground type typeParametersUsed.Add((TypeParameter)cl); return true; - } else if (cl is OpaqueTypeDecl) { + } else if (cl is AbstractTypeDecl) { // an opaque is like a ground type return true; } else if (cl is InternalTypeSynonymDecl) { diff --git a/Source/DafnyCore/Rewriters/InductionRewriter.cs b/Source/DafnyCore/Rewriters/InductionRewriter.cs index 18e708da24a..6eed358b7c9 100644 --- a/Source/DafnyCore/Rewriters/InductionRewriter.cs +++ b/Source/DafnyCore/Rewriters/InductionRewriter.cs @@ -170,7 +170,7 @@ void ComputeInductionVariables(IToken tok, List boundVars, Lis } foreach (IVariable n in boundVars) { - if (!(n.Type.IsTypeParameter || n.Type.IsOpaqueType || n.Type.IsInternalTypeSynonym) && (args != null || + if (!(n.Type.IsTypeParameter || n.Type.IsAbstractType || n.Type.IsInternalTypeSynonym) && (args != null || searchExprs.Exists(expr => InductionHeuristic.VarOccursInArgumentToRecursiveFunction(Reporter.Options, expr, n)))) { inductionVariables.Add(new IdentifierExpr(n.Tok, n)); } diff --git a/Source/DafnyCore/Rewriters/RefinementTransformer.cs b/Source/DafnyCore/Rewriters/RefinementTransformer.cs index 5733909aa3c..a39c52890d5 100644 --- a/Source/DafnyCore/Rewriters/RefinementTransformer.cs +++ b/Source/DafnyCore/Rewriters/RefinementTransformer.cs @@ -241,7 +241,7 @@ void PreResolveWorker(ModuleDefinition m) { m.TopLevelDecls.Add(refinementCloner.CloneDeclaration(d, m)); } else { var nw = m.TopLevelDecls[index]; - if (d.Name == "_default" || nw.IsRefining || d is OpaqueTypeDecl) { + if (d.Name == "_default" || nw.IsRefining || d is AbstractTypeDecl) { MergeTopLevelDecls(m, nw, d, index); } else if (nw is TypeSynonymDecl) { var msg = $"a type synonym ({nw.Name}) is not allowed to replace a {d.WhatKind} from the refined module ({m.RefinementQId}), even if it denotes the same type"; @@ -321,18 +321,18 @@ private void MergeTopLevelDecls(ModuleDefinition m, TopLevelDecl nw, TopLevelDec Reporter.Error(MessageSource.RefinementTransformer, nw.tok, "a module ({0}) can only be replaced by a refinement of the original module", d.Name); } } - } else if (d is OpaqueTypeDecl) { + } else if (d is AbstractTypeDecl) { if (nw is ModuleDecl) { Reporter.Error(MessageSource.RefinementTransformer, nw, "a module ({0}) must refine another module", nw.Name); } else { - var od = (OpaqueTypeDecl)d; - if (nw is OpaqueTypeDecl) { - if (od.SupportsEquality != ((OpaqueTypeDecl)nw).SupportsEquality) { + var od = (AbstractTypeDecl)d; + if (nw is AbstractTypeDecl) { + if (od.SupportsEquality != ((AbstractTypeDecl)nw).SupportsEquality) { Reporter.Error(MessageSource.RefinementTransformer, nw, "type declaration '{0}' is not allowed to change the requirement of supporting equality", nw.Name); } - if (od.Characteristics.HasCompiledValue != ((OpaqueTypeDecl)nw).Characteristics.HasCompiledValue) { + if (od.Characteristics.HasCompiledValue != ((AbstractTypeDecl)nw).Characteristics.HasCompiledValue) { Reporter.Error(MessageSource.RefinementTransformer, nw.tok, "type declaration '{0}' is not allowed to change the requirement of supporting auto-initialization", nw.Name); - } else if (od.Characteristics.IsNonempty != ((OpaqueTypeDecl)nw).Characteristics.IsNonempty) { + } else if (od.Characteristics.IsNonempty != ((AbstractTypeDecl)nw).Characteristics.IsNonempty) { Reporter.Error(MessageSource.RefinementTransformer, nw.tok, "type declaration '{0}' is not allowed to change the requirement of being nonempty", nw.Name); } } else { @@ -383,7 +383,7 @@ private void MergeTopLevelDecls(ModuleDefinition m, TopLevelDecl nw, TopLevelDec CheckAgreement_TypeParameters(nw.tok, d.TypeArgs, nw.TypeArgs, nw.Name, "type", false); } } - } else if (nw is OpaqueTypeDecl) { + } else if (nw is AbstractTypeDecl) { Reporter.Error(MessageSource.RefinementTransformer, nw, "an abstract type declaration ({0}) in a refining module cannot replace a more specific type declaration in the refinement base", nw.Name); } else if ((d is IndDatatypeDecl && nw is IndDatatypeDecl) || (d is CoDatatypeDecl && nw is CoDatatypeDecl)) { diff --git a/Source/DafnyCore/Verifier/Translator.cs b/Source/DafnyCore/Verifier/Translator.cs index 1084128c590..f1b236093ca 100644 --- a/Source/DafnyCore/Verifier/Translator.cs +++ b/Source/DafnyCore/Verifier/Translator.cs @@ -755,8 +755,8 @@ private Bpl.Program DoTranslation(Program p, ModuleDefinition forModule) { foreach (TopLevelDecl d in program.BuiltIns.SystemModule.TopLevelDecls) { currentDeclaration = d; - if (d is OpaqueTypeDecl) { - var dd = (OpaqueTypeDecl)d; + if (d is AbstractTypeDecl) { + var dd = (AbstractTypeDecl)d; AddTypeDecl(dd); AddClassMembers(dd, true, true); } else if (d is NewtypeDecl) { @@ -796,8 +796,8 @@ private Bpl.Program DoTranslation(Program p, ModuleDefinition forModule) { foreach (ModuleDefinition m in mods) { foreach (TopLevelDecl d in m.TopLevelDecls.FindAll(VisibleInScope)) { currentDeclaration = d; - if (d is OpaqueTypeDecl) { - var dd = (OpaqueTypeDecl)d; + if (d is AbstractTypeDecl) { + var dd = (AbstractTypeDecl)d; AddTypeDecl(dd); AddClassMembers(dd, true, true); } else if (d is ModuleDecl) { @@ -1212,7 +1212,7 @@ void AddTypeDecl_Aux(IToken tok, string nm, List typeArgs, TypePa abstractTypes.Add(nm); } - void AddTypeDecl(OpaqueTypeDecl td) { + void AddTypeDecl(AbstractTypeDecl td) { Contract.Requires(td != null); AddTypeDecl_Aux(td.tok, nameTypeParam(td), td.TypeArgs, td.Characteristics); } @@ -4387,7 +4387,7 @@ void AddWellformednessCheck(Function f) { { var args = new List(); foreach (var p in GetTypeParams(f)) { - args.Add(trTypeParamOrOpaqueType(p)); + args.Add(trTypeParamOrAbstractType(p)); } if (f.IsFuelAware()) { args.Add(etran.layerInterCluster.GetFunctionFuel(f)); @@ -4430,7 +4430,7 @@ void AddWellformednessCheck(Function f) { var funcID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullSanitizedName, TrType(f.ResultType))); var args = new List(); foreach (var p in GetTypeParams(f)) { - args.Add(trTypeParamOrOpaqueType(p)); + args.Add(trTypeParamOrAbstractType(p)); } if (f.IsFuelAware()) { args.Add(etran.layerInterCluster.GetFunctionFuel(f)); @@ -7165,7 +7165,7 @@ Bpl.Type TrType(Type type) { return Bpl.Type.Int; } else if (type is ArrowType) { return predef.HandleType; - } else if (type.IsTypeParameter || type.IsOpaqueType) { + } else if (type.IsTypeParameter || type.IsAbstractType) { return predef.BoxType; } else if (type.IsInternalTypeSynonym) { return predef.BoxType; @@ -7271,7 +7271,7 @@ public static bool ModeledAsBoxType(Type t) { // unresolved proxy return false; } - var res = t.IsTypeParameter || t.IsOpaqueType || t.IsInternalTypeSynonym; + var res = t.IsTypeParameter || t.IsAbstractType || t.IsInternalTypeSynonym; Contract.Assert(t.IsArrowType ? !res : true); return res; } @@ -7756,7 +7756,7 @@ Expression Zero(IToken tok, Type typ) { } else if (typ is ArrowType) { // TODO: do better than just returning null return null; - } else if (typ.IsOpaqueType || typ.IsInternalTypeSynonym) { + } else if (typ.IsAbstractType || typ.IsInternalTypeSynonym) { return null; } else { Contract.Assume(false); // unexpected type @@ -8058,7 +8058,7 @@ bool CompatibleDecreasesTypes(Type t, Type u) { } else if (t is BigOrdinalType) { return u is BigOrdinalType; } else { - Contract.Assert(t.IsTypeParameter || t.IsOpaqueType || t.IsInternalTypeSynonym); + Contract.Assert(t.IsTypeParameter || t.IsAbstractType || t.IsInternalTypeSynonym); return false; // don't consider any type parameters to be the same (since we have no comparison function for them anyway) } } @@ -8192,7 +8192,7 @@ void ComputeLessEq(IToken tok, Type ty0, Type ty1, Bpl.Expr e0, Bpl.Expr e1, out less = FunctionCall(tok, "ORD#Less", Bpl.Type.Bool, e0, e1); atmost = BplOr(eq, less); - } else if (ty0.IsTypeParameter || ty0.IsOpaqueType) { + } else if (ty0.IsTypeParameter || ty0.IsAbstractType) { eq = Bpl.Expr.Eq(e0, e1); less = Bpl.Expr.False; atmost = BplOr(less, eq); @@ -8247,9 +8247,9 @@ Bpl.Expr TypeToTy(Type type) { type = type.NormalizeExpandKeepConstraints(); - if (type.IsTypeParameter || type.IsOpaqueType) { + if (type.IsTypeParameter || type.IsAbstractType) { var udt = (UserDefinedType)type; - return trTypeParamOrOpaqueType(udt.ResolvedClass, udt.TypeArgs); + return trTypeParamOrAbstractType(udt.ResolvedClass, udt.TypeArgs); } else if (type is UserDefinedType) { // Classes, (co-)datatypes, newtypes, subset types, ... var args = type.TypeArgs.ConvertAll(TypeToTy); @@ -8280,14 +8280,14 @@ Bpl.Expr TypeToTy(Type type) { } else if (type is BigOrdinalType) { return new Bpl.IdentifierExpr(Token.NoToken, "TORDINAL", predef.Ty); } else if (type is ParamTypeProxy) { - return trTypeParamOrOpaqueType(((ParamTypeProxy)type).orig); + return trTypeParamOrAbstractType(((ParamTypeProxy)type).orig); } else { Contract.Assert(false); throw new cce.UnreachableException(); // unexpected type } } static string nameTypeParam(TopLevelDecl x) { - Contract.Requires(x is TypeParameter || x is OpaqueTypeDecl); + Contract.Requires(x is TypeParameter || x is AbstractTypeDecl); if (x is TypeParameter tp && tp.Parent != null) { return tp.Parent.FullName + "$" + x.Name; } else { @@ -8296,17 +8296,17 @@ static string nameTypeParam(TopLevelDecl x) { } } - Bpl.Expr trTypeParamOrOpaqueType(TopLevelDecl x, List/*?*/ tyArguments = null) { - Contract.Requires(x is TypeParameter || x is OpaqueTypeDecl); + Bpl.Expr trTypeParamOrAbstractType(TopLevelDecl x, List/*?*/ tyArguments = null) { + Contract.Requires(x is TypeParameter || x is AbstractTypeDecl); Contract.Requires(!(x is TypeParameter) || tyArguments == null || tyArguments.Count == 0); - Contract.Requires(!(x is OpaqueTypeDecl) || tyArguments != null); + Contract.Requires(!(x is AbstractTypeDecl) || tyArguments != null); if (x is TypeParameter tp) { Contract.Assert(tyArguments == null || tyArguments.Count == 0); var nm = nameTypeParam(tp); // return an identifier denoting a constant return new Bpl.IdentifierExpr(x.tok, nm, predef.Ty); } else { - var ot = (OpaqueTypeDecl)x; + var ot = (AbstractTypeDecl)x; var nm = nameTypeParam(ot); if (tyArguments.Count != 0) { List args = tyArguments.ConvertAll(TypeToTy); diff --git a/Source/DafnyLanguageServer/Language/SyntaxTreeVisitor.cs b/Source/DafnyLanguageServer/Language/SyntaxTreeVisitor.cs index b79f8f457e5..12502809d92 100644 --- a/Source/DafnyLanguageServer/Language/SyntaxTreeVisitor.cs +++ b/Source/DafnyLanguageServer/Language/SyntaxTreeVisitor.cs @@ -39,7 +39,7 @@ public virtual void Visit(TopLevelDecl topLevelDeclaration) { break; case ModuleDecl moduleDeclaration: case ValuetypeDecl valueTypeDeclaration: - case OpaqueTypeDecl opaqueTypeDeclaration: + case AbstractTypeDecl opaqueTypeDeclaration: case NewtypeDecl newTypeDeclaration: case TypeSynonymDecl typeSynonymDeclaration: default: diff --git a/Source/DafnyPipeline.Test/DocstringTest.cs b/Source/DafnyPipeline.Test/DocstringTest.cs index 19829e567d9..d0e2a6e2951 100644 --- a/Source/DafnyPipeline.Test/DocstringTest.cs +++ b/Source/DafnyPipeline.Test/DocstringTest.cs @@ -227,13 +227,13 @@ function flip(): BinDigit { type ZeroOrMore2 = nat // Unattached comment -type OpaqueType -// OpaqueType has opaque methods so you don't see them +type AbstractType +// AbstractType has opaque methods so you don't see them { } -/** OpaqueType2 has opaque methods so you don't see them */ -type OpaqueType2 +/** AbstractType2 has opaque methods so you don't see them */ +type AbstractType2 { } ", new List<(string nodeTokenValue, string? expectedDocstring)> { @@ -245,8 +245,8 @@ type OpaqueType2 ("BinDigit", "A binary digit"), ("ZeroOrMore", "ZeroOrMore is the same as nat"), ("ZeroOrMore2", "ZeroOrMore2 is the same as nat"), - ("OpaqueType", "OpaqueType has opaque methods so you don't see them"), - ("OpaqueType2", "OpaqueType2 has opaque methods so you don't see them") + ("AbstractType", "AbstractType has opaque methods so you don't see them"), + ("AbstractType2", "AbstractType2 has opaque methods so you don't see them") }); } diff --git a/Test/git-issues/git-issue-2100.dfy b/Test/git-issues/git-issue-2100.dfy index 1b69603d482..affa34cdebf 100644 --- a/Test/git-issues/git-issue-2100.dfy +++ b/Test/git-issues/git-issue-2100.dfy @@ -14,9 +14,9 @@ module Client { // The mention of the export-provided Cl below (in the case where // its parent type, Tr, is not exported) once generated malformed - // Boogie. In particular, Cl should be treated as an abstract type in + // Boogie. In particular, Cl should be treated as an opaque type in // this Client module, but in some places in the translation to Boogie, - // the type was still treated as a non-abstract type. + // the type was still treated as a non-opaque type. method Test(cl: Library.Cl) { } } From eed2c802a3bb0e390ab56fb6431bebbb6baea134 Mon Sep 17 00:00:00 2001 From: davidcok Date: Wed, 10 May 2023 18:27:19 -0400 Subject: [PATCH 7/9] Fixing Dafny,atg --- Source/DafnyCore/Dafny.atg | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg index fc34dfa7f86..071c1b7c7d7 100644 --- a/Source/DafnyCore/Dafny.atg +++ b/Source/DafnyCore/Dafny.atg @@ -1673,7 +1673,7 @@ SynonymTypeDecl Date: Wed, 10 May 2023 20:26:10 -0400 Subject: [PATCH 8/9] One more expected test result --- Test/exports/ExportResolve.dfy.expect | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/Test/exports/ExportResolve.dfy.expect b/Test/exports/ExportResolve.dfy.expect index 422a112a16c..495d97f96b0 100644 --- a/Test/exports/ExportResolve.dfy.expect +++ b/Test/exports/ExportResolve.dfy.expect @@ -36,24 +36,24 @@ ExportResolve.dfy(89,18): Error: 'M' cannot be revealed in an export. Use "provi ExportResolve.dfy(90,18): Error: 'x' cannot be revealed in an export. Use "provides" instead. ExportResolve.dfy(91,18): Error: 'FromInt' cannot be revealed in an export. Use "provides" instead. ExportResolve.dfy(156,18): Error: Raised while checking export set P0: unresolved identifier: X -ExportResolve.dfy(156,26): Error: Raised while checking export set P0: member 'X' does not exist in opaque type 'Dt' -ExportResolve.dfy(156,34): Error: Raised while checking export set P0: member 'More?' does not exist in opaque type 'Dt' -ExportResolve.dfy(156,45): Error: Raised while checking export set P0: member 'u' does not exist in opaque type 'Dt' +ExportResolve.dfy(156,26): Error: Raised while checking export set P0: member 'X' does not exist in abstract type 'Dt' +ExportResolve.dfy(156,34): Error: Raised while checking export set P0: member 'More?' does not exist in abstract type 'Dt' +ExportResolve.dfy(156,45): Error: Raised while checking export set P0: member 'u' does not exist in abstract type 'Dt' ExportResolve.dfy(111,9): Error: This export set is not consistent: P0 ExportResolve.dfy(158,18): Error: Raised while checking export set P1: type of corresponding source/RHS (Trait) does not match type of bound variable (object?) ExportResolve.dfy(158,46): Error: Raised while checking export set P1: type of corresponding source/RHS (Klass) does not match type of bound variable (object?) ExportResolve.dfy(113,9): Error: This export set is not consistent: P1 -ExportResolve.dfy(160,15): Error: Raised while checking export set P2: member 'Valid' does not exist in opaque type 'Trait' -ExportResolve.dfy(160,28): Error: Raised while checking export set P2: member 'Valid' does not exist in opaque type 'Klass' -ExportResolve.dfy(160,41): Error: Raised while checking export set P2: member 'Valid' does not exist in opaque type 'Dt' +ExportResolve.dfy(160,15): Error: Raised while checking export set P2: member 'Valid' does not exist in abstract type 'Trait' +ExportResolve.dfy(160,28): Error: Raised while checking export set P2: member 'Valid' does not exist in abstract type 'Klass' +ExportResolve.dfy(160,41): Error: Raised while checking export set P2: member 'Valid' does not exist in abstract type 'Dt' ExportResolve.dfy(115,9): Error: This export set is not consistent: P2 -ExportResolve.dfy(162,19): Error: Raised while checking export set P3: member 'N' does not exist in opaque type 'Trait' -ExportResolve.dfy(162,30): Error: Raised while checking export set P3: member 'N' does not exist in opaque type 'Klass' -ExportResolve.dfy(162,38): Error: Raised while checking export set P3: member 'N' does not exist in opaque type 'Dt' +ExportResolve.dfy(162,19): Error: Raised while checking export set P3: member 'N' does not exist in abstract type 'Trait' +ExportResolve.dfy(162,30): Error: Raised while checking export set P3: member 'N' does not exist in abstract type 'Klass' +ExportResolve.dfy(162,38): Error: Raised while checking export set P3: member 'N' does not exist in abstract type 'Dt' ExportResolve.dfy(117,9): Error: This export set is not consistent: P3 -ExportResolve.dfy(164,15): Error: Raised while checking export set P4: member 'M' does not exist in opaque type 'Trait' -ExportResolve.dfy(164,22): Error: Raised while checking export set P4: member 'M' does not exist in opaque type 'Klass' -ExportResolve.dfy(164,29): Error: Raised while checking export set P4: member 'M' does not exist in opaque type 'Dt' +ExportResolve.dfy(164,15): Error: Raised while checking export set P4: member 'M' does not exist in abstract type 'Trait' +ExportResolve.dfy(164,22): Error: Raised while checking export set P4: member 'M' does not exist in abstract type 'Klass' +ExportResolve.dfy(164,29): Error: Raised while checking export set P4: member 'M' does not exist in abstract type 'Dt' ExportResolve.dfy(119,9): Error: This export set is not consistent: P4 ExportResolve.dfy(123,19): Error: Cannot export type member 'FromInt' without providing its enclosing class 'Klass' ExportResolve.dfy(126,19): Error: Cannot export mutable field 'x' without revealing its enclosing trait 'Trait' From 31b43ddfed818a001f6ffb9cf93df013c996c2bc Mon Sep 17 00:00:00 2001 From: davidcok Date: Thu, 18 May 2023 19:21:58 -0400 Subject: [PATCH 9/9] Review edits --- Source/DafnyCore/AST/Types/Types.cs | 4 +-- .../Verifier/Translator.ClassMembers.cs | 2 +- Source/DafnyCore/Verifier/Translator.cs | 26 +++++++++---------- 3 files changed, 15 insertions(+), 17 deletions(-) diff --git a/Source/DafnyCore/AST/Types/Types.cs b/Source/DafnyCore/AST/Types/Types.cs index 9d7d00f680c..ea9b958c164 100644 --- a/Source/DafnyCore/AST/Types/Types.cs +++ b/Source/DafnyCore/AST/Types/Types.cs @@ -2370,9 +2370,7 @@ public UserDefinedType(TypeParameter tp) } /// - /// This constructor constructs a resolved type parameter (but shouldn't be called if "tp" denotes - /// the .TheType of an abstract type -- use the (AbstractType_AsParameter, AbstractTypeDecl, List(Type)) - /// constructor for that). + /// This constructor constructs a resolved type parameter /// public UserDefinedType(IToken tok, TypeParameter tp) { Contract.Requires(tok != null); diff --git a/Source/DafnyCore/Verifier/Translator.ClassMembers.cs b/Source/DafnyCore/Verifier/Translator.ClassMembers.cs index 27abffcc08a..006ba7057cb 100644 --- a/Source/DafnyCore/Verifier/Translator.ClassMembers.cs +++ b/Source/DafnyCore/Verifier/Translator.ClassMembers.cs @@ -994,7 +994,7 @@ private void AddOverrideCheckTypeArgumentInstantiations(MemberDecl member, Boogi } var typeMap = GetTypeArgumentSubstitutionMap(overriddenMember, member); foreach (var tp in Util.Concat(overriddenMember.EnclosingClass.TypeArgs, overriddenTypeParameters)) { - var local = BplLocalVar(nameTypeParam(tp), predef.Ty, out var lhs); + var local = BplLocalVar(NameTypeParam(tp), predef.Ty, out var lhs); localVariables.Add(local); var rhs = TypeToTy(typeMap[tp]); builder.Add(new Boogie.AssumeCmd(tp.tok, Boogie.Expr.Eq(lhs, rhs))); diff --git a/Source/DafnyCore/Verifier/Translator.cs b/Source/DafnyCore/Verifier/Translator.cs index f1b236093ca..66dfce80fd3 100644 --- a/Source/DafnyCore/Verifier/Translator.cs +++ b/Source/DafnyCore/Verifier/Translator.cs @@ -1214,7 +1214,7 @@ void AddTypeDecl_Aux(IToken tok, string nm, List typeArgs, TypePa void AddTypeDecl(AbstractTypeDecl td) { Contract.Requires(td != null); - AddTypeDecl_Aux(td.tok, nameTypeParam(td), td.TypeArgs, td.Characteristics); + AddTypeDecl_Aux(td.tok, NameTypeParam(td), td.TypeArgs, td.Characteristics); } @@ -4387,7 +4387,7 @@ void AddWellformednessCheck(Function f) { { var args = new List(); foreach (var p in GetTypeParams(f)) { - args.Add(trTypeParamOrAbstractType(p)); + args.Add(TrTypeParamOrAbstractType(p)); } if (f.IsFuelAware()) { args.Add(etran.layerInterCluster.GetFunctionFuel(f)); @@ -4430,7 +4430,7 @@ void AddWellformednessCheck(Function f) { var funcID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullSanitizedName, TrType(f.ResultType))); var args = new List(); foreach (var p in GetTypeParams(f)) { - args.Add(trTypeParamOrAbstractType(p)); + args.Add(TrTypeParamOrAbstractType(p)); } if (f.IsFuelAware()) { args.Add(etran.layerInterCluster.GetFunctionFuel(f)); @@ -8249,7 +8249,7 @@ Bpl.Expr TypeToTy(Type type) { if (type.IsTypeParameter || type.IsAbstractType) { var udt = (UserDefinedType)type; - return trTypeParamOrAbstractType(udt.ResolvedClass, udt.TypeArgs); + return TrTypeParamOrAbstractType(udt.ResolvedClass, udt.TypeArgs); } else if (type is UserDefinedType) { // Classes, (co-)datatypes, newtypes, subset types, ... var args = type.TypeArgs.ConvertAll(TypeToTy); @@ -8280,13 +8280,13 @@ Bpl.Expr TypeToTy(Type type) { } else if (type is BigOrdinalType) { return new Bpl.IdentifierExpr(Token.NoToken, "TORDINAL", predef.Ty); } else if (type is ParamTypeProxy) { - return trTypeParamOrAbstractType(((ParamTypeProxy)type).orig); + return TrTypeParamOrAbstractType(((ParamTypeProxy)type).orig); } else { Contract.Assert(false); throw new cce.UnreachableException(); // unexpected type } } - static string nameTypeParam(TopLevelDecl x) { + static string NameTypeParam(TopLevelDecl x) { Contract.Requires(x is TypeParameter || x is AbstractTypeDecl); if (x is TypeParameter tp && tp.Parent != null) { return tp.Parent.FullName + "$" + x.Name; @@ -8296,18 +8296,18 @@ static string nameTypeParam(TopLevelDecl x) { } } - Bpl.Expr trTypeParamOrAbstractType(TopLevelDecl x, List/*?*/ tyArguments = null) { + Bpl.Expr TrTypeParamOrAbstractType(TopLevelDecl x, List/*?*/ tyArguments = null) { Contract.Requires(x is TypeParameter || x is AbstractTypeDecl); Contract.Requires(!(x is TypeParameter) || tyArguments == null || tyArguments.Count == 0); Contract.Requires(!(x is AbstractTypeDecl) || tyArguments != null); if (x is TypeParameter tp) { Contract.Assert(tyArguments == null || tyArguments.Count == 0); - var nm = nameTypeParam(tp); + var nm = NameTypeParam(tp); // return an identifier denoting a constant return new Bpl.IdentifierExpr(x.tok, nm, predef.Ty); } else { var ot = (AbstractTypeDecl)x; - var nm = nameTypeParam(ot); + var nm = NameTypeParam(ot); if (tyArguments.Count != 0) { List args = tyArguments.ConvertAll(TypeToTy); return FunctionCall(x.tok, nm, predef.Ty, args); @@ -9478,7 +9478,7 @@ public List GAsVars(Translator translator, bool wantFormals, out Bpl.E Contract.Requires(translator != null); var vv = new List(); // first, add the type variables - vv.AddRange(Map(FTVs, tp => NewVar(nameTypeParam(tp), translator.predef.Ty, wantFormals))); + vv.AddRange(Map(FTVs, tp => NewVar(NameTypeParam(tp), translator.predef.Ty, wantFormals))); typeAntecedents = Bpl.Expr.True; if (UsesHeap) { var nv = NewVar("$heap", translator.predef.HeapType, wantFormals); @@ -10867,7 +10867,7 @@ public override BinderExpr VisitBinderExpr(BinderExpr node) { var vars = new List(); exprs = new List(); foreach (TypeParameter v in args) { - vars.Add(BplBoundVar(nameTypeParam(v), predef.Ty, out var e)); + vars.Add(BplBoundVar(NameTypeParam(v), predef.Ty, out var e)); exprs.Add(e); } return vars; @@ -10883,8 +10883,8 @@ List MkTyParamFormals(List args, bool includeWhereClaus var vars = new List(); exprs = new List(); foreach (TypeParameter v in args) { - var whereClause = includeWhereClause ? GetTyWhereClause(new Bpl.IdentifierExpr(v.tok, nameTypeParam(v), predef.Ty), v.Characteristics) : null; - vars.Add(BplFormalVar(named ? nameTypeParam(v) : null, predef.Ty, true, out var e, whereClause)); + var whereClause = includeWhereClause ? GetTyWhereClause(new Bpl.IdentifierExpr(v.tok, NameTypeParam(v), predef.Ty), v.Characteristics) : null; + vars.Add(BplFormalVar(named ? NameTypeParam(v) : null, predef.Ty, true, out var e, whereClause)); exprs.Add(e); } return vars;