merge: #1017

Do ReplaceWith

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

@@ -61,7 +61,7 @@ public static class DesugarInterruption extends Exception {}
         yield pre(new BinExprParser(info, seq.view()).build(pos));
       }
       case Expr.Do(var sourcePos, var monadBind, var binds) -> {
-        var last = binds.last();
+        var last = binds.getLast();
         if (last.var() != LocalVar.IGNORED) {
           info.opSet().reporter.report(new DoNotationError(last.sourcePos(), expr));
           yield new Expr.Error(sourcePos, expr);

base/src/main/java/org/aya/core/ops/Eta.java

@@ -1,4 +1,4 @@
-// Copyright (c) 2020-2022 Tesla (Yinsen) Zhang.
+// 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.core.ops;
 
@@ -29,7 +29,7 @@ case TupTerm(var items) -> {
         var etaItems = items.map(x -> x.descent(this::uneta));
         var defaultRes = new TupTerm(etaItems);
         // Get first item's Proj.of Term to compare with other items'
-        var firstItem = etaItems.first().term();
+        var firstItem = etaItems.getFirst().term();
         if (!(firstItem instanceof ProjTerm proj
           && proj.of() instanceof RefTerm ref
           && ctx.get(ref.var()) instanceof SigmaTerm sigmaTerm)) yield defaultRes;

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

@@ -114,7 +114,7 @@ protected BasePrettier(@NotNull PrettierOptions options) {
     var visibleArgs = (showImplicits ? args : args.filter(BinOpParser.Elem::explicit)).toImmutableSeq();
     if (visibleArgs.isEmpty()) return assoc != null ? Doc.parened(fn) : fn;
     if (assoc != null) {
-      var firstArg = visibleArgs.first();
+      var firstArg = visibleArgs.getFirst();
       if (!firstArg.explicit()) return prefix(Doc.parened(fn), fmt, outer, visibleArgs.view());
       var first = fmt.apply(Outer.BinOp, firstArg.term());
       if (assoc.isBinary()) {
@@ -196,14 +196,14 @@ public static <T extends AyaDocile> Doc arg(@NotNull Fmt<T> fmt, @NotNull BinOpP
     @Nullable Term body, @NotNull ToIntBiFunction<Term, AnyVar> altF7
   ) {
     if (telescope.isEmpty()) return Doc.empty();
-    var last = telescope.first();
+    var last = telescope.getFirst();
     var buf = MutableList.<Doc>create();
     var names = MutableList.of(last.ref());
     for (int i = 1; i < telescope.size(); i++) {
       var param = telescope.get(i);
       if (!Objects.equals(param.type(), last.type())) {
         if (body != null && names.sizeEquals(1)) {
-          var ref = names.first();
+          var ref = names.getFirst();
           var used = telescope.sliceView(i, telescope.size())
             .map(ParamLike::type).appended(body)
             .anyMatch(p -> altF7.applyAsInt(p, ref) > 0);
@@ -216,7 +216,7 @@ public static <T extends AyaDocile> Doc arg(@NotNull Fmt<T> fmt, @NotNull BinOpP
       names.append(param.ref());
     }
     if (body != null && names.sizeEquals(1)
-      && altF7.applyAsInt(body, names.first()) == 0) {
+      && altF7.applyAsInt(body, names.getFirst()) == 0) {
       buf.append(justType(last, Outer.ProjHead));
     } else buf.append(mutableListNames(names, last));
     return Doc.sep(buf);

base/src/main/java/org/aya/tyck/ExprTycker.java

@@ -166,7 +166,7 @@ public final class ExprTycker extends UnifiedTycker {
           fTy = whnf(fTy);
         } else if (fTy instanceof SortTerm) {
           if (whnf(app) instanceof ClassCall classCall) {
-            var member = classCall.missingMembers().firstOrNull();
+            var member = classCall.missingMembers().getFirstOrNull();
             if (member == null) {
               throw new InternalException("TODO: too many fields");
             }
@@ -226,7 +226,7 @@ public final class ExprTycker extends UnifiedTycker {
           var type = ctx.freshTyHole("_ty" + lit.integer() + "'", lit.sourcePos());
           yield new Result.Default(new MetaLitTerm(lit.sourcePos(), lit.integer(), defs, type.component1()), type.component1());
         }
-        var match = defs.first();
+        var match = defs.getFirst();
         var type = new DataCall(((DataDef) match.component1()).ref, 0, ImmutableSeq.empty());
         yield new Result.Default(new IntegerTerm(integer, match.component2(), type), type);
       }
@@ -253,11 +253,11 @@ public final class ExprTycker extends UnifiedTycker {
         if (defs.sizeGreaterThan(1)) yield fail(expr, new Zonker.UnsolvedLit(new MetaLitTerm(
           arr.sourcePos(), arr, defs, ErrorTerm.typeOf(arr))));
 
-        var match = defs.first();
+        var match = defs.getFirst();
         var def = (DataDef) match.component1();
 
         // preparing
-        var dataParam = Def.defTele(def.ref).first();
+        var dataParam = Def.defTele(def.ref).getFirst();
         var sort = dataParam.type();    // the sort of type below.
         var hole = ctx.freshHole(sort, arr.sourcePos());
         var type = new DataCall(def.ref(), 0, ImmutableSeq.of(

base/src/main/java/org/aya/tyck/env/LocalCtx.java

@@ -89,6 +89,10 @@ default void forward(@NotNull LocalCtx dest, @NotNull Term term, @NotNull TyckSt
       }
     }.accept(term);
   }
+
+  /**
+   * Perform {@param action} under this context + ({@param var} : {@param type})
+   */
   default <T> T with(@NotNull LocalVar var, @NotNull Term type, @NotNull Supplier<T> action) {
     put(var, type);
     try {
@@ -97,9 +101,17 @@ default <T> T with(@NotNull LocalVar var, @NotNull Term type, @NotNull Supplier<
       remove(SeqView.of(var));
     }
   }
+
+  /**
+   * Perform {@param action} under this context + {@param param}
+   */
   default <T> T with(@NotNull Supplier<T> action, @NotNull Term.Param... param) {
     return with(action, Seq.of(param).view());
   }
+
+  /**
+   * Perform {@param action} under this context + {@param param}
+   */
   default <T> T with(@NotNull Supplier<T> action, @NotNull SeqView<Term.Param> param) {
     for (var p : param) put(p);
     try {
@@ -108,6 +120,10 @@ default <T> T with(@NotNull Supplier<T> action, @NotNull SeqView<Term.Param> par
       remove(param.map(Term.Param::ref));
     }
   }
+
+  /**
+   * @return this context in telescope style
+   */
   default @NotNull ImmutableSeq<Term.Param> extract() {
     var ctx = MutableList.<Term.Param>create();
     var map = this;
@@ -117,6 +133,7 @@ default <T> T with(@NotNull Supplier<T> action, @NotNull SeqView<Term.Param> par
     }
     return ctx.toImmutableSeq();
   }
+
   @Contract(mutates = "param1") void extractToLocal(@NotNull MutableList<Term.Param> dest);
   @Contract(pure = true) default @NotNull Term get(@NotNull LocalVar var) {
     var res = getUnchecked(var);

base/src/main/java/org/aya/tyck/env/SeqLocalCtx.java

@@ -31,7 +31,7 @@ public record P(@NotNull LocalVar var, @NotNull Term type) {
   }
 
   @Override public @Nullable Term getLocal(@NotNull LocalVar var) {
-    return localSeq.firstOption(p -> p.var.equals(var)).map(p -> p.type).getOrNull();
+    return localSeq.findFirst(p -> p.var.equals(var)).map(p -> p.type).getOrNull();
   }
 
   @Override public void putUnchecked(@NotNull LocalVar var, @NotNull Term term) {

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

@@ -147,7 +147,7 @@ case InTerm(var phi, var u) -> {
       }
       case OutTerm outS -> {
         var ty = tryPress(outS.of());
-        if (ty instanceof PrimCall sub) yield sub.args().first().term();
+        if (ty instanceof PrimCall sub) yield sub.args().getFirst().term();
         yield null;
       }
       case PAppTerm app -> {

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

@@ -211,7 +211,7 @@ private <T> T checkParams(
   ) {
     if (!l.sizeEquals(r)) return fail.get();
     if (l.isEmpty()) return success.apply(lsub, rsub);
-    return checkParam(l.first(), r.first(), lsub, rsub, lr, rl, fail, (ls, rs) ->
+    return checkParam(l.getFirst(), r.getFirst(), lsub, rsub, lr, rl, fail, (ls, rs) ->
       checkParams(l.drop(1), r.drop(1), ls, rs, lr, rl, fail, success));
   }
 
@@ -227,7 +227,7 @@ private boolean visitLists(SeqView<Term> l, SeqView<Term> r, Sub lr, Sub rl, @No
     var ru = r.toImmutableSeq();
     for (int i = 0; lu.sizeGreaterThan(i); i++) {
       var li = lu.get(i);
-      var head = typesSubst.first();
+      var head = typesSubst.getFirst();
       if (!compare(li, ru.get(i), lr, rl, head.type())) return false;
       typesSubst = typesSubst.drop(1).map(type -> type.subst(head.ref(), li));
     }
@@ -277,7 +277,7 @@ case SigmaTerm(var paramsSeq) -> {
         var params = paramsSeq.view();
         for (int i = 1, size = paramsSeq.size(); i <= size; i++) {
           var l = ProjTerm.proj(lhs, i);
-          var currentParam = params.first();
+          var currentParam = params.getFirst();
           ctx.put(currentParam);
           if (!compare(l, ProjTerm.proj(rhs, i), lr, rl, currentParam.type())) yield false;
           params = params.drop(1).map(x -> x.subst(currentParam.ref(), l));
@@ -450,12 +450,12 @@ case AppTerm(var lOf, var lArg) -> {
         var subst = new Subst(MutableMap.create());
         for (int i = 1; i < lhs.ix(); i++) {
           var l = ProjTerm.proj(lhs, i);
-          var currentParam = params.first();
+          var currentParam = params.getFirst();
           subst.add(currentParam.ref(), l);
           params = params.drop(1);
         }
-        if (params.isNotEmpty()) yield params.first().subst(subst).type();
-        yield params.last().subst(subst).type();
+        if (params.isNotEmpty()) yield params.getFirst().subst(subst).type();
+        yield params.getLast().subst(subst).type();
       }
       case FormulaTerm lhs -> {
         if (!(preRhs instanceof FormulaTerm rhs)) yield null;

base/src/test/java/org/aya/concrete/ParseTest.java

@@ -172,19 +172,19 @@ def uncurry (A : Type) (B : Type) (C : Type)
   }
 
   private void parseImport(@Language("Aya") String code) {
-    assertTrue(parseStmt(code).first() instanceof Command.Import s && !s.toDoc(AyaPrettierOptions.debug()).debugRender().isEmpty());
+    assertTrue(parseStmt(code).getFirst() instanceof Command.Import s && !s.toDoc(AyaPrettierOptions.debug()).debugRender().isEmpty());
   }
 
   private void parseOpen(@Language("Aya") String code) {
     assertTrue(parseStmt(code).last() instanceof Command.Open s && !s.toDoc(AyaPrettierOptions.debug()).debugRender().isEmpty());
   }
 
   private void parseFn(@Language("Aya") String code) {
-    assertTrue(parseDecl(code).first() instanceof TeleDecl.FnDecl s && !s.toDoc(AyaPrettierOptions.debug()).debugRender().isEmpty());
+    assertTrue(parseDecl(code).getFirst() instanceof TeleDecl.FnDecl s && !s.toDoc(AyaPrettierOptions.debug()).debugRender().isEmpty());
   }
 
   private void parseData(@Language("Aya") String code) {
-    assertTrue(parseDecl(code).first() instanceof TeleDecl.DataDecl);
+    assertTrue(parseDecl(code).getFirst() instanceof TeleDecl.DataDecl);
   }
 
   @Test

cli-impl/src/test/java/org/aya/cli/ModifierParserTest.java

@@ -44,7 +44,7 @@ public class ModifierParserTest {
     assertEquals(1, reporter.problems().size());
     assertEquals(1, reporter.problemSize(Problem.Severity.WARN));
 
-    var warn = reporter.problems().first();
+    var warn = reporter.problems().getFirst();
     assertInstanceOf(ModifierProblem.class, warn);
     assertEquals(Private, ((ModifierProblem) warn).modifier());
 

ide-lsp/src/test/java/org/aya/lsp/LspTest.java

@@ -57,7 +57,7 @@ public class LspTest {
         .filter(x -> x.ref.name().equals("test"))
         .firstOption();
       assertFalse(testOpt.isEmpty(), "Do not delete the function called test in Vec");
-      var testClause = ((TeleDecl.BlockBody) testOpt.get().body).clauses().first();
+      var testClause = ((TeleDecl.BlockBody) testOpt.get().body).clauses().getFirst();
       // vnil, ys => 0
       var testPat = (Pattern.Bind) testClause.patterns.last().term();
       var testTy = assertInstanceOf(DataCall.class, testPat.type().get());