Fix 5724 compile suffix main arguments #5910
Conversation
| @@ -468,7 +468,7 @@ protected override void GetNativeInfo(NativeType.Selection sel, out string name, | |||
| private Sequence<DAST.Formal> GenFormals(List<Formal> formals) { | |||
| List<DAST.Formal> paramsList = new(); | |||
| foreach (var param in formals) { | |||
| if (param is not ImplicitFormal && !param.IsGhost) { | |||
| if (!param.IsGhost) { | |||
There was a problem hiding this comment.
Not supporting implicit formals was there originally because the Rust backend did not support method arguments, which were automatically added in main methods generated for tests. There was no reason to skip ImplicitFormal and keeping that would have hurt development for e.g. implicit ordinal parameters
| @@ -216,7 +216,7 @@ pub mod dafny_runtime_conversions { | |||
| } | |||
| } | |||
|
|
|||
| // --unicode-chars:false | |||
| // --unicode-char:false | |||
| pub mod unicode_chars_false { | |||
There was a problem hiding this comment.
I wish I could change the module name here but it's a breaking change, so I'm not sure it's be a good idea at this point.
| @@ -1781,7 +1781,7 @@ protected override string TypeName_UDT(string fullCompileName, List<TypeParamete | |||
| return s; | |||
| } | |||
|
|
|||
| protected override string TypeName_Companion(Type type, ConcreteSyntaxTree wr, IToken tok, MemberDecl/*?*/ member) { | |||
| internal override string TypeName_Companion(Type type, ConcreteSyntaxTree wr, IToken tok, MemberDecl/*?*/ member) { | |||
There was a problem hiding this comment.
Changing the visibility here because I needed to access this method to emit the proper path here.
https://github.com/dafny-lang/dafny/pull/5910/files#diff-88e28efa63a86a01c970f8732d7414bb1f8c5bcb77cbba8e4ae7e7b7bad18711R69
It's very Dafny-compiler specific but I could not change the visibility to anything less than internal to make it work.
I could have created another method that calls the protected one, but at this point I think it would have created redundancy for nothing.
| s := s + escapeName(fullName[i]); | ||
| i := i + 1; | ||
| method EmitCallToMain(companion: Expression, mainMethodName: string, hasArgs: bool) returns (s: string) { | ||
| s := "\nfn main() {"; |
There was a problem hiding this comment.
Having test tree vs. formal tree: At this point, the emitted main method is emitted directly into the resulting text file, so any automated refactoring here is useless, as there is zero knowledge of everything that was imported before. We could change the entire architecture but that's too big of a change for this PR.
| i := i + 1; | ||
| method EmitCallToMain(companion: Expression, mainMethodName: string, hasArgs: bool) returns (s: string) { | ||
| s := "\nfn main() {"; | ||
| if hasArgs { |
There was a problem hiding this comment.
This test of whether the method has arguments is there for historical reasons, but it seems that SinglePassCodeGenerator always add an implicit formal for arguments on main methods even if it's not declared, so I'm not sure the case !hasArgs is tested.
Fixes #5724
Description
--compile-suffixfor emitting the main method name.How has this been tested?
comp/rust/tests.dfytest in a way that was reproducing the two issues mentioned in In Rust, Main fails to pass arguments #5724By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.