/
UserWidget.lean
444 lines (370 loc) · 17.8 KB
/
UserWidget.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
/-
Copyright (c) 2022 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: E.W.Ayers, Wojciech Nawrocki
-/
prelude
import Lean.Elab.Eval
import Lean.Server.Rpc.RequestHandling
namespace Lean.Widget
open Meta Elab
/-- A widget module is a unit of source code that can execute in the infoview.
Every module definition must either be annotated with `@[widget_module]`,
or use a value of `javascript` identical to that of another definition
annotated with `@[widget_module]`.
This makes it possible for the infoview to load the module.
See the [manual entry](https://lean-lang.org/lean4/doc/examples/widgets.lean.html)
for more information on how to use the widgets system. -/
structure Module where
/-- A JS [module](https://developer.mozilla.org/en-US/docs/Web/JavaScript/Guide/Modules)
intended for use in user widgets.
The JS environment in which modules execute
provides a fixed set of libraries accessible via direct `import`,
notably [`@leanprover/infoview`](https://www.npmjs.com/package/@leanprover/infoview)
and [`react`](https://www.npmjs.com/package/react).
To initialize this field from an external JS file,
you may use `include_str "path"/"to"/"file.js"`.
However **beware** that this does not register a dependency with Lake,
so your Lean module will not automatically be rebuilt
when the `.js` file changes. -/
javascript : String
/-- The hash is cached to avoid recomputing it whenever the `Module` is used. -/
javascriptHash : { x : UInt64 // x = hash javascript } := ⟨hash javascript, rfl⟩
private unsafe def evalModuleUnsafe (e : Expr) : MetaM Module :=
evalExpr' Module ``Module e
@[implemented_by evalModuleUnsafe]
opaque evalModule (e : Expr) : MetaM Module
private unsafe def evalWidgetInstanceUnsafe (e : Expr) : MetaM WidgetInstance :=
evalExpr' WidgetInstance ``WidgetInstance e
@[implemented_by evalWidgetInstanceUnsafe]
opaque evalWidgetInstance (e : Expr) : MetaM WidgetInstance
/-! ## Storage of widget modules -/
class ToModule (α : Type u) where
toModule : α → Module
instance : ToModule Module := ⟨id⟩
private builtin_initialize builtinModulesRef : IO.Ref (RBMap UInt64 (Name × Module) compare) ←
IO.mkRef ∅
def addBuiltinModule (id : Name) (m : Module) : IO Unit :=
builtinModulesRef.modify (·.insert m.javascriptHash (id, m))
/-- Every constant `c : α` marked with `@[widget_module]` is registered here.
The registry maps `hash (toModule c).javascript` to ``(`c, `(@toModule α inst c))``
where `inst : ToModule α` is synthesized during registration time
and stored thereafter. -/
private abbrev ModuleRegistry := SimplePersistentEnvExtension
(UInt64 × Name × Expr)
(RBMap UInt64 (Name × Expr) compare)
builtin_initialize moduleRegistry : ModuleRegistry ←
registerSimplePersistentEnvExtension {
addImportedFn := fun xss => xss.foldl (Array.foldl (fun s n => s.insert n.1 n.2)) ∅
addEntryFn := fun s n => s.insert n.1 n.2
toArrayFn := fun es => es.toArray
}
/--
Registers `[builtin_widget_module]` and `[widget_module]` and binds the latter's implementation
(used for creating the obsolete `[widget]` alias below).
-/
builtin_initialize widgetModuleAttrImpl : AttributeImpl ←
let mkAttr (builtin : Bool) (name : Name) := do
let impl := {
name
descr := (if builtin then "(builtin) " else "") ++
"Registers a widget module. Its type must implement Lean.Widget.ToModule."
applicationTime := .afterCompilation
add := fun decl stx kind => Prod.fst <$> MetaM.run do
Attribute.Builtin.ensureNoArgs stx
unless kind == AttributeKind.global do throwError "invalid attribute '{name}', must be global"
let e ← mkAppM ``ToModule.toModule #[.const decl []]
let mod ← evalModule e
let env ← getEnv
unless builtin do -- don't warn on collision between previous and current stage
if let some _ := (← builtinModulesRef.get).find? mod.javascriptHash then
logWarning m!"A builtin widget module with the same hash(JS source code) was already registered."
if let some (n, _) := moduleRegistry.getState env |>.find? mod.javascriptHash then
logWarning m!"A widget module with the same hash(JS source code) was already registered at {Expr.const n []}."
let env ← getEnv
if builtin then
let h := mkConst decl
declareBuiltin decl <| mkApp2 (mkConst ``addBuiltinModule) (toExpr decl) h
else
setEnv <| moduleRegistry.addEntry env (mod.javascriptHash, decl, e)
}
registerBuiltinAttribute impl
return impl
let _ ← mkAttr true `builtin_widget_module
mkAttr false `widget_module
/-! ## Retrieval of widget modules -/
structure GetWidgetSourceParams where
/-- Hash of the JS module to retrieve. -/
hash : UInt64
pos : Lean.Lsp.Position
deriving ToJson, FromJson
structure WidgetSource where
/-- Sourcetext of the JS module to run. -/
sourcetext : String
deriving Inhabited, ToJson, FromJson
open Server RequestM in
def getWidgetSource (args : GetWidgetSourceParams) : RequestM (RequestTask WidgetSource) := do
if let some (_, m) := (← builtinModulesRef.get).find? args.hash then
return .pure { sourcetext := m.javascript }
let doc ← readDoc
let pos := doc.meta.text.lspPosToUtf8Pos args.pos
let notFound := throwThe RequestError ⟨.invalidParams, s!"No widget module with hash {args.hash} registered"⟩
withWaitFindSnap doc (notFoundX := notFound)
(fun s => s.endPos >= pos || (moduleRegistry.getState s.env).contains args.hash)
fun snap => do
if let some (_, e) := moduleRegistry.getState snap.env |>.find? args.hash then
runTermElabM snap do
return { sourcetext := (← evalModule e).javascript }
else
notFound
builtin_initialize
Server.registerBuiltinRpcProcedure ``getWidgetSource _ _ getWidgetSource
/-! ## Storage of panel widget instances -/
inductive PanelWidgetsExtEntry where
| «global» (n : Name)
| «local» (wi : WidgetInstance)
/-- Keeps track of panel widget instances that should be displayed.
Instances can be registered for display global
(i.e., persisted in `.olean`s) and locally (not persisted)
For globally displayed widgets
we cannot store a `WidgetInstance` in the persistent state
because it contains a `StateM` closure.
Instead, we add a global constant of type `WidgetInstance`
to the environment, and store its name in the extension.
For locally displayed ones, we just store a `WidgetInstance`
in the extension directly.
This is okay because it is never persisted.
The (persistent) entries are then of the form `(h, n)`
where `h` is a hash stored in the `moduleRegistry`
and `n` is the name of a `WidgetInstance` global constant.
The extension state maps each `h` as above
to a list of entries that can be either global or local ones.
Each element of the state indicates that the widget module `h`
should be displayed with the given `WidgetInstance` as its arguments.
This is similar to a parametric attribute, except that:
- parametric attributes map at most one parameter to one tagged declaration,
whereas we may display multiple instances of a single widget module; and
- parametric attributes use the same type for local and global entries,
which we cannot do owing to the closure. -/
private abbrev PanelWidgetsExt := SimpleScopedEnvExtension
(UInt64 × Name)
(RBMap UInt64 (List PanelWidgetsExtEntry) compare)
builtin_initialize panelWidgetsExt : PanelWidgetsExt ←
registerSimpleScopedEnvExtension {
addEntry := fun s (h, n) => s.insert h (.global n :: s.findD h [])
initial := .empty
}
def evalPanelWidgets : MetaM (Array WidgetInstance) := do
let mut ret := #[]
for (_, l) in panelWidgetsExt.getState (← getEnv) do
for e in l do
match e with
| .global n =>
let wi ← evalWidgetInstance (mkConst n)
ret := ret.push wi
| .local wi => ret := ret.push wi
return ret
def addPanelWidgetGlobal [Monad m] [MonadEnv m] [MonadResolveName m] (h : UInt64) (n : Name) : m Unit := do
panelWidgetsExt.add (h, n)
def addPanelWidgetScoped [Monad m] [MonadEnv m] [MonadResolveName m] (h : UInt64) (n : Name) : m Unit := do
panelWidgetsExt.add (h, n) .scoped
def addPanelWidgetLocal [Monad m] [MonadEnv m] (wi : WidgetInstance) : m Unit := do
modifyEnv fun env => panelWidgetsExt.modifyState env fun s =>
s.insert wi.javascriptHash (.local wi :: s.findD wi.javascriptHash [])
def erasePanelWidget [Monad m] [MonadEnv m] (h : UInt64) : m Unit := do
modifyEnv fun env => panelWidgetsExt.modifyState env fun st => st.erase h
/-- Save the data of a panel widget which will be displayed whenever the text cursor is on `stx`.
`hash` must be `hash (toModule c).javascript`
where `c` is some global constant annotated with `@[widget_module]`. -/
def savePanelWidgetInfo (hash : UInt64) (props : StateM Server.RpcObjectStore Json) (stx : Syntax) :
CoreM Unit := do
let env ← getEnv
let builtins ← builtinModulesRef.get
let some id :=
(builtins.find? hash |>.map (·.1)) <|> (moduleRegistry.getState env |>.find? hash |>.map (·.1))
| throwError s!"No widget module with hash {hash} registered"
pushInfoLeaf <| .ofUserWidgetInfo { id, javascriptHash := hash, props, stx }
/-! ## `show_panel_widgets` command -/
syntax widgetInstanceSpec := ident ("with " term)?
def elabWidgetInstanceSpecAux (mod : Ident) (props : Term) : TermElabM Expr := do
Term.elabTerm (expectedType? := mkConst ``WidgetInstance) <| ← `(
{ id := $(quote mod.getId)
javascriptHash := (ToModule.toModule $mod).javascriptHash
props := Server.RpcEncodable.rpcEncode $props })
def elabWidgetInstanceSpec : TSyntax ``widgetInstanceSpec → TermElabM Expr
| `(widgetInstanceSpec| $mod:ident) => do
elabWidgetInstanceSpecAux mod (← ``(Json.mkObj []))
| `(widgetInstanceSpec| $mod:ident with $props:term) => do
elabWidgetInstanceSpecAux mod props
| _ => throwUnsupportedSyntax
syntax addWidgetSpec := Parser.Term.attrKind widgetInstanceSpec
syntax eraseWidgetSpec := "-" ident
syntax showWidgetSpec := addWidgetSpec <|> eraseWidgetSpec
/-- Use `show_panel_widgets [<widget>]` to mark that `<widget>`
should always be displayed, including in downstream modules.
The type of `<widget>` must implement `Widget.ToModule`,
and the type of `<props>` must implement `Server.RpcEncodable`.
In particular, `<props> : Json` works.
Use `show_panel_widgets [<widget> with <props>]`
to specify the `<props>` that the widget should be given
as arguments.
Use `show_panel_widgets [local <widget> (with <props>)?]` to mark it
for display in the current section, namespace, or file only.
Use `show_panel_widgets [scoped <widget> (with <props>)?]` to mark it
for display only when the current namespace is open.
Use `show_panel_widgets [-<widget>]` to temporarily hide a previously shown widget
in the current section, namespace, or file.
Note that persistent erasure is not possible, i.e.,
`-<widget>` has no effect on downstream modules. -/
syntax (name := showPanelWidgetsCmd) "show_panel_widgets " "[" sepBy1(showWidgetSpec, ", ") "]" : command
open Command in
@[command_elab showPanelWidgetsCmd] def elabShowPanelWidgetsCmd : CommandElab
| `(show_panel_widgets [ $ws ,*]) => liftTermElabM do
for w in ws.getElems do
match w with
| `(showWidgetSpec| - $mod:ident) =>
let mod : Term ← ``(ToModule.toModule $mod)
let mod : Expr ← Term.elabTerm (expectedType? := mkConst ``Module) mod
let mod : Module ← evalModule mod
erasePanelWidget mod.javascriptHash
| `(showWidgetSpec| $attr:attrKind $spec:widgetInstanceSpec) =>
let attr ← liftMacroM <| toAttributeKind attr
let wiExpr ← elabWidgetInstanceSpec spec
let wi ← evalWidgetInstance wiExpr
if let .local := attr then
addPanelWidgetLocal wi
else
let name ← mkFreshUserName (wi.id ++ `_instance)
let wiExpr ← instantiateMVars wiExpr
if wiExpr.hasMVar then
throwError "failed to compile expression, it contains metavariables{indentExpr wiExpr}"
addAndCompile <| Declaration.defnDecl {
name
levelParams := []
type := mkConst ``WidgetInstance
value := wiExpr
hints := .opaque
safety := .safe
}
if let .global := attr then
addPanelWidgetGlobal wi.javascriptHash name
else
addPanelWidgetScoped wi.javascriptHash name
| _ => throwUnsupportedSyntax
| _ => throwUnsupportedSyntax
/-! ## `#widget` command -/
/-- Use `#widget <widget>` to display a panel widget,
and `#widget <widget> with <props>` to display it with the given props.
Useful for debugging widgets.
The type of `<widget>` must implement `Widget.ToModule`,
and the type of `<props>` must implement `Server.RpcEncodable`.
In particular, `<props> : Json` works. -/
syntax (name := widgetCmd) "#widget " widgetInstanceSpec : command
open Command in
@[command_elab widgetCmd] def elabWidgetCmd : CommandElab
| stx@`(#widget $s) => liftTermElabM do
let wi : Expr ← elabWidgetInstanceSpec s
let wi : WidgetInstance ← evalWidgetInstance wi
savePanelWidgetInfo wi.javascriptHash wi.props stx
| _ => throwUnsupportedSyntax
/-! ## Deprecated definitions -/
/-- Use this structure and the `@[widget]` attribute to define your own widgets.
```lean
@[widget]
def rubiks : UserWidgetDefinition :=
{ name := "Rubiks cube app"
javascript := include_str ...
}
```
-/
structure UserWidgetDefinition where
/-- Pretty name of user widget to display to the user. -/
name : String
/-- An ESmodule that exports a react component to render. -/
javascript: String
deriving Inhabited, ToJson, FromJson
instance : ToModule UserWidgetDefinition where
toModule uwd := { uwd with }
private def widgetAttrImpl : AttributeImpl where
name := `widget
descr := "The `@[widget]` attribute has been deprecated, use `@[widget_module]` instead."
applicationTime := AttributeApplicationTime.afterCompilation
add := widgetModuleAttrImpl.add
builtin_initialize registerBuiltinAttribute widgetAttrImpl
private unsafe def evalUserWidgetDefinitionUnsafe [Monad m] [MonadEnv m] [MonadOptions m] [MonadError m]
(id : Name) : m UserWidgetDefinition := do
ofExcept <| (← getEnv).evalConstCheck UserWidgetDefinition (← getOptions) ``UserWidgetDefinition id
@[implemented_by evalUserWidgetDefinitionUnsafe]
opaque evalUserWidgetDefinition [Monad m] [MonadEnv m] [MonadOptions m] [MonadError m]
(id : Name) : m UserWidgetDefinition
/-- Save a user-widget instance to the infotree.
The given `widgetId` should be the declaration name of the widget definition. -/
@[deprecated savePanelWidgetInfo] def saveWidgetInfo (widgetId : Name) (props : Json)
(stx : Syntax) : CoreM Unit := do
let uwd ← evalUserWidgetDefinition widgetId
savePanelWidgetInfo (ToModule.toModule uwd).javascriptHash (pure props) stx
/-! ## Retrieving panel widget instances -/
deriving instance Server.RpcEncodable for WidgetInstance
/-- Retrieve all the `UserWidgetInfo`s that intersect a given line. -/
def widgetInfosAt? (text : FileMap) (t : InfoTree) (hoverLine : Nat) : List UserWidgetInfo :=
t.deepestNodes fun
| _ctx, i@(Info.ofUserWidgetInfo wi), _cs => do
if let (some pos, some tailPos) := (i.pos?, i.tailPos?) then
-- Does the widget's line range contain `hoverLine`?
guard <| (text.utf8PosToLspPos pos).line ≤ hoverLine ∧ hoverLine ≤ (text.utf8PosToLspPos tailPos).line
return wi
else
failure
| _, _, _ => none
structure PanelWidgetInstance extends WidgetInstance where
/-- The syntactic span in the Lean file at which the panel widget is displayed. -/
range? : Option Lsp.Range := none
/-- When present, the infoview will wrap the widget
in `<details><summary>{name}</summary>...</details>`.
This functionality is deprecated
but retained for backwards compatibility
with `UserWidgetDefinition`. -/
name? : Option String := none
deriving Server.RpcEncodable
/-- Output of `getWidgets` RPC.-/
structure GetWidgetsResponse where
widgets : Array PanelWidgetInstance
deriving Server.RpcEncodable
open Lean Server RequestM in
/-- Get the panel widgets present around a particular position. -/
def getWidgets (pos : Lean.Lsp.Position) : RequestM (RequestTask (GetWidgetsResponse)) := do
let doc ← readDoc
let filemap := doc.meta.text
let nextLine := { line := pos.line + 1, character := 0 }
let t := doc.cmdSnaps.waitUntil fun snap => filemap.lspPosToUtf8Pos nextLine ≤ snap.endPos
mapTask t fun (snaps, _) => do
let some snap := snaps.getLast?
| return ⟨∅⟩
runTermElabM snap do
let env ← getEnv
/- Panels from the environment. -/
let ws' ← evalPanelWidgets
let ws' : Array PanelWidgetInstance ← ws'.mapM fun wi => do
-- Check if the definition uses the deprecated `UserWidgetDefinition`
-- on a best-effort basis.
-- If it does, also send the `name` field.
let name? ← env.find? wi.id
|>.filter (·.type.isConstOf ``UserWidgetDefinition)
|>.mapM fun _ => do
let uwd ← evalUserWidgetDefinition wi.id
return uwd.name
return { wi with name? }
/- Panels from the infotree. -/
let ws := widgetInfosAt? filemap snap.infoTree pos.line
let ws : Array PanelWidgetInstance ← ws.toArray.mapM fun (wi : UserWidgetInfo) => do
let name? ← env.find? wi.id
|>.filter (·.type.isConstOf ``UserWidgetDefinition)
|>.mapM fun _ => do
let uwd ← evalUserWidgetDefinition wi.id
return uwd.name
return { wi with range? := String.Range.toLspRange filemap <$> Syntax.getRange? wi.stx, name? }
return { widgets := ws' ++ ws }
builtin_initialize
Server.registerBuiltinRpcProcedure ``getWidgets _ _ getWidgets
attribute [deprecated Module] UserWidgetDefinition
end Lean.Widget