Support members for the new newtypes (dafny-lang#5311)

This PR adds support for members of the recently expanded newtypes. In
particular, inheritance of user-defined members and built-in members
(such as `.RotateLeft` for bitvector types) are handled. Under
`--general-trait=full`, inheritance from both `newtype` base types and
parent traits are handled.

A `newtype`'s inherited members can only be figured out once the
`newtype`'s base type is known. Since the base type is in general
inferred, this means that member registration cannot happen until
resolution has started. So, this PR moves that process from
`Register...` to `Resolve...`.

As part of this PR, other built-in types (`char`, `set`, ...) were added
to the `valuetypeDecls` array. This has an effect on the `--rprint`
output.

The PR also improves some error messages (e.g., making them more
consistent by using the format `type 'T'`) and removes some unused code
that was left in abandoned `#if ...` directives during the resolver
refresh.

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

Source/DafnyCore/AST/Grammar/Printer/Printer.cs

@@ -889,7 +889,7 @@ public void PrintField(Field field, int indent) {
       if (field.IsGhost) {
         wr.Write("ghost ");
       }
-      if (field is ConstantField) {
+      if (!field.IsMutable) {
         wr.Write("const");
       } else {
         wr.Write("var");
@@ -906,12 +906,8 @@ public void PrintField(Field field, int indent) {
           wr.Write(" := ");
           PrintExpression(c.Rhs, true);
         }
-      } else if (field.IsUserMutable) {
-        // nothing more to say
-      } else if (field.IsMutable) {
+      } else if (!field.IsUserMutable && field.IsMutable) {
         wr.Write("  // non-assignable");
-      } else {
-        wr.Write("  // immutable");
       }
       wr.WriteLine();
     }

Source/DafnyCore/AST/Members/MemberDecl.cs

@@ -7,6 +7,7 @@ namespace Microsoft.Dafny;
 
 public abstract class MemberDecl : Declaration {
   public abstract string WhatKind { get; }
+  public string WhatKindAndName => $"{WhatKind} '{Name}'";
   public virtual string WhatKindMentionGhost => (IsGhost ? "ghost " : "") + WhatKind;
   protected bool hasStaticKeyword;
   public bool HasStaticKeyword => hasStaticKeyword;

Source/DafnyCore/AST/SystemModuleManager.cs

@@ -122,18 +122,34 @@ public SystemModuleManager(DafnyOptions options) {
     CreateArrowTypeDecl(1);
 
     valuetypeDecls = new[] {
-        new ValuetypeDecl("bool", SystemModule, t => t.IsBoolType, typeArgs => Type.Bool),
-        new ValuetypeDecl("int", SystemModule, t => t.IsNumericBased(Type.NumericPersuasion.Int), typeArgs => Type.Int),
-        new ValuetypeDecl("real", SystemModule, t => t.IsNumericBased(Type.NumericPersuasion.Real), typeArgs => Type.Real),
-        new ValuetypeDecl("ORDINAL", SystemModule, t => t.IsBigOrdinalType, typeArgs => Type.BigOrdinal),
-        new ValuetypeDecl("_bv", SystemModule, t => t.IsBitVectorType, null), // "_bv" represents a family of classes, so no typeTester or type creator is supplied
-        new ValuetypeDecl("map", SystemModule,
-          new List<TypeParameter.TPVarianceSyntax>() { TypeParameter.TPVarianceSyntax.Covariant_Strict , TypeParameter.TPVarianceSyntax.Covariant_Strict },
-          t => t.IsMapType, typeArgs => new MapType(true, typeArgs[0], typeArgs[1])),
-        new ValuetypeDecl("imap", SystemModule,
-          new List<TypeParameter.TPVarianceSyntax>() { TypeParameter.TPVarianceSyntax.Covariant_Permissive , TypeParameter.TPVarianceSyntax.Covariant_Strict },
-          t => t.IsIMapType, typeArgs => new MapType(false, typeArgs[0], typeArgs[1]))
-      };
+      new ValuetypeDecl("bool", SystemModule, t => t.IsBoolType, typeArgs => Type.Bool),
+      new ValuetypeDecl("char", SystemModule, t => t.IsCharType, typeArgs => Type.Char),
+      new ValuetypeDecl("int", SystemModule, t => t.IsNumericBased(Type.NumericPersuasion.Int), typeArgs => Type.Int),
+      new ValuetypeDecl("real", SystemModule, t => t.IsNumericBased(Type.NumericPersuasion.Real), typeArgs => Type.Real),
+      new ValuetypeDecl("ORDINAL", SystemModule, t => t.IsBigOrdinalType, typeArgs => Type.BigOrdinal),
+      new ValuetypeDecl("_bv", SystemModule, t => t.IsBitVectorType && !Options.Get(CommonOptionBag.TypeSystemRefresh),
+        null), // "_bv" represents a family of classes, so no typeTester or type creator is supplied (it's used only in the legacy resolver)
+      new ValuetypeDecl("set", SystemModule,
+        new List<TypeParameter.TPVarianceSyntax>() { TypeParameter.TPVarianceSyntax.Covariant_Strict },
+        t => t.AsSetType is { Finite: true }, typeArgs => new SetType(true, typeArgs[0])),
+      new ValuetypeDecl("iset", SystemModule,
+        new List<TypeParameter.TPVarianceSyntax>() { TypeParameter.TPVarianceSyntax.Covariant_Permissive },
+        t => t.IsISetType, typeArgs => new SetType(false, typeArgs[0])),
+      new ValuetypeDecl("seq", SystemModule,
+        new List<TypeParameter.TPVarianceSyntax>() { TypeParameter.TPVarianceSyntax.Covariant_Strict },
+        t => t.AsSeqType != null, typeArgs => new SeqType(typeArgs[0])),
+      new ValuetypeDecl("multiset", SystemModule,
+        new List<TypeParameter.TPVarianceSyntax>() { TypeParameter.TPVarianceSyntax.Covariant_Strict },
+        t => t.AsMultiSetType != null, typeArgs => new MultiSetType(typeArgs[0])),
+      new ValuetypeDecl("map", SystemModule,
+        new List<TypeParameter.TPVarianceSyntax>()
+          { TypeParameter.TPVarianceSyntax.Covariant_Strict, TypeParameter.TPVarianceSyntax.Covariant_Strict },
+        t => t.IsMapType, typeArgs => new MapType(true, typeArgs[0], typeArgs[1])),
+      new ValuetypeDecl("imap", SystemModule,
+        new List<TypeParameter.TPVarianceSyntax>()
+          { TypeParameter.TPVarianceSyntax.Covariant_Permissive, TypeParameter.TPVarianceSyntax.Covariant_Strict },
+        t => t.IsIMapType, typeArgs => new MapType(false, typeArgs[0], typeArgs[1]))
+    };
     SystemModule.SourceDecls.AddRange(valuetypeDecls);
     // Resolution error handling relies on being able to get to the 0-tuple declaration
     TupleType(Token.NoToken, 0, true);
@@ -531,10 +547,15 @@ public void CheckHasAllArrowAritiesUpTo(int max) {
 
 enum ValuetypeVariety {
   Bool = 0,
+  Char,
   Int,
   Real,
   BigOrdinal,
   Bitvector,
+  Set,
+  ISet,
+  Seq,
+  Multiset,
   Map,
   IMap,
   None

Source/DafnyCore/AST/TypeDeclarations/TopLevelDecl.cs

@@ -6,6 +6,7 @@ namespace Microsoft.Dafny;
 
 public abstract class TopLevelDecl : Declaration, TypeParameter.ParentType {
   public abstract string WhatKind { get; }
+  public string WhatKindAndName => $"{WhatKind} '{Name}'";
   public ModuleDefinition EnclosingModuleDefinition;
   public readonly List<TypeParameter> TypeArgs;
   [ContractInvariantMethod]

Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs

@@ -3795,6 +3795,10 @@ protected override ConcreteSyntaxTree EmitCoercionIfNecessary(Type/*?*/ from, Ty
           wr.Write(".({0})", TypeName(to, wr, tok));
           return w;
         }
+      } else if (from.AsNewtype is { } fromNewtypeDecl) {
+        var subst = TypeParameter.SubstitutionMap(fromNewtypeDecl.TypeArgs, from.TypeArgs);
+        from = fromNewtypeDecl.BaseType.Subst(subst);
+        return EmitCoercionIfNecessary(from, to, tok, wr, toOrig);
       } else {
         // It's unclear to me whether it's possible to hit this case with a valid Dafny program,
         // so I'm not using UnsupportedFeatureError for now.