From 27fc2643a265689fc07334a9db98015cae911b38 Mon Sep 17 00:00:00 2001 From: ice1000 Date: Tue, 12 Dec 2023 19:17:12 -0500 Subject: [PATCH 01/10] deps: upgrade gradle --- base/src/main/java/org/aya/core/serde/SerTerm.java | 2 +- base/src/main/java/org/aya/core/term/IntegerTerm.java | 2 +- base/src/main/java/org/aya/generic/Shaped.java | 7 ++++--- gradle/wrapper/gradle-wrapper.properties | 2 +- 4 files changed, 7 insertions(+), 6 deletions(-) diff --git a/base/src/main/java/org/aya/core/serde/SerTerm.java b/base/src/main/java/org/aya/core/serde/SerTerm.java index d3e191c643..bced96028d 100644 --- a/base/src/main/java/org/aya/core/serde/SerTerm.java +++ b/base/src/main/java/org/aya/core/serde/SerTerm.java @@ -187,7 +187,7 @@ record ConReduceRule( public @NotNull Term de(@NotNull DeState state) { return new RuleReducer.Con( (Shaped.Applicable) head.deShape(state), - dataArgs().ulift, dataArgs.de(state), conArgs.map(x -> x.de(state)) + dataArgs.ulift, dataArgs.de(state), conArgs.map(x -> x.de(state)) ); } } diff --git a/base/src/main/java/org/aya/core/term/IntegerTerm.java b/base/src/main/java/org/aya/core/term/IntegerTerm.java index 0651430db1..29d8447299 100644 --- a/base/src/main/java/org/aya/core/term/IntegerTerm.java +++ b/base/src/main/java/org/aya/core/term/IntegerTerm.java @@ -44,7 +44,7 @@ public record IntegerTerm( var ctorTele = head().ref().core.selfTele; assert ctorTele.sizeEquals(1); - return ImmutableSeq.of(new Arg<>(new IntegerTerm(repr - 1, recognition, type), ctorTele.first().explicit())); + return ImmutableSeq.of(new Arg<>(new IntegerTerm(repr - 1, recognition, type), ctorTele.getFirst().explicit())); } @Override public @NotNull IntegerTerm descent(@NotNull UnaryOperator f, @NotNull UnaryOperator g) { diff --git a/base/src/main/java/org/aya/generic/Shaped.java b/base/src/main/java/org/aya/generic/Shaped.java index a814fb155a..8b5c747be0 100644 --- a/base/src/main/java/org/aya/generic/Shaped.java +++ b/base/src/main/java/org/aya/generic/Shaped.java @@ -9,7 +9,10 @@ import org.aya.core.pat.Pat; import org.aya.core.repr.CodeShape; import org.aya.core.repr.ShapeRecognition; -import org.aya.core.term.*; +import org.aya.core.term.DataCall; +import org.aya.core.term.IntegerTerm; +import org.aya.core.term.RuleReducer; +import org.aya.core.term.Term; import org.aya.ref.DefVar; import org.aya.tyck.unify.TermComparator; import org.aya.util.Arg; @@ -70,8 +73,6 @@ default boolean compareUntyped(@NotNull Shaped.Nat othe } @NotNull Shaped.Nat map(@NotNull IntUnaryOperator f); - - // int construct(@NotNull T term); } non-sealed interface List extends Inductive { diff --git a/gradle/wrapper/gradle-wrapper.properties b/gradle/wrapper/gradle-wrapper.properties index 3530e0f440..974619d93d 100644 --- a/gradle/wrapper/gradle-wrapper.properties +++ b/gradle/wrapper/gradle-wrapper.properties @@ -2,7 +2,7 @@ # Use of this source code is governed by the MIT license that can be found in the LICENSE.md file. distributionBase=GRADLE_USER_HOME distributionPath=wrapper/dists -distributionUrl=https\://services.gradle.org/distributions/gradle-8.4-bin.zip +distributionUrl=https\://services.gradle.org/distributions/gradle-8.5-bin.zip networkTimeout=10000 validateDistributionUrl=true zipStoreBase=GRADLE_USER_HOME From 1ce17ebfe8a9e760db5e5c5562685d634e958a22 Mon Sep 17 00:00:00 2001 From: ice1000 Date: Tue, 12 Dec 2023 21:58:04 -0500 Subject: [PATCH 02/10] docs: changelog --- .github/README.md | 6 +++--- gradle/libs.versions.toml | 4 +++- note/early-changelog.md | 18 +++++++++++++++++- settings.gradle.kts | 2 ++ 4 files changed, 25 insertions(+), 5 deletions(-) diff --git a/.github/README.md b/.github/README.md index 2eb427a93e..36dddde5ab 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 20]: https://jdk.java.net/20 +[Java 21]: https://jdk.java.net/21 [1lab]: https://1lab.dev ## Contributing to Aya -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. +Since you need [Java 21] to set this project up, in case your choice +of IDE is IntelliJ IDEA, version 2023.3 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. diff --git a/gradle/libs.versions.toml b/gradle/libs.versions.toml index d7d23d175b..17a7e1d231 100644 --- a/gradle/libs.versions.toml +++ b/gradle/libs.versions.toml @@ -5,7 +5,7 @@ project = "0.30-SNAPSHOT" # https://openjdk.org/ -java = "20" +java = "21" # https://github.com/JetBrains/java-annotations annotations = "24.0.1" @@ -44,6 +44,8 @@ aya-build-util = { group = "org.aya-prover.upstream", name = "build-util", versi aya-build-jflex = { group = "org.aya-prover.upstream", name = "build-util-jflex", version.ref = "build-util" } aya-guest0x0 = { group = "org.aya-prover.guest0x0", name = "cubical", version.ref = "guest0x0" } +kala-base = { group = "org.glavo.kala", name = "kala-base", version.ref = "kala" } +kala-collection = { group = "org.glavo.kala", name = "kala-collection", version.ref = "kala" } kala-common = { group = "org.glavo.kala", name = "kala-common", version.ref = "kala" } picocli-runtime = { group = "info.picocli", name = "picocli", version.ref = "picocli" } diff --git a/note/early-changelog.md b/note/early-changelog.md index 51d9e4103d..7775c05f93 100644 --- a/note/early-changelog.md +++ b/note/early-changelog.md @@ -2,7 +2,23 @@ This file contains the changelog of the Aya language 0.x. -Upgraded from Java 19 to Java 20. +## 0.30 + +Upgraded from Java 19 to Java 21. + +New features: + ++ Improve `Doc` implementation to account for the nested structure for real ++ Improve stability in pattern matching conversion check, pretty print (thanks @dannypsnl) ++ Clean up something related to `Prop` ++ Introduce the "fake literate" language, which allows one to generate beautifully annotated code using Aya's literate backend with custom, naïve syntax highlighting ++ Literate now works with library system ++ Use Gradle version catalog to replace `deps.properties` ++ Introduce `ij-parsing-wrapper` and use it in the parsing code ++ Improve `let` handling ++ Improve "count usages" in language server ++ The new classifier is in `tools` now ++ Loads of build system improvements Welcome [AliasQli](https://github.com/AliasQli)! diff --git a/settings.gradle.kts b/settings.gradle.kts index 7f3e36a622..9ca50af212 100644 --- a/settings.gradle.kts +++ b/settings.gradle.kts @@ -11,6 +11,8 @@ include( "cli-impl", "cli-console", "tools", + // Uses kala-primitives + "tools-kala", "tools-md", "tools-repl", "base", From acc3ad9b8352a16bf17f37aa6b39da8b030db64d Mon Sep 17 00:00:00 2001 From: ice1000 Date: Tue, 12 Dec 2023 22:11:30 -0500 Subject: [PATCH 03/10] proj: move source roots --- base/build.gradle.kts | 7 +++++-- tools-kala/build.gradle.kts | 6 ++++++ tools-kala/src/main/java/module-info.java | 9 +++++++++ .../src/main/java/org/aya/util/terck/CallGraph.java | 2 +- .../src/main/java/org/aya/util/terck/CallMatrix.java | 2 +- .../src/main/java/org/aya/util/terck/Diagonal.java | 12 ++++++------ .../main/java/org/aya/util/terck/MutableGraph.java | 2 +- .../src/main/java/org/aya/util/terck/Relation.java | 0 .../src/main/java/org/aya/util/terck/Selector.java | 0 .../java/org/aya/util/tyck/pat/ClassifierUtil.java | 0 .../src/main/java/org/aya/util/tyck/pat/Indexed.java | 0 .../main/java/org/aya/util/tyck/pat/PatClass.java | 0 tools-repl/build.gradle.kts | 5 ++--- tools/build.gradle.kts | 2 +- tools/src/main/java/module-info.java | 2 -- 15 files changed, 32 insertions(+), 17 deletions(-) create mode 100644 tools-kala/build.gradle.kts create mode 100644 tools-kala/src/main/java/module-info.java rename {tools => tools-kala}/src/main/java/org/aya/util/terck/CallGraph.java (99%) rename {tools => tools-kala}/src/main/java/org/aya/util/terck/CallMatrix.java (98%) rename {tools => tools-kala}/src/main/java/org/aya/util/terck/Diagonal.java (71%) rename {tools => tools-kala}/src/main/java/org/aya/util/terck/MutableGraph.java (98%) rename {tools => tools-kala}/src/main/java/org/aya/util/terck/Relation.java (100%) rename {tools => tools-kala}/src/main/java/org/aya/util/terck/Selector.java (100%) rename {tools => tools-kala}/src/main/java/org/aya/util/tyck/pat/ClassifierUtil.java (100%) rename {tools => tools-kala}/src/main/java/org/aya/util/tyck/pat/Indexed.java (100%) rename {tools => tools-kala}/src/main/java/org/aya/util/tyck/pat/PatClass.java (100%) diff --git a/base/build.gradle.kts b/base/build.gradle.kts index 9781777587..28274b41f2 100644 --- a/base/build.gradle.kts +++ b/base/build.gradle.kts @@ -1,10 +1,13 @@ // 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. -import org.aya.gradle.* +import org.aya.gradle.CommonTasks +import org.aya.gradle.GenerateReflectionConfigTask +import org.aya.gradle.GenerateVersionTask + CommonTasks.nativeImageConfig(project) dependencies { - api(project(":tools")) + api(project(":tools-kala")) api(project(":tools-md")) api(project(":pretty")) api(libs.aya.guest0x0) diff --git a/tools-kala/build.gradle.kts b/tools-kala/build.gradle.kts new file mode 100644 index 0000000000..d01878aa0d --- /dev/null +++ b/tools-kala/build.gradle.kts @@ -0,0 +1,6 @@ +// 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. +dependencies { + api(libs.kala.common) + api(project(":tools")) +} diff --git a/tools-kala/src/main/java/module-info.java b/tools-kala/src/main/java/module-info.java new file mode 100644 index 0000000000..cfa08cf9ec --- /dev/null +++ b/tools-kala/src/main/java/module-info.java @@ -0,0 +1,9 @@ +module aya.util.kala { + requires transitive aya.util; + + requires static org.jetbrains.annotations; + requires transitive kala.collection.primitive; + + exports org.aya.util.tyck.pat; + exports org.aya.util.terck; +} diff --git a/tools/src/main/java/org/aya/util/terck/CallGraph.java b/tools-kala/src/main/java/org/aya/util/terck/CallGraph.java similarity index 99% rename from tools/src/main/java/org/aya/util/terck/CallGraph.java rename to tools-kala/src/main/java/org/aya/util/terck/CallGraph.java index 2b36a781d2..50ca2d84df 100644 --- a/tools/src/main/java/org/aya/util/terck/CallGraph.java +++ b/tools-kala/src/main/java/org/aya/util/terck/CallGraph.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; diff --git a/tools/src/main/java/org/aya/util/terck/CallMatrix.java b/tools-kala/src/main/java/org/aya/util/terck/CallMatrix.java similarity index 98% rename from tools/src/main/java/org/aya/util/terck/CallMatrix.java rename to tools-kala/src/main/java/org/aya/util/terck/CallMatrix.java index d37b1e9f7d..0a08d609eb 100644 --- a/tools/src/main/java/org/aya/util/terck/CallMatrix.java +++ b/tools-kala/src/main/java/org/aya/util/terck/CallMatrix.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; diff --git a/tools/src/main/java/org/aya/util/terck/Diagonal.java b/tools-kala/src/main/java/org/aya/util/terck/Diagonal.java similarity index 71% rename from tools/src/main/java/org/aya/util/terck/Diagonal.java rename to tools-kala/src/main/java/org/aya/util/terck/Diagonal.java index 8114950176..1a9d2f1953 100644 --- a/tools/src/main/java/org/aya/util/terck/Diagonal.java +++ b/tools-kala/src/main/java/org/aya/util/terck/Diagonal.java @@ -1,23 +1,23 @@ -// 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; import kala.collection.immutable.ImmutableSeq; +import kala.collection.mutable.MutableList; +import kala.range.primitive.IntRange; import org.aya.pretty.doc.Doc; import org.aya.pretty.doc.Docile; import org.jetbrains.annotations.NotNull; -import java.util.stream.IntStream; - public record Diagonal( @NotNull CallMatrix matrix, @NotNull ImmutableSeq diagonal ) implements Docile { public static @NotNull Diagonal create(@NotNull CallMatrix matrix) { assert matrix.rows() == matrix.cols(); - var diag = IntStream.range(0, matrix.rows()) - .mapToObj(i -> matrix.matrix()[i][i]) - .collect(ImmutableSeq.factory()); + var diag = IntRange.openClosed(0, matrix.rows()) + .mapToObjTo(MutableList.create(), i -> matrix.matrix()[i][i]) + .toImmutableSeq(); return new Diagonal<>(matrix, diag); } diff --git a/tools/src/main/java/org/aya/util/terck/MutableGraph.java b/tools-kala/src/main/java/org/aya/util/terck/MutableGraph.java similarity index 98% rename from tools/src/main/java/org/aya/util/terck/MutableGraph.java rename to tools-kala/src/main/java/org/aya/util/terck/MutableGraph.java index 987eb8a979..c241c77ac5 100644 --- a/tools/src/main/java/org/aya/util/terck/MutableGraph.java +++ b/tools-kala/src/main/java/org/aya/util/terck/MutableGraph.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; diff --git a/tools/src/main/java/org/aya/util/terck/Relation.java b/tools-kala/src/main/java/org/aya/util/terck/Relation.java similarity index 100% rename from tools/src/main/java/org/aya/util/terck/Relation.java rename to tools-kala/src/main/java/org/aya/util/terck/Relation.java diff --git a/tools/src/main/java/org/aya/util/terck/Selector.java b/tools-kala/src/main/java/org/aya/util/terck/Selector.java similarity index 100% rename from tools/src/main/java/org/aya/util/terck/Selector.java rename to tools-kala/src/main/java/org/aya/util/terck/Selector.java diff --git a/tools/src/main/java/org/aya/util/tyck/pat/ClassifierUtil.java b/tools-kala/src/main/java/org/aya/util/tyck/pat/ClassifierUtil.java similarity index 100% rename from tools/src/main/java/org/aya/util/tyck/pat/ClassifierUtil.java rename to tools-kala/src/main/java/org/aya/util/tyck/pat/ClassifierUtil.java diff --git a/tools/src/main/java/org/aya/util/tyck/pat/Indexed.java b/tools-kala/src/main/java/org/aya/util/tyck/pat/Indexed.java similarity index 100% rename from tools/src/main/java/org/aya/util/tyck/pat/Indexed.java rename to tools-kala/src/main/java/org/aya/util/tyck/pat/Indexed.java diff --git a/tools/src/main/java/org/aya/util/tyck/pat/PatClass.java b/tools-kala/src/main/java/org/aya/util/tyck/pat/PatClass.java similarity index 100% rename from tools/src/main/java/org/aya/util/tyck/pat/PatClass.java rename to tools-kala/src/main/java/org/aya/util/tyck/pat/PatClass.java diff --git a/tools-repl/build.gradle.kts b/tools-repl/build.gradle.kts index ef13223abb..04b1a7a8a1 100644 --- a/tools-repl/build.gradle.kts +++ b/tools-repl/build.gradle.kts @@ -1,8 +1,7 @@ -// 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. dependencies { - api(project(":pretty")) - api(project(":tools")) + api(project(":tools-kala")) api(libs.jline.reader) api(libs.jline.terminal.api) } diff --git a/tools/build.gradle.kts b/tools/build.gradle.kts index fd3a8e52e2..0a26a759d0 100644 --- a/tools/build.gradle.kts +++ b/tools/build.gradle.kts @@ -2,7 +2,7 @@ // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file. dependencies { api(libs.annotations) - api(libs.kala.common) + api(libs.kala.collection) api(project(":pretty")) implementation(libs.aya.ij.text) testImplementation(libs.junit.jupiter) diff --git a/tools/src/main/java/module-info.java b/tools/src/main/java/module-info.java index 6a40a0d8f4..a1f8861cd2 100644 --- a/tools/src/main/java/module-info.java +++ b/tools/src/main/java/module-info.java @@ -9,8 +9,6 @@ exports org.aya.util.error; exports org.aya.util.prettier; exports org.aya.util.reporter; - exports org.aya.util.terck; - exports org.aya.util.tyck.pat; exports org.aya.util.tyck; exports org.aya.util; } From 09490b82592f09b133ed2f1309115e495648253e Mon Sep 17 00:00:00 2001 From: ice1000 Date: Tue, 12 Dec 2023 22:41:32 -0500 Subject: [PATCH 04/10] proj: `tools` no longer depend on `kala-primitive` --- .../src/main/java/org/aya/cli/library/LibraryCompiler.java | 2 +- tools-kala/src/main/java/module-info.java | 3 ++- .../src/main/java/org/aya/util/more}/StringUtil.java | 2 +- 3 files changed, 4 insertions(+), 3 deletions(-) rename {tools/src/main/java/org/aya/util => tools-kala/src/main/java/org/aya/util/more}/StringUtil.java (98%) diff --git a/cli-impl/src/main/java/org/aya/cli/library/LibraryCompiler.java b/cli-impl/src/main/java/org/aya/cli/library/LibraryCompiler.java index 31ce957bce..8deac0e91e 100644 --- a/cli-impl/src/main/java/org/aya/cli/library/LibraryCompiler.java +++ b/cli-impl/src/main/java/org/aya/cli/library/LibraryCompiler.java @@ -26,8 +26,8 @@ import org.aya.resolve.error.NameProblem; import org.aya.resolve.module.CachedModuleLoader; import org.aya.resolve.module.ModuleLoader; -import org.aya.util.StringUtil; import org.aya.util.error.InternalException; +import org.aya.util.more.StringUtil; import org.aya.util.reporter.CountingReporter; import org.aya.util.reporter.Reporter; import org.aya.util.terck.MutableGraph; diff --git a/tools-kala/src/main/java/module-info.java b/tools-kala/src/main/java/module-info.java index cfa08cf9ec..18ef271d90 100644 --- a/tools-kala/src/main/java/module-info.java +++ b/tools-kala/src/main/java/module-info.java @@ -4,6 +4,7 @@ requires static org.jetbrains.annotations; requires transitive kala.collection.primitive; - exports org.aya.util.tyck.pat; + exports org.aya.util.more; exports org.aya.util.terck; + exports org.aya.util.tyck.pat; } diff --git a/tools/src/main/java/org/aya/util/StringUtil.java b/tools-kala/src/main/java/org/aya/util/more/StringUtil.java similarity index 98% rename from tools/src/main/java/org/aya/util/StringUtil.java rename to tools-kala/src/main/java/org/aya/util/more/StringUtil.java index 74032529f6..e687d09108 100644 --- a/tools/src/main/java/org/aya/util/StringUtil.java +++ b/tools-kala/src/main/java/org/aya/util/more/StringUtil.java @@ -1,6 +1,6 @@ // 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; +package org.aya.util.more; import kala.collection.immutable.ImmutableSeq; import kala.collection.mutable.MutableList; From 73e206de4624b0a6da3c80b245bfa327d8fed106 Mon Sep 17 00:00:00 2001 From: ice1000 Date: Tue, 12 Dec 2023 22:43:34 -0500 Subject: [PATCH 05/10] proj: move more to fix compile --- base/src/main/java/module-info.java | 2 ++ base/src/main/java/org/aya/concrete/Expr.java | 4 ++-- .../src/main/java/org/aya/prettier/BasePrettier.java | 12 ++++++------ pretty/build.gradle.kts | 6 +++--- tools-kala/src/main/java/module-info.java | 2 ++ .../src/main/java/org/aya/util/binop/Assoc.java | 2 +- .../main/java/org/aya/util/binop/BinOpParser.java | 7 ++----- .../src/main/java/org/aya/util/binop/BinOpSet.java | 2 +- .../src/main/java/org/aya/util/binop/OpDecl.java | 2 +- tools-md/build.gradle.kts | 2 +- tools-md/src/main/java/module-info.java | 2 ++ .../java/org/aya/literate/parser/BaseMdParser.java | 2 +- tools-repl/build.gradle.kts | 2 +- tools/src/main/java/module-info.java | 3 +-- tools/src/main/java/org/aya/util/Arg.java | 3 +-- tools/src/main/java/org/aya/util/BinOpElem.java | 10 ++++++++++ 16 files changed, 37 insertions(+), 26 deletions(-) rename {tools => tools-kala}/src/main/java/org/aya/util/binop/Assoc.java (94%) rename {tools => tools-kala}/src/main/java/org/aya/util/binop/BinOpParser.java (98%) rename {tools => tools-kala}/src/main/java/org/aya/util/binop/BinOpSet.java (98%) rename {tools => tools-kala}/src/main/java/org/aya/util/binop/OpDecl.java (91%) create mode 100644 tools/src/main/java/org/aya/util/BinOpElem.java diff --git a/base/src/main/java/module-info.java b/base/src/main/java/module-info.java index 2c83038d99..45d82812e4 100644 --- a/base/src/main/java/module-info.java +++ b/base/src/main/java/module-info.java @@ -2,6 +2,7 @@ requires transitive aya.md; requires transitive aya.pretty; requires transitive aya.util; + requires transitive aya.util.kala; requires transitive aya.guest.cubical; requires transitive kala.base; requires transitive kala.collection; @@ -15,6 +16,7 @@ exports org.aya.concrete.error; exports org.aya.concrete.remark; exports org.aya.concrete.stmt.decl; + exports org.aya.concrete.stmt; exports org.aya.concrete.visitor; exports org.aya.concrete; diff --git a/base/src/main/java/org/aya/concrete/Expr.java b/base/src/main/java/org/aya/concrete/Expr.java index 57afc8dbf6..b659d5de2c 100644 --- a/base/src/main/java/org/aya/concrete/Expr.java +++ b/base/src/main/java/org/aya/concrete/Expr.java @@ -28,8 +28,8 @@ import org.aya.resolve.visitor.ExprResolver; import org.aya.resolve.visitor.StmtShallowResolver; import org.aya.tyck.Result; +import org.aya.util.BinOpElem; import org.aya.util.ForLSP; -import org.aya.util.binop.BinOpParser; import org.aya.util.error.SourceNode; import org.aya.util.error.SourcePos; import org.aya.util.error.WithPos; @@ -158,7 +158,7 @@ record App( * @author AustinZhu */ record NamedArg(@Override boolean explicit, @Nullable String name, @Override @NotNull Expr term) - implements AyaDocile, SourceNode, BinOpParser.Elem { + implements AyaDocile, SourceNode, BinOpElem { public NamedArg(boolean explicit, @NotNull Expr expr) { this(explicit, null, expr); diff --git a/base/src/main/java/org/aya/prettier/BasePrettier.java b/base/src/main/java/org/aya/prettier/BasePrettier.java index bd79872973..6944ec2ea3 100644 --- a/base/src/main/java/org/aya/prettier/BasePrettier.java +++ b/base/src/main/java/org/aya/prettier/BasePrettier.java @@ -23,8 +23,8 @@ import org.aya.ref.DefVar; import org.aya.ref.LocalVar; import org.aya.util.Arg; +import org.aya.util.BinOpElem; import org.aya.util.binop.Assoc; -import org.aya.util.binop.BinOpParser; import org.aya.util.prettier.PrettierOptions; import org.jetbrains.annotations.NotNull; import org.jetbrains.annotations.Nullable; @@ -76,7 +76,7 @@ protected BasePrettier(@NotNull PrettierOptions options) { public @NotNull Doc visitCalls( @Nullable Assoc assoc, @NotNull Doc fn, - @NotNull SeqView> args, + @NotNull SeqView> args, @NotNull Outer outer, boolean showImplicits ) { return visitCalls(assoc, fn, this::term, outer, args, showImplicits); @@ -109,9 +109,9 @@ protected BasePrettier(@NotNull PrettierOptions options) { */ @NotNull Doc visitCalls( @Nullable Assoc assoc, @NotNull Doc fn, @NotNull Fmt fmt, Outer outer, - @NotNull SeqView> args, boolean showImplicits + @NotNull SeqView> args, boolean showImplicits ) { - var visibleArgs = (showImplicits ? args : args.filter(BinOpParser.Elem::explicit)).toImmutableSeq(); + var visibleArgs = (showImplicits ? args : args.filter(BinOpElem::explicit)).toImmutableSeq(); if (visibleArgs.isEmpty()) return assoc != null ? Doc.parened(fn) : fn; if (assoc != null) { var firstArg = visibleArgs.getFirst(); @@ -137,14 +137,14 @@ protected BasePrettier(@NotNull PrettierOptions options) { * @see #visitCalls(Assoc, Doc, Fmt, Outer, SeqView, boolean) */ private @NotNull Doc - prefix(@NotNull Doc fn, @NotNull Fmt fmt, Outer outer, SeqView> args) { + prefix(@NotNull Doc fn, @NotNull Fmt fmt, Outer outer, SeqView> args) { var call = Doc.sep(fn, Doc.sep(args.map(arg -> arg(fmt, arg, Outer.AppSpine)))); // If we're in a spine, add parentheses return checkParen(outer, call, Outer.AppSpine); } - public static Doc arg(@NotNull Fmt fmt, @NotNull BinOpParser.Elem arg, @NotNull Outer outer) { + public static Doc arg(@NotNull Fmt fmt, @NotNull BinOpElem arg, @NotNull Outer outer) { if (arg.explicit()) return fmt.apply(outer, arg.term()); return Doc.braced(fmt.apply(Outer.Free, arg.term())); } diff --git a/pretty/build.gradle.kts b/pretty/build.gradle.kts index 06e493b690..3f48022355 100644 --- a/pretty/build.gradle.kts +++ b/pretty/build.gradle.kts @@ -1,8 +1,8 @@ -// Copyright (c) 2020-2021 Yinsen (Tesla) Zhang. -// Use of this source code is governed by the MIT license that can be found in the LICENSE file. +// 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. dependencies { api(libs.annotations) - api(libs.kala.common) + api(libs.kala.collection) testImplementation(libs.junit.jupiter) testImplementation(libs.hamcrest) } diff --git a/tools-kala/src/main/java/module-info.java b/tools-kala/src/main/java/module-info.java index 18ef271d90..e9b248bde2 100644 --- a/tools-kala/src/main/java/module-info.java +++ b/tools-kala/src/main/java/module-info.java @@ -1,9 +1,11 @@ module aya.util.kala { + requires aya.pretty; requires transitive aya.util; requires static org.jetbrains.annotations; requires transitive kala.collection.primitive; + exports org.aya.util.binop; exports org.aya.util.more; exports org.aya.util.terck; exports org.aya.util.tyck.pat; diff --git a/tools/src/main/java/org/aya/util/binop/Assoc.java b/tools-kala/src/main/java/org/aya/util/binop/Assoc.java similarity index 94% rename from tools/src/main/java/org/aya/util/binop/Assoc.java rename to tools-kala/src/main/java/org/aya/util/binop/Assoc.java index a55c1290bc..8168b79d9f 100644 --- a/tools/src/main/java/org/aya/util/binop/Assoc.java +++ b/tools-kala/src/main/java/org/aya/util/binop/Assoc.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; diff --git a/tools/src/main/java/org/aya/util/binop/BinOpParser.java b/tools-kala/src/main/java/org/aya/util/binop/BinOpParser.java similarity index 98% rename from tools/src/main/java/org/aya/util/binop/BinOpParser.java rename to tools-kala/src/main/java/org/aya/util/binop/BinOpParser.java index 3e238cb48e..0ea58a6211 100644 --- a/tools/src/main/java/org/aya/util/binop/BinOpParser.java +++ b/tools-kala/src/main/java/org/aya/util/binop/BinOpParser.java @@ -8,6 +8,7 @@ import kala.collection.mutable.*; import kala.tuple.Tuple; import kala.tuple.Tuple2; +import org.aya.util.BinOpElem; import org.aya.util.error.SourceNode; import org.aya.util.error.SourcePos; import org.jetbrains.annotations.NotNull; @@ -18,7 +19,7 @@ public abstract class BinOpParser< OpSet extends BinOpSet, Expr extends SourceNode, - Elm extends BinOpParser.Elem> { + Elm extends BinOpElem> { protected final @NotNull OpSet opSet; private final @NotNull SeqView<@NotNull Elm> seq; @@ -214,8 +215,4 @@ enum AppliedSide { return a.term().sourcePos(); } - public interface Elem { - @NotNull Expr term(); - boolean explicit(); - } } diff --git a/tools/src/main/java/org/aya/util/binop/BinOpSet.java b/tools-kala/src/main/java/org/aya/util/binop/BinOpSet.java similarity index 98% rename from tools/src/main/java/org/aya/util/binop/BinOpSet.java rename to tools-kala/src/main/java/org/aya/util/binop/BinOpSet.java index 70adbc9bad..5711ef697d 100644 --- a/tools/src/main/java/org/aya/util/binop/BinOpSet.java +++ b/tools-kala/src/main/java/org/aya/util/binop/BinOpSet.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; diff --git a/tools/src/main/java/org/aya/util/binop/OpDecl.java b/tools-kala/src/main/java/org/aya/util/binop/OpDecl.java similarity index 91% rename from tools/src/main/java/org/aya/util/binop/OpDecl.java rename to tools-kala/src/main/java/org/aya/util/binop/OpDecl.java index 74bbed2c42..6d0bd91021 100644 --- a/tools/src/main/java/org/aya/util/binop/OpDecl.java +++ b/tools-kala/src/main/java/org/aya/util/binop/OpDecl.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; diff --git a/tools-md/build.gradle.kts b/tools-md/build.gradle.kts index 15fc7fda58..e15af34946 100644 --- a/tools-md/build.gradle.kts +++ b/tools-md/build.gradle.kts @@ -1,7 +1,7 @@ // 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. dependencies { - api(project(":tools")) + api(project(":tools-kala")) api(libs.annotations) implementation(libs.aya.commonmark) testImplementation(libs.junit.jupiter) diff --git a/tools-md/src/main/java/module-info.java b/tools-md/src/main/java/module-info.java index b625525d84..71adab181d 100644 --- a/tools-md/src/main/java/module-info.java +++ b/tools-md/src/main/java/module-info.java @@ -1,9 +1,11 @@ module aya.md { requires aya.util; + requires aya.util.kala; requires transitive aya.pretty; requires org.commonmark; requires static org.jetbrains.annotations; + requires kala.collection.primitive; exports org.aya.literate; exports org.aya.literate.parser; 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 10ed4a7d0e..40d4c40667 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 @@ -17,10 +17,10 @@ import org.aya.pretty.backend.md.MdStyle; import org.aya.pretty.doc.Doc; import org.aya.pretty.doc.Style; -import org.aya.util.StringUtil; import org.aya.util.error.InternalException; import org.aya.util.error.SourceFile; import org.aya.util.error.SourcePos; +import org.aya.util.more.StringUtil; import org.aya.util.reporter.Reporter; import org.commonmark.node.*; import org.commonmark.parser.IncludeSourceSpans; diff --git a/tools-repl/build.gradle.kts b/tools-repl/build.gradle.kts index 04b1a7a8a1..5542ccedd5 100644 --- a/tools-repl/build.gradle.kts +++ b/tools-repl/build.gradle.kts @@ -1,7 +1,7 @@ // 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. dependencies { - api(project(":tools-kala")) + api(project(":tools")) api(libs.jline.reader) api(libs.jline.terminal.api) } diff --git a/tools/src/main/java/module-info.java b/tools/src/main/java/module-info.java index a1f8861cd2..bbb3aa370c 100644 --- a/tools/src/main/java/module-info.java +++ b/tools/src/main/java/module-info.java @@ -3,9 +3,8 @@ requires aya.pretty; requires static org.jetbrains.annotations; - requires transitive kala.collection.primitive; + requires transitive kala.collection; - exports org.aya.util.binop; exports org.aya.util.error; exports org.aya.util.prettier; exports org.aya.util.reporter; diff --git a/tools/src/main/java/org/aya/util/Arg.java b/tools/src/main/java/org/aya/util/Arg.java index 6760ca6109..bb261de06e 100644 --- a/tools/src/main/java/org/aya/util/Arg.java +++ b/tools/src/main/java/org/aya/util/Arg.java @@ -4,7 +4,6 @@ import kala.collection.SeqView; import kala.collection.immutable.ImmutableSeq; -import org.aya.util.binop.BinOpParser; import org.jetbrains.annotations.NotNull; import java.util.function.Consumer; @@ -16,7 +15,7 @@ * In Aya, it is either core term, core pattern, concrete term, or concrete pattern. * @author ice1000 */ -public record Arg(@Override @NotNull T term, @Override boolean explicit) implements BinOpParser.Elem { +public record Arg(@Override @NotNull T term, @Override boolean explicit) implements BinOpElem { public static @NotNull Arg ofExplicitly(@NotNull T term) { return new Arg<>(term, true); } diff --git a/tools/src/main/java/org/aya/util/BinOpElem.java b/tools/src/main/java/org/aya/util/BinOpElem.java new file mode 100644 index 0000000000..c6ef2e3249 --- /dev/null +++ b/tools/src/main/java/org/aya/util/BinOpElem.java @@ -0,0 +1,10 @@ +// 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; + +import org.jetbrains.annotations.NotNull; + +public interface BinOpElem { + @NotNull Expr term(); + boolean explicit(); +} From 881a8f06fb72ef9a60c7b3949eb4ecebae91de37 Mon Sep 17 00:00:00 2001 From: ice1000 Date: Tue, 12 Dec 2023 23:08:24 -0500 Subject: [PATCH 06/10] proj: hope to fix logical error --- .github/README.md | 7 ++++--- base/src/main/java/module-info.java | 2 +- tools-kala/src/main/java/module-info.java | 2 +- tools-kala/src/main/java/org/aya/util/terck/Diagonal.java | 2 +- tools-md/src/main/java/module-info.java | 2 +- 5 files changed, 8 insertions(+), 7 deletions(-) diff --git a/.github/README.md b/.github/README.md index 36dddde5ab..f7dae83d1c 100644 --- a/.github/README.md +++ b/.github/README.md @@ -104,13 +104,14 @@ implementation group: 'org.aya-prover', name: '[project name]', version: '[lates ``` + `[project name]` specifies the subproject of Aya you want to use, - and the options are `pretty`, `base`, `cli-impl`, `cli-console`, `parser`, etc. + and the options are `pretty`, `base`, `cli-impl`, `parser`, etc. + The type checker lives in `base` and `parser`. + The generalized pretty printing framework is in `pretty`. + The library system, literate mode, single-file type checker, and basic REPL are in `cli-impl`. - + The generalized binary operator parser, generalized tree builder, - generalized mutable graph, generalized termination checker, + + The generalized tree builder, generalized termination checker, and a bunch of other utilities (files, etc.) are in `tools`. + + The generalized binary operator parser, generalized mutable graph are + in `tools-kala` because they depend on a larger subset of the kala library. + 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`. diff --git a/base/src/main/java/module-info.java b/base/src/main/java/module-info.java index 45d82812e4..f472005bef 100644 --- a/base/src/main/java/module-info.java +++ b/base/src/main/java/module-info.java @@ -2,7 +2,7 @@ requires transitive aya.md; requires transitive aya.pretty; requires transitive aya.util; - requires transitive aya.util.kala; + requires transitive aya.util.more; requires transitive aya.guest.cubical; requires transitive kala.base; requires transitive kala.collection; diff --git a/tools-kala/src/main/java/module-info.java b/tools-kala/src/main/java/module-info.java index e9b248bde2..f787616a44 100644 --- a/tools-kala/src/main/java/module-info.java +++ b/tools-kala/src/main/java/module-info.java @@ -1,4 +1,4 @@ -module aya.util.kala { +module aya.util.more { requires aya.pretty; requires transitive aya.util; diff --git a/tools-kala/src/main/java/org/aya/util/terck/Diagonal.java b/tools-kala/src/main/java/org/aya/util/terck/Diagonal.java index 1a9d2f1953..57c1b93e00 100644 --- a/tools-kala/src/main/java/org/aya/util/terck/Diagonal.java +++ b/tools-kala/src/main/java/org/aya/util/terck/Diagonal.java @@ -15,7 +15,7 @@ public record Diagonal( ) implements Docile { public static @NotNull Diagonal create(@NotNull CallMatrix matrix) { assert matrix.rows() == matrix.cols(); - var diag = IntRange.openClosed(0, matrix.rows()) + var diag = IntRange.closedOpen(0, matrix.rows()) .mapToObjTo(MutableList.create(), i -> matrix.matrix()[i][i]) .toImmutableSeq(); return new Diagonal<>(matrix, diag); diff --git a/tools-md/src/main/java/module-info.java b/tools-md/src/main/java/module-info.java index 71adab181d..28343be996 100644 --- a/tools-md/src/main/java/module-info.java +++ b/tools-md/src/main/java/module-info.java @@ -1,6 +1,6 @@ module aya.md { requires aya.util; - requires aya.util.kala; + requires aya.util.more; requires transitive aya.pretty; requires org.commonmark; From fd9533fa94066c33e566f5d46de59cd2de72798c Mon Sep 17 00:00:00 2001 From: ice1000 Date: Tue, 12 Dec 2023 23:24:38 -0500 Subject: [PATCH 07/10] java: use some Java 21 features --- .../org/aya/cli/library/LibraryCompiler.java | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/cli-impl/src/main/java/org/aya/cli/library/LibraryCompiler.java b/cli-impl/src/main/java/org/aya/cli/library/LibraryCompiler.java index 8deac0e91e..9044fa9c34 100644 --- a/cli-impl/src/main/java/org/aya/cli/library/LibraryCompiler.java +++ b/cli-impl/src/main/java/org/aya/cli/library/LibraryCompiler.java @@ -89,13 +89,13 @@ public static int compile( @NotNull Path libraryRoot ) throws IOException { if (!Files.exists(libraryRoot)) { - reporter.reportString("Specified library root does not exist: " + libraryRoot); + reporter.reportString(STR."Specified library root does not exist: \{libraryRoot}"); return 1; } try { return newCompiler(primFactory, reporter, flags, advisor, libraryRoot).start(); } catch (LibraryConfigData.BadConfig bad) { - reporter.reportString("Cannot load malformed library: " + bad.getMessage()); + reporter.reportString(STR."Cannot load malformed library: \{bad.getMessage()}"); return 1; } } @@ -141,8 +141,8 @@ private void resolveImportsIfNeeded(@NotNull LibrarySource source) throws IOExce known.noneMatch(k -> k.moduleName().equals(s.moduleName()))); known.appendAll(dedup); }); - reporter.reportNest("Done in " + StringUtil.timeToString( - System.currentTimeMillis() - startTime), LibraryOwner.DEFAULT_INDENT + 2); + reporter.reportNest(STR."Done in \{StringUtil.timeToString( + System.currentTimeMillis() - startTime)}", LibraryOwner.DEFAULT_INDENT + 2); return depGraph; } @@ -188,7 +188,7 @@ private void pretty(ImmutableSeq modified) throws IOException { }); // THE BIG GAME modified.forEachChecked(src -> { - // reportNest("[Pretty] " + QualifiedID.join(src.moduleName())); + // reportNest(STR."[Pretty] \{QualifiedID.join(src.moduleName())}"); var doc = src.pretty(ImmutableSeq.empty(), prettierOptions); var text = renderOptions.render(outputTarget, doc, setup); var outputFileName = AyaFiles.stripAyaSourcePostfix(src.displayPath().toString()) + outputTarget.fileExt; @@ -214,7 +214,7 @@ private boolean make() throws IOException { owner.addModulePath(dep.outDir()); } - reporter.reportString("Compiling " + library.name()); + reporter.reportString(STR."Compiling \{library.name()}"); var startTime = System.currentTimeMillis(); if (anyDepChanged || flags.remake()) { owner.librarySources().forEach(this::clearModified); @@ -231,8 +231,8 @@ private boolean make() throws IOException { } var make = make(modified); - reporter.reportNest("Library loaded in " + StringUtil.timeToString( - System.currentTimeMillis() - startTime), LibraryOwner.DEFAULT_INDENT + 2); + reporter.reportNest(STR."Library loaded in \{StringUtil.timeToString( + System.currentTimeMillis() - startTime)}", LibraryOwner.DEFAULT_INDENT + 2); pretty(modified); return make; } @@ -376,7 +376,7 @@ private void tyckOne(@NotNull LibrarySource file) { QualifiedID.join(moduleName), file.displayPath()), LibraryOwner.DEFAULT_INDENT); var mod = moduleLoader.load(moduleName); if (mod == null || file.resolveInfo().get() == null) - throw new InternalException("Unable to load module: " + moduleName); + throw new InternalException(STR."Unable to load module: \{moduleName}"); } } From ee300d7f2f905873daa1caecee391c62e2e9ee9e Mon Sep 17 00:00:00 2001 From: ice1000 Date: Tue, 12 Dec 2023 23:47:59 -0500 Subject: [PATCH 08/10] java: an attempt to fix a JDK 21 caused bug --- .../org/aya/cli/literate/SyntaxHighlight.java | 32 +++++++++---------- 1 file changed, 16 insertions(+), 16 deletions(-) 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 4dffda9367..0f59d39097 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 @@ -18,7 +18,6 @@ import org.aya.concrete.stmt.GeneralizedVar; import org.aya.concrete.stmt.Stmt; import org.aya.concrete.stmt.decl.ClassDecl; -import org.aya.concrete.stmt.decl.Decl; import org.aya.concrete.stmt.decl.TeleDecl; import org.aya.concrete.visitor.StmtFolder; import org.aya.core.def.*; @@ -33,6 +32,7 @@ import org.aya.ref.GenerateKind; import org.aya.ref.LocalVar; import org.aya.resolve.context.ModuleName; +import org.aya.util.error.InternalException; import org.aya.util.error.SourceFile; import org.aya.util.error.SourcePos; import org.jetbrains.annotations.NotNull; @@ -154,23 +154,23 @@ else if (SPECIAL_SYMBOL.contains(tokenType)) @SuppressWarnings("unused") public static @NotNull DefKind kindOf(@NotNull AnyVar var) { - record P(Decl decl, GenericDef def) {} return switch (var) { case GeneralizedVar ignored -> DefKind.Generalized; - case DefVar defVar -> switch (new P(defVar.concrete, defVar.core)) { - case P(TeleDecl.FnDecl $, var $$) -> DefKind.Fn; - case P(ClassDecl $, var $$) -> DefKind.Clazz; - case P(TeleDecl.ClassMember $, var $$) -> DefKind.Member; - case P(TeleDecl.DataDecl $, var $$) -> DefKind.Data; - case P(TeleDecl.DataCtor $, var $$) -> DefKind.Con; - case P(TeleDecl.PrimDecl $, var $$) -> DefKind.Prim; - case P(var $, FnDef $$) -> DefKind.Fn; - case P(var $, ClassDef $$) -> DefKind.Clazz; - case P(var $, MemberDef $$) -> DefKind.Member; - case P(var $, DataDef $$) -> DefKind.Data; - case P(var $, CtorDef $$) -> DefKind.Con; - case P(var $, PrimDef $$) -> DefKind.Prim; - }; + case DefVar defVar -> { + if (defVar.concrete instanceof TeleDecl.FnDecl || defVar.core instanceof FnDef) + yield DefKind.Fn; + else if (defVar.concrete instanceof TeleDecl.ClassMember || defVar.core instanceof MemberDef) + yield DefKind.Member; + else if (defVar.concrete instanceof TeleDecl.DataDecl || defVar.core instanceof DataDef) + yield DefKind.Data; + else if (defVar.concrete instanceof TeleDecl.DataCtor || defVar.core instanceof CtorDef) + yield DefKind.Con; + else if (defVar.concrete instanceof TeleDecl.PrimDecl || defVar.core instanceof PrimDef) + yield DefKind.Prim; + 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; default -> DefKind.Unknown; From 451a843ed60de0da08ca4f0b6151600c58258adf Mon Sep 17 00:00:00 2001 From: ice1000 Date: Tue, 12 Dec 2023 23:54:30 -0500 Subject: [PATCH 09/10] 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)); From 1e74abbbcd3b34d48d7c35d10d65505db705c35b Mon Sep 17 00:00:00 2001 From: ice1000 Date: Wed, 13 Dec 2023 01:20:44 -0500 Subject: [PATCH 10/10] ci: update upstream --- gradle/libs.versions.toml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/gradle/libs.versions.toml b/gradle/libs.versions.toml index 17a7e1d231..e374082a1d 100644 --- a/gradle/libs.versions.toml +++ b/gradle/libs.versions.toml @@ -2,7 +2,7 @@ # The Version of this project, aka, The Aya Theorem Prover. # Remove "-SNAPSHOT" suffix and run gradle publish to release a new version. # After that, increase the version number and add "-SNAPSHOT" suffix back for next cycle. -project = "0.30-SNAPSHOT" +project = "0.30" # https://openjdk.org/ java = "21" @@ -11,7 +11,7 @@ java = "21" annotations = "24.0.1" kala = "0.69.0" picocli = "4.7.5" -build-util = "0.0.20" +build-util = "0.0.21" # https://github.com/graalvm/native-build-tools graal-tools = "0.9.28" # https://github.com/jline/jline3