Change of argument syntax for reveal statements #2689
Labels
breaking-change
Any change that will cause existing Dafny codebases to break (excluding verification instability)
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
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 functionF
of any arity, today's syntax to reveal it isreveal F()
. That is,F
is followed by a pair of parentheses, but never any arguments. I propose we change the syntax and meaning ofreveal
for functions as follows:F
is an opaque function without type arguments, thenreveal F
says to reveal the body ofF
for all arguments. (In other words, this is likereveal F()
today.)F
is an opaque function with (say, 2) type parameters, thenreveal F<A, B>
says to reveal the body ofF
for all arguments after instantiatingF
's type parameters with the typesA
andB
.F
is an opaque function, thenreveal F<A, B>(args)
whereargs
is a (possibly empty) list of arguments and the optional<A, B>
gives explicit type arguments toF
(if<A, B>
is omitted, then Dafny tries to infer the type arguments in the usual way) says to reveal the body ofF
for the given parameters (after filling in any default values for parameters).F
is a function that is not opaque, then the forms above give a warning that the attempted revelation has no effect.{:opaque}
functions andreveal
statements work via implicitly generated lemmas (calledreveal_F
for a functionF
. 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:
F
has no type arguments, then the proposedreveal F
(bullet 0) is like today'sreveal F()
. However, ifF
does take type arguments, then today'sreveal 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.reveal F()
even for functions with a non-0 number of default-less parameters. Such a statement could be treated likereveal F
(that is, as today'sreveal F()
, ifF
has no type parameters) while producing a deprecation warning.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 thereveal
statements temporarily, too.The text was updated successfully, but these errors were encountered: