From 7d4203dba2915efae35ce73750c4ee61e98073a7 Mon Sep 17 00:00:00 2001
From: Guannan Wei <wei220@purdue.edu>
Date: Wed, 10 Jul 2024 16:46:25 +0200
Subject: [PATCH] remove fresh from filter; more tests

---
 src/main/scala/avoidancestlc/Parser.scala    |  2 +-
 src/main/scala/avoidancestlc/TypeCheck.scala | 10 +--
 src/test/scala/avoidancestlc/TypeCheck.scala | 66 ++++++++++++++++++++
 3 files changed, 73 insertions(+), 5 deletions(-)

diff --git a/src/main/scala/avoidancestlc/Parser.scala b/src/main/scala/avoidancestlc/Parser.scala
index 552c4ea..20c6ca2 100644
--- a/src/main/scala/avoidancestlc/Parser.scala
+++ b/src/main/scala/avoidancestlc/Parser.scala
@@ -104,7 +104,7 @@ class DiamondVisitor extends DiamondParserBaseVisitor[ir.IR] {
   import DiamondParser._
   import ir._
 
-  val coreTop: core.QType = ??? //core.QType(core.Type.TTop, core.Qual.fresh)
+  lazy val coreTop: core.QType = ??? //core.QType(core.Type.TTop, core.Qual.fresh)
 
   def error = ???
 
diff --git a/src/main/scala/avoidancestlc/TypeCheck.scala b/src/main/scala/avoidancestlc/TypeCheck.scala
index b8c8411..87ac15a 100644
--- a/src/main/scala/avoidancestlc/TypeCheck.scala
+++ b/src/main/scala/avoidancestlc/TypeCheck.scala
@@ -357,6 +357,7 @@ def isVar(e: Expr): Boolean = e match
 def wellFormed(tenv: TEnv, t: QType): Boolean =
   t.freeVars.subsetOf(tenv.dom)
 
+// check returns the filter
 def check(tenv: TEnv, e: Expr, tq: QType): Qual = e match {
   case ELam(f, x, at@QType(t, p), body, rt@Some(QType(u, r))) =>
     // Note: assume that at/rt is consistent with the provided ft
@@ -364,16 +365,17 @@ def check(tenv: TEnv, e: Expr, tq: QType): Qual = e match {
     val r1 = if (p.contains(f)) r else r.subst(f, q)
     val x1 = if (p.isFresh && p ⊆ r1) Qual.singleton(x) else Qual.untrack
     val fl = check(tenv + (x -> QType(t, p.subst(f, q))), body,
-              QType(u, x1 ++ r.subst(f, q)))
-    assert(fl ⊆ (q + x), "must be a subset of the provided qualifier")
-    p ++ q
+                   QType(u, x1 ++ r.subst(f, q)))
+    assert(fl ⊆ (q + x), s"filter must be a subset of the provided qualifier: $fl ⊆ ${q + x}")
+    (p ++ q) - Fresh()
   case _ =>
     val QType(t, q) = tq
     val (fl1, q1) = checkInfer(tenv, e, t)
     val Some(fl2) = subQualCheck(tenv, q1, q)
-    fl1 ++ fl2
+    (fl1 ++ fl2) - Fresh()
 }
 
+// infer returns the filter and the inferred type
 def infer(tenv: TEnv, e: Expr): (Qual, QType) = {
   e match {
     case EUnit => (Qual.untrack, QType(TUnit, Qual.untrack))
diff --git a/src/test/scala/avoidancestlc/TypeCheck.scala b/src/test/scala/avoidancestlc/TypeCheck.scala
index 31236cb..7f39aad 100644
--- a/src/test/scala/avoidancestlc/TypeCheck.scala
+++ b/src/test/scala/avoidancestlc/TypeCheck.scala
@@ -4,6 +4,7 @@ import org.scalatest.matchers.should.Matchers
 
 import diamond._
 import diamond.avoidancestlc.core._
+import diamond.avoidancestlc.Parser._
 
 import core.Type._
 import core.Expr._
@@ -14,6 +15,8 @@ import TypeSyntax.given_Conversion_Type_QType
 import ExprSyntax.given_Conversion_Int_ENum
 
 class AvoidanceSTLCTests extends AnyFunSuite {
+  def parseAndCheck(s: String): QType = topTypeCheck(parseToCore(s))
+
   test("escaping closures") {
     val e1 =
       let("x" ⇐ alloc(3)) {
@@ -70,4 +73,67 @@ class AvoidanceSTLCTests extends AnyFunSuite {
     }
     assert(topTypeCheck(e5) == (TFun("f", "z", TNum^(), TRef(TNum)^"f") ^ ◆))
   }
+
+  test("escaping closures -- surface syntax") {
+    val p0 = """
+    def f0(x: Int) =
+      val c = Ref x;
+      g() => { c };
+    f0(0)
+    """
+    assert(parseAndCheck(p0) == (TFun("g","𝑥#0",TUnit^(),TRef(TNum)^"g")^ ◆))
+
+    val p1 = """
+    def f1(x: Int) =
+      val c = Ref x;
+      g(): Ref[Int]^g => { c };
+    f1(0)
+    """
+    assert(parseAndCheck(p1) == (TFun("g","𝑥#0",TUnit^(),TRef(TNum)^"g")^ ◆))
+
+    val p2 = """
+    def f2(x: Int): (g() => Ref[Int]^g)^<> =
+      val c = Ref x;
+      g(): Ref[Int]^g => { c };
+    f2(0)
+    """
+    assert(parseAndCheck(p2) == (TFun("g","𝑥#0",TUnit^(),TRef(TNum)^"g")^ ◆))
+
+    val p3 = """
+    def f3(x: Int): (g() => Ref[Int]^g)^<> =
+      val c = Ref x;
+      def g(): Ref[Int]^g = c;
+      g;
+    f3(0)
+    """
+    assert(parseAndCheck(p3) == (TFun("g","𝑥#0",TUnit^(),TRef(TNum)^"g")^ ◆))
+
+    val p4 = """
+    def f4(x: Int): (g() => Ref[Int]^g)^<> =
+      val c = Ref x;
+      val g = g(): Ref[Int]^g => { c };
+      g;
+    f4(0)
+    """
+    assert(parseAndCheck(p4) == (TFun("g","𝑥#0",TUnit^(),TRef(TNum)^"g")^ ◆))
+
+    val p5 = """
+    def f5(x: Int): (g() => Ref[Int]^g)^<> =
+      val c = Ref x;
+      val g: (g() => Ref[Int]^g)^c = g(): Ref[Int]^g => { c };
+      g;
+    f5(0)
+    """
+    assert(parseAndCheck(p5) == (TFun("g","𝑥#0",TUnit^(),TRef(TNum)^"g")^ ◆))
+
+    // written as anonymous functions:
+    val p6 = """
+    def f6(x: Int): (g() => Ref[Int]^g)^<> =
+      ((c: Ref[Int]^<>) => {
+         g(): Ref[Int]^g => { c }
+      })(Ref x);
+    f6(0)
+    """
+    assert(parseAndCheck(p6) == (TFun("g","𝑥#0",TUnit^(),TRef(TNum)^"g")^ ◆))
+  }
 }
\ No newline at end of file