fix bugs and more test of avoidance

Kraks · Jul 10, 2024 · 6af456f · 6af456f
1 parent 9f65e4d
commit 6af456f
Show file tree

Hide file tree

Showing 2 changed files with 65 additions and 6 deletions.
diff --git a/src/main/scala/avoidancestlc/TypeCheck.scala b/src/main/scala/avoidancestlc/TypeCheck.scala
@@ -377,8 +377,8 @@ def check(tenv: TEnv, e: Expr, tq: QType): Qual = e match {
 def infer(tenv: TEnv, e: Expr): (Qual, QType) = {
   e match {
     case EUnit => (Qual.untrack, QType(TUnit, Qual.untrack))
-    case ENum(_) => (Qual.untrack, QType(TUnit, Qual.untrack))
-    case EBool(_) => (Qual.untrack, QType(TUnit, Qual.untrack))
+    case ENum(_) => (Qual.untrack, QType(TNum, Qual.untrack))
+    case EBool(_) => (Qual.untrack, QType(TBool, Qual.untrack))
     case EVar(x) =>
       val QType(t, q) = tenv(x)
       (Qual.singleton(x), QType(t, Qual.singleton(x)))
@@ -407,6 +407,10 @@ def infer(tenv: TEnv, e: Expr): (Qual, QType) = {
       val fl = (fl2 ++ fl1 ++ fl3 ++ p ++ r ++ gr) -- Qual(Set(x, Fresh()))
       val rq = (r ++ gr).subst(x, p)
       (fl, QType(v, rq))
+    case EApp(ELam(f, x, at, body, rt), e2, _) =>
+      // If an application's left-hand side is a literal lambda term,
+      // we delegate the inference using TA-LET rule
+      infer(tenv, ELet(x, Some(at), e2, body, false))
     case EApp(e1, e2, _) =>
       val (fl1, QType(TFun(f, x, QType(t, p), QType(u, r)), q)) = infer(tenv, e1)
       val (fl2, p1) = checkInfer(tenv, e2, t)
@@ -422,17 +426,25 @@ def infer(tenv: TEnv, e: Expr): (Qual, QType) = {
         else if (p.isFresh && !p.contains(f)) {
           val (fl, p2) = qualUpcast(tenv, p1, p)
           given TEnv = tenv
-          assert((p2 \ p) ⋒ q ⊆ Qual.untrack, "qualifiers not separate")
+          assert(((p2 \ p) ⋒ q) ⊆ Qual.fresh, s"qualifiers not separate: ${p2 \ p} and $q")
           fl
         } else Qual.untrack
       val fl = fl1 ++ fl2 ++ fl3 ++ (r \ Qual(Set(f, x, Fresh())))
       (fl, QType(u, r.subst(x, p1).subst(f, q)))
-    // We consider a lambda term with type annotation as "ascription"
     case ELam(f, x, at, body, Some(rt)) =>
+      // We consider a lambda term with full type annotation as "ascription"
       val q = Qual((body.freeVars -- Set(f, x)).asInstanceOf[Set[QElem]])
       val tq = QType(TFun(f, x, at, rt), q)
       val fl = check(tenv, e, tq)
       (fl, tq)
+    case ELam(f, x, at, body, None) =>
+      // If there is only argument type, we infer the return type and
+      // check the whole lambda term again
+      val q = Qual((body.freeVars -- Set(f, x)).asInstanceOf[Set[QElem]])
+      val (bodyFl, rt) = infer(tenv + (x -> at), body)
+      val tq = QType(TFun(f, x, at, rt), q)
+      val fl = check(tenv, ELam(f, x, at, body, Some(rt)), tq)
+      (fl, tq)
   }
 }
 

diff --git a/src/test/scala/avoidancestlc/TypeCheck.scala b/src/test/scala/avoidancestlc/TypeCheck.scala
@@ -14,13 +14,60 @@ import TypeSyntax.given_Conversion_Type_QType
 import ExprSyntax.given_Conversion_Int_ENum
 
 class AvoidanceSTLCTests extends AnyFunSuite {
-  /*
   test("escaping closures") {
     val e1 =
       let("x" ⇐ alloc(3)) {
         λ("f", "z")("f"♯(TNum ~> TNum)) { x.deref }
       }
     assert(topTypeCheck(e1) == (TFun("f", "z", TNum^(), TNum^()) ^ ◆))
+
+    val e2 =
+      (λ("x" ⦂ (TRef(TNum) ^ ◆)) { λ("f", "z")("f"♯(TNum ~> TNum)) { x.deref } })(alloc(3))
+    assert(topTypeCheck(e2) == (TFun("f", "z", TNum^(), TNum^()) ^ ◆))
+
+    //    let x = alloc(3) in λf(z).x
+    // or ( λ(x). λf(z).x )(alloc(3))
+    val e3 =
+      (λ("x" ⦂ (TRef(TNum) ^ ◆)) { λ("f", "z")("f"♯(TNum ~> (TRef(TNum) ^ "x"))) { x } })(alloc(3))
+    // The type checker should infer the avoidance of `x` and instead use `f` in the return qualifier
+    assert(topTypeCheck(e3) == (TFun("f", "z", TNum^(), TRef(TNum^())^"f") ^ ◆))
+
+    val e3_let =
+      let("x" ⇐ alloc(0)) {
+        λ("f", "z")("f"♯(TNum ~> (TRef(TNum) ^ "x"))) { x }
+      }
+    assert(topTypeCheck(e3_let) == (TFun("f", "z", TNum^(), TRef(TNum^())^"f") ^ ◆))
+
+    val e3_alias = {
+      val f = λ("x" ⦂ (TRef(TNum) ^ ◆)) {
+        let ("y" ⇐ x) {
+          λ("f", "z")("f"♯(TNum ~> (TRef(TNum) ^ "y"))) { y }
+        }
+      }
+      val arg = alloc(3)
+      f(arg)
+    }
+    assert(topTypeCheck(e3_alias) == (TFun("f", "z", TNum^(), TRef(TNum^())^"f") ^ ◆))
+
+    // Manually annotate the return qualifier to self-ref `f` (not necessary)
+    val e4 =
+      (λ("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 =
+      let("x" ⇐ alloc(0)) {
+        λ("f", "z")("f"♯(TNum ~> (TRef(TNum) ^ "f"))) { x }
+      }
+    assert(topTypeCheck(e4_let) == (TFun("f", "z", TNum^(), TRef(TNum)^"f") ^ ◆))
+
+    val e5 = {
+      val f = λ("x" ⦂ (TRef(TNum) ^ ◆)) {
+        let ("y" ⇐ x) {
+          λ("f", "z")("f"♯(TNum ~> (TRef(TNum) ^ "f"))) { y }
+        }
+      }
+      val arg = alloc(3)
+      f(arg)
+    }
+    assert(topTypeCheck(e5) == (TFun("f", "z", TNum^(), TRef(TNum)^"f") ^ ◆))
   }
-    */
 }