From 417421dbae588234bfed736e6ee549572c1a44ba Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 9 Apr 2022 09:11:45 -0700 Subject: [PATCH] fix: auto completion when `autoBoundImplicit` is active --- src/Lean/Elab/Term.lean | 9 +++++++++ tests/lean/1018unknowMVarIssue.lean.expected.out | 5 +++++ tests/lean/infoTree.lean.expected.out | 4 ++++ tests/lean/interactive/compHeader.lean | 3 +++ tests/lean/interactive/compHeader.lean.expected.out | 6 ++++++ 5 files changed, 27 insertions(+) create mode 100644 tests/lean/interactive/compHeader.lean create mode 100644 tests/lean/interactive/compHeader.lean.expected.out diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index b191e3faf5..97b30a60aa 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -1491,6 +1491,15 @@ private def mkConsts (candidates : List (Name × List String)) (explicitLevels : def resolveName (stx : Syntax) (n : Name) (preresolved : List (Name × List String)) (explicitLevels : List Level) (expectedType? : Option Expr := none) : TermElabM (List (Expr × List String)) := do try if let some (e, projs) ← resolveLocalName n then + if (← read).autoBoundImplicit then + /- We used to generate completion info nodes only for names that could not be resolved. + However, this is very unsatisfactory for when elaborating headers when `autoBoundImplicit` is turned on. + The problem is that new local declarations are introduced by `autoBoundImplicit` and we eventually can always resolve the name. + Thus, we add the completion info in this case. + TODO: revisit this design decision. Alternative design: always create a completion info node. + Note that in the current design if a constant name is a prefix of another one, we will not have a completion info node. + -/ + addCompletionInfo <| CompletionInfo.id stx stx.getId (danglingDot := false) (← getLCtx) expectedType? unless explicitLevels.isEmpty do throwError "invalid use of explicit universe parameters, '{e}' is a local" return [(e, projs)] diff --git a/tests/lean/1018unknowMVarIssue.lean.expected.out b/tests/lean/1018unknowMVarIssue.lean.expected.out index df7a71dbaf..51ac69b5ee 100644 --- a/tests/lean/1018unknowMVarIssue.lean.expected.out +++ b/tests/lean/1018unknowMVarIssue.lean.expected.out @@ -7,20 +7,25 @@ a : α ⊢ α [Elab.info] command @ ⟨7, 0⟩-⟨10, 19⟩ @ Lean.Elab.Command.elabDeclaration α : Type @ ⟨7, 13⟩-⟨7, 14⟩ @ Lean.Elab.Term.elabIdent + [.] `α : some Sort.{?_uniq.313} @ ⟨7, 13⟩-⟨7, 14⟩ α : Type @ ⟨7, 13⟩-⟨7, 14⟩ a (isBinder := true) : α @ ⟨7, 9⟩-⟨7, 10⟩ α : Type @ ⟨7, 13⟩-⟨7, 14⟩ @ Lean.Elab.Term.elabIdent + [.] `α : some Sort.{?_uniq.319} @ ⟨7, 13⟩-⟨7, 14⟩ α : Type @ ⟨7, 13⟩-⟨7, 14⟩ a (isBinder := true) : α @ ⟨7, 9⟩-⟨7, 10⟩ Fam2 α β : Type 1 @ ⟨7, 21⟩-⟨7, 29⟩ @ Lean.Elab.Term.elabApp [.] `Fam2 : some Sort.{?_uniq.321} @ ⟨7, 21⟩-⟨7, 25⟩ Fam2 : Type → Type → Type 1 @ ⟨7, 21⟩-⟨7, 25⟩ α : Type @ ⟨7, 26⟩-⟨7, 27⟩ @ Lean.Elab.Term.elabIdent + [.] `α : some Type @ ⟨7, 26⟩-⟨7, 27⟩ α : Type @ ⟨7, 26⟩-⟨7, 27⟩ β : Type @ ⟨7, 28⟩-⟨7, 29⟩ @ Lean.Elab.Term.elabIdent + [.] `β : some Type @ ⟨7, 28⟩-⟨7, 29⟩ β : Type @ ⟨7, 28⟩-⟨7, 29⟩ x (isBinder := true) : Fam2 α β @ ⟨7, 17⟩-⟨7, 18⟩ β : Type @ ⟨7, 33⟩-⟨7, 34⟩ @ Lean.Elab.Term.elabIdent + [.] `β : some Sort.{?_uniq.323} @ ⟨7, 33⟩-⟨7, 34⟩ β : Type @ ⟨7, 33⟩-⟨7, 34⟩ _example (isBinder := true) : {α β : Type} → α → Fam2 α β → β @ ⟨7, 0⟩†-⟨10, 19⟩† a (isBinder := true) : α @ ⟨7, 9⟩-⟨7, 10⟩ diff --git a/tests/lean/infoTree.lean.expected.out b/tests/lean/infoTree.lean.expected.out index 51ca11ded8..7dff77f2a9 100644 --- a/tests/lean/infoTree.lean.expected.out +++ b/tests/lean/infoTree.lean.expected.out @@ -67,9 +67,11 @@ binop% HAdd.hAdd✝ x 0 x + 0 : Nat @ ⟨17, 35⟩†-⟨17, 40⟩ @ Lean.Elab.Term.BinOp.elabBinOp x : Nat @ ⟨17, 35⟩-⟨17, 36⟩ @ Lean.Elab.Term.elabIdent + [.] `x : none @ ⟨17, 35⟩-⟨17, 36⟩ x : Nat @ ⟨17, 35⟩-⟨17, 36⟩ 0 : Nat @ ⟨17, 39⟩-⟨17, 40⟩ @ Lean.Elab.Term.elabNumLit x : Nat @ ⟨17, 43⟩-⟨17, 44⟩ @ Lean.Elab.Term.elabIdent + [.] `x : none @ ⟨17, 43⟩-⟨17, 44⟩ x : Nat @ ⟨17, 43⟩-⟨17, 44⟩ h (isBinder := true) : ∀ (x y : Nat), Bool → x + 0 = x @ ⟨17, 4⟩-⟨17, 5⟩ fun x y b => @@ -368,8 +370,10 @@ infoTree.lean:44:0: error: expected stx (Term.binrel "binrel%" `Eq._@.infoTree._hyg.179 `x `x) Eq.{1} Nat _uniq.892 _uniq.892 : Prop @ ⟨45, 21⟩†-⟨45, 26⟩ @ Lean.Elab.Term.elabBinRel _uniq.892 : Nat @ ⟨45, 21⟩-⟨45, 22⟩ @ Lean.Elab.Term.elabIdent + [.] `x : none @ ⟨45, 21⟩-⟨45, 22⟩ _uniq.892 : Nat @ ⟨45, 21⟩-⟨45, 22⟩ _uniq.892 : Nat @ ⟨45, 25⟩-⟨45, 26⟩ @ Lean.Elab.Term.elabIdent + [.] `x : none @ ⟨45, 25⟩-⟨45, 26⟩ _uniq.892 : Nat @ ⟨45, 25⟩-⟨45, 26⟩ _uniq.898 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨45, 4⟩-⟨45, 6⟩ _uniq.901 (isBinder := true) : Nat @ ⟨45, 8⟩-⟨45, 9⟩ diff --git a/tests/lean/interactive/compHeader.lean b/tests/lean/interactive/compHeader.lean new file mode 100644 index 0000000000..4a0cb1bbd9 --- /dev/null +++ b/tests/lean/interactive/compHeader.lean @@ -0,0 +1,3 @@ +def veryLongNameForCompletion := Nat + --v textDocument/completion +def f (x : veryLongNam) := x diff --git a/tests/lean/interactive/compHeader.lean.expected.out b/tests/lean/interactive/compHeader.lean.expected.out new file mode 100644 index 0000000000..3be618a0fc --- /dev/null +++ b/tests/lean/interactive/compHeader.lean.expected.out @@ -0,0 +1,6 @@ +{"textDocument": {"uri": "file://compHeader.lean"}, + "position": {"line": 2, "character": 22}} +{"items": + [{"label": "veryLongNam", "kind": 6, "detail": "Sort u_1"}, + {"label": "veryLongNameForCompletion", "kind": 21, "detail": "Type"}], + "isIncomplete": true}