Support the macro_pat parsing object (#101)

This PR adds support for the `macro_pat` capture during patterns matches.
verus-lang · Oct 7, 2024 · 90130f5 · 90130f5
2 parents 27fe344 + 6c4dcba
commit 90130f5
Show file tree

Hide file tree

Showing 2 changed files with 16 additions and 2 deletions.
diff --git a/src/lib.rs b/src/lib.rs
@@ -1315,7 +1315,7 @@ fn to_doc<'a>(
         Rule::path_pat => map_to_doc(ctx, arena, pair),
         Rule::box_pat => map_to_doc(ctx, arena, pair),
         Rule::rest_pat => map_to_doc(ctx, arena, pair),
-        Rule::macro_pat => unsupported(pair),
+        Rule::macro_pat => map_to_doc(ctx, arena, pair),
         Rule::const_block_pat => unsupported(pair),
 
         //************************//

diff --git a/tests/verus-consistency.rs b/tests/verus-consistency.rs
@@ -484,7 +484,13 @@ verus!{
         cong;
         done;
     ");
-
+    fn foo(x: usize) {
+        match x {
+            inj_ord_choice_pat!((_,x), *, *) => (),
+            inj_ord_choice_pat!(*, (_,x), *) => (),
+            inj_ord_choice_pat!(*, *, _) => (),
+        };
+    }
 }
 "#;
 
@@ -505,6 +511,14 @@ verus!{
             cong;
             done;
         ");
+    
+    fn foo(x: usize) {
+        match x {
+            inj_ord_choice_pat!((_,x), *, *) => (),
+            inj_ord_choice_pat!(*, (_,x), *) => (),
+            inj_ord_choice_pat!(*, *, _) => (),
+        };
+    }
 
     } // verus!
     "###);