TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

NN.Tensor.Internal.Syntax.Parser.Pack

Pack-pattern parsing #

This module parses the fixed axes surrounding a unique packed * axis and proves canonical rendering round trips. Fixed axes must be distinct names; numeric axes, underscores, groups, and ellipses are not part of this grammar. The parser does not check tensor shapes or unpacked component sizes.

source
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.

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

    Parse the separate pack and unpack pattern grammar.

    Instances For
      source
      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.