Support parsing for const generic literals (#92)

Fixes #90

CHANGELOG.md

@@ -2,6 +2,7 @@
 
 * Improved handling of comments around clauses/stanzas
   - Each comment now maintains loyalty to the clause the user picked it to stay with, rather than automatically migrating to the previous clause in the presence of `assert ... by { ... }`-style constructs
+* Support parsing for const generic literals
 
 # v0.4.1
 

src/verus.pest

@@ -485,7 +485,13 @@ lifetime_arg = {
 }
 
 const_arg = {
-    expr
+    // Currently stable Rust only support literals as const args inside generic
+    // args. In general, it could be arbitrary expressions, but that causes
+    // headaches for parsing (in particular, we need to parse an `expr` that
+    // does _not_ have a `>` sign in it, but our `expr` parsing greedily eats
+    // any `>` that exists within it. Thus, for now, we simply restrict to
+    // literals.
+    literal
 }
 
 generic_args_binding = {

tests/verus-consistency.rs

@@ -2533,3 +2533,33 @@ pub fn foo() {
     } // verus!
     "###);
 }
+
+#[test]
+fn verus_const_generics() {
+    // Regression test for https://github.com/verus-lang/verusfmt/issues/90
+    let file = r#"
+verus! {
+       pub fn f<const N: u64>() -> u64 { N }
+       pub fn g<const N: u64, const O: u64>() -> u64 { N }
+ fn main() { f::<123>(); g::<123, 456>(); }
+}
+"#;
+    assert_snapshot!(parse_and_format(file).unwrap(), @r###"
+    verus! {
+
+    pub fn f<const N: u64>() -> u64 {
+        N
+    }
+
+    pub fn g<const N: u64, const O: u64>() -> u64 {
+        N
+    }
+
+    fn main() {
+        f::<123>();
+        g::<123, 456>();
+    }
+
+    } // verus!
+    "###);
+}