refactor: replace InfoWithCtx with ExprWithCtx
This is potentially controversial. There are still some [todo]s that need sorting.
This commit is contained in:
E.W.Ayers
Leonardo de Moura
parent
3d561a3ab0
commit
f64cb95eca
3 changed files with 46 additions and 58 deletions
|
|
@ -57,34 +57,33 @@ structure InfoPopup where
|
|||
|
||||
/-- Given elaborator info for a particular subexpression. Produce the `InfoPopup`.
|
||||
|
||||
The intended usage of this is for the infoview to pass the `InfoWithCtx` which
|
||||
The intended usage of this is for the infoview to pass the `ExprWithCtx` which
|
||||
was stored for a particular `SubexprInfo` tag in a `TaggedText` generated with `ppExprTagged`.
|
||||
-/
|
||||
def makePopup : WithRpcRef InfoWithCtx → RequestM (RequestTask InfoPopup)
|
||||
def makePopup : WithRpcRef ExprWithCtx → RequestM (RequestTask InfoPopup)
|
||||
| ⟨i⟩ => RequestM.asTask do
|
||||
i.ctx.runMetaM i.info.lctx do
|
||||
let type? ← match (← i.info.type?) with
|
||||
| some type => some <$> ppExprTagged type
|
||||
| none => pure none
|
||||
let exprExplicit? ← match i.info with
|
||||
| Elab.Info.ofTermInfo ti =>
|
||||
let ti ← ppExprTagged ti.expr (explicit := true)
|
||||
-- remove top-level expression highlight
|
||||
pure <| some <| match ti with
|
||||
| .tag _ tt => tt
|
||||
| tt => tt
|
||||
| Elab.Info.ofFieldInfo fi => pure <| some <| TaggedText.text fi.fieldName.toString
|
||||
| _ => pure none
|
||||
i.ctx.runMetaM i.lctx do
|
||||
let type? ←
|
||||
(do return some <|← ppExprTagged <|← Meta.inferType i.expr)
|
||||
<|> pure none
|
||||
let ti ← ppExprTagged i.expr (explicit := true)
|
||||
-- remove top-level expression highlight
|
||||
let tt := match ti with
|
||||
| .tag _ tt => tt
|
||||
| tt => tt
|
||||
let doc? ←
|
||||
if let some n := i.expr.constName?
|
||||
then findDocString? (← getEnv) n else pure none
|
||||
return {
|
||||
type := type?
|
||||
exprExplicit := exprExplicit?
|
||||
doc := ← i.info.docString? : InfoPopup
|
||||
exprExplicit := some tt
|
||||
doc := doc? : InfoPopup
|
||||
}
|
||||
|
||||
builtin_initialize
|
||||
registerBuiltinRpcProcedure
|
||||
`Lean.Widget.InteractiveDiagnostics.infoToInteractive
|
||||
(WithRpcRef InfoWithCtx)
|
||||
(WithRpcRef ExprWithCtx)
|
||||
InfoPopup
|
||||
makePopup
|
||||
|
||||
|
|
@ -132,23 +131,25 @@ builtin_initialize
|
|||
|
||||
structure GetGoToLocationParams where
|
||||
kind : GoToKind
|
||||
info : WithRpcRef InfoWithCtx
|
||||
info : WithRpcRef ExprWithCtx
|
||||
deriving RpcEncoding
|
||||
|
||||
def getGoToLocation : GetGoToLocationParams → RequestM (RequestTask (Array Lsp.LocationLink))
|
||||
| ⟨kind, ⟨i⟩⟩ => RequestM.asTask do
|
||||
let rc ← read
|
||||
let ls ← FileWorker.locationLinksOfInfo kind i.ctx (ExprWithCtx.toTermInfo i)
|
||||
if !ls.isEmpty then return ls
|
||||
-- TODO(WN): unify handling of delab'd (infoview) and elab'd (editor) applications
|
||||
let .app _ _ _ := i.expr | return #[]
|
||||
let some nm := i.expr.getAppFn.constName? | return #[]
|
||||
i.ctx.runMetaM i.lctx <|
|
||||
locationLinksFromDecl rc.srcSearchPath rc.doc.meta.uri nm none
|
||||
|
||||
builtin_initialize
|
||||
registerBuiltinRpcProcedure
|
||||
`Lean.Widget.getGoToLocation
|
||||
GetGoToLocationParams
|
||||
(Array Lsp.LocationLink)
|
||||
fun ⟨kind, ⟨i⟩⟩ => RequestM.asTask do
|
||||
let rc ← read
|
||||
let ls ← FileWorker.locationLinksOfInfo kind i.ctx i.info
|
||||
if !ls.isEmpty then return ls
|
||||
-- TODO(WN): unify handling of delab'd (infoview) and elab'd (editor) applications
|
||||
let .ofTermInfo ti := i.info | return #[]
|
||||
let .app _ _ _ := ti.expr | return #[]
|
||||
let some nm := ti.expr.getAppFn.constName? | return #[]
|
||||
i.ctx.runMetaM ti.lctx <|
|
||||
locationLinksFromDecl rc.srcSearchPath rc.doc.meta.uri nm none
|
||||
getGoToLocation
|
||||
|
||||
end Lean.Widget
|
||||
|
|
|
|||
|
|
@ -6,38 +6,24 @@ namespace Lean.Widget
|
|||
|
||||
open Elab Server
|
||||
|
||||
/-- Expression with the context required to render it interactively in the infoview.
|
||||
|
||||
The difference with `InfoWithCtx` is that this is an explicitly an expression which is not necessarily created during the elaboration step.
|
||||
|
||||
The purpose of `ExprWithCtx` is so that widget writers can send an expression over and display it,
|
||||
as well as send it back in another RPC call for further processing.
|
||||
The former functionality can be achieved by sending `CodeWithInfos`, and even the latter could by inspecting the root tag for its `.ofTermInfo`.
|
||||
However `ExprWithCtx` gives a cleaner interface, and it gives the option to not pretty-print the expression,
|
||||
which can be useful if the widget code just needs it around as data, or wants to delay printing until the user requests it.
|
||||
-/
|
||||
/-- Expression with the context required to render it interactively in the infoview. -/
|
||||
structure ExprWithCtx where
|
||||
ctx : Elab.ContextInfo
|
||||
lctx : LocalContext
|
||||
expr : Expr
|
||||
deriving Inhabited, RpcEncoding with { withRef := true }
|
||||
|
||||
/-- Elaborator information with elaborator context.
|
||||
|
||||
This is used to tag different parts of expressions in `ppExprTagged`.
|
||||
This is the input to the RPC call `Lean.Widget.InteractiveDiagnostics.infoToInteractive`.
|
||||
|
||||
The purpose of `InfoWithCtx` is to carry over information about delaborated
|
||||
`Info` nodes in a `CodeWithInfos`, and the associated pretty-printing
|
||||
functionality is purpose-specific to showing the contents of infoview popups.
|
||||
-/
|
||||
structure InfoWithCtx where
|
||||
ctx : Elab.ContextInfo
|
||||
info : Elab.Info
|
||||
deriving Inhabited, RpcEncoding with { withRef := true }
|
||||
|
||||
deriving instance RpcEncoding with { withRef := true } for MessageData
|
||||
|
||||
/-- Creates a dummy Elab.Info from an ExprWithCtx. -/
|
||||
def ExprWithCtx.toTermInfo (e : ExprWithCtx) : Elab.Info :=
|
||||
Elab.Info.ofTermInfo {
|
||||
elaborator := Name.anonymous -- [todo] is this right?
|
||||
stx := Syntax.missing -- [todo] is this right?
|
||||
lctx := e.lctx
|
||||
expr := e.expr
|
||||
expectedType? := none
|
||||
}
|
||||
|
||||
instance : ToJson FVarId := ⟨fun f => toJson f.name⟩
|
||||
instance : ToJson MVarId := ⟨fun f => toJson f.name⟩
|
||||
instance : FromJson FVarId := ⟨fun j => FVarId.mk <$> fromJson? j⟩
|
||||
|
|
|
|||
|
|
@ -17,8 +17,8 @@ open Server
|
|||
|
||||
/-- Information about a subexpression within delaborated code. -/
|
||||
structure SubexprInfo where
|
||||
/-- The `Elab.Info` node with the semantics of this part of the output. -/
|
||||
info : WithRpcRef InfoWithCtx
|
||||
/-- The Expression and context node with the semantics of this part of the output. -/
|
||||
info : WithRpcRef ExprWithCtx
|
||||
/-- The position of this subexpression within the top-level expression.
|
||||
See `Lean.SubExpr`. -/
|
||||
subexprPos : Lean.SubExpr.Pos
|
||||
|
|
@ -40,8 +40,9 @@ where
|
|||
go (tt : TaggedText (Nat × Nat)) :=
|
||||
tt.rewrite fun (n, _) subTt =>
|
||||
match infos.find? n with
|
||||
| none => go subTt
|
||||
| some i => TaggedText.tag ⟨WithRpcRef.mk { ctx, info := i }, n⟩ (go subTt)
|
||||
| some (.ofTermInfo ti) => TaggedText.tag ⟨WithRpcRef.mk { ctx, lctx := ti.lctx, expr := ti.expr }, n⟩ (go subTt)
|
||||
| some (.ofFieldInfo _fi) => go subTt -- [todo] what to do in this case?
|
||||
| _ => go subTt
|
||||
|
||||
def ppExprTagged (e : Expr) (explicit : Bool := false) : MetaM CodeWithInfos := do
|
||||
let optsPerPos := if explicit then
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue