vargo fmt

verus-lang · Jan 31, 2025 · f8cedc8 · f8cedc8
1 parent a33c997
commit f8cedc8
Show file tree

Hide file tree

Showing 20 changed files with 232 additions and 171 deletions.
diff --git a/dependencies/prettyplease/src/attr.rs b/dependencies/prettyplease/src/attr.rs
@@ -91,7 +91,11 @@ impl Printer {
 
     fn meta_list(&mut self, meta: &MetaList) {
         self.path(&meta.path, PathKind::Simple);
-        if meta.path.get_ident().is_some_and(|x| x.to_string() == "trigger") {
+        if meta
+            .path
+            .get_ident()
+            .is_some_and(|x| x.to_string() == "trigger")
+        {
             self.attr_tokens(meta.tokens.clone());
             return;
         }

diff --git a/dependencies/prettyplease/src/classify.rs b/dependencies/prettyplease/src/classify.rs
@@ -1,7 +1,9 @@
 use proc_macro2::{Delimiter, TokenStream, TokenTree};
 use std::ops::ControlFlow;
 use syn_verus::punctuated::Punctuated;
-use syn_verus::{Expr, MacroDelimiter, Path, PathArguments, ReturnType, Token, Type, TypeParamBound};
+use syn_verus::{
+    Expr, MacroDelimiter, Path, PathArguments, ReturnType, Token, Type, TypeParamBound,
+};
 
 pub(crate) fn requires_semi_to_be_stmt(expr: &Expr) -> bool {
     match expr {

diff --git a/dependencies/prettyplease/src/expr.rs b/dependencies/prettyplease/src/expr.rs
@@ -1276,69 +1276,65 @@ impl Printer {
     }
 
     fn binary_operator(&mut self, op: &BinOp) {
-        self.word(
-            match op {
-                BinOp::Add(_) => "+",
-                BinOp::Sub(_) => "-",
-                BinOp::Mul(_) => "*",
-                BinOp::Div(_) => "/",
-                BinOp::Rem(_) => "%",
-                BinOp::And(_) => "&&",
-                BinOp::Or(_) => "||",
-                BinOp::BitXor(_) => "^",
-                BinOp::BitAnd(_) => "&",
-                BinOp::BitOr(_) => "|",
-                BinOp::Shl(_) => "<<",
-                BinOp::Shr(_) => ">>",
-                BinOp::Eq(_) => "==",
-                BinOp::Lt(_) => "<",
-                BinOp::Le(_) => "<=",
-                BinOp::Ne(_) => "!=",
-                BinOp::Ge(_) => ">=",
-                BinOp::Gt(_) => ">",
-                BinOp::AddAssign(_) => "+=",
-                BinOp::SubAssign(_) => "-=",
-                BinOp::MulAssign(_) => "*=",
-                BinOp::DivAssign(_) => "/=",
-                BinOp::RemAssign(_) => "%=",
-                BinOp::BitXorAssign(_) => "^=",
-                BinOp::BitAndAssign(_) => "&=",
-                BinOp::BitOrAssign(_) => "|=",
-                BinOp::ShlAssign(_) => "<<=",
-                BinOp::ShrAssign(_) => ">>=",
-
-                // verus
-                BinOp::Equiv(_) => "<==>",
-                BinOp::Imply(_) => "==>",
-                BinOp::Exply(_) => "<==",
-                BinOp::BigEq(_) => "===",
-                BinOp::BigNe(_) => "!==",
-                BinOp::ExtEq(_) => "=~=",
-                BinOp::ExtNe(_) => "!~=",
-                BinOp::ExtDeepEq(_) => "=~~=",
-                BinOp::ExtDeepNe(_) => "!~~=",
-
-                _ => unimplemented!("unknown BinOp"),
-            },
-        );
+        self.word(match op {
+            BinOp::Add(_) => "+",
+            BinOp::Sub(_) => "-",
+            BinOp::Mul(_) => "*",
+            BinOp::Div(_) => "/",
+            BinOp::Rem(_) => "%",
+            BinOp::And(_) => "&&",
+            BinOp::Or(_) => "||",
+            BinOp::BitXor(_) => "^",
+            BinOp::BitAnd(_) => "&",
+            BinOp::BitOr(_) => "|",
+            BinOp::Shl(_) => "<<",
+            BinOp::Shr(_) => ">>",
+            BinOp::Eq(_) => "==",
+            BinOp::Lt(_) => "<",
+            BinOp::Le(_) => "<=",
+            BinOp::Ne(_) => "!=",
+            BinOp::Ge(_) => ">=",
+            BinOp::Gt(_) => ">",
+            BinOp::AddAssign(_) => "+=",
+            BinOp::SubAssign(_) => "-=",
+            BinOp::MulAssign(_) => "*=",
+            BinOp::DivAssign(_) => "/=",
+            BinOp::RemAssign(_) => "%=",
+            BinOp::BitXorAssign(_) => "^=",
+            BinOp::BitAndAssign(_) => "&=",
+            BinOp::BitOrAssign(_) => "|=",
+            BinOp::ShlAssign(_) => "<<=",
+            BinOp::ShrAssign(_) => ">>=",
+
+            // verus
+            BinOp::Equiv(_) => "<==>",
+            BinOp::Imply(_) => "==>",
+            BinOp::Exply(_) => "<==",
+            BinOp::BigEq(_) => "===",
+            BinOp::BigNe(_) => "!==",
+            BinOp::ExtEq(_) => "=~=",
+            BinOp::ExtNe(_) => "!~=",
+            BinOp::ExtDeepEq(_) => "=~~=",
+            BinOp::ExtDeepNe(_) => "!~~=",
+
+            _ => unimplemented!("unknown BinOp"),
+        });
     }
 
     fn unary_operator(&mut self, op: &UnOp) {
-        self.word(
-            match op {
-                UnOp::Deref(_) => "*",
-                UnOp::Not(_) => "!",
-                UnOp::Neg(_) => "-",
-
-                // verus
-                UnOp::Proof(_) => "proof ",
-                UnOp::Forall(_) => "forall ",
-                UnOp::Exists(_) => "exists ",
-                UnOp::Choose(_) => "choose ",
-
-                _ => unimplemented!("unknown UnOp"),
-            },
-        );
+        self.word(match op {
+            UnOp::Deref(_) => "*",
+            UnOp::Not(_) => "!",
+            UnOp::Neg(_) => "-",
+
+            // verus
+            UnOp::Proof(_) => "proof ",
+            UnOp::Forall(_) => "forall ",
+            UnOp::Exists(_) => "exists ",
+            UnOp::Choose(_) => "choose ",
+
+            _ => unimplemented!("unknown UnOp"),
+        });
     }
 
     fn pointer_mutability(&mut self, mutability: &PointerMutability) {

diff --git a/dependencies/syn/src/attr.rs b/dependencies/syn/src/attr.rs
@@ -733,11 +733,17 @@ pub(crate) mod parsing {
 
     fn parse_meta_list_after_path(path: Path, input: ParseStream) -> Result<MetaList> {
         if path.get_ident().is_some_and(|x| x.to_string() == "trigger") {
-            use crate::spanned::Spanned;
             use crate::span::IntoSpans;
-            let paren = token::Paren { span: path.span().into_spans() };
+            use crate::spanned::Spanned;
+            let paren = token::Paren {
+                span: path.span().into_spans(),
+            };
             let delimiter = crate::MacroDelimiter::Paren(paren);
-            return Ok(MetaList { path, delimiter, tokens: input.parse()? });
+            return Ok(MetaList {
+                path,
+                delimiter,
+                tokens: input.parse()?,
+            });
         }
         let (delimiter, tokens) = mac::parse_delimiter(input)?;
         Ok(MetaList {
@@ -831,7 +837,11 @@ mod printing {
     impl ToTokens for MetaList {
         fn to_tokens(&self, tokens: &mut TokenStream) {
             path::printing::print_path(tokens, &self.path, PathStyle::Mod);
-            if self.path.get_ident().is_some_and(|x| x.to_string() == "trigger") {
+            if self
+                .path
+                .get_ident()
+                .is_some_and(|x| x.to_string() == "trigger")
+            {
                 self.tokens.to_tokens(tokens);
                 return;
             }

diff --git a/dependencies/syn/src/classify.rs b/dependencies/syn/src/classify.rs
@@ -286,7 +286,7 @@ pub(crate) fn expr_trailing_brace(mut expr: &Expr) -> bool {
             Expr::Matches(e) => match &e.op_expr {
                 Some(op_expr) => expr = &op_expr.rhs,
                 None => return pat_trailing_brace(&e.pat),
-            }
+            },
         }
     }
 
@@ -304,7 +304,7 @@ pub(crate) fn expr_trailing_brace(mut expr: &Expr) -> bool {
             Pat::Range(e) => match &e.end {
                 Some(end) => expr_trailing_brace(end),
                 None => false,
-            }
+            },
             Pat::Reference(p) => pat_trailing_brace(&p.pat),
             Pat::Rest(_) => false,
             Pat::Slice(_) => false,

diff --git a/dependencies/syn/src/expr.rs b/dependencies/syn/src/expr.rs
@@ -24,8 +24,8 @@ use crate::token;
 use crate::ty::ReturnType;
 use crate::ty::Type;
 use crate::verus::{
-    Assert, Assume, AssertForall, BigAnd, BigOr, Decreases, Ensures, ExprGetField, ExprHas, ExprIs,
-    ExprMatches, Invariant, InvariantExceptBreak, InvariantEnsures, Requires, RevealHide, View,
+    Assert, AssertForall, Assume, BigAnd, BigOr, Decreases, Ensures, ExprGetField, ExprHas, ExprIs,
+    ExprMatches, Invariant, InvariantEnsures, InvariantExceptBreak, Requires, RevealHide, View,
 };
 use proc_macro2::{Span, TokenStream};
 #[cfg(feature = "printing")]
@@ -1559,9 +1559,7 @@ pub(crate) mod parsing {
                     break;
                 }
             } else if next == precedence && Associativity::of(precedence) == Associativity::None {
-                return Err(
-                    input.error("non-associative operator requires additional parentheses")
-                );
+                return Err(input.error("non-associative operator requires additional parentheses"));
             } else {
                 break;
             }

diff --git a/dependencies/syn/src/item.rs b/dependencies/syn/src/item.rs
@@ -15,7 +15,7 @@ use crate::token;
 use crate::ty::{Abi, ReturnType, Type};
 use crate::verus::{
     AssumeSpecification, BroadcastUse, DataMode, Ensures, FnMode, Global, ItemBroadcastGroup,
-    Publish, SignatureSpec
+    Publish, SignatureSpec,
 };
 use proc_macro2::TokenStream;
 #[cfg(feature = "parsing")]
@@ -966,6 +966,7 @@ ast_enum! {
 
 #[cfg(feature = "parsing")]
 pub(crate) mod parsing {
+    use super::FnArgKind;
     use crate::attr::{self, Attribute};
     use crate::derive;
     use crate::error::{Error, Result};
@@ -995,7 +996,6 @@ pub(crate) mod parsing {
     use crate::ty::{Abi, ReturnType, Type, TypePath, TypeReference};
     use crate::verbatim;
     use crate::verus::{DataMode, Ensures, FnMode, Publish};
-    use super::FnArgKind;
     use proc_macro2::TokenStream;
 
     #[cfg_attr(docsrs, doc(cfg(feature = "parsing")))]
@@ -1071,7 +1071,12 @@ pub(crate) mod parsing {
                     Ok(Item::Verbatim(verbatim::between(&begin, input)))
                 } else {
                     let (eq_token, expr, block, semi_token) = if ensures.is_none() {
-                        (Some(input.parse()?), Some(input.parse()?), None, Some(input.parse()?))
+                        (
+                            Some(input.parse()?),
+                            Some(input.parse()?),
+                            None,
+                            Some(input.parse()?),
+                        )
                     } else {
                         (None, None, Some(input.parse()?), None)
                     };
@@ -1123,9 +1128,11 @@ pub(crate) mod parsing {
             let ensures: Option<Ensures> = input.parse()?;
             let (value, block, semi_token) = match (value, &ensures) {
                 (None, None) => (None, None, Some(input.parse()?)),
-                (Some((eq_token, expr)), None) => {
-                    (Some((Some(eq_token), Some(Box::new(expr)))), None, Some(input.parse()?))
-                }
+                (Some((eq_token, expr)), None) => (
+                    Some((Some(eq_token), Some(Box::new(expr)))),
+                    None,
+                    Some(input.parse()?),
+                ),
                 (None, Some(_)) => (Some((None, None)), Some(input.parse()?), None),
                 _ => return Err(lookahead.error()),
             };
@@ -1612,7 +1619,12 @@ pub(crate) mod parsing {
             let ty: Type = input.parse()?;
             let ensures: Option<Ensures> = input.parse()?;
             let (eq_token, expr, block, semi_token) = if ensures.is_none() {
-                (Some(input.parse()?), Some(Box::new(input.parse()?)), None, Some(input.parse()?))
+                (
+                    Some(input.parse()?),
+                    Some(Box::new(input.parse()?)),
+                    None,
+                    Some(input.parse()?),
+                )
             } else {
                 (None, None, Some(input.parse()?), None)
             };
@@ -1809,7 +1821,12 @@ pub(crate) mod parsing {
             }
         }
 
-        let pat_ty = PatType { attrs, pat, colon_token, ty: input.parse()? };
+        let pat_ty = PatType {
+            attrs,
+            pat,
+            colon_token,
+            ty: input.parse()?,
+        };
         let kind = FnArgKind::Typed(pat_ty);
         let fn_arg = FnArg { tracked, kind };
         Ok(FnArgOrVariadic::FnArg(fn_arg))
@@ -3014,7 +3031,10 @@ pub(crate) mod parsing {
             // is emitted later than parsing) and it can be useful for macro
             // DSLs.
             let span = sig.paren_token.span;
-            let block = Block { brace_token: token::Brace { span }, stmts: vec![] };
+            let block = Block {
+                brace_token: token::Brace { span },
+                stmts: vec![],
+            };
             (block, Some(semi))
         } else {
             let content;

diff --git a/dependencies/syn/src/precedence.rs b/dependencies/syn/src/precedence.rs
@@ -211,7 +211,7 @@ impl Precedence {
             | Expr::View(_)
             | Expr::GetField(_) => Precedence::Unambiguous,
             Expr::BigAnd(_) | Expr::BigOr(_) => Precedence::Assign,
-            Expr::Has(_) | Expr::Is(_) | Expr::Matches(_) => Precedence::HasIsMatches,  
+            Expr::Has(_) | Expr::Is(_) | Expr::Matches(_) => Precedence::HasIsMatches,
         }
     }
 }

diff --git a/dependencies/syn/src/restriction.rs b/dependencies/syn/src/restriction.rs
@@ -91,7 +91,7 @@ pub(crate) mod parsing {
 
     impl Visibility {
         pub(crate) fn parse_restricted(
-            input: ParseStream
+            input: ParseStream,
         ) -> Result<Option<(token::Paren, Option<Token![in]>, Box<Path>)>> {
             if input.peek(token::Paren) {
                 let ahead = input.fork();

diff --git a/dependencies/syn/src/ty.rs b/dependencies/syn/src/ty.rs
@@ -9,7 +9,7 @@ use crate::pat::Pat;
 use crate::path::{Path, QSelf};
 use crate::punctuated::Punctuated;
 use crate::token;
-use crate::verus::{TypeFnSpec};
+use crate::verus::TypeFnSpec;
 use proc_macro2::TokenStream;
 
 ast_enum_of_structs! {

diff --git a/dependencies/syn/src/verus.rs b/dependencies/syn/src/verus.rs
@@ -1993,7 +1993,10 @@ pub(crate) fn parse_prefix_binop(
                 )?
             };
 
-            exprs.push(BigAndExpr { tok: token, expr: Box::new(expr) });
+            exprs.push(BigAndExpr {
+                tok: token,
+                expr: Box::new(expr),
+            });
         }
         Ok(Some(Expr::BigAnd(BigAnd { exprs })))
     } else if !big_and_only && input.peek(Token![|||]) {
@@ -2003,7 +2006,10 @@ pub(crate) fn parse_prefix_binop(
         let mut exprs: Vec<BigOrExpr> = Vec::new();
         while let Ok(token) = input.parse() {
             let expr: Expr = input.parse()?;
-            exprs.push(BigOrExpr { tok: token, expr: Box::new(expr) });
+            exprs.push(BigOrExpr {
+                tok: token,
+                expr: Box::new(expr),
+            });
         }
         Ok(Some(Expr::BigOr(BigOr { exprs })))
     } else {

diff --git a/source/builtin_macros/src/attr_block_trait.rs b/source/builtin_macros/src/attr_block_trait.rs
@@ -1,6 +1,4 @@
-use syn::{
-    Attribute, Block, ExprForLoop, ExprLoop, ExprWhile, ImplItemFn, ItemFn, TraitItemFn,
-};
+use syn::{Attribute, Block, ExprForLoop, ExprLoop, ExprWhile, ImplItemFn, ItemFn, TraitItemFn};
 
 pub trait AnyAttrBlock {
     #[allow(dead_code)]

diff --git a/source/builtin_macros/src/attr_rewrite.rs b/source/builtin_macros/src/attr_rewrite.rs
@@ -172,11 +172,9 @@ pub fn rewrite_verus_attribute(
                 attributes.push(mk_verus_attr_syn(arg.span(), quote! { #arg }));
             } else {
                 let span = arg.span();
-                return proc_macro2::TokenStream::from(
-                    quote_spanned!(span =>
-                        compile_error!("unsupported parameters {:?} in #[verus_verify(...)]");
-                    )
-                );
+                return proc_macro2::TokenStream::from(quote_spanned!(span =>
+                    compile_error!("unsupported parameters {:?} in #[verus_verify(...)]");
+                ));
             }
         }
         if attributes.len() == 0 {