merge: #1005

1005: Aya quality fake literate r=ice1000 a=ice1000 Fix #1004 bors r+ Co-authored-by: ice1000 <ice1000kotlin@foxmail.com>
aya-prover · Oct 30, 2023 · 28b96b4 · 28b96b4
2 parents e9f0854 + 77299a1
commit 28b96b4
Show file tree

Hide file tree

Showing 26 changed files with 690 additions and 142 deletions.
diff --git a/.gitignore b/.gitignore
@@ -17,9 +17,7 @@ gradle.properties
 local.properties
 .DS_Store
 lombok.config
-/test.aya
-/test.aya.md
-/test.html
+/test.*
 /highlight-hover.js
 
 /cli-*-all.jar

diff --git a/...rg/aya/literate/FaithfulPrettierTest.java → ...iterate/LiterateFaithfulPrettierTest.java b/...rg/aya/literate/FaithfulPrettierTest.java → ...iterate/LiterateFaithfulPrettierTest.java
@@ -4,7 +4,7 @@
 
 import kala.collection.immutable.ImmutableSeq;
 import kala.control.Option;
-import org.aya.cli.literate.FaithfulPrettier;
+import org.aya.cli.literate.LiterateFaithfulPrettier;
 import org.aya.cli.literate.SyntaxHighlight;
 import org.aya.cli.parse.AyaParserImpl;
 import org.aya.prettier.AyaPrettierOptions;
@@ -20,7 +20,7 @@
 import java.io.IOException;
 import java.nio.file.Files;
 
-public class FaithfulPrettierTest {
+public class LiterateFaithfulPrettierTest {
   @Test public void test() throws IOException {
     var reporter = AyaThrowingReporter.INSTANCE;
 
@@ -37,7 +37,7 @@ public class FaithfulPrettierTest {
     var highlights = SyntaxHighlight.highlight(null, Option.some(sourceFile), stmts);
     var mockPos = new SourcePos(sourceFile, 0, sourceFile.sourceCode().length() - 1, // <- tokenEndIndex is inclusive
       -1, -1, -1, -1);
-    var doc = new FaithfulPrettier(ImmutableSeq.empty(), highlights, AyaPrettierOptions.pretty())
+    var doc = new LiterateFaithfulPrettier(ImmutableSeq.empty(), highlights, AyaPrettierOptions.pretty())
       .highlight(sourceFile.sourceCode(), mockPos);
     var output = Doc.codeBlock(Language.Builtin.Aya, doc).renderToHtml(true);
     Files.writeString(root.resolve(outputFileName), output);

diff --git a/cli-console/src/main/java/org/aya/cli/console/Main.java b/cli-console/src/main/java/org/aya/cli/console/Main.java
@@ -5,6 +5,8 @@
 import org.aya.cli.interactive.ReplConfig;
 import org.aya.cli.library.LibraryCompiler;
 import org.aya.cli.library.incremental.CompilerAdvisor;
+import org.aya.cli.literate.FlclFaithfulPrettier;
+import org.aya.cli.parse.FlclParser;
 import org.aya.cli.plct.PLCTReport;
 import org.aya.cli.render.RenderOptions;
 import org.aya.cli.repl.AyaRepl;
@@ -14,10 +16,13 @@
 import org.aya.pretty.printer.PrinterConfig;
 import org.aya.tyck.trace.MarkdownTrace;
 import org.aya.tyck.trace.Trace;
+import org.aya.util.error.SourceFile;
+import org.aya.util.error.SourceFileLocator;
 import org.jetbrains.annotations.NotNull;
 import picocli.CommandLine;
 
 import java.io.IOException;
+import java.nio.charset.StandardCharsets;
 import java.nio.file.Files;
 import java.nio.file.Paths;
 import java.util.concurrent.Callable;
@@ -36,10 +41,29 @@ public static void main(String... args) {
       return AyaRepl.start(modulePaths().map(Paths::get), action.repl);
     if (action.plct != null)
       return new PLCTReport().run(action.plct);
+    if (action.flcl != null)
+      return doFakeLiterate(action.flcl.fakeLiterate);
     assert action.compile != null;
     return doCompile(action.compile);
   }
 
+  private int doFakeLiterate(String filePath) throws IOException {
+    var replConfig = ReplConfig.loadFromDefault();
+    var prettierOptions = replConfig.literatePrettier.prettierOptions;
+    var reporter = AnsiReporter.stdio(!asciiOnly, prettierOptions, verbosity);
+    var renderOptions = createRenderOptions(replConfig);
+    replConfig.close();
+    var path = Paths.get(filePath);
+    var file = SourceFile.from(SourceFileLocator.EMPTY, path);
+    var doc = new FlclFaithfulPrettier(prettierOptions).highlight(
+      new FlclParser(reporter, file).computeAst());
+    // Garbage code
+    var setup = new RenderOptions.DefaultSetup(false, false, true, true, -1, false);
+    var output = renderOptions.render(RenderOptions.OutputTarget.LaTeX, doc, setup);
+    Files.writeString(Paths.get("a.out"), output, StandardCharsets.UTF_8);
+    return 0;
+  }
+
   private int doCompile(@NotNull CompileAction compile) throws IOException {
     var message = asciiOnly
       ? CompilerFlags.Message.ASCII
@@ -51,12 +75,7 @@ private int doCompile(@NotNull CompileAction compile) throws IOException {
     var replConfig = ReplConfig.loadFromDefault();
     var prettierOptions = replConfig.literatePrettier.prettierOptions;
     var reporter = AnsiReporter.stdio(!asciiOnly, prettierOptions, verbosity);
-    var renderOptions = replConfig.literatePrettier.renderOptions;
-    switch (prettyColor) {
-      case emacs -> renderOptions.colorScheme = RenderOptions.ColorSchemeName.Emacs;
-      case intellij -> renderOptions.colorScheme = RenderOptions.ColorSchemeName.IntelliJ;
-      case null -> {}
-    }
+    var renderOptions = createRenderOptions(replConfig);
     replConfig.close();
     var pretty = prettyStage == null
       ? (outputPath != null ? CompilerFlags.prettyInfoFromOutput(
@@ -94,4 +113,14 @@ private int doCompile(@NotNull CompileAction compile) throws IOException {
         .docify(traceBuilder).renderToString(PrinterConfig.INFINITE_SIZE, !asciiOnly));
     return status;
   }
+
+  private @NotNull RenderOptions createRenderOptions(@NotNull ReplConfig replConfig) {
+    var renderOptions = replConfig.literatePrettier.renderOptions;
+    switch (prettyColor) {
+      case emacs -> renderOptions.colorScheme = RenderOptions.ColorSchemeName.Emacs;
+      case intellij -> renderOptions.colorScheme = RenderOptions.ColorSchemeName.IntelliJ;
+      case null -> {}
+    }
+    return renderOptions;
+  }
 }
diff --git a/cli-console/src/main/java/org/aya/cli/console/MainArgs.java b/cli-console/src/main/java/org/aya/cli/console/MainArgs.java
@@ -60,6 +60,12 @@ public static class PlctAction {
     public String repoName;
   }
 
+  public static class LiterateAction {
+    @Option(names = {"--fake-literate"}, paramLabel = "<input-file>",
+      description = "Generate fake language literate output from this file")
+    public String fakeLiterate;
+  }
+
   /** Either `repl` or `compile` is not null */
   public static class Action {
     @CommandLine.ArgGroup(heading = "REPL arguments:%n", exclusive = false)
@@ -70,6 +76,9 @@ public static class Action {
 
     @CommandLine.ArgGroup(heading = "PLCT report arguments:%n", exclusive = false)
     public @Nullable PlctAction plct;
+
+    @CommandLine.ArgGroup(heading = "Aya-quality highlighting tools:%n", exclusive = false)
+    public @Nullable LiterateAction flcl;
   }
 
   @Option(names = {"--interrupted-trace"}, hidden = true)

diff --git a/cli-impl/src/main/java/org/aya/cli/literate/FaithfulPrettier.java b/cli-impl/src/main/java/org/aya/cli/literate/FaithfulPrettier.java
@@ -7,50 +7,19 @@
 import kala.collection.immutable.ImmutableSeq;
 import kala.collection.mutable.MutableList;
 import kala.text.StringSlice;
-import org.aya.cli.utils.InlineHintProblem;
-import org.aya.concrete.remark.AyaLiterate;
 import org.aya.generic.AyaDocile;
-import org.aya.literate.Literate;
-import org.aya.literate.LiterateConsumer;
 import org.aya.prettier.BasePrettier;
 import org.aya.pretty.doc.Doc;
 import org.aya.pretty.doc.Language;
 import org.aya.util.error.SourcePos;
 import org.aya.util.prettier.PrettierOptions;
-import org.aya.util.reporter.Problem;
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
-/**
- * This prettier maintains all highlights created from {@link SyntaxHighlight} and all
- * problems reported by Aya compiler.
- * Implementation-wise, this prettier can be seen as a highlight server for a single file.
- * <p>
- * When the highlight of a code block is requested, it filters out
- * all highlights and problems that belong to the code block, and then
- * build a {@link Doc} containing the highlighted source code mixed with compiler
- * outputs, as done in {@link #highlight(String, SourcePos)}.
- *
- * @param problems   All problems of a single file
- * @param highlights All highlights of a single file
- */
-public record FaithfulPrettier(
-  @NotNull ImmutableSeq<Problem> problems,
-  @NotNull ImmutableSeq<HighlightInfo> highlights,
-  @NotNull PrettierOptions options
-) implements LiterateConsumer {
-
-  /**
-   * Highlight all visible aya code blocks
-   */
-  @Override public void accept(@NotNull Literate literate) {
-    if (literate instanceof AyaLiterate.AyaVisibleCodeBlock code && code.sourcePos != null) {
-      code.highlighted = highlight(code.code, code.sourcePos);
-    }
-    LiterateConsumer.super.accept(literate);
-  }
+public interface FaithfulPrettier {
+  @NotNull PrettierOptions options();
 
-  private static void checkHighlights(@NotNull ImmutableSeq<HighlightInfo> highlights) {
+  static void checkHighlights(@NotNull ImmutableSeq<HighlightInfo> highlights) {
     highlights.foldLeft(-1, (lastEndIndex, h) -> {
       var sp = h.sourcePos();
       if (!(sp.tokenStartIndex() <= sp.tokenEndIndex()))
@@ -61,50 +30,19 @@ private static void checkHighlights(@NotNull ImmutableSeq<HighlightInfo> highlig
     });
   }
 
-  /** find highlights and problems inside the code range, and merge them as new highlights */
-  private static @NotNull ImmutableSeq<HighlightInfo> merge(
-    @NotNull SourcePos codeRange,
-    @NotNull PrettierOptions options,
-    @NotNull ImmutableSeq<HighlightInfo> highlights,
-    @NotNull ImmutableSeq<Problem> problems
-  ) {
+  static @NotNull ImmutableSeq<HighlightInfo>
+  highlightsInRange(@NotNull SourcePos codeRange, @NotNull ImmutableSeq<HighlightInfo> highlights) {
     var highlightInRange = highlights.view()
       .filter(h -> h.sourcePos() != SourcePos.NONE)
       .filterNot(h -> h.sourcePos().isEmpty())
       .filter(x -> codeRange.containsIndex(x.sourcePos()))
       .sorted().distinct()
       .toImmutableSeq();
     checkHighlights(highlightInRange);
-
-    var problemsInRange = problems.view()
-      .filter(p -> codeRange.containsIndex(p.sourcePos()))
-      .flatMap(p -> InlineHintProblem.withInlineHints(p, options))
-      .distinct()
-      .toImmutableSeq();
-
-    return problemsInRange.foldLeft(highlightInRange, (acc, p) -> {
-      var partition = acc.partition(
-        h -> p.sourcePos().containsIndex(h.sourcePos()));
-      var inP = partition.component1().sorted();
-      var wrap = new HighlightInfo.Err(p, inP);
-      return partition.component2().appended(wrap);
-    });
-  }
-
-  /**
-   * Apply highlights to source code string.
-   *
-   * @param raw       the source code
-   * @param codeRange where the raw start from (the 'raw' might be a piece of the source code,
-   *                  so it probably not starts from 0).
-   */
-  public @NotNull Doc highlight(@NotNull String raw, @NotNull SourcePos codeRange) {
-    var merged = merge(codeRange, options, highlights, problems).sorted();
-    checkHighlights(merged);
-    return doHighlight(StringSlice.of(raw), codeRange.tokenStartIndex(), merged);
+    return highlightInRange;
   }
 
-  private @NotNull Doc doHighlight(@NotNull StringSlice raw, int base, @NotNull ImmutableSeq<HighlightInfo> highlights) {
+  default @NotNull Doc doHighlight(@NotNull StringSlice raw, int base, @NotNull ImmutableSeq<HighlightInfo> highlights) {
     var docs = MutableList.<Doc>create();
 
     for (var current : highlights) {
@@ -146,7 +84,7 @@ private static void checkHighlights(@NotNull ImmutableSeq<HighlightInfo> highlig
         };
         yield style == null ? doc : new Doc.Tooltip(Doc.styled(style, doc), () -> Doc.codeBlock(
           Language.Builtin.Aya,
-          err.problem().brief(options).toDoc()
+          err.problem().brief(options()).toDoc()
         ));
       }
     };
@@ -157,7 +95,7 @@ private static void checkHighlights(@NotNull ImmutableSeq<HighlightInfo> highlig
     return term.toDoc(options()).commonRender();
   }
 
-  private @NotNull Doc highlightVar(@NotNull String raw, @NotNull HighlightInfo.DefKind defKind) {
+  private static @NotNull Doc highlightVar(@NotNull String raw, @NotNull HighlightInfo.DefKind defKind) {
     var style = switch (defKind) {
       case Data -> BasePrettier.DATA;
       case Con -> BasePrettier.CON;
@@ -172,7 +110,7 @@ private static void checkHighlights(@NotNull ImmutableSeq<HighlightInfo> highlig
     return style != null ? Doc.styled(style, raw) : Doc.plain(raw);
   }
 
-  private @NotNull Doc highlightLit(@NotNull String raw, @NotNull HighlightInfo.LitKind litKind) {
+  private static @NotNull Doc highlightLit(@NotNull String raw, @NotNull HighlightInfo.LitKind litKind) {
     return switch (litKind) {
       case Int, Whitespace -> Doc.plain(raw);
       case String -> Doc.plain(StringUtil.escapeStringCharacters(raw));

diff --git a/cli-impl/src/main/java/org/aya/cli/literate/FlclFaithfulPrettier.java b/cli-impl/src/main/java/org/aya/cli/literate/FlclFaithfulPrettier.java
@@ -0,0 +1,16 @@
+// Copyright (c) 2020-2023 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.literate;
+
+import org.aya.pretty.doc.Doc;
+import org.aya.util.prettier.PrettierOptions;
+import org.jetbrains.annotations.NotNull;
+
+public record FlclFaithfulPrettier(@Override @NotNull PrettierOptions options)
+  implements FaithfulPrettier {
+  public @NotNull Doc highlight(@NotNull FlclToken.File file) {
+    var highlights = file.tokens().map(FlclToken::toInfo).sorted();
+    FaithfulPrettier.checkHighlights(highlights);
+    return doHighlight(file.sourceCode(), file.startIndex(), highlights);
+  }
+}
diff --git a/cli-impl/src/main/java/org/aya/cli/literate/FlclToken.java b/cli-impl/src/main/java/org/aya/cli/literate/FlclToken.java
@@ -0,0 +1,42 @@
+// Copyright (c) 2020-2023 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.literate;
+
+import kala.collection.immutable.ImmutableSeq;
+import kala.text.StringSlice;
+import org.aya.pretty.doc.Link;
+import org.aya.util.error.SourcePos;
+import org.jetbrains.annotations.NotNull;
+
+public record FlclToken(
+  @NotNull SourcePos range,
+  @NotNull Type type
+) {
+  public static final @NotNull Link EMPTY_LINK = Link.page("");
+
+  public record File(
+    @NotNull ImmutableSeq<FlclToken> tokens,
+    @NotNull StringSlice sourceCode,
+    int startIndex
+  ) {}
+
+  public enum Type {
+    Keyword, Fn, Data, Number, Local, Comment, Symbol
+  }
+
+  public @NotNull HighlightInfo toInfo() {
+    return switch (type) {
+      case Keyword -> new HighlightInfo.Lit(range, HighlightInfo.LitKind.Keyword);
+      case Number -> new HighlightInfo.Lit(range, HighlightInfo.LitKind.Int);
+      case Comment -> new HighlightInfo.Lit(range, HighlightInfo.LitKind.Comment);
+      case Symbol -> new HighlightInfo.Lit(range, HighlightInfo.LitKind.SpecialSymbol);
+      case Fn -> createRef(HighlightInfo.DefKind.Fn);
+      case Data -> createRef(HighlightInfo.DefKind.Data);
+      case Local -> createRef(HighlightInfo.DefKind.LocalVar);
+    };
+  }
+
+  private @NotNull HighlightInfo.Ref createRef(HighlightInfo.@NotNull DefKind kind) {
+    return new HighlightInfo.Ref(range, EMPTY_LINK, kind, null);
+  }
+}