Temporarily support ADT and ADT matching typing in InvalML

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

@@ -82,8 +82,11 @@ class BBTyper(using elState: Elaborator.State, tl: TL):
   // A temporary solution for ADT matching exhausive checking
   // `adtCtors` maps IDs of ADTs to their constructors' IDs
   // `adtParent` maps constructors' IDs to the ADT class symbol they belong to
+  // `typeNames` maintains all type names 
+  // since we need to reject all non-variable patterns in ADT match for now
   private val adtCtors = HashMap.empty[Uid[Symbol], ListBuffer[Uid[Symbol]]]
   private val adtParent = HashMap.empty[Uid[Symbol], Symbol]
+  private val typeNames = HashSet.empty[Str]
 
   private def freshSkolem(sym: Symbol, hint: Str = "")(using ctx: BbCtx): InfVar =
     InfVar(ctx.lvl, infVarState.nextUid, new VarState(), true)(sym, hint)
@@ -115,6 +118,8 @@ class BBTyper(using elState: Elaborator.State, tl: TL):
       adtCtors += pSym.uid -> ListBuffer(cSym.uid)
     else adtCtors(pSym.uid) += cSym.uid
     adtParent += cSym.uid -> pSym
+    typeNames.add(pSym.nme)
+    typeNames.add(cSym.nme)
 
   private def typeAndSubstType
       (ty: Term, pol: Bool)(using map: Map[Uid[Symbol], TypeArg])(using ctx: BbCtx, cctx: CCtx)
@@ -336,6 +341,13 @@ class BBTyper(using elState: Elaborator.State, tl: TL):
       val map = HashMap[Uid[Symbol], TypeArg]()
       pattern match
         case Pattern.ResolvedClassOrModule(sym, paramsOpt) =>
+          paramsOpt.foreach: params =>
+            params.foreach:
+              case (_, p, _) => p match
+                case Under() => ()
+                case Ident(nme) if !typeNames(nme) => ()
+                case _ =>
+                  error(msg"Pattern ${p.toString} is not supported yet." -> split.toLoc :: Nil)
           val clsTy = adtParent.get(sym.uid).flatMap(_.asCls.flatMap(_.defn)) match
             case S(cls) =>
               ClassLikeType(cls.sym, cls.tparams.map(_ => freshWildcard(sym)))
@@ -372,7 +384,7 @@ class BBTyper(using elState: Elaborator.State, tl: TL):
             params.iterator.zip(paramList).foreach:
               case (p, Param(_, _, S(ty), _)) =>
                 nestCtx += p.scrutinee -> typeAndSubstType(ty, true)(using map.toMap)
-            val (consTy, consEff, _) = typeADTMatch(cons, sign)(using nestCtx)
+            val (consTy, consEff) = typeAllSplits(cons, sign)(using nestCtx)
             val (altsTy, altsEff, altCases) = typeADTMatch(alts, sign)
             val allEff = scrutineeEff | (consEff | altsEff)
             (sign.getOrElse(tryMkMono(consTy, cons) | tryMkMono(altsTy, alts)), allEff, sym :: altCases)
@@ -621,11 +633,13 @@ class BBTyper(using elState: Elaborator.State, tl: TL):
             ctx += td.sym -> typeType(sig)
             goStats(stats)
           case (clsDef: ClassDef) :: stats =>
+            typeNames.add(clsDef.sym.nme)
             clsDef.ext match
               case S(Term.New(ty, _, N)) => createADTCtor(clsDef, ty)
               case _ => ()
             goStats(stats)
           case (modDef: ModuleDef) :: stats =>
+            typeNames.add(modDef.sym.nme)
             goStats(stats)
           case Import(sym, pth) :: stats =>
             goStats(stats) // TODO:

hkmc2/shared/src/test/mlscript/bbml/ConSolver.mls

@@ -22,16 +22,16 @@ class Iter[T, R]
 fun
 
   // empty:   [A, R] -> Region[R] ->{R} ArrayList[out A, out R]  // TODO investigate: why does this break things?
-  empty:   [A, R] -> Region[R] ->{R} ArrayList[A, R]
+  empty:   [A, R] -> Region[R] ->{R} ArrayList[A, out R]
 
-  clear:   [A, R] -> (ArrayList[A, R]) ->{R} ()
-  push:    [A, R] -> (ArrayList[A, R], A) ->{R} ()
+  clear:   [A, R] -> (ArrayList[A, out R]) ->{R} ()
+  push:    [A, R] -> (ArrayList[A, out R], A) ->{R} ()
   foreach: [E, R, T] -> (Iter[T, R], T ->{E} ()) ->{R | E} ()
   iter: [Res, R, E extends ~R, T] ->
-    (ArrayList[T, R], [S] -> Iter[T, S] ->{S | E} Res) ->{E | R} Res
+    (ArrayList[T, out R], [S] -> Iter[T, S] ->{S | E} Res) ->{E | R} Res
 
 push
-//│ Type: ['A, 'R] -> (ArrayList['A, 'R], 'A) ->{'R} ()
+//│ Type: ['A, 'R] -> (ArrayList['A, out 'R], 'A) ->{'R} ()
 
 
 class Type[R] with
@@ -55,6 +55,24 @@ fun pp = case
 pp(ty)
 //│ Type: Str
 
+
+:e
+fun matchP = case
+  Pair(IntType, IntType) then ()
+//│ ╔══[ERROR] Pattern Ident(IntType) is not supported yet.
+//│ ║  l.61: 	  Pair(IntType, IntType) then ()
+//│ ╙──      	  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+//│ ╔══[ERROR] Pattern Ident(IntType) is not supported yet.
+//│ ║  l.61: 	  Pair(IntType, IntType) then ()
+//│ ╙──      	  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+//│ ╔══[ERROR] Expect 3 cases, but 1 got.
+//│ ║  l.61: 	  Pair(IntType, IntType) then ()
+//│ ╙──      	                ^^^^^^^^^^^^^^^^
+//│ ╔══[ERROR] Expect 3 cases, but 1 got.
+//│ ║  l.61: 	  Pair(IntType, IntType) then ()
+//│ ╙──      	       ^^^^^^^^^^^^^^^^^^^^^^^^^
+
+
 fun error() = error()
 
 fun solve = case
@@ -81,12 +99,10 @@ solve
 //│ Where:
 //│   ⊥ <: 'Fun
 //│   'Fun <: ⊤
-//│   'Fun <: ⊥
 //│   'Fun <: 'Fun
 //│   ⊥ <: 'Fun
 //│   'Fun <: ⊤
 //│   'Fun <: 'Fun
-//│   'Fun <: ⊥
 //│   'Fun <: 'Unif
 //│   'Fun <: 'Unif
 //│   'Fun <: 'eff
@@ -99,12 +115,9 @@ solve
 //│   'eff1 <: 'eff
 //│   'Unif <: 'eff
 //│   'Unif <: 'eff1
-//│   'Unif <: ⊥
-
-
-
 
 
+solve(Cons(Pair(ty, ty), Nil))
 
 
 // * Paper example
@@ -113,9 +126,7 @@ solve
 region r in
   let xs = empty(r)
   xs
-//│ Type: ArrayList['A, in 'R]
-//│ Where:
-//│   'R <: ⊥
+//│ Type: ArrayList['A, ?]
 
 region r in
   let xs = empty(r)
@@ -135,7 +146,7 @@ region r in // This is used to delimit the scope of mutation
   push(xs, "1"); push(xs, "2"); push(xs, "3")
   iter(xs, it => foreach(it, e => println(e); clear(xs)))
 //│ ╔══[ERROR] Type error in function literal with expected type (Iter['T, S]) ->{S ∨ 'E} 'Res
-//│ ║  l.136: 	  iter(xs, it => foreach(it, e => println(e); clear(xs)))
+//│ ║  l.163: 	  iter(xs, it => foreach(it, e => println(e); clear(xs)))
 //│ ║         	           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 //│ ╟── because: cannot constrain  'R ∨ 'E1  <:  S ∨ 'E
 //│ ╟── because: cannot constrain  'E1  <:  'E ∨ S
@@ -163,8 +174,6 @@ fun test(x) = case
 
 test
 //│ Type: ['Unif] -> ⊤ -> (((Type[out 'Unif] ∧ Type[?]) ∧ Type[?]) ->{'Unif} ())
-//│ Where:
-//│   'Unif <: ⊥
 
 
 
@@ -190,22 +199,21 @@ fun solve = case
           // Handle unification case here
           error() // Placeholder for unification logic
 //│ ╔══[ERROR] Expect 3 cases, but 1 got.
-//│ ║  l.182: 	          IntType then ()
+//│ ║  l.207: 	          IntType then ()
 //│ ║         	          ^^^^^^^^^^^^^^^
-//│ ║  l.183: 	          else error()
+//│ ║  l.208: 	          else error()
 //│ ╙──       	^^^^^^^^^^^^^^^^^^^^^^
 //│ ╔══[ERROR] Expect 3 cases, but 1 got.
-//│ ║  l.185: 	          Fun(l2, r2) then
+//│ ║  l.210: 	          Fun(l2, r2) then
 //│ ║         	          ^^^^^^^^^^^^^^^^
-//│ ║  l.186: 	            solve(Cons(Pair(l2, l1), cs))
+//│ ║  l.211: 	            solve(Cons(Pair(l2, l1), cs))
 //│ ║         	^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-//│ ║  l.187: 	            solve(Cons(Pair(r1, r2), cs))
+//│ ║  l.212: 	            solve(Cons(Pair(r1, r2), cs))
 //│ ║         	^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-//│ ║  l.188: 	          else error()
+//│ ║  l.213: 	          else error()
 //│ ╙──       	^^^^^^^^^^^^^^^^^^^^^^
 
-// Q: why is it not complaining, here?
-// :fixme
+:fixme
 fun solve = case
   Nil then ()
   Cons(c, cs) and c is
@@ -221,6 +229,22 @@ fun solve = case
       Unif(id, lbs, ubs) then
         // Handle unification case here
         error() // Placeholder for unification logic
+//│ ╔══[ERROR] Expect 3 cases, but 1 got.
+//│ ║  l.238: 	        IntType then ()
+//│ ║         	        ^^^^^^^^^^^^^^^
+//│ ║  l.239: 	        else error()
+//│ ╙──       	^^^^^^^^^^^^^^^^^^^^
+//│ ╔══[ERROR] Expect 3 cases, but 1 got.
+//│ ║  l.240: 	      Fun(l1, r1) and rhs is
+//│ ║         	          ^^^^^^^^^^^^^^^^^^
+//│ ║  l.241: 	        Fun(l2, r2) then
+//│ ║         	^^^^^^^^^^^^^^^^^^^^^^^^
+//│ ║  l.242: 	          solve(Cons(Pair(l2, l1), cs))
+//│ ║         	^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+//│ ║  l.243: 	          solve(Cons(Pair(r1, r2), cs))
+//│ ║         	^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+//│ ║  l.244: 	        else error()
+//│ ╙──       	^^^^^^^^^^^^^^^^^^^^
 
 solve
 //│ Type: (Stack[out PairOf[out Type[?], out Type[?]]] ∧ Stack[?]) -> ()