Implement quantified variable domains and ranges #2187
Assignees
Labels
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
part: language definition
Relating to the Dafny language definition itself
status: designed
Issues that have a complete story on how to implement this feature and why we want it
Comments
robin-aws
added
kind: enhancement
robin-aws
added a commit
that referenced
this issue
Jun 10, 2022
Resolves #2187. First phase of implementing dafny-lang/rfcs#10. This change adds two new features on several uses of quantified variables in the language: 1. Quantified variable *domains*, specified with the syntax `x <- C`, where C is an expression with a collection type (i.e. set, multiset, sequence, or map). Besides offering a more compact syntax for a common pattern (i.e. replacing `myLovelyButLongVariableName | myLovelyButLongVariableName in someSet` with `myLovelyButLongVariableName <- someSet`), this is forwards-compatible with the notion of *ordered quantification*, which the two features designed in the linked RFC depend on, and potentially others in the future. 2. Quantified variable *ranges*, specified with the syntax `x | E`, where E is a boolean expression. These replace the existing concept of a single `| E` range after all quantified variables (which is now bound to the last declared variable, with equivalent semantics). These are helpful for restricting the values of one quantified variable so that it can be used in the domain expression of another variable. These features apply to the quantifier domains used in `forall` and `exists` expressions, `set` and `map` comprehensions, and `forall` statements, and the parsing for quantifier domains is now shared between these features. As a small consequence, set comprehensions now no longer require range expressions, and will default to `| true`. This new syntax is not fully backwards-compatible: the statement `print set x | 0 <= x < 10, y`, for example, was previously parsed as `print (set x | 0 <= x < 10), (y)` but will now be parsed as `print (set x | 0 <= x < 10, y)` and rejected. The `/quantifierSyntax` option is used to help migrate this otherwise breaking change: * `/quantifierSyntax:3` keeps the old behaviour where a `| <Range>` always terminates the list of quantified variables. * `/quantifierSyntax:4` instead attempts to parse additional quantified variables. Like `/functionSyntax`, this option will default to `4` instead in Dafny 4.0. This is implemented with pure desugaring for now: the `QuantifiedDomain` production parses a list of `QuantifiedVar` objects, but then immediately rewrites a snippet such as `x <- C | P(x), y <- D(x) | Q(x, y)` into the equivalent (for now) `x | x in C && P(x) && y in D(x) && Q(x, y)`. Token wrappers are used to ensure error messages can still refer to the original syntax. This will not be equivalent once features that depend on the ordering of quantification are added, though, so a subsequent change will add the new fields to `BoundVar` instead and plumb these extra components through the whole Dafny pipeline. On testing: I duplicated several existing test files and modified them to use the new syntax features, to get good white-box test coverage even though the implementation is very simple for now. Also resolves #2038 (and the same issue for Java) since I hit it when converting test cases, and it was dead easy to fix.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Alternate syntax for quantification that will support future features that depend on ordered quantification (sequence comprehensions and
foreachloops).See dafny-lang/rfcs#10 for detailed design.
The text was updated successfully, but these errors were encountered: