From d108e0222c768a35b2d57c363caa7fd812029097 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Wed, 4 Sep 2024 09:39:52 +0200 Subject: [PATCH 1/4] fix: travelling auto-completions This breaks pipe auto-completion because of an elaborator bug. --- src/Lean/Server/Completion.lean | 53 +++++++++++++++++++-------------- src/Lean/Server/InfoUtils.lean | 9 +++++- 2 files changed, 39 insertions(+), 23 deletions(-) diff --git a/src/Lean/Server/Completion.lean b/src/Lean/Server/Completion.lean index f3f6b5b046a8..3ffd1c7816ab 100644 --- a/src/Lean/Server/Completion.lean +++ b/src/Lean/Server/Completion.lean @@ -235,7 +235,6 @@ private def normPrivateName? (declName : Name) : MetaM (Option Name) := do Remark: `danglingDot == true` when the completion point is an identifier followed by `.`. -/ private def matchDecl? (ns : Name) (id : Name) (danglingDot : Bool) (declName : Name) : MetaM (Option (Name × Float)) := do - -- dbg_trace "{ns}, {id}, {declName}, {danglingDot}" let some declName ← normPrivateName? declName | return none if !ns.isPrefixOf declName then @@ -333,7 +332,6 @@ private def idCompletionCore if let HoverInfo.inside delta := hoverInfo then id := truncate id delta danglingDot := false - -- dbg_trace ">> id {id} : {expectedType?}" if id.isAtomic then -- search for matches in the local context for localDecl in (← getLCtx) do @@ -679,37 +677,48 @@ where : Option (HoverInfo × ContextInfo × Info) := if !info.isCompletion then best? - else if info.occursInside? hoverPos |>.isSome then - let headPos := info.pos?.get! + else if info.occursInOrOnBoundary hoverPos then + let headPos := info.pos?.get! + let tailPos := info.tailPos?.get! + let hoverInfo := + if hoverPos < tailPos then + HoverInfo.inside (hoverPos - headPos).byteIdx + else + HoverInfo.after let ⟨headPosLine, _⟩ := fileMap.toPosition headPos let ⟨tailPosLine, _⟩ := fileMap.toPosition info.tailPos?.get! if headPosLine != hoverLine || headPosLine != tailPosLine then best? else match best? with - | none => (HoverInfo.inside (hoverPos - headPos).byteIdx, ctx, info) - | some (HoverInfo.after, _, _) => (HoverInfo.inside (hoverPos - headPos).byteIdx, ctx, info) - | some (_, _, best) => - if info.isSmaller best then - (HoverInfo.inside (hoverPos - headPos).byteIdx, ctx, info) - else - best? - else if let some (HoverInfo.inside _, _, _) := best? then - -- We assume the "inside matches" have precedence over "before ones". - best? - else if info.occursDirectlyBefore hoverPos then - let pos := info.tailPos?.get! - let ⟨line, _⟩ := fileMap.toPosition pos - if line != hoverLine then best? - else match best? with - | none => (HoverInfo.after, ctx, info) + | none => (hoverInfo, ctx, info) | some (_, _, best) => - if info.isSmaller best then - (HoverInfo.after, ctx, info) + if isBetter info best then + (hoverInfo, ctx, info) else best? else best? + isBetter : Info → Info → Bool + | i₁@(.ofCompletionInfo ci₁), i₂@(.ofCompletionInfo ci₂) => + -- Use the smallest info available and prefer non-id completion over id completions as a + -- tie-breaker. + -- This is necessary because the elaborator sometimes generates both for the same range. + -- If two infos are equivalent, always prefer the first one. + if i₁.isSmaller i₂ then + true + else if i₂.isSmaller i₁ then + false + else if !(ci₁ matches .id ..) && ci₂ matches .id .. then + true + else if ci₁ matches .id .. && !(ci₂ matches .id ..) then + false + else + true + | .ofCompletionInfo _, _ => true + | _, .ofCompletionInfo _ => false + | _, _ => true + /-- Assigns the `CompletionItem.sortText?` for all items in `completions` according to their order in `completions`. This is necessary because clients will use their own sort order if the server diff --git a/src/Lean/Server/InfoUtils.lean b/src/Lean/Server/InfoUtils.lean index 9e4fc1913c50..70c817298853 100644 --- a/src/Lean/Server/InfoUtils.lean +++ b/src/Lean/Server/InfoUtils.lean @@ -165,7 +165,7 @@ def Info.size? (i : Info) : Option String.Pos := do -- `Info` without position information are considered to have "infinite" size def Info.isSmaller (i₁ i₂ : Info) : Bool := - match i₁.size?, i₂.pos? with + match i₁.size?, i₂.size? with | some sz₁, some sz₂ => sz₁ < sz₂ | some _, none => true | _, _ => false @@ -181,6 +181,13 @@ def Info.occursInside? (i : Info) (hoverPos : String.Pos) : Option String.Pos := guard (headPos ≤ hoverPos && hoverPos < tailPos) return hoverPos - headPos +def Info.occursInOrOnBoundary (i : Info) (hoverPos : String.Pos) : Bool := Id.run do + let some headPos := i.pos? + | return false + let some tailPos := i.tailPos? + | return false + return headPos <= hoverPos && hoverPos <= tailPos + def InfoTree.smallestInfo? (p : Info → Bool) (t : InfoTree) : Option (ContextInfo × Info) := let ts := t.deepestNodes fun ctx i _ => if p i then some (ctx, i) else none From 89bacd9c1f1a1ba44e836fe5a3eeedac9edbe7b2 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Wed, 4 Sep 2024 10:01:17 +0200 Subject: [PATCH 2/4] test: travelling completions --- .../interactive/travellingCompletions.lean | 44 ++++++++++++ .../travellingCompletions.lean.expected.out | 72 +++++++++++++++++++ 2 files changed, 116 insertions(+) create mode 100644 tests/lean/interactive/travellingCompletions.lean create mode 100644 tests/lean/interactive/travellingCompletions.lean.expected.out diff --git a/tests/lean/interactive/travellingCompletions.lean b/tests/lean/interactive/travellingCompletions.lean new file mode 100644 index 000000000000..459f38da4c43 --- /dev/null +++ b/tests/lean/interactive/travellingCompletions.lean @@ -0,0 +1,44 @@ +import Lean + + + +-- https://github.com/leanprover/lean4/issues/4455 +def aaaaaaaa := 1 + +#eval ([1,2,3].map λ c => aaaaaaa).length + --^ textDocument/completion + + + +-- https://github.com/leanprover/lean4/issues/4705 +structure Bar where + foobar : Nat + +structure Foo where + x : Bar + +example (f : Foo) : Nat × Nat := + ⟨f.x.foobar, f.x.f⟩ + --^ textDocument/completion + +example (b : Bar) : Nat × Nat := + ⟨b.foobar, b.f⟩ + --^ textDocument/completion + + + +-- https://github.com/leanprover/lean4/issues/5219 +structure ContinuousSMul (M X : Type) : Prop where +structure ContinuousAdd (X : Type) : Prop where + +theorem Prod.continuousSMul {M X Y : Type} : ContinuousSMul M (X × Y) := ⟨⟩ + +theorem Prod.continuousAdd {X Y : Type} : ContinuousAdd (X × Y) := ⟨⟩ + +example : (ContinuousSMul Nat (Nat × Nat)) ∧ (ContinuousAdd (Nat × Nat)) := by + exact ⟨Prod.continuousSMul, Prod.continuous⟩ + --^ textDocument/completion + +example : True ∧ True := by + exact ⟨trivial, True.in⟩ + --^ textDocument/completion diff --git a/tests/lean/interactive/travellingCompletions.lean.expected.out b/tests/lean/interactive/travellingCompletions.lean.expected.out new file mode 100644 index 000000000000..46409f6f6b53 --- /dev/null +++ b/tests/lean/interactive/travellingCompletions.lean.expected.out @@ -0,0 +1,72 @@ +{"textDocument": {"uri": "file:///travellingCompletions.lean"}, + "position": {"line": 7, "character": 33}} +{"items": + [{"sortText": "0", + "label": "aaaaaaaa", + "kind": 21, + "data": + {"params": + {"textDocument": {"uri": "file:///travellingCompletions.lean"}, + "position": {"line": 7, "character": 33}}, + "id": {"const": {"declName": "aaaaaaaa"}}}}], + "isIncomplete": true} +{"textDocument": {"uri": "file:///travellingCompletions.lean"}, + "position": {"line": 20, "character": 20}} +{"items": + [{"sortText": "0", + "label": "foobar", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///travellingCompletions.lean"}, + "position": {"line": 20, "character": 20}}, + "id": {"const": {"declName": "Bar.foobar"}}}}], + "isIncomplete": true} +{"textDocument": {"uri": "file:///travellingCompletions.lean"}, + "position": {"line": 24, "character": 16}} +{"items": + [{"sortText": "0", + "label": "foobar", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///travellingCompletions.lean"}, + "position": {"line": 24, "character": 16}}, + "id": {"const": {"declName": "Bar.foobar"}}}}], + "isIncomplete": true} +{"textDocument": {"uri": "file:///travellingCompletions.lean"}, + "position": {"line": 38, "character": 45}} +{"items": + [{"sortText": "0", + "label": "continuousAdd", + "kind": 3, + "data": + {"params": + {"textDocument": {"uri": "file:///travellingCompletions.lean"}, + "position": {"line": 38, "character": 45}}, + "id": {"const": {"declName": "Prod.continuousAdd"}}}}, + {"sortText": "1", + "label": "continuousSMul", + "kind": 3, + "data": + {"params": + {"textDocument": {"uri": "file:///travellingCompletions.lean"}, + "position": {"line": 38, "character": 45}}, + "id": {"const": {"declName": "Prod.continuousSMul"}}}}], + "isIncomplete": true} +{"textDocument": {"uri": "file:///travellingCompletions.lean"}, + "position": {"line": 42, "character": 25}} +{"items": + [{"sortText": "0", + "label": "intro", + "kind": 4, + "documentation": + {"value": + "`True` is true, and `True.intro` (or more commonly, `trivial`)\nis the proof. ", + "kind": "markdown"}, + "data": + {"params": + {"textDocument": {"uri": "file:///travellingCompletions.lean"}, + "position": {"line": 42, "character": 25}}, + "id": {"const": {"declName": "True.intro"}}}}], + "isIncomplete": true} From dddb57743120e7a70b1ee3c345d53c2976ec0f64 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Fri, 6 Sep 2024 14:27:21 +0200 Subject: [PATCH 3/4] fix: retain `SourceInfo` in `pipeProj` elaborator Co-authored-by: Sebastian Ullrich --- src/Lean/Elab/App.lean | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean index a9b0f9ff865b..373e029f9876 100644 --- a/src/Lean/Elab/App.lean +++ b/src/Lean/Elab/App.lean @@ -1594,10 +1594,13 @@ private def elabAtom : TermElab := fun stx expectedType? => do @[builtin_term_elab dotIdent] def elabDotIdent : TermElab := elabAtom @[builtin_term_elab explicitUniv] def elabExplicitUniv : TermElab := elabAtom @[builtin_term_elab pipeProj] def elabPipeProj : TermElab - | `($e |>.$f $args*), expectedType? => + | `($e |>.%$tk$f $args*), expectedType? => universeConstraintsCheckpoint do let (namedArgs, args, ellipsis) ← expandArgs args - elabAppAux (← `($e |>.$f)) namedArgs args (ellipsis := ellipsis) expectedType? + let mut stx ← `($e |>.%$tk$f) + if let (some startPos, some stopPos) := (e.raw.getPos?, f.raw.getTailPos?) then + stx := ⟨stx.raw.setInfo <| .synthetic (canonical := true) startPos stopPos⟩ + elabAppAux stx namedArgs args (ellipsis := ellipsis) expectedType? | _, _ => throwUnsupportedSyntax @[builtin_term_elab explicit] def elabExplicit : TermElab := fun stx expectedType? => From b3cd3d247a7c2e32235994f5189c0a0fe1c697a9 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Mon, 9 Sep 2024 11:43:23 +0200 Subject: [PATCH 4/4] fix: don't use id completion for expected type dot --- src/Lean/Server/Completion.lean | 22 ++++++++++++++----- .../interactive/completionBracketedDot.lean | 10 +++++++++ .../completionBracketedDot.lean.expected.out | 3 +++ 3 files changed, 29 insertions(+), 6 deletions(-) create mode 100644 tests/lean/interactive/completionBracketedDot.lean create mode 100644 tests/lean/interactive/completionBracketedDot.lean.expected.out diff --git a/src/Lean/Server/Completion.lean b/src/Lean/Server/Completion.lean index 3ffd1c7816ab..d3324bac9c0c 100644 --- a/src/Lean/Server/Completion.lean +++ b/src/Lean/Server/Completion.lean @@ -323,11 +323,20 @@ def completeNamespaces (ctx : ContextInfo) (id : Name) (danglingDot : Bool) : M private def idCompletionCore (ctx : ContextInfo) + (stx : Syntax) (id : Name) (hoverInfo : HoverInfo) (danglingDot : Bool) : M Unit := do - let mut id := id.eraseMacroScopes + let mut id := id + if id.hasMacroScopes then + if stx.getHeadInfo matches .original .. then + id := id.eraseMacroScopes + else + -- Identifier is synthetic and has macro scopes => no completions + -- Erasing the macro scopes does not make sense in this case because the identifier name + -- is some random synthetic string. + return let mut danglingDot := danglingDot if let HoverInfo.inside delta := hoverInfo then id := truncate id delta @@ -417,12 +426,13 @@ private def idCompletion (params : CompletionParams) (ctx : ContextInfo) (lctx : LocalContext) + (stx : Syntax) (id : Name) (hoverInfo : HoverInfo) (danglingDot : Bool) : IO (Option CompletionList) := runM params ctx lctx do - idCompletionCore ctx id hoverInfo danglingDot + idCompletionCore ctx stx id hoverInfo danglingDot private def unfoldeDefinitionGuarded? (e : Expr) : MetaM (Option Expr) := try unfoldDefinition? e catch _ => pure none @@ -523,10 +533,10 @@ private def dotCompletion if nameSet.isEmpty then let stx := info.stx if stx.isIdent then - idCompletionCore ctx stx.getId hoverInfo (danglingDot := false) + idCompletionCore ctx stx stx.getId hoverInfo (danglingDot := false) else if stx.getKind == ``Lean.Parser.Term.completion && stx[0].isIdent then -- TODO: truncation when there is a dangling dot - idCompletionCore ctx stx[0].getId HoverInfo.after (danglingDot := true) + idCompletionCore ctx stx stx[0].getId HoverInfo.after (danglingDot := true) else failure return @@ -749,8 +759,8 @@ partial def find? match info with | .dot info .. => dotCompletion params ctx info hoverInfo - | .id _ id danglingDot lctx .. => - idCompletion params ctx lctx id hoverInfo danglingDot + | .id stx id danglingDot lctx .. => + idCompletion params ctx lctx stx id hoverInfo danglingDot | .dotId _ id lctx expectedType? => dotIdCompletion params ctx lctx id expectedType? | .fieldId _ id lctx structName => diff --git a/tests/lean/interactive/completionBracketedDot.lean b/tests/lean/interactive/completionBracketedDot.lean new file mode 100644 index 000000000000..bae0bd125307 --- /dev/null +++ b/tests/lean/interactive/completionBracketedDot.lean @@ -0,0 +1,10 @@ +inductive Direction where + | up + | right + | down + | left + +-- It would be nice if this actually provided `up`, `right`, `down` and `left` in the future +def foo : Direction := + (.) + --^ textDocument/completion diff --git a/tests/lean/interactive/completionBracketedDot.lean.expected.out b/tests/lean/interactive/completionBracketedDot.lean.expected.out new file mode 100644 index 000000000000..0ec8beed7c8f --- /dev/null +++ b/tests/lean/interactive/completionBracketedDot.lean.expected.out @@ -0,0 +1,3 @@ +{"textDocument": {"uri": "file:///completionBracketedDot.lean"}, + "position": {"line": 8, "character": 4}} +{"items": [], "isIncomplete": true}