Allow non-reference-type traits

Source/DafnyCore/AST/Cloner.cs

@@ -69,7 +69,10 @@ public virtual TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition ne
 
       if (d is AbstractTypeDecl) {
         var dd = (AbstractTypeDecl)d;
-        return new AbstractTypeDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), newParent, CloneTPChar(dd.Characteristics), dd.TypeArgs.ConvertAll(CloneTypeParam), dd.Members.ConvertAll(d => CloneMember(d, false)), CloneAttributes(dd.Attributes), dd.IsRefining);
+        return new AbstractTypeDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), newParent,
+          CloneTPChar(dd.Characteristics), dd.TypeArgs.ConvertAll(CloneTypeParam),
+          dd.ParentTraits.ConvertAll(CloneType),
+          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;
@@ -83,10 +86,12 @@ public virtual TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition ne
         var dd = (NewtypeDecl)d;
         if (dd.Var == null) {
           return new NewtypeDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), newParent, CloneType(dd.BaseType),
+            dd.ParentTraits.ConvertAll(CloneType),
             dd.Members.ConvertAll(d => CloneMember(d, false)), CloneAttributes(dd.Attributes), dd.IsRefining);
         } else {
           return new NewtypeDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), newParent, CloneBoundVar(dd.Var, false),
             CloneExpr(dd.Constraint), dd.WitnessKind, CloneExpr(dd.Witness),
+            dd.ParentTraits.ConvertAll(CloneType),
             dd.Members.ConvertAll(d => CloneMember(d, false)), CloneAttributes(dd.Attributes), dd.IsRefining);
         }
       } else if (d is TupleTypeDecl) {
@@ -97,13 +102,17 @@ public virtual TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition ne
         var dd = (IndDatatypeDecl)d;
         var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);
         var ctors = dd.Ctors.ConvertAll(CloneCtor);
-        var dt = new IndDatatypeDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), newParent, tps, ctors, dd.Members.ConvertAll(d => CloneMember(d, false)), CloneAttributes(dd.Attributes), dd.IsRefining);
+        var dt = new IndDatatypeDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), newParent, tps, ctors,
+          dd.ParentTraits.ConvertAll(CloneType),
+          dd.Members.ConvertAll(d => CloneMember(d, false)), CloneAttributes(dd.Attributes), dd.IsRefining);
         return dt;
       } else if (d is CoDatatypeDecl) {
         var dd = (CoDatatypeDecl)d;
         var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);
         var ctors = dd.Ctors.ConvertAll(CloneCtor);
-        var dt = new CoDatatypeDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), newParent, tps, ctors, dd.Members.ConvertAll(d => CloneMember(d, false)), CloneAttributes(dd.Attributes), dd.IsRefining);
+        var dt = new CoDatatypeDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), newParent, tps, ctors,
+          dd.ParentTraits.ConvertAll(CloneType),
+          dd.Members.ConvertAll(d => CloneMember(d, false)), CloneAttributes(dd.Attributes), dd.IsRefining);
         return dt;
       } else if (d is IteratorDecl) {
         var dd = (IteratorDecl)d;

Source/DafnyCore/AST/Grammar/ParseErrors.cs

@@ -32,7 +32,6 @@ public enum ErrorId {
     p_module_level_function_always_static,
     p_module_level_method_always_static,
     p_bad_datatype_refinement,
-    p_no_mutable_fields_in_value_types,
     p_module_level_const_always_static,
     p_const_decl_missing_identifier,
     p_bad_const_initialize_op,
@@ -138,7 +137,7 @@ public enum ErrorId {
     p_deprecated_statement_refinement,
     p_internal_exception,
     p_file_has_no_code,
-
+    p_general_traits_beta,
   }
 
   static ParseErrors() {
@@ -152,6 +151,11 @@ static ParseErrors() {
     Add(ErrorId.p_abstract_not_allowed,
     @"
 Only modules may be declared abstract.
+", Remove(true));
+
+    Add(ErrorId.p_general_traits_beta,
+      @"
+Use of traits as non-reference types is a beta feature. To engage, use /generalTraits:1.
 ", Remove(true));
 
     Add(ErrorId.p_no_ghost_for_by_method,
@@ -299,13 +303,6 @@ This mistake is easy to make when the clauses are on the same line.
 It is only allowed to add members to the body of the datatype.
 ");
 
-    Add(ErrorId.p_no_mutable_fields_in_value_types,
-    @"
-The `var` declaration declares a mutable field, which is only permitted within
-classes, traits and iterators. 
-`const` declarations can be members of value-types, such as datatypes.
-", Replace("const"));
-
     Add(ErrorId.p_module_level_function_always_static,
     @"
 All names declared in a module (outside a class-like entity) are implicitly `static`.

Source/DafnyCore/AST/Grammar/Printer.cs

@@ -277,6 +277,7 @@ public void PrintTopLevelDecls(CompilationData compilation, IEnumerable<TopLevel
           if (i++ != 0) { wr.WriteLine(); }
           Indent(indent);
           PrintClassMethodHelper("type", at.Attributes, at.Name + TPCharacteristicsSuffix(at.Characteristics), d.TypeArgs);
+          PrintExtendsClause(at);
           if (at.Members.Count == 0) {
             wr.WriteLine();
           } else {
@@ -290,6 +291,7 @@ public void PrintTopLevelDecls(CompilationData compilation, IEnumerable<TopLevel
           if (i++ != 0) { wr.WriteLine(); }
           Indent(indent);
           PrintClassMethodHelper("newtype", dd.Attributes, dd.Name, new List<TypeParameter>());
+          PrintExtendsClause(dd);
           wr.Write(" = ");
           if (dd.Var == null) {
             PrintType(dd.BaseType);
@@ -365,6 +367,11 @@ public void PrintTopLevelDecls(CompilationData compilation, IEnumerable<TopLevel
           if (i++ != 0) { wr.WriteLine(); }
           PrintClass(cl, indent, fileBeingPrinted);
 
+        } else if (d is ClassLikeDecl) {
+          var cl = (ClassLikeDecl)d;
+          if (i++ != 0) { wr.WriteLine(); }
+          PrintClass(cl, indent, fileBeingPrinted);
+
         } else if (d is ValuetypeDecl) {
           var vtd = (ValuetypeDecl)d;
           if (i++ != 0) { wr.WriteLine(); }
@@ -604,7 +611,7 @@ void PrintIteratorSignature(IteratorDecl iter, int indent) {
       Indent(indent);
       PrintClassMethodHelper("iterator", iter.Attributes, iter.Name, iter.TypeArgs);
       if (iter.IsRefining) {
-        wr.Write(" ... ");
+        wr.Write(" ...");
       } else {
         PrintFormals(iter.Ins, iter);
         if (iter.Outs.Count != 0) {
@@ -650,14 +657,9 @@ public void PrintClass(ClassLikeDecl c, int indent, string fileBeingPrinted) {
       Indent(indent);
       PrintClassMethodHelper((c is TraitDecl) ? "trait" : "class", c.Attributes, c.Name, c.TypeArgs);
       if (c.IsRefining) {
-        wr.Write(" ... ");
+        wr.Write(" ...");
       } else {
-        string sep = " extends ";
-        foreach (var trait in c.ParentTraits) {
-          wr.Write(sep);
-          PrintType(trait);
-          sep = ", ";
-        }
+        PrintExtendsClause(c);
       }
 
       if (c.Members.Count == 0) {
@@ -680,6 +682,15 @@ public void PrintClass(ClassLikeDecl c, int indent, string fileBeingPrinted) {
       }
     }
 
+    private void PrintExtendsClause(TopLevelDeclWithMembers c) {
+      string sep = " extends ";
+      foreach (var trait in c.ParentTraits) {
+        wr.Write(sep);
+        PrintType(trait);
+        sep = ", ";
+      }
+    }
+
     public void PrintMembers(List<MemberDecl> members, int indent, string fileBeingPrinted) {
       Contract.Requires(members != null);
 
@@ -805,6 +816,7 @@ public void PrintDatatype(DatatypeDecl dt, int indent, string fileBeingPrinted)
       Contract.Requires(dt != null);
       Indent(indent);
       PrintClassMethodHelper(dt is IndDatatypeDecl ? "datatype" : "codatatype", dt.Attributes, dt.Name, dt.TypeArgs);
+      PrintExtendsClause(dt);
       wr.Write(" =");
       string sep = "";
       foreach (DatatypeCtor ctor in dt.Ctors) {

Source/DafnyCore/AST/Grammar/ProgramParser.cs

@@ -145,8 +145,8 @@ public static void AddParseResultToProgram(DfyParseResult parseResult, Program p
         literalModuleDecl.ModuleDef.EnclosingModule = defaultModule;
       }
 
-      if (declToMove is ClassLikeDecl classDecl) {
-        classDecl.NonNullTypeDecl.EnclosingModuleDefinition = defaultModule;
+      if (declToMove is ClassLikeDecl { NonNullTypeDecl: { } nonNullTypeDecl }) {
+        nonNullTypeDecl.EnclosingModuleDefinition = defaultModule;
       }
       if (declToMove is DefaultClassDecl defaultClassDecl) {
         foreach (var member in defaultClassDecl.Members) {

Source/DafnyCore/AST/Modules/ModuleDefinition.cs

@@ -580,6 +580,9 @@ public ModuleSignature RegisterTopLevelDecls(Resolver resolver, bool useImports)
         registerThisDecl = nntd;
         registerUnderThisName = d.Name;
       } else {
+        // Register each class and trait C under its own name, C. Below, we will change this for reference types (which includes all classes
+        // and some of the traits), so that C? maps to the class/trait and C maps to the corresponding NonNullTypeDecl. We will need these
+        // initial mappings in order to look through the parent traits of traits, below.
         registerThisDecl = d;
         registerUnderThisName = d.Name;
       }
@@ -737,16 +740,22 @@ public ModuleSignature RegisterTopLevelDecls(Resolver resolver, bool useImports)
       }
     }
 
-    // Now, for each class, register its possibly-null type
+    DetermineReferenceTypes(resolver, sig);
+
+    // Now, for each reference type (class and some traits), register its possibly-null type.
+    // In the big loop above, each class and trait was registered under its own name. We're now going to change that for the reference types.
     foreach (TopLevelDecl d in TopLevelDecls) {
-      if ((d as ClassLikeDecl)?.NonNullTypeDecl != null) {
+      if (d is ClassLikeDecl { NonNullTypeDecl: { } nntd }) {
         var name = d.Name + "?";
-        TopLevelDecl prev;
-        if (toplevels.TryGetValue(name, out prev)) {
+        if (toplevels.ContainsKey(name)) {
           resolver.reporter.Error(MessageSource.Resolver, d,
-            "a module that already contains a top-level declaration '{0}' is not allowed to declare a {1} '{2}'",
+            "a module that already contains a top-level declaration '{0}' is not allowed to declare a reference type ({1}) '{2}'",
             name, d.WhatKind, d.Name);
         } else {
+          // change the mapping of d.Name to d.NonNullTypeDecl
+          toplevels[d.Name] = nntd;
+          sig.TopLevels[d.Name] = nntd;
+          // map the name d.Name+"?" to d
           toplevels[name] = d;
           sig.TopLevels[name] = d;
         }
@@ -755,4 +764,103 @@ public ModuleSignature RegisterTopLevelDecls(Resolver resolver, bool useImports)
 
     return sig;
   }
+
+  private void DetermineReferenceTypes(Resolver resolver, ModuleSignature sig) {
+    // Figure out which TraitDecl's are reference types, and for each of them, create a corresponding NonNullTypeDecl.
+    // To figure this out, we need to look at the parents of each TraitDecl, but those parents have not yet been resolved.
+    // Since we just need the head of each parent, we'll do that name resolution here (and will redo it later, when each parent
+    // type is resolved properly).
+    //
+    // Some inaccuracies can occur here, since possibly-null types have not yet been registered. However, since such types aren't allowed
+    // as parents, it doesn't matter that they aren't available yet.
+    //
+    // If the head of a parent trait cannot be resolved, it is ignored here. An error will be reported later, when trait declarations are
+    // resolved properly. Similarly, any cycle detected among the trait-parent heads is ignored. Cycles are detected (again) later and an
+    // error will be reported then (in the meantime, we may have computed incorrectly whether or not a TraitDecl is a reference type, but
+    // the cycle still remains, so an error will be reported later). (Btw, the later cycle detection detects not only cycles among parent
+    // heads, but also among the type arguments of parent traits.)
+    //
+    // In the following dictionary, a TraitDecl not being present among the keys means it has not been visited in the InheritsFromObject traversal.
+    // If a TraitDecl is a key and maps to "false", then it is currently being visited.
+    // If a TraitDecl is a key and maps to "true", then its .IsReferenceTypeDecl has been computed and is ready to be used.
+    var traitsProgress = new Dictionary<TraitDecl, bool>();
+    foreach (var decl in TopLevelDecls.Where(d => d is TraitDecl)) {
+      // Resolve a "path" to a top-level declaration, if possible. On error, return null.
+      // The path is expected to consist of NameSegment or ExprDotName nodes.
+      TopLevelDecl ResolveNamePath(Expression path) {
+        // A single NameSegment is a little different, because it may refer to built-in type (of interest here: "object").
+        if (path is NameSegment nameSegment) {
+          if (sig.TopLevels.TryGetValue(nameSegment.Name, out var topLevelDecl)) {
+            return topLevelDecl;
+          } else if (resolver.moduleInfo != null && resolver.moduleInfo.TopLevels.TryGetValue(nameSegment.Name, out topLevelDecl)) {
+            // For "object" and other reference-type declarations from other modules, we're picking up the NonNullTypeDecl; if so, return
+            // the original declaration.
+            return topLevelDecl is NonNullTypeDecl nntd ? nntd.ViewAsClass : topLevelDecl;
+          } else if (resolver.ProgramResolver.SystemModuleManager.systemNameInfo.TopLevels.TryGetValue(nameSegment.Name, out topLevelDecl)) {
+            // For "object" and other reference-type declarations from other modules, we're picking up the NonNullTypeDecl; if so, return
+            // the original declaration.
+            return topLevelDecl is NonNullTypeDecl nntd ? nntd.ViewAsClass : topLevelDecl;
+          } else {
+            return null;
+          }
+        }
+
+        // convert the ExprDotName to a list of strings
+        var names = new List<string>();
+        while (path is ExprDotName exprDotName) {
+          names.Add(exprDotName.SuffixName);
+          path = exprDotName.Lhs;
+        }
+        names.Add(((NameSegment)path).Name);
+        var s = sig;
+        var i = names.Count;
+        while (true) {
+          i--;
+          if (!s.TopLevels.TryGetValue(names[i], out var topLevelDecl)) {
+            return null;
+          } else if (i == 0) {
+            // For reference-type declarations from other modules, we're picking up the NonNullTypeDecl; if so, return
+            // the original declaration.
+            return topLevelDecl is NonNullTypeDecl nntd ? nntd.ViewAsClass : topLevelDecl;
+          } else if (topLevelDecl is ModuleDecl moduleDecl) {
+            var signature = moduleDecl.AccessibleSignature(false);
+            s = resolver.GetSignature(signature);
+          } else {
+            return null;
+          }
+        }
+      }
+
+      bool InheritsFromObject(TraitDecl traitDecl) {
+        if (traitsProgress.TryGetValue(traitDecl, out var isDone)) {
+          if (isDone) {
+            return traitDecl.IsReferenceTypeDecl;
+          } else {
+            // there is a cycle among the parents, so we'll suppose the trait does inherit from "object"
+            return true;
+          }
+        }
+        traitsProgress[traitDecl] = false; // indicate that traitDecl is currently being visited
+
+        var inheritsFromObject = traitDecl.IsObjectTrait;
+        foreach (var parent in traitDecl.ParentTraits) {
+          if (parent is UserDefinedType udt) {
+            if (ResolveNamePath(udt.NamePath) is TraitDecl parentTrait) {
+              if (parentTrait.EnclosingModuleDefinition == this) {
+                inheritsFromObject = InheritsFromObject(parentTrait) || inheritsFromObject;
+              } else {
+                inheritsFromObject = parentTrait.IsReferenceTypeDecl || inheritsFromObject;
+              }
+            }
+          }
+        }
+
+        traitDecl.SetUpAsReferenceType(resolver.Options.Get(CommonOptionBag.GeneralTraits) ? inheritsFromObject : true);
+        traitsProgress[traitDecl] = true; // indicate that traitDecl.IsReferenceTypeDecl can now be called
+        return inheritsFromObject;
+      }
+
+      InheritsFromObject((TraitDecl)decl);
+    }
+  }
 }

Source/DafnyCore/AST/Modules/ScopeCloner.cs

@@ -94,7 +94,10 @@ public override TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition n
       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 AbstractTypeDecl(Range(d.RangeToken), d.NameNode.Clone(this), newParent, characteristics, tps, members, CloneAttributes(d.Attributes), d.IsRefining);
+      // copy the newParent traits only if "d" is already an AbstractTypeDecl and is being export-revealed
+      var otd = new AbstractTypeDecl(Range(d.RangeToken), d.NameNode.Clone(this), newParent, characteristics, tps,
+        new List<Type>(), // omit the newParent traits
+        members, CloneAttributes(d.Attributes), d.IsRefining);
       based = otd;
       if (d is ClassLikeDecl { IsReferenceTypeDecl: true } cl) {
         reverseMap.Add(based, cl.NonNullTypeDecl);

Source/DafnyCore/AST/TypeDeclarations/AbstractTypeDecl.cs

@@ -11,8 +11,9 @@ public bool SupportsEquality {
     get { return Characteristics.EqualitySupport != TypeParameter.EqualitySupportValue.Unspecified; }
   }
 
-  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) {
+  public AbstractTypeDecl(RangeToken rangeToken, Name name, ModuleDefinition module, TypeParameter.TypeParameterCharacteristics characteristics,
+    List<TypeParameter> typeArgs, List<Type> parentTraits, List<MemberDecl> members, Attributes attributes, bool isRefining)
+    : base(rangeToken, name, module, typeArgs, members, attributes, isRefining, parentTraits) {
     Contract.Requires(rangeToken != null);
     Contract.Requires(name != null);
     Contract.Requires(module != null);

Source/DafnyCore/AST/TypeDeclarations/ClassDecl.cs

@@ -8,7 +8,6 @@ public class ClassDecl : ClassLikeDecl, IHasDocstring {
   public override bool IsReferenceTypeDecl => true;
   public override bool AcceptThis => true;
 
-  public override bool CanBeRevealed() { return true; }
   [FilledInDuringResolution] public bool HasConstructor;  // filled in (early) during resolution; true iff there exists a member that is a Constructor
   [ContractInvariantMethod]
   void ObjectInvariant() {