Add support for !is/!has syntax (#117)

See verus-lang/verus#1435

CHANGELOG.md

@@ -1,5 +1,7 @@
 # Unreleased
 
+* Add support for `!is`/`!has` syntax (see [verus#1435](https://github.com/verus-lang/verus/pull/1435))
+
 # v0.5.2
 
 * Fix parser for `assume_specification` to improve support

src/lib.rs

@@ -657,6 +657,7 @@ fn to_doc<'a>(
         | Rule::arrow_expr_str => s,
         Rule::fn_traits | Rule::impl_str => s,
         Rule::calc_str | Rule::seq_str => s,
+        Rule::has_str | Rule::is_str => s,
         Rule::pipe_str => docs!(arena, arena.line(), s, arena.space()),
         //        Rule::triple_and |
         //        Rule::triple_or =>
@@ -755,9 +756,8 @@ fn to_doc<'a>(
 
         Rule::as_str
         | Rule::by_str_inline
-        | Rule::has_str
         | Rule::implies_str
-        | Rule::is_str
+        | Rule::spaced_is_str
         | Rule::matches_str => arena.space().append(s).append(arena.space()),
 
         Rule::by_str | Rule::via_str | Rule::when_str => arena
@@ -1091,6 +1091,10 @@ fn to_doc<'a>(
         Rule::expr_inner_no_struct => map_to_doc(ctx, arena, pair),
         Rule::expr_with_block => map_to_doc(ctx, arena, pair),
         Rule::expr_as => map_to_doc(ctx, arena, pair),
+        Rule::is_or_notis | Rule::has_or_nothas => arena
+            .space()
+            .append(map_to_doc(ctx, arena, pair))
+            .append(arena.space()),
         Rule::expr_has => map_to_doc(ctx, arena, pair),
         Rule::expr_is => map_to_doc(ctx, arena, pair),
         Rule::expr_matches => map_to_doc(ctx, arena, pair),

src/verus.pest

@@ -537,7 +537,7 @@ seq_macro_call = {
 macro_call = {
     calc_macro_call
   | seq_macro_call
-  | attr* ~ path ~ bang_str ~ !"=" ~ token_tree
+  | attr* ~ path ~ bang_str ~ delim_token_tree
 }
 
 // NOTE: By convention, stmt-like or item-like macros (e.g., calc!{}) tend to
@@ -613,8 +613,10 @@ global_sizeof = {
     sizeof_str ~ type ~ eq_eq_str ~ expr
 }
 
+spaced_is_str = { is_str }
+
 global_layout = {
-    layout_str ~ type ~ is_str ~ identifier ~ eq_eq_str ~ literal
+    layout_str ~ type ~ spaced_is_str ~ identifier ~ eq_eq_str ~ literal
     ~ (spaced_comma_str ~ identifier ~ eq_eq_str ~ literal)?
 }
 
@@ -1116,12 +1118,20 @@ expr_as = {
     as_str ~ type
 }
 
+has_or_nothas = {
+    bang_str? ~ has_str
+}
+
 expr_has = {
-    has_str ~ expr
+    has_or_nothas ~ expr
+}
+
+is_or_notis = {
+    bang_str? ~ is_str
 }
 
 expr_is = {
-    is_str ~ type
+    is_or_notis ~ type
 }
 
 expr_matches = {

tests/verus-consistency.rs

@@ -2780,3 +2780,42 @@ verus!{
     } // verus!
     ")
 }
+
+#[test]
+fn verus_support_is_has_notis_nothas() {
+    let file = r#"
+verus!{
+proof fn uses_spec_has(s: Set<int>)
+    requires
+        s has 3,
+        s !has 4,
+{
+}
+proof fn uses_spec_is(t: ThisOrThat)
+    requires
+        t is This,
+        t !is That
+{
+}
+}
+"#;
+    assert_snapshot!(parse_and_format(file).unwrap(), @r"
+    verus! {
+
+    proof fn uses_spec_has(s: Set<int>)
+        requires
+            s has 3,
+            s !has 4,
+    {
+    }
+
+    proof fn uses_spec_is(t: ThisOrThat)
+        requires
+            t is This,
+            t !is That,
+    {
+    }
+
+    } // verus!
+    ")
+}