misc tests

Kraks · Oct 16, 2023 · ebf1f12 · ebf1f12
1 parent 04ac211
commit ebf1f12
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 4 deletions.
diff --git a/src/test/scala/qualfsub/TypeCheckBasic.scala b/src/test/scala/qualfsub/TypeCheckBasic.scala
@@ -126,6 +126,10 @@ class QualSTLCTests extends AnyFunSuite {
     assert(Qual(Set("x1", "x3")).isSubqual(Qual(Set("g")))(using Γ10))
     assert(Qual(Set("x1", "x2")).isSubqual(Qual(Set("f")))(using Γ10))
     assert(Qual(Set("x1", "x2", "x3")).isSubqual(Qual(Set("f", "g")))(using Γ10))
+
+    val Γ11 = TEnv.empty + ("x" -> (TNum ^ ◆)) + ("y" -> (TNum ^ "x"))
+    assert(!Qual(Set("x")).isSubqual(Qual(Set("y")))(using Γ11))
+    assert(Qual(Set("y")).isSubqual(Qual(Set("x")))(using Γ11))
   }
 
   test("alloc") {
@@ -214,7 +218,7 @@ class QualSTLCTests extends AnyFunSuite {
   }
 
   test("escaping closures") {
-    val e1 = 
+    val e1 =
       let("x" ⇐ alloc(3)) {
         λ("f", "z")("f"♯(TNum ~> TNum)) { x.deref }
       }
@@ -255,7 +259,7 @@ class QualSTLCTests extends AnyFunSuite {
       (λ("x" ⦂ (TRef(TNum) ^ ◆)) { λ("f", "z")("f"♯(TNum ~> (TRef(TNum) ^ "f"))) { x } })(alloc(3))
     assert(topTypeCheck(e4) == (TFun("f", "z", TNum^(), TRef(TNum)^"f") ^ ◆))
 
-    val e4_let = 
+    val e4_let =
       let("x" ⇐ alloc(0)) {
         λ("f", "z")("f"♯(TNum ~> (TRef(TNum) ^ "f"))) { x }
       }

diff --git a/src/test/scala/qualstlc/TypeCheck.scala b/src/test/scala/qualstlc/TypeCheck.scala
@@ -122,6 +122,10 @@ class QualSTLCTests extends AnyFunSuite {
     assert(Qual(Set("x1", "x3")).isSubqual(Qual(Set("g")))(using Γ10))
     assert(Qual(Set("x1", "x2")).isSubqual(Qual(Set("f")))(using Γ10))
     assert(Qual(Set("x1", "x2", "x3")).isSubqual(Qual(Set("f", "g")))(using Γ10))
+
+    val Γ11 = TEnv.empty + ("x" -> (TNum ^ ◆)) + ("y" -> (TNum ^ "x"))
+    assert(!Qual(Set("x")).isSubqual(Qual(Set("y")))(using Γ11))
+    assert(Qual(Set("y")).isSubqual(Qual(Set("x")))(using Γ11))
   }
 
   test("alloc") {
@@ -210,7 +214,7 @@ class QualSTLCTests extends AnyFunSuite {
   }
 
   test("escaping closures") {
-    val e1 = 
+    val e1 =
       let("x" ⇐ alloc(3)) {
         λ("f", "z")("f"♯(TNum ~> TNum)) { x.deref }
       }
@@ -251,7 +255,7 @@ class QualSTLCTests extends AnyFunSuite {
       (λ("x" ⦂ (TRef(TNum) ^ ◆)) { λ("f", "z")("f"♯(TNum ~> (TRef(TNum) ^ "f"))) { x } })(alloc(3))
     assert(topTypeCheck(e4) == (TFun("f", "z", TNum^(), TRef(TNum)^"f") ^ ◆))
 
-    val e4_let = 
+    val e4_let =
       let("x" ⇐ alloc(0)) {
         λ("f", "z")("f"♯(TNum ~> (TRef(TNum) ^ "f"))) { x }
       }