Support members for the new newtypes (#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 partial class Printer {
  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 partial class Printer {
  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 class SystemModuleManager {
  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 class SystemModuleManager {
 
 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 class ClassWriter : IClassWriter {
  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.