Support dividing statement lists into clauses/stanzas (#79)

This commit adds support for dividing statement lists into clauses/stanzas. This prevents the need for the empty `//` workaround to divide code into stanzas.

Specifically, with this, the following code is considered well-formatted:

```rs
verus! {

fn fff() {
    reveal(f1);

    foo;

    bar;
    baz;
}

} // verus!
```

Prior to this, verusfmt would have collapsed the additional newlines around `foo;`. With this PR, we maintain the additional
newlines (_however_ if there are too many newlines, we bring it down to just the two, as a stylistic choice).

Note: this _only_ adds support for stanzas for statement lists. It explicitly does _not_ work in general contexts (such as dividing a single expression up via extra newlines). I believe that supporting stanzas at the statement level should cover most people's use cases for them, while limiting the scope of the shenanigans necessary for the parser to be able to handle the special case of the double/multi-newline.

CHANGELOG.md

@@ -1,5 +1,7 @@
 # Unreleased
 
+* Support dividing statement lists into clauses/stanzas
+
 # v0.3.7
 
 * Support attributes in `broadcast group`s

examples/ironfleet.rs

@@ -2899,7 +2899,6 @@ pub open spec fn is_valid_lio_op<IdType, MessageType>(
 // send interaces.
 // LIoOpOrderingOKForAction
 // LIoOpSeqCompatibleWithReduction
-
 } // verus!
     // verus
 }
@@ -12360,7 +12359,6 @@ pub proof fn flatten_sets_singleton_auto<A>()
 
 // TODO(Tej): We strongly suspect there is a trigger loop in these auto
 // lemmas somewhere, but it's not easy to see from the profiler yet.
-
 } // verus!
     }
 }

examples/pagetable.rs

@@ -10722,7 +10722,6 @@ pub open spec fn next(s1: HWVariables, s2: HWVariables) -> bool {
 //         HWStep::TLBEvict { vaddr }                  => (),
 //     }
 // }
-
 } // verus!
     }
 

src/lib.rs

@@ -539,7 +539,7 @@ fn expr_only_block(r: Rule, pairs: &Pairs<Rule>) -> bool {
     let count = pairs.clone().fold(0, |count, p| {
         count
             + match p.as_rule() {
-                Rule::attr | Rule::stmt | Rule::COMMENT => 1,
+                Rule::attr | Rule::stmt | Rule::COMMENT | Rule::MULTI_NEWLINE => 1,
                 Rule::expr => {
                     // We don't want to treat a triple expr as an expr only block,
                     // since that would result in it being grouped with its surrounding braces
@@ -1334,6 +1334,7 @@ fn to_doc<'a>(
         Rule::trigger_attribute => unsupported(pair),
 
         Rule::WHITESPACE => arena.nil(),
+        Rule::MULTI_NEWLINE => arena.hardline(),
         Rule::COMMENT => comment_to_doc(ctx, arena, pair, true),
         Rule::multiline_comment => s.append(arena.line()),
         Rule::verus_macro_body => items_to_doc(ctx, arena, pair, false),
@@ -1602,7 +1603,7 @@ fn parse_and_format(s: &str) -> miette::Result<String> {
         match rule {
             Rule::non_verus | Rule::COMMENT => {
                 formatted_output += pair.as_str();
-                if matches!(pair.as_rule(), Rule::COMMENT) && is_multiline_comment(&pair) {
+                if matches!(pair.as_rule(), Rule::COMMENT) {
                     formatted_output += "\n";
                 }
             }
@@ -1624,12 +1625,8 @@ fn parse_and_format(s: &str) -> miette::Result<String> {
                     (prefix_comments, body, suffix_comments)
                 };
                 formatted_output += VERUS_PREFIX;
-                let mut final_prefix_comment_is_multiline = false;
                 for comment in &prefix_comments {
                     formatted_output += comment.as_str();
-                    final_prefix_comment_is_multiline = is_multiline_comment(comment);
-                }
-                if !prefix_comments.is_empty() && final_prefix_comment_is_multiline {
                     formatted_output += "\n";
                 }
 
@@ -1638,7 +1635,13 @@ fn parse_and_format(s: &str) -> miette::Result<String> {
                 if !suffix_comments.is_empty() {
                     formatted_output += "\n";
                 }
+                let mut first = true;
                 for comment in suffix_comments {
+                    if !first {
+                        formatted_output += "\n";
+                    } else {
+                        first = false;
+                    }
                     formatted_output += comment.as_str();
                 }
                 formatted_output += VERUS_SUFFIX;

src/verus.pest

@@ -40,17 +40,25 @@ WHITESPACE = _{
   " " | "\t" | NEWLINE
 }
 
+/// Multiple-newlines that can be collapsed into a single double-newline
+///
+/// Only supported on a subset of syntactic locations; anywhere else,
+/// double-newlines are collapsed as if they were just normal whitespace.
+MULTI_NEWLINE = @{
+    (" " | "\t")* ~ NEWLINE ~ ((" " | "\t")* ~ NEWLINE)+ ~ (" " | "\t")*
+}
+
 /// Comment syntax; NOT ignored in the syntax tree that is parsed. Allowed to
 /// exist between any tokens (except atomic tokens, of course).
 COMMENT = @{
     // Outer docstring
-    ("//!" ~ (!NEWLINE ~ ANY)* ~ NEWLINE)
+    ("//!" ~ (!NEWLINE ~ ANY)* ~ &NEWLINE)
     // Inner docstring
-  | ("///" ~ (!NEWLINE ~ ANY)* ~ NEWLINE)
+  | ("///" ~ (!NEWLINE ~ ANY)* ~ &NEWLINE)
     // Multiline comment
   | multiline_comment
     // Singleline comment
-  | ("//" ~ (!NEWLINE ~ ANY)* ~ NEWLINE)
+  | ("//" ~ (!NEWLINE ~ ANY)* ~ &NEWLINE)
 }
 
 multiline_comment = @{
@@ -922,7 +930,7 @@ attr_core = {
     | "#" ~ bang_str? ~ "[" ~ !"verusfmt" ~ meta ~ "]"
 }
 // Two aliases for attr_core, so that we can print them differently
-attr = {
+attr = !{
    attr_core
 }
 
@@ -939,7 +947,11 @@ broadcast_use_list = {
 }
 
 broadcast_uses = {
-    broadcast_use+
+    // We explicitly eat up the extra WHITESPACEs here
+    // to prevent it from messing with the MULTI_NEWLINE
+    // handling, which would otherwise cause extra newlines
+    // to show up.
+    broadcast_use+ ~ WHITESPACE*
 }
 
 broadcast_use = {
@@ -970,7 +982,7 @@ verusfmt_skipped_stmt = {
     stmt
 }
 
-stmt = {
+stmt = !{
     (attr* ~ verusfmt_skip_attribute ~ attr* ~ verusfmt_skipped_stmt)
   | semi_str
   | proof_block
@@ -1007,7 +1019,7 @@ verusfmt_skipped_expr_no_struct = {
 
 // This split of `expr` and `expr_inner` is to simply break the left-recursion
 // that would happen otherwise.
-expr = {
+expr = !{
     (attr* ~ verusfmt_skip_attribute ~ attr* ~ verusfmt_skipped_expr)
   | expr_inner ~
     expr_outer*
@@ -1200,11 +1212,11 @@ path_expr_no_generics = {
     attr* ~ path_no_generics
 }
 
-stmt_list = {
-    "{" ~
-    attr* ~
-    stmt* ~
-    expr? ~
+stmt_list = ${
+    "{" ~ (WHITESPACE | COMMENT)* ~
+    (attr ~ (WHITESPACE | COMMENT)*)* ~
+    (stmt ~ (MULTI_NEWLINE | WHITESPACE | COMMENT)*)* ~
+    expr? ~ (WHITESPACE | COMMENT)* ~
     "}"
 }
 
@@ -1221,13 +1233,13 @@ block_expr = {
     | attr* ~ label? ~ (try_str | unsafe_str | async_str | const_str)? ~ stmt_list
 }
 
-fn_block_expr = {
-    "{" ~
-    attr* ~
-    stmt* ~
-    expr? ~
+fn_block_expr = ${
+    "{" ~ (WHITESPACE | COMMENT)* ~
+    (attr ~ (WHITESPACE | COMMENT)*)* ~
+    (stmt ~ (MULTI_NEWLINE | WHITESPACE | COMMENT)*)* ~
+    expr? ~ (WHITESPACE | COMMENT)* ~
     "}"
-  | "{" ~ bulleted_expr_inner ~ "}"
+  | "{" ~ (WHITESPACE | COMMENT)* ~ bulleted_expr_inner ~ (WHITESPACE | COMMENT)* ~ "}"
 }
 
 prefix_expr = {

tests/verus-consistency.rs

@@ -383,6 +383,7 @@ pub fn test() {
 
     pub fn test() {
         let Some((key, val)) = cur else { panic!()  /* covered by while condition */  };
+
         let Some((key, val)) = cur else { panic!() };
     }
 
@@ -782,7 +783,6 @@ fn len<T>(l: List<T>) -> nat {
             _ => false,
         }
     }
-
 }
 
 }
@@ -2402,3 +2402,41 @@ pub broadcast group group_hash_axioms { axiom_hash_map_contains_deref_key,
     } // verus!
     "###);
 }
+
+#[test]
+fn verus_support_separating_logical_blocks() {
+    let file = r#"
+verus! {
+
+fn fff() {
+    reveal(f1);  // reveal f1's definition just inside this block
+
+
+    reveal(f1);  // reveal f1's definition just inside this block
+
+    foo;
+
+    bar;
+    baz;
+}
+
+} // verus!
+"#;
+
+    assert_snapshot!(parse_and_format(file).unwrap(), @r###"
+    verus! {
+
+    fn fff() {
+        reveal(f1);  // reveal f1's definition just inside this block
+
+        reveal(f1);  // reveal f1's definition just inside this block
+
+        foo;
+
+        bar;
+        baz;
+    }
+
+    } // verus!
+    "###);
+}