max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: auto completion improvements

Browse source
This commit is contained in:
Leonardo de Moura 2021-04-12 19:22:56 -07:00
parent d35091da56
commit 40a42128be
4 changed files with 69 additions and 25 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Elab/InfoTree.lean
View file

@ -39,7 +39,7 @@ structure CommandInfo where
inductive CompletionInfo where
| dot (termInfo : TermInfo) (field? : Option Syntax) (expectedType? : Option Expr)
| id (stx : Syntax) (lctx : LocalContext) (expectedType? : Option Expr)
| id (stx : Syntax) (id : Name) (danglingDot : Bool) (lctx : LocalContext) (expectedType? : Option Expr)
| namespaceId (stx : Syntax)
| option (stx : Syntax)
| endSection (stx : Syntax) (scopeNames : List String)
@ -161,7 +161,7 @@ def TermInfo.format (ctx : ContextInfo) (info : TermInfo) : IO Format := do
def CompletionInfo.format (ctx : ContextInfo) (info : CompletionInfo) : IO Format :=
match info with
| CompletionInfo.dot i (expectedType? := expectedType?) .. => return f!"[.] {← i.format ctx} : {expectedType?}"
| CompletionInfo.id stx lctx expectedType? => ctx.runMetaM lctx do return f!"[.] {stx} : {expectedType?} @ {formatStxRange ctx info.stx}"
| CompletionInfo.id stx _ _ lctx expectedType? => ctx.runMetaM lctx do return f!"[.] {stx} : {expectedType?} @ {formatStxRange ctx info.stx}"
| _ => return f!"[.] {info.stx} @ {formatStxRange ctx info.stx}"
def CommandInfo.format (ctx : ContextInfo) (info : CommandInfo) : IO Format := do

36
src/Lean/Elab/Term.lean
View file

@ -103,7 +103,7 @@ structure Context where
/-- Map from internal name to fvar -/
sectionFVars : NameMap Expr := {}
/-- Enable/disable implicit lambdas feature. -/
implicitLambda : Bool := true
implicitLambda : Bool := true
/-- Saved context for postponed terms and tactics to be executed. -/
structure SavedContext where
@ -1243,20 +1243,34 @@ private def elabOptLevel (stx : Syntax) : TermElabM Level :=
@[builtinTermElab «type»] def elabTypeStx : TermElab := fun stx _ =>
return mkSort (mkLevelSucc (← elabOptLevel stx[1]))
@[builtinTermElab «completion»] def elabCompletion : TermElab := fun stx expectedType? => do
/-
`ident.` is ambiguous in Lean, we may try to be completing a declaration name or access a "field".
If the identifier `ident`, the method `resolveName` adds a completion point for it using the given
/-
the method `resolveName` adds a completion point for it using the given
expected type. Thus, we propagate the expected type if `stx[0]` is an identifier.
It doesn't "hurt" if the identifier can be resolved because the expected type is not used in this case.
Recall that if the name resolution fails a synthetic sorry is returned.-/
let e ← elabTerm stx[0] (if stx[0].isIdent then expectedType? else none)
@[builtinTermElab «pipeCompletion»] def elabPipeCompletion : TermElab := fun stx expectedType? => do
let e ← elabTerm stx[0] none
unless e.isSorry do
addDotCompletionInfo stx e expectedType?
throwErrorAt stx[1] "invalid field notation, identifier or numeral expected"
@[builtinTermElab «pipeCompletion»] def elabPipeCompletion : TermElab :=
elabCompletion
@[builtinTermElab «completion»] def elabCompletion : TermElab := fun stx expectedType? => do
/- `ident.` is ambiguous in Lean, we may try to be completing a declaration name or access a "field". -/
if stx[0].isIdent then
/- If we can elaborate the identifier successfully, we assume it a dot-completion. Otherwise, we treat it as
identifier completion with a dangling `.`.
Recall that the server falls back to identifier completion when dot-completion fails. -/
let s ← saveState
try
let e ← elabTerm stx[0] none
addDotCompletionInfo stx e expectedType?
catch _ =>
s.restore
addCompletionInfo <| CompletionInfo.id stx stx[0].getId (danglingDot := true) (← getLCtx) expectedType?
throwErrorAt stx[1] "invalid field notation, identifier or numeral expected"
else
elabPipeCompletion stx expectedType?
@[builtinTermElab «hole»] def elabHole : TermElab := fun stx expectedType? => do
let mvar ← mkFreshExprMVar expectedType?
@ -1354,7 +1368,7 @@ private def mkConsts (candidates : List (Name × List String)) (explicitLevels :
let const ← mkConst constName explicitLevels
return (const, projs) :: result
def resolveName (stx : Syntax) (n : Name) (preresolved : List (Name × List String)) (explicitLevels : List Level) (expectedType? : Option Expr := none): TermElabM (List (Expr × List String)) := do
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
unless explicitLevels.isEmpty do
@ -1369,7 +1383,7 @@ def resolveName (stx : Syntax) (n : Name) (preresolved : List (Name × List Stri
process preresolved
catch ex =>
if preresolved.isEmpty && explicitLevels.isEmpty then
addCompletionInfo <| CompletionInfo.id stx (← getLCtx) expectedType?
addCompletionInfo <| CompletionInfo.id stx stx.getId (danglingDot := false) (← getLCtx) expectedType?
throw ex
where process (candidates : List (Name × List String)) : TermElabM (List (Expr × List String)) := do
if candidates.isEmpty then
@ -1377,6 +1391,8 @@ where process (candidates : List (Name × List String)) : TermElabM (List (Expr
throwAutoBoundImplicitLocal n
else
throwError "unknown identifier '{Lean.mkConst n}'"
if preresolved.isEmpty && explicitLevels.isEmpty then
addCompletionInfo <| CompletionInfo.id stx stx.getId (danglingDot := false) (← getLCtx) expectedType?
mkConsts candidates explicitLevels
/--

31
src/Lean/Server/Completion.lean
View file

@ -55,7 +55,7 @@ private def isTypeApplicable (type : Expr) (expectedType? : Option Expr) : MetaM
-- TODO take coercions into account
-- We use `withReducible` to make sure we don't spend too much time unfolding definitions
-- Alternative: use default and small number of heartbeats
withReducible <| isDefEq type expectedType
withReducible <| withoutModifyingState <| isDefEq type expectedType
catch _ =>
return false
@ -98,19 +98,22 @@ private def matchAtomic (id: Name) (declName : Name) : Bool :=
/--
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) (declName : Name) : Option Name :=
private def matchDecl? (ns : Name) (id : Name) (danglingDot : Bool) (declName : Name) : Option Name :=
-- dbg_trace "{ns}, {id}, {declName}, {danglingDot}"
if !ns.isPrefixOf declName then
none
else
let declName := declName.replacePrefix ns Name.anonymous
if id.isPrefixOf declName then
if id.isPrefixOf declName && danglingDot then
let declName := declName.replacePrefix id Name.anonymous
if declName.isAtomic && !declName.isAnonymous then
some declName
else
none
else
else if !danglingDot then
match id, declName with
| Name.str p₁ s₁ _, Name.str p₂ s₂ _ =>
if p₁ == p₂ && s₁.isPrefixOf s₂ then
@ -118,9 +121,11 @@ private def matchDecl? (ns : Name) (id : Name) (declName : Name) : Option Name :
else
none
| _, _ => none
else
none
private def idCompletionCore (ctx : ContextInfo) (stx : Syntax) (expectedType? : Option Expr) : M Unit := do
let id := stx.getId.eraseMacroScopes
private def idCompletionCore (ctx : ContextInfo) (id : Name) (danglingDot : Bool) (expectedType? : Option Expr) : M Unit := do
let id := id.eraseMacroScopes
-- dbg_trace ">> id {id} : {expectedType?}"
if id.isAtomic then
-- search for matches in the local context
@ -132,7 +137,7 @@ private def idCompletionCore (ctx : ContextInfo) (stx : Syntax) (expectedType? :
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 declName then
if let some label := matchDecl? ns id danglingDot declName then
-- dbg_trace "matched with {id}, {declName}, {label}"
addCompletionItem label c.type expectedType?
return true
@ -172,9 +177,9 @@ private def idCompletionCore (ctx : ContextInfo) (stx : Syntax) (expectedType? :
-- TODO search macros
-- TODO search namespaces
private def idCompletion (ctx : ContextInfo) (lctx : LocalContext) (stx : Syntax) (expectedType? : Option Expr) : IO (Option CompletionList) :=
private def idCompletion (ctx : ContextInfo) (lctx : LocalContext) (id : Name) (danglingDot : Bool) (expectedType? : Option Expr) : IO (Option CompletionList) :=
runM ctx lctx do
idCompletionCore ctx stx expectedType?
idCompletionCore ctx id danglingDot expectedType?
private def isDotCompletionMethod (info : ConstantInfo) : MetaM Bool :=
forallTelescopeReducing info.type fun xs _ => do
@ -214,9 +219,9 @@ private def dotCompletion (ctx : ContextInfo) (info : TermInfo) (expectedType? :
pure {}
if nameSet.isEmpty then
if info.stx.isIdent then
idCompletionCore ctx info.stx expectedType?
else if info.stx.getKind == ``Lean.Parser.Term.completion then
idCompletionCore ctx info.stx[0] expectedType?
idCompletionCore ctx info.stx.getId (danglingDot := false) expectedType?
else if info.stx.getKind == ``Lean.Parser.Term.completion && info.stx[0].isIdent then
idCompletionCore ctx info.stx[0].getId (danglingDot := true) expectedType?
else
failure
else
@ -249,7 +254,7 @@ partial def find? (fileMap : FileMap) (hoverPos : String.Pos) (infoTree : InfoTr
| some (ctx, Info.ofCompletionInfo info) =>
match info with
| CompletionInfo.dot info (expectedType? := expectedType?) .. => dotCompletion ctx info expectedType?
| CompletionInfo.id stx lctx expectedType? => idCompletion ctx lctx stx expectedType?
| CompletionInfo.id stx id danglingDot lctx expectedType? => idCompletion ctx lctx id danglingDot expectedType?
| CompletionInfo.option .. => optionCompletion ctx
| CompletionInfo.tactic .. => tacticCompletion ctx
| _ => return none

23
tests/lean/infoTree.lean.expected.out
View file

@ -1,5 +1,6 @@
[Elab.info] command @ ⟨13, 0⟩-⟨15, 6⟩
Nat : Type @ ⟨13, 11⟩-⟨13, 14⟩
[.] `Nat : some Sort.{?_uniq.237} @ ⟨13, 11⟩-⟨13, 14⟩
Nat : Type @ ⟨13, 11⟩-⟨13, 14⟩
x : Nat @ ⟨13, 7⟩-⟨13, 8⟩
Nat × Nat : Type @ ⟨13, 18⟩-⟨13, 27⟩
@ -9,8 +10,10 @@
Prod✝ Nat Nat
Prod : Type → Type → Type @ ⟨13, 18⟩†-⟨13, 22⟩†
Nat : Type @ ⟨13, 18⟩-⟨13, 21⟩
[.] `Nat : some Type.{?_uniq.241} @ ⟨13, 18⟩-⟨13, 21⟩
Nat : Type @ ⟨13, 18⟩-⟨13, 21⟩
Nat : Type @ ⟨13, 24⟩-⟨13, 27⟩
[.] `Nat : some Type.{?_uniq.240} @ ⟨13, 24⟩-⟨13, 27⟩
Nat : Type @ ⟨13, 24⟩-⟨13, 27⟩
let y : Nat × Nat := (x, x);
id y : Nat × Nat @ ⟨14, 2⟩-⟨15, 6⟩
@ -28,19 +31,23 @@
x : Nat @ ⟨14, 15⟩-⟨14, 16⟩
y : Nat × Nat @ ⟨14, 6⟩-⟨14, 7⟩
id y : Nat × Nat @ ⟨15, 2⟩-⟨15, 6⟩
[.] `id : some Prod.{0 0} Nat Nat @ ⟨15, 2⟩-⟨15, 4⟩
id : {α : Type} → α → α @ ⟨15, 2⟩-⟨15, 4⟩
y : Nat × Nat @ ⟨15, 5⟩-⟨15, 6⟩
y : Nat × Nat @ ⟨15, 5⟩-⟨15, 6⟩
[Elab.info] command @ ⟨17, 0⟩-⟨19, 8⟩
∀ (x y : Nat), Bool → x + 0 = x : Prop @ ⟨17, 8⟩-⟨17, 44⟩
Nat : Type @ ⟨17, 15⟩-⟨17, 18⟩
[.] `Nat : some Sort.{?_uniq.270} @ ⟨17, 15⟩-⟨17, 18⟩
Nat : Type @ ⟨17, 15⟩-⟨17, 18⟩
x : Nat @ ⟨17, 9⟩-⟨17, 10⟩
Nat : Type @ ⟨17, 15⟩-⟨17, 18⟩
[.] `Nat : some Sort.{?_uniq.272} @ ⟨17, 15⟩-⟨17, 18⟩
Nat : Type @ ⟨17, 15⟩-⟨17, 18⟩
y : Nat @ ⟨17, 11⟩-⟨17, 12⟩
Bool → x + 0 = x : Prop @ ⟨17, 22⟩-⟨17, 44⟩
Bool : Type @ ⟨17, 27⟩-⟨17, 31⟩
[.] `Bool : some Sort.{?_uniq.275} @ ⟨17, 27⟩-⟨17, 31⟩
Bool : Type @ ⟨17, 27⟩-⟨17, 31⟩
b : Bool @ ⟨17, 23⟩-⟨17, 24⟩
x + 0 = x : Prop @ ⟨17, 35⟩-⟨17, 44⟩
@ -90,16 +97,20 @@
[Elab.info] command @ ⟨21, 0⟩-⟨25, 10⟩
Nat → Nat → Bool → Nat : Type @ ⟨21, 9⟩-⟨21, 39⟩
Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩
[.] `Nat : some Sort.{?_uniq.592} @ ⟨21, 16⟩-⟨21, 19⟩
Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩
x : Nat @ ⟨21, 10⟩-⟨21, 11⟩
Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩
[.] `Nat : some Sort.{?_uniq.594} @ ⟨21, 16⟩-⟨21, 19⟩
Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩
y : Nat @ ⟨21, 12⟩-⟨21, 13⟩
Bool → Nat : Type @ ⟨21, 23⟩-⟨21, 39⟩
Bool : Type @ ⟨21, 28⟩-⟨21, 32⟩
[.] `Bool : some Sort.{?_uniq.597} @ ⟨21, 28⟩-⟨21, 32⟩
Bool : Type @ ⟨21, 28⟩-⟨21, 32⟩
b : Bool @ ⟨21, 24⟩-⟨21, 25⟩
Nat : Type @ ⟨21, 36⟩-⟨21, 39⟩
[.] `Nat : some Sort.{?_uniq.599} @ ⟨21, 36⟩-⟨21, 39⟩
Nat : Type @ ⟨21, 36⟩-⟨21, 39⟩
fun (x y : Nat) (b : Bool) =>
let x : Nat × Nat := (x + y, x - y);
@ -211,18 +222,24 @@
Prod✝ Nat (Array (Array Nat))
Prod : Type → Type → Type @ ⟨27, 12⟩†-⟨27, 16⟩†
Nat : Type @ ⟨27, 12⟩-⟨27, 15⟩
[.] `Nat : some Type.{?_uniq.1452} @ ⟨27, 12⟩-⟨27, 15⟩
Nat : Type @ ⟨27, 12⟩-⟨27, 15⟩
Array (Array Nat) : Type @ ⟨27, 18⟩-⟨27, 35⟩
[.] `Array : some Type.{?_uniq.1451} @ ⟨27, 18⟩-⟨27, 23⟩
Array : Type → Type @ ⟨27, 18⟩-⟨27, 23⟩
Array Nat : Type @ ⟨27, 24⟩-⟨27, 35⟩
Array Nat : Type @ ⟨27, 25⟩-⟨27, 34⟩
[.] `Array : some Type.{?_uniq.1453} @ ⟨27, 25⟩-⟨27, 30⟩
Array : Type → Type @ ⟨27, 25⟩-⟨27, 30⟩
Nat : Type @ ⟨27, 31⟩-⟨27, 34⟩
[.] `Nat : some Type.{?_uniq.1454} @ ⟨27, 31⟩-⟨27, 34⟩
Nat : Type @ ⟨27, 31⟩-⟨27, 34⟩
s : Nat × Array (Array Nat) @ ⟨27, 8⟩-⟨27, 9⟩
Array Nat : Type @ ⟨27, 39⟩-⟨27, 48⟩
[.] `Array : some Sort.{?_uniq.1456} @ ⟨27, 39⟩-⟨27, 44⟩
Array : Type → Type @ ⟨27, 39⟩-⟨27, 44⟩
Nat : Type @ ⟨27, 45⟩-⟨27, 48⟩
[.] `Nat : some Type.{?_uniq.1457} @ ⟨27, 45⟩-⟨27, 48⟩
Nat : Type @ ⟨27, 45⟩-⟨27, 48⟩
Array.push (Array.getOp s.snd 1) s.fst : Array Nat @ ⟨28, 2⟩-⟨28, 17⟩
s : Nat × Array (Array Nat) @ ⟨28, 2⟩-⟨28, 3⟩
@ -236,9 +253,11 @@
Prod.fst : {α β : Type} → α × β → α @ ⟨28, 16⟩-⟨28, 17⟩
[Elab.info] command @ ⟨30, 0⟩-⟨31, 20⟩
B : Type @ ⟨30, 14⟩-⟨30, 15⟩
[.] `B : some Sort.{?_uniq.1498} @ ⟨30, 14⟩-⟨30, 15⟩
B : Type @ ⟨30, 14⟩-⟨30, 15⟩
arg : B @ ⟨30, 8⟩-⟨30, 11⟩
Nat : Type @ ⟨30, 19⟩-⟨30, 22⟩
[.] `Nat : some Sort.{?_uniq.1500} @ ⟨30, 19⟩-⟨30, 22⟩
Nat : Type @ ⟨30, 19⟩-⟨30, 22⟩
A.val arg.pair.fst 0 : Nat @ ⟨31, 2⟩-⟨31, 20⟩
arg : B @ ⟨31, 2⟩-⟨31, 5⟩
@ -251,9 +270,11 @@
0 : Nat @ ⟨31, 19⟩-⟨31, 20⟩
[Elab.info] command @ ⟨33, 0⟩-⟨35, 1⟩
Nat : Type @ ⟨33, 12⟩-⟨33, 15⟩
[.] `Nat : some Sort.{?_uniq.1520} @ ⟨33, 12⟩-⟨33, 15⟩
Nat : Type @ ⟨33, 12⟩-⟨33, 15⟩
x : Nat @ ⟨33, 8⟩-⟨33, 9⟩
B : Type @ ⟨33, 19⟩-⟨33, 20⟩
[.] `B : some Sort.{?_uniq.1522} @ ⟨33, 19⟩-⟨33, 20⟩
B : Type @ ⟨33, 19⟩-⟨33, 20⟩
{ pair := ({ val := id }, { val := id }) } : B @ ⟨33, 24⟩-⟨35, 1⟩
({ val := id }, { val := id }) : A × A @ ⟨34, 10⟩-⟨34, 40⟩
@ -265,10 +286,12 @@
Prod.mk : {α β : Type} → α → β → α × β @ ⟨34, 10⟩†-⟨34, 17⟩†
{ val := id } : A @ ⟨34, 11⟩-⟨34, 24⟩
id : Nat → Nat @ ⟨34, 20⟩-⟨34, 22⟩
[.] `id : some Nat -> Nat @ ⟨34, 20⟩-⟨34, 22⟩
id : {α : Type} → α → α @ ⟨34, 20⟩-⟨34, 22⟩
val : Nat → Nat := id @ ⟨34, 13⟩-⟨34, 16⟩
{ val := id } : A @ ⟨34, 26⟩-⟨34, 39⟩
id : Nat → Nat @ ⟨34, 35⟩-⟨34, 37⟩
[.] `id : some Nat -> Nat @ ⟨34, 35⟩-⟨34, 37⟩
id : {α : Type} → α → α @ ⟨34, 35⟩-⟨34, 37⟩
val : Nat → Nat := id @ ⟨34, 28⟩-⟨34, 31⟩
pair : A × A := ({ val := id }, { val := id }) @ ⟨34, 2⟩-⟨34, 6⟩