From da512a7961093309c7dcd9b8003ab94923b0b21f Mon Sep 17 00:00:00 2001 From: Harry Li Date: Sat, 4 Jan 2025 03:08:09 +0800 Subject: [PATCH] Introduce light elaboration for imported defs --- .../src/test/scala/hkmc2/MLsDiffMaker.scala | 8 +- .../src/main/scala/hkmc2/MLsCompiler.scala | 3 +- .../scala/hkmc2/semantics/Elaborator.scala | 16 +++- .../main/scala/hkmc2/semantics/Importer.scala | 12 +-- .../src/main/scala/hkmc2/semantics/Term.scala | 1 + .../mlscript/ucs/examples/EitherOrBoth.mls | 15 ++++ .../ucs/normalization/OverlapOfPrimitives.mls | 25 ++++++ .../test/mlscript/ucs/patterns/Refinement.mls | 82 +++++++++++++++---- 8 files changed, 133 insertions(+), 29 deletions(-) diff --git a/hkmc2/jvm/src/test/scala/hkmc2/MLsDiffMaker.scala b/hkmc2/jvm/src/test/scala/hkmc2/MLsDiffMaker.scala index 541c02870..a295a01de 100644 --- a/hkmc2/jvm/src/test/scala/hkmc2/MLsDiffMaker.scala +++ b/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 diff --git a/hkmc2/shared/src/main/scala/hkmc2/MLsCompiler.scala b/hkmc2/shared/src/main/scala/hkmc2/MLsCompiler.scala index 5e07decb6..8a5cc709f 100644 --- a/hkmc2/shared/src/main/scala/hkmc2/MLsCompiler.scala +++ b/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() diff --git a/hkmc2/shared/src/main/scala/hkmc2/semantics/Elaborator.scala b/hkmc2/shared/src/main/scala/hkmc2/semantics/Elaborator.scala index 3fcb2b072..8e86f5c86 100644 --- a/hkmc2/shared/src/main/scala/hkmc2/semantics/Elaborator.scala +++ b/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) diff --git a/hkmc2/shared/src/main/scala/hkmc2/semantics/Importer.scala b/hkmc2/shared/src/main/scala/hkmc2/semantics/Importer.scala index a4ea11b1c..316a9755a 100644 --- a/hkmc2/shared/src/main/scala/hkmc2/semantics/Importer.scala +++ b/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 diff --git a/hkmc2/shared/src/main/scala/hkmc2/semantics/Term.scala b/hkmc2/shared/src/main/scala/hkmc2/semantics/Term.scala index 24c7a5b16..669e60154 100644 --- a/hkmc2/shared/src/main/scala/hkmc2/semantics/Term.scala +++ b/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) diff --git a/hkmc2/shared/src/test/mlscript/ucs/examples/EitherOrBoth.mls b/hkmc2/shared/src/test/mlscript/ucs/examples/EitherOrBoth.mls index 9f9619e5c..ecdc48f38 100644 --- a/hkmc2/shared/src/test/mlscript/ucs/examples/EitherOrBoth.mls +++ b/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 diff --git a/hkmc2/shared/src/test/mlscript/ucs/normalization/OverlapOfPrimitives.mls b/hkmc2/shared/src/test/mlscript/ucs/normalization/OverlapOfPrimitives.mls index 7836d7f0d..1fd03c8d9 100644 --- a/hkmc2/shared/src/test/mlscript/ucs/normalization/OverlapOfPrimitives.mls +++ b/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:&�(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" diff --git a/hkmc2/shared/src/test/mlscript/ucs/patterns/Refinement.mls b/hkmc2/shared/src/test/mlscript/ucs/patterns/Refinement.mls index 7d8c19c56..7a7c0bd49 100644 --- a/hkmc2/shared/src/test/mlscript/ucs/patterns/Refinement.mls +++ b/hkmc2/shared/src/test/mlscript/ucs/patterns/Refinement.mls @@ -1,7 +1,61 @@ :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:&�(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:&(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 @@ -9,10 +63,10 @@ open Option 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