b34379554d
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.
857 lines
32 KiB
Text
857 lines
32 KiB
Text
/-
|
||
Copyright (c) 2021 Microsoft Corporation. All rights reserved.
|
||
Released under Apache 2.0 license as described in the file LICENSE.
|
||
Authors: Leonardo de Moura
|
||
-/
|
||
prelude
|
||
import Lean.Environment
|
||
import Lean.Parser.Term
|
||
import Lean.Data.FuzzyMatching
|
||
import Lean.Data.Lsp.LanguageFeatures
|
||
import Lean.Data.Lsp.Capabilities
|
||
import Lean.Data.Lsp.Utf16
|
||
import Lean.Meta.CompletionName
|
||
import Lean.Meta.Tactic.Apply
|
||
import Lean.Meta.Match.MatcherInfo
|
||
import Lean.Server.InfoUtils
|
||
import Lean.Parser.Extension
|
||
import Lean.Server.FileSource
|
||
import Lean.Server.CompletionItemData
|
||
|
||
private partial def Lean.Server.Completion.consumeImplicitPrefix (e : Expr) (k : Expr → MetaM α) : MetaM α := do
|
||
match e with
|
||
| Expr.forallE n d b c =>
|
||
-- We do not consume instance implicit arguments because the user probably wants be aware of this dependency
|
||
if c == .implicit then
|
||
Meta.withLocalDecl n c d fun arg =>
|
||
consumeImplicitPrefix (b.instantiate1 arg) k
|
||
else
|
||
k e
|
||
| _ => k e
|
||
|
||
namespace Lean.Lsp
|
||
|
||
/--
|
||
Identifier that is sent from the server to the client as part of the `CompletionItem.data?` field.
|
||
Needed to resolve the `CompletionItem` when the client sends a `completionItem/resolve` request
|
||
for that item, again containing the `data?` field provided by the server.
|
||
-/
|
||
inductive CompletionIdentifier where
|
||
| const (declName : Name)
|
||
| fvar (id : FVarId)
|
||
deriving FromJson, ToJson
|
||
|
||
/--
|
||
`CompletionItemData` that also contains a `CompletionIdentifier`.
|
||
See the documentation of`CompletionItemData` and `CompletionIdentifier`.
|
||
-/
|
||
structure CompletionItemDataWithId extends CompletionItemData where
|
||
id? : Option CompletionIdentifier
|
||
deriving FromJson, ToJson
|
||
|
||
/--
|
||
Fills the `CompletionItem.detail?` field of `item` using the pretty-printed type identified by `id`.
|
||
-/
|
||
def CompletionItem.resolve
|
||
(item : CompletionItem)
|
||
(id : CompletionIdentifier)
|
||
: MetaM CompletionItem := do
|
||
let env ← getEnv
|
||
let lctx ← getLCtx
|
||
let mut item := item
|
||
|
||
if item.detail?.isNone then
|
||
let type? := match id with
|
||
| .const declName =>
|
||
env.find? declName |>.map ConstantInfo.type
|
||
| .fvar id =>
|
||
lctx.find? id |>.map LocalDecl.type
|
||
let detail? ← type?.mapM fun type =>
|
||
Lean.Server.Completion.consumeImplicitPrefix type fun typeWithoutImplicits =>
|
||
return toString (← Meta.ppExpr typeWithoutImplicits)
|
||
item := { item with detail? := detail? }
|
||
|
||
return item
|
||
|
||
end Lean.Lsp
|
||
|
||
namespace Lean.Server.Completion
|
||
open Lsp
|
||
open Elab
|
||
open Meta
|
||
open FuzzyMatching
|
||
|
||
abbrev EligibleHeaderDecls := Std.HashMap Name ConstantInfo
|
||
|
||
/-- Cached header declarations for which `allowCompletion headerEnv decl` is true. -/
|
||
builtin_initialize eligibleHeaderDeclsRef : IO.Ref (Option EligibleHeaderDecls) ←
|
||
IO.mkRef none
|
||
|
||
/--
|
||
Returns the declarations in the header for which `allowCompletion env decl` is true, caching them
|
||
if not already cached.
|
||
-/
|
||
def getEligibleHeaderDecls (env : Environment) : IO EligibleHeaderDecls := do
|
||
eligibleHeaderDeclsRef.modifyGet fun
|
||
| some eligibleHeaderDecls => (eligibleHeaderDecls, some eligibleHeaderDecls)
|
||
| none =>
|
||
let (_, eligibleHeaderDecls) :=
|
||
StateT.run (m := Id) (s := {}) do
|
||
-- `map₁` are the header decls
|
||
env.constants.map₁.forM fun declName c => do
|
||
modify fun eligibleHeaderDecls =>
|
||
if allowCompletion env declName then
|
||
eligibleHeaderDecls.insert declName c
|
||
else
|
||
eligibleHeaderDecls
|
||
(eligibleHeaderDecls, some eligibleHeaderDecls)
|
||
|
||
/-- Iterate over all declarations that are allowed in completion results. -/
|
||
private def forEligibleDeclsM [Monad m] [MonadEnv m] [MonadLiftT (ST IO.RealWorld) m]
|
||
[MonadLiftT IO m] (f : Name → ConstantInfo → m PUnit) : m PUnit := do
|
||
let env ← getEnv
|
||
(← getEligibleHeaderDecls env).forM f
|
||
-- map₂ are exactly the local decls
|
||
env.constants.map₂.forM fun name c => do
|
||
if allowCompletion env name then
|
||
f name c
|
||
|
||
/-- Checks whether this declaration can appear in completion results. -/
|
||
private def allowCompletion (eligibleHeaderDecls : EligibleHeaderDecls) (env : Environment)
|
||
(declName : Name) : Bool :=
|
||
eligibleHeaderDecls.contains declName ||
|
||
env.constants.map₂.contains declName && Lean.Meta.allowCompletion env declName
|
||
|
||
/--
|
||
Sorts `items` descendingly according to their score and ascendingly according to their label
|
||
for equal scores.
|
||
-/
|
||
private def sortCompletionItems (items : Array (CompletionItem × Float)) : Array CompletionItem :=
|
||
let items := items.qsort fun (i1, s1) (i2, s2) =>
|
||
if s1 != s2 then
|
||
s1 > s2
|
||
else
|
||
i1.label.map (·.toLower) < i2.label.map (·.toLower)
|
||
items.map (·.1)
|
||
|
||
/-- Intermediate state while completions are being computed. -/
|
||
structure State where
|
||
/-- All completion items and their fuzzy match scores so far. -/
|
||
items : Array (CompletionItem × Float) := #[]
|
||
|
||
/--
|
||
Monad used for completion computation that allows modifying a completion `State` and reading
|
||
`CompletionParams`.
|
||
-/
|
||
abbrev M := OptionT $ ReaderT CompletionParams $ StateRefT State MetaM
|
||
|
||
/-- Adds a new completion item to the state in `M`. -/
|
||
private def addItem
|
||
(item : CompletionItem)
|
||
(score : Float)
|
||
(id? : Option CompletionIdentifier := none)
|
||
: M Unit := do
|
||
let params ← read
|
||
let data := { params, id? : CompletionItemDataWithId }
|
||
let item := { item with data? := toJson data }
|
||
modify fun s => { s with items := s.items.push (item, score) }
|
||
|
||
/--
|
||
Adds a new completion item with the given `label`, `id`, `kind` and `score` to the state in `M`.
|
||
Computes the doc string from the environment if available.
|
||
-/
|
||
private def addUnresolvedCompletionItem
|
||
(label : Name)
|
||
(id : CompletionIdentifier)
|
||
(kind : CompletionItemKind)
|
||
(score : Float)
|
||
: M Unit := do
|
||
let doc? ← do
|
||
match id with
|
||
| .const declName =>
|
||
let docString? ← findDocString? (← getEnv) declName
|
||
pure <| docString?.map fun docString =>
|
||
{ value := docString, kind := MarkupKind.markdown : MarkupContent }
|
||
| .fvar _ => pure none
|
||
let item := { label := label.toString, kind? := kind, documentation? := doc? }
|
||
addItem item score id
|
||
|
||
private def getCompletionKindForDecl (constInfo : ConstantInfo) : M CompletionItemKind := do
|
||
let env ← getEnv
|
||
if constInfo.isCtor then
|
||
return CompletionItemKind.constructor
|
||
else if constInfo.isInductive then
|
||
if isClass env constInfo.name then
|
||
return CompletionItemKind.class
|
||
else if (← isEnumType constInfo.name) then
|
||
return CompletionItemKind.enum
|
||
else
|
||
return CompletionItemKind.struct
|
||
else if (← isProjectionFn constInfo.name) then
|
||
return CompletionItemKind.field
|
||
else if (← whnf constInfo.type).isForall then
|
||
return CompletionItemKind.function
|
||
else
|
||
return CompletionItemKind.constant
|
||
|
||
private def addUnresolvedCompletionItemForDecl (label : Name) (declName : Name) (score : Float) : M Unit := do
|
||
if let some c := (← getEnv).find? declName then
|
||
addUnresolvedCompletionItem label (.const declName) (← getCompletionKindForDecl c) score
|
||
|
||
private def addKeywordCompletionItem (keyword : String) (score : Float) : M Unit := do
|
||
let item := { label := keyword, detail? := "keyword", documentation? := none, kind? := CompletionItemKind.keyword }
|
||
addItem item score
|
||
|
||
private def addNamespaceCompletionItem (ns : Name) (score : Float) : M Unit := do
|
||
let item := { label := ns.toString, detail? := "namespace", documentation? := none, kind? := CompletionItemKind.module }
|
||
addItem item score
|
||
|
||
private def runM (params : CompletionParams) (ctx : ContextInfo) (lctx : LocalContext) (x : M Unit)
|
||
: IO (Option CompletionList) :=
|
||
ctx.runMetaM lctx do
|
||
match (← x.run |>.run params |>.run {}) with
|
||
| (none, _) => return none
|
||
| (some _, s) =>
|
||
return some { items := sortCompletionItems s.items, isIncomplete := true }
|
||
|
||
private def matchAtomic (id : Name) (declName : Name) : Option Float :=
|
||
match id, declName with
|
||
| .str .anonymous s₁, .str .anonymous s₂ => fuzzyMatchScoreWithThreshold? s₁ s₂
|
||
| _, _ => none
|
||
|
||
private def normPrivateName? (declName : Name) : MetaM (Option Name) := do
|
||
match privateToUserName? declName with
|
||
| none => return declName
|
||
| some userName =>
|
||
if mkPrivateName (← getEnv) userName == declName then
|
||
return userName
|
||
else
|
||
return none
|
||
|
||
/--
|
||
Return the auto-completion label if `id` can be auto completed using `declName` assuming namespace `ns` is open.
|
||
This function only succeeds with atomic labels. BTW, it seems most clients only use the last part.
|
||
|
||
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
|
||
let some declName ← normPrivateName? declName
|
||
| return none
|
||
if !ns.isPrefixOf declName then
|
||
return none
|
||
let declName := declName.replacePrefix ns Name.anonymous
|
||
if danglingDot then
|
||
-- If the input is `id.` and `declName` is of the form `id.atomic`, complete with `atomicName`
|
||
if id.isPrefixOf declName then
|
||
let declName := declName.replacePrefix id Name.anonymous
|
||
if declName.isAtomic && !declName.isAnonymous then
|
||
return some (declName, 1)
|
||
else if let (.str p₁ s₁, .str p₂ s₂) := (id, declName) then
|
||
if p₁ == p₂ then
|
||
-- If the namespaces agree, fuzzy-match on the trailing part
|
||
return fuzzyMatchScoreWithThreshold? s₁ s₂ |>.map (.mkSimple s₂, ·)
|
||
else if p₁.isAnonymous then
|
||
-- If `id` is namespace-less, also fuzzy-match declaration names in arbitrary namespaces
|
||
-- (but don't match the namespace itself).
|
||
-- Penalize score by component length of added namespace.
|
||
return fuzzyMatchScoreWithThreshold? s₁ s₂ |>.map (declName, · / (p₂.getNumParts + 1).toFloat)
|
||
return none
|
||
|
||
/--
|
||
Truncate the given identifier and make sure it has length `≤ newLength`.
|
||
This function assumes `id` does not contain `Name.num` constructors.
|
||
-/
|
||
private partial def truncate (id : Name) (newLen : Nat) : Name :=
|
||
let rec go (id : Name) : Name × Nat :=
|
||
match id with
|
||
| Name.anonymous => (id, 0)
|
||
| Name.num .. => unreachable!
|
||
| .str p s =>
|
||
let (p', len) := go p
|
||
if len + 1 >= newLen then
|
||
(p', len)
|
||
else
|
||
let optDot := if p.isAnonymous then 0 else 1
|
||
let len' := len + optDot + s.length
|
||
if len' ≤ newLen then
|
||
(id, len')
|
||
else
|
||
(Name.mkStr p (s.extract 0 ⟨newLen - optDot - len⟩), newLen)
|
||
(go id).1
|
||
|
||
inductive HoverInfo where
|
||
| after
|
||
| inside (delta : Nat)
|
||
|
||
def matchNamespace (ns : Name) (nsFragment : Name) (danglingDot : Bool) : Option Float :=
|
||
if danglingDot then
|
||
if nsFragment != ns && nsFragment.isPrefixOf ns then
|
||
some 1
|
||
else
|
||
none
|
||
else
|
||
match ns, nsFragment with
|
||
| .str p₁ s₁, .str p₂ s₂ =>
|
||
if p₁ == p₂ then fuzzyMatchScoreWithThreshold? s₂ s₁ else none
|
||
| _, _ => none
|
||
|
||
def completeNamespaces (ctx : ContextInfo) (id : Name) (danglingDot : Bool) : M Unit := do
|
||
let env ← getEnv
|
||
let add (ns : Name) (ns' : Name) (score : Float) : M Unit :=
|
||
if danglingDot then
|
||
addNamespaceCompletionItem (ns.replacePrefix (ns' ++ id) Name.anonymous) score
|
||
else
|
||
addNamespaceCompletionItem (ns.replacePrefix ns' Name.anonymous) score
|
||
env.getNamespaceSet |>.forM fun ns => do
|
||
unless ns.isInternal || env.contains ns do -- Ignore internal and namespaces that are also declaration names
|
||
for openDecl in ctx.openDecls do
|
||
match openDecl with
|
||
| OpenDecl.simple ns' _ =>
|
||
if let some score := matchNamespace ns (ns' ++ id) danglingDot then
|
||
add ns ns' score
|
||
return ()
|
||
| _ => pure ()
|
||
-- use current namespace
|
||
let rec visitNamespaces (ns' : Name) : M Unit := do
|
||
if let some score := matchNamespace ns (ns' ++ id) danglingDot then
|
||
add ns ns' score
|
||
else
|
||
match ns' with
|
||
| Name.str p .. => visitNamespaces p
|
||
| _ => return ()
|
||
visitNamespaces ctx.currNamespace
|
||
|
||
private def idCompletionCore
|
||
(ctx : ContextInfo)
|
||
(stx : Syntax)
|
||
(id : Name)
|
||
(hoverInfo : HoverInfo)
|
||
(danglingDot : Bool)
|
||
: M Unit := do
|
||
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
|
||
danglingDot := false
|
||
if id.isAtomic then
|
||
-- search for matches in the local context
|
||
for localDecl in (← getLCtx) do
|
||
if let some score := matchAtomic id localDecl.userName then
|
||
addUnresolvedCompletionItem localDecl.userName (.fvar localDecl.fvarId) (kind := CompletionItemKind.variable) score
|
||
-- search for matches in the environment
|
||
let env ← getEnv
|
||
forEligibleDeclsM fun declName c => do
|
||
let bestMatch? ← (·.2) <$> StateT.run (s := none) do
|
||
let matchUsingNamespace (ns : Name) : StateT (Option (Name × Float)) M Unit := do
|
||
let some (label, score) ← matchDecl? ns id danglingDot declName
|
||
| return
|
||
modify fun
|
||
| none =>
|
||
some (label, score)
|
||
| some (bestLabel, bestScore) =>
|
||
-- for open namespaces `A` and `A.B` and a decl `A.B.c`, pick the decl `c` over `B.c`
|
||
if label.isSuffixOf bestLabel then
|
||
some (label, score)
|
||
else
|
||
some (bestLabel, bestScore)
|
||
let rec visitNamespaces (ns : Name) : StateT (Option (Name × Float)) M Unit := do
|
||
let Name.str p .. := ns
|
||
| return ()
|
||
matchUsingNamespace ns
|
||
visitNamespaces p
|
||
-- use current namespace
|
||
visitNamespaces ctx.currNamespace
|
||
-- use open decls
|
||
for openDecl in ctx.openDecls do
|
||
let OpenDecl.simple ns exs := openDecl
|
||
| pure ()
|
||
if exs.contains declName then
|
||
continue
|
||
matchUsingNamespace ns
|
||
matchUsingNamespace Name.anonymous
|
||
if let some (bestLabel, bestScore) := bestMatch? then
|
||
addUnresolvedCompletionItem bestLabel (.const declName) (← getCompletionKindForDecl c) bestScore
|
||
-- Recall that aliases may not be atomic and include the namespace where they were created.
|
||
let matchAlias (ns : Name) (alias : Name) : Option Float :=
|
||
if ns.isPrefixOf alias then
|
||
matchAtomic id (alias.replacePrefix ns Name.anonymous)
|
||
else
|
||
none
|
||
let eligibleHeaderDecls ← getEligibleHeaderDecls env
|
||
-- Auxiliary function for `alias`
|
||
let addAlias (alias : Name) (declNames : List Name) (score : Float) : M Unit := do
|
||
declNames.forM fun declName => do
|
||
if allowCompletion eligibleHeaderDecls env declName then
|
||
addUnresolvedCompletionItemForDecl (.mkSimple alias.getString!) declName score
|
||
-- search explicitly open `ids`
|
||
for openDecl in ctx.openDecls do
|
||
match openDecl with
|
||
| OpenDecl.explicit openedId resolvedId =>
|
||
if allowCompletion eligibleHeaderDecls env resolvedId then
|
||
if let some score := matchAtomic id openedId then
|
||
addUnresolvedCompletionItemForDecl (.mkSimple openedId.getString!) resolvedId score
|
||
| OpenDecl.simple ns _ =>
|
||
getAliasState env |>.forM fun alias declNames => do
|
||
if let some score := matchAlias ns alias then
|
||
addAlias alias declNames score
|
||
-- search for aliases
|
||
getAliasState env |>.forM fun alias declNames => do
|
||
-- use current namespace
|
||
let rec searchAlias (ns : Name) : M Unit := do
|
||
if let some score := matchAlias ns alias then
|
||
addAlias alias declNames score
|
||
else
|
||
match ns with
|
||
| Name.str p .. => searchAlias p
|
||
| _ => return ()
|
||
searchAlias ctx.currNamespace
|
||
-- Search keywords
|
||
if let .str .anonymous s := id then
|
||
let keywords := Parser.getTokenTable env
|
||
for keyword in keywords.findPrefix s do
|
||
if let some score := fuzzyMatchScoreWithThreshold? s keyword then
|
||
addKeywordCompletionItem keyword score
|
||
-- Search namespaces
|
||
completeNamespaces ctx id danglingDot
|
||
|
||
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 stx id hoverInfo danglingDot
|
||
|
||
private def unfoldeDefinitionGuarded? (e : Expr) : MetaM (Option Expr) :=
|
||
try unfoldDefinition? e catch _ => pure none
|
||
|
||
/-- Return `true` if `e` is a `declName`-application, or can be unfolded (delta-reduced) to one. -/
|
||
private partial def isDefEqToAppOf (e : Expr) (declName : Name) : MetaM Bool := do
|
||
let isConstOf := match e.getAppFn with
|
||
| .const name .. => (privateToUserName? name).getD name == declName
|
||
| _ => false
|
||
if isConstOf then
|
||
return true
|
||
let some e ← unfoldeDefinitionGuarded? e | return false
|
||
isDefEqToAppOf e declName
|
||
|
||
private def isDotCompletionMethod (typeName : Name) (info : ConstantInfo) : MetaM Bool :=
|
||
forallTelescopeReducing info.type fun xs _ => do
|
||
for x in xs do
|
||
let localDecl ← x.fvarId!.getDecl
|
||
let type := localDecl.type.consumeMData
|
||
if (← isDefEqToAppOf type typeName) then
|
||
return true
|
||
return false
|
||
|
||
/--
|
||
Checks whether the expected type of `info.type` can be reduced to an application of `typeName`.
|
||
-/
|
||
private def isDotIdCompletionMethod (typeName : Name) (info : ConstantInfo) : MetaM Bool := do
|
||
forallTelescopeReducing info.type fun _ type =>
|
||
isDefEqToAppOf type.consumeMData typeName
|
||
|
||
/--
|
||
Converts `n` to `Name.anonymous` if `n` is a private prefix (see `Lean.isPrivatePrefix`).
|
||
-/
|
||
private def stripPrivatePrefix (n : Name) : Name :=
|
||
match n with
|
||
| .num _ 0 => if isPrivatePrefix n then .anonymous else n
|
||
| _ => n
|
||
|
||
/--
|
||
Compares `n₁` and `n₂` modulo private prefixes. Similar to `Name.cmp` but ignores all
|
||
private prefixes in both names.
|
||
Necessary because the namespaces of private names do not contain private prefixes.
|
||
-/
|
||
partial def cmpModPrivate (n₁ n₂ : Name) : Ordering :=
|
||
let n₁ := stripPrivatePrefix n₁
|
||
let n₂ := stripPrivatePrefix n₂
|
||
match n₁, n₂ with
|
||
| .anonymous, .anonymous => Ordering.eq
|
||
| .anonymous, _ => Ordering.lt
|
||
| _, .anonymous => Ordering.gt
|
||
| .num p₁ i₁, .num p₂ i₂ =>
|
||
match compare i₁ i₂ with
|
||
| Ordering.eq => cmpModPrivate p₁ p₂
|
||
| ord => ord
|
||
| .num _ _, .str _ _ => Ordering.lt
|
||
| .str _ _, .num _ _ => Ordering.gt
|
||
| .str p₁ n₁, .str p₂ n₂ =>
|
||
match compare n₁ n₂ with
|
||
| Ordering.eq => cmpModPrivate p₁ p₂
|
||
| ord => ord
|
||
|
||
/--
|
||
`NameSet` where names are compared according to `cmpModPrivate`.
|
||
Helps speed up dot completion because it allows us to look up names without first having to
|
||
strip the private prefix from deep in the name, letting us reject most names without
|
||
having to scan the full name first.
|
||
-/
|
||
def NameSetModPrivate := RBTree Name cmpModPrivate
|
||
|
||
/--
|
||
Given a type, try to extract relevant type names for dot notation field completion.
|
||
We extract the type name, parent struct names, and unfold the type.
|
||
The process mimics the dot notation elaboration procedure at `App.lean` -/
|
||
private partial def getDotCompletionTypeNames (type : Expr) : MetaM NameSetModPrivate :=
|
||
return (← visit type |>.run RBTree.empty).2
|
||
where
|
||
visit (type : Expr) : StateRefT NameSetModPrivate MetaM Unit := do
|
||
let .const typeName _ := type.getAppFn | return ()
|
||
modify fun s => s.insert typeName
|
||
if isStructure (← getEnv) typeName then
|
||
for parentName in getAllParentStructures (← getEnv) typeName do
|
||
modify fun s => s.insert parentName
|
||
let some type ← unfoldeDefinitionGuarded? type | return ()
|
||
visit type
|
||
|
||
private def dotCompletion
|
||
(params : CompletionParams)
|
||
(ctx : ContextInfo)
|
||
(info : TermInfo)
|
||
(hoverInfo : HoverInfo)
|
||
: IO (Option CompletionList) :=
|
||
runM params ctx info.lctx do
|
||
let nameSet ← try
|
||
getDotCompletionTypeNames (← instantiateMVars (← inferType info.expr))
|
||
catch _ =>
|
||
pure RBTree.empty
|
||
|
||
if nameSet.isEmpty then
|
||
let stx := info.stx
|
||
if stx.isIdent then
|
||
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 stx[0].getId HoverInfo.after (danglingDot := true)
|
||
else
|
||
failure
|
||
return
|
||
|
||
forEligibleDeclsM fun declName c => do
|
||
let unnormedTypeName := declName.getPrefix
|
||
if ! nameSet.contains unnormedTypeName then
|
||
return
|
||
let some declName ← normPrivateName? declName
|
||
| return
|
||
let typeName := declName.getPrefix
|
||
if ! (← isDotCompletionMethod typeName c) then
|
||
return
|
||
let completionKind ← getCompletionKindForDecl c
|
||
addUnresolvedCompletionItem (.mkSimple c.name.getString!) (.const c.name) (kind := completionKind) 1
|
||
|
||
private def dotIdCompletion
|
||
(params : CompletionParams)
|
||
(ctx : ContextInfo)
|
||
(lctx : LocalContext)
|
||
(id : Name)
|
||
(expectedType? : Option Expr)
|
||
: IO (Option CompletionList) :=
|
||
runM params ctx lctx do
|
||
let some expectedType := expectedType?
|
||
| return ()
|
||
|
||
let resultTypeFn := (← instantiateMVars expectedType).cleanupAnnotations.getAppFn.cleanupAnnotations
|
||
let .const .. := resultTypeFn
|
||
| return ()
|
||
|
||
let nameSet ← try
|
||
getDotCompletionTypeNames resultTypeFn
|
||
catch _ =>
|
||
pure RBTree.empty
|
||
|
||
forEligibleDeclsM fun declName c => do
|
||
let unnormedTypeName := declName.getPrefix
|
||
if ! nameSet.contains unnormedTypeName then
|
||
return
|
||
|
||
let some declName ← normPrivateName? declName
|
||
| return
|
||
|
||
let typeName := declName.getPrefix
|
||
if ! (← isDotIdCompletionMethod typeName c) then
|
||
return
|
||
|
||
let completionKind ← getCompletionKindForDecl c
|
||
if id.isAnonymous then
|
||
-- We're completing a lone dot => offer all decls of the type
|
||
addUnresolvedCompletionItem (.mkSimple c.name.getString!) (.const c.name) completionKind 1
|
||
return
|
||
|
||
let some (label, score) ← matchDecl? typeName id (danglingDot := false) declName | pure ()
|
||
addUnresolvedCompletionItem label (.const c.name) completionKind score
|
||
|
||
private def fieldIdCompletion
|
||
(params : CompletionParams)
|
||
(ctx : ContextInfo)
|
||
(lctx : LocalContext)
|
||
(id : Name)
|
||
(structName : Name)
|
||
: IO (Option CompletionList) :=
|
||
runM params ctx lctx do
|
||
let idStr := id.toString
|
||
let fieldNames := getStructureFieldsFlattened (← getEnv) structName (includeSubobjectFields := false)
|
||
for fieldName in fieldNames do
|
||
let .str _ fieldName := fieldName | continue
|
||
let some score := fuzzyMatchScoreWithThreshold? idStr fieldName | continue
|
||
let item := { label := fieldName, detail? := "field", documentation? := none, kind? := CompletionItemKind.field }
|
||
addItem item score
|
||
|
||
private def optionCompletion
|
||
(params : CompletionParams)
|
||
(ctx : ContextInfo)
|
||
(stx : Syntax)
|
||
(caps : ClientCapabilities)
|
||
: IO (Option CompletionList) :=
|
||
ctx.runMetaM {} do
|
||
let (partialName, trailingDot) :=
|
||
-- `stx` is from `"set_option" >> ident`
|
||
match stx[1].getSubstring? (withLeading := false) (withTrailing := false) with
|
||
| none => ("", false) -- the `ident` is `missing`, list all options
|
||
| some ss =>
|
||
if !ss.str.atEnd ss.stopPos && ss.str.get ss.stopPos == '.' then
|
||
-- include trailing dot, which is not parsed by `ident`
|
||
(ss.toString ++ ".", true)
|
||
else
|
||
(ss.toString, false)
|
||
-- HACK(WN): unfold the type so ForIn works
|
||
let (decls : RBMap _ _ _) ← getOptionDecls
|
||
let opts ← getOptions
|
||
let mut items := #[]
|
||
for ⟨name, decl⟩ in decls do
|
||
if let some score := fuzzyMatchScoreWithThreshold? partialName name.toString then
|
||
let textEdit :=
|
||
if !caps.textDocument?.any (·.completion?.any (·.completionItem?.any (·.insertReplaceSupport?.any (·)))) then
|
||
none -- InsertReplaceEdit not supported by client
|
||
else if let some ⟨start, stop⟩ := stx[1].getRange? then
|
||
let stop := if trailingDot then stop + ' ' else stop
|
||
let range := ⟨ctx.fileMap.utf8PosToLspPos start, ctx.fileMap.utf8PosToLspPos stop⟩
|
||
some { newText := name.toString, insert := range, replace := range : InsertReplaceEdit }
|
||
else
|
||
none
|
||
items := items.push
|
||
({ label := name.toString
|
||
detail? := s!"({opts.get name decl.defValue}), {decl.descr}"
|
||
documentation? := none,
|
||
kind? := CompletionItemKind.property -- TODO: investigate whether this is the best kind for options.
|
||
textEdit? := textEdit
|
||
data? := toJson { params, id? := none : CompletionItemDataWithId } }, score)
|
||
return some { items := sortCompletionItems items, isIncomplete := true }
|
||
|
||
private def tacticCompletion (params : CompletionParams) (ctx : ContextInfo) : IO (Option CompletionList) :=
|
||
-- Just return the list of tactics for now.
|
||
ctx.runMetaM {} do
|
||
let table := Parser.getCategory (Parser.parserExtension.getState (← getEnv)).categories `tactic |>.get!.tables.leadingTable
|
||
let items : Array (CompletionItem × Float) := table.fold (init := #[]) fun items tk _ =>
|
||
-- TODO pretty print tactic syntax
|
||
items.push ({
|
||
label := tk.toString
|
||
detail? := none
|
||
documentation? := none
|
||
kind? := CompletionItemKind.keyword
|
||
data? := toJson { params, id? := none : CompletionItemDataWithId }
|
||
}, 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)
|
||
(infoTree : InfoTree)
|
||
: Option (HoverInfo × ContextInfo × CompletionInfo) :=
|
||
let ⟨hoverLine, _⟩ := fileMap.toPosition hoverPos
|
||
match infoTree.foldInfo (init := none) (choose hoverLine) with
|
||
| some (hoverInfo, ctx, Info.ofCompletionInfo info) =>
|
||
some (hoverInfo, ctx, info)
|
||
| _ => 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)
|
||
(ctx : ContextInfo)
|
||
(info : Info)
|
||
(best? : Option (HoverInfo × ContextInfo × Info))
|
||
: Option (HoverInfo × ContextInfo × Info) :=
|
||
if !info.isCompletion then
|
||
best?
|
||
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, ctx, info)
|
||
| some (_, _, best) =>
|
||
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
|
||
does not set it.
|
||
-/
|
||
private def assignSortTexts (completions : CompletionList) : CompletionList := Id.run do
|
||
if completions.items.isEmpty then
|
||
return completions
|
||
let items := completions.items.mapIdx fun i item =>
|
||
{ item with sortText? := toString i.val }
|
||
let maxDigits := items[items.size - 1]!.sortText?.get!.length
|
||
let items := items.map fun item =>
|
||
let sortText := item.sortText?.get!
|
||
let pad := List.replicate (maxDigits - sortText.length) '0' |>.asString
|
||
{ item with sortText? := pad ++ sortText }
|
||
{ completions with items := items }
|
||
|
||
partial def find?
|
||
(params : CompletionParams)
|
||
(fileMap : FileMap)
|
||
(hoverPos : String.Pos)
|
||
(infoTree : InfoTree)
|
||
(caps : ClientCapabilities)
|
||
: IO (Option CompletionList) := do
|
||
let some (hoverInfo, ctx, info) := findCompletionInfoAt? fileMap hoverPos infoTree
|
||
| return none
|
||
let completionList? ←
|
||
match info with
|
||
| .dot info .. =>
|
||
dotCompletion params ctx info hoverInfo
|
||
| .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 =>
|
||
fieldIdCompletion params ctx lctx id structName
|
||
| .option stx =>
|
||
optionCompletion params ctx stx caps
|
||
| .tactic .. =>
|
||
tacticCompletion params ctx
|
||
| _ => return none
|
||
return completionList?.map assignSortTexts
|
||
|
||
/--
|
||
Fills the `CompletionItem.detail?` field of `item` using the pretty-printed type identified by `id`
|
||
in the context found at `hoverPos` in `infoTree`.
|
||
-/
|
||
def resolveCompletionItem?
|
||
(fileMap : FileMap)
|
||
(hoverPos : String.Pos)
|
||
(infoTree : InfoTree)
|
||
(item : CompletionItem)
|
||
(id : CompletionIdentifier)
|
||
: IO CompletionItem := do
|
||
let some (_, ctx, info) := findCompletionInfoAt? fileMap hoverPos infoTree
|
||
| return item
|
||
ctx.runMetaM info.lctx (item.resolve id)
|
||
|
||
end Lean.Server.Completion
|