Allow forall statements in expressions

[wilcoxjay]

Occasionally, when a function has a universally quantified precondition, it would be convenient to be able to use a forall statement to prove the precondition inline in an expression context.

[RustanLeino]

Nice idea. I think this would be simple to implement. It would involve another use of the StmtExpr production, which already handles (calls and the more similar) assert/assume/calc statements.

[wilcoxjay]

It's good to hear that this shouldn't introduce any new difficulties in translation.

One thing I'm worried about is parsing it. I think it will be impossible to distinguish forall statement-expressions from universal quantifiers until the opening curly brace or ensures token. I don't think we can even distinguish these with a lookahead, because we need to skip over arbitrary expressions. Instead, we may need to introduce new nonterminals for "a prefix of either a universal quantifier or a forall statement-expression".