merge: Turn some classes into records (#1292)

Including `DataDef` and `PrimDef`. Also some comments-related changes.

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<PrimDef, PrimDecl> 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;
   }

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)));
   }
 

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<LocalVar> collect(@NotNull MutableList<LocalVar> 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<LocalVar> collect(@NotNull MutableList<LocalVar> container)
   }
 
   class ResolvingInterruptedException extends InterruptException {
-    @Override public InterruptStage stage() {
-      return InterruptStage.Resolving;
-    }
+    @Override public InterruptStage stage() { return InterruptStage.Resolving; }
   }
 }

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);

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

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> 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 -> { }
       }
     }

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.<WithPos<AnyVar>>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<TyckDef> withChildren(@NotNull TyckDef def) {
     return switch (def) {
-      case DataDef data -> SeqView.<TyckDef>of(data).appendedAll(data.body);
-      // case ClassDef struct -> SeqView.<Def>of(struct).appendedAll(struct.members);
+      case DataDef data -> SeqView.<TyckDef>of(data).appendedAll(data.body());
+      case ClassDef struct -> SeqView.<TyckDef>of(struct).appendedAll(struct.members());
       default -> SeqView.of(def);
     };
   }
 
   static @NotNull SeqView<DefVar<?, ?>> withChildren(@NotNull Decl def) {
     return switch (def) {
-      case DataDecl data -> SeqView.<DefVar<?, ?>>of(data.ref).appendedAll(data.body.clauses.map(DataCon::ref));
-      // case ClassDecl struct ->
-      //   SeqView.<DefVar<?, ?>>of(struct.ref).appendedAll(struct.members.map(TeleDecl.ClassMember::ref));
+      case DataDecl data -> SeqView.<DefVar<?, ?>>of(data.ref)
+        .appendedAll(data.body.clauses.map(DataCon::ref));
+      case ClassDecl struct -> SeqView.<DefVar<?, ?>>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<WithPos<AnyVar>> 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);
     }

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<DataDef> {
   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.<DefVar<?, ?>, 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<FreeJavaExpr> 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);

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) {

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<PrimDef> {
   public PrimSerializer(ModuleSerializer.@NotNull MatchyRecorder recorder) {
     super(JitPrim.class, recorder);
@@ -26,7 +26,7 @@ public PrimSerializer(ModuleSerializer.@NotNull MatchyRecorder recorder) {
 
   @Override
   protected @NotNull ImmutableSeq<FreeJavaExpr> 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) {