Reimplement operator apps, operator splits, and "placeholder syntax" for lambdas (#302)

Co-authored-by: Luyu Cheng <[email protected]>

Author: LPTK

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

@@ -339,7 +339,7 @@ class BBTyper(using elState: Elaborator.State, tl: TL):
     (lhs, rhs) match
     case (Term.Lam(PlainParamList(params), body), ft @ PolyFunType(args, ret, eff)) => // * annoted functions
       if params.length != args.length then
-         (error(msg"Cannot type function ${lhs.toString} as ${rhs.show}" -> lhs.toLoc :: Nil), Bot)
+        (error(msg"Cannot type function ${lhs.toString} as ${rhs.show}" -> lhs.toLoc :: Nil), Bot)
       else
         val nestCtx = ctx.nest
         val argsTy = params.zip(args).map:

hkmc2/shared/src/main/scala/hkmc2/codegen/Printer.scala

@@ -19,7 +19,9 @@ object Printer:
       // ts.trmTree
     case ts: semantics.InnerSymbol => ts.nme
     case ts: semantics.BuiltinSymbol => ts.nme
-    case _ => summon[Scope].lookup_!(l)
+    case _ => summon[Scope].lookup(l) match
+      case S(str) => str
+      case N => s"‹not in scope: ${l}›"
 
   def mkDocument(blk: Block)(using Raise, Scope): Document = blk match
     case Match(scrut, arms, dflt, rest) =>
@@ -95,6 +97,10 @@ object Printer:
     case Value.Arr(elems) =>
       val docElems = elems.map(x => mkDocument(x)).mkString(", ")
       doc"[${docElems}]"
+    case Value.Rcd(args) =>
+      doc"{ ${
+        args.map(x => x.idx.fold(doc"...")(p => mkDocument(p) :: ": ") :: mkDocument(x.value)).mkString(", ")
+      } }"
 
   def mkDocument(path: Path)(using Raise, Scope): Document = path match
     case Select(qual, name) =>

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

@@ -252,12 +252,18 @@ sealed trait Statement extends AutoLocated with ProductWithExtraInfo:
     case Neg(e) => e :: Nil
     case Annotated(ann, target) => ann.subTerms ::: target :: Nil
 
+  // private def treeOrSubterms(t: Tree, t: Term): Ls[Located] = t match
+  private def treeOrSubterms(t: Tree): Ls[Located] = t match
+    case Tree.DummyApp | Tree.DummyTup => subTerms
+    case _ => t :: Nil
+  
   protected def children: Ls[Located] = this match
     case t: Lit => t.lit.asTree :: Nil
-    case t: Ref => t.tree :: Nil
-    case t: Tup => t.tree :: Nil
+    case t: Ref => treeOrSubterms(t.tree)
+    case t: Tup => treeOrSubterms(t.tree)
     case l: Lam => l.params.paramSyms.map(_.id) ::: l.body :: Nil
-    case t: App => t.tree :: Nil
+    case t: App => treeOrSubterms(t.tree)
+    case IfLike(kw, desug) => desug :: Nil
     case SynthSel(pre, nme) => pre :: nme :: Nil
     case Sel(pre, nme) => pre :: nme :: Nil
     case SelProj(prefix, cls, proj) => prefix :: cls :: proj :: Nil

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

@@ -21,7 +21,7 @@ object DeBrujinSplit:
     /** Resolve the constructor in the elaborator context. */
     def resolve(ctor: Ident | Sel, params: Ls[Tree]): Opt[F] =
       val term = scoped("ucs:mute"):
-        elaborator.cls(ctor, inAppPrefix = false)
+        elaborator.cls(elaborator.term(ctor), inAppPrefix = false)
       term.symbol.flatMap(_.asClsLike).map:
         case symbol: (ClassSymbol | ModuleSymbol) =>
           val pattern = ClassLike(ConstructorLike.Symbol(symbol))
@@ -70,9 +70,6 @@ object DeBrujinSplit:
       * not found.
       */
     def dealWithCtor(ctor: Ident | Sel, params: Ls[Tree]): F = ctor match
-      case Ident("~") => (scrutinee, innermost, alternative) =>
-        Branch(scrutinee, ClassLike(ConstructorLike.StringJoin), innermost.increment(2), alternative)
-        alternative
       case Ident(ctorName) => patternParams.find(_.sym.name == ctorName) match
         case S(Param(sym = symbol)) => (scrutinee, innermost, alternative) =>
           log(s"found an input pattern: ${symbol.name}")
@@ -93,6 +90,9 @@ object DeBrujinSplit:
         val buildRight = go(rhs)
         val latter = buildRight(scrutinee, consequence, alternative)
         buildLeft(scrutinee, consequence, latter)
+      case lhs ~ rhs => (scrutinee, innermost, alternative) =>
+        Branch(scrutinee, ClassLike(ConstructorLike.StringJoin), innermost.increment(2), alternative)
+        alternative
       case Under() => (_, consequence, _) => consequence
       case ctor: (Ident | Sel) => dealWithCtor(ctor, Nil)
       case App(Ident("-"), Tup(IntLit(n) :: Nil)) =>
@@ -110,6 +110,7 @@ object DeBrujinSplit:
         (_, _, alternative) => alternative
       // END TODO: Support range patterns
       case App(ctor: (Ident | Sel), Tup(params)) => dealWithCtor(ctor, params)
+      case OpApp(lhs, op: Ident, rhs :: Nil) => dealWithCtor(op, Ls(lhs, rhs))
       case literal: syntax.Literal => Branch(_, Literal(literal), _, _)
     scoped("ucs:rp:elaborate"):
       log(s"tree: ${tree.showDbg}")

hkmc2/shared/src/main/scala/hkmc2/semantics/ucs/DeBrujinSplit.scala

@@ -9,7 +9,7 @@ import utils.TraceLogger
 import syntax.Literal
 import Keyword.{as, and, `do`, `else`, is, let, `then`, where}
 import collection.mutable.{HashMap, SortedSet}
-import Elaborator.{ctx, Ctxl}
+import Elaborator.{ctx, Ctxl, UnderCtx}
 import scala.annotation.targetName
 import hkmc2.semantics.ClassDef.Parameterized
 
@@ -26,11 +26,11 @@ object Desugarer:
     val tupleLast: HashMap[Int, BlockLocalSymbol] = HashMap.empty
 end Desugarer
 
-class Desugarer(val elaborator: Elaborator)
+class Desugarer(val elaborator: Elaborator)(using UnderCtx)
     (using raise: Raise, state: Elaborator.State, c: Elaborator.Ctx) extends DesugaringBase:
   import Desugarer.*
   import Elaborator.Ctx
-  import elaborator.term, elaborator.tl.*
+  import elaborator.term, elaborator.subterm, elaborator.tl.*
 
   given Ordering[Loc] = Ordering.by: loc =>
     (loc.spanStart, loc.spanEnd)
@@ -126,7 +126,7 @@ class Desugarer(val elaborator: Elaborator)
           raise(ErrorReport(msg"only one branch is supported in shorthands" -> tree.toLoc :: Nil))
         termSplitShorthands(branch, finish)(fallback)(ctx)
     case coda is rhs => fallback => ctx =>
-      nominate(ctx, finish(term(coda)(using ctx))):
+      nominate(ctx, finish(subterm(coda)(using ctx))):
         patternSplitShorthands(rhs, _)(fallback)
     case matches => fallback =>
       // There are N > 0 conjunct matches. We use `::[T]` instead of `List[T]`.
@@ -177,6 +177,35 @@ class Desugarer(val elaborator: Elaborator)
             nominate(ctx, term(coda)(using ctx)):
               expandMatch(_, pat, sequel)(fallback)
       expandMatch(scrutSymbol, headPattern, tailSplit)(fallback)
+  
+  def termSplit(trees: Ls[Tree], finish: Term => Term): Split => Sequel =
+    trees.foldRight(default): (t, elabFallback) =>
+      t match
+      case LetLike(`let`, ident @ Ident(_), N, N) => ???
+      case LetLike(`let`, ident @ Ident(_), S(termTree), N) => fallback => ctx => trace(
+        pre = s"termSplit: let ${ident.name} = $termTree",
+        post = (res: Split) => s"termSplit: let >>> $res"
+      ):
+        val sym = VarSymbol(ident)
+        val fallbackCtx = ctx + (ident.name -> sym)
+        Split.Let(sym, term(termTree)(using ctx), elabFallback(fallback)(fallbackCtx)).withLocOf(t)
+      case Modified(Keyword.`do`, doLoc, computation) => fallback => ctx => trace(
+        pre = s"termSplit: do $computation",
+        post = (res: Split) => s"termSplit: else >>> $res"
+      ):
+        val sym = TempSymbol(N, "doTemp")
+        Split.Let(sym, term(computation)(using ctx), elabFallback(fallback)(ctx)).withLocOf(t)
+      case Modified(Keyword.`else`, elsLoc, default) => fallback => ctx => trace(
+        pre = s"termSplit: else $default",
+        post = (res: Split) => s"termSplit: else >>> $res"
+      ):
+        // TODO: report `rest` as unreachable
+        Split.default(term(default)(using ctx)).withLocOf(t)
+      case branch => fallback => ctx => trace(
+        pre = s"termSplit: $branch",
+        post = (res: Split) => s"termSplit >>> $res"
+      ):
+        termSplit(branch, finish)(elabFallback(fallback)(ctx))(ctx)
 
   /** Desugar a _term split_ (TS) into a _split_ of core abstract syntax.
    *  @param tree the tree representing the term split.
@@ -186,35 +215,9 @@ class Desugarer(val elaborator: Elaborator)
    *          matches and splits
    */
   def termSplit(tree: Tree, finish: Term => Term): Split => Sequel =
+    log(s"termSplit: $tree")
     tree match
-    case blk: Block =>
-      blk.desugStmts.foldRight(default): (t, elabFallback) =>
-        t match
-        case LetLike(`let`, ident @ Ident(_), N, N) => ???
-        case LetLike(`let`, ident @ Ident(_), S(termTree), N) => fallback => ctx => trace(
-          pre = s"termSplit: let ${ident.name} = $termTree",
-          post = (res: Split) => s"termSplit: let >>> $res"
-        ):
-          val sym = VarSymbol(ident)
-          val fallbackCtx = ctx + (ident.name -> sym)
-          Split.Let(sym, term(termTree)(using ctx), elabFallback(fallback)(fallbackCtx)).withLocOf(t)
-        case Modified(Keyword.`do`, doLoc, computation) => fallback => ctx => trace(
-          pre = s"termSplit: do $computation",
-          post = (res: Split) => s"termSplit: else >>> $res"
-        ):
-          val sym = TempSymbol(N, "doTemp")
-          Split.Let(sym, term(computation)(using ctx), elabFallback(fallback)(ctx)).withLocOf(t)
-        case Modified(Keyword.`else`, elsLoc, default) => fallback => ctx => trace(
-          pre = s"termSplit: else $default",
-          post = (res: Split) => s"termSplit: else >>> $res"
-        ):
-          // TODO: report `rest` as unreachable
-          Split.default(term(default)(using ctx)).withLocOf(t)
-        case branch => fallback => ctx => trace(
-          pre = s"termSplit: $branch",
-          post = (res: Split) => s"termSplit >>> $res"
-        ):
-          termSplit(branch, finish)(elabFallback(fallback)(ctx))(ctx).withLocOf(t)
+    case blk: Block => termSplit(blk.desugStmts, finish)
     case coda is rhs => fallback => ctx =>
       nominate(ctx, finish(term(coda)(using ctx))):
         patternSplit(rhs, _)(fallback)
@@ -246,7 +249,8 @@ class Desugarer(val elaborator: Elaborator)
         ):
           nominate(ctx, finish(term(headCoda)(using ctx))):
             expandMatch(_, headPattern, tailSplit)(fallback)
-    case tree @ App(opIdent @ Ident(opName), rawTup @ Tup(lhs :: rhs :: Nil)) => fallback => ctx => trace(
+    // Handle binary operators.
+    case tree @ OpApp(lhs, opIdent @ Ident(opName), rhss) => fallback => ctx => trace(
       pre = s"termSplit: after op <<< $opName",
       post = (res: Split) => s"termSplit: after op >>> $res"
     ):
@@ -258,22 +262,16 @@ class Desugarer(val elaborator: Elaborator)
         val finishInner = (rhsTerm: Term) =>
           val first = Fld(FldFlags.empty, lhsSymbol.ref(/* FIXME ident? */), N)
           val second = Fld(FldFlags.empty, rhsTerm, N)
-          val arguments = Term.Tup(first :: second :: Nil)(rawTup)
+          val arguments = Term.Tup(first :: second :: Nil)(Tree.DummyTup)
           val joint = FlowSymbol("‹applied-result›")
-          Term.App(opRef, arguments)(tree, N, joint)
-        termSplit(rhs, finishInner)(fallback)
-    case tree @ App(lhs, blk @ OpBlock(opRhsApps)) => fallback => ctx =>
+          Term.App(opRef, arguments)(Tree.DummyApp, N, joint)
+        termSplit(rhss, finishInner)(fallback)
+    // Handle operator splits.
+    case tree @ OpSplit(lhs, rhss) => fallback => ctx =>
       nominate(ctx, finish(term(lhs)(using ctx))): vs =>
-        val mkInnerFinish = (op: Term) => (rhsTerm: Term) =>
-          val first = Fld(FldFlags.empty, vs.ref(/* FIXME ident? */), N)
-          val second = Fld(FldFlags.empty, rhsTerm, N)
-          val rawTup = Tup(lhs :: Nil): Tup // <-- loc might be wrong
-          val arguments = Term.Tup(first :: second :: Nil)(rawTup)
-          val joint = FlowSymbol("‹applied-result›")
-          Term.App(op, arguments)(tree, N, joint)
-        opRhsApps.foldRight(Function.const(fallback): Sequel): (tt, elabFallback) =>
-          tt match
-          case (Tree.Empty(), LetLike(`let`, pat, termTree, N)) => ctx =>
+        rhss.foldRight(Function.const(fallback): Sequel): (branch, elabFallback) =>
+          branch match
+          case LetLike(`let`, pat, termTree, N) => ctx =>
             val ident = pat match // TODO handle patterns and rm special cases
               case ident: Ident => ident
               case und: Under => new Ident("_").withLocOf(und)
@@ -283,22 +281,20 @@ class Desugarer(val elaborator: Elaborator)
               val sym = VarSymbol(ident)
               val fallbackCtx = ctx + (ident.name -> sym)
               Split.Let(sym, term(termTree)(using ctx), elabFallback(fallbackCtx))
-          case (Tree.Empty(), Modified(Keyword.`do`, doLoc, computation)) => ctx => trace(
+          case Modified(Keyword.`do`, doLoc, computation) => ctx => trace(
             pre = s"termSplit: do $computation",
-            post = (res: Split) => s"termSplit: else >>> $res"
+            post = (res: Split) => s"termSplit: do >>> $res"
           ):
             val sym = TempSymbol(N, "doTemp")
             Split.Let(sym, term(computation)(using ctx), elabFallback(ctx))
-          case (Tree.Empty(), Modified(Keyword.`else`, elsLoc, default)) => ctx =>
+          case Modified(Keyword.`else`, elsLoc, default) => ctx =>
             // TODO: report `rest` as unreachable
             Split.default(term(default)(using ctx))
-          case ((rawOp @ Ident(_)), rhs) => ctx =>
-            val op = term(rawOp)(using ctx)
-            val innerFinish = mkInnerFinish(op)
-            termSplit(rhs, innerFinish)(elabFallback(ctx))(ctx)
-          case (op, rhs) => ctx =>
-            raise(ErrorReport(msg"Unrecognized operator branch." -> op.toLoc :: Nil))
-            elabFallback(ctx)
+          case rawRhs => ctx =>
+            log(s"rawRhs: $rawRhs")
+            val rhs = rawRhs.splitOn(Trm(vs.ref(/* FIXME ident? */)))
+            log(s"rhs: $rhs")
+            termSplit(rhs, identity)(elabFallback(ctx))(ctx)
     case _ => fallback => _ =>
       raise(ErrorReport(msg"Unrecognized term split (${tree.describe})." -> tree.toLoc :: Nil))
       fallback.withoutLoc // Hacky... a loc is always added for the result
@@ -308,15 +304,14 @@ class Desugarer(val elaborator: Elaborator)
    *  @param scrutinee the elaborated scrutinee
    *  @param cont the continuation that needs the symbol and the context
    */
-  def nominate(baseCtx: Ctx, scrutinee: Term)
+  def nominate(baseCtx: Ctx, scrutinee: Term, nameHint: Str = "scrut")
               (cont: BlockLocalSymbol => Sequel): Split = scrutinee match
     case ref @ Term.Ref(symbol: VarSymbol) =>
       val innerCtx = baseCtx + (ref.tree.name -> symbol)
       cont(symbol)(innerCtx)
     case _ =>
-      val name = "scrut"
-      val symbol = TempSymbol(N, name)
-      val innerCtx = baseCtx + (name -> symbol)
+      val symbol = TempSymbol(N, nameHint)
+      val innerCtx = baseCtx + (nameHint -> symbol)
       Split.Let(symbol, scrutinee, cont(symbol)(innerCtx))
 
   /** Decompose a `Tree` of conjunct matches. The tree is from the same line in
@@ -435,7 +430,7 @@ class Desugarer(val elaborator: Elaborator)
         pre = s"patternBranch <<< $patternAndMatches -> ${consequent.fold(_.showDbg, _.showDbg)}",
         post = (res: Split) => s"patternBranch >>> ${res.showDbg}")
     case _ =>
-      raise(ErrorReport(msg"Unrecognized pattern split." -> tree.toLoc :: Nil))
+      raise(ErrorReport(msg"Unrecognized pattern split (${tree.describe})." -> tree.toLoc :: Nil))
       _ => _ => Split.default(Term.Error)
 
   /** Elaborate a single match (a scrutinee and a pattern) and forms a split
@@ -448,7 +443,7 @@ class Desugarer(val elaborator: Elaborator)
   def expandMatch(scrutSymbol: BlockLocalSymbol, pattern: Tree, sequel: Sequel): Split => Sequel =
     def ref = scrutSymbol.ref(/* FIXME ident? */)
     def dealWithCtorCase(ctor: Ctor, compile: Bool)(fallback: Split): Sequel = ctx =>
-      val clsTrm = elaborator.cls(ctor, inAppPrefix = false)
+      val clsTrm = elaborator.cls(term(ctor), inAppPrefix = false)
       clsTrm.symbol.flatMap(_.asClsLike) match
       case S(cls: ClassSymbol) =>
         if compile then warn(msg"Cannot compile the class `${cls.name}`" -> ctor.toLoc)
@@ -475,7 +470,7 @@ class Desugarer(val elaborator: Elaborator)
       pre = s"expandMatch <<< ${ctor}(${args.iterator.map(_.showDbg).mkString(", ")})",
       post = (r: Split) => s"expandMatch >>> ${r.showDbg}"
     ):
-      val clsTrm = elaborator.cls(ctor, inAppPrefix = false)
+      val clsTrm = elaborator.cls(term(ctor), inAppPrefix = false)
       clsTrm.symbol.flatMap(_.asClsLike) match
       case S(cls: ClassSymbol) =>
         val paramSymbols = cls.defn match
@@ -584,10 +579,10 @@ class Desugarer(val elaborator: Elaborator)
         Branch(ref, Pattern.Lit(IntLit(-value)), sequel(ctx)) ~: fallback
       case App(Ident("-"), Tup(DecLit(value) :: Nil)) => fallback => ctx =>
         Branch(ref, Pattern.Lit(DecLit(-value)), sequel(ctx)) ~: fallback
-      case App(Ident("&"), Tree.Tup(lhs :: rhs :: Nil)) => fallback => ctx =>
+      case OpApp(lhs, Ident("&"), rhs :: Nil) => fallback => ctx =>
         val newSequel = expandMatch(scrutSymbol, rhs, sequel)(fallback)
         expandMatch(scrutSymbol, lhs, newSequel)(fallback)(ctx)
-      case App(Ident("|"), Tree.Tup(lhs :: rhs :: Nil)) => fallback => ctx =>
+      case OpApp(lhs, Ident("|"), rhs :: Nil) => fallback => ctx =>
         val newFallback = expandMatch(scrutSymbol, rhs, sequel)(fallback)(ctx)
         expandMatch(scrutSymbol, lhs, sequel)(newFallback)(ctx)
       // A single constructor pattern.
@@ -598,6 +593,9 @@ class Desugarer(val elaborator: Elaborator)
         dealWithAppCtorCase(app, ctor, args, false)
       case app @ App(ctor: Ctor, Tup(args)) =>
         dealWithAppCtorCase(app, ctor, args, false)
+      case app @ OpApp(lhs, ctor: Ctor, rhss) =>
+        // TODO improve (eventually remove DummyApp)
+        dealWithAppCtorCase(Tree.DummyApp, ctor, lhs :: rhss, false)
       // A single literal pattern
       case literal: Literal => fallback => ctx => trace(
         pre = s"expandMatch: literal <<< $literal",

hkmc2/shared/src/main/scala/hkmc2/semantics/ucs/Desugarer.scala

@@ -10,7 +10,7 @@ object HelperExtractors:
   /** A helper extractor for matching the tree of `x | y`. */
   object or:
     infix def unapply(tree: Tree): Opt[(Tree, Tree)] = tree match
-      case App(Ident("|"), Tup(lhs :: rhs :: Nil)) => S(lhs, rhs)
+      case OpApp(lhs, Ident("|"), rhs :: Nil) => S(lhs, rhs)
       case _ => N
 
   /** A helper extractor for matching the tree of `x a y`.*/
@@ -24,11 +24,11 @@ object HelperExtractors:
    */
   object to:
     infix def unapply(tree: Tree): Opt[(Tree, (Bool, Tree))] = tree match
-      case App(Ident("..="), Tup(lhs :: rhs :: Nil)) => S(lhs, (true, rhs))
-      case App(Ident("..<"), Tup(lhs :: rhs :: Nil)) => S(lhs, (false, rhs))
+      case OpApp(lhs, Ident("..="), rhs :: Nil) => S(lhs, (true, rhs))
+      case OpApp(lhs, Ident("..<"), rhs :: Nil) => S(lhs, (false, rhs))
       case _ => N
 
   object `~`:
     infix def unapply(tree: Tree): Opt[(Tree, Tree)] = tree match
-      case App(Ident("~"), Tup(lhs :: rhs :: Nil)) => S(lhs, rhs)
+      case OpApp(lhs, Ident("~"), rhs :: Nil) => S(lhs, rhs)
       case _ => N