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 meant for examples and debugging, not proof scripts.

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 intentionally keep a single "inspect graph" panel: in practice this is the fastest way to sanity-check 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