doc: InfoTree docstrings
This commit is contained in:
E.W.Ayers
Leonardo de Moura
parent
458da0e27b
commit
9598e39c82
2 changed files with 80 additions and 10 deletions
|
|
@ -145,6 +145,9 @@ 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' {α β} : m α → (Option α → m β) → m (α × β)
|
||||
|
||||
export MonadFinally (tryFinally')
|
||||
|
|
|
|||
|
|
@ -15,7 +15,7 @@ namespace Lean.Elab
|
|||
|
||||
open Std (PersistentArray PersistentArray.empty PersistentHashMap)
|
||||
|
||||
/- Context after executing `liftTermElabM`.
|
||||
/-- Context after executing `liftTermElabM`.
|
||||
Note that the term information collected during elaboration may contain metavariables, and their
|
||||
assignments are stored at `mctx`. -/
|
||||
structure ContextInfo where
|
||||
|
|
@ -70,9 +70,11 @@ structure FieldInfo where
|
|||
stx : Syntax
|
||||
deriving Inhabited
|
||||
|
||||
/- 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...`. -/
|
||||
/-- 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...`. -/
|
||||
structure TacticInfo extends ElabInfo where
|
||||
mctxBefore : MetavarContext
|
||||
goalsBefore : List MVarId
|
||||
|
|
@ -96,6 +98,7 @@ def CustomInfo.format : CustomInfo → Format
|
|||
|
||||
instance : ToFormat CustomInfo := ⟨CustomInfo.format⟩
|
||||
|
||||
/-- Header information for a node in `InfoTree`. -/
|
||||
inductive Info where
|
||||
| ofTacticInfo (i : TacticInfo)
|
||||
| ofTermInfo (i : TermInfo)
|
||||
|
|
@ -106,10 +109,36 @@ inductive Info where
|
|||
| ofCustomInfo (i : CustomInfo)
|
||||
deriving Inhabited
|
||||
|
||||
/-- The InfoTree is a structure that is generated during elaboration that is 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.
|
||||
|
||||
The infotree consists of nodes which may have child nodes. Each node
|
||||
has an `Info` object that contains details about what kind of information
|
||||
is present. Each `Info` object also contains a `Syntax` instance, this is used to
|
||||
map positions in the Lean document to particular info objects.
|
||||
|
||||
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.
|
||||
|
||||
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
|
||||
`hole`s which are filled in later in the same way that unassigned metavariables are.
|
||||
-/
|
||||
inductive InfoTree where
|
||||
| context (i : ContextInfo) (t : InfoTree) -- The context object is created by `liftTermElabM` at `Command.lean`
|
||||
| node (i : Info) (children : PersistentArray InfoTree) -- The children contains information for nested term elaboration and tactic evaluation
|
||||
| hole (mvarId : MVarId) -- The elaborator creates holes (aka metavariables) for tactics and postponed terms
|
||||
| /-- 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 -/
|
||||
node (i : Info) (children : PersistentArray InfoTree)
|
||||
| /-- For user data. -/
|
||||
ofJson (j : Json)
|
||||
| /-- The elaborator creates holes (aka metavariables) for tactics and postponed terms -/
|
||||
hole (mvarId : MVarId)
|
||||
deriving Inhabited
|
||||
|
||||
partial def InfoTree.findInfo? (p : Info → Bool) (t : InfoTree) : Option Info :=
|
||||
|
|
@ -122,9 +151,22 @@ partial def InfoTree.findInfo? (p : Info → Bool) (t : InfoTree) : Option Info
|
|||
ts.findSome? (findInfo? p)
|
||||
| _ => none
|
||||
|
||||
/-- 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.
|
||||
|
||||
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.
|
||||
|
||||
To see how `trees` is used, look at the function body of `withInfoContext'`.
|
||||
-/
|
||||
structure InfoState where
|
||||
enabled : Bool := false -- whether info trees should be recorded
|
||||
assignment : PersistentHashMap MVarId InfoTree := {} -- map from holeId to InfoTree
|
||||
/-- Whether info trees should be recorded. -/
|
||||
enabled : Bool := false
|
||||
/-- Map from holes in the infotree to child infotrees. -/
|
||||
assignment : PersistentHashMap MVarId InfoTree := {}
|
||||
/-- Pending child trees of a node. -/
|
||||
trees : PersistentArray InfoTree := {}
|
||||
deriving Inhabited
|
||||
|
||||
|
|
@ -138,6 +180,8 @@ instance [MonadLift m n] [MonadInfoTree m] : MonadInfoTree n where
|
|||
getInfoState := liftM (getInfoState : m _)
|
||||
modifyInfoState f := liftM (modifyInfoState f : m _)
|
||||
|
||||
/-- Instantiate the holes on the given `tree` with the assignment table.
|
||||
(analoguous to instantiating the metavariables in an expression) -/
|
||||
partial def InfoTree.substitute (tree : InfoTree) (assignment : PersistentHashMap MVarId InfoTree) : InfoTree :=
|
||||
match tree with
|
||||
| node i c => node i <| c.map (substitute · assignment)
|
||||
|
|
@ -272,6 +316,7 @@ variable [Monad m] [MonadInfoTree m]
|
|||
@[inline] private def modifyInfoTrees (f : PersistentArray InfoTree → PersistentArray InfoTree) : m Unit :=
|
||||
modifyInfoState fun s => { s with trees := f s.trees }
|
||||
|
||||
/-- Returns the current array of InfoTrees and resets it to an empty array. -/
|
||||
def getResetInfoTrees : m (PersistentArray InfoTree) := do
|
||||
let trees := (← getInfoState).trees
|
||||
modifyInfoTrees fun _ => {}
|
||||
|
|
@ -288,6 +333,10 @@ def pushInfoLeaf (t : Info) : m Unit := do
|
|||
def addCompletionInfo (info : CompletionInfo) : m Unit := do
|
||||
pushInfoLeaf <| Info.ofCompletionInfo info
|
||||
|
||||
/-- 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
|
||||
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
|
||||
if (← getInfoState).enabled then
|
||||
|
|
@ -295,6 +344,7 @@ def resolveGlobalConstNoOverloadWithInfo [MonadResolveName m] [MonadEnv m] [Mona
|
|||
pushInfoLeaf <| Info.ofTermInfo { elaborator := Name.anonymous, lctx := LocalContext.empty, expr := (← mkConstWithLevelParams n), stx := id, expectedType? }
|
||||
return n
|
||||
|
||||
/-- Similar to resolveGlobalConstNoOverloadWithInfo, except if there are multiple name resolutions then it returns them as a list. -/
|
||||
def resolveGlobalConstWithInfos [MonadResolveName m] [MonadEnv m] [MonadError m] (id : Syntax) (expectedType? : Option Expr := none) : m (List Name) := do
|
||||
let ns ← resolveGlobalConst id
|
||||
if (← getInfoState).enabled then
|
||||
|
|
@ -302,6 +352,12 @@ def resolveGlobalConstWithInfos [MonadResolveName m] [MonadEnv m] [MonadError m]
|
|||
pushInfoLeaf <| Info.ofTermInfo { elaborator := Name.anonymous, lctx := LocalContext.empty, expr := (← mkConstWithLevelParams n), stx := id, expectedType? }
|
||||
return ns
|
||||
|
||||
/-- Use this to descend a node on the infotree that is being built.
|
||||
|
||||
It saves the current list of trees `t₀` and resets it and then runs `x >>= mkInfo`, producing either an `i : Info` or a hole id.
|
||||
Running `x >>= mkInfo` will modify the trees state and produce a new list of trees `t₁`.
|
||||
In the `i : Info` case, `t₁` become the children of a node `node i t₁` that is appended to `t₀`.
|
||||
-/
|
||||
def withInfoContext' [MonadFinally m] (x : m α) (mkInfo : α → m (Sum Info MVarId)) : m α := do
|
||||
if (← getInfoState).enabled then
|
||||
let treesSaved ← getResetInfoTrees
|
||||
|
|
@ -317,6 +373,8 @@ def withInfoContext' [MonadFinally m] (x : m α) (mkInfo : α → m (Sum Info MV
|
|||
else
|
||||
x
|
||||
|
||||
/-- Saves the current list of trees `t₀`, runs `x` to produce a new tree list `t₁` and
|
||||
runs `mkInfoTree t₁` to get `n : InfoTree` and then restores the trees to be `t₀ ++ [n]`.-/
|
||||
def withInfoTreeContext [MonadFinally m] (x : m α) (mkInfoTree : PersistentArray InfoTree → m InfoTree) : m α := do
|
||||
if (← getInfoState).enabled then
|
||||
let treesSaved ← getResetInfoTrees
|
||||
|
|
@ -327,9 +385,13 @@ def withInfoTreeContext [MonadFinally m] (x : m α) (mkInfoTree : PersistentArra
|
|||
else
|
||||
x
|
||||
|
||||
/-- Run `x` as a new child infotree node with header given by `mkInfo`. -/
|
||||
@[inline] def withInfoContext [MonadFinally m] (x : m α) (mkInfo : m Info) : m α := do
|
||||
withInfoTreeContext x (fun trees => do return InfoTree.node (← mkInfo) trees)
|
||||
|
||||
/-- Resets the trees state `t₀`, runs `x` to produce a new trees
|
||||
state `t₁` and sets the state to be `t₀ ++ (InfoTree.context Γ <$> t₁)`
|
||||
where `Γ` is the context derived from the monad state. -/
|
||||
def withSaveInfoContext [MonadFinally m] [MonadEnv m] [MonadOptions m] [MonadMCtx m] [MonadResolveName m] [MonadFileMap m] (x : m α) : m α := do
|
||||
if (← getInfoState).enabled then
|
||||
let treesSaved ← getResetInfoTrees
|
||||
|
|
@ -338,7 +400,12 @@ def withSaveInfoContext [MonadFinally m] [MonadEnv m] [MonadOptions m] [MonadMCt
|
|||
let trees ← st.trees.mapM fun tree => do
|
||||
let tree := tree.substitute st.assignment
|
||||
pure <| InfoTree.context {
|
||||
env := (← getEnv), fileMap := (← getFileMap), mctx := (← getMCtx), currNamespace := (← getCurrNamespace), openDecls := (← getOpenDecls), options := (← getOptions)
|
||||
env := (← getEnv),
|
||||
fileMap := (← getFileMap),
|
||||
mctx := (← getMCtx),
|
||||
currNamespace := (← getCurrNamespace),
|
||||
openDecls := (← getOpenDecls),
|
||||
options := (← getOptions)
|
||||
} tree
|
||||
modifyInfoTrees fun _ => treesSaved ++ trees
|
||||
else
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue