From 5f2e230cfb4a2b0d7f0497e0569b13603c1ab9dc Mon Sep 17 00:00:00 2001
From: Robin Salkeld <salkeldr@amazon.com>
Date: Fri, 12 Aug 2022 16:13:45 -0700
Subject: [PATCH 1/4] Support for x to y

---
 Source/Dafny/Dafny.atg | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 34042e97926..e7306b348ff 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -381,6 +381,7 @@ bool IsParenStar() {
 bool IsEquivOp() => IsEquivOp(la);
 bool IsImpliesOp() => IsImpliesOp(la);
 bool IsExpliesOp() => IsExpliesOp(la);
+bool IsToOp() => IsToOp(la);
 bool IsAndOp() => IsAndOp(la);
 bool IsOrOp() => IsOrOp(la);
 static bool IsEquivOp(IToken la) {
@@ -392,6 +393,9 @@ static bool IsImpliesOp(IToken la) {
 static bool IsExpliesOp(IToken la) {
   return la.val == "<==" || la.val == "\u21d0";
 }
+static bool IsToOp(IToken la) {
+  return la.val == "to";
+}
 static bool IsAndOp(IToken la) {
   return la.val == "&&" || la.val == "\u2227";
 }
@@ -3735,7 +3739,7 @@ EquivExpression<out Expression e0, bool allowLemma, bool allowLambda, bool allow
 ImpliesExpliesExpression<out Expression e0, bool allowLemma, bool allowLambda, bool allowBitwiseOps>
 = (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1; .)
   LogicalExpression<out e0, allowLemma, allowLambda, allowBitwiseOps>
-  [ IF(IsImpliesOp() || IsExpliesOp())  /* read an ImpliesExpliesExpression as far as possible */
+  [ IF(IsImpliesOp() || IsExpliesOp() || IsToOp())  /* read an ImpliesExpliesExpression as far as possible */
     /* Note, the asymmetry in the parsing of implies and explies expressions stems from the fact that
      * implies is right associative whereas reverse implication is left associative
      */
@@ -3751,6 +3755,9 @@ ImpliesExpliesExpression<out Expression e0, bool allowLemma, bool allowLambda, b
                                                               .)
       }
       [ IF(IsImpliesOp()) ImpliesOp (. SemErr(t, "Ambiguous use of ==> and <==. Use parentheses to disambiguate."); .) ]
+    // TODO: Hack
+    | ident                                                   (. x = t; .)
+      LogicalExpression<out e1, allowLemma, allowLambda, allowBitwiseOps>       (. e0 = new SeqDisplayExpr(x, new List<Expression>()); .)
     )
   ]
   .

From 897241e06de0defda2cb79f492734ba676f2c07e Mon Sep 17 00:00:00 2001
From: Robin Salkeld <salkeldr@amazon.com>
Date: Fri, 12 Aug 2022 16:51:47 -0700
Subject: [PATCH 2/4] Adding `<- C | R` as alternative for `:|`

---
 Source/Dafny/Dafny.atg | 38 +++++++++++++++++++++++++++++++++++---
 1 file changed, 35 insertions(+), 3 deletions(-)

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index e7306b348ff..c7c97df21ef 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -2872,6 +2872,13 @@ UpdateStmt<out Statement/*!*/ s>
         "assume"                   (. suchThatAssume = t; .)
       ]
       Expression<out suchThat, false, true>
+    | "<" "-"                      (. x = Token.NoToken; .)
+      Expression<out e, false, true, false>        (. /* Ignore for now */ .)
+      "|"
+      [ IF(la.kind == _assume)     /* an Expression can also begin with an "assume", so this says to resolve it to pick up any "assume" here */
+        "assume"                   (. suchThatAssume = t; .)
+      ]
+      Expression<out suchThat, false, true>
     | ":-"                         (. x = t; .)
       [ IF(IsAssumeTypeKeyword(la))     /* an Expression can also begin with these keywords, so this says to resolve it to pick up the keyword here */
         ("expect"|"assert"|"assume")    (. keywordToken = t; .)
@@ -3017,6 +3024,13 @@ VarDeclStatement<.out Statement/*!*/ s.>
         "assume"                     (. suchThatAssume = t; .)
       ]
       Expression<out suchThat, false, true>
+    | "<" "-"                        (. assignTok = Token.NoToken; .)
+      Expression<out suchThat, false, true, false>        (. /* Ignore for now */ .)
+      "|"
+      [ IF(la.kind == _assume)       /* an Expression can also begin with an "assume", so this says to resolve it to pick up any "assume" here */
+        "assume"                     (. suchThatAssume = t; .)
+      ]
+      Expression<out suchThat, false, true>
     | ":-"                           (. assignTok = t; .)
       [ IF(IsAssumeTypeKeyword(la))     /* an Expression can also begin with these keywords, so this says to resolve it to pick up the keyword here */
         ("expect"|"assert"|"assume")    (. keywordToken = t; .)
@@ -3310,15 +3324,23 @@ BindingGuard<out Expression e, bool allowLambda>
      BoundVar bv;  IToken x;
      Attributes attrs = null;
      Expression body;
+     e = dummyExpr; /* mute the warning */
   .)
   IdentTypeOptional<out bv>                    (. bvars.Add(bv); x = bv.tok; .)
   { ","
     IdentTypeOptional<out bv>                  (. bvars.Add(bv); .)
   }
   { Attribute<ref attrs> }
-  ":|"
-  Expression<out body, true, allowLambda>
-  (. e = new ExistsExpr(x, t, bvars, null, body, attrs); .)
+  (
+    ":|"
+    Expression<out body, true, allowLambda>
+    (. e = new ExistsExpr(x, t, bvars, null, body, attrs); .)
+  | "<" "-"
+    Expression<out body, false, true, false>        (. /* Ignore for now */ .)
+    "|"
+    Expression<out body, true, allowLambda>
+    (. e = new ExistsExpr(x, t, bvars, null, body, attrs); .)
+  )
   .
 
 
@@ -4438,6 +4460,16 @@ LetExprWithLHS<out Expression e, bool allowLemma, bool allowLambda, bool allowBi
                                          }
                                        }
                                     .)
+    | "<" "-"
+      Expression<out e, false, true, false>        (. /* Ignore for now */ .)
+      "|"
+                                    (. exact = false;
+                                       foreach (var lhs in letLHSs) {
+                                         if (lhs.Arguments != null) {
+                                           SemErr(lhs.tok, "LHS of let-such-that expression must be variables, not general patterns");
+                                         }
+                                       }
+                                    .)
     | ":-"                          (. isLetOrFail = true; .)
     )
     Expression<out e, false, true>        (. letRHSs.Add(e); .)

From 56e8236231752cd1b84fc0d5f46e142d218e1946 Mon Sep 17 00:00:00 2001
From: Robin Salkeld <salkeldr@amazon.com>
Date: Sat, 13 Aug 2022 07:51:06 -0700
Subject: [PATCH 3/4] Add SeqRangeExpr

---
 Source/Dafny/AST/DafnyAst.cs | 15 +++++++++++++++
 Source/Dafny/Dafny.atg       | 33 ++++++++++++++++++++-------------
 2 files changed, 35 insertions(+), 13 deletions(-)

diff --git a/Source/Dafny/AST/DafnyAst.cs b/Source/Dafny/AST/DafnyAst.cs
index 4e621620fc4..ad90d012c4e 100644
--- a/Source/Dafny/AST/DafnyAst.cs
+++ b/Source/Dafny/AST/DafnyAst.cs
@@ -10139,6 +10139,21 @@ public SeqDisplayExpr(IToken tok, List<Expression> elements)
     }
   }
 
+  public class SeqRangeExpr : Expression {
+    public readonly Expression Start;
+    public readonly Expression End;
+    public readonly bool GoingUp;
+    public SeqRangeExpr(IToken tok, Expression start, Expression end, bool goingUp)
+      : base(tok) {
+      Contract.Requires(tok != null);
+      Contract.Requires(start != null);
+      Contract.Requires(end != null);
+      Start = start;
+      End = end;
+      GoingUp = goingUp;
+    }
+  }
+
   public class MemberSelectExpr : Expression {
     public readonly Expression Obj;
     public readonly string MemberName;
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index c7c97df21ef..2c1bae74cbf 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -381,7 +381,7 @@ bool IsParenStar() {
 bool IsEquivOp() => IsEquivOp(la);
 bool IsImpliesOp() => IsImpliesOp(la);
 bool IsExpliesOp() => IsExpliesOp(la);
-bool IsToOp() => IsToOp(la);
+bool IsRangeOp() => IsRangeOp(la);
 bool IsAndOp() => IsAndOp(la);
 bool IsOrOp() => IsOrOp(la);
 static bool IsEquivOp(IToken la) {
@@ -393,8 +393,8 @@ static bool IsImpliesOp(IToken la) {
 static bool IsExpliesOp(IToken la) {
   return la.val == "<==" || la.val == "\u21d0";
 }
-static bool IsToOp(IToken la) {
-  return la.val == "to";
+static bool IsRangeOp(IToken la) {
+  return la.val == "to" || la.val == "downto";
 }
 static bool IsAndOp(IToken la) {
   return la.val == "&&" || la.val == "\u2227";
@@ -3234,6 +3234,7 @@ ForLoopStmt<out Statement stmt>
 = (. Contract.Ensures(Contract.ValueAtReturn(out stmt) != null);
      IToken x;
      BoundVar loopIndex;
+     Expression over;
      Expression start;
      Expression end = null;
      bool goingUp = true;
@@ -3255,11 +3256,18 @@ ForLoopStmt<out Statement stmt>
   { Attribute<ref attrs> }
   IdentTypeOptional<out loopIndex>
   ":="
-  Expression<out start, false, false>
-  ForLoopDirection<out goingUp>
-  ( Expression<out end, false, false>
-  | "*"
-  )
+  Expression<out over, false, false>
+  (. 
+    if (over is SeqRangeExpr range) {
+      start = range.Start;
+      end = range.End;
+      goingUp = range.GoingUp;
+    } else {
+      SemErr(over.tok, "A 'for' loop must iterate over a range expression");
+      start = dummyExpr;
+      end = dummyExpr;
+    }
+  .)
   LoopSpec<invariants, decreases, ref mod, ref decAttrs, ref modAttrs>
   ( IF(la.kind == _lbrace)      /* if there's an open brace, claim it as the beginning of the loop body (as opposed to a BlockStmt following the loop) */
     BlockStmt<out body, out bodyStart, out bodyEnd>  (. endTok = body.EndTok; isDirtyLoop = false; .)
@@ -3759,9 +3767,9 @@ EquivExpression<out Expression e0, bool allowLemma, bool allowLambda, bool allow
 
 /*------------------------------------------------------------------------*/
 ImpliesExpliesExpression<out Expression e0, bool allowLemma, bool allowLambda, bool allowBitwiseOps>
-= (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1; .)
+= (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1; bool goingUp;.)
   LogicalExpression<out e0, allowLemma, allowLambda, allowBitwiseOps>
-  [ IF(IsImpliesOp() || IsExpliesOp() || IsToOp())  /* read an ImpliesExpliesExpression as far as possible */
+  [ IF(IsImpliesOp() || IsExpliesOp() || IsRangeOp())  /* read an ImpliesExpliesExpression as far as possible */
     /* Note, the asymmetry in the parsing of implies and explies expressions stems from the fact that
      * implies is right associative whereas reverse implication is left associative
      */
@@ -3777,9 +3785,8 @@ ImpliesExpliesExpression<out Expression e0, bool allowLemma, bool allowLambda, b
                                                               .)
       }
       [ IF(IsImpliesOp()) ImpliesOp (. SemErr(t, "Ambiguous use of ==> and <==. Use parentheses to disambiguate."); .) ]
-    // TODO: Hack
-    | ident                                                   (. x = t; .)
-      LogicalExpression<out e1, allowLemma, allowLambda, allowBitwiseOps>       (. e0 = new SeqDisplayExpr(x, new List<Expression>()); .)
+    | ForLoopDirection<out goingUp>                                             
+      LogicalExpression<out e1, allowLemma, allowLambda, allowBitwiseOps>       (. e0 = new SeqRangeExpr(t, e0, e1, goingUp); .)
     )
   ]
   .

From 0b6bb17887a545e4a00a34939942e7a8d51ea350 Mon Sep 17 00:00:00 2001
From: Robin Salkeld <salkeldr@amazon.com>
Date: Sat, 13 Aug 2022 08:48:27 -0700
Subject: [PATCH 4/4] Support wildcard

---
 Source/Dafny/Dafny.atg | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 2c1bae74cbf..4434f1f614f 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -3260,7 +3260,7 @@ ForLoopStmt<out Statement stmt>
   (. 
     if (over is SeqRangeExpr range) {
       start = range.Start;
-      end = range.End;
+      end = range.End is WildcardExpr ? null : range.End;
       goingUp = range.GoingUp;
     } else {
       SemErr(over.tok, "A 'for' loop must iterate over a range expression");
@@ -3786,7 +3786,7 @@ ImpliesExpliesExpression<out Expression e0, bool allowLemma, bool allowLambda, b
       }
       [ IF(IsImpliesOp()) ImpliesOp (. SemErr(t, "Ambiguous use of ==> and <==. Use parentheses to disambiguate."); .) ]
     | ForLoopDirection<out goingUp>                                             
-      LogicalExpression<out e1, allowLemma, allowLambda, allowBitwiseOps>       (. e0 = new SeqRangeExpr(t, e0, e1, goingUp); .)
+      PossiblyWildExpression<out e1, allowLambda, true>       (. e0 = new SeqRangeExpr(t, e0, e1, goingUp); .)
     )
   ]
   .