Feat: Support for --bprint in language server. (#4206)

I add this as a way to simplify boogie debugging, especially in cases
when VSCode is not consistent with the command-line like in #4205

I did not add any test for that as it's meant for Dafny development
only, but I tested it manually. I borrowed the code from the driver.
Should I still list it as a feature?

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

Source/DafnyDriver/DafnyDriver.cs

@@ -607,16 +607,16 @@ public enum CommandLineArgumentsResult {
  }
 
  public static IEnumerable<Tuple<string, Bpl.Program>> Translate(ExecutionEngineOptions options, Program dafnyProgram) {
- var nmodules = Translator.VerifiableModules(dafnyProgram).Count();
+ var modulesCount = Translator.VerifiableModules(dafnyProgram).Count();
 
 
  foreach (var prog in Translator.Translate(dafnyProgram, dafnyProgram.Reporter)) {
 
  if (options.PrintFile != null) {
 
- var nm = nmodules > 1 ? Dafny.DafnyMain.BoogieProgramSuffix(options.PrintFile, prog.Item1) : options.PrintFile;
+ var fileName = modulesCount > 1 ? Dafny.DafnyMain.BoogieProgramSuffix(options.PrintFile, prog.Item1) : options.PrintFile;
 
- ExecutionEngine.PrintBplFile(options, nm, prog.Item2, false, false, options.PrettyPrint);
+ ExecutionEngine.PrintBplFile(options, fileName, prog.Item2, false, false, options.PrettyPrint);
  }
 
  yield return prog;

Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs

@@ -52,10 +52,17 @@ DafnyOptions options
 
  cancellationToken.ThrowIfCancellationRequested();
 
+ if (engine.Options.PrintFile != null) {
+ var moduleCount = Translator.VerifiableModules(program).Count();
+ foreach (var (suffix, boogieProgram) in translated) {
+ var fileName = moduleCount > 1 ? DafnyMain.BoogieProgramSuffix(engine.Options.PrintFile, suffix) : engine.Options.PrintFile;
+ ExecutionEngine.PrintBplFile(engine.Options, fileName, boogieProgram, false, false, engine.Options.PrettyPrint);
+ }
+ }
+
  return translated.SelectMany(t => {
  var (_, boogieProgram) = t;
- var results = engine.GetImplementationTasks(boogieProgram);
- return results;
+ return engine.GetImplementationTasks(boogieProgram);
  }).ToList();
  }
 

Source/DafnyLanguageServer/ServerCommand.cs

@@ -59,6 +59,7 @@ related locations
  GhostIndicators,
  LineVerificationStatus,
  VerifySnapshots,
+ DeveloperOptionBag.BoogiePrint,
  CommonOptionBag.EnforceDeterminism,
  CommonOptionBag.UseJavadocLikeDocstringRewriterOption
  }.Concat(ICommandSpec.VerificationOptions).

docs/dev/news/bprint-option-in language-server.feat

@@ -0,0 +1 @@
+Support for the `--bprint` option for language server arguments