Skip to content

Commit

Permalink
Back-porting of #5676
Browse files Browse the repository at this point in the history
  • Loading branch information
@MikaelMayer
MikaelMayer committed Aug 8, 2024
1 parent 8b78ef5 commit 2412e86
Show file tree
Hide file tree
Showing 35 changed files with 7,257 additions and 7,712 deletions.
198 changes: 99 additions & 99 deletions Source/DafnyCore.Test/GeneratedFromDafny/DafnyToRustCompilerCoverage_RASTCoverage.cs
View file

Large diffs are not rendered by default.

36 changes: 12 additions & 24 deletions Source/DafnyCore.Test/GeneratedFromDafny/FactorPathsOptimizationTest.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,31 +14,19 @@ namespace FactorPathsOptimizationTest {
public partial class __default {
public static void TestApply()
{
RAST._ITypeParamDecl _1246_T__Decl;
_1246_T__Decl = RAST.TypeParamDecl.create(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("T"), Dafny.Sequence<RAST._IType>.FromElements(RAST.__default.DafnyType));
RAST._ITypeParamDecl _1247_T__Decl__simp;
_1247_T__Decl__simp = RAST.TypeParamDecl.create(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("T"), Dafny.Sequence<RAST._IType>.FromElements(RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("DafnyType"))));
RAST._IType _1248_T;
_1248_T = RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("T"));
RAST._IPath _1249_std__any__Any;
_1249_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 _1250_Any;
_1250_Any = RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Any"));
Dafny.ISequence<Dafny.Rune> _1251___e00 = (FactorPathsOptimization.__default.apply(RAST.Mod.create_Mod(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"), Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_StructDecl(RAST.Struct.create(Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.FromElements(), Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"), Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_1246_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"), (_1249_std__any__Any).AsType())))))), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_Impl(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_1246_T__Decl), (RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"))).Apply(Dafny.Sequence<RAST._IType>.FromElements(_1248_T)), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""), Dafny.Sequence<RAST._IImplMember>.FromElements())), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_1246_T__Decl), (_1249_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(_1248_T)), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""), Dafny.Sequence<RAST._IImplMember>.FromElements()))))))._ToString(Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""));
Dafny.ISequence<Dafny.Rune> _1252___e10 = (RAST.Mod.create_Mod(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"), Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), _1249_std__any__Any)), RAST.ModDecl.create_StructDecl(RAST.Struct.create(Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.FromElements(), Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"), Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_1247_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"), _1250_Any)))))), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_Impl(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_1247_T__Decl__simp), (RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"))).Apply(Dafny.Sequence<RAST._IType>.FromElements(_1248_T)), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""), Dafny.Sequence<RAST._IImplMember>.FromElements())), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_1247_T__Decl__simp), _1250_Any, (RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"))).Apply(Dafny.Sequence<RAST._IType>.FromElements(_1248_T)), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""), Dafny.Sequence<RAST._IImplMember>.FromElements())))))._ToString(Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""));
if (!((_1251___e00).Equals(_1252___e10))) {
Dafny.Helpers.Print((Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Left:\n")));
Dafny.Helpers.Print((_1251___e00).ToVerbatimString(false));
Dafny.Helpers.Print((Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Right:\n")));
Dafny.Helpers.Print((_1252___e10).ToVerbatimString(false));
RAST._ITypeParamDecl _0_T__Decl;
_0_T__Decl = RAST.TypeParamDecl.create(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("T"), Dafny.Sequence<RAST._IType>.FromElements(RAST.__default.DafnyType));
RAST._ITypeParamDecl _1_T__Decl__simp;
_1_T__Decl__simp = RAST.TypeParamDecl.create(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("T"), Dafny.Sequence<RAST._IType>.FromElements(RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("DafnyType"))));
RAST._IType _2_T;
_2_T = RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("T"));
RAST._IPath _3_std__any__Any;
_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"));
if (!(((FactorPathsOptimization.__default.apply(RAST.Mod.create_Mod(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"), Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.FromElements(), Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_StructDecl(RAST.Struct.create(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<Dafny.Rune>.UnicodeFromString(""), 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<Dafny.Rune>.UnicodeFromString(""), Dafny.Sequence<RAST._IImplMember>.FromElements()))))))._ToString(Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""))).Equals((RAST.Mod.create_Mod(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"), Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.FromElements(), Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), _3_std__any__Any)), RAST.ModDecl.create_StructDecl(RAST.Struct.create(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<Dafny.Rune>.UnicodeFromString(""), 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<Dafny.Rune>.UnicodeFromString(""), Dafny.Sequence<RAST._IImplMember>.FromElements())))))._ToString(Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""))))) {
throw new Dafny.HaltException("Backends/Rust/Dafny-compiler-rust-path-simplification.dfy(12,4): " + Dafny.Sequence<Dafny.Rune>.UnicodeFromString("expectation violation").ToVerbatimString(false));}
Dafny.ISequence<Dafny.Rune> _1253___e01 = (FactorPathsOptimization.__default.apply(RAST.Mod.create_Mod(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"), Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_1246_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(_1248_T)), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""), Dafny.Sequence<RAST._IImplMember>.FromElements()))))))._ToString(Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""));
Dafny.ISequence<Dafny.Rune> _1254___e11 = (RAST.Mod.create_Mod(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("UpcastObject")))), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_1247_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(_1248_T)), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""), Dafny.Sequence<RAST._IImplMember>.FromElements())))))._ToString(Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""));
if (!((_1253___e01).Equals(_1254___e11))) {
Dafny.Helpers.Print((Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Left:\n")));
Dafny.Helpers.Print((_1253___e01).ToVerbatimString(false));
Dafny.Helpers.Print((Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Right:\n")));
Dafny.Helpers.Print((_1254___e11).ToVerbatimString(false));
if (!(((FactorPathsOptimization.__default.apply(RAST.Mod.create_Mod(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"), Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.FromElements(), 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<Dafny.Rune>.UnicodeFromString(""), Dafny.Sequence<RAST._IImplMember>.FromElements()))))))._ToString(Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""))).Equals((RAST.Mod.create_Mod(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"), Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.FromElements(), 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("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<Dafny.Rune>.UnicodeFromString(""), Dafny.Sequence<RAST._IImplMember>.FromElements())))))._ToString(Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""))))) {
throw new Dafny.HaltException("Backends/Rust/Dafny-compiler-rust-path-simplification.dfy(29,4): " + Dafny.Sequence<Dafny.Rune>.UnicodeFromString("expectation violation").ToVerbatimString(false));}
}
}
Expand Down
4 changes: 2 additions & 2 deletions Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -163,7 +163,7 @@ protected override void EmitBuiltInDecls(SystemModuleManager systemModuleManager
wr.WriteLine("#if ISDAFNYRUNTIMELIB");
}

var dafnyNamespace = CreateModule("Dafny", false, null, null, wr);
var dafnyNamespace = CreateModule("Dafny", false, null, null, null, wr);
EmitInitNewArrays(systemModuleManager, dafnyNamespace);
if (Synthesize) {
CsharpSynthesizer.EmitMultiMatcher(dafnyNamespace);
Expand Down Expand Up @@ -269,7 +269,7 @@ string IdProtectModule(string moduleName) {
}

protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, ModuleDefinition externModule,
string libraryName /*?*/, ConcreteSyntaxTree wr) {
string libraryName /*?*/, Attributes moduleAttributes, ConcreteSyntaxTree wr) {
moduleName = IdProtectModule(moduleName);
return wr.NewBlock($"namespace {moduleName}", " // end of " + $"namespace {moduleName}");
}
Expand Down
2 changes: 1 addition & 1 deletion Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -160,7 +160,7 @@ protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string a
}

protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, ModuleDefinition externModule,
string libraryName /*?*/, ConcreteSyntaxTree wr) {
string libraryName /*?*/, Attributes moduleAttributes, ConcreteSyntaxTree wr) {
var s = $"namespace {IdProtect(moduleName)} ";
string footer = "// end of " + s + " declarations";
this.modDeclWr = this.modDeclsWr.NewBlock(s, footer);
Expand Down
1 change: 1 addition & 0 deletions Source/DafnyCore/Backends/Dafny/AST.dfy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -202,6 +202,7 @@ module {:extern "DAST"} DAST {
datatype Formal = Formal(name: VarName, typ: Type, attributes: seq<Attribute>)

datatype Method = Method(
attributes: seq<Attribute>,
isStatic: bool,
hasBody: bool,
outVarsAreUninitFieldsToAssign: bool, // For constructors
Expand Down
15 changes: 9 additions & 6 deletions Source/DafnyCore/Backends/Dafny/ASTBuilder.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -365,15 +365,14 @@ interface ClassLike {

void AddField(DAST.Formal item, _IOption<DAST._IExpression> defaultValue);

public MethodBuilder Method(
bool isStatic, bool hasBody, bool outVarsAreUninitFieldsToAssign, bool wasFunction,
public MethodBuilder Method(bool isStatic, bool hasBody, bool outVarsAreUninitFieldsToAssign, bool wasFunction,
ISequence<ISequence<Rune>> overridingPath,
ISequence<_IAttribute> attributes,
string name,
List<DAST.TypeArgDecl> typeArgs,
List<TypeArgDecl> typeArgs,
Sequence<DAST.Formal> params_,
List<DAST.Type> outTypes, List<ISequence<Rune>> outVars
) {
return new MethodBuilder(this, isStatic, hasBody, outVarsAreUninitFieldsToAssign, wasFunction, overridingPath, name, typeArgs, params_, outTypes, outVars);
List<DAST.Type> outTypes, List<ISequence<Rune>> outVars) {
return new MethodBuilder(this, isStatic, hasBody, outVarsAreUninitFieldsToAssign, wasFunction, overridingPath, attributes, name, typeArgs, params_, outTypes, outVars);
}

public object Finish();
Expand All @@ -392,11 +391,13 @@ class MethodBuilder : StatementContainer {
readonly List<DAST.Type> outTypes;
readonly List<ISequence<Rune>> outVars;
readonly List<object> body = new();
private ISequence<_IAttribute> attributes;

public MethodBuilder(
ClassLike parent,
bool isStatic, bool hasBody, bool outVarsAreUninitFieldsToAssign, bool wasFunction,
ISequence<ISequence<Rune>> overridingPath,
ISequence<_IAttribute> attributes,
string name,
List<DAST.TypeArgDecl> typeArgs,
Sequence<DAST.Formal> params_,
Expand All @@ -408,6 +409,7 @@ public MethodBuilder(
this.outVarsAreUninitFieldsToAssign = outVarsAreUninitFieldsToAssign;
this.wasFunction = wasFunction;
this.overridingPath = overridingPath;
this.attributes = attributes;
this.name = name;
this.typeArgs = typeArgs;
this.params_ = params_;
Expand All @@ -434,6 +436,7 @@ public DAST.Method Build() {
StatementContainer.RecursivelyBuild(body, builtStatements);

return (DAST.Method)DAST.Method.create(
attributes,
isStatic,
hasBody,
outVarsAreUninitFieldsToAssign,
Expand Down
13 changes: 10 additions & 3 deletions Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -126,9 +126,9 @@ private bool NeedsExternalImport(MemberDecl memberDecl) {
}

protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, ModuleDefinition externModule,
string libraryName, ConcreteSyntaxTree wr) {
string libraryName, Attributes moduleAttributes, ConcreteSyntaxTree wr) {
if (currentBuilder is ModuleContainer moduleBuilder) {
var attributes = (Sequence<DAST.Attribute>)Sequence<DAST.Attribute>.Empty;
var attributes = (Sequence<DAST.Attribute>)ParseAttributes(moduleAttributes);
if (externModule != null) {
attributes = (Sequence<DAST.Attribute>)ParseAttributes(externModule.Attributes);
}
Expand Down Expand Up @@ -552,9 +552,12 @@ public ConcreteSyntaxTree CreateMethod(Method m, List<TypeArgumentInstantiation>
GenType(md.GetType())
).ToList();*/
}

var attributes = compiler.ParseAttributes(m.Attributes);
var builder = this.builder.Method(
m.IsStatic, createBody, m is Constructor, false,
overridingTrait != null ? compiler.PathFromTopLevel(overridingTrait) : null,
attributes,
m.GetCompileName(compiler.Options),
astTypeArgs, params_,
outTypes, outVars
Expand Down Expand Up @@ -587,10 +590,11 @@ public ConcreteSyntaxTree CreateFunction(string name, List<TypeArgumentInstantia
var params_ = compiler.GenFormals(formals);

var overridingTrait = member.OverriddenMember?.EnclosingClass;

var attributes = compiler.ParseAttributes(member.Attributes);
var builder = this.builder.Method(
isStatic, createBody, false, true,
overridingTrait != null ? compiler.PathFromTopLevel(overridingTrait) : null,
attributes,
name,
astTypeArgs, params_,
new() {
Expand All @@ -614,10 +618,13 @@ public ConcreteSyntaxTree CreateGetter(string name, TopLevelDecl enclosingDecl,
}

var overridingTrait = member.OverriddenMember?.EnclosingClass;

var attributes = compiler.ParseAttributes(enclosingDecl.Attributes);

var builder = this.builder.Method(
isStatic, createBody, false, true,
overridingTrait != null ? compiler.PathFromTopLevel(overridingTrait) : null,
attributes,
name,
new(), (Sequence<DAST.Formal>)Sequence<DAST.Formal>.Empty,
new() {
Expand Down
2 changes: 1 addition & 1 deletion Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -181,7 +181,7 @@ private Import CreateImport(string moduleName, bool isDefault, ModuleDefinition

protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault,
ModuleDefinition externModule,
string libraryName /*?*/, ConcreteSyntaxTree wr) {
string libraryName /*?*/, Attributes moduleAttributes, ConcreteSyntaxTree wr) {
if (isDefault) {
// Fold the default module into the main module
return wr;
Expand Down
Loading

0 comments on commit 2412e86

Please sign in to comment.