Support Self and generic variables in loop invariants#102
Closed
coord-e wants to merge 11 commits into
Closed
Conversation
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
…nd 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.
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.
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.
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.
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.
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.
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.
…batim 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).
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.
Owner
Author
|
mistakenly duplicated #99 ...... |
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
2 participants
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.
Add
#[thrust_macros::invariant_context]— a new attribute that threads thesurrounding generic context (and, in methods,
Self) into everythrust_macros::invariant!(...)inside the annotated function, impl, ortrait. 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,
Selfis re-declared asa synthetic type parameter and instantiated with the real
Self(legal inexpression position), so an invariant may refer to generic- and
Self-typedvariables that the standalone
invariant!macro cannot see.thrust_macros::contextand the standalonethrust_macros::invariant!macroare unchanged;
invariant_contextrewrites the macro tokens beforeinvariant!would otherwise expand, so the simpleinvariant!path keepsworking as-is for concrete invariants.
Adds pass/fail UI test pairs for the generic and
Selfcases. Note that astruct used as an invariant variable must model structurally (its
Model::Tymust 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