From f8809805201265bf3ef95d009da335d0f8e227e3 Mon Sep 17 00:00:00 2001 From: Guannan Wei Date: Fri, 12 Jul 2024 10:31:32 +0200 Subject: [PATCH] poly pair examples --- src/main/scala/avoidancefsub/TypeCheck.scala | 3 +- src/test/scala/avoidancefsub/TypeCheck.scala | 101 +++++++++++++++++++ 2 files changed, 103 insertions(+), 1 deletion(-) diff --git a/src/main/scala/avoidancefsub/TypeCheck.scala b/src/main/scala/avoidancefsub/TypeCheck.scala index 152aac2..5e5ccdb 100644 --- a/src/main/scala/avoidancefsub/TypeCheck.scala +++ b/src/main/scala/avoidancefsub/TypeCheck.scala @@ -658,8 +658,9 @@ def infer(tenv: TEnv, e: Expr): (Qual, QType) = { (fl, tq) case ETyApp(e, tq, _) => val (fl1, QType(TForall(f, tvar, qvar, bound@QType(t, p), rt@QType(u, r)), q)) = infer(tenv, e) + val (fl2, gr) = subtypeCheck(tenv, tq.ty, u) assert(wellFormed(tenv, tq), "must be well-formed") - val fl = (fl1 ++ p ++ r) -- Qual(Set(f, qvar, Fresh())) + val fl = (fl1 ++ fl2 ++ p ++ r) -- Qual(Set(f, qvar, Fresh())) (fl -- Qual(Set(f, qvar, Fresh())), QType(u, r.subst(qvar, tq.q))) } } diff --git a/src/test/scala/avoidancefsub/TypeCheck.scala b/src/test/scala/avoidancefsub/TypeCheck.scala index bdae575..54afba8 100644 --- a/src/test/scala/avoidancefsub/TypeCheck.scala +++ b/src/test/scala/avoidancefsub/TypeCheck.scala @@ -41,4 +41,105 @@ class AvoidanceFSubTests extends AnyFunSuite { // TFun("𝑓#3","x",TVar("A")^"a",TVar("A")^"x")^"a")^())) } + test("transparent poly pair") { + def makePair(a: String, b: String) = s""" + [A <: Top] => { [B <: Top] => { + [C <: Top] => { + p(f: (f(x: A^$a) => (g(y: B^$b) => C^g)^f)^{<>, p})^{$a, $b}: C^f => { f($a)($b) } + } + } } + """ + def fstT(a: String)(p: String) = s""" + [A <: Top] => { [B <: Top] => { + $p(f(x: A^$a)^$a: (g(y: B^{<>, g}) => A^g)^f => { g(y: B^{<>, g})^f: A^g => { x } }) + } } + """ + def sndT(b: String)(p: String) = s""" + [A <: Top] => { [B <: Top] => { + $p(f(x: A^{<>, f})^$b: (g(y: B^$b) => B^g)^f => { g(y: B^$b)^f: B^g => { y } }) + } } + """ + //println(parseToCore(makePair("r1", "r2"))) + //println(parseToCore(fstT("r1")("p"))) + //println(parseToCore(sndT("r1")("p"))) + + /* + val prog1 = s""" + val r1 = Ref 1; + val r2 = Ref 2; + val p = ${makePair("Ref[Int]")("r1", "r2")}; + ${fstT("Ref[Int]", "r1")("p")} + """ + assert(parseAndCheck(prog1) == (TRef(TNum^()) ^ ◆)) + val prog2 = s""" + val r1 = Ref 1; + val r2 = Ref 2; + val p = ${makePair("Ref[Int]")("r1", "r2")}; + ${sndT("Ref[Int]", "r2")("p")} + """ + assert(parseAndCheck(prog2) == (TRef(TNum^()) ^ ◆)) + */ + } + + test("opaque mono pair") { + def makePair(a: String, b: String) = s""" + [A <: Top] => { [B <: Top] => { + [C <: Top] => { + p(f: (f(x: A^$a) => (g(y: B^$b) => C^g)^f)^{<>, p})^{$a, $b}: C^f => { f($a)($b) } + } + } } + """ + def fstO(p: String) = s""" + [A <: Top] => { [B <: Top] => { + $p(f(x: A^{<>, f}): (g(y: B^{<>,g}) => A^{g,y})^{x, f} => { g(y: B^{<>, g})^{x, f}: A^{g, y} => { x } }) + } } + """ + def sndO(p: String) = s""" + [A <: Top] => { [B <: Top] => { + $p(f(x: A^{<>, f}): (g(y: B^{<>,g}) => B^{g,y})^{x, f} => { g(y: B^{<>, g})^{x, f}: A^{g, y} => { y } }) + } } + """ + + /* + val prog1 = s""" + def makePair() = { + val r1 = Ref 1; + val r2 = Ref 2; + val p0 = ${makePair("Ref[Int]")("r1", "r2")}; + p0 + }; + makePair() + """ + assert(parseAndCheck(prog1) == + (TFun("p","f", + TFun("f","x",TRef(TNum^()) ^ ("f", ◆), + TFun("g","y",TRef(TNum^()) ^ ("g", ◆), + TRef(TNum^()) ^ ("g","y")) ^ ("f","x")) ^ ("p", ◆), TRef(TNum^()) ^ ("f", "p")) ^ ◆)) + + val prog2 = s""" + def makePair() = { + val r1 = Ref 1; + val r2 = Ref 2; + val p0 = ${makePair("Ref[Int]")("r1", "r2")}; + p0 + }; + val p1 = makePair(); + ${fstO("Ref[Int]")("p1")} + """ + assert(parseAndCheck(prog2) == (TRef(TNum^())^ ◆)) + + val prog3 = s""" + def makePair() = { + val r1 = Ref 1; + val r2 = Ref 2; + val p0 = ${makePair("Ref[Int]")("r1", "r2")}; + p0 + }; + val p1 = makePair(); + ${sndO("Ref[Int]")("p1")} + """ + assert(parseAndCheck(prog3) == (TRef(TNum^())^ ◆)) + */ + } + } \ No newline at end of file