returns (#1283)

dependencies/syn/src/item.rs

@@ -947,6 +947,7 @@ ast_struct! {
         pub requires: Option<Requires>,
         pub recommends: Option<Recommends>,
         pub ensures: Option<Ensures>,
+        pub returns: Option<Returns>,
         pub decreases: Option<SignatureDecreases>,
         pub invariants: Option<SignatureInvariants>,
         pub unwind: Option<SignatureUnwind>,
@@ -976,6 +977,7 @@ impl Signature {
         self.requires = None;
         self.recommends = None;
         self.ensures = None;
+        self.returns = None;
         self.decreases = None;
         self.invariants = None;
         self.unwind = None;
@@ -1725,6 +1727,7 @@ pub mod parsing {
             let requires: Option<Requires> = input.parse()?;
             let recommends: Option<Recommends> = input.parse()?;
             let ensures: Option<Ensures> = input.parse()?;
+            let returns: Option<Returns> = input.parse()?;
             let decreases: Option<SignatureDecreases> = input.parse()?;
             let invariants: Option<SignatureInvariants> = input.parse()?;
             let unwind: Option<SignatureUnwind> = input.parse()?;
@@ -1748,6 +1751,7 @@ pub mod parsing {
                 requires,
                 recommends,
                 ensures,
+                returns,
                 decreases,
                 invariants,
                 unwind,
@@ -3591,6 +3595,7 @@ mod printing {
             self.requires.to_tokens(tokens);
             self.recommends.to_tokens(tokens);
             self.ensures.to_tokens(tokens);
+            self.returns.to_tokens(tokens);
             self.decreases.to_tokens(tokens);
         }
     }

dependencies/syn/src/lib.rs

@@ -462,7 +462,7 @@ pub use crate::verus::{
     GlobalSizeOf, Invariant, InvariantEnsures, InvariantExceptBreak, InvariantNameSet,
     InvariantNameSetAny, InvariantNameSetList, InvariantNameSetNone, ItemBroadcastGroup,
     MatchesOpExpr, MatchesOpToken, Mode, ModeExec, ModeGhost, ModeProof, ModeSpec, ModeSpecChecked,
-    ModeTracked, Open, OpenRestricted, Publish, Recommends, Requires, RevealHide,
+    ModeTracked, Open, OpenRestricted, Publish, Recommends, Requires, Returns, RevealHide,
     SignatureDecreases, SignatureInvariants, SignatureUnwind, Specification, TypeFnSpec, View,
 };
 

dependencies/syn/src/token.rs

@@ -714,6 +714,7 @@ define_keywords! {
     "requires"    pub struct Requires     /// `requires`
     "recommends"  pub struct Recommends   /// `recommends`
     "ensures"     pub struct Ensures      /// `ensures`
+    "returns"     pub struct Returns      /// `returns`
     "decreases"   pub struct Decreases    /// `decreases`
     "opens_invariants"   pub struct OpensInvariants    /// `opens_invariants`
     "invariant_except_break"   pub struct InvariantExceptBreak    /// `invariant_except_break`
@@ -938,6 +939,7 @@ macro_rules! export_token_macro {
             [requires]    => { $crate::token::Requires };
             [recommends]  => { $crate::token::Recommends };
             [ensures]     => { $crate::token::Ensures };
+            [returns]     => { $crate::token::Returns };
             [decreases]   => { $crate::token::Decreases };
             [opens_invariants]   => { $crate::token::OpensInvariants };
             [invariant_except_break]   => { $crate::token::InvariantExceptBreak };

dependencies/syn/src/verus.rs

@@ -126,6 +126,13 @@ ast_struct! {
     }
 }
 
+ast_struct! {
+    pub struct Returns {
+        pub token: Token![returns],
+        pub exprs: Specification,
+    }
+}
+
 ast_struct! {
     pub struct InvariantExceptBreak {
         pub token: Token![invariant_except_break],
@@ -505,6 +512,7 @@ pub mod parsing {
                 || input.peek(Token![invariant])
                 || input.peek(Token![invariant_ensures])
                 || input.peek(Token![ensures])
+                || input.peek(Token![returns])
                 || input.peek(Token![decreases])
                 || input.peek(Token![via])
                 || input.peek(Token![when])
@@ -586,6 +594,17 @@ pub mod parsing {
         }
     }
 
+    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
+    impl Parse for Returns {
+        fn parse(input: ParseStream) -> Result<Self> {
+            let token = input.parse()?;
+            Ok(Returns {
+                token,
+                exprs: input.parse()?,
+            })
+        }
+    }
+
     #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
     impl Parse for InvariantExceptBreak {
         fn parse(input: ParseStream) -> Result<Self> {
@@ -772,6 +791,17 @@ pub mod parsing {
         }
     }
 
+    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
+    impl Parse for Option<Returns> {
+        fn parse(input: ParseStream) -> Result<Self> {
+            if input.peek(Token![returns]) {
+                input.parse().map(Some)
+            } else {
+                Ok(None)
+            }
+        }
+    }
+
     #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
     impl Parse for Option<InvariantExceptBreak> {
         fn parse(input: ParseStream) -> Result<Self> {
@@ -1262,6 +1292,14 @@ mod printing {
         }
     }
 
+    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
+    impl ToTokens for Returns {
+        fn to_tokens(&self, tokens: &mut TokenStream) {
+            self.token.to_tokens(tokens);
+            self.exprs.to_tokens(tokens);
+        }
+    }
+
     #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
     impl ToTokens for InvariantExceptBreak {
         fn to_tokens(&self, tokens: &mut TokenStream) {

dependencies/syn/syn.json

@@ -5611,6 +5611,20 @@
         ]
       }
     },
+    {
+      "ident": "Returns",
+      "features": {
+        "any": []
+      },
+      "fields": {
+        "token": {
+          "token": "Returns"
+        },
+        "exprs": {
+          "syn": "Specification"
+        }
+      }
+    },
     {
       "ident": "RevealHide",
       "features": {
@@ -5758,6 +5772,11 @@
             "syn": "Ensures"
           }
         },
+        "returns": {
+          "option": {
+            "syn": "Returns"
+          }
+        },
         "decreases": {
           "option": {
             "syn": "SignatureDecreases"
@@ -7116,6 +7135,7 @@
     "RemEq": "%=",
     "Requires": "requires",
     "Return": "return",
+    "Returns": "returns",
     "Reveal": "reveal",
     "RevealWithFuel": "reveal_with_fuel",
     "SelfType": "Self",