feat: Domains and ranges for quantified variables #2195

robin-aws · 2022-06-02T04:45:23Z

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:

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.
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.

~~NOTE: I still have one more commit to add changes to the reference manual and a few more tests (especially of the /quantifierSyntax option), but a review of the rest is welcome in the meantime!~~

Also resolves #2038 (and the same issue for Java) since I hit it when converting test cases, and it was dead easy to fix.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

…to new-quantifier-syntax

MikaelMayer

A few minor things, but the feature introduced in this PR looks great, very well documented and tested, congratulations for the big effort.

Source/Dafny/AST/DafnyAst.cs

Source/Dafny/Compilers/SinglePassCompiler.cs

Source/Dafny/Dafny.atg

MikaelMayer · 2022-06-03T21:18:24Z

Test/comp/ComprehensionsNewSyntax.dfy

+  // thus needs to capture the value of "s" into another variable, which these tests check on.
+  var s := [0, 1, 1, 2];
+  s := s + [3, 5, 8, 13];
+  print forall x <- s :: x < 20, " ";  // true


I'm so happy to see the reduction in the duplication of the variable x! Great job!

Oh, I didn't realize that this would be supported in forall/exists! I thought it was just for set/seq/multiset

Might as well! They all have the same underlying quantifier domain semantics, so I like the simplicity of aligning the syntax.

Still worth checking a bit more broadly, maybe ^^

I'm afraid I'm not following, checking what exactly? This was the intention in the RFC all along at least.

It was unexpected to me, despite having read the proposals, so I'm guessing it might be unexpected to other people who provided feedback as well; that's it :)

Test/comp/ComprehensionsNewSyntax.dfy

MikaelMayer · 2022-06-03T21:21:16Z

Test/comp/ForallNewSyntax.dfy

@@ -0,0 +1,356 @@
+// RUN: %dafny /quantifierSyntax:4 /compile:3 /spillTargetCode:2 /compileTarget:cs "%s" > "%t"


Could you verify once, and then use /compile:4 here as well?

Good call, this is just what the original test file was doing.

MikaelMayer · 2022-06-03T21:26:48Z

docs/DafnyRef/Grammar.md

+    [ <- Expression(allowLemma, allowLambda) ]
+    { Attribute }
+    [ | Expression(allowLemma, allowLambda) ]
+````


Only three backticks are necessary.

Also, I think we all agreed on that and all the documentation needs to be reformatted accordingly, but could you perhaps start the effort by moving this grammar to the end of this section and replace it with a few examples? That would be less frightening.

I did have trouble finding the best place for this content. It's shared syntax between multiple features but it's not an Expression or Statement or Type or anything else independent like that. But it's also substantially less "low-level" than the other productions.

Are you suggesting moving it to the end of Section 2, as a 2.7?

Are you suggesting moving it to the end of Section 2, as a 2.7?

No I'm not suggesting changing numbering or the order of sections and sub-sections.
I'm only suggesting to not place the grammar at the beginning of this section, only at the end (until it will be moved to another place). The beginning of the section should consist of introductory text to the features and example covering most use cases.

So, instead of:

### 2.6.5. Quantifier Domains {#sec-quantifier-domains} <frightening and unreadable grammar definitions> <introduction text> <examples> <more text>

I strongly suggest you write:

### 2.6.5. Quantifier Domains {#sec-quantifier-domains} <introduction text> <examples> <more text> <frightening and unreadable grammar definitions>

Aha thanks for clarifying. I will gladly start setting a better example. :)

Co-authored-by: Mikaël Mayer <MikaelMayer@users.noreply.github.com>

atomb

This is very nice! All of the changes I requested are tiny little things (and one question).

docs/DafnyRef/UserGuide.md

Test/comp/ComprehensionsNewSyntax.dfy

atomb · 2022-06-06T23:02:52Z

Source/Dafny/Dafny.atg

  }
+  (. QuantifiedVar.ExtractSingleRange(qvars, out bvars, out range); .)


Do I understand correctly that future uses of this new syntax won't call ExtractSingleRange, but will keep the components separate? That seems like it would be necessary for the expected operational semantics of foreach, for example (once you get to that!).

That's right, the next PR will add domains and ranges to BoundVar instead, and ExtractSingleRange will likely be removed. But this PR will establish a ton of test cases that still have to work after that refactoring. :)

keyboardDrummer · 2022-06-10T10:01:54Z

Source/Dafny/DafnyOptions.cs

@@ -992,6 +1010,16 @@ is printed.
    experimentalPredicateAlwaysGhost - Compiled functions are written `function`.
        Ghost functions are written `ghost function`. Predicates are always ghost
        and are written `predicate`.
+/quantifierSyntax:<version>


Would be nice if we can reuse Options.txt here.

I had that thought too, perhaps in the future we can have a common Options.md that we strip the markdown from when outputting it as part of /help

keyboardDrummer

Love the relatively small scope of this PR :-) makes the review manageable.

Quality of code, documentation and tests looks excellent!

atomb

Nice work! I'm looking forward to the point when we can start using these new features. :)

MikaelMayer

Great job with the documentation, I like it much much better!
A few tweaks to make documentation more friendly.

RELEASE_NOTES.md

MikaelMayer · 2022-06-10T15:21:41Z

docs/DafnyRef/Grammar.md

+- `x <- integerSet`
+- `x: nat <- integerSet`
+- `x: nat <- integerSet | x % 2 == 0`
+- `x: nat, y: nat | x < 2 && y < 2`


Suggested change

- `x: nat, y: nat | x < 2 && y < 2`

- `x: nat, y: nat | x < 2 && y < 2`

- `x: nat | x < 2, y: nat | y < x`

It would be good to have a simpler example just before the next one, because the next one uses vertical bars for a different meaning.

Yeah I like this, more of a gradual onramp of complexity :)

MikaelMayer · 2022-06-10T15:25:45Z

docs/DafnyRef/Grammar.md

+   which restricts the bindings to values that satisfy this expression.
+   In the example above `x <= 5` is the range attached to the `x` variable declaration.
+
+3. The optional syntax `<- C` attaches a collection expression `C` as a *quantified variable domain*.


Could you move this one before 2, so that it's the order in which we parse things?

I was on the edge of doing this already and you have tipped me over :)

Co-authored-by: Mikaël Mayer <MikaelMayer@users.noreply.github.com>

robin-aws added 30 commits March 16, 2022 19:02

Add SeqComprehension and parsing support

e154fc2

First cut of resolution, dummy translation for now

1f55a85

Fix parsing ambiguity with sequence constructions

9c86216

First try at parsing changes

1d564a5

Unify QuantifierDomain parsing, bug fix

fe946d7

Fix precedence issue with |

d67c1fe

Sequence comprehension printing

529c75e

Partial fix

9eb0cf8

Fix lambdas (incorrect type check in resolver)

fc75a3c

Split off seq construction production to fix suffixes

3618756

Merge branch 'master' into sequence-comprehensions

675e28e

Default to null range

386ea1f

Handle seq constructions with explicit type args too

d819d59

Fix parsing of “<-“

20eccfc

Just a spoonful of lookahead makes the medicine go down

0525859

Missing file

53628aa

Added IsQuantifierVariableDecl lookahead

db8534e

Undoing sequence comprehension changes for this branch

0964304

Whitespace cleanup

5cf115d

Merge branch 'master' into new-quantifier-syntax

3bc4f59

Hook up /quantifierSyntax, copy and modify several test files

5694696

Merge branch 'new-quantifier-syntax' of github.com:robin-aws/dafny in…

c5c1ca9

…to new-quantifier-syntax

Enable IsGenericInstantiation lookahead outside expressions

d24a665

Various test/runtime fixes

7d44c65

Formatting

2eef52a

Rename test

85ebc3a

Improve resolution errors through token wrappers

21ec6bb

Singletons, more tests

cb97941

Don’t force | true on all quantifications, add comments

4c4bb4d

Formatting

c1934ca

Document /quantifierSyntax

450b9a7

robin-aws requested review from cpitclaudel, atomb and MikaelMayer June 3, 2022 02:12

MikaelMayer requested changes Jun 3, 2022

View reviewed changes

robin-aws and others added 2 commits June 3, 2022 15:45

Apply suggestions from code review

5441b09

Co-authored-by: Mikaël Mayer <MikaelMayer@users.noreply.github.com>

More PR feedback

39bd359

atomb requested changes Jun 6, 2022

View reviewed changes

robin-aws added 5 commits June 6, 2022 19:26

Reorder and improve Quantifier Domains refman content

341e927

Bit more PR feedback

4df4b5d

Merge branch 'master' into new-quantifier-syntax-sugar-only

9140144

Fix test file

7c80d10

Add release notes and note on CLI option

e7c1900

keyboardDrummer reviewed Jun 10, 2022

View reviewed changes

keyboardDrummer previously approved these changes Jun 10, 2022

View reviewed changes

Merge branch 'master' into new-quantifier-syntax-sugar-only

b4af540

atomb previously approved these changes Jun 10, 2022

View reviewed changes

MikaelMayer requested changes Jun 10, 2022

View reviewed changes

robin-aws dismissed stale reviews from atomb and keyboardDrummer via 48250b8 June 10, 2022 15:40

robin-aws and others added 3 commits June 10, 2022 08:40

Update RELEASE_NOTES.md

48250b8

Co-authored-by: Mikaël Mayer <MikaelMayer@users.noreply.github.com>

PR feedback

a29f370

I can count, I swear

cbd0f03

MikaelMayer approved these changes Jun 10, 2022

View reviewed changes

robin-aws merged commit f22a8af into dafny-lang:master Jun 10, 2022

robin-aws deleted the new-quantifier-syntax-sugar-only branch June 10, 2022 16:35

cpitclaudel added a commit to dafny-lang/compiler-bootstrap that referenced this pull request Jun 30, 2022

interop: Adjust model to dafny-lang/dafny#2195

7876436

robin-aws mentioned this pull request Jun 30, 2022

Feature idea: quantified variable domains in assign/let-such-that #2340

Open

cpitclaudel added a commit to dafny-lang/compiler-bootstrap that referenced this pull request Jul 12, 2022

interop: Adjust model to dafny-lang/dafny#2195

14abf35

robin-aws mentioned this pull request Feb 22, 2023

Change default values of CLI options for Dafny 4.0 #2548

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: Domains and ranges for quantified variables #2195

feat: Domains and ranges for quantified variables #2195

robin-aws commented Jun 2, 2022 •

edited

Loading

MikaelMayer left a comment

MikaelMayer Jun 3, 2022

cpitclaudel Jun 3, 2022

robin-aws Jun 3, 2022

cpitclaudel Jun 3, 2022

robin-aws Jun 4, 2022

cpitclaudel Jun 6, 2022

MikaelMayer Jun 3, 2022

robin-aws Jun 3, 2022

MikaelMayer Jun 3, 2022

robin-aws Jun 3, 2022 •

edited

Loading

MikaelMayer Jun 6, 2022

robin-aws Jun 6, 2022

atomb left a comment

atomb Jun 6, 2022

robin-aws Jun 7, 2022

keyboardDrummer Jun 10, 2022

robin-aws Jun 10, 2022

keyboardDrummer left a comment

atomb left a comment

MikaelMayer left a comment

MikaelMayer Jun 10, 2022

robin-aws Jun 10, 2022

MikaelMayer Jun 10, 2022

robin-aws Jun 10, 2022

		@@ -0,0 +1,356 @@
		// RUN: %dafny /quantifierSyntax:4 /compile:3 /spillTargetCode:2 /compileTarget:cs "%s" > "%t"

		}
		(. QuantifiedVar.ExtractSingleRange(qvars, out bvars, out range); .)

	- `x: nat, y: nat \| x < 2 && y < 2`
	- `x: nat, y: nat \| x < 2 && y < 2`
	- `x: nat \| x < 2, y: nat \| y < x`

feat: Domains and ranges for quantified variables #2195

feat: Domains and ranges for quantified variables #2195

Conversation

robin-aws commented Jun 2, 2022 • edited Loading

MikaelMayer left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

robin-aws Jun 3, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

atomb left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

keyboardDrummer left a comment

Choose a reason for hiding this comment

atomb left a comment

Choose a reason for hiding this comment

MikaelMayer left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

robin-aws commented Jun 2, 2022 •

edited

Loading

robin-aws Jun 3, 2022 •

edited

Loading