merge: Cleverly create bind amount, not calculate them upon jIT (#1110)

Fix #1066

base/src/main/java/org/aya/resolve/context/ModuleSymbol.java

@@ -23,12 +23,8 @@
  *              It says a `Symbol` can be referred by `{Component}::{Unqualified}`
  * @apiNote the methods that end with `Definitely` will get/remove only one symbol or fail if ambiguous.
  */
-public record ModuleSymbol<T>(
-  @NotNull MutableMap<String, MutableMap<ModuleName, T>> table
-) {
-  public ModuleSymbol() {
-    this(MutableMap.create());
-  }
+public record ModuleSymbol<T>(@NotNull MutableMap<String, MutableMap<ModuleName, T>> table) {
+  public ModuleSymbol() { this(MutableMap.create()); }
 
   public ModuleSymbol(@NotNull ModuleSymbol<T> other) {
     this(other.table.toImmutableSeq().collect(MutableMap.collector(
@@ -38,8 +34,10 @@ public ModuleSymbol(@NotNull ModuleSymbol<T> other) {
   }
 
   /** @apiNote should not use this after {@link #asMut} is called. */
-  public record UnqualifiedResolve<T>(@NotNull MapView<ModuleName, T> map,
-                                      @NotNull LazyValue<MutableMap<ModuleName, T>> asMut) {
+  public record UnqualifiedResolve<T>(
+    @NotNull MapView<ModuleName, T> map,
+    @NotNull LazyValue<MutableMap<ModuleName, T>> asMut
+  ) {
     public @NotNull ImmutableSeq<T> uniqueCandidates() {
       return map.valuesView().distinct().toImmutableSeq();
     }
@@ -95,8 +93,8 @@ public record UnqualifiedResolve<T>(@NotNull MapView<ModuleName, T> map,
    */
   public @NotNull Result<T, Error> getMaybe(@NotNull ModuleName component, @NotNull String unqualifiedName) {
     return switch (component) {
-      case ModuleName.Qualified qualified -> getQualifiedMaybe(component, unqualifiedName).toResult(Error.NotFound);
-      case ModuleName.ThisRef aThis -> getUnqualifiedMaybe(unqualifiedName);
+      case ModuleName.Qualified qualified -> getQualifiedMaybe(qualified, unqualifiedName).toResult(Error.NotFound);
+      case ModuleName.ThisRef _ -> getUnqualifiedMaybe(unqualifiedName);
     };
   }
 
@@ -118,11 +116,7 @@ public enum Error {
    *
    * @implNote This method always overwrites the symbol that is added in the past.
    */
-  public Option<T> add(
-    @NotNull ModuleName componentName,
-    @NotNull String name,
-    @NotNull T ref
-  ) {
+  public Option<T> add(@NotNull ModuleName componentName, @NotNull String name, @NotNull T ref) {
     var candidates = resolveUnqualified(name).asMut.get();
     return candidates.put(componentName, ref);
   }

base/src/main/java/org/aya/tyck/pat/ClauseTycker.java

@@ -114,10 +114,11 @@ public record Worker(
     exprTycker.solveMetas();
 
     // inline terms in rhsResult
-    rhsResult = rhsResult.map(x -> new Pat.Preclause<>(
-      x.sourcePos(),
-      x.pats().map(p -> p.descent(UnaryOperator.identity(), exprTycker::zonk)),
-      x.expr() == null ? null : x.expr().descent((_, t) -> exprTycker.zonk(t))
+    rhsResult = rhsResult.map(preclause -> new Pat.Preclause<>(
+      preclause.sourcePos(),
+      preclause.pats().map(p -> p.descent(UnaryOperator.identity(), exprTycker::zonk)),
+      preclause.bindCount(),
+      preclause.expr() == null ? null : preclause.expr().descent((_, t) -> exprTycker.zonk(t))
     ));
 
     return new TyckResult(
@@ -170,8 +171,10 @@ public record Worker(
       ctx = ctx.map(TermInline::apply);
       var patWithTypeBound = Pat.collectVariables(patResult.wellTyped().view());
 
-      var newClause = new Pat.Preclause<>(clause.sourcePos, patWithTypeBound.component2(), patResult.newBody());
-      return new LhsResult(ctx, resultTerm, patWithTypeBound.component1().toImmutableSeq(),
+      var allBinds = patWithTypeBound.component1().toImmutableSeq();
+      var newClause = new Pat.Preclause<>(clause.sourcePos, patWithTypeBound.component2(),
+        allBinds.size(), patResult.newBody());
+      return new LhsResult(ctx, resultTerm, allBinds,
         patResult.wellTyped(), patResult.paramSubst(), patResult.asSubst(), newClause, patResult.hasError());
     });
   }
@@ -189,6 +192,7 @@ public record Worker(
       var clause = result.clause;
       var bodyExpr = clause.expr();
       Term wellBody;
+      var bindCount = 0;
       if (bodyExpr == null) wellBody = null;
       else if (result.hasError) {
         // In case the patterns are malformed, do not check the body
@@ -204,11 +208,13 @@ else if (result.hasError) {
         wellBody = exprTycker.inherit(bodyExpr, result.type).wellTyped();
 
         // bind all pat bindings
-        var patBindTele = Pat.collectVariables(result.clause.pats().view()).component1().view();
-        wellBody = wellBody.bindTele(patBindTele);
+        var patBindTele = Pat.collectVariables(result.clause.pats().view()).component1();
+        bindCount = patBindTele.size();
+        wellBody = wellBody.bindTele(patBindTele.view());
       }
 
-      return new Pat.Preclause<>(clause.sourcePos(), clause.pats(), wellBody == null ? null : WithPos.dummy(wellBody));
+      return new Pat.Preclause<>(clause.sourcePos(), clause.pats(), bindCount,
+        wellBody == null ? null : WithPos.dummy(wellBody));
     });
   }
 

cli-impl/src/test/java/org/aya/test/TestRunner.java

@@ -140,6 +140,7 @@ private static void runSingleCase(String code, SingleFileCompiler compiler) thro
 
   public static @NotNull CompilerFlags flags() {
     var modulePaths = ImmutableSeq.of(DEFAULT_TEST_DIR.resolve("shared/src"));
-    return new CompilerFlags(CompilerFlags.Message.ASCII, false, false, null, modulePaths, null);
+    return new CompilerFlags(CompilerFlags.Message.ASCII,
+      false, false, null, modulePaths, null);
   }
 }

cli-impl/src/test/java/org/aya/test/fixtures/ParseError.java

@@ -6,12 +6,8 @@
 
 @SuppressWarnings("unused")
 public interface ParseError {
-  String testTrivial = """
-    def
-    """;
-  @Language("Aya") String testModifier = """
-    overlap inductive Empty
-    """;
+  String testTrivial = "def";
+  @Language("Aya") String testModifier = "overlap inductive E";
   @Language("Aya") String testIgnoredModifier = """
     inline def id {A : Type} A : A
     | a => a

cli-impl/src/test/resources/negative/ParseError.txt

@@ -12,7 +12,7 @@ What are you doing?
 Modifier:
 In file $FILE:1:0 ->
 
-  1 │   overlap inductive Empty
+  1 │   overlap inductive E
     │   ╰─────╯
 
 Error: The modifier overlap is not suitable here.

jit-compiler/src/main/java/org/aya/compiler/FnSerializer.java

@@ -57,7 +57,7 @@ private void buildInvoke(FnDef unit, @NotNull String onStuckTerm, @NotNull Immut
       case Either.Right(var clauses) -> {
         var ser = new PatternSerializer(this.sourceBuilder, argTerms, onStuckCon, onStuckCon);
         ser.serialize(clauses.map(matching -> new PatternSerializer.Matching(
-          matching.patterns(), (s, bindSize) ->
+          matching.bindCount(), matching.patterns(), (s, bindSize) ->
           s.buildReturn(serializeTermUnderTele(matching.body(), PatternSerializer.VARIABLE_RESULT, bindSize))
         )));
       }

jit-compiler/src/main/java/org/aya/compiler/PatternExprializer.java

@@ -4,7 +4,6 @@
 
 import kala.collection.immutable.ImmutableSeq;
 import org.aya.syntax.core.pat.Pat;
-import org.aya.syntax.core.term.ErrorTerm;
 import org.aya.syntax.core.term.Term;
 import org.aya.syntax.core.term.call.ConCallLike;
 import org.aya.syntax.ref.LocalVar;
@@ -21,7 +20,6 @@ public class PatternExprializer extends AbstractExprializer<Pat> {
   public static final @NotNull String CLASS_PAT_INT = ExprializeUtils.makeSub(CLASS_PAT, ExprializeUtils.getJavaReference(Pat.ShapedInt.class));
   public static final @NotNull String CLASS_LOCALVAR = ExprializeUtils.getJavaReference(LocalVar.class);
   public static final @NotNull String CLASS_CONHEAD = ExprializeUtils.makeSub(ExprializeUtils.getJavaReference(ConCallLike.class), ExprializeUtils.getJavaReference(ConCallLike.Head.class));
-  public static final @NotNull String CLASS_ERROR = ExprializeUtils.getJavaReference(ErrorTerm.class);
   public static final @NotNull String CLASS_PAT_TUPLE = ExprializeUtils.makeSub(CLASS_PAT, ExprializeUtils.getJavaReference(Pat.Tuple.class));
 
   private final boolean allowLocalTerm;
@@ -67,8 +65,5 @@ protected PatternExprializer(@NotNull NameGenerator nameGen, boolean allowLocalT
     };
   }
 
-  @Override
-  public @NotNull String serialize(Pat unit) {
-    return doSerialize(unit);
-  }
+  @Override public @NotNull String serialize(Pat unit) { return doSerialize(unit); }
 }

jit-compiler/src/main/java/org/aya/compiler/PatternSerializer.java

@@ -6,7 +6,6 @@
 import kala.collection.immutable.ImmutableSeq;
 import kala.collection.immutable.primitive.ImmutableIntSeq;
 import kala.range.primitive.IntRange;
-import kala.value.primitive.MutableIntValue;
 import org.aya.generic.AyaDocile;
 import org.aya.generic.State;
 import org.aya.syntax.core.pat.Pat;
@@ -27,28 +26,23 @@ public interface SuccessContinuation extends BiConsumer<PatternSerializer, Integ
   }
 
   public final static class Once implements Runnable {
-    public static @NotNull Once of(@NotNull Runnable run) {
-      return new Once(run);
-    }
-
+    public static @NotNull Once of(@NotNull Runnable run) { return new Once(run); }
     private final @NotNull Runnable run;
     private boolean dirty = false;
 
     public Once(@NotNull Runnable run) { this.run = run; }
 
-    @Override
-    public void run() {
-      if (dirty) {
-        throw new Panic("Once");
-      }
-
+    @Override public void run() {
+      if (dirty) throw new Panic("Once");
       dirty = true;
       this.run.run();
     }
   }
 
-  public record Matching(@NotNull ImmutableSeq<Pat> patterns, @NotNull SuccessContinuation onSucc) {
-  }
+  public record Matching(
+    int bindCount, @NotNull ImmutableSeq<Pat> patterns,
+    @NotNull SuccessContinuation onSucc
+  ) { }
 
   public static final @NotNull String VARIABLE_RESULT = "result";
   public static final @NotNull String VARIABLE_STATE = "matchState";
@@ -135,9 +129,7 @@ private void multiStage(
     buildLocalVar(CLASS_TERM, tmpName, term);
 
     for (var pre : preContinuation) {
-      buildIf(STR."! \{VARIABLE_SUBSTATE}", () -> {
-        pre.accept(tmpName);
-      });
+      buildIf(STR."! \{VARIABLE_SUBSTATE}", () -> pre.accept(tmpName));
     }
 
     buildIf(VARIABLE_SUBSTATE, continuation);
@@ -190,20 +182,14 @@ private void onMatchBind(@NotNull String term) {
     appendLine(STR."\{VARIABLE_RESULT}.set(\{bindCount++}, \{term});");
   }
 
-  private int bindAmount(@NotNull ImmutableSeq<Pat> pats) {
-    var acc = MutableIntValue.create();
-    pats.forEach(pat -> pat.consumeBindings((_, _) -> acc.increment()));
-    return acc.get();
-  }
-
   /// endregion Java Source Code Generate API
 
   @Override public PatternSerializer serialize(@NotNull ImmutableSeq<Matching> unit) {
     if (unit.isEmpty()) {
       onMismatch.accept(this);
       return this;
     }
-    var bindSize = unit.mapToInt(ImmutableIntSeq.factory(), x -> bindAmount(x.patterns));
+    var bindSize = unit.mapToInt(ImmutableIntSeq.factory(), Matching::bindCount);
     int maxBindSize = bindSize.max();
 
     buildLocalVar(STR."\{CLASS_MUTSEQ}<\{CLASS_TERM}>", VARIABLE_RESULT, STR."\{CLASS_MUTSEQ}.fill(\{maxBindSize}, (\{CLASS_TERM}) null)");

syntax/src/main/java/org/aya/syntax/core/pat/Pat.java

@@ -49,7 +49,6 @@ public sealed interface Pat extends AyaDocile {
    */
   void consumeBindings(@NotNull BiConsumer<LocalVar, Term> consumer);
 
-
   /**
    * Bind the types in {@link Pat}s
    *
@@ -263,7 +262,7 @@ public ShapedInt update(DataCall type) {
   record Preclause<T extends AyaDocile>(
     @NotNull SourcePos sourcePos,
     @NotNull ImmutableSeq<Pat> pats,
-    @Nullable WithPos<T> expr
+    int bindCount, @Nullable WithPos<T> expr
   ) implements AyaDocile {
     @Override public @NotNull Doc toDoc(@NotNull PrettierOptions options) {
       var prettier = new CorePrettier(options);
@@ -273,13 +272,14 @@ record Preclause<T extends AyaDocile>(
     }
 
     public static @NotNull Preclause<Term> weaken(@NotNull Term.Matching clause) {
-      return new Preclause<>(clause.sourcePos(), clause.patterns(), WithPos.dummy(clause.body()));
+      return new Preclause<>(clause.sourcePos(), clause.patterns(), clause.bindCount(),
+        WithPos.dummy(clause.body()));
     }
 
     public static @NotNull Option<Term.Matching>
     lift(@NotNull Preclause<Term> clause) {
       if (clause.expr == null) return Option.none();
-      var match = new Term.Matching(clause.sourcePos, clause.pats, clause.expr.data());
+      var match = new Term.Matching(clause.sourcePos, clause.pats, clause.bindCount, clause.expr.data());
       return Option.some(match);
     }
   }

syntax/src/main/java/org/aya/syntax/core/term/Term.java

@@ -181,15 +181,15 @@ public sealed interface Term extends Serializable, AyaDocile
   record Matching(
     @NotNull SourcePos sourcePos,
     @NotNull ImmutableSeq<Pat> patterns,
-    @NotNull Term body
+    int bindCount, @NotNull Term body
   ) implements AyaDocile {
     @Override public @NotNull Doc toDoc(@NotNull PrettierOptions options) {
       return Pat.Preclause.weaken(this).toDoc(options);
     }
 
     public @NotNull Matching update(@NotNull ImmutableSeq<Pat> patterns, @NotNull Term body) {
       return body == body() && patterns.sameElements(patterns(), true) ? this
-        : new Matching(sourcePos, patterns, body);
+        : new Matching(sourcePos, patterns, bindCount, body);
     }
 
     public @NotNull Matching descent(@NotNull UnaryOperator<Term> f, @NotNull UnaryOperator<Pat> g) {