feat: Domains and ranges for quantified variables (#2195)

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.

RELEASE_NOTES.md

@@ -1,6 +1,7 @@
 # Upcoming
 
 - feat: The IDE will show verification errors for a method immediately after that method has been verified, instead of after all methods are verified.
+- feat: New syntax for quantified variables, allowing per-variable domains (`x <- C`) and ranges (`x | P(x), y | Q(x, y)`). See [the quantifier domain section](https://dafny-lang.github.io/dafny/DafnyRef/DafnyRef#sec-quantifier-domains) of the Reference Manual.
 - fix: No more display of previous obsolete verification diagnostics if newer are available. (https://github.com/dafny-lang/dafny/pull/2142)
 - feat: Live verification diagnostics for the language server (https://github.com/dafny-lang/dafny/pull/1942)
 - fix: Prevent the language server from crashing and not responding on resolution or ghost diagnostics errors (https://github.com/dafny-lang/dafny/pull/2080)

Source/Dafny/AST/DafnyAst.cs

@@ -6128,6 +6128,63 @@ public BoundVar(IToken tok, string name, Type type)
     }
   }
 
+  /// <summary>
+  /// A QuantifiedVar is a bound variable used in a quantifier such as "forall x :: ...",
+  /// a comprehension such as "set x | 0 <= x < 10", etc.
+  /// In addition to its type, which may be inferred, it can have an optional domain collection expression
+  /// (x <- C) and an optional range boolean expressions (x | E).
+  /// </summary>
+  [DebuggerDisplay("Quantified<{name}>")]
+  public class QuantifiedVar : BoundVar {
+    public readonly Expression Domain;
+    public readonly Expression Range;
+
+    public QuantifiedVar(IToken tok, string name, Type type, Expression domain, Expression range)
+      : base(tok, name, type) {
+      Contract.Requires(tok != null);
+      Contract.Requires(name != null);
+      Contract.Requires(type != null);
+      Domain = domain;
+      Range = range;
+    }
+
+    /// <summary>
+    /// Map a list of quantified variables to an eqivalent list of bound variables plus a single range expression.
+    /// The transformation looks like this in general:
+    ///
+    /// x1 <- C1 | E1, ..., xN <- CN | EN
+    ///
+    /// becomes:
+    ///
+    /// x1, ... xN | x1 in C1 && E1 && ... && xN in CN && EN
+    ///
+    /// Note the result will be null rather than "true" if there are no such domains or ranges.
+    /// Some quantification contexts (such as comprehensions) will replace this with "true".
+    /// </summary>
+    public static void ExtractSingleRange(List<QuantifiedVar> qvars, out List<BoundVar> bvars, out Expression range) {
+      bvars = new List<BoundVar>();
+      range = null;
+
+      foreach (var qvar in qvars) {
+        BoundVar bvar = new BoundVar(qvar.tok, qvar.Name, qvar.SyntacticType);
+        bvars.Add(bvar);
+
+        if (qvar.Domain != null) {
+          // Attach a token wrapper so we can produce a better error message if the domain is not a collection
+          var domainWithToken = QuantifiedVariableDomainCloner.Instance.CloneExpr(qvar.Domain);
+          var inDomainExpr = new BinaryExpr(domainWithToken.tok, BinaryExpr.Opcode.In, new IdentifierExpr(bvar.tok, bvar), domainWithToken);
+          range = range == null ? inDomainExpr : new BinaryExpr(domainWithToken.tok, BinaryExpr.Opcode.And, range, inDomainExpr);
+        }
+
+        if (qvar.Range != null) {
+          // Attach a token wrapper so we can produce a better error message if the range is not a boolean expression
+          var rangeWithToken = QuantifiedVariableRangeCloner.Instance.CloneExpr(qvar.Range);
+          range = range == null ? qvar.Range : new BinaryExpr(rangeWithToken.tok, BinaryExpr.Opcode.And, range, rangeWithToken);
+        }
+      }
+    }
+  }
+
   public class ActualBinding {
     public readonly IToken /*?*/ FormalParameterName;
     public readonly Expression Actual;
@@ -9046,6 +9103,54 @@ public override string val {
     }
   }
 
+  /// <summary>
+  /// A token wrapper used to produce better type checking errors
+  /// for quantified variables. See QuantifierVar.ExtractSingleRange()
+  /// </summary>
+  public class QuantifiedVariableDomainToken : TokenWrapper {
+    public QuantifiedVariableDomainToken(IToken wrappedToken)
+      : base(wrappedToken) {
+      Contract.Requires(wrappedToken != null);
+    }
+
+    public override string val {
+      get { return WrappedToken.val; }
+      set { WrappedToken.val = value; }
+    }
+  }
+
+  /// <summary>
+  /// A token wrapper used to produce better type checking errors
+  /// for quantified variables. See QuantifierVar.ExtractSingleRange()
+  /// </summary>
+  public class QuantifiedVariableRangeToken : TokenWrapper {
+    public QuantifiedVariableRangeToken(IToken wrappedToken)
+      : base(wrappedToken) {
+      Contract.Requires(wrappedToken != null);
+    }
+
+    public override string val {
+      get { return WrappedToken.val; }
+      set { WrappedToken.val = value; }
+    }
+  }
+
+  class QuantifiedVariableDomainCloner : Cloner {
+    public static readonly QuantifiedVariableDomainCloner Instance = new QuantifiedVariableDomainCloner();
+    private QuantifiedVariableDomainCloner() { }
+    public override IToken Tok(IToken tok) {
+      return new QuantifiedVariableDomainToken(tok);
+    }
+  }
+
+  class QuantifiedVariableRangeCloner : Cloner {
+    public static readonly QuantifiedVariableRangeCloner Instance = new QuantifiedVariableRangeCloner();
+    private QuantifiedVariableRangeCloner() { }
+    public override IToken Tok(IToken tok) {
+      return new QuantifiedVariableRangeToken(tok);
+    }
+  }
+
   // ------------------------------------------------------------------------------------------------------
   [DebuggerDisplay("{Printer.ExprToString(this)}")]
   public abstract class Expression {
@@ -11452,11 +11557,19 @@ public LetOrFailExpr(IToken tok, CasePattern<BoundVar>/*?*/ lhs, Expression rhs,
 
   /// <summary>
   /// A ComprehensionExpr has the form:
-  ///   BINDER x Attributes | Range(x) :: Term(x)
-  /// When BINDER is "forall" or "exists", the range may be "null" (which stands for the logical value "true").
-  /// For other BINDERs (currently, "set"), the range is non-null.
-  /// where "Attributes" is optional, and "| Range(x)" is optional and defaults to "true".
-  /// Currently, BINDER is one of the logical quantifiers "exists" or "forall".
+  ///   BINDER { x [: Type] [<- Domain] [Attributes] [| Range] } [:: Term(x)]
+  /// Where BINDER is currently "forall", "exists", "iset"/"set", or "imap"/"map".
+  ///
+  /// Quantifications used to only support a single range, but now each
+  /// quantified variable can have a range attached.
+  /// The overall Range is now filled in by the parser by extracting any implicit
+  /// "x in Domain" constraints and per-variable Range constraints into a single conjunct.
+  ///
+  /// The Term is optional if the expression only has one quantified variable,
+  /// but required otherwise.
+  /// 
+  /// LambdaExpr also inherits from this base class but isn't really a comprehension,
+  /// and should be considered implementation inheritance.
   /// </summary>
   public abstract class ComprehensionExpr : Expression, IAttributeBearingDeclaration, IBoundVarsBearingExpression {
     public virtual string WhatKind => "comprehension";

Source/Dafny/Dafny.atg

@@ -219,6 +219,44 @@ bool IsIdentifier(int kind) {
   return kind == _ident || kind == _least || kind == _greatest || kind == _older;
 }
 
+bool IsQuantifierVariableDecl(QuantifiedVar previousVar) {
+  // Introducing per-quantified variable ranges creates some ambiguities in the grammar,
+  // since before that the range would terminate the quantifed domain. For example, the following statement:
+  //
+  // print set x | E, y;
+  //
+  // This would previously parse as two separate arguments to the print statement, but
+  // could now also be parsed as a single set comprehension argument with two quantified variables
+  // (and an invalid one since it would need an explicit ":: <Term>" section).
+  //
+  // Even worse:
+  //
+  // print set x | E, y <- C;
+  //
+  // This was a valid statement before as well, because "y <- C" would be parsed as the expression
+  // "y < (-C)".
+  //
+  // 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.
+  if (previousVar.Range != null && theOptions.QuantifierSyntax == DafnyOptions.QuantifierSyntaxOptions.Version3) {
+    return false;
+  }
+
+  scanner.ResetPeek();
+  IToken x = scanner.Peek();
+  return la.kind == _comma && IsIdentifier(x.kind);
+}
+
+// Checks for "<-", which has to be parsed as two separate tokens,
+// but ensures no whitespace between them.
+bool IsFromArrow() {
+  scanner.ResetPeek();
+  IToken x = scanner.Peek();
+  return la.kind == _openAngleBracket && x.kind == _minus
+    && la.line == x.line && la.col == x.col - 1; 
+}
+
 bool IsLabel(bool allowLabel) {
   if (!allowLabel) {
     return false;
@@ -500,18 +538,18 @@ bool IsNotEndOfCase() {
 
 /* The following is the largest lookahead there is. It needs to check if what follows
  * can be nothing but "<" Type { "," Type } ">".
- * If inExpressionContext == false and there is an opening '<', then
- * it is assumed, without checking, that what follows is a type parameter list
+ * If inExpressionContext == true, it also checks the token immediately after
+ * the ">" to help disambiguate some cases (see implementation comment).   
  */
 bool IsGenericInstantiation(bool inExpressionContext) {
   scanner.ResetPeek();
-  if (!inExpressionContext) {
-    return la.kind == _openAngleBracket;
-  }
   IToken pt = la;
   if (!IsTypeList(ref pt)) {
     return false;
   }
+  if (!inExpressionContext) {
+    return true;
+  }  
   /* There are ambiguities in the parsing.  For example:
    *     F( a < b , c > (d) )
    * can either be a unary function F whose argument is a function "a" with type arguments "<b,c>" and
@@ -887,6 +925,7 @@ TOKENS
   sarrow = "->".
   qarrow = "~>".
   larrow = "-->".
+  minus = "-".
 COMMENTS FROM "/*" TO "*/" NESTED
 COMMENTS FROM "//" TO lf
 IGNORE cr + lf + tab
@@ -1668,6 +1707,7 @@ GenericParameters<.List<TypeParameter/*!*/>/*!*/ typeArgs, bool allowVariance.>
   // If a "<" combined with a Variance symbol could be a new token, then the parser here will need to be more complex,
   // since, for example, a < followed immediately by a Variance symbol would scan as the wrong token.
   // Fortunately that is not currently the case.
+  // (Only because we parse the new "<-" symbol as separate "<" "-" tokens precisely to avoid this issue :)
   "<"
   [ Variance<out variance>  (. if (!allowVariance) { SemErr(t, "type-parameter variance is not allowed to be specified in this context"); } .)
   ]
@@ -3401,9 +3441,9 @@ ForallStmt<out Statement/*!*/ s>
   "forall"                                  (. x = t; tok = x; .)
 
   ( IF(la.kind == _openparen)  /* disambiguation needed, because of the possibility of a body-less forall statement */
-    "(" [ QuantifierDomain<out bvars, out qattrs, out range> ] ")"
+    "(" [ QuantifierDomain<out bvars, out qattrs, out range, true, true, true> ] ")"
   |     [ IF(IsIdentifier(la.kind))  /* disambiguation needed, because of the possibility of a body-less forall statement */
-          QuantifierDomain<out bvars, out qattrs, out range>
+          QuantifierDomain<out bvars, out qattrs, out range, true, true, true>
         ]
   )
   (. if (bvars == null) { bvars = new List<BoundVar>(); }
@@ -4199,7 +4239,6 @@ MapLiteralExpressions<.out List<ExpressionPair> elements.>
 /*------------------------------------------------------------------------*/
 MapComprehensionExpr<out Expression e, bool allowLemma, bool allowLambda, bool allowBitwiseOps>
 = (. Contract.Ensures(Contract.ValueAtReturn(out e) != null);
-     BoundVar bv;
      List<BoundVar> bvars = new List<BoundVar>();
      Expression range = null;
      Expression bodyLeft = null;
@@ -4208,12 +4247,7 @@ MapComprehensionExpr<out Expression e, bool allowLemma, bool allowLambda, bool a
      bool finite = true;
   .)
   ( "map" | "imap" (. finite = false; .) )     (. IToken mapToken = t; .)
-  IdentTypeOptional<out bv>                    (. bvars.Add(bv); .)
-  { ","
-    IdentTypeOptional<out bv>                  (. bvars.Add(bv); .)
-  }
-  { Attribute<ref attrs> }
-  [ "|" Expression<out range, true, true, true> ]
+  QuantifierDomain<out bvars, out attrs, out range, allowLemma, allowLambda, allowBitwiseOps>
   QSep
   Expression<out bodyRight, allowLemma, allowLambda, allowBitwiseOps>
   [ IF(IsGets())  /* greedily parse ":=" */    (. bodyLeft = bodyRight; .)
@@ -4690,7 +4724,7 @@ QuantifierExpression<out Expression q, bool allowLemma, bool allowLambda>
   ( Forall                                     (. x = t;  univ = true; .)
   | Exists                                     (. x = t; .)
   )
-  QuantifierDomain<out bvars, out attrs, out range>
+  QuantifierDomain<out bvars, out attrs, out range, allowLemma, allowLambda, true>
   QSep
   Expression<out body, allowLemma, allowLambda>
   (. if (univ) {
@@ -4702,41 +4736,59 @@ QuantifierExpression<out Expression q, bool allowLemma, bool allowLambda>
   .
 
 /*------------------------------------------------------------------------*/
-QuantifierDomain<.out List<BoundVar> bvars, out Attributes attrs, out Expression range.>
+QuantifierDomain<.out List<BoundVar> bvars, out Attributes attrs, out Expression range, bool allowLemma, bool allowLambda, bool allowBitwiseOps.>
 = (.
-     bvars = new List<BoundVar>();
-     BoundVar/*!*/ bv;
+     List<QuantifiedVar> qvars = new List<QuantifiedVar>();
+     QuantifiedVar/*!*/ qv;
      attrs = null;
      range = null;
   .)
-  IdentTypeOptional<out bv>                    (. bvars.Add(bv); .)
-  { ","
-    IdentTypeOptional<out bv>                  (. bvars.Add(bv); .)
+  QuantifierVariableDecl<out qv, ref attrs, allowLemma, allowLambda, allowBitwiseOps>         (. qvars.Add(qv); .)
+  { IF(IsQuantifierVariableDecl(qv))
+    ","
+    QuantifierVariableDecl<out qv, ref attrs, allowLemma, allowLambda, allowBitwiseOps>       (. qvars.Add(qv); .)
   }
+  (. QuantifiedVar.ExtractSingleRange(qvars, out bvars, out range); .)
+  .
+
+/*------------------------------------------------------------------------*/
+QuantifierVariableDecl<.out QuantifiedVar qvar, ref Attributes attrs, bool allowLemma, bool allowLambda, bool allowBitwiseOps.>
+= (.
+     BoundVar bv;
+     Expression domain = null;
+     Expression range = null;
+  .)
+  IdentTypeOptional<out bv>
+  [ // "<-" can also appear in GenericParameters in something like "<-T>",
+    // so we parse it as two separate tokens, but use lookahead to ensure
+    // we don't allow whitespace between them.
+    IF(IsFromArrow())
+    "<" "-"
+    // We can't allow bitwise ops here since otherwise we'll swallow up any
+    // optional "| <Range>" suffix 
+    Expression<out domain, allowLemma, allowLambda, false>
+  ]
   { Attribute<ref attrs> }
-  [ IF(la.kind == _verticalbar)   /* Coco complains about this ambiguity, thinking that a "|" can follow a body-less forall statement; I don't see how that's possible, but this IF is good and suppresses the reported ambiguity */
+  [ // Coco complains about this ambiguity, thinking that a "|" can follow a body-less forall statement; 
+    // I don't see how that's possible, but this IF is good and suppresses the reported ambiguity
+    IF(la.kind == _verticalbar) 
     "|"
-    Expression<out range, true, true>
+    Expression<out range, allowLemma, allowLambda, allowBitwiseOps>
   ]
+  (. qvar = new QuantifiedVar(bv.tok, bv.Name, bv.SyntacticType, domain, range); .)
   .
 
 /*------------------------------------------------------------------------*/
 SetComprehensionExpr<out Expression q, bool allowLemma, bool allowLambda, bool allowBitwiseOps>
 = (. Contract.Ensures(Contract.ValueAtReturn(out q) != null);
-     BoundVar bv;
      List<BoundVar/*!*/> bvars = new List<BoundVar>();
      Expression range;
      Expression body = null;
      Attributes attrs = null;
      bool finite = true;
   .)
   ( "set" | "iset" (. finite = false; .) )     (. IToken setToken = t; .)
-  IdentTypeOptional<out bv>                    (. bvars.Add(bv); .)
-  { ","
-    IdentTypeOptional<out bv>                  (. bvars.Add(bv); .)
-  }
-  { Attribute<ref attrs> }
-  "|" Expression<out range, allowLemma, allowLambda, allowBitwiseOps>
+  QuantifierDomain<out bvars, out attrs, out range, allowLemma, allowLambda, allowBitwiseOps>
   [ IF(IsQSep())  /* let any given body bind to the closest enclosing set comprehension */
     QSep
     Expression<out body, allowLemma, allowLambda, allowBitwiseOps || !finite>
@@ -4745,6 +4797,12 @@ SetComprehensionExpr<out Expression q, bool allowLemma, bool allowLambda, bool a
        SemErr(t, "a set comprehension with more than one bound variable must have a term expression");
        q = dummyExpr;
      } else {
+       // This production used to have its own version of QuantifierDomain in which the
+       // range was not optional, so we map null to "true" here so that the rest of the
+       // logic doesn't hit exceptions.
+       if (range == null) {
+         range = LiteralExpr.CreateBoolLiteral(Token.NoToken, true);
+       }
        q = new SetComprehension(setToken, t, finite, bvars, range, body, attrs);
      }
   .)