Change of argument syntax for reveal statements

[RustanLeino]

Today, reveal statements can have two kinds of arguments. One kind is a label (see, e.g., Section 7 of the Dafny Power User note on Different Styles of Proofs). The other kind is a function. (And maybe there will be additional kinds of arguments in the future.)

The syntax for the second kind of reveal statement (that is, using a function) is inconsistent with other uses of functions. For a function F of any arity, today's syntax to reveal it is reveal F(). That is, F is followed by a pair of parentheses, but never any arguments. I propose we change the syntax and meaning of reveal for functions as follows:

0. If F is an opaque function without type arguments, then reveal F says to reveal the body of F for all arguments. (In other words, this is like reveal F() today.)
1. If F is an opaque function with (say, 2) type parameters, then reveal F<A, B> says to reveal the body of F for all arguments after instantiating F's type parameters with the types A and B.
2. If F is an opaque function, then reveal F<A, B>(args) where args is a (possibly empty) list of arguments and the optional <A, B> gives explicit type arguments to F (if <A, B> is omitted, then Dafny tries to infer the type arguments in the usual way) says to reveal the body of F for the given parameters (after filling in any default values for parameters).
3. If F is a function that is not opaque, then the forms above give a warning that the attempted revelation has no effect.
4. Today, the {:opaque} functions and reveal statements work via implicitly generated lemmas (called reveal_F for a function F. These lemmas are surfaced in programs and can be called directly. Those lemmas should be removed (which will also address issue Bad error message when forgetting the parens on a reveal statement #1618).

Remarks and design points:

• If F has no type arguments, then the proposed reveal F (bullet 0) is like today's reveal F(). However, if F does take type arguments, then today's reveal F() also quantifies over them. In the new syntax proposed, there is no way to quantify over all type arguments. I don't actually know if this breaking change is onerous to existing programs, but it seems more wholesome and consistent with the rest of the language.
• As an aid in syntax migration, we could allow reveal F() even for functions with a non-0 number of default-less parameters. Such a statement could be treated like reveal F (that is, as today's reveal F(), if F has no type parameters) while producing a deprecation warning.
• I'm suggesting that we generate a warning, rather than an error, for bullet 3 above. Today, we generate an error. A warning is nice, because if your function is opaque and you have a bunch of reveal statements in your code and you decide to temporarily make the function not opaque, then it's nice not to have to go remove all the reveal statements temporarily, too.

[cpitclaudel]

A side note:

A warning is nice, because if your function is opaque and you have a bunch of reveal statements in your code and you decide to temporarily make the function not opaque, then it's nice not to have to go remove all the reveal statements temporarily, too.

Alternatively, with the current style, you can temporarily create a lemma called reveal_F.

[MikaelMayer]

Excellent proposal. I agree to all of your points. I don't have data to add about the breaking change to not quantify over type parameters though.

As a side note, reveal is providing fuel to the function; would it be possible to give a custom fuel during the invocation of reveal somehow?

[kjx]

A warning is nice, because if your function is opaque ... it's nice not to have to go remove all the reveal statements temporarily, too.

absolutely. i've hit this repeatedly recently.

[atomb]

There's another issue with the argument syntax for reveal that I've come across a number of times recently. It currently requires a valid expression, which means that if you want an instance function of a data type or class you need to have an instance of that type in scope. That is, you need an object, o, so you can write o.f. It should, instead, be possible to write T.f, where T is the type containing f. That way, if one of the functions that you call creates an instance o of T as an intermediate value, and calls f on it, you can reveal that f even without having direct access to o.