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

Add freeze operator #2941

Closed
eholk opened this issue Jul 17, 2012 · 4 comments
Closed

Add freeze operator #2941

eholk opened this issue Jul 17, 2012 · 4 comments
Labels
A-type-system Area: Type system E-hard Call for participation: Hard difficulty. Experience needed to fix: A lot.
Milestone

Comments

@eholk
Copy link
Contributor

eholk commented Jul 17, 2012

It'd be nice to be able to treat things as const. Since this involves changing the type, it will probably require language support, although it might be possible to do it with reflection.

@eholk
Copy link
Contributor Author

eholk commented Jul 17, 2012

@graydon suggests calling it const as an expression.

@nikomatsakis
Copy link
Contributor

My current thoughts on this are that freezing and thawing are kind of unnecessary, but we need to make a few changes to mutability and unique ptrs to make this all work. Right now, mutability for default fields (those without an explicit mut qualifier) is inherited from the container. So if you write:

let mut v = {x: 3, y: 4};

You can indeed mutate v.x and v.y even though the fields are not declared mutable. This seems surprising at first but is a logical consequence of the variable v being mutable; after all, if I wanted to do v.x = x1 I could always write v = {x: x1 with v}. However, if you write:

let mut v = ~{x: 3, y: 4};

then, currently, x and y are truly immutable. This is true despite the fact that v is a unique box, and hence I can write something like v = ~{x: x1 with *v} which is basically the same as what we saw before in effect. At some point,
@pcwalton and I both independently came to the conclusion that we ought to "inherit" mutability through unique pointers in the same way.

We also already have the rule that borrowck allows you to borrow the contents of a mutable unique ptr as immutable. That is, we can do something like this:

let x: ~mut int = ~mut 5;
let y: &int = &*x;       // *Immutable* int

This works because borrowck will detect and prevent any attempt to modify *x while y is live.

Anyway, if we did this, then properly designed data structures can be "frozen" and "thawed" in a rather automatic way, just by borrowing and moving them. At least I think they can. I'll write up an example in a gist and post it.

@nikomatsakis
Copy link
Contributor

Here is a gist explaining the idea in a bit more detail: https://gist.github.com/3130874

@nikomatsakis
Copy link
Contributor

The send_map module shows how this can work now. Fixed.

bors pushed a commit to rust-lang-ci/rust that referenced this issue May 15, 2021
bors pushed a commit to rust-lang-ci/rust that referenced this issue May 15, 2021
RalfJung pushed a commit to RalfJung/rust that referenced this issue Jun 29, 2023
Update ui test crate

The main changes:

* we don't need to roll our own `status_emitter` anymore
* there's only one way to filter now: with the closure passed to `run_tests_generic`
celinval pushed a commit to celinval/rust-dev that referenced this issue Jun 4, 2024
## What's Changed
* Rust toolchain upgraded to `nightly-2023-12-14` by @tautschnig and
@adpaco-aws

**Full Changelog**:
model-checking/kani@kani-0.42.0...kani-0.43.0

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
A-type-system Area: Type system E-hard Call for participation: Hard difficulty. Experience needed to fix: A lot.
Projects
None yet
Development

No branches or pull requests

2 participants