Commit 729d743
authored
Separation checking for product types (#22539)
This is based on #22588 and contains changes to make product types
containing fresh entities work (at least in simple cases). There's a
neat combination with both path capabilities and reach capabilities
which makes this work.
In short, if we have
```scala
class Ref { var current: Int }
case class Pair[+A, +B](fst: A, snd: B)
```
then we can form a `Pair[Ref^, Ref^]`:
```scala
val r1 = Ref()
val r2 = Ref()
val p_exact: Pair[Ref^{r1}, Ref^{r2}] = Pair(r1, r2)
val p: Pair[Ref^, Ref^] = p_exact
```
And if `p` has this type, then we can also take it apart:
```scala
val x = p.fst
val y = p.snd
```
With types added, this is
```scala
val x: Ref^{p.fst*} = p.fst
val y: Ref^{p.snd*} = p.snd
```
That is, we can get at the position of the boxed first element with
`p.fst` and we can access what's in the box via `p.fst*`.
Furthermore, `p.fst*` is known to be separate from `p.snd*`, so this
means we can form another pair from them:
```scala
val p2: Pair[Ref^, Ref^] = Pair(x, y)
```
In short, separation is preserved by forming products and taking them
apart. It took quite a bit of work to get there.File tree
218 files changed
+6190
-1917
lines changed- compiler
- src/dotty/tools
- backend/jvm
- dotc
- ast
- cc
- config
- core
- parsing
- printing
- reporting
- sbt
- transform
- init
- typer
- util
- test/dotty/tools/dotc
- docs/_docs/internals
- library/src/scala
- annotation/internal
- project
- scala2-library-cc/src/scala/collection
- immutable
- mutable
- tests
- neg-custom-args/captures
- caseclass
- neg
- pos-custom-args/captures
- pos-special/stdlib
- run-custom-args/captures/colltest5
Some content is hidden
Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.
218 files changed
+6190
-1917
lines changed| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
1 | 1 | | |
2 | | - | |
3 | | - | |
| 2 | + | |
| 3 | + | |
4 | 4 | | |
5 | 5 | | |
Lines changed: 1 addition & 1 deletion
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
285 | 285 | | |
286 | 286 | | |
287 | 287 | | |
288 | | - | |
| 288 | + | |
289 | 289 | | |
290 | 290 | | |
291 | 291 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
2262 | 2262 | | |
2263 | 2263 | | |
2264 | 2264 | | |
| 2265 | + | |
| 2266 | + | |
2265 | 2267 | | |
2266 | 2268 | | |
2267 | 2269 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
759 | 759 | | |
760 | 760 | | |
761 | 761 | | |
762 | | - | |
| 762 | + | |
763 | 763 | | |
764 | 764 | | |
765 | 765 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
206 | 206 | | |
207 | 207 | | |
208 | 208 | | |
| 209 | + | |
| 210 | + | |
209 | 211 | | |
210 | 212 | | |
211 | 213 | | |
| |||
332 | 334 | | |
333 | 335 | | |
334 | 336 | | |
| 337 | + | |
335 | 338 | | |
336 | 339 | | |
337 | 340 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
42 | 42 | | |
43 | 43 | | |
44 | 44 | | |
45 | | - | |
| 45 | + | |
| 46 | + | |
46 | 47 | | |
47 | 48 | | |
48 | 49 | | |
| |||
0 commit comments