ShapeInfer

Shape inference / checking viewer for NN.IR.Graph.

TorchLean’s IR carries a declared outShape at each node. In practice, there are two common debugging questions when working with graphs:

• "Do the declared shapes match what the op semantics would infer from parent shapes?"
• "Where exactly did shape propagation fail, and what parent shapes caused it?"

This module provides a small infoview panel that answers those questions in a compact table.

Main command:

• #shape_infer_view g

Main definitions

• inferRows: perform sequential shape inference and collect row diagnostics.
• shapeInferHtml: render declared vs inferred shapes in a status table.
• #shape_infer_view: command entry point.

Implementation notes

• A per-node row model exposes inference and mismatch details directly.
• Inference stops after the first hard failure, and later rows are marked as "stopped"; this mirrors real debugging sessions where one upstream error explains many downstream unknowns.
• Status badges distinguish "mismatch" (inferred but different) from "error" (could not infer).

References

• ProofWidgets
• Lean community documentation style

Tags

shape-inference, ir, diagnostics, proofwidgets

def NN.Widgets.shapeInferHtml (g : IR.Graph) : ProofWidgets.Html

Render a per-node table comparing declared shapes vs inferred shapes for an IR graph.

Command

def NN.Widgets.shapeInferViewCmd : Lean.ParserDescr

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