poly pair examples

Kraks · Jul 12, 2024 · f880980 · f880980
1 parent 9717066
commit f880980
Show file tree

Hide file tree

Showing 2 changed files with 103 additions and 1 deletion.
diff --git 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
@@ -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^())^ ◆))
+    */
+  }
+
 }