diff --git a/Source/DafnyCore.Test/GeneratedFromDafny/FactorPathsOptimizationTest.cs b/Source/DafnyCore.Test/GeneratedFromDafny/FactorPathsOptimizationTest.cs index b2f3f183384..619b9656ad7 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(), 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()))))); + FactorPathsOptimizationTest.__default.ShouldBeEqual(Dafny.Helpers.Id>(FactorPathsOptimization.__default.apply(RAST.__default.crate))(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(Dafny.Helpers.Id>(FactorPathsOptimization.__default.apply(RAST.__default.crate))(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/DafnyExecutableBackend.cs b/Source/DafnyCore/Backends/DafnyExecutableBackend.cs index b3d74485093..00efe28dca5 100644 --- a/Source/DafnyCore/Backends/DafnyExecutableBackend.cs +++ b/Source/DafnyCore/Backends/DafnyExecutableBackend.cs @@ -55,13 +55,12 @@ public override void Compile(Program dafnyProgram, string dafnyProgramName, Conc ((DafnyCodeGenerator)codeGenerator).Start(); codeGenerator.Compile(dafnyProgram, new ConcreteSyntaxTree()); var dast = ((DafnyCodeGenerator)codeGenerator).Build(); - var o = DafnyCodeGenerator.Compile( + DafnyCodeGenerator.Compile( (Sequence)Sequence.FromArray(dast.ToArray()), (Sequence>)Sequence>.FromArray( ImportFiles(dafnyProgramName).Select(fileName => Sequence.UnicodeFromString(Path.GetFileName(fileName))).ToArray() - )); - output.Write(o.ToVerbatimString(false)); + ), output); } public override void EmitCallToMain(Method mainMethod, string baseName, ConcreteSyntaxTree output) { diff --git a/Source/DafnyCore/Backends/DafnyWrittenCodeGenerator.cs b/Source/DafnyCore/Backends/DafnyWrittenCodeGenerator.cs index e2a67e13d7a..ba6d3b79dfe 100644 --- a/Source/DafnyCore/Backends/DafnyWrittenCodeGenerator.cs +++ b/Source/DafnyCore/Backends/DafnyWrittenCodeGenerator.cs @@ -5,7 +5,7 @@ namespace Microsoft.Dafny.Compilers { public abstract class DafnyWrittenCodeGenerator { - public abstract ISequence Compile(Sequence program, Sequence> otherFiles); + public abstract void Compile(Sequence program, Sequence> otherFiles, ConcreteSyntaxTree w); public abstract ISequence EmitCallToMain(string fullName); diff --git a/Source/DafnyCore/Backends/ResolvedDesugaredExecutableDafny/ResolvedDesugaredExecutableDafnyCodeGenerator.cs b/Source/DafnyCore/Backends/ResolvedDesugaredExecutableDafny/ResolvedDesugaredExecutableDafnyCodeGenerator.cs index 6691d140b93..73dd85af21f 100644 --- a/Source/DafnyCore/Backends/ResolvedDesugaredExecutableDafny/ResolvedDesugaredExecutableDafnyCodeGenerator.cs +++ b/Source/DafnyCore/Backends/ResolvedDesugaredExecutableDafny/ResolvedDesugaredExecutableDafnyCodeGenerator.cs @@ -8,8 +8,8 @@ namespace Microsoft.Dafny.Compilers; class ResolvedDesugaredExecutableDafnyCodeGenerator : DafnyWrittenCodeGenerator { - public override ISequence Compile(Sequence program, Sequence> otherFiles) { - return COMP.Compile(program); + public override void Compile(Sequence program, Sequence> otherFiles, ConcreteSyntaxTree w) { + w.Write(COMP.Compile(program).ToVerbatimString(false)); } public override ISequence EmitCallToMain(string fullName) { 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 2a3afea326f..4956c4d01e7 100644 --- a/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-path-simplification.dfy +++ b/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-path-simplification.dfy @@ -19,7 +19,7 @@ module FactorPathsOptimizationTest { var T := TIdentifier("T"); var std_any_Any := global.MSel("std").MSel("any").MSel("Any"); var Any := TIdentifier("Any"); - ShouldBeEqual(apply( + ShouldBeEqual(apply(crate)( Mod("onemodule", [], [ StructDecl( Struct([], "test", [T_Decl], @@ -40,7 +40,7 @@ module FactorPathsOptimizationTest { ImplDecl(Impl([T_Decl_simp], TIdentifier("test").Apply([T]), "", [])), ImplDecl(ImplFor([T_Decl_simp], Any, TIdentifier("test").Apply([T]), "", [])) ])); - ShouldBeEqual(apply( + ShouldBeEqual(apply(crate)( Mod("onemodule", [], [ ImplDecl( ImplFor( @@ -71,8 +71,8 @@ module FactorPathsOptimization { return s; }*/ - function apply(mod: Mod): Mod { - applyPrefix(mod, crate.MSel(mod.name)) + function apply(thisFile: Path): (Mod -> Mod) { + (mod: Mod) => applyPrefix(mod, thisFile.MSel(mod.name)) } function applyPrefix(mod: Mod, SelfPath: Path): Mod { diff --git a/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy b/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy index e46014287b9..1ce953015fc 100644 --- a/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy +++ b/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy @@ -1676,7 +1676,9 @@ module {:extern "DCOMP"} DafnyToRustCompiler { ASSIGNED_PREFIX + "_" + rustName } - datatype ObjectType = RawPointers | RcMut + datatype PointerType = Raw | RcMut + datatype CharType = UTF16 | UTF32 + datatype RootType = RootCrate | RootPath(moduleName: string) datatype GenTypeContext = GenTypeContext(forTraitParents: bool) @@ -1791,43 +1793,47 @@ module {:extern "DCOMP"} DafnyToRustCompiler { } class COMP { - const UnicodeChars: bool - const DafnyChar := if UnicodeChars then "DafnyChar" else "DafnyCharUTF16" - const DafnyCharUnderlying := if UnicodeChars then R.RawType("char") else R.RawType("u16") - const string_of := if UnicodeChars then "string_of" else "string_utf16_of" + const charType: CharType + const pointerType: PointerType + const rootType: RootType + + const thisFile: R.Path := if rootType.RootCrate? then R.crate else R.crate.MSel(rootType.moduleName) + + const DafnyChar := if charType.UTF32? then "DafnyChar" else "DafnyCharUTF16" + const DafnyCharUnderlying := if charType.UTF32? then R.RawType("char") else R.RawType("u16") + const string_of := if charType.UTF32? then "string_of" else "string_utf16_of" const allocate := - if ObjectType.RawPointers? then "allocate" else "allocate_object" + if pointerType.Raw? then "allocate" else "allocate_object" const allocate_fn := "_" + allocate const update_field_uninit_macro := - if ObjectType.RawPointers? then "update_field_uninit!" else "update_field_uninit_object!" + if pointerType.Raw? then "update_field_uninit!" else "update_field_uninit_object!" const thisInConstructor := - if ObjectType.RawPointers? then R.Identifier("this") else R.Identifier("this").Clone() + if pointerType.Raw? then R.Identifier("this") else R.Identifier("this").Clone() const array_construct := - if ObjectType.RawPointers? then "construct" else "construct_object" - const modify_macro := R.dafny_runtime.MSel(if ObjectType.RawPointers? then "modify!" else "md!").AsExpr() - const read_macro := R.dafny_runtime.MSel(if ObjectType.RawPointers? then "read!" else "rd!").AsExpr() + if pointerType.Raw? then "construct" else "construct_object" + const modify_macro := R.dafny_runtime.MSel(if pointerType.Raw? then "modify!" else "md!").AsExpr() + const read_macro := R.dafny_runtime.MSel(if pointerType.Raw? then "read!" else "rd!").AsExpr() function Object(underlying: R.Type): R.Type { - if ObjectType.RawPointers? then R.PtrType(underlying) else R.ObjectType(underlying) + if pointerType.Raw? then R.PtrType(underlying) else R.ObjectType(underlying) } - const placebos_usize := if ObjectType.RawPointers? then "placebos_usize" else "placebos_usize_object" + const placebos_usize := if pointerType.Raw? then "placebos_usize" else "placebos_usize_object" const update_field_if_uninit_macro := - if ObjectType.RawPointers? then "update_field_if_uninit!" else "update_field_if_uninit_object!" + if pointerType.Raw? then "update_field_if_uninit!" else "update_field_if_uninit_object!" const Upcast := - if ObjectType.RawPointers? then "Upcast" else "UpcastObject" + if pointerType.Raw? then "Upcast" else "UpcastObject" const UpcastFnMacro := Upcast + "Fn!" const upcast := - if ObjectType.RawPointers? then "upcast" else "upcast_object" + if pointerType.Raw? then "upcast" else "upcast_object" const downcast := - if ObjectType.RawPointers? then "cast!" else "cast_object!" + if pointerType.Raw? then "cast!" else "cast_object!" function UnreachablePanicIfVerified(optText: string := ""): string { - if ObjectType.RawPointers? then "unsafe { ::std::hint::unreachable_unchecked() }" else + if pointerType.Raw? then "unsafe { ::std::hint::unreachable_unchecked() }" else if optText == "" then "panic!()" else "panic!(\"" + optText + "\")" } - const ObjectType: ObjectType static const TailRecursionPrefix := "_r" @@ -1837,11 +1843,12 @@ module {:extern "DCOMP"} DafnyToRustCompiler { static const DAFNY_EXTERN_MODULE := "_dafny_externs" - constructor(unicodeChars: bool, objectType: ObjectType) { - this.UnicodeChars := unicodeChars; - this.ObjectType := objectType; + constructor(charType: CharType, pointerType: PointerType, rootType: RootType) { + this.charType := charType; + this.pointerType := pointerType; + this.rootType := rootType; this.error := None; // If error, then the generated code contains Unsupported: .* - this.optimizations := [FactorPathsOptimization.apply]; + this.optimizations := [FactorPathsOptimization.apply(thisFile)]; new; } @@ -1873,7 +1880,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler { var body, allmodules := GenModuleBody(mod, mod.body.value, containingPath + [Ident.Ident(innerName)]); if optExtern.SimpleExtern? { if mod.requiresExterns { - body := [R.UseDecl(R.Use(R.PUB, R.crate.MSel(DAFNY_EXTERN_MODULE).MSel(ReplaceDotByDoubleColon(optExtern.overrideName)).MSel("*")))] + body; + body := [R.UseDecl(R.Use(R.PUB, thisFile.MSel(DAFNY_EXTERN_MODULE).MSel(ReplaceDotByDoubleColon(optExtern.overrideName)).MSel("*")))] + body; } } else if optExtern.AdvancedExtern? { error := Some("Externs on modules can only have 1 string argument"); @@ -2939,7 +2946,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler { } } - static method GenPath(p: seq, escape: bool := true) returns (r: R.Path) { + method GenPath(p: seq, escape: bool := true) returns (r: R.Path) { if |p| == 0 { return R.Self(); } else { @@ -2949,7 +2956,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler { else if p[0].id.dafny_name == "_System" then R.dafny_runtime else - R.Crate(); + thisFile; for i := 0 to |p| { var name := p[i].id; if escape { @@ -2966,12 +2973,12 @@ module {:extern "DCOMP"} DafnyToRustCompiler { } } - static method GenPathType(p: seq) returns (t: R.Type) { + method GenPathType(p: seq) returns (t: R.Type) { var p := GenPath(p, true); t := p.AsType(); } - static method GenPathExpr(p: seq, escape: bool := true) returns (e: R.Expr) { + method GenPathExpr(p: seq, escape: bool := true) returns (e: R.Expr) { if |p| == 0 { return R.self; } @@ -3219,18 +3226,18 @@ module {:extern "DCOMP"} DafnyToRustCompiler { if (forTrait) { // Mutability is required when not using raw pointers, even for functione, because // --release optimisations sometimes removes the code to increment the reference counting on upcasting - var selfFormal := if m.wasFunction && ObjectType.RawPointers? then R.Formal.selfBorrowed else R.Formal.selfBorrowedMut; + var selfFormal := if m.wasFunction && pointerType.Raw? then R.Formal.selfBorrowed else R.Formal.selfBorrowedMut; params := [selfFormal] + params; } else { var tpe := GenType(instanceType, GenTypeContext.default()); if selfId == "this" { - if ObjectType.RcMut? { + if pointerType.RcMut? { tpe := R.Borrowed(tpe); } // For raw pointers, no borrowing is necessary, because it implements the Copy type } else if selfId == "self" { if tpe.IsObjectOrPointer() { // For classes and traits - if m.wasFunction && ObjectType.RawPointers? { + if m.wasFunction && pointerType.Raw? { tpe := R.SelfBorrowed; } else { tpe := R.SelfBorrowedMut; @@ -3937,7 +3944,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler { } case Literal(CharLiteral(c)) => { r := R.LiteralInt(Strings.OfNat(c as nat)); - if !UnicodeChars { + if !charType.UTF32? { r := R.TypeAscription(r, R.U16); } else { r := @@ -3952,7 +3959,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler { } case Literal(Null(tpe)) => { var tpeGen := GenType(tpe, GenTypeContext.default()); - if ObjectType.RawPointers? { + if pointerType.Raw? { r := R.std.MSel("ptr").FSel("null_mut"); } else { r := R.TypeAscription(R.dafny_runtime.MSel("Object").AsExpr().Apply1(R.RawExpr("None")), tpeGen); @@ -4086,7 +4093,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler { match op { case Eq(referential) => { if (referential) { - if ObjectType.RawPointers? { + if pointerType.Raw? { error := Some("Cannot compare raw pointers yet - need to wrap them with a structure to ensure they are compared properly"); r := R.RawExpr(error.value); } else { @@ -4448,7 +4455,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler { case (Primitive(Int), Primitive(Char)) => { var rhsType := GenType(toTpe, GenTypeContext.default()); var recursiveGen, _, recIdents := GenExpr(expr, selfIdent, env, OwnershipOwned); - r := R.RawExpr("::dafny_runtime::" + DafnyChar + "(" + (if UnicodeChars then "char::from_u32(::from(" + recursiveGen.ToString(IND) + ").unwrap())" + if UnicodeChars then ".unwrap())" else ""); + r := R.RawExpr("::dafny_runtime::" + DafnyChar + "(" + (if charType.UTF32? then "char::from_u32(::from(" + recursiveGen.ToString(IND) + ").unwrap())" + if charType.UTF32? then ".unwrap())" else ""); r, resultingOwnership := FromOwned(r, expectedOwnership); readIdents := recIdents; } @@ -5151,12 +5158,10 @@ module {:extern "DCOMP"} DafnyToRustCompiler { r := R.Identifier("this"); case _ => } - if ObjectType.RcMut? { - r := r.Clone(); - } - if ObjectType.RawPointers? { + if pointerType.Raw? { r := read_macro.Apply1(r); } else { + r := r.Clone(); r := modify_macro.Apply1(r); // Functions have to take &mut because of upcasting } } @@ -5205,7 +5210,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler { case IndexRange(on, isArray, low, high) => { var onExpectedOwnership := if isArray then - if ObjectType.RawPointers? then + if pointerType.Raw? then OwnershipOwned else OwnershipBorrowed @@ -5243,7 +5248,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler { methodName := "_" + methodName; } var object_suffix := - if ObjectType.RawPointers? then "" else "_object"; + if pointerType.Raw? then "" else "_object"; r := R.dafny_runtime_Sequence.FSel("from_array"+methodName+object_suffix).Apply([onExpr] + arguments); } else { if methodName != "" { @@ -5283,14 +5288,14 @@ module {:extern "DCOMP"} DafnyToRustCompiler { var onExpr, recOwnership, recIdents; if base.Trait? || base.Class? { onExpr, recOwnership, recIdents := GenExpr(on, selfIdent, env, OwnershipOwned); - if ObjectType.RawPointers? { + if pointerType.Raw? { onExpr := read_macro.Apply1(onExpr); } else { onExpr := modify_macro.Apply1(onExpr); } readIdents := readIdents + recIdents; } else { - var expectedOnOwnership := if ObjectType.RawPointers? then OwnershipBorrowed else OwnershipBorrowedMut; + var expectedOnOwnership := if pointerType.Raw? then OwnershipBorrowed else OwnershipBorrowedMut; onExpr, recOwnership, recIdents := GenExpr(on, selfIdent, env, expectedOnOwnership); readIdents := readIdents + recIdents; } @@ -5311,7 +5316,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler { case CallName(_, Some(tpe), _, _, _) => var typ := GenType(tpe, GenTypeContext.default()); if typ.IsObjectOrPointer() { - if ObjectType.RawPointers? { + if pointerType.Raw? { onExpr := read_macro.Apply1(onExpr); } else { onExpr := modify_macro.Apply1(onExpr); diff --git a/Source/DafnyCore/Backends/Rust/RustBackend.cs b/Source/DafnyCore/Backends/Rust/RustBackend.cs index b6f17bcec10..c0d06a59631 100644 --- a/Source/DafnyCore/Backends/Rust/RustBackend.cs +++ b/Source/DafnyCore/Backends/Rust/RustBackend.cs @@ -1,6 +1,7 @@ using System; using System.Collections.Generic; using System.Collections.ObjectModel; +using System.CommandLine; using System.Diagnostics.Contracts; using System.IO; using System.Linq; @@ -24,6 +25,15 @@ public class RustBackend : DafnyExecutableBackend { public override bool SupportsInMemoryCompilation => false; public override bool TextualTargetIsExecutable => false; + public static readonly Option RustModuleNameOption = new("--rust-module-name", + @"The enclosing Rust module name for the currently translated code, i.e. what goes between crate:: ... ::module_name".TrimStart()) { + }; + public override IEnumerable> SupportedOptions => new List> { RustModuleNameOption }; + + static RustBackend() { + OptionRegistry.RegisterOption(RustModuleNameOption, OptionScope.Translation); + } + public override IReadOnlySet SupportedNativeTypes => new HashSet { "byte", "sbyte", "ushort", "short", "uint", "int", "ulong", "long", "udoublelong", "doublelong" }; diff --git a/Source/DafnyCore/Backends/Rust/RustCodeGenerator.cs b/Source/DafnyCore/Backends/Rust/RustCodeGenerator.cs index 243eb5ba08f..c731b7386bf 100644 --- a/Source/DafnyCore/Backends/Rust/RustCodeGenerator.cs +++ b/Source/DafnyCore/Backends/Rust/RustCodeGenerator.cs @@ -1,4 +1,5 @@ using System; +using System.CommandLine; using System.Configuration; using System.IO; using System.Linq; @@ -14,15 +15,23 @@ public RustCodeGenerator(DafnyOptions options) { this.Options = options; } - public override ISequence Compile(Sequence program, Sequence> otherFiles) { + public override void Compile(Sequence program, Sequence> otherFiles, ConcreteSyntaxTree w) { var c = new DCOMP.COMP(); - c.__ctor(Options.Get(CommonOptionBag.UnicodeCharacters), - Options.Get(CommonOptionBag.RawPointers) ? ObjectType.create_RawPointers() : ObjectType.create_RcMut()); + var charType = Options.Get(CommonOptionBag.UnicodeCharacters) + ? DCOMP.CharType.create_UTF32() + : DCOMP.CharType.create_UTF16(); + var pointerType = Options.Get(CommonOptionBag.RawPointers) + ? PointerType.create_Raw() + : PointerType.create_RcMut(); + var rootType = Options.Get(RustBackend.RustModuleNameOption) is { } opt && opt != "" ? + RootType.create_RootPath(Sequence.UnicodeFromString(opt)) + : RootType.create_RootCrate(); + c.__ctor(charType, pointerType, rootType); var s = c.Compile(program, otherFiles); if (!Options.Get(CommonOptionBag.EmitUncompilableCode) && c.error.is_Some) { throw new UnsupportedInvalidOperationException(c.error.dtor_value.ToVerbatimString(false)); } - return s; + w.Write(s.ToVerbatimString(false)); } public override ISequence EmitCallToMain(string fullName) { diff --git a/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs b/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs index 51824995fd8..4da78606df1 100644 --- a/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs +++ b/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs @@ -513,47 +513,47 @@ public DCOMP._IEnvironment RemoveAssigned(Dafny.ISequence name) { } } - public interface _IObjectType { - bool is_RawPointers { get; } + public interface _IPointerType { + bool is_Raw { get; } bool is_RcMut { get; } - _IObjectType DowncastClone(); + _IPointerType DowncastClone(); } - public abstract class ObjectType : _IObjectType { - public ObjectType() { + public abstract class PointerType : _IPointerType { + public PointerType() { } - private static readonly DCOMP._IObjectType theDefault = create_RawPointers(); - public static DCOMP._IObjectType Default() { + private static readonly DCOMP._IPointerType theDefault = create_Raw(); + public static DCOMP._IPointerType Default() { return theDefault; } - private static readonly Dafny.TypeDescriptor _TYPE = new Dafny.TypeDescriptor(DCOMP.ObjectType.Default()); - public static Dafny.TypeDescriptor _TypeDescriptor() { + private static readonly Dafny.TypeDescriptor _TYPE = new Dafny.TypeDescriptor(DCOMP.PointerType.Default()); + public static Dafny.TypeDescriptor _TypeDescriptor() { return _TYPE; } - public static _IObjectType create_RawPointers() { - return new ObjectType_RawPointers(); + public static _IPointerType create_Raw() { + return new PointerType_Raw(); } - public static _IObjectType create_RcMut() { - return new ObjectType_RcMut(); + public static _IPointerType create_RcMut() { + return new PointerType_RcMut(); } - public bool is_RawPointers { get { return this is ObjectType_RawPointers; } } - public bool is_RcMut { get { return this is ObjectType_RcMut; } } - public static System.Collections.Generic.IEnumerable<_IObjectType> AllSingletonConstructors { + public bool is_Raw { get { return this is PointerType_Raw; } } + public bool is_RcMut { get { return this is PointerType_RcMut; } } + public static System.Collections.Generic.IEnumerable<_IPointerType> AllSingletonConstructors { get { - yield return ObjectType.create_RawPointers(); - yield return ObjectType.create_RcMut(); + yield return PointerType.create_Raw(); + yield return PointerType.create_RcMut(); } } - public abstract _IObjectType DowncastClone(); + public abstract _IPointerType DowncastClone(); } - public class ObjectType_RawPointers : ObjectType { - public ObjectType_RawPointers() : base() { + public class PointerType_Raw : PointerType { + public PointerType_Raw() : base() { } - public override _IObjectType DowncastClone() { - if (this is _IObjectType dt) { return dt; } - return new ObjectType_RawPointers(); + public override _IPointerType DowncastClone() { + if (this is _IPointerType dt) { return dt; } + return new PointerType_Raw(); } public override bool Equals(object other) { - var oth = other as DCOMP.ObjectType_RawPointers; + var oth = other as DCOMP.PointerType_Raw; return oth != null; } public override int GetHashCode() { @@ -562,19 +562,19 @@ public override int GetHashCode() { return (int) hash; } public override string ToString() { - string s = "DafnyToRustCompiler.ObjectType.RawPointers"; + string s = "DafnyToRustCompiler.PointerType.Raw"; return s; } } - public class ObjectType_RcMut : ObjectType { - public ObjectType_RcMut() : base() { + public class PointerType_RcMut : PointerType { + public PointerType_RcMut() : base() { } - public override _IObjectType DowncastClone() { - if (this is _IObjectType dt) { return dt; } - return new ObjectType_RcMut(); + public override _IPointerType DowncastClone() { + if (this is _IPointerType dt) { return dt; } + return new PointerType_RcMut(); } public override bool Equals(object other) { - var oth = other as DCOMP.ObjectType_RcMut; + var oth = other as DCOMP.PointerType_RcMut; return oth != null; } public override int GetHashCode() { @@ -583,7 +583,164 @@ public override int GetHashCode() { return (int) hash; } public override string ToString() { - string s = "DafnyToRustCompiler.ObjectType.RcMut"; + string s = "DafnyToRustCompiler.PointerType.RcMut"; + return s; + } + } + + public interface _ICharType { + bool is_UTF16 { get; } + bool is_UTF32 { get; } + _ICharType DowncastClone(); + } + public abstract class CharType : _ICharType { + public CharType() { + } + private static readonly DCOMP._ICharType theDefault = create_UTF16(); + public static DCOMP._ICharType Default() { + return theDefault; + } + private static readonly Dafny.TypeDescriptor _TYPE = new Dafny.TypeDescriptor(DCOMP.CharType.Default()); + public static Dafny.TypeDescriptor _TypeDescriptor() { + return _TYPE; + } + public static _ICharType create_UTF16() { + return new CharType_UTF16(); + } + public static _ICharType create_UTF32() { + return new CharType_UTF32(); + } + public bool is_UTF16 { get { return this is CharType_UTF16; } } + public bool is_UTF32 { get { return this is CharType_UTF32; } } + public static System.Collections.Generic.IEnumerable<_ICharType> AllSingletonConstructors { + get { + yield return CharType.create_UTF16(); + yield return CharType.create_UTF32(); + } + } + public abstract _ICharType DowncastClone(); + } + public class CharType_UTF16 : CharType { + public CharType_UTF16() : base() { + } + public override _ICharType DowncastClone() { + if (this is _ICharType dt) { return dt; } + return new CharType_UTF16(); + } + public override bool Equals(object other) { + var oth = other as DCOMP.CharType_UTF16; + return oth != null; + } + public override int GetHashCode() { + ulong hash = 5381; + hash = ((hash << 5) + hash) + 0; + return (int) hash; + } + public override string ToString() { + string s = "DafnyToRustCompiler.CharType.UTF16"; + return s; + } + } + public class CharType_UTF32 : CharType { + public CharType_UTF32() : base() { + } + public override _ICharType DowncastClone() { + if (this is _ICharType dt) { return dt; } + return new CharType_UTF32(); + } + public override bool Equals(object other) { + var oth = other as DCOMP.CharType_UTF32; + return oth != null; + } + public override int GetHashCode() { + ulong hash = 5381; + hash = ((hash << 5) + hash) + 1; + return (int) hash; + } + public override string ToString() { + string s = "DafnyToRustCompiler.CharType.UTF32"; + return s; + } + } + + public interface _IRootType { + bool is_RootCrate { get; } + bool is_RootPath { get; } + Dafny.ISequence dtor_moduleName { get; } + _IRootType DowncastClone(); + } + public abstract class RootType : _IRootType { + public RootType() { + } + private static readonly DCOMP._IRootType theDefault = create_RootCrate(); + public static DCOMP._IRootType Default() { + return theDefault; + } + private static readonly Dafny.TypeDescriptor _TYPE = new Dafny.TypeDescriptor(DCOMP.RootType.Default()); + public static Dafny.TypeDescriptor _TypeDescriptor() { + return _TYPE; + } + public static _IRootType create_RootCrate() { + return new RootType_RootCrate(); + } + public static _IRootType create_RootPath(Dafny.ISequence moduleName) { + return new RootType_RootPath(moduleName); + } + public bool is_RootCrate { get { return this is RootType_RootCrate; } } + public bool is_RootPath { get { return this is RootType_RootPath; } } + public Dafny.ISequence dtor_moduleName { + get { + var d = this; + return ((RootType_RootPath)d)._moduleName; + } + } + public abstract _IRootType DowncastClone(); + } + public class RootType_RootCrate : RootType { + public RootType_RootCrate() : base() { + } + public override _IRootType DowncastClone() { + if (this is _IRootType dt) { return dt; } + return new RootType_RootCrate(); + } + public override bool Equals(object other) { + var oth = other as DCOMP.RootType_RootCrate; + return oth != null; + } + public override int GetHashCode() { + ulong hash = 5381; + hash = ((hash << 5) + hash) + 0; + return (int) hash; + } + public override string ToString() { + string s = "DafnyToRustCompiler.RootType.RootCrate"; + return s; + } + } + public class RootType_RootPath : RootType { + public readonly Dafny.ISequence _moduleName; + public RootType_RootPath(Dafny.ISequence moduleName) : base() { + this._moduleName = moduleName; + } + public override _IRootType DowncastClone() { + if (this is _IRootType dt) { return dt; } + return new RootType_RootPath(_moduleName); + } + public override bool Equals(object other) { + var oth = other as DCOMP.RootType_RootPath; + return oth != null && object.Equals(this._moduleName, oth._moduleName); + } + public override int GetHashCode() { + ulong hash = 5381; + hash = ((hash << 5) + hash) + 1; + hash = ((hash << 5) + hash) + ((ulong)Dafny.Helpers.GetHashCode(this._moduleName)); + return (int) hash; + } + public override string ToString() { + string s = "DafnyToRustCompiler.RootType.RootPath"; + s += "("; + s += this._moduleName.ToVerbatimString(true); + s += ")"; return s; } } @@ -913,18 +1070,19 @@ public partial class COMP { public COMP() { this.error = Std.Wrappers.Option>.Default(); this.optimizations = Dafny.Sequence>.Empty; - this._UnicodeChars = false; - this._ObjectType = DCOMP.ObjectType.Default(); + this._charType = DCOMP.CharType.Default(); + this._pointerType = DCOMP.PointerType.Default(); + this._rootType = DCOMP.RootType.Default(); } public RAST._IType Object(RAST._IType underlying) { - if (((this).ObjectType).is_RawPointers) { + if (((this).pointerType).is_Raw) { return RAST.__default.PtrType(underlying); } else { return RAST.__default.ObjectType(underlying); } } public Dafny.ISequence UnreachablePanicIfVerified(Dafny.ISequence optText) { - if (((this).ObjectType).is_RawPointers) { + if (((this).pointerType).is_Raw) { return Dafny.Sequence.UnicodeFromString("unsafe { ::std::hint::unreachable_unchecked() }"); } else if ((optText).Equals(Dafny.Sequence.UnicodeFromString(""))) { return Dafny.Sequence.UnicodeFromString("panic!()"); @@ -934,12 +1092,13 @@ public RAST._IType Object(RAST._IType underlying) { } public Std.Wrappers._IOption> error {get; set;} public Dafny.ISequence> optimizations {get; set;} - public void __ctor(bool unicodeChars, DCOMP._IObjectType objectType) + public void __ctor(DCOMP._ICharType charType, DCOMP._IPointerType pointerType, DCOMP._IRootType rootType) { - (this)._UnicodeChars = unicodeChars; - (this)._ObjectType = objectType; + (this)._charType = charType; + (this)._pointerType = pointerType; + (this)._rootType = rootType; (this).error = Std.Wrappers.Option>.create_None(); - (this).optimizations = Dafny.Sequence>.FromElements(FactorPathsOptimization.__default.apply); + (this).optimizations = Dafny.Sequence>.FromElements(FactorPathsOptimization.__default.apply((this).thisFile)); } public static Dafny.ISequence> ContainingPathToRust(Dafny.ISequence> containingPath) { return Std.Collections.Seq.__default.Map, Dafny.ISequence>(((System.Func, Dafny.ISequence>)((_0_i) => { @@ -982,7 +1141,7 @@ public bool HasAttribute(Dafny.ISequence attributes, Dafny.ISe _7_allmodules = _out1; if ((_4_optExtern).is_SimpleExtern) { if ((mod).dtor_requiresExterns) { - _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); + _6_body = Dafny.Sequence.Concat(Dafny.Sequence.FromElements(RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), ((((this).thisFile).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")); @@ -1274,7 +1433,7 @@ public bool IsSameResolvedType(DAST._IResolvedType r1, DAST._IResolvedType r2) } RAST._IType _33_genSelfPath; RAST._IType _out13; - _out13 = DCOMP.COMP.GenPathType(path); + _out13 = (this).GenPathType(path); _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(_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))))))))); @@ -1301,7 +1460,7 @@ public bool IsSameResolvedType(DAST._IResolvedType r1, DAST._IResolvedType r2) { RAST._IType _40_pathStr; RAST._IType _out14; - _out14 = DCOMP.COMP.GenPathType(_37_traitPath); + _out14 = (this).GenPathType(_37_traitPath); _40_pathStr = _out14; Dafny.ISequence _41_typeArgs; Dafny.ISequence _out15; @@ -2054,7 +2213,7 @@ public bool DatatypeIsEq(DAST._IDatatype c) { } return s; } - public static RAST._IPath GenPath(Dafny.ISequence> p, bool escape) + public RAST._IPath GenPath(Dafny.ISequence> p, bool escape) { RAST._IPath r = RAST.Path.Default(); if ((new BigInteger((p).Count)).Sign == 0) { @@ -2066,7 +2225,7 @@ public static RAST._IPath GenPath(Dafny.ISequence> p } else if (((((p).Select(BigInteger.Zero)))).Equals(Dafny.Sequence.UnicodeFromString("_System"))) { r = RAST.__default.dafny__runtime; } else { - r = RAST.Path.create_Crate(); + r = (this).thisFile; } BigInteger _hi0 = new BigInteger((p).Count); for (BigInteger _0_i = BigInteger.Zero; _0_i < _hi0; _0_i++) { @@ -2088,17 +2247,17 @@ public static RAST._IPath GenPath(Dafny.ISequence> p } return r; } - public static RAST._IType GenPathType(Dafny.ISequence> p) + public RAST._IType GenPathType(Dafny.ISequence> p) { RAST._IType t = RAST.Type.Default(); RAST._IPath _0_p; RAST._IPath _out0; - _out0 = DCOMP.COMP.GenPath(p, true); + _out0 = (this).GenPath(p, true); _0_p = _out0; t = (_0_p).AsType(); return t; } - public static RAST._IExpr GenPathExpr(Dafny.ISequence> p, bool escape) + public RAST._IExpr GenPathExpr(Dafny.ISequence> p, bool escape) { RAST._IExpr e = RAST.Expr.Default(); if ((new BigInteger((p).Count)).Sign == 0) { @@ -2107,7 +2266,7 @@ public static RAST._IExpr GenPathExpr(Dafny.ISequence _2_typeArgs; Dafny.ISequence _out1; @@ -2556,7 +2715,7 @@ public RAST._IImplMember GenMethod(DAST._IMethod m, bool forTrait, DAST._IType e after_match0: ; if (forTrait) { RAST._IFormal _14_selfFormal; - if (((m).dtor_wasFunction) && (((this).ObjectType).is_RawPointers)) { + if (((m).dtor_wasFunction) && (((this).pointerType).is_Raw)) { _14_selfFormal = RAST.Formal.selfBorrowed; } else { _14_selfFormal = RAST.Formal.selfBorrowedMut; @@ -2568,12 +2727,12 @@ public RAST._IImplMember GenMethod(DAST._IMethod m, bool forTrait, DAST._IType e _out1 = (this).GenType(_10_instanceType, DCOMP.GenTypeContext.@default()); _15_tpe = _out1; if ((_9_selfId).Equals(Dafny.Sequence.UnicodeFromString("this"))) { - if (((this).ObjectType).is_RcMut) { + if (((this).pointerType).is_RcMut) { _15_tpe = RAST.Type.create_Borrowed(_15_tpe); } } else if ((_9_selfId).Equals(Dafny.Sequence.UnicodeFromString("self"))) { if ((_15_tpe).IsObjectOrPointer()) { - if (((m).dtor_wasFunction) && (((this).ObjectType).is_RawPointers)) { + if (((m).dtor_wasFunction) && (((this).pointerType).is_Raw)) { _15_tpe = RAST.__default.SelfBorrowed; } else { _15_tpe = RAST.__default.SelfBorrowedMut; @@ -3404,7 +3563,7 @@ public void GenStmt(DAST._IStatement stmt, DCOMP._ISelfInfo selfIdent, DCOMP._IE DAST._IResolvedTypeBase _100_base = value0.dtor_kind; RAST._IExpr _101_fullPath; RAST._IExpr _out56; - _out56 = DCOMP.COMP.GenPathExpr(_98_path, true); + _out56 = (this).GenPathExpr(_98_path, true); _101_fullPath = _out56; Dafny.ISequence _102_onTypeExprs; Dafny.ISequence _out57; @@ -3913,7 +4072,7 @@ public void GenExprLiteral(DAST._IExpression e, DCOMP._ISelfInfo selfIdent, DCOM Dafny.Rune _13_c = _h175.dtor_CharLiteral_a0; { r = RAST.Expr.create_LiteralInt(Std.Strings.__default.OfNat(new BigInteger((_13_c).Value))); - if (!((this).UnicodeChars)) { + if (!(((this).charType).is_UTF32)) { r = RAST.Expr.create_TypeAscription(r, RAST.Type.create_U16()); } else { r = (((((((RAST.__default.@global).MSel(Dafny.Sequence.UnicodeFromString("std"))).MSel(Dafny.Sequence.UnicodeFromString("primitive"))).MSel(Dafny.Sequence.UnicodeFromString("char"))).FSel(Dafny.Sequence.UnicodeFromString("from_u32"))).Apply1(r)).Sel(Dafny.Sequence.UnicodeFromString("unwrap"))).Apply(Dafny.Sequence.FromElements()); @@ -3939,7 +4098,7 @@ public void GenExprLiteral(DAST._IExpression e, DCOMP._ISelfInfo selfIdent, DCOM RAST._IType _out14; _out14 = (this).GenType(_14_tpe, DCOMP.GenTypeContext.@default()); _15_tpeGen = _out14; - if (((this).ObjectType).is_RawPointers) { + if (((this).pointerType).is_Raw) { r = ((RAST.__default.std).MSel(Dafny.Sequence.UnicodeFromString("ptr"))).FSel(Dafny.Sequence.UnicodeFromString("null_mut")); } else { r = RAST.Expr.create_TypeAscription((((RAST.__default.dafny__runtime).MSel(Dafny.Sequence.UnicodeFromString("Object"))).AsExpr()).Apply1(RAST.Expr.create_RawExpr(Dafny.Sequence.UnicodeFromString("None"))), _15_tpeGen); @@ -4292,7 +4451,7 @@ public void GenExprBinary(DAST._IExpression e, DCOMP._ISelfInfo selfIdent, DCOMP bool _15_referential = _source4.dtor_referential; { if (_15_referential) { - if (((this).ObjectType).is_RawPointers) { + if (((this).pointerType).is_Raw) { (this).error = Std.Wrappers.Option>.create_Some(Dafny.Sequence.UnicodeFromString("Cannot compare raw pointers yet - need to wrap them with a structure to ensure they are compared properly")); r = RAST.Expr.create_RawExpr((this.error).dtor_value); } else { @@ -5042,7 +5201,7 @@ public void GenExprConvert(DAST._IExpression e, DCOMP._ISelfInfo selfIdent, DCOM _29_recursiveGen = _out34; _30___v144 = _out35; _31_recIdents = _out36; - r = RAST.Expr.create_RawExpr(Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.UnicodeFromString("::dafny_runtime::"), (this).DafnyChar), Dafny.Sequence.UnicodeFromString("(")), (((this).UnicodeChars) ? (Dafny.Sequence.UnicodeFromString("char::from_u32(.UnicodeFromString(".UnicodeFromString(" as ::dafny_runtime::NumCast>::from(")), (_29_recursiveGen)._ToString(DCOMP.__default.IND)), Dafny.Sequence.UnicodeFromString(").unwrap())")), (((this).UnicodeChars) ? (Dafny.Sequence.UnicodeFromString(".unwrap())")) : (Dafny.Sequence.UnicodeFromString(""))))); + r = RAST.Expr.create_RawExpr(Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.UnicodeFromString("::dafny_runtime::"), (this).DafnyChar), Dafny.Sequence.UnicodeFromString("(")), ((((this).charType).is_UTF32) ? (Dafny.Sequence.UnicodeFromString("char::from_u32(.UnicodeFromString(".UnicodeFromString(" as ::dafny_runtime::NumCast>::from(")), (_29_recursiveGen)._ToString(DCOMP.__default.IND)), Dafny.Sequence.UnicodeFromString(").unwrap())")), ((((this).charType).is_UTF32) ? (Dafny.Sequence.UnicodeFromString(".unwrap())")) : (Dafny.Sequence.UnicodeFromString(""))))); RAST._IExpr _out37; DCOMP._IOwnership _out38; (this).FromOwned(r, expectedOwnership, out _out37, out _out38); @@ -5383,7 +5542,7 @@ public void GenExpr(DAST._IExpression e, DCOMP._ISelfInfo selfIdent, DCOMP._IEnv Dafny.ISequence> _1_path = _source0.dtor_ExternCompanion_a0; { RAST._IExpr _out6; - _out6 = DCOMP.COMP.GenPathExpr(_1_path, false); + _out6 = (this).GenPathExpr(_1_path, false); r = _out6; if (object.Equals(expectedOwnership, DCOMP.Ownership.create_OwnershipBorrowed())) { resultingOwnership = DCOMP.Ownership.create_OwnershipBorrowed(); @@ -5408,7 +5567,7 @@ public void GenExpr(DAST._IExpression e, DCOMP._ISelfInfo selfIdent, DCOMP._IEnv Dafny.ISequence _3_typeArgs = _source0.dtor_typeArgs; { RAST._IExpr _out9; - _out9 = DCOMP.COMP.GenPathExpr(_2_path, true); + _out9 = (this).GenPathExpr(_2_path, true); r = _out9; if ((new BigInteger((_3_typeArgs).Count)).Sign == 1) { Dafny.ISequence _4_typeExprs; @@ -5508,7 +5667,7 @@ public void GenExpr(DAST._IExpression e, DCOMP._ISelfInfo selfIdent, DCOMP._IEnv Dafny.ISequence _17_args = _source0.dtor_args; { RAST._IExpr _out21; - _out21 = DCOMP.COMP.GenPathExpr(_15_path, true); + _out21 = (this).GenPathExpr(_15_path, true); r = _out21; if ((new BigInteger((_16_typeArgs).Count)).Sign == 1) { Dafny.ISequence _18_typeExprs; @@ -5687,7 +5846,7 @@ public void GenExpr(DAST._IExpression e, DCOMP._ISelfInfo selfIdent, DCOMP._IEnv Dafny.ISequence<_System._ITuple2, DAST._IExpression>> _52_values = _source0.dtor_contents; { RAST._IExpr _out45; - _out45 = DCOMP.COMP.GenPathExpr((_48_datatypeType).dtor_path, true); + _out45 = (this).GenPathExpr((_48_datatypeType).dtor_path, true); r = _out45; Dafny.ISequence _53_genTypeArgs; _53_genTypeArgs = Dafny.Sequence.FromElements(); @@ -6623,12 +6782,10 @@ public void GenExpr(DAST._IExpression e, DCOMP._ISelfInfo selfIdent, DCOMP._IEnv { } after_match2: ; - if (((this).ObjectType).is_RcMut) { - r = (r).Clone(); - } - if (((this).ObjectType).is_RawPointers) { + if (((this).pointerType).is_Raw) { r = ((this).read__macro).Apply1(r); } else { + r = (r).Clone(); r = ((this).modify__macro).Apply1(r); } } @@ -6729,7 +6886,7 @@ public void GenExpr(DAST._IExpression e, DCOMP._ISelfInfo selfIdent, DCOMP._IEnv { DCOMP._IOwnership _249_onExpectedOwnership; if (_246_isArray) { - if (((this).ObjectType).is_RawPointers) { + if (((this).pointerType).is_Raw) { _249_onExpectedOwnership = DCOMP.Ownership.create_OwnershipOwned(); } else { _249_onExpectedOwnership = DCOMP.Ownership.create_OwnershipBorrowed(); @@ -6816,7 +6973,7 @@ public void GenExpr(DAST._IExpression e, DCOMP._ISelfInfo selfIdent, DCOMP._IEnv _253_methodName = Dafny.Sequence.Concat(Dafny.Sequence.UnicodeFromString("_"), _253_methodName); } Dafny.ISequence _263_object__suffix; - if (((this).ObjectType).is_RawPointers) { + if (((this).pointerType).is_Raw) { _263_object__suffix = Dafny.Sequence.UnicodeFromString(""); } else { _263_object__suffix = Dafny.Sequence.UnicodeFromString("_object"); @@ -6912,7 +7069,7 @@ public void GenExpr(DAST._IExpression e, DCOMP._ISelfInfo selfIdent, DCOMP._IEnv DAST._IResolvedTypeBase _282_base = value0.dtor_kind; RAST._IExpr _283_fullPath; RAST._IExpr _out228; - _out228 = DCOMP.COMP.GenPathExpr(_280_path, true); + _out228 = (this).GenPathExpr(_280_path, true); _283_fullPath = _out228; Dafny.ISequence _284_onTypeExprs; Dafny.ISequence _out229; @@ -6929,7 +7086,7 @@ public void GenExpr(DAST._IExpression e, DCOMP._ISelfInfo selfIdent, DCOMP._IEnv _285_onExpr = _out230; _286_recOwnership = _out231; _287_recIdents = _out232; - if (((this).ObjectType).is_RawPointers) { + if (((this).pointerType).is_Raw) { _285_onExpr = ((this).read__macro).Apply1(_285_onExpr); } else { _285_onExpr = ((this).modify__macro).Apply1(_285_onExpr); @@ -6937,7 +7094,7 @@ public void GenExpr(DAST._IExpression e, DCOMP._ISelfInfo selfIdent, DCOMP._IEnv readIdents = Dafny.Set>.Union(readIdents, _287_recIdents); } else { DCOMP._IOwnership _288_expectedOnOwnership; - if (((this).ObjectType).is_RawPointers) { + if (((this).pointerType).is_Raw) { _288_expectedOnOwnership = DCOMP.Ownership.create_OwnershipBorrowed(); } else { _288_expectedOnOwnership = DCOMP.Ownership.create_OwnershipBorrowedMut(); @@ -7004,7 +7161,7 @@ public void GenExpr(DAST._IExpression e, DCOMP._ISelfInfo selfIdent, DCOMP._IEnv _out241 = (this).GenType(_293_tpe, DCOMP.GenTypeContext.@default()); _294_typ = _out241; if ((_294_typ).IsObjectOrPointer()) { - if (((this).ObjectType).is_RawPointers) { + if (((this).pointerType).is_Raw) { _289_onExpr = ((this).read__macro).Apply1(_289_onExpr); } else { _289_onExpr = ((this).modify__macro).Apply1(_289_onExpr); @@ -7307,7 +7464,7 @@ public void GenExpr(DAST._IExpression e, DCOMP._ISelfInfo selfIdent, DCOMP._IEnv _363_recIdents = _out283; RAST._IType _364_dTypePath; RAST._IType _out284; - _out284 = DCOMP.COMP.GenPathType(Dafny.Sequence>.Concat(_359_dType, Dafny.Sequence>.FromElements(_360_variant))); + _out284 = (this).GenPathType(Dafny.Sequence>.Concat(_359_dType, Dafny.Sequence>.FromElements(_360_variant))); _364_dTypePath = _out284; r = (RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("matches!"))).Apply(Dafny.Sequence.FromElements(((_361_exprGen).Sel(Dafny.Sequence.UnicodeFromString("as_ref"))).Apply(Dafny.Sequence.FromElements()), RAST.Expr.create_RawExpr(Dafny.Sequence.Concat((_364_dTypePath)._ToString(DCOMP.__default.IND), Dafny.Sequence.UnicodeFromString("{ .. }"))))); RAST._IExpr _out285; @@ -7752,37 +7909,48 @@ public void GenExpr(DAST._IExpression e, DCOMP._ISelfInfo selfIdent, DCOMP._IEnv s = Dafny.Sequence.Concat(s, Dafny.Sequence.UnicodeFromString("();\n}")); return s; } - public bool _UnicodeChars {get; set;} - public bool UnicodeChars { get { - return this._UnicodeChars; + public DCOMP._ICharType _charType {get; set;} + public DCOMP._ICharType charType { get { + return this._charType; + } } + public DCOMP._IPointerType _pointerType {get; set;} + public DCOMP._IPointerType pointerType { get { + return this._pointerType; + } } + public DCOMP._IRootType _rootType {get; set;} + public DCOMP._IRootType rootType { get { + return this._rootType; + } } + public RAST._IPath thisFile { get { + if (((this).rootType).is_RootCrate) { + return RAST.__default.crate; + } else { + return (RAST.__default.crate).MSel(((this).rootType).dtor_moduleName); + } } } public Dafny.ISequence DafnyChar { get { - if ((this).UnicodeChars) { + if (((this).charType).is_UTF32) { return Dafny.Sequence.UnicodeFromString("DafnyChar"); } else { return Dafny.Sequence.UnicodeFromString("DafnyCharUTF16"); } } } public RAST._IType DafnyCharUnderlying { get { - if ((this).UnicodeChars) { + if (((this).charType).is_UTF32) { return RAST.__default.RawType(Dafny.Sequence.UnicodeFromString("char")); } else { return RAST.__default.RawType(Dafny.Sequence.UnicodeFromString("u16")); } } } public Dafny.ISequence string__of { get { - if ((this).UnicodeChars) { + if (((this).charType).is_UTF32) { return Dafny.Sequence.UnicodeFromString("string_of"); } else { return Dafny.Sequence.UnicodeFromString("string_utf16_of"); } } } - public DCOMP._IObjectType _ObjectType {get; set;} - public DCOMP._IObjectType ObjectType { get { - return this._ObjectType; - } } public Dafny.ISequence allocate { get { - if (((this).ObjectType).is_RawPointers) { + if (((this).pointerType).is_Raw) { return Dafny.Sequence.UnicodeFromString("allocate"); } else { return Dafny.Sequence.UnicodeFromString("allocate_object"); @@ -7792,48 +7960,48 @@ public Dafny.ISequence allocate__fn { get { return Dafny.Sequence.Concat(Dafny.Sequence.UnicodeFromString("_"), (this).allocate); } } public Dafny.ISequence update__field__uninit__macro { get { - if (((this).ObjectType).is_RawPointers) { + if (((this).pointerType).is_Raw) { return Dafny.Sequence.UnicodeFromString("update_field_uninit!"); } else { return Dafny.Sequence.UnicodeFromString("update_field_uninit_object!"); } } } public RAST._IExpr thisInConstructor { get { - if (((this).ObjectType).is_RawPointers) { + if (((this).pointerType).is_Raw) { return RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("this")); } else { return (RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("this"))).Clone(); } } } public Dafny.ISequence array__construct { get { - if (((this).ObjectType).is_RawPointers) { + if (((this).pointerType).is_Raw) { return Dafny.Sequence.UnicodeFromString("construct"); } else { return Dafny.Sequence.UnicodeFromString("construct_object"); } } } public RAST._IExpr modify__macro { get { - return ((RAST.__default.dafny__runtime).MSel(((((this).ObjectType).is_RawPointers) ? (Dafny.Sequence.UnicodeFromString("modify!")) : (Dafny.Sequence.UnicodeFromString("md!"))))).AsExpr(); + return ((RAST.__default.dafny__runtime).MSel(((((this).pointerType).is_Raw) ? (Dafny.Sequence.UnicodeFromString("modify!")) : (Dafny.Sequence.UnicodeFromString("md!"))))).AsExpr(); } } public RAST._IExpr read__macro { get { - return ((RAST.__default.dafny__runtime).MSel(((((this).ObjectType).is_RawPointers) ? (Dafny.Sequence.UnicodeFromString("read!")) : (Dafny.Sequence.UnicodeFromString("rd!"))))).AsExpr(); + return ((RAST.__default.dafny__runtime).MSel(((((this).pointerType).is_Raw) ? (Dafny.Sequence.UnicodeFromString("read!")) : (Dafny.Sequence.UnicodeFromString("rd!"))))).AsExpr(); } } public Dafny.ISequence placebos__usize { get { - if (((this).ObjectType).is_RawPointers) { + if (((this).pointerType).is_Raw) { return Dafny.Sequence.UnicodeFromString("placebos_usize"); } else { return Dafny.Sequence.UnicodeFromString("placebos_usize_object"); } } } public Dafny.ISequence update__field__if__uninit__macro { get { - if (((this).ObjectType).is_RawPointers) { + if (((this).pointerType).is_Raw) { return Dafny.Sequence.UnicodeFromString("update_field_if_uninit!"); } else { return Dafny.Sequence.UnicodeFromString("update_field_if_uninit_object!"); } } } public Dafny.ISequence Upcast { get { - if (((this).ObjectType).is_RawPointers) { + if (((this).pointerType).is_Raw) { return Dafny.Sequence.UnicodeFromString("Upcast"); } else { return Dafny.Sequence.UnicodeFromString("UpcastObject"); @@ -7843,14 +8011,14 @@ public Dafny.ISequence UpcastFnMacro { get { return Dafny.Sequence.Concat((this).Upcast, Dafny.Sequence.UnicodeFromString("Fn!")); } } public Dafny.ISequence upcast { get { - if (((this).ObjectType).is_RawPointers) { + if (((this).pointerType).is_Raw) { return Dafny.Sequence.UnicodeFromString("upcast"); } else { return Dafny.Sequence.UnicodeFromString("upcast_object"); } } } public Dafny.ISequence downcast { get { - if (((this).ObjectType).is_RawPointers) { + if (((this).pointerType).is_Raw) { return Dafny.Sequence.UnicodeFromString("cast!"); } else { return Dafny.Sequence.UnicodeFromString("cast_object!"); diff --git a/Source/DafnyCore/GeneratedFromDafny/FactorPathsOptimization.cs b/Source/DafnyCore/GeneratedFromDafny/FactorPathsOptimization.cs index a3e803ffb88..f84ad3e437e 100644 --- a/Source/DafnyCore/GeneratedFromDafny/FactorPathsOptimization.cs +++ b/Source/DafnyCore/GeneratedFromDafny/FactorPathsOptimization.cs @@ -15,8 +15,10 @@ namespace FactorPathsOptimization { public partial class __default { - public static RAST._IMod apply(RAST._IMod mod) { - return FactorPathsOptimization.__default.applyPrefix(mod, (RAST.__default.crate).MSel((mod).dtor_name)); + public static Func apply(RAST._IPath thisFile) { + return Dafny.Helpers.Id>>((_0_thisFile) => ((System.Func)((_1_mod) => { + return FactorPathsOptimization.__default.applyPrefix(_1_mod, (_0_thisFile).MSel((_1_mod).dtor_name)); + })))(thisFile); } public static RAST._IMod applyPrefix(RAST._IMod mod, RAST._IPath SelfPath) { diff --git a/Source/DafnyCore/Makefile b/Source/DafnyCore/Makefile index 32190f29bb0..60c0ad6123e 100644 --- a/Source/DafnyCore/Makefile +++ b/Source/DafnyCore/Makefile @@ -17,8 +17,8 @@ build-regenerated-from-dafny: ./DafnyGeneratedFromDafny.sh $(REGENERATED_FROM_DAFNY) test: build-regenerated-from-dafny - (diff $(GENERATED_FROM_DAFNY) $(REGENERATED_FROM_DAFNY) || (echo 'Consider running ./DafnyGeneratedFromDafny.sh'; exit 1; )) - (diff ../DafnyCore.Test/$(GENERATED_FROM_DAFNY) ../DafnyCore.Test/$(REGENERATED_FROM_DAFNY) || (echo 'Consider running ./DafnyGeneratedFromDafny.sh'; exit 1; )) + (diff $(GENERATED_FROM_DAFNY) $(REGENERATED_FROM_DAFNY) || (echo 'Consider running `make dfy-to-cs`'; exit 1; )) + (diff ../DafnyCore.Test/$(GENERATED_FROM_DAFNY) ../DafnyCore.Test/$(REGENERATED_FROM_DAFNY) || (echo 'Consider running `make dfy-to-cs`'; exit 1; )) rm -rf $(REGENERATED_FROM_DAFNY) rm -rf ../DafnyCore.Test/$(REGENERATED_FROM_DAFNY) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/translate-additional/more_dafny.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/translate-additional/more_dafny.dfy new file mode 100644 index 00000000000..e4facc514b9 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/translate-additional/more_dafny.dfy @@ -0,0 +1,20 @@ +// RUN: %baredafny translate rs --rust-module-name additional_module "%s" +// RUN: %exits-with -any %rm -f "%S/project_depending_on_dafny/src/additional_module.rs" +// RUN: %mv "%S/more_dafny-rust/src/more_dafny.rs" "%S/project_depending_on_dafny/src/additional_module.rs" +// RUN: "%S/project_depending_on_dafny/cargo" run > "%t" +// RUN: %diff "%s.expect" "%t" + +module SubModule { + function reverse(input: bv16): bv16 { + ((input & 0xFF) << 8) | ((input & 0xFF00) >> 8) + } +} + +function reverse(input: bv16): (result: bv16) { + SubModule.reverse(input) +} + +lemma reverseDoubleIsIdentity(input: bv16) + ensures reverse(reverse(input)) == input +{ +} \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/translate-additional/more_dafny.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/translate-additional/more_dafny.dfy.expect new file mode 100644 index 00000000000..3617feec37f --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/translate-additional/more_dafny.dfy.expect @@ -0,0 +1,2 @@ +Intermediate result is 2560 +Result should be 10, got 10 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/translate-additional/project_depending_on_dafny/.gitignore b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/translate-additional/project_depending_on_dafny/.gitignore new file mode 100644 index 00000000000..bc950be1152 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/translate-additional/project_depending_on_dafny/.gitignore @@ -0,0 +1,2 @@ +src/additional_module.rs +target/ \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/translate-additional/project_depending_on_dafny/Cargo.lock b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/translate-additional/project_depending_on_dafny/Cargo.lock new file mode 100644 index 00000000000..af315037a76 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/translate-additional/project_depending_on_dafny/Cargo.lock @@ -0,0 +1,7 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 3 + +[[package]] +name = "ProjectDependingOnDafny" +version = "0.1.0" diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/translate-additional/project_depending_on_dafny/Cargo.toml b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/translate-additional/project_depending_on_dafny/Cargo.toml new file mode 100644 index 00000000000..f7079b63c99 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/translate-additional/project_depending_on_dafny/Cargo.toml @@ -0,0 +1,9 @@ +[package] +name = "ProjectDependingOnDafny" +version = "0.1.0" +edition = "2021" + +[[bin]] +name = "projectdependingondafny" +path = "src/project_depending_on_dafny.rs" + diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/translate-additional/project_depending_on_dafny/src/project_depending_on_dafny.rs b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/translate-additional/project_depending_on_dafny/src/project_depending_on_dafny.rs new file mode 100644 index 00000000000..3dc44c6beae --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/translate-additional/project_depending_on_dafny/src/project_depending_on_dafny.rs @@ -0,0 +1,8 @@ +pub mod additional_module; + +fn main() { + let x = additional_module::_module::_default::reverse(10); + println!("Intermediate result is {:?}", x); + let y = additional_module::_module::_default::reverse(x); + println!("Result should be 10, got {:?}", y); +} \ No newline at end of file