Handle macro-call statements

Note: we explicitly need to check that the macro call itself is not a
terminating expression, otherwise in statement lists that have macro
calls as the last expression, we would accidentally consider that
particular macro call to be a statement rather than an expression.
While _technically_ that would be fine (since without knowing more about
a macro, it is somewhat ambiguous), the more common use case for macros
in such a position is an expression, so it is better to parse such a
macro as an expression rather than as a statement

src/lib.rs

@@ -727,6 +727,7 @@ fn to_doc<'a>(
         Rule::lifetime_arg => map_to_doc(ctx, arena, pair),
         Rule::const_arg => unsupported(pair),
         Rule::macro_call => s,
+        Rule::macro_call_stmt => s,
         Rule::punctuation => map_to_doc(ctx, arena, pair),
         Rule::token => map_to_doc(ctx, arena, pair),
         Rule::delim_token_tree => map_to_doc(ctx, arena, pair),

src/verus.pest

@@ -464,6 +464,20 @@ macro_call = {
     attr* ~ path ~ bang_str ~ !"=" ~ token_tree
 }
 
+// NOTE: By convention, stmt-like or item-like macros (e.g., calc!{}) tend to
+// use curly braces; this is only a convention though, and _technically_ one
+// could use parens or square brackets for the same. However, we use this to
+// disambiguate unknown macros when used in statement lists _without_
+// semi-colons; if it is intended as an expr, the user better be using parens.
+//
+// Another alternative is to use `!(expr ~ "}") ~ macro_call` rather than
+// `macro_call_stmt`, but as of now, I believe this to be a better choice; we
+// can switch to the alternative if we find situations where it might be better
+// suited.
+macro_call_stmt = {
+    attr* ~ path ~ bang_str ~ !"=" ~ lbrace_str ~ token_tree* ~ rbrace_str
+}
+
 // See https://doc.rust-lang.org/beta/reference/tokens.html#punctuation
 punctuation = {
     bin_expr_ops
@@ -869,6 +883,7 @@ stmt = {
   | expr_with_block ~ semi_str?
   | expr ~ semi_str
   | item_no_macro_call
+  | macro_call_stmt
 }
 
 let_stmt = {

tests/verus-consistency.rs

@@ -457,6 +457,59 @@ verus!{
     "###);
 }
 
+#[test]
+fn verus_macro_statements() {
+    let file = r#"
+    verus! {
+
+    // Notice that the semicolon is optional
+    proof fn foo() {
+        calc! {
+        (==)
+        1int; {}
+        (0int + 1int); {}
+    };
+        calc! {
+        (==)
+        1int; {}
+        (0int + 1int); {}
+    }
+        calc! {
+        (==)
+        1int; {}
+        (0int + 1int); {}
+    }
+    }
+
+    }
+"#;
+
+    assert_snapshot!(parse_and_format(file).unwrap(), @r###"
+    verus! {
+
+    // Notice that the semicolon is optional
+    proof fn foo() {
+        calc! {
+            (==)
+            1int; {}
+            (0int + 1int); {}
+        };
+        calc! {
+            (==)
+            1int; {}
+            (0int + 1int); {}
+        }
+        calc! {
+            (==)
+            1int; {}
+            (0int + 1int); {}
+        }
+    }
+
+    } // verus!
+    "###);
+}
+
 #[test]
 fn verus_impl() {
     let file = r#"