feat: auto-completion for dotted identifier notation

RELEASES.md

@@ -1,6 +1,13 @@
 Unreleased
 ---------
 
+* Auto-completion for dotted identifier notation. Example:
+  ```lean
+  example : Nat :=
+    .su
+  ```
+  `succ` now appears in the list of auto-completion suggestions.
+
 * `nat_lit` is not needed anymore when declaring `OfNat` instances. See issues [#1389](https://github.com/leanprover/lean4/issues/1389) and [#875](https://github.com/leanprover/lean4/issues/875). Example:
   ```lean
   inductive Bit where

src/Lean/Elab/App.lean

@@ -1294,6 +1294,7 @@ private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Arra
     | `(@$_)     => throwUnsupportedSyntax -- invalid occurrence of `@`
     | `(_)       => throwError "placeholders '_' cannot be used where a function is expected"
     | `(.$id:ident) =>
+        addCompletionInfo <| CompletionInfo.dotId f id.getId (← getLCtx) expectedType?
         let fConst ← mkConst (← resolveDotName id expectedType?)
         let fConst ← addTermInfo f fConst
         let s ← observing do

src/Lean/Elab/InfoTree/Main.lean

@@ -38,6 +38,7 @@ end ContextInfo
 def CompletionInfo.stx : CompletionInfo → Syntax
   | dot i .. => i.stx
   | id stx .. => stx
+  | dotId stx .. => stx
   | namespaceId stx => stx
   | option stx => stx
   | endSection stx .. => stx

src/Lean/Elab/InfoTree/Types.lean

@@ -41,6 +41,7 @@ structure CommandInfo extends ElabInfo where
 inductive CompletionInfo where
   | dot (termInfo : TermInfo) (field? : Option Syntax) (expectedType? : Option Expr)
   | id (stx : Syntax) (id : Name) (danglingDot : Bool) (lctx : LocalContext) (expectedType? : Option Expr)
+  | dotId (stx : Syntax) (id : Name) (lctx : LocalContext) (expectedType? : Option Expr)
   | namespaceId (stx : Syntax)
   | option (stx : Syntax)
   | endSection (stx : Syntax) (scopeNames : List String)

src/Lean/Server/Completion.lean

@@ -372,6 +372,15 @@ private def dotCompletion (ctx : ContextInfo) (info : TermInfo) (hoverInfo : Hov
             if (← isDotCompletionMethod typeName c) then
               addCompletionItem c.name.getString! c.type expectedType? c.name (kind := (← getCompletionKindForDecl c)) 1
 
+private def dotIdCompletion (ctx : ContextInfo) (lctx : LocalContext) (id : Name) (hoverInfo : HoverInfo) (expectedType? : Option Expr) : IO (Option CompletionList) :=
+  runM ctx lctx do
+    let some expectedType := expectedType? | return ()
+    let resultTypeFn := (← instantiateMVars expectedType).cleanupAnnotations.getAppFn
+    let .const typeName .. := resultTypeFn.cleanupAnnotations | return ()
+    (← getEnv).constants.forM fun declName c => do
+      let some (label, score) ← matchDecl? typeName id (danglingDot := false) declName | pure ()
+      addCompletionItem label c.type expectedType? declName (← getCompletionKindForDecl c) score
+
 private def optionCompletion (ctx : ContextInfo) (stx : Syntax) (caps : ClientCapabilities) : IO (Option CompletionList) :=
   ctx.runMetaM {} do
     let (partialName, trailingDot) :=
@@ -423,6 +432,7 @@ partial def find? (fileMap : FileMap) (hoverPos : String.Pos) (infoTree : InfoTr
     match info with
     | .dot info (expectedType? := expectedType?) .. => dotCompletion ctx info hoverInfo expectedType?
     | .id _   id danglingDot lctx expectedType? => idCompletion ctx lctx id hoverInfo danglingDot expectedType?
+    | .dotId _  id lctx expectedType? => dotIdCompletion ctx lctx id hoverInfo expectedType?
     | .option stx => optionCompletion ctx stx caps
     | .tactic .. => tacticCompletion ctx
     | _ => return none

tests/lean/interactive/dotIdCompletion.lean

@@ -0,0 +1,6 @@
+inductive Boo where
+  | true | false | truth
+
+def f : Boo :=
+  .tr
+   --^ textDocument/completion

tests/lean/interactive/dotIdCompletion.lean.expected.out

@@ -0,0 +1,7 @@
+{"textDocument": {"uri": "file://dotIdCompletion.lean"},
+ "position": {"line": 4, "character": 5}}
+{"items":
+ [{"label": "true", "kind": 4, "detail": "Boo"},
+  {"label": "truth", "kind": 4, "detail": "Boo"},
+  {"label": "toCtorIdx", "kind": 3, "detail": "Boo → Nat"}],
+ "isIncomplete": true}