Widgets IR

IR graph viewer widget (for debugging / teaching).

This module defines #ir_view g, which renders an NN.IR.Graph as an interactive HTML panel with:

• a well-formedness check result,
• a per-node expandable view,
• and a DOT snippet you can paste into GraphViz if needed.

Like other widgets, this is an inspection surface for examples and pass debugging. Proof scripts should cite the underlying graph definitions and theorems directly.

Main definitions

• irHtml: render checks, node details, and DOT text for one NN.IR.Graph.
• #ir_view: command frontend for interactive infoview inspection.

Implementation notes

• We keep a single "inspect graph" panel: in practice this is the fastest way to inspect graph structure during pass development.
• DOT preview is clipped on large graphs because huge text blocks make infoview interaction slow.
• Theme-aware badge styles are used so the panel remains readable in dark/light setups.

References

• ProofWidgets
• GraphViz DOT language
• Lean community documentation style

Tags

ir, graph, visualization, dot, proofwidgets

def NN.Widgets.irHtml (g : IR.Graph) (maxDotChars : ℕ := 6000) : ProofWidgets.Html

Render an IR graph as a rich HTML panel.

Commands

def NN.Widgets.irViewCmd : Lean.ParserDescr

def NN.Widgets.«command#ir_view_» : Lean.ParserDescr