Temporarily support ADT and ADT matching typing in InvalML

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

@@ -14,7 +14,7 @@ type Cache = Set[(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, BbCtx) =
     raise(ErrorReport(
       msg"Type error in ${origin.describe}${exp match
           case S(ty) => msg" with expected type ${ty.show}"

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

@@ -14,7 +14,7 @@ final case class Disj(conjs: Ls[Conj]) extends NormalForm with CachedBasicType:
   def mkBasic: BasicType =
     BasicType.union(conjs.map(_.toBasic))
   def toDnf(using TL): Disj = this
-  override def show(using Scope): Str =
+  override def show(using Scope, BbCtx): Str =
     if conjs.isEmpty then "⊥"
     else conjs.map(_.show).mkString(" ∨ ")
 
@@ -53,7 +53,7 @@ extends NormalForm with CachedBasicType:
       case (tv, false) => NegType(tv)
     })
   def toDnf(using TL): Disj = Disj(this :: Nil)
-  override def show(using Scope): Str =
+  override def show(using Scope, BbCtx): Str =
     val s = ((i :: Nil).filterNot(_.isTop).map(_.show) :::
       (u :: Nil).filterNot(_.isBot).map("¬{"+_.show+"}") :::
       vars.map:
@@ -100,7 +100,7 @@ final case class Inter(v: Opt[ClassLikeType | FunType]) extends NormalForm:
     case _ => N
   def toBasic: BasicType = v.getOrElse(Top)
   def toDnf(using TL): Disj = Disj(Conj(this, Union(N, Nil), Nil) :: Nil)
-  override def show(using Scope): Str =
+  override def show(using Scope, BbCtx): Str =
     toBasic.show
 
   override def showDbg: Str = toBasic.showDbg
@@ -130,7 +130,7 @@ extends NormalForm with CachedBasicType:
   def mkBasic: BasicType =
     BasicType.union(fun.toList ::: cls)
   def toDnf(using TL): Disj = NormalForm.neg(this)
-  override def show(using Scope): Str =
+  override def show(using Scope, BbCtx): Str =
     toType.show
 
   override def showDbg: Str = toType.showDbg
@@ -145,7 +145,7 @@ sealed abstract class NormalForm extends TypeExt:
   def subst(using map: Map[Uid[InfVar], InfVar]): ThisType =
     toBasic.subst
 
-  def show(using Scope): Str
+  def show(using Scope, BbCtx): Str
   def showDbg: Str
 
 object NormalForm:

hkmc2/shared/src/main/scala/hkmc2/bbml/PrettyPrinter.scala

@@ -3,9 +3,12 @@ package bbml
 import scala.collection.mutable.{Set => MutSet, ListBuffer}
 import utils.Scope
 
-class PrettyPrinter(output: String => Unit)(using Scope):
+class PrettyPrinter(output: String => Unit)(using Scope, BbCtx):
   def print(ty: GeneralType): Unit =
-    output(s"Type: ${ty.show}")
+    ty.show match
+    case "()" =>
+    case tyStr =>
+      output(s"Type: ${tyStr}")
     val bounds = PrettyPrinter.collectBounds(ty).distinct
     if !bounds.isEmpty then
       output("Where:")
@@ -14,7 +17,7 @@ class PrettyPrinter(output: String => Unit)(using Scope):
       }
 
 object PrettyPrinter:
-  def apply(output: String => Unit)(using Scope): PrettyPrinter = new PrettyPrinter(output)
+  def apply(output: String => Unit)(using Scope, BbCtx): PrettyPrinter = new PrettyPrinter(output)
 
   type Bound = (Type, Type) // * Type <: Type
 

hkmc2/shared/src/main/scala/hkmc2/bbml/types.scala

@@ -6,7 +6,7 @@ import syntax.*
 import semantics.*, semantics.Term.*
 import utils.*
 import scala.collection.mutable.{Set => MutSet}
-import utils.Scope
+import utils.Scope, Scope.scope
 import Elaborator.State
 
 // * General types include mono types (i.e., Type), forall quantified type, and poly function types
@@ -23,14 +23,14 @@ sealed abstract class GeneralType:
   protected type ThisType <: GeneralType
   def map(f: ThisType => ThisType): ThisType
   def subst(using map: Map[Uid[InfVar], InfVar]): ThisType
-  def show(using Scope): Str
+  def show(using Scope, BbCtx): Str
   def showDbg: Str
 
 // * Types that can be used as class type arguments
 sealed trait TypeArg:
   def lvl: Int
   def mapArg(f: Type => Type): TypeArg
-  def show(using Scope): Str
+  def show(using Scope, BbCtx): Str
   def showDbg: Str
   def & (that: TypeArg): TypeArg = (this, that) match
     case (Wildcard(in1, out1), Wildcard(in2, out2)) => Wildcard(in1 | in2, out1 & out2)
@@ -52,7 +52,7 @@ sealed trait TypeArg:
 case class Wildcard(in: Type, out: Type) extends TypeArg {
   def mapArg(f: Type => Type): Wildcard = Wildcard(f(in), f(out))
 
-  override def show(using Scope): Str = in match
+  override def show(using Scope, BbCtx): Str = in match
     case `out` => in.show
     case Bot =>
       out match
@@ -130,7 +130,7 @@ sealed abstract class Type extends GeneralType with TypeArg:
     case ComposedType(l, r, false) => l.! | r.!
     case _ => NegType(this)
 
-  protected[bbml] def paren(using Scope): Str = toBasic match
+  protected[bbml] def paren(using Scope, BbCtx): Str = toBasic match
     case _: InfVar | _: ClassLikeType | _: NegType | Top | Bot => show
     case _: ComposedType | _: FunType => s"($show)"
 
@@ -158,12 +158,13 @@ sealed abstract class BasicType extends Type:
     case NegType(ty) => Type.mkNegType(f(ty))
     case Top | Bot | _: InfVar => this
 
-  override def show(using scope: Scope): Str =
+  override def show(using Scope, BbCtx): Str =
     def printEff(eff: Type) = eff match
       case Bot => ""
       // case ty if ty == allocSkolem => ""
       case _ => s"{${eff.show}}"
     this match
+    case ClassLikeType(sym, Nil) if sym is bbctx.getCls("Unit") => "()"
     case ClassLikeType(name, targs) =>
       if targs.isEmpty then s"${name.nme}" else s"${name.nme}[${targs.map(_.show).mkString(", ")}]"
     case v @ InfVar(lvl, uid, _, isSkolem) =>
@@ -286,7 +287,7 @@ case class PolyType(tvs: Ls[InfVar], outer: Opt[InfVar], body: GeneralType) exte
 
   override lazy val isPoly: Bool = true
   override lazy val lvl: Int = (body :: tvs).map(_.lvl).max
-  override def show(using scope: Scope): Str =
+  override def show(using Scope, BbCtx): Str =
     given Scope = scope.nest
     val lst = (outer match {
       case S(outer) =>
@@ -364,7 +365,7 @@ case class PolyFunType(args: Ls[GeneralType], ret: GeneralType, eff: Type) exten
 
   lazy val isPoly: Bool = (ret :: args).exists(_.isPoly)
   lazy val lvl: Int = (ret :: eff :: args).map(_.lvl).max
-  override def show(using Scope): Str = s"(${args.map(_.show).mkString(", ")}) ->{${eff.show}} ${ret.show}"
+  override def show(using Scope, BbCtx): Str = s"(${args.map(_.show).mkString(", ")}) ->{${eff.show}} ${ret.show}"
   override def showDbg: Str = s"(${args.map(_.showDbg).mkString(", ")}) ->{${eff.showDbg}} ${ret.showDbg}"
   private lazy val mono: Opt[FunType] = if isPoly then N else
     Some(FunType(args.map {

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

@@ -17,9 +17,54 @@ trait BlockImpl(using Elaborator.State):
         stmt.desugared match
         case PossiblyAnnotated(anns, h @ Hndl(body = N)) =>
           PossiblyAnnotated(anns, h.copy(body = S(Block(stmts)))) :: Nil
-        case PossiblyAnnotated(anns, TypeDef(syntax.Cls, Ident(name), rhs, S(Block(Constructor(Block(ctors)) :: rest)))) =>
-          PossiblyAnnotated(anns, TypeDef(syntax.Cls, Ident(name), rhs, if rest.isEmpty then N else S(Block(rest)))) ::
-            (ctors.map(head => PossiblyAnnotated(anns, TypeDef(syntax.Cls, InfixApp(head, syntax.Keyword.`extends`, Ident(name)), N, N))))
+        case PossiblyAnnotated(anns, TypeDef(syntax.Cls, head, rhs, S(Block(Constructor(Block(ctors)) :: rest)))) =>
+          // A temp solution for ADTs, which desugars ADTs to normal class definitions.
+          // This will be removed after we truly support ADTs correctly.
+          // TODO: No raise contextual variable. Only `Error` nodes are returned if there is an error. 
+          val (headId, headPs) = head match
+            case id: Ident => (id, Nil)
+            case App(id: Ident, TyTup(ps)) => (id, ps)
+            case _ => Error()
+          // Temporarily use `data` annotation to distinguish the following ctors:
+          // - Ctor(...)
+          // - Ctor[...](...) extends ADT[...]
+          // since the former will be desugared to `class Ctor[...](...) extends ADT[...]`,
+          // where `Ctor[...]` and `ADT[...]` share the same type parameter list
+          def wrapGeneric(decl: Tree, res: Tree) = decl match
+            case InfixApp(_, syntax.Keyword.`extends`, _) =>
+              Annotated(Keywrd(syntax.Keyword.data), res)
+            case _ => res
+          // Generate `extends` suffix if it is not provided by users
+          // Also check if the number of type parameters is correct
+          def genExt(decl: Tree) = decl match
+            case InfixApp(_, syntax.Keyword.`extends`, ext) => ext match
+              case _: Ident if headPs.isEmpty => ext
+              case App(id: Ident, TyTup(ps)) if id.name == headId.name && ps.length == headPs.length => ext
+              case _ => Error()
+            case _ => headPs match
+              case Nil => headId
+              case ps => App(headId, TyTup(ps.map(
+                t => Tup(Tree.Modified(syntax.Keyword.`in`, N, t) :: Tree.Modified(syntax.Keyword.`out`, N, t) :: Nil)
+              )))
+          // Insert type parameters for constructors.
+          // e.g. `class Foo[T] with constructor Bar(x: T)` will be desugared to
+          // `class Bar[T](x: T) extends Foo[T]`
+          // Otherwise, the elaborator will complain `T` is not defined.
+          def genCtorHead(decl: Tree) = decl match
+            case InfixApp(decl, syntax.Keyword.`extends`, _) => decl // check will be applied in genExt
+            case App(_: Ident, tup: TyTup) => Error()
+            case App(id: Ident, ps: Tup) => App(App(id, TyTup(headPs)), ps)
+            case id: Ident => App(id, TyTup(headPs))
+            case _ => Error()
+          // Only fields modified by `val` can be extracted by pattern matching.
+          // For ADTs, all fields can be extracted, but we don't want to add `val`s manumally.
+          def insertVal(decl: Tree): Tree = decl match
+            case id: Ident => id
+            case App(f, Tup(ps)) => App(f, Tup(ps.map(p => TermDef(syntax.ImmutVal, p, N))))
+            case App(f, tup: TyTup) => App(insertVal(f), tup)
+            case _ => Error()
+          PossiblyAnnotated(anns, TypeDef(syntax.Cls, head, rhs, if rest.isEmpty then N else S(Block(rest)))) ::
+            (ctors.map(h => PossiblyAnnotated(anns, wrapGeneric(h, TypeDef(syntax.Cls, InfixApp(insertVal(genCtorHead(h)), syntax.Keyword.`extends`, genExt(h)), N, N)))))
           ::: desug(stmts)
         case stmt => stmt :: desug(stmts)
       case Nil => Nil

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

@@ -68,6 +68,11 @@ object Pattern:
    */
   type Argument = (scrutinee: BlockLocalSymbol, pattern: Tree, split: Opt[DeBrujinSplit])
 
+  /** A class-like pattern whose symbol is resolved to a class or a module. */
+  object ResolvedClassOrModule:
+    def unapply(p: Pattern.ClassLike): Opt[(ClassSymbol | ModuleSymbol, Opt[Ls[Argument]])] =
+      p.constructor.symbol.flatMap(_.asClsOrMod).map(_ -> p.arguments)
+
   /** A class-like pattern whose symbol is resolved to a class. */
   object Class:
     def unapply(p: Pattern): Opt[ClassSymbol] = p match

hkmc2/shared/src/test/mlscript/basics/ADTs.mls

@@ -15,11 +15,8 @@ class Expr[A] with
   constructor
     Lit(n: Int) { A = Int }
     Add(lhs: Expr[Int], rhs: Expr[Int]) { A = Int }
-//│ ╔══[ERROR] Unsupported constructor in this position.
-//│ ║  l.16: 	    Lit(n: Int) { A = Int }
-//│ ║        	    ^^^^^^^^^^^^^^^^^^^^^^^
-//│ ║  l.17: 	    Add(lhs: Expr[Int], rhs: Expr[Int]) { A = Int }
-//│ ╙──      	^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+//│ ═══[ERROR] Expected a valid class definition head; found ‹erroneous syntax› instead
+//│ ═══[ERROR] Expected a valid class definition head; found ‹erroneous syntax› instead
 
 
 // * one can also go the TypeScript way
@@ -36,7 +33,7 @@ enum Expr =
   | Lit(n: Int)
   | Add(lhs: Expr, rhs: Expr)
 //│ ╔══[ERROR] Unrecognized definitional assignment left-hand side: juxtaposition
-//│ ║  l.35: 	enum Expr =
+//│ ║  l.32: 	enum Expr =
 //│ ╙──      	^^^^^^^^^