From 8d04ac171da0b59d3802ad6fba9f69fa2b4e511b Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Thu, 21 Dec 2023 07:24:33 +0100 Subject: [PATCH] feat: bundle of widget improvements (#2964) Implements RFC #2963. Leftover tasks: - [x] Provide companion PR to vscode-lean4 (leanprover/vscode-lean4#376) - [x] Companion PR to std4 (leanprover/std4#467) - [x] Companion PR to ProofWidgets4 (leanprover-community/ProofWidgets4#36) - [X] Companion commit to mathlib4 (https://github.com/leanprover-community/mathlib4/commit/0f4660f6552d2a6aaae7adb90a6a3a830cd7fa1c) - [ ] ~~Update the manual chapter~~ (will do in a follow-up) --- doc/examples/widgets.lean | 27 +- src/Lean/Attributes.lean | 2 +- src/Lean/Elab/InfoTree/Main.lean | 2 +- src/Lean/Elab/InfoTree/Types.lean | 17 +- src/Lean/Server/Rpc/Basic.lean | 42 +- src/Lean/Server/Rpc/Deriving.lean | 12 +- src/Lean/Widget/Basic.lean | 1 + src/Lean/Widget/Types.lean | 29 ++ src/Lean/Widget/UserWidget.lean | 488 +++++++++++++----- tests/lean/derivingRpcEncoding.lean | 10 - .../derivingRpcEncoding.lean.expected.out | 10 - tests/lean/interactive/run.lean | 26 +- tests/lean/interactive/userWidget.lean | 45 +- .../interactive/userWidget.lean.expected.out | 47 +- 14 files changed, 553 insertions(+), 205 deletions(-) create mode 100644 src/Lean/Widget/Types.lean diff --git a/doc/examples/widgets.lean b/doc/examples/widgets.lean index 886f7914b6..d69662c994 100644 --- a/doc/examples/widgets.lean +++ b/doc/examples/widgets.lean @@ -15,9 +15,8 @@ sections of a Lean document. User widgets are rendered in the Lean infoview. To try it out, simply type in the following code and place your cursor over the `#widget` command. -/ -@[widget] -def helloWidget : UserWidgetDefinition where - name := "Hello" +@[widget_module] +def helloWidget : Widget.Module where javascript := " import * as React from 'react'; export default function(props) { @@ -25,7 +24,7 @@ def helloWidget : UserWidgetDefinition where return React.createElement('p', {}, name + '!') }" -#widget helloWidget .null +#widget helloWidget /-! If you want to dive into a full sample right away, check out @@ -56,7 +55,11 @@ to the React component. In our first invocation of `#widget`, we set it to `.nul happens when you type in: -/ -#widget helloWidget (Json.mkObj [("name", "")]) +structure HelloWidgetProps where + name? : Option String := none + deriving Server.RpcEncodable + +#widget helloWidget with { name? := "" : HelloWidgetProps } /-! 💡 NOTE: The RPC system presented below does not depend on JavaScript. However the primary use case @@ -132,9 +135,8 @@ on this we either display an `InteractiveCode` with the type, `mapRpcError` the to turn it into a readable message, or show a `Loading..` message, respectively. -/ -@[widget] -def checkWidget : UserWidgetDefinition where - name := "#check as a service" +@[widget_module] +def checkWidget : Widget.Module where javascript := " import * as React from 'react'; const e = React.createElement; @@ -160,7 +162,7 @@ export default function(props) { Finally we can try out the widget. -/ -#widget checkWidget .null +#widget checkWidget /-! ![`#check` as a service](../images/widgets_caas.png) @@ -193,9 +195,8 @@ interact with the text editor. You can see the full API for this [here](https://github.com/leanprover/vscode-lean4/blob/master/lean4-infoview-api/src/infoviewApi.ts#L52) -/ -@[widget] -def insertTextWidget : UserWidgetDefinition where - name := "textInserter" +@[widget_module] +def insertTextWidget : Widget.Module where javascript := " import * as React from 'react'; const e = React.createElement; @@ -213,4 +214,4 @@ export default function(props) { /-! Finally, we can try this out: -/ -#widget insertTextWidget .null +#widget insertTextWidget diff --git a/src/Lean/Attributes.lean b/src/Lean/Attributes.lean index 004d2d8fda..fbf20ad545 100644 --- a/src/Lean/Attributes.lean +++ b/src/Lean/Attributes.lean @@ -330,7 +330,7 @@ private def AttributeExtension.mkInitial : IO AttributeExtensionState := do unsafe def mkAttributeImplOfConstantUnsafe (env : Environment) (opts : Options) (declName : Name) : Except String AttributeImpl := match env.find? declName with - | none => throw ("unknow constant '" ++ toString declName ++ "'") + | none => throw ("unknown constant '" ++ toString declName ++ "'") | some info => match info.type with | Expr.const `Lean.AttributeImpl _ => env.evalConst AttributeImpl opts declName diff --git a/src/Lean/Elab/InfoTree/Main.lean b/src/Lean/Elab/InfoTree/Main.lean index 10ee3eb13b..9b55c386ee 100644 --- a/src/Lean/Elab/InfoTree/Main.lean +++ b/src/Lean/Elab/InfoTree/Main.lean @@ -142,7 +142,7 @@ def MacroExpansionInfo.format (ctx : ContextInfo) (info : MacroExpansionInfo) : return f!"Macro expansion\n{stx}\n===>\n{output}" def UserWidgetInfo.format (info : UserWidgetInfo) : Format := - f!"UserWidget {info.widgetId}\n{Std.ToFormat.format info.props}" + f!"UserWidget {info.id}\n{Std.ToFormat.format <| info.props.run' {}}" def FVarAliasInfo.format (info : FVarAliasInfo) : Format := f!"FVarAlias {info.userName.eraseMacroScopes}" diff --git a/src/Lean/Elab/InfoTree/Types.lean b/src/Lean/Elab/InfoTree/Types.lean index afd685518c..b6b6bbec5a 100644 --- a/src/Lean/Elab/InfoTree/Types.lean +++ b/src/Lean/Elab/InfoTree/Types.lean @@ -9,6 +9,8 @@ import Lean.Data.OpenDecl import Lean.MetavarContext import Lean.Environment import Lean.Data.Json +import Lean.Server.Rpc.Basic +import Lean.Widget.Types namespace Lean.Elab @@ -95,17 +97,12 @@ structure CustomInfo where stx : Syntax value : Dynamic -/-- An info that represents a user-widget. -User-widgets are custom pieces of code that run on the editor client. -You can learn about user widgets at `src/Lean/Widget/UserWidget` --/ -structure UserWidgetInfo where +/-- Information about a user widget associated with a syntactic span. +This must be a panel widget. +A panel widget is a widget that can be displayed +in the infoview alongside the goal state. -/ +structure UserWidgetInfo extends Widget.WidgetInstance where stx : Syntax - /-- Id of `WidgetSource` object to use. -/ - widgetId : Name - /-- Json representing the props to be loaded in to the component. -/ - props : Json - deriving Inhabited /-- Specifies that the given free variables should be considered semantically identical. diff --git a/src/Lean/Server/Rpc/Basic.lean b/src/Lean/Server/Rpc/Basic.lean index 482c266e8b..1edf67a4a2 100644 --- a/src/Lean/Server/Rpc/Basic.lean +++ b/src/Lean/Server/Rpc/Basic.lean @@ -62,18 +62,28 @@ def rpcReleaseRef (r : Lsp.RpcRef) : StateM RpcObjectStore Bool := do else return false -/-- -`RpcEncodable α` means that `α` can be serialized in the RPC system of the Lean server. -This is required when `α` contains fields which should be serialized as an RPC reference -instead of being sent in full. -The type wrapper `WithRpcRef` is used for these fields which should be sent as -a reference. +/-- `RpcEncodable α` means that `α` can be deserialized from and serialized into JSON +for the purpose of receiving arguments to and sending return values from +Remote Procedure Calls (RPCs). -- Any type with `FromJson` and `ToJson` instance is automatically `RpcEncodable`. -- If a type has an `Dynamic` instance, then `WithRpcRef` can be used for its references. -- `deriving RpcEncodable` acts like `FromJson`/`ToJson` but marshalls any `WithRpcRef` fields - as `Lsp.RpcRef`s. --/ +Any type with `FromJson` and `ToJson` instances is `RpcEncodable`. + +Furthermore, types that do not have these instances may still be `RpcEncodable`. +Use `deriving RpcEncodable` to automatically derive instances for such types. + +This occurs when `α` contains data that should not or cannot be serialized: +for instance, heavy objects such as `Lean.Environment`, or closures. +For such data, we use the `WithRpcRef` marker. +Note that for `WithRpcRef α` to be `RpcEncodable`, +`α` must have a `TypeName` instance + +On the server side, `WithRpcRef α` is just a structure +containing a value of type `α`. +On the client side, it is an opaque reference of (structural) type `Lsp.RpcRef`. +Thus, `WithRpcRef α` is cheap to transmit over the network +but may only be accessed on the server side. +In practice, it is used by the client to pass data +between various RPC methods provided by the server. -/ -- TODO(WN): for Lean.js, compile `WithRpcRef` to "opaque reference" on the client class RpcEncodable (α : Type) where rpcEncode : α → StateM RpcObjectStore Json @@ -103,7 +113,15 @@ instance [RpcEncodable α] [RpcEncodable β] : RpcEncodable (α × β) where let (a, b) ← fromJson? j return (← rpcDecode a, ← rpcDecode b) -/-- Marks fields to encode as opaque references in LSP packets. -/ +instance [RpcEncodable α] : RpcEncodable (StateM RpcObjectStore α) where + rpcEncode fn := fn >>= rpcEncode + rpcDecode j := do + let a : α ← rpcDecode j + return return a + +/-- Marks values to be encoded as opaque references in RPC packets. + +See the docstring for `RpcEncodable`. -/ structure WithRpcRef (α : Type u) where val : α deriving Inhabited diff --git a/src/Lean/Server/Rpc/Deriving.lean b/src/Lean/Server/Rpc/Deriving.lean index 32e95ce673..326d8548eb 100644 --- a/src/Lean/Server/Rpc/Deriving.lean +++ b/src/Lean/Server/Rpc/Deriving.lean @@ -42,7 +42,10 @@ private def deriveStructureInstance (indVal : InductiveVal) (params : Array Expr let paramIds ← params.mapM fun p => return mkIdent (← getFVarLocalDecl p).userName - `(structure RpcEncodablePacket where + let indName := mkIdent indVal.name + `(-- Workaround for https://github.com/leanprover/lean4/issues/2044 + namespace $indName + structure RpcEncodablePacket where $[($fieldIds : $fieldTys)]* deriving FromJson, ToJson @@ -55,6 +58,7 @@ private def deriveStructureInstance (indVal : InductiveVal) (params : Array Expr dec j := do let a : RpcEncodablePacket ← fromJson? j return { $[$decInits],* } + end $indName ) private def matchAltTerm := Lean.Parser.Term.matchAlt (rhsParser := Lean.Parser.termParser) @@ -92,7 +96,10 @@ private def deriveInductiveInstance (indVal : InductiveVal) (params : Array Expr let paramIds ← params.mapM fun p => return mkIdent (← getFVarLocalDecl p).userName let typeId ← `(@$(mkIdent indVal.name) $paramIds*) - `(inductive RpcEncodablePacket where + let indName := mkIdent indVal.name + `(-- Workaround for https://github.com/leanprover/lean4/issues/2044 + namespace $indName + inductive RpcEncodablePacket where $[$ctors:ctor]* deriving FromJson, ToJson @@ -107,6 +114,7 @@ private def deriveInductiveInstance (indVal : InductiveVal) (params : Array Expr have inst : RpcEncodable $typeId := { rpcEncode := enc, rpcDecode := dec } let pkt : RpcEncodablePacket ← fromJson? j id <| match pkt with $[$decodes:matchAlt]* + end $indName ) /-- Creates an `RpcEncodablePacket` for `typeName`. For structures, the packet is a structure diff --git a/src/Lean/Widget/Basic.lean b/src/Lean/Widget/Basic.lean index fd0dd3005c..ed0a5827c3 100644 --- a/src/Lean/Widget/Basic.lean +++ b/src/Lean/Widget/Basic.lean @@ -2,6 +2,7 @@ import Lean.Elab.InfoTree import Lean.Message import Lean.Server.Rpc.Basic import Lean.Server.InfoUtils +import Lean.Widget.Types namespace Lean.Widget diff --git a/src/Lean/Widget/Types.lean b/src/Lean/Widget/Types.lean new file mode 100644 index 0000000000..c86199110f --- /dev/null +++ b/src/Lean/Widget/Types.lean @@ -0,0 +1,29 @@ +/- +Copyright (c) 2023 Wojciech Nawrocki. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Authors: Wojciech Nawrocki +-/ +import Lean.Server.Rpc.Basic + +namespace Lean.Widget + +/-- An instance of a widget component: +the identifier of a widget module and the hash of its JS source code +together with props. + +See the [manual entry](https://lean-lang.org/lean4/doc/examples/widgets.lean.html) +for more information about widgets. -/ +structure WidgetInstance where + /-- Name of the `@[widget_module]`. -/ + id : Name + /-- Hash of the JS source of the widget module. -/ + javascriptHash : UInt64 + /-- Arguments to be passed to the component's default exported function. + + Props may contain RPC references, + so must be stored as a computation + with access to the RPC object store. -/ + props : StateM Server.RpcObjectStore Json + +end Lean.Widget diff --git a/src/Lean/Widget/UserWidget.lean b/src/Lean/Widget/UserWidget.lean index f4e3354a71..66f3cbcdad 100644 --- a/src/Lean/Widget/UserWidget.lean +++ b/src/Lean/Widget/UserWidget.lean @@ -2,29 +2,309 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: E.W.Ayers +Authors: E.W.Ayers, Wojciech Nawrocki -/ import Lean.Elab.Eval import Lean.Server.Rpc.RequestHandling -open Lean +namespace Lean.Server +open Elab Command in +/-- Derive `Lean.Server.RpcEncodable` for a type. + +TODO: remove after update-stage0 -/ +elab "#mkrpcenc" n:ident : command => do + elabCommand <| ← `( + namespace $n + deriving instance Lean.Server.RpcEncodable for $n + end $n + ) +end Lean.Server namespace Lean.Widget +open Meta Elab -/-- A custom piece of code that is run on the editor client. +/-- A widget module is a unit of source code that can execute in the infoview. -The editor can use the `Lean.Widget.getWidgetSource` RPC method to -get this object. +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](doc/widgets.md) above this declaration for more information on -how to use the widgets system. +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⟩ + +/-- 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 + } + +private def widgetModuleAttrImpl : AttributeImpl where + name := `widget_module + descr := "Registers a widget module. Its type must implement Lean.Widget.ToModule." + applicationTime := AttributeApplicationTime.afterCompilation + add decl _stx _kind := Prod.fst <$> MetaM.run do + let e ← mkAppM ``ToModule.toModule #[.const decl []] + let mod ← evalModule e + let env ← getEnv + 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 []}." + setEnv <| moduleRegistry.addEntry env (mod.javascriptHash, decl, e) + +builtin_initialize registerBuiltinAttribute widgetModuleAttrImpl + +/-! ## 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 code to run.-/ + /-- Sourcetext of the JS module to run. -/ sourcetext : String deriving Inhabited, ToJson, FromJson +open Server RequestM in +@[server_rpc_method] +def getWidgetSource (args : GetWidgetSourceParams) : RequestM (RequestTask WidgetSource) := do + 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 + +/-! ## 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 [Monad m] [MonadEnv m] [MonadError m] [MonadInfoTree m] + (hash : UInt64) (props : StateM Server.RpcObjectStore Json) (stx : Syntax) : m Unit := do + let env ← getEnv + let some (id, _) := moduleRegistry.getState env |>.find? hash + | 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 []` to mark that `` +should always be displayed, including in downstream modules. + +The type of `` must implement `Widget.ToModule`, +and the type of `` must implement `Server.RpcEncodable`. +In particular, ` : Json` works. + +Use `show_panel_widgets [ with ]` +to specify the `` that the widget should be given +as arguments. + +Use `show_panel_widgets [local (with )?]` to mark it +for display in the current section, namespace, or file only. + +Use `show_panel_widgets [scoped (with )?]` to mark it +for display only when the current namespace is open. + +Use `show_panel_widgets [-]` to temporarily hide a previously shown widget +in the current section, namespace, or file. +Note that persistent erasure is not possible, i.e., +`-` 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 ` to display a panel widget, +and `#widget with ` to display it with the given props. +Useful for debugging widgets. + +The type of `` must implement `Widget.ToModule`, +and the type of `` must implement `Server.RpcEncodable`. +In particular, ` : 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 @@ -42,149 +322,101 @@ structure UserWidgetDefinition where javascript: String deriving Inhabited, ToJson, FromJson -structure UserWidget where - id : Name - /-- Pretty name of widget to display to the user.-/ - name : String - javascriptHash: UInt64 - deriving Inhabited, ToJson, FromJson +instance : ToModule UserWidgetDefinition where + toModule uwd := { uwd with } -private abbrev WidgetSourceRegistry := SimplePersistentEnvExtension - (UInt64 × Name) - (RBMap UInt64 Name compare) - --- Mapping widgetSourceId to hash of sourcetext -builtin_initialize userWidgetRegistry : MapDeclarationExtension UserWidget ← mkMapDeclarationExtension -builtin_initialize widgetSourceRegistry : WidgetSourceRegistry ← - 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 - } - -private unsafe def getUserWidgetDefinitionUnsafe - (decl : Name) : CoreM UserWidgetDefinition := - evalConstCheck UserWidgetDefinition ``UserWidgetDefinition decl - -@[implemented_by getUserWidgetDefinitionUnsafe] -private opaque getUserWidgetDefinition - (decl : Name) : CoreM UserWidgetDefinition - -private def attributeImpl : AttributeImpl where +private def widgetAttrImpl : AttributeImpl where name := `widget - descr := "Mark a string as static code that can be loaded by a widget handler." + descr := "The `@[widget]` attribute has been deprecated, use `@[widget_module]` instead." applicationTime := AttributeApplicationTime.afterCompilation - add decl _stx _kind := do - let env ← getEnv - let defn ← getUserWidgetDefinition decl - let javascriptHash := hash defn.javascript - let env := userWidgetRegistry.insert env decl {id := decl, name := defn.name, javascriptHash} - let env := widgetSourceRegistry.addEntry env (javascriptHash, decl) - setEnv <| env + add := widgetModuleAttrImpl.add -builtin_initialize registerBuiltinAttribute attributeImpl +builtin_initialize registerBuiltinAttribute widgetAttrImpl -/-- Input for `getWidgetSource` RPC. -/ -structure GetWidgetSourceParams where - /-- The hash of the sourcetext to retrieve. -/ - hash: UInt64 - pos : Lean.Lsp.Position - deriving ToJson, FromJson +private unsafe def evalUserWidgetDefinitionUnsafe [Monad m] [MonadEnv m] [MonadOptions m] [MonadError m] + (id : Name) : m UserWidgetDefinition := do + ofExcept <| (← getEnv).evalConstCheck UserWidgetDefinition (← getOptions) ``UserWidgetDefinition id -open Server RequestM in -@[server_rpc_method] -def getWidgetSource (args : GetWidgetSourceParams) : RequestM (RequestTask WidgetSource) := do - let doc ← readDoc - let pos := doc.meta.text.lspPosToUtf8Pos args.pos - let notFound := throwThe RequestError ⟨.invalidParams, s!"No registered user-widget with hash {args.hash}"⟩ - withWaitFindSnap doc (notFoundX := notFound) - (fun s => s.endPos >= pos || (widgetSourceRegistry.getState s.env).contains args.hash) - fun snap => do - if let some id := widgetSourceRegistry.getState snap.env |>.find? args.hash then - runCoreM snap do - return {sourcetext := (← getUserWidgetDefinition id).javascript} - else - notFound +@[implemented_by evalUserWidgetDefinitionUnsafe] +opaque evalUserWidgetDefinition [Monad m] [MonadEnv m] [MonadOptions m] [MonadError m] + (id : Name) : m UserWidgetDefinition -open Lean Elab +/-- Save a user-widget instance to the infotree. + The given `widgetId` should be the declaration name of the widget definition. -/ +@[deprecated savePanelWidgetInfo] def saveWidgetInfo + [Monad m] [MonadEnv m] [MonadError m] [MonadOptions m] [MonadInfoTree m] + (widgetId : Name) (props : Json) (stx : Syntax) : m Unit := do + let uwd ← evalUserWidgetDefinition widgetId + savePanelWidgetInfo (ToModule.toModule uwd).javascriptHash (pure props) stx -/-- - Try to retrieve the `UserWidgetInfo` at a particular position. --/ -def widgetInfosAt? (text : FileMap) (t : InfoTree) (hoverPos : String.Pos) : List UserWidgetInfo := +/-! ## Retrieving panel widget instances -/ + +#mkrpcenc 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 - let trailSize := i.stx.getTrailingSize - -- show info at EOF even if strictly outside token + trail - let atEOF := tailPos.byteIdx + trailSize == text.source.endPos.byteIdx - guard <| pos ≤ hoverPos ∧ (hoverPos.byteIdx < tailPos.byteIdx + trailSize || atEOF) + -- Does the widget's line range contain `hoverLine`? + guard <| (text.utf8PosToLspPos pos).line ≤ hoverLine ∧ hoverLine ≤ (text.utf8PosToLspPos tailPos).line return wi else failure | _, _, _ => none -/-- UserWidget accompanied by component props. -/ -structure UserWidgetInstance extends UserWidget where - /-- Arguments to be fed to the widget's main component. -/ - props : Json - /-- The location of the widget instance in the Lean file. -/ - range? : Option Lsp.Range - deriving ToJson, FromJson +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 `
{name}...
`. + This functionality is deprecated + but retained for backwards compatibility + with `UserWidgetDefinition`. -/ + name? : Option String := none +#mkrpcenc PanelWidgetInstance /-- Output of `getWidgets` RPC.-/ structure GetWidgetsResponse where - widgets : Array UserWidgetInstance - deriving ToJson, FromJson + widgets : Array PanelWidgetInstance +#mkrpcenc GetWidgetsResponse open Lean Server RequestM in -/-- Get the `UserWidget`s present at a particular position. -/ +/-- Get the panel widgets present around a particular position. -/ @[server_rpc_method] -def getWidgets (args : Lean.Lsp.Position) : RequestM (RequestTask (GetWidgetsResponse)) := do +def getWidgets (pos : Lean.Lsp.Position) : RequestM (RequestTask (GetWidgetsResponse)) := do let doc ← readDoc let filemap := doc.meta.text - let pos := filemap.lspPosToUtf8Pos args - withWaitFindSnap doc (·.endPos >= pos) (notFoundX := return ⟨∅⟩) fun snap => do - let env := snap.env - let ws := widgetInfosAt? filemap snap.infoTree pos - let ws ← ws.toArray.mapM (fun (w : UserWidgetInfo) => do - let some widget := userWidgetRegistry.find? env w.widgetId - | throw <| RequestError.mk .invalidParams s!"No registered user-widget with id {w.widgetId}" - return { - widget with - props := w.props - range? := String.Range.toLspRange filemap <$> Syntax.getRange? w.stx - }) - return {widgets := ws} + 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 } -/-- Save a user-widget instance to the infotree. - The given `widgetId` should be the declaration name of the widget definition. -/ -def saveWidgetInfo [Monad m] [MonadEnv m] [MonadError m] [MonadInfoTree m] (widgetId : Name) (props : Json) (stx : Syntax): m Unit := do - let info := Info.ofUserWidgetInfo { - widgetId := widgetId - props := props - stx := stx - } - pushInfoLeaf info - -/-! # Widget command -/ - -/-- Use `#widget ` to display a widget. Useful for debugging widgets. -/ -syntax (name := widgetCmd) "#widget " ident ppSpace term : command - -open Lean Lean.Meta Lean.Elab Lean.Elab.Term in -private unsafe def evalJsonUnsafe (stx : Syntax) : TermElabM Json := - Lean.Elab.Term.evalTerm Json (mkConst ``Json) stx - -@[implemented_by evalJsonUnsafe] -private opaque evalJson (stx : Syntax) : TermElabM Json - -open Elab Command in - -@[command_elab widgetCmd] def elabWidgetCmd : CommandElab := fun - | stx@`(#widget $id:ident $props) => do - let props : Json ← runTermElabM fun _ => evalJson props - saveWidgetInfo id.getId props stx - | _ => throwUnsupportedSyntax +attribute [deprecated Module] UserWidgetDefinition end Lean.Widget diff --git a/tests/lean/derivingRpcEncoding.lean b/tests/lean/derivingRpcEncoding.lean index e2383b903d..4d71d8455a 100644 --- a/tests/lean/derivingRpcEncoding.lean +++ b/tests/lean/derivingRpcEncoding.lean @@ -16,7 +16,6 @@ structure FooRef where a : Array Nat deriving Inhabited, TypeName -#check instTypeNameFooRef #eval test (WithRpcRef FooRef) default structure FooJson where @@ -28,21 +27,18 @@ structure Bar where fooJson : FooJson deriving RpcEncodable, Inhabited -#check instRpcEncodableBar #eval test Bar default structure BarTrans where bar : Bar deriving RpcEncodable, Inhabited -#check instRpcEncodableBarTrans #eval test BarTrans default structure Baz where arr : Array String -- non-constant field deriving RpcEncodable, Inhabited -#check instRpcEncodableBaz #eval test Baz default structure FooGeneric (α : Type) where @@ -50,7 +46,6 @@ structure FooGeneric (α : Type) where b? : Option α deriving RpcEncodable, Inhabited -#check instRpcEncodableFooGeneric #eval test (FooGeneric Nat) default #eval test (FooGeneric Nat) { a := 3, b? := some 42 } @@ -58,7 +53,6 @@ inductive BazInductive | baz (arr : Array Bar) deriving RpcEncodable, Inhabited -#check instRpcEncodableBazInductive #eval test BazInductive ⟨#[default, default]⟩ inductive FooInductive (α : Type) where @@ -66,7 +60,6 @@ inductive FooInductive (α : Type) where | b : (n : Nat) → (a : α) → (m : Nat) → FooInductive α deriving RpcEncodable, Inhabited -#check instRpcEncodableFooInductive #eval test (FooInductive BazInductive) (.a default default) #eval test (FooInductive BazInductive) (.b 42 default default) @@ -80,20 +73,17 @@ inductive FooParam (n : Nat) where | a : Nat → FooParam n deriving RpcEncodable, Inhabited -#check instRpcEncodableFooParam #eval test (FooParam 10) (.a 42) inductive Unused (α : Type) | a deriving RpcEncodable, Inhabited -#check instRpcEncodableUnused structure NoRpcEncodable #eval test (Unused NoRpcEncodable) default structure UnusedStruct (α : Type) deriving RpcEncodable, Inhabited -#check instRpcEncodableUnusedStruct #eval test (UnusedStruct NoRpcEncodable) default deriving instance Repr, RpcEncodable for Empty diff --git a/tests/lean/derivingRpcEncoding.lean.expected.out b/tests/lean/derivingRpcEncoding.lean.expected.out index 19f47d9a02..aac04bcd3e 100644 --- a/tests/lean/derivingRpcEncoding.lean.expected.out +++ b/tests/lean/derivingRpcEncoding.lean.expected.out @@ -1,27 +1,17 @@ -instTypeNameFooRef : TypeName FooRef ok: {"p": "0"} -instRpcEncodableBar : RpcEncodable Bar ok: {"fooRef": {"p": "0"}, "fooJson": {"s": ""}} -instRpcEncodableBarTrans : RpcEncodable BarTrans ok: {"bar": {"fooRef": {"p": "0"}, "fooJson": {"s": ""}}} -instRpcEncodableBaz : RpcEncodable Baz ok: {"arr": []} -instRpcEncodableFooGeneric {α : Type} [inst✝ : RpcEncodable α] : RpcEncodable (FooGeneric α) ok: {"a": 0} ok: {"b": 42, "a": 3} -instRpcEncodableBazInductive : RpcEncodable BazInductive ok: {"baz": {"arr": [{"fooRef": {"p": "0"}, "fooJson": {"s": ""}}, {"fooRef": {"p": "1"}, "fooJson": {"s": ""}}]}} -instRpcEncodableFooInductive {α : Type} [inst✝ : RpcEncodable α] : RpcEncodable (FooInductive α) ok: {"a": [{"baz": {"arr": []}}, {"p": "0"}]} ok: {"b": {"n": 42, "m": 0, "a": {"baz": {"arr": []}}}} ok: {"a": [{"baz": {"arr": []}}, [{"a": [{"baz": {"arr": []}}, []]}]]} -instRpcEncodableFooParam {n : Nat} : RpcEncodable (FooParam n) ok: {"a": 42} -instRpcEncodableUnused {α : Type} : RpcEncodable (Unused α) ok: "a" -instRpcEncodableUnusedStruct {α : Type} : RpcEncodable (UnusedStruct α) ok: {} Except.error "no inductive constructor matched" diff --git a/tests/lean/interactive/run.lean b/tests/lean/interactive/run.lean index 5b56d44f20..26f2272ca6 100644 --- a/tests/lean/interactive/run.lean +++ b/tests/lean/interactive/run.lean @@ -33,6 +33,30 @@ structure InteractiveGoals where end Client +/-! Test-only instances -/ + +instance : FromJson Widget.PanelWidgetInstance where + fromJson? j := do + let id ← j.getObjValAs? Name "id" + let javascriptHash ← j.getObjValAs? UInt64 "javascriptHash" + let props ← j.getObjVal? "props" + let range? ← j.getObjValAs? (Option Lsp.Range) "range" + return { id, javascriptHash, props := pure props, range? } + +deriving instance FromJson for Widget.GetWidgetsResponse + +def Lean.Widget.GetWidgetsResponse.debugJson (r : Widget.GetWidgetsResponse) : Json := + Json.mkObj [ + ("widgets", Json.arr (r.widgets.map fun w => + Json.mkObj [ + ("id", toJson w.id), + ("javascriptHash", toJson w.javascriptHash), + ("props", w.props.run' {}), + ("range", toJson w.range?), + ]) + ) + ] + def word : Parsec String := Parsec.many1Chars <| Parsec.digit <|> Parsec.asciiLetter <|> Parsec.pchar '_' @@ -155,7 +179,7 @@ partial def main (args : List String) : IO Unit := do Ipc.writeRequest ⟨requestNo, "$/lean/rpc/call", ps⟩ let response ← Ipc.readResponseAs requestNo Lean.Widget.GetWidgetsResponse requestNo := requestNo + 1 - IO.eprintln (toJson response.result) + IO.eprintln response.result.debugJson for w in response.result.widgets do let params : Lean.Widget.GetWidgetSourceParams := { pos, hash := w.javascriptHash } let ps : RpcCallParams := { diff --git a/tests/lean/interactive/userWidget.lean b/tests/lean/interactive/userWidget.lean index 96a56240cf..f69fe19668 100644 --- a/tests/lean/interactive/userWidget.lean +++ b/tests/lean/interactive/userWidget.lean @@ -1,15 +1,38 @@ import Lean -open Lean Widget +open Lean -@[widget] -def widget1 : UserWidgetDefinition := { - name := "my fancy widget" - javascript:= " - import * as React from 'react'; - export default function (props) { - return React.createElement('p', {}, 'hello') - }" -} +@[widget_module] +def helloWidget : Widget.Module where + javascript := " + import * as React from 'react'; + export default function(props) { + const name = props.name || 'world' + return React.createElement('p', {}, name + '!') + }" -#widget widget1 (Json.mkObj []) +#widget helloWidget --^ widgets + +structure HelloWidgetProps where + name? : Option String := none + deriving Server.RpcEncodable + +#widget helloWidget with { name? := "lean" : HelloWidgetProps } + --^ widgets + +show_panel_widgets [helloWidget with { name? := "global" : HelloWidgetProps }] + +section +show_panel_widgets [local helloWidget with { name? := "local" : HelloWidgetProps }] +--^ widgets +end + +namespace Foo +show_panel_widgets [scoped helloWidget with { name? := "scoped" : HelloWidgetProps }] +end Foo + +open scoped Foo +--^ widgets + +show_panel_widgets [-helloWidget] +--^ widgets diff --git a/tests/lean/interactive/userWidget.lean.expected.out b/tests/lean/interactive/userWidget.lean.expected.out index 0472f9dac0..df966547fe 100644 --- a/tests/lean/interactive/userWidget.lean.expected.out +++ b/tests/lean/interactive/userWidget.lean.expected.out @@ -1,10 +1,45 @@ {"widgets": [{"range": - {"start": {"line": 13, "character": 0}, - "end": {"line": 13, "character": 31}}, + {"start": {"line": 12, "character": 0}, + "end": {"line": 12, "character": 19}}, "props": {}, - "name": "my fancy widget", - "javascriptHash": "11948876261158841348", - "id": "widget1"}]} + "javascriptHash": "2874772427606622741", + "id": "helloWidget"}]} {"sourcetext": - "\n import * as React from 'react';\n export default function (props) {\n return React.createElement('p', {}, 'hello')\n }"} + "\n import * as React from 'react';\n export default function(props) {\n const name = props.name || 'world'\n return React.createElement('p', {}, name + '!')\n }"} +{"widgets": + [{"range": + {"start": {"line": 19, "character": 0}, + "end": {"line": 19, "character": 63}}, + "props": {"name": "lean"}, + "javascriptHash": "2874772427606622741", + "id": "helloWidget"}]} +{"sourcetext": + "\n import * as React from 'react';\n export default function(props) {\n const name = props.name || 'world'\n return React.createElement('p', {}, name + '!')\n }"} +{"widgets": + [{"range": null, + "props": {"name": "local"}, + "javascriptHash": "2874772427606622741", + "id": "helloWidget"}, + {"range": null, + "props": {"name": "global"}, + "javascriptHash": "2874772427606622741", + "id": "helloWidget"}]} +{"sourcetext": + "\n import * as React from 'react';\n export default function(props) {\n const name = props.name || 'world'\n return React.createElement('p', {}, name + '!')\n }"} +{"sourcetext": + "\n import * as React from 'react';\n export default function(props) {\n const name = props.name || 'world'\n return React.createElement('p', {}, name + '!')\n }"} +{"widgets": + [{"range": null, + "props": {"name": "scoped"}, + "javascriptHash": "2874772427606622741", + "id": "helloWidget"}, + {"range": null, + "props": {"name": "global"}, + "javascriptHash": "2874772427606622741", + "id": "helloWidget"}]} +{"sourcetext": + "\n import * as React from 'react';\n export default function(props) {\n const name = props.name || 'world'\n return React.createElement('p', {}, name + '!')\n }"} +{"sourcetext": + "\n import * as React from 'react';\n export default function(props) {\n const name = props.name || 'world'\n return React.createElement('p', {}, name + '!')\n }"} +{"widgets": []}