Skip to content

Commit 633d548

Browse files
committed
Add more tests for consume along paths
1 parent aa69c58 commit 633d548

File tree

3 files changed

+94
-0
lines changed

3 files changed

+94
-0
lines changed
Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
import language.experimental.captureChecking
2+
import language.experimental.separationChecking
3+
import caps.cap
4+
5+
class B
6+
7+
class A(consume val b: B^):
8+
val bb: B^ = B()
9+
10+
class C(consume val a: A^):
11+
val aa: A^ = A(B())
12+
13+
// Test deep nested access paths
14+
def testDeepPaths =
15+
val b: B^ = B()
16+
val a = A(b)
17+
val c = C(a)
18+
19+
// All these should work - accessing through ownership chain
20+
println(c.a) // c owns a
21+
println(c.a.b) // c owns a, a owns b
22+
println(c.a.bb) // c owns a, accessing other field
23+
println(c.aa) // accessing other field of c
24+
println(c.aa.b) // accessing nested field through c.aa
Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
import language.experimental.captureChecking
2+
import language.experimental.separationChecking
3+
import caps.cap
4+
5+
class B
6+
7+
class A(consume val b: B^):
8+
val bb: B^ = B()
9+
10+
class C(consume val a: A^):
11+
val aa: A^ = A(B())
12+
13+
// Test: After consuming b into a, then consuming a into c,
14+
// we should be able to access c.a.b (nested field selection)
15+
def testNestedAccess =
16+
val b: B^ = B()
17+
val a = A(b)
18+
println(a.b) // OK - a consumed b, accessing through a
19+
val c = C(a)
20+
println(c.a) // Should be OK - c consumed a, accessing through c
21+
println(c.a.b) // Should be OK - accessing b through c.a, where c owns a and a owns b
22+
23+
// Test: The deeper path c.a.b should work even though a was consumed
24+
def testDeepPath =
25+
val b: B^ = B()
26+
val a = A(b)
27+
val c = C(a)
28+
// At this point:
29+
// - b was consumed by a (so we can't use b directly)
30+
// - a was consumed by c (so we can't use a directly)
31+
// But we should be able to access:
32+
println(c.a.b) // OK - full path through ownership chain
33+
println(c.a.bb) // OK - other field of c.a
Lines changed: 37 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,37 @@
1+
import language.experimental.captureChecking
2+
import language.experimental.separationChecking
3+
import caps.cap
4+
5+
// Create a deep nesting structure for testing suffix paths
6+
class D
7+
class C(val d: D^)
8+
class B(val c: C^)
9+
class A(consume val b: B^)
10+
11+
// Test 1: Simple suffix paths after consume
12+
def test1 =
13+
val d: D^ = D()
14+
val c: C^ = C(d)
15+
val b: B^ = B(c)
16+
val a = A(b)
17+
18+
// After 'a' consumes 'b', access nested fields:
19+
println(a.b) // OK - consumed field
20+
println(a.b.c) // OK - suffix: .c after consumed field
21+
println(a.b.c.d) // OK - suffix: .c.d after consumed field
22+
23+
// Test 2: Non-consume wrapper with consumed inner field
24+
class Holder(val a: A^) // Note: NOT consume
25+
26+
def test2 =
27+
val d: D^ = D()
28+
val c: C^ = C(d)
29+
val b: B^ = B(c)
30+
val a = A(b)
31+
val holder = Holder(a)
32+
33+
// Access through holder.a.b where b was consumed by a:
34+
println(holder.a) // OK - not consumed
35+
println(holder.a.b) // OK - accessing consumed field through prefix
36+
println(holder.a.b.c) // OK - suffix .c
37+
println(holder.a.b.c.d) // OK - suffix .c.d

0 commit comments

Comments
 (0)