render-dynkin.lean

import algebra.lie.cartan_matrix

open widget

variables {α : Type}

namespace svg

meta def fill : string → attr α
| s := attr.val "fill" $ s

meta def stroke : string → attr α
| s := attr.val "stroke" $ s

meta def circle.cx : string → attr α
| s := attr.val "cx" $ s

meta def circle.cy : string → attr α
| s := attr.val "cy" $ s

meta def circle.r : string → attr α
| s := attr.val "r" $ s

meta def line.x1 : string → attr α
| s := attr.val "x1" $ s

meta def line.x2 : string → attr α
| s := attr.val "x2" $ s

meta def line.y1 : string → attr α
| s := attr.val "y1" $ s

meta def line.y2 : string → attr α
| s := attr.val "y2" $ s

end svg

namespace matrix

variables {n : ℕ} (A : matrix (fin n) (fin n) ℤ)

include A

def nat_index (i j : ℕ) : ℤ := if h : i < n ∧ j < n then A ⟨i, h.1⟩ ⟨j, h.2⟩ else 999

/-- TODO Delete me once `get_node_pos` smart enough to infer layout from values in `A`. -/
def get_node_pos_E : ℕ → ℕ × ℕ
| 0     := ⟨0, 0⟩
| 1     := ⟨2, 1⟩
| (i+1) := ⟨i, 0⟩

/-- TODO Use `A` to infer sensible layout. -/
def get_node_pos : ℕ → ℕ × ℕ := if n < 6 then (λ i, ⟨i, 0⟩) else A.get_node_pos_E

def get_node_cx (i : ℕ) : ℤ := 40 + (A.get_node_pos i).1 * 80

def get_node_cy (i : ℕ) : ℤ := 40 + (A.get_node_pos i).2 * 80

meta def get_node_html (i : ℕ) : html α :=
h "circle" [
  svg.circle.cx $ to_string $ A.get_node_cx i,
  svg.circle.cy $ to_string $ A.get_node_cy i,
  svg.circle.r "10",
  svg.fill "white",
  svg.stroke "black"
] []

/-- TODO
 * Error if `j ≤ i`
 * Error if `(A i j, A j i) ∉ [((0 : ℤ), (0 : ℤ)), (-1, -1), (-1, -2), (-2, -1), (-1, -3), (-3, -1)]`
 * Render `(A i j) * (A j i)` edges
 * Render arrow on double or triple edge with direction decided by `A i j < A j i` -/
meta def get_edge_html : ℕ × ℕ → list (html α) :=
function.uncurry $ λ i j, if A.nat_index i j = 0 then [] else
[h "line" [
  svg.line.x1 $ to_string $ A.get_node_cx i,
  svg.line.y1 $ to_string $ A.get_node_cy i,
  svg.line.x2 $ to_string $ A.get_node_cx j,
  svg.line.y2 $ to_string $ A.get_node_cy j,
  svg.fill "black",
  svg.stroke "black"
] []]

meta def get_nodes_html : list (html α) := (list.range n).map A.get_node_html

meta def get_edges_html : list (html α) :=
list.foldl list.append [] $
list.map A.get_edge_html $
list.filter (λ (ij : ℕ × ℕ), ij.1 < ij.2) $
list.product (list.range n) (list.range n)

end matrix

-- def A := cartan_matrix.G₂
-- def A := cartan_matrix.F₄
def A := cartan_matrix.E₈

#html h "div" [] [
  with_style "height" "200px" $
  with_style "width" "600px" $
  with_style "background" "grey" $
  h "svg" [] $ A.get_edges_html ++ A.get_nodes_html]