Fixes: Rust supports overriding traits

Source/DafnyCore.Test/GeneratedFromDafny/FactorPathsOptimizationTest.cs

@@ -40,7 +40,7 @@ public static void TestApply()
       _3_std__any__Any = (((RAST.__default.@global).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("std"))).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("any"))).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Any"));
       RAST._IType _4_Any;
       _4_Any = RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Any"));
-      FactorPathsOptimizationTest.__default.ShouldBeEqual(Dafny.Helpers.Id<Func<RAST._IMod, RAST._IMod>>(FactorPathsOptimization.__default.apply(RAST.__default.crate))(RAST.Mod.create_Mod(RAST.__default.NoDoc, RAST.__default.NoAttr, Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"), Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_StructDecl(RAST.Struct.create(RAST.__default.NoDoc, Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.FromElements(), Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"), Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_0_T__Decl), RAST.Fields.create_NamedFields(Dafny.Sequence<RAST._IField>.FromElements(RAST.Field.create(RAST.Visibility.create_PUB(), RAST.Formal.create(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("a"), (_3_std__any__Any).AsType())))))), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_Impl(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_0_T__Decl), (RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"))).Apply(Dafny.Sequence<RAST._IType>.FromElements(_2_T)), Dafny.Sequence<RAST._IImplMember>.FromElements())), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_0_T__Decl), (_3_std__any__Any).AsType(), ((((RAST.__default.crate).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"))).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"))).AsType()).Apply(Dafny.Sequence<RAST._IType>.FromElements(_2_T)), Dafny.Sequence<RAST._IImplMember>.FromElements()))))), RAST.Mod.create_Mod(RAST.__default.NoDoc, RAST.__default.NoAttr, Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"), Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), (RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("DafnyType")))), RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), _3_std__any__Any)), RAST.ModDecl.create_StructDecl(RAST.Struct.create(RAST.__default.NoDoc, Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.FromElements(), Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"), Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_1_T__Decl__simp), RAST.Fields.create_NamedFields(Dafny.Sequence<RAST._IField>.FromElements(RAST.Field.create(RAST.Visibility.create_PUB(), RAST.Formal.create(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("a"), _4_Any)))))), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_Impl(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_1_T__Decl__simp), (RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"))).Apply(Dafny.Sequence<RAST._IType>.FromElements(_2_T)), Dafny.Sequence<RAST._IImplMember>.FromElements())), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_1_T__Decl__simp), _4_Any, (RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"))).Apply(Dafny.Sequence<RAST._IType>.FromElements(_2_T)), Dafny.Sequence<RAST._IImplMember>.FromElements())))));
+      FactorPathsOptimizationTest.__default.ShouldBeEqual(Dafny.Helpers.Id<Func<RAST._IMod, RAST._IMod>>(FactorPathsOptimization.__default.apply(RAST.__default.crate))(RAST.Mod.create_Mod(RAST.__default.NoDoc, RAST.__default.NoAttr, Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"), Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_StructDecl(RAST.Struct.create(RAST.__default.NoDoc, Dafny.Sequence<RAST._IAttribute>.FromElements(), Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"), Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_0_T__Decl), RAST.Fields.create_NamedFields(Dafny.Sequence<RAST._IField>.FromElements(RAST.Field.create(RAST.Visibility.create_PUB(), RAST.Formal.create(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("a"), (_3_std__any__Any).AsType())))))), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_Impl(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_0_T__Decl), (RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"))).Apply(Dafny.Sequence<RAST._IType>.FromElements(_2_T)), Dafny.Sequence<RAST._IImplMember>.FromElements())), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_0_T__Decl), (_3_std__any__Any).AsType(), ((((RAST.__default.crate).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"))).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"))).AsType()).Apply(Dafny.Sequence<RAST._IType>.FromElements(_2_T)), Dafny.Sequence<RAST._IImplMember>.FromElements()))))), RAST.Mod.create_Mod(RAST.__default.NoDoc, RAST.__default.NoAttr, Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"), Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), (RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("DafnyType")))), RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), _3_std__any__Any)), RAST.ModDecl.create_StructDecl(RAST.Struct.create(RAST.__default.NoDoc, Dafny.Sequence<RAST._IAttribute>.FromElements(), Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"), Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_1_T__Decl__simp), RAST.Fields.create_NamedFields(Dafny.Sequence<RAST._IField>.FromElements(RAST.Field.create(RAST.Visibility.create_PUB(), RAST.Formal.create(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("a"), _4_Any)))))), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_Impl(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_1_T__Decl__simp), (RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"))).Apply(Dafny.Sequence<RAST._IType>.FromElements(_2_T)), Dafny.Sequence<RAST._IImplMember>.FromElements())), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_1_T__Decl__simp), _4_Any, (RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"))).Apply(Dafny.Sequence<RAST._IType>.FromElements(_2_T)), Dafny.Sequence<RAST._IImplMember>.FromElements())))));
       FactorPathsOptimizationTest.__default.ShouldBeEqual(Dafny.Helpers.Id<Func<RAST._IMod, RAST._IMod>>(FactorPathsOptimization.__default.apply(RAST.__default.crate))(RAST.Mod.create_Mod(RAST.__default.NoDoc, RAST.__default.NoAttr, Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"), Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_0_T__Decl), (((RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("UpcastObject"))).AsType()).Apply(Dafny.Sequence<RAST._IType>.FromElements(RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("x")))), (RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"))).Apply(Dafny.Sequence<RAST._IType>.FromElements(_2_T)), Dafny.Sequence<RAST._IImplMember>.FromElements()))))), RAST.Mod.create_Mod(RAST.__default.NoDoc, RAST.__default.NoAttr, Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"), Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), (RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("DafnyType")))), RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), (RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("UpcastObject")))), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_1_T__Decl__simp), (RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("UpcastObject"))).Apply(Dafny.Sequence<RAST._IType>.FromElements(RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("x")))), (RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"))).Apply(Dafny.Sequence<RAST._IType>.FromElements(_2_T)), Dafny.Sequence<RAST._IImplMember>.FromElements())))));
       FactorPathsOptimizationTest.__default.ShouldBeEqual(Dafny.Helpers.Id<Func<RAST._IMod, RAST._IMod>>(FactorPathsOptimization.__default.apply(RAST.__default.crate))(RAST.Mod.create_Mod(RAST.__default.NoDoc, RAST.__default.NoAttr, Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"), Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_ConstDecl(RAST.Constant.create(RAST.__default.NoDoc, RAST.__default.NoAttr, Dafny.Sequence<Dafny.Rune>.UnicodeFromString("dummy"), (_3_std__any__Any).AsType(), RAST.Expr.create_StmtExpr(RAST.Expr.create_DeclareVar(RAST.DeclareType.create_MUT(), Dafny.Sequence<Dafny.Rune>.UnicodeFromString("doit"), Std.Wrappers.Option<RAST._IType>.create_Some((RAST.__default.RcType).Apply1(RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("unknown")))), Std.Wrappers.Option<RAST._IExpr>.create_Some(((RAST.Expr.create_Identifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("something"))).ApplyType(Dafny.Sequence<RAST._IType>.FromElements(RAST.Type.create_DynType((RAST.__default.std__default__Default).AsType())))).Apply(Dafny.Sequence<RAST._IExpr>.FromElements(RAST.__default.std__default__Default__default, (((RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("rd!"))).AsExpr()).Apply1(RAST.Expr.create_Identifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("obj"))))))), RAST.Expr.create_TypeAscription(RAST.Expr.create_ExprFromType(((RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("DafnyString"))).AsType()), ((RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("DafnyType"))).AsType()))))))), RAST.Mod.create_Mod(RAST.__default.NoDoc, RAST.__default.NoAttr, Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"), Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), _3_std__any__Any)), RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), RAST.__default.RcPath)), RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), RAST.__default.std__default__Default)), RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), (RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("rd")))), RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), (RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("DafnyString")))), RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), (RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("DafnyType")))), RAST.ModDecl.create_ConstDecl(RAST.Constant.create(RAST.__default.NoDoc, RAST.__default.NoAttr, Dafny.Sequence<Dafny.Rune>.UnicodeFromString("dummy"), RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Any")), RAST.Expr.create_StmtExpr(RAST.Expr.create_DeclareVar(RAST.DeclareType.create_MUT(), Dafny.Sequence<Dafny.Rune>.UnicodeFromString("doit"), Std.Wrappers.Option<RAST._IType>.create_Some((RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Rc"))).Apply1(RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("unknown")))), Std.Wrappers.Option<RAST._IExpr>.create_Some(((RAST.Expr.create_Identifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("something"))).ApplyType(Dafny.Sequence<RAST._IType>.FromElements(RAST.Type.create_DynType(RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Default")))))).Apply(Dafny.Sequence<RAST._IExpr>.FromElements(((RAST.Expr.create_Identifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Default"))).FSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("default"))).Apply(Dafny.Sequence<RAST._IExpr>.FromElements()), (RAST.Expr.create_Identifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("rd!"))).Apply1(RAST.Expr.create_Identifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("obj"))))))), RAST.Expr.create_TypeAscription(RAST.Expr.create_ExprFromType(RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("DafnyString"))), RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("DafnyType")))))))));
       FactorPathsOptimizationTest.__default.ShouldBeEqual(Dafny.Helpers.Id<Func<RAST._IMod, RAST._IMod>>(FactorPathsOptimization.__default.apply(RAST.__default.crate))(RAST.Mod.create_Mod(RAST.__default.NoDoc, RAST.__default.NoAttr, Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"), Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_TraitDecl(RAST.Trait.create(RAST.__default.NoDoc, RAST.__default.NoAttr, Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(), RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Something")), Dafny.Sequence<RAST._IType>.FromElements(), Dafny.Sequence<RAST._IImplMember>.FromElements())), RAST.ModDecl.create_ConstDecl(RAST.Constant.create(RAST.__default.NoDoc, RAST.__default.NoAttr, Dafny.Sequence<Dafny.Rune>.UnicodeFromString("dummyExtern"), (((RAST.__default.crate).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("anothermodule"))).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Something"))).AsType(), RAST.Expr.create_RawExpr(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("nothing")))), RAST.ModDecl.create_ConstDecl(RAST.Constant.create(RAST.__default.NoDoc, RAST.__default.NoAttr, Dafny.Sequence<Dafny.Rune>.UnicodeFromString("dummyIntern"), (((RAST.__default.crate).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"))).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Something"))).AsType(), RAST.Expr.create_RawExpr(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("nothing"))))))), RAST.Mod.create_Mod(RAST.__default.NoDoc, RAST.__default.NoAttr, Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"), Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_TraitDecl(RAST.Trait.create(RAST.__default.NoDoc, RAST.__default.NoAttr, Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(), RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Something")), Dafny.Sequence<RAST._IType>.FromElements(), Dafny.Sequence<RAST._IImplMember>.FromElements())), RAST.ModDecl.create_ConstDecl(RAST.Constant.create(RAST.__default.NoDoc, RAST.__default.NoAttr, Dafny.Sequence<Dafny.Rune>.UnicodeFromString("dummyExtern"), (((RAST.__default.crate).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("anothermodule"))).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Something"))).AsType(), RAST.Expr.create_RawExpr(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("nothing")))), RAST.ModDecl.create_ConstDecl(RAST.Constant.create(RAST.__default.NoDoc, RAST.__default.NoAttr, Dafny.Sequence<Dafny.Rune>.UnicodeFromString("dummyIntern"), RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Something")), RAST.Expr.create_RawExpr(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("nothing")))))));

Source/DafnyCore/AST/TypeDeclarations/Declaration.cs

@@ -27,14 +27,14 @@
 
   private bool scopeIsInherited = false;
 
   protected Declaration(Cloner cloner, Declaration original) : base(cloner, original) {
     NameNode = original.NameNode.Clone(cloner);
     BodyStartTok = cloner.Origin(original.BodyStartTok);
     Attributes = cloner.CloneAttributes(original.Attributes);
   }
 
   [SyntaxConstructor]
   protected Declaration(IOrigin origin, Name nameNode, Attributes attributes) : base(origin) {
     Contract.Requires(origin != null);
     this.NameNode = nameNode;
     this.Attributes = attributes;
@@ -111,17 +111,42 @@
   protected string? sanitizedName;
   public virtual string SanitizedName => sanitizedName ??= NonglobalVariable.SanitizeName(Name);
 
+  protected string enclosingModuleName; // Computed at the same time as compileName
+
   protected string? compileName;
 
   public virtual string GetCompileName(DafnyOptions options) {
     if (compileName == null) {
-      this.IsExtern(options, out _, out compileName);
+      this.IsExtern(options, out var possibleEnclosingModuleName, out compileName);
+      if (!IsCompiled) {
+        enclosingModuleName = possibleEnclosingModuleName;
+      }
+      if (this is TopLevelDecl topDecl) {
+        enclosingModuleName ??= topDecl.EnclosingModuleDefinition.GetCompileName(options);
+      }
+
       compileName ??= SanitizedName;
     }
 
     return compileName;
   }
 
+  public bool IsCompiled {
+    get {
+      var compile = true;
+      return !Attributes.ContainsBool(Attributes, "compile", ref compile) || compile;
+    }
+  }
+
+  public string GetQualificationName(DafnyOptions options) {
+    if (compileName == null) {
+      GetCompileName(options); // Sets the enclosing module name if defined by externs.
+      return enclosingModuleName;
+    }
+
+    return enclosingModuleName;
+  }
+
   public Attributes? Attributes;  // readonly, except during class merging in the refinement transformations and when changed by Compiler.MarkCapitalizationConflict
   Attributes? IAttributeBearingDeclaration.Attributes {
     get => Attributes;