Pack-pattern parsing

This module parses the fixed axes surrounding a unique packed * axis and proves canonical rendering round trips.

def TorchLean.Tensor.Internal.Syntax.Parser.Impl.parsePackTokens (policy : IdentifierPolicy) (whole : Span) : List Token → List (Located String) → Option Span → List (Located String) → List String → Result PackPattern

Parse the fixed axes before and after the unique packed * axis.

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

Parse the separate pack and unpack pattern grammar.

theorem TorchLean.Tensor.Internal.Syntax.parsePackPattern_render_eq_ok (source : String) (pattern : PackPattern) (hParse : parsePackPattern source = Except.ok pattern) : Except.map PackPattern.render (parsePackPattern pattern.render) = Except.ok pattern.render

Parsing a successful pack or unpack pattern's canonical rendering succeeds with the same ordered fixed axes and packed-segment boundary.

The reparsed pattern has fresh source spans. Comparing renderings intentionally ignores those diagnostic locations while preserving every syntactic choice used by pack and unpack checking.