For loop fixes (#41)

* Adds support for `for` loops with invariants, recently added to Verus
* Improve parsing of range expressions (e.g., `0..(1 + 2)`) that start "float-like"

CHANGELOG.md

@@ -1,5 +1,8 @@
 # Unreleased
 
+* Add support for `for` loops with invariants, recently added to Verus
+* Improve parsing of range expressions (e.g., `0..(1 + 2)`) that start "float-like"
+
 # v0.2.7
 
 * Improve `verus!{ ... }` macro collapsing inside indented contexts (#39)

src/lib.rs

@@ -476,6 +476,11 @@ fn loop_to_doc<'a>(
     arena.concat(pair.into_inner().map(|p| {
         if p.as_rule() == Rule::condition {
             to_doc(ctx, p, arena).append(arena.space())
+        } else if p.as_rule() == Rule::in_str {
+            // Used for for-loops
+            arena.space().append(to_doc(ctx, p, arena))
+        } else if p.as_rule() == Rule::expr_no_struct {
+            to_doc(ctx, p, arena).append(arena.space())
         } else if let Some(c) = last_clause {
             if p.as_rule() == c {
                 to_doc(ctx, p, arena).append(arena.line())
@@ -1138,11 +1143,7 @@ fn to_doc<'a>(
         Rule::condition => map_to_doc(ctx, arena, pair),
         Rule::if_expr => if_expr_to_doc(ctx, arena, pair),
         Rule::loop_expr => loop_to_doc(ctx, arena, pair),
-        Rule::for_expr => arena.concat(pair.into_inner().map(|p| match p.as_rule() {
-            Rule::in_str => arena.space().append(to_doc(ctx, p, arena)),
-            Rule::expr_no_struct => to_doc(ctx, p, arena).append(arena.space()),
-            _ => to_doc(ctx, p, arena),
-        })),
+        Rule::for_expr => loop_to_doc(ctx, arena, pair),
         Rule::while_expr => loop_to_doc(ctx, arena, pair),
         Rule::label => unsupported(pair),
         Rule::break_expr => map_to_doc(ctx, arena, pair),

src/verus.pest

@@ -132,7 +132,7 @@ int_number = @{
 
 float_decimal = @{
     (ASCII_DIGIT | "_")+ ~
-    "." ~
+    !".." ~ "." ~
     (ASCII_DIGIT | "_")* ~
     ("f32" | "f64")?   
 }
@@ -1285,6 +1285,7 @@ loop_expr = {
 
 for_expr = {
     attr* ~ label? ~ for_str ~ pat ~ in_str ~ expr_no_struct ~
+    invariant_clause? ~ invariant_ensures_clause? ~ ensures_clause? ~ decreases_clause? ~
     fn_block_expr
 }
 

tests/verus-consistency.rs

@@ -1675,3 +1675,82 @@ proof fn uses_arrow_matches_1(t: ThisOrThat) { assert(t matches ThisOrThat::This
     } // verus!
     "###);
 }
+
+#[test]
+fn verus_range_operator() {
+    let file = r#"
+verus! {
+
+fn foo() { for i in 0..(10 + 5) {
+
+} }
+
+}
+
+"#;
+    assert_snapshot!(parse_and_format(file).unwrap(), @r###"
+    verus! {
+
+    fn foo() {
+        for i in 0..(10 + 5) {
+        }
+    }
+
+    } // verus!
+    "###);
+}
+
+#[test]
+fn verus_for_loops() {
+    let file = r#"
+verus!{
+fn reverse(v: &mut Vec<u64>)
+    ensures
+        v.len() == old(v).len(),
+        forall|i: int| 0 <= i < old(v).len() ==> v[i] == old(v)[old(v).len() - i - 1],
+{
+    let length = v.len();
+    let ghost v1 = v@;
+    for n in 0..(length / 2)
+        invariant
+            length == v.len(),
+            forall|i: int| 0 <= i < n ==> v[i] == v1[length - i - 1],
+            forall|i: int| 0 <= i < n ==> v1[i] == v[length - i - 1],
+            forall|i: int| n <= i && i + n < length ==> #[trigger] v[i] == v1[i],
+    {
+        let x = v[n];
+        let y = v[length - 1 - n];
+        v.set(n, y);
+        v.set(length - 1 - n, x);
+    }
+}
+
+}
+"#;
+    assert_snapshot!(parse_and_format(file).unwrap(), @r###"
+    verus! {
+
+    fn reverse(v: &mut Vec<u64>)
+        ensures
+            v.len() == old(v).len(),
+            forall|i: int| 0 <= i < old(v).len() ==> v[i] == old(v)[old(v).len() - i - 1],
+    {
+        let length = v.len();
+        let ghost v1 = v@;
+        for n in 0..(length / 2)
+            invariant
+                length == v.len(),
+                forall|i: int| 0 <= i < n ==> v[i] == v1[length - i - 1],
+                forall|i: int| 0 <= i < n ==> v1[i] == v[length - i - 1],
+                forall|i: int| n <= i && i + n < length ==> #[trigger] v[i] == v1[i],
+        {
+            let x = v[n];
+            let y = v[length - 1 - n];
+            v.set(n, y);
+            v.set(length - 1 - n, x);
+        }
+    }
+
+    } // verus!
+    "###);
+}