From 4c8d5b9baef5a6796271950974ccc4bc5a484fdf Mon Sep 17 00:00:00 2001
From: HoshinoTented <hoshinotented@qq.com>
Date: Tue, 21 Jan 2025 18:43:12 +0800
Subject: [PATCH 01/16] pretty: abstraction

---
 .../java/org/aya/cli/repl/ReplCommands.java   |   8 +-
 .../java/org/aya/prettier/CorePrettier.java   | 199 ++++++++++++------
 .../main/java/org/aya/prettier/Tokens.java    |   6 +-
 .../java/org/aya/syntax/compile/JitData.java  |   4 +-
 .../java/org/aya/syntax/compile/JitFn.java    |  16 +-
 .../java/org/aya/syntax/compile/JitUnit.java  |   4 +-
 .../java/org/aya/syntax/core/RichParam.java   |   4 +-
 .../java/org/aya/syntax/core/def/DataDef.java |   4 +-
 .../org/aya/syntax/core/def/DataDefLike.java  |   4 +-
 9 files changed, 175 insertions(+), 74 deletions(-)

diff --git a/cli-console/src/main/java/org/aya/cli/repl/ReplCommands.java b/cli-console/src/main/java/org/aya/cli/repl/ReplCommands.java
index af5b39bfd1..1ac23840e1 100644
--- a/cli-console/src/main/java/org/aya/cli/repl/ReplCommands.java
+++ b/cli-console/src/main/java/org/aya/cli/repl/ReplCommands.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.cli.repl;
 
@@ -13,6 +13,7 @@
 import org.aya.repl.Command;
 import org.aya.repl.CommandArg;
 import org.aya.repl.ReplUtil;
+import org.aya.syntax.compile.JitDef;
 import org.aya.syntax.core.def.AnyDef;
 import org.aya.syntax.core.def.ConDefLike;
 import org.aya.syntax.core.def.MemberDefLike;
@@ -65,9 +66,14 @@ record StyleParam(@NotNull Either<RenderOptions.StyleFamilyName, Path> value)
         default -> {
         }
       }
+
       if (topLevel instanceof TyckAnyDef<?> tyckDef) {
         return new Command.Result(Output.stdout(repl.render(tyckDef.core())), true);
       }
+
+      if (topLevel instanceof JitDef jitDef) {
+      }
+
       return Command.Result.ok(topLevel.name(), true);      // TODO: pretty print
     }
   };
diff --git a/syntax/src/main/java/org/aya/prettier/CorePrettier.java b/syntax/src/main/java/org/aya/prettier/CorePrettier.java
index a25f46a1eb..3348524258 100644
--- a/syntax/src/main/java/org/aya/prettier/CorePrettier.java
+++ b/syntax/src/main/java/org/aya/prettier/CorePrettier.java
@@ -6,13 +6,15 @@
 import kala.collection.SeqLike;
 import kala.collection.SeqView;
 import kala.collection.immutable.ImmutableSeq;
+import kala.collection.mutable.FreezableMutableList;
 import kala.collection.mutable.MutableList;
 import org.aya.generic.AyaDocile;
+import org.aya.generic.Modifier;
 import org.aya.generic.Renamer;
 import org.aya.generic.term.DTKind;
 import org.aya.generic.term.ParamLike;
 import org.aya.pretty.doc.Doc;
-import org.aya.syntax.compile.JitMatchy;
+import org.aya.syntax.compile.*;
 import org.aya.syntax.concrete.stmt.decl.DataCon;
 import org.aya.syntax.core.RichParam;
 import org.aya.syntax.core.def.*;
@@ -25,9 +27,11 @@
 import org.aya.syntax.core.term.repr.MetaLitTerm;
 import org.aya.syntax.core.term.repr.StringTerm;
 import org.aya.syntax.core.term.xtt.*;
+import org.aya.syntax.ref.CompiledVar;
 import org.aya.syntax.ref.DefVar;
 import org.aya.syntax.ref.GenerateKind.Basic;
 import org.aya.syntax.ref.LocalVar;
+import org.aya.syntax.telescope.AbstractTele;
 import org.aya.util.Arg;
 import org.aya.util.error.SourcePos;
 import org.aya.util.error.WithPos;
@@ -35,6 +39,8 @@
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
+import java.util.EnumSet;
+import java.util.function.BiFunction;
 import java.util.function.Function;
 import java.util.function.UnaryOperator;
 
@@ -271,99 +277,152 @@ private ImmutableSeq<Term> visibleArgsOf(Callable call) {
     return switch (predef) {
       case PrimDef def -> primDoc(def.ref());
       case FnDef def -> {
-        var line1 = MutableList.of(KW_DEF);
-        def.modifiers().forEach(m -> line1.append(Doc.styled(KEYWORD, m.keyword)));
-        var tele = enrich(def.telescope());
-        var subst = tele.view().<Term>map(p -> new FreeTerm(p.ref()));
-        line1.appendAll(new Doc[]{
-          defVar(def.ref()),
-          visitTele(tele),
-          HAS_TYPE,
-          term(Outer.Free, def.result().instTeleVar(tele.view().map(ParamLike::ref)))
-        });
-        var line1sep = Doc.sepNonEmpty(line1);
-        yield def.body().fold(
-          term -> Doc.sep(line1sep, FN_DEFINED_AS, term(Outer.Free, term.instTele(subst))),
-          clauses -> Doc.vcat(line1sep,
-            Doc.nest(2, visitClauses(clauses.view().map(WithPos::data), tele.view().map(ParamLike::explicit)))));
+        var absTele = TyckDef.defSignature(def);
+        yield visitFn(defVar(def.ref()), def.modifiers(), absTele,
+          (prefix, subst) -> def.body().fold(
+            term -> Doc.sep(prefix, FN_DEFINED_AS, term(Outer.Free, term.instTele(subst.view()))),
+            clauses -> Doc.vcat(prefix,
+              Doc.nest(2, visitClauses(clauses.view().map(WithPos::data), def.telescope().view().map(Param::explicit))))));
       }
       case MemberDef field -> Doc.sepNonEmpty(Doc.symbol("|"),
         defVar(field.ref()),
         visitTele(enrich(field.telescope())),
         Doc.symbol(":"),
         term(Outer.Free, field.result()));
-      case ConDef con -> {
-        var doc = Doc.sepNonEmpty(coe(con.coerce),
-          defVar(con.ref()),
-          visitTele(enrich(con.selfTele)));
-        if (con.pats.isNotEmpty()) {
-          var pats = Doc.commaList(con.pats.view().map(pat -> pat(pat, true, Outer.Free)));
-          yield Doc.sep(Doc.symbol("|"), pats, Doc.symbol("=>"), doc);
-        } else {
-          yield Doc.sep(BAR, doc);
-        }
-      }
+      case ConDef con -> visitCon(con.ref, con.coerce, con.selfTele);
       case ClassDef def -> Doc.vcat(Doc.sepNonEmpty(KW_CLASS,
         defVar(def.ref()),
         Doc.nest(2, Doc.vcat(def.members().view().map(this::def)))));
-      case DataDef def -> {
-        var richDataTele = enrich(def.telescope());
-        var dataArgs = richDataTele.view().<Term>map(t -> new FreeTerm(t.ref()));
-
-        var line1 = MutableList.of(KW_DATA,
-          defVar(def.ref()),
-          visitTele(richDataTele),
-          HAS_TYPE,
-          term(Outer.Free, def.result()));
-        var cons = def.body.view().map(con ->
-          // we need to instantiate the tele of con, but we can't modify the CtorDef
-          visitCon(con.ref, enrich(con.selfTele.mapIndexed((i, p) -> {
-            // i: nth param
-            // p: the param
-            // instantiate reference to data tele
-            return p.descent(t -> t.instTeleFrom(i, dataArgs));
-          })), con.coerce));
-
-        yield Doc.vcat(Doc.sepNonEmpty(line1),
-          Doc.nest(2, Doc.vcat(cons)));
+      case DataDef def -> visitData(defVar(def.ref()), TyckDef.defSignature(def), dataLine -> {
+        var consDoc = def.body.view().map(this::def);
+        return Doc.vcat(dataLine, Doc.nest(2, Doc.vcat(consDoc)));
+      });
+    };
+  }
+
+  public @NotNull Doc def(@NotNull JitDef unit) {
+    var dummyVar = new CompiledVar(unit);
+
+    return switch (unit) {
+      case JitFn jitFn -> visitFn(defVar(dummyVar), jitFn.modifiers(), jitFn, (prefix, _) ->
+        Doc.sep(prefix, FN_DEFINED_AS, COMMENT_COMPILED_CODE));
+      case JitCon jitCon -> {
+        var dummyOwnerArgs = ImmutableSeq.<Term>fill(jitCon.ownerTeleSize(), i -> new FreeTerm(jitCon.telescopeName(i)));
+        var rhs = visitConRhs(defVar(dummyVar), true && false, jitCon.inst(dummyOwnerArgs));
+        yield Doc.sep(BAR, COMMENT_COMPILED_PATTERN, FN_DEFINED_AS, rhs);
       }
+      case JitData jitData -> visitData(defVar(dummyVar), jitData, dataLine -> {
+        var consDoc = jitData.body().view().map(this::def);
+        return Doc.vcat(dataLine, Doc.nest(2, Doc.vcat(consDoc)));
+      });
+      case JitClass jiClasst -> null;
+      case JitMember jitMember -> null;
+      case JitPrim jitPrim -> null;
     };
   }
 
+  private @NotNull Doc visitFn(
+    @NotNull Doc name,
+    @NotNull EnumSet<Modifier> modifiers,
+    @NotNull AbstractTele telescope,
+    @NotNull BiFunction<Doc, ImmutableSeq<Term>, Doc> cont
+  ) {
+    var line1 = MutableList.of(KW_DEF);
+    modifiers.forEach(m -> line1.append(Doc.styled(KEYWORD, m.keyword)));
+    line1.append(name);
+
+    var tele = enrich(telescope);
+    line1.append(visitTele(tele));
+
+    line1.append(HAS_TYPE);
+
+    var subst = tele.<Term>map(x -> new FreeTerm(x.ref()));
+    line1.append(term(Outer.Free, telescope.result(subst)));
+
+    var line1Doc = Doc.sepNonEmpty(line1);
+    return cont.apply(line1Doc, subst);
+  }
+
+  /// @param selfTele self tele of the constructor, unlike [JitCon], the data args/owner args should be supplied.
+  private @NotNull Doc visitConRhs(
+    @NotNull Doc name,
+    boolean coerce,
+    @NotNull AbstractTele selfTele
+  ) {
+    return Doc.sepNonEmpty(coe(coerce), name, visitTele(enrich(selfTele)));
+  }
+
   private @NotNull Doc visitCon(
     @NotNull DefVar<ConDef, DataCon> ref,
-    @NotNull ImmutableSeq<ParamLike<Term>> richSelfTele,
-    boolean coerce
+    boolean coerce,
+    @NotNull ImmutableSeq<Param> rawSelfTele
   ) {
-    var doc = Doc.sepNonEmpty(coe(coerce), defVar(ref), visitTele(richSelfTele));
     var con = ref.core;
-    if (con.pats.isNotEmpty()) {
-      var pats = Doc.commaList(con.pats.view().map(pat -> pat(pat, true, Outer.Free)));
-      return Doc.sep(BAR, pats, FN_DEFINED_AS, doc);
+    var conName = defVar(ref);
+    var pats = con.pats;
+
+    if (pats.isNotEmpty()) {
+      var dataSig = con.dataRef.signature();
+      var licits = ImmutableSeq.fill(dataSig.telescopeSize(), dataSig::telescopeLicit).view();
+      return visitClause(pats, licits, ownerArgs -> {
+        var realSelfTele = Param.instTele(rawSelfTele.view(), ownerArgs).toImmutableSeq();
+        return visitConRhs(conName, coerce, new AbstractTele.Locns(realSelfTele, ErrorTerm.DUMMY));
+      });
     } else {
-      return Doc.sep(BAR, doc);
+      var ownerArgs = con.ownerTele.<Term>map(Param::toFreshTerm);
+      var realSelfTele = Param.instTele(rawSelfTele.view(), ownerArgs.view()).toImmutableSeq();
+      return Doc.sep(BAR, visitConRhs(conName, coerce, new AbstractTele.Locns(realSelfTele, ErrorTerm.DUMMY)));
     }
   }
 
-  public @NotNull Doc visitClauseLhs(@NotNull SeqView<Boolean> licits, @NotNull Term.Matching clause) {
-    var enrichPats = clause.patterns().zip(licits,
-      (pat, licit) -> pat(pat, licit, Outer.Free));
+  private @NotNull Doc visitData(
+    @NotNull Doc name,
+    @NotNull AbstractTele telescope,
+    @NotNull Function<Doc, Doc> cont
+  ) {
+    var richDataTele = enrich(telescope);
+    var dataArgs = richDataTele.<Term>map(t -> new FreeTerm(t.ref()));
+
+    var line1 = Doc.sepNonEmpty(KW_DATA,
+      name,
+      visitTele(richDataTele),
+      HAS_TYPE,
+      term(Outer.Free, telescope.result(dataArgs)));
+
+    return cont.apply(line1);
+  }
+
+  public @NotNull Doc visitClauseLhs(@NotNull ImmutableSeq<Pat> patterns, @NotNull SeqView<Boolean> licits) {
+    var enrichPats = patterns.zip(licits, (pat, licit) -> pat(pat, licit, Outer.Free));
     return Doc.commaList(enrichPats);
   }
 
-  private @NotNull Doc visitClause(@NotNull Term.Matching clause, @NotNull SeqView<Boolean> licits) {
-    var patSubst = Pat.collectRichBindings(clause.patterns().view());
-    var lhsWithoutBar = visitClauseLhs(licits, clause);
-    var rhs = term(Outer.Free, clause.body().instTele(patSubst.view().map(RichParam::toTerm)));
+  private @NotNull Doc visitClause(
+    @NotNull ImmutableSeq<Pat> patterns,
+    @NotNull SeqView<Boolean> licits,
+    @NotNull Function<SeqView<Term>, Doc> bodyCont
+  ) {
+    var patSubst = Pat.collectRichBindings(patterns.view());
+    var lhsWithoutBar = visitClauseLhs(patterns, licits);
+    var subst = patSubst.view().<Term>map(RichParam::toTerm);
+    var rhs = bodyCont.apply(subst);
 
     return Doc.sep(BAR, lhsWithoutBar, FN_DEFINED_AS, rhs);
   }
 
+  private @NotNull Doc visitClause(@NotNull Term.Matching clause, @NotNull SeqView<Boolean> licits) {
+    return visitClause(clause.patterns(), licits, subst -> term(Outer.Free, clause.body().instTele(subst)));
+  }
+
   private @NotNull Doc visitClauses(@NotNull SeqView<Term.Matching> clauses, @NotNull SeqView<Boolean> licits) {
     return Doc.vcat(clauses.map(matching -> visitClause(matching, licits)));
   }
 
   // region Name Generation
+  private @NotNull ImmutableSeq<Term> toTerm(@NotNull ImmutableSeq<ParamLike<Term>> params) {
+    return params.map(x -> new FreeTerm(x.ref()));
+  }
+
   private @NotNull ImmutableSeq<ParamLike<Term>> enrich(@NotNull SeqLike<Param> tele) {
     var richTele = MutableList.<ParamLike<Term>>create();
 
@@ -376,6 +435,24 @@ private ImmutableSeq<Term> visibleArgsOf(Callable call) {
     return richTele.toImmutableSeq();
   }
 
+  private @NotNull ImmutableSeq<ParamLike<Term>> enrich(@NotNull AbstractTele tele) {
+    var richTele = FreezableMutableList.<ParamLike<Term>>create();
+
+    for (var i = 0; i < tele.telescopeSize(); ++i) {
+      var binds = richTele.view()
+        .<Term>map(x -> new FreeTerm(x.ref()))
+        .toImmutableSeq();
+      var type = tele.telescope(i, binds);
+      richTele.append(new RichParam(
+        new LocalVar(tele.telescopeName(i), SourcePos.NONE, Basic.Pretty),
+        type,
+        tele.telescopeLicit(i))
+      );
+    }
+
+    return richTele.toImmutableSeq();
+  }
+
   private @NotNull LocalVar generateName(@Nullable Term whty) {
     return nameGen.bindName(whty);
   }
diff --git a/syntax/src/main/java/org/aya/prettier/Tokens.java b/syntax/src/main/java/org/aya/prettier/Tokens.java
index 0b65f50d70..fb50da422b 100644
--- a/syntax/src/main/java/org/aya/prettier/Tokens.java
+++ b/syntax/src/main/java/org/aya/prettier/Tokens.java
@@ -4,8 +4,7 @@
 
 import org.aya.pretty.doc.Doc;
 
-import static org.aya.prettier.BasePrettier.KEYWORD;
-import static org.aya.prettier.BasePrettier.PRIM;
+import static org.aya.prettier.BasePrettier.*;
 
 public final class Tokens {
 
@@ -52,4 +51,7 @@ private Tokens() {
   public static final Doc KW_IMPORT = Doc.styled(KEYWORD, "import");
   public static final Doc KW_INTERVAL = Doc.styled(PRIM, "I");
   public static final Doc KW_COE = Doc.styled(KEYWORD, "coe");
+
+  public static final Doc COMMENT_COMPILED_CODE = Doc.styled(COMMENT, "/* compiled code */");
+  public static final Doc COMMENT_COMPILED_PATTERN = Doc.styled(COMMENT, "/* compiled pattern */");
 }
diff --git a/syntax/src/main/java/org/aya/syntax/compile/JitData.java b/syntax/src/main/java/org/aya/syntax/compile/JitData.java
index 4d437cc789..a36940d60f 100644
--- a/syntax/src/main/java/org/aya/syntax/compile/JitData.java
+++ b/syntax/src/main/java/org/aya/syntax/compile/JitData.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.compile;
 
@@ -26,7 +26,7 @@ protected JitData(int telescopeSize, boolean[] telescopeLicit, String[] telescop
    * @implNote We should use `constructors()` rather than `constructors`,
    * since `constructors()` will initialize them
    */
-  @Override public @NotNull ImmutableSeq<ConDefLike> body() {
+  @Override public @NotNull ImmutableSeq<JitCon> body() {
     return ImmutableArray.Unsafe.wrap(constructors());
   }
 }
diff --git a/syntax/src/main/java/org/aya/syntax/compile/JitFn.java b/syntax/src/main/java/org/aya/syntax/compile/JitFn.java
index e261d15a4f..e11ded5c37 100644
--- a/syntax/src/main/java/org/aya/syntax/compile/JitFn.java
+++ b/syntax/src/main/java/org/aya/syntax/compile/JitFn.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.compile;
 
@@ -9,6 +9,8 @@
 import org.aya.syntax.telescope.JitTele;
 import org.jetbrains.annotations.NotNull;
 
+import java.util.EnumSet;
+
 public abstract non-sealed class JitFn extends JitTele implements FnDefLike {
   public final int modifiers;
 
@@ -24,4 +26,16 @@ protected JitFn(int telescopeSize, boolean[] telescopeLicit, String[] telescopeN
   @Override public boolean is(@NotNull Modifier mod) {
     return (modifiers & (1 << mod.ordinal())) != 0;
   }
+
+  public @NotNull EnumSet<Modifier> modifiers() {
+    var set = EnumSet.noneOf(Modifier.class);
+
+    for (var modi : Modifier.values()) {
+      if (is(modi)) {
+        set.add(modi);
+      }
+    }
+
+    return set;
+  }
 }
diff --git a/syntax/src/main/java/org/aya/syntax/compile/JitUnit.java b/syntax/src/main/java/org/aya/syntax/compile/JitUnit.java
index fe1705bf3a..b81650422f 100644
--- a/syntax/src/main/java/org/aya/syntax/compile/JitUnit.java
+++ b/syntax/src/main/java/org/aya/syntax/compile/JitUnit.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.compile;
 
@@ -9,7 +9,7 @@
 import org.aya.util.error.Panic;
 import org.jetbrains.annotations.NotNull;
 
-public abstract class JitUnit {
+public abstract sealed class JitUnit permits JitDef, JitMatchy {
   private CompiledAya metadata;
 
   public @NotNull final CompiledAya metadata() {
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 48943b0989..92d72831c3 100644
--- a/syntax/src/main/java/org/aya/syntax/core/RichParam.java
+++ b/syntax/src/main/java/org/aya/syntax/core/RichParam.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;
 
+import kala.collection.SeqView;
+import kala.collection.immutable.ImmutableSeq;
 import org.aya.generic.term.ParamLike;
 import org.aya.syntax.core.term.FreeTerm;
 import org.aya.syntax.core.term.Param;
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 d2e52313f7..87536dfe28 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
@@ -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;
 
@@ -28,7 +28,7 @@ public DataDef(@NotNull DefVar<DataDef, DataDecl> ref, @NotNull ImmutableSeq<Con
 
   public static final class Delegate extends TyckAnyDef<DataDef> implements DataDefLike {
     public Delegate(@NotNull DefVar<DataDef, ?> ref) { super(ref); }
-    @Override public @NotNull ImmutableSeq<ConDefLike>
+    @Override public @NotNull ImmutableSeq<ConDef.Delegate>
     body() { return ref.core.body.map(x -> new ConDef.Delegate(x.ref)); }
   }
 }
diff --git a/syntax/src/main/java/org/aya/syntax/core/def/DataDefLike.java b/syntax/src/main/java/org/aya/syntax/core/def/DataDefLike.java
index 1f7595b965..9456ebe5e1 100644
--- a/syntax/src/main/java/org/aya/syntax/core/def/DataDefLike.java
+++ b/syntax/src/main/java/org/aya/syntax/core/def/DataDefLike.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;
 
@@ -7,5 +7,5 @@
 import org.jetbrains.annotations.NotNull;
 
 public sealed interface DataDefLike extends AnyDef permits JitData, DataDef.Delegate {
-  @NotNull ImmutableSeq<ConDefLike> body();
+  @NotNull ImmutableSeq<? extends ConDefLike> body();
 }

From 6b437237d28072a47506142b0be2963b88ee91b6 Mon Sep 17 00:00:00 2001
From: HoshinoTented <hoshinotented@qq.com>
Date: Wed, 22 Jan 2025 06:33:36 +0800
Subject: [PATCH 02/16] repl: pretty for core

---
 .../java/org/aya/cli/repl/ReplCommands.java   | 19 +++++++------------
 .../java/org/aya/syntax/compile/JitDef.java   | 13 +++++++++++--
 .../java/org/aya/syntax/compile/JitUnit.java  |  4 ++++
 3 files changed, 22 insertions(+), 14 deletions(-)

diff --git a/cli-console/src/main/java/org/aya/cli/repl/ReplCommands.java b/cli-console/src/main/java/org/aya/cli/repl/ReplCommands.java
index 1ac23840e1..6714c05999 100644
--- a/cli-console/src/main/java/org/aya/cli/repl/ReplCommands.java
+++ b/cli-console/src/main/java/org/aya/cli/repl/ReplCommands.java
@@ -8,16 +8,14 @@
 import org.aya.cli.render.RenderOptions;
 import org.aya.prettier.AyaPrettierOptions;
 import org.aya.prettier.BasePrettier;
+import org.aya.prettier.CorePrettier;
 import org.aya.pretty.doc.Doc;
 import org.aya.producer.AyaParserImpl;
 import org.aya.repl.Command;
 import org.aya.repl.CommandArg;
 import org.aya.repl.ReplUtil;
 import org.aya.syntax.compile.JitDef;
-import org.aya.syntax.core.def.AnyDef;
-import org.aya.syntax.core.def.ConDefLike;
-import org.aya.syntax.core.def.MemberDefLike;
-import org.aya.syntax.core.def.TyckAnyDef;
+import org.aya.syntax.core.def.*;
 import org.aya.syntax.literate.CodeOptions;
 import org.aya.syntax.ref.AnyDefVar;
 import org.jetbrains.annotations.NotNull;
@@ -67,14 +65,11 @@ record StyleParam(@NotNull Either<RenderOptions.StyleFamilyName, Path> value)
         }
       }
 
-      if (topLevel instanceof TyckAnyDef<?> tyckDef) {
-        return new Command.Result(Output.stdout(repl.render(tyckDef.core())), true);
-      }
-
-      if (topLevel instanceof JitDef jitDef) {
-      }
-
-      return Command.Result.ok(topLevel.name(), true);      // TODO: pretty print
+      return switch (topLevel) {
+        case JitDef jitDef -> new Result(Output.stdout(repl.render(jitDef)), true);
+        case TyckAnyDef<?> tyckDef -> new Result(Output.stdout(repl.render(tyckDef.core())), true);
+        default -> Result.ok(topLevel.name(), true);
+      };
     }
   };
 
diff --git a/syntax/src/main/java/org/aya/syntax/compile/JitDef.java b/syntax/src/main/java/org/aya/syntax/compile/JitDef.java
index d5543978a5..075f152426 100644
--- a/syntax/src/main/java/org/aya/syntax/compile/JitDef.java
+++ b/syntax/src/main/java/org/aya/syntax/compile/JitDef.java
@@ -1,11 +1,15 @@
-// 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.compile;
 
+import org.aya.generic.AyaDocile;
+import org.aya.prettier.CorePrettier;
+import org.aya.pretty.doc.Doc;
 import org.aya.syntax.core.def.AnyDef;
 import org.aya.syntax.ref.ModulePath;
 import org.aya.syntax.telescope.JitTele;
 import org.aya.util.binop.Assoc;
+import org.aya.util.prettier.PrettierOptions;
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
@@ -14,7 +18,7 @@
  *
  * @implNote every definition should be annotated by {@link CompiledAya}
  */
-public abstract sealed class JitDef extends JitUnit implements AnyDef permits JitClass, JitTele {
+public abstract sealed class JitDef extends JitUnit implements AnyDef, AyaDocile permits JitClass, JitTele {
   @Override public @NotNull ModulePath fileModule() {
     return new ModulePath(module().module().take(metadata().fileModuleSize()));
   }
@@ -32,4 +36,9 @@ public abstract sealed class JitDef extends JitUnit implements AnyDef permits Ji
   }
 
   @Override public abstract @NotNull JitTele signature();
+
+  @Override
+  public @NotNull Doc toDoc(@NotNull PrettierOptions options) {
+    return new CorePrettier(options).def(this);
+  }
 }
diff --git a/syntax/src/main/java/org/aya/syntax/compile/JitUnit.java b/syntax/src/main/java/org/aya/syntax/compile/JitUnit.java
index b81650422f..918c2c00b3 100644
--- a/syntax/src/main/java/org/aya/syntax/compile/JitUnit.java
+++ b/syntax/src/main/java/org/aya/syntax/compile/JitUnit.java
@@ -3,10 +3,14 @@
 package org.aya.syntax.compile;
 
 import kala.collection.immutable.ImmutableArray;
+import org.aya.generic.AyaDocile;
+import org.aya.prettier.CorePrettier;
+import org.aya.pretty.doc.Doc;
 import org.aya.syntax.ref.ModulePath;
 import org.aya.syntax.ref.QName;
 import org.aya.syntax.ref.QPath;
 import org.aya.util.error.Panic;
+import org.aya.util.prettier.PrettierOptions;
 import org.jetbrains.annotations.NotNull;
 
 public abstract sealed class JitUnit permits JitDef, JitMatchy {

From 781e47146419b6912650b71e81cdf936e1a5f968 Mon Sep 17 00:00:00 2001
From: HoshinoTented <hoshinotented@qq.com>
Date: Thu, 23 Jan 2025 14:10:57 +0800
Subject: [PATCH 03/16] pretty: member

---
 .../java/org/aya/prettier/CorePrettier.java   | 22 ++++++++++++++-----
 .../java/org/aya/syntax/compile/JitUnit.java  |  4 ----
 2 files changed, 16 insertions(+), 10 deletions(-)

diff --git a/syntax/src/main/java/org/aya/prettier/CorePrettier.java b/syntax/src/main/java/org/aya/prettier/CorePrettier.java
index 3348524258..90afcee188 100644
--- a/syntax/src/main/java/org/aya/prettier/CorePrettier.java
+++ b/syntax/src/main/java/org/aya/prettier/CorePrettier.java
@@ -284,11 +284,7 @@ yield visitFn(defVar(def.ref()), def.modifiers(), absTele,
             clauses -> Doc.vcat(prefix,
               Doc.nest(2, visitClauses(clauses.view().map(WithPos::data), def.telescope().view().map(Param::explicit))))));
       }
-      case MemberDef field -> Doc.sepNonEmpty(Doc.symbol("|"),
-        defVar(field.ref()),
-        visitTele(enrich(field.telescope())),
-        Doc.symbol(":"),
-        term(Outer.Free, field.result()));
+      case MemberDef field -> visitMember(defVar(field.ref()), TyckDef.defSignature(field));
       case ConDef con -> visitCon(con.ref, con.coerce, con.selfTele);
       case ClassDef def -> Doc.vcat(Doc.sepNonEmpty(KW_CLASS,
         defVar(def.ref()),
@@ -315,8 +311,8 @@ yield visitFn(defVar(def.ref()), def.modifiers(), absTele,
         var consDoc = jitData.body().view().map(this::def);
         return Doc.vcat(dataLine, Doc.nest(2, Doc.vcat(consDoc)));
       });
+      case JitMember jitMember -> visitMember(defVar(dummyVar), jitMember);
       case JitClass jiClasst -> null;
-      case JitMember jitMember -> null;
       case JitPrim jitPrim -> null;
     };
   }
@@ -392,6 +388,20 @@ yield visitFn(defVar(def.ref()), def.modifiers(), absTele,
     return cont.apply(line1);
   }
 
+  /// @param telescope the telescope of a [MemberDefLike], including the `self` parameter
+  private @NotNull Doc visitMember(
+    @NotNull Doc name,
+    @NotNull AbstractTele telescope
+  ) {
+    // TODO: should we pretty print the `self` parameter?
+    //       The use of `self` parameter still appears in other parameters.
+
+    var richTele = enrich(telescope);
+    var binds = richTele.<Term>map(x -> new FreeTerm(x.ref()));
+
+    return Doc.sepNonEmpty(BAR, name, visitTele(richTele), HAS_TYPE, term(Outer.Free, telescope.result(binds)));
+  }
+
   public @NotNull Doc visitClauseLhs(@NotNull ImmutableSeq<Pat> patterns, @NotNull SeqView<Boolean> licits) {
     var enrichPats = patterns.zip(licits, (pat, licit) -> pat(pat, licit, Outer.Free));
     return Doc.commaList(enrichPats);
diff --git a/syntax/src/main/java/org/aya/syntax/compile/JitUnit.java b/syntax/src/main/java/org/aya/syntax/compile/JitUnit.java
index 918c2c00b3..b81650422f 100644
--- a/syntax/src/main/java/org/aya/syntax/compile/JitUnit.java
+++ b/syntax/src/main/java/org/aya/syntax/compile/JitUnit.java
@@ -3,14 +3,10 @@
 package org.aya.syntax.compile;
 
 import kala.collection.immutable.ImmutableArray;
-import org.aya.generic.AyaDocile;
-import org.aya.prettier.CorePrettier;
-import org.aya.pretty.doc.Doc;
 import org.aya.syntax.ref.ModulePath;
 import org.aya.syntax.ref.QName;
 import org.aya.syntax.ref.QPath;
 import org.aya.util.error.Panic;
-import org.aya.util.prettier.PrettierOptions;
 import org.jetbrains.annotations.NotNull;
 
 public abstract sealed class JitUnit permits JitDef, JitMatchy {

From 7100bcbd67dff2a39c05e965d42b5bf708c93c88 Mon Sep 17 00:00:00 2001
From: HoshinoTented <hoshinotented@qq.com>
Date: Thu, 23 Jan 2025 15:38:20 +0800
Subject: [PATCH 04/16] pretty: remove unused

---
 .../java/org/aya/prettier/CorePrettier.java   | 35 ++++++++-----------
 1 file changed, 15 insertions(+), 20 deletions(-)

diff --git a/syntax/src/main/java/org/aya/prettier/CorePrettier.java b/syntax/src/main/java/org/aya/prettier/CorePrettier.java
index 90afcee188..03d3de37d7 100644
--- a/syntax/src/main/java/org/aya/prettier/CorePrettier.java
+++ b/syntax/src/main/java/org/aya/prettier/CorePrettier.java
@@ -8,6 +8,7 @@
 import kala.collection.immutable.ImmutableSeq;
 import kala.collection.mutable.FreezableMutableList;
 import kala.collection.mutable.MutableList;
+import kala.value.LazyValue;
 import org.aya.generic.AyaDocile;
 import org.aya.generic.Modifier;
 import org.aya.generic.Renamer;
@@ -395,11 +396,9 @@ yield visitFn(defVar(def.ref()), def.modifiers(), absTele,
   ) {
     // TODO: should we pretty print the `self` parameter?
     //       The use of `self` parameter still appears in other parameters.
+    var visitTele = visitTele(telescope);
 
-    var richTele = enrich(telescope);
-    var binds = richTele.<Term>map(x -> new FreeTerm(x.ref()));
-
-    return Doc.sepNonEmpty(BAR, name, visitTele(richTele), HAS_TYPE, term(Outer.Free, telescope.result(binds)));
+    return Doc.sepNonEmpty(BAR, name, visitTele.tele, HAS_TYPE, visitTele.result.get());
   }
 
   public @NotNull Doc visitClauseLhs(@NotNull ImmutableSeq<Pat> patterns, @NotNull SeqView<Boolean> licits) {
@@ -429,22 +428,6 @@ yield visitFn(defVar(def.ref()), def.modifiers(), absTele,
   }
 
   // region Name Generation
-  private @NotNull ImmutableSeq<Term> toTerm(@NotNull ImmutableSeq<ParamLike<Term>> params) {
-    return params.map(x -> new FreeTerm(x.ref()));
-  }
-
-  private @NotNull ImmutableSeq<ParamLike<Term>> enrich(@NotNull SeqLike<Param> tele) {
-    var richTele = MutableList.<ParamLike<Term>>create();
-
-    for (var param : tele) {
-      var freeTy = param.type().instTeleVar(richTele.view().map(ParamLike::ref));
-      richTele.append(new RichParam(new LocalVar(
-        param.name(), SourcePos.NONE, Basic.Pretty), freeTy, param.explicit()));
-    }
-
-    return richTele.toImmutableSeq();
-  }
-
   private @NotNull ImmutableSeq<ParamLike<Term>> enrich(@NotNull AbstractTele tele) {
     var richTele = FreezableMutableList.<ParamLike<Term>>create();
 
@@ -466,5 +449,17 @@ yield visitFn(defVar(def.ref()), def.modifiers(), absTele,
   private @NotNull LocalVar generateName(@Nullable Term whty) {
     return nameGen.bindName(whty);
   }
+
+  record VisitTele(@NotNull Doc tele, @NotNull LazyValue<Doc> result) { }
+
+  private @NotNull VisitTele visitTele(@NotNull AbstractTele tele) {
+    var richTele = enrich(tele);
+    var teleDoc = visitTele(richTele);
+
+    return new VisitTele(teleDoc, LazyValue.of(() -> {
+      var binds = richTele.<Term>map(x -> new FreeTerm(x.ref()));
+      return term(Outer.Free, tele.result(binds));
+    }));
+  }
   // endregion Name Generating
 }

From 00c895177ec709fb8da17bfce73b019e851dffce Mon Sep 17 00:00:00 2001
From: HoshinoTented <hoshinotented@qq.com>
Date: Thu, 23 Jan 2025 23:30:44 +0800
Subject: [PATCH 05/16] pretty: class and prim

---
 .../java/org/aya/prettier/BasePrettier.java   |  4 ++--
 .../java/org/aya/prettier/CorePrettier.java   | 24 ++++++++++++-------
 .../java/org/aya/syntax/compile/JitClass.java |  4 ++--
 .../org/aya/syntax/core/def/ClassDef.java     |  6 ++---
 .../org/aya/syntax/core/def/ClassDefLike.java |  4 ++--
 5 files changed, 24 insertions(+), 18 deletions(-)

diff --git a/syntax/src/main/java/org/aya/prettier/BasePrettier.java b/syntax/src/main/java/org/aya/prettier/BasePrettier.java
index 36bc7a18be..4276da65a1 100644
--- a/syntax/src/main/java/org/aya/prettier/BasePrettier.java
+++ b/syntax/src/main/java/org/aya/prettier/BasePrettier.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.prettier;
 
@@ -281,7 +281,7 @@ protected boolean optionImplicit() {
     return coerce ? Doc.styled(KEYWORD, "coerce") : Doc.empty();
   }
 
-  static @NotNull Doc primDoc(DefVar<?, ?> ref) {
+  static @NotNull Doc primDoc(AnyDefVar ref) {
     return Doc.sep(KW_PRIM, refVar(ref));
   }
 
diff --git a/syntax/src/main/java/org/aya/prettier/CorePrettier.java b/syntax/src/main/java/org/aya/prettier/CorePrettier.java
index 03d3de37d7..c0416ddab1 100644
--- a/syntax/src/main/java/org/aya/prettier/CorePrettier.java
+++ b/syntax/src/main/java/org/aya/prettier/CorePrettier.java
@@ -287,9 +287,7 @@ yield visitFn(defVar(def.ref()), def.modifiers(), absTele,
       }
       case MemberDef field -> visitMember(defVar(field.ref()), TyckDef.defSignature(field));
       case ConDef con -> visitCon(con.ref, con.coerce, con.selfTele);
-      case ClassDef def -> Doc.vcat(Doc.sepNonEmpty(KW_CLASS,
-        defVar(def.ref()),
-        Doc.nest(2, Doc.vcat(def.members().view().map(this::def)))));
+      case ClassDef def -> visitClass(defVar(def.ref()), def.members().view().map(this::def));
       case DataDef def -> visitData(defVar(def.ref()), TyckDef.defSignature(def), dataLine -> {
         var consDoc = def.body.view().map(this::def);
         return Doc.vcat(dataLine, Doc.nest(2, Doc.vcat(consDoc)));
@@ -299,22 +297,23 @@ yield visitFn(defVar(def.ref()), def.modifiers(), absTele,
 
   public @NotNull Doc def(@NotNull JitDef unit) {
     var dummyVar = new CompiledVar(unit);
+    var nameDoc = defVar(dummyVar);
 
     return switch (unit) {
-      case JitFn jitFn -> visitFn(defVar(dummyVar), jitFn.modifiers(), jitFn, (prefix, _) ->
+      case JitFn jitFn -> visitFn(nameDoc, jitFn.modifiers(), jitFn, (prefix, _) ->
         Doc.sep(prefix, FN_DEFINED_AS, COMMENT_COMPILED_CODE));
       case JitCon jitCon -> {
         var dummyOwnerArgs = ImmutableSeq.<Term>fill(jitCon.ownerTeleSize(), i -> new FreeTerm(jitCon.telescopeName(i)));
-        var rhs = visitConRhs(defVar(dummyVar), true && false, jitCon.inst(dummyOwnerArgs));
+        var rhs = visitConRhs(nameDoc, true && false, jitCon.inst(dummyOwnerArgs));
         yield Doc.sep(BAR, COMMENT_COMPILED_PATTERN, FN_DEFINED_AS, rhs);
       }
-      case JitData jitData -> visitData(defVar(dummyVar), jitData, dataLine -> {
+      case JitData jitData -> visitData(nameDoc, jitData, dataLine -> {
         var consDoc = jitData.body().view().map(this::def);
         return Doc.vcat(dataLine, Doc.nest(2, Doc.vcat(consDoc)));
       });
-      case JitMember jitMember -> visitMember(defVar(dummyVar), jitMember);
-      case JitClass jiClasst -> null;
-      case JitPrim jitPrim -> null;
+      case JitMember jitMember -> visitMember(nameDoc, jitMember);
+      case JitClass jitClass -> visitClass(nameDoc, jitClass.members().view().map(this::def));
+      case JitPrim _ -> primDoc(dummyVar);
     };
   }
 
@@ -401,6 +400,13 @@ yield visitFn(defVar(def.ref()), def.modifiers(), absTele,
     return Doc.sepNonEmpty(BAR, name, visitTele.tele, HAS_TYPE, visitTele.result.get());
   }
 
+  private @NotNull Doc visitClass(
+    @NotNull Doc name,
+    @NotNull SeqView<Doc> members
+  ) {
+    return Doc.sepNonEmpty(KW_CLASS, name, Doc.nest(2, Doc.vcat(members)));
+  }
+
   public @NotNull Doc visitClauseLhs(@NotNull ImmutableSeq<Pat> patterns, @NotNull SeqView<Boolean> licits) {
     var enrichPats = patterns.zip(licits, (pat, licit) -> pat(pat, licit, Outer.Free));
     return Doc.commaList(enrichPats);
diff --git a/syntax/src/main/java/org/aya/syntax/compile/JitClass.java b/syntax/src/main/java/org/aya/syntax/compile/JitClass.java
index 437266dcdf..cc631c6344 100644
--- a/syntax/src/main/java/org/aya/syntax/compile/JitClass.java
+++ b/syntax/src/main/java/org/aya/syntax/compile/JitClass.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.compile;
 
@@ -20,7 +20,7 @@ protected JitClass() {
 
   public abstract @NotNull JitMember[] membars();
 
-  @Override public final @NotNull ImmutableSeq<MemberDefLike> members() {
+  @Override public final @NotNull ImmutableSeq<JitMember> members() {
     return ImmutableArray.Unsafe.wrap(membars());
   }
 
diff --git a/syntax/src/main/java/org/aya/syntax/core/def/ClassDef.java b/syntax/src/main/java/org/aya/syntax/core/def/ClassDef.java
index c158446ac4..a90b725ec0 100644
--- a/syntax/src/main/java/org/aya/syntax/core/def/ClassDef.java
+++ b/syntax/src/main/java/org/aya/syntax/core/def/ClassDef.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;
 
@@ -28,10 +28,10 @@ public record ClassDef(
 ) implements TopLevelDef {
   public ClassDef { ref.initialize(this); }
   public static final class Delegate extends TyckAnyDef<ClassDef> implements ClassDefLike {
-    private final @NotNull LazyValue<ImmutableSeq<MemberDefLike>> members = LazyValue.of(() ->
+    private final @NotNull LazyValue<ImmutableSeq<MemberDef.Delegate>> members = LazyValue.of(() ->
       core().members.map(x -> new MemberDef.Delegate(x.ref())));
 
     public Delegate(@NotNull DefVar<ClassDef, ?> ref) { super(ref); }
-    @Override public @NotNull ImmutableSeq<MemberDefLike> members() { return members.get(); }
+    @Override public @NotNull ImmutableSeq<MemberDef.Delegate> members() { return members.get(); }
   }
 }
diff --git a/syntax/src/main/java/org/aya/syntax/core/def/ClassDefLike.java b/syntax/src/main/java/org/aya/syntax/core/def/ClassDefLike.java
index 644e13e9d9..92243f9581 100644
--- a/syntax/src/main/java/org/aya/syntax/core/def/ClassDefLike.java
+++ b/syntax/src/main/java/org/aya/syntax/core/def/ClassDefLike.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;
 
@@ -10,7 +10,7 @@
 import org.jetbrains.annotations.NotNull;
 
 public sealed interface ClassDefLike extends AnyDef permits JitClass, ClassDef.Delegate {
-  @NotNull ImmutableSeq<MemberDefLike> members();
+  @NotNull ImmutableSeq<? extends MemberDefLike> members();
 
   default @NotNull Term telescope(int i, @NotNull Seq<Term> restriction) {
     var member = members().get(i);

From d358e0a47471f37673b003ab0e1bd25d7af0636a Mon Sep 17 00:00:00 2001
From: HoshinoTented <hoshinotented@qq.com>
Date: Fri, 24 Jan 2025 19:19:30 +0800
Subject: [PATCH 06/16] pretty: is this good?

---
 .../java/org/aya/prettier/CorePrettier.java   | 29 +++++++++++--------
 1 file changed, 17 insertions(+), 12 deletions(-)

diff --git a/syntax/src/main/java/org/aya/prettier/CorePrettier.java b/syntax/src/main/java/org/aya/prettier/CorePrettier.java
index c0416ddab1..b31712f0fb 100644
--- a/syntax/src/main/java/org/aya/prettier/CorePrettier.java
+++ b/syntax/src/main/java/org/aya/prettier/CorePrettier.java
@@ -28,12 +28,14 @@
 import org.aya.syntax.core.term.repr.MetaLitTerm;
 import org.aya.syntax.core.term.repr.StringTerm;
 import org.aya.syntax.core.term.xtt.*;
+import org.aya.syntax.ref.AnyDefVar;
 import org.aya.syntax.ref.CompiledVar;
 import org.aya.syntax.ref.DefVar;
 import org.aya.syntax.ref.GenerateKind.Basic;
 import org.aya.syntax.ref.LocalVar;
 import org.aya.syntax.telescope.AbstractTele;
 import org.aya.util.Arg;
+import org.aya.util.error.Panic;
 import org.aya.util.error.SourcePos;
 import org.aya.util.error.WithPos;
 import org.aya.util.prettier.PrettierOptions;
@@ -288,10 +290,15 @@ yield visitFn(defVar(def.ref()), def.modifiers(), absTele,
       case MemberDef field -> visitMember(defVar(field.ref()), TyckDef.defSignature(field));
       case ConDef con -> visitCon(con.ref, con.coerce, con.selfTele);
       case ClassDef def -> visitClass(defVar(def.ref()), def.members().view().map(this::def));
-      case DataDef def -> visitData(defVar(def.ref()), TyckDef.defSignature(def), dataLine -> {
-        var consDoc = def.body.view().map(this::def);
-        return Doc.vcat(dataLine, Doc.nest(2, Doc.vcat(consDoc)));
-      });
+      case DataDef def -> visitData(new DataDef.Delegate(def.ref()));
+    };
+  }
+
+  public @NotNull Doc def(@NotNull AnyDef unit) {
+    return switch (unit) {
+      case JitDef jitDef -> def(jitDef);
+      case TyckAnyDef<?> tyckAnyDef -> def(tyckAnyDef.ref.core);
+      default -> Panic.unreachable();
     };
   }
 
@@ -307,10 +314,7 @@ yield visitFn(defVar(def.ref()), def.modifiers(), absTele,
         var rhs = visitConRhs(nameDoc, true && false, jitCon.inst(dummyOwnerArgs));
         yield Doc.sep(BAR, COMMENT_COMPILED_PATTERN, FN_DEFINED_AS, rhs);
       }
-      case JitData jitData -> visitData(nameDoc, jitData, dataLine -> {
-        var consDoc = jitData.body().view().map(this::def);
-        return Doc.vcat(dataLine, Doc.nest(2, Doc.vcat(consDoc)));
-      });
+      case JitData jitData -> visitData(jitData);
       case JitMember jitMember -> visitMember(nameDoc, jitMember);
       case JitClass jitClass -> visitClass(nameDoc, jitClass.members().view().map(this::def));
       case JitPrim _ -> primDoc(dummyVar);
@@ -372,10 +376,10 @@ yield visitFn(defVar(def.ref()), def.modifiers(), absTele,
   }
 
   private @NotNull Doc visitData(
-    @NotNull Doc name,
-    @NotNull AbstractTele telescope,
-    @NotNull Function<Doc, Doc> cont
+    @NotNull DataDefLike dataDef
   ) {
+    var name = defVar(AnyDef.toVar(dataDef));
+    var telescope = dataDef.signature();
     var richDataTele = enrich(telescope);
     var dataArgs = richDataTele.<Term>map(t -> new FreeTerm(t.ref()));
 
@@ -384,8 +388,9 @@ yield visitFn(defVar(def.ref()), def.modifiers(), absTele,
       visitTele(richDataTele),
       HAS_TYPE,
       term(Outer.Free, telescope.result(dataArgs)));
+    var consDoc = dataDef.body().view().map(this::def);
 
-    return cont.apply(line1);
+    return Doc.cat(line1, Doc.nest(2, Doc.vcat(consDoc)));
   }
 
   /// @param telescope the telescope of a [MemberDefLike], including the `self` parameter

From ee152bd0fdb6fbb0956f6c5fbd89576ed11cf9dc Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Sat, 25 Jan 2025 07:47:35 -0500
Subject: [PATCH 07/16] repl: improve code

---
 .../java/org/aya/cli/repl/ReplCommands.java   | 29 ++++++++++---------
 .../java/org/aya/prettier/CorePrettier.java   |  2 +-
 .../src/main/java/org/aya/repl/Command.java   | 14 ++++-----
 .../src/main/java/org/aya/repl/ReplUtil.java  | 20 +++++++------
 4 files changed, 34 insertions(+), 31 deletions(-)

diff --git a/cli-console/src/main/java/org/aya/cli/repl/ReplCommands.java b/cli-console/src/main/java/org/aya/cli/repl/ReplCommands.java
index 6714c05999..8617d6f555 100644
--- a/cli-console/src/main/java/org/aya/cli/repl/ReplCommands.java
+++ b/cli-console/src/main/java/org/aya/cli/repl/ReplCommands.java
@@ -2,29 +2,31 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.cli.repl;
 
+import java.io.IOException;
+import java.nio.file.Files;
+import java.nio.file.Path;
+
 import kala.collection.immutable.ImmutableSeq;
 import kala.collection.mutable.MutableList;
 import kala.control.Either;
 import org.aya.cli.render.RenderOptions;
 import org.aya.prettier.AyaPrettierOptions;
 import org.aya.prettier.BasePrettier;
-import org.aya.prettier.CorePrettier;
 import org.aya.pretty.doc.Doc;
 import org.aya.producer.AyaParserImpl;
 import org.aya.repl.Command;
 import org.aya.repl.CommandArg;
 import org.aya.repl.ReplUtil;
 import org.aya.syntax.compile.JitDef;
-import org.aya.syntax.core.def.*;
+import org.aya.syntax.core.def.AnyDef;
+import org.aya.syntax.core.def.ConDefLike;
+import org.aya.syntax.core.def.MemberDefLike;
+import org.aya.syntax.core.def.TyckAnyDef;
 import org.aya.syntax.literate.CodeOptions;
 import org.aya.syntax.ref.AnyDefVar;
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
-import java.io.IOException;
-import java.nio.file.Files;
-import java.nio.file.Path;
-
 public interface ReplCommands {
   record Code(@NotNull String code) { }
   record Prompt(@NotNull String prompt) { }
@@ -65,11 +67,10 @@ record StyleParam(@NotNull Either<RenderOptions.StyleFamilyName, Path> value)
         }
       }
 
-      return switch (topLevel) {
-        case JitDef jitDef -> new Result(Output.stdout(repl.render(jitDef)), true);
-        case TyckAnyDef<?> tyckDef -> new Result(Output.stdout(repl.render(tyckDef.core())), true);
-        default -> Result.ok(topLevel.name(), true);
-      };
+      return new Result(Output.stdout((switch (topLevel) {
+        case JitDef jitDef -> repl.render(jitDef);
+        case TyckAnyDef<?> tyckDef -> repl.render(tyckDef.core());
+      })), true);
     }
   };
 
@@ -83,7 +84,7 @@ record StyleParam(@NotNull Either<RenderOptions.StyleFamilyName, Path> value)
   @NotNull Command SHOW_SHAPES = new Command(ImmutableSeq.of("debug-show-shapes"), "Show recognized shapes") {
     @Entry public @NotNull Command.Result execute(@NotNull AyaRepl repl) {
       var discovered = repl.replCompiler.getShapeFactory().discovered;
-      return Result.ok(repl.renderDoc(Doc.vcat(discovered.mapTo(MutableList.create(),
+      return new Result(Output.stdout(Doc.vcat(discovered.mapTo(MutableList.create(),
         (def, recog) ->
           Doc.sep(BasePrettier.refVar(def),
             Doc.symbol("=>"),
@@ -99,7 +100,7 @@ record StyleParam(@NotNull Either<RenderOptions.StyleFamilyName, Path> value)
         return Result.err("Unable to load file or library: " + e.getLocalizedMessage(), true);
       }
       // SingleFileCompiler would print result to REPL.
-      return new Result(Output.empty(), true);
+      return new Result(Output.EMPTY, true);
     }
   };
 
@@ -119,7 +120,7 @@ record StyleParam(@NotNull Either<RenderOptions.StyleFamilyName, Path> value)
       repl.cwd = path;
       // for jline completer to work properly, but it does not have any effect actually
       System.setProperty("user.dir", path.toAbsolutePath().toString());
-      return new Result(Output.empty(), true);
+      return new Result(Output.EMPTY, true);
     }
   };
 
diff --git a/syntax/src/main/java/org/aya/prettier/CorePrettier.java b/syntax/src/main/java/org/aya/prettier/CorePrettier.java
index 4f5489d17b..c2483299ee 100644
--- a/syntax/src/main/java/org/aya/prettier/CorePrettier.java
+++ b/syntax/src/main/java/org/aya/prettier/CorePrettier.java
@@ -283,7 +283,7 @@ yield visitFn(defVar(def.ref()), def.modifiers(), absTele,
           (prefix, subst) -> switch (def.body()) {
           case Either.Left(var term) -> Doc.sep(prefix, FN_DEFINED_AS, term(Outer.Free, term.instTele(subst.view())));
           case Either.Right(var body) -> Doc.vcat(prefix,
-            Doc.nest(2, visitClauses(body.matchingsView(), def.telescope().view().map(ParamLike::explicit))));
+            Doc.nest(2, visitClauses(body.matchingsView(), def.telescope().view().map(Param::explicit))));
         });
       }
       case MemberDef field -> visitMember(defVar(field.ref()), TyckDef.defSignature(field));
diff --git a/tools-repl/src/main/java/org/aya/repl/Command.java b/tools-repl/src/main/java/org/aya/repl/Command.java
index 73adb0b608..eb140dcc8a 100644
--- a/tools-repl/src/main/java/org/aya/repl/Command.java
+++ b/tools-repl/src/main/java/org/aya/repl/Command.java
@@ -1,17 +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.repl;
 
-import kala.collection.immutable.ImmutableSeq;
-import org.aya.pretty.doc.Doc;
-import org.jetbrains.annotations.NonNls;
-import org.jetbrains.annotations.NotNull;
-
 import java.lang.annotation.ElementType;
 import java.lang.annotation.Retention;
 import java.lang.annotation.RetentionPolicy;
 import java.lang.annotation.Target;
 
+import kala.collection.immutable.ImmutableSeq;
+import org.aya.pretty.doc.Doc;
+import org.jetbrains.annotations.NonNls;
+import org.jetbrains.annotations.NotNull;
+
 public abstract class Command {
   @Retention(RetentionPolicy.RUNTIME)
   @Target(ElementType.METHOD)
@@ -33,7 +33,7 @@ public Command(@NotNull ImmutableSeq<String> names, @NotNull String help) {
   public final @NotNull String help() { return help; }
 
   public record Output(@NotNull Doc stdout, @NotNull Doc stderr) {
-    public static @NotNull Output empty() { return new Output(Doc.empty(), Doc.empty()); }
+    public static final Output EMPTY = new Output(Doc.empty(), Doc.empty());
     public static @NotNull Output stdout(@NotNull Doc doc) { return new Output(doc, Doc.empty()); }
     public static @NotNull Output stderr(@NotNull Doc doc) { return new Output(Doc.empty(), doc); }
     public static @NotNull Output stdout(@NotNull String doc) { return new Output(Doc.english(doc), Doc.empty()); }
diff --git a/tools-repl/src/main/java/org/aya/repl/ReplUtil.java b/tools-repl/src/main/java/org/aya/repl/ReplUtil.java
index 33122c0998..36053870c7 100644
--- a/tools-repl/src/main/java/org/aya/repl/ReplUtil.java
+++ b/tools-repl/src/main/java/org/aya/repl/ReplUtil.java
@@ -1,25 +1,27 @@
-// 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.repl;
 
+import java.io.IOException;
+import java.nio.file.Path;
+import java.util.function.Consumer;
+
 import org.aya.pretty.doc.Doc;
+import org.aya.repl.Command.Output;
+import org.aya.repl.Command.Result;
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 import org.jline.terminal.TerminalBuilder;
 import org.jline.utils.AttributedStringBuilder;
 import org.jline.utils.AttributedStyle;
 
-import java.io.IOException;
-import java.nio.file.Path;
-import java.util.function.Consumer;
-
 public interface ReplUtil {
-  static @NotNull Command.Result invokeHelp(CommandManager commandManager, @Nullable HelpItem argument) {
+  static @NotNull Result invokeHelp(CommandManager commandManager, @Nullable HelpItem argument) {
     if (argument != null && !argument.cmd.isEmpty()) {
       return commandManager.cmd.find(c -> c.owner().names().contains(argument.cmd))
         .getOrElse(
-          it -> Command.Result.ok(it.owner().help(), true),
-          () -> Command.Result.err("No such command: " + argument.cmd, true));
+          it -> Result.ok(it.owner().help(), true),
+          () -> Result.err("No such command: " + argument.cmd, true));
     }
     var commands = Doc.vcat(commandManager.cmd.view()
       .map(command -> Doc.sep(
@@ -27,7 +29,7 @@ public interface ReplUtil {
         Doc.symbol("-"),
         Doc.english(command.owner().help())
       )));
-    return new Command.Result(new Command.Output(commands, Doc.empty()), true);
+    return new Result(Output.stdout(commands), true);
   }
 
   record HelpItem(@NotNull String cmd) {

From b9d49e5946a82244f32cd40f1394f8cd90aa7581 Mon Sep 17 00:00:00 2001
From: HoshinoTented <hoshinotented@qq.com>
Date: Sat, 25 Jan 2025 20:51:35 +0800
Subject: [PATCH 08/16] lsp-test: advisor now extends `DiskCompilerAdvisor`
 (with some bug)

---
 .../src/test/java/org/aya/lsp/LspTest.java    | 10 ++++-
 .../lsp/tester/LspTestCompilerAdvisor.java    | 38 +++++++++++++++++--
 .../java/org/aya/syntax/compile/JitUnit.java  |  2 +-
 3 files changed, 44 insertions(+), 6 deletions(-)

diff --git a/ide-lsp/src/test/java/org/aya/lsp/LspTest.java b/ide-lsp/src/test/java/org/aya/lsp/LspTest.java
index 0c8e9f5578..686c795706 100644
--- a/ide-lsp/src/test/java/org/aya/lsp/LspTest.java
+++ b/ide-lsp/src/test/java/org/aya/lsp/LspTest.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.lsp;
 
@@ -15,13 +15,16 @@
 import org.aya.syntax.concrete.stmt.decl.FnDecl;
 import org.aya.syntax.core.term.MetaPatTerm;
 import org.aya.syntax.core.term.call.DataCall;
+import org.aya.util.FileUtil;
 import org.javacs.lsp.InitializeParams;
 import org.javacs.lsp.Position;
 import org.javacs.lsp.TextDocumentIdentifier;
 import org.javacs.lsp.TextDocumentPositionParams;
 import org.jetbrains.annotations.NotNull;
+import org.junit.jupiter.api.BeforeEach;
 import org.junit.jupiter.api.Test;
 
+import java.io.IOException;
 import java.nio.file.Path;
 
 import static org.aya.lsp.tester.TestCommand.compile;
@@ -37,6 +40,11 @@ public class LspTest {
     return client;
   }
 
+  // FIXME: remove this after fixing the prim factory problem
+  @BeforeEach public void clearCore() throws IOException {
+    FileUtil.deleteRecursively(TEST_LIB.resolve("build"));
+  }
+
   @Test public void testJustLoad() {
     launch(TEST_LIB).execute(compile((_, _) -> {}));
   }
diff --git a/ide-lsp/src/test/java/org/aya/lsp/tester/LspTestCompilerAdvisor.java b/ide-lsp/src/test/java/org/aya/lsp/tester/LspTestCompilerAdvisor.java
index ce37d8eda4..2cb0dcda37 100644
--- a/ide-lsp/src/test/java/org/aya/lsp/tester/LspTestCompilerAdvisor.java
+++ b/ide-lsp/src/test/java/org/aya/lsp/tester/LspTestCompilerAdvisor.java
@@ -1,10 +1,12 @@
-// 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.lsp.tester;
 
 import kala.collection.SeqView;
 import kala.collection.immutable.ImmutableSeq;
 import kala.collection.mutable.MutableList;
+import kala.collection.mutable.MutableMap;
+import org.aya.cli.library.incremental.DiskCompilerAdvisor;
 import org.aya.cli.library.incremental.InMemoryCompilerAdvisor;
 import org.aya.cli.library.source.LibrarySource;
 import org.aya.resolve.ResolveInfo;
@@ -13,10 +15,16 @@
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
+import java.io.IOException;
+import java.nio.file.Files;
+import java.nio.file.Path;
+import java.nio.file.attribute.FileTime;
+import java.time.Instant;
 import java.util.function.Function;
 
-public class LspTestCompilerAdvisor extends InMemoryCompilerAdvisor {
+public class LspTestCompilerAdvisor extends DiskCompilerAdvisor {
   public @Nullable ImmutableSeq<ImmutableSeq<LibrarySource>> lastJob;
+  public final @NotNull MutableMap<Path, FileTime> newlyModified = MutableMap.create();
   public final @NotNull MutableList<ResolveInfo> newlyCompiled = MutableList.create();
 
   public @NotNull SeqView<LibrarySource> lastCompiled() {
@@ -26,7 +34,24 @@ public class LspTestCompilerAdvisor extends InMemoryCompilerAdvisor {
   }
 
   public void mutate(@NotNull LibrarySource source) {
-    coreTimestamp.remove(timestampKey(source));
+    newlyModified.put(source.underlyingFile(), FileTime.from(Instant.now()));
+  }
+
+  @Override
+  public boolean isSourceModified(@NotNull LibrarySource source) {
+    var tempFileTime = newlyModified.getOrNull(source.underlyingFile());
+    if (tempFileTime != null) {
+      try {
+        // TODO: duplicate code as in [InMemoryCompilerAdvisor] and [DiskCompilerAdvisor]
+        var core = source.compiledCorePath();
+        if (!Files.exists(core)) return true;
+        return tempFileTime.compareTo(Files.getLastModifiedTime(core)) > 0;
+      } catch (IOException e) {
+        return true;
+      }
+    }
+
+    return super.isSourceModified(source);
   }
 
   public void prepareCompile() {
@@ -40,7 +65,12 @@ public void prepareCompile() {
   }
 
   @Override public @NotNull ResolveInfo
-  doSaveCompiledCore(@NotNull LibrarySource file, @NotNull ResolveInfo resolveInfo, @NotNull ImmutableSeq<TyckDef> defs, @NotNull ModuleLoader recurseLoader) {
+  doSaveCompiledCore(
+    @NotNull LibrarySource file,
+    @NotNull ResolveInfo resolveInfo,
+    @NotNull ImmutableSeq<TyckDef> defs,
+    @NotNull ModuleLoader recurseLoader
+  ) throws IOException, ClassNotFoundException {
     var info = super.doSaveCompiledCore(file, resolveInfo, defs, recurseLoader);
     newlyCompiled.append(resolveInfo);
     return info;
diff --git a/syntax/src/main/java/org/aya/syntax/compile/JitUnit.java b/syntax/src/main/java/org/aya/syntax/compile/JitUnit.java
index b81650422f..1c07866bf0 100644
--- a/syntax/src/main/java/org/aya/syntax/compile/JitUnit.java
+++ b/syntax/src/main/java/org/aya/syntax/compile/JitUnit.java
@@ -9,7 +9,7 @@
 import org.aya.util.error.Panic;
 import org.jetbrains.annotations.NotNull;
 
-public abstract sealed class JitUnit permits JitDef, JitMatchy {
+public abstract class JitUnit {
   private CompiledAya metadata;
 
   public @NotNull final CompiledAya metadata() {

From df5cd6f16b23bcb9537c93baefbed25741f027c0 Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Sat, 25 Jan 2025 08:00:21 -0500
Subject: [PATCH 09/16] revert: "lsp-test: advisor now extends
 `DiskCompilerAdvisor` (with some bug)"

This reverts commit b9d49e5946a82244f32cd40f1394f8cd90aa7581.
---
 .../test/resources/negative/PatCohError.txt   |  2 +-
 .../src/test/java/org/aya/lsp/LspTest.java    | 10 +----
 .../lsp/tester/LspTestCompilerAdvisor.java    | 38 ++-----------------
 3 files changed, 6 insertions(+), 44 deletions(-)

diff --git a/cli-impl/src/test/resources/negative/PatCohError.txt b/cli-impl/src/test/resources/negative/PatCohError.txt
index 5de67a76d7..9ce9df5caf 100644
--- a/cli-impl/src/test/resources/negative/PatCohError.txt
+++ b/cli-impl/src/test/resources/negative/PatCohError.txt
@@ -9,7 +9,7 @@ In file $FILE:10:0 ->
      │ ╰─────────────────╯
 
 Error: I'm unsure if there should be a case for constructor
-         | suc m ⇒ fsuc (_ : Fin+1 ^0)
+         | suc m ⇒ fsuc (_ : Fin+1 m)
        because I got stuck on the index unification of type
          Fin+1 m
 
diff --git a/ide-lsp/src/test/java/org/aya/lsp/LspTest.java b/ide-lsp/src/test/java/org/aya/lsp/LspTest.java
index 686c795706..0c8e9f5578 100644
--- a/ide-lsp/src/test/java/org/aya/lsp/LspTest.java
+++ b/ide-lsp/src/test/java/org/aya/lsp/LspTest.java
@@ -1,4 +1,4 @@
-// Copyright (c) 2020-2025 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2024 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.lsp;
 
@@ -15,16 +15,13 @@
 import org.aya.syntax.concrete.stmt.decl.FnDecl;
 import org.aya.syntax.core.term.MetaPatTerm;
 import org.aya.syntax.core.term.call.DataCall;
-import org.aya.util.FileUtil;
 import org.javacs.lsp.InitializeParams;
 import org.javacs.lsp.Position;
 import org.javacs.lsp.TextDocumentIdentifier;
 import org.javacs.lsp.TextDocumentPositionParams;
 import org.jetbrains.annotations.NotNull;
-import org.junit.jupiter.api.BeforeEach;
 import org.junit.jupiter.api.Test;
 
-import java.io.IOException;
 import java.nio.file.Path;
 
 import static org.aya.lsp.tester.TestCommand.compile;
@@ -40,11 +37,6 @@ public class LspTest {
     return client;
   }
 
-  // FIXME: remove this after fixing the prim factory problem
-  @BeforeEach public void clearCore() throws IOException {
-    FileUtil.deleteRecursively(TEST_LIB.resolve("build"));
-  }
-
   @Test public void testJustLoad() {
     launch(TEST_LIB).execute(compile((_, _) -> {}));
   }
diff --git a/ide-lsp/src/test/java/org/aya/lsp/tester/LspTestCompilerAdvisor.java b/ide-lsp/src/test/java/org/aya/lsp/tester/LspTestCompilerAdvisor.java
index 2cb0dcda37..ce37d8eda4 100644
--- a/ide-lsp/src/test/java/org/aya/lsp/tester/LspTestCompilerAdvisor.java
+++ b/ide-lsp/src/test/java/org/aya/lsp/tester/LspTestCompilerAdvisor.java
@@ -1,12 +1,10 @@
-// Copyright (c) 2020-2025 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2024 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.lsp.tester;
 
 import kala.collection.SeqView;
 import kala.collection.immutable.ImmutableSeq;
 import kala.collection.mutable.MutableList;
-import kala.collection.mutable.MutableMap;
-import org.aya.cli.library.incremental.DiskCompilerAdvisor;
 import org.aya.cli.library.incremental.InMemoryCompilerAdvisor;
 import org.aya.cli.library.source.LibrarySource;
 import org.aya.resolve.ResolveInfo;
@@ -15,16 +13,10 @@
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
-import java.io.IOException;
-import java.nio.file.Files;
-import java.nio.file.Path;
-import java.nio.file.attribute.FileTime;
-import java.time.Instant;
 import java.util.function.Function;
 
-public class LspTestCompilerAdvisor extends DiskCompilerAdvisor {
+public class LspTestCompilerAdvisor extends InMemoryCompilerAdvisor {
   public @Nullable ImmutableSeq<ImmutableSeq<LibrarySource>> lastJob;
-  public final @NotNull MutableMap<Path, FileTime> newlyModified = MutableMap.create();
   public final @NotNull MutableList<ResolveInfo> newlyCompiled = MutableList.create();
 
   public @NotNull SeqView<LibrarySource> lastCompiled() {
@@ -34,24 +26,7 @@ public class LspTestCompilerAdvisor extends DiskCompilerAdvisor {
   }
 
   public void mutate(@NotNull LibrarySource source) {
-    newlyModified.put(source.underlyingFile(), FileTime.from(Instant.now()));
-  }
-
-  @Override
-  public boolean isSourceModified(@NotNull LibrarySource source) {
-    var tempFileTime = newlyModified.getOrNull(source.underlyingFile());
-    if (tempFileTime != null) {
-      try {
-        // TODO: duplicate code as in [InMemoryCompilerAdvisor] and [DiskCompilerAdvisor]
-        var core = source.compiledCorePath();
-        if (!Files.exists(core)) return true;
-        return tempFileTime.compareTo(Files.getLastModifiedTime(core)) > 0;
-      } catch (IOException e) {
-        return true;
-      }
-    }
-
-    return super.isSourceModified(source);
+    coreTimestamp.remove(timestampKey(source));
   }
 
   public void prepareCompile() {
@@ -65,12 +40,7 @@ public void prepareCompile() {
   }
 
   @Override public @NotNull ResolveInfo
-  doSaveCompiledCore(
-    @NotNull LibrarySource file,
-    @NotNull ResolveInfo resolveInfo,
-    @NotNull ImmutableSeq<TyckDef> defs,
-    @NotNull ModuleLoader recurseLoader
-  ) throws IOException, ClassNotFoundException {
+  doSaveCompiledCore(@NotNull LibrarySource file, @NotNull ResolveInfo resolveInfo, @NotNull ImmutableSeq<TyckDef> defs, @NotNull ModuleLoader recurseLoader) {
     var info = super.doSaveCompiledCore(file, resolveInfo, defs, recurseLoader);
     newlyCompiled.append(resolveInfo);
     return info;

From 94e3c56358d16cad089911c70f1b2715d402d8e2 Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Sat, 25 Jan 2025 08:26:14 -0500
Subject: [PATCH 10/16] test: the pretty print

---
 .../org/aya/test/cli/ReplCompilerTest.java    | 20 +++++++++++--------
 1 file changed, 12 insertions(+), 8 deletions(-)

diff --git a/cli-impl/src/test/java/org/aya/test/cli/ReplCompilerTest.java b/cli-impl/src/test/java/org/aya/test/cli/ReplCompilerTest.java
index 1778a195bc..96134697f6 100644
--- a/cli-impl/src/test/java/org/aya/test/cli/ReplCompilerTest.java
+++ b/cli-impl/src/test/java/org/aya/test/cli/ReplCompilerTest.java
@@ -1,7 +1,12 @@
-// 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.test.cli;
 
+import java.io.IOException;
+import java.nio.file.Paths;
+
+import static org.junit.jupiter.api.Assertions.*;
+
 import kala.collection.immutable.ImmutableSeq;
 import org.aya.cli.interactive.ReplCompiler;
 import org.aya.generic.Constants;
@@ -14,6 +19,7 @@
 import org.aya.syntax.core.term.repr.IntegerTerm;
 import org.aya.syntax.literate.CodeOptions.NormalizeMode;
 import org.aya.syntax.ref.AnyVar;
+import org.aya.syntax.ref.CompiledVar;
 import org.aya.syntax.ref.DefVar;
 import org.aya.util.error.SourcePos;
 import org.aya.util.reporter.ThrowingReporter;
@@ -22,11 +28,6 @@
 import org.junit.jupiter.api.BeforeEach;
 import org.junit.jupiter.api.Test;
 
-import java.io.IOException;
-import java.nio.file.Paths;
-
-import static org.junit.jupiter.api.Assertions.*;
-
 public class ReplCompilerTest {
   public final @NotNull ReplCompiler compiler = new ReplCompiler(ImmutableSeq.empty(), new ThrowingReporter(AyaPrettierOptions.debug()), null);
 
@@ -37,9 +38,12 @@ public class ReplCompilerTest {
 
   @Test public void library() throws IOException {
     compiler.loadToContext(Paths.get("../ide-lsp", "src", "test", "resources", "lsp-test-lib"));
-    assertNotNull(findContext("Nat::Core::zero"));
-    assertNotNull(findContext("VecCore::vnil"));
     assertNotNull(findContext("VecCore:::>"));
+    assertNotNull(findContext("VecCore::vnil"));
+    var zero = assertInstanceOf(CompiledVar.class, findContext("Nat::Core::zero"));
+    assertNotNull(zero);
+    assertEquals("| /* compiled pattern */ ⇒ zero",
+      zero.core().toDoc(AyaPrettierOptions.debug()).commonRender());
 
     // Don't be too harsh on the test lib structure, maybe we will change it
     var rootHints = compiler.getContext().giveMeHint(ImmutableSeq.empty());

From 298eb84deedc29f8c44cd8dc868c91242d6a53b6 Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Sat, 25 Jan 2025 08:28:11 -0500
Subject: [PATCH 11/16] test: this seems wrong

---
 .../src/test/java/org/aya/test/cli/ReplCompilerTest.java    | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/cli-impl/src/test/java/org/aya/test/cli/ReplCompilerTest.java b/cli-impl/src/test/java/org/aya/test/cli/ReplCompilerTest.java
index 96134697f6..5551414f99 100644
--- a/cli-impl/src/test/java/org/aya/test/cli/ReplCompilerTest.java
+++ b/cli-impl/src/test/java/org/aya/test/cli/ReplCompilerTest.java
@@ -43,7 +43,11 @@ public class ReplCompilerTest {
     var zero = assertInstanceOf(CompiledVar.class, findContext("Nat::Core::zero"));
     assertNotNull(zero);
     assertEquals("| /* compiled pattern */ ⇒ zero",
-      zero.core().toDoc(AyaPrettierOptions.debug()).commonRender());
+      zero.core().easyToString());
+
+    var Nat = assertInstanceOf(CompiledVar.class, findContext("Nat::Core::Nat"));
+    assertNotNull(Nat);
+    System.out.println(Nat.core().easyToString());
 
     // Don't be too harsh on the test lib structure, maybe we will change it
     var rootHints = compiler.getContext().giveMeHint(ImmutableSeq.empty());

From d7f8a56a1a786c59584ab499fa88e8deb3dd334c Mon Sep 17 00:00:00 2001
From: HoshinoTented <hoshinotented@qq.com>
Date: Sat, 25 Jan 2025 21:34:02 +0800
Subject: [PATCH 12/16] pretty: try fix something

---
 .../src/main/java/org/aya/prettier/CorePrettier.java  | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

diff --git a/syntax/src/main/java/org/aya/prettier/CorePrettier.java b/syntax/src/main/java/org/aya/prettier/CorePrettier.java
index c2483299ee..fcf74ff1c8 100644
--- a/syntax/src/main/java/org/aya/prettier/CorePrettier.java
+++ b/syntax/src/main/java/org/aya/prettier/CorePrettier.java
@@ -311,7 +311,14 @@ yield visitFn(defVar(def.ref()), def.modifiers(), absTele,
       case JitCon jitCon -> {
         var dummyOwnerArgs = ImmutableSeq.<Term>fill(jitCon.ownerTeleSize(), i -> new FreeTerm(jitCon.telescopeName(i)));
         var rhs = visitConRhs(nameDoc, true && false, jitCon.inst(dummyOwnerArgs));
-        yield Doc.sep(BAR, COMMENT_COMPILED_PATTERN, FN_DEFINED_AS, rhs);
+        var wholeClause = rhs;
+
+        if (jitCon.dataRef().signature().telescopeSize() > 0) {
+          // may have pattern, but we don't know!
+          wholeClause = Doc.sep(COMMENT_COMPILED_PATTERN, FN_DEFINED_AS, rhs);
+        }
+
+        yield Doc.sep(BAR, wholeClause);
       }
       case JitData jitData -> visitData(jitData);
       case JitMember jitMember -> visitMember(nameDoc, jitMember);
@@ -389,7 +396,7 @@ yield visitFn(defVar(def.ref()), def.modifiers(), absTele,
       term(Outer.Free, telescope.result(dataArgs)));
     var consDoc = dataDef.body().view().map(this::def);
 
-    return Doc.cat(line1, Doc.nest(2, Doc.vcat(consDoc)));
+    return Doc.vcat(line1, Doc.nest(2, Doc.vcat(consDoc)));
   }
 
   /// @param telescope the telescope of a [MemberDefLike], including the `self` parameter

From 9f8fabb484b8f5d10479b41aad406c7b8705bba5 Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Sat, 25 Jan 2025 08:46:45 -0500
Subject: [PATCH 13/16] test: why it passes for me?

---
 .../org/aya/test/cli/ReplCompilerTest.java    | 11 +++-
 .../java/org/aya/prettier/BasePrettier.java   | 25 ++++----
 .../java/org/aya/prettier/CorePrettier.java   | 59 +++++++------------
 3 files changed, 40 insertions(+), 55 deletions(-)

diff --git a/cli-impl/src/test/java/org/aya/test/cli/ReplCompilerTest.java b/cli-impl/src/test/java/org/aya/test/cli/ReplCompilerTest.java
index 5551414f99..876d14f7b7 100644
--- a/cli-impl/src/test/java/org/aya/test/cli/ReplCompilerTest.java
+++ b/cli-impl/src/test/java/org/aya/test/cli/ReplCompilerTest.java
@@ -21,6 +21,7 @@
 import org.aya.syntax.ref.AnyVar;
 import org.aya.syntax.ref.CompiledVar;
 import org.aya.syntax.ref.DefVar;
+import org.aya.util.error.Global;
 import org.aya.util.error.SourcePos;
 import org.aya.util.reporter.ThrowingReporter;
 import org.jetbrains.annotations.NotNull;
@@ -34,6 +35,7 @@ public class ReplCompilerTest {
   @BeforeEach public void setup() {
     compiler.getContext().clear();
     compiler.imports.clear();
+    Global.NO_RANDOM_NAME = true;
   }
 
   @Test public void library() throws IOException {
@@ -42,12 +44,15 @@ public class ReplCompilerTest {
     assertNotNull(findContext("VecCore::vnil"));
     var zero = assertInstanceOf(CompiledVar.class, findContext("Nat::Core::zero"));
     assertNotNull(zero);
-    assertEquals("| /* compiled pattern */ ⇒ zero",
-      zero.core().easyToString());
+    assertEquals("| zero", zero.core().easyToString());
 
     var Nat = assertInstanceOf(CompiledVar.class, findContext("Nat::Core::Nat"));
     assertNotNull(Nat);
-    System.out.println(Nat.core().easyToString());
+    assertEquals("""
+      inductive Nat : Type 0
+        | zero
+        | suc (_ : Nat)
+      """.trim(), Nat.core().easyToString());
 
     // Don't be too harsh on the test lib structure, maybe we will change it
     var rootHints = compiler.getContext().giveMeHint(ImmutableSeq.empty());
diff --git a/syntax/src/main/java/org/aya/prettier/BasePrettier.java b/syntax/src/main/java/org/aya/prettier/BasePrettier.java
index 4276da65a1..80cfec1dbc 100644
--- a/syntax/src/main/java/org/aya/prettier/BasePrettier.java
+++ b/syntax/src/main/java/org/aya/prettier/BasePrettier.java
@@ -2,6 +2,12 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.prettier;
 
+import java.util.Objects;
+import java.util.function.BiFunction;
+import java.util.function.ToIntBiFunction;
+
+import static org.aya.prettier.Tokens.KW_PRIM;
+
 import kala.collection.Seq;
 import kala.collection.SeqLike;
 import kala.collection.SeqView;
@@ -30,12 +36,6 @@
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
-import java.util.Objects;
-import java.util.function.BiFunction;
-import java.util.function.ToIntBiFunction;
-
-import static org.aya.prettier.Tokens.KW_PRIM;
-
 public abstract class BasePrettier<Term extends AyaDocile> {
   public static @NotNull Doc coreArgsDoc(@NotNull PrettierOptions options, @NotNull SeqView<? extends AyaDocile> self) {
     return Doc.commaList(self.map(t -> t.toDoc(options)));
@@ -191,11 +191,9 @@ protected static <T extends AyaDocile> Doc arg(@NotNull Fmt<T> fmt, @NotNull Bin
         ? Doc.parened(withEx) : withEx;
   }
 
-  /**
-   * Pretty-print a telescope in a dumb (but conservative) way.
-   *
-   * @see #visitTele(Seq, AyaDocile, Usage)
-   */
+  /// Pretty-print a telescope in a dumb (but conservative) way.
+  ///
+  /// @see #visitTele(Seq, AyaDocile, Usage)
   public @NotNull Doc visitTele(@NotNull Seq<? extends ParamLike<Term>> telescope) {
     return visitTele(telescope, null, (_, _) -> 1);
   }
@@ -211,7 +209,7 @@ protected static <T extends AyaDocile> Doc arg(@NotNull Fmt<T> fmt, @NotNull Bin
    * @param altF7 a function for finding usages.
    * @see #visitTele(Seq)
    */
-  public @NotNull Doc visitTele(
+  public final @NotNull Doc visitTele(
     @NotNull Seq<? extends ParamLike<Term>> telescope,
     @Nullable Term body, @NotNull Usage<Term, LocalVar> altF7
   ) {
@@ -256,8 +254,7 @@ protected static <T extends AyaDocile> Doc arg(@NotNull Fmt<T> fmt, @NotNull Bin
 
   private Doc mutableListNames(MutableList<? extends ParamLike<?>> names, ParamLike<?> param) {
     // We HAVE TO collect the results, since {names} is mutable, therefore {names.view()} becomes mutable.
-    var namesDocs = names.view().map(ParamLike::nameDoc)
-      .toImmutableSeq();
+    var namesDocs = names.map(ParamLike::nameDoc);
     return param.toDoc(Doc.sep(namesDocs), options);
   }
 
diff --git a/syntax/src/main/java/org/aya/prettier/CorePrettier.java b/syntax/src/main/java/org/aya/prettier/CorePrettier.java
index fcf74ff1c8..7eea4c54cf 100644
--- a/syntax/src/main/java/org/aya/prettier/CorePrettier.java
+++ b/syntax/src/main/java/org/aya/prettier/CorePrettier.java
@@ -10,6 +10,7 @@
 import static org.aya.prettier.Tokens.*;
 
 import com.intellij.openapi.util.text.StringUtil;
+import kala.collection.Seq;
 import kala.collection.SeqView;
 import kala.collection.immutable.ImmutableSeq;
 import kala.collection.mutable.FreezableMutableList;
@@ -41,7 +42,6 @@
 import org.aya.syntax.ref.LocalVar;
 import org.aya.syntax.telescope.AbstractTele;
 import org.aya.util.Arg;
-import org.aya.util.error.Panic;
 import org.aya.util.error.SourcePos;
 import org.aya.util.prettier.PrettierOptions;
 import org.jetbrains.annotations.NotNull;
@@ -63,10 +63,9 @@ public class CorePrettier extends BasePrettier<Term> {
     return switch (preterm) {
       case FreeTerm(var var) -> varDoc(var);
       case LocalTerm(var idx) -> Doc.plain("^" + idx);
-      case MetaCall term -> {
-        var name = term.ref();
+      case MetaCall(var name, var args) -> {
         var inner = Doc.cat(Doc.plain("?"), varDoc(name));
-        Function<Outer, Doc> factory = o -> visitCoreApp(null, inner, term.args().view(), o, optionImplicit());
+        Function<Outer, Doc> factory = o -> visitCoreApp(null, inner, args.view(), o, optionImplicit());
         if (options.map.get(AyaPrettierOptions.Key.InlineMetas)) yield factory.apply(outer);
         yield Doc.wrap(HOLE_LEFT, HOLE_RIGHT, factory.apply(Outer.Free));
       }
@@ -80,10 +79,8 @@ public class CorePrettier extends BasePrettier<Term> {
       case IntegerTerm shaped -> shaped.repr() == 0
         ? linkLit(0, shaped.zero(), CON)
         : linkLit(shaped.repr(), shaped.suc(), CON);
-      case ListTerm shaped -> {
-        var subterms = shaped.repr().map(x -> term(Outer.Free, x));
-        var nil = shaped.nil();
-        var cons = shaped.cons();
+      case ListTerm(var repr, var nil, var cons, _) -> {
+        var subterms = repr.map(x -> term(Outer.Free, x));
         yield Doc.sep(
           linkListLit(Doc.symbol("["), nil, CON),
           Doc.join(linkListLit(Doc.COMMA, cons, CON), subterms),
@@ -244,8 +241,7 @@ private ImmutableSeq<Term> visibleArgsOf(Callable call) {
   }
 
   private @NotNull Doc visitAccessHead(@NotNull MemberCall term) {
-    return Doc.cat(term(Outer.ProjHead, term.of()), Doc.symbol("."),
-      refVar(term.ref()));
+    return Doc.cat(term(Outer.ProjHead, term.of()), Doc.symbol("."), refVar(term.ref()));
   }
 
   public @NotNull Doc pat(@NotNull Pat pat, boolean licit, Outer outer) {
@@ -281,10 +277,10 @@ private ImmutableSeq<Term> visibleArgsOf(Callable call) {
         var absTele = TyckDef.defSignature(def);
         yield visitFn(defVar(def.ref()), def.modifiers(), absTele,
           (prefix, subst) -> switch (def.body()) {
-          case Either.Left(var term) -> Doc.sep(prefix, FN_DEFINED_AS, term(Outer.Free, term.instTele(subst.view())));
-          case Either.Right(var body) -> Doc.vcat(prefix,
-            Doc.nest(2, visitClauses(body.matchingsView(), def.telescope().view().map(Param::explicit))));
-        });
+            case Either.Left(var term) -> Doc.sep(prefix, FN_DEFINED_AS, term(Outer.Free, term.instTele(subst.view())));
+            case Either.Right(var body) -> Doc.vcat(prefix,
+              Doc.nest(2, visitClauses(body.matchingsView(), def.telescope().view().map(Param::explicit))));
+          });
       }
       case MemberDef field -> visitMember(defVar(field.ref()), TyckDef.defSignature(field));
       case ConDef con -> visitCon(con.ref, con.coerce, con.selfTele);
@@ -297,10 +293,13 @@ yield visitFn(defVar(def.ref()), def.modifiers(), absTele,
     return switch (unit) {
       case JitDef jitDef -> def(jitDef);
       case TyckAnyDef<?> tyckAnyDef -> def(tyckAnyDef.ref.core);
-      default -> Panic.unreachable();
     };
   }
 
+  @Override public @NotNull Doc visitTele(@NotNull Seq<? extends ParamLike<Term>> telescope) {
+    return visitTele(telescope, null, FindUsage::free);
+  }
+
   public @NotNull Doc def(@NotNull JitDef unit) {
     var dummyVar = new CompiledVar(unit);
     var nameDoc = defVar(dummyVar);
@@ -310,7 +309,7 @@ yield visitFn(defVar(def.ref()), def.modifiers(), absTele,
         Doc.sep(prefix, FN_DEFINED_AS, COMMENT_COMPILED_CODE));
       case JitCon jitCon -> {
         var dummyOwnerArgs = ImmutableSeq.<Term>fill(jitCon.ownerTeleSize(), i -> new FreeTerm(jitCon.telescopeName(i)));
-        var rhs = visitConRhs(nameDoc, true && false, jitCon.inst(dummyOwnerArgs));
+        var rhs = visitConRhs(nameDoc, false, jitCon.inst(dummyOwnerArgs));
         var wholeClause = rhs;
 
         if (jitCon.dataRef().signature().telescopeSize() > 0) {
@@ -339,7 +338,6 @@ yield visitFn(defVar(def.ref()), def.modifiers(), absTele,
 
     var tele = enrich(telescope);
     line1.append(visitTele(tele));
-
     line1.append(HAS_TYPE);
 
     var subst = tele.<Term>map(x -> new FreeTerm(x.ref()));
@@ -350,11 +348,7 @@ yield visitFn(defVar(def.ref()), def.modifiers(), absTele,
   }
 
   /// @param selfTele self tele of the constructor, unlike [JitCon], the data args/owner args should be supplied.
-  private @NotNull Doc visitConRhs(
-    @NotNull Doc name,
-    boolean coerce,
-    @NotNull AbstractTele selfTele
-  ) {
+  private @NotNull Doc visitConRhs(@NotNull Doc name, boolean coerce, @NotNull AbstractTele selfTele) {
     return Doc.sepNonEmpty(coe(coerce), name, visitTele(enrich(selfTele)));
   }
 
@@ -381,16 +375,13 @@ yield visitFn(defVar(def.ref()), def.modifiers(), absTele,
     }
   }
 
-  private @NotNull Doc visitData(
-    @NotNull DataDefLike dataDef
-  ) {
+  private @NotNull Doc visitData(@NotNull DataDefLike dataDef) {
     var name = defVar(AnyDef.toVar(dataDef));
     var telescope = dataDef.signature();
     var richDataTele = enrich(telescope);
     var dataArgs = richDataTele.<Term>map(t -> new FreeTerm(t.ref()));
 
-    var line1 = Doc.sepNonEmpty(KW_DATA,
-      name,
+    var line1 = Doc.sepNonEmpty(KW_DATA, name,
       visitTele(richDataTele),
       HAS_TYPE,
       term(Outer.Free, telescope.result(dataArgs)));
@@ -400,10 +391,7 @@ yield visitFn(defVar(def.ref()), def.modifiers(), absTele,
   }
 
   /// @param telescope the telescope of a [MemberDefLike], including the `self` parameter
-  private @NotNull Doc visitMember(
-    @NotNull Doc name,
-    @NotNull AbstractTele telescope
-  ) {
+  private @NotNull Doc visitMember(@NotNull Doc name, @NotNull AbstractTele telescope) {
     // TODO: should we pretty print the `self` parameter?
     //       The use of `self` parameter still appears in other parameters.
     var visitTele = visitTele(telescope);
@@ -411,10 +399,7 @@ yield visitFn(defVar(def.ref()), def.modifiers(), absTele,
     return Doc.sepNonEmpty(BAR, name, visitTele.tele, HAS_TYPE, visitTele.result.get());
   }
 
-  private @NotNull Doc visitClass(
-    @NotNull Doc name,
-    @NotNull SeqView<Doc> members
-  ) {
+  private @NotNull Doc visitClass(@NotNull Doc name, @NotNull SeqView<Doc> members) {
     return Doc.sepNonEmpty(KW_CLASS, name, Doc.nest(2, Doc.vcat(members)));
   }
 
@@ -449,9 +434,7 @@ yield visitFn(defVar(def.ref()), def.modifiers(), absTele,
     var richTele = FreezableMutableList.<ParamLike<Term>>create();
 
     for (var i = 0; i < tele.telescopeSize(); ++i) {
-      var binds = richTele.view()
-        .<Term>map(x -> new FreeTerm(x.ref()))
-        .toImmutableSeq();
+      var binds = richTele.<Term>map(x -> new FreeTerm(x.ref()));
       var type = tele.telescope(i, binds);
       richTele.append(new RichParam(
         new LocalVar(tele.telescopeName(i), SourcePos.NONE, Basic.Pretty),

From 042360141c5926420c3c9ba0936ff3a595dbbca4 Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Sat, 25 Jan 2025 08:51:49 -0500
Subject: [PATCH 14/16] test: also test fn

---
 .../src/test/java/org/aya/test/cli/ReplCompilerTest.java     | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/cli-impl/src/test/java/org/aya/test/cli/ReplCompilerTest.java b/cli-impl/src/test/java/org/aya/test/cli/ReplCompilerTest.java
index 876d14f7b7..598e8dfbd9 100644
--- a/cli-impl/src/test/java/org/aya/test/cli/ReplCompilerTest.java
+++ b/cli-impl/src/test/java/org/aya/test/cli/ReplCompilerTest.java
@@ -54,6 +54,11 @@ public class ReplCompilerTest {
         | suc (_ : Nat)
       """.trim(), Nat.core().easyToString());
 
+    var refl = assertInstanceOf(CompiledVar.class, findContext("Path::refl"));
+    assertNotNull(refl);
+    assertEquals("def refl {A : Type 0} {a : A} : a = a => /* compiled code */",
+      refl.core().easyToString());
+
     // Don't be too harsh on the test lib structure, maybe we will change it
     var rootHints = compiler.getContext().giveMeHint(ImmutableSeq.empty());
     assertTrue(rootHints.contains("Nat"));

From 2e9813dd7eed2e91fe73c9b16330f59f58a18878 Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Sat, 25 Jan 2025 08:56:16 -0500
Subject: [PATCH 15/16] test: also test compiled patterns

---
 .../src/test/java/org/aya/test/cli/ReplCompilerTest.java    | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/cli-impl/src/test/java/org/aya/test/cli/ReplCompilerTest.java b/cli-impl/src/test/java/org/aya/test/cli/ReplCompilerTest.java
index 598e8dfbd9..4cd32a4477 100644
--- a/cli-impl/src/test/java/org/aya/test/cli/ReplCompilerTest.java
+++ b/cli-impl/src/test/java/org/aya/test/cli/ReplCompilerTest.java
@@ -41,7 +41,11 @@ public class ReplCompilerTest {
   @Test public void library() throws IOException {
     compiler.loadToContext(Paths.get("../ide-lsp", "src", "test", "resources", "lsp-test-lib"));
     assertNotNull(findContext("VecCore:::>"));
-    assertNotNull(findContext("VecCore::vnil"));
+
+    var vnil = assertInstanceOf(CompiledVar.class, findContext("VecCore::vnil"));
+    assertNotNull(vnil);
+    assertEquals("| /* compiled pattern */ => vnil", vnil.core().easyToString());
+
     var zero = assertInstanceOf(CompiledVar.class, findContext("Nat::Core::zero"));
     assertNotNull(zero);
     assertEquals("| zero", zero.core().easyToString());

From 90bf168e0772e1e391e338529c6b267b5ef891fa Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Sat, 25 Jan 2025 09:00:13 -0500
Subject: [PATCH 16/16] misc: refactor, optimize imports

---
 .../src/main/java/org/aya/syntax/compile/JitDef.java |  3 +--
 .../src/main/java/org/aya/syntax/compile/JitFn.java  | 12 +++---------
 .../src/main/java/org/aya/syntax/core/RichParam.java |  2 --
 3 files changed, 4 insertions(+), 13 deletions(-)

diff --git a/syntax/src/main/java/org/aya/syntax/compile/JitDef.java b/syntax/src/main/java/org/aya/syntax/compile/JitDef.java
index 075f152426..2071ff8809 100644
--- a/syntax/src/main/java/org/aya/syntax/compile/JitDef.java
+++ b/syntax/src/main/java/org/aya/syntax/compile/JitDef.java
@@ -37,8 +37,7 @@ public abstract sealed class JitDef extends JitUnit implements AnyDef, AyaDocile
 
   @Override public abstract @NotNull JitTele signature();
 
-  @Override
-  public @NotNull Doc toDoc(@NotNull PrettierOptions options) {
+  @Override public @NotNull Doc toDoc(@NotNull PrettierOptions options) {
     return new CorePrettier(options).def(this);
   }
 }
diff --git a/syntax/src/main/java/org/aya/syntax/compile/JitFn.java b/syntax/src/main/java/org/aya/syntax/compile/JitFn.java
index e11ded5c37..e25147efbc 100644
--- a/syntax/src/main/java/org/aya/syntax/compile/JitFn.java
+++ b/syntax/src/main/java/org/aya/syntax/compile/JitFn.java
@@ -2,6 +2,8 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.syntax.compile;
 
+import java.util.EnumSet;
+
 import kala.collection.Seq;
 import org.aya.generic.Modifier;
 import org.aya.syntax.core.def.FnDefLike;
@@ -9,8 +11,6 @@
 import org.aya.syntax.telescope.JitTele;
 import org.jetbrains.annotations.NotNull;
 
-import java.util.EnumSet;
-
 public abstract non-sealed class JitFn extends JitTele implements FnDefLike {
   public final int modifiers;
 
@@ -29,13 +29,7 @@ protected JitFn(int telescopeSize, boolean[] telescopeLicit, String[] telescopeN
 
   public @NotNull EnumSet<Modifier> modifiers() {
     var set = EnumSet.noneOf(Modifier.class);
-
-    for (var modi : Modifier.values()) {
-      if (is(modi)) {
-        set.add(modi);
-      }
-    }
-
+    for (var modi : Modifier.values()) if (is(modi)) set.add(modi);
     return set;
   }
 }
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 92d72831c3..78d97ec54f 100644
--- a/syntax/src/main/java/org/aya/syntax/core/RichParam.java
+++ b/syntax/src/main/java/org/aya/syntax/core/RichParam.java
@@ -2,8 +2,6 @@
 // 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;
 
-import kala.collection.SeqView;
-import kala.collection.immutable.ImmutableSeq;
 import org.aya.generic.term.ParamLike;
 import org.aya.syntax.core.term.FreeTerm;
 import org.aya.syntax.core.term.Param;