From d7c201a2d4c4a0d0e76405e6d5325b63cb08ea11 Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Fri, 15 Jan 2021 16:17:20 -0500 Subject: [PATCH] chore: minor hover code cleanup --- src/Lean/Server/FileWorker.lean | 69 ++++++++++++++------------------- src/Lean/Server/InfoUtils.lean | 26 +++++++++---- 2 files changed, 49 insertions(+), 46 deletions(-) diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean index 868c8c4e75..23f75339a3 100644 --- a/src/Lean/Server/FileWorker.lean +++ b/src/Lean/Server/FileWorker.lean @@ -260,6 +260,9 @@ section RequestHandling -- TODO(WN): the type is too complicated abbrev RequestM α := ServerM $ Task $ Except IO.Error $ Except RequestError α + def mapTask (t : Task α) (f : α → ExceptT RequestError ServerM β) : RequestM β := fun st => + (IO.mapTask · t) fun a => f a st + /- Requests that need data from a certain command should traverse the snapshots by successively getting the next task, meaning that we might need to wait for elaboration. When that happens, the request should send a "content changed" error to the user @@ -279,69 +282,56 @@ section RequestHandling value := s } range? := some { start := text.utf8PosToLspPos f «end» := text.utf8PosToLspPos t } } - (IO.mapTask · findTask) fun + mapTask findTask fun | Except.error ElabTaskError.aborted => - pure $ Except.error RequestError.fileChanged + throwThe RequestError RequestError.fileChanged | Except.error (ElabTaskError.ioError e) => throwThe IO.Error e | Except.error ElabTaskError.eof => - pure $ Except.ok none + return none | Except.ok (some snap) => do for t in snap.toCmdState.infoState.trees do let ts := t.smallestNodes fun | Info.ofTermInfo i => - match i.pos?, i.endPos? with - | some pos, some endPos => - /- TODO(WN): We search for the syntax in the original command because some macro expansions - introduce phantom terms which actually contain position info but do not correspond - to anything in the source. Example: `ForInStep.yield { .. }` in `for .. in .. do` -/ - if pos ≤ hoverPos ∧ hoverPos ≤ endPos ∧ (snap.stx.find? fun s => s == i.stx).isSome then - if let Syntax.node `Lean.Parser.Term.app args := i.stx then - let hd := args.get! 0 - match hd.getPos, hd.getTailPos with - | some pos, some endPos => pos ≤ hoverPos ∧ hoverPos ≤ endPos - | _, _ => false - else - /- TODO(WN): Currently only these kinds are displayed. This misses a lot of cases that we - want to display but which will need to be tweaked to display correctly. -/ - #[`ident, - `Lean.Parser.Term.proj - ].contains i.stx.getKind + match i.pos?, i.tailPos? with + | some pos, some tailPos => + /- TODO(WN): when we have a way to do so, + check for synthetic syntax and allow arbitrary syntax kinds. -/ + if pos ≤ hoverPos ∧ hoverPos < tailPos then + #[identKind, + strLitKind, + charLitKind, + numLitKind, + scientificLitKind, + nameLitKind, + fieldIdxKind, + interpolatedStrLitKind, + interpolatedStrKind + ].contains i.stx.getKind else false | _, _ => false | _ => false let mut nds : Array (Nat × ContextInfo × TermInfo) := #[] for t in ts do if let InfoTree.context ci (InfoTree.node (Info.ofTermInfo i) _) := t then - let diff := i.endPos?.get! - i.pos?.get! + let diff := i.tailPos?.get! - i.pos?.get! nds := nds.push (diff, ci, i) if let some (_, ci, i) := nds.getMax? (fun a b => a.1 > b.1) then - let (stx, expr, pos, endPos) : (Syntax × Expr × String.Pos × String.Pos) := - (if let Syntax.node `Lean.Parser.Term.app args := i.stx then - let hd := args.get! 0 - let (pos, endPos) := (hd.getPos.get!, hd.getTailPos.get!) - (hd, i.expr.getAppFn, pos, endPos) - else - (i.stx, i.expr, i.pos?.get!, i.endPos?.get!)) - let tFmt ← ci.runMetaM i.lctx do - return f!"{← Meta.ppExpr (← Meta.inferType expr)}" - --return f!"{stx.getKind} --> {← Meta.ppExpr expr} <{pos}->{endPos}> : {← Meta.ppExpr (← Meta.inferType expr)}" - let mut hoverStr := s!"```lean + return f!"{← Meta.ppExpr i.expr} : {← Meta.ppExpr (← Meta.inferType i.expr)}" + let mut hoverFmt := f!"```lean {tFmt} ```" - if let Expr.const n .. := expr then + if let Expr.const n .. := i.expr then if let some doc ← ci.runMetaM i.lctx <| findDocString? n then - hoverStr := s!"{hoverStr}\n***\n{doc}" + hoverFmt := f!"{hoverFmt}\n***\n{doc}" - return (Except.ok $ some $ mkHover hoverStr pos endPos - -- Type inference fails - : Except RequestError _) + return some <| mkHover (toString hoverFmt) i.pos?.get! i.tailPos?.get! pure () - return Except.ok none - | Except.ok none => return Except.ok none + return none + | Except.ok none => return none def handleWaitForDiagnostics (id : RequestID) (p : WaitForDiagnosticsParam) : ServerM (Task (Except IO.Error (Except RequestError WaitForDiagnostics))) := do @@ -512,3 +502,4 @@ def workerMain : IO UInt32 := do return 1 end Lean.Server.FileWorker + diff --git a/src/Lean/Server/InfoUtils.lean b/src/Lean/Server/InfoUtils.lean index c5934bc451..f5f7ca223a 100644 --- a/src/Lean/Server/InfoUtils.lean +++ b/src/Lean/Server/InfoUtils.lean @@ -1,21 +1,27 @@ +/- +Copyright (c) 2021 Wojciech Nawrocki. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Authors: Wojciech Nawrocki +-/ import Lean.Elab namespace Lean.Elab -/-- Finds the smallest node matching `p` in the first subtree which contains a matching node. -Wraps the result in all outer `ContextInfo`s. -/ +/-- Find the deepest node matching `p` in the first subtree which contains a matching node. +The result is wrapped in all outer `ContextInfo`s. -/ partial def InfoTree.smallestNode? (p : Info → Bool) : InfoTree → Option InfoTree | context i t => context i <$> t.smallestNode? p | n@(node i cs) => - let cs := cs.map (fun c => c.smallestNode? p) - let cs := cs.filter (fun c? => c?.isSome) + let cs := cs.map (·.smallestNode? p) + let cs := cs.filter (·.isSome) if !cs.isEmpty then cs.get! 0 else if p i then some n else none | _ => none -/-- Finds the smallest node matching `p` in the first subtree which contains a matching node. -Wraps the result in all outer `ContextInfo`s. -/ +/-- For every branch, find the deepest node in that branch matching `p` +and return all of them. Each result is wrapper in all outer `ContextInfo`s. -/ partial def InfoTree.smallestNodes (p : Info → Bool) : InfoTree → List InfoTree | context i t => t.smallestNodes p |>.map (context i) | n@(node i cs) => @@ -30,7 +36,13 @@ partial def InfoTree.smallestNodes (p : Info → Bool) : InfoTree → List InfoT def TermInfo.pos? (i : TermInfo) : Option String.Pos := i.stx.getPos -def TermInfo.endPos? (i : TermInfo) : Option String.Pos := +def TermInfo.tailPos? (i : TermInfo) : Option String.Pos := + i.stx.getTailPos + +def TacticInfo.pos? (i : TacticInfo) : Option String.Pos := + i.stx.getPos + +def TacticInfo.tailPos? (i : TacticInfo) : Option String.Pos := i.stx.getTailPos end Lean.Elab