Use more restrictive parse for returns clauses

verus-lang · Jan 14, 2025 · b1a295c · b1a295c
1 parent 4adfbf5
commit b1a295c
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 1 deletion.
diff --git 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
@@ -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 = {