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.

Sign up for GitHub

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

Jump to bottom

Mutability translation with mutable cells #164

Closed
wants to merge 54 commits into from
Closed

Mutability translation with mutable cells #164

wants to merge 54 commits into from

Conversation

yannbolliger
Copy link
Collaborator

@yannbolliger yannbolliger commented Jun 25, 2021 •
edited
Loading

This PR introduces the Mutability Translation presented in my thesis.

Closes #157. Closes #140. Closes #99.

Summary
The PR contains roughly these features/changes and all the refactoring/fixing that goes along:

  • Mutability is modelled with a mutable cell case class for all ADT fields and local variables: 
    case class MutCell[@mutable T](var t: T)
  • var and mutable flags are thus removed from the user-interface.
  • Mutable references are extracted and verified by means of the mutable cells.

This PR supersedes the two former mutability-related PRs #158 #159.
It contains the grand majority of their changes though.

Two tests currently fail in the test suite, trait_bounds::verification and type_class::verification, due to the solver timing out, documented in this Stainless issue: epfl-lara/stainless#1093.

@yannbolliger yannbolliger requested a review from romac June 25, 2021 13:26
This was referenced Jun 25, 2021
Closed
Closed
@yannbolliger yannbolliger force-pushed the mutable-cells branch 2 times, most recently from 9093815 to efcdb65 Compare June 25, 2021 15:23
@yannbolliger yannbolliger requested a review from gsps July 16, 2021 06:55
@yannbolliger yannbolliger force-pushed the mutable-cells branch 4 times, most recently from 67e4839 to cc8d0d4 Compare July 22, 2021 12:32
@yannbolliger
Make all params var, all tparams mutable, all functions pure.
0674104
@yannbolliger
Copy mutable params of tparam type.
20acaf5
@yannbolliger
Adapt tests.
65bea74
@yannbolliger
Fresh copy on immutable/aliasable/safe borrow.
f85423f
@yannbolliger
Fresh copy the return value.
61e5bda
@yannbolliger
Refactor to reduce unnecessary fresh copies.
e099413
@yannbolliger
Remove mutable and var flag form user-facing side.
61823a8
@yannbolliger
Fix the map for mutable value types.
39a1a9a
@yannbolliger
Improve documentation.
da0fb07
@yannbolliger
Fresh copy let var initializer.
2fb5f06 
This is safe becaues it consumes whatever is the initializer.
@yannbolliger
Don't fresh copy matches/ifs.
dbef2a3 
(They fresh copy the last expression of each arm themselves.)
@yannbolliger
Add clone test case with fresh copy.
67adab8
@yannbolliger
Add negative test case.
b12c594
@yannbolliger
Be sure to fresh copy cloned objects.
d374f11
@yannbolliger
Add cast correctness test case.
9da10f8
@yannbolliger
Improve comment.
87b85cf
@yannbolliger
Add benchmarks for mutable references.
4a67625
@yannbolliger
Extract mutable references (without drop/reassignment)
0c8a769
@yannbolliger
Wrap all fields in MutCells.
82bb074
@yannbolliger
Support mutably borrowing fields.
a273631
@yannbolliger
Add test with mutable pattern match.
53c35d1
@yannbolliger
Support pattern match on mutably borrowed fields.
5f409f7
@yannbolliger
Make linter happy.
43d5684
@yannbolliger
Fix tuples to use mutcells.
35420c4
@yannbolliger
Add test (large) with tuples.
de9f1d1
@yannbolliger
Fix pattern matching with mutable refs.
cd1101e
@yannbolliger
Check for deep mutability before fresh copy.
3b9b447
@yannbolliger
Fix purity detection for nested mutable types.
9d04ef8
@yannbolliger
Fix mutable by-value params containing mutable refs.
b6238a3
@yannbolliger
Fix mutable borrow of tuple field.
5009bf5
@yannbolliger
Add test with mutable tuples.
c004e7a
@yannbolliger
Add test with by value type containing mut ref.
f240d19
@yannbolliger
Adapt translation
6705102
@yannbolliger
Improve naming and docs.
cbcb0dc
@yannbolliger
Fix cloning for mutable cells.
5636145
@yannbolliger
Add support for mutating tuples.
050369b
@yannbolliger
Update demo examples.
db869c5
@yannbolliger
Fix specs on mut self methods in implementations.
67b596d
@yannbolliger
Add thesis example to demo folder.
d08a1df
@yannbolliger
Add test for nested mutable cells.
ab6801c
@yannbolliger
Fix nesting of mutable cells.
66c7658
@yannbolliger
Add old helper.
6376e1a
@yannbolliger
Implement mem::replace and add test.
99840ff
@yannbolliger
Disable two tests that time out due to Stainless bug
1df1d28
@yannbolliger
Copy link
Collaborator Author

Closing this as an archival action.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@romac romac Awaiting requested review from romac

@gsps gsps Awaiting requested review from gsps

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Mutable fields with generics Mutable references Infer if fields are mutated
1 participant
@yannbolliger