Einsum-pattern parsing

This module parses comma-separated operands, the output expression, and their canonical rendering round trip. Empty operand expressions represent scalar tensors; leading, adjacent, and trailing commas therefore preserve empty operands. Dimension compatibility and supported axis forms belong to the einsum checker.

def TorchLean.Tensor.Internal.Syntax.Parser.Impl.splitCommas : List Token → List Token → List (List Token) → List (List Token)

Split at commas without discarding empty scalar-operand expressions.

def TorchLean.Tensor.Internal.Syntax.Parser.Impl.tokenListSpan (fallback : Span) : List Token → Span

Compute the smallest span covering a token list, or use the fallback when empty.

def TorchLean.Tensor.Internal.Syntax.Parser.Impl.parseEinsumInputs (policy : IdentifierPolicy) : List (List Token) → List Expression → Result (List Expression)

Parse comma-separated einsum operands in source order.

def TorchLean.Tensor.Internal.Syntax.parseEinsumPattern (source : String) (policy : IdentifierPolicy := IdentifierPolicy.pythonUnicode) : Result EinsumPattern

Parse an einsum pattern with one or more comma-separated input expressions.

theorem TorchLean.Tensor.Internal.Syntax.parseEinsumPattern_render_eq_ok (source : String) (pattern : EinsumPattern) (hParse : parseEinsumPattern source = Except.ok pattern) : Except.map EinsumPattern.render (parseEinsumPattern pattern.render) = Except.ok pattern.render

Parsing a successful einsum pattern's canonical rendering succeeds with the same canonical syntax.

The theorem applies to any number of input tensors. It preserves their order and comma boundaries, including empty expressions denoting scalar operands. Repeated labels and ellipses inside inputs are retained; only source locations and anonymous-axis occurrence offsets are intentionally refreshed.