proof-search: use records

aya-prover · Jan 28, 2025 · a3229cb · a3229cb
1 parent 5e60953
commit a3229cb
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 8 deletions.
diff --git a/src/main/java/org/aya/intellij/actions/search/ProofSearch.java b/src/main/java/org/aya/intellij/actions/search/ProofSearch.java
@@ -57,8 +57,8 @@ record Arg(@NotNull ProofShape shape, boolean explicit) {}
       ps -> {
         var scope = FindSymbolParameters.searchScopeFor(project, everywhere);
         return SearchEverywhere.searchGenericDecl(project, scope)
-          .filter(t -> matches(ps, t.component1()))
-          .map(t -> new Proof.Yes(t.component1(), t.component2()));
+          .filter(t -> matches(ps, t.defVar()))
+          .map(t -> new Proof.Yes(t.defVar(), t.decl()));
       }
     );
   }

diff --git a/src/main/java/org/aya/intellij/actions/search/SearchEverywhere.java b/src/main/java/org/aya/intellij/actions/search/SearchEverywhere.java
@@ -57,14 +57,19 @@ public interface SearchEverywhere extends ChooseByNameContributorEx2 {
       .map(tup -> Tuple.of(tup.component1(), tup.component2())));
   }
 
-  static @NotNull SeqView<Tuple2<DefVar<?, ?>, AyaPsiGenericDecl>> searchGenericDecl(@NotNull Project project, @NotNull GlobalSearchScope searchScope) {
+  record SearchItem(
+    DefVar<?, ?> defVar,
+    AyaPsiGenericDecl decl
+  ) {}
+
+  static @NotNull SeqView<SearchItem> searchGenericDecl(@NotNull Project project, @NotNull GlobalSearchScope searchScope) {
     return search(project, searchScope).flatMap(tup -> tup.component2().mapNotNull(defVar -> {
       var psi = JB.elementAt(tup.component1(), defVar.concrete.sourcePos(), AyaPsiGenericDecl.class);
-      return psi == null ? null : Tuple.of(defVar, psi);
+      return psi == null ? null : new SearchItem(defVar, psi);
     }));
   }
 
-  private static @NotNull SeqView<Tuple2<DefVar<?, ?>, AyaPsiGenericDecl>> searchGenericDecl(@NotNull FindSymbolParameters parameters) {
+  private static @NotNull SeqView<SearchItem> searchGenericDecl(@NotNull FindSymbolParameters parameters) {
     return searchGenericDecl(parameters.getProject(), parameters.getSearchScope());
   }
 
@@ -73,7 +78,7 @@ class Symbol implements SearchEverywhere {
       @NotNull Processor<? super String> processor,
       @NotNull FindSymbolParameters parameters
     ) {
-      searchGenericDecl(parameters).forEach(psi -> processor.process(psi.component2().nameOrEmpty()));
+      searchGenericDecl(parameters).forEach(psi -> processor.process(psi.decl.nameOrEmpty()));
     }
 
     @Override public void processElementsWithName(
@@ -82,8 +87,8 @@ class Symbol implements SearchEverywhere {
       @NotNull FindSymbolParameters parameters
     ) {
       searchGenericDecl(parameters)
-        .filter(psi -> psi.component1().name().equals(name))
-        .map(t -> new AyaNavItem(t.component2(), true))
+        .filter(psi -> psi.defVar.name().equals(name))
+        .map(t -> new AyaNavItem(t.decl, true))
         .forEach(processor::process);
     }
   }