MERGE: #424

424: New features to LSP r=ice1000 a=imkiva

this PR upgraded LSP4j to 0.14 with inlay hints support; added some features to the LSP backend:
- Inlay type hints for bind patterns (feel free to suggest more)
- CodeLens of each definition showing `%d usages`
- Code folding for definitions that occupy 3 or more LOC.
- Search Everywhere in VSCode (symbols only since VSC does not ask more from backend)

Try it: https://github.com/aya-prover/aya-vscode/suites/6895435995/artifacts/267446633

## See also
Language Server Protocol has recently upgraded to 3.17, and VSCode stabilized their inlay hints APIs
- https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#textDocument_inlayHint
- rust-lang/rust-analyzer#11445
- microsoft/vscode-languageserver-node#495
- aya-prover/aya-vscode#21


Co-authored-by: imkiva <imkiva@islovely.icu>

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
   ) {}
 
   /**

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 {
   }
 

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) {

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

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 {

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;
   }

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,

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);
   }

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<>(),

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() {

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

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

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;

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);

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);
   }
 }

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

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;
+  }
+}

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.aya.util.distill.DistillerOptions;
+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 && 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(": " + type));
+      hint.setKind(InlayHintKind.Type);
+      hint.setPaddingLeft(true);
+      hints.append(hint);
+    }
+    return Ranged.super.visitPattern(pattern, pp);
+  }
+}