From c1c3847df15438e104069df054736eabed07eb8f Mon Sep 17 00:00:00 2001 From: HoshinoTented Date: Thu, 9 Jan 2025 16:06:12 +0800 Subject: [PATCH 1/3] term: use `bindAllFrom` primitively --- .../java/org/aya/tyck/tycker/TeleTycker.java | 16 ++----------- .../java/org/aya/syntax/compile/JitCon.java | 2 +- .../java/org/aya/syntax/core/def/ConDef.java | 4 ++-- .../org/aya/syntax/core/term/FreeTerm.java | 18 +++++++++++---- .../java/org/aya/syntax/core/term/Param.java | 9 ++++++-- .../java/org/aya/syntax/core/term/Term.java | 23 +++++++++++++------ 6 files changed, 42 insertions(+), 30 deletions(-) diff --git a/base/src/main/java/org/aya/tyck/tycker/TeleTycker.java b/base/src/main/java/org/aya/tyck/tycker/TeleTycker.java index 44c029a1fb..a8a00a73d8 100644 --- a/base/src/main/java/org/aya/tyck/tycker/TeleTycker.java +++ b/base/src/main/java/org/aya/tyck/tycker/TeleTycker.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.tycker; @@ -77,19 +77,7 @@ public sealed interface TeleTycker extends Contextful { */ @Contract(mutates = "param2") static void bindTele(ImmutableSeq binds, MutableSeq tele) { - final var lastIndex = tele.size() - 1; - // fix some param, say [p] - // we skip the last parameter, which need no binds - for (int i = lastIndex - 1; i >= 0; i--) { - var p = binds.get(i); - // for any other param that is able to refer to [p] - for (int j = i + 1; j < tele.size(); j++) { - var og = tele.get(j); - // j - i is the human distance between [p] and [og]. However, we count from 0 - int ii = i, jj = j; - tele.set(j, og.descent(x -> x.bindAt(p, jj - ii - 1))); - } - } + tele.replaceAllIndexed((i, p) -> p.descent(t -> t.bindTele(binds.sliceView(0, i)))); } @Contract(mutates = "param3") diff --git a/syntax/src/main/java/org/aya/syntax/compile/JitCon.java b/syntax/src/main/java/org/aya/syntax/compile/JitCon.java index 6f7b177c2e..43002c7b3f 100644 --- a/syntax/src/main/java/org/aya/syntax/compile/JitCon.java +++ b/syntax/src/main/java/org/aya/syntax/compile/JitCon.java @@ -76,6 +76,6 @@ protected JitCon( this.selfTele = selfTele.toImmutableSeq(); } - return Param.substTele(selfTele.view(), ownerArgs.view()).toImmutableSeq(); + return Param.instTele(selfTele.view(), ownerArgs.view()).toImmutableSeq(); } } diff --git a/syntax/src/main/java/org/aya/syntax/core/def/ConDef.java b/syntax/src/main/java/org/aya/syntax/core/def/ConDef.java index 451003aa74..d9f85b0581 100644 --- a/syntax/src/main/java/org/aya/syntax/core/def/ConDef.java +++ b/syntax/src/main/java/org/aya/syntax/core/def/ConDef.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.syntax.core.def; @@ -55,7 +55,7 @@ public static final class Delegate extends TyckAnyDef implements ConDefL @Override public int selfTeleSize() { return core().selfTele.size(); } @Override public int ownerTeleSize() { return core().ownerTele.size(); } @Override public @NotNull ImmutableSeq selfTele(@NotNull ImmutableSeq ownerArgs) { - return Param.substTele(core().selfTele.view(), ownerArgs.view()).toImmutableSeq(); + return Param.instTele(core().selfTele.view(), ownerArgs.view()).toImmutableSeq(); } @Override public @NotNull DataDefLike dataRef() { return core().dataRef; } diff --git a/syntax/src/main/java/org/aya/syntax/core/term/FreeTerm.java b/syntax/src/main/java/org/aya/syntax/core/term/FreeTerm.java index 0b6ed20c7c..19615eab5a 100644 --- a/syntax/src/main/java/org/aya/syntax/core/term/FreeTerm.java +++ b/syntax/src/main/java/org/aya/syntax/core/term/FreeTerm.java @@ -1,7 +1,8 @@ -// 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.core.term; +import kala.collection.immutable.ImmutableSeq; import kala.function.IndexedFunction; import org.aya.syntax.core.term.marker.TyckInternal; import org.aya.syntax.ref.LocalVar; @@ -10,8 +11,17 @@ public record FreeTerm(@NotNull LocalVar name) implements TyckInternal { public FreeTerm(@NotNull String name) { this(LocalVar.generate(name)); } @Override public @NotNull Term descent(@NotNull IndexedFunction f) { return this; } - @Override public @NotNull Term bindAt(@NotNull LocalVar var, int depth) { - if (name == var) return new LocalTerm(depth); - return this; + // @Override public @NotNull Term bindAt(@NotNull LocalVar var, int depth) { + // if (name == var) return new LocalTerm(depth); + // return this; + // } + + @Override + public @NotNull Term bindAllFrom(@NotNull ImmutableSeq vars, int fromDepth) { + var idx = vars.indexOf(this.name); + if (idx == -1) return this; + + var realDepth = fromDepth + idx; + return new LocalTerm(realDepth); } } diff --git a/syntax/src/main/java/org/aya/syntax/core/term/Param.java b/syntax/src/main/java/org/aya/syntax/core/term/Param.java index 32da559af1..e371911e58 100644 --- a/syntax/src/main/java/org/aya/syntax/core/term/Param.java +++ b/syntax/src/main/java/org/aya/syntax/core/term/Param.java @@ -1,8 +1,9 @@ -// 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.core.term; import kala.collection.SeqView; +import kala.collection.immutable.ImmutableSeq; import org.aya.generic.AyaDocile; import org.aya.pretty.doc.Doc; import org.aya.syntax.core.RichParam; @@ -17,10 +18,14 @@ import java.util.function.UnaryOperator; public record Param(@NotNull String name, @NotNull Term type, boolean explicit) implements AyaDocile { - public static @NotNull SeqView substTele(SeqView tele, SeqView subst) { + public static @NotNull SeqView instTele(SeqView tele, SeqView subst) { return tele.mapIndexed((idx, p) -> p.descent(ty -> ty.instTeleFrom(idx, subst))); } + public static @NotNull SeqView bindTele(@NotNull SeqView tele, @NotNull SeqView vars) { + return tele.mapIndexed((idx, p) -> p.descent(t -> t.bindTele(idx, vars))); + } + public boolean nameEq(@Nullable String otherName) { return name.equals(otherName); } // public @NotNull Arg toArg() { return new Arg<>(type, explicit); } public @NotNull Pat toFreshPat() { return new Pat.Bind(LocalVar.generate(name), type); } diff --git a/syntax/src/main/java/org/aya/syntax/core/term/Term.java b/syntax/src/main/java/org/aya/syntax/core/term/Term.java index a8db3a88ad..a2efa3aaab 100644 --- a/syntax/src/main/java/org/aya/syntax/core/term/Term.java +++ b/syntax/src/main/java/org/aya/syntax/core/term/Term.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.syntax.core.term; @@ -34,7 +34,16 @@ public sealed interface Term extends Serializable, AyaDocile } default @NotNull Term bindAt(@NotNull LocalVar var, int depth) { - return descent((i, t) -> t.bindAt(var, depth + i)); + return bindAllFrom(ImmutableSeq.of(var), depth); + } + + /// Bind all [LocalVar] since `fromDepth`, + /// the i-th [LocalVar] in `vars` will be replaced by a [LocalTerm] with index `fromDepth + i`. + /// + /// @see #replaceAllFrom + default @NotNull Term bindAllFrom(@NotNull ImmutableSeq vars, int fromDepth) { + if (vars.isEmpty()) return this; + return descent((i, t) -> t.bindAllFrom(vars, fromDepth + i)); } /** @@ -60,17 +69,17 @@ public sealed interface Term extends Serializable, AyaDocile */ default @NotNull Term bindTele(int depth, @NotNull SeqView teleVars) { if (teleVars.isEmpty()) return this; - return teleVars.reversed().foldLeftIndexed(this, - (idx, acc, var) -> acc.bindAt(var, depth + idx)); + return bindAllFrom(teleVars.reversed().toImmutableSeq(), depth); } default @NotNull Term bindTele(@NotNull SeqView teleVars) { return bindTele(0, teleVars); } - /** - * Replacing indexes from {@code from} to {@code from + list.size()} (exclusive) with {@code list} - */ + /// Replacing indexes from `from` to `from + list.size()` (exclusive) with `list`, + /// a [LocalTerm] with index `from + i` will be replaced by `list[i]` if possible. + /// + /// @see #bindAllFrom @ApiStatus.Internal default @NotNull Term replaceAllFrom(int from, @NotNull ImmutableSeq list) { if (list.isEmpty()) return this; From 58ec58db4351561ee758f603468a34b88b8ddcaf Mon Sep 17 00:00:00 2001 From: HoshinoTented Date: Thu, 9 Jan 2025 16:10:20 +0800 Subject: [PATCH 2/3] ci: coverage > beauty --- syntax/src/main/java/org/aya/syntax/core/term/Param.java | 4 ---- 1 file changed, 4 deletions(-) diff --git a/syntax/src/main/java/org/aya/syntax/core/term/Param.java b/syntax/src/main/java/org/aya/syntax/core/term/Param.java index e371911e58..bd703fdd7a 100644 --- a/syntax/src/main/java/org/aya/syntax/core/term/Param.java +++ b/syntax/src/main/java/org/aya/syntax/core/term/Param.java @@ -22,10 +22,6 @@ public record Param(@NotNull String name, @NotNull Term type, boolean explicit) return tele.mapIndexed((idx, p) -> p.descent(ty -> ty.instTeleFrom(idx, subst))); } - public static @NotNull SeqView bindTele(@NotNull SeqView tele, @NotNull SeqView vars) { - return tele.mapIndexed((idx, p) -> p.descent(t -> t.bindTele(idx, vars))); - } - public boolean nameEq(@Nullable String otherName) { return name.equals(otherName); } // public @NotNull Arg toArg() { return new Arg<>(type, explicit); } public @NotNull Pat toFreshPat() { return new Pat.Bind(LocalVar.generate(name), type); } From 858c1d6ac22804dc38c234b2d822fe925ab51025 Mon Sep 17 00:00:00 2001 From: ice1000 Date: Thu, 9 Jan 2025 16:33:18 -0500 Subject: [PATCH 3/3] review: optimize import --- .../main/java/org/aya/syntax/core/term/FreeTerm.java | 3 +-- .../java/org/aya/syntax/core/term/LocalTerm.java | 12 +++--------- .../main/java/org/aya/syntax/core/term/Param.java | 1 - 3 files changed, 4 insertions(+), 12 deletions(-) diff --git a/syntax/src/main/java/org/aya/syntax/core/term/FreeTerm.java b/syntax/src/main/java/org/aya/syntax/core/term/FreeTerm.java index 19615eab5a..94fc2dc59c 100644 --- a/syntax/src/main/java/org/aya/syntax/core/term/FreeTerm.java +++ b/syntax/src/main/java/org/aya/syntax/core/term/FreeTerm.java @@ -16,8 +16,7 @@ public record FreeTerm(@NotNull LocalVar name) implements TyckInternal { // return this; // } - @Override - public @NotNull Term bindAllFrom(@NotNull ImmutableSeq vars, int fromDepth) { + @Override public @NotNull Term bindAllFrom(@NotNull ImmutableSeq vars, int fromDepth) { var idx = vars.indexOf(this.name); if (idx == -1) return this; diff --git a/syntax/src/main/java/org/aya/syntax/core/term/LocalTerm.java b/syntax/src/main/java/org/aya/syntax/core/term/LocalTerm.java index 1313889efd..992b23b3bc 100644 --- a/syntax/src/main/java/org/aya/syntax/core/term/LocalTerm.java +++ b/syntax/src/main/java/org/aya/syntax/core/term/LocalTerm.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.syntax.core.term; @@ -12,14 +12,8 @@ public record LocalTerm(int index) implements Term { assert index >= 0 : "Sanity check"; } - @Override - public @NotNull Term descent(@NotNull IndexedFunction f) { - return this; - } - - @Override public @NotNull Term bindAt(@NotNull LocalVar var, int depth) { - return this; - } + @Override public @NotNull Term descent(@NotNull IndexedFunction f) { return this; } + @Override public @NotNull Term bindAt(@NotNull LocalVar var, int depth) { return this; } @Override public @NotNull Term replaceAllFrom(int from, @NotNull ImmutableSeq list) { var i = index - from; diff --git a/syntax/src/main/java/org/aya/syntax/core/term/Param.java b/syntax/src/main/java/org/aya/syntax/core/term/Param.java index bd703fdd7a..7f0e1dd573 100644 --- a/syntax/src/main/java/org/aya/syntax/core/term/Param.java +++ b/syntax/src/main/java/org/aya/syntax/core/term/Param.java @@ -3,7 +3,6 @@ package org.aya.syntax.core.term; import kala.collection.SeqView; -import kala.collection.immutable.ImmutableSeq; import org.aya.generic.AyaDocile; import org.aya.pretty.doc.Doc; import org.aya.syntax.core.RichParam;