Einsum-pattern parsing

This module parses comma-separated operands, the output expression, and their canonical rendering round trip.

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

Split an einsum input token stream at top-level commas.

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.