merge: Use onEach and refactor some stream to view (#1315)

Kala 0.81

base/src/main/java/org/aya/resolve/context/Candidate.java

@@ -87,24 +87,13 @@ record Imported<T>(@NotNull ImmutableMap<ModuleName.Qualified, T> symbols) imple
     @Override public T get() {
       var view = symbols.valuesView().distinct();
       if (view.sizeGreaterThan(1)) Panic.unreachable();
-      //noinspection OptionalGetWithoutIsPresent
-      return symbols.valuesView().stream().findFirst().get();
+      return symbols.valuesView().getAny();
     }
-
-    @Override
-    public CollectionView<T> getAll() {
-      return symbols.valuesView();
-    }
-
-    @Override
-    public @NotNull ImmutableSeq<ModuleName> from() {
-      return ImmutableSeq.from(symbols.keysView());
-    }
-
+    @Override public CollectionView<T> getAll() { return symbols.valuesView(); }
+    @Override public @NotNull ImmutableSeq<ModuleName> from() { return ImmutableSeq.from(symbols.keysView()); }
     @Override public boolean contains(@NotNull ModuleName modName) {
       return modName instanceof ModuleName.Qualified qmod && symbols.containsKey(qmod);
     }
-
     @Override public @NotNull Candidate<T> merge(@NotNull Candidate<T> candy) {
       return switch (candy) {
         case Candidate.Defined<T> v -> v;

base/src/main/java/org/aya/tyck/error/ClausesProblem.java

@@ -20,6 +20,8 @@
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
+import java.util.Objects;
+
 public sealed interface ClausesProblem extends Problem {
   @Override default @NotNull Severity level() { return Severity.ERROR; }
 
@@ -116,7 +118,8 @@ record UnsureCase(
     }
   }
 
-  record Domination(int dom, int sub, @Override @NotNull SourcePos sourcePos) implements ClausesProblem {
+  record Domination(int dom, int sub, @Override @NotNull SourcePos sourcePos)
+    implements ClausesProblem, Comparable<Domination> {
     @Override public @NotNull Doc describe(@NotNull PrettierOptions options) {
       var subOrdinal = Doc.ordinal(sub);
       return Doc.sep(
@@ -128,6 +131,15 @@ record Domination(int dom, int sub, @Override @NotNull SourcePos sourcePos) impl
     }
 
     @Override public @NotNull Severity level() { return Severity.WARN; }
+    @Override public int compareTo(@NotNull ClausesProblem.Domination o) {
+      var domCmp = Integer.compare(dom, o.dom);
+      return domCmp != 0 ? domCmp : Integer.compare(sub, o.sub);
+    }
+    @Override public boolean equals(Object o) {
+      if (!(o instanceof Domination that)) return false;
+      return dom == that.dom && sub == that.sub;
+    }
+    @Override public int hashCode() { return Objects.hash(dom, sub); }
   }
 
   record FMDomination(int sub, @Override @NotNull SourcePos sourcePos) implements ClausesProblem {

base/src/main/java/org/aya/tyck/pat/YouTrack.java

@@ -4,9 +4,9 @@
 
 import kala.collection.Seq;
 import kala.collection.immutable.ImmutableSeq;
-import kala.collection.mutable.MutableLinkedSet;
 import kala.collection.mutable.MutableList;
 import kala.collection.mutable.MutableSet;
+import kala.collection.mutable.MutableTreeSet;
 import org.aya.syntax.core.def.FnClauseBody;
 import org.aya.syntax.core.term.FreeTerm;
 import org.aya.syntax.core.term.Param;
@@ -66,7 +66,7 @@ private void domination(
   }
 
   public void check(@NotNull FnClauseBody body, @NotNull Term type) {
-    var doms = MutableLinkedSet.<ClausesProblem.Domination>create();
+    var doms = MutableTreeSet.<ClausesProblem.Domination>create();
     body.classes.forEach(results -> {
       var contents = results.cls().mapToObj(i -> new Info(i, body.clauses.get(i)));
       for (int i = 1, size = contents.size(); i < size; i++) {

cli-impl/src/main/java/org/aya/cli/interactive/ReplContext.java

@@ -6,10 +6,10 @@
 import kala.collection.SeqView;
 import kala.collection.immutable.ImmutableMap;
 import kala.collection.immutable.ImmutableSeq;
-import kala.collection.mutable.MutableLinkedSet;
 import kala.collection.mutable.MutableList;
 import kala.collection.mutable.MutableMap;
 import kala.collection.mutable.MutableSet;
+import kala.collection.mutable.MutableTreeSet;
 import kala.tuple.Tuple2;
 import org.aya.resolve.context.Context;
 import org.aya.resolve.context.ModuleExport;
@@ -137,7 +137,7 @@ public record ModuleTrie(@NotNull ImmutableMap<String, ModuleTrie> children, boo
     var node = resolve(prefix);
     if (node == null) return ImmutableSeq.empty();
 
-    var hint = MutableLinkedSet.<String>create();
+    var hint = MutableTreeSet.<String>create();
 
     hint.addAll(node.children().keysView());
     if (node.inhabited) {

cli-impl/src/main/java/org/aya/cli/render/vscode/ColorTheme.java

@@ -2,6 +2,10 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.cli.render.vscode;
 
+import java.nio.file.Files;
+import java.nio.file.Path;
+import java.nio.file.Paths;
+
 import com.google.gson.GsonBuilder;
 import com.google.gson.JsonParseException;
 import com.google.gson.Strictness;
@@ -21,10 +25,6 @@
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
-import java.nio.file.Files;
-import java.nio.file.Path;
-import java.nio.file.Paths;
-
 public class ColorTheme {
   public static Try<ColorTheme> loadFrom(@NotNull Path path) throws JsonParseException {
     return Try.of(() -> {
@@ -103,10 +103,10 @@ public Option<VscColorTheme.TokenColor.Settings> find(@NotNull String scope) {
   }
 
   public void findAndPut(@NotNull MutableMap<String, Integer> putTo, @NotNull String key, @NotNull Seq<String> scope, @NotNull Map<String, Integer> fallback) {
-    var result = scope.view().map(this::find).findFirst(Option::isDefined);
+    var result = scope.view().flatMap(this::find).getFirstOption();
 
     if (result.isDefined()) {
-      var settings = result.get().get();
+      var settings = result.get();
       var foreground = settings.foreground;
 
       if (foreground != null) {

cli-impl/src/test/resources/negative/PatCohError.txt

@@ -174,6 +174,16 @@ In file $FILE:5:2 ->
 Warning: The 2nd clause dominates the 3rd clause. The 3rd clause will be 
          unreachable
 
+In file $FILE:8:2 ->
+
+  6 │   | suc (suc a) => a
+  7 │   | 2147483647 => 3
+  8 │   | 2147483647 => 4
+    │     ╰─────────────╯
+
+Warning: The 2nd clause dominates the 6th clause. The 6th clause will be 
+         unreachable
+
 In file $FILE:9:2 ->
 
   7 │   | 2147483647 => 3
@@ -214,16 +224,6 @@ In file $FILE:7:2 ->
 Warning: The 6th clause dominates the 5th clause. The 5th clause will be 
          unreachable
 
-In file $FILE:8:2 ->
-
-  6 │   | suc (suc a) => a
-  7 │   | 2147483647 => 3
-  8 │   | 2147483647 => 4
-    │     ╰─────────────╯
-
-Warning: The 2nd clause dominates the 6th clause. The 6th clause will be 
-         unreachable
-
 6 error(s), 7 warning(s).
 Let's learn from that.
 
@@ -329,24 +329,24 @@ Error: The 2nd and the 1st clauses are not confluent because we failed to unify
        and
          suc b
 
-In file $FILE:13:2 ->
+In file $FILE:12:2 ->
 
+  10 │   overlap def largeInt3 Nat Nat : Nat
   11 │   | a, b => b
   12 │   | a, suc b => b
-  13 │   | a, 1919810 => 1
-     │     ╰─────────────╯
+     │     ╰───────────╯
 
-Warning: The 1st clause dominates the 3rd clause. The 3rd clause will be 
+Warning: The 1st clause dominates the 2nd clause. The 2nd clause will be 
          unreachable
 
-In file $FILE:12:2 ->
+In file $FILE:13:2 ->
 
-  10 │   overlap def largeInt3 Nat Nat : Nat
   11 │   | a, b => b
   12 │   | a, suc b => b
-     │     ╰───────────╯
+  13 │   | a, 1919810 => 1
+     │     ╰─────────────╯
 
-Warning: The 1st clause dominates the 2nd clause. The 2nd clause will be 
+Warning: The 1st clause dominates the 3rd clause. The 3rd clause will be 
          unreachable
 
 In file $FILE:15:12 ->
@@ -450,24 +450,24 @@ Error: The 2nd and the 1st clauses are not confluent because we failed to unify
        and
          suc b
 
-In file $FILE:26:2 ->
+In file $FILE:25:2 ->
 
+  23 │   overlap def largeInt3-inv Nat Nat : Nat
   24 │   | b, a => b
   25 │   | suc b, a => b
-  26 │   | 1919810, a => 1
-     │     ╰─────────────╯
+     │     ╰───────────╯
 
-Warning: The 1st clause dominates the 3rd clause. The 3rd clause will be 
+Warning: The 1st clause dominates the 2nd clause. The 2nd clause will be 
          unreachable
 
-In file $FILE:25:2 ->
+In file $FILE:26:2 ->
 
-  23 │   overlap def largeInt3-inv Nat Nat : Nat
   24 │   | b, a => b
   25 │   | suc b, a => b
-     │     ╰───────────╯
+  26 │   | 1919810, a => 1
+     │     ╰─────────────╯
 
-Warning: The 1st clause dominates the 2nd clause. The 2nd clause will be 
+Warning: The 1st clause dominates the 3rd clause. The 3rd clause will be 
          unreachable
 
 In file $FILE:28:12 ->
@@ -488,16 +488,6 @@ Error: The 2nd and the 3rd clauses are not confluent because we failed to unify
        and
          515
 
-In file $FILE:29:2 ->
-
-  27 │   
-  28 │   overlap def multi-nodes Nat Nat : Nat
-  29 │   | 114, 0 => 0
-     │     ╰─────────╯
-
-Warning: The 5th clause dominates the 1st clause. The 1st clause will be 
-         unreachable
-
 In file $FILE:31:2 ->
 
   29 │   | 114, 0 => 0
@@ -508,6 +498,16 @@ In file $FILE:31:2 ->
 Warning: The 2nd clause dominates the 3rd clause. The 3rd clause will be 
          unreachable
 
+In file $FILE:29:2 ->
+
+  27 │   
+  28 │   overlap def multi-nodes Nat Nat : Nat
+  29 │   | 114, 0 => 0
+     │     ╰─────────╯
+
+Warning: The 5th clause dominates the 1st clause. The 1st clause will be 
+         unreachable
+
 In file $FILE:30:2 ->
 
   28 │   overlap def multi-nodes Nat Nat : Nat

gradle/libs.versions.toml

@@ -9,13 +9,13 @@ java = "22"
 # https://github.com/JetBrains/java-annotations
 annotations = "26.0.1"
 # https://github.com/Glavo/kala-common
-kala = "0.78.0"
+kala = "0.81.0"
 # https://picocli.info
 picocli = "4.7.6"
 # https://repo1.maven.org/maven2/org/aya-prover/upstream/build-util
-aya-upstream = "0.0.33"
+aya-upstream = "0.0.34"
 # https://github.com/jline/jline3
-jline = "3.28.0"
+jline = "3.29.0"
 # https://junit.org/junit5
 junit = "5.11.3"
 hamcrest = "2.2"

ide-lsp/src/main/java/org/aya/lsp/server/AyaLanguageServer.java

@@ -2,6 +2,15 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.lsp.server;
 
+import java.io.IOException;
+import java.net.URI;
+import java.nio.file.Files;
+import java.nio.file.Path;
+import java.util.Collections;
+import java.util.List;
+import java.util.Optional;
+import java.util.stream.Collectors;
+
 import com.google.gson.Gson;
 import kala.collection.CollectionView;
 import kala.collection.SeqView;
@@ -45,16 +54,6 @@
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
-import java.io.IOException;
-import java.net.URI;
-import java.nio.file.Files;
-import java.nio.file.Path;
-import java.util.Collections;
-import java.util.List;
-import java.util.Optional;
-import java.util.stream.Collectors;
-import java.util.stream.Stream;
-
 public class AyaLanguageServer implements LanguageServer {
   private static final @NotNull CompilerFlags FLAGS = new CompilerFlags(CompilerFlags.Message.EMOJI, false, false, null, SeqView.empty(), null);
 
@@ -83,9 +82,7 @@ public AyaLanguageServer(@NotNull CompilerAdvisor advisor, @NotNull AyaLanguageC
     Log.init(this.client);
   }
 
-  public @NotNull CollectionView<LibraryOwner> libraries() {
-    return libraries.valuesView();
-  }
+  public @NotNull CollectionView<LibraryOwner> libraries() { return libraries.valuesView(); }
 
   /// @return the libraries that are actually loaded
   public @NotNull SeqView<LibraryOwner> registerLibrary(@NotNull Path path) {
@@ -143,6 +140,7 @@ private SeqView<WsLibrary> mockLibraries(@NotNull Path path) {
     var mocked = AyaFiles.collectAyaSourceFiles(path, 1)
       .map(f -> Tuple.of(f, WsLibrary.mock(f)));
 
+    // Cannot replace with `onEach` due to the laziness of `onEach`
     mocked.forEach(libraries::put);
     return mocked.view().map(Tuple2::component2);
   }
@@ -261,11 +259,11 @@ private void initializeOptions(@Nullable ServerOptions options) {
   }
 
   public void publishProblems(@NotNull BufferReporter reporter, @NotNull PrettierOptions options) {
-    var diags = reporter.problems().stream()
+    var diags = reporter.problems().view()
       .filter(p -> p.sourcePos().belongsToSomeFile())
-      .peek(p -> Log.d("%s", p.describe(options).debugRender()))
-      .flatMap(p -> Stream.concat(Stream.of(p), p.inlineHints(options).stream().map(t -> new InlineHintProblem(p, t))))
-      .flatMap(p -> p.sourcePos().file().underlying().stream().map(uri -> Tuple.of(uri, p)))
+      .onEach(p -> Log.d("%s", p.describe(options).debugRender()))
+      .flatMap(p -> SeqView.of(p).appendedAll(p.inlineHints(options).map(t -> new InlineHintProblem(p, t))))
+      .flatMap(p -> p.sourcePos().file().underlying().map(uri -> Tuple.of(uri, p)))
       .collect(Collectors.groupingBy(
         Tuple2::component1,
         Collectors.mapping(Tuple2::component2, ImmutableSeq.factory())
@@ -347,8 +345,7 @@ private void clearProblems(@NotNull ImmutableSeq<ImmutableSeq<LibrarySource>> af
     return Optional.of(new Hover(List.of(marked)));
   }
 
-  @Override
-  public Optional<SignatureHelp> signatureHelp(TextDocumentPositionParams params) {
+  @Override public Optional<SignatureHelp> signatureHelp(TextDocumentPositionParams params) {
     throw new UnsupportedOperationException();
   }
 
@@ -396,7 +393,7 @@ public Optional<SignatureHelp> signatureHelp(TextDocumentPositionParams params)
       // only highlight references in the current file
       .filter(pos -> pos.file().underlying().equals(currentFile))
       .map(pos -> new DocumentHighlight(LspRange.toRange(pos), DocumentHighlightKind.Read))
-      .stream().toList();
+      .toSeq().asJava();
   }
 
   @Override public List<CodeLens> codeLens(CodeLensParams params) {

ide-lsp/src/test/java/org/aya/lsp/tester/LspTestClient.java

@@ -2,6 +2,7 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.lsp.tester;
 
+import kala.collection.Seq;
 import kala.collection.SeqView;
 import kala.collection.immutable.ImmutableSeq;
 import kala.tuple.Unit;
@@ -73,11 +74,9 @@ private void executeOne(@NotNull TestCommand cmd) {
 
   @Override
   public void publishDiagnostics(@NotNull PublishDiagnosticsParams diagnostics) {
-    var errors = diagnostics.diagnostics.stream()
-      .filter(d -> d.severity == DiagnosticSeverity.Error)
-      .collect(ImmutableSeq.factory());
+    var errors = Seq.wrapJava(diagnostics.diagnostics)
+      .filter(d -> d.severity == DiagnosticSeverity.Error);
     Assertions.assertTrue(errors.isEmpty(),
-      "Unexpected compiler errors: " +
-        errors.joinToString("\n", d -> d.message));
+      errors.joinToString("\n", "Unexpected compiler errors: ", "", d -> d.message));
   }
 }