diff --git a/src/Lean/Server/Completion.lean b/src/Lean/Server/Completion.lean index d7cba3b320..3bafabee56 100644 --- a/src/Lean/Server/Completion.lean +++ b/src/Lean/Server/Completion.lean @@ -5,6 +5,7 @@ Authors: Leonardo de Moura -/ 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 @@ -17,6 +18,7 @@ namespace Lean.Server.Completion open Lsp open Elab open Meta +open FuzzyMatching builtin_initialize completionBlackListExt : TagDeclarationExtension ← mkTagDeclarationExtension `blackListCompletion @@ -61,8 +63,9 @@ private def isTypeApplicable (type : Expr) (expectedType? : Option Expr) : MetaM catch _ => return false -private def sortCompletionItems (items : Array CompletionItem) : Array CompletionItem := - items.qsort fun i1 i2 => i1.label < i2.label +private def sortCompletionItems (items : Array (CompletionItem × Float)) : Array CompletionItem := + -- TODO fix float eq comparison + items.qsort (fun (i1, s1) (i2, s2) => if s1 == s2 then i1.label < i2.label else s1 > s2) |>.map (·.1) private def mkCompletionItem (label : Name) (type : Expr) (docString? : Option String) (kind : CompletionItemKind) : MetaM CompletionItem := do let doc? := docString?.map fun docString => { value := docString, kind := MarkupKind.markdown : MarkupContent } @@ -70,18 +73,18 @@ private def mkCompletionItem (label : Name) (type : Expr) (docString? : Option S return { label := label.getString!, detail? := detail, documentation? := doc?, kind? := kind } structure State where - itemsMain : Array CompletionItem := #[] - itemsOther : Array CompletionItem := #[] + itemsMain : Array (CompletionItem × Float) := #[] + itemsOther : Array (CompletionItem × Float) := #[] abbrev M := OptionT $ StateRefT State MetaM -private def addCompletionItem (label : Name) (type : Expr) (expectedType? : Option Expr) (declName? : Option Name) (kind : CompletionItemKind) : M Unit := do +private def addCompletionItem (label : Name) (type : Expr) (expectedType? : Option Expr) (declName? : Option Name) (kind : CompletionItemKind) (score : Float) : M Unit := do let docString? ← if let some declName := declName? then findDocString? (← getEnv) declName else pure none let item ← mkCompletionItem label type docString? kind if (← isTypeApplicable type expectedType?) then - modify fun s => { s with itemsMain := s.itemsMain.push item } + modify fun s => { s with itemsMain := s.itemsMain.push (item, score) } else - modify fun s => { s with itemsOther := s.itemsOther.push item } + modify fun s => { s with itemsOther := s.itemsOther.push (item, score) } private def getCompletionKindForDecl (constInfo : ConstantInfo) : M CompletionItemKind := do let env ← getEnv @@ -101,17 +104,17 @@ private def getCompletionKindForDecl (constInfo : ConstantInfo) : M CompletionIt else return CompletionItemKind.constant -private def addCompletionItemForDecl (label : Name) (declName : Name) (expectedType? : Option Expr) : M Unit := do +private def addCompletionItemForDecl (label : Name) (declName : Name) (expectedType? : Option Expr) (score : Float) : M Unit := do if let some c := (← getEnv).find? declName then - addCompletionItem label c.type expectedType? (some declName) (← getCompletionKindForDecl c) + addCompletionItem label c.type expectedType? (some declName) (← getCompletionKindForDecl c) score private def addKeywordCompletionItem (keyword : String) : M Unit := do let item := { label := keyword, detail? := "keyword", documentation? := none, kind? := CompletionItemKind.keyword } - modify fun s => { s with itemsMain := s.itemsMain.push item } + modify fun s => { s with itemsMain := s.itemsMain.push (item, 1) } -private def addNamespaceCompletionItem (ns : Name) : M Unit := do +private def addNamespaceCompletionItem (ns : Name) (score : Float) : M Unit := do let item := { label := ns.toString, detail? := "namespace", documentation? := none, kind? := CompletionItemKind.module } - modify fun s => { s with itemsMain := s.itemsMain.push item } + modify fun s => { s with itemsMain := s.itemsMain.push (item, score) } private def runM (ctx : ContextInfo) (lctx : LocalContext) (x : M Unit) : IO (Option CompletionList) := ctx.runMetaM lctx do @@ -120,10 +123,10 @@ private def runM (ctx : ContextInfo) (lctx : LocalContext) (x : M Unit) : IO (Op | (some _, s) => return some { items := sortCompletionItems s.itemsMain ++ sortCompletionItems s.itemsOther, isIncomplete := true } -private def matchAtomic (id : Name) (declName : Name) : Bool := +private def matchAtomic (id : Name) (declName : Name) : Option Float := match id, declName with - | Name.str Name.anonymous s₁ _, Name.str Name.anonymous s₂ _ => s₁.isPrefixOf s₂ - | _, _ => false + | Name.str Name.anonymous s₁ _, Name.str Name.anonymous s₂ _ => fuzzyMatchScoreWithThreshold? s₁ s₂ + | _, _ => none private def normPrivateName (declName : Name) : MetaM Name := do match privateToUserName? declName with @@ -140,7 +143,7 @@ private def normPrivateName (declName : Name) : MetaM 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) := do +private def matchDecl? (ns : Name) (id : Name) (danglingDot : Bool) (declName : Name) : MetaM (Option (Name × Float)) := do -- dbg_trace "{ns}, {id}, {declName}, {danglingDot}" let declName ← normPrivateName declName if !ns.isPrefixOf declName then @@ -150,14 +153,14 @@ private def matchDecl? (ns : Name) (id : Name) (danglingDot : Bool) (declName : if id.isPrefixOf declName && danglingDot then let declName := declName.replacePrefix id Name.anonymous if declName.isAtomic && !declName.isAnonymous then - return some declName + return some (declName, 1) else return none else if !danglingDot then match id, declName with | Name.str p₁ s₁ _, Name.str p₂ s₂ _ => - if p₁ == p₂ && s₁.isPrefixOf s₂ then - return some s₂ + if p₁ == p₂ then + return fuzzyMatchScoreWithThreshold? s₁ s₂ |>.map (s₂, ·) else return none | _, _ => return none @@ -190,34 +193,38 @@ inductive HoverInfo where | after | inside (delta : Nat) -def matchNamespace (ns : Name) (nsFragment : Name) (danglingDot : Bool) : Bool := +def matchNamespace (ns : Name) (nsFragment : Name) (danglingDot : Bool) : Option Float := if danglingDot then - nsFragment != ns && nsFragment.isPrefixOf ns + if nsFragment != ns && nsFragment.isPrefixOf ns then + some 1 + else + none else match ns, nsFragment with - | Name.str p₁ s₁ _, Name.str p₂ s₂ _ => p₁ == p₂ && s₂.isPrefixOf s₁ - | _, _ => false + | Name.str p₁ s₁ _, Name.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) : M Unit := + let add (ns : Name) (ns' : Name) (score : Float) : M Unit := if danglingDot then - addNamespaceCompletionItem (ns.replacePrefix (ns' ++ id) Name.anonymous) + addNamespaceCompletionItem (ns.replacePrefix (ns' ++ id) Name.anonymous) score else - addNamespaceCompletionItem (ns.replacePrefix ns' Name.anonymous) + 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' except => - if matchNamespace ns (ns' ++ id) danglingDot then - add ns 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 matchNamespace ns (ns' ++ id) danglingDot then - add ns ns' + if let some score := matchNamespace ns (ns' ++ id) danglingDot then + add ns ns' score else match ns' with | Name.str p .. => visitNamespaces p @@ -234,16 +241,16 @@ private def idCompletionCore (ctx : ContextInfo) (id : Name) (hoverInfo : HoverI if id.isAtomic then -- search for matches in the local context for localDecl in (← getLCtx) do - if matchAtomic id localDecl.userName then - addCompletionItem localDecl.userName localDecl.type expectedType? none (kind := CompletionItemKind.variable) + if let some score := matchAtomic id localDecl.userName then + addCompletionItem localDecl.userName localDecl.type expectedType? none (kind := CompletionItemKind.variable) score -- search for matches in the environment let env ← getEnv env.constants.forM fun declName c => do unless (← isBlackListed declName) do let matchUsingNamespace (ns : Name): M Bool := do - if let some label ← matchDecl? ns id danglingDot declName then + if let some (label, score) ← matchDecl? ns id danglingDot declName then -- dbg_trace "matched with {id}, {declName}, {label}" - addCompletionItem label c.type expectedType? declName (← getCompletionKindForDecl c) + addCompletionItem label c.type expectedType? declName (← getCompletionKindForDecl c) score return true else return false @@ -265,30 +272,33 @@ private def idCompletionCore (ctx : ContextInfo) (id : Name) (hoverInfo : HoverI return () | _ => pure () -- Recall that aliases may not be atomic and include the namespace where they were created. - let matchAlias (ns : Name) (alias : Name) : Bool := - ns.isPrefixOf alias && matchAtomic id (alias.replacePrefix ns Name.anonymous) + let matchAlias (ns : Name) (alias : Name) : Option Float := + if ns.isPrefixOf alias then + matchAtomic id (alias.replacePrefix ns Name.anonymous) + else + none -- Auxiliary function for `alias` - let addAlias (alias : Name) (declNames : List Name) : M Unit := do + let addAlias (alias : Name) (declNames : List Name) (score : Float) : M Unit := do declNames.forM fun declName => do unless (← isBlackListed declName) do - addCompletionItemForDecl alias declName expectedType? + addCompletionItemForDecl alias declName expectedType? score -- search explicitily open `ids` for openDecl in ctx.openDecls do match openDecl with | OpenDecl.explicit openedId resolvedId => unless (← isBlackListed resolvedId) do - if matchAtomic id openedId then - addCompletionItemForDecl openedId resolvedId expectedType? + if let some score := matchAtomic id openedId then + addCompletionItemForDecl openedId resolvedId expectedType? score | OpenDecl.simple ns except => getAliasState env |>.forM fun alias declNames => do - if matchAlias ns alias then - addAlias alias declNames + 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 matchAlias ns alias then - addAlias alias declNames + if let some score := matchAlias ns alias then + addAlias alias declNames score else match ns with | Name.str p .. => searchAlias p @@ -356,7 +366,7 @@ private def dotCompletion (ctx : ContextInfo) (info : TermInfo) (hoverInfo : Hov if nameSet.contains typeName then unless (← isBlackListed c.name) do if (← isDotCompletionMethod typeName c) then - addCompletionItem c.name.getString! c.type expectedType? c.name (kind := (← getCompletionKindForDecl c)) + addCompletionItem c.name.getString! c.type expectedType? c.name (kind := (← getCompletionKindForDecl c)) 1 private def optionCompletion (ctx : ContextInfo) (stx : Syntax) (caps : ClientCapabilities) : IO (Option CompletionList) := ctx.runMetaM {} do @@ -375,7 +385,7 @@ private def optionCompletion (ctx : ContextInfo) (stx : Syntax) (caps : ClientCa let opts ← getOptions let mut items := #[] for ⟨name, decl⟩ in decls do - if partialName.isPrefixOf name.toString then + 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 @@ -386,20 +396,20 @@ private def optionCompletion (ctx : ContextInfo) (stx : Syntax) (caps : ClientCa 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 } + ({ 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 }, score) return some { items := sortCompletionItems items, isIncomplete := true } private def tacticCompletion (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 := table.fold (init := #[]) fun items tk parser => + let items : Array (CompletionItem × Float) := table.fold (init := #[]) fun items tk parser => -- TODO pretty print tactic syntax - items.push { label := tk.toString, detail? := none, documentation? := none, kind? := CompletionItemKind.keyword } + items.push ({ label := tk.toString, detail? := none, documentation? := none, kind? := CompletionItemKind.keyword }, 1) return some { items := sortCompletionItems items, isIncomplete := true } partial def find? (fileMap : FileMap) (hoverPos : String.Pos) (infoTree : InfoTree) (caps : ClientCapabilities) : IO (Option CompletionList) := do diff --git a/tests/lean/interactive/533.lean.expected.out b/tests/lean/interactive/533.lean.expected.out index b12c3b5100..12af05069f 100644 --- a/tests/lean/interactive/533.lean.expected.out +++ b/tests/lean/interactive/533.lean.expected.out @@ -23,5 +23,95 @@ {"label": "Function", "kind": 9, "detail": "namespace"}, {"label": "Functor", "kind": 7, - "detail": "(Type u → Type v) → Type (max (u + 1) v)"}], + "detail": "(Type u → Type v) → Type (max (u + 1) v)"}, + {"label": "fix", + "kind": 3, + "detail": "[inst : Inhabited β] → ((α → β) → α → β) → α → β"}, + {"label": "fix1", + "kind": 3, + "detail": "[inst : Inhabited β] → ((α → β) → α → β) → α → β"}, + {"label": "fix2", + "kind": 3, + "detail": + "[inst : Inhabited β] → ((α₁ → α₂ → β) → α₁ → α₂ → β) → α₁ → α₂ → β"}, + {"label": "fix3", + "kind": 3, + "detail": + "[inst : Inhabited β] → ((α₁ → α₂ → α₃ → β) → α₁ → α₂ → α₃ → β) → α₁ → α₂ → α₃ → β"}, + {"label": "fix4", + "kind": 3, + "detail": + "[inst : Inhabited β] → ((α₁ → α₂ → α₃ → α₄ → β) → α₁ → α₂ → α₃ → α₄ → β) → α₁ → α₂ → α₃ → α₄ → β"}, + {"label": "fix5", + "kind": 3, + "detail": + "[inst : Inhabited β] → ((α₁ → α₂ → α₃ → α₄ → α₅ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → β"}, + {"label": "fix6", + "kind": 3, + "detail": + "[inst : Inhabited β] →\n ((α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β"}, + {"label": "fixCore", + "kind": 3, + "detail": "(α → β) → ((α → β) → α → β) → α → β"}, + {"label": "fixCore1", + "kind": 3, + "detail": "(α → β) → ((α → β) → α → β) → α → β"}, + {"label": "fixCore2", + "kind": 3, + "detail": "(α₁ → α₂ → β) → ((α₁ → α₂ → β) → α₁ → α₂ → β) → α₁ → α₂ → β"}, + {"label": "fixCore3", + "kind": 3, + "detail": + "(α₁ → α₂ → α₃ → β) → ((α₁ → α₂ → α₃ → β) → α₁ → α₂ → α₃ → β) → α₁ → α₂ → α₃ → β"}, + {"label": "fixCore4", + "kind": 3, + "detail": + "(α₁ → α₂ → α₃ → α₄ → β) → ((α₁ → α₂ → α₃ → α₄ → β) → α₁ → α₂ → α₃ → α₄ → β) → α₁ → α₂ → α₃ → α₄ → β"}, + {"label": "fixCore5", + "kind": 3, + "detail": + "(α₁ → α₂ → α₃ → α₄ → α₅ → β) → ((α₁ → α₂ → α₃ → α₄ → α₅ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → β"}, + {"label": "fixCore6", + "kind": 3, + "detail": + "(α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) →\n ((α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β"}, + {"label": "failure", + "kind": 5, + "detail": "[self : Alternative f] → {α : Type u} → f α"}, + {"label": "false", "kind": 4, "detail": "Bool"}, + {"label": "false_and", + "kind": 3, + "detail": "∀ (p : Prop), (False ∧ p) = False"}, + {"label": "false_iff", "kind": 3, "detail": "∀ (p : Prop), (False ↔ p) = ¬p"}, + {"label": "false_implies", + "kind": 3, + "detail": "∀ (p : Prop), (False → p) = True"}, + {"label": "false_of_ne", "kind": 3, "detail": "a ≠ a → False"}, + {"label": "false_or", "kind": 3, "detail": "∀ (p : Prop), (False ∨ p) = p"}, + {"label": "flip", "kind": 3, "detail": "(α → β → φ) → β → α → φ"}, + {"label": "floatDecLe", + "kind": 3, + "detail": "(a b : Float) → Decidable (a ≤ b)"}, + {"label": "floatDecLt", + "kind": 3, + "detail": "(a b : Float) → Decidable (a < b)"}, + {"label": "floatSpec", "kind": 21, "detail": "FloatSpec"}, + {"label": "forIn", + "kind": 5, + "detail": + "[self : ForIn m ρ α] → {β : Type u₁} → [inst : Monad m] → ρ → β → (α → β → m (ForInStep β)) → m β"}, + {"label": "forIn'", + "kind": 5, + "detail": + "[self : ForIn' m ρ α d] → {β : Type u₁} → [inst : Monad m] → (x : ρ) → β → ((a : α) → a ∈ x → β → m (ForInStep β)) → m β"}, + {"label": "forM", + "kind": 5, + "detail": + "[self : ForM m γ α] → [inst : Monad m] → γ → (α → m PUnit) → m PUnit"}, + {"label": "forall_congr", + "kind": 3, + "detail": "(∀ (a : α), p a = q a) → (∀ (a : α), p a) = ∀ (a : α), q a"}, + {"label": "funext", + "kind": 3, + "detail": "(∀ (x : α), f₁ x = f₂ x) → f₁ = f₂"}], "isIncomplete": true} diff --git a/tests/lean/interactive/863.lean.expected.out b/tests/lean/interactive/863.lean.expected.out index e9c3090bdf..f084a6edeb 100644 --- a/tests/lean/interactive/863.lean.expected.out +++ b/tests/lean/interactive/863.lean.expected.out @@ -21,7 +21,11 @@ "detail": "Environment → Name → Option Name"}, {"label": "getRevAliases", "kind": 3, - "detail": "Environment → Name → List Name"}], + "detail": "Environment → Name → List Name"}, + {"label": "getConstInfoRec", + "kind": 3, + "detail": + "[inst : Monad m] → [inst : MonadEnv m] → [inst : MonadError m] → Name → m RecursorVal"}], "isIncomplete": true} {"textDocument": {"uri": "file://863.lean"}, "position": {"line": 7, "character": 12}} @@ -46,5 +50,9 @@ "detail": "Environment → Name → Option Name"}, {"label": "getRevAliases", "kind": 3, - "detail": "Environment → Name → List Name"}], + "detail": "Environment → Name → List Name"}, + {"label": "getConstInfoRec", + "kind": 3, + "detail": + "[inst : Monad m] → [inst : MonadEnv m] → [inst : MonadError m] → Name → m RecursorVal"}], "isIncomplete": true} diff --git a/tests/lean/interactive/completion7.lean.expected.out b/tests/lean/interactive/completion7.lean.expected.out index 25f83ae60a..188f4363d6 100644 --- a/tests/lean/interactive/completion7.lean.expected.out +++ b/tests/lean/interactive/completion7.lean.expected.out @@ -3,7 +3,51 @@ {"items": [{"label": "And", "kind": 22, "detail": "Prop → Prop → Prop"}, {"label": "AndOp", "kind": 7, "detail": "Type u → Type u"}, - {"label": "AndThen", "kind": 7, "detail": "Type u → Type u"}], + {"label": "AndThen", "kind": 7, "detail": "Type u → Type u"}, + {"label": "and", "kind": 3, "detail": "Bool → Bool → Bool"}, + {"label": "andM", + "kind": 3, + "detail": "[inst : Monad m] → [inst : ToBool β] → m β → m β → m β"}, + {"label": "and_false", + "kind": 3, + "detail": "∀ (p : Prop), (p ∧ False) = False"}, + {"label": "and_self", "kind": 3, "detail": "∀ (p : Prop), (p ∧ p) = p"}, + {"label": "and_true", "kind": 3, "detail": "∀ (p : Prop), (p ∧ True) = p"}, + {"label": "Append", "kind": 7, "detail": "Type u → Type u"}, + {"label": "HAnd", + "kind": 7, + "detail": "Type u → Type v → outParam (Type w) → Type (max (max u v) w)"}, + {"label": "HAndThen", + "kind": 7, + "detail": "Type u → Type v → outParam (Type w) → Type (max (max u v) w)"}, + {"label": "false_and", + "kind": 3, + "detail": "∀ (p : Prop), (False ∧ p) = False"}, + {"label": "instAndOpUInt16", "kind": 21, "detail": "AndOp UInt16"}, + {"label": "instAndOpUInt32", "kind": 21, "detail": "AndOp UInt32"}, + {"label": "instAndOpUInt64", "kind": 21, "detail": "AndOp UInt64"}, + {"label": "instAndOpUInt8", "kind": 21, "detail": "AndOp UInt8"}, + {"label": "instAndOpUSize", "kind": 21, "detail": "AndOp USize"}, + {"label": "strictAnd", "kind": 3, "detail": "Bool → Bool → Bool"}, + {"label": "true_and", "kind": 3, "detail": "∀ (p : Prop), (True ∧ p) = p"}, + {"label": "instDecidableAnd", + "kind": 3, + "detail": "[dp : Decidable p] → [dq : Decidable q] → Decidable (p ∧ q)"}, + {"label": "instHAnd", "kind": 3, "detail": "[inst : AndOp α] → HAnd α α α"}, + {"label": "instHAndThen", + "kind": 3, + "detail": "[inst : AndThen α] → HAndThen α α α"}, + {"label": "compareOfLessAndEq", + "kind": 3, + "detail": + "(x y : α) → [inst : LT α] → [inst : Decidable (x < y)] → [inst : DecidableEq α] → Ordering"}, + {"label": "iff_iff_implies_and_implies", + "kind": 3, + "detail": "∀ (a b : Prop), (a ↔ b) ↔ (a → b) ∧ (b → a)"}, + {"label": "HAppend", + "kind": 7, + "detail": "Type u → Type v → outParam (Type w) → Type (max (max u v) w)"}, + {"label": "instAppendSubarray", "kind": 3, "detail": "Append (Subarray α)"}], "isIncomplete": true} {"textDocument": {"uri": "file://completion7.lean"}, "position": {"line": 2, "character": 11}} diff --git a/tests/lean/interactive/completionOption.lean.expected.out b/tests/lean/interactive/completionOption.lean.expected.out index 8924ec00df..409061b031 100644 --- a/tests/lean/interactive/completionOption.lean.expected.out +++ b/tests/lean/interactive/completionOption.lean.expected.out @@ -70,7 +70,19 @@ "end": {"line": 4, "character": 17}}}, "label": "format.width", "kind": 10, - "detail": "(120), indentation"}], + "detail": "(120), indentation"}, + {"textEdit": + {"replace": + {"start": {"line": 4, "character": 11}, + "end": {"line": 4, "character": 17}}, + "newText": "trace.PrettyPrinter.format", + "insert": + {"start": {"line": 4, "character": 11}, + "end": {"line": 4, "character": 17}}}, + "label": "trace.PrettyPrinter.format", + "kind": 10, + "detail": + "(false), enable/disable tracing for the given module and submodules"}], "isIncomplete": true} {"textDocument": {"uri": "file://completionOption.lean"}, "position": {"line": 7, "character": 20}} @@ -91,6 +103,54 @@ "position": {"line": 10, "character": 18}} {"items": [{"textEdit": + {"replace": + {"start": {"line": 10, "character": 11}, + "end": {"line": 10, "character": 18}}, + "newText": "trace.PrettyPrinter", + "insert": + {"start": {"line": 10, "character": 11}, + "end": {"line": 10, "character": 18}}}, + "label": "trace.PrettyPrinter", + "kind": 10, + "detail": + "(false), enable/disable tracing for the given module and submodules"}, + {"textEdit": + {"replace": + {"start": {"line": 10, "character": 11}, + "end": {"line": 10, "character": 18}}, + "newText": "trace.PrettyPrinter.delab", + "insert": + {"start": {"line": 10, "character": 11}, + "end": {"line": 10, "character": 18}}}, + "label": "trace.PrettyPrinter.delab", + "kind": 10, + "detail": + "(false), enable/disable tracing for the given module and submodules"}, + {"textEdit": + {"replace": + {"start": {"line": 10, "character": 11}, + "end": {"line": 10, "character": 18}}, + "newText": "trace.PrettyPrinter.format", + "insert": + {"start": {"line": 10, "character": 11}, + "end": {"line": 10, "character": 18}}}, + "label": "trace.PrettyPrinter.format", + "kind": 10, + "detail": + "(false), enable/disable tracing for the given module and submodules"}, + {"textEdit": + {"replace": + {"start": {"line": 10, "character": 11}, + "end": {"line": 10, "character": 18}}, + "newText": "trace.PrettyPrinter.parenthesize", + "insert": + {"start": {"line": 10, "character": 11}, + "end": {"line": 10, "character": 18}}}, + "label": "trace.PrettyPrinter.parenthesize", + "kind": 10, + "detail": + "(false), enable/disable tracing for the given module and submodules"}, + {"textEdit": {"replace": {"start": {"line": 10, "character": 11}, "end": {"line": 10, "character": 18}}, @@ -137,6 +197,90 @@ "label": "trace.pp.analyze.tryUnify", "kind": 10, "detail": + "(false), enable/disable tracing for the given module and submodules"}, + {"textEdit": + {"replace": + {"start": {"line": 10, "character": 11}, + "end": {"line": 10, "character": 18}}, + "newText": "trace.Elab.postpone", + "insert": + {"start": {"line": 10, "character": 11}, + "end": {"line": 10, "character": 18}}}, + "label": "trace.Elab.postpone", + "kind": 10, + "detail": + "(false), enable/disable tracing for the given module and submodules"}, + {"textEdit": + {"replace": + {"start": {"line": 10, "character": 11}, + "end": {"line": 10, "character": 18}}, + "newText": "trace.Meta.IndPredBelow", + "insert": + {"start": {"line": 10, "character": 11}, + "end": {"line": 10, "character": 18}}}, + "label": "trace.Meta.IndPredBelow", + "kind": 10, + "detail": + "(false), enable/disable tracing for the given module and submodules"}, + {"textEdit": + {"replace": + {"start": {"line": 10, "character": 11}, + "end": {"line": 10, "character": 18}}, + "newText": "trace.Meta.IndPredBelow.match", + "insert": + {"start": {"line": 10, "character": 11}, + "end": {"line": 10, "character": 18}}}, + "label": "trace.Meta.IndPredBelow.match", + "kind": 10, + "detail": + "(false), enable/disable tracing for the given module and submodules"}, + {"textEdit": + {"replace": + {"start": {"line": 10, "character": 11}, + "end": {"line": 10, "character": 18}}, + "newText": "trace.Meta.synthPending", + "insert": + {"start": {"line": 10, "character": 11}, + "end": {"line": 10, "character": 18}}}, + "label": "trace.Meta.synthPending", + "kind": 10, + "detail": + "(false), enable/disable tracing for the given module and submodules"}, + {"textEdit": + {"replace": + {"start": {"line": 10, "character": 11}, + "end": {"line": 10, "character": 18}}, + "newText": "trace.compiler.ir.push_proj", + "insert": + {"start": {"line": 10, "character": 11}, + "end": {"line": 10, "character": 18}}}, + "label": "trace.compiler.ir.push_proj", + "kind": 10, + "detail": + "(false), (trace) enable/disable tracing for the given module and submodules"}, + {"textEdit": + {"replace": + {"start": {"line": 10, "character": 11}, + "end": {"line": 10, "character": 18}}, + "newText": "trace.compiler.lambda_pure", + "insert": + {"start": {"line": 10, "character": 11}, + "end": {"line": 10, "character": 18}}}, + "label": "trace.compiler.lambda_pure", + "kind": 10, + "detail": + "(false), (trace) enable/disable tracing for the given module and submodules"}, + {"textEdit": + {"replace": + {"start": {"line": 10, "character": 11}, + "end": {"line": 10, "character": 18}}, + "newText": "trace.Meta.isLevelDefEq.postponed", + "insert": + {"start": {"line": 10, "character": 11}, + "end": {"line": 10, "character": 18}}}, + "label": "trace.Meta.isLevelDefEq.postponed", + "kind": 10, + "detail": "(false), enable/disable tracing for the given module and submodules"}], "isIncomplete": true} {"textDocument": {"uri": "file://completionOption.lean"}, @@ -189,6 +333,90 @@ "label": "trace.pp.analyze.tryUnify", "kind": 10, "detail": + "(false), enable/disable tracing for the given module and submodules"}, + {"textEdit": + {"replace": + {"start": {"line": 13, "character": 11}, + "end": {"line": 13, "character": 19}}, + "newText": "trace.PrettyPrinter", + "insert": + {"start": {"line": 13, "character": 11}, + "end": {"line": 13, "character": 19}}}, + "label": "trace.PrettyPrinter", + "kind": 10, + "detail": + "(false), enable/disable tracing for the given module and submodules"}, + {"textEdit": + {"replace": + {"start": {"line": 13, "character": 11}, + "end": {"line": 13, "character": 19}}, + "newText": "trace.PrettyPrinter.delab", + "insert": + {"start": {"line": 13, "character": 11}, + "end": {"line": 13, "character": 19}}}, + "label": "trace.PrettyPrinter.delab", + "kind": 10, + "detail": + "(false), enable/disable tracing for the given module and submodules"}, + {"textEdit": + {"replace": + {"start": {"line": 13, "character": 11}, + "end": {"line": 13, "character": 19}}, + "newText": "trace.PrettyPrinter.format", + "insert": + {"start": {"line": 13, "character": 11}, + "end": {"line": 13, "character": 19}}}, + "label": "trace.PrettyPrinter.format", + "kind": 10, + "detail": + "(false), enable/disable tracing for the given module and submodules"}, + {"textEdit": + {"replace": + {"start": {"line": 13, "character": 11}, + "end": {"line": 13, "character": 19}}, + "newText": "trace.PrettyPrinter.parenthesize", + "insert": + {"start": {"line": 13, "character": 11}, + "end": {"line": 13, "character": 19}}}, + "label": "trace.PrettyPrinter.parenthesize", + "kind": 10, + "detail": + "(false), enable/disable tracing for the given module and submodules"}, + {"textEdit": + {"replace": + {"start": {"line": 13, "character": 11}, + "end": {"line": 13, "character": 19}}, + "newText": "trace.compiler.ir.push_proj", + "insert": + {"start": {"line": 13, "character": 11}, + "end": {"line": 13, "character": 19}}}, + "label": "trace.compiler.ir.push_proj", + "kind": 10, + "detail": + "(false), (trace) enable/disable tracing for the given module and submodules"}, + {"textEdit": + {"replace": + {"start": {"line": 13, "character": 11}, + "end": {"line": 13, "character": 19}}, + "newText": "trace.Elab.postpone", + "insert": + {"start": {"line": 13, "character": 11}, + "end": {"line": 13, "character": 19}}}, + "label": "trace.Elab.postpone", + "kind": 10, + "detail": + "(false), enable/disable tracing for the given module and submodules"}, + {"textEdit": + {"replace": + {"start": {"line": 13, "character": 11}, + "end": {"line": 13, "character": 19}}, + "newText": "trace.Meta.isLevelDefEq.postponed", + "insert": + {"start": {"line": 13, "character": 11}, + "end": {"line": 13, "character": 19}}}, + "label": "trace.Meta.isLevelDefEq.postponed", + "kind": 10, + "detail": "(false), enable/disable tracing for the given module and submodules"}], "isIncomplete": true} {"textDocument": {"uri": "file://completionOption.lean"}, diff --git a/tests/lean/interactive/completionPrv.lean.expected.out b/tests/lean/interactive/completionPrv.lean.expected.out index fa49a1af16..c0cda68c20 100644 --- a/tests/lean/interactive/completionPrv.lean.expected.out +++ b/tests/lean/interactive/completionPrv.lean.expected.out @@ -4,7 +4,12 @@ "isIncomplete": true} {"textDocument": {"uri": "file://completionPrv.lean"}, "position": {"line": 9, "character": 11}} -{"items": [{"label": "booBoo", "kind": 21, "detail": "Nat"}], +{"items": + [{"label": "booBoo", "kind": 21, "detail": "Nat"}, + {"label": "instToBoolBool", "kind": 21, "detail": "ToBool Bool"}, + {"label": "instLawfulBEqBoolInstBEqInstDecidableEqBool", + "kind": 21, + "detail": "LawfulBEq Bool"}], "isIncomplete": true} {"textDocument": {"uri": "file://completionPrv.lean"}, "position": {"line": 21, "character": 5}} diff --git a/tests/lean/interactive/keywordCompletion.lean.expected.out b/tests/lean/interactive/keywordCompletion.lean.expected.out index c7d4b7e877..11123ebbd7 100644 --- a/tests/lean/interactive/keywordCompletion.lean.expected.out +++ b/tests/lean/interactive/keywordCompletion.lean.expected.out @@ -1,10 +1,19 @@ {"textDocument": {"uri": "file://keywordCompletion.lean"}, "position": {"line": 4, "character": 16}} -{"items": [{"label": "register_string", "kind": 14, "detail": "keyword"}], +{"items": + [{"label": "register_string", "kind": 14, "detail": "keyword"}, + {"label": "termRegister_string_", "kind": 21, "detail": "Lean.ParserDescr"}], "isIncomplete": true} {"textDocument": {"uri": "file://keywordCompletion.lean"}, "position": {"line": 7, "character": 10}} {"items": [{"label": "register_string", "kind": 14, "detail": "keyword"}, - {"label": "regular", "kind": 21, "detail": "Nat"}], + {"label": "regular", "kind": 21, "detail": "Nat"}, + {"label": "recSubsingleton", + "kind": 3, + "detail": + "∀ [h : Decidable p] {h₁ : p → Sort u} {h₂ : ¬p → Sort u} [h₃ : ∀ (h : p), Subsingleton (h₁ h)]\n [h₄ : ∀ (h : ¬p), Subsingleton (h₂ h)], Subsingleton (Decidable.casesOn h h₂ h₁)"}, + {"label": "reprArg", "kind": 3, "detail": "[inst : Repr α] → α → Std.Format"}, + {"label": "termRegister_string_", "kind": 21, "detail": "Lean.ParserDescr"}, + {"label": "instReprStdGen", "kind": 21, "detail": "Repr StdGen"}], "isIncomplete": true}