Add support for type_bound_list

examples/wip.rs

@@ -1,6 +1,20 @@
 verus! {
 
-fn syntactic_eq(&self, other: &Self) {
+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!

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,10 +439,8 @@ fn to_doc<'a>(
         | Rule::i64_str
         | Rule::i8_str
         | Rule::if_str
-        | Rule::impl_str
         | Rule::in_str
         | Rule::int_str
-        | Rule::invariant_str
         | Rule::isize_str
         | Rule::let_str
         | Rule::loop_str
@@ -497,9 +496,11 @@ fn to_doc<'a>(
             .append(arena.space())
             .nest(INDENT_SPACES),
 
-        Rule::decreases_str | Rule::ensures_str | Rule::recommends_str | Rule::requires_str => {
-            arena.hardline().append(s).nest(INDENT_SPACES)
-        }
+        Rule::decreases_str
+        | Rule::ensures_str
+        | Rule::invariant_str
+        | Rule::recommends_str
+        | Rule::requires_str => arena.hardline().append(s).nest(INDENT_SPACES),
 
         Rule::assert_str
         | Rule::assume_str
@@ -585,7 +586,12 @@ fn to_doc<'a>(
                             saw_comment_after_param_list = true;
                         };
                         // Special case where we don't want an extra newline after the possibly inline comment
-                        comment_to_doc(ctx, arena, p, !has_qualifier || !saw_comment_after_param_list)
+                        comment_to_doc(
+                            ctx,
+                            arena,
+                            p,
+                            !has_qualifier || !saw_comment_after_param_list,
+                        )
                     }
                     Rule::param_list => {
                         saw_param_list = true;
@@ -632,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),
@@ -742,7 +768,28 @@ fn to_doc<'a>(
         Rule::if_expr => map_to_doc(ctx, arena, pair),
         Rule::loop_expr => unsupported(pair),
         Rule::for_expr => unsupported(pair),
-        Rule::while_expr => map_to_doc(ctx, arena, pair),
+        Rule::while_expr => {
+            // We need to add a newline after the very last clause,
+            // so that the opening brace of the loop body is on a fresh line
+            let mut last_clause = None;
+            pair.clone().into_inner().for_each(|p| match p.as_rule() {
+                Rule::invariant_clause => last_clause = Some(Rule::invariant_clause),
+                Rule::ensures_clause => last_clause = Some(Rule::ensures_clause),
+                Rule::decreases_clause => last_clause = Some(Rule::decreases_clause),
+                _ => (),
+            });
+            arena.concat(pair.into_inner().map(|p| {
+                if let Some(c) = last_clause {
+                    if p.as_rule() == c {
+                        to_doc(ctx, p, arena).append(arena.line())
+                    } else {
+                        to_doc(ctx, p, arena)
+                    }
+                } else {
+                    to_doc(ctx, p, arena)
+                }
+            }))
+        }
         Rule::label => unsupported(pair),
         Rule::break_expr => map_to_doc(ctx, arena, pair),
         Rule::continue_expr => map_to_doc(ctx, arena, pair),
@@ -794,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),
 
         //************************//
@@ -839,7 +886,7 @@ fn to_doc<'a>(
         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),
-        Rule::invariant_clause => unsupported(pair),
+        Rule::invariant_clause => map_to_doc(ctx, arena, pair),
         Rule::recommends_clause => map_to_doc(ctx, arena, pair),
         Rule::decreases_clause => map_to_doc(ctx, arena, pair),
         Rule::assert_requires => map_to_doc(ctx, arena, pair).append(arena.line()),

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]
@@ -368,6 +368,4 @@ let (temp_owl__x607, Tracked(itree)): ( _
 }
 "#;
     compare(file);
-
 }
-

tests/snap-tests.rs

@@ -696,7 +696,7 @@ pub exec fn foo()
 }
 
 #[test]
-fn keyword_prefixed_identifier_parsing() {
+fn verus_keyword_prefixed_identifier_parsing() {
     let file = r#"
 verus! {
 pub exec fn foo(mut_state: &mut Blah, selfie_stick: SelfieStick) {
@@ -717,3 +717,94 @@ pub exec fn foo(mut_state: &mut Blah, selfie_stick: SelfieStick) {
     } // verus!
     "###);
 }
+
+#[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#"
+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;
+    }
+}
+
+} // verus!
+"#;
+
+    assert_snapshot!(parse_and_format(file).unwrap(), @r###"
+    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;
+        }
+    }
+
+    } // verus!
+    "###);
+}