diff --git a/base/src/main/java/org/aya/tyck/ctx/LocalLet.java b/base/src/main/java/org/aya/tyck/ctx/LocalLet.java index 8a8726e8f9..123279b84e 100644 --- a/base/src/main/java/org/aya/tyck/ctx/LocalLet.java +++ b/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 subst + @NotNull MutableLinkedHashMap let ) implements Scoped { 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 let) { + return new LocalLet(this, let); } @Override public @NotNull Option 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); } } diff --git a/base/src/main/java/org/aya/tyck/pat/ClauseTycker.java b/base/src/main/java/org/aya/tyck/pat/ClauseTycker.java index 09287b5221..d28a15194f 100644 --- a/base/src/main/java/org/aya/tyck/pat/ClauseTycker.java +++ b/base/src/main/java/org/aya/tyck/pat/ClauseTycker.java @@ -49,23 +49,23 @@ public record TyckResult(@NotNull ImmutableSeq> 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 allBinds, @NotNull ImmutableSeq freePats, @NotNull ImmutableSeq paramSubst, @@ -74,24 +74,18 @@ public record LhsResult( boolean hasError ) { public @NotNull LhsResult mapPats(@NotNull UnaryOperator f) { - return new LhsResult(localCtx, unpiedResult, allBinds, + return new LhsResult(localCtx, result, unpiParamSize, allBinds, freePats.map(f), paramSubst, asSubst, clause, hasError); } public @NotNull SeqView 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 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()); } diff --git a/syntax/src/main/java/org/aya/syntax/core/term/DepTypeTerm.java b/syntax/src/main/java/org/aya/syntax/core/term/DepTypeTerm.java index f4743da52b..5ed70a1329 100644 --- a/syntax/src/main/java/org/aya/syntax/core/term/DepTypeTerm.java +++ b/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 pre) { + /// @param bound -1 for unlimited + public static @NotNull Unpi unpiDBI(@NotNull Term term, @NotNull UnaryOperator pre, int bound) { var params = MutableList.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(); diff --git a/syntax/src/main/java/org/aya/syntax/telescope/Signature.java b/syntax/src/main/java/org/aya/syntax/telescope/Signature.java index eba45936ed..78419c948e 100644 --- a/syntax/src/main/java/org/aya/syntax/telescope/Signature.java +++ b/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 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)));