From b808b5a754bd0743a6a81756d827dfed8e449569 Mon Sep 17 00:00:00 2001 From: Jay Bosamiya Date: Mon, 19 Feb 2024 12:28:32 -0500 Subject: [PATCH 1/3] Add support for arrow expressions --- src/lib.rs | 3 ++- src/verus.pest | 10 ++++++++++ tests/verus-consistency.rs | 29 +++++++++++++++++++++++++++++ 3 files changed, 41 insertions(+), 1 deletion(-) diff --git a/src/lib.rs b/src/lib.rs index 2462fb1..8df26b9 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -620,7 +620,8 @@ fn to_doc<'a>( | Rule::semi_str | Rule::star_str | Rule::tilde_str - | Rule::underscore_str => s, + | Rule::underscore_str + | Rule::arrow_expr_str => s, Rule::fn_traits | Rule::impl_str => s, Rule::pipe_str => docs!(arena, arena.line(), s, arena.space()), // Rule::triple_and | diff --git a/src/verus.pest b/src/verus.pest index 0bab838..fb4b1fd 100644 --- a/src/verus.pest +++ b/src/verus.pest @@ -998,6 +998,12 @@ expr_is = { is_str ~ type } +// Separate rule for `->` (rarrow_str) because rarrow_str is normally used for +// functions, and that introduces spaces before and after. +arrow_expr_str = { + rarrow_str +} + expr_outer = _{ // await_expr dot_str ~ await_str @@ -1021,6 +1027,8 @@ expr_outer = _{ | dot_str ~ name_ref ~ generic_arg_list? ~ arg_list // field_expr | dot_str ~ name_ref + // arrow_expr + | arrow_expr_str ~ (int_number | name_ref) // bin_expr | bin_expr_ops ~ expr // range_expr @@ -1050,6 +1058,8 @@ expr_outer_no_struct = _{ | dot_str ~ name_ref ~ generic_arg_list? ~ arg_list // field_expr | dot_str ~ name_ref + // arrow_expr + | arrow_expr_str ~ (int_number | name_ref) // bin_expr | bin_expr_ops ~ expr_no_struct // range_expr diff --git a/tests/verus-consistency.rs b/tests/verus-consistency.rs index 3cf265e..c4a7334 100644 --- a/tests/verus-consistency.rs +++ b/tests/verus-consistency.rs @@ -1602,3 +1602,32 @@ fn baz() { } // verus! "###); } + +#[test] +fn verus_arrow_expr() { + let file = r#" +verus! { + +proof fn uses_arrow_matches_1(t: ThisOrThat) + requires + t is That ==> t->v == 3, + t is This ==> t->0 == 4, +{ +} + +} + +"#; + assert_snapshot!(parse_and_format(file).unwrap(), @r###" + verus! { + + proof fn uses_arrow_matches_1(t: ThisOrThat) + requires + t is That ==> t->v == 3, + t is This ==> t->0 == 4, + { + } + + } // verus! + "###); +} From 11e6b896961f4c30085e21335b82109da5a4f45a Mon Sep 17 00:00:00 2001 From: Jay Bosamiya Date: Mon, 19 Feb 2024 12:40:18 -0500 Subject: [PATCH 2/3] Add matches expression support --- src/lib.rs | 10 +++++++--- src/verus.pest | 9 +++++++++ tests/verus-consistency.rs | 28 ++++++++++++++++++++++++++++ 3 files changed, 44 insertions(+), 3 deletions(-) diff --git a/src/lib.rs b/src/lib.rs index 8df26b9..f108f20 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -716,9 +716,12 @@ fn to_doc<'a>( | Rule::yeet_str | Rule::yield_str => s.append(arena.space()), - Rule::as_str | Rule::by_str_inline | Rule::has_str | Rule::implies_str | Rule::is_str => { - arena.space().append(s).append(arena.space()) - } + Rule::as_str + | Rule::by_str_inline + | Rule::has_str + | Rule::implies_str + | Rule::is_str + | Rule::matches_str => arena.space().append(s).append(arena.space()), Rule::by_str | Rule::via_str | Rule::when_str => arena .line() @@ -972,6 +975,7 @@ fn to_doc<'a>( Rule::expr_as => map_to_doc(ctx, arena, pair), Rule::expr_has => map_to_doc(ctx, arena, pair), Rule::expr_is => map_to_doc(ctx, arena, pair), + Rule::expr_matches => map_to_doc(ctx, arena, pair), Rule::expr_outer => map_to_doc(ctx, arena, pair), Rule::expr_outer_no_struct => map_to_doc(ctx, arena, pair), Rule::expr_no_struct => map_to_doc(ctx, arena, pair), diff --git a/src/verus.pest b/src/verus.pest index fb4b1fd..10f0064 100644 --- a/src/verus.pest +++ b/src/verus.pest @@ -287,6 +287,7 @@ loop_str = ${ "loop" ~ !("_" | ASCII_ALPHANUMERIC) } macro_str = ${ "macro" ~ !("_" | ASCII_ALPHANUMERIC) } macro_rules_str = ${ "macro_rules" ~ !("_" | ASCII_ALPHANUMERIC) } match_str = ${ "match" ~ !("_" | ASCII_ALPHANUMERIC) } +matches_str = ${ "matches" ~ !("_" | ASCII_ALPHANUMERIC) } mod_str = ${ "mod" ~ !("_" | ASCII_ALPHANUMERIC) } move_str = ${ "move" ~ !("_" | ASCII_ALPHANUMERIC) } mut_str = ${ "mut" ~ !("_" | ASCII_ALPHANUMERIC) } @@ -998,6 +999,10 @@ expr_is = { is_str ~ type } +expr_matches = { + matches_str ~ pat +} + // Separate rule for `->` (rarrow_str) because rarrow_str is normally used for // functions, and that introduces spaces before and after. arrow_expr_str = { @@ -1029,6 +1034,8 @@ expr_outer = _{ | dot_str ~ name_ref // arrow_expr | arrow_expr_str ~ (int_number | name_ref) + // matches_expr + | expr_matches // bin_expr | bin_expr_ops ~ expr // range_expr @@ -1060,6 +1067,8 @@ expr_outer_no_struct = _{ | dot_str ~ name_ref // arrow_expr | arrow_expr_str ~ (int_number | name_ref) + // matches_expr + | expr_matches // bin_expr | bin_expr_ops ~ expr_no_struct // range_expr diff --git a/tests/verus-consistency.rs b/tests/verus-consistency.rs index c4a7334..70e7a49 100644 --- a/tests/verus-consistency.rs +++ b/tests/verus-consistency.rs @@ -1631,3 +1631,31 @@ proof fn uses_arrow_matches_1(t: ThisOrThat) } // verus! "###); } + +#[test] +fn verus_matches_expr() { + let file = r#" +verus! { + +proof fn uses_arrow_matches_1(t: ThisOrThat) { assert(t matches ThisOrThat::This(k) ==> k == 4); + assert(t matches ThisOrThat::That { v } ==> v == 3); assert({ &&& t matches ThisOrThat::This(k) + &&& baz }); } + +} + +"#; + assert_snapshot!(parse_and_format(file).unwrap(), @r###" + verus! { + + proof fn uses_arrow_matches_1(t: ThisOrThat) { + assert(t matches ThisOrThat::This(k) ==> k == 4); + assert(t matches ThisOrThat::That { v } ==> v == 3); + assert({ + &&& t matches ThisOrThat::This(k) + &&& baz + }); + } + + } // verus! + "###); +} From 78d4709cb3d686c4befb8c153443bf9f7a5c60d7 Mon Sep 17 00:00:00 2001 From: Jay Bosamiya Date: Mon, 19 Feb 2024 12:44:55 -0500 Subject: [PATCH 3/3] Update to latest syntax.rs --- examples/syntax.rs | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/examples/syntax.rs b/examples/syntax.rs index 038a7ef..e7bbd68 100644 --- a/examples/syntax.rs +++ b/examples/syntax.rs @@ -560,6 +560,22 @@ proof fn uses_is(t: ThisOrThat) { } } +proof fn uses_arrow_matches_1(t: ThisOrThat) + requires + t is That ==> t->v == 3, + t is This ==> t->0 == 4, +{ + assert(t matches ThisOrThat::This(k) ==> k == 4); + assert(t matches ThisOrThat::That { v } ==> v == 3); +} + +proof fn uses_arrow_matches_2(t: ThisOrThat) + requires + t matches ThisOrThat::That { v: a } && a == 3, +{ + assert(t is That && t->v == 3); +} + #[verifier::external_body] struct Collection {}