merge: Implement :case-tree in repl (#1287)

![image](https://github.com/user-attachments/assets/d9a53cf6-154c-4952-88e1-8ede61592370)

Author: ice1000

Diff for: cli-console/src/main/java/org/aya/cli/repl/AyaRepl.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.cli.repl;
 
+import java.io.Closeable;
+import java.io.IOException;
+import java.nio.file.Path;
+import java.nio.file.Paths;
+
 import kala.collection.immutable.ImmutableSeq;
 import kala.control.Either;
 import org.aya.cli.console.AnsiReporter;
@@ -19,15 +24,11 @@
 import org.aya.syntax.core.def.TopLevelDef;
 import org.aya.syntax.literate.CodeOptions;
 import org.aya.util.reporter.Problem;
+import org.jetbrains.annotations.Contract;
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 import org.jline.builtins.Completers;
 
-import java.io.Closeable;
-import java.io.IOException;
-import java.nio.file.Path;
-import java.nio.file.Paths;
-
 public abstract class AyaRepl implements Closeable, Runnable, Repl {
   public static int start(
     @NotNull ImmutableSeq<Path> modulePaths,
@@ -81,6 +82,7 @@ public CommandManager makeCommand() {
       ReplCommands.CHANGE_NORM_MODE,
       ReplCommands.TOGGLE_PRETTY,
       ReplCommands.SHOW_TYPE,
+      ReplCommands.SHOW_MCT,
       ReplCommands.SHOW_INFO,
       ReplCommands.SHOW_PARSE_TREE,
       ReplCommands.CHANGE_PP_WIDTH,
@@ -150,11 +152,11 @@ private boolean singleLoop() {
     ));
   }
 
-  public @NotNull Doc render(@NotNull AyaDocile ayaDocile) {
+  @Contract(pure = true) public @NotNull Doc render(@NotNull AyaDocile ayaDocile) {
     return ayaDocile.toDoc(prettierOptions());
   }
 
-  public @NotNull AyaPrettierOptions prettierOptions() {
+  @Contract(pure = true) public @NotNull AyaPrettierOptions prettierOptions() {
     return config.literatePrettier.prettierOptions;
   }
 

Diff for: cli-console/src/main/java/org/aya/cli/repl/ReplCommands.java

@@ -18,12 +18,10 @@
 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.aya.syntax.ref.DefVar;
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
@@ -54,6 +52,21 @@ record StyleParam(@NotNull Either<RenderOptions.StyleFamilyName, Path> value)
     }
   };
 
+  @NotNull Command SHOW_MCT = new Command(ImmutableSeq.of("case-tree"), "Show the case tree of a pattern-matching function") {
+    @Entry public @NotNull Command.Result execute(@NotNull AyaRepl repl, @NotNull Code code) {
+      var resolved = repl.replCompiler.parseToAnyVar(code.code);
+      if (!(resolved instanceof AnyDefVar anyDefVar)) return Result.err("Not a valid reference", true);
+      if (!(anyDefVar instanceof DefVar<?, ?> defVar)) return Result.err("JIT-compiled defs are unsupported", true);
+      if (!(defVar.core instanceof FnDef fn)) return Result.err("Not a function", true);
+      if (!(fn.body() instanceof Either.Right(var body))) return Result.err("Not a pattern-matching function", true);
+      var classes = body.classes.map(cl ->
+        Doc.sep(Doc.commaList(cl.term().view().map(t -> t.toDoc(repl.prettierOptions()))),
+          Doc.symbol("=>"),
+          Doc.commaList(cl.cls().mapToObj(Doc::ordinal))));
+      return new Result(Output.stdout(Doc.vcat(classes)), true);
+    }
+  };
+
   @NotNull Command SHOW_INFO = new Command(ImmutableSeq.of("info"), "Show the information of the given definition") {
     @Entry public @NotNull Command.Result execute(@NotNull AyaRepl repl, @NotNull Code code) {
       var resolved = repl.replCompiler.parseToAnyVar(code.code);

Diff for: syntax/src/main/java/org/aya/prettier/BasePrettier.java

@@ -222,10 +222,10 @@ protected static <T extends AyaDocile> Doc arg(@NotNull Fmt<T> fmt, @NotNull Bin
     for (int i = 1; i < telescope.size(); i++) {
       var param = telescope.get(i);
       if (!Objects.equals(param.type(), last.type())) {
-        if (body != null && names.sizeEquals(1)) {
+        if (names.sizeEquals(1)) {
           var ref = names.getFirst();
-          var used = telescope.sliceView(i, telescope.size())
-            .map(ParamLike::type).appended(body)
+          var prefix = telescope.sliceView(i, telescope.size()).map(ParamLike::type);
+          var used = (body == null ? prefix : prefix.appended(body))
             .anyMatch(p -> altF7.applyAsInt(p, ref.ref()) > 0);
           // We omit the name if there is no usage.
           if (!used) buf.append(justType(last, Outer.ProjHead));

Diff for: syntax/src/main/java/org/aya/prettier/CorePrettier.java

@@ -220,7 +220,7 @@ case MatchCall(JitMatchy _, var discriminant, _) -> {
   private @NotNull Doc visitDT(@NotNull Outer outer, DepTypeTerm.UnpiNamed pair, Doc kw, Doc operator) {
     var params = pair.names().zip(pair.params(), RichParam::ofExplicit);
     var body = pair.body().instTeleVar(params.view().map(ParamLike::ref));
-    var teleDoc = visitTele(params, body, FindUsage::free);
+    var teleDoc = visitTele(params, body);
     var cod = term(Outer.Codomain, body);
     var doc = Doc.sep(kw, teleDoc, operator, cod);
     pair.names().forEach(nameGen::unbindName);
@@ -296,8 +296,8 @@ yield visitFn(defVar(def.ref()), def.modifiers(), absTele,
     };
   }
 
-  @Override public @NotNull Doc visitTele(@NotNull Seq<? extends ParamLike<Term>> telescope) {
-    return visitTele(telescope, null, FindUsage::free);
+  public @NotNull Doc visitTele(@NotNull Seq<? extends ParamLike<Term>> telescope, @Nullable Term body) {
+    return visitTele(telescope, body, FindUsage::free);
   }
 
   public @NotNull Doc def(@NotNull JitDef unit) {
@@ -337,19 +337,20 @@ yield visitFn(defVar(def.ref()), def.modifiers(), absTele,
     line1.append(name);
 
     var tele = enrich(telescope);
+    var subst = tele.<Term>map(x -> new FreeTerm(x.ref()));
+    var result = telescope.result(subst);
+
     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)));
+    line1.append(term(Outer.Free, result));
 
     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)));
+    return Doc.sepNonEmpty(coe(coerce), name, visitTele(enrich(selfTele), null));
   }
 
   private @NotNull Doc visitCon(
@@ -382,7 +383,7 @@ yield visitFn(defVar(def.ref()), def.modifiers(), absTele,
     var dataArgs = richDataTele.<Term>map(t -> new FreeTerm(t.ref()));
 
     var line1 = Doc.sepNonEmpty(KW_DATA, name,
-      visitTele(richDataTele),
+      visitTele(richDataTele, null),
       HAS_TYPE,
       term(Outer.Free, telescope.result(dataArgs)));
     var consDoc = dataDef.body().view().map(this::def);
@@ -454,7 +455,7 @@ record VisitTele(@NotNull Doc tele, @NotNull LazyValue<Doc> result) { }
 
   private @NotNull VisitTele visitTele(@NotNull AbstractTele tele) {
     var richTele = enrich(tele);
-    var teleDoc = visitTele(richTele);
+    var teleDoc = visitTele(richTele, null);
 
     return new VisitTele(teleDoc, LazyValue.of(() -> {
       var binds = richTele.<Term>map(x -> new FreeTerm(x.ref()));