diff --git a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs index c945b8e100..1afe19c97c 100644 --- a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs +++ b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs @@ -331,9 +331,9 @@ string PrintVariance(TypeParameter.TPVariance variance) { return $"<{targs.Comma(PrintTypeParameter)}>"; } - protected override IClassWriter CreateClass(string moduleName, TopLevelDecl tl, bool isExtern, string /*?*/ fullPrintName, + protected override IClassWriter CreateClass(string moduleName, bool isExtern, string /*?*/ fullPrintName, List typeParameters, TopLevelDecl cls, List/*?*/ superClasses, IOrigin tok, ConcreteSyntaxTree wr) { - var name = className(tl); + var name = className(cls); var wBody = WriteTypeHeader("partial class", name, typeParameters, superClasses, tok, wr); ConcreteSyntaxTree/*?*/ wCtorBody = null; @@ -469,7 +469,7 @@ protected override ConcreteSyntaxTree CreateIterator(IteratorDecl iter, Concrete // } // } - var cw = (ClassWriter)CreateClass(IdProtect(iter.EnclosingModuleDefinition.GetCompileName(Options)), iter, iter, wr); + var cw = (ClassWriter)CreateClass(IdProtect(iter.EnclosingModuleDefinition.GetCompileName(Options)), iter, wr); var w = cw.InstanceMemberWriter; // here come the fields @@ -1262,7 +1262,7 @@ string DtCreateName(DatatypeCtor ctor) { } protected override IClassWriter DeclareNewtype(NewtypeDecl nt, ConcreteSyntaxTree wr) { - var cw = (ClassWriter)CreateClass(IdProtect(nt.EnclosingModuleDefinition.GetCompileName(Options)), nt, nt, wr); + var cw = (ClassWriter)CreateClass(IdProtect(nt.EnclosingModuleDefinition.GetCompileName(Options)), nt, wr); var w = cw.StaticMemberWriter; if (nt.NativeType != null) { var wEnum = w.NewBlock($"public static System.Collections.Generic.IEnumerable<{GetNativeTypeName(nt.NativeType)}> IntegerRange(BigInteger lo, BigInteger hi)"); @@ -1331,7 +1331,7 @@ void DeclareBoxedNewtype(NewtypeDecl nt, ConcreteSyntaxTree wr) { } protected override void DeclareSubsetType(SubsetTypeDecl sst, ConcreteSyntaxTree wr) { - var cw = (ClassWriter)CreateClass(IdProtect(sst.EnclosingModuleDefinition.GetCompileName(Options)), sst, sst, wr); + var cw = (ClassWriter)CreateClass(IdProtect(sst.EnclosingModuleDefinition.GetCompileName(Options)), sst, wr); if (sst.WitnessKind == SubsetTypeDecl.WKind.Compiled) { var sw = new ConcreteSyntaxTree(cw.InstanceMemberWriter.RelativeIndentLevel); var wStmts = cw.InstanceMemberWriter.Fork(); diff --git a/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs b/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs index dbf8d2c275..80f74a2071 100644 --- a/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs +++ b/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs @@ -228,14 +228,14 @@ private string InstantiateTemplate(List typeArgs) { private string clName(TopLevelDecl cl) { var className = IdName(cl); - if (className == "__default" || true) { + if (cl is ClassDecl || cl is DefaultClassDecl) { return className; } return "class_" + className; } - protected override IClassWriter CreateClass(string moduleName, TopLevelDecl cl, bool isExtern, string/*?*/ fullPrintName, List/*?*/ typeParameters, TopLevelDecl cls, List/*?*/ superClasses, IOrigin tok, ConcreteSyntaxTree wr) { - var className = clName(cl); + protected override IClassWriter CreateClass(string moduleName, bool isExtern, string/*?*/ fullPrintName, List/*?*/ typeParameters, TopLevelDecl cls, List/*?*/ superClasses, IOrigin tok, ConcreteSyntaxTree wr) { + var className = clName(cls); if (isExtern) { throw new UnsupportedFeatureException(tok, Feature.ExternalClasses, String.Format("extern in class {0}", className)); } @@ -624,7 +624,7 @@ protected override IClassWriter DeclareNewtype(NewtypeDecl nt, ConcreteSyntaxTre } else { throw new UnsupportedFeatureException(nt.Origin, Feature.NonNativeNewtypes); } - var cw = CreateClass(nt.EnclosingModuleDefinition.GetCompileName(Options), nt, nt, wr) as ClassWriter; + var cw = CreateClass(nt.EnclosingModuleDefinition.GetCompileName(Options), nt, wr) as ClassWriter; var className = clName(nt); var w = cw.MethodDeclWriter; if (nt.WitnessKind == SubsetTypeDecl.WKind.Compiled) { @@ -662,7 +662,7 @@ protected override void DeclareSubsetType(SubsetTypeDecl sst, ConcreteSyntaxTree this.modDeclWr.WriteLine("{0} using {1} = {2};", templateDecl, IdName(sst), TypeName(sst.Var.Type, wr, sst.Origin)); - var cw = CreateClass(sst.EnclosingModuleDefinition.GetCompileName(Options), sst, sst, wr) as ClassWriter; + var cw = CreateClass(sst.EnclosingModuleDefinition.GetCompileName(Options), sst, wr) as ClassWriter; var className = clName(sst); var w = cw.MethodDeclWriter; diff --git a/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs b/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs index 80b8b9e45f..ba17c4a4d1 100644 --- a/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs +++ b/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs @@ -193,13 +193,13 @@ protected override ConcreteSyntaxTree EmitCoercionIfNecessary(Type from, Type to } } - protected override IClassWriter CreateClass(string moduleName, TopLevelDecl cl, bool isExtern, string fullPrintName, + protected override IClassWriter CreateClass(string moduleName, bool isExtern, string fullPrintName, List typeParameters, TopLevelDecl cls, List superClasses, IOrigin tok, ConcreteSyntaxTree wr) { if (currentBuilder is ClassContainer builder) { List typeParams = typeParameters.Select(tp => GenTypeArgDecl(tp)).ToList(); return new ClassWriter(this, typeParams.Count > 0, builder.Class( - IdName(cl), moduleName, typeParams, superClasses.Select(t => GenType(t)).ToList(), + IdName(cls), moduleName, typeParams, superClasses.Select(t => GenType(t)).ToList(), ParseAttributes(cls.Attributes), GetDocString(cls)) ); } else { diff --git a/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs b/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs index 0f854146b7..953f7d4347 100644 --- a/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs +++ b/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs @@ -329,16 +329,16 @@ private void EmitImport(Import import, ConcreteSyntaxTree importWriter, Concrete private string HelperModulePrefix => ModuleName == "dafny" ? "" : $"{GetHelperModuleName()}."; - protected override IClassWriter CreateClass(string moduleName, TopLevelDecl cl, bool isExtern, string/*?*/ fullPrintName, + protected override IClassWriter CreateClass(string moduleName, bool isExtern, string/*?*/ fullPrintName, List typeParameters, TopLevelDecl cls, List/*?*/ superClasses, IOrigin tok, ConcreteSyntaxTree wr) { var isDefaultClass = cls is DefaultClassDecl; bool isSequence = superClasses.Any(superClass => superClass is UserDefinedType udt && IsDafnySequence(udt.ResolvedClass)); - return CreateClass(cls, cl, isExtern, fullPrintName, typeParameters, superClasses, tok, wr, includeRtd: !isDefaultClass, includeEquals: !isSequence, includeString: !isSequence); + return CreateClass(cls, isExtern, fullPrintName, typeParameters, superClasses, tok, wr, includeRtd: !isDefaultClass, includeEquals: !isSequence, includeString: !isSequence); } // TODO Consider splitting this into two functions; most things seem to be passing includeRtd: false, includeEquals: false and includeString: true. - private GoCodeGenerator.ClassWriter CreateClass(TopLevelDecl classContext, TopLevelDecl cl, bool isExtern, string/*?*/ fullPrintName, List/*?*/ typeParameters, List/*?*/ superClasses, IOrigin tok, ConcreteSyntaxTree wr, bool includeRtd, bool includeEquals, bool includeString) { + private GoCodeGenerator.ClassWriter CreateClass(TopLevelDecl classContext, bool isExtern, string/*?*/ fullPrintName, List/*?*/ typeParameters, List/*?*/ superClasses, IOrigin tok, ConcreteSyntaxTree wr, bool includeRtd, bool includeEquals, bool includeString) { // See docs/Compilation/ReferenceTypes.md for a description of how instance members of classes and traits are compiled into Go. // // func New_Class_(Type0 _dafny.TypeDescriptor, Type1 _dafny.TypeDescriptor) *Class { @@ -382,7 +382,7 @@ private GoCodeGenerator.ClassWriter CreateClass(TopLevelDecl classContext, TopLe // return "module.Class" // } // - var name = Capitalize(IdName(cl)); + var name = Capitalize(IdName(classContext)); var w = CreateDescribedSection("class {0}", wr, name); @@ -586,7 +586,7 @@ protected override ConcreteSyntaxTree CreateIterator(IteratorDecl iter, Concrete // // break becomes: // return // }() - var cw = CreateClass(iter, iter, false, null, iter.TypeArgs, null, null, wr, includeRtd: false, includeEquals: false, includeString: true); + var cw = CreateClass(iter, false, null, iter.TypeArgs, null, null, wr, includeRtd: false, includeEquals: false, includeString: true); cw.InstanceFieldWriter.WriteLine("cont chan<- struct{}"); cw.InstanceFieldWriter.WriteLine("yielded <-chan struct{}"); @@ -1084,7 +1084,7 @@ string StructOfCtor(DatatypeCtor ctor) { } protected override IClassWriter DeclareNewtype(NewtypeDecl nt, ConcreteSyntaxTree wr) { - var cw = CreateClass(nt, nt, false, null, nt.TypeArgs, + var cw = CreateClass(nt, false, null, nt.TypeArgs, nt.ParentTypeInformation.UniqueParentTraits(), null, wr, includeRtd: false, includeEquals: false, includeString: true); var w = cw.ConcreteMethodWriter; var nativeType = nt.NativeType != null ? GetNativeTypeName(nt.NativeType) : null; @@ -1130,7 +1130,7 @@ protected override IClassWriter DeclareNewtype(NewtypeDecl nt, ConcreteSyntaxTre } protected override void DeclareSubsetType(SubsetTypeDecl sst, ConcreteSyntaxTree wr) { - var cw = CreateClass(sst, sst, false, null, sst.TypeArgs, null, null, wr, includeRtd: false, includeEquals: false, includeString: true); + var cw = CreateClass(sst, false, null, sst.TypeArgs, null, null, wr, includeRtd: false, includeEquals: false, includeString: true); var w = cw.ConcreteMethodWriter; if (sst.WitnessKind == SubsetTypeDecl.WKind.Compiled) { var witness = new ConcreteSyntaxTree(w.RelativeIndentLevel); diff --git a/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs b/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs index e71ef393c2..88a80e524e 100644 --- a/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs +++ b/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs @@ -373,7 +373,7 @@ protected override void FinishModule() { } protected override void DeclareSubsetType(SubsetTypeDecl sst, ConcreteSyntaxTree wr) { - var cw = (ClassWriter)CreateClass(IdProtect(sst.EnclosingModuleDefinition.GetCompileName(Options)), sst, sst, wr); + var cw = (ClassWriter)CreateClass(IdProtect(sst.EnclosingModuleDefinition.GetCompileName(Options)), sst, wr); if (sst.WitnessKind == SubsetTypeDecl.WKind.Compiled) { var sw = new ConcreteSyntaxTree(cw.InstanceMemberWriter.RelativeIndentLevel); var wStmts = cw.InstanceMemberWriter.Fork(); @@ -870,9 +870,9 @@ protected override string TypeName_UDT(string fullCompileName, List typeParameters, TopLevelDecl cls, List /*?*/ superClasses, IOrigin tok, ConcreteSyntaxTree wr) { - var name = IdName(cl); + var name = IdName(cls); var javaName = isExtern ? FormatExternBaseClassName(name) : name; var filename = $"{ModulePath}/{javaName}.java"; var w = wr.NewFile(filename); @@ -3602,7 +3602,7 @@ protected override void EmitHalt(IOrigin tok, Expression messageExpr, ConcreteSy } protected override IClassWriter DeclareNewtype(NewtypeDecl nt, ConcreteSyntaxTree wr) { - var cw = (ClassWriter)CreateClass(IdProtect(nt.EnclosingModuleDefinition.GetCompileName(Options)), nt, nt, wr); + var cw = (ClassWriter)CreateClass(IdProtect(nt.EnclosingModuleDefinition.GetCompileName(Options)), nt, wr); var w = cw.StaticMemberWriter; if (nt.NativeType != null) { var nativeType = GetBoxedNativeTypeName(nt.NativeType); diff --git a/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs b/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs index 2ce752f965..a75fd312f4 100644 --- a/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs +++ b/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs @@ -90,9 +90,9 @@ protected override ConcreteSyntaxTree CreateModule(ModuleDefinition module, stri protected override string GetHelperModuleName() => "_dafny"; - protected override IClassWriter CreateClass(string moduleName, TopLevelDecl cl, bool isExtern, string/*?*/ fullPrintName, + protected override IClassWriter CreateClass(string moduleName, bool isExtern, string/*?*/ fullPrintName, List typeParameters, TopLevelDecl cls, List/*?*/ superClasses, IOrigin tok, ConcreteSyntaxTree wr) { - var name = IdName(cl); + var name = IdName(cls); var w = wr.NewBlock(string.Format("$module.{0} = class {0}" + (isExtern ? " extends $module.{0}" : ""), name), ";"); w.Write("constructor ("); var sep = ""; @@ -161,7 +161,7 @@ protected override ConcreteSyntaxTree CreateIterator(IteratorDecl iter, Concrete // } // } - var cw = CreateClass(IdProtect(iter.EnclosingModuleDefinition.GetCompileName(Options)), iter, iter, wr) as JavaScriptCodeGenerator.ClassWriter; + var cw = CreateClass(IdProtect(iter.EnclosingModuleDefinition.GetCompileName(Options)), iter, wr) as JavaScriptCodeGenerator.ClassWriter; var w = cw.MethodWriter; var instanceFieldsWriter = cw.FieldWriter; // here come the fields @@ -576,7 +576,7 @@ protected override ConcreteSyntaxTree CreateIterator(IteratorDecl iter, Concrete } protected override IClassWriter DeclareNewtype(NewtypeDecl nt, ConcreteSyntaxTree wr) { - var cw = (ClassWriter)CreateClass(IdProtect(nt.EnclosingModuleDefinition.GetCompileName(Options)), nt, nt, wr); + var cw = (ClassWriter)CreateClass(IdProtect(nt.EnclosingModuleDefinition.GetCompileName(Options)), nt, wr); var w = cw.MethodWriter; if (nt.NativeType != null) { var wIntegerRangeBody = w.NewBlock("static *IntegerRange(lo, hi)"); @@ -639,7 +639,7 @@ void GenerateIsMethod(RedirectingTypeDecl declWithConstraints, ConcreteSyntaxTre } protected override void DeclareSubsetType(SubsetTypeDecl sst, ConcreteSyntaxTree wr) { - var cw = (ClassWriter)CreateClass(IdProtect(sst.EnclosingModuleDefinition.GetCompileName(Options)), sst, sst, wr); + var cw = (ClassWriter)CreateClass(IdProtect(sst.EnclosingModuleDefinition.GetCompileName(Options)), sst, wr); var w = cw.MethodWriter; var udt = UserDefinedType.FromTopLevelDecl(sst.Origin, sst); string d; diff --git a/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs b/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs index f322c10823..e95837a998 100644 --- a/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs +++ b/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs @@ -231,13 +231,13 @@ private static string MangleName(string name) { return name; } - protected override IClassWriter CreateClass(string moduleName, TopLevelDecl cl, bool isExtern, string/*?*/ fullPrintName, + protected override IClassWriter CreateClass(string moduleName, bool isExtern, string/*?*/ fullPrintName, List typeParameters, TopLevelDecl cls, List superClasses, IOrigin tok, ConcreteSyntaxTree wr) { var realSuperClasses = superClasses?.Where(trait => !trait.IsObject).ToList() ?? new List(); var baseClasses = realSuperClasses.Any() ? $"({realSuperClasses.Comma(trait => TypeName(trait, wr, tok))})" : ""; - var name = IdName(cl); + var name = IdName(cls); var methodWriter = wr.NewBlockPy(header: $"class {IdProtect(name)}{baseClasses}:"); var relevantTypeParameters = typeParameters.Where(NeedsTypeDescriptor).ToList(); @@ -277,7 +277,7 @@ protected override IClassWriter CreateTrait(string name, bool isExtern, List true; protected virtual bool TraitRepeatsInheritedDeclarations => false; protected virtual bool InstanceMethodsAllowedToCallTraitMethods => true; - protected IClassWriter CreateClass(string moduleName, TopLevelDecl cl, TopLevelDecl cls, ConcreteSyntaxTree wr) { - return CreateClass(moduleName, cl, false, null, cls.TypeArgs, + protected IClassWriter CreateClass(string moduleName, TopLevelDecl cls, ConcreteSyntaxTree wr) { + return CreateClass(moduleName, false, null, cls.TypeArgs, cls, (cls as TopLevelDeclWithMembers)?.ParentTypeInformation.UniqueParentTraits(), null, wr); } /// /// "tok" can be "null" if "superClasses" is. /// - protected abstract IClassWriter CreateClass(string moduleName, TopLevelDecl cl, bool isExtern, string/*?*/ fullPrintName, + protected abstract IClassWriter CreateClass(string moduleName, bool isExtern, string/*?*/ fullPrintName, List typeParameters, TopLevelDecl cls, List/*?*/ superClasses, IOrigin tok, ConcreteSyntaxTree wr); /// @@ -1684,8 +1684,8 @@ private void EmitModule(Program program, ConcreteSyntaxTree programNode, ModuleD var (classIsExtern, include) = GetIsExternAndIncluded(defaultClassDecl); if (include) { + // HERE: was using IdName(defaultClassDecl) as name, now using clName(defaultClassDecl) var cw = CreateClass(IdProtect(d.EnclosingModuleDefinition.GetCompileName(Options)), - defaultClassDecl, classIsExtern, defaultClassDecl.FullName, defaultClassDecl.TypeArgs, defaultClassDecl, defaultClassDecl.ParentTypeInformation.UniqueParentTraits(), defaultClassDecl.Origin, wr); @@ -1700,7 +1700,8 @@ private void EmitModule(Program program, ConcreteSyntaxTree programNode, ModuleD var (classIsExtern, include) = GetIsExternAndIncluded(cl); if (include) { - var cw = CreateClass(IdProtect(d.EnclosingModuleDefinition.GetCompileName(Options)), cl, + // HERE: was using IdName(cl) as name, now using clName(cl) + var cw = CreateClass(IdProtect(d.EnclosingModuleDefinition.GetCompileName(Options)), classIsExtern, cl.FullName, cl.TypeArgs, cl, cl.ParentTypeInformation.UniqueParentTraits(), cl.Origin, wr); CompileClassMembers(program, cl, cw);