From 83ee9b1a57e95a58dba4ab86b2734218a6412d8e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 30 Jul 2022 10:19:05 -0700 Subject: [PATCH] feat: auto-completion for dotted identifier notation --- RELEASES.md | 7 +++++++ src/Lean/Elab/App.lean | 1 + src/Lean/Elab/InfoTree/Main.lean | 1 + src/Lean/Elab/InfoTree/Types.lean | 1 + src/Lean/Server/Completion.lean | 10 ++++++++++ tests/lean/interactive/dotIdCompletion.lean | 6 ++++++ .../lean/interactive/dotIdCompletion.lean.expected.out | 7 +++++++ 7 files changed, 33 insertions(+) create mode 100644 tests/lean/interactive/dotIdCompletion.lean create mode 100644 tests/lean/interactive/dotIdCompletion.lean.expected.out diff --git a/RELEASES.md b/RELEASES.md index db77858be0..4a0058e4ca 100644 --- a/RELEASES.md +++ b/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 diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean index c33e88c23b..c5f310836d 100644 --- a/src/Lean/Elab/App.lean +++ b/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 diff --git a/src/Lean/Elab/InfoTree/Main.lean b/src/Lean/Elab/InfoTree/Main.lean index 7789a74fb8..132219e658 100644 --- a/src/Lean/Elab/InfoTree/Main.lean +++ b/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 diff --git a/src/Lean/Elab/InfoTree/Types.lean b/src/Lean/Elab/InfoTree/Types.lean index 71f28eb989..688ab74d98 100644 --- a/src/Lean/Elab/InfoTree/Types.lean +++ b/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) diff --git a/src/Lean/Server/Completion.lean b/src/Lean/Server/Completion.lean index 890781a3b0..8799a07583 100644 --- a/src/Lean/Server/Completion.lean +++ b/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 diff --git a/tests/lean/interactive/dotIdCompletion.lean b/tests/lean/interactive/dotIdCompletion.lean new file mode 100644 index 0000000000..658338c69a --- /dev/null +++ b/tests/lean/interactive/dotIdCompletion.lean @@ -0,0 +1,6 @@ +inductive Boo where + | true | false | truth + +def f : Boo := + .tr + --^ textDocument/completion diff --git a/tests/lean/interactive/dotIdCompletion.lean.expected.out b/tests/lean/interactive/dotIdCompletion.lean.expected.out new file mode 100644 index 0000000000..2165d5c735 --- /dev/null +++ b/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}