More tests

Author: odersky

tests/neg-custom-args/captures/sep-box.check

@@ -0,0 +1,14 @@
+-- Error: tests/neg-custom-args/captures/sep-box.scala:41:9 ------------------------------------------------------------
+41 |  par(h1.value, h2.value) // error
+   |      ^^^^^^^^
+   |      Separation failure: argument of type  Ref^{xs*}
+   |      to method par: (x: Ref^, y: Ref^): Unit
+   |      corresponds to capture-polymorphic formal parameter x of type  Ref^
+   |      and hides capabilities  {xs*}.
+   |      Some of these overlap with the captures of the second argument with type  Ref^{xs*}.
+   |
+   |        Hidden set of current argument        : {xs*}
+   |        Hidden footprint of current argument  : {xs*}
+   |        Capture set of second argument        : {xs*}
+   |        Footprint set of second argument      : {xs*}
+   |        The two sets overlap at               : {xs*}

tests/neg-custom-args/captures/sep-box.scala

@@ -0,0 +1,41 @@
+import caps.Mutable
+import caps.cap
+
+abstract class LIST[+T]:
+  def isEmpty: Boolean
+  def head: T
+  def tail: LIST[T]
+  def map[U](f: T => U): LIST[U] =
+    if isEmpty then NIL
+    else CONS(f(head), tail.map(f))
+
+class CONS[+T](x: T, xs: LIST[T]) extends LIST[T]:
+  def isEmpty = false
+  def head = x
+  def tail = xs
+object NIL extends LIST[Nothing]:
+  def isEmpty = true
+  def head = ???
+  def tail = ???
+
+class Ref extends Mutable:
+  var x = 0
+  def get: Int = x
+  mut def put(y: Int): Unit = x = y
+
+class Box[+X](val value: X)
+
+def listFresh(n: Int): LIST[Box[Ref^]] =
+  if n == 0 then NIL
+  else
+    val hd = Ref()
+    val tl = listFresh(n - 1)
+    CONS(Box(hd), tl)
+
+def par(x: Ref^, y: Ref^): Unit = ()
+
+def test =
+  val xs = listFresh(10)
+  val h1 = xs.head
+  val h2 = xs.head
+  par(h1.value, h2.value) // error

tests/neg-custom-args/captures/sep-list.check

@@ -0,0 +1,14 @@
+-- Error: tests/neg-custom-args/captures/sep-list.scala:39:6 -----------------------------------------------------------
+39 |  par(h1, h2) // error
+   |      ^^
+   |      Separation failure: argument of type  (h1 : Ref^{xs*})
+   |      to method par: (x: Ref^, y: Ref^): Unit
+   |      corresponds to capture-polymorphic formal parameter x of type  Ref^
+   |      and hides capabilities  {h1}.
+   |      Some of these overlap with the captures of the second argument with type  (h2 : Ref^{xs*}).
+   |
+   |        Hidden set of current argument        : {h1}
+   |        Hidden footprint of current argument  : {h1, xs*}
+   |        Capture set of second argument        : {h2}
+   |        Footprint set of second argument      : {h2, xs*}
+   |        The two sets overlap at               : {xs*}

tests/neg-custom-args/captures/sep-list.scala

@@ -0,0 +1,39 @@
+import caps.Mutable
+import caps.cap
+
+abstract class LIST[+T]:
+  def isEmpty: Boolean
+  def head: T
+  def tail: LIST[T]
+  def map[U](f: T => U): LIST[U] =
+    if isEmpty then NIL
+    else CONS(f(head), tail.map(f))
+
+class CONS[+T](x: T, xs: LIST[T]) extends LIST[T]:
+  def isEmpty = false
+  def head = x
+  def tail = xs
+object NIL extends LIST[Nothing]:
+  def isEmpty = true
+  def head = ???
+  def tail = ???
+
+class Ref extends Mutable:
+  var x = 0
+  def get: Int = x
+  mut def put(y: Int): Unit = x = y
+
+def listFresh(n: Int): LIST[Ref^] =
+  if n == 0 then NIL
+  else
+    val hd = Ref()
+    val tl = listFresh(n - 1)
+    CONS(hd, tl)
+
+def par(x: Ref^, y: Ref^): Unit = ()
+
+def test =
+  val xs = listFresh(10)
+  val h1 = xs.head
+  val h2 = xs.head
+  par(h1, h2) // error

tests/pos-custom-args/captures/sep-pairs.scala

@@ -0,0 +1,21 @@
+import caps.Mutable
+import caps.{cap, consume, use}
+
+class Ref extends Mutable:
+  var x = 0
+  def get: Int = x
+  mut def put(y: Int): Unit = x = y
+
+case class Pair[+A, +B](fst: A, snd: B)
+
+def mkPair: Pair[Ref^, Ref^] =
+  val r1 = Ref()
+  val r2 = Ref()
+  val p_exact: Pair[Ref^{r1}, Ref^{r2}] = Pair(r1, r2)
+  p_exact
+
+def copyPair(@consume @use p: Pair[Ref^, Ref^]): Pair[Ref^, Ref^] =
+  val x: Ref^{p.fst*} = p.fst
+  val y: Ref^{p.snd*} = p.snd
+  Pair(x, y)
+