-
Notifications
You must be signed in to change notification settings - Fork 1.1k
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Check separation of different parts of a declared type.
- Loading branch information
Showing
9 changed files
with
222 additions
and
48 deletions.
There are no files selected for viewing
This file contains 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
This file contains 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 |
|---|---|---|
| @@ -1,13 +1,7 @@ | ||
| -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt-depfun.scala:10:43 ---------------------------------- | ||
| 10 | val dc: ((Str^{y, z}) => Str^{y, z}) = ac(g()) // error // error sepcheck | ||
| 10 | val dc: ((Str^{y, z}) => Str^{y, z}) = ac(g()) // error | ||
| | ^^^^^^^ | ||
| | Found: Str^{} ->{ac, y, z} Str^{y, z} | ||
| | Required: Str^{y, z} ->{fresh} Str^{y, z} | ||
| | | ||
| | longer explanation available when compiling with `-explain` | ||
| -- Error: tests/neg-custom-args/captures/capt-depfun.scala:10:24 ------------------------------------------------------- | ||
| 10 | val dc: ((Str^{y, z}) => Str^{y, z}) = ac(g()) // error // error sepcheck | ||
| | ^^^^^^^^^^^^^^^^^^^^^^^^^^ | ||
| | Separation failure: Str^{y, z} => Str^{y, z} captures a root element hiding {ac, y, z} | ||
| | and also refers to {y, z}. | ||
| | The two sets overlap at {y, z} |
This file contains 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
This file contains 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 |
|---|---|---|
| @@ -1,10 +1,25 @@ | ||
| -- Error: tests/neg-custom-args/captures/reaches2.scala:8:10 ----------------------------------------------------------- | ||
| 8 | ps.map((x, y) => compose1(x, y)) // error // error | ||
| | ^ | ||
| |reference ps* is not included in the allowed capture set {} | ||
| |of an enclosing function literal with expected type ((box A ->{ps*} A, box A ->{ps*} A)) -> box (x$0: A^?) ->? A^? | ||
| -- Error: tests/neg-custom-args/captures/reaches2.scala:8:13 ----------------------------------------------------------- | ||
| 8 | ps.map((x, y) => compose1(x, y)) // error // error | ||
| | ^ | ||
| |reference ps* is not included in the allowed capture set {} | ||
| |of an enclosing function literal with expected type ((box A ->{ps*} A, box A ->{ps*} A)) -> box (x$0: A^?) ->? A^? | ||
| -- Error: tests/neg-custom-args/captures/reaches2.scala:10:10 ---------------------------------------------------------- | ||
| 10 | ps.map((x, y) => compose1(x, y)) // error // error // error | ||
| | ^ | ||
| |reference ps* is not included in the allowed capture set {} | ||
| |of an enclosing function literal with expected type ((box A ->{ps*} A, box A ->{ps*} A)) -> box (x$0: A^?) ->? A^? | ||
| -- Error: tests/neg-custom-args/captures/reaches2.scala:10:13 ---------------------------------------------------------- | ||
| 10 | ps.map((x, y) => compose1(x, y)) // error // error // error | ||
| | ^ | ||
| |reference ps* is not included in the allowed capture set {} | ||
| |of an enclosing function literal with expected type ((box A ->{ps*} A, box A ->{ps*} A)) -> box (x$0: A^?) ->? A^? | ||
| -- Error: tests/neg-custom-args/captures/reaches2.scala:10:31 ---------------------------------------------------------- | ||
| 10 | ps.map((x, y) => compose1(x, y)) // error // error // error | ||
| | ^ | ||
| | Separation failure: argument of type (x$0: A) ->{y} box A^? | ||
| | to method compose1: [A, B, C](f: A => B, g: B => C): A ->{f, g} C | ||
| | corresponds to capture-polymorphic formal parameter g of type box A^? => box A^? | ||
| | and captures {ps*}, but this capability is also passed separately | ||
| | in the first argument with type (x$0: A) ->{x} box A^?. | ||
| | | ||
| | Capture set of first argument : {x} | ||
| | Hidden set of current argument : {y} | ||
| | Footprint of first argument : {x, ps*} | ||
| | Hidden footprint of current argument : {y, ps*} | ||
| | Declared footprint of current argument: {} | ||
| | Undeclared overlap of footprints : {ps*} |
This file contains 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 |
|---|---|---|
| @@ -1,9 +1,11 @@ | ||
| import language.`3.8` // sepchecks on | ||
|
|
||
| class List[+A]: | ||
| def map[B](f: A -> B): List[B] = ??? | ||
|
|
||
| def compose1[A, B, C](f: A => B, g: B => C): A ->{f, g} C = | ||
| z => g(f(z)) | ||
|
|
||
| def mapCompose[A](ps: List[(A => A, A => A)]): List[A ->{ps*} A] = | ||
| ps.map((x, y) => compose1(x, y)) // error // error | ||
| ps.map((x, y) => compose1(x, y)) // error // error // error | ||
|
|
This file contains 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
This file contains 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 |
|---|---|---|
| @@ -1,10 +1,28 @@ | ||
| import language.future // sepchecks on | ||
|
|
||
|
|
||
| def foo(xs: List[() => Unit], y: Object^) = ??? | ||
|
|
||
| def bar(x: (Object^, Object^)): Unit = ??? | ||
|
|
||
| def Test(c: Object^) = | ||
| val xs: List[() => Unit] = (() => println(c)) :: Nil | ||
| println(c) // error | ||
|
|
||
| def Test2(c: Object^) = | ||
| def Test2(c: Object^, d: Object^): Unit = | ||
| foo((() => println(c)) :: Nil, c) // error | ||
| val x1: (Object^, Object^) = (c, c) // error | ||
| val x2: (Object^, Object^{d}) = (d, d) // error | ||
|
|
||
| def Test3(c: Object^, d: Object^) = | ||
| val x: (Object^, Object^) = (c, d) // ok | ||
|
|
||
| def Test4(c: Object^, d: Object^) = | ||
| val x: (Object^, Object^{c}) = (d, c) // ok | ||
|
|
||
| def Test5(c: Object^, d: Object^): Unit = | ||
| bar((c, d)) // ok | ||
|
|
||
| def Test6(c: Object^, d: Object^): Unit = | ||
| bar((c, c)) // error | ||
|
|
This file contains 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
This file contains 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