Temporarily support ADT and ADT matching typing in InvalML

hkmc2/shared/src/main/scala/hkmc2/codegen/Lowering.scala

@@ -596,7 +596,7 @@ class Lowering()(using Config, TL, Raise, State, Ctx):
 
     case Quoted(body) => quote(body)(k)
 
-    // * BbML-specific cases: t.Cls#field and mutable operations
+    // * InvalML-specific cases: t.Cls#field and mutable operations
     case sp @ SelProj(prefix, _, proj) =>
       setupSelection(prefix, proj, sp.sym)(k)
     case Region(reg, body) =>

hkmc2/shared/src/main/scala/hkmc2/bbml/ConstraintSolver.scala → hkmc2/shared/src/main/scala/hkmc2/invalml/ConstraintSolver.scala

@@ -1,5 +1,5 @@
 package hkmc2
-package bbml
+package invalml
 
 import scala.collection.mutable
 
@@ -9,12 +9,11 @@ import mlscript.utils.*, shorthands.*
 import utils.*
 import utils.Scope
 
-// * TODO use mutabnle cache instead for correct asymptotic complexity
-type Cache = Set[(Type, Type)]
+type Cache = mutable.HashSet[(Type, Type)]
 type ExtrudeCache = mutable.HashMap[(Uid[InfVar], Bool), InfVar]
 
 case class CCtx(cache: Cache, parents: Ls[(Type, Type)], origin: Term, exp: Opt[GeneralType])(using Scope):
-  def err(using Raise) =
+  def err(using Raise, InvalCtx) =
     raise(ErrorReport(
       msg"Type error in ${origin.describe}${exp match
           case S(ty) => msg" with expected type ${ty.show}"
@@ -25,23 +24,23 @@ case class CCtx(cache: Cache, parents: Ls[(Type, Type)], origin: Term, exp: Opt[
       )
     ))
   def nest(sub: (Type, Type)): CCtx =
-    copy(cache = cache + sub, parents = parents match
+    copy(cache = cache += sub, parents = parents match
       case `sub` :: _ => parents
       case _ =>  sub :: parents
     )
 object CCtx:
-  inline def init(origin: Term, exp: Opt[GeneralType])(using Scope) = CCtx(Set.empty, Nil, origin, exp)
+  inline def init(origin: Term, exp: Opt[GeneralType])(using Scope) = CCtx(mutable.HashSet.empty, Nil, origin, exp)
 def cctx(using CCtx): CCtx = summon
 
 class ConstraintSolver(infVarState: InfVarUid.State, elState: Elaborator.State, tl: TraceLogger):
   import tl.{trace, log}
 
-  import hkmc2.bbml.NormalForm.*
+  import hkmc2.invalml.NormalForm.*
 
   private def freshXVar(lvl: Int, sym: Symbol, hint: Str): InfVar =
     InfVar(lvl, infVarState.nextUid, new VarState(), false)(InstSymbol(sym)(using elState), hint)
 
-  def extrude(ty: Type)(using lvl: Int, pol: Bool, cache: ExtrudeCache, bbctx: BbCtx, cctx: CCtx, tl: TL): Type =
+  def extrude(ty: Type)(using lvl: Int, pol: Bool, cache: ExtrudeCache, invalctx: InvalCtx, cctx: CCtx, tl: TL): Type =
   trace[Type](s"Extruding[${printPol(pol)}] ${ty.showDbg}", r => s"~> ${r.showDbg}"):
     if ty.lvl <= lvl then ty else ty.toBasic/*TODO improve extrude directly*/ match
     case ClassLikeType(sym, targs) =>
@@ -79,7 +78,7 @@ class ConstraintSolver(infVarState: InfVarUid.State, elState: Elaborator.State,
     case NegType(ty) => Type.mkNegType(extrude(ty)(using lvl, !pol))
     case Top | Bot => ty
 
-  private def constrainConj(conj: Conj)(using BbCtx, CCtx, TL): Unit = trace(s"Constraining ${conj.showDbg}"):
+  private def constrainConj(conj: Conj)(using InvalCtx, CCtx, TL): Unit = trace(s"Constraining ${conj.showDbg}"):
     conj match
       case Conj(i, u, (v, pol) :: tail) =>
         var rest = Conj(i, u, tail)
@@ -89,13 +88,13 @@ class ConstraintSolver(infVarState: InfVarUid.State, elState: Elaborator.State,
           if pol then
             val nc = Type.mkNegType(bd).toDnf // always cache the normal form to avoid unexpected cache misses
             log(s"New bound: ${v.showDbg} <: ${nc.showDbg}")
-            cctx.nest(v -> nc) givenIn:
+            cctx.nest(v.toDnf -> nc) givenIn:
               v.state.upperBounds ::= nc
               v.state.lowerBounds.foreach(lb => constrainImpl(lb, nc))
           else
             val c = bd.toDnf // always cache the normal form to avoid unexpected cache misses
             log(s"New bound: ${v.showDbg} :> ${c.showDbg}")
-            cctx.nest(c -> v) givenIn:
+            cctx.nest(c -> v.toDnf) givenIn:
               v.state.lowerBounds ::= c
               v.state.upperBounds.foreach(ub => constrainImpl(c, ub))
       case Conj(i, u, Nil) => (conj.i, conj.u) match
@@ -122,10 +121,10 @@ class ConstraintSolver(infVarState: InfVarUid.State, elState: Elaborator.State,
           // raise(ErrorReport(msg"Cannot solve ${conj.i.toString()} <: ${conj.u.toString()}" -> N :: Nil))
           cctx.err
 
-  private def constrainDNF(disj: Disj)(using BbCtx, CCtx, TL): Unit =
+  private def constrainDNF(disj: Disj)(using InvalCtx, CCtx, TL): Unit =
     disj.conjs.foreach(constrainConj(_))
 
-  private def constrainArgs(lhs: TypeArg, rhs: TypeArg)(using BbCtx, CCtx, TL): Unit =
+  private def constrainArgs(lhs: TypeArg, rhs: TypeArg)(using InvalCtx, CCtx, TL): Unit =
     constrainImpl(rhs.negPart, lhs.negPart)
     constrainImpl(lhs.posPart, rhs.posPart)
 
@@ -137,13 +136,13 @@ class ConstraintSolver(infVarState: InfVarUid.State, elState: Elaborator.State,
     case NegType(ty) => NegType(inlineSkolemBounds(ty, !pol))
     case _: ClassLikeType | _: FunType | _: InfVar | Top | Bot => ty
 
-  private def constrainImpl(lhs: Type, rhs: Type)(using BbCtx, CCtx, TL): Unit =
+  private def constrainImpl(lhs: Type, rhs: Type)(using InvalCtx, CCtx, TL): Unit =
     val p = lhs.toDnf -> rhs.toDnf
     if cctx.cache(p) then log(s"Cached!")
     else trace(s"CONSTRAINT ${lhs.showDbg} <: ${rhs.showDbg}"):
       cctx.nest(p) givenIn:
         val ty = dnf(inlineSkolemBounds(lhs & rhs.!, true)(using Set.empty)) 
         constrainDNF(ty)
-  def constrain(lhs: Type, rhs: Type)(using BbCtx, CCtx, TL): Unit =
+  def constrain(lhs: Type, rhs: Type)(using InvalCtx, CCtx, TL): Unit =
     constrainImpl(lhs, rhs)