diff --git a/effekt/jvm/src/test/scala/effekt/TyperTests.scala b/effekt/jvm/src/test/scala/effekt/TyperTests.scala index 808a5db72..5466cabb7 100644 --- a/effekt/jvm/src/test/scala/effekt/TyperTests.scala +++ b/effekt/jvm/src/test/scala/effekt/TyperTests.scala @@ -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 } @@ -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") } } @@ -282,6 +273,10 @@ 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 }") @@ -289,6 +284,12 @@ class TyperTests extends AbstractTyperTests { } } + 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]") @@ -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") @@ -312,8 +334,5 @@ class TyperTests extends AbstractTyperTests { } } - - testTyperFile("Debug")("examples/pts/test24.effekt"){ - C => C.assertBlockType("func", "") - } + } diff --git a/examples/pts/test23.effekt b/examples/pts/FIXME.effekt similarity index 76% rename from examples/pts/test23.effekt rename to examples/pts/FIXME.effekt index 9edd6a7b7..063c3c652 100644 --- a/examples/pts/test23.effekt +++ b/examples/pts/FIXME.effekt @@ -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 } diff --git a/examples/pts/neg/blockParameters.check b/examples/pts/neg/blockParameters.check index 9d73d16f6..d55bf3b8f 100644 --- a/examples/pts/neg/blockParameters.check +++ b/examples/pts/neg/blockParameters.check @@ -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" ^^^^^^^^^^^^^^^^^^^^^^^^^^^ \ No newline at end of file diff --git a/examples/pts/neg/boxInference.check b/examples/pts/neg/boxInference.check index e2676f6e5..8f766fe0b 100644 --- a/examples/pts/neg/boxInference.check +++ b/examples/pts/neg/boxInference.check @@ -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) + ^ \ No newline at end of file diff --git a/examples/pts/neg/boxParametricFunction.check b/examples/pts/neg/boxParametricFunction.check index 1b40ceb1a..3e5fd310f 100644 --- a/examples/pts/neg/boxParametricFunction.check +++ b/examples/pts/neg/boxParametricFunction.check @@ -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) - ^ \ No newline at end of file +[error] examples/pts/neg/boxParametricFunction.effekt:8:6: Cannot infer function type for callee. + (unbox boxedParam)(1) + ^ \ No newline at end of file diff --git a/examples/pts/neg/effectInBlockParam.check b/examples/pts/neg/effectInBlockParam.check index e69de29bb..ad0d0759e 100644 --- a/examples/pts/neg/effectInBlockParam.check +++ b/examples/pts/neg/effectInBlockParam.check @@ -0,0 +1,3 @@ +[error] examples/pts/neg/effectInBlockParam.effekt:6:5: EffectSetWildcard is not allowed in block parameter + func() + ^ \ No newline at end of file diff --git a/examples/pts/neg/externDefCaptures.check b/examples/pts/neg/externDefCaptures.check new file mode 100644 index 000000000..e5fbb6e0d --- /dev/null +++ b/examples/pts/neg/externDefCaptures.check @@ -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" + ^ \ No newline at end of file diff --git a/examples/pts/test16.effekt b/examples/pts/neg/externDefCaptures.effekt similarity index 56% rename from examples/pts/test16.effekt rename to examples/pts/neg/externDefCaptures.effekt index ec5fd9141..4afbc3f9e 100644 --- a/examples/pts/test16.effekt +++ b/examples/pts/neg/externDefCaptures.effekt @@ -1,3 +1,5 @@ +module examples/pts/neg/externDefCaptures + extern _ def func(x: Int): Int = "test" def main() = { diff --git a/examples/pts/neg/externDefParameter.check b/examples/pts/neg/externDefParameter.check new file mode 100644 index 000000000..cfcc2824e --- /dev/null +++ b/examples/pts/neg/externDefParameter.check @@ -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" +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ \ No newline at end of file diff --git a/examples/pts/neg/externFunction.effekt b/examples/pts/neg/externDefParameter.effekt similarity index 61% rename from examples/pts/neg/externFunction.effekt rename to examples/pts/neg/externDefParameter.effekt index 005f4ee05..56431f163 100644 --- a/examples/pts/neg/externFunction.effekt +++ b/examples/pts/neg/externDefParameter.effekt @@ -1,3 +1,5 @@ +module examples/pts/neg/externDefParameter + extern pure def test(x: _): Unit = "test" val a = test(1) diff --git a/examples/pts/neg/externDefReturn.check b/examples/pts/neg/externDefReturn.check new file mode 100644 index 000000000..c8be789bb --- /dev/null +++ b/examples/pts/neg/externDefReturn.check @@ -0,0 +1,3 @@ +[error] examples/pts/neg/externDefReturn.effekt:3:1: Cannot fully infer type for func: EffectSetWildcard +extern def func(x: _): _ / _ = "Test" +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ \ No newline at end of file diff --git a/examples/pts/test17.effekt b/examples/pts/neg/externDefReturn.effekt similarity index 56% rename from examples/pts/test17.effekt rename to examples/pts/neg/externDefReturn.effekt index bfff3b183..16b1e01b4 100644 --- a/examples/pts/test17.effekt +++ b/examples/pts/neg/externDefReturn.effekt @@ -1,3 +1,5 @@ +module examples/pts/neg/externDefReturn + extern def func(x: _): _ / _ = "Test" def main() = { diff --git a/examples/pts/neg/externFunction.check b/examples/pts/neg/externFunction.check deleted file mode 100644 index e69de29bb..000000000 diff --git a/examples/pts/neg/externResource.check b/examples/pts/neg/externResource.check new file mode 100644 index 000000000..9f3d7c757 --- /dev/null +++ b/examples/pts/neg/externResource.check @@ -0,0 +1,3 @@ +[error] examples/pts/neg/externResource.effekt:3:1: Cannot fully infer type for test: _ +extern resource test: _ +^^^^^^^^^^^^^^^^^^^^^^^ \ No newline at end of file diff --git a/examples/pts/neg/externResource.effekt b/examples/pts/neg/externResource.effekt index 500b31936..28f4273ae 100644 --- a/examples/pts/neg/externResource.effekt +++ b/examples/pts/neg/externResource.effekt @@ -1,3 +1,5 @@ +module examples/pts/neg/externResource + extern resource test: _ def main() = { diff --git a/examples/pts/neg/functionParameter.check b/examples/pts/neg/functionParameter.check index c8f5e92fb..76c998b56 100644 --- a/examples/pts/neg/functionParameter.check +++ b/examples/pts/neg/functionParameter.check @@ -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" ^^^^^^^^^^^^^^^^^^^^^^^^ diff --git a/examples/pts/neg/operation.check b/examples/pts/neg/operation.check new file mode 100644 index 000000000..66144b83b --- /dev/null +++ b/examples/pts/neg/operation.check @@ -0,0 +1,3 @@ +[error] examples/pts/neg/operation.effekt:3:1: Wildcard not usable in interface operations +effect Test { +^ \ No newline at end of file diff --git a/examples/pts/test10.effekt b/examples/pts/neg/operation.effekt similarity index 63% rename from examples/pts/test10.effekt rename to examples/pts/neg/operation.effekt index 9b6645f92..8c81b64a4 100644 --- a/examples/pts/test10.effekt +++ b/examples/pts/neg/operation.effekt @@ -1,4 +1,4 @@ -// opClause wildcard +module examples/pts/neg/operation effect Test { def output(x: Int): Int / _ diff --git a/examples/pts/neg/typeAlias.check b/examples/pts/neg/typeAlias.check new file mode 100644 index 000000000..b17651da7 --- /dev/null +++ b/examples/pts/neg/typeAlias.check @@ -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 +^ \ No newline at end of file diff --git a/examples/pts/neg/typeAlias.effekt b/examples/pts/neg/typeAlias.effekt new file mode 100644 index 000000000..ffaa80b5c --- /dev/null +++ b/examples/pts/neg/typeAlias.effekt @@ -0,0 +1,9 @@ +module examples/pts/neg/typeAlias + +type A = _ + +def f(x: A) = 1 + +def main() = { + 1 +} \ No newline at end of file diff --git a/examples/pts/neg/variable.check b/examples/pts/neg/variable.check index 7989ff105..9c53d113d 100644 --- a/examples/pts/neg/variable.check +++ b/examples/pts/neg/variable.check @@ -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" ^^^ \ No newline at end of file diff --git a/examples/pts/pos/blockLiteral.effekt b/examples/pts/pos/blockLiteral.effekt index f3bfb128f..b4aee26ee 100644 --- a/examples/pts/pos/blockLiteral.effekt +++ b/examples/pts/pos/blockLiteral.effekt @@ -11,3 +11,7 @@ def outer{interfaceEff: InterfaceEff} = { } func } + +def main() = { + () +} \ No newline at end of file diff --git a/examples/pts/pos/blockParameter.effekt b/examples/pts/pos/blockParameter.effekt index c6a66f4d5..508150700 100644 --- a/examples/pts/pos/blockParameter.effekt +++ b/examples/pts/pos/blockParameter.effekt @@ -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 \ No newline at end of file +def func1{f: _}: Boolean = f(1, 2) == 2 + +def main() = { + () +} \ No newline at end of file diff --git a/examples/pts/pos/boxedInterface.effekt b/examples/pts/pos/boxedInterface.effekt index 425d7f633..2e559044a 100644 --- a/examples/pts/pos/boxedInterface.effekt +++ b/examples/pts/pos/boxedInterface.effekt @@ -18,4 +18,8 @@ def func{ eff: Eff } = { def unboxed: _ = boxed boxed +} + +def main() = { + () } \ No newline at end of file diff --git a/examples/pts/pos/defWithEff.effekt b/examples/pts/pos/defWithEff.effekt deleted file mode 100644 index 22b04668a..000000000 --- a/examples/pts/pos/defWithEff.effekt +++ /dev/null @@ -1,11 +0,0 @@ -effect Eff(): Unit - -def run{func: _} = { - val a: Int = func(1) - def b: Int => Int / Eff = func - 1 -} - -def main() = { - () -} \ No newline at end of file diff --git a/examples/pts/pos/effectfulBox.effekt b/examples/pts/pos/effectfulBox.effekt index e69de29bb..c8c3fc71c 100644 --- a/examples/pts/pos/effectfulBox.effekt +++ b/examples/pts/pos/effectfulBox.effekt @@ -0,0 +1,12 @@ +effect Eff(): Unit + +def f(): Int / Eff = { + do Eff() + 1 +} + +val boxed: _ at {} = box f + +def main() = { + () +} \ No newline at end of file diff --git a/examples/pts/pos/effects.effekt b/examples/pts/pos/effects.effekt index 4ee823494..f3d0cfb16 100644 --- a/examples/pts/pos/effects.effekt +++ b/examples/pts/pos/effects.effekt @@ -14,4 +14,6 @@ def func2(): Int / _ = { 1 } -def main() = { () } \ No newline at end of file +def main() = { + () +} \ No newline at end of file diff --git a/examples/pts/pos/functionDoubleUse.effekt b/examples/pts/pos/functionMultipleUses.effekt similarity index 100% rename from examples/pts/pos/functionDoubleUse.effekt rename to examples/pts/pos/functionMultipleUses.effekt diff --git a/examples/pts/pos/interface.effekt b/examples/pts/pos/interface.effekt index b56a230eb..b6c295404 100644 --- a/examples/pts/pos/interface.effekt +++ b/examples/pts/pos/interface.effekt @@ -13,4 +13,8 @@ def withConstantInt[R]{ body: { Constant[Int] } => R }: R = { def foo() = withConstantInt { {interfaceParam: _} => interfaceParam.output() + 1 +} + +def main() = { + () } \ No newline at end of file diff --git a/examples/pts/pos/nestedTypes.effekt b/examples/pts/pos/nestedTypes.effekt index 67cee2f11..37df6ea3f 100644 --- a/examples/pts/pos/nestedTypes.effekt +++ b/examples/pts/pos/nestedTypes.effekt @@ -22,4 +22,8 @@ def func(listParam: _): Int = record Constant[A](value: A) -val constant: Constant[_] = Constant(1) \ No newline at end of file +val constant: Constant[_] = Constant(1) + +def main() = { + () +} \ No newline at end of file diff --git a/examples/pts/twoWildcards.effekt b/examples/pts/pos/nestedWildcards.effekt similarity index 77% rename from examples/pts/twoWildcards.effekt rename to examples/pts/pos/nestedWildcards.effekt index 17ef7c246..2df7dac82 100644 --- a/examples/pts/twoWildcards.effekt +++ b/examples/pts/pos/nestedWildcards.effekt @@ -4,5 +4,5 @@ def f(x: _): Int = { } def main() = { - f("1") + () } \ No newline at end of file diff --git a/examples/pts/pos/parametricBox.effekt b/examples/pts/pos/parametricBox.effekt index 3cb93e0ad..8bab554f2 100644 --- a/examples/pts/pos/parametricBox.effekt +++ b/examples/pts/pos/parametricBox.effekt @@ -2,8 +2,6 @@ def f[A](x: A): Int = 2 val boxed: _ at {} = box f -val d: Int = boxed - def main() = { () } \ No newline at end of file diff --git a/examples/pts/test22.effekt b/examples/pts/pos/recursiveFunction.effekt similarity index 100% rename from examples/pts/test22.effekt rename to examples/pts/pos/recursiveFunction.effekt diff --git a/examples/pts/pos/typeParameter.effekt b/examples/pts/pos/typeParameter.effekt index 20ffb62ee..1aaaf82e7 100644 --- a/examples/pts/pos/typeParameter.effekt +++ b/examples/pts/pos/typeParameter.effekt @@ -1 +1,8 @@ -def id[A](x: A): A = x \ No newline at end of file +def id[A](x: _): A = { + val y: A = x + x +} + +def main() = { + () +} \ No newline at end of file diff --git a/examples/pts/test11.effekt b/examples/pts/test11.effekt deleted file mode 100644 index e27728286..000000000 --- a/examples/pts/test11.effekt +++ /dev/null @@ -1,13 +0,0 @@ -// Parametric Captures - -effect Eff[A]{ def output(): Int } - -def f{ eff: Eff[Int] } = { - val a = fun() { eff.output() } - val b: _ = a - 1 -} - -def main() = { - () -} \ No newline at end of file diff --git a/examples/pts/test12.effekt b/examples/pts/test12.effekt deleted file mode 100644 index 7ef7f17de..000000000 --- a/examples/pts/test12.effekt +++ /dev/null @@ -1,6 +0,0 @@ -// Wildcards in anonymous functions - -def main() = { - - -} \ No newline at end of file diff --git a/examples/pts/test14.effekt b/examples/pts/test14.effekt deleted file mode 100644 index cb1646e02..000000000 --- a/examples/pts/test14.effekt +++ /dev/null @@ -1,26 +0,0 @@ -effect Eff { def use(): Unit } - -def myModule { eff : Eff } = { - val e = fun() { eff.use(); () }; - def x = unbox e; - - val f: () => Unit at _ = x; - val g: _ at _ = x - val h: _ = x - - def m(x: Int => Int at {eff}): Int = { - println("called") - 1 - } - - def n: _ = m - def o: Int => Int = n - - f -} - - - -def main() = { - () -} \ No newline at end of file diff --git a/examples/pts/test18.effekt b/examples/pts/test18.effekt deleted file mode 100644 index 704dff2b9..000000000 --- a/examples/pts/test18.effekt +++ /dev/null @@ -1,5 +0,0 @@ -val res = fun(x: _) { 1 } - -def main() = { - println(res(1)) -} diff --git a/examples/pts/test19.effekt b/examples/pts/test19.effekt deleted file mode 100644 index be0882157..000000000 --- a/examples/pts/test19.effekt +++ /dev/null @@ -1,7 +0,0 @@ -def run{ f: Int => Int / _ }: Int = f(1) - -val res = run{ (x: Int) => x + 1 } - -def main() = { - println(res) -} \ No newline at end of file diff --git a/examples/pts/test20.effekt b/examples/pts/test20.effekt deleted file mode 100644 index 2e53a5b19..000000000 --- a/examples/pts/test20.effekt +++ /dev/null @@ -1,5 +0,0 @@ -def identity[A](x: A): A = x - -def runFunc{block: _}: Int = block(1) - -def main() = { runFunc{identity} } \ No newline at end of file diff --git a/examples/pts/test21.effekt b/examples/pts/test21.effekt deleted file mode 100644 index 396dcf93d..000000000 --- a/examples/pts/test21.effekt +++ /dev/null @@ -1,9 +0,0 @@ -def id(x: Int): Int = x - -def id(x: String): String = x - -def main() = { - val a = id(1) - val b = id("a") - println(a) -} \ No newline at end of file diff --git a/examples/pts/test24.effekt b/examples/pts/test24.effekt deleted file mode 100644 index e57b39268..000000000 --- a/examples/pts/test24.effekt +++ /dev/null @@ -1,12 +0,0 @@ -def runFunc[A](x: A){func: _}: Int = { - func(x) -} - -def f(x: Int): Int = x + 1 - -def g(x: String): Int = 1 - -def main() = { - println(runFunc(1){f}) - println(runFunc("a"){g}) -} \ No newline at end of file diff --git a/examples/pts/test25.effekt b/examples/pts/test25.effekt deleted file mode 100644 index 648c27a68..000000000 --- a/examples/pts/test25.effekt +++ /dev/null @@ -1,5 +0,0 @@ -def f[_](x: Int): Int = x + 1 - -def main() = { - f(1) -} \ No newline at end of file diff --git a/examples/pts/test26.effekt b/examples/pts/test26.effekt deleted file mode 100644 index f7e02c9fc..000000000 --- a/examples/pts/test26.effekt +++ /dev/null @@ -1,5 +0,0 @@ -extern resource test: Int => Int - -def main() = { - () -} \ No newline at end of file diff --git a/examples/pts/test27.effekt b/examples/pts/test27.effekt deleted file mode 100644 index 59abcc6dc..000000000 --- a/examples/pts/test27.effekt +++ /dev/null @@ -1,8 +0,0 @@ -type A = _ - -val b: A = 1 -val c: A = "a" - -def main() = { - () -} \ No newline at end of file diff --git a/examples/pts/test28.effekt b/examples/pts/test28.effekt deleted file mode 100644 index a79cd2f89..000000000 --- a/examples/pts/test28.effekt +++ /dev/null @@ -1,10 +0,0 @@ -def f(x: Int): _ = { - if(x == 0) - "a" - else - f(x - 1) + 1 -} - -def main() = { - () -} \ No newline at end of file diff --git a/examples/pts/test29.effekt b/examples/pts/test29.effekt deleted file mode 100644 index f3f237dc8..000000000 --- a/examples/pts/test29.effekt +++ /dev/null @@ -1,7 +0,0 @@ -type A = _ - -def main() = { - val x: A = 5 - val y: A = "a" - 1 -} \ No newline at end of file diff --git a/examples/pts/testExternDef.effekt b/examples/pts/testExternDef.effekt deleted file mode 100644 index 3407163b2..000000000 --- a/examples/pts/testExternDef.effekt +++ /dev/null @@ -1,5 +0,0 @@ -extern def test(x: Int): Int / _ = "test" - -def main() = { - () -} \ No newline at end of file diff --git a/examples/pts/typeAlias.effekt b/examples/pts/typeAlias.effekt deleted file mode 100644 index 5df7f934a..000000000 --- a/examples/pts/typeAlias.effekt +++ /dev/null @@ -1,7 +0,0 @@ -type AA = _ - -def f(x: AA) = 1 - -def main() = { - 1 -} \ No newline at end of file