-
Notifications
You must be signed in to change notification settings - Fork 1.1k
Add Unscoped classifier #24470
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
Merged
Merged
Add Unscoped classifier #24470
Changes from 1 commit
Commits
Show all changes
13 commits
Select commit
Hold shift + click to select a range
1d48e30
Add Unscoped classifier
odersky 54de369
Revert "Represent read-only with a classifier"
odersky da00515
Expand level owner of unscoped fresh caps only where necessary
odersky 48f8c0f
Consume Unscoped caps assigned to outer variables
odersky 21e7a30
Drop `Read` as a classifier
odersky 81d56a5
Fix parsing of derived capabilities
odersky 3cf2e5c
Let implied class capabilities respect read-only
odersky 503ba4a
Don't consider `val _: T = e` as a binding in SepChecks
odersky f43149a
Require that consume parameters are covered by a FreshCap
odersky 2a0ba0e
Don't treat consume class parameters as refining accessors
odersky d54f0fc
Update classifiers.md
odersky f7db3fd
Add more tests for consume constructor parameters
bracevac df8c615
Update internals/syntax.md
bracevac File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Add more tests for consume constructor parameters
- Loading branch information
commit f7db3fd82b956d02f6921ecbcf8800fbc32594c6
There are no files selected for viewing
97 changes: 97 additions & 0 deletions
97
tests/neg-custom-args/captures/paths-complex-consume.scala
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,97 @@ | ||
| import language.experimental.captureChecking | ||
| import language.experimental.separationChecking | ||
| import caps.cap | ||
| import scala.caps.Mutable | ||
|
|
||
| // Create a deeper nesting structure | ||
| class D() | ||
| class C(val d: D^) | ||
| class B(val c: C^) | ||
| class A(consume val b: B^) extends Mutable: | ||
| update def use() = println("Using A") | ||
|
|
||
| // Test 1: Accessing nested fields through a consumed path | ||
| def testNestedFieldsAfterConsume = | ||
| val d: D^ = D() | ||
| val c: C^ = C(d) | ||
| val b: B^ = B(c) | ||
| val a = A(b) | ||
|
|
||
| // After a consumed b, we should be able to access: | ||
| println(a.b) // OK - a owns b | ||
| println(a.b.c) // OK - accessing field of consumed b through a | ||
| println(a.b.c.d) // OK - deeper nesting through consumed path | ||
|
|
||
| // Test 2: Non-trivial prefix accessing a consumed field | ||
| class Container(consume val a: A^) extends Mutable: | ||
| val other: A^ = A(B(C(D()))) | ||
| update def operate() = other.use() | ||
|
|
||
| class Outer(consume val container: Container^) extends Mutable: | ||
| update def execute() = container.operate() | ||
|
|
||
| def testComplexPrefix = | ||
| val d1: D^ = D() | ||
| val c1: C^ = C(d1) | ||
| val b1: B^ = B(c1) | ||
| val a1 = A(b1) | ||
| val container1 = Container(a1) | ||
| val outer = Outer(container1) | ||
|
|
||
| // Non-trivial prefix: outer.container.a (where 'a' was consumed by container) | ||
| println(outer.container) // OK - outer consumed container | ||
| println(outer.container.a) // OK - accessing consumed field through prefix | ||
| println(outer.container.a.b) // OK - and then its nested fields | ||
| println(outer.container.a.b.c) // OK - even deeper | ||
| println(outer.container.a.b.c.d) // OK - deepest level | ||
|
|
||
| println(container1) // error | ||
| println(a1) // error | ||
|
|
||
| // Test 3: Multiple consume parameters with nested access | ||
| class Multi(consume val b1: B^, consume val b2: B^) extends Mutable: | ||
| val b3: B^ = B(C(D())) | ||
| update def combine() = () | ||
|
|
||
| def testMultipleConsume = | ||
| val b1: B^ = B(C(D())) | ||
| val b2: B^ = B(C(D())) | ||
| val multi = Multi(b1, b2) | ||
|
|
||
| // All of these should work: | ||
| println(multi.b1) // OK | ||
| println(multi.b1.c) // OK - nested field of consumed b1 | ||
| println(multi.b1.c.d) // OK - deeper nesting | ||
| println(multi.b2) // OK | ||
| println(multi.b2.c) // OK - nested field of consumed b2 | ||
| println(multi.b2.c.d) // OK - deeper nesting | ||
| println(multi.b3.c.d) // OK - non-consumed field | ||
|
|
||
| println(b1) // error | ||
| println(b2) // error | ||
|
|
||
| // Test 4: Consume at multiple levels with complex paths | ||
| class Top(consume val outer: Outer^) extends Mutable: | ||
| update def topAction() = outer.execute() | ||
|
|
||
| def testMultiLevelConsume = | ||
| val d2: D^ = D() | ||
| val c2: C^ = C(d2) | ||
| val b2: B^ = B(c2) | ||
| val a2 = A(b2) | ||
| val container2 = Container(a2) | ||
| val outer2 = Outer(container2) | ||
| val top = Top(outer2) | ||
|
|
||
| // Very deep path through multiple consume levels: | ||
| println(top.outer) // OK - top consumed outer | ||
| println(top.outer.container) // OK - continue through path | ||
| println(top.outer.container.a) // OK - container consumed a | ||
| println(top.outer.container.a.b) // OK - a consumed b | ||
| println(top.outer.container.a.b.c) // OK - nested field | ||
| println(top.outer.container.a.b.c.d) // OK - deepest field | ||
|
|
||
| println(a2) // error | ||
| println(container2) // error | ||
| println(outer2) // error | ||
| println(top) // ok |
56 changes: 56 additions & 0 deletions
56
tests/neg-custom-args/captures/paths-derivedcaps-consume.scala
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,56 @@ | ||
| import language.experimental.captureChecking | ||
| import language.experimental.separationChecking | ||
| import caps.* | ||
|
|
||
| class Foo extends ExclusiveCapability, Classifier | ||
|
|
||
| // Testing with various DerivedCapabilities | ||
| class D | ||
| class C(val d: D) | ||
| class B(val c: C) extends Foo, Mutable: | ||
| update def foo() = println("foo") | ||
| class A(consume val b: B^) extends Mutable: | ||
| update def bar() = b.foo() | ||
| class A2(consume val b: B^) extends Mutable: | ||
| update def bar() = b.foo() | ||
| class A3(consume var b: B^) extends Mutable: | ||
| update def bar() = b.foo() | ||
| class A4(consume val b: A2^{cap.only[Foo]}) extends Mutable: // FIXME needs to be classified as Foo, too | ||
| update def bar() = b.b.foo() | ||
|
|
||
| // Test: Access nested fields (suffix paths) after consume | ||
| def testSuffixPaths = | ||
| val d: D = D() | ||
| val c: C = C(d) | ||
| val b: B^ = B(c) | ||
| val a1 = A(b) | ||
| val b2: B^ = B(c) | ||
| val a2 = A2(b2) | ||
| val b3: B^ = B(c) | ||
| val a3 = A3(b3) | ||
| val b4: B^ = B(c) | ||
| val a22 = A2(b4) | ||
| //val a4 = A4(a22) // FIXME should work? | ||
| val b5: B^{cap.only[Foo]} = B(c) | ||
| val a5 = A(b5) | ||
| val b6: B^{cap.only[Foo]} = B(c) | ||
| val a222 = A2(b6) | ||
| //val a6 = A4(a222) // FIXME should work? | ||
|
|
||
|
|
||
| println(a1.b) // ok | ||
| println(a2.b) // ok | ||
| println(a3.b) // ok | ||
| //println(a4.b) // ok needs fixing | ||
| //println(a4.b.b) // ok needs fixing | ||
| println(a5.b) // ok | ||
| // println(a6.b) // ok needs fixing | ||
| // println(a6.b.b) // ok needs fixing | ||
|
|
||
| println(b) // error | ||
| println(b2) // error | ||
| println(b3) // error | ||
| println(b4) // error | ||
| println(b5) // error | ||
| println(b6) // error | ||
| //println(a222) // should error, but doesn't work yet |
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Note: We still have some quirks w.r.t. classifiers which should be addressed in a follow-up PR.