Skip to content

Feat: Add --rust-module-name to specify a module name #5747

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 18 commits into from
Sep 16, 2024
Merged

Feat: Add --rust-module-name to specify a module name #5747

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
18 commits
Select commit Hold shift + click to select a range
0c724cb
WIP to amend: --root option
MikaelMayer Aug 22, 2024
e5981b8
WIP to make paths relative to the file if not root
MikaelMayer Aug 22, 2024
5ad4484
WIP to have better names
MikaelMayer Sep 3, 2024
3feba0e
Update on the creation of the compiler
MikaelMayer Sep 3, 2024
e21719d
Created the specific option for specifying the module name
MikaelMayer Sep 4, 2024
782019d
Regenerated files
MikaelMayer Sep 4, 2024
534b237
Update Source/DafnyCore/Backends/Rust/RustCodeGenerator.cs
MikaelMayer Sep 5, 2024
42557bc
Merge branch 'master' into fix-5641-rust-module-name
MikaelMayer Sep 5, 2024
5a6d920
Merge branch 'master' into fix-5641-rust-module-name
MikaelMayer Sep 6, 2024
661e945
Merge branch 'master' into fix-5641-rust-module-name
MikaelMayer Sep 6, 2024
ee85678
Merge branch 'master' into fix-5641-rust-module-name
MikaelMayer Sep 10, 2024
e9a76ba
Merge branch 'master' into fix-5641-rust-module-name
MikaelMayer Sep 12, 2024
ce3cd8c
Fixed an issue related to factorization
MikaelMayer Sep 12, 2024
c1e8e68
Regenerated files
MikaelMayer Sep 12, 2024
426f73a
Update Source/DafnyCore/Backends/Rust/RustBackend.cs
MikaelMayer Sep 13, 2024
f330e1f
Review comments: UTF32, Real use of --rust-module-name
MikaelMayer Sep 13, 2024
0355e5e
Merge branch 'master' into fix-5641-rust-module-name
MikaelMayer Sep 13, 2024
5999808
Merge branch 'master' into fix-5641-rust-module-name
robin-aws Sep 16, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions Source/DafnyCore.Test/GeneratedFromDafny/FactorPathsOptimizationTest.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,8 +40,8 @@ public static void TestApply()
_3_std__any__Any = (((RAST.__default.@global).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("std"))).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("any"))).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Any"));
RAST._IType _4_Any;
_4_Any = RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Any"));
FactorPathsOptimizationTest.__default.ShouldBeEqual(FactorPathsOptimization.__default.apply(RAST.Mod.create_Mod(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"), Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.FromElements(), Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_StructDecl(RAST.Struct.create(Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.FromElements(), Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"), Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_0_T__Decl), RAST.Fields.create_NamedFields(Dafny.Sequence<RAST._IField>.FromElements(RAST.Field.create(RAST.Visibility.create_PUB(), RAST.Formal.create(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("a"), (_3_std__any__Any).AsType())))))), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_Impl(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_0_T__Decl), (RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"))).Apply(Dafny.Sequence<RAST._IType>.FromElements(_2_T)), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""), Dafny.Sequence<RAST._IImplMember>.FromElements())), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_0_T__Decl), (_3_std__any__Any).AsType(), ((((RAST.__default.crate).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"))).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"))).AsType()).Apply(Dafny.Sequence<RAST._IType>.FromElements(_2_T)), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""), Dafny.Sequence<RAST._IImplMember>.FromElements()))))), RAST.Mod.create_Mod(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"), Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.FromElements(), Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), (RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("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<Dafny.ISequence<Dafny.Rune>>.FromElements(), Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"), Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_1_T__Decl__simp), RAST.Fields.create_NamedFields(Dafny.Sequence<RAST._IField>.FromElements(RAST.Field.create(RAST.Visibility.create_PUB(), RAST.Formal.create(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("a"), _4_Any)))))), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_Impl(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_1_T__Decl__simp), (RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"))).Apply(Dafny.Sequence<RAST._IType>.FromElements(_2_T)), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""), Dafny.Sequence<RAST._IImplMember>.FromElements())), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_1_T__Decl__simp), _4_Any, (RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"))).Apply(Dafny.Sequence<RAST._IType>.FromElements(_2_T)), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""), Dafny.Sequence<RAST._IImplMember>.FromElements())))));
FactorPathsOptimizationTest.__default.ShouldBeEqual(FactorPathsOptimization.__default.apply(RAST.Mod.create_Mod(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"), Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.FromElements(), Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_0_T__Decl), (((RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("UpcastObject"))).AsType()).Apply(Dafny.Sequence<RAST._IType>.FromElements(RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("x")))), (RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"))).Apply(Dafny.Sequence<RAST._IType>.FromElements(_2_T)), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""), Dafny.Sequence<RAST._IImplMember>.FromElements()))))), RAST.Mod.create_Mod(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"), Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.FromElements(), Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), (RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("DafnyType")))), RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), (RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("UpcastObject")))), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_1_T__Decl__simp), (RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("UpcastObject"))).Apply(Dafny.Sequence<RAST._IType>.FromElements(RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("x")))), (RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"))).Apply(Dafny.Sequence<RAST._IType>.FromElements(_2_T)), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""), Dafny.Sequence<RAST._IImplMember>.FromElements())))));
FactorPathsOptimizationTest.__default.ShouldBeEqual(Dafny.Helpers.Id<Func<RAST._IMod, RAST._IMod>>(FactorPathsOptimization.__default.apply(RAST.__default.crate))(RAST.Mod.create_Mod(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"), Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.FromElements(), Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_StructDecl(RAST.Struct.create(Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.FromElements(), Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"), Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_0_T__Decl), RAST.Fields.create_NamedFields(Dafny.Sequence<RAST._IField>.FromElements(RAST.Field.create(RAST.Visibility.create_PUB(), RAST.Formal.create(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("a"), (_3_std__any__Any).AsType())))))), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_Impl(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_0_T__Decl), (RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"))).Apply(Dafny.Sequence<RAST._IType>.FromElements(_2_T)), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""), Dafny.Sequence<RAST._IImplMember>.FromElements())), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_0_T__Decl), (_3_std__any__Any).AsType(), ((((RAST.__default.crate).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"))).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"))).AsType()).Apply(Dafny.Sequence<RAST._IType>.FromElements(_2_T)), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""), Dafny.Sequence<RAST._IImplMember>.FromElements()))))), RAST.Mod.create_Mod(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"), Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.FromElements(), Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), (RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("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<Dafny.ISequence<Dafny.Rune>>.FromElements(), Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"), Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_1_T__Decl__simp), RAST.Fields.create_NamedFields(Dafny.Sequence<RAST._IField>.FromElements(RAST.Field.create(RAST.Visibility.create_PUB(), RAST.Formal.create(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("a"), _4_Any)))))), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_Impl(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_1_T__Decl__simp), (RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"))).Apply(Dafny.Sequence<RAST._IType>.FromElements(_2_T)), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""), Dafny.Sequence<RAST._IImplMember>.FromElements())), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_1_T__Decl__simp), _4_Any, (RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"))).Apply(Dafny.Sequence<RAST._IType>.FromElements(_2_T)), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""), Dafny.Sequence<RAST._IImplMember>.FromElements())))));
FactorPathsOptimizationTest.__default.ShouldBeEqual(Dafny.Helpers.Id<Func<RAST._IMod, RAST._IMod>>(FactorPathsOptimization.__default.apply(RAST.__default.crate))(RAST.Mod.create_Mod(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"), Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.FromElements(), Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_0_T__Decl), (((RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("UpcastObject"))).AsType()).Apply(Dafny.Sequence<RAST._IType>.FromElements(RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("x")))), (RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"))).Apply(Dafny.Sequence<RAST._IType>.FromElements(_2_T)), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""), Dafny.Sequence<RAST._IImplMember>.FromElements()))))), RAST.Mod.create_Mod(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"), Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.FromElements(), Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), (RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("DafnyType")))), RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), (RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("UpcastObject")))), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_1_T__Decl__simp), (RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("UpcastObject"))).Apply(Dafny.Sequence<RAST._IType>.FromElements(RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("x")))), (RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"))).Apply(Dafny.Sequence<RAST._IType>.FromElements(_2_T)), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""), Dafny.Sequence<RAST._IImplMember>.FromElements())))));
}
}
} // end of namespace FactorPathsOptimizationTest
5 changes: 2 additions & 3 deletions Source/DafnyCore/Backends/DafnyExecutableBackend.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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<DAST.Module>)Sequence<DAST.Module>.FromArray(dast.ToArray()),
(Sequence<ISequence<Rune>>)Sequence<ISequence<Rune>>.FromArray(
ImportFiles(dafnyProgramName).Select(fileName =>
Sequence<Rune>.UnicodeFromString(Path.GetFileName(fileName))).ToArray()
));
output.Write(o.ToVerbatimString(false));
), output);
}

public override void EmitCallToMain(Method mainMethod, string baseName, ConcreteSyntaxTree output) {
Expand Down
2 changes: 1 addition & 1 deletion Source/DafnyCore/Backends/DafnyWrittenCodeGenerator.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ namespace Microsoft.Dafny.Compilers {

public abstract class DafnyWrittenCodeGenerator {

public abstract ISequence<Rune> Compile(Sequence<DAST.Module> program, Sequence<ISequence<Rune>> otherFiles);
public abstract void Compile(Sequence<DAST.Module> program, Sequence<ISequence<Rune>> otherFiles, ConcreteSyntaxTree w);

public abstract ISequence<Rune> EmitCallToMain(string fullName);

Expand Down
4 changes: 2 additions & 2 deletions ...ackends/ResolvedDesugaredExecutableDafny/ResolvedDesugaredExecutableDafnyCodeGenerator.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,8 +8,8 @@ namespace Microsoft.Dafny.Compilers;

class ResolvedDesugaredExecutableDafnyCodeGenerator : DafnyWrittenCodeGenerator {

public override ISequence<Rune> Compile(Sequence<DAST.Module> program, Sequence<ISequence<Rune>> otherFiles) {
return COMP.Compile(program);
public override void Compile(Sequence<DAST.Module> program, Sequence<ISequence<Rune>> otherFiles, ConcreteSyntaxTree w) {
w.Write(COMP.Compile(program).ToVerbatimString(false));
}

public override ISequence<Rune> EmitCallToMain(string fullName) {
Expand Down
8 changes: 4 additions & 4 deletions Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-path-simplification.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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],
Expand All @@ -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(
Expand Down Expand Up @@ -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 {
Expand Down
Loading