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

Refactoring #13

Merged
merged 78 commits into from
Mar 3, 2025
Merged

Refactoring #13

merged 78 commits into from
Mar 3, 2025

Conversation

zgrannan
Copy link
Collaborator

@zgrannan zgrannan commented Feb 20, 2025

Too many refactorings to count

@zgrannan zgrannan marked this pull request as ready for review February 28, 2025 00:02
@zgrannan zgrannan changed the title Current development branch (WIP) Refactoring Feb 28, 2025
@zgrannan
Copy link
Collaborator Author

zgrannan commented Mar 2, 2025

@Aurel300 let me know when you have Prusti working using the latest version of this branch, I'll merge it into master

@Aurel300
Copy link
Member

Aurel300 commented Mar 3, 2025

@zgrannan I think it all works, but I still need this patch:

--- a/src/borrow_pcg/borrow_pcg_expansion.rs
+++ b/src/borrow_pcg/borrow_pcg_expansion.rs
@@ -34,7 +34,7 @@ use crate::{
 /// *x.f.b}
 #[derive(PartialEq, Eq, Clone, Debug, Hash)]
 pub struct ExpansionOfBorrowed<'tcx, P = LocalNode<'tcx>> {
-    pub(crate) base: P,
+    pub base: P,
     pub(crate) expansion: BorrowExpansion<'tcx>,
 }

Or should I be accessing this field differently? I use this field when processing BorrowPCGExpansions to emit folds/unfolds.

@zgrannan
Copy link
Collaborator Author

zgrannan commented Mar 3, 2025

@zgrannan I think it all works, but I still need this patch:

--- a/src/borrow_pcg/borrow_pcg_expansion.rs
+++ b/src/borrow_pcg/borrow_pcg_expansion.rs
@@ -34,7 +34,7 @@ use crate::{
 /// *x.f.b}
 #[derive(PartialEq, Eq, Clone, Debug, Hash)]
 pub struct ExpansionOfBorrowed<'tcx, P = LocalNode<'tcx>> {
-    pub(crate) base: P,
+    pub base: P,
     pub(crate) expansion: BorrowExpansion<'tcx>,
 }

Or should I be accessing this field differently? I use this field when processing BorrowPCGExpansions to emit folds/unfolds.

I just added a .base() method for ExpansioOfBorrowed, so you can use that

impl<P: Copy> ExpansionOfBorrowed<'_, P> {
pub fn base(&self) -> P {
self.base
}
}

@zgrannan zgrannan merged commit bdbdeb4 into main Mar 3, 2025
8 checks passed
@zgrannan zgrannan deleted the zgrannan/next branch March 3, 2025 19:42
@zgrannan zgrannan restored the zgrannan/next branch March 3, 2025 19:43
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