Add support for arrow expressions and matches expressions (#32)

verus-lang · Feb 19, 2024 · 25d604c · 25d604c
2 parents 0a17e24 + 78d4709
commit 25d604c
Show file tree

Hide file tree

Showing 4 changed files with 101 additions and 4 deletions.
diff --git 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 {}
 

diff --git 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 |
@@ -715,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()
@@ -971,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
@@ -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,16 @@ 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 = {
+    rarrow_str
+}
+
 expr_outer = _{
     // await_expr
     dot_str ~ await_str
@@ -1021,6 +1032,10 @@ 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)
+    // matches_expr
+    | expr_matches
     // bin_expr
     | bin_expr_ops ~ expr
     // range_expr
@@ -1050,6 +1065,10 @@ 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)
+    // 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
@@ -1602,3 +1602,60 @@ 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!
+    "###);
+}
+
+#[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!
+    "###);
+}