test: why it passes for me?

Author: ice1000

Diff for: 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 for: 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 for: 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,21 +391,15 @@ 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);
 
     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),