From 46c35f65eccca03313f91e1fe072ad4b2ef50486 Mon Sep 17 00:00:00 2001
From: imkiva <imkiva@islovely.icu>
Date: Fri, 10 Jun 2022 15:58:15 +0800
Subject: [PATCH 01/16] LSP: slightly improve code

Signed-off-by: imkiva <imkiva@islovely.icu>
---
 .../org/aya/lsp/actions/SyntaxHighlight.java  | 24 ++++++++++++++++++-
 .../java/org/aya/lsp/server/AyaService.java   | 21 ++++------------
 2 files changed, 27 insertions(+), 18 deletions(-)

diff --git a/lsp/src/main/java/org/aya/lsp/actions/SyntaxHighlight.java b/lsp/src/main/java/org/aya/lsp/actions/SyntaxHighlight.java
index 631d69041c..fe9ef9b9c5 100644
--- a/lsp/src/main/java/org/aya/lsp/actions/SyntaxHighlight.java
+++ b/lsp/src/main/java/org/aya/lsp/actions/SyntaxHighlight.java
@@ -4,6 +4,8 @@
 
 import kala.collection.mutable.MutableList;
 import kala.control.Option;
+import org.aya.cli.library.source.LibraryOwner;
+import org.aya.cli.library.source.LibrarySource;
 import org.aya.concrete.Expr;
 import org.aya.concrete.Pattern;
 import org.aya.concrete.stmt.*;
@@ -17,8 +19,28 @@
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
+import java.util.List;
+
 public final class SyntaxHighlight implements StmtOps<@NotNull MutableList<HighlightResult.Symbol>> {
-  public static final SyntaxHighlight INSTANCE = new SyntaxHighlight();
+  public static @NotNull List<HighlightResult> invoke(@NotNull LibraryOwner owner) {
+    var symbols = MutableList.<HighlightResult>create();
+    highlight(owner, symbols);
+    return symbols.asJava();
+  }
+
+  private static void highlight(@NotNull LibraryOwner owner, @NotNull MutableList<HighlightResult> result) {
+    owner.librarySources().forEach(src -> result.append(highlightOne(src)));
+    for (var dep : owner.libraryDeps()) highlight(dep, result);
+  }
+
+  private static @NotNull HighlightResult highlightOne(@NotNull LibrarySource source) {
+    var symbols = MutableList.<HighlightResult.Symbol>create();
+    var program = source.program().value;
+    if (program != null) program.forEach(d -> SyntaxHighlight.INSTANCE.visit(d, symbols));
+    return new HighlightResult(source.file().toUri().toString(), symbols.view().filter(t -> t.range() != LspRange.NONE));
+  }
+
+  private static final SyntaxHighlight INSTANCE = new SyntaxHighlight();
 
   private @NotNull Range rangeOf(@NotNull Signatured signatured) {
     return LspRange.toRange(signatured.sourcePos());
diff --git a/lsp/src/main/java/org/aya/lsp/server/AyaService.java b/lsp/src/main/java/org/aya/lsp/server/AyaService.java
index 8957cef759..514602c280 100644
--- a/lsp/src/main/java/org/aya/lsp/server/AyaService.java
+++ b/lsp/src/main/java/org/aya/lsp/server/AyaService.java
@@ -151,22 +151,7 @@ private void mockLibraries(@NotNull Path path) {
       sharedPrimFactory.clear();
     }
     reportErrors(reporter, DistillerOptions.pretty());
-    // build highlight
-    var symbols = MutableList.<HighlightResult>create();
-    highlight(owner, symbols);
-    return symbols.asJava();
-  }
-
-  private void highlight(@NotNull LibraryOwner owner, @NotNull MutableList<HighlightResult> result) {
-    owner.librarySources().forEach(src -> result.append(highlightOne(src)));
-    for (var dep : owner.libraryDeps()) highlight(dep, result);
-  }
-
-  private @NotNull HighlightResult highlightOne(@NotNull LibrarySource source) {
-    var symbols = MutableList.<HighlightResult.Symbol>create();
-    var program = source.program().value;
-    if (program != null) program.forEach(d -> SyntaxHighlight.INSTANCE.visit(d, symbols));
-    return new HighlightResult(source.file().toUri().toString(), symbols.view().filter(t -> t.range() != LspRange.NONE));
+    return SyntaxHighlight.invoke(owner);
   }
 
   public void reportErrors(@NotNull BufferReporter reporter, @NotNull DistillerOptions options) {
@@ -323,8 +308,10 @@ public CompletableFuture<List<? extends DocumentHighlight>> documentHighlight(Do
     return CompletableFuture.supplyAsync(() -> {
       var source = find(params.getTextDocument().getUri());
       if (source == null) return Collections.emptyList();
+      var currentFile = Option.of(source.file());
       return FindReferences.findOccurrences(source, params.getPosition(), SeqView.of(source.owner()))
-        .filter(pos -> pos.file().underlying().equals(Option.of(source.file())))
+        // 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();
     });

From ac761ed2b1e612d4b51bfeb03835fc621ab5fde4 Mon Sep 17 00:00:00 2001
From: imkiva <imkiva@islovely.icu>
Date: Fri, 10 Jun 2022 16:16:12 +0800
Subject: [PATCH 02/16] FIX: `ReferringResolver` should call super for patterns

Signed-off-by: imkiva <imkiva@islovely.icu>
---
 lsp/src/main/java/org/aya/lsp/utils/Resolver.java | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lsp/src/main/java/org/aya/lsp/utils/Resolver.java b/lsp/src/main/java/org/aya/lsp/utils/Resolver.java
index bc4822bdcd..46cf63a126 100644
--- a/lsp/src/main/java/org/aya/lsp/utils/Resolver.java
+++ b/lsp/src/main/java/org/aya/lsp/utils/Resolver.java
@@ -132,7 +132,7 @@ public void visitAll(ImmutableSeq<Stmt> program, P xy) {
         case Pattern.Bind bind -> check(param, bind.bind(), bind.sourcePos());
         default -> {}
       }
-      return pattern;
+      return StmtOps.super.visitPattern(pattern, param);
     }
   }
 

From ebb7fc5a5c3e41fb8ea6eedbabf3a1c3dba0a1a1 Mon Sep 17 00:00:00 2001
From: imkiva <imkiva@islovely.icu>
Date: Fri, 10 Jun 2022 16:17:16 +0800
Subject: [PATCH 03/16] LSP: show usage count in CodeLens

---
 .../org/aya/lsp/actions/FindReferences.java   |  9 ++++-
 .../java/org/aya/lsp/actions/LensMaker.java   | 37 +++++++++++++++++++
 .../org/aya/lsp/actions/SyntaxHighlight.java  |  7 +---
 .../org/aya/lsp/server/AyaLanguageClient.java |  3 +-
 .../java/org/aya/lsp/server/AyaServer.java    | 13 ++++---
 .../java/org/aya/lsp/server/AyaService.java   | 14 +++++++
 .../main/java/org/aya/lsp/utils/LspRange.java |  7 +++-
 7 files changed, 76 insertions(+), 14 deletions(-)
 create mode 100644 lsp/src/main/java/org/aya/lsp/actions/LensMaker.java

diff --git a/lsp/src/main/java/org/aya/lsp/actions/FindReferences.java b/lsp/src/main/java/org/aya/lsp/actions/FindReferences.java
index 4551802221..13e4dd3904 100644
--- a/lsp/src/main/java/org/aya/lsp/actions/FindReferences.java
+++ b/lsp/src/main/java/org/aya/lsp/actions/FindReferences.java
@@ -34,8 +34,15 @@ public interface FindReferences {
     @NotNull SeqView<LibraryOwner> libraries
   ) {
     var vars = Resolver.resolveVar(source, position);
+    return findRefs(vars.map(WithPos::data), libraries);
+  }
+
+  static @NotNull SeqView<SourcePos> findRefs(
+    @NotNull SeqView<Var> vars,
+    @NotNull SeqView<LibraryOwner> libraries
+  ) {
     var resolver = new Resolver.UsageResolver();
-    vars.forEach(var -> libraries.forEach(lib -> resolve(resolver, lib, var.data())));
+    vars.forEach(def -> libraries.forEach(lib -> resolve(resolver, lib, def)));
     return resolver.refs.view();
   }
 
diff --git a/lsp/src/main/java/org/aya/lsp/actions/LensMaker.java b/lsp/src/main/java/org/aya/lsp/actions/LensMaker.java
new file mode 100644
index 0000000000..71213ec9a2
--- /dev/null
+++ b/lsp/src/main/java/org/aya/lsp/actions/LensMaker.java
@@ -0,0 +1,37 @@
+// Copyright (c) 2020-2022 Yinsen (Tesla) Zhang.
+// Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
+package org.aya.lsp.actions;
+
+import kala.collection.SeqView;
+import kala.collection.mutable.MutableList;
+import org.aya.cli.library.source.LibraryOwner;
+import org.aya.cli.library.source.LibrarySource;
+import org.aya.concrete.stmt.Decl;
+import org.aya.concrete.visitor.StmtOps;
+import org.aya.lsp.utils.LspRange;
+import org.eclipse.lsp4j.CodeLens;
+import org.eclipse.lsp4j.Command;
+import org.jetbrains.annotations.NotNull;
+
+import java.util.List;
+
+public record LensMaker(@NotNull SeqView<LibraryOwner> libraries) implements StmtOps<@NotNull MutableList<CodeLens>> {
+  public static @NotNull List<CodeLens> invoke(@NotNull LibrarySource source, @NotNull SeqView<LibraryOwner> libraries) {
+    var lens = MutableList.<CodeLens>create();
+    var maker = new LensMaker(libraries);
+    var program = source.program().value;
+    if (program != null) program.forEach(decl -> maker.visit(decl, lens));
+    return lens.asJava();
+  }
+
+  @Override
+  public void visitDecl(@NotNull Decl decl, @NotNull MutableList<CodeLens> pp) {
+    var refs = FindReferences.findRefs(SeqView.of(decl.ref()), libraries).size();
+    if (refs > 0) {
+      pp.append(new CodeLens(LspRange.toRange(decl),
+        new Command("%d %s".formatted(refs, refs > 1 ? "usages" : "usage"), ""),
+        null));
+    }
+    StmtOps.super.visitDecl(decl, pp);
+  }
+}
diff --git a/lsp/src/main/java/org/aya/lsp/actions/SyntaxHighlight.java b/lsp/src/main/java/org/aya/lsp/actions/SyntaxHighlight.java
index fe9ef9b9c5..8374a5bcbc 100644
--- a/lsp/src/main/java/org/aya/lsp/actions/SyntaxHighlight.java
+++ b/lsp/src/main/java/org/aya/lsp/actions/SyntaxHighlight.java
@@ -15,7 +15,6 @@
 import org.aya.lsp.utils.LspRange;
 import org.aya.ref.DefVar;
 import org.aya.util.error.SourcePos;
-import org.eclipse.lsp4j.Range;
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
@@ -42,14 +41,10 @@ private static void highlight(@NotNull LibraryOwner owner, @NotNull MutableList<
 
   private static final SyntaxHighlight INSTANCE = new SyntaxHighlight();
 
-  private @NotNull Range rangeOf(@NotNull Signatured signatured) {
-    return LspRange.toRange(signatured.sourcePos());
-  }
-
   // region def, data, struct, prim, levels
   @Override
   public void visitSignatured(@NotNull Signatured signatured, @NotNull MutableList<HighlightResult.Symbol> buffer) {
-    buffer.append(new HighlightResult.Symbol(rangeOf(signatured), switch (signatured) {
+    buffer.append(new HighlightResult.Symbol(LspRange.toRange(signatured), switch (signatured) {
       case Decl.DataDecl $ -> HighlightResult.Kind.DataDef;
       case Decl.StructField $ -> HighlightResult.Kind.FieldDef;
       case Decl.PrimDecl $ -> HighlightResult.Kind.PrimDef;
diff --git a/lsp/src/main/java/org/aya/lsp/server/AyaLanguageClient.java b/lsp/src/main/java/org/aya/lsp/server/AyaLanguageClient.java
index 70f824779f..ff15600cc5 100644
--- a/lsp/src/main/java/org/aya/lsp/server/AyaLanguageClient.java
+++ b/lsp/src/main/java/org/aya/lsp/server/AyaLanguageClient.java
@@ -1,4 +1,4 @@
-// Copyright (c) 2020-2021 Yinsen (Tesla) Zhang.
+// Copyright (c) 2020-2022 Yinsen (Tesla) Zhang.
 // 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;
 
@@ -8,5 +8,6 @@
 
 public interface AyaLanguageClient extends LanguageClient {
   @JsonNotification("aya/publishSyntaxHighlight")
+  @SuppressWarnings("unused")
   void publishSyntaxHighlight(HighlightResult highlight);
 }
diff --git a/lsp/src/main/java/org/aya/lsp/server/AyaServer.java b/lsp/src/main/java/org/aya/lsp/server/AyaServer.java
index d0f75e2c07..9ee55c6984 100644
--- a/lsp/src/main/java/org/aya/lsp/server/AyaServer.java
+++ b/lsp/src/main/java/org/aya/lsp/server/AyaServer.java
@@ -7,7 +7,6 @@
 import org.aya.lsp.models.HighlightResult;
 import org.aya.lsp.utils.Log;
 import org.eclipse.lsp4j.*;
-import org.eclipse.lsp4j.jsonrpc.messages.Either;
 import org.eclipse.lsp4j.jsonrpc.services.JsonRequest;
 import org.eclipse.lsp4j.services.*;
 import org.jetbrains.annotations.NotNull;
@@ -22,17 +21,20 @@ public class AyaServer implements LanguageClientAware, LanguageServer {
   private final AyaService service = new AyaService();
 
   @JsonRequest("aya/load")
+  @SuppressWarnings("unused")
   public @NotNull CompletableFuture<@NotNull List<HighlightResult>> load(Object uri) {
     var uriString = (String) uri; // see JavaDoc of JsonRequest
     return CompletableFuture.supplyAsync(() -> service.loadFile(uriString));
   }
 
   @JsonRequest("aya/computeType")
+  @SuppressWarnings("unused")
   public @NotNull CompletableFuture<@NotNull ComputeTermResult> computeType(ComputeTermResult.Params input) {
     return CompletableFuture.supplyAsync(() -> service.computeTerm(input, ComputeTerm.Kind.type(service.sharedPrimFactory)));
   }
 
   @JsonRequest("aya/computeNF")
+  @SuppressWarnings("unused")
   public @NotNull CompletableFuture<@NotNull ComputeTermResult> computeNF(ComputeTermResult.Params input) {
     return CompletableFuture.supplyAsync(() -> service.computeTerm(input, ComputeTerm.Kind.nf(service.sharedPrimFactory)));
   }
@@ -45,19 +47,20 @@ public class AyaServer implements LanguageClientAware, LanguageServer {
     return CompletableFuture.supplyAsync(() -> {
       var cap = new ServerCapabilities();
       cap.setTextDocumentSync(TextDocumentSyncKind.None);
-      cap.setCompletionProvider(new CompletionOptions(true, Collections.singletonList(
-        "QWERTYUIOPASDFGHJKLZXCVBNM.qwertyuiopasdfghjklzxcvbnm+-*/_[]:")));
-      cap.setDefinitionProvider(Either.forLeft(true));
       var workCap = new WorkspaceServerCapabilities();
       var workOps = new WorkspaceFoldersOptions();
       workOps.setSupported(true);
       workOps.setChangeNotifications(true);
       workCap.setWorkspaceFolders(workOps);
+      cap.setCompletionProvider(new CompletionOptions(true, Collections.singletonList(
+        "QWERTYUIOPASDFGHJKLZXCVBNM.qwertyuiopasdfghjklzxcvbnm+-*/_[]:")));
       cap.setWorkspace(workCap);
-      cap.setHoverProvider(true);
+      cap.setDefinitionProvider(true);
       cap.setReferencesProvider(true);
+      cap.setHoverProvider(true);
       cap.setRenameProvider(new RenameOptions(true));
       cap.setDocumentHighlightProvider(true);
+      cap.setCodeLensProvider(new CodeLensOptions(true));
 
       var folders = params.getWorkspaceFolders();
       // In case we open a single file, this value will be null, so be careful.
diff --git a/lsp/src/main/java/org/aya/lsp/server/AyaService.java b/lsp/src/main/java/org/aya/lsp/server/AyaService.java
index 514602c280..153dfdcf0d 100644
--- a/lsp/src/main/java/org/aya/lsp/server/AyaService.java
+++ b/lsp/src/main/java/org/aya/lsp/server/AyaService.java
@@ -317,6 +317,20 @@ public CompletableFuture<List<? extends DocumentHighlight>> documentHighlight(Do
     });
   }
 
+  @Override
+  public CompletableFuture<List<? extends CodeLens>> codeLens(CodeLensParams params) {
+    return CompletableFuture.supplyAsync(() -> {
+      var source = find(params.getTextDocument().getUri());
+      if (source == null) return Collections.emptyList();
+      return LensMaker.invoke(source, libraries.view());
+    });
+  }
+
+  @Override
+  public CompletableFuture<CodeLens> resolveCodeLens(CodeLens unresolved) {
+    return CompletableFuture.completedFuture(unresolved);
+  }
+
   public ComputeTermResult computeTerm(@NotNull ComputeTermResult.Params input, ComputeTerm.Kind type) {
     var source = find(input.uri);
     if (source == null) return ComputeTermResult.bad(input);
diff --git a/lsp/src/main/java/org/aya/lsp/utils/LspRange.java b/lsp/src/main/java/org/aya/lsp/utils/LspRange.java
index c0a8c7e39d..9b454e4f1d 100644
--- a/lsp/src/main/java/org/aya/lsp/utils/LspRange.java
+++ b/lsp/src/main/java/org/aya/lsp/utils/LspRange.java
@@ -1,7 +1,8 @@
-// Copyright (c) 2020-2021 Yinsen (Tesla) Zhang.
+// Copyright (c) 2020-2022 Yinsen (Tesla) Zhang.
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.lsp.utils;
 
+import org.aya.concrete.stmt.Signatured;
 import org.aya.util.error.SourcePos;
 import org.eclipse.lsp4j.Location;
 import org.eclipse.lsp4j.LocationLink;
@@ -22,6 +23,10 @@ public class LspRange {
       new Position(sourcePos.endLine() - 1, sourcePos.endColumn() + 1));
   }
 
+  public static @NotNull Range toRange(@NotNull Signatured signatured) {
+    return toRange(signatured.sourcePos());
+  }
+
   public static @Nullable LocationLink toLoc(@NotNull SourcePos from, @NotNull SourcePos to) {
     var uri = to.file().underlying().map(Path::toUri).map(Objects::toString);
     if (uri.isEmpty()) return null;

From a41cfb74d06fcdc5686cbb0e08005ccc16d31d6a Mon Sep 17 00:00:00 2001
From: imkiva <imkiva@islovely.icu>
Date: Fri, 10 Jun 2022 19:39:59 +0800
Subject: [PATCH 04/16] LSP: show references popup in CodeLens

Signed-off-by: imkiva <imkiva@islovely.icu>
---
 .../java/org/aya/lsp/actions/LensMaker.java   | 41 ++++++++++++++++---
 .../java/org/aya/lsp/server/AyaService.java   |  5 ++-
 .../main/java/org/aya/lsp/utils/LspRange.java | 11 +++--
 3 files changed, 47 insertions(+), 10 deletions(-)

diff --git a/lsp/src/main/java/org/aya/lsp/actions/LensMaker.java b/lsp/src/main/java/org/aya/lsp/actions/LensMaker.java
index 71213ec9a2..3f9e6cf573 100644
--- a/lsp/src/main/java/org/aya/lsp/actions/LensMaker.java
+++ b/lsp/src/main/java/org/aya/lsp/actions/LensMaker.java
@@ -2,6 +2,8 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.lsp.actions;
 
+import com.google.gson.Gson;
+import com.google.gson.JsonElement;
 import kala.collection.SeqView;
 import kala.collection.mutable.MutableList;
 import org.aya.cli.library.source.LibraryOwner;
@@ -24,13 +26,42 @@ public record LensMaker(@NotNull SeqView<LibraryOwner> libraries) implements Stm
     return lens.asJava();
   }
 
+  public static @NotNull CodeLens resolve(@NotNull CodeLens codeLens) {
+    var cmd = new Gson().fromJson((JsonElement) codeLens.getData(), Command.class);
+    return new CodeLens(codeLens.getRange(), cmd, codeLens.getData());
+  }
+
   @Override
   public void visitDecl(@NotNull Decl decl, @NotNull MutableList<CodeLens> pp) {
-    var refs = FindReferences.findRefs(SeqView.of(decl.ref()), libraries).size();
-    if (refs > 0) {
-      pp.append(new CodeLens(LspRange.toRange(decl),
-        new Command("%d %s".formatted(refs, refs > 1 ? "usages" : "usage"), ""),
-        null));
+    var refs = FindReferences.findRefs(SeqView.of(decl.ref()), libraries).toImmutableSeq();
+    if (refs.size() > 0) {
+      var range = LspRange.toRange(decl);
+      var uri = LspRange.fileUri(decl.sourcePos());
+      // https://code.visualstudio.com/api/references/commands
+      // editor.action.showReferences (or vscode.executeReferenceProvider) - Execute all reference providers.
+      //   uri - Uri of a text document
+      //   position - A position in a text document
+      //   (returns) - A promise that resolves to an array of Location-instances.
+      var cmd = uri.isDefined()
+        ? new Command(
+        refs.sizeEquals(1) ? "1 usage" : "%d usages".formatted(refs.size()),
+        "editor.action.showReferences",
+        List.of(uri.get(), range.getEnd(), refs.mapNotNull(LspRange::toLoc).asJava()))
+        : null;
+
+      // the type of variable `cmd` is Command, but it cannot be used as
+      // the command of the CodeLens created below, because VSCode cannot parse
+      // the argument of the command directly due to some Uri serialization problems.
+      // see: https://github.com/microsoft/vscode-languageserver-node/issues/495
+
+      // To address the annoying, we use the following workaround:
+      // 1. Put the `cmd` as the data field of the CodeLens, so VSCode will not
+      //    think the CodeLens _resolved_. A separated resolving stage is required
+      //    to make the CodeLens visible to users.
+      // 2. In AyaService, register a CodeLens resolver which simply set the command field from data.
+      // 3. Together with step2, register a middleware in LSP client (the VSCode side)
+      //    to convert Java serialized Uris to vscode.Uri
+      pp.append(new CodeLens(range, null, cmd));
     }
     StmtOps.super.visitDecl(decl, pp);
   }
diff --git a/lsp/src/main/java/org/aya/lsp/server/AyaService.java b/lsp/src/main/java/org/aya/lsp/server/AyaService.java
index 153dfdcf0d..3c4ebabd1d 100644
--- a/lsp/src/main/java/org/aya/lsp/server/AyaService.java
+++ b/lsp/src/main/java/org/aya/lsp/server/AyaService.java
@@ -55,6 +55,7 @@ public class AyaService implements WorkspaceService, TextDocumentService {
   /**
    * When working with LSP, we need to track all previously created Primitives.
    * This is shared among all loaded libraries just like a Global PrimFactory before.
+   *
    * @implNote consider using one shared factory among all mocked libraries, and separate factory for each real library.
    */
   protected final @NotNull PrimDef.Factory sharedPrimFactory = new PrimDef.Factory();
@@ -327,8 +328,8 @@ public CompletableFuture<List<? extends CodeLens>> codeLens(CodeLensParams param
   }
 
   @Override
-  public CompletableFuture<CodeLens> resolveCodeLens(CodeLens unresolved) {
-    return CompletableFuture.completedFuture(unresolved);
+  public CompletableFuture<CodeLens> resolveCodeLens(CodeLens codeLens) {
+    return CompletableFuture.supplyAsync(() -> LensMaker.resolve(codeLens));
   }
 
   public ComputeTermResult computeTerm(@NotNull ComputeTermResult.Params input, ComputeTerm.Kind type) {
diff --git a/lsp/src/main/java/org/aya/lsp/utils/LspRange.java b/lsp/src/main/java/org/aya/lsp/utils/LspRange.java
index 9b454e4f1d..3167395ed5 100644
--- a/lsp/src/main/java/org/aya/lsp/utils/LspRange.java
+++ b/lsp/src/main/java/org/aya/lsp/utils/LspRange.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.utils;
 
+import kala.control.Option;
 import org.aya.concrete.stmt.Signatured;
 import org.aya.util.error.SourcePos;
 import org.eclipse.lsp4j.Location;
@@ -11,8 +12,8 @@
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
+import java.net.URI;
 import java.nio.file.Path;
-import java.util.Objects;
 
 public class LspRange {
   public static final Range NONE = new Range();
@@ -27,8 +28,12 @@ public class LspRange {
     return toRange(signatured.sourcePos());
   }
 
+  public static @NotNull Option<String> fileUri(@NotNull SourcePos sourcePos) {
+    return sourcePos.file().underlying().map(Path::toUri).map(URI::toString);
+  }
+
   public static @Nullable LocationLink toLoc(@NotNull SourcePos from, @NotNull SourcePos to) {
-    var uri = to.file().underlying().map(Path::toUri).map(Objects::toString);
+    var uri = fileUri(to);
     if (uri.isEmpty()) return null;
     var fromRange = toRange(from);
     var toRange = toRange(to);
@@ -36,7 +41,7 @@ public class LspRange {
   }
 
   public static @Nullable Location toLoc(@NotNull SourcePos to) {
-    var uri = to.file().underlying().map(Path::toUri).map(Objects::toString);
+    var uri = fileUri(to);
     if (uri.isEmpty()) return null;
     var toRange = toRange(to);
     return new Location(uri.get(), toRange);

From 73687d3153d139dfc3244504d3c282f3dba89f42 Mon Sep 17 00:00:00 2001
From: imkiva <imkiva@islovely.icu>
Date: Sat, 11 Jun 2022 15:35:23 +0800
Subject: [PATCH 05/16] LSP: CodeLens for constructors and fields

---
 .../java/org/aya/lsp/actions/LensMaker.java   | 35 +++++++++++++------
 .../main/java/org/aya/lsp/utils/Resolver.java | 15 ++++++--
 2 files changed, 36 insertions(+), 14 deletions(-)

diff --git a/lsp/src/main/java/org/aya/lsp/actions/LensMaker.java b/lsp/src/main/java/org/aya/lsp/actions/LensMaker.java
index 3f9e6cf573..615c153480 100644
--- a/lsp/src/main/java/org/aya/lsp/actions/LensMaker.java
+++ b/lsp/src/main/java/org/aya/lsp/actions/LensMaker.java
@@ -10,7 +10,10 @@
 import org.aya.cli.library.source.LibrarySource;
 import org.aya.concrete.stmt.Decl;
 import org.aya.concrete.visitor.StmtOps;
+import org.aya.lsp.utils.Log;
 import org.aya.lsp.utils.LspRange;
+import org.aya.lsp.utils.Resolver;
+import org.aya.ref.DefVar;
 import org.eclipse.lsp4j.CodeLens;
 import org.eclipse.lsp4j.Command;
 import org.jetbrains.annotations.NotNull;
@@ -32,23 +35,34 @@ public record LensMaker(@NotNull SeqView<LibraryOwner> libraries) implements Stm
   }
 
   @Override
-  public void visitDecl(@NotNull Decl decl, @NotNull MutableList<CodeLens> pp) {
-    var refs = FindReferences.findRefs(SeqView.of(decl.ref()), libraries).toImmutableSeq();
+  public void visitDecl(@NotNull Decl maybe, @NotNull MutableList<CodeLens> pp) {
+    Resolver.withChildren(maybe).forEach(defVar -> buildLens(defVar, pp));
+    StmtOps.super.visitDecl(maybe, pp);
+  }
+
+  private void buildLens(@NotNull DefVar<?, ?> defVar, @NotNull MutableList<CodeLens> pp) {
+    if (defVar.concrete == null) {
+      Log.d("LensMaker: concrete is null for %s, skipped", defVar.name());
+      return;
+    }
+
+    var refs = FindReferences.findRefs(SeqView.of(defVar), libraries).toImmutableSeq();
+
     if (refs.size() > 0) {
-      var range = LspRange.toRange(decl);
-      var uri = LspRange.fileUri(decl.sourcePos());
+      var sourcePos = defVar.concrete.sourcePos();
+      var uri = LspRange.fileUri(sourcePos);
+      var range = LspRange.toRange(sourcePos);
+
       // https://code.visualstudio.com/api/references/commands
       // editor.action.showReferences (or vscode.executeReferenceProvider) - Execute all reference providers.
       //   uri - Uri of a text document
       //   position - A position in a text document
       //   (returns) - A promise that resolves to an array of Location-instances.
+      var title = refs.sizeEquals(1) ? "1 usage" : "%d usages".formatted(refs.size());
+      var locations = refs.mapNotNull(LspRange::toLoc).asJava();
       var cmd = uri.isDefined()
-        ? new Command(
-        refs.sizeEquals(1) ? "1 usage" : "%d usages".formatted(refs.size()),
-        "editor.action.showReferences",
-        List.of(uri.get(), range.getEnd(), refs.mapNotNull(LspRange::toLoc).asJava()))
-        : null;
-
+        ? new Command(title, "editor.action.showReferences", List.of(uri.get(), range.getEnd(), locations))
+        : new Command(title, "");
       // the type of variable `cmd` is Command, but it cannot be used as
       // the command of the CodeLens created below, because VSCode cannot parse
       // the argument of the command directly due to some Uri serialization problems.
@@ -63,6 +77,5 @@ public void visitDecl(@NotNull Decl decl, @NotNull MutableList<CodeLens> pp) {
       //    to convert Java serialized Uris to vscode.Uri
       pp.append(new CodeLens(range, null, cmd));
     }
-    StmtOps.super.visitDecl(decl, pp);
   }
 }
diff --git a/lsp/src/main/java/org/aya/lsp/utils/Resolver.java b/lsp/src/main/java/org/aya/lsp/utils/Resolver.java
index 46cf63a126..183c4d47cf 100644
--- a/lsp/src/main/java/org/aya/lsp/utils/Resolver.java
+++ b/lsp/src/main/java/org/aya/lsp/utils/Resolver.java
@@ -11,6 +11,7 @@
 import org.aya.concrete.Expr;
 import org.aya.concrete.Pattern;
 import org.aya.concrete.stmt.Command;
+import org.aya.concrete.stmt.Decl;
 import org.aya.concrete.stmt.Signatured;
 import org.aya.concrete.stmt.Stmt;
 import org.aya.concrete.visitor.StmtOps;
@@ -35,7 +36,7 @@ public interface Resolver {
   ) {
     var mod = resolveModule(owner, module);
     return mod.mapNotNull(m -> m.tycked().value)
-      .map(defs -> defs.flatMap(Resolver::withSubLevel))
+      .map(defs -> defs.flatMap(Resolver::withChildren))
       .flatMap(defs -> defs.find(def -> def.ref().name().equals(name)));
   }
 
@@ -51,7 +52,7 @@ public interface Resolver {
     return resolver.targetVars.view().mapNotNull(pos -> switch (pos.data()) {
       case DefVar<?, ?> defVar -> {
         if (defVar.concrete != null) yield new WithPos<>(pos.sourcePos(), defVar);
-          // defVar is an imported and serialized symbol, so we need to find the original one
+        // defVar is an imported and serialized symbol, so we need to find the original one
         else if (defVar.module != null) {
           yield Resolver.resolveDef(source.owner(), defVar.module, defVar.name())
             .map(target -> new WithPos<Var>(pos.sourcePos(), target.ref()))
@@ -66,7 +67,7 @@ else if (defVar.module != null) {
     });
   }
 
-  private static @NotNull SeqView<Def> withSubLevel(@NotNull Def def) {
+  private static @NotNull SeqView<Def> withChildren(@NotNull Def def) {
     return switch (def) {
       case DataDef data -> SeqView.<Def>of(data).appendedAll(data.body);
       case StructDef struct -> SeqView.<Def>of(struct).appendedAll(struct.fields);
@@ -74,6 +75,14 @@ else if (defVar.module != null) {
     };
   }
 
+  static @NotNull SeqView<DefVar<?, ?>> withChildren(@NotNull Decl def) {
+    return switch (def) {
+      case Decl.DataDecl data -> SeqView.<DefVar<?, ?>>of(data.ref).appendedAll(data.body.map(Decl.DataCtor::ref));
+      case Decl.StructDecl struct -> SeqView.<DefVar<?, ?>>of(struct.ref).appendedAll(struct.fields.map(Decl.StructField::ref));
+      default -> SeqView.of(def.ref());
+    };
+  }
+
   /** resolve a top-level module by its qualified name */
   static @NotNull Option<LibrarySource> resolveModule(@NotNull LibraryOwner owner, @NotNull ImmutableSeq<String> module) {
     if (module.isEmpty()) return Option.none();

From c2dfd0aec82fd3dac211661ad9a0f4adea094285 Mon Sep 17 00:00:00 2001
From: imkiva <imkiva@islovely.icu>
Date: Sat, 11 Jun 2022 14:54:27 +0800
Subject: [PATCH 06/16] BUILD: upgrade lsp4j to 0.14.0

---
 gradle/deps.properties | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/gradle/deps.properties b/gradle/deps.properties
index 69783fc490..a2e1fea669 100644
--- a/gradle/deps.properties
+++ b/gradle/deps.properties
@@ -9,7 +9,7 @@ version.junit=5.8.2
 version.jacoco=0.8.8
 version.picocli=4.6.3
 version.jimgui=v0.21.0
-version.lsp4j=0.12.0
+version.lsp4j=0.14.0
 version.gson=2.9.0
 version.commonmark=0.18.1
 version.jline=3.21.0

From d131baa8014083c35851b3dc6e3701e085bc16a7 Mon Sep 17 00:00:00 2001
From: imkiva <imkiva@islovely.icu>
Date: Sat, 11 Jun 2022 14:58:11 +0800
Subject: [PATCH 07/16] LSP: inlay hint

---
 lsp/build.gradle.kts                          |  1 -
 lsp/src/main/java/module-info.java            |  1 +
 .../java/org/aya/lsp/actions/ComputeTerm.java |  8 ++--
 .../org/aya/lsp/actions/InlayHintMaker.java   | 41 +++++++++++++++++++
 .../org/aya/lsp/actions/SyntaxNodeAction.java | 30 +++++++++++---
 .../java/org/aya/lsp/server/AyaServer.java    |  1 +
 .../java/org/aya/lsp/server/AyaService.java   | 14 +++++++
 lsp/src/main/java/org/aya/lsp/utils/XY.java   |  3 +-
 lsp/src/main/java/org/aya/lsp/utils/XYXY.java | 18 ++++++++
 9 files changed, 105 insertions(+), 12 deletions(-)
 create mode 100644 lsp/src/main/java/org/aya/lsp/actions/InlayHintMaker.java
 create mode 100644 lsp/src/main/java/org/aya/lsp/utils/XYXY.java

diff --git a/lsp/build.gradle.kts b/lsp/build.gradle.kts
index 7d0ae4998a..2513a4d8e9 100644
--- a/lsp/build.gradle.kts
+++ b/lsp/build.gradle.kts
@@ -29,7 +29,6 @@ jlink {
   addExtraDependencies("jline-terminal-jansi")
   mergedModule {
     additive = true
-    requires("com.google.gson")
     uses("org.jline.terminal.spi.JansiSupport")
   }
   launcher {
diff --git a/lsp/src/main/java/module-info.java b/lsp/src/main/java/module-info.java
index 9a71bdf9de..1fc4567d8d 100644
--- a/lsp/src/main/java/module-info.java
+++ b/lsp/src/main/java/module-info.java
@@ -2,6 +2,7 @@
   requires static org.jetbrains.annotations;
   requires org.aya;
   requires org.aya.cli;
+  requires com.google.gson;
   requires org.eclipse.lsp4j;
   requires org.eclipse.lsp4j.jsonrpc;
   requires info.picocli;
diff --git a/lsp/src/main/java/org/aya/lsp/actions/ComputeTerm.java b/lsp/src/main/java/org/aya/lsp/actions/ComputeTerm.java
index ef6a9531fb..97cb9e4d80 100644
--- a/lsp/src/main/java/org/aya/lsp/actions/ComputeTerm.java
+++ b/lsp/src/main/java/org/aya/lsp/actions/ComputeTerm.java
@@ -17,7 +17,7 @@
 
 import java.util.function.Function;
 
-public final class ComputeTerm implements SyntaxNodeAction {
+public final class ComputeTerm implements SyntaxNodeAction.Cursor {
   private @Nullable WithPos<Term> result = null;
   private final @NotNull LibrarySource source;
   private final @NotNull Kind kind;
@@ -52,14 +52,14 @@ public ComputeTerm(@NotNull LibrarySource source, @NotNull Kind kind) {
     return result == null ? ComputeTermResult.bad(params) : ComputeTermResult.good(params, result);
   }
 
-  @Override public @NotNull Expr visitExpr(@NotNull Expr expr, XY pp) {
+  @Override public @NotNull Expr visitExpr(@NotNull Expr expr, XY xy) {
     if (expr instanceof Expr.WithTerm withTerm) {
       var sourcePos = withTerm.sourcePos();
-      if (pp.inside(sourcePos)) {
+      if (xy.inside(sourcePos)) {
         var core = withTerm.core();
         if (core != null) result = new WithPos<>(sourcePos, kind.map.apply(core));
       }
     }
-    return SyntaxNodeAction.super.visitExpr(expr, pp);
+    return Cursor.super.visitExpr(expr, xy);
   }
 }
diff --git a/lsp/src/main/java/org/aya/lsp/actions/InlayHintMaker.java b/lsp/src/main/java/org/aya/lsp/actions/InlayHintMaker.java
new file mode 100644
index 0000000000..64c9a0731e
--- /dev/null
+++ b/lsp/src/main/java/org/aya/lsp/actions/InlayHintMaker.java
@@ -0,0 +1,41 @@
+// Copyright (c) 2020-2022 Yinsen (Tesla) Zhang.
+// Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
+package org.aya.lsp.actions;
+
+import kala.collection.mutable.MutableList;
+import org.aya.cli.library.source.LibrarySource;
+import org.aya.concrete.Pattern;
+import org.aya.lsp.utils.LspRange;
+import org.aya.lsp.utils.XYXY;
+import org.eclipse.lsp4j.InlayHint;
+import org.eclipse.lsp4j.InlayHintKind;
+import org.eclipse.lsp4j.Range;
+import org.eclipse.lsp4j.jsonrpc.messages.Either;
+import org.jetbrains.annotations.NotNull;
+
+import java.util.Collections;
+import java.util.List;
+
+public record InlayHintMaker(
+  @NotNull MutableList<InlayHint> hints
+) implements SyntaxNodeAction.Ranged {
+  public static @NotNull List<InlayHint> invoke(@NotNull LibrarySource source, @NotNull Range range) {
+    var program = source.program().value;
+    if (program == null) return Collections.emptyList();
+    var xyxy = new XYXY(range);
+    var maker = new InlayHintMaker(MutableList.create());
+    maker.visitAll(program, xyxy);
+    return maker.hints.asJava();
+  }
+
+  @Override public @NotNull Pattern visitPattern(@NotNull Pattern pattern, XYXY pp) {
+    if (pattern instanceof Pattern.Bind bind) {
+      var range = LspRange.toRange(bind.sourcePos());
+      var hint = new InlayHint(range.getEnd(), Either.forLeft(": {?}"));
+      hint.setKind(InlayHintKind.Type);
+      hint.setPaddingLeft(true);
+      hints.append(hint);
+    }
+    return Ranged.super.visitPattern(pattern, pp);
+  }
+}
diff --git a/lsp/src/main/java/org/aya/lsp/actions/SyntaxNodeAction.java b/lsp/src/main/java/org/aya/lsp/actions/SyntaxNodeAction.java
index 3c266d3f10..e585cec750 100644
--- a/lsp/src/main/java/org/aya/lsp/actions/SyntaxNodeAction.java
+++ b/lsp/src/main/java/org/aya/lsp/actions/SyntaxNodeAction.java
@@ -8,6 +8,8 @@
 import org.aya.concrete.stmt.Stmt;
 import org.aya.concrete.visitor.StmtOps;
 import org.aya.lsp.utils.XY;
+import org.aya.lsp.utils.XYXY;
+import org.aya.util.error.SourcePos;
 import org.jetbrains.annotations.NotNull;
 
 /**
@@ -16,16 +18,32 @@
  * @author ice1000
  * @implNote This does not modify the AST.
  */
-public interface SyntaxNodeAction extends StmtOps<XY> {
-  default void visitAll(@NotNull ImmutableSeq<@NotNull Stmt> stmts, XY xy) {
+public interface SyntaxNodeAction<P> extends StmtOps<P> {
+  boolean accept(@NotNull P xy, @NotNull SourcePos sourcePos);
+
+  default void visitAll(@NotNull ImmutableSeq<@NotNull Stmt> stmts, P xy) {
     stmts.forEach(stmt -> {
-      if (!(stmt instanceof Signatured decl) || xy.inside(decl.entireSourcePos))
+      if (!(stmt instanceof Signatured decl) || accept(xy, decl.entireSourcePos))
         visit(stmt, xy);
     });
   }
 
-  @Override default @NotNull Expr visitExpr(@NotNull Expr expr, XY pp) {
-    if (!pp.inside(expr.sourcePos())) return expr;
-    return StmtOps.super.visitExpr(expr, pp);
+  @Override default @NotNull Expr visitExpr(@NotNull Expr expr, P xy) {
+    if (!accept(xy, expr.sourcePos())) return expr;
+    return StmtOps.super.visitExpr(expr, xy);
+  }
+
+  /** Need to visit the decl/expr placed at the cursor position XY */
+  interface Cursor extends SyntaxNodeAction<XY> {
+    @Override default boolean accept(@NotNull XY xy, @NotNull SourcePos sourcePos) {
+      return xy.inside(sourcePos);
+    }
+  }
+
+  /** Need to visit all decls inside XYXY range */
+  interface Ranged extends SyntaxNodeAction<XYXY> {
+    @Override default boolean accept(@NotNull XYXY xy, @NotNull SourcePos sourcePos) {
+      return xy.contains(sourcePos);
+    }
   }
 }
diff --git a/lsp/src/main/java/org/aya/lsp/server/AyaServer.java b/lsp/src/main/java/org/aya/lsp/server/AyaServer.java
index 9ee55c6984..ee724fbd29 100644
--- a/lsp/src/main/java/org/aya/lsp/server/AyaServer.java
+++ b/lsp/src/main/java/org/aya/lsp/server/AyaServer.java
@@ -61,6 +61,7 @@ public class AyaServer implements LanguageClientAware, LanguageServer {
       cap.setRenameProvider(new RenameOptions(true));
       cap.setDocumentHighlightProvider(true);
       cap.setCodeLensProvider(new CodeLensOptions(true));
+      cap.setInlayHintProvider(true);
 
       var folders = params.getWorkspaceFolders();
       // In case we open a single file, this value will be null, so be careful.
diff --git a/lsp/src/main/java/org/aya/lsp/server/AyaService.java b/lsp/src/main/java/org/aya/lsp/server/AyaService.java
index 3c4ebabd1d..83e4ebe8de 100644
--- a/lsp/src/main/java/org/aya/lsp/server/AyaService.java
+++ b/lsp/src/main/java/org/aya/lsp/server/AyaService.java
@@ -332,6 +332,20 @@ public CompletableFuture<CodeLens> resolveCodeLens(CodeLens codeLens) {
     return CompletableFuture.supplyAsync(() -> LensMaker.resolve(codeLens));
   }
 
+  @Override
+  public CompletableFuture<List<InlayHint>> inlayHint(InlayHintParams params) {
+    return CompletableFuture.supplyAsync(() -> {
+      var source = find(params.getTextDocument().getUri());
+      if (source == null) return Collections.emptyList();
+      return InlayHintMaker.invoke(source, params.getRange());
+    });
+  }
+
+  @Override
+  public CompletableFuture<InlayHint> resolveInlayHint(InlayHint hint) {
+    return CompletableFuture.completedFuture(hint);
+  }
+
   public ComputeTermResult computeTerm(@NotNull ComputeTermResult.Params input, ComputeTerm.Kind type) {
     var source = find(input.uri);
     if (source == null) return ComputeTermResult.bad(input);
diff --git a/lsp/src/main/java/org/aya/lsp/utils/XY.java b/lsp/src/main/java/org/aya/lsp/utils/XY.java
index 4df5754e31..7729935af0 100644
--- a/lsp/src/main/java/org/aya/lsp/utils/XY.java
+++ b/lsp/src/main/java/org/aya/lsp/utils/XY.java
@@ -1,4 +1,4 @@
-// Copyright (c) 2020-2021 Yinsen (Tesla) Zhang.
+// Copyright (c) 2020-2022 Yinsen (Tesla) Zhang.
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.lsp.utils;
 
@@ -6,6 +6,7 @@
 import org.eclipse.lsp4j.Position;
 import org.jetbrains.annotations.NotNull;
 
+/** @see Position */
 public record XY(int x, int y) {
   public XY(@NotNull Position position) {
     this(position.getLine() + 1, position.getCharacter() - 1);
diff --git a/lsp/src/main/java/org/aya/lsp/utils/XYXY.java b/lsp/src/main/java/org/aya/lsp/utils/XYXY.java
new file mode 100644
index 0000000000..77950889f4
--- /dev/null
+++ b/lsp/src/main/java/org/aya/lsp/utils/XYXY.java
@@ -0,0 +1,18 @@
+// Copyright (c) 2020-2022 Yinsen (Tesla) Zhang.
+// Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
+package org.aya.lsp.utils;
+
+import org.aya.util.error.SourcePos;
+import org.eclipse.lsp4j.Range;
+import org.jetbrains.annotations.NotNull;
+
+/** @see Range */
+public record XYXY(@NotNull XY start, @NotNull XY end) {
+  public XYXY(@NotNull Range position) {
+    this(new XY(position.getStart()), new XY(position.getEnd()));
+  }
+
+  public boolean contains(@NotNull SourcePos sourcePos) {
+    return sourcePos.startLine() >= start.x() && sourcePos.endLine() <= end.x();
+  }
+}

From c28ad33f3b7f38f731bf8a62c35df230d1bb7e0a Mon Sep 17 00:00:00 2001
From: imkiva <imkiva@islovely.icu>
Date: Sat, 11 Jun 2022 17:09:27 +0800
Subject: [PATCH 08/16] MISC: add @ForLSP annotation for clarity

---
 base/src/main/java/org/aya/concrete/Expr.java      |  5 +++--
 .../main/java/org/aya/concrete/stmt/BindBlock.java |  5 +++--
 tools/src/main/java/org/aya/util/ForLSP.java       | 14 ++++++++++++++
 3 files changed, 20 insertions(+), 4 deletions(-)
 create mode 100644 tools/src/main/java/org/aya/util/ForLSP.java

diff --git a/base/src/main/java/org/aya/concrete/Expr.java b/base/src/main/java/org/aya/concrete/Expr.java
index f4922660bb..6df6c38c46 100644
--- a/base/src/main/java/org/aya/concrete/Expr.java
+++ b/base/src/main/java/org/aya/concrete/Expr.java
@@ -20,6 +20,7 @@
 import org.aya.resolve.visitor.ExprResolver;
 import org.aya.resolve.visitor.StmtShallowResolver;
 import org.aya.tyck.ExprTycker;
+import org.aya.util.ForLSP;
 import org.aya.util.binop.BinOpParser;
 import org.aya.util.distill.DistillerOptions;
 import org.aya.util.error.SourceNode;
@@ -50,7 +51,7 @@ default Expr resolve(@NotNull ModuleContext context) {
     return new ConcreteDistiller(options).term(BaseDistiller.Outer.Free, this);
   }
 
-  sealed interface WithTerm extends Expr {
+  @ForLSP sealed interface WithTerm extends Expr {
     @NotNull Ref<ExprTycker.Result> theCore();
     default @Nullable ExprTycker.Result core() {
       return theCore().value;
@@ -230,7 +231,7 @@ record Field(
     @NotNull WithPos<String> name,
     @NotNull ImmutableSeq<WithPos<LocalVar>> bindings,
     @NotNull Expr body,
-    @NotNull Ref<Var> resolvedField
+    @ForLSP @NotNull Ref<Var> resolvedField
   ) {}
 
   /**
diff --git a/base/src/main/java/org/aya/concrete/stmt/BindBlock.java b/base/src/main/java/org/aya/concrete/stmt/BindBlock.java
index 202c6845be..30855ef057 100644
--- a/base/src/main/java/org/aya/concrete/stmt/BindBlock.java
+++ b/base/src/main/java/org/aya/concrete/stmt/BindBlock.java
@@ -6,6 +6,7 @@
 import kala.value.Ref;
 import org.aya.ref.DefVar;
 import org.aya.resolve.context.Context;
+import org.aya.util.ForLSP;
 import org.aya.util.error.SourcePos;
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
@@ -18,8 +19,8 @@ public record BindBlock(
   @NotNull Ref<@Nullable Context> context,
   @NotNull ImmutableSeq<QualifiedID> loosers,
   @NotNull ImmutableSeq<QualifiedID> tighters,
-  @NotNull Ref<ImmutableSeq<DefVar<?, ?>>> resolvedLoosers,
-  @NotNull Ref<ImmutableSeq<DefVar<?, ?>>> resolvedTighters
+  @ForLSP @NotNull Ref<ImmutableSeq<DefVar<?, ?>>> resolvedLoosers,
+  @ForLSP @NotNull Ref<ImmutableSeq<DefVar<?, ?>>> resolvedTighters
 ) {
   public static final @NotNull BindBlock EMPTY = new BindBlock(SourcePos.NONE, new Ref<>(), ImmutableSeq.empty(), ImmutableSeq.empty(), new Ref<>(), new Ref<>());
 }
diff --git a/tools/src/main/java/org/aya/util/ForLSP.java b/tools/src/main/java/org/aya/util/ForLSP.java
new file mode 100644
index 0000000000..879dfe87e0
--- /dev/null
+++ b/tools/src/main/java/org/aya/util/ForLSP.java
@@ -0,0 +1,14 @@
+// Copyright (c) 2020-2022 Yinsen (Tesla) 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 java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+
+/** annotated that the element is an LSP hole. */
+@Retention(RetentionPolicy.SOURCE)
+@Target({ElementType.FIELD, ElementType.METHOD, ElementType.TYPE})
+public @interface ForLSP {
+}

From 4bd2dccc792c4e102d98813e842483852514ce43 Mon Sep 17 00:00:00 2001
From: imkiva <imkiva@islovely.icu>
Date: Sat, 11 Jun 2022 17:09:55 +0800
Subject: [PATCH 09/16] CONCRETE: store type to Pattern.Bind for LSP

---
 base/src/main/java/org/aya/concrete/Pattern.java            | 6 +++++-
 .../java/org/aya/concrete/desugar/BinPatternParser.java     | 6 ++++--
 base/src/main/java/org/aya/tyck/pat/PatTree.java            | 5 +++--
 base/src/main/java/org/aya/tyck/pat/PatTycker.java          | 1 +
 cli/src/main/java/org/aya/cli/parse/AyaProducer.java        | 2 +-
 5 files changed, 14 insertions(+), 6 deletions(-)

diff --git a/base/src/main/java/org/aya/concrete/Pattern.java b/base/src/main/java/org/aya/concrete/Pattern.java
index b21e49b938..dbfe9f2ada 100644
--- a/base/src/main/java/org/aya/concrete/Pattern.java
+++ b/base/src/main/java/org/aya/concrete/Pattern.java
@@ -4,12 +4,15 @@
 
 import kala.collection.immutable.ImmutableSeq;
 import kala.control.Option;
+import kala.value.Ref;
+import org.aya.core.term.Term;
 import org.aya.distill.BaseDistiller;
 import org.aya.distill.ConcreteDistiller;
 import org.aya.generic.AyaDocile;
 import org.aya.pretty.doc.Doc;
 import org.aya.ref.LocalVar;
 import org.aya.ref.Var;
+import org.aya.util.ForLSP;
 import org.aya.util.binop.BinOpParser;
 import org.aya.util.distill.DistillerOptions;
 import org.aya.util.error.SourceNode;
@@ -60,7 +63,8 @@ record CalmFace(
   record Bind(
     @NotNull SourcePos sourcePos,
     boolean explicit,
-    @NotNull LocalVar bind
+    @NotNull LocalVar bind,
+    @ForLSP @NotNull Ref<@Nullable Term> type
   ) implements Pattern {
   }
 
diff --git a/base/src/main/java/org/aya/concrete/desugar/BinPatternParser.java b/base/src/main/java/org/aya/concrete/desugar/BinPatternParser.java
index 42522b702d..cc1bfeb37b 100644
--- a/base/src/main/java/org/aya/concrete/desugar/BinPatternParser.java
+++ b/base/src/main/java/org/aya/concrete/desugar/BinPatternParser.java
@@ -3,6 +3,7 @@
 package org.aya.concrete.desugar;
 
 import kala.collection.SeqView;
+import kala.value.Ref;
 import org.aya.concrete.Pattern;
 import org.aya.concrete.error.OperatorProblem;
 import org.aya.ref.DefVar;
@@ -37,7 +38,8 @@ public BinPatternParser(boolean outerMostLicit, @NotNull ResolveInfo resolveInfo
 
   private static final Pattern OP_APP = new Pattern.Bind(
     SourcePos.NONE, true,
-    new LocalVar(BinOpSet.APP_ELEM.name()));
+    new LocalVar(BinOpSet.APP_ELEM.name()),
+    new Ref<>());
 
   @Override protected @NotNull Pattern appOp() {
     return OP_APP;
@@ -57,7 +59,7 @@ public BinPatternParser(boolean outerMostLicit, @NotNull ResolveInfo resolveInfo
   }
 
   @Override protected @NotNull Pattern createErrorExpr(@NotNull SourcePos sourcePos) {
-    return new Pattern.Bind(sourcePos, true, new LocalVar("a broken constructor pattern"));
+    return new Pattern.Bind(sourcePos, true, new LocalVar("a broken constructor pattern"), new Ref<>());
   }
 
   @Override protected @Nullable OpDecl underlyingOpDecl(@NotNull Pattern elem) {
diff --git a/base/src/main/java/org/aya/tyck/pat/PatTree.java b/base/src/main/java/org/aya/tyck/pat/PatTree.java
index f02bec36fe..d60d279731 100644
--- a/base/src/main/java/org/aya/tyck/pat/PatTree.java
+++ b/base/src/main/java/org/aya/tyck/pat/PatTree.java
@@ -4,8 +4,9 @@
 
 import kala.collection.immutable.ImmutableSeq;
 import kala.collection.mutable.MutableList;
-import org.aya.ref.LocalVar;
+import kala.value.Ref;
 import org.aya.concrete.Pattern;
+import org.aya.ref.LocalVar;
 import org.aya.util.TreeBuilder;
 import org.aya.util.error.SourcePos;
 import org.aya.util.error.WithPos;
@@ -25,7 +26,7 @@ public PatTree(@NotNull String s, boolean explicit, int argsCount) {
 
   public @NotNull Pattern toPattern() {
     var childPatterns = children.isEmpty()
-      ? ImmutableSeq.<Pattern>fill(argsCount, new Pattern.Bind(SourcePos.NONE, true, new LocalVar("_")))
+      ? ImmutableSeq.<Pattern>fill(argsCount, new Pattern.Bind(SourcePos.NONE, true, new LocalVar("_"), new Ref<>()))
       : children.view().map(PatTree::toPattern).toImmutableSeq();
     return new Pattern.Ctor(SourcePos.NONE, explicit, new WithPos<>(SourcePos.NONE, new LocalVar(s)), childPatterns, null);
   }
diff --git a/base/src/main/java/org/aya/tyck/pat/PatTycker.java b/base/src/main/java/org/aya/tyck/pat/PatTycker.java
index 0c407bb8a3..d282414516 100644
--- a/base/src/main/java/org/aya/tyck/pat/PatTycker.java
+++ b/base/src/main/java/org/aya/tyck/pat/PatTycker.java
@@ -192,6 +192,7 @@ private void addPatSubst(@NotNull Var var, @NotNull Pat pat, @NotNull SourcePos
       case Pattern.Bind bind -> {
         var v = bind.bind();
         exprTycker.localCtx.put(v, term);
+        bind.type().value = term;
         yield new Pat.Bind(bind.explicit(), v, term);
       }
       case Pattern.CalmFace face -> new Pat.Meta(face.explicit(), new Ref<>(),
diff --git a/cli/src/main/java/org/aya/cli/parse/AyaProducer.java b/cli/src/main/java/org/aya/cli/parse/AyaProducer.java
index 6560e94df6..09dc5c3192 100644
--- a/cli/src/main/java/org/aya/cli/parse/AyaProducer.java
+++ b/cli/src/main/java/org/aya/cli/parse/AyaProducer.java
@@ -694,7 +694,7 @@ public BiFunction<Boolean, LocalVar, Pattern> visitAtomPatterns(@NotNull AyaPars
     var number = ctx.NUMBER();
     if (number != null) return ex -> new Pattern.Number(sourcePos, ex, Integer.parseInt(number.getText()));
     var id = ctx.weakId();
-    if (id != null) return ex -> new Pattern.Bind(sourcePos, ex, new LocalVar(id.getText(), sourcePosOf(id)));
+    if (id != null) return ex -> new Pattern.Bind(sourcePos, ex, new LocalVar(id.getText(), sourcePosOf(id)), new Ref<>());
 
     return unreachable(ctx);
   }

From 621d930bdac4d96b2d4dba2f20f19259f2d06624 Mon Sep 17 00:00:00 2001
From: imkiva <imkiva@islovely.icu>
Date: Sat, 11 Jun 2022 17:21:23 +0800
Subject: [PATCH 10/16] LSP: display type of bind patterns

---
 .../main/java/org/aya/lsp/actions/InlayHintMaker.java  | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/lsp/src/main/java/org/aya/lsp/actions/InlayHintMaker.java b/lsp/src/main/java/org/aya/lsp/actions/InlayHintMaker.java
index 64c9a0731e..a6a4b2a756 100644
--- a/lsp/src/main/java/org/aya/lsp/actions/InlayHintMaker.java
+++ b/lsp/src/main/java/org/aya/lsp/actions/InlayHintMaker.java
@@ -7,6 +7,7 @@
 import org.aya.concrete.Pattern;
 import org.aya.lsp.utils.LspRange;
 import org.aya.lsp.utils.XYXY;
+import org.aya.util.distill.DistillerOptions;
 import org.eclipse.lsp4j.InlayHint;
 import org.eclipse.lsp4j.InlayHintKind;
 import org.eclipse.lsp4j.Range;
@@ -16,9 +17,7 @@
 import java.util.Collections;
 import java.util.List;
 
-public record InlayHintMaker(
-  @NotNull MutableList<InlayHint> hints
-) implements SyntaxNodeAction.Ranged {
+public record InlayHintMaker(@NotNull MutableList<InlayHint> hints) implements SyntaxNodeAction.Ranged {
   public static @NotNull List<InlayHint> invoke(@NotNull LibrarySource source, @NotNull Range range) {
     var program = source.program().value;
     if (program == null) return Collections.emptyList();
@@ -29,9 +28,10 @@ public record InlayHintMaker(
   }
 
   @Override public @NotNull Pattern visitPattern(@NotNull Pattern pattern, XYXY pp) {
-    if (pattern instanceof Pattern.Bind bind) {
+    if (pattern instanceof Pattern.Bind bind && bind.type().value != null) {
+      var type = bind.type().value.toDoc(DistillerOptions.pretty()).commonRender();
       var range = LspRange.toRange(bind.sourcePos());
-      var hint = new InlayHint(range.getEnd(), Either.forLeft(": {?}"));
+      var hint = new InlayHint(range.getEnd(), Either.forLeft(": " + type));
       hint.setKind(InlayHintKind.Type);
       hint.setPaddingLeft(true);
       hints.append(hint);

From 888c3071053d6c2b09031d8531e1f723ec65c35b Mon Sep 17 00:00:00 2001
From: imkiva <imkiva@islovely.icu>
Date: Sat, 11 Jun 2022 17:41:30 +0800
Subject: [PATCH 11/16] MISC: reduce unnecessary traversal in LSP

---
 .../java/org/aya/lsp/actions/LensMaker.java   |  5 ++--
 .../org/aya/lsp/actions/SyntaxDeclAction.java | 29 +++++++++++++++++++
 2 files changed, 31 insertions(+), 3 deletions(-)
 create mode 100644 lsp/src/main/java/org/aya/lsp/actions/SyntaxDeclAction.java

diff --git a/lsp/src/main/java/org/aya/lsp/actions/LensMaker.java b/lsp/src/main/java/org/aya/lsp/actions/LensMaker.java
index 615c153480..ebef329758 100644
--- a/lsp/src/main/java/org/aya/lsp/actions/LensMaker.java
+++ b/lsp/src/main/java/org/aya/lsp/actions/LensMaker.java
@@ -9,7 +9,6 @@
 import org.aya.cli.library.source.LibraryOwner;
 import org.aya.cli.library.source.LibrarySource;
 import org.aya.concrete.stmt.Decl;
-import org.aya.concrete.visitor.StmtOps;
 import org.aya.lsp.utils.Log;
 import org.aya.lsp.utils.LspRange;
 import org.aya.lsp.utils.Resolver;
@@ -20,7 +19,7 @@
 
 import java.util.List;
 
-public record LensMaker(@NotNull SeqView<LibraryOwner> libraries) implements StmtOps<@NotNull MutableList<CodeLens>> {
+public record LensMaker(@NotNull SeqView<LibraryOwner> libraries) implements SyntaxDeclAction<@NotNull MutableList<CodeLens>> {
   public static @NotNull List<CodeLens> invoke(@NotNull LibrarySource source, @NotNull SeqView<LibraryOwner> libraries) {
     var lens = MutableList.<CodeLens>create();
     var maker = new LensMaker(libraries);
@@ -37,7 +36,7 @@ public record LensMaker(@NotNull SeqView<LibraryOwner> libraries) implements Stm
   @Override
   public void visitDecl(@NotNull Decl maybe, @NotNull MutableList<CodeLens> pp) {
     Resolver.withChildren(maybe).forEach(defVar -> buildLens(defVar, pp));
-    StmtOps.super.visitDecl(maybe, pp);
+    SyntaxDeclAction.super.visitDecl(maybe, pp);
   }
 
   private void buildLens(@NotNull DefVar<?, ?> defVar, @NotNull MutableList<CodeLens> pp) {
diff --git a/lsp/src/main/java/org/aya/lsp/actions/SyntaxDeclAction.java b/lsp/src/main/java/org/aya/lsp/actions/SyntaxDeclAction.java
new file mode 100644
index 0000000000..1e94255bc5
--- /dev/null
+++ b/lsp/src/main/java/org/aya/lsp/actions/SyntaxDeclAction.java
@@ -0,0 +1,29 @@
+// Copyright (c) 2020-2022 Yinsen (Tesla) Zhang.
+// Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
+package org.aya.lsp.actions;
+
+import org.aya.concrete.stmt.Command;
+import org.aya.concrete.stmt.Decl;
+import org.aya.concrete.stmt.Stmt;
+import org.aya.concrete.visitor.StmtOps;
+import org.jetbrains.annotations.NotNull;
+
+/**
+ * Traverse only definitions' name and commands.
+ *
+ * @author kiva
+ * @implNote This does not modify the AST.
+ */
+public interface SyntaxDeclAction<P> extends StmtOps<P> {
+  @Override default void visit(@NotNull Stmt stmt, P pp) {
+    switch (stmt) {
+      case Decl decl -> visitDecl(decl, pp);
+      case Command cmd -> visitCommand(cmd, pp);
+      case Stmt misc -> {}
+    }
+  }
+
+  @Override default void visitDecl(@NotNull Decl decl, P pp) {
+    // should not call super
+  }
+}

From 8272100a8131add61f22f3d92c8e89ba28107bbf Mon Sep 17 00:00:00 2001
From: imkiva <imkiva@islovely.icu>
Date: Sat, 11 Jun 2022 17:52:45 +0800
Subject: [PATCH 12/16] LSP: collect symbols

---
 .../org/aya/lsp/actions/ComputeSignature.java |  3 +-
 .../java/org/aya/lsp/actions/LensMaker.java   | 75 +++++++---------
 .../org/aya/lsp/actions/ProjectSymbol.java    | 87 +++++++++++++++++++
 .../org/aya/lsp/actions/SyntaxHighlight.java  |  2 +-
 .../java/org/aya/lsp/server/AyaServer.java    |  2 +
 .../java/org/aya/lsp/server/AyaService.java   | 33 ++++---
 6 files changed, 145 insertions(+), 57 deletions(-)
 create mode 100644 lsp/src/main/java/org/aya/lsp/actions/ProjectSymbol.java

diff --git a/lsp/src/main/java/org/aya/lsp/actions/ComputeSignature.java b/lsp/src/main/java/org/aya/lsp/actions/ComputeSignature.java
index 8e371903c0..5ccfdc31c0 100644
--- a/lsp/src/main/java/org/aya/lsp/actions/ComputeSignature.java
+++ b/lsp/src/main/java/org/aya/lsp/actions/ComputeSignature.java
@@ -41,7 +41,8 @@ public interface ComputeSignature {
       default -> Doc.empty();
     };
   }
-  static @NotNull Doc computeSignature(ImmutableSeq<Term.Param> defTele, Term defResult, boolean withResult) {
+
+  static @NotNull Doc computeSignature(@NotNull ImmutableSeq<Term.Param> defTele, @NotNull Term defResult, boolean withResult) {
     var options = DistillerOptions.pretty();
     var distiller = new CoreDistiller(options);
     var tele = distiller.visitTele(defTele, defResult, Term::findUsages);
diff --git a/lsp/src/main/java/org/aya/lsp/actions/LensMaker.java b/lsp/src/main/java/org/aya/lsp/actions/LensMaker.java
index ebef329758..e961245bdb 100644
--- a/lsp/src/main/java/org/aya/lsp/actions/LensMaker.java
+++ b/lsp/src/main/java/org/aya/lsp/actions/LensMaker.java
@@ -9,10 +9,8 @@
 import org.aya.cli.library.source.LibraryOwner;
 import org.aya.cli.library.source.LibrarySource;
 import org.aya.concrete.stmt.Decl;
-import org.aya.lsp.utils.Log;
 import org.aya.lsp.utils.LspRange;
 import org.aya.lsp.utils.Resolver;
-import org.aya.ref.DefVar;
 import org.eclipse.lsp4j.CodeLens;
 import org.eclipse.lsp4j.Command;
 import org.jetbrains.annotations.NotNull;
@@ -33,48 +31,39 @@ public record LensMaker(@NotNull SeqView<LibraryOwner> libraries) implements Syn
     return new CodeLens(codeLens.getRange(), cmd, codeLens.getData());
   }
 
-  @Override
-  public void visitDecl(@NotNull Decl maybe, @NotNull MutableList<CodeLens> pp) {
-    Resolver.withChildren(maybe).forEach(defVar -> buildLens(defVar, pp));
-    SyntaxDeclAction.super.visitDecl(maybe, pp);
-  }
-
-  private void buildLens(@NotNull DefVar<?, ?> defVar, @NotNull MutableList<CodeLens> pp) {
-    if (defVar.concrete == null) {
-      Log.d("LensMaker: concrete is null for %s, skipped", defVar.name());
-      return;
-    }
+  @Override public void visitDecl(@NotNull Decl maybe, @NotNull MutableList<CodeLens> pp) {
+    Resolver.withChildren(maybe).filter(dv -> dv.concrete != null).forEach(dv -> {
+      var refs = FindReferences.findRefs(SeqView.of(dv), libraries).toImmutableSeq();
+      if (refs.size() > 0) {
+        var sourcePos = dv.concrete.sourcePos();
+        var uri = LspRange.fileUri(sourcePos);
+        var range = LspRange.toRange(sourcePos);
 
-    var refs = FindReferences.findRefs(SeqView.of(defVar), libraries).toImmutableSeq();
+        // https://code.visualstudio.com/api/references/commands
+        // editor.action.showReferences (or vscode.executeReferenceProvider) - Execute all reference providers.
+        //   uri - Uri of a text document
+        //   position - A position in a text document
+        //   (returns) - A promise that resolves to an array of Location-instances.
+        var title = refs.sizeEquals(1) ? "1 usage" : "%d usages".formatted(refs.size());
+        var locations = refs.mapNotNull(LspRange::toLoc).asJava();
+        var cmd = uri.isDefined()
+          ? new Command(title, "editor.action.showReferences", List.of(uri.get(), range.getEnd(), locations))
+          : new Command(title, "");
+        // the type of variable `cmd` is Command, but it cannot be used as
+        // the command of the CodeLens created below, because VSCode cannot parse
+        // the argument of the command directly due to some Uri serialization problems.
+        // see: https://github.com/microsoft/vscode-languageserver-node/issues/495
 
-    if (refs.size() > 0) {
-      var sourcePos = defVar.concrete.sourcePos();
-      var uri = LspRange.fileUri(sourcePos);
-      var range = LspRange.toRange(sourcePos);
-
-      // https://code.visualstudio.com/api/references/commands
-      // editor.action.showReferences (or vscode.executeReferenceProvider) - Execute all reference providers.
-      //   uri - Uri of a text document
-      //   position - A position in a text document
-      //   (returns) - A promise that resolves to an array of Location-instances.
-      var title = refs.sizeEquals(1) ? "1 usage" : "%d usages".formatted(refs.size());
-      var locations = refs.mapNotNull(LspRange::toLoc).asJava();
-      var cmd = uri.isDefined()
-        ? new Command(title, "editor.action.showReferences", List.of(uri.get(), range.getEnd(), locations))
-        : new Command(title, "");
-      // the type of variable `cmd` is Command, but it cannot be used as
-      // the command of the CodeLens created below, because VSCode cannot parse
-      // the argument of the command directly due to some Uri serialization problems.
-      // see: https://github.com/microsoft/vscode-languageserver-node/issues/495
-
-      // To address the annoying, we use the following workaround:
-      // 1. Put the `cmd` as the data field of the CodeLens, so VSCode will not
-      //    think the CodeLens _resolved_. A separated resolving stage is required
-      //    to make the CodeLens visible to users.
-      // 2. In AyaService, register a CodeLens resolver which simply set the command field from data.
-      // 3. Together with step2, register a middleware in LSP client (the VSCode side)
-      //    to convert Java serialized Uris to vscode.Uri
-      pp.append(new CodeLens(range, null, cmd));
-    }
+        // To address the annoying, we use the following workaround:
+        // 1. Put the `cmd` as the data field of the CodeLens, so VSCode will not
+        //    think the CodeLens _resolved_. A separated resolving stage is required
+        //    to make the CodeLens visible to users.
+        // 2. In AyaService, register a CodeLens resolver which simply set the command field from data.
+        // 3. Together with step2, register a middleware in LSP client (the VSCode side)
+        //    to convert Java serialized Uris to vscode.Uri
+        pp.append(new CodeLens(range, null, cmd));
+      }
+    });
+    SyntaxDeclAction.super.visitDecl(maybe, pp);
   }
 }
diff --git a/lsp/src/main/java/org/aya/lsp/actions/ProjectSymbol.java b/lsp/src/main/java/org/aya/lsp/actions/ProjectSymbol.java
new file mode 100644
index 0000000000..50e894f669
--- /dev/null
+++ b/lsp/src/main/java/org/aya/lsp/actions/ProjectSymbol.java
@@ -0,0 +1,87 @@
+// Copyright (c) 2020-2022 Yinsen (Tesla) Zhang.
+// Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
+package org.aya.lsp.actions;
+
+import kala.collection.SeqView;
+import kala.collection.immutable.ImmutableSeq;
+import kala.collection.mutable.MutableList;
+import org.aya.cli.library.source.LibraryOwner;
+import org.aya.cli.library.source.LibrarySource;
+import org.aya.concrete.stmt.Decl;
+import org.aya.lsp.utils.LspRange;
+import org.aya.lsp.utils.Resolver;
+import org.aya.ref.DefVar;
+import org.eclipse.lsp4j.DocumentSymbol;
+import org.eclipse.lsp4j.Location;
+import org.eclipse.lsp4j.SymbolKind;
+import org.eclipse.lsp4j.WorkspaceSymbol;
+import org.eclipse.lsp4j.jsonrpc.messages.Either;
+import org.jetbrains.annotations.NotNull;
+
+public final class ProjectSymbol implements SyntaxDeclAction<@NotNull MutableList<ProjectSymbol.Symbol>> {
+  private static final @NotNull ProjectSymbol INSTANCE = new ProjectSymbol();
+
+  public static @NotNull ImmutableSeq<Symbol> invoke(@NotNull LibrarySource source) {
+    var symbols = MutableList.<Symbol>create();
+    collect(source, symbols);
+    return symbols.toImmutableSeq();
+  }
+
+  public static @NotNull ImmutableSeq<Symbol> invoke(@NotNull SeqView<LibraryOwner> libraries) {
+    var symbols = MutableList.<Symbol>create();
+    libraries.forEach(lib -> collect(lib, symbols));
+    return symbols.toImmutableSeq();
+  }
+
+  private static void collect(@NotNull LibraryOwner owner, @NotNull MutableList<Symbol> symbols) {
+    owner.librarySources().forEach(src -> collect(src, symbols));
+    owner.libraryDeps().forEach(lib -> collect(lib, symbols));
+  }
+
+  private static void collect(@NotNull LibrarySource src, @NotNull MutableList<Symbol> symbols) {
+    var program = src.program().value;
+    if (program != null) program.forEach(decl -> INSTANCE.visit(decl, symbols));
+  }
+
+  @Override public void visitDecl(@NotNull Decl decl, @NotNull MutableList<Symbol> pp) {
+    var children = MutableList.<Symbol>create();
+    Resolver.withChildren(decl)
+      .filter(dv -> dv.concrete != decl && dv.concrete != null)
+      .forEach(dv -> collect(children, dv, ImmutableSeq.empty()));
+    collect(pp, decl.ref(), children.toImmutableSeq());
+    SyntaxDeclAction.super.visitDecl(decl, pp);
+  }
+
+  private void collect(@NotNull MutableList<Symbol> pp, @NotNull DefVar<?, ?> dv, @NotNull ImmutableSeq<Symbol> children) {
+    var nameLoc = LspRange.toLoc(dv.concrete.sourcePos());
+    if (nameLoc == null) return;
+    var symbol = new Symbol(
+      dv.name(),
+      ComputeSignature.computeSignature(dv, true).commonRender(),
+      SymbolKind.Function, // TODO: refactor kindOf from SyntaxHighlight
+      nameLoc,
+      nameLoc, // TODO: entireSourcePos for GenericDecl
+      children
+    );
+    pp.append(symbol);
+  }
+
+  /** Our superclass of {@link org.eclipse.lsp4j.WorkspaceSymbol} and {@link org.eclipse.lsp4j.DocumentSymbol} */
+  public record Symbol(
+    @NotNull String name,
+    @NotNull String description,
+    @NotNull SymbolKind kind,
+    @NotNull Location nameLocation,
+    @NotNull Location entireLocation,
+    @NotNull ImmutableSeq<Symbol> children
+  ) {
+    public @NotNull DocumentSymbol document() {
+      return new DocumentSymbol(name, kind, entireLocation.getRange(), nameLocation.getRange(),
+        description, children.map(Symbol::document).asJava());
+    }
+
+    public @NotNull WorkspaceSymbol workspace() {
+      return new WorkspaceSymbol(name, kind, Either.forLeft(nameLocation));
+    }
+  }
+}
diff --git a/lsp/src/main/java/org/aya/lsp/actions/SyntaxHighlight.java b/lsp/src/main/java/org/aya/lsp/actions/SyntaxHighlight.java
index 8374a5bcbc..3fc2e3ddb4 100644
--- a/lsp/src/main/java/org/aya/lsp/actions/SyntaxHighlight.java
+++ b/lsp/src/main/java/org/aya/lsp/actions/SyntaxHighlight.java
@@ -29,7 +29,7 @@ public final class SyntaxHighlight implements StmtOps<@NotNull MutableList<Highl
 
   private static void highlight(@NotNull LibraryOwner owner, @NotNull MutableList<HighlightResult> result) {
     owner.librarySources().forEach(src -> result.append(highlightOne(src)));
-    for (var dep : owner.libraryDeps()) highlight(dep, result);
+    owner.libraryDeps().forEach(dep -> highlight(dep, result));
   }
 
   private static @NotNull HighlightResult highlightOne(@NotNull LibrarySource source) {
diff --git a/lsp/src/main/java/org/aya/lsp/server/AyaServer.java b/lsp/src/main/java/org/aya/lsp/server/AyaServer.java
index ee724fbd29..fbe6bbb2e4 100644
--- a/lsp/src/main/java/org/aya/lsp/server/AyaServer.java
+++ b/lsp/src/main/java/org/aya/lsp/server/AyaServer.java
@@ -62,6 +62,8 @@ public class AyaServer implements LanguageClientAware, LanguageServer {
       cap.setDocumentHighlightProvider(true);
       cap.setCodeLensProvider(new CodeLensOptions(true));
       cap.setInlayHintProvider(true);
+      cap.setDocumentSymbolProvider(true);
+      cap.setWorkspaceSymbolProvider(true);
 
       var folders = params.getWorkspaceFolders();
       // In case we open a single file, this value will be null, so be careful.
diff --git a/lsp/src/main/java/org/aya/lsp/server/AyaService.java b/lsp/src/main/java/org/aya/lsp/server/AyaService.java
index 83e4ebe8de..b316be2dc2 100644
--- a/lsp/src/main/java/org/aya/lsp/server/AyaService.java
+++ b/lsp/src/main/java/org/aya/lsp/server/AyaService.java
@@ -96,8 +96,7 @@ private void mockLibraries(@NotNull Path path) {
   }
 
   private @Nullable LibrarySource find(@NotNull LibraryOwner owner, Path moduleFile) {
-    var sources = owner.librarySources();
-    var found = sources.find(src -> src.file().equals(moduleFile));
+    var found = owner.librarySources().find(src -> src.file().equals(moduleFile));
     if (found.isDefined()) return found.get();
     for (var dep : owner.libraryDeps()) {
       var foundDep = find(dep, moduleFile);
@@ -276,8 +275,7 @@ public CompletableFuture<Either<List<? extends Location>, List<? extends Locatio
     });
   }
 
-  @Override
-  public CompletableFuture<List<? extends Location>> references(ReferenceParams params) {
+  @Override public CompletableFuture<List<? extends Location>> references(ReferenceParams params) {
     return CompletableFuture.supplyAsync(() -> {
       var source = find(params.getTextDocument().getUri());
       if (source == null) return Collections.emptyList();
@@ -318,8 +316,7 @@ public CompletableFuture<List<? extends DocumentHighlight>> documentHighlight(Do
     });
   }
 
-  @Override
-  public CompletableFuture<List<? extends CodeLens>> codeLens(CodeLensParams params) {
+  @Override public CompletableFuture<List<? extends CodeLens>> codeLens(CodeLensParams params) {
     return CompletableFuture.supplyAsync(() -> {
       var source = find(params.getTextDocument().getUri());
       if (source == null) return Collections.emptyList();
@@ -327,13 +324,11 @@ public CompletableFuture<List<? extends CodeLens>> codeLens(CodeLensParams param
     });
   }
 
-  @Override
-  public CompletableFuture<CodeLens> resolveCodeLens(CodeLens codeLens) {
+  @Override public CompletableFuture<CodeLens> resolveCodeLens(CodeLens codeLens) {
     return CompletableFuture.supplyAsync(() -> LensMaker.resolve(codeLens));
   }
 
-  @Override
-  public CompletableFuture<List<InlayHint>> inlayHint(InlayHintParams params) {
+  @Override public CompletableFuture<List<InlayHint>> inlayHint(InlayHintParams params) {
     return CompletableFuture.supplyAsync(() -> {
       var source = find(params.getTextDocument().getUri());
       if (source == null) return Collections.emptyList();
@@ -342,8 +337,22 @@ public CompletableFuture<List<InlayHint>> inlayHint(InlayHintParams params) {
   }
 
   @Override
-  public CompletableFuture<InlayHint> resolveInlayHint(InlayHint hint) {
-    return CompletableFuture.completedFuture(hint);
+  public CompletableFuture<List<Either<SymbolInformation, DocumentSymbol>>> documentSymbol(DocumentSymbolParams params) {
+    return CompletableFuture.supplyAsync(() -> {
+      var source = find(params.getTextDocument().getUri());
+      if (source == null) return Collections.emptyList();
+      return ProjectSymbol.invoke(source)
+        .map(symbol -> Either.<SymbolInformation, DocumentSymbol>forRight(symbol.document()))
+        .asJava();
+    });
+  }
+
+  @Override
+  public CompletableFuture<Either<List<? extends SymbolInformation>, List<? extends WorkspaceSymbol>>> symbol(WorkspaceSymbolParams params) {
+    return CompletableFuture.supplyAsync(() -> Either.forRight(
+      ProjectSymbol.invoke(libraries.view())
+        .map(ProjectSymbol.Symbol::workspace)
+        .asJava()));
   }
 
   public ComputeTermResult computeTerm(@NotNull ComputeTermResult.Params input, ComputeTerm.Kind type) {

From 5260119f500c9def2d968e219e65ae957b5a2238 Mon Sep 17 00:00:00 2001
From: imkiva <imkiva@islovely.icu>
Date: Sat, 11 Jun 2022 21:03:50 +0800
Subject: [PATCH 13/16] CONCRETE: add entireSourcePos to GenericDecl

---
 base/src/main/java/org/aya/concrete/stmt/Command.java     | 1 +
 base/src/main/java/org/aya/concrete/stmt/GenericDecl.java | 3 +++
 base/src/main/java/org/aya/concrete/stmt/Signatured.java  | 4 ++++
 cli/src/main/java/org/aya/cli/parse/AyaProducer.java      | 2 +-
 4 files changed, 9 insertions(+), 1 deletion(-)

diff --git a/base/src/main/java/org/aya/concrete/stmt/Command.java b/base/src/main/java/org/aya/concrete/stmt/Command.java
index aae308c2ec..77bbe01525 100644
--- a/base/src/main/java/org/aya/concrete/stmt/Command.java
+++ b/base/src/main/java/org/aya/concrete/stmt/Command.java
@@ -81,6 +81,7 @@ public record UseHideName(
    */
   record Module(
     @Override @NotNull SourcePos sourcePos,
+    @NotNull SourcePos entireSourcePos,
     @NotNull String name,
     @NotNull ImmutableSeq<@NotNull Stmt> contents
   ) implements Command {
diff --git a/base/src/main/java/org/aya/concrete/stmt/GenericDecl.java b/base/src/main/java/org/aya/concrete/stmt/GenericDecl.java
index e888b51a8d..096c7f6b35 100644
--- a/base/src/main/java/org/aya/concrete/stmt/GenericDecl.java
+++ b/base/src/main/java/org/aya/concrete/stmt/GenericDecl.java
@@ -6,6 +6,7 @@
 import org.aya.ref.DefVar;
 import org.aya.tyck.order.TyckUnit;
 import org.aya.util.error.SourceNode;
+import org.aya.util.error.SourcePos;
 import org.jetbrains.annotations.Contract;
 import org.jetbrains.annotations.NotNull;
 
@@ -16,6 +17,8 @@
 public sealed interface GenericDecl extends SourceNode, TyckUnit permits TopLevelDecl, Signatured {
   @Contract(pure = true) @NotNull DefVar<?, ?> ref();
 
+  @NotNull SourcePos entireSourcePos();
+
   @Override default boolean needTyck(@NotNull ImmutableSeq<String> currentMod) {
     return ref().isInModule(currentMod) && ref().core == null;
   }
diff --git a/base/src/main/java/org/aya/concrete/stmt/Signatured.java b/base/src/main/java/org/aya/concrete/stmt/Signatured.java
index f0a8781afd..5b46d42f33 100644
--- a/base/src/main/java/org/aya/concrete/stmt/Signatured.java
+++ b/base/src/main/java/org/aya/concrete/stmt/Signatured.java
@@ -29,6 +29,10 @@ public sealed abstract class Signatured implements OpDecl, GenericDecl permits D
     return sourcePos;
   }
 
+  @Override public @NotNull SourcePos entireSourcePos() {
+    return entireSourcePos;
+  }
+
   protected Signatured(
     @NotNull SourcePos sourcePos,
     @NotNull SourcePos entireSourcePos,
diff --git a/cli/src/main/java/org/aya/cli/parse/AyaProducer.java b/cli/src/main/java/org/aya/cli/parse/AyaProducer.java
index 09dc5c3192..3010ff5fa4 100644
--- a/cli/src/main/java/org/aya/cli/parse/AyaProducer.java
+++ b/cli/src/main/java/org/aya/cli/parse/AyaProducer.java
@@ -859,7 +859,7 @@ public Stream<Command.Open.UseHideName> visitUseIdsComma(@NotNull AyaParser.UseI
   public @NotNull Command.Module visitModule(AyaParser.ModuleContext ctx) {
     var id = ctx.weakId();
     return new Command.Module(
-      sourcePosOf(id), id.getText(),
+      sourcePosOf(id), sourcePosOf(ctx), id.getText(),
       Seq.wrapJava(ctx.stmt()).flatMap(this::visitStmt)
     );
   }

From cd7761b5f76e6cef55443b85c4ec534d09595350 Mon Sep 17 00:00:00 2001
From: imkiva <imkiva@islovely.icu>
Date: Sat, 11 Jun 2022 21:04:12 +0800
Subject: [PATCH 14/16] LSP: compute folding ranges

---
 .../java/org/aya/lsp/actions/Folding.java     | 49 +++++++++++++++++++
 .../org/aya/lsp/actions/ProjectSymbol.java    |  8 ++-
 .../java/org/aya/lsp/server/AyaServer.java    |  1 +
 .../java/org/aya/lsp/server/AyaService.java   |  8 +++
 .../java/org/aya/util/error/SourcePos.java    |  6 ++-
 5 files changed, 66 insertions(+), 6 deletions(-)
 create mode 100644 lsp/src/main/java/org/aya/lsp/actions/Folding.java

diff --git a/lsp/src/main/java/org/aya/lsp/actions/Folding.java b/lsp/src/main/java/org/aya/lsp/actions/Folding.java
new file mode 100644
index 0000000000..d7cf4dc3f6
--- /dev/null
+++ b/lsp/src/main/java/org/aya/lsp/actions/Folding.java
@@ -0,0 +1,49 @@
+// Copyright (c) 2020-2022 Yinsen (Tesla) Zhang.
+// Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
+package org.aya.lsp.actions;
+
+import kala.collection.mutable.MutableList;
+import org.aya.cli.library.source.LibrarySource;
+import org.aya.concrete.stmt.Command;
+import org.aya.concrete.stmt.Decl;
+import org.aya.lsp.utils.LspRange;
+import org.aya.lsp.utils.Resolver;
+import org.aya.util.error.SourcePos;
+import org.eclipse.lsp4j.FoldingRange;
+import org.eclipse.lsp4j.FoldingRangeKind;
+import org.jetbrains.annotations.NotNull;
+
+import java.util.List;
+
+public final class Folding implements SyntaxDeclAction<@NotNull MutableList<FoldingRange>> {
+  public static @NotNull List<FoldingRange> invoke(@NotNull LibrarySource source) {
+    var ranges = MutableList.<FoldingRange>create();
+    var folder = new Folding();
+    var program = source.program().value;
+    if (program != null) program.forEach(decl -> folder.visit(decl, ranges));
+    return ranges.asJava();
+  }
+
+  @Override
+  public void visitCommand(@NotNull Command cmd, @NotNull MutableList<FoldingRange> pp) {
+    if (cmd instanceof Command.Module mod) pp.append(toFoldingRange(mod.entireSourcePos()));
+    SyntaxDeclAction.super.visitCommand(cmd, pp);
+  }
+
+  @Override public void visitDecl(@NotNull Decl maybe, @NotNull MutableList<FoldingRange> pp) {
+    Resolver.withChildren(maybe).filter(dv -> dv.concrete != null)
+      .map(dv -> dv.concrete.entireSourcePos())
+      .filter(pos -> pos.linesOfCode() >= 3)
+      .forEach(pos -> pp.append(toFoldingRange(pos)));
+    SyntaxDeclAction.super.visitDecl(maybe, pp);
+  }
+
+  private @NotNull FoldingRange toFoldingRange(@NotNull SourcePos sourcePos) {
+    var range = LspRange.toRange(sourcePos);
+    var fr = new FoldingRange(range.getStart().getLine(), range.getEnd().getLine());
+    fr.setStartCharacter(range.getStart().getCharacter());
+    fr.setEndCharacter(range.getEnd().getCharacter());
+    fr.setKind(FoldingRangeKind.Region);
+    return fr;
+  }
+}
diff --git a/lsp/src/main/java/org/aya/lsp/actions/ProjectSymbol.java b/lsp/src/main/java/org/aya/lsp/actions/ProjectSymbol.java
index 50e894f669..20294bbdd6 100644
--- a/lsp/src/main/java/org/aya/lsp/actions/ProjectSymbol.java
+++ b/lsp/src/main/java/org/aya/lsp/actions/ProjectSymbol.java
@@ -54,15 +54,13 @@ private static void collect(@NotNull LibrarySource src, @NotNull MutableList<Sym
 
   private void collect(@NotNull MutableList<Symbol> pp, @NotNull DefVar<?, ?> dv, @NotNull ImmutableSeq<Symbol> children) {
     var nameLoc = LspRange.toLoc(dv.concrete.sourcePos());
-    if (nameLoc == null) return;
+    var entireLoc = LspRange.toLoc(dv.concrete.entireSourcePos());
+    if (nameLoc == null || entireLoc == null) return;
     var symbol = new Symbol(
       dv.name(),
       ComputeSignature.computeSignature(dv, true).commonRender(),
       SymbolKind.Function, // TODO: refactor kindOf from SyntaxHighlight
-      nameLoc,
-      nameLoc, // TODO: entireSourcePos for GenericDecl
-      children
-    );
+      nameLoc, entireLoc, children);
     pp.append(symbol);
   }
 
diff --git a/lsp/src/main/java/org/aya/lsp/server/AyaServer.java b/lsp/src/main/java/org/aya/lsp/server/AyaServer.java
index fbe6bbb2e4..00764596d7 100644
--- a/lsp/src/main/java/org/aya/lsp/server/AyaServer.java
+++ b/lsp/src/main/java/org/aya/lsp/server/AyaServer.java
@@ -64,6 +64,7 @@ public class AyaServer implements LanguageClientAware, LanguageServer {
       cap.setInlayHintProvider(true);
       cap.setDocumentSymbolProvider(true);
       cap.setWorkspaceSymbolProvider(true);
+      cap.setFoldingRangeProvider(true);
 
       var folders = params.getWorkspaceFolders();
       // In case we open a single file, this value will be null, so be careful.
diff --git a/lsp/src/main/java/org/aya/lsp/server/AyaService.java b/lsp/src/main/java/org/aya/lsp/server/AyaService.java
index b316be2dc2..b93f689542 100644
--- a/lsp/src/main/java/org/aya/lsp/server/AyaService.java
+++ b/lsp/src/main/java/org/aya/lsp/server/AyaService.java
@@ -355,6 +355,14 @@ public CompletableFuture<Either<List<? extends SymbolInformation>, List<? extend
         .asJava()));
   }
 
+  @Override public CompletableFuture<List<FoldingRange>> foldingRange(FoldingRangeRequestParams params) {
+    return CompletableFuture.supplyAsync(() -> {
+      var source = find(params.getTextDocument().getUri());
+      if (source == null) return Collections.emptyList();
+      return Folding.invoke(source);
+    });
+  }
+
   public ComputeTermResult computeTerm(@NotNull ComputeTermResult.Params input, ComputeTerm.Kind type) {
     var source = find(input.uri);
     if (source == null) return ComputeTermResult.bad(input);
diff --git a/tools/src/main/java/org/aya/util/error/SourcePos.java b/tools/src/main/java/org/aya/util/error/SourcePos.java
index d221d40952..1a9bd9e119 100644
--- a/tools/src/main/java/org/aya/util/error/SourcePos.java
+++ b/tools/src/main/java/org/aya/util/error/SourcePos.java
@@ -1,4 +1,4 @@
-// Copyright (c) 2020-2021 Yinsen (Tesla) Zhang.
+// Copyright (c) 2020-2022 Yinsen (Tesla) 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.error;
 
@@ -109,6 +109,10 @@ public boolean belongsToSomeFile() {
     return this != SourcePos.NONE && file.isSomeFile();
   }
 
+  public int linesOfCode() {
+    return endLine - startLine + 1;
+  }
+
   @Override public String toString() {
     return "(" + tokenStartIndex + "-" + tokenEndIndex + ") ["
       + startLine + "," + startColumn + "-" + endLine + "," + endColumn + ']';

From 3d2af90fa6eaea7ef16440836561c7ded7662b95 Mon Sep 17 00:00:00 2001
From: imkiva <imkiva@islovely.icu>
Date: Sun, 12 Jun 2022 06:19:24 +0800
Subject: [PATCH 15/16] BUILD: still requires gson

---
 lsp/build.gradle.kts | 1 +
 1 file changed, 1 insertion(+)

diff --git a/lsp/build.gradle.kts b/lsp/build.gradle.kts
index 2513a4d8e9..7d0ae4998a 100644
--- a/lsp/build.gradle.kts
+++ b/lsp/build.gradle.kts
@@ -29,6 +29,7 @@ jlink {
   addExtraDependencies("jline-terminal-jansi")
   mergedModule {
     additive = true
+    requires("com.google.gson")
     uses("org.jline.terminal.spi.JansiSupport")
   }
   launcher {

From a5d765fc9f67ddde5295c83f223ae90e3df928c6 Mon Sep 17 00:00:00 2001
From: imkiva <imkiva@islovely.icu>
Date: Sun, 12 Jun 2022 06:52:37 +0800
Subject: [PATCH 16/16] TEST: fix test

---
 base/src/test/java/org/aya/concrete/ParseTest.java | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/base/src/test/java/org/aya/concrete/ParseTest.java b/base/src/test/java/org/aya/concrete/ParseTest.java
index 8444ddc4b6..a518ea6a1d 100644
--- a/base/src/test/java/org/aya/concrete/ParseTest.java
+++ b/base/src/test/java/org/aya/concrete/ParseTest.java
@@ -59,7 +59,7 @@ public class ParseTest {
   @Test
   public void issue141() {
     Assertions.assertEquals(parseStmt("module a {}"),
-      ImmutableSeq.of(new Command.Module(SourcePos.NONE, "a", ImmutableSeq.empty())));
+      ImmutableSeq.of(new Command.Module(SourcePos.NONE, SourcePos.NONE, "a", ImmutableSeq.empty())));
   }
 
   @Test public void successCmd() {