Fix precedence for quantifiers and triple-op exprs (#26)

Fixes #25 

Basically, rather than considering `&&&` and `|||` to be prefix+binary
operations (as the actual Verus parser does), we instead split them out
into their own expression group. This allows us to fix the parsing
precedence with respect to quantifiers.

Co-authored-by: Jay Bosamiya

src/lib.rs

@@ -952,6 +952,25 @@ fn to_doc<'a>(
         Rule::expr_outer => map_to_doc(ctx, arena, pair),
         Rule::expr_outer_no_struct => map_to_doc(ctx, arena, pair),
         Rule::expr_no_struct => map_to_doc(ctx, arena, pair),
+        Rule::bulleted_expr => block_braces(arena, map_to_doc(ctx, arena, pair), true),
+        Rule::bulleted_expr_inner => {
+            let pairs = pair.into_inner();
+            let mut first = true;
+            arena.concat(pairs.map(|p| {
+                let d = to_doc(ctx, p.clone(), arena);
+                match p.as_rule() {
+                    Rule::triple_and | Rule::triple_or => {
+                        if first {
+                            first = false;
+                            d
+                        } else {
+                            arena.hardline().append(d)
+                        }
+                    }
+                    _ => d,
+                }
+            }))
+        }
         Rule::macro_expr => unsupported(pair),
         Rule::literal => map_to_doc(ctx, arena, pair),
         Rule::path_expr => map_to_doc(ctx, arena, pair),
@@ -982,12 +1001,18 @@ fn to_doc<'a>(
         Rule::fn_block_expr => {
             let pairs = pair.into_inner();
             let mapped = map_pairs_to_doc(ctx, arena, &pairs);
-            block_braces(arena, mapped, terminal_expr(&pairs))
+            block_braces(
+                arena,
+                mapped,
+                terminal_expr(&pairs)
+                    || pairs
+                        .clone()
+                        .any(|x| x.as_rule() == Rule::bulleted_expr_inner),
+            )
         }
         Rule::prefix_expr => map_to_doc(ctx, arena, pair),
         Rule::prefix_expr_no_struct => map_to_doc(ctx, arena, pair),
         Rule::assignment_ops => docs![arena, arena.space(), s, arena.line()],
-        Rule::bin_expr_ops_special => arena.hardline().append(map_to_doc(ctx, arena, pair)),
         Rule::bin_expr_ops_normal => docs![arena, arena.line(), s, arena.space()]
             .nest(INDENT_SPACES)
             .group(),

src/verus.pest

@@ -923,6 +923,8 @@ expr_inner_no_struct = _{
   | assert_expr
   | assume_expr
   | assert_forall_expr
+  | bulleted_expr
+  | bulleted_expr_inner
   | block_expr
   | box_expr
   | break_expr
@@ -1038,6 +1040,15 @@ expr_with_block = {
   | assert_forall_expr
 }
 
+bulleted_expr = {
+    "{" ~ bulleted_expr_inner ~ "}"
+}
+
+bulleted_expr_inner = {
+    (triple_and ~ expr)+
+  | (triple_or ~ expr)+
+}
+
 macro_expr = {
     macro_call
 }
@@ -1091,28 +1102,25 @@ fn_block_expr = {
     attr* ~
     stmt* ~
     expr? ~
-    "}"     
+    "}"
+  | "{" ~ bulleted_expr_inner ~ "}"
 }
 
 prefix_expr = {
-    attr* ~ (dash_str | bang_str | star_str | triple_or | triple_and) ~ expr
+    attr* ~ (dash_str | bang_str | star_str) ~ expr
 }
 
 prefix_expr_no_struct = {
-    attr* ~ (dash_str | bang_str | star_str | triple_or | triple_and) ~ expr_no_struct
+    attr* ~ (dash_str | bang_str | star_str) ~ expr_no_struct
 }
 
 assignment_ops = {
     "=" | "+=" | "/=" | "*=" | "%=" | ">>=" | "<<=" | "-=" | "|=" | "&=" | "^="
 }
 
-bin_expr_ops_special = {
-    triple_or | triple_and
-}
-
 bin_expr_ops_normal = {
-    | ("||" | "|")
-    | ("&&" | "&")
+    | (!"|||" ~ ("||" | "|"))
+    | (!"&&&" ~ ("&&" | "&"))
     | "<==>"
     | "===" | "=~=" | "=~~="
     | "==>" | "<=="
@@ -1124,7 +1132,7 @@ bin_expr_ops_normal = {
 }
 
 bin_expr_ops = {
-    bin_expr_ops_special | bin_expr_ops_normal
+    bin_expr_ops_normal
 }
 
 paren_expr_inner = {

tests/verus-consistency.rs

@@ -1435,3 +1435,20 @@ fn test()
     } // verus!
     "###);
 }
+
+#[test]
+fn verus_quantifier_and_bulleted_expr_precedence() {
+    // Regression test for https://github.com/jaybosamiya/verusfmt/issues/25
+    let file = r#"  verus! { spec fn foo() { &&& forall|x:int| f &&& g } }  "#;
+
+    assert_snapshot!(parse_and_format(file).unwrap(), @r###"
+    verus! {
+
+    spec fn foo() {
+        &&& forall|x: int| f
+        &&& g
+    }
+
+    } // verus!
+    "###);
+}