From f0652ce340a6134788f54dbff1e6a3ca70f7a4e3 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 16 Aug 2026 11:47:21 +0000 Subject: [PATCH] Fold invariant_context into context `#[thrust_macros::context]` stamped each method of an `impl`/`trait` with the enclosing header, while `#[thrust_macros::invariant_context]` threaded the same header -- plus the host signature -- into the `invariant!` calls in a function body. Two attributes for one question: what does the code inside this item see? They become one. `#[thrust_macros::context]` now takes a function as well, and on an `impl`/`trait` it threads every method's body as it stamps it, so a method carrying a loop invariant no longer needs an attribute of its own: #[thrust_macros::context] impl Counter { fn run(&mut self) -> i64 { while rand() { thrust_macros::invariant!(|init: Self, self: &mut Self| ..); } } } Threading a body that names no such macro leaves it alone, rather than extending its where clause with `Model` predicates nothing asked for: with every method of a `#[context]` item threaded, those bounds would otherwise land on methods that have no formula to justify them. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01PJ6XNNsSBdPkAzrWHftvqV --- .../fail/loop_invariant_fn_param_at_entry.rs | 2 +- .../fail/loop_invariant_fn_param_closure.rs | 4 +- tests/ui/fail/loop_invariant_generic.rs | 2 +- tests/ui/fail/loop_invariant_outer_param.rs | 2 +- tests/ui/fail/loop_invariant_self.rs | 1 - tests/ui/fail/loop_invariant_self_receiver.rs | 1 - tests/ui/fail/loop_invariant_trait.rs | 1 - tests/ui/fail/loop_invariant_trait_self.rs | 1 - .../pass/loop_invariant_fn_param_at_entry.rs | 2 +- .../pass/loop_invariant_fn_param_closure.rs | 4 +- tests/ui/pass/loop_invariant_generic.rs | 2 +- .../ui/pass/loop_invariant_generic_closure.rs | 2 +- tests/ui/pass/loop_invariant_outer_param.rs | 2 +- tests/ui/pass/loop_invariant_self.rs | 1 - tests/ui/pass/loop_invariant_self_receiver.rs | 1 - tests/ui/pass/loop_invariant_trait.rs | 1 - tests/ui/pass/loop_invariant_trait_self.rs | 1 - thrust-macros/src/context.rs | 153 ++++++++++++++++-- thrust-macros/src/invariant.rs | 6 +- thrust-macros/src/invariant_context.rs | 93 ----------- thrust-macros/src/lib.rs | 22 +-- 21 files changed, 165 insertions(+), 139 deletions(-) delete mode 100644 thrust-macros/src/invariant_context.rs diff --git a/tests/ui/fail/loop_invariant_fn_param_at_entry.rs b/tests/ui/fail/loop_invariant_fn_param_at_entry.rs index 51500ab9..fd9f2164 100644 --- a/tests/ui/fail/loop_invariant_fn_param_at_entry.rs +++ b/tests/ui/fail/loop_invariant_fn_param_at_entry.rs @@ -3,7 +3,7 @@ #[thrust_macros::requires(true)] #[thrust_macros::ensures(result.length == v.length + 2)] -#[thrust_macros::invariant_context] +#[thrust_macros::context] fn push_two(v: Vec) -> Vec { let mut w = v; let mut i = 0_i64; diff --git a/tests/ui/fail/loop_invariant_fn_param_closure.rs b/tests/ui/fail/loop_invariant_fn_param_closure.rs index c808b111..1195361c 100644 --- a/tests/ui/fail/loop_invariant_fn_param_closure.rs +++ b/tests/ui/fail/loop_invariant_fn_param_closure.rs @@ -5,7 +5,7 @@ // `f.at_entry()` yields `Closure`. Here the invariant relates `acc` to the // entry closure's postcondition, from which the postcondition below is proven. #[thrust_macros::ensures((n > 0) ==> thrust_macros::post!(f(n - 1), result))] -#[thrust_macros::invariant_context] +#[thrust_macros::context] fn last_apply(f: F, n: i64) -> i64 where F: Fn(i64) -> i64, @@ -25,7 +25,7 @@ where // A capture-free closure is null (singleton) sorted; comparing its identity // must collapse to a canonical value rather than ICE during clause building. -#[thrust_macros::invariant_context] +#[thrust_macros::context] fn unchanged(mut f: F) where F: FnMut(i64) -> i64, diff --git a/tests/ui/fail/loop_invariant_generic.rs b/tests/ui/fail/loop_invariant_generic.rs index 5342e970..05c390e0 100644 --- a/tests/ui/fail/loop_invariant_generic.rs +++ b/tests/ui/fail/loop_invariant_generic.rs @@ -6,7 +6,7 @@ #[thrust::trusted] fn rand() -> i64 { unimplemented!() } -#[thrust_macros::invariant_context] +#[thrust_macros::context] fn keep(v: T) { let mut x = v; while rand() == 0 { diff --git a/tests/ui/fail/loop_invariant_outer_param.rs b/tests/ui/fail/loop_invariant_outer_param.rs index 5543908b..4c88dca5 100644 --- a/tests/ui/fail/loop_invariant_outer_param.rs +++ b/tests/ui/fail/loop_invariant_outer_param.rs @@ -9,7 +9,7 @@ fn rand() -> bool { } #[thrust_macros::ensures(result == a)] -#[thrust_macros::invariant_context] +#[thrust_macros::context] fn keep_argument(a: i64) -> i64 { let mut v = a; diff --git a/tests/ui/fail/loop_invariant_self.rs b/tests/ui/fail/loop_invariant_self.rs index 5ff43b67..4fb50ba0 100644 --- a/tests/ui/fail/loop_invariant_self.rs +++ b/tests/ui/fail/loop_invariant_self.rs @@ -13,7 +13,6 @@ impl thrust_models::Model for Counter { #[thrust_macros::context] impl Counter { - #[thrust_macros::invariant_context] fn run(self) { let mut c = self; let mut x = 1_i64; diff --git a/tests/ui/fail/loop_invariant_self_receiver.rs b/tests/ui/fail/loop_invariant_self_receiver.rs index beee1692..7d803189 100644 --- a/tests/ui/fail/loop_invariant_self_receiver.rs +++ b/tests/ui/fail/loop_invariant_self_receiver.rs @@ -18,7 +18,6 @@ impl thrust_models::Model for Counter { #[thrust_macros::context] impl Counter { - #[thrust_macros::invariant_context] fn run(&mut self) -> i64 { let init = *self; while rand() { diff --git a/tests/ui/fail/loop_invariant_trait.rs b/tests/ui/fail/loop_invariant_trait.rs index cc7d95ed..2409f4bb 100644 --- a/tests/ui/fail/loop_invariant_trait.rs +++ b/tests/ui/fail/loop_invariant_trait.rs @@ -8,7 +8,6 @@ fn rand() -> i64 { unimplemented!() } #[thrust_macros::context] trait Foo { - #[thrust_macros::invariant_context] fn run(&mut self) { let mut x: i64 = 0; while rand() == 0 { diff --git a/tests/ui/fail/loop_invariant_trait_self.rs b/tests/ui/fail/loop_invariant_trait_self.rs index 914a9214..286a9d10 100644 --- a/tests/ui/fail/loop_invariant_trait_self.rs +++ b/tests/ui/fail/loop_invariant_trait_self.rs @@ -16,7 +16,6 @@ trait Gauge { fn update(&mut self) -> i32; - #[thrust_macros::invariant_context] fn run(&mut self) -> i32 { let mut state = 0; while rand() == 0 { diff --git a/tests/ui/pass/loop_invariant_fn_param_at_entry.rs b/tests/ui/pass/loop_invariant_fn_param_at_entry.rs index d7eced52..e8418369 100644 --- a/tests/ui/pass/loop_invariant_fn_param_at_entry.rs +++ b/tests/ui/pass/loop_invariant_fn_param_at_entry.rs @@ -3,7 +3,7 @@ #[thrust_macros::requires(true)] #[thrust_macros::ensures(result.length == v.length + 2)] -#[thrust_macros::invariant_context] +#[thrust_macros::context] fn push_two(v: Vec) -> Vec { let mut w = v; let mut i = 0_i64; diff --git a/tests/ui/pass/loop_invariant_fn_param_closure.rs b/tests/ui/pass/loop_invariant_fn_param_closure.rs index 79d3928f..546ba625 100644 --- a/tests/ui/pass/loop_invariant_fn_param_closure.rs +++ b/tests/ui/pass/loop_invariant_fn_param_closure.rs @@ -5,7 +5,7 @@ // `f.at_entry()` yields `Closure`. Here the invariant relates `acc` to the // entry closure's postcondition, from which the postcondition below is proven. #[thrust_macros::ensures((n > 0) ==> thrust_macros::post!(f(n - 1), result))] -#[thrust_macros::invariant_context] +#[thrust_macros::context] fn last_apply(f: F, n: i64) -> i64 where F: Fn(i64) -> i64, @@ -25,7 +25,7 @@ where // A capture-free closure is null (singleton) sorted; comparing its identity // must collapse to a canonical value rather than ICE during clause building. -#[thrust_macros::invariant_context] +#[thrust_macros::context] fn unchanged(mut f: F) where F: FnMut(i64) -> i64, diff --git a/tests/ui/pass/loop_invariant_generic.rs b/tests/ui/pass/loop_invariant_generic.rs index 7e31b002..1cf831a1 100644 --- a/tests/ui/pass/loop_invariant_generic.rs +++ b/tests/ui/pass/loop_invariant_generic.rs @@ -6,7 +6,7 @@ #[thrust::trusted] fn rand() -> i64 { unimplemented!() } -#[thrust_macros::invariant_context] +#[thrust_macros::context] fn keep(v: T) { let mut x = v; while rand() == 0 { diff --git a/tests/ui/pass/loop_invariant_generic_closure.rs b/tests/ui/pass/loop_invariant_generic_closure.rs index 73668ebe..443edabe 100644 --- a/tests/ui/pass/loop_invariant_generic_closure.rs +++ b/tests/ui/pass/loop_invariant_generic_closure.rs @@ -9,7 +9,7 @@ fn rand() -> i64 { unimplemented!() } // A closure-typed generic param must not be given a `Model` bound: the // invariant only constrains the `Model`-typed `T`, and `keep` must still be // callable with a real closure. -#[thrust_macros::invariant_context] +#[thrust_macros::context] fn keep i64, T: Copy + PartialEq>(f: F, v: T) { let _ = f; let mut x = v; diff --git a/tests/ui/pass/loop_invariant_outer_param.rs b/tests/ui/pass/loop_invariant_outer_param.rs index 03838b2f..97bfea9a 100644 --- a/tests/ui/pass/loop_invariant_outer_param.rs +++ b/tests/ui/pass/loop_invariant_outer_param.rs @@ -9,7 +9,7 @@ fn rand() -> bool { } #[thrust_macros::ensures(result == a)] -#[thrust_macros::invariant_context] +#[thrust_macros::context] fn keep_argument(a: i64) -> i64 { let mut v = a; diff --git a/tests/ui/pass/loop_invariant_self.rs b/tests/ui/pass/loop_invariant_self.rs index f24809d0..acef38f4 100644 --- a/tests/ui/pass/loop_invariant_self.rs +++ b/tests/ui/pass/loop_invariant_self.rs @@ -13,7 +13,6 @@ impl thrust_models::Model for Counter { #[thrust_macros::context] impl Counter { - #[thrust_macros::invariant_context] fn run(self) { let mut c = self; let mut x = 1_i64; diff --git a/tests/ui/pass/loop_invariant_self_receiver.rs b/tests/ui/pass/loop_invariant_self_receiver.rs index 7ff56537..afdbcacf 100644 --- a/tests/ui/pass/loop_invariant_self_receiver.rs +++ b/tests/ui/pass/loop_invariant_self_receiver.rs @@ -18,7 +18,6 @@ impl thrust_models::Model for Counter { #[thrust_macros::context] impl Counter { - #[thrust_macros::invariant_context] fn run(&mut self) -> i64 { let init = *self; while rand() { diff --git a/tests/ui/pass/loop_invariant_trait.rs b/tests/ui/pass/loop_invariant_trait.rs index 8acf26ee..2c4d4c9c 100644 --- a/tests/ui/pass/loop_invariant_trait.rs +++ b/tests/ui/pass/loop_invariant_trait.rs @@ -8,7 +8,6 @@ fn rand() -> i64 { unimplemented!() } #[thrust_macros::context] trait Foo { - #[thrust_macros::invariant_context] fn run(&mut self) { let mut x: i64 = 0; while rand() == 0 { diff --git a/tests/ui/pass/loop_invariant_trait_self.rs b/tests/ui/pass/loop_invariant_trait_self.rs index 5047710b..3c205b59 100644 --- a/tests/ui/pass/loop_invariant_trait_self.rs +++ b/tests/ui/pass/loop_invariant_trait_self.rs @@ -16,7 +16,6 @@ trait Gauge { fn update(&mut self) -> i32; - #[thrust_macros::invariant_context] fn run(&mut self) -> i32 { let mut state = 0; while rand() == 0 { diff --git a/thrust-macros/src/context.rs b/thrust-macros/src/context.rs index 6eff4a7b..0ba272a5 100644 --- a/thrust-macros/src/context.rs +++ b/thrust-macros/src/context.rs @@ -1,24 +1,77 @@ //! Expansion of `#[thrust_macros::context]`. //! -//! Stamps each method in an `impl`/`trait` block with the enclosing header so -//! method-level `requires`/`ensures` can recover the outer generics. +//! Makes the enclosing context available to the specifications written inside an item: +//! +//! - On a function, every `thrust_macros::invariant!(...)` in the body is rewritten into +//! its context-carrying counterpart, carrying the host signature (and, in a method, the +//! enclosing `impl`/`trait` header), so an invariant may refer to generic- and +//! `Self`-typed variables that the standalone macro cannot see. +//! - On an `impl`/`trait`, each method is stamped with the enclosing header so +//! method-level `requires`/`ensures` can recover the outer generics, and its body is +//! threaded as above. +//! +//! Threading a body also extends the function's where clause with the `Model` predicates +//! for every in-scope type parameter (and for `Self` when used), since each injected +//! marker call instantiates a `Model`-bounded formula function with the host's own +//! generics. use proc_macro::TokenStream; -use quote::ToTokens as _; +use proc_macro2::TokenStream as TokenStream2; +use quote::{quote, ToTokens as _}; +use syn::{ + parse::{Parse, ParseStream}, + visit_mut::VisitMut, + Signature, +}; use crate::fn_outer_item::FnOuterItem; pub fn expand(item: TokenStream) -> TokenStream { - let mut outer_item = syn::parse_macro_input!(item as FnOuterItem); - let outer_header = outer_item.clone().into_header_only(); + let item = syn::parse_macro_input!(item as ContextItem); + match item { + ContextItem::Fn(mut item_fn) => { + let outer = match crate::extract_outer_context(&item_fn.attrs) { + Ok(outer) => outer, + Err(e) => return e.to_compile_error().into(), + }; + thread_into_body(&mut item_fn.sig, &mut item_fn.block, outer.as_ref()); + item_fn.into_token_stream().into() + } + ContextItem::Outer(outer_item) => expand_outer(outer_item).into(), + } +} + +/// An item `#[thrust_macros::context]` applies to. +enum ContextItem { + Fn(syn::ItemFn), + Outer(FnOuterItem), +} + +impl Parse for ContextItem { + fn parse(input: ParseStream) -> syn::Result { + use syn::parse::discouraged::Speculative as _; + + let fork = input.fork(); + if let Ok(item_fn) = fork.parse::() { + input.advance_to(&fork); + return Ok(Self::Fn(item_fn)); + } + + input.parse().map(Self::Outer) + } +} + +fn expand_outer(mut outer_item: FnOuterItem) -> TokenStream2 { + let header = outer_item.clone().into_header_only(); + let header_attr: syn::Attribute = syn::parse_quote!(#[thrust::_outer_context(#header)]); match &mut outer_item { FnOuterItem::ItemImpl(item_impl) => { for item in &mut item_impl.items { let syn::ImplItem::Fn(item) = item else { continue; }; - item.attrs - .push(syn::parse_quote!(#[thrust::_outer_context(#outer_header)])); + item.attrs.push(header_attr.clone()); + thread_into_body(&mut item.sig, &mut item.block, Some(&header)); } } FnOuterItem::ItemTrait(item_trait) => { @@ -26,11 +79,91 @@ pub fn expand(item: TokenStream) -> TokenStream { let syn::TraitItem::Fn(item) = item else { continue; }; - item.attrs - .push(syn::parse_quote!(#[thrust::_outer_context(#outer_header)])); + item.attrs.push(header_attr.clone()); + if let Some(default) = &mut item.default { + thread_into_body(&mut item.sig, default, Some(&header)); + } } } } + outer_item.into_token_stream() +} + +/// Rewrites each spec macro in `body` into its context-carrying counterpart, carrying +/// `sig` and the `outer` header of the `impl`/`trait` the function is a method of, and +/// extends `sig`'s where clause with the `Model` predicates those calls need. A body +/// naming no spec macro is left as it is. +fn thread_into_body(sig: &mut Signature, body: &mut syn::Block, outer: Option<&FnOuterItem>) { + let host_sig = sig.clone(); + let mut injector = ContextInjector { + sig: &host_sig, + outer, + injected: false, + self_used: false, + }; + injector.visit_block_mut(body); + if !injector.injected { + return; + } - outer_item.into_token_stream().into() + let type_lowering = match outer { + Some(outer) => crate::FormulaFnTypeLowering::with_outer_context(&host_sig, outer), + None => crate::FormulaFnTypeLowering::new(&host_sig), + }; + let mut predicates = type_lowering.model_where_predicates(); + if injector.self_used { + predicates.extend(type_lowering.model_where_predicates_for("e::format_ident!("Self"))); + } + if !predicates.is_empty() { + sig.generics + .make_where_clause() + .predicates + .extend(predicates); + } +} + +struct ContextInjector<'a> { + sig: &'a Signature, + outer: Option<&'a FnOuterItem>, + injected: bool, + self_used: bool, +} + +impl ContextInjector<'_> { + fn inject_context(&self, closure: &TokenStream2) -> TokenStream2 { + let sig = self.sig; + let outer_attr = self + .outer + .map(|outer| quote!(#[thrust::_outer_context(#outer)])); + + quote! { + #outer_attr + #sig; + #closure + } + } +} + +impl VisitMut for ContextInjector<'_> { + fn visit_macro_mut(&mut self, mac: &mut syn::Macro) { + let Some(with_context) = context_carrying_form(&mac.path) else { + return; + }; + self.injected = true; + if crate::tokens_contain_ident(&mac.tokens, "Self") { + self.self_used = true; + } + mac.tokens = self.inject_context(&mac.tokens); + mac.path = with_context; + } +} + +/// The context-carrying counterpart of a spec macro that takes a formula over live +/// variables, or `None` for any other macro. +fn context_carrying_form(path: &syn::Path) -> Option { + // TODO: identify the macro precisely + match path.segments.last()?.ident.to_string().as_str() { + "invariant" => Some(syn::parse_quote!(::thrust_macros::_invariant_with_context)), + _ => None, + } } diff --git a/thrust-macros/src/invariant.rs b/thrust-macros/src/invariant.rs index f94f3db2..9c519aa8 100644 --- a/thrust-macros/src/invariant.rs +++ b/thrust-macros/src/invariant.rs @@ -8,7 +8,7 @@ //! - `invariant!(|x: i64| x >= 1)` takes a bare predicate closure and only sees //! concrete types. //! - `_invariant_with_context!(..)` additionally carries the enclosing generic -//! context. It is never written by hand: `#[thrust_macros::invariant_context]` +//! context. It is never written by hand: `#[thrust_macros::context]` //! rewrites each `invariant!` it finds into this form, pasting the host //! function's signature (and, in methods, a `#[thrust::_outer_context(..)]` //! attribute carrying the enclosing `impl`/`trait` header) ahead of the @@ -57,7 +57,7 @@ pub fn expand(input: TokenStream) -> TokenStream { } /// Expands `_invariant_with_context!(#outer_attr #sig; CLOSURE)`, the form -/// `#[thrust_macros::invariant_context]` rewrites each `invariant!` into. +/// `#[thrust_macros::context]` rewrites each `invariant!` into. pub fn expand_with_context(input: TokenStream) -> TokenStream { struct WithContext { context: Context, @@ -90,7 +90,7 @@ pub fn expand_with_context(input: TokenStream) -> TokenStream { } /// The enclosing context threaded into an invariant by -/// `#[thrust_macros::invariant_context]`: the host function signature and, for a +/// `#[thrust_macros::context]`: the host function signature and, for a /// method, its `impl`/`trait` header. A standalone `invariant!` has none. struct Context { sig: Signature, diff --git a/thrust-macros/src/invariant_context.rs b/thrust-macros/src/invariant_context.rs deleted file mode 100644 index 1468b305..00000000 --- a/thrust-macros/src/invariant_context.rs +++ /dev/null @@ -1,93 +0,0 @@ -//! Expansion of `#[thrust_macros::invariant_context]`. -//! -//! Threads the surrounding generic context (and, in methods, `Self`) into -//! every `thrust_macros::invariant!(...)` call inside the annotated function, so -//! an invariant may refer to generic- and `Self`-typed variables that the -//! standalone `invariant!` macro cannot see. -//! -//! It also extends the host function's where clause with the `Model` predicates for every in-scope -//! type parameter (and for `Self` when used), since each injected marker call instantiates a -//! `Model`-bounded formula function with the host's own generics. - -use proc_macro::TokenStream; -use proc_macro2::TokenStream as TokenStream2; -use quote::{quote, ToTokens}; -use syn::{visit_mut::VisitMut, Signature}; - -use crate::fn_outer_item::FnOuterItem; - -pub fn expand(item: TokenStream) -> TokenStream { - let mut item_fn = syn::parse_macro_input!(item as syn::ItemFn); - - let outer = match crate::extract_outer_context(&item_fn.attrs) { - Ok(outer) => outer, - Err(e) => return e.to_compile_error().into(), - }; - - let sig = item_fn.sig.clone(); - let mut injector = ContextInjector { - sig: &sig, - outer: outer.as_ref(), - self_used: false, - }; - injector.visit_block_mut(&mut item_fn.block); - - let type_lowering = if let Some(outer) = &outer { - crate::FormulaFnTypeLowering::with_outer_context(&sig, outer) - } else { - crate::FormulaFnTypeLowering::new(&sig) - }; - let mut predicates = type_lowering.model_where_predicates(); - if injector.self_used { - predicates.extend(type_lowering.model_where_predicates_for("e::format_ident!("Self"))); - } - if !predicates.is_empty() { - item_fn - .sig - .generics - .make_where_clause() - .predicates - .extend(predicates); - } - - item_fn.into_token_stream().into() -} - -struct ContextInjector<'a> { - sig: &'a Signature, - outer: Option<&'a FnOuterItem>, - self_used: bool, -} - -impl<'a> ContextInjector<'a> { - fn inject_context(&self, closure: &TokenStream2) -> TokenStream2 { - let sig = self.sig; - let outer_attr = self - .outer - .map(|outer| quote!(#[thrust::_outer_context(#outer)])); - - quote! { - #outer_attr - #sig; - #closure - } - } -} - -impl VisitMut for ContextInjector<'_> { - fn visit_macro_mut(&mut self, mac: &mut syn::Macro) { - if !is_invariant_macro(&mac.path) { - return; - } - if crate::tokens_contain_ident(&mac.tokens, "Self") { - self.self_used = true; - } - mac.tokens = self.inject_context(&mac.tokens); - mac.path = syn::parse_quote!(::thrust_macros::_invariant_with_context); - } -} - -fn is_invariant_macro(path: &syn::Path) -> bool { - // TODO: identify the macro precisely - path.segments.last().is_some_and(|s| s.ident == "invariant") -} diff --git a/thrust-macros/src/lib.rs b/thrust-macros/src/lib.rs index 165409a3..2d81ec0d 100644 --- a/thrust-macros/src/lib.rs +++ b/thrust-macros/src/lib.rs @@ -8,7 +8,6 @@ mod formula; mod formula_fn_type_lowering; mod ghost; mod invariant; -mod invariant_context; mod pre_post; mod rty; mod spec; @@ -53,6 +52,11 @@ pub fn ghost(input: TokenStream) -> TokenStream { ghost::expand(input) } +/// Makes the enclosing context available to the specifications written inside an +/// item. On an `impl`/`trait`, each method recovers the outer generics (and `Self`) +/// in its `requires`/`ensures`; on a function — including a method reached that way — +/// every `thrust_macros::invariant!(...)` in the body may refer to generic- and +/// `Self`-typed variables that the standalone macro cannot see. See [`mod@context`]. #[proc_macro_attribute] pub fn context(_attr: TokenStream, item: TokenStream) -> TokenStream { context::expand(item) @@ -84,7 +88,7 @@ pub fn invariant(input: TokenStream) -> TokenStream { } /// Context-carrying counterpart of `invariant!`, emitted by -/// `#[thrust_macros::invariant_context]`. Not intended to be written by hand: +/// `#[thrust_macros::context]`. Not intended to be written by hand: /// it takes a `fn` header carrying the threaded generics/where clause whose /// body is the predicate closure (see [`invariant`]). #[proc_macro] @@ -92,16 +96,6 @@ pub fn _invariant_with_context(input: TokenStream) -> TokenStream { invariant::expand_with_context(input) } -/// Threads the surrounding generic context (and, in methods, `Self`) into -/// every `thrust_macros::invariant!(...)` inside the annotated function, so an -/// invariant may refer to generic- and `Self`-typed variables that the -/// standalone `invariant!` macro cannot see. Each such call is rewritten into -/// `thrust_macros::_invariant_with_context!`. -#[proc_macro_attribute] -pub fn invariant_context(_attr: TokenStream, item: TokenStream) -> TokenStream { - invariant_context::expand(item) -} - #[proc_macro_attribute] pub fn predicate(_attr: TokenStream, item: TokenStream) -> TokenStream { spec::expand_predicate(item) @@ -123,8 +117,8 @@ pub fn _requires_ensures(attr: TokenStream, item: TokenStream) -> TokenStream { } /// Reads the `#[thrust::_outer_context(..)]` attribute stamped onto methods by -/// `#[thrust_macros::context]` (and threaded by `invariant_context`), returning -/// the enclosing `impl`/`trait` header it carries, or `None` if absent. +/// `#[thrust_macros::context]` (and threaded into the spec macros in their bodies), +/// returning the enclosing `impl`/`trait` header it carries, or `None` if absent. fn extract_outer_context(attrs: &[syn::Attribute]) -> syn::Result> { let outer_context_path: syn::Path = syn::parse_quote!(thrust::_outer_context); let mut outer_context = None;