thrust-macros: split lib.rs into context, invariant, and spec modules#101
Merged
Conversation
Pure refactor: move the existing `context` impl into `context.rs`, and the `predicate`/`requires`/`ensures`/`_requires_ensures` machinery (plus `FnItemWithSignature`, `ExpandedTokens`, and their helpers) into `spec.rs`. The crate root now holds only the proc-macro entry points (thin delegations) and the two helpers shared across modules (`FnOuterItem`, `fn_params_with_model_ty`). The shared helpers stay private: a private root item is visible to every descendant module, so no `pub(crate)` is required. No behavior change. https://claude.ai/code/session_01WB28auaD8dSQrckqBwJWBt
There was a problem hiding this comment.
Pull request overview
This PR refactors the thrust-macros proc-macro crate by splitting the previously monolithic src/lib.rs into focused modules (context, fn_outer_item, and spec), leaving the crate root primarily as proc-macro entry points plus a small shared helper.
Changes:
- Moved
#[thrust_macros::context]expansion logic intosrc/context.rs. - Extracted the “outer impl/trait header carrier” type into
src/fn_outer_item.rs. - Moved
requires/ensures/predicate+_requires_ensuresexpansion logic intosrc/spec.rs, and updatedlib.rsto delegate to it.
Reviewed changes
Copilot reviewed 4 out of 4 changed files in this pull request and generated no comments.
| File | Description |
|---|---|
| thrust-macros/src/lib.rs | Simplifies the proc-macro crate root to module wiring + proc-macro entry points delegating into submodules. |
| thrust-macros/src/spec.rs | Hosts the requires/ensures/predicate and _requires_ensures expansion implementation previously in lib.rs. |
| thrust-macros/src/context.rs | Hosts the #[thrust_macros::context] expansion implementation previously in lib.rs. |
| thrust-macros/src/fn_outer_item.rs | Defines FnOuterItem used to carry impl/trait headers for _outer_context handling. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
coord-e
pushed a commit
that referenced
this pull request
Jun 4, 2026
Resolution of the rebase onto latest main: main (#101) extracted FnOuterItem into its own fn_outer_item module and dropped it from the crate root. Adapt the loop-invariant work accordingly — reference crate::fn_outer_item::FnOuterItem and keep the shared helpers (extract_outer_context, has_fn_bound, model_predicates, model_where_predicates, tokens_contain_ident) in the crate root.
coord-e
added a commit
that referenced
this pull request
Jun 4, 2026
* Support Self and generic variables in loop invariants Add `#[thrust_macros::invariant_context]` — a new attribute that threads the surrounding generic context (and, in methods, `Self`) into every `thrust_macros::invariant!(...)` inside the annotated function, impl, or trait. Each call is replaced in-place by an expanded `#[thrust::formula_fn]` plus a marker call, with the threaded generics declared on the formula function and instantiated via turbofish. In methods, `Self` is re-declared as a synthetic type parameter and instantiated with the real `Self` (legal in expression position), so an invariant may refer to generic- and `Self`-typed variables that the standalone `invariant!` macro cannot see. `thrust_macros::context` and the standalone `thrust_macros::invariant!` macro are unchanged; `invariant_context` rewrites the macro tokens before `invariant!` would otherwise expand, so the simple `invariant!` path keeps working as-is for concrete invariants. Adds pass/fail UI test pairs for the generic and `Self` cases. Note that a struct used as an invariant variable must model structurally (its `Model::Ty` must mirror its fields, e.g. a one-field tuple struct models as a one-tuple); a mismatching model trips an existing subtyping panic unrelated to this change. https://claude.ai/code/session_01WB28auaD8dSQrckqBwJWBt * thrust-macros: make invariant_context inject context, invariant! expand it Previously invariant_context re-implemented the whole invariant! expansion (closure parsing, formula_fn synthesis, marker call), duplicating the logic already in invariant.rs. Now the responsibilities are split, mirroring the existing requires/ensures _outer_context convention: - invariant_context only *injects* the enclosing context into each invariant!(CLOSURE) call, rewriting it into a context-carrying form built from existing syntax (a fn header carrying the in-scope generics/where clause, tagged for methods with #[thrust::_outer_context(impl/trait header)]). It still extends the host fn's where clause with the Model/PartialEq bounds, which a function-like macro cannot do itself. - invariant! now performs the single, shared expansion for both the standalone concrete form and the threaded form, re-declaring the threaded generics (and synthetic Self) on the formula function and instantiating via turbofish. No new bracket syntax is introduced; the context rides on ordinary Rust fn header syntax and the existing _outer_context attribute. * thrust-macros: route threaded invariants through a dedicated macro Rather than having invariant! accept two different input shapes (a bare closure, or a context-carrying fn header), introduce a dedicated internal macro thrust_macros::_invariant_with_context! for the threaded form. - invariant! now only accepts a bare predicate closure. - _invariant_with_context! only accepts the context-carrying fn header. - invariant_context rewrites each invariant!(CLOSURE) into _invariant_with_context!(<context fn> { CLOSURE }) by swapping the macro path as well as injecting the context tokens. Both macros share Invariant::expand, so there is still a single expansion implementation. The leading underscore follows the existing _requires_ensures convention for macros emitted by other macros and not written by hand. * thrust-macros: model invariant context as Option<Context> Replace the Invariant struct, which represented a standalone invariant as empty param/where vecs plus is_method=false, with an explicit Option<&Context> argument to a shared expand_invariant function. None now unambiguously means "no threaded context" (standalone invariant!), distinct from a contextful invariant that merely has no generics. * thrust-macros: share extract_outer_context via crate root invariant.rs and spec.rs each had their own copy of the _outer_context attribute reader. Hoist the shared attribute-reading logic into the crate root (alongside FnOuterItem and the other shared helpers); spec's wrapper now calls it and keeps only its method-specific mentions_self diagnostic. * thrust-macros: invariant_context accepts only a function item invariant_context previously walked impl/trait blocks itself, duplicating the method-iteration that #[thrust_macros::context] already does. Restrict it to a single function: a method recovers its enclosing impl/trait context from the #[thrust::_outer_context(..)] attribute stamped by #[thrust_macros::context], the same mechanism requires/ensures use. Update the loop_invariant_self tests to combine #[context] on the impl with #[invariant_context] on the method accordingly. * thrust-macros: share Model-predicate construction with spec The [T: Model, <T as Model>::Ty: PartialEq] predicate pair was built by hand in three places (twice in spec, once in invariant_context). Hoist it into a shared crate-root helper model_predicates(ty); each caller keeps its own which-types-to-bound logic but no longer open-codes the predicate pair. * thrust-macros: exclude closure-typed params from invariant Model bounds spec skips Fn/FnMut/FnOnce-bounded type params when adding Model predicates (closures have no Model instance), but the invariant path bounded every type param unconditionally. A generic invariant inside a function with a closure- typed generic param therefore generated F: Model and failed at the call site with "the trait bound {closure}: Model is not satisfied". Share spec's Fn-bound check as a crate-root helper has_fn_bound and apply it in both the formula function (invariant.rs) and the host where clause (invariant_context.rs). Add a regression test. * thrust-macros: reuse model_where_predicates; carry host signature verbatim Address three points: 1. Reuse the whole model_where_predicates (not just has_fn_bound). Move it to the crate root, retargeted at &Signature, and call it from both the formula function (invariant) and the host where clause (invariant_context). Each path adds Self handling on top (synthetic param vs Self: Model) but no longer open-codes generic collection or the Fn-bound exclusion. 2. Rename InvariantInjector to ContextInjector. 3. Change the _invariant_with_context input to '#outer_attr #signature; #closure'. ContextInjector now pastes the host function signature verbatim, and the expansion parses it back, so model_where_predicates sees the real signature (its generics, where clause, and parameter/return projections). * style fix * thrust-macros: reconcile rebase with main's fn_outer_item module Resolution of the rebase onto latest main: main (#101) extracted FnOuterItem into its own fn_outer_item module and dropped it from the crate root. Adapt the loop-invariant work accordingly — reference crate::fn_outer_item::FnOuterItem and keep the shared helpers (extract_outer_context, has_fn_bound, model_predicates, model_where_predicates, tokens_contain_ident) in the crate root. * style fix * style fix --------- Co-authored-by: Claude <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
separated from #99; splits thrust-macros/src/lib.rs