merge: #1006

1006: Slightly polish code to respect more pretty settings r=ice1000 a=ice1000

bors r+

Co-authored-by: ice1000 <ice1000kotlin@foxmail.com>

base/src/test/java/org/aya/literate/AyaMdParserTest.java

@@ -15,6 +15,7 @@
 import org.aya.test.AyaThrowingReporter;
 import org.aya.test.EmptyModuleLoader;
 import org.aya.test.TestRunner;
+import org.aya.util.FileUtil;
 import org.aya.util.error.Global;
 import org.aya.util.error.SourceFile;
 import org.aya.util.reporter.CollectingReporter;
@@ -91,7 +92,7 @@ public void testExtract(String caseName) throws IOException {
     var mdFile = new SingleAyaFile.CodeAyaFile(file(oneCase.mdFile()));
     var literate = SingleAyaFile.createLiterateFile(mdFile, AyaThrowingReporter.INSTANCE);
     var actualCode = literate.codeFile().sourceCode();
-    Files.writeString(oneCase.ayaFile(), actualCode);
+    FileUtil.writeString(oneCase.ayaFile(), actualCode);
 
     var expPath = oneCase.expectedAyaFile();
 
@@ -125,10 +126,10 @@ public void testHighlight(String caseName) throws IOException {
     var actualTexInlinedStyle = doc.renderToTeX();
     var expectedMd = doc.renderToAyaMd();
 
-    Files.writeString(oneCase.htmlFile(), doc.renderToHtml());
-    Files.writeString(oneCase.outMdFile(), expectedMd);
-    Files.writeString(oneCase.texFile(), actualTexInlinedStyle);
-    Files.writeString(oneCase.plainTextFile(), doc.debugRender());
+    FileUtil.writeString(oneCase.htmlFile(), doc.renderToHtml());
+    FileUtil.writeString(oneCase.outMdFile(), expectedMd);
+    FileUtil.writeString(oneCase.texFile(), actualTexInlinedStyle);
+    FileUtil.writeString(oneCase.plainTextFile(), doc.debugRender());
 
     // test single file compiler
     var compiler = new SingleFileCompiler(IgnoringReporter.INSTANCE, null, null);

base/src/test/java/org/aya/literate/LiterateFaithfulPrettierTest.java → base/src/test/java/org/aya/literate/FaithfulPrettierTest.java

@@ -4,24 +4,27 @@
 
 import kala.collection.immutable.ImmutableSeq;
 import kala.control.Option;
+import org.aya.cli.literate.FlclFaithfulPrettier;
 import org.aya.cli.literate.LiterateFaithfulPrettier;
 import org.aya.cli.literate.SyntaxHighlight;
 import org.aya.cli.parse.AyaParserImpl;
+import org.aya.cli.parse.FlclParser;
 import org.aya.prettier.AyaPrettierOptions;
 import org.aya.pretty.doc.Doc;
 import org.aya.pretty.doc.Language;
 import org.aya.resolve.context.EmptyContext;
 import org.aya.test.AyaThrowingReporter;
 import org.aya.tyck.TyckDeclTest;
+import org.aya.util.FileUtil;
 import org.aya.util.error.SourceFile;
 import org.aya.util.error.SourcePos;
 import org.junit.jupiter.api.Test;
 
 import java.io.IOException;
 import java.nio.file.Files;
 
-public class LiterateFaithfulPrettierTest {
-  @Test public void test() throws IOException {
+public class FaithfulPrettierTest {
+  @Test public void literate() throws IOException {
     var reporter = AyaThrowingReporter.INSTANCE;
 
     var root = AyaMdParserTest.TEST_DIR;
@@ -40,6 +43,16 @@ public class LiterateFaithfulPrettierTest {
     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);
+    FileUtil.writeString(root.resolve(outputFileName), output);
+  }
+
+  @Test public void fakeLiterate() throws IOException {
+    var root = AyaMdParserTest.TEST_DIR.getParent().resolve("flcl");
+    var fileName = "test.flcl";
+    var file = new SourceFile("FLCL", root, Files.readString(root.resolve(fileName)));
+    var parser = new FlclParser(AyaThrowingReporter.INSTANCE, file);
+    var prettier = new FlclFaithfulPrettier(AyaPrettierOptions.pretty());
+    var doc = prettier.highlight(parser.computeAst());
+    FileUtil.writeString(root.resolve("test.tex"), doc.renderToTeX());
   }
 }

base/src/test/java/org/aya/literate/HighlighterTester.java

@@ -32,7 +32,7 @@
 import static org.junit.jupiter.api.Assertions.*;
 
 public class HighlighterTester {
-  record ExpectedHighlightInfo(
+  public record ExpectedHighlightInfo(
     @NotNull SourcePos sourcePos,
     @NotNull ExpectedHighlightType expected
   ) implements Comparable<ExpectedHighlightInfo> {

base/src/test/java/org/aya/test/TestRunner.java

@@ -8,6 +8,7 @@
 import org.aya.cli.single.SingleFileCompiler;
 import org.aya.generic.util.AyaFiles;
 import org.aya.prelude.GeneratedVersion;
+import org.aya.util.FileUtil;
 import org.aya.util.error.Global;
 import org.aya.util.error.SourceFileLocator;
 import org.aya.util.reporter.CountingReporter;
@@ -124,7 +125,7 @@ private void generateWorkflow(@NotNull Path testFile, Path expectedOutFile, Stri
     hookOut = instantiateHoles(testFile, hookOut);
     var workflowFile = testFile.resolveSibling(testFile.getFileName() + ".txt");
     try {
-      Files.writeString(workflowFile, hookOut, StandardCharsets.UTF_8);
+      FileUtil.writeString(workflowFile, hookOut);
     } catch (IOException e) {
       fail("error generating todo file " + workflowFile.toAbsolutePath());
     }

base/src/test/resources/flcl/.gitignore

@@ -0,0 +1 @@
+*.tex

base/src/test/resources/flcl/test.flcl

@@ -0,0 +1,10 @@
+keyword: data where;
+data: Int Nat;
+symbol: ->;
+---------------------
+data Int where
+  zero : Int
+  succ : Int ≃ Int
+data Nat where
+  zero : Int
+  succ : Int -> Int

cli-console/src/main/java/org/aya/cli/console/Main.java

@@ -12,18 +12,22 @@
 import org.aya.cli.repl.AyaRepl;
 import org.aya.cli.single.CompilerFlags;
 import org.aya.cli.single.SingleFileCompiler;
+import org.aya.cli.utils.CliEnums;
 import org.aya.core.def.PrimDef;
+import org.aya.prettier.AyaPrettierOptions;
 import org.aya.pretty.printer.PrinterConfig;
 import org.aya.tyck.trace.MarkdownTrace;
 import org.aya.tyck.trace.Trace;
+import org.aya.util.FileUtil;
 import org.aya.util.error.SourceFile;
 import org.aya.util.error.SourceFileLocator;
 import org.jetbrains.annotations.NotNull;
+import org.jetbrains.annotations.Nullable;
 import picocli.CommandLine;
 
 import java.io.IOException;
-import java.nio.charset.StandardCharsets;
 import java.nio.file.Files;
+import java.nio.file.Path;
 import java.nio.file.Paths;
 import java.util.concurrent.Callable;
 
@@ -41,56 +45,52 @@ 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);
+    if (action.fileIO == null) {
+      System.err.println("Missing <input-files> arguments");
+      return 1;
+    }
+    if (fakeLiterate) return doFakeLiterate(action.fileIO);
+    if (action.compile == null) action.compile = new CompileAction();
+    return doCompile(action.compile, action.fileIO);
   }
 
-  private int doFakeLiterate(String filePath) throws IOException {
+  private int doFakeLiterate(@NotNull FileIO filePath) throws IOException {
     var replConfig = ReplConfig.loadFromDefault();
     var prettierOptions = replConfig.literatePrettier.prettierOptions;
     var reporter = AnsiReporter.stdio(!asciiOnly, prettierOptions, verbosity);
     var renderOptions = createRenderOptions(replConfig);
+    var outputPath = filePath.outputFile != null ? Paths.get(filePath.outputFile) : null;
+    // Force it to have a pretty stage so info != null
+    prettyStage = CliEnums.PrettyStage.literate;
+    var info = computePrettyInfo(outputPath, renderOptions, prettierOptions);
+    assert info != null;
     replConfig.close();
-    var path = Paths.get(filePath);
+    var path = Paths.get(filePath.inputFile);
     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 setup = info.backendOpts(false);
     var output = renderOptions.render(RenderOptions.OutputTarget.LaTeX, doc, setup);
-    Files.writeString(Paths.get("a.out"), output, StandardCharsets.UTF_8);
+    if (outputPath != null) FileUtil.writeString(outputPath, output);
+    else System.out.println(output);
     return 0;
   }
 
-  private int doCompile(@NotNull CompileAction compile) throws IOException {
+  private int doCompile(@NotNull CompileAction compile, @NotNull FileIO files) throws IOException {
     var message = asciiOnly
       ? CompilerFlags.Message.ASCII
       : CompilerFlags.Message.EMOJI;
-    var inputFile = compile.inputFile;
-    var outputFile = compile.outputFile;
+    var inputFile = files.inputFile;
+    var outputFile = files.outputFile;
     var filePath = Paths.get(inputFile);
     var outputPath = outputFile == null ? null : Paths.get(outputFile);
     var replConfig = ReplConfig.loadFromDefault();
     var prettierOptions = replConfig.literatePrettier.prettierOptions;
     var reporter = AnsiReporter.stdio(!asciiOnly, prettierOptions, verbosity);
     var renderOptions = createRenderOptions(replConfig);
     replConfig.close();
-    var pretty = prettyStage == null
-      ? (outputPath != null ? CompilerFlags.prettyInfoFromOutput(
-      outputPath, renderOptions, prettyNoCodeStyle, prettyInlineCodeStyle, prettySSR) : null)
-      : new CompilerFlags.PrettyInfo(
-        asciiOnly,
-        prettyNoCodeStyle,
-        prettyInlineCodeStyle,
-        prettySSR,
-        prettyStage,
-        prettyFormat,
-        prettierOptions,
-        renderOptions,
-        prettyDir
-      );
+    var pretty = computePrettyInfo(outputPath, renderOptions, prettierOptions);
     var flags = new CompilerFlags(message, interruptedTrace,
       compile.isRemake, pretty,
       modulePaths().view().map(Paths::get),
@@ -114,6 +114,27 @@ private int doCompile(@NotNull CompileAction compile) throws IOException {
     return status;
   }
 
+  private @Nullable CompilerFlags.PrettyInfo
+  computePrettyInfo(
+    @Nullable Path outputPath,
+    RenderOptions renderOptions, AyaPrettierOptions prettierOptions
+  ) {
+    return prettyStage == null
+      ? (outputPath != null ? CompilerFlags.prettyInfoFromOutput(
+      outputPath, renderOptions, prettyNoCodeStyle, prettyInlineCodeStyle, prettySSR) : null)
+      : new CompilerFlags.PrettyInfo(
+        asciiOnly,
+        prettyNoCodeStyle,
+        prettyInlineCodeStyle,
+        prettySSR,
+        prettyStage,
+        prettyFormat,
+        prettierOptions,
+        renderOptions,
+        prettyDir
+      );
+  }
+
   private @NotNull RenderOptions createRenderOptions(@NotNull ReplConfig replConfig) {
     var renderOptions = replConfig.literatePrettier.renderOptions;
     switch (prettyColor) {

cli-console/src/main/java/org/aya/cli/console/MainArgs.java

@@ -41,10 +41,6 @@ public static class CompileAction {
     @Option(names = {"--no-code"}, description =
       "Treat input file as a library root (no outputs will be saved to disk)")
     public boolean isNoCode;
-    @Parameters(paramLabel = "<input-file>", description = "File to compile")
-    public String inputFile;
-    @Option(names = {"-o", "--output"}, description = "Set literate output file")
-    public String outputFile;
   }
 
   public static class PlctAction {
@@ -60,12 +56,6 @@ 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)
@@ -77,8 +67,8 @@ 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;
+    @CommandLine.ArgGroup(heading = "Files:%n", exclusive = false)
+    public @Nullable FileIO fileIO;
   }
 
   @Option(names = {"--interrupted-trace"}, hidden = true)
@@ -110,6 +100,15 @@ public static class Action {
   public List<String> modulePaths;
   @Option(names = {"--verbosity", "-v"}, description = "Minimum severity of error reported." + CANDIDATES, defaultValue = "WARN")
   public Problem.Severity verbosity;
+  @Option(names = {"--fake-literate"}, description = "Generate literate output without compiling.")
+  public boolean fakeLiterate;
+
+  public static class FileIO {
+    @Parameters(paramLabel = "<input-file>", description = "File to compile")
+    public String inputFile;
+    @Option(names = {"-o", "--output"}, description = "Set literate output file")
+    public String outputFile;
+  }
 
   @CommandLine.ArgGroup
   public Action action;

tools/src/main/java/org/aya/util/FileUtil.java

@@ -18,6 +18,7 @@ public interface FileUtil {
   static void writeString(@NotNull Path path, @NotNull String content) throws IOException {
     var parent = path.toAbsolutePath().getParent();
     if (parent != null && Files.notExists(parent)) Files.createDirectories(parent);
+    // No need to set UTF_8 since Java 17
     Files.writeString(path, content);
   }