From b34379554d3e75ac021c5cddd7101b482c600a98 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Thu, 12 Sep 2024 18:09:20 +0200 Subject: [PATCH] feat: completion fallback (#5299) When the elaborator doesn't provide us with any `CompletionInfo`, we currently provide no completions whatsoever. But in many cases, we can still provide some helpful identifier completions without elaborator information. This PR adds a fallback mode for this situation. There is more potential here, but this should be a good start. In principle, this issue alleviates #5172 (since we now provide completions in these contexts). I'll leave it up to an elaboration maintainer whether we also want to ensure that the completion infos are provided correctly in these cases. --- src/Lean/Server/Completion.lean | 73 ++++++++++++++++- src/Lean/Server/InfoUtils.lean | 10 ++- .../lean/interactive/completionFallback.lean | 31 +++++++ .../completionFallback.lean.expected.out | 80 +++++++++++++++++++ tests/lean/interactive/fieldCompletion.lean | 8 -- .../fieldCompletion.lean.expected.out | 3 - 6 files changed, 187 insertions(+), 18 deletions(-) create mode 100644 tests/lean/interactive/completionFallback.lean create mode 100644 tests/lean/interactive/completionFallback.lean.expected.out delete mode 100644 tests/lean/interactive/fieldCompletion.lean delete mode 100644 tests/lean/interactive/fieldCompletion.lean.expected.out diff --git a/src/Lean/Server/Completion.lean b/src/Lean/Server/Completion.lean index d3324bac9c..cde43a624c 100644 --- a/src/Lean/Server/Completion.lean +++ b/src/Lean/Server/Completion.lean @@ -666,6 +666,50 @@ private def tacticCompletion (params : CompletionParams) (ctx : ContextInfo) : I }, 1) return some { items := sortCompletionItems items, isIncomplete := true } +/-- +If there are `Info`s that contain `hoverPos` and have a nonempty `LocalContext`, +yields the closest one of those `Info`s. +Otherwise, yields the closest `Info` that contains `hoverPos` and has an empty `LocalContext`. +-/ +private def findClosestInfoWithLocalContextAt? + (hoverPos : String.Pos) + (infoTree : InfoTree) + : Option (ContextInfo × Info) := + infoTree.visitM (m := Id) (postNode := choose) |>.join +where + choose + (ctx : ContextInfo) + (info : Info) + (_ : PersistentArray InfoTree) + (childValues : List (Option (Option (ContextInfo × Info)))) + : Option (ContextInfo × Info) := + let bestChildValue := childValues.map (·.join) |>.foldl (init := none) fun v best => + if isBetter v best then + v + else + best + if info.occursInOrOnBoundary hoverPos && isBetter (ctx, info) bestChildValue then + (ctx, info) + else + bestChildValue + + isBetter (a b : Option (ContextInfo × Info)) : Bool := + match a, b with + | none, none => false + | some _, none => true + | none, some _ => false + | some (_, ia), some (_, ib) => + if !ia.lctx.isEmpty && ib.lctx.isEmpty then + true + else if ia.lctx.isEmpty && !ib.lctx.isEmpty then + false + else if ia.isSmaller ib then + true + else if ib.isSmaller ia then + false + else + false + private def findCompletionInfoAt? (fileMap : FileMap) (hoverPos : String.Pos) @@ -675,9 +719,32 @@ private def findCompletionInfoAt? match infoTree.foldInfo (init := none) (choose hoverLine) with | some (hoverInfo, ctx, Info.ofCompletionInfo info) => some (hoverInfo, ctx, info) - | _ => - -- TODO try to extract id from `fileMap` and some `ContextInfo` from `InfoTree` - none + | _ => do + -- No completion info => Attempt providing identifier completions + let some (ctx, info) := findClosestInfoWithLocalContextAt? hoverPos infoTree + | none + let some stack := info.stx.findStack? (·.getRange?.any (·.contains hoverPos (includeStop := true))) + | none + let stack := stack.dropWhile fun (stx, _) => !(stx matches `($_:ident) || stx matches `($_:ident.)) + let some (stx, _) := stack.head? + | none + let isDotIdCompletion := stack.any fun (stx, _) => stx matches `(.$_:ident) + if isDotIdCompletion then + -- An identifier completion is never useful in a dotId completion context. + none + let some (id, danglingDot) := + match stx with + | `($id:ident) => some (id.getId, false) + | `($id:ident.) => some (id.getId, true) + | _ => none + | none + let tailPos := stx.getTailPos?.get! + let hoverInfo := + if hoverPos < tailPos then + HoverInfo.inside (tailPos - hoverPos).byteIdx + else + HoverInfo.after + some (hoverInfo, ctx, .id stx id danglingDot info.lctx none) where choose (hoverLine : Nat) diff --git a/src/Lean/Server/InfoUtils.lean b/src/Lean/Server/InfoUtils.lean index 70c8172988..361c37d39c 100644 --- a/src/Lean/Server/InfoUtils.lean +++ b/src/Lean/Server/InfoUtils.lean @@ -141,10 +141,12 @@ def Info.stx : Info → Syntax | ofOmissionInfo i => i.stx def Info.lctx : Info → LocalContext - | Info.ofTermInfo i => i.lctx - | Info.ofFieldInfo i => i.lctx - | Info.ofOmissionInfo i => i.lctx - | _ => LocalContext.empty + | .ofTermInfo i => i.lctx + | .ofFieldInfo i => i.lctx + | .ofOmissionInfo i => i.lctx + | .ofMacroExpansionInfo i => i.lctx + | .ofCompletionInfo i => i.lctx + | _ => LocalContext.empty def Info.pos? (i : Info) : Option String.Pos := i.stx.getPos? (canonicalOnly := true) diff --git a/tests/lean/interactive/completionFallback.lean b/tests/lean/interactive/completionFallback.lean new file mode 100644 index 0000000000..5297577e11 --- /dev/null +++ b/tests/lean/interactive/completionFallback.lean @@ -0,0 +1,31 @@ +-- When the elaborator doesn't provide `CompletionInfo`, try to provide identifier completions. +-- As of when this test case was written, the elaborator did not provide `CompletionInfo` in these cases. + +-- https://github.com/leanprover/lean4/issues/5172 + +inductive Direction where + | up + | right + | down + | left +deriving Repr + +def angle (d: Direction) := + match d with + | Direction. => 90 + --^ textDocument/completion + | Direction.right => 0 + | Direction.down => 270 + | Direction.left => 180 + +-- Ensure that test is stable when changes to the `And` namespace are made. +structure CustomAnd (a b : Prop) : Prop where + ha : a + hb : b + +example : p ∨ (q ∧ r) → CustomAnd (p ∨ q) (p ∨ r) := by + intro h + cases h with + | inl hp => apply CustomAnd. (Or.intro_left q hp) (Or.intro_left r hp) + --^ textDocument/completion + | inr hqr => apply CustomAnd.mk (Or.intro_right p hqr.left) (Or.intro_right p hqr.right) diff --git a/tests/lean/interactive/completionFallback.lean.expected.out b/tests/lean/interactive/completionFallback.lean.expected.out new file mode 100644 index 0000000000..7cd2e288a0 --- /dev/null +++ b/tests/lean/interactive/completionFallback.lean.expected.out @@ -0,0 +1,80 @@ +{"textDocument": {"uri": "file:///completionFallback.lean"}, + "position": {"line": 14, "character": 14}} +{"items": + [{"sortText": "0", + "label": "down", + "kind": 4, + "data": + {"params": + {"textDocument": {"uri": "file:///completionFallback.lean"}, + "position": {"line": 14, "character": 14}}, + "id": {"const": {"declName": "Direction.down"}}}}, + {"sortText": "1", + "label": "left", + "kind": 4, + "data": + {"params": + {"textDocument": {"uri": "file:///completionFallback.lean"}, + "position": {"line": 14, "character": 14}}, + "id": {"const": {"declName": "Direction.left"}}}}, + {"sortText": "2", + "label": "noConfusionType", + "kind": 3, + "data": + {"params": + {"textDocument": {"uri": "file:///completionFallback.lean"}, + "position": {"line": 14, "character": 14}}, + "id": {"const": {"declName": "Direction.noConfusionType"}}}}, + {"sortText": "3", + "label": "right", + "kind": 4, + "data": + {"params": + {"textDocument": {"uri": "file:///completionFallback.lean"}, + "position": {"line": 14, "character": 14}}, + "id": {"const": {"declName": "Direction.right"}}}}, + {"sortText": "4", + "label": "toCtorIdx", + "kind": 3, + "data": + {"params": + {"textDocument": {"uri": "file:///completionFallback.lean"}, + "position": {"line": 14, "character": 14}}, + "id": {"const": {"declName": "Direction.toCtorIdx"}}}}, + {"sortText": "5", + "label": "up", + "kind": 4, + "data": + {"params": + {"textDocument": {"uri": "file:///completionFallback.lean"}, + "position": {"line": 14, "character": 14}}, + "id": {"const": {"declName": "Direction.up"}}}}], + "isIncomplete": true} +{"textDocument": {"uri": "file:///completionFallback.lean"}, + "position": {"line": 28, "character": 30}} +{"items": + [{"sortText": "0", + "label": "ha", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///completionFallback.lean"}, + "position": {"line": 28, "character": 30}}, + "id": {"const": {"declName": "CustomAnd.ha"}}}}, + {"sortText": "1", + "label": "hb", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///completionFallback.lean"}, + "position": {"line": 28, "character": 30}}, + "id": {"const": {"declName": "CustomAnd.hb"}}}}, + {"sortText": "2", + "label": "mk", + "kind": 4, + "data": + {"params": + {"textDocument": {"uri": "file:///completionFallback.lean"}, + "position": {"line": 28, "character": 30}}, + "id": {"const": {"declName": "CustomAnd.mk"}}}}], + "isIncomplete": true} diff --git a/tests/lean/interactive/fieldCompletion.lean b/tests/lean/interactive/fieldCompletion.lean deleted file mode 100644 index 2d9ad2627c..0000000000 --- a/tests/lean/interactive/fieldCompletion.lean +++ /dev/null @@ -1,8 +0,0 @@ -import Lean - -open Lean Elab - -def f (s : DefView) : DefView := { - m - --^ textDocument/completion -} diff --git a/tests/lean/interactive/fieldCompletion.lean.expected.out b/tests/lean/interactive/fieldCompletion.lean.expected.out deleted file mode 100644 index 527d9d7e87..0000000000 --- a/tests/lean/interactive/fieldCompletion.lean.expected.out +++ /dev/null @@ -1,3 +0,0 @@ -{"textDocument": {"uri": "file:///fieldCompletion.lean"}, - "position": {"line": 5, "character": 3}} -{"items": [], "isIncomplete": true}