Further elaboration for module method applications

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

@@ -182,6 +182,9 @@ extends Importer:
 
   def term(tree: Tree, inAppPrefix: Bool = false): Ctxl[Term] =
   trace[Term](s"Elab term ${tree.showDbg}", r => s"~> $r"):
+    def maybeModuleMethodApp(t: Term): Ctxl[Term] =
+      if !inAppPrefix then moduleMethodApp(t)
+      else t
     tree.desugared match
     case Bra(k, e) =>
       k match
@@ -376,15 +379,15 @@ extends Importer:
                 msg"Only module parameters may receive module arguments (values)." -> 
                 arg.toLoc :: Nil
 
-      Term.App(lt, rt)(tree, sym)
+      maybeModuleMethodApp(Term.App(lt, rt)(tree, sym))
     case SynthSel(pre, nme) =>
       val preTrm = term(pre)
       val sym = resolveField(nme, preTrm.symbol, nme)
-      Term.SynthSel(preTrm, nme)(sym)
+      maybeModuleMethodApp(Term.SynthSel(preTrm, nme)(sym))
     case Sel(pre, nme) =>
       val preTrm = term(pre)
       val sym = resolveField(nme, preTrm.symbol, nme)
-      Term.Sel(preTrm, nme)(sym)
+      maybeModuleMethodApp(Term.Sel(preTrm, nme)(sym))
     case MemberProj(ct, nme) =>
       val c = cls(ct, inAppPrefix = false)
       val f = c.symbol.flatMap(_.asCls) match
@@ -520,6 +523,51 @@ extends Importer:
     // case _ =>
     //   ???
 
+  /** Module method applications that require further elaboration with type information. */
+  def moduleMethodApp(t: Term): Ctxl[Term] =
+  trace[Term](s"Elab module method ${t.showDbg}", r => s"~> $r"):
+    /** Returns the module method definition of the innermost Sel wrapped by some App and TyApp. */
+    def defn(t: Term, argLists: Ls[Term]): (Opt[Definition], Term, Ls[Term]) = t match
+      case Term.App(f, r) => defn(f, r :: argLists)
+      case Term.TyApp(f, _) => defn(f, argLists)
+      case Term.SynthSel(pre, nme) if ModuleChecker.evalsToModule(pre) =>
+        (t.symbol.flatMap(_.asBlkMember).flatMap(_.defn), t, argLists)
+      case Term.Sel(pre, nme) if ModuleChecker.evalsToModule(pre) =>
+        (t.symbol.flatMap(_.asBlkMember).flatMap(_.defn), t, argLists)
+      case _ => (N, t, argLists)
+    defn(t, Nil) match
+      case (S(defn: TermDefinition), inner, argLists) =>
+        log(s"Elab module method definition w/ type information ${defn}.")
+        val emptyTreeApp = new Tree.App(Tree.Empty(), Tree.Empty())
+        /**
+         * Zips a module method application term along with its parameter lists,
+         * inserting any missing contextual argument lists.
+         * 
+         * M.foo -> M.foo(<using> ...)
+         * M.foo(a, b) -> M.foo(<using> ...)(a, b)(<using> ...)
+         * 
+         * Note: This *doesn't* handle explicit contextual arguments.
+         */
+        def zip(t: Term, paramLists: Ls[ParamList]): Term = (t, paramLists) match
+            case (_, params :: pRest) if params.flags.ctx =>
+              log(s"Insert a missing contextual argument list for ${params}")
+              val args = Term.Tup(params.params.map(CtxArgImpl(_)))(Tree.Tup(Nil))
+              Term.App(zip(t, pRest), args)(emptyTreeApp, FlowSymbol("‹app-res›"))
+            case (t @ Term.App(lhs, rhs), params :: pRest) =>
+              // Match the outermost App with the next non-contextual parameter list.
+              Term.App(zip(lhs, pRest), rhs)(t.tree, t.resSym)
+            case (t, params :: pRest) =>
+              // LHS is not a app but it still expects more param lists - a partial application.
+              // Just suppose it is legal and don't fail here. 
+              // TODO: Check in the implicit resolver.
+              t
+            case (_, Nil) => t
+        val newTerm = zip(t, defn.params.reverse)
+        log(s"Zip module method application: ${newTerm}")
+        newTerm
+      case _ => 
+        t
+
   def fld(tree: Tree): Ctxl[Elem] = tree match
     case InfixApp(lhs, Keyword.`:`, rhs) =>
       Fld(FldFlags.empty, term(lhs), S(term(rhs)))

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

@@ -0,0 +1,7 @@
+package hkmc2.semantics
+
+import mlscript.utils.*, shorthands.*
+
+class CtxArgImpl(val param: Param) extends CtxArg:
+  override def term: Opt[Term] = N
+

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

@@ -47,6 +47,10 @@ abstract class Symbol(using State) extends Located:
     (asCls: Opt[ClassSymbol | ModuleSymbol | PatternSymbol]) orElse asMod orElse asPat
   def asTpe: Opt[TypeSymbol] = asCls orElse asAls
 
+  def asBlkMember: Opt[BlockMemberSymbol] = this match
+    case mem: BlockMemberSymbol => S(mem)
+    case _ => N
+
   override def equals(x: Any): Bool = x match
     case that: Symbol => uid === that.uid
     case _ => false

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

@@ -366,6 +366,15 @@ object PlainFld:
 final case class Spd(eager: Bool, term: Term) extends Elem:
   def showDbg: Str = (if eager then "..." else "..") + term.showDbg
 
+/** 
+ * Context arguments. 
+ * 
+ * Placeholders represents a nil term by default; 
+ * to be populated (resolved) by the implicit resolver later to represent some concrete term.
+ */
+abstract class CtxArg extends Elem:
+  def term: Opt[Term]
+  def showDbg: Str = s"‹using› ${term.fold("‹unpopulated›")(_.showDbg)}"
 
 final case class TyParam(flags: FldFlags, vce: Opt[Bool], sym: VarSymbol) extends Declaration: