java: use Java 21 features

aya-prover · Dec 13, 2023 · 451a843 · 451a843
1 parent ee300d7
commit 451a843
Show file tree

Hide file tree

Showing 13 changed files with 34 additions and 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
@@ -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
@@ -45,9 +45,9 @@ public record FormulaTerm(@NotNull Formula<Term> asFormula) implements Term {
 
   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();
     };
   }
 }
diff --git 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,17 +260,17 @@ 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);
         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);
         }

diff --git 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
@@ -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
@@ -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();
   }

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
@@ -120,7 +120,7 @@ else if (SPECIAL_SYMBOL.contains(tokenType))
   @Override
   public @NotNull MutableList<HighlightInfo> fold(@NotNull MutableList<HighlightInfo> 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,15 +147,15 @@ 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);
   }
 
   @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
@@ -568,7 +568,7 @@ private interface LicitParser<T> extends BooleanObjBiFunction<GenericNode<?>, 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
@@ -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
@@ -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
@@ -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
@@ -112,7 +112,7 @@ protected void renderDoc(@NotNull Cursor cursor, @NotNull Doc doc, EnumSet<Outer
       case Doc.InlineMath inlineMath -> 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
@@ -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));