Introduce light elaboration for imported defs

hkmc2/jvm/src/test/scala/hkmc2/MLsDiffMaker.scala

@@ -81,9 +81,13 @@ 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)
     curCtx = curCtx.nest(N)
+    prelude = curCtx
     super.run()
 
 
@@ -182,7 +186,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

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

@@ -66,8 +66,9 @@ class MLsCompiler(preludeFile: os.Path):
     val (pblk, newCtx) = elab.importFrom(preludeParse.resultBlk)(using initState)
 
     newCtx.nest(N).givenIn:
+      val elab = Elaborator(etl, wd, newCtx)
 
-      val (blk, newCtx) = elab.importFrom(mainParse.resultBlk)
+      val (blk, _) = elab.importFrom(mainParse.resultBlk)
       val low = ltl.givenIn:
         codegen.Lowering()
       val jsb = codegen.js.JSBuilder()

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 = Mode.Full):
 
     def +(local: Str -> Symbol): Ctx = copy(outer, env = env + local.mapSecond(Ctx.RefElem(_)))
     def ++(locals: IterableOnce[Str -> Symbol]): Ctx =
@@ -118,6 +119,10 @@ object Elaborator:
       def symbol: Opt[Symbol] = base.symbol
     given Conversion[Symbol, Elem] = RefElem(_)
     val empty: Ctx = Ctx(N, N, Map.empty)
+
+  enum Mode:
+    case Full
+    case Light
 
   type Ctxl[A] = Ctx ?=> A
 
@@ -147,7 +152,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 = Ctx.empty)
 (using val raise: Raise, val state: State)
 extends Importer:
   import tl.*
@@ -801,7 +806,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 real_pss =
                 // * Local functions (i.e. those without owner) with no parameter lists
@@ -1046,6 +1053,9 @@ extends Importer:
     // TODO handle name clashes
     (res, newCtx)
 
+  def importPreludeFrom(sts: Tree.Block)(using Ctx): Ctx =
+    val (_, newCtx) = importFrom(sts)
+    newCtx
 
   def topLevel(sts: Tree.Block)(using c: Ctx): (Term.Blk, Ctx) =
     val (res, ctx) = block(sts)

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 = self.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

@@ -10,6 +10,7 @@ final case class QuantVar(sym: VarSymbol, ub: Opt[Term], lb: Opt[Term])
 
 enum Term extends Statement:
   case Error
+  case Missing
   case Lit(lit: Literal)
   case Builtin(id: Tree.Ident, nme: Str)
   case Ref(sym: Symbol)(val tree: Tree.Ident, val refNum: Int)

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

hkmc2/shared/src/test/mlscript/ucs/normalization/OverlapOfPrimitives.mls

@@ -1,5 +1,30 @@
 :ucs desugared
 
+//│ Desugared:
+//│ >  if
+//│ >    let $scrut = builtin:>#1(functionName#666.length, 0)
+//│ >    $scrut is true then builtin:+#1(builtin:+#2(" '", functionName#666), "'")
+//│ >    else ""
+//│ Desugared:
+//│ >  if
+//│ >    let $scrut = builtin:||#0(builtin:<#0(got#666, expected#666), builtin:&&#0(isUB#666, builtin:>#0(got#666, expected#666)))
+//│ >    $scrut is true then { let name; name = if { let $scrut = builtin:>#1(functionName#666.length, 0); scrut is true -> { else builtin:+#1(builtin:+#2(" '", functionName#666), "'") }; else "" }; throw globalThis:globalThis#666.Error(builtin:+#3(builtin:+#4(builtin:+#5(builtin:+#6(builtin:+#7("Function", name#666), " expected "), expected#666), " arguments but got "), got#666)) }
+//│ >    else null
+//│ Desugared:
+//│ >  if
+//│ >    let $scrut = module:TraceLogger#666(.)enabled‹member:enabled›
+//│ >    $scrut is true then { let prev; prev = module:TraceLogger#666(.)indentLvl‹member:indentLvl›; module:TraceLogger#666(.)indentLvl‹member:indentLvl› := builtin:+#8(prev#666, 1); prev#666 }
+//│ >    else null
+//│ Desugared:
+//│ >  if
+//│ >    let $scrut = module:TraceLogger#666(.)enabled‹member:enabled›
+//│ >    $scrut is true then module:TraceLogger#666(.)indentLvl‹member:indentLvl› := n#666
+//│ >    else null
+//│ Desugared:
+//│ >  if
+//│ >    let $scrut = module:TraceLogger#666(.)enabled‹member:enabled›
+//│ >    $scrut is true then globalThis:import#Prelude#666(.)console‹member:console›.log(builtin:+#9("| ".repeat(module:TraceLogger#666(.)indentLvl‹member:indentLvl›), msg#666.replaceAll("\n", builtin:+#10("\n", "  ".repeat(module:TraceLogger#666(.)indentLvl‹member:indentLvl›)))))
+//│ >    else null
 fun test(x, p) = if x is
   Int and p(x) then "foo"
   0 then "bar"

hkmc2/shared/src/test/mlscript/ucs/patterns/Refinement.mls

@@ -1,18 +1,72 @@
 :todo
 :ucs normalized
 
+//│ Normalized:
+//│ >  if
+//│ >    let $scrut = builtin:>#1(functionName#666.length, 0)
+//│ >    $scrut is true then builtin:+#1(builtin:+#2(" '", functionName#666), "'")
+//│ >    else ""
+//│ Normalized:
+//│ >  if
+//│ >    let $scrut = builtin:||#0(builtin:<#0(got#666, expected#666), builtin:&&#0(isUB#666, builtin:>#0(got#666, expected#666)))
+//│ >    $scrut is true then { let name; name = if { let $scrut = builtin:>#1(functionName#666.length, 0); scrut is true -> { else builtin:+#1(builtin:+#2(" '", functionName#666), "'") }; else "" }; throw globalThis:globalThis#666.Error(builtin:+#3(builtin:+#4(builtin:+#5(builtin:+#6(builtin:+#7("Function", name#666), " expected "), expected#666), " arguments but got "), got#666)) }
+//│ >    else null
+//│ Normalized:
+//│ >  if
+//│ >    let $scrut = module:TraceLogger#666(.)enabled‹member:enabled›
+//│ >    $scrut is true then { let prev; prev = module:TraceLogger#666(.)indentLvl‹member:indentLvl›; module:TraceLogger#666(.)indentLvl‹member:indentLvl› := builtin:+#8(prev#666, 1); prev#666 }
+//│ >    else null
+//│ Normalized:
+//│ >  if
+//│ >    let $scrut = module:TraceLogger#666(.)enabled‹member:enabled›
+//│ >    $scrut is true then module:TraceLogger#666(.)indentLvl‹member:indentLvl› := n#666
+//│ >    else null
+//│ Normalized:
+//│ >  if
+//│ >    let $scrut = module:TraceLogger#666(.)enabled‹member:enabled›
+//│ >    $scrut is true then globalThis:import#Prelude#666(.)console‹member:console›.log(builtin:+#9("| ".repeat(module:TraceLogger#666(.)indentLvl‹member:indentLvl›), msg#666.replaceAll("\n", builtin:+#10("\n", "  ".repeat(module:TraceLogger#666(.)indentLvl‹member:indentLvl›)))))
+//│ >    else null
 import "../../../mlscript-compile/Option.mls"
+//│ Normalized:
+//│ >  if
+//│ >    let $scrut = builtin:>#3(functionName#666.length, 0)
+//│ >    $scrut is true then builtin:+#12(builtin:+#13(" '", functionName#666), "'")
+//│ >    else ""
+//│ Normalized:
+//│ >  if
+//│ >    let $scrut = builtin:||#1(builtin:<#1(got#666, expected#666), builtin:&&#1(isUB#666, builtin:>#2(got#666, expected#666)))
+//│ >    $scrut is true then { let name; name = if { let $scrut = builtin:>#3(functionName#666.length, 0); scrut is true -> { else builtin:+#12(builtin:+#13(" '", functionName#666), "'") }; else "" }; throw globalThis:globalThis#666.Error(builtin:+#14(builtin:+#15(builtin:+#16(builtin:+#17(builtin:+#18("Function", name#666), " expected "), expected#666), " arguments but got "), got#666)) }
+//│ >    else null
+//│ Normalized:
+//│ >  if
+//│ >    let $scrut = module:TraceLogger#666(.)enabled‹member:enabled›
+//│ >    $scrut is true then { let prev; prev = module:TraceLogger#666(.)indentLvl‹member:indentLvl›; module:TraceLogger#666(.)indentLvl‹member:indentLvl› := builtin:+#19(prev#666, 1); prev#666 }
+//│ >    else null
+//│ Normalized:
+//│ >  if
+//│ >    let $scrut = module:TraceLogger#666(.)enabled‹member:enabled›
+//│ >    $scrut is true then module:TraceLogger#666(.)indentLvl‹member:indentLvl› := n#666
+//│ >    else null
+//│ Normalized:
+//│ >  if
+//│ >    let $scrut = module:TraceLogger#666(.)enabled‹member:enabled›
+//│ >    $scrut is true then globalThis:import#Prelude#666(.)console‹member:console›.log(builtin:+#20("| ".repeat(module:TraceLogger#666(.)indentLvl‹member:indentLvl›), msg#666.replaceAll("\n", builtin:+#21("\n", "  ".repeat(module:TraceLogger#666(.)indentLvl‹member:indentLvl›)))))
+//│ >    else null
+//│ Normalized:
+//│ >  if
+//│ >    x is Some then true
+//│ >    x is None then false
 
 open Option
 
 // OK
 x => if x is
   refined(None) then x
 //│ ╔══[ERROR] Name not found: refined
-//│ ║  l.10: 	  refined(None) then x
+//│ ║  l.64: 	  refined(None) then x
 //│ ╙──      	  ^^^^^^^
 //│ ╔══[ERROR] Cannot use this identifier as an extractor
-//│ ║  l.10: 	  refined(None) then x
+//│ ║  l.64: 	  refined(None) then x
 //│ ╙──      	  ^^^^^^^
 //│ Normalized:
 //│ >  if
@@ -21,10 +75,10 @@ x => if x is
 x => if x is
   refined(Some) then x
 //│ ╔══[ERROR] Name not found: refined
-//│ ║  l.22: 	  refined(Some) then x
+//│ ║  l.76: 	  refined(Some) then x
 //│ ╙──      	  ^^^^^^^
 //│ ╔══[ERROR] Cannot use this identifier as an extractor
-//│ ║  l.22: 	  refined(Some) then x
+//│ ║  l.76: 	  refined(Some) then x
 //│ ╙──      	  ^^^^^^^
 //│ Normalized:
 //│ >  if
@@ -34,10 +88,10 @@ x => if x is
   refined(None) then x
   Some then x
 //│ ╔══[ERROR] Name not found: refined
-//│ ║  l.34: 	  refined(None) then x
+//│ ║  l.88: 	  refined(None) then x
 //│ ╙──      	  ^^^^^^^
 //│ ╔══[ERROR] Cannot use this identifier as an extractor
-//│ ║  l.34: 	  refined(None) then x
+//│ ║  l.88: 	  refined(None) then x
 //│ ╙──      	  ^^^^^^^
 //│ Normalized:
 //│ >  if x is Some then x#666
@@ -46,16 +100,16 @@ x => if x is
   refined(None) then x
   refined(Some) then x
 //│ ╔══[ERROR] Name not found: refined
-//│ ║  l.47: 	  refined(Some) then x
-//│ ╙──      	  ^^^^^^^
+//│ ║  l.101: 	  refined(Some) then x
+//│ ╙──       	  ^^^^^^^
 //│ ╔══[ERROR] Cannot use this identifier as an extractor
-//│ ║  l.47: 	  refined(Some) then x
-//│ ╙──      	  ^^^^^^^
+//│ ║  l.101: 	  refined(Some) then x
+//│ ╙──       	  ^^^^^^^
 //│ ╔══[ERROR] Name not found: refined
-//│ ║  l.46: 	  refined(None) then x
-//│ ╙──      	  ^^^^^^^
+//│ ║  l.100: 	  refined(None) then x
+//│ ╙──       	  ^^^^^^^
 //│ ╔══[ERROR] Cannot use this identifier as an extractor
-//│ ║  l.46: 	  refined(None) then x
-//│ ╙──      	  ^^^^^^^
+//│ ║  l.100: 	  refined(None) then x
+//│ ╙──       	  ^^^^^^^
 //│ Normalized:
 //│ >  if