File tree Expand file tree Collapse file tree 6 files changed +65
-0
lines changed Expand file tree Collapse file tree 6 files changed +65
-0
lines changed Original file line number Diff line number Diff line change 1+ import language .experimental .captureChecking
2+ import caps .*
3+ class Ref (private var x : Int ):
4+ def get = x
5+ def set (y : Int ) = x = y
6+ trait Region extends SharedCapability :
7+ r : Region ^ =>
8+ type R ^
9+ def alloc (x : Int ): Ref ^ {R } = Ref (x)
10+ def subregion [T ](f : (Region { type R >: r.R }) => T ): T =
11+ class R2 extends Region :
12+ type R = r.R
13+ f(new R2 )
14+ def withRegion [T ](f : Region => T ): T = f(new Region {})
15+ @ main def main () =
16+ withRegion : r1 =>
17+ val x = r1.subregion[Ref ^ {r1.R }]: r2 => // error, limitation
18+ var a : Ref ^ {r1.R } = r1.alloc(0 )
19+ var b : Ref ^ {r2.R } = r2.alloc(0 )
20+ val c : Ref ^ {r1.R } = b
21+ a
22+ 0
Original file line number Diff line number Diff line change 1+ import language .experimental .captureChecking
2+ def runOps [C ^ ](ops : List [() -> {C } Unit ]): Unit = ???
3+ def runOps1 [C ^ ](xs : Object ^ {C }): Unit = runOps[{C }](??? ) // ok
4+ def runOps2 [C ^ ](): Unit = runOps[{C }](??? ) // error
Original file line number Diff line number Diff line change 1+ import language .experimental .captureChecking
2+ import language .experimental .separationChecking
3+
4+ import caps .*
5+
6+ object Regions :
7+ class Ref (private var x : Int ):
8+ def get = x
9+ def set (y : Int ) = x = y
10+
11+ trait Region [R ^ ] extends SharedCapability :
12+ region : Region [R ]^ =>
13+ def alloc (value : Int ): Ref ^ {R } = Ref (value)
14+
15+ def subregion [T ](f : [R2 ^ >: R ] => (Region [R2 ]) => T ): T =
16+ val r = new Region [R ] {}
17+ f(r)
18+
19+
20+ object Region :
21+ def apply [T ](f : [R ^ ] => Region [R ] => T ): T =
22+ val r = new Region [{}] {}
23+ f(r)
24+
25+ @ main def main () =
26+ import Region .*
27+ Region : [R ^ ] =>
28+ r1 =>
29+ val x = r1.subregion: [R2 ^ >: R ] =>
30+ r2 =>
31+ val a = r1.alloc(0 )
32+ val b = r2.alloc(0 )
33+ a
34+ 0
Original file line number Diff line number Diff line change 1+ import language .experimental .captureChecking
2+ trait Region [R ^ ]
3+ def id [T ](x : T ): T = ???
4+ def foo [R ^ ](r : Region [R ]): Unit =
5+ val t2 = () => id[Object ^ {R }](??? ) // was error, now ok
You can’t perform that action at this time.
0 commit comments