From 09bbd6d2a20861b53f00ff77bc63712583a84571 Mon Sep 17 00:00:00 2001
From: Bryan Parno <parno@cmu.edu>
Date: Wed, 15 Nov 2023 12:34:41 -0500
Subject: [PATCH] Fix spacing around lifetimes

---
 examples/wip.rs     |  3 +--
 src/lib.rs          |  4 +++-
 src/verus.pest      | 11 ++++++-----
 tests/snap-tests.rs |  2 +-
 4 files changed, 11 insertions(+), 9 deletions(-)

diff --git a/examples/wip.rs b/examples/wip.rs
index 85c7230..e12dd7c 100644
--- a/examples/wip.rs
+++ b/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!
diff --git a/src/lib.rs b/src/lib.rs
index 58830cb..bee4694 100644
--- a/src/lib.rs
+++ b/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),
diff --git a/src/verus.pest b/src/verus.pest
index 49ba5db..a294907 100644
--- a/src/verus.pest
+++ b/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,7 +740,7 @@ const_param = {
 }
 
 lifetime_param = {
-    attr* ~ lifetime ~ (colon_str ~ type_bound_list)?
+    attr* ~ lifetime_no_space ~ (colon_str ~ type_bound_list)?
 }
 
 where_clause = {
@@ -747,7 +748,7 @@ where_clause = {
 }
 
 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
 }
 
diff --git a/tests/snap-tests.rs b/tests/snap-tests.rs
index 2554058..1a1b5f3 100644
--- a/tests/snap-tests.rs
+++ b/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
     }