Add Logic Subtyping Implementation

hkmc2/shared/src/main/scala/hkmc2/semantics/Symbol.scala

@@ -265,6 +265,12 @@ class InstSymbol(val origin: Symbol)(using State) extends LocalSymbol:
   override def toLoc: Option[Loc] = origin.toLoc
   def subst(using sub: SymbolSubst): InstSymbol = sub.mapInstSym(this)
 
+class InfVarSymbol(val origin: Symbol | Term, val hint: Str = "")(using State) extends LocalSymbol:
+  override def nme: Str = origin match
+    case x: Symbol => x.nme ++ hint
+    case x: Term => hint
+  override def toLoc: Option[Loc] = origin.toLoc
+  def subst(using sub: SymbolSubst): InfVarSymbol = ???
 
 class VarSymbol(val id: Ident)(using State)
     extends LocalVarSymbol(id.name)

hkmc2/shared/src/main/scala/hkmc2/typing/ConstraintSolver.scala

@@ -0,0 +1,151 @@
+package hkmc2
+package typing
+package logicsub
+
+import scala.collection.mutable
+import syntax.*
+import semantics.*
+import Message.MessageContext
+import hkmc2.utils.*, shorthands.*
+import utils.*
+import utils.Scope
+
+type Cache = mutable.HashSet[(Type, Type)]
+type ExtrudeCache = mutable.HashMap[(InfVarSymbol, Bool), InfVar]
+
+case class CCtx(cache: Cache, parents: Ls[(Type, Type)], origin: Term, exp: Opt[InfType])(using Scope):
+  def err(using ctx: KCtx)(using TL, Raise) = 
+    given CCtx = this
+    ctx.err(parents, origin, exp)
+  def nest(sub: (Type, Type)): CCtx =
+    copy(cache = cache += sub, parents = parents match
+      case `sub` :: _ => parents
+      case _ =>  sub :: parents
+    )
+object CCtx:
+  inline def init(origin: Term, exp: Opt[InfType])(using Scope) =
+    CCtx(mutable.HashSet.empty, Nil, origin, exp)
+
+object ConstraintSolver:
+  private def log(msg: => Any, noIndent: Bool = false)(using tl: TL) = tl.log(msg, noIndent)
+
+  private def constrainConj(conj: Conj)(using ctx: KCtx, cctx:CCtx)(using TL, Raise): Unit =
+  tl.trace(s"Constraining ${conj.showDbg}"):
+    conj match
+      case Conj(i, u, S(v), S(w), xs, ys) if w.lvl > v.lvl =>
+        val rest = Conj(i, u, S(v), N, xs, ys)
+        val nc = rest.toDnf // always cache the normal form to avoid unexpected cache misses
+        log(s"New bound: ${v.showDbg} >: ${nc.showDbg}")
+        cctx.nest(nc -> w.toDnf) givenIn:
+          ctx.addlb(nc, w)
+      case Conj(i, u, S(v), w, xs, ys) =>
+        val rest = Conj(i, u, N, w, xs, ys)
+        val nc = (~rest).toDnf // always cache the normal form to avoid unexpected cache misses
+        log(s"New bound: ${v.showDbg} <: ${nc.showDbg}")
+        cctx.nest(v.toDnf -> nc) givenIn:
+          ctx.addub(v, nc)
+      case Conj(i, u, N, S(v), xs,ys) =>
+        val rest = Conj(i, u, N,N,xs,ys)
+        val c = rest.toDnf // always cache the normal form to avoid unexpected cache misses
+        log(s"New bound: ${v.showDbg} :> ${c.showDbg}")
+        cctx.nest(c -> v.toDnf) givenIn:
+          ctx.addlb(c, v)
+      case Conj(NF.Inter(x :: Nil), NF.Union(Nil), N,N,_,_) =>
+        val da = x.args.iterator.zip(x.congr).collect:
+          case (t, true) => t.posPart
+        val d = (x.refinement.values ++ da).toList
+        if d.isEmpty then cctx.err
+        else ctx.constrain(d.tail.foldLeft(ctx.sub(d.head, Bot))((k, t) => ctx.or(k, ctx.sub(t, Bot))))
+      case Conj(NF.Inter(x :: Nil), NF.Union(y :: Nil), N,N,_,_) =>
+        val da = x.args.iterator.zip(x.congr).collect:
+          case (t, true) => t.posPart
+        val d = (x.refinement.values ++ da).toList
+        val xrm = x.refinement.toMap
+        val yrm = y.refinement.toMap
+        val sp = ctx.asSubcls(x,y.sym)
+        if sp.isEmpty || !yrm.keySet.subsetOf(xrm.keySet) then
+          if d.isEmpty then cctx.err
+          else ctx.constrain(d.map(ctx.sub(_, Bot)).reduce(ctx.or))
+        else
+          val x = sp.get
+          val u = x.args.zip(y.args).flatMap(ctx.subArg)
+          val w = y.refinement.map:
+            case (a,b) => ctx.sub(xrm(a), b)
+          val ds = x.refinement.filterNot(f => yrm.contains(f._1)).map:
+            case (_,t) => ctx.sub(t,Bot)
+          (u++w).foreach: k =>
+            ctx.constrain((ds ++ Ls(k)).reduce(ctx.or))
+      case Conj(NF.Inter(xs @ (x :: _)), NF.Union(y :: Nil), N,N,_,_) =>
+        if x.sym === y.sym then
+          val k = x.ov.get
+          val u = xs.map(_.args(k).negPart.discriminator)
+          val w = u.reduce[Type](_|_)
+          val in = y.args(k)
+          ctx.constrain(ctx.sub(in.negPart, w))
+          u.lazyZip(xs).foreach: (p, c) =>
+            val d = ctx.sub(in.negPart, ~p)
+            val r = y.copy(args = y.args.updated(k, Wildcard(p & in.negPart, in.posPart)))
+            val s = ctx.sub(c, r)
+            ctx.constrain(ctx.or(d, s))
+        else cctx.err
+      case Conj(k @ NF.Inter(x :: _), NF.Union(ys @ (_ :: _)), N,N,ws,zs) =>
+        def h(y: ClassLikeType) =
+          def f(u: Ls[TypeArg], w: Ls[TypeArg], s: Ls[TypeArg], p:Ls[Bool])
+              : Ls[ClassLikeType] = (w,p) match
+            case (Nil, _) => Nil
+            case (t::ws, true::ps) =>
+              val a = u ++ (Wildcard.out(~t.posPart)::s)
+              y.copy(args = a) :: f(s.head::u, ws, s.tail, ps)
+            case (t::ws, false::ps) => f(s.head::u, ws, s.tail, ps)
+            case _ => ???
+          def g(u: Ls[(Tree.Ident, Type)]) =
+            val w = y.args.map(_ => Wildcard.empty)
+            y.refinement.map((a,t) => y.copy(args = w, refinement = (a,~t)::Nil))
+          f(Nil, y.args, y.args.map(_ => Wildcard.empty), y.congr) ++ g(y.refinement)
+        val (ps,t) = ys.partition(_.partialpattern)
+        val xrs = x.refinement.keys.toSet
+        val qs = ps.filter: p =>
+          ctx.asSubcls(x,p.sym).isDefined && p.refinement.keys.forall(xrs.contains)
+        val ks = qs.foldLeft(Ls(k)): (ks, y) =>
+          ks.flatMap(k => h(y).map(c => k.merge(NF.Inter(Ls(c))).get))
+        ks.foreach(k => constrainConj(Conj(k, NF.Union(t),N,N,ws,zs)))
+      case _ =>
+        raise(ErrorReport(msg"Cannot solve ${conj.i.toString()} <: ⊥" -> N :: Nil))
+        cctx.err
+
+  // private class SkolemBoundsInliner(using ctx: KCtx) extends TypeMap:
+  //   val cache: mutable.HashSet[InfVarSymbol] = mutable.HashSet.empty
+  //   override def apply(pol: Bool)(t: Type) = t.toBasic match
+  //     case v @ InfVar(_, s, true) if !cache(s) =>
+  //       cache += s
+  //       apply(pol)(if pol
+  //         then ctx.ubs(s).foldLeft[Type](v)(_ & _)
+  //         else ctx.lbs(s).foldLeft[Type](v)(_ | _))
+  //     case _: ClassLikeType | _: InfVar => t
+  //     case t => super.apply(pol)(t)
+  private def inlineSkolemBounds(ty: Type)(using KCtx): Type = ty // TODO
+  //   (new SkolemBoundsInliner)(true)(ty)
+
+  def constrainImpl(lhs: Type, rhs: Type)
+      (using ctx: KCtx, cctx:CCtx)(using TL, Raise)
+      : Unit =
+    val p = lhs.toDnf -> rhs.toDnf
+    if cctx.cache(p) then log(s"Cached!")
+    else tl.trace(s"CONSTRAINT ${lhs.showDbg} <: ${rhs.showDbg}"):
+      cctx.nest(p) givenIn:
+        val disj = inlineSkolemBounds(lhs & ~rhs).toDnf
+        disj.cs.foreach(constrainConj(_))
+
+  def constrain(lhs: Type, rhs: Type)(using ctx: KCtx, cctx:CCtx)(using TL, Raise): Unit =
+    val (ps, ts) = rhs.disjuncts.toList.partition(_.partialpattern)
+    if ts.length > 1 then
+      val p = lhs.toDnf -> rhs
+      if cctx.cache(p) then log(s"Cached!")
+      else tl.trace(s"CONSTRAINT ${lhs.showDbg} <: ${rhs.showDbg}"):
+        cctx.nest(p) givenIn:
+          val u = ps.foldLeft(lhs)((x, y) => x & ~y)
+          val qs = ts.map(_.discriminator)
+          constrainImpl(u, qs.reduce(_ | _))
+          qs.zip(ts).foreach((q, y) => constrainImpl(q & u, y))
+    else
+      constrainImpl(lhs, rhs)

hkmc2/shared/src/main/scala/hkmc2/typing/NormalForm.scala

@@ -0,0 +1,100 @@
+package hkmc2
+package typing
+package logicsub
+
+import scala.annotation.tailrec
+
+import syntax.*
+import semantics.*
+import Message.MessageContext
+import hkmc2.utils.*, shorthands.*
+import utils.*
+import utils.Scope
+
+sealed abstract class NormalForm extends TypeExt
+
+object NF:
+  final case class Inter(v: Ls[ClassLikeType]) extends NormalForm:
+    lazy val toBasic = v.foldLeft[Type](Top)(_ & _).toBasic
+    def merge(other: Inter): Opt[Inter] =
+      other.v.foldLeft(Opt(v))((r, w) => r.flatMap(w.merge(_))).map(Inter(_))
+
+  final case class Union(v: Ls[ClassLikeType]) extends NormalForm:
+    lazy val toBasic = v.foldLeft[Type](Bot)(_ | _).toBasic
+    def merge(other: Union) = Union(v ++ other.v)
+
+  object Inter:
+    val empty = Inter(Nil)
+  object Union:
+    val empty = Union(Nil)
+
+final case class Disj(cs: Ls[Conj]) extends NormalForm:
+  lazy val toBasic = cs.foldLeft[Type](Bot)(_ | _).toBasic
+  def isBot = cs.isEmpty
+
+final case class Conj(
+  i: NF.Inter, u: NF.Union,
+  v1: Opt[InfVar], v2: Opt[InfVar],
+  ps: Ls[InfVar], ns: Ls[InfVar]
+) extends NormalForm:
+  lazy val toBasic = (i.toBasic & ~u.toBasic & v1.getOrElse(Top) & v2.fold(Top)(~_)).toBasic
+  def merge(that: Conj)(using TL): Opt[Conj] =
+  tl.traceNot[Opt[Conj]](s"merge ${this.showDbg} and ${that.showDbg}", r => s"= ${r.map(_.showDbg)}"):
+    val Conj(i1, u1, v1, w1, x1, y1) = this
+    val Conj(i2, u2, v2, w2, x2, y2) = that
+    val xs = (x1 ++ x2).distinct
+    val ys = (y1 ++ y2).distinct
+    if xs.intersect(ys).nonEmpty then N
+    else i1.merge(i2).flatMap: i =>
+      val u = u1.merge(u2)
+      (v1.orElse(v2), w1.orElse(w2)) match
+        case (S(v), S(w)) if v.sym === w.sym => N
+        case (v,w) => S(Conj(i, u, v, w, xs, ys))
+
+object Conj:
+  val empty: Conj = Conj(NF.Inter.empty, NF.Union.empty, N, N, Nil, Nil)
+  def mkVar(v: InfVar, pol: Bool) =
+    if pol then
+      Conj(NF.Inter.empty, NF.Union.empty, S(v), N, Nil, Nil)
+    else Conj(NF.Inter.empty, NF.Union.empty, N, S(v), Nil, Nil)
+  def mkInter(inter: ClassLikeType) =
+    Conj(NF.Inter(Ls(inter)), NF.Union.empty, N, N, Nil, Nil)
+  def mkUnion(union: ClassLikeType) =
+    Conj(NF.Inter.empty, NF.Union(Ls(union)), N, N, Nil, Nil)
+object Disj:
+  val bot = Disj(Nil)
+  val top = Disj(Ls(Conj.empty))
+
+object NormalForm:
+  def inter(lhs: Disj, rhs: Disj)(using TL): Disj =
+  tl.traceNot[Disj](s"inter ${lhs.showDbg} and ${rhs.showDbg}", r => s"= ${r.showDbg}"):
+    if lhs.isBot || rhs.isBot then Disj.bot
+    else Disj(lhs.cs.flatMap(lhs => rhs.cs.flatMap(rhs => lhs.merge(rhs) match {
+      case S(conj) => conj :: Nil
+      case N => Nil
+    })))
+
+  def union(lhs: Disj, rhs: Disj): Disj = Disj(lhs.cs ++ rhs.cs)
+
+  def neg(ty: Type)(using TL): Disj =
+  tl.traceNot[Disj](s"~Disj ${ty.showDbg} ${ty.getClass} ${ty.toBasic.showDbg}", r => s"= ${r.showDbg}"):
+    ty match
+    case u: NF.Union => Disj(Ls(Conj(NF.Inter(Nil), u, N, N, Nil, Nil)))
+    case v: InfVar => Disj(Ls(Conj.mkVar(v, false)))
+    case ct: ClassLikeType => Disj(Ls(Conj.mkUnion(ct)))
+    case _ => (~ty.toBasic).toDnf
+
+  def dnf(ty: Type)(using TL): Disj =
+  tl.traceNot[Disj](s"Disj ${ty.showDbg} ${ty.getClass}", r => s"= ${r.showDbg}"):
+    ty match
+    case d: Disj => d
+    case c: Conj => Disj(Ls(c))
+    case i: NF.Inter => Disj(Ls(Conj(i, NF.Union.empty, N, N, Nil, Nil)))
+    case _ => ty.toBasic match
+    case Top => Disj.top
+    case Bot => Disj.bot
+    case v: InfVar => Disj(Ls(Conj.mkVar(v, true)))
+    case ct: ClassLikeType => Disj(Conj.mkInter(ct) :: Nil)
+    case Inter(lhs, rhs) => inter(lhs.toDnf, rhs.toDnf)
+    case Union(lhs, rhs) => union(lhs.toDnf, rhs.toDnf)
+    case Neg(ty) => neg(ty)

hkmc2/shared/src/main/scala/hkmc2/typing/TypeTraverser.scala

@@ -0,0 +1,36 @@
+package hkmc2
+package typing
+package logicsub
+
+import hkmc2.utils.*, shorthands.*
+
+// class TypeTraverser:
+//   def apply(pol: Bool)(ty: Type): Unit = ty.toBasic match
+//     case Union(x, y) => 
+//       apply(pol)(x)
+//       apply(pol)(y)
+//     case Inter(x, y) =>
+//       apply(pol)(x)
+//       apply(pol)(y)
+//     case Neg(ty) => apply(!pol)(ty)
+//     case ClassLikeType(name, targs, refine) =>
+//       targs.foreach:
+//         case Wildcard(in, out) =>
+//           apply(!pol)(in)
+//           apply(pol)(out)
+//         case ty: Type =>
+//           apply(pol)(ty)
+//           apply(!pol)(ty)
+//       refine.values.foreach(apply(pol))
+//     case _ =>
+
+class TypeMap:
+  def applyArg(pol: Bool)(t: TypeArg): TypeArg =
+    Wildcard(apply(!pol)(t.negPart), apply(pol)(t.posPart))
+  def apply(pol: Bool)(t: Type): Type = t.toBasic match
+    case Bot | Top | _: InfVar => t
+    case Union(x, y) => Union(apply(pol)(x), apply(pol)(y))
+    case Inter(x, y) => Inter(apply(pol)(x), apply(pol)(y))
+    case Neg(x) => Neg(apply(!pol)(x))
+    case ClassLikeType(n, args, refine, i,o) =>
+      ClassLikeType(n, args.map(applyArg(pol)), refine.mapValues(t => apply(pol)(t)), i,o)