From 9fec468a2a52f880e06a5a2497799759f3fa55b6 Mon Sep 17 00:00:00 2001 From: Mattis Krauch Date: Mon, 26 Jun 2023 16:49:12 +0200 Subject: [PATCH] Further changes for BlockType Wildcards --- .../main/scala/effekt/core/Transformer.scala | 6 +++--- .../main/scala/effekt/typer/Constraints.scala | 6 ++++-- .../scala/effekt/typer/TypeComparer.scala | 10 +++++++++- examples/pts/blockType.effekt | 19 +++++++++++++------ examples/pts/blockTypes.effekt | 18 ++++++++++++++++++ examples/pts/functionParameterTypes.effekt | 12 ++++++++++++ examples/pts/longType.effekt | 16 ++++++++++++++++ examples/pts/nestedTypes.effekt | 19 +++++++++++++++++++ examples/pts/valueType.effekt | 5 +++-- 9 files changed, 97 insertions(+), 14 deletions(-) create mode 100644 examples/pts/blockTypes.effekt create mode 100644 examples/pts/functionParameterTypes.effekt create mode 100644 examples/pts/longType.effekt create mode 100644 examples/pts/nestedTypes.effekt diff --git a/effekt/shared/src/main/scala/effekt/core/Transformer.scala b/effekt/shared/src/main/scala/effekt/core/Transformer.scala index d826ea8b0..b6f9194cd 100644 --- a/effekt/shared/src/main/scala/effekt/core/Transformer.scala +++ b/effekt/shared/src/main/scala/effekt/core/Transformer.scala @@ -177,7 +177,7 @@ object Transformer extends Phase[Typechecked, CoreTransformed] { case v: source.Var => val sym = v.definition Context.blockTypeOf(sym) match { - case BlockTypeRef(x : BlockTypeWildcard) => Context.panic("Wildcard in unexpected place") + case BlockTypeRef(x) => Context.panic("Wildcard in unexpected place") case _: BlockType.FunctionType => transformAsControlBlock(tree) case _: BlockType.InterfaceType => transformAsObject(tree) } @@ -218,7 +218,7 @@ object Transformer extends Phase[Typechecked, CoreTransformed] { val sym = v.definition val tpe = Context.blockTypeOf(sym) tpe match { - case BlockTypeRef(x : BlockTypeWildcard) => Context.abort("Wildcard in unexpected place") + case BlockTypeRef(x) => Context.panic("Wildcard in unexpected place") case BlockType.FunctionType(tparams, cparams, vparamtps, bparamtps, restpe, effects) => // if this block argument expects to be called using PureApp or DirectApp, make sure it is // by wrapping it in a BlockLit @@ -525,7 +525,7 @@ object Transformer extends Phase[Typechecked, CoreTransformed] { } def transform(tpe: BlockType)(using Context): core.BlockType = tpe match { - case BlockTypeRef(x : BlockTypeWildcard) => Context.panic("Wildcard in unexpected place") + case BlockTypeRef(x) => Context.panic("Wildcard in unexpected place") case BlockType.FunctionType(tparams, cparams, vparams, bparams, result, effects) => val capabilityTypes = effects.canonical.map(transform) diff --git a/effekt/shared/src/main/scala/effekt/typer/Constraints.scala b/effekt/shared/src/main/scala/effekt/typer/Constraints.scala index d8df8865f..cc38a2755 100644 --- a/effekt/shared/src/main/scala/effekt/typer/Constraints.scala +++ b/effekt/shared/src/main/scala/effekt/typer/Constraints.scala @@ -231,8 +231,10 @@ class Constraints( } y match { - case BlockTypeRef(y: BlockUnificationVar) => connectNodes(getNode(x), getNode(y)) - case tpe => learnType(getNode(x), tpe) + case BlockTypeRef(y: BlockUnificationVar) => + connectNodes(getNode(x), getNode(y)) + case tpe => + learnType(getNode(x), tpe) } } diff --git a/effekt/shared/src/main/scala/effekt/typer/TypeComparer.scala b/effekt/shared/src/main/scala/effekt/typer/TypeComparer.scala index e29f0ad33..16dcf9c34 100644 --- a/effekt/shared/src/main/scala/effekt/typer/TypeComparer.scala +++ b/effekt/shared/src/main/scala/effekt/typer/TypeComparer.scala @@ -59,10 +59,16 @@ trait TypeUnifier { val unificationVar : UnificationVar = unificationVarFromWildcard(w) requireEqual(unificationVar, tpe1, ctx) + case (ValueTypeRef(w: ValueTypeWildcard), ValueTypeApp(t2, args2), _) => + val unificationVar : UnificationVar = unificationVarFromWildcard(w) + requireEqual(unificationVar, tpe2, ctx) + // For now, we treat all type constructors as invariant. case (ValueTypeApp(t1, args1), ValueTypeApp(t2, args2), _) => - if (t1 != t2) { error(tpe1, tpe2, ErrorContext.TypeConstructor(ctx)) } + if (t1 != t2) { + error(tpe1, tpe2, ErrorContext.TypeConstructor(ctx)) + } if (args1.size != args2.size) abort(pp"Argument count does not match $t1 vs. $t2", ctx) // TODO add to context @@ -81,6 +87,8 @@ trait TypeUnifier { def unifyBlockTypes(tpe1: BlockType, tpe2: BlockType, ctx: ErrorContext): Unit = (tpe1, tpe2) match { case (t, BlockTypeRef(x : BlockTypeWildcard)) => requireEqual(unificationVarFromWildcard(x), t, ctx) + case (BlockTypeRef(x : BlockTypeWildcard), t) => + requireEqual(unificationVarFromWildcard(x), t, ctx) case (t: FunctionType, s: FunctionType) => unifyFunctionTypes(t, s, ctx) case (t: InterfaceType, s: InterfaceType) => unifyInterfaceTypes(t, s, ctx) case (t, s) => error(t, s, ctx) diff --git a/examples/pts/blockType.effekt b/examples/pts/blockType.effekt index 41624ee16..ea28d0e77 100644 --- a/examples/pts/blockType.effekt +++ b/examples/pts/blockType.effekt @@ -1,7 +1,14 @@ -module examples/pts/blockType - -def main() = { - var num : _ = 1 - num = 2 - println(num) +module examples/pts/blockType + +def runFunc{func : _} = { + func("abc", 1) +} + +def main() = { + def test(x : String, y : Int) : String = { + "a" + } + + val res : Int = runFunc { test } + println(res) } \ No newline at end of file diff --git a/examples/pts/blockTypes.effekt b/examples/pts/blockTypes.effekt new file mode 100644 index 000000000..7c7962238 --- /dev/null +++ b/examples/pts/blockTypes.effekt @@ -0,0 +1,18 @@ +module examples/pts/blockTypes + +def main() = { + def test1(x : String, y : Int) : String = { + "a" + } + + def test2(x : String, y : String) : String = { + "a turtle" + } + + val res : Int = runFunc { test1 } { test2 } + println(res) +} + +def runFunc{func1 : _}{func2 : _} = { + func2(func1("abc", 1), " turtle") +} \ No newline at end of file diff --git a/examples/pts/functionParameterTypes.effekt b/examples/pts/functionParameterTypes.effekt new file mode 100644 index 000000000..27384b53c --- /dev/null +++ b/examples/pts/functionParameterTypes.effekt @@ -0,0 +1,12 @@ +module examples/pts/functionParameterTypes + +def constant(num : _) = { + val a : Test = num + return 5 +} + +def main() = { + val input : Int = 2 + val res : Int = constant(input) + println(res) +} \ No newline at end of file diff --git a/examples/pts/longType.effekt b/examples/pts/longType.effekt new file mode 100644 index 000000000..ee524abd3 --- /dev/null +++ b/examples/pts/longType.effekt @@ -0,0 +1,16 @@ +module examples/pts/longType + + +type List[A] { + Nil(); + Cons(head: A, tail: List[A]) +} + +type TypeWithReallyLongName { + X(y : Int) +} + +def main() = { + val listA : List[_] = Cons(X(1), Cons(X(2), Cons(X(3), Nil()))) + println(listA) +} \ No newline at end of file diff --git a/examples/pts/nestedTypes.effekt b/examples/pts/nestedTypes.effekt new file mode 100644 index 000000000..aeed203c9 --- /dev/null +++ b/examples/pts/nestedTypes.effekt @@ -0,0 +1,19 @@ +module examples/pts/nestedTypes + +type List[A] { + Nil(); + Cons(head: A, tail: List[A]) +} + +type Map[A, B] { + Map(keys : List[A], values : List[B]) +} + +def main() = { + val listA : List[_] = Cons(1, Cons(2, Cons(3, Nil()))) + val listB : List[_] = Cons("a", Cons("b", Cons("c", Nil()))) + + val map1 : Map[_, _] = Map(listA, listB) + val map2 : Map[String, Int] = map1 + println("end") +} \ No newline at end of file diff --git a/examples/pts/valueType.effekt b/examples/pts/valueType.effekt index 65f955fa2..4920ee753 100644 --- a/examples/pts/valueType.effekt +++ b/examples/pts/valueType.effekt @@ -1,6 +1,7 @@ module examples/pts/valueType def main() = { - val num : Int = 1; - println(num); + val num1 : _ = 1 + val num2 : String = num1 + println(num1) } \ No newline at end of file