From 6c198d206be10e2ad06ca8d6301fc4ab0055f44b Mon Sep 17 00:00:00 2001 From: ice1000 Date: Sat, 11 Nov 2023 16:11:37 -0500 Subject: [PATCH 1/3] ci: remove mentioning of bors --- .github/README.md | 1 - bors.toml | 3 --- .../main/groovy/org/aya/gradle/JdkUrls.java | 27 ------------------- 3 files changed, 31 deletions(-) delete mode 100644 bors.toml delete mode 100644 buildSrc/src/main/groovy/org/aya/gradle/JdkUrls.java diff --git a/.github/README.md b/.github/README.md index 69a34f6128..ec9e2ffc0f 100644 --- a/.github/README.md +++ b/.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: diff --git a/bors.toml b/bors.toml deleted file mode 100644 index e08612e8b9..0000000000 --- a/bors.toml +++ /dev/null @@ -1,3 +0,0 @@ -status = ["gradle-check", "commit-check"] -commit_title = "merge: ${PR_REFS}" -delete_merged_branches = true diff --git a/buildSrc/src/main/groovy/org/aya/gradle/JdkUrls.java b/buildSrc/src/main/groovy/org/aya/gradle/JdkUrls.java deleted file mode 100644 index f604ae4400..0000000000 --- a/buildSrc/src/main/groovy/org/aya/gradle/JdkUrls.java +++ /dev/null @@ -1,27 +0,0 @@ -// 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.gradle; - -import org.jetbrains.annotations.NotNull; - -// TODO: move to build utils -public record JdkUrls(int javaVersion, String platform) { - public @NotNull String libericaJDK() { - var libericaJdkVersion = System.getProperty("java.vm.version"); - - var fixAmd64 = platform.replace("x64", "amd64"); - var suffix = platform.contains("linux") ? "tar.gz" : "zip"; - // "https://download.bell-sw.com/java/${libericaJdkVersion}/bellsoft-jdk${libericaJdkVersion}-${fixAmd64}.$suffix" - return "https://download.bell-sw.com/java/" + libericaJdkVersion + "/bellsoft-jdk" - + libericaJdkVersion + '-' + fixAmd64 + '.' + suffix; - } - - public @NotNull String riscv64JDK() { - return "https://github.com/imkiva/openjdk-riscv-build/releases/download/bootstrap/openjdk-jdk" + javaVersion + "-" + platform + ".tar.gz"; - } - - public @NotNull String jdk() { - if (platform.contains("linux") && platform.contains("riscv")) return riscv64JDK(); - return libericaJDK(); - } -} From 607a989fdf7e9ab8f3c8490084bb1d4d6424d068 Mon Sep 17 00:00:00 2001 From: ice1000 Date: Tue, 6 Dec 2022 10:25:53 -0500 Subject: [PATCH 2/3] kala: `first` & `last` --- base/src/main/java/org/aya/concrete/Expr.java | 2 +- .../java/org/aya/concrete/stmt/QualifiedID.java | 2 +- base/src/main/java/org/aya/core/def/PrimDef.java | 10 +++++----- .../main/java/org/aya/core/term/PathTerm.java | 2 +- .../main/java/org/aya/core/term/SigmaTerm.java | 2 +- base/src/main/java/org/aya/generic/Shaped.java | 4 ++-- .../java/org/aya/prettier/ConcretePrettier.java | 10 ++++------ .../main/java/org/aya/prettier/CorePrettier.java | 6 +++--- .../java/org/aya/resolve/error/NameProblem.java | 2 +- .../java/org/aya/tyck/error/HoleProblem.java | 2 +- .../java/org/aya/tyck/order/AyaSccTycker.java | 4 ++-- .../java/org/aya/tyck/tycker/UnifiedTycker.java | 2 +- .../main/java/org/aya/cli/parse/AyaProducer.java | 16 ++++++++-------- .../main/java/org/aya/cli/parse/FlclParser.java | 2 +- .../java/org/aya/cli/parse/ModifierParser.java | 2 +- .../org/aya/cli/render/vscode/ColorTheme.java | 2 +- .../java/org/aya/cli/single/SingleAyaFile.java | 10 +++++----- .../org/aya/literate/parser/BaseMdParser.java | 8 ++++---- .../src/main/java/org/aya/repl/CommandArg.java | 8 ++++---- .../main/java/org/aya/repl/CommandManager.java | 2 +- .../src/main/java/org/aya/repl/ReplParser.java | 4 ++-- tools/src/main/java/org/aya/util/FileUtil.java | 2 +- .../java/org/aya/util/binop/BinOpParser.java | 4 ++-- .../main/java/org/aya/util/terck/Selector.java | 4 ++-- .../org/aya/util/tyck/pat/ClassifierUtil.java | 4 ++-- 25 files changed, 57 insertions(+), 59 deletions(-) diff --git a/base/src/main/java/org/aya/concrete/Expr.java b/base/src/main/java/org/aya/concrete/Expr.java index 949a809602..57afc8dbf6 100644 --- a/base/src/main/java/org/aya/concrete/Expr.java +++ b/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)); } } diff --git a/base/src/main/java/org/aya/concrete/stmt/QualifiedID.java b/base/src/main/java/org/aya/concrete/stmt/QualifiedID.java index 03dd4a0616..d5cfe47ad8 100644 --- a/base/src/main/java/org/aya/concrete/stmt/QualifiedID.java +++ b/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 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) { diff --git a/base/src/main/java/org/aya/core/def/PrimDef.java b/base/src/main/java/org/aya/core/def/PrimDef.java index 853517d4b0..427529fd87 100644 --- a/base/src/main/java/org/aya/core/def/PrimDef.java +++ b/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 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); } diff --git a/base/src/main/java/org/aya/core/term/PathTerm.java b/base/src/main/java/org/aya/core/term/PathTerm.java index 5b8793d795..e44e410fc2 100644 --- a/base/src/main/java/org/aya/core/term/PathTerm.java +++ b/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 -> { diff --git a/base/src/main/java/org/aya/core/term/SigmaTerm.java b/base/src/main/java/org/aya/core/term/SigmaTerm.java index cf5c96b0fd..a6edd4f5a4 100644 --- a/base/src/main/java/org/aya/core/term/SigmaTerm.java +++ b/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(); diff --git a/base/src/main/java/org/aya/generic/Shaped.java b/base/src/main/java/org/aya/generic/Shaped.java index 08f4ec87c8..c5edcd04bb 100644 --- a/base/src/main/java/org/aya/generic/Shaped.java +++ b/base/src/main/java/org/aya/generic/Shaped.java @@ -93,12 +93,12 @@ default boolean compareUntyped(@NotNull Shaped.List 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)); } } diff --git a/base/src/main/java/org/aya/prettier/ConcretePrettier.java b/base/src/main/java/org/aya/prettier/ConcretePrettier.java index 528ae9a2bc..7f27cd4d59 100644 --- a/base/src/main/java/org/aya/prettier/ConcretePrettier.java +++ b/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)); diff --git a/base/src/main/java/org/aya/prettier/CorePrettier.java b/base/src/main/java/org/aya/prettier/CorePrettier.java index 837c530581..66a0231033 100644 --- a/base/src/main/java/org/aya/prettier/CorePrettier.java +++ b/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> 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; diff --git a/base/src/main/java/org/aya/resolve/error/NameProblem.java b/base/src/main/java/org/aya/resolve/error/NameProblem.java index b8c14d5fdc..fedc2ca289 100644 --- a/base/src/main/java/org/aya/resolve/error/NameProblem.java +++ b/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); diff --git a/base/src/main/java/org/aya/tyck/error/HoleProblem.java b/base/src/main/java/org/aya/tyck/error/HoleProblem.java index d1ec944286..5b62285831 100644 --- a/base/src/main/java/org/aya/tyck/error/HoleProblem.java +++ b/base/src/main/java/org/aya/tyck/error/HoleProblem.java @@ -96,7 +96,7 @@ record CannotFindGeneralSolution( @NotNull ImmutableSeq eqns ) implements Problem { @Override public @NotNull SourcePos sourcePos() { - return eqns.last().pos(); + return eqns.getLast().pos(); } @Override public @NotNull SeqView> inlineHints(@NotNull PrettierOptions options) { diff --git a/base/src/main/java/org/aya/tyck/order/AyaSccTycker.java b/base/src/main/java/org/aya/tyck/order/AyaSccTycker.java index be3d37ceac..c810147fc5 100644 --- a/base/src/main/java/org/aya/tyck/order/AyaSccTycker.java +++ b/base/src/main/java/org/aya/tyck/order/AyaSccTycker.java @@ -60,7 +60,7 @@ public record AyaSccTycker( public @NotNull ImmutableSeq tyckSCC(@NotNull ImmutableSeq 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 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() .map(TyckOrder.Head::new) diff --git a/base/src/main/java/org/aya/tyck/tycker/UnifiedTycker.java b/base/src/main/java/org/aya/tyck/tycker/UnifiedTycker.java index bbf1b70d80..73e36e6d58 100644 --- a/base/src/main/java/org/aya/tyck/tycker/UnifiedTycker.java +++ b/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); diff --git a/cli-impl/src/main/java/org/aya/cli/parse/AyaProducer.java b/cli-impl/src/main/java/org/aya/cli/parse/AyaProducer.java index c8ca2cf6ce..c02ea0a464 100644 --- a/cli-impl/src/main/java/org/aya/cli/parse/AyaProducer.java +++ b/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 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 extends BooleanObjBiFunction, 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 extends BooleanObjBiFunction, T> // when no as, entirePos == innerPatternPos Arg 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 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) { diff --git a/cli-impl/src/main/java/org/aya/cli/parse/FlclParser.java b/cli-impl/src/main/java/org/aya/cli/parse/FlclParser.java index 7176e4e8e3..13b7006bd9 100644 --- a/cli-impl/src/main/java/org/aya/cli/parse/FlclParser.java +++ b/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); }); diff --git a/cli-impl/src/main/java/org/aya/cli/parse/ModifierParser.java b/cli-impl/src/main/java/org/aya/cli/parse/ModifierParser.java index 9883326227..e6a950cb1b 100644 --- a/cli-impl/src/main/java/org/aya/cli/parse/ModifierParser.java +++ b/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; } diff --git a/cli-impl/src/main/java/org/aya/cli/render/vscode/ColorTheme.java b/cli-impl/src/main/java/org/aya/cli/render/vscode/ColorTheme.java index f55c1a96eb..210ff111d0 100644 --- a/cli-impl/src/main/java/org/aya/cli/render/vscode/ColorTheme.java +++ b/cli-impl/src/main/java/org/aya/cli/render/vscode/ColorTheme.java @@ -102,7 +102,7 @@ public Option find(@NotNull String scope) { } public void findAndPut(@NotNull MutableMap putTo, @NotNull String key, @NotNull Seq scope, @NotNull Map 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(); diff --git a/cli-impl/src/main/java/org/aya/cli/single/SingleAyaFile.java b/cli-impl/src/main/java/org/aya/cli/single/SingleAyaFile.java index a74447748d..e69bcc3688 100644 --- a/cli-impl/src/main/java/org/aya/cli/single/SingleAyaFile.java +++ b/cli-impl/src/main/java/org/aya/cli/single/SingleAyaFile.java @@ -4,6 +4,7 @@ import kala.collection.immutable.ImmutableSeq; import kala.collection.mutable.MutableList; +import kala.function.BooleanObjBiFunction; import org.aya.cli.render.RenderOptions; import org.aya.cli.utils.CliEnums; import org.aya.cli.utils.LiterateData; @@ -32,7 +33,6 @@ import java.io.IOException; import java.nio.file.Path; -import java.util.function.BiFunction; public sealed interface SingleAyaFile extends GenericAyaFile { private static @Nullable CompilerFlags.PrettyInfo parsePrettyInfo(@NotNull CompilerFlags flags) { @@ -69,7 +69,7 @@ public sealed interface SingleAyaFile extends GenericAyaFile { FileUtil.writeString(prettyDir.resolve(fileName), text); } else { doWrite(doc, prettyDir, flags.prettierOptions(), fileName, out.fileExt, - (d, hdr) -> renderOptions.render(out, d, flags.backendOpts(hdr))); + (hdr, d) -> renderOptions.render(out, d, flags.backendOpts(hdr))); } } @VisibleForTesting default @NotNull Doc toDoc( @@ -83,7 +83,7 @@ public sealed interface SingleAyaFile extends GenericAyaFile { private void doWrite( ImmutableSeq doc, Path prettyDir, @NotNull PrettierOptions options, String fileName, String fileExt, - BiFunction toString + BooleanObjBiFunction toString ) throws IOException { var docs = MutableList.create(); var eachPrettyDir = prettyDir.resolve(fileName + ".each"); @@ -93,9 +93,9 @@ private void doWrite( var thisDoc = item.toDoc(options); docs.append(thisDoc); if (item instanceof PrimDef) continue; - FileUtil.writeString(eachPrettyDir.resolve(FileUtil.escapeFileName(nameOf(i, item)) + fileExt), toString.apply(thisDoc, false)); + FileUtil.writeString(eachPrettyDir.resolve(FileUtil.escapeFileName(nameOf(i, item)) + fileExt), toString.apply(false, thisDoc)); } - FileUtil.writeString(prettyDir.resolve(fileName), toString.apply(Doc.vcat(docs), true)); + FileUtil.writeString(prettyDir.resolve(fileName), toString.apply(true, Doc.vcat(docs))); } private static @NotNull String nameOf(int i, AyaDocile item) { diff --git a/tools-md/src/main/java/org/aya/literate/parser/BaseMdParser.java b/tools-md/src/main/java/org/aya/literate/parser/BaseMdParser.java index 8103bf3617..10ed4a7d0e 100644 --- a/tools-md/src/main/java/org/aya/literate/parser/BaseMdParser.java +++ b/tools-md/src/main/java/org/aya/literate/parser/BaseMdParser.java @@ -147,7 +147,7 @@ public BaseMdParser(@NotNull SourceFile file, @NotNull Reporter reporter, @NotNu } protected Literate flatten(@NotNull Seq children) { - return children.sizeEquals(1) ? children.first() + return children.sizeEquals(1) ? children.getFirst() : new Literate.Many(null, children.toImmutableSeq()); } @@ -169,7 +169,7 @@ protected Literate flatten(@NotNull Seq children) { codeBlocks = codeBlocks.filter(x -> x.sourcePos != null); var builder = new StringBuilder(file.sourceCode().length()); - @Nullable Literate.CodeBlock next = codeBlocks.firstOrNull(); + @Nullable Literate.CodeBlock next = codeBlocks.getFirstOrNull(); codeBlocks = codeBlocks.drop(1); for (var idx = 0; idx < file.sourceCode().length(); ++idx) { @@ -179,7 +179,7 @@ protected Literate flatten(@NotNull Seq children) { assert next.sourcePos != null : "Physical doesn't exist!!"; if (next.sourcePos.tokenEndIndex() < idx) { assert idx - next.sourcePos.tokenEndIndex() == 1; - next = codeBlocks.firstOrNull(); + next = codeBlocks.getFirstOrNull(); codeBlocks = codeBlocks.drop(1); } @@ -198,7 +198,7 @@ protected Literate flatten(@NotNull Seq children) { public @Nullable SourcePos fromSourceSpans(@NotNull Seq sourceSpans) { if (sourceSpans.isEmpty()) return null; - var startFrom = linesIndex.get(sourceSpans.first().getLineIndex()); + var startFrom = linesIndex.get(sourceSpans.getFirst().getLineIndex()); return fromSourceSpans(file, startFrom, sourceSpans); } diff --git a/tools-repl/src/main/java/org/aya/repl/CommandArg.java b/tools-repl/src/main/java/org/aya/repl/CommandArg.java index 23735db695..3253c070df 100644 --- a/tools-repl/src/main/java/org/aya/repl/CommandArg.java +++ b/tools-repl/src/main/java/org/aya/repl/CommandArg.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.repl; @@ -83,9 +83,9 @@ static > CommandArgImpl fromEither( return Enum.valueOf(enumClass, trimName); } catch (IllegalArgumentException ignored) { var one = Seq.of(enumClass.getEnumConstants()) - .firstOrNull(n -> n.name().toLowerCase().startsWith(trimName.toLowerCase())); - if (one == null) throw new IllegalArgumentException("No such enum constant: " + name); - return one; + .findFirst(n -> n.name().toLowerCase().startsWith(trimName.toLowerCase())); + if (one.isEmpty()) throw new IllegalArgumentException("No such enum constant: " + name); + return one.get(); } } diff --git a/tools-repl/src/main/java/org/aya/repl/CommandManager.java b/tools-repl/src/main/java/org/aya/repl/CommandManager.java index 3a1bbacd13..20487836b4 100644 --- a/tools-repl/src/main/java/org/aya/repl/CommandManager.java +++ b/tools-repl/src/main/java/org/aya/repl/CommandManager.java @@ -70,7 +70,7 @@ public record Clue( ) { public Command.Result run(@NotNull Object repl) throws Throwable { return switch (command.size()) { - case 1 -> command.first().invoke(repl, argument); + case 1 -> command.getFirst().invoke(repl, argument); case 0 -> Command.Result.err("Command `" + name + "` not found", true); default -> Command.Result.err(command.view() .flatMap(s -> s.owner.names()) diff --git a/tools-repl/src/main/java/org/aya/repl/ReplParser.java b/tools-repl/src/main/java/org/aya/repl/ReplParser.java index e14d625a28..d8c87004c5 100644 --- a/tools-repl/src/main/java/org/aya/repl/ReplParser.java +++ b/tools-repl/src/main/java/org/aya/repl/ReplParser.java @@ -62,11 +62,11 @@ public record ReplParsedLine( .view() .filterNot(lexer::isWhitespace) .toImmutableSeq(); - var wordOpt = tokens.firstOption(token -> + var wordOpt = tokens.findFirst(token -> lexer.containsOffset(token, cursor)); // In case we're in a whitespace or at the end if (wordOpt.isEmpty()) { - var tokenOpt = tokens.firstOption(tok -> lexer.startOffset(tok) >= cursor); + var tokenOpt = tokens.findFirst(tok -> lexer.startOffset(tok) >= cursor); if (tokenOpt.isEmpty()) return simplest(line, cursor, tokens.size(), tokens .map(tok -> textOf(line, tok)).asJava()); diff --git a/tools/src/main/java/org/aya/util/FileUtil.java b/tools/src/main/java/org/aya/util/FileUtil.java index 0b3ec7ba9b..86a2f328ee 100644 --- a/tools/src/main/java/org/aya/util/FileUtil.java +++ b/tools/src/main/java/org/aya/util/FileUtil.java @@ -69,6 +69,6 @@ static void deleteRecursively(@NotNull Path path) throws IOException { static @Nullable Path resolveFile(@NotNull SeqView basePaths, @NotNull Seq moduleName, String postfix) { return basePaths.map(basePath -> resolveFile(basePath, moduleName, postfix)) - .firstOrNull(Files::exists); + .findFirst(Files::exists).getOrNull(); } } diff --git a/tools/src/main/java/org/aya/util/binop/BinOpParser.java b/tools/src/main/java/org/aya/util/binop/BinOpParser.java index 36dd607946..3e238cb48e 100644 --- a/tools/src/main/java/org/aya/util/binop/BinOpParser.java +++ b/tools/src/main/java/org/aya/util/binop/BinOpParser.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.util.binop; @@ -104,7 +104,7 @@ public BinOpParser(@NotNull OpSet opSet, @NotNull SeqView<@NotNull Elm> seq) { } assert prefixes.sizeEquals(1); - return prefixes.first().term(); + return prefixes.getFirst().term(); } protected abstract void reportAmbiguousPred(String op1, String op2, SourcePos pos); diff --git a/tools/src/main/java/org/aya/util/terck/Selector.java b/tools/src/main/java/org/aya/util/terck/Selector.java index f1adab0df5..58cc7dad9e 100644 --- a/tools/src/main/java/org/aya/util/terck/Selector.java +++ b/tools/src/main/java/org/aya/util/terck/Selector.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.util.terck; @@ -21,7 +21,7 @@ record Evolve(@NotNull SeqView junks, @NotNull SeqView betters) impleme static > @NotNull Result select(@NotNull A a, @NotNull SeqView had) { if (had.isEmpty()) return new Evolve<>(SeqView.empty(), SeqView.empty()); - var b = had.first(); + var b = had.getFirst(); var bs = had.drop(1); // The code below looks confusing on "what is better?". // In Relation class, we say `a` is better than `b` if a decreases more. diff --git a/tools/src/main/java/org/aya/util/tyck/pat/ClassifierUtil.java b/tools/src/main/java/org/aya/util/tyck/pat/ClassifierUtil.java index 3d97a3e1f9..049e93df03 100644 --- a/tools/src/main/java/org/aya/util/tyck/pat/ClassifierUtil.java +++ b/tools/src/main/java/org/aya/util/tyck/pat/ClassifierUtil.java @@ -28,9 +28,9 @@ public interface ClassifierUtil { ) { if (params.isEmpty()) return ImmutableSeq.of(new PatClass<>( ImmutableSeq.empty(), Indexed.indices(clauses))); - var first = params.first(); + var first = params.getFirst(); var cls = classify1(subst, subst(subst, first), - clauses.mapIndexed((ix, it) -> new Indexed<>(normalize(it.pat().first()), ix)), fuel); + clauses.mapIndexed((ix, it) -> new Indexed<>(normalize(it.pat().getFirst()), ix)), fuel); return cls.flatMap(subclauses -> classifyN(add(subst, ref(first), subclauses.term().term()), // Drop heads of both From fe6ae514837a6b52c0e023b677e0eb7a5dbcf77c Mon Sep 17 00:00:00 2001 From: ice1000 Date: Sat, 11 Nov 2023 17:03:38 -0500 Subject: [PATCH 3/3] docs: update, also update ci --- .github/README.md | 8 +++++--- .github/workflows/commit-check.yaml | 2 -- .github/workflows/gradle-check.yaml | 2 +- 3 files changed, 6 insertions(+), 6 deletions(-) diff --git a/.github/README.md b/.github/README.md index ec9e2ffc0f..a6b333fdda 100644 --- a/.github/README.md +++ b/.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 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. @@ -113,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]. diff --git a/.github/workflows/commit-check.yaml b/.github/workflows/commit-check.yaml index fab65f188b..c009e0b1ce 100644 --- a/.github/workflows/commit-check.yaml +++ b/.github/workflows/commit-check.yaml @@ -1,7 +1,5 @@ name: commit message on: - push: - branches: [staging, trying] pull_request: branches: [main] merge_group: diff --git a/.github/workflows/gradle-check.yaml b/.github/workflows/gradle-check.yaml index 1218e860da..54db430f5f 100644 --- a/.github/workflows/gradle-check.yaml +++ b/.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: