From d8e2d58da76e09003a4d3756f65d67537521fafa Mon Sep 17 00:00:00 2001 From: Ed Ayers Date: Thu, 14 Apr 2022 11:59:51 -0400 Subject: [PATCH] doc: InfoTree code review Co-authored-by: Wojciech Nawrocki --- src/Init/Control/Except.lean | 8 +++++--- src/Lean/Elab/InfoTree.lean | 20 +++++++++++--------- 2 files changed, 16 insertions(+), 12 deletions(-) diff --git a/src/Init/Control/Except.lean b/src/Init/Control/Except.lean index 259331a08b..1cf68d58dc 100644 --- a/src/Init/Control/Except.lean +++ b/src/Init/Control/Except.lean @@ -145,9 +145,11 @@ instance (ε : Type u) (m : Type u → Type v) [Monad m] : MonadControl m (Excep restoreM x := x class MonadFinally (m : Type u → Type v) where - /-- `tryFinally' x f` runs `x` to get `a : α` and then the finally function `f (some a)`. - If `x` fails for `m`'s definition of failure, it will run `f none`. - Hence it can be thought of as performing the same role as a `finally` block in an imperative programming language.-/ + /-- `tryFinally' x f` runs `x` and then the "finally" computation `f`. + When `x` succeeds with `a : α`, `f (some a)` is returned. If `x` fails + for `m`'s definition of failure, `f none` is returned. Hence `tryFinally'` + can be thought of as performing the same role as a `finally` block in + an imperative programming language. -/ tryFinally' {α β} : m α → (Option α → m β) → m (α × β) export MonadFinally (tryFinally') diff --git a/src/Lean/Elab/InfoTree.lean b/src/Lean/Elab/InfoTree.lean index 5edb599e94..7afc523d48 100644 --- a/src/Lean/Elab/InfoTree.lean +++ b/src/Lean/Elab/InfoTree.lean @@ -73,8 +73,8 @@ structure FieldInfo where /-- The information needed to render the tactic state in the infoview. We store the list of goals before and after the execution of a tactic. - We also store the metavariable context at each time since, we want to unassigned metavariables - at tactic execution time to be displayed as `?m...`. -/ + We also store the metavariable context at each time since we want metavariables + unassigned at tactic execution time to be displayed as `?m...`. -/ structure TacticInfo extends ElabInfo where mctxBefore : MetavarContext goalsBefore : List MVarId @@ -109,7 +109,7 @@ inductive Info where | ofCustomInfo (i : CustomInfo) deriving Inhabited -/-- The InfoTree is a structure that is generated during elaboration that is used +/-- The InfoTree is a structure that is generated during elaboration and used by the language server to look up information about objects at particular points in the Lean document. For example, tactic information and expected type information in the infoview and information about completions. @@ -122,9 +122,9 @@ inductive Info where An example of a function that extracts information from an infotree for a given position is `InfoTree.goalsAt?` which finds `TacticInfo`. - Information concerning expressions requires that a context also be saved, - `context` nodes store a local context that are used to properly the expressions - in lower nodes. + Information concerning expressions requires that a context also be saved. + `context` nodes store a local context that is used to process expressions + in nodes below. Because the info tree is generated during elaboration, some parts of the infotree for a particular piece of syntax may not be ready yet. Hence InfoTree supports metavariable-like @@ -133,7 +133,7 @@ inductive Info where inductive InfoTree where | /-- The context object is created by `liftTermElabM` at `Command.lean` -/ context (i : ContextInfo) (t : InfoTree) - | /-- The children contains information for nested term elaboration and tactic evaluation -/ + | /-- The children contain information for nested term elaboration and tactic evaluation -/ node (i : Info) (children : PersistentArray InfoTree) | /-- For user data. -/ ofJson (j : Json) @@ -154,7 +154,7 @@ partial def InfoTree.findInfo? (p : Info → Bool) (t : InfoTree) : Option Info /-- This structure is the state that is being used to build an InfoTree object. During elaboration, some parts of the info tree may be `holes` which need to be filled later. The `assignments` field is used to assign these holes. -The `trees` field is a list of pending child trees. For the current infotree node that is being built. +The `trees` field is a list of pending child trees for the infotree node currently being built. You should not need to use `InfoState` directly, instead infotrees should be built with the help of the methods here such as `pushInfoLeaf` to create leaf nodes and `withInfoContext` to create a nested child node. @@ -186,6 +186,7 @@ partial def InfoTree.substitute (tree : InfoTree) (assignment : PersistentHashMa match tree with | node i c => node i <| c.map (substitute · assignment) | context i t => context i (substitute t assignment) + | ofJson j => ofJson j | hole id => match assignment.find? id with | none => hole id | some tree => substitute tree assignment @@ -298,6 +299,7 @@ def Info.updateContext? : Option ContextInfo → Info → Option ContextInfo 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.name | context i t => format t i | node i cs => match ctx? with @@ -335,7 +337,7 @@ def addCompletionInfo (info : CompletionInfo) : m Unit := do /-- This does the same job as resolveGlobalConstNoOverload; resolving an identifier syntax to a unique fully resolved name or throwing if there are ambiguities. -But also adds this reolved name to the infotree, this means that when you hover +But also adds this resolved name to the infotree. This means that when you hover over a name in the sourcefile you will see the fully resolved name in the hover info.-/ def resolveGlobalConstNoOverloadWithInfo [MonadResolveName m] [MonadEnv m] [MonadError m] (id : Syntax) (expectedType? : Option Expr := none) : m Name := do let n ← resolveGlobalConstNoOverload id