Components & presentations

.vscode/settings.json

@@ -0,0 +1,11 @@
+{
+  "editor.insertSpaces": true,
+  "editor.tabSize": 2,
+  "editor.rulers" : [100],
+  "files.encoding": "utf8",
+  "files.eol": "\n",
+  "files.insertFinalNewline": true,
+  "files.trimFinalNewlines": true,
+  "files.trimTrailingWhitespace": true,
+  "search.usePCRE2": true
+}

WidgetKit/Compat.lean

@@ -0,0 +1,165 @@
+import Lean.Attributes
+import Lean.Widget.UserWidget
+
+import WidgetKit.Data.Json
+
+/-!
+A compatibility layer aimed at redefining the user widget API in terms of modules and components.
+New features:
+- component props have Lean types
+- props can be RpcEncodable
+- we distinguish between an arbitrary 'widget module' (any ES module) and a 'widget component',
+  that is a module which can be rendered
+- moreover only 'panel widget components' can appear as top-level panels in the infoview
+
+TODO: If the design works out, it could replace the current Lean core definitions.
+-/
+
+namespace WidgetKit
+open Lean Server Elab
+
+deriving instance TypeName for LocalContext
+deriving instance TypeName for Elab.ContextInfo
+deriving instance TypeName for Expr
+
+abbrev LazyEncodable α := StateM RpcObjectStore α
+
+instance : RpcEncodable (LazyEncodable Json) where
+  rpcEncode fn := fn
+  rpcDecode j := return return j
+
+-- back from exile
+structure ExprWithCtx where
+  ci : Elab.ContextInfo
+  lctx : LocalContext
+  expr : Expr
+  deriving TypeName
+
+def ExprWithCtx.runMetaM (e : ExprWithCtx) (x : Expr → MetaM α) : IO α :=
+  e.ci.runMetaM e.lctx (x e.expr)
+
+def ExprWithCtx.save (e : Expr) : MetaM ExprWithCtx :=
+  return {
+    ci := ← ContextInfo.save
+    lctx := ← getLCtx
+    expr := e
+  }
+
+def widgetDefPostfix : Name := `userWidgetDef
+
+-- NOTE: Compared to core, this is almost like UserWidgetDefinition but with a different "attitude":
+-- the module itself need not be a user widget, i.e. it can also be a support library. It doesn't
+-- need a displayable `name`.
+structure Module where
+  /-- An arbitrary JS [module](https://developer.mozilla.org/en-US/docs/Web/JavaScript/Guide/Modules)
+  intended for use in user widgets. -/
+  javascript: String
+
+-- This could maybe be a macro but good luck actually writing it.
+open Lean Meta Elab Command in
+initialize
+  registerBuiltinAttribute {
+    name := `widget_module
+    descr := "Registers a widget module. Its type must extend WidgetKit.Module."
+    applicationTime := AttributeApplicationTime.afterCompilation
+    -- The implementation is a hack due to the fact that widgetSource is tied to the storage
+    -- of user widgets. I think a single widgetModuleRegistry should suffice. TODO fix in core.
+    add := fun nm _ _ => do
+      -- The type is not checked; really we just need it to have a `javascript : String` field.
+      let proc : CommandElabM Unit := do
+        elabCommand <| ← `(command|
+          @[widget]
+          def $(mkIdent <| nm ++ widgetDefPostfix) : Lean.Widget.UserWidgetDefinition where
+            name := $(quote nm.toString)
+            javascript := $(mkIdent nm).javascript)
+      let ctx ← read
+      let st ← get
+      -- Cursed manual CommandElabM => CoreM lift punning all fields
+      let (_, st') ← proc.run { st, ctx with tacticCache? := none } |>.run { st, ctx with }
+      set { st' with : Core.State }
+  : AttributeImpl }
+
+-- "goal widget"/"at cursor widget"/"panel widget"/"info block widget"
+structure PanelWidgetInfo where
+  /-- Name of the `widget_module` to show. -/
+  id : Name
+  props : LazyEncodable Json
+  -- Compatibility hack. Remove if in core.
+  infoId : Name
+  deriving TypeName
+
+/-- A widget component with a resolved source hash and its props. -/
+structure WidgetInstance where
+  /-- Name of the `widget_module`. -/
+  id : Name
+  srcHash : UInt64
+  props : LazyEncodable Json
+  -- Compatibility hack. Remove if in core.
+  infoId : Name
+  deriving Server.RpcEncodable
+
+structure PanelWidgetInstance extends WidgetInstance where
+  range? : Option Lsp.Range
+  deriving Server.RpcEncodable
+
+structure GetPanelWidgetsParams where
+  pos : Lsp.Position
+  deriving FromJson, ToJson
+
+structure GetPanelWidgetsResponse where
+  widgets : Array PanelWidgetInstance
+  deriving Server.RpcEncodable
+
+def customInfosAt? (text : FileMap) (t : InfoTree) (hoverPos : String.Pos) : List CustomInfo :=
+  t.deepestNodes fun
+    | _ctx, i@(Info.ofCustomInfo ci), _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)
+        return ci
+      else
+        failure
+    | _, _, _ => none
+
+open RequestM in
+@[server_rpc_method]
+def getPanelWidgets (args : GetPanelWidgetsParams) : RequestM (RequestTask GetPanelWidgetsResponse) := do
+  let doc ← readDoc
+  let filemap := doc.meta.text
+  let pos := filemap.lspPosToUtf8Pos args.pos
+  withWaitFindSnap doc (·.endPos >= pos) (notFoundX := return ⟨∅⟩) fun snap => do
+    let ws := customInfosAt? filemap snap.infoTree pos
+    let ws ← ws.toArray.mapM (fun (w : CustomInfo) => do
+      let some wi := w.value.get? PanelWidgetInfo
+        | throw <| RequestError.invalidParams "Oops! Unknown ofCustomInfo found. TODO add kinds"
+      let some widgetDef := Widget.userWidgetRegistry.find? snap.env (wi.id ++ widgetDefPostfix)
+        | throw <| RequestError.invalidParams s!"No registered widget source with id {wi.id}"
+      return {
+        wi with
+        srcHash := widgetDef.javascriptHash
+        range? := String.Range.toLspRange filemap <$> Syntax.getRange? w.stx
+      })
+    return {widgets := ws}
+
+@[widget]
+def metaWidget : Lean.Widget.UserWidgetDefinition where
+  name := "We should get rid of this header and make panels general block elements"
+  javascript := include_str ".." / "widget" / "dist" / "compat.js"
+
+open scoped Json in
+def savePanelWidgetInfo [Monad m] [MonadInfoTree m] [MonadNameGenerator m]
+    (stx : Syntax) (id : Name) (props : LazyEncodable Json)  : m Unit := do
+  let infoId := `panelWidget ++ (← mkFreshId)
+  pushInfoLeaf <| .ofUserWidgetInfo {
+    stx
+    widgetId := ``metaWidget
+    props := json% {
+      infoId : $(infoId)
+    }
+  }
+  let wi : PanelWidgetInfo := { id, props, infoId }
+  pushInfoLeaf <| .ofCustomInfo { stx, value := Dynamic.mk wi }
+
+end WidgetKit

WidgetKit/Component/Basic.lean

@@ -0,0 +1,54 @@
+import Lean.Widget.InteractiveCode
+import WidgetKit.Compat
+
+namespace WidgetKit
+
+/-- A widget module whose `default` export is a
+[React component](https://reactjs.org/docs/components-and-props.html). It must be annotated with
+`@[widget_module]` to work.
+
+## Lean encoding of props
+
+`Props` is expected to have a `Lean.Server.RpcEncodable` instance. The export should then have type
+`function(props: JsProps & { pos : DocumentPosition }): React.ReactNode` where `JsProps` is the JSON
+encoding of `Props` and `DocumentPosition` is defined in `@leanprover/infoview`. -/
+structure Component (Props : Type) extends Module
+
+open Lean
+
+structure InteractiveCodeProps where
+  fmt : Widget.CodeWithInfos
+  deriving Server.RpcEncodable
+
+@[widget_module]
+def InteractiveCode : Component InteractiveCodeProps where
+  javascript := "
+    import { InteractiveCode } from '@leanprover/infoview'
+    import * as React from 'react'
+    export default function(props) {
+      return React.createElement(InteractiveCode, props)
+    }"
+
+structure InteractiveExprProps where
+  expr : Server.WithRpcRef ExprWithCtx
+  deriving Server.RpcEncodable
+
+@[server_rpc_method]
+def ppExprTagged : InteractiveExprProps → Server.RequestM (Server.RequestTask Widget.CodeWithInfos)
+  | ⟨⟨expr⟩⟩ => Server.RequestM.asTask <| expr.runMetaM Widget.ppExprTagged
+
+/-- Pretty-print and present a `Lean.Expr` as interactive text.
+
+If you are producing a `Component`in a `MetaM` context where `Widget.ppExprTagged` can be used
+directly, it is preferrable to use that and the `InteractiveCode` component instead. This avoids
+one extra roundtrip to make the RPC call. -/
+@[widget_module]
+def InteractiveExpr : Component InteractiveExprProps where
+  javascript := include_str ".." / ".." / "widget" / "dist" / "interactiveExpr.js"
+
+/-- A panel widget is a component which can appear as a top-level panel in the infoview. A goal
+state display is one example. -/
+-- TODO: This is in `userWidget.tsx`
+structure PanelWidgetProps where
+
+end WidgetKit

WidgetKit/Component/HtmlDisplay.lean

@@ -0,0 +1,48 @@
+import Lean.Server.Rpc.Basic
+
+import WidgetKit.Data.Html
+
+namespace WidgetKit
+open Lean Server
+
+structure HtmlDisplayProps where
+  html : EncodableHtml
+  deriving RpcEncodable
+
+@[widget_module]
+def HtmlDisplay : Component HtmlDisplayProps where
+  javascript := include_str ".." / ".." / "widget" / "dist" / "htmlDisplay.js"
+
+open Elab in
+unsafe def evalEncodableHtmlUnsafe (stx : Term) : TermElabM EncodableHtml := do
+  let htmlT := mkConst ``EncodableHtml
+  Term.evalTerm EncodableHtml htmlT stx
+
+open Elab in
+@[implemented_by evalEncodableHtmlUnsafe]
+opaque evalEncodableHtml : Term → TermElabM EncodableHtml
+
+syntax (name := htmlCmd) "#html " term : command
+
+open Elab Command Json in
+@[command_elab htmlCmd]
+def elabHtmlCmd : CommandElab := fun
+  | stx@`(#html $t:term) =>
+    runTermElabM fun _ => do
+      let ht ← evalEncodableHtml <| ← `(WidgetKit.EncodableHtml.ofHtml $t)
+      savePanelWidgetInfo stx ``HtmlDisplay do
+        return json% { html: $(← rpcEncode ht) }
+  | stx => throwError "Unexpected syntax {stx}."
+
+syntax (name := htmlTac) "html! " term : tactic
+
+open Elab Tactic Json in
+@[tactic htmlTac]
+def elabHtmlTac : Tactic
+  | stx@`(tactic| html! $t:term) => do
+    let ht ← evalEncodableHtml <| ← `(WidgetKit.EncodableHtml.ofHtml $t)
+    savePanelWidgetInfo stx ``HtmlDisplay do
+      return json% { html: $(← rpcEncode ht) }
+  | stx => throwError "Unexpected syntax {stx}."
+
+end WidgetKit

WidgetKit/InteractiveSvg.lean → WidgetKit/Component/InteractiveSvg.lean

@@ -1,12 +1,9 @@
-import Lean.Elab
+import WidgetKit.Data.Svg
 
-import WidgetKit.Svg
+namespace WidgetKit
+open Lean
 
-open Lean.Widget.Jsx
-open Lean Widget
-
-
-private def Float.toInt (x : Float) : Int :=
+private def _root_.Float.toInt (x : Float) : Int :=
   if x >= 0 then
     x.toUInt64.toNat
   else
@@ -27,7 +24,7 @@ structure Action where
   data : Option Json
   deriving ToJson, FromJson
 
-/-- The input type `State` is any state the user wants to use and update 
+/-- The input type `State` is any state the user wants to use and update
 
 SvgState in addition automatically handles tracking of time, selection and custom data -/
 structure SvgState (State : Type) where
@@ -36,7 +33,7 @@ structure SvgState (State : Type) where
   selected : Option String
   mousePos : Option (Int × Int)
   idToData : List (String × Json)
-deriving ToJson, FromJson
+deriving ToJson, FromJson, Server.RpcEncodable
 
 structure UpdateParams (State : Type) where
   elapsed : Float
@@ -46,24 +43,24 @@ structure UpdateParams (State : Type) where
   deriving ToJson, FromJson
 
 structure UpdateResult (State : Type) where
-  html : Widget.Html
+  html : EncodableHtml
   state : SvgState State
   /-- Approximate number of milliseconds to wait before calling again. -/
   callbackTime : Option Float := some 33
-  deriving ToJson, FromJson
+  deriving Server.RpcEncodable
 
 -- maybe add title, refresh rate, initial time?, custom selection rendering
 structure InteractiveSvg (State : Type) where
   init : State
   frame : Svg.Frame
-  update (time_ms Δt_ms : Float) (action : Action) 
-         (mouseStart mouseEnd : Option (Svg.Point frame)) 
+  update (time_ms Δt_ms : Float) (action : Action)
+         (mouseStart mouseEnd : Option (Svg.Point frame))
          (selectedId : Option String) (getSelectedData : (α : Type) → [FromJson α] → Option α)
          : State → State
   render (time_ms : Float) (mouseStart mouseEnd : Option (Svg.Point frame)) : State → Svg frame
 
-open Server RequestM in
-def InteractiveSvg.serverRpcMethod {State : Type} (isvg : InteractiveSvg State) (params : UpdateParams State) 
+open Server RequestM Jsx in
+def InteractiveSvg.serverRpcMethod {State : Type} (isvg : InteractiveSvg State) (params : UpdateParams State)
   : RequestM (RequestTask (UpdateResult State)) := do
 
   -- Ideally, each action should have time and mouse position attached
@@ -76,14 +73,14 @@ def InteractiveSvg.serverRpcMethod {State : Type} (isvg : InteractiveSvg State)
   let mut state := params.state.state
   let mut selected := params.state.selected
 
-  let getData := λ (α : Type) [FromJson α] => do 
-    let id ← selected; 
+  let getData := λ (α : Type) [FromJson α] => do
+    let id ← selected;
     let data ← idToData[id]
     match fromJson? (α:=α) data with
     | .error _ => none
     | .ok val => some val
 
-  
+
   let mouseStart := params.state.mousePos.map λ (i,j) => (i, j)
   let mouseEnd := params.mousePos.map λ (x,y) => (x.toInt, y.toInt)
 
@@ -103,9 +100,9 @@ def InteractiveSvg.serverRpcMethod {State : Type} (isvg : InteractiveSvg State)
     time := time + Δt
 
   let mut svg := isvg.render time mouseStart mouseEnd state
-  
-  let svgState : SvgState State := 
-    { state := state 
+
+  let svgState : SvgState State :=
+    { state := state
       time := params.elapsed
       selected := selected
       mousePos := mouseEnd.map λ p => p.toPixels
@@ -119,7 +116,7 @@ def InteractiveSvg.serverRpcMethod {State : Type} (isvg : InteractiveSvg State)
 
 
   return RequestTask.pure {
-    html :=
+    html := EncodableHtml.ofHtml
       <div>
         {svg.toHtml}
       </div>,
@@ -128,4 +125,4 @@ def InteractiveSvg.serverRpcMethod {State : Type} (isvg : InteractiveSvg State)
   }
 
 end Svg
-
+end WidgetKit