diff --git a/examples/wip.rs b/examples/wip.rs index fadcf8e..abf7b73 100644 --- a/examples/wip.rs +++ b/examples/wip.rs @@ -1,6 +1,20 @@ verus! { -fn syntactic_eq(&self, other: &Self) { +struct StrictlyOrderedVec { + a: int, +} + +struct DelegationMap< + #[verifier(maybe_negative)] + K: KeyTrait + VerusClone, +> { + b: int, +} + +impl DelegationMap { + fn view() -> Map { + c + } } } // verus! diff --git a/src/lib.rs b/src/lib.rs index b9ef63c..d67e168 100644 --- a/src/lib.rs +++ b/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()), diff --git a/src/verus.pest b/src/verus.pest index 9e2ad61..49ba5db 100644 --- a/src/verus.pest +++ b/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 = { diff --git a/tests/rustfmt-tests.rs b/tests/rustfmt-tests.rs index 0978a92..ace6673 100644 --- a/tests/rustfmt-tests.rs +++ b/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); - } - diff --git a/tests/snap-tests.rs b/tests/snap-tests.rs index 05fae25..1b346ed 100644 --- a/tests/snap-tests.rs +++ b/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 { + a: int +} + +struct DelegationMap<#[verifier(maybe_negative)] K: KeyTrait + VerusClone> { + b: int +} + +impl DelegationMap { + fn view() -> Map { + c + } +} + +} // verus! +"#; + + assert_snapshot!(parse_and_format(file).unwrap(), @r###" + verus! { + + struct StrictlyOrderedVec { + a: int, + } + + struct DelegationMap< + #[verifier(maybe_negative)] + K: KeyTrait + VerusClone, + > { + b: int, + } + + impl DelegationMap { + fn view() -> Map { + 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! + "###); +}