#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 に表示させる」ということが可能です。¹

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

/-- ３つ組データを構造体の項に変換する -/
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 }

/-- ２分木の描画情報が与えられたときに、それを 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

/-- ２分木のレイアウト情報が渡されたときに、各ノードのレイアウト位置を一様にずらす -/
def BinTree.shift {β γ : Type} (tree : BinTree (α × β)) (shiftFn : β → γ) : BinTree (α × γ) :=
  (fun (a, pos) => (a, shiftFn pos)) <$> tree

/-- ２分木の描画幅。二分木を描画したときに何グリッド占めるか。 -/
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 さんにご助力をいただきました。 ↩

Lean by Example

#html

コンポーネント紹介

MarkdownDisplay

GraphDisplay

LineChart

使用例