Skip to content

Commit

Permalink
Simplification to remove duplicate argument to CreateClass
Browse files Browse the repository at this point in the history
  • Loading branch information
@olivier-aws
olivier-aws committed Jan 8, 2025
1 parent 72d4da6 commit 9244f82
Show file tree
Hide file tree
Showing 8 changed files with 38 additions and 37 deletions.
10 changes: 5 additions & 5 deletions Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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<TypeParameter> typeParameters, TopLevelDecl cls, List<Type>/*?*/ 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;
Expand Down Expand Up @@ -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

Expand Down Expand Up @@ -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)");
Expand Down Expand Up @@ -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();
Expand Down
10 changes: 5 additions & 5 deletions Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -228,14 +228,14 @@ private string InstantiateTemplate(List<Type> 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<TypeParameter>/*?*/ typeParameters, TopLevelDecl cls, List<Type>/*?*/ superClasses, IOrigin tok, ConcreteSyntaxTree wr) {
var className = clName(cl);
protected override IClassWriter CreateClass(string moduleName, bool isExtern, string/*?*/ fullPrintName, List<TypeParameter>/*?*/ typeParameters, TopLevelDecl cls, List<Type>/*?*/ superClasses, IOrigin tok, ConcreteSyntaxTree wr) {
var className = clName(cls);
if (isExtern) {
throw new UnsupportedFeatureException(tok, Feature.ExternalClasses, String.Format("extern in class {0}", className));
}
Expand Down Expand Up @@ -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) {
Expand Down Expand Up @@ -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;

Expand Down
4 changes: 2 additions & 2 deletions Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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<TypeParameter> typeParameters, TopLevelDecl cls, List<Type> superClasses, IOrigin tok, ConcreteSyntaxTree wr) {
if (currentBuilder is ClassContainer builder) {
List<DAST.TypeArgDecl> 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 {
Expand Down
14 changes: 7 additions & 7 deletions Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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<TypeParameter> typeParameters, TopLevelDecl cls, List<Type>/*?*/ 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<TypeParameter>/*?*/ typeParameters, List<Type>/*?*/ superClasses, IOrigin tok, ConcreteSyntaxTree wr, bool includeRtd, bool includeEquals, bool includeString) {
private GoCodeGenerator.ClassWriter CreateClass(TopLevelDecl classContext, bool isExtern, string/*?*/ fullPrintName, List<TypeParameter>/*?*/ typeParameters, List<Type>/*?*/ 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 {
Expand Down Expand Up @@ -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);

Expand Down Expand Up @@ -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{}");
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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);
Expand Down
8 changes: 4 additions & 4 deletions Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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();
Expand Down Expand Up @@ -870,9 +870,9 @@ protected override string TypeName_UDT(string fullCompileName, List<TypeParamete
// }
// }
//
protected override IClassWriter CreateClass(string moduleName, TopLevelDecl cl, bool isExtern, string /*?*/ fullPrintName,
protected override IClassWriter CreateClass(string moduleName, bool isExtern, string /*?*/ fullPrintName,
List<TypeParameter> typeParameters, TopLevelDecl cls, List<Type> /*?*/ 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);
Expand Down Expand Up @@ -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);
Expand Down
10 changes: 5 additions & 5 deletions Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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<TypeParameter> typeParameters, TopLevelDecl cls, List<Type>/*?*/ 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 = "";
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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)");
Expand Down Expand Up @@ -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;
Expand Down
8 changes: 4 additions & 4 deletions Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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<TypeParameter> typeParameters, TopLevelDecl cls, List<Type> superClasses, IOrigin tok, ConcreteSyntaxTree wr) {
var realSuperClasses = superClasses?.Where(trait => !trait.IsObject).ToList() ?? new List<Type>();
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();
Expand Down Expand Up @@ -277,7 +277,7 @@ protected override IClassWriter CreateTrait(string name, bool isExtern, List<Typ
}

protected override ConcreteSyntaxTree CreateIterator(IteratorDecl iter, ConcreteSyntaxTree wr) {
var cw = (ClassWriter)CreateClass(PublicModuleIdProtect(iter.EnclosingModuleDefinition.GetCompileName(Options)), iter, false,
var cw = (ClassWriter)CreateClass(PublicModuleIdProtect(iter.EnclosingModuleDefinition.GetCompileName(Options)), false,
iter.FullName, iter.TypeArgs, iter, null, iter.Origin, wr);
var constructorWriter = cw.ConstructorWriter;
var w = cw.MethodWriter;
Expand Down Expand Up @@ -459,7 +459,7 @@ private string DtCtorDeclarationName(DatatypeCtor ctor, bool full = false) {
protected IClassWriter DeclareType(TopLevelDecl d, SubsetTypeDecl.WKind witnessKind, Expression witness, ConcreteSyntaxTree wr) {
Contract.Requires(d is SubsetTypeDecl or NewtypeDecl);

var cw = (ClassWriter)CreateClass(IdProtect(d.EnclosingModuleDefinition.GetCompileName(Options)), d, d, wr);
var cw = (ClassWriter)CreateClass(IdProtect(d.EnclosingModuleDefinition.GetCompileName(Options)), d, wr);
var w = cw.MethodWriter;
var udt = UserDefinedType.FromTopLevelDecl(d.Origin, d);
w.WriteLine("@staticmethod");
Expand Down
11 changes: 6 additions & 5 deletions Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -218,15 +218,15 @@ protected interface IClassWriter {
protected virtual bool SupportsStaticsInGenericClasses => 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);
}

/// <summary>
/// "tok" can be "null" if "superClasses" is.
/// </summary>
protected abstract IClassWriter CreateClass(string moduleName, TopLevelDecl cl, bool isExtern, string/*?*/ fullPrintName,
protected abstract IClassWriter CreateClass(string moduleName, bool isExtern, string/*?*/ fullPrintName,
List<TypeParameter> typeParameters, TopLevelDecl cls, List<Type>/*?*/ superClasses, IOrigin tok, ConcreteSyntaxTree wr);

/// <summary>
Expand Down Expand Up @@ -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);
Expand All @@ -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);
Expand Down

0 comments on commit 9244f82

Please sign in to comment.