Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

WIP: Iterator tracking issues #980

Open
wants to merge 45 commits into
base: master
Choose a base branch
from

Conversation

vl0w
Copy link
Contributor

@vl0w vl0w commented Apr 27, 2022

Some (smaller / bigger) changes needed to enable iterator support
(WIP / tracking PR)

  • Moved normalization of constraint param env (for assoc types) for better logging
  • Fixed a bug in SpecGraph: Preconditions of the base spec were copied to the constrained spec
  • Ghost constraint resolving is a bit relaxed (predicate_may_hold instead of predicate_must_hold_considering_regions) to account for references in associated types. See test associated_types_6.rs
  • merge_generics now also merges lifetimes to accout for lifetimes appearing in #[refine_trait_spec]
  • Lifetimes in type models are not converted to the anonymous lifetime '_ anymore
  • Do not #[derive(Copy, Clone] on type models, because the derive macro "conditionally" implements it when generics are involved. That is, #[derive(Copy)] struct Foo<T> adds impl<T: Copy> Copy for Foo {}, but we do not want to implement Copy only if T is Copy.
  • Quantified variables now support associated types: forall(|x: Self::SomeAssocType| ...)

@vl0w vl0w force-pushed the iterators-feature-flag branch 3 times, most recently from 546c701 to fb7d09e Compare April 28, 2022 09:53
@vl0w vl0w force-pushed the iterators-feature-flag branch 2 times, most recently from 32ccf0e to ae6589d Compare April 28, 2022 17:46
@vl0w vl0w force-pushed the iterators-feature-flag branch 4 times, most recently from 12f63cf to ec42da1 Compare April 29, 2022 12:51
@Aurel300
Copy link
Member

bors r+

bors bot added a commit that referenced this pull request Jul 19, 2022
980: WIP: Iterator tracking issues r=Aurel300 a=vl0w

Some (smaller / bigger) changes needed to enable iterator support
(WIP / tracking PR)

- Moved normalization of constraint param env (for assoc types) for better logging
- Fixed a bug in `SpecGraph`: Preconditions of the base spec were copied to the constrained spec
- Ghost constraint resolving is a bit relaxed (`predicate_may_hold` instead of `predicate_must_hold_considering_regions`) to account for references in associated types. See test `associated_types_6.rs`
- `merge_generics` now also merges lifetimes to accout for lifetimes appearing in `#[refine_trait_spec]`
- Lifetimes in type models are not converted to the anonymous lifetime `'_` anymore
- Do not `#[derive(Copy, Clone]` on type models, because the derive macro "conditionally" implements it when generics are involved. That is, `#[derive(Copy)] struct Foo<T>` adds `impl<T: Copy> Copy for Foo {}`, but we do not want to implement `Copy` only if `T` is `Copy`.
- Quantified variables now support associated types: `forall(|x: Self::SomeAssocType| ...)`

Co-authored-by: Jonas Hansen <ganymed92@gmail.com>
@bors
Copy link
Contributor

bors bot commented Jul 19, 2022

Build failed:

@Aurel300
Copy link
Member

bors r+

bors bot added a commit that referenced this pull request Jul 20, 2022
980: WIP: Iterator tracking issues r=Aurel300 a=vl0w

Some (smaller / bigger) changes needed to enable iterator support
(WIP / tracking PR)

- Moved normalization of constraint param env (for assoc types) for better logging
- Fixed a bug in `SpecGraph`: Preconditions of the base spec were copied to the constrained spec
- Ghost constraint resolving is a bit relaxed (`predicate_may_hold` instead of `predicate_must_hold_considering_regions`) to account for references in associated types. See test `associated_types_6.rs`
- `merge_generics` now also merges lifetimes to accout for lifetimes appearing in `#[refine_trait_spec]`
- Lifetimes in type models are not converted to the anonymous lifetime `'_` anymore
- Do not `#[derive(Copy, Clone]` on type models, because the derive macro "conditionally" implements it when generics are involved. That is, `#[derive(Copy)] struct Foo<T>` adds `impl<T: Copy> Copy for Foo {}`, but we do not want to implement `Copy` only if `T` is `Copy`.
- Quantified variables now support associated types: `forall(|x: Self::SomeAssocType| ...)`

Co-authored-by: Jonas Hansen <ganymed92@gmail.com>
@bors
Copy link
Contributor

bors bot commented Jul 20, 2022

Build failed:

@Aurel300
Copy link
Member

@vakaras Could you have a look at the two failures here? I think they are the last ones before I can merge this and they are happening only in the unsafe core proof version.

@Aurel300 Aurel300 self-assigned this Jul 28, 2022
@Aurel300
Copy link
Member

bors r+

bors bot added a commit that referenced this pull request Jul 29, 2022
980: WIP: Iterator tracking issues r=Aurel300 a=vl0w

Some (smaller / bigger) changes needed to enable iterator support
(WIP / tracking PR)

- Moved normalization of constraint param env (for assoc types) for better logging
- Fixed a bug in `SpecGraph`: Preconditions of the base spec were copied to the constrained spec
- Ghost constraint resolving is a bit relaxed (`predicate_may_hold` instead of `predicate_must_hold_considering_regions`) to account for references in associated types. See test `associated_types_6.rs`
- `merge_generics` now also merges lifetimes to accout for lifetimes appearing in `#[refine_trait_spec]`
- Lifetimes in type models are not converted to the anonymous lifetime `'_` anymore
- Do not `#[derive(Copy, Clone]` on type models, because the derive macro "conditionally" implements it when generics are involved. That is, `#[derive(Copy)] struct Foo<T>` adds `impl<T: Copy> Copy for Foo {}`, but we do not want to implement `Copy` only if `T` is `Copy`.
- Quantified variables now support associated types: `forall(|x: Self::SomeAssocType| ...)`

Co-authored-by: Jonas Hansen <ganymed92@gmail.com>
@bors
Copy link
Contributor

bors bot commented Jul 29, 2022

Build failed:

@Aurel300 Aurel300 mentioned this pull request Aug 8, 2022
bors bot added a commit that referenced this pull request Aug 8, 2022
1123: Snapshot equality r=Aurel300 a=Aurel300

Pulling this out of #980. `@vakaras` 

Co-authored-by: Aurel Bílý <aurel.bily@gmail.com>
Aurel300 pushed a commit to Aurel300/prusti-dev that referenced this pull request Aug 17, 2022
@Aurel300 Aurel300 mentioned this pull request Aug 17, 2022
3 tasks
bors bot added a commit that referenced this pull request Aug 18, 2022
1135: Generics improvements r=Aurel300 a=Aurel300

- [x] Improved associated types resolution (thanks `@vl0w,` from #980). The hope is that this won't erase too many regions...
- [x] Normalise associated types when monomorphising MIR bodies for pure functions.
- [x] Cache encoded pure functions by `DefId` + (full) encoded signature, not just "type parameters".

Co-authored-by: Aurel Bílý <aurel.bily@gmail.com>
Co-authored-by: Jonas <ganymed92@gmail.com>
bors bot added a commit that referenced this pull request Aug 18, 2022
1135: Generics improvements r=Aurel300 a=Aurel300

- [x] Improved associated types resolution (thanks `@vl0w,` from #980). The hope is that this won't erase too many regions...
- [x] Normalise associated types when monomorphising MIR bodies for pure functions.
- [x] Cache encoded pure functions by `DefId` + (full) encoded signature, not just "type parameters".

Co-authored-by: Aurel Bílý <aurel.bily@gmail.com>
Co-authored-by: Jonas <ganymed92@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants