Add support for type_bound_list

examples/wip.rs

@@ -1,18 +1,19 @@
 verus! {
 
-pub fn clone_vec_u8() {
-    let i = 0;
-    while i < v.len()
-        invariant
-            i <= v.len(),
-            i == out.len(),
-            forall |j| #![auto] 0 <= j < i  ==> out@[j] == v@[j],
-        ensures
-            i > 0,
-        decreases
-            72,
-    {
-        i = i + 1;
+struct StrictlyOrderedVec<K: KeyTrait> {
+    a: int,
+}
+
+struct DelegationMap<
+    #[verifier(maybe_negative)]
+    K: KeyTrait + VerusClone,
+> {
+    b: int,
+}
+
+impl<K: KeyTrait + VerusClone> DelegationMap<K> {
+    fn view() -> Map<K, AbstractEndPoint> {
+        c
     }
 }
 

src/lib.rs

@@ -400,9 +400,8 @@ fn to_doc<'a>(
         | Rule::star_str
         | Rule::tilde_str
         | Rule::underscore_str => s,
-        Rule::fn_traits => s,
+        Rule::fn_traits | Rule::impl_str => s,
         Rule::pipe_str => docs!(arena, arena.line(), s, arena.space()),
-        Rule::rarrow_str => docs!(arena, arena.space(), s, arena.space()),
         //        Rule::triple_and |
         //        Rule::triple_or =>
         //            docs![arena, arena.hardline(), s, arena.space()].nest(INDENT_SPACES),
@@ -412,7 +411,9 @@ fn to_doc<'a>(
         Rule::eq_str => docs![arena, arena.space(), s, arena.line_(), arena.space()]
             .nest(INDENT_SPACES - 1)
             .group(),
-        Rule::else_str => docs![arena, arena.space(), s, arena.space()],
+        Rule::plus_str | Rule::rarrow_str | Rule::else_str => {
+            docs![arena, arena.space(), s, arena.space()]
+        }
         Rule::assert_space_str
         | Rule::async_str
         | Rule::auto_str
@@ -438,7 +439,6 @@ fn to_doc<'a>(
         | Rule::i64_str
         | Rule::i8_str
         | Rule::if_str
-        | Rule::impl_str
         | Rule::in_str
         | Rule::int_str
         | Rule::isize_str
@@ -638,11 +638,31 @@ fn to_doc<'a>(
                 .append(block_braces(arena, map_to_doc(ctx, arena, pair), true))
         }
         Rule::assoc_item => map_to_doc(ctx, arena, pair),
-        Rule::r#impl => map_to_doc(ctx, arena, pair),
+        Rule::r#impl => {
+            let has_generic_params = pair
+                .clone()
+                .into_inner()
+                .find(|p| matches!(p.as_rule(), Rule::spaced_generic_param_list));
+            arena.concat(pair.into_inner().map(|p| {
+                let r = p.as_rule();
+                let d = to_doc(ctx, p, arena);
+                match r {
+                    Rule::impl_str => {
+                        if has_generic_params.is_none() {
+                            d.append(arena.space())
+                        } else {
+                            d
+                        }
+                    }
+                    _ => d,
+                }
+            }))
+        }
         Rule::extern_block => unsupported(pair),
         Rule::extern_item_list => unsupported(pair),
         Rule::extern_item => unsupported(pair),
         Rule::generic_param_list => comma_delimited(ctx, arena, pair).angles().group(),
+        Rule::spaced_generic_param_list => map_to_doc(ctx, arena, pair).append(arena.space()),
         Rule::generic_param => map_to_doc(ctx, arena, pair),
         Rule::type_param => map_to_doc(ctx, arena, pair),
         Rule::const_param => unsupported(pair),
@@ -821,7 +841,7 @@ fn to_doc<'a>(
         Rule::for_type => map_to_doc(ctx, arena, pair),
         Rule::impl_trait_type => map_to_doc(ctx, arena, pair),
         Rule::dyn_trait_type => map_to_doc(ctx, arena, pair),
-        Rule::type_bound_list => unsupported(pair),
+        Rule::type_bound_list => map_to_doc(ctx, arena, pair),
         Rule::type_bound => map_to_doc(ctx, arena, pair),
 
         //************************//

src/verus.pest

@@ -187,6 +187,7 @@ lbrace_str = { "{" }
 lbracket_str = { "[" }
 lparen_str = { "(" }
 pipe_str = { "|" }
+plus_str = { "+" }
 pound_str = { "#" }
 question_str = { "?" }
 rangle_str = { ">" }
@@ -693,7 +694,7 @@ assoc_item = {
 impl = {
     attr* ~ visibility? ~
     default_str? ~ unsafe_str? ~
-    impl_str ~ generic_param_list? ~ (const_str? ~ bang_str? ~ type ~ for_str)? ~ type ~ where_clause? ~
+    impl_str ~ spaced_generic_param_list? ~ (const_str? ~ bang_str? ~ type ~ for_str)? ~ type ~ where_clause? ~
     assoc_item_list
 }
 
@@ -716,6 +717,11 @@ generic_param_list = {
     "<" ~ (generic_param ~ ("," ~ generic_param)* ~ ","?)? ~ ">"
 }
 
+// A generic_param_list that should be followed by a space
+spaced_generic_param_list = {
+    generic_param_list
+}
+
 generic_param = {
     const_param
   | lifetime_param
@@ -1244,7 +1250,7 @@ dyn_trait_type = {
 }
 
 type_bound_list = {
-    type_bound ~ ("+" ~ type_bound)* ~ "+"?
+    type_bound ~ (plus_str ~ type_bound)* ~ plus_str?
 }
 
 type_bound = {

tests/rustfmt-tests.rs

@@ -19,7 +19,7 @@ fn compare(file: &str) {
         3,
         Some(("rust", "verus")),
     );
-    assert_eq!(rust_fmt, verus_inner, "{diff}");
+    assert_eq!(rust_fmt, verus_inner, "\n{diff}");
 }
 
 #[test]

tests/snap-tests.rs

@@ -718,6 +718,51 @@ pub exec fn foo(mut_state: &mut Blah, selfie_stick: SelfieStick) {
     "###);
 }
 
+#[test]
+fn verus_impl_bounds() {
+    let file = r#"
+verus! {
+struct StrictlyOrderedVec<K: KeyTrait> {
+    a: int
+}
+
+struct DelegationMap<#[verifier(maybe_negative)] K: KeyTrait + VerusClone> {
+    b: int
+}
+
+impl<K: KeyTrait + VerusClone> DelegationMap<K> {
+    fn view() -> Map<K,AbstractEndPoint> {
+        c
+    }
+}
+
+} // verus!
+"#;
+
+    assert_snapshot!(parse_and_format(file).unwrap(), @r###"
+    verus! {
+
+    struct StrictlyOrderedVec<K: KeyTrait> {
+        a: int,
+    }
+
+    struct DelegationMap<
+        #[verifier(maybe_negative)]
+        K: KeyTrait + VerusClone,
+    > {
+        b: int,
+    }
+
+    impl<K: KeyTrait + VerusClone> DelegationMap<K> {
+        fn view() -> Map<K, AbstractEndPoint> {
+            c
+        }
+    }
+
+    } // verus!
+    "###);
+}
+
 #[test]
 fn verus_loops() {
     let file = r#"