Merge branch 'main' into jb-separate-files-snapshots

CHANGELOG.md

@@ -1,5 +1,10 @@
 # Unreleased
 
+* Improved handling of comments around clauses/stanzas
+  - Each comment now maintains loyalty to the clause the user picked it to stay with, rather than automatically migrating to the previous clause in the presence of `assert ... by { ... }`-style constructs
+* Support parsing for const generic literals
+* Support parsing `opens_invariants` with specific concrete sets
+
 # v0.4.1
 
 * Minor fix to prevent panic on formatting files containing unbalanced parentheses in strings/chars/...

src/lib.rs

@@ -562,8 +562,18 @@ fn terminal_expr(pairs: &Pairs<Rule>) -> bool {
 }
 
 fn debug_print(pair: Pair<Rule>, indent: usize) {
-    print!("{:indent$}{:?} {{", "", pair.as_rule(), indent = indent);
-    let pairs = pair.into_inner();
+    if pair.as_rule() == Rule::COMMENT {
+        print!(
+            "{:indent$}{:?} {{ {comment:?} ",
+            "",
+            pair.as_rule(),
+            indent = indent,
+            comment = pair.as_str()
+        );
+    } else {
+        print!("{:indent$}{:?} {{", "", pair.as_rule(), indent = indent);
+    }
+    let pairs = pair.clone().into_inner();
     if pairs.peek().is_some() {
         println!();
         pairs.for_each(|p| debug_print(p, indent + 2));

src/verus.pest

@@ -485,7 +485,13 @@ lifetime_arg = {
 }
 
 const_arg = {
-    expr
+    // Currently stable Rust only support literals as const args inside generic
+    // args. In general, it could be arbitrary expressions, but that causes
+    // headaches for parsing (in particular, we need to parse an `expr` that
+    // does _not_ have a `>` sign in it, but our `expr` parsing greedily eats
+    // any `>` that exists within it. Thus, for now, we simply restrict to
+    // literals.
+    literal
 }
 
 generic_args_binding = {
@@ -988,7 +994,11 @@ stmt = !{
   | proof_block
   | let_stmt
   | assignment_stmt
-  | expr_with_block ~ semi_str?
+  // We can't use `expr_with_block ~ semi_str?` here, and instead need to do it
+  // as the two separate ordered alternatives (`ewb ~ semi_str | ewb`) to
+  // prevent munching of multi-newlines that happens otherwise
+  | expr_with_block ~ semi_str
+  | expr_with_block
   | expr ~ semi_str
   | item_no_macro_call
   | macro_call_stmt
@@ -1750,6 +1760,7 @@ unwind_clause = {
 opens_invariants_mode = {
     any_str
   | none_str
+  | lbracket_str ~ comma_delimited_exprs? ~ rbracket_str
 }
 
 opens_invariants_clause = {

tests/verus-consistency.rs

@@ -2453,6 +2453,36 @@ fn fff() {
     baz;
 }
 
+pub fn foo() {
+    // this should stay stuck to the `a`
+    assert(a) by {
+        // whatever
+    }
+    // this should also stay stuck to the `a`
+    // and so should this line
+
+    // but this line
+    // and this line should stick to the `b`
+    b;
+    // and this comment should also stick to the `b`
+
+    // similarly `c`
+    c;
+    // `c` again
+
+    // and an empty comment stands alone
+
+    // similarly `d`
+    d;
+    // `d` again
+
+    // and finally, `d`
+    assert(d) by {
+        // whatever
+    }
+    // well, now done with `d`
+}
+
 } // verus!
 "#;
 
@@ -2470,6 +2500,104 @@ fn fff() {
         baz;
     }
 
+    pub fn foo() {
+        // this should stay stuck to the `a`
+        assert(a) by {
+            // whatever
+        }
+        // this should also stay stuck to the `a`
+        // and so should this line
+
+        // but this line
+        // and this line should stick to the `b`
+        b;
+        // and this comment should also stick to the `b`
+
+        // similarly `c`
+        c;
+        // `c` again
+
+        // and an empty comment stands alone
+
+        // similarly `d`
+        d;
+        // `d` again
+
+        // and finally, `d`
+        assert(d) by {
+            // whatever
+        }
+        // well, now done with `d`
+    }
+
     } // verus!
     "###);
 }
+
+#[test]
+fn verus_const_generics() {
+    // Regression test for https://github.com/verus-lang/verusfmt/issues/90
+    let file = r#"
+verus! {
+       pub fn f<const N: u64>() -> u64 { N }
+       pub fn g<const N: u64, const O: u64>() -> u64 { N }
+ fn main() { f::<123>(); g::<123, 456>(); }
+}
+"#;
+    assert_snapshot!(parse_and_format(file).unwrap(), @r###"
+    verus! {
+
+    pub fn f<const N: u64>() -> u64 {
+        N
+    }
+
+    pub fn g<const N: u64, const O: u64>() -> u64 {
+        N
+    }
+
+    fn main() {
+        f::<123>();
+        g::<123, 456>();
+    }
+
+    } // verus!
+    "###);
+}
+
+#[test]
+fn verus_support_opens_invariants() {
+    // Regression test for https://github.com/verus-lang/verusfmt/issues/91
+    let file = r#"
+verus! {
+    proof fn a() opens_invariants none {}
+    proof fn f() opens_invariants [ 123u8 ] {}
+    proof fn g() opens_invariants [ 123u8, 456u8 ] {}
+    proof fn z() opens_invariants any {}
+}
+"#;
+    assert_snapshot!(parse_and_format(file).unwrap(), @r###"
+    verus! {
+
+    proof fn a()
+        opens_invariants none
+    {
+    }
+
+    proof fn f()
+        opens_invariants [123u8]
+    {
+    }
+
+    proof fn g()
+        opens_invariants [123u8, 456u8]
+    {
+    }
+
+    proof fn z()
+        opens_invariants any
+    {
+    }
+
+    } // verus!
+    "###)
+}