Add support for while loops with invariants.

examples/wip.rs

@@ -1,6 +1,19 @@
 verus! {
 
-fn syntactic_eq(&self, other: &Self) {
+pub fn clone_vec_u8() {
+    let i = 0;
+    while i < v.len()
+        invariant
+            i <= v.len(),
+            i == out.len(),
+            forall |j| #![auto] 0 <= j < i  ==> out@[j] == v@[j],
+        ensures
+            i > 0,
+        decreases
+            72,
+    {
+        i = i + 1;
+    }
 }
 
 } // verus!

src/lib.rs

@@ -441,7 +441,6 @@ fn to_doc<'a>(
         | Rule::impl_str
         | Rule::in_str
         | Rule::int_str
-        | Rule::invariant_str
         | Rule::isize_str
         | Rule::let_str
         | Rule::loop_str
@@ -497,9 +496,11 @@ fn to_doc<'a>(
             .append(arena.space())
             .nest(INDENT_SPACES),
 
-        Rule::decreases_str | Rule::ensures_str | Rule::recommends_str | Rule::requires_str => {
-            arena.hardline().append(s).nest(INDENT_SPACES)
-        }
+        Rule::decreases_str
+        | Rule::ensures_str
+        | Rule::invariant_str
+        | Rule::recommends_str
+        | Rule::requires_str => arena.hardline().append(s).nest(INDENT_SPACES),
 
         Rule::assert_str
         | Rule::assume_str
@@ -585,7 +586,12 @@ fn to_doc<'a>(
                             saw_comment_after_param_list = true;
                         };
                         // Special case where we don't want an extra newline after the possibly inline comment
-                        comment_to_doc(ctx, arena, p, !has_qualifier || !saw_comment_after_param_list)
+                        comment_to_doc(
+                            ctx,
+                            arena,
+                            p,
+                            !has_qualifier || !saw_comment_after_param_list,
+                        )
                     }
                     Rule::param_list => {
                         saw_param_list = true;
@@ -742,7 +748,28 @@ fn to_doc<'a>(
         Rule::if_expr => map_to_doc(ctx, arena, pair),
         Rule::loop_expr => unsupported(pair),
         Rule::for_expr => unsupported(pair),
-        Rule::while_expr => map_to_doc(ctx, arena, pair),
+        Rule::while_expr => {
+            // We need to add a newline after the very last clause,
+            // so that the opening brace of the loop body is on a fresh line
+            let mut last_clause = None;
+            pair.clone().into_inner().for_each(|p| match p.as_rule() {
+                Rule::invariant_clause => last_clause = Some(Rule::invariant_clause),
+                Rule::ensures_clause => last_clause = Some(Rule::ensures_clause),
+                Rule::decreases_clause => last_clause = Some(Rule::decreases_clause),
+                _ => (),
+            });
+            arena.concat(pair.into_inner().map(|p| {
+                if let Some(c) = last_clause {
+                    if p.as_rule() == c {
+                        to_doc(ctx, p, arena).append(arena.line())
+                    } else {
+                        to_doc(ctx, p, arena)
+                    }
+                } else {
+                    to_doc(ctx, p, arena)
+                }
+            }))
+        }
         Rule::label => unsupported(pair),
         Rule::break_expr => map_to_doc(ctx, arena, pair),
         Rule::continue_expr => map_to_doc(ctx, arena, pair),
@@ -839,7 +866,7 @@ fn to_doc<'a>(
         Rule::verus_clause_non_expr => map_to_doc(ctx, arena, pair),
         Rule::requires_clause => map_to_doc(ctx, arena, pair),
         Rule::ensures_clause => map_to_doc(ctx, arena, pair),
-        Rule::invariant_clause => unsupported(pair),
+        Rule::invariant_clause => map_to_doc(ctx, arena, pair),
         Rule::recommends_clause => map_to_doc(ctx, arena, pair),
         Rule::decreases_clause => map_to_doc(ctx, arena, pair),
         Rule::assert_requires => map_to_doc(ctx, arena, pair).append(arena.line()),

tests/rustfmt-tests.rs

@@ -368,6 +368,4 @@ let (temp_owl__x607, Tracked(itree)): ( _
 }
 "#;
     compare(file);
-
 }
-

tests/snap-tests.rs

@@ -696,7 +696,7 @@ pub exec fn foo()
 }
 
 #[test]
-fn keyword_prefixed_identifier_parsing() {
+fn verus_keyword_prefixed_identifier_parsing() {
     let file = r#"
 verus! {
 pub exec fn foo(mut_state: &mut Blah, selfie_stick: SelfieStick) {
@@ -717,3 +717,49 @@ pub exec fn foo(mut_state: &mut Blah, selfie_stick: SelfieStick) {
     } // verus!
     "###);
 }
+
+#[test]
+fn verus_loops() {
+    let file = r#"
+verus! {
+
+pub fn clone_vec_u8() {
+    let i = 0;
+    while i < v.len()
+        invariant
+            i <= v.len(),
+            i == out.len(),
+            forall |j| #![auto] 0 <= j < i  ==> out@[j] == v@[j],
+        ensures
+            i > 0,
+        decreases
+            72,
+    {
+        i = i + 1;
+    }
+}
+
+} // verus!
+"#;
+
+    assert_snapshot!(parse_and_format(file).unwrap(), @r###"
+    verus! {
+
+    pub fn clone_vec_u8() {
+        let i = 0;
+        while i < v.len() 
+            invariant
+                i <= v.len(),
+                i == out.len(),
+                forall|j| #![auto] 0 <= j < i ==> out@[j] == v@[j],
+            ensures
+                i > 0,
+            decreases 72,
+        {
+            i = i + 1;
+        }
+    }
+
+    } // verus!
+    "###);
+}