feat: add recharts example

UserWidget/Demos/Plot.lean

@@ -0,0 +1,44 @@
+import UserWidget.ToHtml.Widget
+import UserWidget.Json
+import Std
+
+open Std
+
+open Lean.Widget in
+@[widget]
+def plotter : UserWidgetDefinition where
+  name := "Function plot"
+  javascript := include_str ".." / ".." / "widget" / "dist" / "plot.js"
+
+def fn (t : Float) (x : Float): Float :=
+   1.2 * x - 4 * x * x+ 1 * (x * x * x) + 0.1 * (x * 45 + (t / 100) * 2 * 3.14 ).sin
+
+
+def N := 100
+def data (fn : Float → Float) := List.range (N + 1) |> List.map Float.ofNat |>.toArray
+      |> Array.map (fun x => x / N.toFloat)
+      |> Array.map (fun x => json% {x: $(x), y: $(fn x)})
+      |> Lean.Json.arr
+
+def props := json% {
+  yDomain : [-2, 1],
+  frame_milliseconds: 10,
+  useTimer : true,
+  data: $(
+    List.range 100
+    |> List.map (fun t => data (fn <| t.toFloat))
+    |> List.toArray
+    |> Lean.Json.arr)}
+def props2 := json% {data: $(data (fn 1 ∘ fn 2))}
+#eval props
+
+-- tip: try pinning the widget in the infoview
+-- and then editing the 'fn' above to watch the
+-- plot animate
+#widget plotter props
+
+
+-- kjhk
+
+
+#widget plotter props2

UserWidget/Json.lean

@@ -35,6 +35,21 @@ instance : OfScientific JsonNumber where
 instance : Neg JsonNumber where
   neg jn := ⟨- jn.mantissa, jn.exponent⟩
 
+instance : ToJson Float where
+  toJson x :=
+    let s :=  toString (if x < 0.0 then - x else x)
+    match Lean.Syntax.decodeScientificLitVal? <| s with
+    | none =>
+      match s with
+      | "inf" => "inf" -- [todo] emit a warning
+      | "-inf" => "-inf"
+      | "nan" => "nan"
+      | _ => panic! s!"unhandled float string {s}"
+    | some (m, e, de) =>
+      let j : JsonNumber := OfScientific.ofScientific m e de
+      let j := if x < 0.0 then -j else j
+      Json.num j
+
 syntax "[" jso,* "]" : jso
 syntax "-"? scientific : jso
 syntax "-"? num : jso

lakefile.lean

@@ -36,6 +36,6 @@ def tsxTarget (pkg : Package) (tsxName : String) [Fact (pkg.name = _package.name
 
 target staticHtml (pkg : Package) : FilePath := tsxTarget pkg "staticHtml"
 target squares (pkg : Package) : FilePath := tsxTarget pkg "squares"
+target plot (pkg : Package) : FilePath := tsxTarget pkg "plot"
 
-@[defaultTarget]
 lean_lib UserWidget

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2022-08-09
+leanprover/lean4:nightly-2022-08-12