Split tools, upgrade to Java 21

.github/README.md

@@ -43,13 +43,13 @@ Aya is under active development, so please expect bugs, usability or performance
 See also [use as a library](#use-as-a-library).
 
 [GitHub Releases]: https://github.com/aya-prover/aya-dev/releases/tag/nightly-build
-[Java 20]: https://jdk.java.net/20
+[Java 21]: https://jdk.java.net/21
 [1lab]: https://1lab.dev
 
 ## Contributing to Aya
 
-Since you need [Java 20] to set this project up, in case your choice
-of IDE is IntelliJ IDEA, version 2023.2 or higher is required.
+Since you need [Java 21] to set this project up, in case your choice
+of IDE is IntelliJ IDEA, version 2023.3 or higher is required.
 
 + Questions or concerns are welcomed in the discussion area.
   We will try our best to answer your questions, but please be nice.
@@ -104,13 +104,14 @@ implementation group: 'org.aya-prover', name: '[project name]', version: '[lates
 ```
 
 + `[project name]` specifies the subproject of Aya you want to use,
-  and the options are `pretty`, `base`, `cli-impl`, `cli-console`, `parser`, etc.
+  and the options are `pretty`, `base`, `cli-impl`, `parser`, etc.
   + The type checker lives in `base` and `parser`.
   + The generalized pretty printing framework is in `pretty`.
   + The library system, literate mode, single-file type checker, and basic REPL are in `cli-impl`.
-  + The generalized binary operator parser, generalized tree builder,
-    generalized mutable graph, generalized termination checker,
+  + The generalized tree builder, generalized termination checker,
     and a bunch of other utilities (files, etc.) are in `tools`.
+  + The generalized binary operator parser, generalized mutable graph are
+    in `tools-kala` because they depend on a larger subset of the kala library.
   + The command and argument parsing framework is in `tools-repl`.
     It offers an implementation of jline3 parser based on Grammar-Kit and relevant facilities.
   + The literate-markdown related infrastructure is in `tools-md`.

base/build.gradle.kts

@@ -1,10 +1,13 @@
 // 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.
-import org.aya.gradle.*
+import org.aya.gradle.CommonTasks
+import org.aya.gradle.GenerateReflectionConfigTask
+import org.aya.gradle.GenerateVersionTask
+
 CommonTasks.nativeImageConfig(project)
 
 dependencies {
-  api(project(":tools"))
+  api(project(":tools-kala"))
   api(project(":tools-md"))
   api(project(":pretty"))
   api(libs.aya.guest0x0)

base/src/main/java/module-info.java

@@ -2,6 +2,7 @@
   requires transitive aya.md;
   requires transitive aya.pretty;
   requires transitive aya.util;
+  requires transitive aya.util.more;
   requires transitive aya.guest.cubical;
   requires transitive kala.base;
   requires transitive kala.collection;
@@ -15,6 +16,7 @@
   exports org.aya.concrete.error;
   exports org.aya.concrete.remark;
   exports org.aya.concrete.stmt.decl;
+
   exports org.aya.concrete.stmt;
   exports org.aya.concrete.visitor;
   exports org.aya.concrete;

base/src/main/java/org/aya/concrete/Expr.java

@@ -28,8 +28,8 @@
 import org.aya.resolve.visitor.ExprResolver;
 import org.aya.resolve.visitor.StmtShallowResolver;
 import org.aya.tyck.Result;
+import org.aya.util.BinOpElem;
 import org.aya.util.ForLSP;
-import org.aya.util.binop.BinOpParser;
 import org.aya.util.error.SourceNode;
 import org.aya.util.error.SourcePos;
 import org.aya.util.error.WithPos;
@@ -158,7 +158,7 @@ record App(
    * @author AustinZhu
    */
   record NamedArg(@Override boolean explicit, @Nullable String name, @Override @NotNull Expr term)
-    implements AyaDocile, SourceNode, BinOpParser.Elem<Expr> {
+    implements AyaDocile, SourceNode, BinOpElem<Expr> {
 
     public NamedArg(boolean explicit, @NotNull Expr expr) {
       this(explicit, null, expr);

base/src/main/java/org/aya/concrete/desugar/Desugarer.java

@@ -107,7 +107,7 @@ public static class DesugarInterruption extends Exception {}
         },
         // do not desugar
         right -> arrayExpr);
-      case Expr.LetOpen(var $, var $$, var $$$, var body) -> pre(body);
+      case Expr.LetOpen(_, _, _, var body) -> pre(body);
       case Expr misc -> StmtConsumer.super.pre(misc);
     };
   }

base/src/main/java/org/aya/core/serde/SerTerm.java

@@ -187,7 +187,7 @@ record ConReduceRule(
     public @NotNull Term de(@NotNull DeState state) {
       return new RuleReducer.Con(
         (Shaped.Applicable<Term, CtorDef, TeleDecl.DataCtor>) head.deShape(state),
-        dataArgs().ulift, dataArgs.de(state), conArgs.map(x -> x.de(state))
+        dataArgs.ulift, dataArgs.de(state), conArgs.map(x -> x.de(state))
       );
     }
   }

base/src/main/java/org/aya/core/term/FormulaTerm.java

@@ -45,9 +45,9 @@
 
   public @NotNull SeqView<Term> view() {
     return switch (asFormula) {
-      case Formula.Conn(var $, var l, var r) -> Seq.of(l, r).view();
+      case Formula.Conn(_, var l, var r) -> Seq.of(l, r).view();
       case Formula.Inv(var i) -> SeqView.of(i);
-      case Formula.Lit<?> $ -> SeqView.empty();
+      case Formula.Lit<?> _ -> SeqView.empty();
     };
   }
 }

base/src/main/java/org/aya/core/term/IntegerTerm.java

@@ -44,7 +44,7 @@ public record IntegerTerm(
     var ctorTele = head().ref().core.selfTele;
     assert ctorTele.sizeEquals(1);
 
-    return ImmutableSeq.of(new Arg<>(new IntegerTerm(repr - 1, recognition, type), ctorTele.first().explicit()));
+    return ImmutableSeq.of(new Arg<>(new IntegerTerm(repr - 1, recognition, type), ctorTele.getFirst().explicit()));
   }
 
   @Override public @NotNull IntegerTerm descent(@NotNull UnaryOperator<Term> f, @NotNull UnaryOperator<Pat> g) {

base/src/main/java/org/aya/generic/Shaped.java

@@ -9,7 +9,10 @@
 import org.aya.core.pat.Pat;
 import org.aya.core.repr.CodeShape;
 import org.aya.core.repr.ShapeRecognition;
-import org.aya.core.term.*;
+import org.aya.core.term.DataCall;
+import org.aya.core.term.IntegerTerm;
+import org.aya.core.term.RuleReducer;
+import org.aya.core.term.Term;
 import org.aya.ref.DefVar;
 import org.aya.tyck.unify.TermComparator;
 import org.aya.util.Arg;
@@ -70,8 +73,6 @@ default <O extends AyaDocile> boolean compareUntyped(@NotNull Shaped.Nat<O> othe
     }
 
     @NotNull Shaped.Nat<T> map(@NotNull IntUnaryOperator f);
-
-    // int construct(@NotNull T term);
   }
 
   non-sealed interface List<T extends AyaDocile> extends Inductive<T> {

base/src/main/java/org/aya/prettier/BasePrettier.java

@@ -23,8 +23,8 @@
 import org.aya.ref.DefVar;
 import org.aya.ref.LocalVar;
 import org.aya.util.Arg;
+import org.aya.util.BinOpElem;
 import org.aya.util.binop.Assoc;
-import org.aya.util.binop.BinOpParser;
 import org.aya.util.prettier.PrettierOptions;
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
@@ -76,7 +76,7 @@ protected BasePrettier(@NotNull PrettierOptions options) {
 
   public @NotNull Doc visitCalls(
     @Nullable Assoc assoc, @NotNull Doc fn,
-    @NotNull SeqView<? extends BinOpParser.@NotNull Elem<Term>> args,
+    @NotNull SeqView<? extends @NotNull BinOpElem<Term>> args,
     @NotNull Outer outer, boolean showImplicits
   ) {
     return visitCalls(assoc, fn, this::term, outer, args, showImplicits);
@@ -109,9 +109,9 @@ protected BasePrettier(@NotNull PrettierOptions options) {
    */
   <T extends AyaDocile> @NotNull Doc visitCalls(
     @Nullable Assoc assoc, @NotNull Doc fn, @NotNull Fmt<T> fmt, Outer outer,
-    @NotNull SeqView<? extends BinOpParser.@NotNull Elem<@NotNull T>> args, boolean showImplicits
+    @NotNull SeqView<? extends @NotNull BinOpElem<@NotNull T>> args, boolean showImplicits
   ) {
-    var visibleArgs = (showImplicits ? args : args.filter(BinOpParser.Elem::explicit)).toImmutableSeq();
+    var visibleArgs = (showImplicits ? args : args.filter(BinOpElem::explicit)).toImmutableSeq();
     if (visibleArgs.isEmpty()) return assoc != null ? Doc.parened(fn) : fn;
     if (assoc != null) {
       var firstArg = visibleArgs.getFirst();
@@ -137,14 +137,14 @@ protected BasePrettier(@NotNull PrettierOptions options) {
    * @see #visitCalls(Assoc, Doc, Fmt, Outer, SeqView, boolean)
    */
   private <T extends AyaDocile> @NotNull Doc
-  prefix(@NotNull Doc fn, @NotNull Fmt<T> fmt, Outer outer, SeqView<? extends BinOpParser.@NotNull Elem<T>> args) {
+  prefix(@NotNull Doc fn, @NotNull Fmt<T> fmt, Outer outer, SeqView<? extends @NotNull BinOpElem<T>> args) {
     var call = Doc.sep(fn, Doc.sep(args.map(arg ->
       arg(fmt, arg, Outer.AppSpine))));
     // If we're in a spine, add parentheses
     return checkParen(outer, call, Outer.AppSpine);
   }
 
-  public static <T extends AyaDocile> Doc arg(@NotNull Fmt<T> fmt, @NotNull BinOpParser.Elem<T> arg, @NotNull Outer outer) {
+  public static <T extends AyaDocile> Doc arg(@NotNull Fmt<T> fmt, @NotNull BinOpElem<T> arg, @NotNull Outer outer) {
     if (arg.explicit()) return fmt.apply(outer, arg.term());
     return Doc.braced(fmt.apply(Outer.Free, arg.term()));
   }

base/src/main/java/org/aya/prettier/ConcretePrettier.java

@@ -155,7 +155,7 @@
       }
       case Expr.Lift expr -> Doc.sep(Seq
         .from(IntRange.closed(1, expr.lift()).iterator()).view()
-        .map($ -> Doc.styled(KEYWORD, Doc.symbol("ulift")))
+        .map(_ -> Doc.styled(KEYWORD, Doc.symbol("ulift")))
         .appended(term(Outer.Lifted, expr.expr())));
       case Expr.PartEl el -> Doc.sep(Doc.symbol("{|"),
         partial(el),
@@ -260,17 +260,17 @@
   public @NotNull Doc pattern(@NotNull Pattern pattern, boolean licit, Outer outer) {
     return switch (pattern) {
       case Pattern.Tuple tuple -> Doc.licit(licit, patterns(tuple.patterns()));
-      case Pattern.Absurd $ -> Doc.bracedUnless(Doc.styled(KEYWORD, "()"), licit);
+      case Pattern.Absurd _ -> Doc.bracedUnless(Doc.styled(KEYWORD, "()"), licit);
       case Pattern.Bind bind -> Doc.bracedUnless(linkDef(bind.bind()), licit);
-      case Pattern.CalmFace $ -> Doc.bracedUnless(Doc.plain(Constants.ANONYMOUS_PREFIX), licit);
+      case Pattern.CalmFace _ -> Doc.bracedUnless(Doc.plain(Constants.ANONYMOUS_PREFIX), licit);
       case Pattern.Number number -> Doc.bracedUnless(Doc.plain(String.valueOf(number.number())), licit);
       case Pattern.Ctor ctor -> {
         var name = linkRef(ctor.resolved().data(), CON);
         var ctorDoc = ctor.params().isEmpty() ? name : Doc.sep(name, visitMaybeCtorPatterns(ctor.params(), Outer.AppSpine, Doc.ALT_WS));
         yield ctorDoc(outer, licit, ctorDoc, ctor.params().isEmpty());
       }
       case Pattern.QualifiedRef qref -> Doc.bracedUnless(Doc.plain(qref.qualifiedID().join()), licit);
-      case Pattern.BinOpSeq(var pos, var param) -> {
+      case Pattern.BinOpSeq(_, var param) -> {
         if (param.sizeEquals(1)) {
           yield pattern(param.getFirst(), outer);
         }

base/src/main/java/org/aya/prettier/CorePrettier.java

@@ -128,7 +128,7 @@ yield visitCalls(null, fn, (nest, t) -> t.toDoc(options), outer,
           options.map.get(AyaPrettierOptions.Key.ShowImplicitArgs)
         );
       }
-      case IntervalTerm $ -> Doc.styled(PRIM, "I");
+      case IntervalTerm _ -> Doc.styled(PRIM, "I");
       case NewTerm(var inner) -> visitCalls(null, Doc.styled(KEYWORD, "new"), (nest, t) -> t.toDoc(options), outer,
         SeqView.of(new Arg<>(o -> term(Outer.AppSpine, inner), true)),
         options.map.get(AyaPrettierOptions.Key.ShowImplicitArgs)

base/src/main/java/org/aya/tyck/unify/TermComparator.java

@@ -278,11 +278,11 @@
         }
         yield true;
       }
-      case LamTerm $ -> throw new InternalException("LamTerm is never type");
-      case ConCall $ -> throw new InternalException("ConCall is never type");
-      case TupTerm $ -> throw new InternalException("TupTerm is never type");
-      case NewTerm $ -> throw new InternalException("NewTerm is never type");
-      case ErrorTerm $ -> true;
+      case LamTerm _ -> throw new InternalException("LamTerm is never type");
+      case ConCall _ -> throw new InternalException("ConCall is never type");
+      case TupTerm _ -> throw new InternalException("TupTerm is never type");
+      case NewTerm _ -> throw new InternalException("NewTerm is never type");
+      case ErrorTerm _ -> true;
       case SigmaTerm(var paramsSeq) -> {
         var params = paramsSeq.view();
         for (int i = 1, size = paramsSeq.size(); i <= size; i++) {

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

@@ -91,7 +91,7 @@ public HighlighterTester(@NotNull String sourceCode, @NotNull ImmutableSeq<Highl
 
   public void runTest() {
     var sortedActual = actual.view().distinct().sorted().toImmutableSeq().view();
-    if (sortedActual.getLast() instanceof HighlightInfo.Lit(var $, var kind) && kind == HighlightInfo.LitKind.Eol)
+    if (sortedActual.getLast() instanceof HighlightInfo.Lit(_, var kind) && kind == HighlightInfo.LitKind.Eol)
       // Remove the last Eol
       sortedActual = sortedActual.dropLast(1);
     runTest(sortedActual.toImmutableSeq(), Seq.of(expected));
@@ -120,13 +120,13 @@ public void runTest(@NotNull ImmutableSeq<HighlightInfo> actuals, @NotNull Seq<E
       assertEquals(expectedText, actualText, "at " + sourcePos);
 
       switch (actual) {
-        case HighlightInfo.Lit(var $, var ty)
+        case HighlightInfo.Lit(_, var ty)
           when ty == HighlightInfo.LitKind.Keyword && expected.expected() instanceof ExpectedHighlightType.Keyword -> {
         }
-        case HighlightInfo.Lit(var $, var ty)
+        case HighlightInfo.Lit(_, var ty)
           when ty == HighlightInfo.LitKind.Int && expected.expected() instanceof LitInt -> {
         }
-        case HighlightInfo.Lit(var $, var ty)
+        case HighlightInfo.Lit(_, var ty)
           when ty == HighlightInfo.LitKind.String && expected.expected() instanceof ExpectedHighlightType.LitString -> {
         }
 
@@ -138,7 +138,7 @@ public void runTest(@NotNull ImmutableSeq<HighlightInfo> actuals, @NotNull Seq<E
           when expected.expected() instanceof ExpectedHighlightType.Ref expectedRef ->
           assertRef(sourcePos, ref, expectedRef);
 
-        case HighlightInfo.Err err -> throw new UnsupportedOperationException("TODO");   // TODO
+        case HighlightInfo.Err _ -> throw new UnsupportedOperationException("TODO");   // TODO
 
         default ->
           fail("expected: " + expected.getClass().getSimpleName() + ", but actual: " + actual.getClass().getSimpleName());
@@ -213,7 +213,7 @@ public static void highlightAndTest(@Language("Aya") @NotNull String code, @Null
     Stmt.resolve(stmts, resolveInfo, EmptyModuleLoader.INSTANCE);
 
     var result = SyntaxHighlight.highlight(null, Option.some(sourceFile), stmts)
-      .filterNot(it -> it instanceof HighlightInfo.Lit(var $, var kind)
+      .filterNot(it -> it instanceof HighlightInfo.Lit(_, var kind)
         && ignored.contains(kind));
     new HighlighterTester(code, result, expected).runTest();
   }

cli-impl/src/main/java/org/aya/cli/library/LibraryCompiler.java

@@ -26,8 +26,8 @@
 import org.aya.resolve.error.NameProblem;
 import org.aya.resolve.module.CachedModuleLoader;
 import org.aya.resolve.module.ModuleLoader;
-import org.aya.util.StringUtil;
 import org.aya.util.error.InternalException;
+import org.aya.util.more.StringUtil;
 import org.aya.util.reporter.CountingReporter;
 import org.aya.util.reporter.Reporter;
 import org.aya.util.terck.MutableGraph;
@@ -89,13 +89,13 @@
     @NotNull Path libraryRoot
   ) throws IOException {
     if (!Files.exists(libraryRoot)) {
-      reporter.reportString("Specified library root does not exist: " + libraryRoot);
+      reporter.reportString(STR."Specified library root does not exist: \{libraryRoot}");
       return 1;
     }
     try {
       return newCompiler(primFactory, reporter, flags, advisor, libraryRoot).start();
     } catch (LibraryConfigData.BadConfig bad) {
-      reporter.reportString("Cannot load malformed library: " + bad.getMessage());
+      reporter.reportString(STR."Cannot load malformed library: \{bad.getMessage()}");
       return 1;
     }
   }
@@ -141,8 +141,8 @@
         known.noneMatch(k -> k.moduleName().equals(s.moduleName())));
       known.appendAll(dedup);
     });
-    reporter.reportNest("Done in " + StringUtil.timeToString(
-      System.currentTimeMillis() - startTime), LibraryOwner.DEFAULT_INDENT + 2);
+    reporter.reportNest(STR."Done in \{StringUtil.timeToString(
+        System.currentTimeMillis() - startTime)}", LibraryOwner.DEFAULT_INDENT + 2);
     return depGraph;
   }
 
@@ -188,7 +188,7 @@
     });
     // THE BIG GAME
     modified.forEachChecked(src -> {
-      // reportNest("[Pretty] " + QualifiedID.join(src.moduleName()));
+      // reportNest(STR."[Pretty] \{QualifiedID.join(src.moduleName())}");
       var doc = src.pretty(ImmutableSeq.empty(), prettierOptions);
       var text = renderOptions.render(outputTarget, doc, setup);
       var outputFileName = AyaFiles.stripAyaSourcePostfix(src.displayPath().toString()) + outputTarget.fileExt;
@@ -214,7 +214,7 @@
       owner.addModulePath(dep.outDir());
     }
 
-    reporter.reportString("Compiling " + library.name());
+    reporter.reportString(STR."Compiling \{library.name()}");
     var startTime = System.currentTimeMillis();
     if (anyDepChanged || flags.remake()) {
       owner.librarySources().forEach(this::clearModified);
@@ -231,8 +231,8 @@
     }
 
     var make = make(modified);
-    reporter.reportNest("Library loaded in " + StringUtil.timeToString(
-      System.currentTimeMillis() - startTime), LibraryOwner.DEFAULT_INDENT + 2);
+    reporter.reportNest(STR."Library loaded in \{StringUtil.timeToString(
+        System.currentTimeMillis() - startTime)}", LibraryOwner.DEFAULT_INDENT + 2);
     pretty(modified);
     return make;
   }
@@ -376,7 +376,7 @@
         QualifiedID.join(moduleName), file.displayPath()), LibraryOwner.DEFAULT_INDENT);
       var mod = moduleLoader.load(moduleName);
       if (mod == null || file.resolveInfo().get() == null)
-        throw new InternalException("Unable to load module: " + moduleName);
+        throw new InternalException(STR."Unable to load module: \{moduleName}");
     }
   }