11use proc_macro:: TokenStream ;
22use proc_macro2:: { Ident , Span } ;
33use quote:: { ToTokens , quote} ;
4+ use syn:: spanned:: Spanned ;
45use syn:: {
5- Expr , ExprClosure , ItemFn , Result , Token ,
6+ Expr , ExprClosure , ItemFn , Pat , Result , Token ,
67 parse:: { Parse , ParseStream } ,
78 parse_macro_input,
89 punctuated:: Punctuated ,
@@ -35,8 +36,7 @@ pub fn contract(args: TokenStream, input: TokenStream) -> TokenStream {
3536/// A container for all parsed arguments from the `#[contract]` attribute.
3637struct ContractArgs {
3738 conditions : Vec < Condition > ,
38- // Optional global rename for the return value.
39- returns_ident : Option < Ident > ,
39+ returns_pat : Option < Pat > ,
4040}
4141
4242/// Represents a single contract condition, e.g., `requires: x > 0`.
@@ -51,45 +51,45 @@ impl Parse for ContractArgs {
5151 /// Custom parser for the contents of `#[contract(...)]`.
5252 fn parse ( input : ParseStream ) -> Result < Self > {
5353 let mut conditions = Vec :: new ( ) ;
54- let mut returns_ident = None ;
54+ let mut returns_pat = None ;
5555
5656 // The arguments are a comma-separated list of conditions or a `returns` key.
5757 let items = Punctuated :: < ContractArgItem , Token ! [ , ] > :: parse_terminated ( input) ?;
5858
5959 for item in items {
6060 match item {
6161 ContractArgItem :: Condition ( condition) => conditions. push ( condition) ,
62- ContractArgItem :: Returns ( ident ) => {
63- if returns_ident . is_some ( ) {
64- return Err ( syn:: Error :: new ( ident . span ( ) , "duplicate `returns` key" ) ) ;
62+ ContractArgItem :: Returns ( pat ) => {
63+ if returns_pat . is_some ( ) {
64+ return Err ( syn:: Error :: new ( pat . span ( ) , "duplicate `returns` key" ) ) ;
6565 }
66- returns_ident = Some ( ident ) ;
66+ returns_pat = Some ( pat ) ;
6767 }
6868 }
6969 }
7070
7171 Ok ( ContractArgs {
7272 conditions,
73- returns_ident ,
73+ returns_pat ,
7474 } )
7575 }
7676}
7777
7878/// An intermediate enum to help parse either a condition or a `returns` key.
7979enum ContractArgItem {
8080 Condition ( Condition ) ,
81- Returns ( Ident ) ,
81+ Returns ( Pat ) ,
8282}
8383
8484impl Parse for ContractArgItem {
8585 fn parse ( input : ParseStream ) -> Result < Self > {
8686 let lookahead = input. lookahead1 ( ) ;
8787 if lookahead. peek ( kw:: returns) {
88- // Parse `returns: new_name `
88+ // Parse `returns: pat `
8989 input. parse :: < kw:: returns > ( ) ?;
9090 input. parse :: < Token ! [ : ] > ( ) ?;
91- let ident = input . parse :: < Ident > ( ) ?;
92- Ok ( ContractArgItem :: Returns ( ident ) )
91+ let pat = Pat :: parse_single ( input ) ?;
92+ Ok ( ContractArgItem :: Returns ( pat ) )
9393 } else if lookahead. peek ( kw:: requires)
9494 || lookahead. peek ( kw:: ensures)
9595 || lookahead. peek ( kw:: maintains)
@@ -151,11 +151,12 @@ fn instrument_body(func: &ItemFn, args: &ContractArgs) -> Result<proc_macro2::To
151151 // The identifier for the return value binding. It's hygienic to prevent collisions.
152152 let binding_ident = Ident :: new ( "__anodized_output" , Span :: mixed_site ( ) ) ;
153153
154- // The identifier used inside the `ensures` predicate. It must be resolvable at the call site.
155- let default_output_ident = args
156- . returns_ident
154+ // The pattern for the `ensures` predicate. It must be resolvable at the call site.
155+ let default_output_pat = args
156+ . returns_pat
157157 . clone ( )
158- . unwrap_or_else ( || Ident :: new ( "output" , Span :: call_site ( ) ) ) ;
158+ . map ( |p| p. to_token_stream ( ) )
159+ . unwrap_or_else ( || quote ! { output } ) ;
159160
160161 // --- Generate Precondition Checks ---
161162 let preconditions = args. conditions . iter ( ) . filter_map ( |c| match c {
@@ -178,7 +179,7 @@ fn instrument_body(func: &ItemFn, args: &ContractArgs) -> Result<proc_macro2::To
178179 }
179180 Condition :: Ensures { predicate } => {
180181 let msg = format ! ( "Postcondition failed: {}" , predicate. to_token_stream( ) ) ;
181- Some ( quote ! { assert!( ( |#default_output_ident | #predicate) ( #binding_ident) , #msg) ; } )
182+ Some ( quote ! { assert!( ( |#default_output_pat | #predicate) ( #binding_ident) , #msg) ; } )
182183 }
183184 Condition :: EnsuresClosure { closure } => {
184185 let msg = format ! ( "Postcondition failed: {}" , closure. to_token_stream( ) ) ;
0 commit comments