-
Notifications
You must be signed in to change notification settings - Fork 261
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.
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
feat: Dafny Main method to accept optional seq<string> argument #2594
Changes from all commits
dd08b02
9f49d95
bf5b81c
9413f53
7e99661
c53df3d
b308899
aa57f69
e86a74a
e159db4
37a3e81
b080587
af0f559
3f081e5
b28e077
ab3e0a0
eef5c3f
3089663
1805a3d
652df6e
1d9066f
803fda9
e00ef86
f79ade5
62a6cc8
b1364a1
e69c668
ebf8dcb
0ca5a2f
bc7ab88
722824d
2472b61
e748bf1
fbfc0ca
c784ad9
955539b
34ff94a
a6668e1
1ca45b8
440f0a5
c0cfb9e
189aafe
6348703
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -52,13 +52,13 @@ protected override void EmitHeader(Program program, ConcreteSyntaxTree wr) { | |
|
||
public override void EmitCallToMain(Method mainMethod, string baseName, ConcreteSyntaxTree wr) { | ||
Coverage.EmitSetup(wr); | ||
wr.WriteLine("_dafny.HandleHaltExceptions({0}.{1});", mainMethod.EnclosingClass.FullCompileName, mainMethod.IsStatic ? IdName(mainMethod) : "Main"); | ||
wr.WriteLine("_dafny.HandleHaltExceptions(() => {0}.{1}(require('process').argv));", mainMethod.EnclosingClass.FullCompileName, mainMethod.IsStatic ? IdName(mainMethod) : "Main"); | ||
Coverage.EmitTearDown(wr); | ||
} | ||
|
||
protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw) { | ||
protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string argsParameterName) { | ||
var wr = (cw as JavaScriptCompiler.ClassWriter).MethodWriter; | ||
return wr.NewBlock("static Main()"); | ||
return wr.NewBlock($"static Main({argsParameterName})"); | ||
} | ||
|
||
protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, bool isExtern, string/*?*/ libraryName, ConcreteSyntaxTree wr) { | ||
|
@@ -2441,6 +2441,12 @@ public override bool RunTargetProgram(string dafnyProgramName, string targetProg | |
return SendToNewNodeProcess(dafnyProgramName, targetProgramText, callToMain, targetFilename, otherFileNames, outputWriter); | ||
} | ||
|
||
public string ToStringLiteral(string s) { | ||
var wr = new ConcreteSyntaxTree(); | ||
EmitStringLiteral(s, false, wr); | ||
return wr.ToString(); | ||
} | ||
|
||
bool SendToNewNodeProcess(string dafnyProgramName, string targetProgramText, string/*?*/ callToMain, string targetFilename, ReadOnlyCollection<string> otherFileNames, | ||
TextWriter outputWriter) { | ||
Contract.Requires(targetFilename != null || otherFileNames.Count == 0); | ||
|
@@ -2461,6 +2467,7 @@ bool SendToNewNodeProcess(string dafnyProgramName, string targetProgramText, str | |
} | ||
nodeProcess.StandardInput.Write(targetProgramText); | ||
if (callToMain != null && DafnyOptions.O.RunAfterCompile) { | ||
nodeProcess.StandardInput.WriteLine("require('process').argv = [\"node\", " + string.Join(",", DafnyOptions.O.MainArgs.Select(ToStringLiteral)) + "];"); | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Don't we need Javascript quoting here (instead of Dafny quoting?) There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. And more importantly, can't we pass these arguments on node's command line directly? There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. This is JavaScript quoting (ToStringLiteral is a compiler to JavaScript function) |
||
nodeProcess.StandardInput.Write(callToMain); | ||
} | ||
nodeProcess.StandardInput.Flush(); | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This looks odd — what happens if someone has a Dafny module called
os
?There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Then there will be a compilation failure. What would be the alternative?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
A clean error produced by Dafny; but what is bothering me is the special case on the string
os
. We could store tuples in the list of modules (maybe("os", "Args")
and(id, DummyTypeName)
)There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
What do you mean by "we could store tuples in the list of modules"?
One could make this error go away by suppressing these dummy calls.
But overall, I think that if this is a problem down the road, the Go compiler will have to compile a Dafny module named "os" to something else, since "os" is a base package in Go anyway.