#html
#html コマンドは、その名の通り html をインフォビューに表示させるコマンドです。ProofWidgets4 というライブラリで定義されています。
JSX によく似た構文を使うことができます。
import ProofWidgets
-- JSX ライクな構文が使えるようにする
open scoped ProofWidgets.Jsx
#html <p>"ここに HTML を書きます"</p>
-- いろんなHTMLタグを書くことができる
#html
<div>
<h3>"見出し"</h3>
<p>
<b>"強調されたテキスト"</b>
<i>"斜体のテキスト"</i>
</p>
<a href="https://lean-lang.org/">"リンク"</a>
</div>
-- 画像も表示できる
#html
<img src={"https://upload.wikimedia.org/wikipedia/commons/6/6a/Julia-set_N_z3-1.png"}
alt="julia set"/>
コンポーネント紹介
HTMLタグを使用できるだけでなく、様々なコンポーネントが定義されています。
MarkdownDisplay
<MarkdownDisplay /> コンポーネントを使用すると、Markdown や TeX を表示させることができます。
import ProofWidgets
open ProofWidgets Jsx
-- Markdown と TeX を表示する
#html <MarkdownDisplay contents={"
## Riemann zeta function
The Riemann zeta function is defined as
$$
\\zeta(s) = \\sum_{n=1}^∞ \\frac{1}{n^s}
$$
for $\\mathrm{Re} (s) > 0$.
"}/>
GraphDisplay
<GraphDisplay /> コンポーネントを使用すると、有向グラフを表示させることができます。
import ProofWidgets
open ProofWidgets Jsx GraphDisplay
/-- `Edge` を作る -/
def mkEdge (st : String × String) : Edge := {source := st.1, target := st.2}
/-- 文字列として与えられたラベルから `Vertex` を作る -/
def mkVertex (id : String) : Vertex := {id := id}
-- 有向グラフを表示する
#html
<GraphDisplay
vertices={#["a", "b", "c", "d", "e"].map mkVertex}
edges={#[("a", "b"), ("b", "c"), ("c", "d"), ("d", "e"), ("e", "a")].map mkEdge}
/>
LineChart
ProofWidgets4 には Recharts ライブラリ に対するサポートがあり、<LineChart /> コンポーネントを使用すると、関数のグラフを表示させることができます。
import ProofWidgets
open Lean ProofWidgets Recharts
open scoped Jsx
/-- 与えられた関数 `fn` の `[0, 1]` 区間上での値のグラフ -/
def Plot (fn : Float → Float) (steps := 100) : Html :=
-- `[0, 1)` 区間を `steps` 個に分割する
let grids := Array.range steps
|>.map (fun x => x.toFloat / steps.toFloat)
-- データを JSON に変換
let y := grids.map fn
let jsonData : Array Json := grids.zip y
|>.map (fun (x,y) => json% {x: $(toJson x), y: $(toJson y)});
<LineChart width={400} height={400} data={jsonData}>
<XAxis dataKey?="x" />
<YAxis dataKey?="y" />
<Line type={.monotone} dataKey="y" stroke="#8884d8" dot?={Bool.false} />
</LineChart>
#html Plot (fun x => (x - 0.3) ^ 2 + 0.1)
#html Plot (fun x => 0.2 + 0.5 * Float.sin (7 * x))
使用例
#html コマンドを使うと SVG 画像を infoview 内で直接表示させることができるという点、さらに ProofWidgets が SVG 画像の作成をある程度サポートしているという点を利用すると、「二分木を画像として infoview に表示させる」ということが可能です。1
import ProofWidgets
open ProofWidgets Svg
/-- デフォルトの表示領域(Frame) -/
private def defaultFrame : Frame := {
xmin := 0 -- 左下隅の x 座標
ymin := 0 -- 左下隅の y 座標
width := 1000 -- 横方向のピクセル数
height := 1000 -- 縦方向のピクセル数
xSize := 1000 -- width と同じ値なので、ピクセル数と座標の値は一致
}
/-- 描画に関する設定 -/
structure RenderConfig where
/-- ノードを描画するときの円の半径 -/
radius : Nat := 16
/-- ノードを描画するときの円の塗りつぶし色(RGB) -/
fillColor : (Float × Float × Float) := (0.74, 0.87, 1.0)
/-- ノードのラベルのフォントサイズ -/
fontsize : Nat := 14
/-- ノードのラベルの色(RGB) -/
textColor : (Float × Float × Float) := (0.0, 0.0, 0.0)
/-- エッジの色(RGB) -/
edgeColor : (Float × Float × Float) := (50.0, 50.0, 50.0)
/-- エッジの太さ(ピクセル) -/
edgeWidth : Nat := 2
/-- ノード間の水平・垂直間隔の基準値 -/
step := 30.0
/-- `RenderConfig`を読み取りできる計算文脈を表すモナド -/
abbrev RenderM := ReaderM RenderConfig
/-- 位置情報を付加したノードのデータ -/
structure NodePos where
/-- ノードのx座標(右に行くほど大きい) -/
x : Float
/-- ノードのy座標(下に行くほど大きい) -/
y : Float
/-- ラベル -/
label : String
/-- 上面と下面を反転して計測したy座標 -/
private def NodePos.y_inv (self : NodePos) (f : Frame) : Float :=
f.height.toFloat - self.y
/-- ノード(円とラベル)を作成する -/
private def createNodeElements (node : NodePos) (f : Frame) : RenderM (Array (Element f)) := do
let radius := (← read).radius
let fillColor := (← read).fillColor
let fontsize := (← read).fontsize
let textColor := (← read).textColor
let circle := circle (node.x, node.y_inv f) (.px radius)
|>.setFill fillColor
let adjust := fontsize.toFloat * 0.35 -- ラベルの位置調整用
let text := text (node.x - adjust, node.y_inv f - adjust) node.label (.px fontsize)
|>.setFill textColor
return #[circle, text]
/-- ノードの描画テスト用の関数 -/
private def createNodeHtml (node : NodePos) (f : Frame) : RenderM Html := do
let elements ← createNodeElements node f
let svg : Svg f := { elements := elements }
return svg.toHtml
#html ReaderT.run (r := {}) <|
createNodeHtml (f := defaultFrame) (node := { x := 150, y := 30, label := "A" })
/-- エッジ(ノードの親子関係)を作成する -/
private def createEdgeElement (parent child : NodePos) (f : Frame) : RenderM (Element f) := do
let edgeColor := (← read).edgeColor
let edgeWidth := (← read).edgeWidth
let element := line (parent.x, parent.y_inv f) (child.x, child.y_inv f)
|>.setStroke edgeColor (.px edgeWidth)
return element
/-- エッジの描画テスト用の関数 -/
private def createEdgeHtml (parent child : NodePos) (f : Frame) : RenderM Html := do
let element ← createEdgeElement parent child f
let svg : Svg f := { elements := #[element] }
return svg.toHtml
#html ReaderT.run (r := {}) <| createEdgeHtml
(parent := { x := 150, y := 30, label := "A" })
(child := { x := 100, y := 80, label := "B" })
(f := defaultFrame)
/-- (ラベル付きの)二分木 -/
inductive BinTree (α : Type) where
/-- 空の木 -/
| empty
/-- ノード -/
| node (val : α) (left right : BinTree α)
variable {α : Type} [ToString α]
/-- 二分木をノードの配列に変換する。 -/
def BinTree.toNodes (tree : BinTree α) : Array α :=
match tree with
| .empty => #[]
| .node val left right => #[val] ++ (left.toNodes ++ right.toNodes)
/-- 二分木のエッジを配列にする。(親, 子) のペアにして返すことに注意。 -/
def BinTree.toEdges {β : Type} (tree : BinTree β) : Array (β × β) :=
match tree with
| .empty => #[]
| .node a left right =>
let leftEdges :=
match left with
| .empty => #[]
| .node b _ _ => (toEdges left).push (a, b)
let rightEdges :=
match right with
| .empty => #[]
| .node c _ _ => (toEdges right).push (a, c)
leftEdges ++ rightEdges
/-- 3つ組データを構造体の項に変換する -/
def NodePos.ofPair (p : α × Nat × Nat) (step : Float) : NodePos :=
let (label, x, y) := p
{ x := x.toFloat * step, y := y.toFloat * step, label := toString label }
/-- 2分木の描画情報が与えられたときに、それを SVG 画像として描画する -/
def BinTree.render (tree : BinTree (α × (Nat × Nat))) (f : Frame := defaultFrame) (cfg : RenderConfig := {}) : Html :=
let html : RenderM Html := do
let step := (← read).step
let nodesArray := (← tree.toNodes
|>.map (NodePos.ofPair (step := step))
|>.mapM (fun node => createNodeElements node f))
|>.flatten
let edgesArray ← tree.toEdges
|>.map (fun (x1, x2) => (NodePos.ofPair x1 step, NodePos.ofPair x2 step))
|>.mapM (fun (parent, child) => createEdgeElement parent child f)
let svg : Svg f := { elements := edgesArray ++ nodesArray }
return svg.toHtml
ReaderT.run html cfg
/-- 二分木の葉 -/
def BinTree.leaf (val : α) : BinTree α :=
.node val .empty .empty
-- 二分木の描画テスト
-- レイアウト情報を手動で与えて描画している
#html
let treeLayout := BinTree.node ("A", (2, 1))
(.leaf ("B", (1, 2)))
(.node ("C", (4, 2))
(.leaf ("D", (3, 3)))
(.leaf ("E", (5, 3))))
BinTree.render treeLayout
/-- 2分木の各要素に一様に関数を適用する -/
def BinTree.map {α β : Type} (f : α → β) (tree : BinTree α) : BinTree β :=
match tree with
| .empty => .empty
| .node val left right =>
.node (f val) (map f left) (map f right)
/-- `BinTree`は関手 -/
instance : Functor BinTree where
map := BinTree.map
/-- 2分木のレイアウト情報が渡されたときに、各ノードのレイアウト位置を一様にずらす -/
def BinTree.shift {β γ : Type} (tree : BinTree (α × β)) (shiftFn : β → γ) : BinTree (α × γ) :=
(fun (a, pos) => (a, shiftFn pos)) <$> tree
/-- 2分木の描画幅。二分木を描画したときに何グリッド占めるか。 -/
def BinTree.width (tree : BinTree α) : Nat :=
tree.toNodes.size - 1
/-- 二分木のレイアウトを計算する関数 -/
def BinTree.layout (tree : BinTree α) : BinTree (α × (Nat × Nat)) :=
match tree with
| .empty => .empty
| .node a .empty .empty =>
.node (a, (1, 1)) .empty .empty
| .node a .empty right =>
let rightLayout := layout right
let rightShifted := rightLayout.shift (fun (x, y) => (x + 1, y + 1))
.node (a, (1, 1)) .empty rightShifted
| .node a left .empty =>
let leftLayout := layout left
let leftShifted := leftLayout.shift (fun (x, y) => (x, y + 1))
.node (a, (left.width + 2) * 1, 1) leftShifted .empty
| .node a left right =>
let leftLayout := layout left
let rightLayout := layout right
let leftShifted := leftLayout.shift (fun (x, y) => (x, y + 1))
let rightShifted := rightLayout.shift (fun (x, y) => (x + (left.width + 2) * 1, y + 1))
.node (a, ((left.width + 2) * 1, 1)) leftShifted rightShifted
-- 二分木の描画テスト
-- 二分木からレイアウト情報を計算し、それを元に描画している
#html
let tree := BinTree.node "A"
(BinTree.leaf "B")
(BinTree.node "C"
(BinTree.leaf "D")
(BinTree.leaf "E"))
BinTree.render tree.layout
-
この例を作成するにあたり、lean-ja Discord サーバーで todaymint さんにご助力をいただきました。 ↩