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

Support mutable generics and remove var flag #158

Closed
wants to merge 18 commits into from
Closed

Conversation

yannbolliger
Copy link
Collaborator

@yannbolliger yannbolliger commented May 14, 2021

This PR is the result of many discussions with @romac @gsps @vkuncak. There was also great support by @jad-hamza on the Stainless side of things, thanks!

The PR brings the mutability support of rust-stainless closer to Rust's semantics by dropping the var annotation on fields.

Closes #157. Closes #99 because now, all fields can be mutated with mut at binding.
This is a big step for #92 and brings us closer to #140.

Theory
The safety of what we do in this PR, mainly on this single line change is guaranteed by the following theoretical argument:

  • Rust has either 1 mutable reference or many shared, immutable, aliasable borrows
  • Stainless allows 1 reference to a mutable object but we can create aliases with freshCopy at our own risk
  • Thanks to Rust, we know that when we borrow something immutably (BorrowKind::Shared), it’s aliasable and we can therefore safely freshCopy it.

There are 3 other places, where freshCopy is/was introduced:

  • For function parameters that are taken by-value. It's safe to freshCopy them because the by-value/move semantics guarantee that they are owned i.e. there are no other references to them.

  • Return values are freshCopy'd to avoid aliasing. This is safe (currently) because we only support returning by-value or by shared, immutable reference.

  • stainless::Map is a special case. In order to get support for mutable value types, we needed to refactor the map extraction. Behind the immutable Rust interface that resides in libstainless the map is now extracted as MutableMap. To combat aliasing, the insert and remove method now consume self. This allows on the extraction side, to extract for example let b = a.insert(0, 1); as the following in Scala:

val b: MutableMap[UInt32, Option[UInt32]] = freshCopy({
  val map: MutableMap[UInt32, Option[UInt32]] = freshCopy(a)
  map(0) = Some[UInt32](1)
  map
})

@yannbolliger yannbolliger requested a review from romac May 14, 2021 11:52
stainless_extraction/src/expr/mod.rs Outdated Show resolved Hide resolved
stainless_extraction/src/lib.rs Show resolved Hide resolved
@yannbolliger
Copy link
Collaborator Author

This is now finished, CI will pass once the latest stainless-noxt is published.
@gsps @romac please review. 🙏

@yannbolliger yannbolliger force-pushed the mut-generics branch 3 times, most recently from 7ca4d59 to 8956844 Compare May 26, 2021 13:52
@yannbolliger yannbolliger changed the base branch from master to refactor June 7, 2021 15:43
Base automatically changed from refactor to master June 8, 2021 10:12
@yannbolliger yannbolliger changed the base branch from master to id-helpers June 24, 2021 10:37
Base automatically changed from id-helpers to master June 24, 2021 10:46
@yannbolliger
Copy link
Collaborator Author

Closing in favour of #164. Most of the changes here are contained there.

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.

Mutable fields with generics Infer if fields are mutated
3 participants