core: fix unpi

Co-authored-by: Hoshino Tented <[email protected]>

base/src/main/java/org/aya/tyck/ctx/LocalLet.java

@@ -1,4 +1,4 @@
-// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2025 Tesla (Yinsen) Zhang.
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.tyck.ctx;
 
@@ -17,18 +17,22 @@
  */
 public record LocalLet(
   @Override @Nullable LocalLet parent,
-  @NotNull MutableLinkedHashMap<LocalVar, Jdg> subst
+  @NotNull MutableLinkedHashMap<LocalVar, Jdg> let
 ) implements Scoped<LocalVar, Jdg, LocalLet> {
   public LocalLet() { this(null, MutableLinkedHashMap.of()); }
   @Override public @NotNull LocalLet self() { return this; }
 
   @Override public @NotNull LocalLet derive() {
-    return new LocalLet(this, MutableLinkedHashMap.of());
+    return derive(MutableLinkedHashMap.of());
+  }
+
+  public @NotNull LocalLet derive(@NotNull MutableLinkedHashMap<LocalVar, Jdg> let) {
+    return new LocalLet(this, let);
   }
 
   @Override public @NotNull Option<Jdg> getLocal(@NotNull LocalVar key) {
-    return subst.getOption(key);
+    return let.getOption(key);
   }
 
-  @Override public void putLocal(@NotNull LocalVar key, @NotNull Jdg value) { subst.put(key, value); }
+  @Override public void putLocal(@NotNull LocalVar key, @NotNull Jdg value) { let.put(key, value); }
 }

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

@@ -49,23 +49,23 @@ public record TyckResult(@NotNull ImmutableSeq<Pat.Preclause<Term>> clauses, boo
   }
 
   /**
-   * @param unpiedResult the result according to the pattern tycking, the
-   *                     {@link DepTypeTerm.Unpi#params} is always empty if the signature result is
-   *                     {@link org.aya.tyck.pat.iter.Pusheenable.Const}
-   * @param paramSubst   substitution for parameter, in the same ordeer as parameter.
-   *                     See {@link PatternTycker#paramSubst}.
-   * @param freePats     a free version of the patterns.
-   *                     In most cases you want to use {@code clause.pats} instead
-   * @param allBinds     all binders in the patterns
-   * @param asSubst      substitution of the {@code as} patterns
+   * @param result     the result according to the pattern tycking, the
+   *                   {@link DepTypeTerm.Unpi#params} is always empty if the signature result is
+   *                   {@link org.aya.tyck.pat.iter.Pusheenable.Const}
+   * @param paramSubst substitution for parameter, in the same ordeer as parameter.
+   *                   See {@link PatternTycker#paramSubst}. Only used by ExprTyckerm, see {@link #addLocalLet}
+   * @param freePats   a free version of the patterns.
+   *                   In most cases you want to use {@code clause.pats} instead
+   * @param allBinds   all binders in the patterns
+   * @param asSubst    substitution of the {@code as} patterns
    * @implNote If there are fewer pats than parameters, there will be some pats inserted,
    * but this will not affect {@code paramSubst}, and the inserted pat are "ignored" in tycking
-   * of the body, because we check the body against to {@link #unpiedResult}.
+   * of the body, because we check the body against to {@link #result}.
    * Then we apply the inserted pats to the body to complete it.
    */
   public record LhsResult(
     @NotNull LocalCtx localCtx,
-    @NotNull DepTypeTerm.Unpi unpiedResult,
+    @NotNull Term result, int unpiParamSize,
     @NotNull ImmutableSeq<LocalVar> allBinds,
     @NotNull ImmutableSeq<Pat> freePats,
     @NotNull ImmutableSeq<Jdg> paramSubst,
@@ -74,24 +74,18 @@ public record LhsResult(
     boolean hasError
   ) {
     public @NotNull LhsResult mapPats(@NotNull UnaryOperator<Pat> f) {
-      return new LhsResult(localCtx, unpiedResult, allBinds,
+      return new LhsResult(localCtx, result, unpiParamSize, allBinds,
         freePats.map(f), paramSubst, asSubst, clause, hasError);
     }
 
     public @NotNull SeqView<Pat> unpiPats() {
-      return clause.pats().view().takeLast(unpiedResult.params().size());
-    }
-
-    /// Returns the instantiated result type of this clause
-    public @NotNull Term instResult() {
-      // We need not to inline this term even we did before. The [paramSubst] is already inlined.
-      return unpiedResult.makePi().instTele(paramSubst.view().map(Jdg::wellTyped));
+      return clause.pats().view().takeLast(unpiParamSize);
     }
 
     @Contract(mutates = "param2")
     public void addLocalLet(@NotNull ImmutableSeq<LocalVar> teleBinds, @NotNull ExprTycker exprTycker) {
       teleBinds.forEachWith(paramSubst, exprTycker.localLet()::put);
-      exprTycker.setLocalLet(new LocalLet(exprTycker.localLet(), asSubst.subst()));
+      exprTycker.setLocalLet(exprTycker.localLet().derive(asSubst.let()));
     }
   }
 
@@ -180,25 +174,33 @@ public record Worker(
 
       clause.hasError |= patResult.hasError();
       patResult = inline(patResult, ctx);
-      clause.patterns.view().map(it -> it.term().data()).forEach(TermInPatInline::apply);
+      clause.patterns.forEach(it -> TermInPatInline.apply(it.term().data()));
 
       // It is safe to replace ctx:
       // * telescope are well-typed and no Meta
       // * PatternTycker doesn't introduce any Meta term
       ctx = ctx.map(new TermInline());
-      var patWithTypeBound = Pat.collectVariables(patResult.wellTyped().view());
 
-      var unpiBody = sigIter.unpiBody();
       // fill missing patterns
-      var missingPats = unpiBody.params().mapIndexed((idx, x) ->
+      var freeUnpiBody = sigIter.unpiBody();
+      var unpiParamSize = freeUnpiBody.params().size();
+      // This is not a typo of "repl"
+      var instRepi = freeUnpiBody.makePi().instTele(patResult.paramSubst().view().map(Jdg::wellTyped));
+      var instUnpiParam = DepTypeTerm.unpiDBI(instRepi, UnaryOperator.identity(), unpiParamSize);
+      var missingPats = instUnpiParam.params().mapIndexed((idx, x) ->
         // It would be nice if we have a SourcePos here
-        new Pat.Bind(new LocalVar("unpi" + idx, SourcePos.NONE, GenerateKind.Basic.Tyck), x.type()));
+        new Pat.Bind(new LocalVar("unpi" + idx, SourcePos.NONE, GenerateKind.Basic.Tyck),
+          x.type()));
+
+      var wellTypedPats = patResult.wellTyped().appendedAll(missingPats);
+      var patWithTypeBound = Pat.collectVariables(wellTypedPats.view());
 
       var allBinds = patWithTypeBound.component1().toImmutableSeq();
-      var newClause = new Pat.Preclause<>(clause.sourcePos, patWithTypeBound.component2(),
+      var newClause = new Pat.Preclause<>(clause.sourcePos,
+        patWithTypeBound.component2(),
         allBinds.size(), patIter.exprBody());
-      return new LhsResult(ctx, sigIter.unpiBody(), allBinds,
-        patResult.wellTyped().appendedAll(missingPats),
+      return new LhsResult(ctx, instRepi, unpiParamSize, allBinds,
+        wellTypedPats,
         patResult.paramSubst(), patResult.asSubst(), newClause, patResult.hasError());
     }
   }
@@ -229,7 +231,7 @@ else if (result.hasError) {
         exprTycker.setLocalCtx(result.localCtx);
         result.addLocalLet(teleBinds, exprTycker);
         // now exprTycker has all substitutions that PatternTycker introduced.
-        wellBody = exprTycker.inherit(bodyExpr, result.instResult()).wellTyped();
+        wellBody = exprTycker.inherit(bodyExpr, result.result()).wellTyped();
         exprTycker.solveMetas();
         wellBody = zonker.zonk(wellBody);
 
@@ -316,7 +318,7 @@ public static void apply(@NotNull Pattern pat) {
     var paramSubst = result.paramSubst().map(ClauseTycker::inlineTerm);
 
     // map in place 😱😱😱😱
-    result.asSubst().subst().replaceAll((_, t) -> inlineTerm(t));
+    result.asSubst().let().replaceAll((_, t) -> inlineTerm(t));
 
     return new PatternTycker.TyckResult(wellTyped, paramSubst, result.asSubst(), result.hasError());
   }

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

@@ -153,10 +153,12 @@ public Unpi(@NotNull Term body) {
     }
   }
 
-  public static @NotNull Unpi unpiDBI(@NotNull Term term, @NotNull UnaryOperator<Term> pre) {
+  /// @param bound -1 for unlimited
+  public static @NotNull Unpi unpiDBI(@NotNull Term term, @NotNull UnaryOperator<Term> pre, int bound) {
     var params = MutableList.<Param>create();
     var i = 0;
-    while (pre.apply(term) instanceof DepTypeTerm(var kk, var param, var body) && kk == DTKind.Pi) {
+    while ((bound == -1 || i < bound)
+      && pre.apply(term) instanceof DepTypeTerm(var kk, var param, var body) && kk == DTKind.Pi) {
       // Note: PatternTycker depends on the licit of unpi param, be careful to change it!
       params.append(new Param(Integer.toString(i++), param, true));
       term = body.toLocns().body();

syntax/src/main/java/org/aya/syntax/telescope/Signature.java

@@ -1,10 +1,10 @@
-// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2025 Tesla (Yinsen) Zhang.
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.syntax.telescope;
 
 import kala.collection.immutable.ImmutableSeq;
-import org.aya.syntax.core.term.Param;
 import org.aya.syntax.core.term.DepTypeTerm;
+import org.aya.syntax.core.term.Param;
 import org.aya.syntax.core.term.Term;
 import org.aya.syntax.ref.LocalVar;
 import org.aya.util.ForLSP;
@@ -34,7 +34,7 @@ public record Signature(@NotNull AbstractTele.Locns telescope, @NotNull Immutabl
    * the unpi-ed version of it will have the correct de Bruijn index.
    */
   public @NotNull Signature pusheen(UnaryOperator<Term> pre) {
-    var resultPushed = DepTypeTerm.unpiDBI(result(), pre);
+    var resultPushed = DepTypeTerm.unpiDBI(result(), pre, -1);
     return new Signature(
       new AbstractTele.Locns(params().appendedAll(resultPushed.params().view()), resultPushed.body()),
       pos.appendedAll(ImmutableSeq.fill(resultPushed.params().size(), SourcePos.NONE)));