Introduce light elaboration for imported defs

hkmc2/shared/src/main/scala/hkmc2/MLsCompiler.scala

@@ -7,6 +7,7 @@ import utils.*
 
 import hkmc2.semantics.MemberSymbol
 import hkmc2.semantics.Elaborator
+import semantics.Elaborator.Ctx
 import hkmc2.syntax.Keyword.`override`
 import semantics.Elaborator.State
 
@@ -65,16 +66,16 @@ class MLsCompiler(preludeFile: os.Path):
     val preludeParse = ParserSetup(preludeFile, dbgParsing)
     val mainParse = ParserSetup(file, dbgParsing)
 
-    val elab = Elaborator(etl, wd)
+    val elab = Elaborator(etl, wd, Ctx.empty)
 
     val initState = State.init.nest(N)
 
     val (pblk, newCtx) = elab.importFrom(preludeParse.resultBlk)(using initState)
 
     newCtx.nest(N).givenIn:
-
+      val elab = Elaborator(etl, wd, newCtx)
       val parsed = mainParse.resultBlk
-      val (blk0, newCtx) = elab.importFrom(parsed)
+      val (blk0, _) = elab.importFrom(parsed)
       val blk = blk0.copy(stats = semantics.Import(State.runtimeSymbol, runtimeFile.toString) :: blk0.stats)
       val low = ltl.givenIn:
         codegen.Lowering(lowerHandlers = false, stackLimit = None) // TODO: properly hook up stack limit

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

@@ -38,7 +38,8 @@ object Elaborator:
 
   val reservedNames = binaryOps.toSet ++ aliasOps.keySet + "NaN" + "Infinity"
 
-  case class Ctx(outer: Opt[InnerSymbol], parent: Opt[Ctx], env: Map[Str, Ctx.Elem]):
+  case class Ctx(outer: Opt[InnerSymbol], parent: Opt[Ctx], env: Map[Str, Ctx.Elem], 
+    mode: Mode):
 
     def +(local: Str -> Symbol): Ctx = copy(outer, env = env + local.mapSecond(Ctx.RefElem(_)))
     def ++(locals: IterableOnce[Str -> Symbol]): Ctx =
@@ -55,7 +56,7 @@ object Elaborator:
           nme -> elem
       )
 
-    def nest(outer: Opt[InnerSymbol]): Ctx = Ctx(outer, Some(this), Map.empty)
+    def nest(outer: Opt[InnerSymbol]): Ctx = Ctx(outer, Some(this), Map.empty, mode)
 
     def get(name: Str): Opt[Ctx.Elem] =
       env.get(name).orElse(parent.flatMap(_.get(name)))
@@ -125,7 +126,11 @@ object Elaborator:
           new Tree.Ident(nme).withLocOf(id))(symOpt)
       def symbol = symOpt
     given Conversion[Symbol, Elem] = RefElem(_)
-    val empty: Ctx = Ctx(N, N, Map.empty)
+    val empty: Ctx = Ctx(N, N, Map.empty, Mode.Full)
+
+  enum Mode:
+    case Full
+    case Light
 
   type Ctxl[A] = Ctx ?=> A
 
@@ -162,7 +167,7 @@ end Elaborator
 import Elaborator.*
 
 
-class Elaborator(val tl: TraceLogger, val wd: os.Path)
+class Elaborator(val tl: TraceLogger, val wd: os.Path, val prelude: Ctx)
 (using val raise: Raise, val state: State)
 extends Importer:
   import tl.*
@@ -885,7 +890,9 @@ extends Importer:
               // * Elaborate signature
               val st = td.annotatedResultType.orElse(newSignatureTrees.get(id.name))
               val s = st.map(term(_)(using newCtx))
-              val b = rhs.map(term(_)(using newCtx))
+              val b = if ctx.mode != Mode.Light
+                then rhs.map(term(_)(using newCtx))
+                else S(Term.Missing)
               val r = FlowSymbol(s"‹result of ${sym}›")
               val tdf = TermDefinition(owner, k, sym, pss, tps, s, b, r, 
                 TermDefFlags.empty.copy(isModMember = isModMember), annotations)
@@ -1134,7 +1141,6 @@ extends Importer:
     // TODO handle name clashes
     (res, newCtx)
 
-
   def topLevel(sts: Tree.Block)(using c: Ctx): (Term.Blk, Ctx) =
     val (res, ctx) = block(sts, hasResult = false)
     computeVariances(res)

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

@@ -60,15 +60,9 @@ class Importer:
           val res = p.parseAll(p.block(allowNewlines = true))
           val resBlk = new syntax.Tree.Block(res)
 
-          // * Note: we don't even need to elaborate the block!
-          // * Though doing so may be needed later for type checking,
-          // * so we should probably do it lazily in the future.
-          /* 
-          given Elaborator.State = new Elaborator.State
-          given Elaborator.Ctx = Elaborator.Ctx.init.nest(N)
-          val elab = Elaborator(tl, file / os.up)
-          val (blk, newCtx) = elab.importFrom(resBlk)
-          */
+          given Elaborator.Ctx = prelude.copy(mode = Mode.Light).nest(N)
+          val elab = Elaborator(tl, file / os.up, prelude)
+          elab.importFrom(resBlk)
 
           resBlk.definedSymbols.find(_._1 === nme) match
           case Some(nme -> sym) => sym

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

@@ -31,6 +31,7 @@ enum Annot extends AutoLocated:
 enum Term extends Statement:
   case Error
   case UnitVal()
+  case Missing // Placeholder terms that were not elaborated due to the "lightweight" elaboration mode `Mode.Light`
   case Lit(lit: Literal)
   case Builtin(id: Tree.Ident, nme: Str)
   case Ref(sym: Symbol)(val tree: Tree.Ident, val refNum: Int)
@@ -210,6 +211,7 @@ sealed trait Statement extends AutoLocated with ProductWithExtraInfo:
     case WildcardTy(in, out) => s"in ${in.map(_.toString).getOrElse("⊥")} out ${out.map(_.toString).getOrElse("⊤")}"
     case Sel(pre, nme) => s"${pre.showDbg}.${nme.name}"
     case SynthSel(pre, nme) => s"(${pre.showDbg}.)${nme.name}"
+    case DynSel(pre, fld, _) => s"${pre.showDbg}[${fld.showDbg}]"
     case IfLike(kw, body) => s"${kw.name} { ${body.showDbg} }"
     case Lam(params, body) => s"λ${params.showDbg}. ${body.showDbg}"
     case Blk(stats, res) =>

hkmc2/shared/src/test/mlscript-compile/Stack.mls

@@ -6,7 +6,7 @@ open Predef
 // TODO
 // type Stack[A] = Stack.Cons[A] | Stack.Nil
 
-module Stack with ...
+module Stack[T] with ...
 
 class (::) Cons[A](head: A, tail: Stack[A])
 object Nil

hkmc2/shared/src/test/mlscript/ucs/examples/EitherOrBoth.mls

@@ -11,23 +11,38 @@ class Both[out A, out B](left: A, right: B) extends EitherOrBoth[A, B]
 
 type Either[A, B] = Left[A, B] | Right[A, B]
 
+// TODO: fix type parameters of Option. See mlscript-compile/Option.mls
+:todo
 fun getLeft[A, B](eob: EitherOrBoth[A, B]): Option[A] =
   if eob is
     Left(left) then Some(left)
     Right(_) then None
     Both(left, _) then Some(left)
+//│ ╔══[ERROR] Wrong number of type arguments
+//│ ║  l.16: 	fun getLeft[A, B](eob: EitherOrBoth[A, B]): Option[A] =
+//│ ╙──      	                                            ^^^^^^^^
 
+// TODO: fix type parameters of Option. See mlscript-compile/Option.mls
+:todo
 fun getRight[A, B](eob: EitherOrBoth[A, B]): Option[B] =
   if eob is
     Left(_) then None
     Right(right) then Some(right)
     Both(_, right) then Some(right)
+//│ ╔══[ERROR] Wrong number of type arguments
+//│ ║  l.27: 	fun getRight[A, B](eob: EitherOrBoth[A, B]): Option[B] =
+//│ ╙──      	                                             ^^^^^^^^
 
+// TODO: fix type parameters of Option. See mlscript-compile/Option.mls
+:todo
 fun getBoth[A, B](eob: EitherOrBoth[A, B]): Option[[A, B]] =
   if eob is
     Left(_) then None
     Right(_) then None
     Both(left, right) then Some([left, right])
+//│ ╔══[ERROR] Wrong number of type arguments
+//│ ║  l.38: 	fun getBoth[A, B](eob: EitherOrBoth[A, B]): Option[[A, B]] =
+//│ ╙──      	                                            ^^^^^^^^^^^^^
 
 fun mapLeft[A, B, C](eob: EitherOrBoth[A, B], f: A -> C): EitherOrBoth[C, B] =
   if eob is

hkmc2DiffTests/src/test/scala/hkmc2/MLsDiffMaker.scala

@@ -8,6 +8,7 @@ import utils.*
 import hkmc2.semantics.Elaborator
 import hkmc2.semantics.ImplicitResolver
 
+import semantics.Elaborator.Ctx
 
 abstract class MLsDiffMaker extends DiffMaker:
 
@@ -82,8 +83,12 @@ abstract class MLsDiffMaker extends DiffMaker:
   var curCtx = Elaborator.State.init
   var curICtx = ImplicitResolver.ICtx.empty
 
+  var prelude = Elaborator.Ctx.empty
+
   override def run(): Unit =
-    if file =/= preludeFile then importFile(preludeFile, verbose = false)
+    if file =/= preludeFile then 
+      importFile(preludeFile, verbose = false)
+      prelude = curCtx
     curCtx = curCtx.nest(N)
     super.run()
 
@@ -95,10 +100,11 @@ abstract class MLsDiffMaker extends DiffMaker:
     given raise: Raise = d =>
       output(s"Error: $d")
       ()
-    processTrees(
-      Modified(`import`, N, StrLit(predefFile.toString))
-      :: Open(Ident("Predef"))
-      :: Nil)
+    if file != preludeFile then
+      processTrees(
+        Modified(`import`, N, StrLit(predefFile.toString))
+        :: Open(Ident("Predef"))
+        :: Nil)
     super.init()
 
 
@@ -126,7 +132,7 @@ abstract class MLsDiffMaker extends DiffMaker:
     val imprtSymbol =
       semantics.TopLevelSymbol("import#"+file.baseName)
     given Elaborator.Ctx = curCtx.nest(N)
-    val elab = Elaborator(etl, wd)
+    val elab = Elaborator(etl, wd, Ctx.empty)
     try
       val resBlk = new syntax.Tree.Block(res)
       val (e, newCtx) = elab.importFrom(resBlk)
@@ -182,7 +188,7 @@ abstract class MLsDiffMaker extends DiffMaker:
   private var blockNum = 0
 
   def processTrees(trees: Ls[syntax.Tree])(using Raise): Unit =
-    val elab = Elaborator(etl, file / os.up)
+    val elab = Elaborator(etl, file / os.up, prelude)
     // val blockSymbol =
     //   semantics.TopLevelSymbol("block#"+blockNum)
     blockNum += 1