From b1a295ce34b5d53e68d124c908997ccafcc82e44 Mon Sep 17 00:00:00 2001
From: Jay Bosamiya <jayb@microsoft.com>
Date: Tue, 14 Jan 2025 14:54:04 -0800
Subject: [PATCH] Use more restrictive parse for `returns` clauses

---
 src/lib.rs     | 3 +++
 src/verus.pest | 6 +++++-
 2 files changed, 8 insertions(+), 1 deletion(-)

diff --git a/src/lib.rs b/src/lib.rs
index 3459074..a0969dc 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -1333,6 +1333,9 @@ fn to_doc<'a>(
         Rule::groupable_comma_delimited_exprs_for_verus_clauses => {
             map_to_doc(ctx, arena, pair).nest(INDENT_SPACES).group()
         }
+        Rule::single_expr_for_verus_clause => {
+            comma_delimited_full(ctx, arena, pair).nest(INDENT_SPACES)
+        }
         Rule::verus_clause_non_expr => map_to_doc(ctx, arena, pair),
         Rule::requires_clause => map_to_doc(ctx, arena, pair),
         Rule::ensures_clause => map_to_doc(ctx, arena, pair),
diff --git a/src/verus.pest b/src/verus.pest
index 271c23b..0b422a8 100644
--- a/src/verus.pest
+++ b/src/verus.pest
@@ -1722,6 +1722,10 @@ groupable_comma_delimited_exprs_for_verus_clauses = {
     comma_delimited_exprs_for_verus_clauses
 }
 
+single_expr_for_verus_clause = {
+    !verus_clause_non_expr ~ expr_no_struct ~ ","?
+}
+
 verus_clause_non_expr = _{
     "{"             // TODO: Why is this permitted here?
   | requires_str
@@ -1746,7 +1750,7 @@ ensures_clause = {
 }
 
 returns_clause = {
-    returns_str ~ comma_delimited_exprs_for_verus_clauses?
+    returns_str ~ single_expr_for_verus_clause
 }
 
 invariant_except_break_clause = {