Simplify things

.github/README.md

@@ -2,7 +2,6 @@
 [![maven]][maven-repo]
 [![gitter]](https://gitter.im/aya-prover/community?utm_source=badge&utm_medium=badge&utm_campaign=pr-badge)
 [![codecov]](https://codecov.io/gh/aya-prover/aya-dev)
-[![Bors enabled](https://bors.tech/images/badge_small.svg)](https://app.bors.tech/repositories/37715)
 
 [**Website**](https://www.aya-prover.org) contains:
 
@@ -44,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 19]: https://jdk.java.net/19
+[Java 20]: https://jdk.java.net/20
 [1lab]: https://1lab.dev
 
 ## Contributing to Aya
 
-Since you need [Java 19] to set this project up, in case your choice
-of IDE is IntelliJ IDEA, version 2022.3 or higher is required.
+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.
 
 + Questions or concerns are welcomed in the discussion area.
   We will try our best to answer your questions, but please be nice.
@@ -114,4 +113,6 @@ implementation group: 'org.aya-prover', name: '[project name]', version: '[lates
     and a bunch of other utilities (files, etc.) are in `tools`.
   + 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`.
+    It offers commonmark extensions for literate mode of any language with a highlighter.
 + `[latest version]` is what you see on this badge ![maven].

.github/workflows/commit-check.yaml

@@ -1,7 +1,5 @@
 name: commit message
 on:
-  push:
-    branches: [staging, trying]
   pull_request:
     branches: [main]
   merge_group:

.github/workflows/gradle-check.yaml

@@ -1,7 +1,7 @@
 name: test
 on:
   push:
-    branches: [main, staging, trying]
+    branches: [main]
   pull_request:
     branches: [main]
   merge_group:

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

@@ -776,7 +776,7 @@ record LetOpen(
     var drop = params.drop(1);
     var subPos = body.sourcePos().sourcePosForSubExpr(sourcePos.file(),
       drop.map(SourceNode::sourcePos));
-    return constructor.apply(sourcePos, params.first(),
+    return constructor.apply(sourcePos, params.getFirst(),
       buildNested(subPos, drop, body, constructor));
   }
 }

base/src/main/java/org/aya/concrete/stmt/QualifiedID.java

@@ -19,7 +19,7 @@ public record QualifiedID(
    * @param ids not empty
    */
   public QualifiedID(@NotNull SourcePos sourcePos, @NotNull ImmutableSeq<String> ids) {
-    this(sourcePos, ModuleName.from(ids.dropLast(1)), ids.last());
+    this(sourcePos, ModuleName.from(ids.dropLast(1)), ids.getLast());
   }
 
   public QualifiedID(@NotNull SourcePos sourcePos, @NotNull String id) {

base/src/main/java/org/aya/core/def/PrimDef.java

@@ -261,16 +261,16 @@ private final class Initializer {
       /** /\ in Cubical Agda, should elaborate to {@link Formula.Conn} */
       public final @NotNull PrimDef.PrimSeed intervalMin = formula(ID.IMIN, prim -> {
         var args = prim.args();
-        return FormulaTerm.and(args.first().term(), args.last().term());
+        return FormulaTerm.and(args.getFirst().term(), args.getLast().term());
       }, "i", "j");
       /** \/ in Cubical Agda, should elaborate to {@link Formula.Conn} */
       public final @NotNull PrimDef.PrimSeed intervalMax = formula(ID.IMAX, prim -> {
         var args = prim.args();
-        return FormulaTerm.or(args.first().term(), args.last().term());
+        return FormulaTerm.or(args.getFirst().term(), args.getLast().term());
       }, "i", "j");
       /** ~ in Cubical Agda, should elaborate to {@link Formula.Inv} */
       public final @NotNull PrimDef.PrimSeed intervalInv = formula(ID.INVOL, prim ->
-        FormulaTerm.inv(prim.args().first().term()), "i");
+        FormulaTerm.inv(prim.args().getFirst().term()), "i");
 
       private @NotNull PrimSeed formula(ID id, Function<PrimCall, Term> unfold, String... tele) {
         return new PrimSeed(id, (prim, state) -> unfold.apply(prim), ref -> new PrimDef(
@@ -283,14 +283,14 @@ private final class Initializer {
 
       private Term inS(@NotNull PrimCall prim, @NotNull TyckState tyckState) {
         var phi = prim.args().get(1).term();
-        var u = prim.args().last().term();
+        var u = prim.args().getLast().term();
         return InTerm.make(phi, u);
       }
 
       private Term outS(@NotNull PrimCall prim, @NotNull TyckState tyckState) {
         var phi = prim.args().get(1).term();
         var par = prim.args().get(2).term();
-        var u = prim.args().last().term();
+        var u = prim.args().getLast().term();
         return OutTerm.make(phi, par, u);
       }
 

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

@@ -93,7 +93,7 @@ public record PathTerm(
         case LamTerm lam -> {
           // TODO: replace with error report¿
           assert lam.param().explicit();
-          pLam = AppTerm.make(lam, new Arg<>(args.first(), true));
+          pLam = AppTerm.make(lam, new Arg<>(args.getFirst(), true));
           args = args.drop(1);
         }
         default -> {

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

@@ -76,7 +76,7 @@ public record SigmaTerm(@NotNull ImmutableSeq<@NotNull Param> params) implements
     var subst = new Subst();
     for (var iter = it.iterator(); iter.hasNext(); ) {
       var item = iter.next();
-      var first = againstTele.first().subst(subst);
+      var first = againstTele.getFirst().subst(subst);
       var result = inherit.apply(item, first.type());
       items.append(new Arg<>(result, first.explicit()));
       var ref = first.ref();

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

@@ -93,12 +93,12 @@ default <O extends AyaDocile> boolean compareUntyped(@NotNull Shaped.List<O> oth
     @Override default @NotNull T constructorForm() {
       var nil = ctorRef(CodeShape.GlobalId.NIL).core;
       var cons = ctorRef(CodeShape.GlobalId.CONS).core;
-      var dataArg = type().args().first(); // Check?
+      var dataArg = type().args().getFirst(); // Check?
       var xLicit = cons.selfTele.get(0).explicit();
       var xsLicit = cons.selfTele.get(1).explicit();
       var elements = repr();
       if (elements.isEmpty()) return makeNil(nil, dataArg);
-      return makeCons(cons, dataArg, new Arg<>(elements.first(), xLicit),
+      return makeCons(cons, dataArg, new Arg<>(elements.getFirst(), xLicit),
         new Arg<>(destruct(elements.drop(1)), xsLicit));
     }
   }

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

@@ -9,8 +9,6 @@
 import kala.collection.immutable.ImmutableSeq;
 import kala.collection.mutable.MutableList;
 import kala.range.primitive.IntRange;
-import kala.tuple.Tuple;
-import kala.tuple.Tuple2;
 import org.aya.concrete.Expr;
 import org.aya.concrete.Pattern;
 import org.aya.concrete.stmt.*;
@@ -49,7 +47,7 @@ public ConcretePrettier(@NotNull PrettierOptions options) {
       case Expr.Tuple expr -> Doc.parened(Doc.commaList(expr.items().view().map(e -> term(Outer.Free, e))));
       case Expr.BinOpSeq binOpSeq -> {
         var seq = binOpSeq.seq();
-        var first = seq.first().term();
+        var first = seq.getFirst().term();
         if (seq.sizeEquals(1)) yield term(outer, first);
         yield visitCalls(null,
           term(Outer.AppSpine, first),
@@ -147,7 +145,7 @@ yield visitCalls(assoc,
         Doc.styled(KEYWORD, Doc.symbol("Sig")),
         visitTele(expr.params().dropLast(1)),
         Doc.symbol("**"),
-        term(Outer.Codomain, expr.params().last().type())), Outer.BinOp);
+        term(Outer.Codomain, expr.params().getLast().type())), Outer.BinOp);
       // ^ Same as Pi
       case Expr.Sort expr -> {
         var fn = Doc.styled(KEYWORD, expr.kind().name());
@@ -208,7 +206,7 @@ yield visitCalls(null, fn, (nc, l) -> l.toDoc(options), outer,
         var body = letsAndBody.component2();
         var oneLine = lets.sizeEquals(1);
         var letSeq = oneLine
-          ? visitLetBind(lets.first())
+          ? visitLetBind(lets.getFirst())
           : Doc.vcat(lets.view()
             .map(this::visitLetBind)
             // | f := g
@@ -274,7 +272,7 @@ private Doc partial(Expr.PartEl el) {
       case Pattern.QualifiedRef qref -> Doc.bracedUnless(Doc.plain(qref.qualifiedID().join()), licit);
       case Pattern.BinOpSeq(var pos, var param) -> {
         if (param.sizeEquals(1)) {
-          yield pattern(param.first(), outer);
+          yield pattern(param.getFirst(), outer);
         }
         var ctorDoc = visitMaybeCtorPatterns(param.view(), Outer.AppSpine, Doc.ALT_WS);
         yield ctorDoc(outer, licit, ctorDoc, param.sizeLessThanOrEquals(1));

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

@@ -73,7 +73,7 @@ public CorePrettier(@NotNull PrettierOptions options) {
       case ConCall conCall -> visitArgsCalls(conCall.ref(), CON, conCall.conArgs(), outer);
       case FnCall fnCall -> visitArgsCalls(fnCall.ref(), FN, fnCall.args(), outer);
       case SigmaTerm(var params) -> {
-        var last = params.last();
+        var last = params.getLast();
         var doc = Doc.sep(
           Doc.styled(KEYWORD, Doc.symbol("Sig")),
           visitTele(params.dropLast(1), last.type(), Term::findUsages),
@@ -91,7 +91,7 @@ case LamTerm(var param0, var body0) -> {
         if (body instanceof Callable call && call.ref() instanceof DefVar<?, ?> defVar) {
           var args = visibleArgsOf(call).view();
           while (params.isNotEmpty() && args.isNotEmpty()) {
-            if (checkUneta(args, params.last())) {
+            if (checkUneta(args, params.getLast())) {
               args = args.dropLast(1);
               params.removeLast();
             } else break;
@@ -248,7 +248,7 @@ case CoeTerm(var ty, var r, var s) -> visitCalls(null,
 
   /** @return if we can eta-contract the last argument */
   private boolean checkUneta(SeqView<Arg<Term>> args, LamTerm.Param param) {
-    var arg = args.last();
+    var arg = args.getLast();
     if (arg.explicit() != param.explicit()) return false;
     if (!(arg.term() instanceof RefTerm(var argVar))) return false;
     if (argVar != param.ref()) return false;

base/src/main/java/org/aya/resolve/error/NameProblem.java

@@ -194,7 +194,7 @@ record UnqualifiedNameNotFoundError(
       var possible = didYouMean();
       if (possible.isEmpty()) return head;
       var tail = possible.sizeEquals(1)
-        ? Doc.sep(Doc.english("Did you mean:"), Doc.code(possible.first()))
+        ? Doc.sep(Doc.english("Did you mean:"), Doc.code(possible.getFirst()))
         : Doc.vcat(Doc.english("Did you mean:"),
           Doc.nest(2, Doc.vcat(possible.view().map(Doc::code))));
       return Doc.vcat(head, tail);

base/src/main/java/org/aya/tyck/error/HoleProblem.java

@@ -96,7 +96,7 @@ record CannotFindGeneralSolution(
     @NotNull ImmutableSeq<TyckState.Eqn> eqns
   ) implements Problem {
     @Override public @NotNull SourcePos sourcePos() {
-      return eqns.last().pos();
+      return eqns.getLast().pos();
     }
 
     @Override public @NotNull SeqView<WithPos<Doc>> inlineHints(@NotNull PrettierOptions options) {

base/src/main/java/org/aya/tyck/order/AyaSccTycker.java

@@ -60,7 +60,7 @@ public record AyaSccTycker(
   public @NotNull ImmutableSeq<TyckOrder> tyckSCC(@NotNull ImmutableSeq<TyckOrder> scc) {
     try {
       if (scc.isEmpty()) return ImmutableSeq.empty();
-      if (scc.sizeEquals(1)) checkUnit(scc.first());
+      if (scc.sizeEquals(1)) checkUnit(scc.getFirst());
       else checkMutual(scc);
       return ImmutableSeq.empty();
     } catch (SCCTyckingFailed failed) {
@@ -77,7 +77,7 @@ private void checkMutual(@NotNull ImmutableSeq<TyckOrder> scc) {
     // that is, what we did before https://github.com/aya-prover/aya-dev/pull/326
     var headerOrder = headerOrder(scc, unit);
     if (headerOrder.sizeEquals(1)) {
-      checkUnit(new TyckOrder.Body(headerOrder.first()));
+      checkUnit(new TyckOrder.Body(headerOrder.getFirst()));
     } else {
       var tyckTasks = headerOrder.view()
         .<TyckOrder>map(TyckOrder.Head::new)

base/src/main/java/org/aya/tyck/tycker/UnifiedTycker.java

@@ -97,7 +97,7 @@ protected final Result inheritFallbackUnify(@NotNull Term upper, @NotNull Result
     } else if (whnf(lower) instanceof PathTerm cube && cube.params().sizeEquals(1)) {
       // TODO: also support n-ary path
       if (upperWHNF instanceof PiTerm pi && pi.param().explicit() && pi.param().type() == IntervalTerm.INSTANCE) {
-        var lamBind = new RefTerm(new LocalVar(cube.params().first().name()));
+        var lamBind = new RefTerm(new LocalVar(cube.params().getFirst().name()));
         var body = new PAppTerm(term, cube, new Arg<>(lamBind, true));
         var inner = inheritFallbackUnify(pi.substBody(lamBind),
           new Result.Default(body, cube.substType(SeqView.of(lamBind))), loc);

cli-impl/src/main/java/org/aya/cli/parse/AyaProducer.java

@@ -260,7 +260,7 @@ private record DeclParseData(
   ) {
     public @Nullable String checkName(@NotNull AyaProducer self, boolean require) {
       if (name != null) return name;
-      if (require) return self.error(node.childrenView().first(), "Expect a name");
+      if (require) return self.error(node.childrenView().getFirst(), "Expect a name");
       return Constants.randomName(info.sourcePos());
     }
   }
@@ -290,7 +290,7 @@ private record DeclParseData(
     if (name == null) return null;
 
     var fnBodyNode = node.peekChild(FN_BODY);
-    if (fnBodyNode == null) return error(node.childrenView().first(), "Expect a function body");
+    if (fnBodyNode == null) return error(node.childrenView().getFirst(), "Expect a function body");
     var dynamite = fnBody(fnBodyNode);
     if (dynamite == null) return null;
     var inline = info.modifier.misc(ModifierParser.Modifier.Inline);
@@ -351,7 +351,7 @@ private void giveMeOpen(@NotNull ModifierParser.Modifiers modiSet, @NotNull Decl
       dataCtorClause.child(DATA_CTOR));
     var dataCtor = node.peekChild(DATA_CTOR);
     if (dataCtor != null) return dataCtor(ImmutableSeq.empty(), dataCtor);
-    return error(node.childrenView().first(), "Expect a data constructor");
+    return error(node.childrenView().getFirst(), "Expect a data constructor");
   }
 
   public @Nullable ClassDecl classDecl(@NotNull GenericNode<?> node, @NotNull MutableList<Stmt> additional) {
@@ -385,7 +385,7 @@ private void giveMeOpen(@NotNull ModifierParser.Modifiers modiSet, @NotNull Decl
 
   public @Nullable TeleDecl.PrimDecl primDecl(@NotNull GenericNode<?> node) {
     var nameEl = node.peekChild(PRIM_NAME);
-    if (nameEl == null) return error(node.childrenView().first(), "Expect a primitive's name");
+    if (nameEl == null) return error(node.childrenView().getFirst(), "Expect a primitive's name");
     var id = weakId(nameEl.child(WEAK_ID));
     return new TeleDecl.PrimDecl(
       id.sourcePos(),
@@ -668,7 +668,7 @@ private interface LicitParser<T> extends BooleanObjBiFunction<GenericNode<?>, T>
     }
     if (node.is(TUPLE_IM_ARGUMENT)) {
       var items = node.child(COMMA_SEP).childrenOfType(EXPR).map(this::expr).toImmutableSeq();
-      if (items.sizeEquals(1)) return new Expr.NamedArg(false, newBinOPScope(items.first()));
+      if (items.sizeEquals(1)) return new Expr.NamedArg(false, newBinOPScope(items.getFirst()));
       var tupExpr = new Expr.Tuple(sourcePosOf(node), items);
       return new Expr.NamedArg(false, tupExpr);
     }
@@ -721,7 +721,7 @@ private interface LicitParser<T> extends BooleanObjBiFunction<GenericNode<?>, T>
     // when no as, entirePos == innerPatternPos
 
     Arg<Pattern> pattern = unitPats.sizeEquals(1)
-      ? unitPats.first()
+      ? unitPats.getFirst()
       : new Arg<>(new Pattern.BinOpSeq(innerPatternPos, unitPats), true);
     return as.isDefined()
       ? Pattern.As.wrap(entirePos, pattern, as.get())
@@ -740,11 +740,11 @@ private Arg<Pattern> unitPattern(@NotNull GenericNode<?> node) {
       child = child.child(COMMA_SEP);
       var patterns = patterns(child);
       var pat = patterns.sizeEquals(1)
-        ? newBinOPScope(patterns.first().term(), explicit)
+        ? newBinOPScope(patterns.getFirst().term(), explicit)
         : new Pattern.Tuple(sourcePosOf(node), patterns);
       return new Arg<>(pat, explicit);
     });
-    return new Arg<>(atomPattern(node.childrenView().first()), true);
+    return new Arg<>(atomPattern(node.childrenView().getFirst()), true);
   }
 
   private @NotNull Pattern atomPattern(@NotNull GenericNode<?> node) {

cli-impl/src/main/java/org/aya/cli/parse/FlclParser.java

@@ -35,7 +35,7 @@ public FlclParser(@NotNull Reporter reporter, @NotNull SourceFile file) {
       var idChildren = rule.childrenOfType(FlclPsiElementTypes.ID)
         .map(MarkerNodeWrapper::tokenText)
         .map(CharSequence::toString);
-      var title = idChildren.first();
+      var title = idChildren.getFirst();
       var ids = idChildren.drop(1).toImmutableSeq();
       insert(title, ids);
     });

cli-impl/src/main/java/org/aya/cli/parse/ModifierParser.java

@@ -220,7 +220,7 @@ private record ModifierSet(
         && !exists.containsKey(modifier)) {
         // one (not None) group one modifier
         assert exists.size() == 1;
-        var contradict = Seq.from(exists.entrySet()).first();
+        var contradict = Seq.from(exists.entrySet()).getFirst();
         reportContradictModifier(data, new WithPos<>(contradict.getValue(), contradict.getKey()));
         continue;
       }

cli-impl/src/main/java/org/aya/cli/render/vscode/ColorTheme.java

@@ -102,7 +102,7 @@ public Option<VscColorTheme.TokenColor.Settings> find(@NotNull String scope) {
   }
 
   public void findAndPut(@NotNull MutableMap<String, Integer> putTo, @NotNull String key, @NotNull Seq<String> scope, @NotNull Map<String, Integer> fallback) {
-    var result = scope.view().map(this::find).firstOption(Option::isDefined);
+    var result = scope.view().map(this::find).findFirst(Option::isDefined);
 
     if (result.isDefined()) {
       var settings = result.get().get();