proofwidget for game search trees

Stream: general

[Frederick Pu]

I'm trying to create a proofwidget for game search trees but i cant get the repulsion between nodes working

import ProofWidgets
import ProofWidgets.Data.Html

open ProofWidgets GraphDisplay Jsx Lean

def mkRect (attrs : Array (String × Json) := #[]) : Html :=
  <rect
    x={.num (-25)}
    y={.num (-100)}
    width={50}
    height={100}
    fill="var(--vscode-editor-background)"
    stroke="var(--vscode-editor-foreground)"
    strokeWidth={.num 1.5}
    {...attrs}
  />

/-- Create a single cell at absolute (x, y) coordinates -/
def mkCell (x y w h : Nat) (content : String) : Html :=
  Html.element "g" #[]
    #[
      -- rectangle background
      Html.element "rect"
        #[ ("x", .num x),
           ("y", .num y),
           ("width", .num w),
           ("height", .num h),
           ("fill", .str "var(--vscode-editor-background)"),
           ("stroke", .str "var(--vscode-editor-foreground)"),
           ("strokeWidth", .num 2) ]
        #[],
      -- text centered inside cell
      Html.element "text"
        #[ ("x", .num (x + w / 2)),
           ("y", .num (y + h / 2)),
           ("text-anchor", .str "middle"),
           ("dominant-baseline", .str "middle"),
           ("class", .str "font-code"),
           ("fill", .str "var(--vscode-editor-foreground)") ]
        #[ Html.text content ]
    ]


/-- Build the 2×3 grid using only for loops and get! -/
def mkGrid (grid : Array (Array String)) (cellW := 50) (cellH := 100) (spacing : Nat := 5) (attrs : Array (String × Json) := #[]) : Html := Id.run do
  let mut children : Array Html := #[]
  for rowIdx in [0: grid.size] do
    let row := grid.get! rowIdx
    for colIdx in [0: row.size] do
      let cell := row.get! colIdx
      children := children.push (mkCell (colIdx * (cellW + spacing)) (rowIdx * (cellH + spacing)) cellW cellH cell)

  -- total width and height of the grid
  let totalCols := if grid.size == 0 then 0 else grid.get! 0 |>.size
  let totalWidth := totalCols * (cellW + spacing) - spacing
  let totalHeight := grid.size * (cellH + spacing) - spacing

  -- wrap the cells in a <g> and shift so bottom middle is at (0,0)
  Html.element "g"
    (#[] ++ attrs ++
      #[ ("transform", .str s!"translate({-(totalWidth / 2 : Int)}, {-(totalHeight : Int) / 2})") ])
    children

/-- Single vertex containing the grid -/
def gridVertex : GraphDisplay.Vertex :=
  { id := "A"
    label := mkGrid #[ #["A", "."], #["B", "A"], #[".", "B"] ] 50 50,
    boundingShape := .rect 50 100
  }

/-- Single vertex containing the grid -/
def gridVertex1 : GraphDisplay.Vertex :=
  { id := "B"
    label := mkGrid #[ #["A", "."], #["B", "A"], #[".", "B"] ] 50 50,
    boundingShape := .rect 50 100
  }

/-- Single vertex containing the grid -/
def gridVertex2 : GraphDisplay.Vertex :=
  { id := "C"
    label := mkGrid #[ #["A", "."], #["B", "A"], #[".", "B"] ] 50 50,
    boundingShape := .rect 50 100
  }

#html mkGrid #[ #["A", "."], #["B", "A"], #[".", "B"] ]
def testGraph : GraphDisplay.Props :=
  { vertices := #[
      gridVertex,
      gridVertex1,
      gridVertex2
    ],
    edges := #[
      { source := "A", target := "B" },
      { source := "A", target := "C" }
    ]
    forces:=#[
        .link { distance? := Float.ofNat 50 },
        .collide { radius? := Float.ofNat 15 },
        .x { strength? := some 0.05 },
        .y { strength? := some 0.05 }
      ]
  }

#widget GraphDisplay with testGraph

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Could you say more about what effect you want to achieve? The nodes are quite large, so you may need to adjust the force parameters to get the desired effect. I get a reasonable behaviour with link distance 200 and collide radius 100. In this demo we set force parameters dynamically, based on node sizes.

[Frederick Pu]

i endedup just using d3 tree https://github.com/FrederickPu/ProofWidgetExperiments/blob/gametree/widget/src/gametree.tsx

[Frederick Pu]

im still having some issues displaying the proof search metadata for the bottom nodes tho, it seems like they're getting clipped