Skip to content

Commit

Permalink
Parse generic-confusables in Verus clauses (#21)
Browse files Browse the repository at this point in the history
Fixes #19 

This passes all the current tests, and I _believe_ it should not
negatively impact any of the tests outside this repo either (I tested on
one large example project and it left the entirety unchanged)
  • Loading branch information
parno authored Dec 29, 2023
2 parents 592b644 + a1da3d8 commit b9af6df
Show file tree
Hide file tree
Showing 3 changed files with 58 additions and 1 deletion.
4 changes: 4 additions & 0 deletions src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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),
Expand Down Expand Up @@ -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();
Expand Down
27 changes: 26 additions & 1 deletion src/verus.pest
Original file line number Diff line number Diff line change
Expand Up @@ -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)* ~ ","?
}
Expand All @@ -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
Expand Down Expand Up @@ -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"
}

Expand Down Expand Up @@ -976,6 +996,7 @@ expr_inner = {
| quantifier_expr
| prefix_expr
| expr_inner_no_struct
| path_expr
}

expr_with_block = {
Expand Down Expand Up @@ -1012,6 +1033,10 @@ path_expr = {
attr* ~ path
}

path_expr_no_generics = {
attr* ~ path_no_generics
}

stmt_list = {
"{" ~
attr* ~
Expand Down
28 changes: 28 additions & 0 deletions tests/verus-consistency.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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!
"###);
}

0 comments on commit b9af6df

Please sign in to comment.