From 97c48460c49f556a37ff305d8103dd17bb4d4454 Mon Sep 17 00:00:00 2001
From: Jay Bosamiya <jaybosamiya@gmail.com>
Date: Fri, 2 Feb 2024 16:25:46 -0500
Subject: [PATCH] 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                 |  1 +
 src/verus.pest             | 15 +++++++++++
 tests/verus-consistency.rs | 53 ++++++++++++++++++++++++++++++++++++++
 3 files changed, 69 insertions(+)

diff --git a/src/lib.rs b/src/lib.rs
index 4371ac4..1a99749 100644
--- a/src/lib.rs
+++ b/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),
diff --git a/src/verus.pest b/src/verus.pest
index 782c525..5ffc4ab 100644
--- a/src/verus.pest
+++ b/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 = {
diff --git a/tests/verus-consistency.rs b/tests/verus-consistency.rs
index 52f148d..154a67e 100644
--- a/tests/verus-consistency.rs
+++ b/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#"