Fix spacing around lifetimes

examples/wip.rs

@@ -1,8 +1,7 @@
 verus! {
 
-fn get<'a>(&'a self) -> (o: Option<&'a V>) {
+fn get<'a>(&'a self, k: &K) -> (o: Option<&'a V>) {
     a
 }
 
-
 } // verus!

src/lib.rs

@@ -517,7 +517,9 @@ fn to_doc<'a>(
         //*************************//
         // Names, Paths and Macros //
         //*************************//
-        Rule::name | Rule::name_ref | Rule::lifetime => s,
+        Rule::name | Rule::name_ref => s,
+        Rule::lifetime => s.append(arena.space()),
+        Rule::lifetime_no_space => s,
         Rule::path => map_to_doc(ctx, arena, pair),
         Rule::path_segment => map_to_doc(ctx, arena, pair),
         Rule::generic_arg_list => map_to_doc(ctx, arena, pair),

src/verus.pest

@@ -366,6 +366,7 @@ name = { identifier | self_str }
 name_ref = { identifier | self_str | super_str | crate_str | Self_str }
 
 lifetime = { lifetime_ident }
+lifetime_no_space = { lifetime }  // A lifetime that shouldn't be followed by a space
 
 path = { (path_segment ~ colons_str)* ~ path_segment }
 
@@ -402,7 +403,7 @@ assoc_type_arg = {
 }
 
 lifetime_arg = {
-    lifetime
+    lifetime_no_space
 }
 
 const_arg = {
@@ -739,15 +740,15 @@ const_param = {
 }
 
 lifetime_param = {
-    attr* ~ lifetime ~ (colon_str ~ type_bound_list)?
+    attr* ~ lifetime_no_space ~ (colon_str ~ type_bound_list)?
 }
 
 where_clause = {
     where_str ~ (where_pred ~ ("," ~ where_pred)* ~ ","?)?
 }
 
 where_pred = {
-    (for_str ~ generic_param_list)? ~ (lifetime | type) ~ colon_str ~ type_bound_list?
+    (for_str ~ generic_param_list)? ~ (lifetime_no_space | type) ~ colon_str ~ type_bound_list?
 }
 
 visibility = {
@@ -1102,7 +1103,7 @@ while_expr = {
 }
 
 label = {
-    lifetime ~ colon_str
+    lifetime_no_space ~ colon_str
 }
 
 break_expr = {
@@ -1254,7 +1255,7 @@ type_bound_list = {
 }
 
 type_bound = {
-    lifetime
+    lifetime_no_space
   | ("?" | "~" ~ const_str)? ~ type
 }
 

tests/snap-tests.rs

@@ -824,7 +824,7 @@ fn get<'a>(&'a self, k: &K) -> (o: Option<&'a V>) {
     assert_snapshot!(parse_and_format(file).unwrap(), @r###"
     verus! {
 
-    fn get<'a>(&'aself, k: &K) -> (o: Option<&'aV>) {
+    fn get<'a>(&'a self, k: &K) -> (o: Option<&'a V>) {
         a
     }