merge: Pretty print JIT-compiled telescope (#1286)

aya-prover · Jan 25, 2025 · d9d2d54 · d9d2d54
2 parents 0830357 + 90bf168
commit d9d2d54
Show file tree

Hide file tree

Showing 18 changed files with 280 additions and 158 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
@@ -1,7 +1,11 @@
-// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2025 Tesla (Yinsen) Zhang.
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.cli.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;
@@ -13,6 +17,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;
@@ -22,10 +27,6 @@
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
-import java.io.IOException;
-import java.nio.file.Files;
-import java.nio.file.Path;
-
 public interface ReplCommands {
   record Code(@NotNull String code) { }
   record Prompt(@NotNull String prompt) { }
@@ -65,10 +66,11 @@ 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);
-      }
-      return Command.Result.ok(topLevel.name(), true);      // TODO: pretty print
+
+      return new Result(Output.stdout((switch (topLevel) {
+        case JitDef jitDef -> repl.render(jitDef);
+        case TyckAnyDef<?> tyckDef -> repl.render(tyckDef.core());
+      })), true);
     }
   };
 
@@ -82,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("=>"),
@@ -98,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);
     }
   };
 
@@ -118,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/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,33 +19,50 @@
 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.Global;
 import org.aya.util.error.SourcePos;
 import org.aya.util.reporter.ThrowingReporter;
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 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);
 
   @BeforeEach public void setup() {
     compiler.getContext().clear();
     compiler.imports.clear();
+    Global.NO_RANDOM_NAME = true;
   }
 
   @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:::>"));
 
+    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());
+
+    var Nat = assertInstanceOf(CompiledVar.class, findContext("Nat::Core::Nat"));
+    assertNotNull(Nat);
+    assertEquals("""
+      inductive Nat : Type 0
+        | zero
+        | 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"));

diff --git 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/syntax/src/main/java/org/aya/prettier/BasePrettier.java b/syntax/src/main/java/org/aya/prettier/BasePrettier.java
@@ -1,7 +1,13 @@
-// 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;
 
+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);
   }
 
@@ -281,7 +278,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));
   }