diff --git a/Source/DafnyCore.Test/GeneratedFromDafny/FactorPathsOptimizationTest.cs b/Source/DafnyCore.Test/GeneratedFromDafny/FactorPathsOptimizationTest.cs index 02b63cfbb13..b2f3f183384 100644 --- a/Source/DafnyCore.Test/GeneratedFromDafny/FactorPathsOptimizationTest.cs +++ b/Source/DafnyCore.Test/GeneratedFromDafny/FactorPathsOptimizationTest.cs @@ -40,8 +40,8 @@ public static void TestApply() _3_std__any__Any = (((RAST.__default.@global).MSel(Dafny.Sequence.UnicodeFromString("std"))).MSel(Dafny.Sequence.UnicodeFromString("any"))).MSel(Dafny.Sequence.UnicodeFromString("Any")); RAST._IType _4_Any; _4_Any = RAST.Type.create_TIdentifier(Dafny.Sequence.UnicodeFromString("Any")); - FactorPathsOptimizationTest.__default.ShouldBeEqual(FactorPathsOptimization.__default.apply(RAST.Mod.create_Mod(Dafny.Sequence.UnicodeFromString("onemodule"), Dafny.Sequence.FromElements(RAST.ModDecl.create_StructDecl(RAST.Struct.create(Dafny.Sequence>.FromElements(), Dafny.Sequence.UnicodeFromString("test"), Dafny.Sequence.FromElements(_0_T__Decl), RAST.Fields.create_NamedFields(Dafny.Sequence.FromElements(RAST.Field.create(RAST.Visibility.create_PUB(), RAST.Formal.create(Dafny.Sequence.UnicodeFromString("a"), (_3_std__any__Any).AsType())))))), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_Impl(Dafny.Sequence.FromElements(_0_T__Decl), (RAST.Type.create_TIdentifier(Dafny.Sequence.UnicodeFromString("test"))).Apply(Dafny.Sequence.FromElements(_2_T)), Dafny.Sequence.UnicodeFromString(""), Dafny.Sequence.FromElements())), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(Dafny.Sequence.FromElements(_0_T__Decl), (_3_std__any__Any).AsType(), ((((RAST.__default.crate).MSel(Dafny.Sequence.UnicodeFromString("onemodule"))).MSel(Dafny.Sequence.UnicodeFromString("test"))).AsType()).Apply(Dafny.Sequence.FromElements(_2_T)), Dafny.Sequence.UnicodeFromString(""), Dafny.Sequence.FromElements()))))), RAST.Mod.create_Mod(Dafny.Sequence.UnicodeFromString("onemodule"), Dafny.Sequence.FromElements(RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), (RAST.__default.dafny__runtime).MSel(Dafny.Sequence.UnicodeFromString("DafnyType")))), RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), _3_std__any__Any)), RAST.ModDecl.create_StructDecl(RAST.Struct.create(Dafny.Sequence>.FromElements(), Dafny.Sequence.UnicodeFromString("test"), Dafny.Sequence.FromElements(_1_T__Decl__simp), RAST.Fields.create_NamedFields(Dafny.Sequence.FromElements(RAST.Field.create(RAST.Visibility.create_PUB(), RAST.Formal.create(Dafny.Sequence.UnicodeFromString("a"), _4_Any)))))), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_Impl(Dafny.Sequence.FromElements(_1_T__Decl__simp), (RAST.Type.create_TIdentifier(Dafny.Sequence.UnicodeFromString("test"))).Apply(Dafny.Sequence.FromElements(_2_T)), Dafny.Sequence.UnicodeFromString(""), Dafny.Sequence.FromElements())), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(Dafny.Sequence.FromElements(_1_T__Decl__simp), _4_Any, (RAST.Type.create_TIdentifier(Dafny.Sequence.UnicodeFromString("test"))).Apply(Dafny.Sequence.FromElements(_2_T)), Dafny.Sequence.UnicodeFromString(""), Dafny.Sequence.FromElements()))))); - FactorPathsOptimizationTest.__default.ShouldBeEqual(FactorPathsOptimization.__default.apply(RAST.Mod.create_Mod(Dafny.Sequence.UnicodeFromString("onemodule"), Dafny.Sequence.FromElements(RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(Dafny.Sequence.FromElements(_0_T__Decl), (((RAST.__default.dafny__runtime).MSel(Dafny.Sequence.UnicodeFromString("UpcastObject"))).AsType()).Apply(Dafny.Sequence.FromElements(RAST.Type.create_TIdentifier(Dafny.Sequence.UnicodeFromString("x")))), (RAST.Type.create_TIdentifier(Dafny.Sequence.UnicodeFromString("test"))).Apply(Dafny.Sequence.FromElements(_2_T)), Dafny.Sequence.UnicodeFromString(""), Dafny.Sequence.FromElements()))))), RAST.Mod.create_Mod(Dafny.Sequence.UnicodeFromString("onemodule"), Dafny.Sequence.FromElements(RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), (RAST.__default.dafny__runtime).MSel(Dafny.Sequence.UnicodeFromString("DafnyType")))), RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), (RAST.__default.dafny__runtime).MSel(Dafny.Sequence.UnicodeFromString("UpcastObject")))), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(Dafny.Sequence.FromElements(_1_T__Decl__simp), (RAST.Type.create_TIdentifier(Dafny.Sequence.UnicodeFromString("UpcastObject"))).Apply(Dafny.Sequence.FromElements(RAST.Type.create_TIdentifier(Dafny.Sequence.UnicodeFromString("x")))), (RAST.Type.create_TIdentifier(Dafny.Sequence.UnicodeFromString("test"))).Apply(Dafny.Sequence.FromElements(_2_T)), Dafny.Sequence.UnicodeFromString(""), Dafny.Sequence.FromElements()))))); + FactorPathsOptimizationTest.__default.ShouldBeEqual(FactorPathsOptimization.__default.apply(RAST.Mod.create_Mod(Dafny.Sequence.UnicodeFromString("onemodule"), Dafny.Sequence>.FromElements(), Dafny.Sequence.FromElements(RAST.ModDecl.create_StructDecl(RAST.Struct.create(Dafny.Sequence>.FromElements(), Dafny.Sequence.UnicodeFromString("test"), Dafny.Sequence.FromElements(_0_T__Decl), RAST.Fields.create_NamedFields(Dafny.Sequence.FromElements(RAST.Field.create(RAST.Visibility.create_PUB(), RAST.Formal.create(Dafny.Sequence.UnicodeFromString("a"), (_3_std__any__Any).AsType())))))), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_Impl(Dafny.Sequence.FromElements(_0_T__Decl), (RAST.Type.create_TIdentifier(Dafny.Sequence.UnicodeFromString("test"))).Apply(Dafny.Sequence.FromElements(_2_T)), Dafny.Sequence.UnicodeFromString(""), Dafny.Sequence.FromElements())), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(Dafny.Sequence.FromElements(_0_T__Decl), (_3_std__any__Any).AsType(), ((((RAST.__default.crate).MSel(Dafny.Sequence.UnicodeFromString("onemodule"))).MSel(Dafny.Sequence.UnicodeFromString("test"))).AsType()).Apply(Dafny.Sequence.FromElements(_2_T)), Dafny.Sequence.UnicodeFromString(""), Dafny.Sequence.FromElements()))))), RAST.Mod.create_Mod(Dafny.Sequence.UnicodeFromString("onemodule"), Dafny.Sequence>.FromElements(), Dafny.Sequence.FromElements(RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), (RAST.__default.dafny__runtime).MSel(Dafny.Sequence.UnicodeFromString("DafnyType")))), RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), _3_std__any__Any)), RAST.ModDecl.create_StructDecl(RAST.Struct.create(Dafny.Sequence>.FromElements(), Dafny.Sequence.UnicodeFromString("test"), Dafny.Sequence.FromElements(_1_T__Decl__simp), RAST.Fields.create_NamedFields(Dafny.Sequence.FromElements(RAST.Field.create(RAST.Visibility.create_PUB(), RAST.Formal.create(Dafny.Sequence.UnicodeFromString("a"), _4_Any)))))), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_Impl(Dafny.Sequence.FromElements(_1_T__Decl__simp), (RAST.Type.create_TIdentifier(Dafny.Sequence.UnicodeFromString("test"))).Apply(Dafny.Sequence.FromElements(_2_T)), Dafny.Sequence.UnicodeFromString(""), Dafny.Sequence.FromElements())), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(Dafny.Sequence.FromElements(_1_T__Decl__simp), _4_Any, (RAST.Type.create_TIdentifier(Dafny.Sequence.UnicodeFromString("test"))).Apply(Dafny.Sequence.FromElements(_2_T)), Dafny.Sequence.UnicodeFromString(""), Dafny.Sequence.FromElements()))))); + FactorPathsOptimizationTest.__default.ShouldBeEqual(FactorPathsOptimization.__default.apply(RAST.Mod.create_Mod(Dafny.Sequence.UnicodeFromString("onemodule"), Dafny.Sequence>.FromElements(), Dafny.Sequence.FromElements(RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(Dafny.Sequence.FromElements(_0_T__Decl), (((RAST.__default.dafny__runtime).MSel(Dafny.Sequence.UnicodeFromString("UpcastObject"))).AsType()).Apply(Dafny.Sequence.FromElements(RAST.Type.create_TIdentifier(Dafny.Sequence.UnicodeFromString("x")))), (RAST.Type.create_TIdentifier(Dafny.Sequence.UnicodeFromString("test"))).Apply(Dafny.Sequence.FromElements(_2_T)), Dafny.Sequence.UnicodeFromString(""), Dafny.Sequence.FromElements()))))), RAST.Mod.create_Mod(Dafny.Sequence.UnicodeFromString("onemodule"), Dafny.Sequence>.FromElements(), Dafny.Sequence.FromElements(RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), (RAST.__default.dafny__runtime).MSel(Dafny.Sequence.UnicodeFromString("DafnyType")))), RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), (RAST.__default.dafny__runtime).MSel(Dafny.Sequence.UnicodeFromString("UpcastObject")))), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(Dafny.Sequence.FromElements(_1_T__Decl__simp), (RAST.Type.create_TIdentifier(Dafny.Sequence.UnicodeFromString("UpcastObject"))).Apply(Dafny.Sequence.FromElements(RAST.Type.create_TIdentifier(Dafny.Sequence.UnicodeFromString("x")))), (RAST.Type.create_TIdentifier(Dafny.Sequence.UnicodeFromString("test"))).Apply(Dafny.Sequence.FromElements(_2_T)), Dafny.Sequence.UnicodeFromString(""), Dafny.Sequence.FromElements()))))); } } } // end of namespace FactorPathsOptimizationTest \ No newline at end of file diff --git a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs index f6e21f77093..5e3ee5c8db5 100644 --- a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs +++ b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs @@ -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); @@ -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}"); } diff --git a/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs b/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs index 8eada0edcdf..8c333c37386 100644 --- a/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs +++ b/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs @@ -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); diff --git a/Source/DafnyCore/Backends/Dafny/AST.dfy b/Source/DafnyCore/Backends/Dafny/AST.dfy index f8bd301ee9d..a4998f529f4 100644 --- a/Source/DafnyCore/Backends/Dafny/AST.dfy +++ b/Source/DafnyCore/Backends/Dafny/AST.dfy @@ -204,6 +204,7 @@ module {:extern "DAST"} DAST { datatype Formal = Formal(name: VarName, typ: Type, attributes: seq) datatype Method = Method( + attributes: seq, isStatic: bool, hasBody: bool, outVarsAreUninitFieldsToAssign: bool, // For constructors diff --git a/Source/DafnyCore/Backends/Dafny/ASTBuilder.cs b/Source/DafnyCore/Backends/Dafny/ASTBuilder.cs index 9e6e32ae148..51eec419470 100644 --- a/Source/DafnyCore/Backends/Dafny/ASTBuilder.cs +++ b/Source/DafnyCore/Backends/Dafny/ASTBuilder.cs @@ -365,15 +365,14 @@ interface ClassLike { void AddField(DAST.Formal item, _IOption defaultValue); - public MethodBuilder Method( - bool isStatic, bool hasBody, bool outVarsAreUninitFieldsToAssign, bool wasFunction, + public MethodBuilder Method(bool isStatic, bool hasBody, bool outVarsAreUninitFieldsToAssign, bool wasFunction, ISequence> overridingPath, + ISequence<_IAttribute> attributes, string name, - List typeArgs, + List typeArgs, Sequence params_, - List outTypes, List> outVars - ) { - return new MethodBuilder(this, isStatic, hasBody, outVarsAreUninitFieldsToAssign, wasFunction, overridingPath, name, typeArgs, params_, outTypes, outVars); + List outTypes, List> outVars) { + return new MethodBuilder(this, isStatic, hasBody, outVarsAreUninitFieldsToAssign, wasFunction, overridingPath, attributes, name, typeArgs, params_, outTypes, outVars); } public object Finish(); @@ -392,11 +391,13 @@ class MethodBuilder : StatementContainer { readonly List outTypes; readonly List> outVars; readonly List body = new(); + private ISequence<_IAttribute> attributes; public MethodBuilder( ClassLike parent, bool isStatic, bool hasBody, bool outVarsAreUninitFieldsToAssign, bool wasFunction, ISequence> overridingPath, + ISequence<_IAttribute> attributes, string name, List typeArgs, Sequence params_, @@ -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_; @@ -434,6 +436,7 @@ public DAST.Method Build() { StatementContainer.RecursivelyBuild(body, builtStatements); return (DAST.Method)DAST.Method.create( + attributes, isStatic, hasBody, outVarsAreUninitFieldsToAssign, diff --git a/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs b/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs index eecd3952b1c..9c5a9b9ddd9 100644 --- a/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs +++ b/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs @@ -125,9 +125,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)Sequence.Empty; + var attributes = (Sequence)ParseAttributes(moduleAttributes); if (externModule != null) { attributes = (Sequence)ParseAttributes(externModule.Attributes); } @@ -551,9 +551,12 @@ public ConcreteSyntaxTree CreateMethod(Method m, List 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 @@ -586,10 +589,11 @@ public ConcreteSyntaxTree CreateFunction(string name, List)Sequence.Empty, new() { diff --git a/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs b/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs index 55ddecdc1e5..37a53d9ae4f 100644 --- a/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs +++ b/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs @@ -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; diff --git a/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs b/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs index c7ee9c2c663..8760a7df39b 100644 --- a/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs +++ b/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs @@ -380,7 +380,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); if (isDefault) { // Fold the default module into the main module diff --git a/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs b/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs index ad1b85bd8f7..7dc6651d668 100644 --- a/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs +++ b/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs @@ -64,7 +64,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) { moduleName = IdProtect(moduleName); if (externModule == null || libraryName != null) { wr.Write("let {0} = ", moduleName); diff --git a/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs b/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs index 7783c33a038..8d1f54c2628 100644 --- a/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs +++ b/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs @@ -99,7 +99,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 pythonModuleName = PythonModuleMode ? PythonModuleName + "." : ""; moduleName = PublicModuleIdProtect(moduleName); diff --git a/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-path-simplification.dfy b/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-path-simplification.dfy index e7dbab864f5..2a3afea326f 100644 --- a/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-path-simplification.dfy +++ b/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-path-simplification.dfy @@ -20,7 +20,7 @@ module FactorPathsOptimizationTest { var std_any_Any := global.MSel("std").MSel("any").MSel("Any"); var Any := TIdentifier("Any"); ShouldBeEqual(apply( - Mod("onemodule", [ + Mod("onemodule", [], [ StructDecl( Struct([], "test", [T_Decl], NamedFields([Field(PUB, Formal("a", std_any_Any.AsType()))]))), @@ -31,7 +31,7 @@ module FactorPathsOptimizationTest { [T_Decl], std_any_Any.AsType(), crate.MSel("onemodule").MSel("test").AsType().Apply([T]), "", [])) // ::std::any::Any ==> Any crate::onemodule::test ==> test ])), - Mod("onemodule", [ + Mod("onemodule", [], [ UseDecl(Use(PUB, dafny_runtime.MSel("DafnyType"))), UseDecl(Use(PUB, std_any_Any)), StructDecl( @@ -41,13 +41,13 @@ module FactorPathsOptimizationTest { ImplDecl(ImplFor([T_Decl_simp], Any, TIdentifier("test").Apply([T]), "", [])) ])); ShouldBeEqual(apply( - Mod("onemodule", [ + Mod("onemodule", [], [ ImplDecl( ImplFor( [T_Decl], dafny_runtime.MSel("UpcastObject").AsType().Apply([TIdentifier("x")]), TIdentifier("test").Apply([T]), "", [])) ])), - Mod("onemodule", [ + Mod("onemodule", [], [ UseDecl(Use(PUB, dafny_runtime.MSel("DafnyType"))), UseDecl(Use(PUB, dafny_runtime.MSel("UpcastObject"))), ImplDecl( diff --git a/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-utils.dfy b/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-utils.dfy index 32671420dd9..6a7089f6ee4 100644 --- a/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-utils.dfy +++ b/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-utils.dfy @@ -67,7 +67,7 @@ module DafnyCompilerRustUtils { { if !GatheringModule? then m2 else if !m2.GatheringModule? then this else GatheringModule( - R.Mod(existingMod.name, existingMod.body + m2.existingMod.body), + R.Mod(existingMod.name, existingMod.attributes, existingMod.body + m2.existingMod.body), MergeSeqMap(submodules, m2.submodules) ) } @@ -82,7 +82,7 @@ module DafnyCompilerRustUtils { else var enclosingModule := containingPath[0]; SeqMap.Single(enclosingModule, - GatheringModule(R.Mod(enclosingModule, []), Wrap(containingPath[1..], rawDecl))) + GatheringModule(R.Mod(enclosingModule, [], []), Wrap(containingPath[1..], rawDecl))) } function ToRust(): R.Mod { if ExternMod? then m else diff --git a/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy b/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy index 60b080e721d..e46014287b9 100644 --- a/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy +++ b/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy @@ -28,7 +28,7 @@ module RAST datatype Mod = // Rust modules - | Mod(name: string, body: seq) + | Mod(name: string, attributes: seq, body: seq) | ExternMod(name: string) { function Fold(acc: T, accBuilder: (T, ModDecl) --> T): T @@ -43,7 +43,8 @@ module RAST match this { case ExternMod(name) => "pub mod " + name + ";" - case Mod(name, body) => + case Mod(name, attributes, body) => + Attribute.ToStringMultiple(attributes, ind) + /* If the module does not start with "use", just separate declarations by one blank line If the module starts with "use", add blank lines only after use declarations */ var startWithUse := |body| > 0 && body[0].UseDecl?; @@ -1848,6 +1849,10 @@ module {:extern "DCOMP"} DafnyToRustCompiler { Std.Collections.Seq.Map((i: Ident) => escapeName(i.id), containingPath) } + predicate HasAttribute(attributes: seq, name: string) { + exists attribute <- attributes :: attribute.name == name && |attribute.args| == 0 + } + // Returns a top-level gathering module that can be merged with other gathering modules method GenModule(mod: Module, containingPath: seq) returns (s: SeqMap) decreases mod, 1 @@ -1861,6 +1866,10 @@ module {:extern "DCOMP"} DafnyToRustCompiler { } else { assume {:axiom} forall m: ModuleItem <- mod.body.value :: m < mod; var optExtern: ExternAttribute := ExtractExternMod(mod); + var attributes := []; + if HasAttribute(mod.attributes, "rust_cfg_test") { + attributes := [R.RawAttribute("#[cfg(test)]")]; + } var body, allmodules := GenModuleBody(mod, mod.body.value, containingPath + [Ident.Ident(innerName)]); if optExtern.SimpleExtern? { if mod.requiresExterns { @@ -1872,7 +1881,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler { error := Some(optExtern.reason); } s := GatheringModule.MergeSeqMap( - GatheringModule.Wrap(ContainingPathToRust(containingPath), R.Mod(modName, body)), + GatheringModule.Wrap(ContainingPathToRust(containingPath), R.Mod(modName, attributes, body)), allmodules); } } @@ -2084,6 +2093,27 @@ module {:extern "DCOMP"} DafnyToRustCompiler { ); s := s + [R.ImplDecl(i)]; } + // Add test methods + var testMethods := []; + if className == "_default" { + for i := 0 to |c.body| { + var m := match c.body[i] case Method(m) => m; + if HasAttribute(m.attributes, "test") && |m.params| == 0 { + var fnName := escapeName(m.name); + testMethods := testMethods + [ + R.TopFnDecl( + R.TopFn( + [R.RawAttribute("#[test]")], R.PUB, + R.Fn( + fnName, [], [], None, + "", + Some(R.Identifier("_default").FSel(fnName).Apply([]))) + )) + ]; + } + } + s := s + testMethods; + } var genSelfPath := GenPathType(path); // TODO: If general traits, check whether the trait extends object or not. if className != "_default" { @@ -5562,7 +5592,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler { } if externUseDecls != [] { - s := s + R.Mod(DAFNY_EXTERN_MODULE, externUseDecls).ToString("") + "\n"; + s := s + R.Mod(DAFNY_EXTERN_MODULE, [], externUseDecls).ToString("") + "\n"; } var allModules := SeqMap.Empty(); diff --git a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs index 7647eb0c11d..98c390f870c 100644 --- a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs +++ b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs @@ -183,7 +183,7 @@ protected void CheckSystemModulePopulatedToCommonLimits(SystemModuleManager syst /// protected abstract ConcreteSyntaxTree CreateStaticMain(IClassWriter wr, string argsParameterName); protected abstract ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, ModuleDefinition externModule, - string libraryName /*?*/, ConcreteSyntaxTree wr); + string libraryName /*?*/, Attributes moduleAttributes, ConcreteSyntaxTree wr); /// /// Indicates the current program depends on the given module without creating it. /// Called when a module is out of scope for compilation, such as when using --library. @@ -1585,7 +1585,7 @@ private void EmitModule(Program program, ConcreteSyntaxTree programNode, ModuleD Contract.Assert(enclosingModule == null); enclosingModule = module; - var wr = CreateModule(module.GetCompileName(Options), module.IsDefaultModule, externModule, libraryName, programNode); + var wr = CreateModule(module.GetCompileName(Options), module.IsDefaultModule, externModule, libraryName, module.Attributes, programNode); var v = new CheckHasNoAssumes_Visitor(this, wr); foreach (TopLevelDecl d in module.TopLevelDecls) { if (!ProgramResolver.ShouldCompile(d)) { diff --git a/Source/DafnyCore/GeneratedFromDafny/DAST.cs b/Source/DafnyCore/GeneratedFromDafny/DAST.cs index 8400f6a4fef..b9c3d448263 100644 --- a/Source/DafnyCore/GeneratedFromDafny/DAST.cs +++ b/Source/DafnyCore/GeneratedFromDafny/DAST.cs @@ -3474,6 +3474,7 @@ public Dafny.ISequence dtor_attributes { public interface _IMethod { bool is_Method { get; } + Dafny.ISequence dtor_attributes { get; } bool dtor_isStatic { get; } bool dtor_hasBody { get; } bool dtor_outVarsAreUninitFieldsToAssign { get; } @@ -3488,6 +3489,7 @@ public interface _IMethod { _IMethod DowncastClone(); } public class Method : _IMethod { + public readonly Dafny.ISequence _attributes; public readonly bool _isStatic; public readonly bool _hasBody; public readonly bool _outVarsAreUninitFieldsToAssign; @@ -3499,7 +3501,8 @@ public class Method : _IMethod { public readonly Dafny.ISequence _body; public readonly Dafny.ISequence _outTypes; public readonly Std.Wrappers._IOption>> _outVars; - public Method(bool isStatic, bool hasBody, bool outVarsAreUninitFieldsToAssign, bool wasFunction, Std.Wrappers._IOption>> overridingPath, Dafny.ISequence name, Dafny.ISequence typeParams, Dafny.ISequence @params, Dafny.ISequence body, Dafny.ISequence outTypes, Std.Wrappers._IOption>> outVars) { + public Method(Dafny.ISequence attributes, bool isStatic, bool hasBody, bool outVarsAreUninitFieldsToAssign, bool wasFunction, Std.Wrappers._IOption>> overridingPath, Dafny.ISequence name, Dafny.ISequence typeParams, Dafny.ISequence @params, Dafny.ISequence body, Dafny.ISequence outTypes, Std.Wrappers._IOption>> outVars) { + this._attributes = attributes; this._isStatic = isStatic; this._hasBody = hasBody; this._outVarsAreUninitFieldsToAssign = outVarsAreUninitFieldsToAssign; @@ -3514,15 +3517,16 @@ public Method(bool isStatic, bool hasBody, bool outVarsAreUninitFieldsToAssign, } public _IMethod DowncastClone() { if (this is _IMethod dt) { return dt; } - return new Method(_isStatic, _hasBody, _outVarsAreUninitFieldsToAssign, _wasFunction, _overridingPath, _name, _typeParams, _params, _body, _outTypes, _outVars); + return new Method(_attributes, _isStatic, _hasBody, _outVarsAreUninitFieldsToAssign, _wasFunction, _overridingPath, _name, _typeParams, _params, _body, _outTypes, _outVars); } public override bool Equals(object other) { var oth = other as DAST.Method; - return oth != null && this._isStatic == oth._isStatic && this._hasBody == oth._hasBody && this._outVarsAreUninitFieldsToAssign == oth._outVarsAreUninitFieldsToAssign && this._wasFunction == oth._wasFunction && object.Equals(this._overridingPath, oth._overridingPath) && object.Equals(this._name, oth._name) && object.Equals(this._typeParams, oth._typeParams) && object.Equals(this._params, oth._params) && object.Equals(this._body, oth._body) && object.Equals(this._outTypes, oth._outTypes) && object.Equals(this._outVars, oth._outVars); + return oth != null && object.Equals(this._attributes, oth._attributes) && this._isStatic == oth._isStatic && this._hasBody == oth._hasBody && this._outVarsAreUninitFieldsToAssign == oth._outVarsAreUninitFieldsToAssign && this._wasFunction == oth._wasFunction && object.Equals(this._overridingPath, oth._overridingPath) && object.Equals(this._name, oth._name) && object.Equals(this._typeParams, oth._typeParams) && object.Equals(this._params, oth._params) && object.Equals(this._body, oth._body) && object.Equals(this._outTypes, oth._outTypes) && object.Equals(this._outVars, oth._outVars); } public override int GetHashCode() { ulong hash = 5381; hash = ((hash << 5) + hash) + 0; + hash = ((hash << 5) + hash) + ((ulong)Dafny.Helpers.GetHashCode(this._attributes)); hash = ((hash << 5) + hash) + ((ulong)Dafny.Helpers.GetHashCode(this._isStatic)); hash = ((hash << 5) + hash) + ((ulong)Dafny.Helpers.GetHashCode(this._hasBody)); hash = ((hash << 5) + hash) + ((ulong)Dafny.Helpers.GetHashCode(this._outVarsAreUninitFieldsToAssign)); @@ -3539,6 +3543,8 @@ public override int GetHashCode() { public override string ToString() { string s = "DAST.Method.Method"; s += "("; + s += Dafny.Helpers.ToString(this._attributes); + s += ", "; s += Dafny.Helpers.ToString(this._isStatic); s += ", "; s += Dafny.Helpers.ToString(this._hasBody); @@ -3563,7 +3569,7 @@ public override string ToString() { s += ")"; return s; } - private static readonly DAST._IMethod theDefault = create(false, false, false, false, Std.Wrappers.Option>>.Default(), Dafny.Sequence.Empty, Dafny.Sequence.Empty, Dafny.Sequence.Empty, Dafny.Sequence.Empty, Dafny.Sequence.Empty, Std.Wrappers.Option>>.Default()); + private static readonly DAST._IMethod theDefault = create(Dafny.Sequence.Empty, false, false, false, false, Std.Wrappers.Option>>.Default(), Dafny.Sequence.Empty, Dafny.Sequence.Empty, Dafny.Sequence.Empty, Dafny.Sequence.Empty, Dafny.Sequence.Empty, Std.Wrappers.Option>>.Default()); public static DAST._IMethod Default() { return theDefault; } @@ -3571,13 +3577,18 @@ public static DAST._IMethod Default() { public static Dafny.TypeDescriptor _TypeDescriptor() { return _TYPE; } - public static _IMethod create(bool isStatic, bool hasBody, bool outVarsAreUninitFieldsToAssign, bool wasFunction, Std.Wrappers._IOption>> overridingPath, Dafny.ISequence name, Dafny.ISequence typeParams, Dafny.ISequence @params, Dafny.ISequence body, Dafny.ISequence outTypes, Std.Wrappers._IOption>> outVars) { - return new Method(isStatic, hasBody, outVarsAreUninitFieldsToAssign, wasFunction, overridingPath, name, typeParams, @params, body, outTypes, outVars); + public static _IMethod create(Dafny.ISequence attributes, bool isStatic, bool hasBody, bool outVarsAreUninitFieldsToAssign, bool wasFunction, Std.Wrappers._IOption>> overridingPath, Dafny.ISequence name, Dafny.ISequence typeParams, Dafny.ISequence @params, Dafny.ISequence body, Dafny.ISequence outTypes, Std.Wrappers._IOption>> outVars) { + return new Method(attributes, isStatic, hasBody, outVarsAreUninitFieldsToAssign, wasFunction, overridingPath, name, typeParams, @params, body, outTypes, outVars); } - public static _IMethod create_Method(bool isStatic, bool hasBody, bool outVarsAreUninitFieldsToAssign, bool wasFunction, Std.Wrappers._IOption>> overridingPath, Dafny.ISequence name, Dafny.ISequence typeParams, Dafny.ISequence @params, Dafny.ISequence body, Dafny.ISequence outTypes, Std.Wrappers._IOption>> outVars) { - return create(isStatic, hasBody, outVarsAreUninitFieldsToAssign, wasFunction, overridingPath, name, typeParams, @params, body, outTypes, outVars); + public static _IMethod create_Method(Dafny.ISequence attributes, bool isStatic, bool hasBody, bool outVarsAreUninitFieldsToAssign, bool wasFunction, Std.Wrappers._IOption>> overridingPath, Dafny.ISequence name, Dafny.ISequence typeParams, Dafny.ISequence @params, Dafny.ISequence body, Dafny.ISequence outTypes, Std.Wrappers._IOption>> outVars) { + return create(attributes, isStatic, hasBody, outVarsAreUninitFieldsToAssign, wasFunction, overridingPath, name, typeParams, @params, body, outTypes, outVars); } public bool is_Method { get { return true; } } + public Dafny.ISequence dtor_attributes { + get { + return this._attributes; + } + } public bool dtor_isStatic { get { return this._isStatic; diff --git a/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs b/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs index 85751234057..51824995fd8 100644 --- a/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs +++ b/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs @@ -946,6 +946,13 @@ public void __ctor(bool unicodeChars, DCOMP._IObjectType objectType) return DCOMP.__default.escapeName((_0_i)); })), containingPath); } + public bool HasAttribute(Dafny.ISequence attributes, Dafny.ISequence name) + { + return Dafny.Helpers.Id, Dafny.ISequence, bool>>((_0_attributes, _1_name) => Dafny.Helpers.Quantifier((_0_attributes).UniqueElements, false, (((_exists_var_0) => { + DAST._IAttribute _2_attribute = (DAST._IAttribute)_exists_var_0; + return ((_0_attributes).Contains(_2_attribute)) && ((((_2_attribute).dtor_name).Equals(_1_name)) && ((new BigInteger(((_2_attribute).dtor_args).Count)).Sign == 0)); + }))))(attributes, name); + } public DafnyCompilerRustUtils._ISeqMap, DafnyCompilerRustUtils._IGatheringModule> GenModule(DAST._IModule mod, Dafny.ISequence> containingPath) { DafnyCompilerRustUtils._ISeqMap, DafnyCompilerRustUtils._IGatheringModule> s = DafnyCompilerRustUtils.SeqMap, DafnyCompilerRustUtils._IGatheringModule>.Default(); @@ -961,23 +968,28 @@ public void __ctor(bool unicodeChars, DCOMP._IObjectType objectType) } else { DCOMP._IExternAttribute _4_optExtern; _4_optExtern = DCOMP.__default.ExtractExternMod(mod); - Dafny.ISequence _5_body; - DafnyCompilerRustUtils._ISeqMap, DafnyCompilerRustUtils._IGatheringModule> _6_allmodules; + Dafny.ISequence> _5_attributes; + _5_attributes = Dafny.Sequence>.FromElements(); + if ((this).HasAttribute((mod).dtor_attributes, Dafny.Sequence.UnicodeFromString("rust_cfg_test"))) { + _5_attributes = Dafny.Sequence>.FromElements(Dafny.Sequence.UnicodeFromString("#[cfg(test)]")); + } + Dafny.ISequence _6_body; + DafnyCompilerRustUtils._ISeqMap, DafnyCompilerRustUtils._IGatheringModule> _7_allmodules; Dafny.ISequence _out0; DafnyCompilerRustUtils._ISeqMap, DafnyCompilerRustUtils._IGatheringModule> _out1; (this).GenModuleBody(((mod).dtor_body).dtor_value, Dafny.Sequence>.Concat(_2_containingPath, Dafny.Sequence>.FromElements(_1_innerName)), out _out0, out _out1); - _5_body = _out0; - _6_allmodules = _out1; + _6_body = _out0; + _7_allmodules = _out1; if ((_4_optExtern).is_SimpleExtern) { if ((mod).dtor_requiresExterns) { - _5_body = Dafny.Sequence.Concat(Dafny.Sequence.FromElements(RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), (((RAST.__default.crate).MSel(DCOMP.COMP.DAFNY__EXTERN__MODULE)).MSel(DCOMP.__default.ReplaceDotByDoubleColon((_4_optExtern).dtor_overrideName))).MSel(Dafny.Sequence.UnicodeFromString("*"))))), _5_body); + _6_body = Dafny.Sequence.Concat(Dafny.Sequence.FromElements(RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), (((RAST.__default.crate).MSel(DCOMP.COMP.DAFNY__EXTERN__MODULE)).MSel(DCOMP.__default.ReplaceDotByDoubleColon((_4_optExtern).dtor_overrideName))).MSel(Dafny.Sequence.UnicodeFromString("*"))))), _6_body); } } else if ((_4_optExtern).is_AdvancedExtern) { (this).error = Std.Wrappers.Option>.create_Some(Dafny.Sequence.UnicodeFromString("Externs on modules can only have 1 string argument")); } else if ((_4_optExtern).is_UnsupportedExtern) { (this).error = Std.Wrappers.Option>.create_Some((_4_optExtern).dtor_reason); } - s = DafnyCompilerRustUtils.GatheringModule.MergeSeqMap(DafnyCompilerRustUtils.GatheringModule.Wrap(DCOMP.COMP.ContainingPathToRust(_2_containingPath), RAST.Mod.create_Mod(_3_modName, _5_body)), _6_allmodules); + s = DafnyCompilerRustUtils.GatheringModule.MergeSeqMap(DafnyCompilerRustUtils.GatheringModule.Wrap(DCOMP.COMP.ContainingPathToRust(_2_containingPath), RAST.Mod.create_Mod(_3_modName, _5_attributes, _6_body)), _7_allmodules); } return s; } @@ -1240,72 +1252,92 @@ public bool IsSameResolvedType(DAST._IResolvedType r1, DAST._IResolvedType r2) _27_i = RAST.Impl.create_Impl(_2_rTypeParamsDecls, RAST.Type.create_TypeApp(_26_selfTypeForImpl, _1_rTypeParams), _3_whereConstraints, _24_implBody); s = Dafny.Sequence.Concat(s, Dafny.Sequence.FromElements(RAST.ModDecl.create_ImplDecl(_27_i))); } - RAST._IType _28_genSelfPath; + Dafny.ISequence _28_testMethods; + _28_testMethods = Dafny.Sequence.FromElements(); + if ((_22_className).Equals(Dafny.Sequence.UnicodeFromString("_default"))) { + BigInteger _hi2 = new BigInteger(((c).dtor_body).Count); + for (BigInteger _29_i = BigInteger.Zero; _29_i < _hi2; _29_i++) { + DAST._IMethod _30_m; + DAST._IMethod _source1 = ((c).dtor_body).Select(_29_i); + { + DAST._IMethod _31_m = _source1; + _30_m = _31_m; + } + after_match1: ; + if (((this).HasAttribute((_30_m).dtor_attributes, Dafny.Sequence.UnicodeFromString("test"))) && ((new BigInteger(((_30_m).dtor_params).Count)).Sign == 0)) { + Dafny.ISequence _32_fnName; + _32_fnName = DCOMP.__default.escapeName((_30_m).dtor_name); + _28_testMethods = Dafny.Sequence.Concat(_28_testMethods, Dafny.Sequence.FromElements(RAST.ModDecl.create_TopFnDecl(RAST.TopFnDecl.create(Dafny.Sequence>.FromElements(Dafny.Sequence.UnicodeFromString("#[test]")), RAST.Visibility.create_PUB(), RAST.Fn.create(_32_fnName, Dafny.Sequence.FromElements(), Dafny.Sequence.FromElements(), Std.Wrappers.Option.create_None(), Dafny.Sequence.UnicodeFromString(""), Std.Wrappers.Option.create_Some(((RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("_default"))).FSel(_32_fnName)).Apply(Dafny.Sequence.FromElements()))))))); + } + } + s = Dafny.Sequence.Concat(s, _28_testMethods); + } + RAST._IType _33_genSelfPath; RAST._IType _out13; _out13 = DCOMP.COMP.GenPathType(path); - _28_genSelfPath = _out13; + _33_genSelfPath = _out13; if (!(_22_className).Equals(Dafny.Sequence.UnicodeFromString("_default"))) { - s = Dafny.Sequence.Concat(s, Dafny.Sequence.FromElements(RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(_2_rTypeParamsDecls, (((RAST.__default.dafny__runtime).MSel((this).Upcast)).AsType()).Apply(Dafny.Sequence.FromElements(RAST.Type.create_DynType(RAST.__default.AnyTrait))), RAST.Type.create_TypeApp(_28_genSelfPath, _1_rTypeParams), _3_whereConstraints, Dafny.Sequence.FromElements(RAST.ImplMember.create_ImplMemberMacro((((RAST.__default.dafny__runtime).MSel((this).UpcastFnMacro)).AsExpr()).Apply1(RAST.Expr.create_ExprFromType(RAST.Type.create_DynType(RAST.__default.AnyTrait))))))))); + s = Dafny.Sequence.Concat(s, Dafny.Sequence.FromElements(RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(_2_rTypeParamsDecls, (((RAST.__default.dafny__runtime).MSel((this).Upcast)).AsType()).Apply(Dafny.Sequence.FromElements(RAST.Type.create_DynType(RAST.__default.AnyTrait))), RAST.Type.create_TypeApp(_33_genSelfPath, _1_rTypeParams), _3_whereConstraints, Dafny.Sequence.FromElements(RAST.ImplMember.create_ImplMemberMacro((((RAST.__default.dafny__runtime).MSel((this).UpcastFnMacro)).AsExpr()).Apply1(RAST.Expr.create_ExprFromType(RAST.Type.create_DynType(RAST.__default.AnyTrait))))))))); } - Dafny.ISequence _29_superClasses; + Dafny.ISequence _34_superClasses; if ((_22_className).Equals(Dafny.Sequence.UnicodeFromString("_default"))) { - _29_superClasses = Dafny.Sequence.FromElements(); + _34_superClasses = Dafny.Sequence.FromElements(); } else { - _29_superClasses = (c).dtor_superClasses; + _34_superClasses = (c).dtor_superClasses; } - BigInteger _hi2 = new BigInteger((_29_superClasses).Count); - for (BigInteger _30_i = BigInteger.Zero; _30_i < _hi2; _30_i++) { - DAST._IType _31_superClass; - _31_superClass = (_29_superClasses).Select(_30_i); - DAST._IType _source1 = _31_superClass; + BigInteger _hi3 = new BigInteger((_34_superClasses).Count); + for (BigInteger _35_i = BigInteger.Zero; _35_i < _hi3; _35_i++) { + DAST._IType _36_superClass; + _36_superClass = (_34_superClasses).Select(_35_i); + DAST._IType _source2 = _36_superClass; { - if (_source1.is_UserDefined) { - DAST._IResolvedType resolved0 = _source1.dtor_resolved; - Dafny.ISequence> _32_traitPath = resolved0.dtor_path; - Dafny.ISequence _33_typeArgs = resolved0.dtor_typeArgs; + if (_source2.is_UserDefined) { + DAST._IResolvedType resolved0 = _source2.dtor_resolved; + Dafny.ISequence> _37_traitPath = resolved0.dtor_path; + Dafny.ISequence _38_typeArgs = resolved0.dtor_typeArgs; DAST._IResolvedTypeBase kind0 = resolved0.dtor_kind; if (kind0.is_Trait) { - Dafny.ISequence> _34_properMethods = resolved0.dtor_properMethods; + Dafny.ISequence> _39_properMethods = resolved0.dtor_properMethods; { - RAST._IType _35_pathStr; + RAST._IType _40_pathStr; RAST._IType _out14; - _out14 = DCOMP.COMP.GenPathType(_32_traitPath); - _35_pathStr = _out14; - Dafny.ISequence _36_typeArgs; + _out14 = DCOMP.COMP.GenPathType(_37_traitPath); + _40_pathStr = _out14; + Dafny.ISequence _41_typeArgs; Dafny.ISequence _out15; - _out15 = (this).GenTypeArgs(_33_typeArgs, DCOMP.GenTypeContext.@default()); - _36_typeArgs = _out15; - Dafny.ISequence _37_body; - _37_body = Dafny.Sequence.FromElements(); - if ((_25_traitBodies).Contains(_32_traitPath)) { - _37_body = Dafny.Map>, Dafny.ISequence>.Select(_25_traitBodies,_32_traitPath); + _out15 = (this).GenTypeArgs(_38_typeArgs, DCOMP.GenTypeContext.@default()); + _41_typeArgs = _out15; + Dafny.ISequence _42_body; + _42_body = Dafny.Sequence.FromElements(); + if ((_25_traitBodies).Contains(_37_traitPath)) { + _42_body = Dafny.Map>, Dafny.ISequence>.Select(_25_traitBodies,_37_traitPath); } - RAST._IType _38_traitType; - _38_traitType = RAST.Type.create_TypeApp(_35_pathStr, _36_typeArgs); + RAST._IType _43_traitType; + _43_traitType = RAST.Type.create_TypeApp(_40_pathStr, _41_typeArgs); if (!((_21_extern).is_NoExtern)) { - if (((new BigInteger((_37_body).Count)).Sign == 0) && ((new BigInteger((_34_properMethods).Count)).Sign != 0)) { + if (((new BigInteger((_42_body).Count)).Sign == 0) && ((new BigInteger((_39_properMethods).Count)).Sign != 0)) { goto continue_1; } - if ((new BigInteger((_37_body).Count)) != (new BigInteger((_34_properMethods).Count))) { - (this).error = Std.Wrappers.Option>.create_Some(Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.UnicodeFromString("Error: In the class "), RAST.__default.SeqToString>(path, ((System.Func, Dafny.ISequence>)((_39_s) => { - return ((_39_s)); -})), Dafny.Sequence.UnicodeFromString("."))), Dafny.Sequence.UnicodeFromString(", some proper methods of ")), (_38_traitType)._ToString(Dafny.Sequence.UnicodeFromString(""))), Dafny.Sequence.UnicodeFromString(" are marked {:extern} and some are not.")), Dafny.Sequence.UnicodeFromString(" For the Rust compiler, please make all methods (")), RAST.__default.SeqToString>(_34_properMethods, ((System.Func, Dafny.ISequence>)((_40_s) => { - return (_40_s); + if ((new BigInteger((_42_body).Count)) != (new BigInteger((_39_properMethods).Count))) { + (this).error = Std.Wrappers.Option>.create_Some(Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.UnicodeFromString("Error: In the class "), RAST.__default.SeqToString>(path, ((System.Func, Dafny.ISequence>)((_44_s) => { + return ((_44_s)); +})), Dafny.Sequence.UnicodeFromString("."))), Dafny.Sequence.UnicodeFromString(", some proper methods of ")), (_43_traitType)._ToString(Dafny.Sequence.UnicodeFromString(""))), Dafny.Sequence.UnicodeFromString(" are marked {:extern} and some are not.")), Dafny.Sequence.UnicodeFromString(" For the Rust compiler, please make all methods (")), RAST.__default.SeqToString>(_39_properMethods, ((System.Func, Dafny.ISequence>)((_45_s) => { + return (_45_s); })), Dafny.Sequence.UnicodeFromString(", "))), Dafny.Sequence.UnicodeFromString(") bodiless and mark as {:extern} and implement them in a Rust file, ")), Dafny.Sequence.UnicodeFromString("or mark none of them as {:extern} and implement them in Dafny. ")), Dafny.Sequence.UnicodeFromString("Alternatively, you can insert an intermediate trait that performs the partial implementation if feasible."))); } } - RAST._IModDecl _41_x; - _41_x = RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(_2_rTypeParamsDecls, _38_traitType, RAST.Type.create_TypeApp(_28_genSelfPath, _1_rTypeParams), _3_whereConstraints, _37_body)); - s = Dafny.Sequence.Concat(s, Dafny.Sequence.FromElements(_41_x)); - s = Dafny.Sequence.Concat(s, Dafny.Sequence.FromElements(RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(_2_rTypeParamsDecls, (((RAST.__default.dafny__runtime).MSel((this).Upcast)).AsType()).Apply(Dafny.Sequence.FromElements(RAST.Type.create_DynType(_38_traitType))), RAST.Type.create_TypeApp(_28_genSelfPath, _1_rTypeParams), _3_whereConstraints, Dafny.Sequence.FromElements(RAST.ImplMember.create_ImplMemberMacro((((RAST.__default.dafny__runtime).MSel((this).UpcastFnMacro)).AsExpr()).Apply1(RAST.Expr.create_ExprFromType(RAST.Type.create_DynType(_38_traitType))))))))); + RAST._IModDecl _46_x; + _46_x = RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(_2_rTypeParamsDecls, _43_traitType, RAST.Type.create_TypeApp(_33_genSelfPath, _1_rTypeParams), _3_whereConstraints, _42_body)); + s = Dafny.Sequence.Concat(s, Dafny.Sequence.FromElements(_46_x)); + s = Dafny.Sequence.Concat(s, Dafny.Sequence.FromElements(RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(_2_rTypeParamsDecls, (((RAST.__default.dafny__runtime).MSel((this).Upcast)).AsType()).Apply(Dafny.Sequence.FromElements(RAST.Type.create_DynType(_43_traitType))), RAST.Type.create_TypeApp(_33_genSelfPath, _1_rTypeParams), _3_whereConstraints, Dafny.Sequence.FromElements(RAST.ImplMember.create_ImplMemberMacro((((RAST.__default.dafny__runtime).MSel((this).UpcastFnMacro)).AsExpr()).Apply1(RAST.Expr.create_ExprFromType(RAST.Type.create_DynType(_43_traitType))))))))); } - goto after_match1; + goto after_match2; } } } { } - after_match1: ; + after_match2: ; continue_1: ; } after_1: ; @@ -2514,7 +2546,7 @@ public RAST._IImplMember GenMethod(DAST._IMethod m, bool forTrait, DAST._IType e { if (_source0.is_UserDefined) { DAST._IResolvedType _11_r = _source0.dtor_resolved; - _10_instanceType = DAST.Type.create_UserDefined(Dafny.Helpers.Let(_11_r, _pat_let20_0 => Dafny.Helpers.Let(_pat_let20_0, _12_dt__update__tmp_h0 => Dafny.Helpers.Let, DAST._IResolvedType>(_pat_let_tv0, _pat_let21_0 => Dafny.Helpers.Let, DAST._IResolvedType>(_pat_let21_0, _13_dt__update_htypeArgs_h0 => DAST.ResolvedType.create((_12_dt__update__tmp_h0).dtor_path, _13_dt__update_htypeArgs_h0, (_12_dt__update__tmp_h0).dtor_kind, (_12_dt__update__tmp_h0).dtor_attributes, (_12_dt__update__tmp_h0).dtor_properMethods, (_12_dt__update__tmp_h0).dtor_extendedTypes)))))); + _10_instanceType = DAST.Type.create_UserDefined(Dafny.Helpers.Let(_11_r, _pat_let25_0 => Dafny.Helpers.Let(_pat_let25_0, _12_dt__update__tmp_h0 => Dafny.Helpers.Let, DAST._IResolvedType>(_pat_let_tv0, _pat_let26_0 => Dafny.Helpers.Let, DAST._IResolvedType>(_pat_let26_0, _13_dt__update_htypeArgs_h0 => DAST.ResolvedType.create((_12_dt__update__tmp_h0).dtor_path, _13_dt__update_htypeArgs_h0, (_12_dt__update__tmp_h0).dtor_kind, (_12_dt__update__tmp_h0).dtor_attributes, (_12_dt__update__tmp_h0).dtor_properMethods, (_12_dt__update__tmp_h0).dtor_extendedTypes)))))); goto after_match0; } } @@ -4633,7 +4665,7 @@ public bool SameTypesButDifferentTypeParameters(DAST._IType fromType, RAST._ITyp var arr16 = new Std.Wrappers._IResult,RAST._IExpr>>>[Dafny.Helpers.ToIntChecked(dim16, "array size exceeds memory limit")]; for (int i16 = 0; i16 < dim16; i16++) { var _11_j = (BigInteger) i16; - arr16[(int)(_11_j)] = Dafny.Helpers.Let,RAST._IExpr>>>>((_4_indices).Select(_11_j), _pat_let22_0 => Dafny.Helpers.Let,RAST._IExpr>>>>(_pat_let22_0, _12_i => (this).UpcastConversionLambda((((_pat_let_tv0).dtor_resolved).dtor_typeArgs).Select(_12_i), ((_pat_let_tv1).dtor_arguments).Select(_12_i), (((_pat_let_tv2).dtor_resolved).dtor_typeArgs).Select(_12_i), ((_pat_let_tv3).dtor_arguments).Select(_12_i), _pat_let_tv4))); + arr16[(int)(_11_j)] = Dafny.Helpers.Let,RAST._IExpr>>>>((_4_indices).Select(_11_j), _pat_let27_0 => Dafny.Helpers.Let,RAST._IExpr>>>>(_pat_let27_0, _12_i => (this).UpcastConversionLambda((((_pat_let_tv0).dtor_resolved).dtor_typeArgs).Select(_12_i), ((_pat_let_tv1).dtor_arguments).Select(_12_i), (((_pat_let_tv2).dtor_resolved).dtor_typeArgs).Select(_12_i), ((_pat_let_tv3).dtor_arguments).Select(_12_i), _pat_let_tv4))); } return Dafny.Sequence,RAST._IExpr>>>>.FromArray(arr16); }))()); @@ -7612,7 +7644,7 @@ public void GenExpr(DAST._IExpression e, DCOMP._ISelfInfo selfIdent, DCOMP._IEnv for (BigInteger _423_i = BigInteger.Zero; _423_i < _hi14; _423_i++) { var _pat_let_tv0 = _420_extraAttributes; var _pat_let_tv1 = _421_formals; - _422_newFormals = Dafny.Sequence.Concat(_422_newFormals, Dafny.Sequence.FromElements(Dafny.Helpers.Let((_421_formals).Select(_423_i), _pat_let23_0 => Dafny.Helpers.Let(_pat_let23_0, _424_dt__update__tmp_h0 => Dafny.Helpers.Let, DAST._IFormal>(Dafny.Sequence.Concat(_pat_let_tv0, ((_pat_let_tv1).Select(_423_i)).dtor_attributes), _pat_let24_0 => Dafny.Helpers.Let, DAST._IFormal>(_pat_let24_0, _425_dt__update_hattributes_h0 => DAST.Formal.create((_424_dt__update__tmp_h0).dtor_name, (_424_dt__update__tmp_h0).dtor_typ, _425_dt__update_hattributes_h0))))))); + _422_newFormals = Dafny.Sequence.Concat(_422_newFormals, Dafny.Sequence.FromElements(Dafny.Helpers.Let((_421_formals).Select(_423_i), _pat_let28_0 => Dafny.Helpers.Let(_pat_let28_0, _424_dt__update__tmp_h0 => Dafny.Helpers.Let, DAST._IFormal>(Dafny.Sequence.Concat(_pat_let_tv0, ((_pat_let_tv1).Select(_423_i)).dtor_attributes), _pat_let29_0 => Dafny.Helpers.Let, DAST._IFormal>(_pat_let29_0, _425_dt__update_hattributes_h0 => DAST.Formal.create((_424_dt__update__tmp_h0).dtor_name, (_424_dt__update__tmp_h0).dtor_typ, _425_dt__update_hattributes_h0))))))); } DAST._IExpression _426_newLambda; DAST._IExpression _427_dt__update__tmp_h1 = _415_lambda; @@ -7674,7 +7706,7 @@ public void GenExpr(DAST._IExpression e, DCOMP._ISelfInfo selfIdent, DCOMP._IEnv _0_externUseDecls = Dafny.Sequence.Concat(_0_externUseDecls, Dafny.Sequence.FromElements(RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), ((RAST.__default.crate).MSel(_3_externalMod)).MSel(Dafny.Sequence.UnicodeFromString("*")))))); } if (!(_0_externUseDecls).Equals(Dafny.Sequence.FromElements())) { - s = Dafny.Sequence.Concat(Dafny.Sequence.Concat(s, (RAST.Mod.create_Mod(DCOMP.COMP.DAFNY__EXTERN__MODULE, _0_externUseDecls))._ToString(Dafny.Sequence.UnicodeFromString(""))), Dafny.Sequence.UnicodeFromString("\n")); + s = Dafny.Sequence.Concat(Dafny.Sequence.Concat(s, (RAST.Mod.create_Mod(DCOMP.COMP.DAFNY__EXTERN__MODULE, Dafny.Sequence>.FromElements(), _0_externUseDecls))._ToString(Dafny.Sequence.UnicodeFromString(""))), Dafny.Sequence.UnicodeFromString("\n")); } DafnyCompilerRustUtils._ISeqMap, DafnyCompilerRustUtils._IGatheringModule> _5_allModules; _5_allModules = DafnyCompilerRustUtils.SeqMap, DafnyCompilerRustUtils._IGatheringModule>.Empty(); diff --git a/Source/DafnyCore/GeneratedFromDafny/DafnyCompilerRustUtils.cs b/Source/DafnyCore/GeneratedFromDafny/DafnyCompilerRustUtils.cs index ad371150899..126e270a319 100644 --- a/Source/DafnyCore/GeneratedFromDafny/DafnyCompilerRustUtils.cs +++ b/Source/DafnyCore/GeneratedFromDafny/DafnyCompilerRustUtils.cs @@ -228,7 +228,7 @@ public DafnyCompilerRustUtils._IGatheringModule Merge(DafnyCompilerRustUtils._IG } else if (!((m2).is_GatheringModule)) { return this; } else { - return DafnyCompilerRustUtils.GatheringModule.create_GatheringModule(RAST.Mod.create_Mod(((this).dtor_existingMod).dtor_name, Dafny.Sequence.Concat(((this).dtor_existingMod).dtor_body, ((m2).dtor_existingMod).dtor_body)), DafnyCompilerRustUtils.GatheringModule.MergeSeqMap((this).dtor_submodules, (m2).dtor_submodules)); + return DafnyCompilerRustUtils.GatheringModule.create_GatheringModule(RAST.Mod.create_Mod(((this).dtor_existingMod).dtor_name, ((this).dtor_existingMod).dtor_attributes, Dafny.Sequence.Concat(((this).dtor_existingMod).dtor_body, ((m2).dtor_existingMod).dtor_body)), DafnyCompilerRustUtils.GatheringModule.MergeSeqMap((this).dtor_submodules, (m2).dtor_submodules)); } } public static DafnyCompilerRustUtils._ISeqMap, DafnyCompilerRustUtils._IGatheringModule> Wrap(Dafny.ISequence> containingPath, RAST._IMod rawDecl) @@ -242,7 +242,7 @@ public DafnyCompilerRustUtils._IGatheringModule Merge(DafnyCompilerRustUtils._IG } } else { Dafny.ISequence _1_enclosingModule = (containingPath).Select(BigInteger.Zero); - return DafnyCompilerRustUtils.SeqMap, DafnyCompilerRustUtils._IGatheringModule>.Single(_1_enclosingModule, DafnyCompilerRustUtils.GatheringModule.create_GatheringModule(RAST.Mod.create_Mod(_1_enclosingModule, Dafny.Sequence.FromElements()), DafnyCompilerRustUtils.GatheringModule.Wrap((containingPath).Drop(BigInteger.One), rawDecl))); + return DafnyCompilerRustUtils.SeqMap, DafnyCompilerRustUtils._IGatheringModule>.Single(_1_enclosingModule, DafnyCompilerRustUtils.GatheringModule.create_GatheringModule(RAST.Mod.create_Mod(_1_enclosingModule, Dafny.Sequence>.FromElements(), Dafny.Sequence.FromElements()), DafnyCompilerRustUtils.GatheringModule.Wrap((containingPath).Drop(BigInteger.One), rawDecl))); } } public RAST._IMod ToRust() { @@ -258,11 +258,11 @@ public RAST._IMod ToRust() { var arr13 = new RAST._IModDecl[Dafny.Helpers.ToIntChecked(dim13, "array size exceeds memory limit")]; for (int i13 = 0; i13 < dim13; i13++) { var _4_i = (BigInteger) i13; - arr13[(int)(_4_i)] = Dafny.Helpers.Let, RAST._IModDecl>((_0_keysWithContent).Select(_4_i), _pat_let18_0 => Dafny.Helpers.Let, RAST._IModDecl>(_pat_let18_0, _5_moduleName => Dafny.Helpers.Let((Dafny.Map, DafnyCompilerRustUtils._IGatheringModule>.Select(((this).dtor_submodules).dtor_values,_5_moduleName)).ToRust(), _pat_let19_0 => Dafny.Helpers.Let(_pat_let19_0, _6_submodule => RAST.ModDecl.create_ModDecl(_6_submodule))))); + arr13[(int)(_4_i)] = Dafny.Helpers.Let, RAST._IModDecl>((_0_keysWithContent).Select(_4_i), _pat_let23_0 => Dafny.Helpers.Let, RAST._IModDecl>(_pat_let23_0, _5_moduleName => Dafny.Helpers.Let((Dafny.Map, DafnyCompilerRustUtils._IGatheringModule>.Select(((this).dtor_submodules).dtor_values,_5_moduleName)).ToRust(), _pat_let24_0 => Dafny.Helpers.Let(_pat_let24_0, _6_submodule => RAST.ModDecl.create_ModDecl(_6_submodule))))); } return Dafny.Sequence.FromArray(arr13); }))()); - return RAST.Mod.create_Mod((_2_dt__update__tmp_h0).dtor_name, _3_dt__update_hbody_h0); + return RAST.Mod.create_Mod((_2_dt__update__tmp_h0).dtor_name, (_2_dt__update__tmp_h0).dtor_attributes, _3_dt__update_hbody_h0); } } } diff --git a/Source/DafnyCore/GeneratedFromDafny/FactorPathsOptimization.cs b/Source/DafnyCore/GeneratedFromDafny/FactorPathsOptimization.cs index f3fa77fd41f..a3e803ffb88 100644 --- a/Source/DafnyCore/GeneratedFromDafny/FactorPathsOptimization.cs +++ b/Source/DafnyCore/GeneratedFromDafny/FactorPathsOptimization.cs @@ -34,11 +34,11 @@ public static RAST._IMod applyPrefix(RAST._IMod mod, RAST._IPath SelfPath) })))(SelfPath, _5_pathsToRemove, mod)); RAST._IMod _13_dt__update__tmp_h0 = mod; Dafny.ISequence _14_dt__update_hbody_h0 = Dafny.Sequence.Concat(_6_imports, _7_rewrittenDeclarations); - return RAST.Mod.create_Mod((_13_dt__update__tmp_h0).dtor_name, _14_dt__update_hbody_h0); + return RAST.Mod.create_Mod((_13_dt__update__tmp_h0).dtor_name, (_13_dt__update__tmp_h0).dtor_attributes, _14_dt__update_hbody_h0); } } public static __T UniqueElementOf<__T>(Dafny.ISet<__T> s) { - return Dafny.Helpers.Let(0, _let_dummy_9 => { + return Dafny.Helpers.Let(0, _let_dummy_14 => { __T _0_e = default(__T); foreach (__T _assign_such_that_0 in (s).Elements) { _0_e = (__T)_assign_such_that_0; @@ -262,9 +262,9 @@ public static RAST._IType ReplaceType(RAST._IType t, Dafny.IMap ReplaceTypeParams(Dafny.ISequence typeParams, Dafny.IMap,RAST._IPath> replacement) { return Std.Collections.Seq.__default.Map(Dafny.Helpers.Id,RAST._IPath>, Func>>((_0_replacement) => ((System.Func)((_1_t) => { - return Dafny.Helpers.Let(_1_t, _pat_let10_0 => Dafny.Helpers.Let(_pat_let10_0, _2_dt__update__tmp_h0 => Dafny.Helpers.Let, RAST._ITypeParamDecl>(Std.Collections.Seq.__default.Map(Dafny.Helpers.Id,RAST._IPath>, Func>>((_3_replacement) => ((System.Func)((_4_constraint) => { + return Dafny.Helpers.Let(_1_t, _pat_let15_0 => Dafny.Helpers.Let(_pat_let15_0, _2_dt__update__tmp_h0 => Dafny.Helpers.Let, RAST._ITypeParamDecl>(Std.Collections.Seq.__default.Map(Dafny.Helpers.Id,RAST._IPath>, Func>>((_3_replacement) => ((System.Func)((_4_constraint) => { return FactorPathsOptimization.__default.ReplaceType(_4_constraint, _3_replacement); - })))(_0_replacement), (_1_t).dtor_constraints), _pat_let11_0 => Dafny.Helpers.Let, RAST._ITypeParamDecl>(_pat_let11_0, _5_dt__update_hconstraints_h0 => RAST.TypeParamDecl.create((_2_dt__update__tmp_h0).dtor_name, _5_dt__update_hconstraints_h0))))); + })))(_0_replacement), (_1_t).dtor_constraints), _pat_let16_0 => Dafny.Helpers.Let, RAST._ITypeParamDecl>(_pat_let16_0, _5_dt__update_hconstraints_h0 => RAST.TypeParamDecl.create((_2_dt__update__tmp_h0).dtor_name, _5_dt__update_hconstraints_h0))))); })))(replacement), typeParams); } public static RAST._IImpl ReplaceImplDecl(RAST._IImpl impl, Dafny.IMap,RAST._IPath> replacement) @@ -306,14 +306,14 @@ public static RAST._IFields ReplaceFields(RAST._IFields fields, Dafny.IMap _0_sFields = _source0.dtor_fields; return RAST.Fields.create_NamedFields(Std.Collections.Seq.__default.Map(Dafny.Helpers.Id,RAST._IPath>, Func>>((_1_replacement) => ((System.Func)((_2_f) => { - return Dafny.Helpers.Let(_2_f, _pat_let12_0 => Dafny.Helpers.Let(_pat_let12_0, _3_dt__update__tmp_h0 => Dafny.Helpers.Let(Dafny.Helpers.Let((_2_f).dtor_formal, _pat_let14_0 => Dafny.Helpers.Let(_pat_let14_0, _4_dt__update__tmp_h1 => Dafny.Helpers.Let(FactorPathsOptimization.__default.ReplaceType(((_2_f).dtor_formal).dtor_tpe, _1_replacement), _pat_let15_0 => Dafny.Helpers.Let(_pat_let15_0, _5_dt__update_htpe_h0 => RAST.Formal.create((_4_dt__update__tmp_h1).dtor_name, _5_dt__update_htpe_h0))))), _pat_let13_0 => Dafny.Helpers.Let(_pat_let13_0, _6_dt__update_hformal_h0 => RAST.Field.create((_3_dt__update__tmp_h0).dtor_visibility, _6_dt__update_hformal_h0))))); + return Dafny.Helpers.Let(_2_f, _pat_let17_0 => Dafny.Helpers.Let(_pat_let17_0, _3_dt__update__tmp_h0 => Dafny.Helpers.Let(Dafny.Helpers.Let((_2_f).dtor_formal, _pat_let19_0 => Dafny.Helpers.Let(_pat_let19_0, _4_dt__update__tmp_h1 => Dafny.Helpers.Let(FactorPathsOptimization.__default.ReplaceType(((_2_f).dtor_formal).dtor_tpe, _1_replacement), _pat_let20_0 => Dafny.Helpers.Let(_pat_let20_0, _5_dt__update_htpe_h0 => RAST.Formal.create((_4_dt__update__tmp_h1).dtor_name, _5_dt__update_htpe_h0))))), _pat_let18_0 => Dafny.Helpers.Let(_pat_let18_0, _6_dt__update_hformal_h0 => RAST.Field.create((_3_dt__update__tmp_h0).dtor_visibility, _6_dt__update_hformal_h0))))); })))(replacement), _0_sFields)); } } { Dafny.ISequence _7_sFields = _source0.dtor_types; return RAST.Fields.create_NamelessFields(Std.Collections.Seq.__default.Map(Dafny.Helpers.Id,RAST._IPath>, Func>>((_8_replacement) => ((System.Func)((_9_f) => { - return Dafny.Helpers.Let(_9_f, _pat_let16_0 => Dafny.Helpers.Let(_pat_let16_0, _10_dt__update__tmp_h2 => Dafny.Helpers.Let(FactorPathsOptimization.__default.ReplaceType((_9_f).dtor_tpe, _8_replacement), _pat_let17_0 => Dafny.Helpers.Let(_pat_let17_0, _11_dt__update_htpe_h1 => RAST.NamelessField.create((_10_dt__update__tmp_h2).dtor_visibility, _11_dt__update_htpe_h1))))); + return Dafny.Helpers.Let(_9_f, _pat_let21_0 => Dafny.Helpers.Let(_pat_let21_0, _10_dt__update__tmp_h2 => Dafny.Helpers.Let(FactorPathsOptimization.__default.ReplaceType((_9_f).dtor_tpe, _8_replacement), _pat_let22_0 => Dafny.Helpers.Let(_pat_let22_0, _11_dt__update_htpe_h1 => RAST.NamelessField.create((_10_dt__update__tmp_h2).dtor_visibility, _11_dt__update_htpe_h1))))); })))(replacement), _7_sFields)); } } diff --git a/Source/DafnyCore/GeneratedFromDafny/RAST.cs b/Source/DafnyCore/GeneratedFromDafny/RAST.cs index fda5a4701fb..5ab668e20a2 100644 --- a/Source/DafnyCore/GeneratedFromDafny/RAST.cs +++ b/Source/DafnyCore/GeneratedFromDafny/RAST.cs @@ -300,6 +300,7 @@ public interface _IMod { bool is_Mod { get; } bool is_ExternMod { get; } Dafny.ISequence dtor_name { get; } + Dafny.ISequence> dtor_attributes { get; } Dafny.ISequence dtor_body { get; } _IMod DowncastClone(); __T Fold<__T>(__T acc, Func<__T, RAST._IModDecl, __T> accBuilder); @@ -308,7 +309,7 @@ public interface _IMod { public abstract class Mod : _IMod { public Mod() { } - private static readonly RAST._IMod theDefault = create_Mod(Dafny.Sequence.Empty, Dafny.Sequence.Empty); + private static readonly RAST._IMod theDefault = create_Mod(Dafny.Sequence.Empty, Dafny.Sequence>.Empty, Dafny.Sequence.Empty); public static RAST._IMod Default() { return theDefault; } @@ -316,8 +317,8 @@ public static RAST._IMod Default() { public static Dafny.TypeDescriptor _TypeDescriptor() { return _TYPE; } - public static _IMod create_Mod(Dafny.ISequence name, Dafny.ISequence body) { - return new Mod_Mod(name, body); + public static _IMod create_Mod(Dafny.ISequence name, Dafny.ISequence> attributes, Dafny.ISequence body) { + return new Mod_Mod(name, attributes, body); } public static _IMod create_ExternMod(Dafny.ISequence name) { return new Mod_ExternMod(name); @@ -331,6 +332,12 @@ public Dafny.ISequence dtor_name { return ((Mod_ExternMod)d)._name; } } + public Dafny.ISequence> dtor_attributes { + get { + var d = this; + return ((Mod_Mod)d)._attributes; + } + } public Dafny.ISequence dtor_body { get { var d = this; @@ -347,6 +354,12 @@ public __T Fold<__T>(__T acc, Func<__T, RAST._IModDecl, __T> accBuilder) } } public Dafny.ISequence _ToString(Dafny.ISequence ind) { + var _pat_let_tv0 = ind; + var _pat_let_tv1 = ind; + var _pat_let_tv2 = ind; + var _pat_let_tv3 = ind; + var _pat_let_tv4 = ind; + var _pat_let_tv5 = ind; RAST._IMod _source0 = this; { if (_source0.is_ExternMod) { @@ -356,37 +369,36 @@ public __T Fold<__T>(__T acc, Func<__T, RAST._IModDecl, __T> accBuilder) } { Dafny.ISequence _1_name = _source0.dtor_name; - Dafny.ISequence _2_body = _source0.dtor_body; - bool _3_startWithUse = ((new BigInteger((_2_body).Count)).Sign == 1) && (((_2_body).Select(BigInteger.Zero)).is_UseDecl); - Dafny.ISequence _4_prefixIfNotUseDecl = ((_3_startWithUse) ? (Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.UnicodeFromString("\n"), ind), RAST.__default.IND)) : (Dafny.Sequence.UnicodeFromString(""))); - Dafny.ISequence _5_prefixIfUseDecl = ((_3_startWithUse) ? (Dafny.Sequence.Concat(ind, RAST.__default.IND)) : (Dafny.Sequence.UnicodeFromString(""))); - Dafny.ISequence _6_infixDecl = ((_3_startWithUse) ? (Dafny.Sequence.UnicodeFromString("\n")) : (Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.UnicodeFromString("\n\n"), ind), RAST.__default.IND))); - Dafny.ISequence _7_initialIdent = ((_3_startWithUse) ? (Dafny.Sequence.UnicodeFromString("")) : (Dafny.Sequence.Concat(ind, RAST.__default.IND))); - return Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.UnicodeFromString("pub mod "), _1_name), Dafny.Sequence.UnicodeFromString(" {")), Dafny.Sequence.UnicodeFromString("\n")), _7_initialIdent), RAST.__default.SeqToString(_2_body, Dafny.Helpers.Id, Dafny.ISequence, Dafny.ISequence, Func>>>((_8_prefixIfUseDecl, _9_prefixIfNotUseDecl, _10_ind) => ((System.Func>)((_11_modDecl) => { - return Dafny.Sequence.Concat((((_11_modDecl).is_UseDecl) ? (_8_prefixIfUseDecl) : (_9_prefixIfNotUseDecl)), (_11_modDecl)._ToString(Dafny.Sequence.Concat(_10_ind, RAST.__default.IND))); - })))(_5_prefixIfUseDecl, _4_prefixIfNotUseDecl, ind), _6_infixDecl)), Dafny.Sequence.UnicodeFromString("\n")), ind), Dafny.Sequence.UnicodeFromString("}")); + Dafny.ISequence> _2_attributes = _source0.dtor_attributes; + Dafny.ISequence _3_body = _source0.dtor_body; + return Dafny.Sequence.Concat(RAST.Attribute.ToStringMultiple(_2_attributes, ind), Dafny.Helpers.Let>(((new BigInteger((_3_body).Count)).Sign == 1) && (((_3_body).Select(BigInteger.Zero)).is_UseDecl), _pat_let5_0 => Dafny.Helpers.Let>(_pat_let5_0, _4_startWithUse => Dafny.Helpers.Let, Dafny.ISequence>(((_4_startWithUse) ? (Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.UnicodeFromString("\n"), _pat_let_tv0), RAST.__default.IND)) : (Dafny.Sequence.UnicodeFromString(""))), _pat_let6_0 => Dafny.Helpers.Let, Dafny.ISequence>(_pat_let6_0, _5_prefixIfNotUseDecl => Dafny.Helpers.Let, Dafny.ISequence>(((_4_startWithUse) ? (Dafny.Sequence.Concat(_pat_let_tv1, RAST.__default.IND)) : (Dafny.Sequence.UnicodeFromString(""))), _pat_let7_0 => Dafny.Helpers.Let, Dafny.ISequence>(_pat_let7_0, _6_prefixIfUseDecl => Dafny.Helpers.Let, Dafny.ISequence>(((_4_startWithUse) ? (Dafny.Sequence.UnicodeFromString("\n")) : (Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.UnicodeFromString("\n\n"), _pat_let_tv2), RAST.__default.IND))), _pat_let8_0 => Dafny.Helpers.Let, Dafny.ISequence>(_pat_let8_0, _7_infixDecl => Dafny.Helpers.Let, Dafny.ISequence>(((_4_startWithUse) ? (Dafny.Sequence.UnicodeFromString("")) : (Dafny.Sequence.Concat(_pat_let_tv3, RAST.__default.IND))), _pat_let9_0 => Dafny.Helpers.Let, Dafny.ISequence>(_pat_let9_0, _8_initialIdent => Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.UnicodeFromString("pub mod "), _1_name), Dafny.Sequence.UnicodeFromString(" {")), Dafny.Sequence.UnicodeFromString("\n")), _8_initialIdent), RAST.__default.SeqToString(_3_body, Dafny.Helpers.Id, Dafny.ISequence, Dafny.ISequence, Func>>>((_9_prefixIfUseDecl, _10_prefixIfNotUseDecl, _11_ind) => ((System.Func>)((_12_modDecl) => { + return Dafny.Sequence.Concat((((_12_modDecl).is_UseDecl) ? (_9_prefixIfUseDecl) : (_10_prefixIfNotUseDecl)), (_12_modDecl)._ToString(Dafny.Sequence.Concat(_11_ind, RAST.__default.IND))); + })))(_6_prefixIfUseDecl, _5_prefixIfNotUseDecl, _pat_let_tv4), _7_infixDecl)), Dafny.Sequence.UnicodeFromString("\n")), _pat_let_tv5), Dafny.Sequence.UnicodeFromString("}"))))))))))))); } } } public class Mod_Mod : Mod { public readonly Dafny.ISequence _name; + public readonly Dafny.ISequence> _attributes; public readonly Dafny.ISequence _body; - public Mod_Mod(Dafny.ISequence name, Dafny.ISequence body) : base() { + public Mod_Mod(Dafny.ISequence name, Dafny.ISequence> attributes, Dafny.ISequence body) : base() { this._name = name; + this._attributes = attributes; this._body = body; } public override _IMod DowncastClone() { if (this is _IMod dt) { return dt; } - return new Mod_Mod(_name, _body); + return new Mod_Mod(_name, _attributes, _body); } public override bool Equals(object other) { var oth = other as RAST.Mod_Mod; - return oth != null && object.Equals(this._name, oth._name) && object.Equals(this._body, oth._body); + return oth != null && object.Equals(this._name, oth._name) && object.Equals(this._attributes, oth._attributes) && object.Equals(this._body, oth._body); } public override int GetHashCode() { ulong hash = 5381; hash = ((hash << 5) + hash) + 0; hash = ((hash << 5) + hash) + ((ulong)Dafny.Helpers.GetHashCode(this._name)); + hash = ((hash << 5) + hash) + ((ulong)Dafny.Helpers.GetHashCode(this._attributes)); hash = ((hash << 5) + hash) + ((ulong)Dafny.Helpers.GetHashCode(this._body)); return (int) hash; } @@ -395,6 +407,8 @@ public override string ToString() { s += "("; s += this._name.ToVerbatimString(true); s += ", "; + s += Dafny.Helpers.ToString(this._attributes); + s += ", "; s += Dafny.Helpers.ToString(this._body); s += ")"; return s; @@ -2833,7 +2847,7 @@ public RAST._IExpr ToNullExpr() { } public bool IsMultiArray() { RAST._IType _0_t = (this).Expand(); - return ((_0_t).is_TypeApp) && (Dafny.Helpers.Let((_0_t).dtor_baseName, _pat_let5_0 => Dafny.Helpers.Let(_pat_let5_0, _1_baseName => Dafny.Helpers.Let, bool>((_0_t).dtor_arguments, _pat_let6_0 => Dafny.Helpers.Let, bool>(_pat_let6_0, _2_args => ((((((new BigInteger((_2_args).Count)) == (BigInteger.One)) && ((_1_baseName).is_TypeFromPath)) && (((_1_baseName).dtor_path).is_PMemberSelect)) && (object.Equals(((_1_baseName).dtor_path).dtor_base, RAST.__default.dafny__runtime))) && ((new BigInteger((((_1_baseName).dtor_path).dtor_name).Count)) >= (new BigInteger(5)))) && (((((_1_baseName).dtor_path).dtor_name).Subsequence(BigInteger.Zero, new BigInteger(5))).Equals(Dafny.Sequence.UnicodeFromString("Array")))))))); + return ((_0_t).is_TypeApp) && (Dafny.Helpers.Let((_0_t).dtor_baseName, _pat_let10_0 => Dafny.Helpers.Let(_pat_let10_0, _1_baseName => Dafny.Helpers.Let, bool>((_0_t).dtor_arguments, _pat_let11_0 => Dafny.Helpers.Let, bool>(_pat_let11_0, _2_args => ((((((new BigInteger((_2_args).Count)) == (BigInteger.One)) && ((_1_baseName).is_TypeFromPath)) && (((_1_baseName).dtor_path).is_PMemberSelect)) && (object.Equals(((_1_baseName).dtor_path).dtor_base, RAST.__default.dafny__runtime))) && ((new BigInteger((((_1_baseName).dtor_path).dtor_name).Count)) >= (new BigInteger(5)))) && (((((_1_baseName).dtor_path).dtor_name).Subsequence(BigInteger.Zero, new BigInteger(5))).Equals(Dafny.Sequence.UnicodeFromString("Array")))))))); } public Dafny.ISequence MultiArrayClass() { return ((((this).Expand()).dtor_baseName).dtor_path).dtor_name; @@ -5818,7 +5832,7 @@ public bool RightRequiresParentheses(RAST._IExpr right) { Dafny.ISequence _50_name = _source0.dtor_name; Std.Wrappers._IOption _51_optType = _source0.dtor_optType; Std.Wrappers._IOption _52_optExpr = _source0.dtor_optRhs; - return Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.UnicodeFromString("let "), ((object.Equals(_49_declareType, RAST.DeclareType.create_MUT())) ? (Dafny.Sequence.UnicodeFromString("mut ")) : (Dafny.Sequence.UnicodeFromString("")))), _50_name), (((_51_optType).is_Some) ? (Dafny.Sequence.Concat(Dafny.Sequence.UnicodeFromString(": "), ((_51_optType).dtor_value)._ToString(Dafny.Sequence.Concat(ind, RAST.__default.IND)))) : (Dafny.Sequence.UnicodeFromString("")))), (((_52_optExpr).is_Some) ? (Dafny.Helpers.Let, Dafny.ISequence>(((_52_optExpr).dtor_value)._ToString(Dafny.Sequence.Concat(ind, RAST.__default.IND)), _pat_let7_0 => Dafny.Helpers.Let, Dafny.ISequence>(_pat_let7_0, _53_optExprString => (((_53_optExprString).Equals(Dafny.Sequence.UnicodeFromString(""))) ? (Dafny.Sequence.Concat(Dafny.Sequence.UnicodeFromString("= /*issue with empty RHS*/"), ((((_52_optExpr).dtor_value).is_RawExpr) ? (Dafny.Sequence.UnicodeFromString("Empty Raw expr")) : (((((_52_optExpr).dtor_value).is_LiteralString) ? (Dafny.Sequence.UnicodeFromString("Empty string literal")) : (((((_52_optExpr).dtor_value).is_LiteralInt) ? (Dafny.Sequence.UnicodeFromString("Empty int literal")) : (Dafny.Sequence.UnicodeFromString("Another case"))))))))) : (Dafny.Sequence.Concat(Dafny.Sequence.UnicodeFromString(" = "), _53_optExprString)))))) : (Dafny.Sequence.UnicodeFromString("")))), Dafny.Sequence.UnicodeFromString(";")); + return Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.UnicodeFromString("let "), ((object.Equals(_49_declareType, RAST.DeclareType.create_MUT())) ? (Dafny.Sequence.UnicodeFromString("mut ")) : (Dafny.Sequence.UnicodeFromString("")))), _50_name), (((_51_optType).is_Some) ? (Dafny.Sequence.Concat(Dafny.Sequence.UnicodeFromString(": "), ((_51_optType).dtor_value)._ToString(Dafny.Sequence.Concat(ind, RAST.__default.IND)))) : (Dafny.Sequence.UnicodeFromString("")))), (((_52_optExpr).is_Some) ? (Dafny.Helpers.Let, Dafny.ISequence>(((_52_optExpr).dtor_value)._ToString(Dafny.Sequence.Concat(ind, RAST.__default.IND)), _pat_let12_0 => Dafny.Helpers.Let, Dafny.ISequence>(_pat_let12_0, _53_optExprString => (((_53_optExprString).Equals(Dafny.Sequence.UnicodeFromString(""))) ? (Dafny.Sequence.Concat(Dafny.Sequence.UnicodeFromString("= /*issue with empty RHS*/"), ((((_52_optExpr).dtor_value).is_RawExpr) ? (Dafny.Sequence.UnicodeFromString("Empty Raw expr")) : (((((_52_optExpr).dtor_value).is_LiteralString) ? (Dafny.Sequence.UnicodeFromString("Empty string literal")) : (((((_52_optExpr).dtor_value).is_LiteralInt) ? (Dafny.Sequence.UnicodeFromString("Empty int literal")) : (Dafny.Sequence.UnicodeFromString("Another case"))))))))) : (Dafny.Sequence.Concat(Dafny.Sequence.UnicodeFromString(" = "), _53_optExprString)))))) : (Dafny.Sequence.UnicodeFromString("")))), Dafny.Sequence.UnicodeFromString(";")); } } { @@ -6107,7 +6121,7 @@ public RAST._IExpr Apply1(RAST._IExpr argument) { return RAST.Expr.create_Call(this, Dafny.Sequence.FromElements(argument)); } public bool IsLhsIdentifier() { - return ((this).is_Identifier) || (((this).is_Call) && (((((((this).dtor_obj).is_ExprFromPath) && (object.Equals(((this).dtor_obj).dtor_path, (RAST.__default.dafny__runtime).MSel(Dafny.Sequence.UnicodeFromString("modify!"))))) && ((new BigInteger(((this).dtor_arguments).Count)) == (BigInteger.One))) && ((((this).dtor_arguments).Select(BigInteger.Zero)).is_Identifier)) || ((((((this).dtor_obj).is_ExprFromPath) && (object.Equals(((this).dtor_obj).dtor_path, (RAST.__default.dafny__runtime).MSel(Dafny.Sequence.UnicodeFromString("md!"))))) && ((new BigInteger(((this).dtor_arguments).Count)) == (BigInteger.One))) && (Dafny.Helpers.Let(((this).dtor_arguments).Select(BigInteger.Zero), _pat_let8_0 => Dafny.Helpers.Let(_pat_let8_0, _0_lhs => (((_0_lhs).is_Call) && (((_0_lhs).dtor_obj).is_Select)) && ((((_0_lhs).dtor_obj).dtor_obj).is_Identifier))))))); + return ((this).is_Identifier) || (((this).is_Call) && (((((((this).dtor_obj).is_ExprFromPath) && (object.Equals(((this).dtor_obj).dtor_path, (RAST.__default.dafny__runtime).MSel(Dafny.Sequence.UnicodeFromString("modify!"))))) && ((new BigInteger(((this).dtor_arguments).Count)) == (BigInteger.One))) && ((((this).dtor_arguments).Select(BigInteger.Zero)).is_Identifier)) || ((((((this).dtor_obj).is_ExprFromPath) && (object.Equals(((this).dtor_obj).dtor_path, (RAST.__default.dafny__runtime).MSel(Dafny.Sequence.UnicodeFromString("md!"))))) && ((new BigInteger(((this).dtor_arguments).Count)) == (BigInteger.One))) && (Dafny.Helpers.Let(((this).dtor_arguments).Select(BigInteger.Zero), _pat_let13_0 => Dafny.Helpers.Let(_pat_let13_0, _0_lhs => (((_0_lhs).is_Call) && (((_0_lhs).dtor_obj).is_Select)) && ((((_0_lhs).dtor_obj).dtor_obj).is_Identifier))))))); } public Dafny.ISequence LhsIdentifierName() { if ((this).is_Identifier) { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/cargotest.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/cargotest.dfy new file mode 100644 index 00000000000..be2eee7921d --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/cargotest.dfy @@ -0,0 +1,21 @@ +// NONUNIFORM: Test of cargo test to support Dafny tests +// RUN: %baredafny build --target=rs "%s" > "%t" +// RUN: %exits-with 101 "%S/cargotest-rust/cargo" test >> "%t" +// RUN: %OutputCheck --file-to-check "%t" "%S/cargotest1.check" +// RUN: %OutputCheck --file-to-check "%t" "%S/cargotest2.check" +// RUN: %OutputCheck --file-to-check "%t" "%S/cargotest3.check" +// RUN: %OutputCheck --file-to-check "%S/cargotest-rust/src/cargotest.rs" "%S/cargotestoutput.check" + +module {:rust_cfg_test} Tests { + method {:test} TestFail1() { + expect true == false; + } + + method {:test} TestFail2() { + expect false == true; + } + + method {:test} TestSucceed3() { + expect true == true; + } +} \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/cargotest1.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/cargotest1.check new file mode 100644 index 00000000000..d5ad83a98a8 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/cargotest1.check @@ -0,0 +1 @@ +// CHECK: test Tests::TestFail1 ... FAILED \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/cargotest2.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/cargotest2.check new file mode 100644 index 00000000000..932619e778b --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/cargotest2.check @@ -0,0 +1 @@ +// CHECK: test Tests::TestFail2 ... FAILED \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/cargotest3.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/cargotest3.check new file mode 100644 index 00000000000..10d9d0f1dc8 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/cargotest3.check @@ -0,0 +1 @@ +// CHECK: test Tests::TestSucceed3 ... ok \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/cargotestoutput.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/cargotestoutput.check new file mode 100644 index 00000000000..3b60de400f9 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/cargotestoutput.check @@ -0,0 +1 @@ +// CHECK-L: #[cfg(test)] \ No newline at end of file diff --git a/Source/XUnitExtensions/Lit/ShellLitCommand.cs b/Source/XUnitExtensions/Lit/ShellLitCommand.cs index 50bdf1fb2f2..8f87d3e8bd9 100644 --- a/Source/XUnitExtensions/Lit/ShellLitCommand.cs +++ b/Source/XUnitExtensions/Lit/ShellLitCommand.cs @@ -23,7 +23,7 @@ public async Task Execute(TextReader inputReader, TextWriter outputWriter, TextWriter errorWriter) { using var process = new Process(); - if (shellCommand.Contains('/') && Path.GetFileName(shellCommand) is var command and "python3") { + if (shellCommand.Contains('/') && Path.GetFileName(shellCommand) is var command and ("python3" or "cargo")) { var workingDir = Path.GetDirectoryName(shellCommand); process.StartInfo.WorkingDirectory = workingDir; shellCommand = command; diff --git a/docs/DafnyRef/integration- rust/IntegrationRust.md b/docs/DafnyRef/integration- rust/IntegrationRust.md index ab78e8b09e9..6eb44ff9d4b 100644 --- a/docs/DafnyRef/integration- rust/IntegrationRust.md +++ b/docs/DafnyRef/integration- rust/IntegrationRust.md @@ -177,3 +177,8 @@ fn main() { super::Test::_default::extern_y(); } ``` + +# Tests + +* Methods with the `{:test}` attribute will produce an equivalent `#[test]` method that can be run via `cargo test` on the code produced by `dafny build`. +* Modules with the `{:rust_cfg_test}` attribute will have the attribute `#[cfg(test)]` when translated to Rust. \ No newline at end of file diff --git a/docs/dev/news/5676.feat b/docs/dev/news/5676.feat new file mode 100644 index 00000000000..0617d12494a --- /dev/null +++ b/docs/dev/news/5676.feat @@ -0,0 +1,2 @@ +Dafny-to-Rust: `{:test}` methods generate `#[test]` wrappers in Rust that can be invoked using `cargo test`. +Similarly, `{:rust_cfg_test}` on modules generates a `#[cfg(test)]` in the resulting rust module.