Support Self and generic variables in loop invariants#99
Draft
coord-e wants to merge 2 commits into
Draft
Conversation
2 tasks
6e84fab to
c4e64ef
Compare
f8dae72 to
5903aba
Compare
c4e64ef to
f6f063e
Compare
5903aba to
4da71aa
Compare
f6f063e to
61e2146
Compare
4da71aa to
abd3602
Compare
61e2146 to
3d93645
Compare
abd3602 to
0605e6b
Compare
3d93645 to
faaaa7c
Compare
0605e6b to
995ff18
Compare
faaaa7c to
ca7f820
Compare
995ff18 to
35176d6
Compare
35176d6 to
b4844c6
Compare
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
Extend `thrust_macros::invariant!` to invariants over generic- and `Self`-typed variables, by extending `#[thrust_macros::context]` to thread the surrounding context into each `invariant!` it encounters. `context` now also accepts free functions and modules (in addition to `impl`/`trait`) and threads the in-scope generics, where-predicates, and (in methods) `Self` into every `invariant!`. `invariant!` accepts a threaded `[self] [params] [wheres] <closure>` input. The generated formula function re-declares the threaded generics (shadowing the enclosing ones) and is instantiated via turbofish; in methods, `Self` is re-declared the same way as a synthetic type parameter and instantiated with the real `Self` (legal in expression position). 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
b4844c6 to
4d56d1c
Compare
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.
Summary
Extends
thrust_macros::invariant!to invariants over generic- andSelf-typed variables, by extending#[thrust_macros::context]to thread the enclosing context into eachinvariant!.Frontend (
thrust-macros)#[thrust_macros::context](which already stamps the enclosingimpl/traitheader onto methods so method-levelrequires/ensuresrecover the outer generics) now also accepts free functions and modules and threads the in-scope generics, where-predicates, and (in methods)Selfinto everyinvariant!it encounters.invariant!accepts a threaded[self] [params] [wheres] <closure>input. The generated formula function re-declares the threaded generics (shadowing the enclosing ones) and is instantiated via turbofish; in methods,Selfis re-declared the same way as a synthetic type parameter and instantiated with the realSelf(legal in expression position).context.context,invariant, andspecmodules; the root keeps only the proc-macro entry points and a few shared private helpers.Test plan
Selfcases (loop_invariant_generic,loop_invariant_self).cargo test --test ui(203 passed),cargo clippy --all-targets,cargo fmt --checkall clean.Notes
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 PR.https://claude.ai/code/session_01WB28auaD8dSQrckqBwJWBt