Canonical rendering of einops patterns

These functions serialize the existing syntax trees; there is no parallel pretty-printing AST. Rendering deliberately omits source spans and the source offset used to distinguish anonymous-axis occurrences. It preserves every syntactic choice that affects checking: axis order, parentheses, unit axes, ellipses, pack boundaries, and einsum operand boundaries.

Canonical output uses ASCII decimal notation for anonymous dimensions, retains named axes exactly (including Unicode), and follows the spacing rules of TokenKind.renderSequence.

def TorchLean.Tensor.Internal.Syntax.Axis.tokenKind : Axis → TokenKind

Convert one elementary axis to its canonical lexer token.

def TorchLean.Tensor.Internal.Syntax.Axis.render (axis : Axis) : String

Render one elementary axis without source-location metadata.

def TorchLean.Tensor.Internal.Syntax.CompositeAxis.tokenKinds (axis : CompositeAxis) : List TokenKind

Canonical token sequence for one top-level or parenthesized axis.

def TorchLean.Tensor.Internal.Syntax.CompositeAxis.render (axis : CompositeAxis) : String

Render one top-level axis, retaining parentheses even for empty or unary groups because grouping is part of the parsed syntax.

def TorchLean.Tensor.Internal.Syntax.Expression.tokenKinds (expression : Expression) : List TokenKind

Canonical lexer tokens for an expression, in axis order.

def TorchLean.Tensor.Internal.Syntax.Expression.render (expression : Expression) : String

Render one expression with exactly one space between top-level axes.

def TorchLean.Tensor.Internal.Syntax.TransformPattern.render (pattern : TransformPattern) : String

Render a rearrange, repeat, or reduce pattern in canonical form.

def TorchLean.Tensor.Internal.Syntax.PackPattern.render (pattern : PackPattern) : String

Render the unique packed segment together with its fixed surrounding axes.

def TorchLean.Tensor.Internal.Syntax.EinsumPattern.render (pattern : EinsumPattern) : String

Render all einsum operands and the requested output expression.