diff --git a/src/Lean/Data/Parsec.lean b/src/Lean/Data/Parsec.lean index 2cfa540abd..c702dab95c 100644 --- a/src/Lean/Data/Parsec.lean +++ b/src/Lean/Data/Parsec.lean @@ -55,6 +55,11 @@ def attempt (p : Parsec α) : Parsec α := λ it => instance : Alternative Parsec := { failure := fail "", orElse } +protected def run (p : Parsec α) (s : String) : Except String α := + match p s.mkIterator with + | Parsec.ParseResult.success _ res => Except.ok res + | Parsec.ParseResult.error it err => Except.error s!"offset {repr it.i.byteIdx}: {err}" + def expectedEndOfInput := "expected end of input" @[inline] @@ -86,6 +91,7 @@ def manyChars (p : Parsec Char) : Parsec String := manyCharsCore p "" @[inline] def many1Chars (p : Parsec Char) : Parsec String := do manyCharsCore p (←p).toString +/-- Parses the given string. -/ def pstring (s : String) : Parsec String := λ it => let substr := it.extract (it.forward s.length) if substr = s then diff --git a/src/Lean/Elab/InfoTree.lean b/src/Lean/Elab/InfoTree.lean index d5ed0d9e40..f86f96663f 100644 --- a/src/Lean/Elab/InfoTree.lean +++ b/src/Lean/Elab/InfoTree.lean @@ -121,7 +121,7 @@ You can learn about user widgets at `src/Lean/Widget/UserWidget` structure UserWidgetInfo where stx : Syntax /-- Id of `WidgetSource` object to use. -/ - widgetSourceId : Name + widgetId : Name /-- Json representing the props to be loaded in to the component. -/ props : Json deriving Inhabited @@ -299,7 +299,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.widgetSourceId}\n{Std.ToFormat.format info.props}" + f!"UserWidget {info.widgetId}\n{Std.ToFormat.format info.props}" def Info.format (ctx : ContextInfo) : Info → IO Format | ofTacticInfo i => i.format ctx diff --git a/src/Lean/Widget/UserWidget.lean b/src/Lean/Widget/UserWidget.lean index 3c676a2ff5..af971ecb6e 100644 --- a/src/Lean/Widget/UserWidget.lean +++ b/src/Lean/Widget/UserWidget.lean @@ -7,8 +7,8 @@ Authors: E.W.Ayers import Lean.Widget.Basic import Lean.Data.Json import Lean.Environment -import Lean.Elab.Eval import Lean.Server +import Lean.Elab.Eval open Lean @@ -24,51 +24,72 @@ how to use the widgets system. -/ structure WidgetSource where - /-- Unique identifier for the widget. -/ - widgetSourceId : Name /-- Sourcetext of the code to run.-/ sourcetext : String - hash : String := toString <| hash sourcetext deriving Inhabited, ToJson, FromJson -namespace WidgetSource +/-- Use this structure and the `@[widget]` attribute to define your own widgets. -builtin_initialize widgetSourceRegistry : MapDeclarationExtension WidgetSource ← mkMapDeclarationExtension `widgetSourceRegistry +```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 + +structure UserWidget where + id : Name + /-- Pretty name of widget to display to the user.-/ + name : String + javascriptHash: UInt64 + deriving Inhabited, ToJson, FromJson + +private def WidgetSourceRegistry := SimplePersistentEnvExtension + (UInt64 × WidgetSource) + (Std.RBMap UInt64 WidgetSource compare) + +instance : Inhabited (Std.RBMap UInt64 WidgetSource compare) := ⟨∅⟩ +instance : Inhabited (WidgetSourceRegistry) := inferInstanceAs (Inhabited (PersistentEnvExtension _ _ (List _ × _))) + +-- Mapping widgetSourceId to hash of sourcetext +builtin_initialize userWidgetRegistry : MapDeclarationExtension UserWidget ← mkMapDeclarationExtension `widgetRegistry +builtin_initialize widgetSourceRegistry : WidgetSourceRegistry ← + registerSimplePersistentEnvExtension { + name := `widgetSourceRegistry, + 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 attributeImplUnsafe : AttributeImpl where - name := `widgetSource + name := `widget descr := "Mark a string as static code that can be loaded by a widget handler." applicationTime := AttributeApplicationTime.afterCompilation add decl _stx _kind := do let env ← getEnv - let value ← evalConstCheck String ``String decl - setEnv <| widgetSourceRegistry.insert env decl {widgetSourceId := decl, sourcetext := value} + let defn ← evalConstCheck UserWidgetDefinition ``UserWidgetDefinition decl + let javascriptHash := hash defn.javascript + let env := userWidgetRegistry.insert env decl {id := decl, name := defn.name, javascriptHash} + let env := widgetSourceRegistry.addEntry env (javascriptHash, {sourcetext := defn.javascript}) + setEnv <| env @[implementedBy attributeImplUnsafe] opaque attributeImpl : AttributeImpl -/-- Find the WidgetSource for given widget id. -/ -protected def find? (env : Environment) (id : Name) : Option WidgetSource := - widgetSourceRegistry.find? env id - -/-- Returns true if the environment contains the given widget id. -/ -protected def contains (env : Environment) (id : Name) : Bool := - widgetSourceRegistry.contains env id - -open Lean.Server in -/-- Gets the hash of the static javascript string for the given widget id, or throws if -there is no static javascript registered. -/ -def getHash [Monad m] [MonadExcept RequestError m] (env : Environment) (id : Name) : m String := do - let some j := WidgetSource.find? env id - | throw <| RequestError.mk .invalidParams s!"getHash: No source found for {id}." - return j.hash - builtin_initialize registerBuiltinAttribute attributeImpl -end WidgetSource + structure GetWidgetSourceParams where - widgetSourceId : Name + hash: UInt64 pos : Lean.Lsp.TextDocumentPositionParams deriving ToJson, FromJson @@ -79,10 +100,10 @@ open RequestM in def getWidgetSource (args : GetWidgetSourceParams) : RequestM (RequestTask WidgetSource) := RequestM.withWaitFindSnapAtPos args.pos fun snap => do let env := snap.cmdState.env - if let some w := WidgetSource.find? env args.widgetSourceId then + if let some w := widgetSourceRegistry.getState env |>.find? args.hash then return w else - throw <| RequestError.mk .invalidParams s!"No registered user-widget with id {args.widgetSourceId}" + throw <| RequestError.mk .invalidParams s!"No registered user-widget with hash {args.hash}" open Lean Elab @@ -102,15 +123,13 @@ def widgetInfoAt? (text : FileMap) (t : InfoTree) (hoverPos : String.Pos) : List failure | _, _, _ => none -structure UserWidget where - widgetSourceId : Name - hash : String +structure UserWidgetInstance extends UserWidget where props : Json range? : Option Lsp.Range deriving ToJson, FromJson structure GetWidgetsResponse where - widgets : Array UserWidget + widgets : Array UserWidgetInstance deriving ToJson, FromJson open RequestM in @@ -123,20 +142,20 @@ def getWidgets (args : Lean.Lsp.TextDocumentPositionParams) : RequestM (RequestT withWaitFindSnapAtPos args fun snap => do let env := snap.env let ws := widgetInfoAt? filemap snap.infoTree pos - let ws ← ws.toArray.mapM (fun w => do - let hash ← WidgetSource.getHash env w.widgetSourceId + 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 { - widgetSourceId := w.widgetSourceId, - hash := hash, + widget with props := w.props, range? := String.Range.toLspRange filemap <$> Syntax.getRange? w.stx, }) return {widgets := ws} /-- Save a user-widget instance to the infotree. -/ -def saveWidgetInfo [Monad m] [MonadEnv m] [MonadError m] [MonadInfoTree m] (widgetSourceId : Name) (props : Json) (stx : Syntax): m Unit := do +def saveWidgetInfo [Monad m] [MonadEnv m] [MonadError m] [MonadInfoTree m] (widgetId : Name) (props : Json) (stx : Syntax): m Unit := do let info := Info.ofUserWidgetInfo { - widgetSourceId := widgetSourceId, + widgetId := widgetId, props := props, stx := stx, } @@ -146,8 +165,10 @@ def saveWidgetInfo [Monad m] [MonadEnv m] [MonadError m] [MonadInfoTree m] (widg syntax (name := widgetCmd) "#widget " ident term : command -private unsafe def evalJsonUnsafe (stx : Syntax) : TermElabM Json := do - Term.evalTerm Json (mkConst ``Json) stx +open Lean Lean.Meta Lean.Elab Lean.Elab.Term in +private unsafe def evalJsonUnsafe (stx : Syntax) : TermElabM Json := do + let j ← Lean.Elab.Term.evalTerm Json (mkConst ``Json) stx + return j @[implementedBy evalJsonUnsafe] private opaque evalJson (stx : Syntax) : TermElabM Json @@ -158,7 +179,6 @@ open Elab Command in | stx@`(#widget $id:ident $props) => do let props : Json ← runTermElabM none (fun _ => evalJson props) saveWidgetInfo id.getId props stx - return () | _ => throwUnsupportedSyntax end Lean.Widget diff --git a/tests/lean/interactive/run.lean b/tests/lean/interactive/run.lean index e19c62e891..38a3ae0f68 100644 --- a/tests/lean/interactive/run.lean +++ b/tests/lean/interactive/run.lean @@ -1,8 +1,18 @@ import Lean.Data.Lsp +import Lean.Widget open Lean open Lean.Lsp open Lean.JsonRpc +def word : Parsec String := Parsec.many1Chars ( + Parsec.digit <|> Parsec.asciiLetter <|> Parsec.pchar '_' + ) + +def ident : Parsec Name := do + let head ← word + let xs ← Parsec.many1 (Parsec.pchar '.' *> word) + return xs.foldl Name.mkStr $ head + partial def main (args : List String) : IO Unit := do let uri := s!"file://{args.head!}" Ipc.runWith (←IO.appPath) #["--server"] do @@ -28,6 +38,7 @@ partial def main (args : List String) : IO Unit := do let mut lastActualLineNo := 0 let mut versionNo : Nat := 2 let mut requestNo : Nat := 2 + let mut rpcSessionId : Option UInt64 := none for line in text.splitOn "\n" do match line.splitOn "--" with | [ws, directive] => @@ -69,6 +80,58 @@ partial def main (args : List String) : IO Unit := do for diag in diags do IO.eprintln (toJson diag.param) requestNo := requestNo + 1 + | "widgets" => + -- [todo] dedup with RPC + if rpcSessionId.isNone then + Ipc.writeRequest ⟨requestNo, "$/lean/rpc/connect", RpcConnectParams.mk uri⟩ + let r ← Ipc.readResponseAs requestNo RpcConnected + rpcSessionId := some r.result.sessionId + requestNo := requestNo + 1 + let tdpp : TextDocumentPositionParams := {textDocument := {uri := uri}, position := pos } + let ps : RpcCallParams := { + textDocument := {uri := uri}, + position := pos, + sessionId := rpcSessionId.get!, + method := `Lean.Widget.getWidgets, + params := toJson tdpp, + } + Ipc.writeRequest ⟨requestNo, "$/lean/rpc/call", ps⟩ + let response ← Ipc.readResponseAs requestNo Lean.Widget.GetWidgetsResponse + requestNo := requestNo + 1 + IO.eprintln (toJson response.result) + for w in response.result.widgets do + let params : Lean.Widget.GetWidgetSourceParams := { pos := tdpp, hash := w.javascriptHash } + let ps : RpcCallParams := { + ps with + method := `Lean.Widget.getWidgetSource, + params := toJson params, + } + Ipc.writeRequest ⟨requestNo, "$/lean/rpc/call", ps⟩ + let resp ← Ipc.readResponseAs requestNo Lean.Widget.WidgetSource + IO.eprintln (toJson resp.result) + requestNo := requestNo + 1 + | "RPC" => + if rpcSessionId.isNone then + Ipc.writeRequest ⟨requestNo, "$/lean/rpc/connect", RpcConnectParams.mk uri⟩ + let r ← Ipc.readResponseAs requestNo RpcConnected + rpcSessionId := some r.result.sessionId + requestNo := requestNo + 1 + let (method, params) ← liftExcept <| Except.mapError IO.userError <| Lean.Parsec.run (Prod.mk <$> ident <*> Json.Parser.any) params + let tdpp : TextDocumentPositionParams := {textDocument := { uri := uri}, position := pos} + -- hack for getWidgets which needs an explicit pos param. + let params := if method == `Lean.Widget.getWidgets then (toJson tdpp) else params + IO.eprintln (method, params) + let ps : RpcCallParams := { + textDocument := {uri := uri}, + position := pos, + sessionId := rpcSessionId.get!, + method := method, + params := params, + } + Ipc.writeRequest ⟨requestNo, "$/lean/rpc/call", ps⟩ + let response ← Ipc.readResponseAs requestNo Json + IO.eprintln response.result + requestNo := requestNo + 1 | _ => let Except.ok params ← pure <| Json.parse params | throw <| IO.userError s!"failed to parse {params}" diff --git a/tests/lean/interactive/userWidget.lean b/tests/lean/interactive/userWidget.lean new file mode 100644 index 0000000000..96a56240cf --- /dev/null +++ b/tests/lean/interactive/userWidget.lean @@ -0,0 +1,15 @@ +import Lean +open Lean Widget + +@[widget] +def widget1 : UserWidgetDefinition := { + name := "my fancy widget" + javascript:= " + import * as React from 'react'; + export default function (props) { + return React.createElement('p', {}, 'hello') + }" +} + +#widget widget1 (Json.mkObj []) + --^ widgets diff --git a/tests/lean/interactive/userWidget.lean.expected.out b/tests/lean/interactive/userWidget.lean.expected.out new file mode 100644 index 0000000000..a4f41b193d --- /dev/null +++ b/tests/lean/interactive/userWidget.lean.expected.out @@ -0,0 +1,10 @@ +{"widgets": + [{"range": + {"start": {"line": 13, "character": 0}, + "end": {"line": 13, "character": 31}}, + "props": {}, + "name": "my fancy widget", + "javascriptHash": "2248127894", + "id": "widget1"}]} +{"sourcetext": + "\n import * as React from 'react';\n export default function (props) {\n return React.createElement('p', {}, 'hello')\n }"}