From 569e665457b3ea06dc3298d1e65d21349a91f84e Mon Sep 17 00:00:00 2001 From: ice1000 Date: Mon, 27 Jan 2025 10:59:22 -0500 Subject: [PATCH 1/3] chore: remove unused methods --- .../java/org/aya/resolve/context/Context.java | 19 ++++++--------- base/src/test/java/org/aya/tyck/TyckTest.java | 23 +++++++++---------- .../java/org/aya/syntax/core/RichParam.java | 5 ---- 3 files changed, 18 insertions(+), 29 deletions(-) diff --git a/base/src/main/java/org/aya/resolve/context/Context.java b/base/src/main/java/org/aya/resolve/context/Context.java index 43e7e2d2ef..295a0ec3d4 100644 --- a/base/src/main/java/org/aya/resolve/context/Context.java +++ b/base/src/main/java/org/aya/resolve/context/Context.java @@ -1,7 +1,11 @@ -// 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.resolve.context; +import java.nio.file.Path; +import java.util.function.Function; +import java.util.function.Predicate; + import kala.collection.SeqLike; import kala.collection.immutable.ImmutableSeq; import kala.collection.mutable.MutableList; @@ -22,10 +26,6 @@ import org.jetbrains.annotations.NotNull; import org.jetbrains.annotations.Nullable; -import java.nio.file.Path; -import java.util.function.Function; -import java.util.function.Predicate; - /** * @author re-xyr */ @@ -175,10 +175,7 @@ default MutableList collect(@NotNull MutableList container) return iterate(c -> c.getModuleLocalMaybe(modName)); } - default @NotNull Context bind( - @NotNull LocalVar ref, - @NotNull Predicate<@Nullable AnyVar> toWarn - ) { + default @NotNull Context bind(@NotNull LocalVar ref, @NotNull Predicate<@Nullable AnyVar> toWarn) { return bind(ref.name(), ref, toWarn); } @@ -218,8 +215,6 @@ default MutableList collect(@NotNull MutableList container) } class ResolvingInterruptedException extends InterruptException { - @Override public InterruptStage stage() { - return InterruptStage.Resolving; - } + @Override public InterruptStage stage() { return InterruptStage.Resolving; } } } diff --git a/base/src/test/java/org/aya/tyck/TyckTest.java b/base/src/test/java/org/aya/tyck/TyckTest.java index 5a5a903744..35ba04944f 100644 --- a/base/src/test/java/org/aya/tyck/TyckTest.java +++ b/base/src/test/java/org/aya/tyck/TyckTest.java @@ -2,6 +2,16 @@ // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file. package org.aya.tyck; +import java.io.IOException; +import java.nio.file.Files; +import java.nio.file.Paths; +import java.util.Random; +import java.util.function.Function; +import java.util.function.IntFunction; + +import static org.junit.jupiter.api.Assertions.assertNotNull; +import static org.junit.jupiter.api.Assertions.assertTrue; + import kala.collection.immutable.ImmutableSeq; import kala.collection.immutable.primitive.ImmutableIntSeq; import org.aya.normalize.Normalizer; @@ -22,16 +32,6 @@ import org.jetbrains.annotations.NotNull; import org.junit.jupiter.api.Test; -import java.io.IOException; -import java.nio.file.Files; -import java.nio.file.Paths; -import java.util.Random; -import java.util.function.Function; -import java.util.function.IntFunction; - -import static org.junit.jupiter.api.Assertions.assertNotNull; -import static org.junit.jupiter.api.Assertions.assertTrue; - public class TyckTest { @Test public void test0() { var result = tyck(""" @@ -159,8 +159,7 @@ class Monoid """).defs.isNotEmpty()); } - @Test - public void what() { + @Test public void what() { assertTrue(tyck(""" class Kontainer | Taipe : Type diff --git a/syntax/src/main/java/org/aya/syntax/core/RichParam.java b/syntax/src/main/java/org/aya/syntax/core/RichParam.java index 78d97ec54f..318b85c9e8 100644 --- a/syntax/src/main/java/org/aya/syntax/core/RichParam.java +++ b/syntax/src/main/java/org/aya/syntax/core/RichParam.java @@ -4,10 +4,8 @@ import org.aya.generic.term.ParamLike; import org.aya.syntax.core.term.FreeTerm; -import org.aya.syntax.core.term.Param; import org.aya.syntax.core.term.Term; import org.aya.syntax.ref.LocalVar; -import org.jetbrains.annotations.Contract; import org.jetbrains.annotations.NotNull; /** @@ -23,7 +21,4 @@ public record RichParam( } public @NotNull FreeTerm toTerm() { return new FreeTerm(ref); } - @Contract("-> new") public @NotNull Param degenerate() { - return new Param(ref.name(), type, explicit); - } } From 9a4851dbb255faba204f6f7f071e0bed04cf5fcd Mon Sep 17 00:00:00 2001 From: ice1000 Date: Tue, 28 Jan 2025 10:41:09 -0500 Subject: [PATCH 2/3] chore: uncomment some class-related code --- .../java/org/aya/primitive/ShapeMatcher.java | 4 +-- ide/src/main/java/org/aya/ide/Resolver.java | 36 +++++++++---------- .../compiler/serializers/DataSerializer.java | 16 ++++----- .../serializers/ModuleSerializer.java | 10 +++--- .../java/org/aya/syntax/core/def/DataDef.java | 15 +++----- .../org/aya/syntax/core/def/TyckAnyDef.java | 8 ++--- 6 files changed, 42 insertions(+), 47 deletions(-) diff --git a/base/src/main/java/org/aya/primitive/ShapeMatcher.java b/base/src/main/java/org/aya/primitive/ShapeMatcher.java index 08b10da7b0..d13526be32 100644 --- a/base/src/main/java/org/aya/primitive/ShapeMatcher.java +++ b/base/src/main/java/org/aya/primitive/ShapeMatcher.java @@ -173,8 +173,8 @@ yield matchMany(MatchMode.OrderedEq, conLike.innerPats(), con.args().view(), private boolean matchData(@NotNull DataShape shape, @NotNull DataDef data) { if (!matchTele(shape.tele(), data.telescope())) return false; - return matchInside(() -> captures.put(shape.name(), data.ref), - () -> matchMany(MatchMode.Eq, shape.cons(), data.body, + return matchInside(() -> captures.put(shape.name(), data.ref()), + () -> matchMany(MatchMode.Eq, shape.cons(), data.body(), (s, c) -> captureIfMatches(s, c, this::matchCon, ConDef::ref))); } diff --git a/ide/src/main/java/org/aya/ide/Resolver.java b/ide/src/main/java/org/aya/ide/Resolver.java index eae86e7949..ac4a20bb57 100644 --- a/ide/src/main/java/org/aya/ide/Resolver.java +++ b/ide/src/main/java/org/aya/ide/Resolver.java @@ -1,7 +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.ide; +import java.util.Objects; + import kala.collection.SeqView; import kala.collection.mutable.MutableList; import kala.control.Option; @@ -12,9 +14,8 @@ import org.aya.ide.util.XY; import org.aya.syntax.concrete.stmt.ModuleName; import org.aya.syntax.concrete.stmt.StmtVisitor; -import org.aya.syntax.concrete.stmt.decl.DataCon; -import org.aya.syntax.concrete.stmt.decl.DataDecl; -import org.aya.syntax.concrete.stmt.decl.Decl; +import org.aya.syntax.concrete.stmt.decl.*; +import org.aya.syntax.core.def.ClassDef; import org.aya.syntax.core.def.DataDef; import org.aya.syntax.core.def.TyckDef; import org.aya.syntax.core.term.Term; @@ -24,8 +25,6 @@ import org.jetbrains.annotations.NotNull; import org.jetbrains.annotations.Nullable; -import java.util.Objects; - public interface Resolver { /** resolve a symbol by its qualified name in the whole library */ static @NotNull Option<@NotNull TyckDef> resolveDef( @@ -45,9 +44,9 @@ public interface Resolver { ) { var program = source.program().get(); if (program == null) return SeqView.empty(); - var collect = MutableList.>create(); - program.view().forEach(new XYResolver(xy, collect)); - return collect.view().mapNotNull(pos -> switch (pos.data()) { + var collect = new XYResolver(xy, MutableList.create()); + program.view().forEach(collect); + return collect.collect.view().mapNotNull(pos -> switch (pos.data()) { case DefVar defVar -> new WithPos<>(pos.sourcePos(), defVar); case LocalVar localVar -> new WithPos<>(pos.sourcePos(), localVar); case ModuleVar moduleVar -> new WithPos<>(pos.sourcePos(), moduleVar); @@ -65,17 +64,18 @@ public interface Resolver { private static @NotNull SeqView withChildren(@NotNull TyckDef def) { return switch (def) { - case DataDef data -> SeqView.of(data).appendedAll(data.body); - // case ClassDef struct -> SeqView.of(struct).appendedAll(struct.members); + case DataDef data -> SeqView.of(data).appendedAll(data.body()); + case ClassDef struct -> SeqView.of(struct).appendedAll(struct.members()); default -> SeqView.of(def); }; } static @NotNull SeqView> withChildren(@NotNull Decl def) { return switch (def) { - case DataDecl data -> SeqView.>of(data.ref).appendedAll(data.body.clauses.map(DataCon::ref)); - // case ClassDecl struct -> - // SeqView.>of(struct.ref).appendedAll(struct.members.map(TeleDecl.ClassMember::ref)); + case DataDecl data -> SeqView.>of(data.ref) + .appendedAll(data.body.clauses.map(DataCon::ref)); + case ClassDecl struct -> SeqView.>of(struct.ref) + .appendedAll(struct.members.map(ClassMember::ref)); default -> SeqView.of(def.ref()); }; } @@ -110,12 +110,12 @@ public interface Resolver { * @author ice1000, kiva, wsx */ record XYResolver(XY xy, MutableList> collect) implements StmtVisitor { - @Override - public void visitVar(@NotNull SourcePos pos, @NotNull AnyVar var, @NotNull LazyValue<@Nullable Term> type) { + @Override public void + visitVar(@NotNull SourcePos pos, @NotNull AnyVar var, @NotNull LazyValue<@Nullable Term> type) { if (xy.inside(pos)) collect.append(new WithPos<>(pos, var)); } - @Override - public void visitVarDecl(@NotNull SourcePos pos, @NotNull AnyVar var, @NotNull LazyValue<@Nullable Term> type) { + @Override public void + visitVarDecl(@NotNull SourcePos pos, @NotNull AnyVar var, @NotNull LazyValue<@Nullable Term> type) { if (var instanceof LocalVar v && v.isGenerated()) return; StmtVisitor.super.visitVarDecl(pos, var, type); } diff --git a/jit-compiler/src/main/java/org/aya/compiler/serializers/DataSerializer.java b/jit-compiler/src/main/java/org/aya/compiler/serializers/DataSerializer.java index 55cd54ff4a..91ad047f65 100644 --- a/jit-compiler/src/main/java/org/aya/compiler/serializers/DataSerializer.java +++ b/jit-compiler/src/main/java/org/aya/compiler/serializers/DataSerializer.java @@ -1,7 +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.compiler.serializers; +import java.lang.constant.ClassDesc; +import java.lang.constant.ConstantDescs; + import kala.collection.immutable.ImmutableMap; import kala.collection.immutable.ImmutableSeq; import kala.tuple.Tuple; @@ -16,9 +19,6 @@ import org.aya.syntax.ref.DefVar; import org.jetbrains.annotations.NotNull; -import java.lang.constant.ClassDesc; -import java.lang.constant.ConstantDescs; - // You should compile this with its constructors public final class DataSerializer extends JitTeleSerializer { private final @NotNull ShapeFactory shapeFactory; @@ -60,7 +60,7 @@ protected CodeShape.GlobalId[] buildRecognition(DataDef unit) { // The capture is one-to-one var flipped = ImmutableMap.from(recog.captures().view() .map((k, v) -> Tuple., CodeShape.GlobalId>of(((TyckAnyDef) v).ref, k))); - var capture = unit.body.map(x -> flipped.get(x.ref)); + var capture = unit.body().map(x -> flipped.get(x.ref)); return capture.toArray(CodeShape.GlobalId.class); } @@ -71,7 +71,7 @@ protected CodeShape.GlobalId[] buildRecognition(DataDef unit) { @Override protected @NotNull ImmutableSeq superConArgs(@NotNull FreeCodeBuilder builder, DataDef unit) { - return super.superConArgs(builder, unit).appended(builder.iconst(unit.body.size())); + return super.superConArgs(builder, unit).appended(builder.iconst(unit.body().size())); } /** @@ -81,13 +81,13 @@ private void buildConstructors(@NotNull FreeCodeBuilder builder, DataDef unit) { var cons = Constants.JITDATA_CONS; var consRef = builder.refField(cons, builder.thisRef()); - if (unit.body.isEmpty()) { + if (unit.body().isEmpty()) { builder.returnWith(consRef); return; } builder.ifNull(builder.getArray(consRef, 0), cb -> { - unit.body.forEachIndexed((idx, con) -> { + unit.body().forEachIndexed((idx, con) -> { cb.updateArray(consRef, idx, AbstractExprializer.getInstance(builder, con)); }); }, null); diff --git a/jit-compiler/src/main/java/org/aya/compiler/serializers/ModuleSerializer.java b/jit-compiler/src/main/java/org/aya/compiler/serializers/ModuleSerializer.java index 5d6f323a51..b46c28e011 100644 --- a/jit-compiler/src/main/java/org/aya/compiler/serializers/ModuleSerializer.java +++ b/jit-compiler/src/main/java/org/aya/compiler/serializers/ModuleSerializer.java @@ -2,6 +2,10 @@ // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file. package org.aya.compiler.serializers; +import java.lang.constant.ClassDesc; + +import static org.aya.compiler.serializers.NameSerializer.getReference; + import kala.collection.immutable.ImmutableSeq; import kala.collection.mutable.MutableList; import org.aya.compiler.free.FreeClassBuilder; @@ -19,10 +23,6 @@ import org.jetbrains.annotations.NotNull; import org.jetbrains.annotations.VisibleForTesting; -import java.lang.constant.ClassDesc; - -import static org.aya.compiler.serializers.NameSerializer.getReference; - /** * Serializing a module, note that it may not a file module, so we need not to make importing. */ @@ -49,7 +49,7 @@ public ModuleSerializer(@NotNull ShapeFactory shapeFactory) { private void serializeCons(@NotNull FreeClassBuilder builder, @NotNull DataDef dataDef) { var ser = new ConSerializer(recorder); - dataDef.body.forEach(con -> ser.serialize(builder, con)); + dataDef.body().forEach(con -> ser.serialize(builder, con)); } private void serializeMems(@NotNull FreeClassBuilder builder, @NotNull ClassDef classDef) { diff --git a/syntax/src/main/java/org/aya/syntax/core/def/DataDef.java b/syntax/src/main/java/org/aya/syntax/core/def/DataDef.java index 87536dfe28..f680eef724 100644 --- a/syntax/src/main/java/org/aya/syntax/core/def/DataDef.java +++ b/syntax/src/main/java/org/aya/syntax/core/def/DataDef.java @@ -13,18 +13,13 @@ * * @author kiva */ -public final class DataDef implements TopLevelDef { - public final @NotNull DefVar ref; - public final @NotNull ImmutableSeq body; - - public DataDef(@NotNull DefVar ref, @NotNull ImmutableSeq body) { - ref.initialize(this); - this.ref = ref; - this.body = body; - } +public record DataDef( + @Override @NotNull DefVar ref, + @NotNull ImmutableSeq body +) implements TopLevelDef { + public DataDef { ref.initialize(this); } @Override public @NotNull SortTerm result() { return (SortTerm) TopLevelDef.super.result(); } - public @NotNull DefVar ref() { return ref; } public static final class Delegate extends TyckAnyDef implements DataDefLike { public Delegate(@NotNull DefVar ref) { super(ref); } diff --git a/syntax/src/main/java/org/aya/syntax/core/def/TyckAnyDef.java b/syntax/src/main/java/org/aya/syntax/core/def/TyckAnyDef.java index 2ba47cd064..c1990dc15c 100644 --- a/syntax/src/main/java/org/aya/syntax/core/def/TyckAnyDef.java +++ b/syntax/src/main/java/org/aya/syntax/core/def/TyckAnyDef.java @@ -1,7 +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.def; +import java.util.Objects; + import org.aya.syntax.ref.DefVar; import org.aya.syntax.ref.ModulePath; import org.aya.syntax.ref.QName; @@ -11,8 +13,6 @@ import org.jetbrains.annotations.Nullable; import org.jetbrains.annotations.UnknownNullability; -import java.util.Objects; - public non-sealed class TyckAnyDef implements AnyDef { public final @NotNull DefVar ref; public @UnknownNullability Interface core() { return ref.core; } @@ -30,7 +30,7 @@ public non-sealed class TyckAnyDef implements AnyDef public static TyckAnyDef make(TyckDef core) { return switch (core) { - case DataDef data -> new DataDef.Delegate(data.ref); + case DataDef data -> new DataDef.Delegate(data.ref()); case FnDef fn -> new FnDef.Delegate(fn.ref()); case PrimDef prim -> new PrimDef.Delegate(prim.ref); case ConDef con -> new ConDef.Delegate(con.ref); From f7e147171ffe1c16d51037c35dc8ca367ce0d427 Mon Sep 17 00:00:00 2001 From: ice1000 Date: Tue, 28 Jan 2025 10:48:13 -0500 Subject: [PATCH 3/3] chore: make `PrimDef` a record --- .../java/org/aya/primitive/PrimFactory.java | 18 ++++---- .../main/java/org/aya/tyck/StmtTycker.java | 2 +- .../org/aya/cli/library/LibraryCompiler.java | 12 ++--- .../compiler/serializers/PrimSerializer.java | 8 ++-- .../java/org/aya/syntax/core/def/PrimDef.java | 46 +++++++------------ .../org/aya/syntax/core/def/TyckAnyDef.java | 2 +- 6 files changed, 37 insertions(+), 51 deletions(-) diff --git a/base/src/main/java/org/aya/primitive/PrimFactory.java b/base/src/main/java/org/aya/primitive/PrimFactory.java index 650847da18..30cd9b6ba2 100644 --- a/base/src/main/java/org/aya/primitive/PrimFactory.java +++ b/base/src/main/java/org/aya/primitive/PrimFactory.java @@ -1,7 +1,14 @@ -// 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.primitive; +import java.util.EnumMap; +import java.util.function.BiFunction; +import java.util.function.Function; + +import static org.aya.syntax.core.def.PrimDef.*; +import static org.aya.syntax.core.term.SortTerm.Type0; + import kala.collection.Map; import kala.collection.immutable.ImmutableMap; import kala.collection.immutable.ImmutableSeq; @@ -26,13 +33,6 @@ import org.aya.util.ForLSP; import org.jetbrains.annotations.NotNull; -import java.util.EnumMap; -import java.util.function.BiFunction; -import java.util.function.Function; - -import static org.aya.syntax.core.def.PrimDef.*; -import static org.aya.syntax.core.term.SortTerm.Type0; - public class PrimFactory { private final @NotNull Map<@NotNull ID, @NotNull PrimSeed> seeds; private final @NotNull EnumMap<@NotNull ID, @NotNull PrimDefLike> defs = new EnumMap<>(ID.class); @@ -166,7 +166,7 @@ public record PrimSeed( ImmutableSeq.empty()); public @NotNull PrimDefLike factory(@NotNull ID name, @NotNull DefVar ref) { - var rst = new PrimDef.Delegate(seeds.get(name).supply(ref).ref); + var rst = new PrimDef.Delegate(seeds.get(name).supply(ref).ref()); definePrim(rst); return rst; } diff --git a/base/src/main/java/org/aya/tyck/StmtTycker.java b/base/src/main/java/org/aya/tyck/StmtTycker.java index 2bf208ab6b..3312c1554c 100644 --- a/base/src/main/java/org/aya/tyck/StmtTycker.java +++ b/base/src/main/java/org/aya/tyck/StmtTycker.java @@ -383,7 +383,7 @@ private void checkPrim(@NotNull ExprTycker tycker, PrimDecl prim) { tycker.unifyTermReported( DepTypeTerm.makePi(tele.params().view().map(Param::type), tele.result()), // No checks, slightly faster than TeleDef.defType - DepTypeTerm.makePi(core.telescope.view().map(Param::type), core.result), + DepTypeTerm.makePi(core.telescope().view().map(Param::type), core.result()), null, prim.entireSourcePos(), msg -> new PrimError.BadSignature(prim, msg, new UnifyInfo(tycker.state))); var zonker = new Finalizer.Zonk<>(tycker); diff --git a/cli-impl/src/main/java/org/aya/cli/library/LibraryCompiler.java b/cli-impl/src/main/java/org/aya/cli/library/LibraryCompiler.java index 71b311326d..f8b4ab47d5 100644 --- a/cli-impl/src/main/java/org/aya/cli/library/LibraryCompiler.java +++ b/cli-impl/src/main/java/org/aya/cli/library/LibraryCompiler.java @@ -1,7 +1,11 @@ -// 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.cli.library; +import java.io.IOException; +import java.nio.file.Files; +import java.nio.file.Path; + import kala.collection.immutable.ImmutableSeq; import kala.collection.mutable.MutableSet; import org.aya.cli.library.incremental.CompilerAdvisor; @@ -36,10 +40,6 @@ import org.jetbrains.annotations.NotNull; import org.jetbrains.annotations.Nullable; -import java.io.IOException; -import java.nio.file.Files; -import java.nio.file.Path; - /** * @author kiva */ @@ -337,7 +337,7 @@ static void clear(@NotNull PrimFactory factory, @NotNull ImmutableSeq stmt static void clear(@NotNull PrimFactory factory, @NotNull Stmt stmt) { switch (stmt) { case Command.Module mod -> clear(factory, mod.contents()); - case PrimDecl decl when decl.ref.core != null -> factory.clear(decl.ref.core.id); + case PrimDecl decl when decl.ref.core != null -> factory.clear(decl.ref.core.id()); default -> { } } } diff --git a/jit-compiler/src/main/java/org/aya/compiler/serializers/PrimSerializer.java b/jit-compiler/src/main/java/org/aya/compiler/serializers/PrimSerializer.java index 35c9936c52..2a64a0900a 100644 --- a/jit-compiler/src/main/java/org/aya/compiler/serializers/PrimSerializer.java +++ b/jit-compiler/src/main/java/org/aya/compiler/serializers/PrimSerializer.java @@ -1,7 +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.compiler.serializers; +import java.lang.constant.ClassDesc; + import kala.collection.immutable.ImmutableSeq; import org.aya.compiler.free.FreeClassBuilder; import org.aya.compiler.free.FreeCodeBuilder; @@ -12,8 +14,6 @@ import org.aya.syntax.core.term.call.PrimCall; import org.jetbrains.annotations.NotNull; -import java.lang.constant.ClassDesc; - public final class PrimSerializer extends JitTeleSerializer { public PrimSerializer(ModuleSerializer.@NotNull MatchyRecorder recorder) { super(JitPrim.class, recorder); @@ -26,7 +26,7 @@ public PrimSerializer(ModuleSerializer.@NotNull MatchyRecorder recorder) { @Override protected @NotNull ImmutableSeq superConArgs(@NotNull FreeCodeBuilder builder, PrimDef unit) { - return super.superConArgs(builder, unit).appended(builder.refEnum(unit.id)); + return super.superConArgs(builder, unit).appended(builder.refEnum(unit.id())); } @Override public @NotNull PrimSerializer serialize(@NotNull FreeClassBuilder builder, PrimDef unit) { diff --git a/syntax/src/main/java/org/aya/syntax/core/def/PrimDef.java b/syntax/src/main/java/org/aya/syntax/core/def/PrimDef.java index 5b2f509f44..010e0fd221 100644 --- a/syntax/src/main/java/org/aya/syntax/core/def/PrimDef.java +++ b/syntax/src/main/java/org/aya/syntax/core/def/PrimDef.java @@ -1,13 +1,17 @@ -// 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; +import java.util.Objects; + +import static org.aya.syntax.core.term.SortTerm.Type0; + import kala.collection.immutable.ImmutableSeq; +import org.aya.generic.term.DTKind; import org.aya.syntax.concrete.stmt.decl.PrimDecl; import org.aya.syntax.core.Closure; -import org.aya.generic.term.DTKind; -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.core.term.xtt.DimTyTerm; import org.aya.syntax.ref.DefVar; @@ -15,28 +19,12 @@ import org.jetbrains.annotations.NotNull; import org.jetbrains.annotations.Nullable; -import java.util.Objects; - -import static org.aya.syntax.core.term.SortTerm.Type0; - -public final class PrimDef implements TopLevelDef { - public final @NotNull ImmutableSeq telescope; - public final @NotNull Term result; - public final @NotNull DefVar<@NotNull PrimDef, @NotNull PrimDecl> ref; - public final @NotNull ID id; - - public PrimDef( - @NotNull DefVar<@NotNull PrimDef, @NotNull PrimDecl> ref, - @NotNull ImmutableSeq telescope, - @NotNull Term result, @NotNull ID id - ) { - this.telescope = telescope; - this.result = result; - this.ref = ref; - this.id = id; - ref.initialize(this); - } - +public record PrimDef( + @Override @NotNull DefVar<@NotNull PrimDef, @NotNull PrimDecl> ref, + @NotNull ImmutableSeq telescope, + @NotNull Term result, PrimDef.@NotNull ID id +) implements TopLevelDef { + public PrimDef { ref.initialize(this); } public PrimDef(@NotNull DefVar<@NotNull PrimDef, @NotNull PrimDecl> ref, @NotNull Term result, @NotNull ID name) { this(ref, ImmutableSeq.empty(), result, name); } @@ -54,10 +42,10 @@ public PrimDef(@NotNull DefVar<@NotNull PrimDef, @NotNull PrimDecl> ref, @NotNul return result; } - /** I -> Type */ + /// `I -> Type` public static final @NotNull Term intervalToType = new DepTypeTerm(DTKind.Pi, DimTyTerm.INSTANCE, Closure.mkConst(Type0)); - /** Let A be argument, then A i -> A j. Handles index shifting. */ + /// Let `A` be argument, then `A i -> A j`. Handles index shifting. public static @NotNull DepTypeTerm familyI2J(Closure term, Term i, Term j) { return new DepTypeTerm(DTKind.Pi, term.apply(i), Closure.mkConst(term.apply(j))); } @@ -68,7 +56,7 @@ public enum ID { I("I"), PATH("Path"), COE("coe"), - HCOMP("hcomp"); + HCOMP("hcom"); public final @NotNull @NonNls String id; @@ -84,8 +72,6 @@ public enum ID { ID(@NotNull String id) { this.id = id; } } - public @NotNull DefVar<@NotNull PrimDef, @NotNull PrimDecl> ref() { return ref; } - public static final class Delegate extends TyckAnyDef implements PrimDefLike { public Delegate(@NotNull DefVar ref) { super(ref); } @Override public @NotNull PrimDef.ID id() { return core().id; } diff --git a/syntax/src/main/java/org/aya/syntax/core/def/TyckAnyDef.java b/syntax/src/main/java/org/aya/syntax/core/def/TyckAnyDef.java index c1990dc15c..80fd10e360 100644 --- a/syntax/src/main/java/org/aya/syntax/core/def/TyckAnyDef.java +++ b/syntax/src/main/java/org/aya/syntax/core/def/TyckAnyDef.java @@ -32,7 +32,7 @@ public static TyckAnyDef make(TyckDef core) { return switch (core) { case DataDef data -> new DataDef.Delegate(data.ref()); case FnDef fn -> new FnDef.Delegate(fn.ref()); - case PrimDef prim -> new PrimDef.Delegate(prim.ref); + case PrimDef prim -> new PrimDef.Delegate(prim.ref()); case ConDef con -> new ConDef.Delegate(con.ref); case ClassDef classDef -> new ClassDef.Delegate(classDef.ref()); case MemberDef memberDef -> new MemberDef.Delegate(memberDef.ref());