feat: Domains and ranges for quantified variables

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 Section [2.6.5](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);
      }
   .)