more tests

Kraks · Jul 12, 2024 · 32030b0 · 32030b0
1 parent b408387
commit 32030b0
Show file tree

Hide file tree

Showing 2 changed files with 24 additions and 10 deletions.
diff --git a/src/main/scala/avoidancestlc/TypeCheck.scala b/src/main/scala/avoidancestlc/TypeCheck.scala
@@ -183,7 +183,7 @@ def qualUpcast(g: TEnv, p: Qual, r: Qual): (Qual /*filter*/, Qual /*ub*/) = {
 
 def subQualCheck(g: TEnv, p: Qual, r: Qual): Option[Qual] =
   val (fl, p1) = qualUpcast(g, p, r)
-  println(s"$g |- p1: $p1 r: $r")
+  //println(s"$g |- p1: $p1 r: $r")
   if (p1 ⊆ r) Some(fl ++ r) else None
 
 /* Subtype checking */
@@ -205,8 +205,6 @@ def subtypeCheck(tenv: TEnv, t1: Type, t2: Type): (Qual /*filter*/, Qual /*growt
         val (fl1, gr1) = subtypeCheck(tenv, t2, t1)
         val (fl2, gr2) = subtypeCheck(tenv, u1, u2)
         assert(p2.subsetAt(Qual(Set(f, Fresh())), p1), "argument qualifier contravariance")
-        println(s"$F <: $G")
-        println(s"r1: $r1 r2: $r2")
         assert(r1.subsetAt(Qual(Set(f, Fresh())), r2), "return qualifier covariance")
         val p1_* = (p2 -- Qual(Set(f, Fresh()))) ++ gr1
         val r2_* = (r1 -- Qual(Set(f, x, Fresh()))) ++ gr2
@@ -470,7 +468,7 @@ def infer(tenv: TEnv, e: Expr): (Qual, QType) = {
 
 def checkInfer(tenv: TEnv, e: Expr, t: Type): (Qual/*filter*/, Qual/*qual*/) = {
   val (fl1, QType(t1, q)) = infer(tenv, e)
-  println(s"checkInfer $t1 <: $t")
+  //println(s"checkInfer $t1 <: $t")
   val (fl2, gr) = subtypeCheck(tenv, t1, t)
   (fl1 ++ fl2, q ++ gr)
 }

diff --git a/src/test/scala/avoidancestlc/TypeCheck.scala b/src/test/scala/avoidancestlc/TypeCheck.scala
@@ -172,9 +172,10 @@ class AvoidanceSTLCTests extends AnyFunSuite {
     def fstO(t: String)(p: String) = s"""
       $p(f(x: $t^{<>, f}): (g(y: $t^{<>,g}) => $t^{g,y})^{x, f} => { g(y: $t^{<>, g})^{x, f}: $t^{g, y} => { x } })
     """
-    def sndO(t: String, b: String)(p: String) = s"""
-      $p(f(x: $t^{<>, f})^$b => { g(y: $t^$b)^y: $t^g => { y } })
+    def sndO(t: String)(p: String) = s"""
+      $p(f(x: $t^{<>, f}): (g(y: $t^{<>,g}) => $t^{g,y})^{x, f} => { g(y: $t^{<>, g})^{x, f}: $t^{g, y} => { y } })
     """
+
     val prog1 = s"""
       def makePair() = {
         val r1 = Ref 1;
@@ -184,8 +185,12 @@ class AvoidanceSTLCTests extends AnyFunSuite {
       };
       makePair()
     """
-    //println(parseToCore(p0))
-    println(parseAndCheck(prog1))
+    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;
@@ -196,7 +201,18 @@ class AvoidanceSTLCTests extends AnyFunSuite {
       val p1 = makePair();
       ${fstO("Ref[Int]")("p1")}
     """
-    println(prog2)
-    //println(parseAndCheck(prog2))
+    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^())^ ◆))
   }
 }