Add X-is-a-statement-not-an-expression error messages

[RustanLeino]

Summary

Dafny makes a hard distinction between expressions and statements. Users can get these mixed up. When an expression context is trying to use a statement (other than those allowed in StmtExpr's), then it would be nice if the error message was more direct about this.

Background and Motivation

Here's an example:

function F(): int {
  for i := 0 to 10 {
  }
}

This currently gives invalid UnaryExpression. Better would be "it looks like your trying to use a for statement in an expression context, but a statement is not an expression".

Proposed Feature

Can this error be substituted in the Coco-generated code? Can it be checked in the parser without causing too many ambiguous-start-symbol errors from the parser generator?

Alternatives

No response