Changing opaque type to abstract type

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<MemberDecl>();
-        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);

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,15 +294,15 @@ [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).
 ");
 
     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.
 ");

Source/DafnyCore/AST/Grammar/Printer.cs

@@ -276,8 +276,8 @@ public void PrintTopLevelDecls(List<TopLevelDecl> decls, int indent, List<IToken
       foreach (TopLevelDecl d in decls) {
         Contract.Assert(d != null);
         if (PrintModeSkipGeneral(d.tok, fileBeingPrinted)) { continue; }
-        if (d is OpaqueTypeDecl) {
-          var at = (OpaqueTypeDecl)d;
+        if (d is AbstractTypeDecl) {
+          var at = (AbstractTypeDecl)d;
           if (i++ != 0) { wr.WriteLine(); }
           Indent(indent);
           PrintClassMethodHelper("type", at.Attributes, at.Name + TPCharacteristicsSuffix(at.Characteristics), d.TypeArgs);

Source/DafnyCore/AST/TopLevelDeclarations.cs

@@ -347,8 +347,8 @@ public override string FullName {
   public static TypeParameterCharacteristics GetExplicitCharacteristics(TopLevelDecl d) {
     Contract.Requires(d != null);
     TypeParameterCharacteristics characteristics = new TypeParameterCharacteristics(false);
-    if (d is OpaqueTypeDecl) {
-      var dd = (OpaqueTypeDecl)d;
+    if (d is AbstractTypeDecl) {
+      var dd = (AbstractTypeDecl)d;
       characteristics = dd.Characteristics;
     } else if (d is TypeSynonymDecl) {
       var dd = (TypeSynonymDecl)d;
@@ -2081,15 +2081,15 @@ public NoContext(ModuleDefinition module) {
   public bool AllowsAllocation => true;
 }
 
-public class OpaqueTypeDecl : TopLevelDeclWithMembers, TypeParameter.ParentType, RevealableTypeDecl, ICanFormat, IHasDocstring {
-  public override string WhatKind { get { return "opaque type"; } }
+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;
   public bool SupportsEquality {
     get { return Characteristics.EqualitySupport != TypeParameter.EqualitySupportValue.Unspecified; }
   }
 
-  public OpaqueTypeDecl(RangeToken rangeToken, Name name, ModuleDefinition module, TypeParameter.TypeParameterCharacteristics characteristics, List<TypeParameter> typeArgs, List<MemberDecl> members, Attributes attributes, bool isRefining)
+  public AbstractTypeDecl(RangeToken rangeToken, Name name, ModuleDefinition module, TypeParameter.TypeParameterCharacteristics characteristics, List<TypeParameter> typeArgs, List<MemberDecl> members, Attributes attributes, bool isRefining)
     : base(rangeToken, name, module, typeArgs, members, attributes, isRefining) {
     Contract.Requires(rangeToken != null);
     Contract.Requires(name != null);

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;
     }
   }
 
@@ -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)) {
@@ -2370,9 +2370,7 @@ public UserDefinedType(TypeParameter tp)
   }
 
   /// <summary>
-  /// 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))
-  /// constructor for that).
+  /// This constructor constructs a resolved type parameter
   /// </summary>
   public UserDefinedType(IToken tok, TypeParameter tp) {
     Contract.Requires(tok != null);
@@ -2549,8 +2547,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 +2632,7 @@ public override bool ComputeMayInvolveReferences(ISet<DatatypeDecl> 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 +2767,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;

Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs

@@ -47,15 +47,15 @@ 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) {
-        // This is unusual. Typically, the compiler never needs to compile an opaque type, but this opaque type
+      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
-        // 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
@@ -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;

Source/DafnyCore/Compilers/Cplusplus/Compiler-cpp.cs

@@ -959,7 +959,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);
@@ -1035,8 +1035,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));
@@ -1134,7 +1134,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 {

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;

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;

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;

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: