init and qualifier upcasting/checking

src/main/scala/Common.scala

@@ -20,4 +20,5 @@ case class AssocList[K, T](m: List[(K, T)]):
   def filter(q: Set[K]): AssocList[K, T] = AssocList(m.filter((k, v) => q.contains(k)))
   def dom: Set[K] = m.map(_._1).toSet
   def contains(k: K): Boolean = dom.contains(k)
+  def isEmpty(): Boolean = m.isEmpty
   override def toString = s"""[${m.mkString("; ")}]"""

src/main/scala/avoidancestlc/Lang.scala

@@ -0,0 +1,52 @@
+package diamond.avoidancestlc
+
+import diamond._
+
+/* STLC + Subtyping + Reference + Diamond-flavored reachability types */
+
+/* Types */
+
+enum Type:
+  case TUnit
+  case TNum
+  case TBool
+  case TFun(id: String, arg: String, t1: QType, t2: QType)
+  case TRef(t: QType)
+
+import Type._
+
+/* Qualifiers */
+
+case class Fresh():
+  override def toString = "◆"
+
+type QElem = String | Fresh
+
+object Qual:
+  def untrack: Qual = Qual(Set())
+  def fresh: Qual = Qual(Set(Fresh()))
+  def singleton(x: String): Qual = Qual(Set(x))
+
+case class Qual(set: Set[QElem]):
+  override def toString =
+    if (set.isEmpty) "∅"
+    else if (set.size == 1) set.head.toString
+    else s"""{${set.mkString(",")}}"""
+
+case class QType(ty: Type, q: Qual = Qual.untrack):
+  override def toString = s"$ty^$q"
+
+/* Expressions */
+
+enum Expr:
+  case EUnit
+  case ENum(n: Int)
+  case EBool(b: Boolean)
+  case EVar(x: String)
+  case ELam(f: String, x: String, at: QType, body: Expr, rt: Option[QType])
+  case EApp(e1: Expr, e2: Expr, fresh: Option[Boolean] = None)
+  case ELet(x: String, t: Option[QType], rhs: Expr, body: Expr, global: Boolean = false)
+  case EAlloc(init: Expr)
+  case EAssign(lhs: Expr, rhs: Expr)
+  case EDeref(e: Expr)
+  case EAscribe(e: Expr, t: QType)

src/main/scala/avoidancestlc/TypeCheck.scala

@@ -0,0 +1,67 @@
+package diamond.avoidancestlc
+
+import diamond._
+import Type._
+import Expr._
+
+/* Typing environment */
+
+case class TEnv(m: AssocList[String, QType], observable: Set[String] = Set()):
+  def apply(x: String): QType = m(x)
+  def +(xt: (String, QType)) = xt match {
+    case (x, t: QType) => TEnv(m + (x -> t), observable + x)
+  }
+  def filter(q: Set[String]): TEnv = TEnv(m, observable.intersect(q))
+  def filter(q: Qual): TEnv = filter(q.varSet)
+  def dom: Set[String] = m.dom
+  def isEmpty(): Boolean = m.isEmpty()
+
+object TEnv:
+  def empty: TEnv = TEnv(AssocList.empty)
+  def unapply(g: TEnv): Option[((String, QType), TEnv)] =
+    if (g.isEmpty()) None else Some((g.m.m.head, TEnv(AssocList(g.m.m.tail))))
+
+extension (q: Qual)
+  def contains(x: QElem): Boolean = q.set.contains(x)
+  def varSet: Set[String] = (q.set - Fresh()).asInstanceOf[Set[String]]
+  def withVarSet[T](f: Set[String] => Qual): Qual =
+    val res = f(varSet)
+    if (q.isFresh) res + Fresh() else res
+  def size: Int = q.set.size
+  def isUntrack: Boolean = q.set.isEmpty
+  def isFresh: Boolean = q.set.contains(Fresh())
+  def nonFresh: Boolean = !q.set.contains(Fresh())
+  def -(x: QElem): Qual = Qual(q.set - x)
+  def +(x: QElem): Qual = Qual(q.set + x)
+  def ++(q2: Set[QElem]): Qual = Qual(q.set ++ q2)
+  def ++(q2: Qual): Qual = Qual(q.set ++ q2.set)
+  def \(q2: Qual): Qual = Qual(q.set -- q2.set)
+  def ∪(q2: Qual): Qual = Qual(q.set ++ q2.set)
+  def ⊆(q2: Qual): Boolean = q.set.subsetOf(q2.set)
+  def ⊆(Γ: TEnv): Boolean = q.set.subsetOf(Γ.dom.asInstanceOf[Set[QElem]] + Fresh())
+  def ⊔(q2: Qual): Qual = Qual(q.set ++ q2.set)
+  def subst(from: String, to: Qual): Qual =
+    if (q.contains(from)) q - from ++ to.set else q
+  def rename(from: String, to: String): Qual =
+    q.subst(from, Qual.singleton(to))
+
+/* Qualifier upcasting */
+
+def qualUpcast(g: TEnv, p: Qual, r: Qual): (Qual, Qual) = {
+  g match {
+    case TEnv((x, QType(t, q)), tail) =>
+      if (p.contains(x) && !r.contains(x) && q.nonFresh) {
+        val (fl, p1) = qualUpcast(tail, p.subst(x, q), r)
+        (fl ++ q, p1) // QA-Head
+      } else {
+        qualUpcast(tail, p, r) // QA-Skip
+      }
+    case _ => (p, p) // QA-Nil
+  }
+}
+
+/* Qualifier checking */
+
+def subQualCheck(g: TEnv, p: Qual, r: Qual): Option[Qual] =
+  val (fl, p1) = qualUpcast(g, p, r)
+  if (p1 ⊆ r) Some(fl ++ r) else None

src/main/scala/qualstlc/TypeCheck.scala

@@ -96,7 +96,7 @@ extension (t: Type)
   def ⊔(t2: Type)(using Γ: TEnv): Type =
     if (t.isSubtype(t2)) t2
     else if (t2.isSubtype(t)) t
-    else throw RuntimeException(s"No least upper bound between $t and $t2") 
+    else throw RuntimeException(s"No least upper bound between $t and $t2")
   def substQual(from: String, to: Qual): Type = t match
     case TUnit | TNum | TBool => t
     case TFun(f, x, t1, t2) =>