Add more nuance for prefix_expr w.r.t. when it can/cannot have structs

examples/wip.rs

@@ -1,12 +1,7 @@
 verus! {
 
-fn has_new_pointsto() {
-    (forall |addr: int| mem_protect == MemProtect { read: true })
-}
-
-fn foo()
-    ensures forall|x:int| x == x
-{
+fn local_direct_update(loc1: Local, loc2: Local, i: int, j: int, pq: int) -> bool {
+    &&& loc2 == Local { heap: loc2.heap, ..loc1 }
 }
 
 } // verus!

src/lib.rs

@@ -388,7 +388,7 @@ fn is_prefix_triple(pair: Pair<Rule>) -> bool {
     match pair.into_inner().find(|p| matches!(p.as_rule(), Rule::expr_inner)) {
         None => false,
         Some(pair) => 
-            match pair.into_inner().find(|p| matches!(p.as_rule(), Rule::prefix_expr)) {
+            match pair.into_inner().find(|p| matches!(p.as_rule(), Rule::prefix_expr) || matches!(p.as_rule(), Rule::prefix_expr_no_struct)) {
                 None => false,
                 Some(pair) => 
                     pair.into_inner().find(|p| matches!(p.as_rule(), Rule::triple_and) || matches!(p.as_rule(), Rule::triple_or)).is_some(),
@@ -841,6 +841,7 @@ fn to_doc<'a>(
             block_braces(arena, mapped, terminal_expr(&pairs))
         }
         Rule::prefix_expr => map_to_doc(ctx, arena, pair),
+        Rule::prefix_expr_no_struct => map_to_doc(ctx, arena, pair),
         Rule::assignment_ops => docs![arena, arena.space(), s, arena.line()],
         Rule::bin_expr_ops_special => arena.hardline().append(map_to_doc(ctx, arena, pair)),
         Rule::bin_expr_ops_normal => docs![arena, arena.line(), s, arena.space()]

src/verus.pest

@@ -873,7 +873,7 @@ expr_inner_no_struct = _{
   | block_expr
   | box_expr
   | break_expr
-  | prefix_expr
+  | prefix_expr_no_struct
   | closure_expr
   | quantifier_expr_no_struct
   | continue_expr
@@ -969,6 +969,7 @@ expr_inner = {
     if_expr  // Must precede struct_expr or struct_expr thinks `if {}` is a struct
   | struct_expr // Must precede expr_inner_no_struct or `my_struct { }` will be `my_struct`: path_expr
   | quantifier_expr
+  | prefix_expr
   | expr_inner_no_struct
 }
 
@@ -1036,6 +1037,10 @@ fn_block_expr = {
 }
 
 prefix_expr = {
+    attr* ~ (dash_str | bang_str | star_str | triple_or | triple_and) ~ expr
+}
+
+prefix_expr_no_struct = {
     attr* ~ (dash_str | bang_str | star_str | triple_or | triple_and) ~ expr_no_struct
 }
 

tests/verus-consistency.rs

@@ -471,6 +471,9 @@ spec fn host_ignoring_unparseable(pre: AbstractHostState, post: AbstractHostStat
     post == AbstractHostState { received_packet: None, ..pre }
 }
 
+fn local_direct_update(loc1: Local, pq: int) -> bool {
+    &&& loc2 == Local { heap: loc2.heap, ..loc1 }
+}
 
 } // verus!
 "#;
@@ -482,6 +485,10 @@ spec fn host_ignoring_unparseable(pre: AbstractHostState, post: AbstractHostStat
         post == AbstractHostState { received_packet: None, ..pre }
     }
 
+    fn local_direct_update(loc1: Local, pq: int) -> bool {
+        &&& loc2 == Local { heap: loc2.heap, ..loc1 }
+    }
+
     } // verus!
     "###);
 }