Skip to content

Commit

Permalink
Improves examples
Browse files Browse the repository at this point in the history
  • Loading branch information
MattisKra committed Oct 19, 2023
1 parent 8976dd7 commit c8acc66
Show file tree
Hide file tree
Showing 49 changed files with 129 additions and 174 deletions.
47 changes: 33 additions & 14 deletions effekt/jvm/src/test/scala/effekt/TyperTests.scala
Original file line number Diff line number Diff line change
Expand Up @@ -219,15 +219,6 @@ abstract class AbstractTyperTests extends munit.FunSuite {
assertNoDiff(symbols.TypePrinter.show(got), expected, clue)
}

// def assertCaptureType(name: String, expected: String, clue: => Any = "capture types don't match"): Unit = {
// val syms = R.module.terms(name)
// assert(syms.size == 1, s"There is a unique symbol named '${name}'.")
// val sym = syms.head
// assert(sym.isInstanceOf[symbols.Captures], s"${sym} is a capture symbol.")
// val got = C.annotation(Annotations.Captures, sym.asInstanceOf[symbols.BlockSymbol])
// assertNoDiff(symbols.TypePrinter.show(got), expected, clue)
// }

// TODO further assertions (e.g. for captures etc) on the context
}

Expand Down Expand Up @@ -269,7 +260,7 @@ class TyperTests extends AbstractTyperTests {
testTyperFile("Box inference tests")("examples/pts/pos/boxInference.effekt"){
C => {
C.assertBlockType("func1", "Int => Int at {} => Int")
C.assertBlockType("func2", "List[Int => Int at {}] => Int")
// C.assertBlockType("func2", "List[Int => Int at {}] => Int")
}
}

Expand All @@ -282,13 +273,23 @@ class TyperTests extends AbstractTyperTests {
}
}

testTyperFile("Effectful box test")("examples/pts/pos/effectfulBox.effekt") {
C => C.assertValueType("boxed", "() => Int / { Eff } at {}")
}

testTyperFile("Effect tests")("examples/pts/pos/effects.effekt"){
C => {
C.assertBlockType("func1", "() => Int / { Eff1 }")
C.assertBlockType("func2", "() => Int / { Eff1, Eff2 }")
}
}

testTyperFile("Multiple uses of block parameter")("examples/pts/pos/functionMultipleUses.effekt") {
C => {
C.assertBlockType("func", "Int => Int")
}
}

testTyperFile("Interface tests")("examples/pts/pos/interface.effekt"){
C => {
C.assertBlockType("interfaceParam", "Constant[Int]")
Expand All @@ -304,6 +305,27 @@ class TyperTests extends AbstractTyperTests {
}
}

testTyperFile("Nested wildcards tests")("examples/pts/pos/nestedWildcards.effekt") {
C => {
C.assertBlockType("f", "Int => Int")
C.assertValueType("y", "Int")
}
}

testTyperFile("Parametric box tests")("examples/pts/pos/parametricBox.effekt") {
C => {
C.assertValueType("boxed", "[A]A => Int at {}")
}
}

testTyperFile("Recursive function tests")("examples/pts/pos/recursiveFunction.effekt") {
C => C.assertBlockType("func", "Int => Int")
}

testTyperFile("TypeParam tests")("examples/pts/pos/typeParameter.effekt") {
C => C.assertBlockType("id", "[A]A => A")
}

testTyperFile("Value type tests")("examples/pts/pos/valueTypes.effekt"){
C => {
C.assertValueType("value1", "Int")
Expand All @@ -312,8 +334,5 @@ class TyperTests extends AbstractTyperTests {
}
}


testTyperFile("Debug")("examples/pts/test24.effekt"){
C => C.assertBlockType("func", "")
}

}
2 changes: 1 addition & 1 deletion examples/pts/test23.effekt → examples/pts/FIXME.effekt
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ effect Eff(): Unit

def run{x: _}: Int = {
val a: Int = x(1)
//def y: Int => Int / Eff = x
def y: Int => Int / Eff = x
1
}

Expand Down
4 changes: 2 additions & 2 deletions examples/pts/neg/blockParameters.check
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
[error] examples\pts\neg\blockTypes.effekt:5:1: Cannot fully infer type for func: {_} => String
def func{param: _} = "test"
[error] examples/pts/neg/blockParameters.effekt:5:1: Cannot fully infer type for func: {_} => String
def func{param: _} = "test"
^^^^^^^^^^^^^^^^^^^^^^^^^^^
6 changes: 3 additions & 3 deletions examples/pts/neg/boxInference.check
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
[error] examples/pts/neg/boxInference.effekt:12:24: Capture parameter count does not match Int => Int / { Eff } vs. Int => Int
val res = func(box f)
^
[error] examples/pts/neg/boxInference.effekt:8:6: Cannot infer function type for callee.
(unbox boxedParam)(1)
^
6 changes: 3 additions & 3 deletions examples/pts/neg/boxParametricFunction.check
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
[error] examples/pts/neg/boxParametricFunction.effekt:12:24: Type parameter count does not match [A]A => A vs. Int => Int
val res = func(box f)
^
[error] examples/pts/neg/boxParametricFunction.effekt:8:6: Cannot infer function type for callee.
(unbox boxedParam)(1)
^
3 changes: 3 additions & 0 deletions examples/pts/neg/effectInBlockParam.check
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
[error] examples/pts/neg/effectInBlockParam.effekt:6:5: EffectSetWildcard is not allowed in block parameter
func()
^
3 changes: 3 additions & 0 deletions examples/pts/neg/externDefCaptures.check
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
[error] examples/pts/neg/externDefCaptures.effekt:3:10: Capture set wildcards are not allowed here!
extern _ def func(x: Int): Int = "test"
^
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
module examples/pts/neg/externDefCaptures

extern _ def func(x: Int): Int = "test"

def main() = {
Expand Down
3 changes: 3 additions & 0 deletions examples/pts/neg/externDefParameter.check
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
[error] examples/pts/neg/externDefParameter.effekt:3:1: Cannot fully infer type for test: ValueTypeWildcard => Unit
extern pure def test(x: _): Unit = "test"
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
module examples/pts/neg/externDefParameter

extern pure def test(x: _): Unit = "test"

val a = test(1)
Expand Down
3 changes: 3 additions & 0 deletions examples/pts/neg/externDefReturn.check
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
[error] examples/pts/neg/externDefReturn.effekt:3:1: Cannot fully infer type for func: EffectSetWildcard
extern def func(x: _): _ / _ = "Test"
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
module examples/pts/neg/externDefReturn

extern def func(x: _): _ / _ = "Test"

def main() = {
Expand Down
Empty file.
3 changes: 3 additions & 0 deletions examples/pts/neg/externResource.check
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
[error] examples/pts/neg/externResource.effekt:3:1: Cannot fully infer type for test: _
extern resource test: _
^^^^^^^^^^^^^^^^^^^^^^^
2 changes: 2 additions & 0 deletions examples/pts/neg/externResource.effekt
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
module examples/pts/neg/externResource

extern resource test: _

def main() = {
Expand Down
2 changes: 1 addition & 1 deletion examples/pts/neg/functionParameter.check
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
[error] examples\pts\neg\functionParameter.effekt:3:1: Cannot fully infer type for func1: ValueTypeWildcard => String
[error] examples/pts/neg/functionParameter.effekt:3:1: Cannot fully infer type for func1: ValueTypeWildcard => String
def func1(x: _) = "test"
^^^^^^^^^^^^^^^^^^^^^^^^
3 changes: 3 additions & 0 deletions examples/pts/neg/operation.check
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
[error] examples/pts/neg/operation.effekt:3:1: Wildcard not usable in interface operations
effect Test {
^
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// opClause wildcard
module examples/pts/neg/operation

effect Test {
def output(x: Int): Int / _
Expand Down
3 changes: 3 additions & 0 deletions examples/pts/neg/typeAlias.check
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
[error] examples/pts/neg/typeAlias.effekt:5:1: Cannot fully infer type for f: ValueTypeWildcard => Int
def f(x: A) = 1
^
9 changes: 9 additions & 0 deletions examples/pts/neg/typeAlias.effekt
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
module examples/pts/neg/typeAlias

type A = _

def f(x: A) = 1

def main() = {
1
}
2 changes: 1 addition & 1 deletion examples/pts/neg/variable.check
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
[error] examples\pts\neg\variable.effekt:6:13: Expected Int but got String.
[error] examples/pts/neg/variable.effekt:6:13: Expected Int but got String.
value = "t"
^^^
4 changes: 4 additions & 0 deletions examples/pts/pos/blockLiteral.effekt
Original file line number Diff line number Diff line change
Expand Up @@ -11,3 +11,7 @@ def outer{interfaceEff: InterfaceEff} = {
}
func
}

def main() = {
()
}
6 changes: 5 additions & 1 deletion examples/pts/pos/blockParameter.effekt
Original file line number Diff line number Diff line change
Expand Up @@ -2,4 +2,8 @@ module examples/pts/pos/blockParameter

def param(x: Int, y: Int): Int = x + y

def func1{f: _}: Boolean = f(1, 2) == 2
def func1{f: _}: Boolean = f(1, 2) == 2

def main() = {
()
}
4 changes: 4 additions & 0 deletions examples/pts/pos/boxedInterface.effekt
Original file line number Diff line number Diff line change
Expand Up @@ -18,4 +18,8 @@ def func{ eff: Eff } = {
def unboxed: _ = boxed

boxed
}

def main() = {
()
}
11 changes: 0 additions & 11 deletions examples/pts/pos/defWithEff.effekt

This file was deleted.

12 changes: 12 additions & 0 deletions examples/pts/pos/effectfulBox.effekt
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
effect Eff(): Unit

def f(): Int / Eff = {
do Eff()
1
}

val boxed: _ at {} = box f

def main() = {
()
}
4 changes: 3 additions & 1 deletion examples/pts/pos/effects.effekt
Original file line number Diff line number Diff line change
Expand Up @@ -14,4 +14,6 @@ def func2(): Int / _ = {
1
}

def main() = { () }
def main() = {
()
}
File renamed without changes.
4 changes: 4 additions & 0 deletions examples/pts/pos/interface.effekt
Original file line number Diff line number Diff line change
Expand Up @@ -13,4 +13,8 @@ def withConstantInt[R]{ body: { Constant[Int] } => R }: R = {

def foo() = withConstantInt { {interfaceParam: _} =>
interfaceParam.output() + 1
}

def main() = {
()
}
6 changes: 5 additions & 1 deletion examples/pts/pos/nestedTypes.effekt
Original file line number Diff line number Diff line change
Expand Up @@ -22,4 +22,8 @@ def func(listParam: _): Int =

record Constant[A](value: A)

val constant: Constant[_] = Constant(1)
val constant: Constant[_] = Constant(1)

def main() = {
()
}
Original file line number Diff line number Diff line change
Expand Up @@ -4,5 +4,5 @@ def f(x: _): Int = {
}

def main() = {
f("1")
()
}
2 changes: 0 additions & 2 deletions examples/pts/pos/parametricBox.effekt
Original file line number Diff line number Diff line change
Expand Up @@ -2,8 +2,6 @@ def f[A](x: A): Int = 2

val boxed: _ at {} = box f

val d: Int = boxed

def main() = {
()
}
File renamed without changes.
9 changes: 8 additions & 1 deletion examples/pts/pos/typeParameter.effekt
Original file line number Diff line number Diff line change
@@ -1 +1,8 @@
def id[A](x: A): A = x
def id[A](x: _): A = {
val y: A = x
x
}

def main() = {
()
}
13 changes: 0 additions & 13 deletions examples/pts/test11.effekt

This file was deleted.

6 changes: 0 additions & 6 deletions examples/pts/test12.effekt

This file was deleted.

26 changes: 0 additions & 26 deletions examples/pts/test14.effekt

This file was deleted.

5 changes: 0 additions & 5 deletions examples/pts/test18.effekt

This file was deleted.

7 changes: 0 additions & 7 deletions examples/pts/test19.effekt

This file was deleted.

5 changes: 0 additions & 5 deletions examples/pts/test20.effekt

This file was deleted.

Loading

0 comments on commit c8acc66

Please sign in to comment.