Add !is/!has syntax as shorthand for negated is/has

dependencies/prettyplease/src/expr.rs

@@ -83,6 +83,7 @@ impl Printer {
                 self.expr_big_op(&expr.exprs.iter().map(|e| &e.expr).collect(), true)
             }
             Expr::Is(expr) => self.expr_is(expr),
+            Expr::IsNot(expr) => self.expr_isnot(expr),
             Expr::Has(expr) => self.expr_has(expr),
             Expr::GetField(expr) => self.expr_get_field(expr),
             Expr::Matches(m) => self.expr_matches(m),
@@ -120,6 +121,13 @@ impl Printer {
         self.ident(&expr.variant_ident);
     }
 
+    pub fn expr_isnot(&mut self, expr: &syn_verus::ExprIsNot) {
+        self.outer_attrs(&expr.attrs);
+        self.expr(&expr.base, FixupContext::NONE);
+        self.word(" !is ");
+        self.ident(&expr.variant_ident);
+    }
+
     pub fn expr_has(&mut self, expr: &syn_verus::ExprHas) {
         self.outer_attrs(&expr.attrs);
         self.expr(&expr.lhs, FixupContext::NONE);

dependencies/syn/src/classify.rs

@@ -44,6 +44,7 @@ pub(crate) fn requires_comma_to_be_match_arm(expr: &Expr) -> bool {
         | Expr::BigOr(_)
         | Expr::Has(_)
         | Expr::Is(_)
+        | Expr::IsNot(_)
         | Expr::Matches(_) => true,
         Expr::Unary(e) if matches!(e.op, crate::op::UnOp::Proof(_)) => false,
 
@@ -205,6 +206,7 @@ pub(crate) fn expr_leading_label(mut expr: &Expr) -> bool {
             | Expr::BigOr(_)
             | Expr::Has(_)
             | Expr::Is(_)
+            | Expr::IsNot(_)
             | Expr::Matches(_) => return false,
         }
     }
@@ -283,6 +285,7 @@ pub(crate) fn expr_trailing_brace(mut expr: &Expr) -> bool {
             Expr::BigOr(e) => expr = &e.exprs.last().unwrap().expr,
             Expr::Has(e) => expr = &e.rhs,
             Expr::Is(_) => return false,
+            Expr::IsNot(_) => return false,
             Expr::Matches(e) => match &e.op_expr {
                 Some(op_expr) => expr = &op_expr.rhs,
                 None => return pat_trailing_brace(&e.pat),

dependencies/syn/src/expr.rs

@@ -25,7 +25,8 @@ use crate::ty::ReturnType;
 use crate::ty::Type;
 use crate::verus::{
     Assert, AssertForall, Assume, BigAnd, BigOr, Decreases, Ensures, ExprGetField, ExprHas, ExprIs,
-    ExprMatches, Invariant, InvariantEnsures, InvariantExceptBreak, Requires, RevealHide, View,
+    ExprIsNot, ExprMatches, Invariant, InvariantEnsures, InvariantExceptBreak, Requires,
+    RevealHide, View,
 };
 use proc_macro2::{Span, TokenStream};
 #[cfg(feature = "printing")]
@@ -259,6 +260,7 @@ ast_enum_of_structs! {
         BigAnd(BigAnd),
         BigOr(BigOr),
         Is(ExprIs),
+        IsNot(ExprIsNot),
         Has(ExprHas),
         Matches(ExprMatches),
         GetField(ExprGetField),
@@ -1002,6 +1004,7 @@ impl Expr {
             | Expr::RevealHide(RevealHide { attrs, .. })
             | Expr::View(View { attrs, .. })
             | Expr::Is(ExprIs { attrs, .. })
+            | Expr::IsNot(ExprIsNot { attrs, .. })
             | Expr::Has(ExprHas { attrs, .. })
             | Expr::GetField(ExprGetField { attrs, .. })
             | Expr::Matches(ExprMatches { attrs, .. }) => mem::replace(attrs, new),
@@ -1256,7 +1259,7 @@ pub(crate) mod parsing {
     #[cfg(feature = "full")]
     use crate::ty::ReturnType;
     use crate::verbatim;
-    use crate::verus::{Ensures, ExprGetField, ExprHas, ExprIs, Requires, View};
+    use crate::verus::{Ensures, ExprGetField, ExprHas, ExprIs, ExprIsNot, Requires, View};
     #[cfg(feature = "full")]
     use proc_macro2::TokenStream;
     use std::mem;
@@ -1471,6 +1474,15 @@ pub(crate) mod parsing {
                     is_token,
                     variant_ident,
                 });
+            } else if Precedence::HasIsMatches >= base && input.peek(Token![isnt]) {
+                let is_not_token: Token![isnt] = input.parse()?;
+                let variant_ident = input.parse()?;
+                lhs = Expr::IsNot(ExprIsNot {
+                    attrs: Vec::new(),
+                    base: Box::new(lhs),
+                    is_not_token,
+                    variant_ident,
+                });
             } else if Precedence::HasIsMatches >= base && input.peek(Token![has]) {
                 let has_token: Token![has] = input.parse()?;
                 let rhs = unary_expr(input, allow_struct)?;
@@ -1571,7 +1583,11 @@ pub(crate) mod parsing {
         if input.peek(Token![&&&]) || input.peek(Token![|||]) {
             return Precedence::Assign;
         }
-        if input.peek(Token![is]) || input.peek(Token![has]) || input.peek(Token![matches]) {
+        if input.peek(Token![is])
+            || input.peek(Token![isnt])
+            || input.peek(Token![has])
+            || input.peek(Token![matches])
+        {
             Precedence::HasIsMatches
         } else if let Ok(op) = input.fork().parse() {
             Precedence::of_binop(&op)
@@ -1662,7 +1678,10 @@ pub(crate) mod parsing {
                     expr,
                 }))
             }
-        } else if input.peek(Token![*]) || input.peek(Token![!]) || input.peek(Token![-]) {
+        } else if input.peek(Token![*])
+            || input.peek(Token![-])
+            || (input.peek(Token![!]) && !input.peek2(Token![is]))
+        {
             expr_unary(input, attrs, allow_struct).map(Expr::Unary)
         } else if input.peek(Token![proof]) && input.peek2(token::Brace) {
             expr_unary(input, attrs, allow_struct).map(Expr::Unary)
@@ -2096,6 +2115,7 @@ pub(crate) mod parsing {
         if qself.is_none()
             && input.peek(Token![!])
             && !input.peek(Token![!=])
+            && !input.peek2(Token![is])
             && path.is_mod_style()
         {
             let bang_token: Token![!] = input.parse()?;
@@ -3498,6 +3518,7 @@ pub(crate) mod printing {
             Expr::BigOr(e) => e.to_tokens(tokens),
             Expr::Has(e) => e.to_tokens(tokens),
             Expr::Is(e) => e.to_tokens(tokens),
+            Expr::IsNot(e) => e.to_tokens(tokens),
             Expr::Matches(e) => e.to_tokens(tokens),
 
             #[cfg(not(feature = "full"))]

dependencies/syn/src/fixup.rs

@@ -771,6 +771,7 @@ fn scan_right(
         | Expr::BigOr(_)
         | Expr::Has(_)
         | Expr::Is(_)
+        | Expr::IsNot(_)
         | Expr::Matches(_)
 
         | Expr::While(_) => match fixup.next_operator {