Disable ShowSnippets during Test Generation

[Dargones]

The --show-snippets breaks test generation because it relies on casting of Boogie.IToken to Dafny.IToken here and test generation makes changes to the Boogie AST that may introduce new tokens that cannot be cast. This PR disables the option, recently enabled by default, during test generation. An alternative would be to surround the cast with try-catch, but it seems that outside test generation purposes it is probably safe to assume that the cast succeeds. @atomb, @robin-aws would it be possible to merge this before the next release to make sure test generation stays stable?

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[davidcok]

I suggest you add a comment in the ref-man as well that --show-snippets is always disabled for these two commands.

[Dargones]

Thank you for pointing out to the reference manual, @davidcok! I have added a note about --show-snippets and have fixed a few things in the existing description of the generate-tests option as well. From the user perspective, I don't think much will change with --snow-snippets being disabled - test generation does not perform verification of the original Dafny code.

[keyboardDrummer]

test generation makes changes to the Boogie AST that may introduce new tokens that cannot be cast.

Can't we change that?

[Dargones]

Can't we change that?

In principle, yes, and I am working on an overhaul of inlining that will move many AST traversals from Boogie to Dafny and move the code closer to addressing this issue. However, I don't think I know of a way to immediately make sure all tokens can be cast. One major obstacle is that I need to copy Boogie ASTs and the only way of doing this is by printing them to file and then parsing, which loses all connection to Dafny tokens.

In the near future, I think, the only way of making sure test generation does not break is by disabling --sow-snippets.

[atomb]

This mostly looks great. The one suggestion I have is to also fix ShowSnippets for the case where there is no Dafny source location information available. I'm thinking that you could replace this code:

dafny/Source/DafnyCore/DafnyConsolePrinter.cs

Lines 104 to 106 in d72dc7a

	if (Options.Get(ShowSnippets)) {
	WriteSourceCodeSnippet(tok, tw);
	}

with something like

    if (Options.Get(ShowSnippets)) {
      if(tok is IToken dafnyTok) {
        WriteSourceCodeSnippet(dafnyTok, tw);
      } else {
        ErrorWriteLine(tw, "No Dafny location information, so snippet can't be generated."); 
      }
    }

And then make WriteSourceCodeSnippet take a Dafny token instead of a Boogie token.

[Dargones]

Thank you, @atomb! This makes sense, I have made the change.

[atomb]

One tiny additional thing: it seems like the format check wants some white space changes.

[atomb]

Looks good!