From 451a843ed60de0da08ca4f0b6151600c58258adf Mon Sep 17 00:00:00 2001 From: ice1000 Date: Tue, 12 Dec 2023 23:54:30 -0500 Subject: [PATCH] java: use Java 21 features --- .../java/org/aya/concrete/desugar/Desugarer.java | 2 +- .../src/main/java/org/aya/core/term/FormulaTerm.java | 4 ++-- .../main/java/org/aya/prettier/ConcretePrettier.java | 8 ++++---- .../src/main/java/org/aya/prettier/CorePrettier.java | 2 +- .../main/java/org/aya/tyck/unify/TermComparator.java | 10 +++++----- .../java/org/aya/literate/HighlighterTester.java | 12 ++++++------ .../java/org/aya/cli/literate/SyntaxHighlight.java | 10 +++++----- .../src/main/java/org/aya/cli/parse/AyaProducer.java | 2 +- .../java/org/aya/lsp/models/HighlightResult.java | 4 ++-- .../org/aya/pretty/backend/html/Html5Stylist.java | 4 ++-- .../org/aya/pretty/backend/latex/TeXStylist.java | 2 +- .../org/aya/pretty/backend/string/StringPrinter.java | 2 +- .../java/org/aya/literate/parser/BaseMdParser.java | 6 +++--- 13 files changed, 34 insertions(+), 34 deletions(-) diff --git a/base/src/main/java/org/aya/concrete/desugar/Desugarer.java b/base/src/main/java/org/aya/concrete/desugar/Desugarer.java index c8be916672..999635d0d0 100644 --- a/base/src/main/java/org/aya/concrete/desugar/Desugarer.java +++ b/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); }; } diff --git a/base/src/main/java/org/aya/core/term/FormulaTerm.java b/base/src/main/java/org/aya/core/term/FormulaTerm.java index 18f2e2af52..581d4e6f01 100644 --- a/base/src/main/java/org/aya/core/term/FormulaTerm.java +++ b/base/src/main/java/org/aya/core/term/FormulaTerm.java @@ -45,9 +45,9 @@ public record FormulaTerm(@NotNull Formula asFormula) implements Term { public @NotNull SeqView 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(); }; } } diff --git a/base/src/main/java/org/aya/prettier/ConcretePrettier.java b/base/src/main/java/org/aya/prettier/ConcretePrettier.java index 7f27cd4d59..30fae9f105 100644 --- a/base/src/main/java/org/aya/prettier/ConcretePrettier.java +++ b/base/src/main/java/org/aya/prettier/ConcretePrettier.java @@ -155,7 +155,7 @@ yield visitCalls(null, fn, (nc, l) -> l.toDoc(options), outer, } 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,9 +260,9 @@ private Doc partial(Expr.PartEl el) { 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); @@ -270,7 +270,7 @@ private Doc partial(Expr.PartEl el) { 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); } diff --git a/base/src/main/java/org/aya/prettier/CorePrettier.java b/base/src/main/java/org/aya/prettier/CorePrettier.java index 80fed17e34..a444171ec4 100644 --- a/base/src/main/java/org/aya/prettier/CorePrettier.java +++ b/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) diff --git a/base/src/main/java/org/aya/tyck/unify/TermComparator.java b/base/src/main/java/org/aya/tyck/unify/TermComparator.java index dc29c78647..a6dc540c38 100644 --- a/base/src/main/java/org/aya/tyck/unify/TermComparator.java +++ b/base/src/main/java/org/aya/tyck/unify/TermComparator.java @@ -278,11 +278,11 @@ private boolean doCompareTyped(@NotNull Term type, @NotNull Term lhs, @NotNull T } 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++) { diff --git a/base/src/test/java/org/aya/literate/HighlighterTester.java b/base/src/test/java/org/aya/literate/HighlighterTester.java index 42a5b56d21..af4e000e42 100644 --- a/base/src/test/java/org/aya/literate/HighlighterTester.java +++ b/base/src/test/java/org/aya/literate/HighlighterTester.java @@ -91,7 +91,7 @@ public HighlighterTester(@NotNull String sourceCode, @NotNull ImmutableSeq actuals, @NotNull Seq { } - 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 actuals, @NotNull Seq 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(); } diff --git a/cli-impl/src/main/java/org/aya/cli/literate/SyntaxHighlight.java b/cli-impl/src/main/java/org/aya/cli/literate/SyntaxHighlight.java index 0f59d39097..6aea2e5a71 100644 --- a/cli-impl/src/main/java/org/aya/cli/literate/SyntaxHighlight.java +++ b/cli-impl/src/main/java/org/aya/cli/literate/SyntaxHighlight.java @@ -120,7 +120,7 @@ else if (SPECIAL_SYMBOL.contains(tokenType)) @Override public @NotNull MutableList fold(@NotNull MutableList acc, @NotNull Pattern pat) { return switch (pat) { - case Pattern.Number(var pos, var $) -> add(acc, LitKind.Int.toLit(pos)); + case Pattern.Number(var pos, _) -> add(acc, LitKind.Int.toLit(pos)); default -> StmtFolder.super.fold(acc, pat); }; } @@ -147,7 +147,7 @@ else if (SPECIAL_SYMBOL.contains(tokenType)) } private @NotNull HighlightInfo linkRef(@NotNull SourcePos sourcePos, @NotNull AnyVar var, @Nullable AyaDocile type) { - if (var instanceof LocalVar(var $, var $$, GenerateKind.Generalized(var origin))) + if (var instanceof LocalVar(var _, var _, GenerateKind.Generalized(var origin))) return linkRef(sourcePos, origin, type); return kindOf(var).toRef(sourcePos, BasePrettier.linkIdOf(currentFileModule, var), type); } @@ -155,7 +155,7 @@ else if (SPECIAL_SYMBOL.contains(tokenType)) @SuppressWarnings("unused") public static @NotNull DefKind kindOf(@NotNull AnyVar var) { return switch (var) { - case GeneralizedVar ignored -> DefKind.Generalized; + case GeneralizedVar _ -> DefKind.Generalized; case DefVar defVar -> { if (defVar.concrete instanceof TeleDecl.FnDecl || defVar.core instanceof FnDef) yield DefKind.Fn; @@ -171,8 +171,8 @@ else if (defVar.concrete instanceof ClassDecl || defVar.core instanceof ClassDef yield DefKind.Clazz; else throw new InternalException(STR."unknown def type: \{defVar}"); } - case LocalVar(var $, var $$, GenerateKind.Generalized(var $$$)) -> DefKind.Generalized; - case LocalVar ignored -> DefKind.LocalVar; + case LocalVar(_, _, GenerateKind.Generalized(_)) -> DefKind.Generalized; + case LocalVar _ -> DefKind.LocalVar; default -> DefKind.Unknown; }; } 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 c02ea0a464..f77c04c889 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 @@ -568,7 +568,7 @@ private interface LicitParser extends BooleanObjBiFunction, T> : newBody.childrenOfType(NEW_ARG).map(arg -> { var id = newArgField(arg.child(NEW_ARG_FIELD)); var bindings = arg.childrenOfType(TELE_PARAM_NAME).map(this::teleParamName) - .map(b -> b.map($ -> LocalVar.from(b))) + .map(b -> b.map(_ -> LocalVar.from(b))) .toImmutableSeq(); var body = expr(arg.child(EXPR)); return new Expr.Field<>(sourcePosOf(arg), id, bindings, body, MutableValue.create()); diff --git a/ide-lsp/src/main/java/org/aya/lsp/models/HighlightResult.java b/ide-lsp/src/main/java/org/aya/lsp/models/HighlightResult.java index 2e935b1215..66a92dfdb5 100644 --- a/ide-lsp/src/main/java/org/aya/lsp/models/HighlightResult.java +++ b/ide-lsp/src/main/java/org/aya/lsp/models/HighlightResult.java @@ -64,8 +64,8 @@ public record Symbol( case Prim -> Option.some(Kind.PrimRef); case Unknown -> Option.none(); }; - case HighlightInfo.Lit $ -> Option.none(); // handled by client - case HighlightInfo.Err $ -> Option.none(); // handled by client + case HighlightInfo.Lit _ -> Option.none(); // handled by client + case HighlightInfo.Err _ -> Option.none(); // handled by client }; } } diff --git a/pretty/src/main/java/org/aya/pretty/backend/html/Html5Stylist.java b/pretty/src/main/java/org/aya/pretty/backend/html/Html5Stylist.java index 45ef1064a9..3fd862e513 100644 --- a/pretty/src/main/java/org/aya/pretty/backend/html/Html5Stylist.java +++ b/pretty/src/main/java/org/aya/pretty/backend/html/Html5Stylist.java @@ -77,8 +77,8 @@ public ClassedPreset(@NotNull ClosingStylist delegate) { case Curly -> "text-decoration-style: wavy;"; }; var colorRef = switch (color) { - case Style.ColorHex(var rgb, var $) -> cssColor(rgb); - case Style.ColorName(var name, var $) -> "var(%s)".formatted(cssVar(name)); + case Style.ColorHex(var rgb, _) -> cssColor(rgb); + case Style.ColorName(var name, _) -> "var(%s)".formatted(cssVar(name)); case null -> null; }; var decoColor = colorRef != null diff --git a/pretty/src/main/java/org/aya/pretty/backend/latex/TeXStylist.java b/pretty/src/main/java/org/aya/pretty/backend/latex/TeXStylist.java index 6270cc6372..21b13e264f 100644 --- a/pretty/src/main/java/org/aya/pretty/backend/latex/TeXStylist.java +++ b/pretty/src/main/java/org/aya/pretty/backend/latex/TeXStylist.java @@ -87,7 +87,7 @@ public ClassedPreset(@NotNull ClosingStylist delegate) { case Italic -> Tuple.of("\\textit{", "}"); case Bold -> Tuple.of("\\textbf{", "}"); }; - case Style.LineThrough(var pos, var $, var $$) -> switch (pos) { + case Style.LineThrough(var pos, _, _) -> switch (pos) { case Strike -> Tuple.of("\\sout{", "}"); case Underline -> Tuple.of("\\underline{", "}"); case Overline -> null; diff --git a/pretty/src/main/java/org/aya/pretty/backend/string/StringPrinter.java b/pretty/src/main/java/org/aya/pretty/backend/string/StringPrinter.java index b66be18c97..5eec6eab13 100644 --- a/pretty/src/main/java/org/aya/pretty/backend/string/StringPrinter.java +++ b/pretty/src/main/java/org/aya/pretty/backend/string/StringPrinter.java @@ -112,7 +112,7 @@ protected void renderDoc(@NotNull Cursor cursor, @NotNull Doc doc, EnumSet renderInlineMath(cursor, inlineMath, outer); case Doc.MathBlock mathBlock -> renderMathBlock(cursor, mathBlock, outer); case Doc.Tooltip tooltip -> renderTooltip(cursor, tooltip, outer); - case Doc.Empty $ -> {} + case Doc.Empty _ -> {} } } 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 40d4c40667..a8e1554d33 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 @@ -89,8 +89,8 @@ public BaseMdParser(@NotNull SourceFile file, @NotNull Reporter reporter, @NotNu return switch (node) { case Text text -> new Literate.Raw(Doc.plain(text.getLiteral())); case Emphasis emphasis -> new Literate.Many(Style.italic(), mapChildren(emphasis)); - case HardLineBreak $ -> new Literate.Raw(Doc.line()); - case SoftLineBreak $ -> new Literate.Raw(Doc.line()); + case HardLineBreak _ -> new Literate.Raw(Doc.line()); + case SoftLineBreak _ -> new Literate.Raw(Doc.line()); case StrongEmphasis emphasis -> new Literate.Many(Style.bold(), mapChildren(emphasis)); case Paragraph p -> new Literate.Many(MdStyle.GFM.Paragraph, mapChildren(p)); case BlockQuote b -> new Literate.Many(MdStyle.GFM.BlockQuote, mapChildren(b)); @@ -125,7 +125,7 @@ public BaseMdParser(@NotNull SourceFile file, @NotNull Reporter reporter, @NotNu case Code inlineCode -> { var spans = inlineCode.getSourceSpans(); if (spans != null && spans.size() == 1) { - var sourceSpan = spans.get(0); + var sourceSpan = spans.getFirst(); var lineIndex = linesIndex.get(sourceSpan.getLineIndex()); var startFrom = lineIndex + sourceSpan.getColumnIndex(); var sourcePos = fromSourceSpans(file, startFrom, Seq.of(sourceSpan));