From ff1d27370c19d642a884f81d540a776466a9dcc1 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 2 Apr 2021 20:44:57 -0700 Subject: [PATCH] feat: add `CompletionInfo` --- src/Lean/Elab/InfoTree.lean | 88 +++++++++++++++++++-------------- src/Lean/Elab/Term.lean | 2 +- src/Lean/Server/Completion.lean | 8 +-- src/Lean/Server/FileWorker.lean | 3 +- src/Lean/Server/InfoUtils.lean | 10 ++-- 5 files changed, 63 insertions(+), 48 deletions(-) diff --git a/src/Lean/Elab/InfoTree.lean b/src/Lean/Elab/InfoTree.lean index 0af6b27d58..16c825a940 100644 --- a/src/Lean/Elab/InfoTree.lean +++ b/src/Lean/Elab/InfoTree.lean @@ -37,9 +37,18 @@ structure CommandInfo where stx : Syntax deriving Inhabited -structure DotCompletionInfo extends TermInfo where - field? : Option Syntax := none - expectedType? : Option Expr +inductive CompletionInfo where + | dot (termInfo : TermInfo) (field? : Option Syntax) (expectedType? : Option Expr) + | id (stx : Syntax) (expectedType? : Option Expr) + | option (stx : Syntax) + | endSection (stx : Syntax) + -- TODO `import` + +def CompletionInfo.stx : CompletionInfo → Syntax + | dot i .. => i.stx + | id stx .. => stx + | option stx => stx + | endSection stx => stx structure FieldInfo where name : Name @@ -71,7 +80,7 @@ inductive Info where | ofCommandInfo (i : CommandInfo) | ofMacroExpansionInfo (i : MacroExpansionInfo) | ofFieldInfo (i : FieldInfo) - | ofDotCompletionInfo (i : DotCompletionInfo) + | ofCompletionInfo (i : CompletionInfo) deriving Inhabited inductive InfoTree where @@ -128,12 +137,12 @@ def ContextInfo.toPPContext (info : ContextInfo) (lctx : LocalContext) : PPConte def ContextInfo.ppSyntax (info : ContextInfo) (lctx : LocalContext) (stx : Syntax) : IO Format := do ppTerm (info.toPPContext lctx) stx -private def formatStxRange (cinfo : ContextInfo) (stx : Syntax) : Format := do +private def formatStxRange (ctx : ContextInfo) (stx : Syntax) : Format := do let pos := stx.getPos?.getD 0 let endPos := stx.getTailPos?.getD pos return f!"{fmtPos pos stx.getHeadInfo}-{fmtPos endPos stx.getTailInfo}" where fmtPos pos info := - let pos := format <| cinfo.fileMap.toPosition pos + let pos := format <| ctx.fileMap.toPosition pos match info with | SourceInfo.original .. => pos | _ => f!"{pos}†" @@ -141,55 +150,60 @@ where fmtPos pos info := def TermInfo.runMetaM (info : TermInfo) (ctx : ContextInfo) (x : MetaM α) : IO α := ctx.runMetaM info.lctx x -def TermInfo.format (cinfo : ContextInfo) (info : TermInfo) : IO Format := do - info.runMetaM cinfo do - return f!"{← Meta.ppExpr info.expr} : {← Meta.ppExpr (← Meta.inferType info.expr)} @ {formatStxRange cinfo info.stx}" +def TermInfo.format (ctx : ContextInfo) (info : TermInfo) : IO Format := do + info.runMetaM ctx do + return f!"{← Meta.ppExpr info.expr} : {← Meta.ppExpr (← Meta.inferType info.expr)} @ {formatStxRange ctx info.stx}" -def CommandInfo.format (cinfo : ContextInfo) (info : CommandInfo) : IO Format := do - return f!"command @ {formatStxRange cinfo info.stx}" +def CompletionInfo.format (ctx : ContextInfo) (info : CompletionInfo) : IO Format := + match info with + | CompletionInfo.dot i .. => return f!"[.] {← i.format ctx}" + | _ => return f!"[.] {info.stx}" -def FieldInfo.format (cinfo : ContextInfo) (info : FieldInfo) : IO Format := do - cinfo.runMetaM info.lctx do - return f!"{info.name} : {← Meta.ppExpr (← Meta.inferType info.val)} := {← Meta.ppExpr info.val} @ {formatStxRange cinfo info.stx}" +def CommandInfo.format (ctx : ContextInfo) (info : CommandInfo) : IO Format := do + return f!"command @ {formatStxRange ctx info.stx}" -def ContextInfo.ppGoals (cinfo : ContextInfo) (goals : List MVarId) : IO Format := +def FieldInfo.format (ctx : ContextInfo) (info : FieldInfo) : IO Format := do + ctx.runMetaM info.lctx do + return f!"{info.name} : {← Meta.ppExpr (← Meta.inferType info.val)} := {← Meta.ppExpr info.val} @ {formatStxRange ctx info.stx}" + +def ContextInfo.ppGoals (ctx : ContextInfo) (goals : List MVarId) : IO Format := if goals.isEmpty then return "no goals" else - cinfo.runMetaM {} (return Std.Format.prefixJoin "\n" (← goals.mapM Meta.ppGoal)) + ctx.runMetaM {} (return Std.Format.prefixJoin "\n" (← goals.mapM Meta.ppGoal)) -def TacticInfo.format (cinfo : ContextInfo) (info : TacticInfo) : IO Format := do - let cinfoB := { cinfo with mctx := info.mctxBefore } - let cinfoA := { cinfo with mctx := info.mctxAfter } - let goalsBefore ← cinfoB.ppGoals info.goalsBefore - let goalsAfter ← cinfoA.ppGoals info.goalsAfter - return f!"Tactic @ {formatStxRange cinfo info.stx}\nbefore {goalsBefore}\nafter {goalsAfter}" +def TacticInfo.format (ctx : ContextInfo) (info : TacticInfo) : IO Format := do + let ctxB := { ctx with mctx := info.mctxBefore } + let ctxA := { ctx with mctx := info.mctxAfter } + let goalsBefore ← ctxB.ppGoals info.goalsBefore + let goalsAfter ← ctxA.ppGoals info.goalsAfter + return f!"Tactic @ {formatStxRange ctx info.stx}\nbefore {goalsBefore}\nafter {goalsAfter}" -def MacroExpansionInfo.format (cinfo : ContextInfo) (info : MacroExpansionInfo) : IO Format := do - let before ← cinfo.ppSyntax info.lctx info.before - let after ← cinfo.ppSyntax info.lctx info.after +def MacroExpansionInfo.format (ctx : ContextInfo) (info : MacroExpansionInfo) : IO Format := do + let before ← ctx.ppSyntax info.lctx info.before + let after ← ctx.ppSyntax info.lctx info.after return f!"Macro expansion\n{before}\n===>\n{after}" -def Info.format (cinfo : ContextInfo) : Info → IO Format - | ofTacticInfo i => i.format cinfo - | ofTermInfo i => i.format cinfo - | ofCommandInfo i => i.format cinfo - | ofMacroExpansionInfo i => i.format cinfo - | ofFieldInfo i => i.format cinfo - | ofDotCompletionInfo i => return f!"[.] {← i.format cinfo}" +def Info.format (ctx : ContextInfo) : Info → IO Format + | ofTacticInfo i => i.format ctx + | ofTermInfo i => i.format ctx + | ofCommandInfo i => i.format ctx + | ofMacroExpansionInfo i => i.format ctx + | ofFieldInfo i => i.format ctx + | ofCompletionInfo i => i.format ctx -partial def InfoTree.format (tree : InfoTree) (cinfo? : Option ContextInfo := none) : IO Format := do +partial def InfoTree.format (tree : InfoTree) (ctx? : Option ContextInfo := none) : IO Format := do match tree with | ofJson j => return toString j | hole id => return toString id | context i t => format t i - | node i cs => match cinfo? with + | node i cs => match ctx? with | none => return "" - | some cinfo => + | some ctx => if cs.size == 0 then - i.format cinfo + i.format ctx else - return f!"{← i.format cinfo}{Std.Format.nestD <| Std.Format.prefixJoin "\n" (← cs.toList.mapM fun c => format c cinfo?)}" + return f!"{← i.format ctx}{Std.Format.nestD <| Std.Format.prefixJoin "\n" (← cs.toList.mapM fun c => format c ctx?)}" section variable [Monad m] [MonadInfoTree m] diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index bc6e773432..b493302f91 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -1076,7 +1076,7 @@ def mkTermInfo (stx : Syntax) (e : Expr) : TermElabM (Sum Info MVarId) := do /-- Store in the `InfoTree` that `e` is a "dot"-completion target. -/ def addDotCompletionInfo (stx : Syntax) (e : Expr) (expectedType? : Option Expr) (field? : Option Syntax := none) : TermElabM Unit := do - pushInfoLeaf <| Info.ofDotCompletionInfo { expr := e, stx := stx, lctx := (← getLCtx), field? := field?, expectedType? := expectedType? } + pushInfoLeaf <| Info.ofCompletionInfo <| CompletionInfo.dot { expr := e, stx := stx, lctx := (← getLCtx) } (field? := field?) (expectedType? := expectedType?) /-- Main function for elaborating terms. diff --git a/src/Lean/Server/Completion.lean b/src/Lean/Server/Completion.lean index 423c0e8172..8a885c16b1 100644 --- a/src/Lean/Server/Completion.lean +++ b/src/Lean/Server/Completion.lean @@ -26,7 +26,8 @@ private def isBlackListedForCompletion (declName : Name) : MetaM Bool := do open Elab in open Meta in partial def find? (fileMap : FileMap) (hoverPos : String.Pos) (infoTree : InfoTree) : IO (Option CompletionList) := do let ⟨hoverLine, _⟩ := fileMap.toPosition hoverPos - if let some (ctx, Info.ofDotCompletionInfo info) := infoTree.foldInfo (init := none) (choose fileMap hoverLine) then + match infoTree.foldInfo (init := none) (choose fileMap hoverLine) with + | some (ctx, Info.ofCompletionInfo (CompletionInfo.dot info ..)) => info.runMetaM ctx do dbg_trace ">> {info.stx}, {info.expr}" let type ← instantiateMVars (← inferType info.expr) @@ -42,11 +43,10 @@ partial def find? (fileMap : FileMap) (hoverPos : String.Pos) (infoTree : InfoTr return some { label := cinfo.name.getString!, detail? := some (toString detail), documentation? := none } return some { items := items, isIncomplete := true } | _ => return none - else - return none + | _ => return none where choose (fileMap : FileMap) (hoverLine : Nat) (ctx : ContextInfo) (info : Info) (best? : Option (ContextInfo × Info)) : Option (ContextInfo × Info) := - if !info.isDotCompletion then best? + if !info.isCompletion then best? else if let some d := info.occursBefore? hoverPos then let pos := info.tailPos?.get! let ⟨line, _⟩ := fileMap.toPosition pos diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean index 5d2ddcb113..711e6b50be 100644 --- a/src/Lean/Server/FileWorker.lean +++ b/src/Lean/Server/FileWorker.lean @@ -371,10 +371,11 @@ section RequestHandling let doc ← st.docRef.get let text := doc.meta.text let pos := text.lspPosToUtf8Pos p.position + dbg_trace ">> handleCompletion invoked {pos}" withWaitFindSnap doc (fun s => s.endPos > pos) (notFoundX := pure { items := #[], isIncomplete := true }) fun snap => do for infoTree in snap.toCmdState.infoState.trees do - for (ctx, info) in infoTree.getDotCompletionInfos do + for (ctx, info) in infoTree.getCompletionInfos do dbg_trace "{← info.format ctx}" if let some r ← Completion.find? doc.meta.text pos infoTree then return r diff --git a/src/Lean/Server/InfoUtils.lean b/src/Lean/Server/InfoUtils.lean index 5836ab2bb7..4f32a55718 100644 --- a/src/Lean/Server/InfoUtils.lean +++ b/src/Lean/Server/InfoUtils.lean @@ -44,14 +44,14 @@ def Info.isTerm : Info → Bool | ofTermInfo _ => true | _ => false -def Info.isDotCompletion : Info → Bool - | ofDotCompletionInfo .. => true +def Info.isCompletion : Info → Bool + | ofCompletionInfo .. => true | _ => false -def InfoTree.getDotCompletionInfos (infoTree : InfoTree) : Array (ContextInfo × DotCompletionInfo) := +def InfoTree.getCompletionInfos (infoTree : InfoTree) : Array (ContextInfo × CompletionInfo) := infoTree.foldInfo (init := #[]) fun ctx info result => match info with - | Info.ofDotCompletionInfo info => result.push (ctx, info) + | Info.ofCompletionInfo info => result.push (ctx, info) | _ => result def Info.stx : Info → Syntax @@ -60,7 +60,7 @@ def Info.stx : Info → Syntax | ofCommandInfo i => i.stx | ofMacroExpansionInfo i => i.before | ofFieldInfo i => i.stx - | ofDotCompletionInfo i => i.stx + | ofCompletionInfo i => i.stx def Info.pos? (i : Info) : Option String.Pos := i.stx.getPos? (originalOnly := true)