Fix some issues with lifetimes (#16)

This builds on #14

examples/wip.rs

@@ -1,20 +1,7 @@
 verus! {
 
-struct StrictlyOrderedVec<K: KeyTrait> {
-    a: int,
-}
-
-struct DelegationMap<
-    #[verifier(maybe_negative)]
-    K: KeyTrait + VerusClone,
-> {
-    b: int,
-}
-
-impl<K: KeyTrait + VerusClone> DelegationMap<K> {
-    fn view() -> Map<K, AbstractEndPoint> {
-        c
-    }
+fn get<'a>(&'a self, k: &K) -> (o: Option<&'a V>) {
+    a
 }
 
 } // verus!

src/lib.rs

@@ -553,7 +553,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),
@@ -702,7 +704,7 @@ fn to_doc<'a>(
         Rule::generic_param => map_to_doc(ctx, arena, pair),
         Rule::type_param => map_to_doc(ctx, arena, pair),
         Rule::const_param => unsupported(pair),
-        Rule::lifetime_param => unsupported(pair),
+        Rule::lifetime_param => map_to_doc(ctx, arena, pair),
         Rule::where_clause => unsupported(pair),
         Rule::where_pred => unsupported(pair),
         Rule::visibility => s.append(arena.space()),

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

@@ -833,3 +833,26 @@ pub fn clone_vec_u8() {
     } // verus!
     "###);
 }
+
+#[test]
+fn verus_lifetimes() {
+    let file = r#"
+verus! {
+
+fn get<'a>(&'a self, k: &K) -> (o: Option<&'a V>) {
+    a
+}
+
+} // verus!
+"#;
+
+    assert_snapshot!(parse_and_format(file).unwrap(), @r###"
+    verus! {
+
+    fn get<'a>(&'a self, k: &K) -> (o: Option<&'a V>) {
+        a
+    }
+
+    } // verus!
+    "###);
+}