feat: continue statements

Source/Dafny/AST/DafnyAst.cs

@@ -7194,11 +7194,11 @@ public class BreakStmt : Statement {
     public readonly IToken TargetLabel;
     public readonly bool IsContinue;
     public string Kind => IsContinue ? "continue" : "break";
-    public readonly int BreakCount; // this includes the final "continue", if any
+    public readonly int BreakAndContinueCount; // this includes the final "continue", if any
     public Statement TargetStmt; // filled in during resolution
     [ContractInvariantMethod]
     void ObjectInvariant() {
-      Contract.Invariant(TargetLabel != null || 1 <= BreakCount);
+      Contract.Invariant(TargetLabel != null || 1 <= BreakAndContinueCount);
     }
 
     public BreakStmt(IToken tok, IToken endTok, IToken targetLabel, bool isContinue)
@@ -7211,15 +7211,15 @@ public BreakStmt(IToken tok, IToken endTok, IToken targetLabel, bool isContinue)
     }
 
     /// <summary>
-    /// For "isContinue == false", represents the statement "break ^breakCount ;".
-    /// For "isContinue == true", represents the statement "break ^(breakCount - 1) continue;".
+    /// For "isContinue == false", represents the statement "break ^breakAndContinueCount ;".
+    /// For "isContinue == true", represents the statement "break ^(breakAndContinueCount - 1) continue;".
     /// </summary>
-    public BreakStmt(IToken tok, IToken endTok, int breakCount, bool isContinue)
+    public BreakStmt(IToken tok, IToken endTok, int breakAndContinueCount, bool isContinue)
       : base(tok, endTok) {
       Contract.Requires(tok != null);
       Contract.Requires(endTok != null);
-      Contract.Requires(1 <= breakCount);
-      this.BreakCount = breakCount;
+      Contract.Requires(1 <= breakAndContinueCount);
+      this.BreakAndContinueCount = breakAndContinueCount;
       this.IsContinue = isContinue;
     }
   }

Source/Dafny/AST/Printer.cs

@@ -1209,7 +1209,7 @@ public void PrintStatement(Statement stmt, int indent) {
         if (s.TargetLabel != null) {
           wr.Write($"{s.Kind} {s.TargetLabel.val};");
         } else {
-          for (int i = 0; i < s.BreakCount - 1; i++) {
+          for (int i = 0; i < s.BreakAndContinueCount - 1; i++) {
             wr.Write("break ");
           }
           wr.Write($"{s.Kind};");

Source/Dafny/Cloner.cs

@@ -580,7 +580,7 @@ public virtual Statement CloneStmt(Statement stmt) {
         if (s.TargetLabel != null) {
           r = new BreakStmt(Tok(s.Tok), Tok(s.EndTok), s.TargetLabel, s.IsContinue);
         } else {
-          r = new BreakStmt(Tok(s.Tok), Tok(s.EndTok), s.BreakCount, s.IsContinue);
+          r = new BreakStmt(Tok(s.Tok), Tok(s.EndTok), s.BreakAndContinueCount, s.IsContinue);
         }
 
       } else if (stmt is ReturnStmt) {

Source/Dafny/Dafny.atg

@@ -2479,24 +2479,24 @@ BreakStmt<out Statement/*!*/ s>
 = (. var isContinue = false;
      IToken start = Token.NoToken;
      IToken label = null;
-     int breakCount = 1;
+     int breakAndContinueCount = 1;
   .)
   ( "continue"              (. start = t; isContinue = true; .)
     [ LabelName<out label> ]
   | "break"                 (. start = t; .)
     ( LabelName<out label>
-    | { "break"             (. breakCount++; .)
+    | { "break"             (. breakAndContinueCount++; .)
       }
-      [ "continue"          (. breakCount++; isContinue = true; .)
+      [ "continue"          (. breakAndContinueCount++; isContinue = true; .)
       ]
     )
   )
   SYNC
   ";"
-  (. Contract.Assert(label == null || breakCount == 1);
+  (. Contract.Assert(label == null || breakAndContinueCount == 1);
      s = label != null ?
        new BreakStmt(start, t, label, isContinue) :
-       new BreakStmt(start, t, breakCount, isContinue);
+       new BreakStmt(start, t, breakAndContinueCount, isContinue);
   .)
   .
 

Source/Dafny/RefinementTransformer.cs

@@ -1536,7 +1536,7 @@ void CheckIsOkayNewStatement(Statement s, Stack<string> labels, int loopLevels)
         Reporter.Error(MessageSource.RefinementTransformer, s, "yield statements are not allowed in skeletons");
       } else if (s is BreakStmt) {
         var b = (BreakStmt)s;
-        if (b.TargetLabel != null ? !labels.Contains(b.TargetLabel.val) : loopLevels < b.BreakCount) {
+        if (b.TargetLabel != null ? !labels.Contains(b.TargetLabel.val) : loopLevels < b.BreakAndContinueCount) {
           Reporter.Error(MessageSource.RefinementTransformer, s, $"{b.Kind} statement in skeleton is not allowed to break outside the skeleton fragment");
         }
       } else if (s is AssignStmt) {

Source/Dafny/Resolver.cs

@@ -11075,16 +11075,17 @@ public void ResolveStatement(Statement stmt, ICodeContext codeContext) {
             s.TargetStmt = target;
           }
         } else {
-          var jumpStmt = s.BreakCount == 1 ?
+          Contract.Assert(1 <= s.BreakAndContinueCount); // follows from BreakStmt class invariant and the guard for this "else" branch
+          var jumpStmt = s.BreakAndContinueCount == 1 ?
             $"a non-labeled '{s.Kind}' statement" :
-            $"a '{Util.Repeat(s.BreakCount - 1, "break ")}{s.Kind}' statement";
+            $"a '{Util.Repeat(s.BreakAndContinueCount - 1, "break ")}{s.Kind}' statement";
           if (loopStack.Count == 0) {
             reporter.Error(MessageSource.Resolver, s, $"{jumpStmt} is allowed only in loops");
-          } else if (loopStack.Count < s.BreakCount) {
+          } else if (loopStack.Count < s.BreakAndContinueCount) {
             reporter.Error(MessageSource.Resolver, s,
-              $"{jumpStmt} is allowed only in contexts with {s.BreakCount} enclosing loops, but the current context only has {loopStack.Count}");
+              $"{jumpStmt} is allowed only in contexts with {s.BreakAndContinueCount} enclosing loops, but the current context only has {loopStack.Count}");
           } else {
-            Statement target = loopStack[loopStack.Count - s.BreakCount];
+            Statement target = loopStack[loopStack.Count - s.BreakAndContinueCount];
             if (target.Labels == null) {
               // make sure there is a label, because the compiler and translator will want to see a unique ID
               target.Labels = new LList<Label>(new Label(target.Tok, null), null);

Source/Dafny/Substituter.cs

@@ -680,7 +680,7 @@ protected virtual Statement SubstStmt(Statement stmt) {
         if (s.TargetLabel != null) {
           rr = new BreakStmt(s.Tok, s.EndTok, s.TargetLabel, s.IsContinue);
         } else {
-          rr = new BreakStmt(s.Tok, s.EndTok, s.BreakCount, s.IsContinue);
+          rr = new BreakStmt(s.Tok, s.EndTok, s.BreakAndContinueCount, s.IsContinue);
         }
         // r.TargetStmt will be filled in as later
         List<BreakStmt> breaks;