Parse generic-confusables in Verus clauses

src/lib.rs

@@ -706,8 +706,11 @@ fn to_doc<'a>(
         Rule::lifetime => s.append(arena.space()),
         Rule::lifetime_no_space => s,
         Rule::path => map_to_doc(ctx, arena, pair),
+        Rule::path_no_generics => map_to_doc(ctx, arena, pair),
         Rule::path_segment => map_to_doc(ctx, arena, pair),
+        Rule::path_segment_no_generics => map_to_doc(ctx, arena, pair),
         Rule::generic_arg_list => map_to_doc(ctx, arena, pair),
+        Rule::generic_arg_list_with_colons => map_to_doc(ctx, arena, pair),
         Rule::generic_args => comma_delimited(ctx, arena, pair, false).group(),
         Rule::generic_arg => map_to_doc(ctx, arena, pair),
         Rule::type_arg => map_to_doc(ctx, arena, pair),
@@ -925,6 +928,7 @@ fn to_doc<'a>(
         Rule::macro_expr => unsupported(pair),
         Rule::literal => map_to_doc(ctx, arena, pair),
         Rule::path_expr => map_to_doc(ctx, arena, pair),
+        Rule::path_expr_no_generics => map_to_doc(ctx, arena, pair),
         Rule::stmt_list => {
             let rule = pair.as_rule();
             let pairs = pair.clone().into_inner();

src/verus.pest

@@ -389,13 +389,29 @@ lifetime_no_space = { lifetime }  // A lifetime that shouldn't be followed by a
 
 path = { (path_segment ~ colons_str)* ~ path_segment }
 
+// A version of path without supporting `a<x>`, to allow for proper parsing of
+// clauses such as
+//
+//   requires foo < 3, foo > 0,
+//
+// See https://github.com/jaybosamiya/verusfmt/issues/19 for more details on
+// what prompted this change.
+path_no_generics = { (path_segment_no_generics ~ colons_str)* ~ path_segment_no_generics }
+
 path_segment = {
     colons_str? ~ name_ref ~ generic_arg_list?
   | colons_str? ~ name_ref ~ param_list ~ ret_type?
   | colons_str? ~ name_ref
   | langle_str ~ path_type ~ (as_str ~ path_type)? ~ rangle_str
 }
 
+path_segment_no_generics = {
+    colons_str? ~ name_ref ~ generic_arg_list_with_colons?
+  | colons_str? ~ name_ref ~ param_list ~ ret_type?
+  | colons_str? ~ name_ref
+  | langle_str ~ path_type ~ (as_str ~ path_type)? ~ rangle_str
+}
+
 generic_args = {
     generic_arg ~ ("," ~ generic_arg)* ~ ","?
 }
@@ -404,6 +420,10 @@ generic_arg_list = {
     colons_str? ~ langle_str ~ generic_args? ~ rangle_str
 }
 
+generic_arg_list_with_colons = {
+    colons_str ~ langle_str ~ generic_args? ~ rangle_str
+}
+
 generic_arg = {
     type_arg
   | assoc_type_arg
@@ -896,7 +916,7 @@ expr_inner_no_struct = _{
   | yield_expr
   | yeet_expr
   | let_expr_no_struct
-  | path_expr   // Needs to be late in this list, or it matches against keywords like "while"  
+  | path_expr_no_generics   // Needs to be late in this list, or it matches against keywords like "while"
   | underscore_expr // Needs to follow path_expr, so we don't parse "_x" as "_" followed by an unexpected "x"
 }
 
@@ -976,6 +996,7 @@ expr_inner = {
   | quantifier_expr
   | prefix_expr
   | expr_inner_no_struct
+  | path_expr
 }
 
 expr_with_block = {
@@ -1012,6 +1033,10 @@ path_expr = {
     attr* ~ path
 }
 
+path_expr_no_generics = {
+    attr* ~ path_no_generics
+}
+
 stmt_list = {
     "{" ~
     attr* ~

tests/verus-consistency.rs

@@ -1312,3 +1312,31 @@ exec static LAZY_X: Lazy<X> ensures LAZY_X.wf() { Lazy::<X>::new() }
     } // verus!
     "###);
 }
+
+#[test]
+fn verus_requires_clauses_confusable_with_generics() {
+    // Regression test for https://github.com/jaybosamiya/verusfmt/issues/19
+    let file = r#"
+verus! {
+
+fn test()
+    requires i < 0, len > 0,
+{
+}
+
+} // verus!
+"#;
+
+    assert_snapshot!(parse_and_format(file).unwrap(), @r###"
+    verus! {
+
+    fn test()
+        requires
+            i < 0,
+            len > 0,
+    {
+    }
+
+    } // verus!
+    "###);
+}